diff --git a/src/CCL/Term.thy b/src/CCL/Term.thy --- a/src/CCL/Term.thy +++ b/src/CCL/Term.thy @@ -1,308 +1,308 @@ (* Title: CCL/Term.thy Author: Martin Coen Copyright 1993 University of Cambridge *) section \Definitions of usual program constructs in CCL\ theory Term imports CCL begin definition one :: "i" where "one == true" definition "if" :: "[i,i,i]\i" ("(3if _/ then _/ else _)" [0,0,60] 60) where "if b then t else u == case(b, t, u, \ x y. bot, \v. bot)" definition inl :: "i\i" where "inl(a) == " definition inr :: "i\i" where "inr(b) == " definition split :: "[i,[i,i]\i]\i" where "split(t,f) == case(t, bot, bot, f, \u. bot)" definition "when" :: "[i,i\i,i\i]\i" where "when(t,f,g) == split(t, \b x. if b then f(x) else g(x))" definition fst :: "i\i" where "fst(t) == split(t, \x y. x)" definition snd :: "i\i" where "snd(t) == split(t, \x y. y)" definition thd :: "i\i" where "thd(t) == split(t, \x p. split(p, \y z. z))" definition zero :: "i" where "zero == inl(one)" definition succ :: "i\i" where "succ(n) == inr(n)" definition ncase :: "[i,i,i\i]\i" where "ncase(n,b,c) == when(n, \x. b, \y. c(y))" definition "let1" :: "[i,i\i]\i" where let_def: "let1(t, f) == case(t,f(true),f(false), \x y. f(), \u. f(lam x. u(x)))" syntax "_let1" :: "[idt,i,i]\i" ("(3let _ be _/ in _)" [0,0,60] 60) translations "let x be a in e" == "CONST let1(a, \x. e)" definition letrec :: "[[i,i\i]\i,(i\i)\i]\i" where "letrec(h, b) == b(\x. fix(\f. lam x. h(x,\y. f`y))`x)" definition letrec2 :: "[[i,i,i\i\i]\i,(i\i\i)\i]\i" where "letrec2 (h, f) == letrec (\p g'. split(p,\x y. h(x,y,\u v. g'())), \g'. f(\x y. g'()))" definition letrec3 :: "[[i,i,i,i\i\i\i]\i,(i\i\i\i)\i]\i" where "letrec3 (h, f) == letrec (\p g'. split(p,\x xs. split(xs,\y z. h(x,y,z,\u v w. g'(>)))), \g'. f(\x y z. g'(>)))" syntax "_letrec" :: "[idt,idt,i,i]\i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) "_letrec2" :: "[idt,idt,idt,i,i]\i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) "_letrec3" :: "[idt,idt,idt,idt,i,i]\i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) parse_translation \ let fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; fun letrec_tr [f, x, a, b] = Syntax.const \<^const_syntax>\letrec\ $ abs_tr x (abs_tr f a) $ abs_tr f b; fun letrec2_tr [f, x, y, a, b] = Syntax.const \<^const_syntax>\letrec2\ $ abs_tr x (abs_tr y (abs_tr f a)) $ abs_tr f b; fun letrec3_tr [f, x, y, z, a, b] = Syntax.const \<^const_syntax>\letrec3\ $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b; in [(\<^syntax_const>\_letrec\, K letrec_tr), (\<^syntax_const>\_letrec2\, K letrec2_tr), (\<^syntax_const>\_letrec3\, K letrec3_tr)] end \ print_translation \ let val bound = Syntax_Trans.mark_bound_abs; fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] = let - val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b) - val (_,a'') = Syntax_Trans.variant_abs'(f,S,a) - val (x',a') = Syntax_Trans.variant_abs'(x,T,a'') + val (f',b') = Syntax_Trans.print_abs(ff,SS,b) + val (_,a'') = Syntax_Trans.print_abs(f,S,a) + val (x',a') = Syntax_Trans.print_abs(x,T,a'') in Syntax.const \<^syntax_const>\_letrec\ $ bound(f',SS) $ bound(x',T) $ a' $ b' end; fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] = let - val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b) - val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a) - val (y',a2) = Syntax_Trans.variant_abs'(y,U,a1) - val (x',a') = Syntax_Trans.variant_abs'(x,T,a2) + val (f',b') = Syntax_Trans.print_abs(ff,SS,b) + val ( _,a1) = Syntax_Trans.print_abs(f,S,a) + val (y',a2) = Syntax_Trans.print_abs(y,U,a1) + val (x',a') = Syntax_Trans.print_abs(x,T,a2) in Syntax.const \<^syntax_const>\_letrec2\ $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ a' $ b' end; fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] = let - val (f',b') = Syntax_Trans.variant_abs'(ff,SS,b) - val ( _,a1) = Syntax_Trans.variant_abs'(f,S,a) - val (z',a2) = Syntax_Trans.variant_abs'(z,V,a1) - val (y',a3) = Syntax_Trans.variant_abs'(y,U,a2) - val (x',a') = Syntax_Trans.variant_abs'(x,T,a3) + val (f',b') = Syntax_Trans.print_abs(ff,SS,b) + val ( _,a1) = Syntax_Trans.print_abs(f,S,a) + val (z',a2) = Syntax_Trans.print_abs(z,V,a1) + val (y',a3) = Syntax_Trans.print_abs(y,U,a2) + val (x',a') = Syntax_Trans.print_abs(x,T,a3) in Syntax.const \<^syntax_const>\_letrec3\ $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b' end; in [(\<^const_syntax>\letrec\, K letrec_tr'), (\<^const_syntax>\letrec2\, K letrec2_tr'), (\<^const_syntax>\letrec3\, K letrec3_tr')] end \ definition nrec :: "[i,i,[i,i]\i]\i" where "nrec(n,b,c) == letrec g x be ncase(x, b, \y. c(y,g(y))) in g(n)" definition nil :: "i" ("([])") where "[] == inl(one)" definition cons :: "[i,i]\i" (infixr "$" 80) where "h$t == inr()" definition lcase :: "[i,i,[i,i]\i]\i" where "lcase(l,b,c) == when(l, \x. b, \y. split(y,c))" definition lrec :: "[i,i,[i,i,i]\i]\i" where "lrec(l,b,c) == letrec g x be lcase(x, b, \h t. c(h,t,g(t))) in g(l)" definition napply :: "[i\i,i,i]\i" ("(_ ^ _ ` _)" [56,56,56] 56) where "f ^n` a == nrec(n,a,\x g. f(g))" lemmas simp_can_defs = one_def inl_def inr_def and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def lemmas simp_defs = simp_can_defs simp_ncan_defs lemmas ind_can_defs = zero_def succ_def nil_def cons_def and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def lemmas ind_defs = ind_can_defs ind_ncan_defs lemmas data_defs = simp_defs ind_defs napply_def and genrec_defs = letrec_def letrec2_def letrec3_def subsection \Beta Rules, including strictness\ lemma letB: "\ t=bot \ let x be t in f(x) = f(t)" apply (unfold let_def) apply (erule rev_mp) apply (rule_tac t = "t" in term_case) apply simp_all done lemma letBabot: "let x be bot in f(x) = bot" unfolding let_def by (rule caseBbot) lemma letBbbot: "let x be t in bot = bot" apply (unfold let_def) apply (rule_tac t = t in term_case) apply (rule caseBbot) apply simp_all done lemma applyB: "(lam x. b(x)) ` a = b(a)" by (simp add: apply_def) lemma applyBbot: "bot ` a = bot" unfolding apply_def by (rule caseBbot) lemma fixB: "fix(f) = f(fix(f))" apply (unfold fix_def) apply (rule applyB [THEN ssubst], rule refl) done lemma letrecB: "letrec g x be h(x,g) in g(a) = h(a,\y. letrec g x be h(x,g) in g(y))" apply (unfold letrec_def) apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl) done lemmas rawBs = caseBs applyB applyBbot method_setup beta_rl = \ Scan.succeed (fn ctxt => let val ctxt' = Context_Position.set_visible false ctxt in SIMPLE_METHOD' (CHANGED o simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))) end) \ lemma ifBtrue: "if true then t else u = t" and ifBfalse: "if false then t else u = u" and ifBbot: "if bot then t else u = bot" unfolding data_defs by beta_rl+ lemma whenBinl: "when(inl(a),t,u) = t(a)" and whenBinr: "when(inr(a),t,u) = u(a)" and whenBbot: "when(bot,t,u) = bot" unfolding data_defs by beta_rl+ lemma splitB: "split(,h) = h(a,b)" and splitBbot: "split(bot,h) = bot" unfolding data_defs by beta_rl+ lemma fstB: "fst() = a" and fstBbot: "fst(bot) = bot" unfolding data_defs by beta_rl+ lemma sndB: "snd() = b" and sndBbot: "snd(bot) = bot" unfolding data_defs by beta_rl+ lemma thdB: "thd(>) = c" and thdBbot: "thd(bot) = bot" unfolding data_defs by beta_rl+ lemma ncaseBzero: "ncase(zero,t,u) = t" and ncaseBsucc: "ncase(succ(n),t,u) = u(n)" and ncaseBbot: "ncase(bot,t,u) = bot" unfolding data_defs by beta_rl+ lemma nrecBzero: "nrec(zero,t,u) = t" and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))" and nrecBbot: "nrec(bot,t,u) = bot" unfolding data_defs by beta_rl+ lemma lcaseBnil: "lcase([],t,u) = t" and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)" and lcaseBbot: "lcase(bot,t,u) = bot" unfolding data_defs by beta_rl+ lemma lrecBnil: "lrec([],t,u) = t" and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))" and lrecBbot: "lrec(bot,t,u) = bot" unfolding data_defs by beta_rl+ lemma letrec2B: "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,\u v. letrec g x y be h(x,y,g) in g(u,v))" unfolding data_defs letrec2_def by beta_rl+ lemma letrec3B: "letrec g x y z be h(x,y,z,g) in g(p,q,r) = h(p,q,r,\u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))" unfolding data_defs letrec3_def by beta_rl+ lemma napplyBzero: "f^zero`a = a" and napplyBsucc: "f^succ(n)`a = f(f^n`a)" unfolding data_defs by beta_rl+ lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot napplyBzero napplyBsucc subsection \Constructors are injective\ lemma term_injs: "(inl(a) = inl(a')) \ (a=a')" "(inr(a) = inr(a')) \ (a=a')" "(succ(a) = succ(a')) \ (a=a')" "(a$b = a'$b') \ (a=a' \ b=b')" by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons) subsection \Constructors are distinct\ ML \ ML_Thms.bind_thms ("term_dstncts", mkall_dstnct_thms \<^context> @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs}) [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]); \ subsection \Rules for pre-order \[=\\ lemma term_porews: "inl(a) [= inl(a') \ a [= a'" "inr(b) [= inr(b') \ b [= b'" "succ(n) [= succ(n') \ n [= n'" "x$xs [= x'$xs' \ x [= x' \ xs [= xs'" by (simp_all add: data_defs ccl_porews) subsection \Rewriting and Proving\ ML \ ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs}); \ lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews lemmas [simp] = term_rews lemmas [elim!] = term_dstncts [THEN notE] lemmas [dest!] = term_injDs end diff --git a/src/Pure/Syntax/syntax_trans.ML b/src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML +++ b/src/Pure/Syntax/syntax_trans.ML @@ -1,502 +1,498 @@ (* Title: Pure/Syntax/syntax_trans.ML Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Syntax translation functions. *) signature BASIC_SYNTAX_TRANS = sig val eta_contract: bool Config.T end signature SYNTAX_TRANS = sig include BASIC_SYNTAX_TRANS val bracketsN: string val no_bracketsN: string val no_brackets: unit -> bool val type_bracketsN: string val no_type_bracketsN: string val no_type_brackets: unit -> bool val abs_tr: term list -> term val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term) val antiquote_tr: string -> term -> term val quote_tr: string -> term -> term val quote_antiquote_tr: string -> string -> string -> string * (Proof.context -> term list -> term) val non_typed_tr': (Proof.context -> term list -> term) -> Proof.context -> typ -> term list -> term val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val mark_bound_abs: string * typ -> term val mark_bound_body: string * typ -> term val bound_vars: (string * typ) list -> term -> term val abs_tr': Proof.context -> term -> term val atomic_abs_tr': string * typ * term -> term * term val const_abs_tr': term -> term val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term) val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term) val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term) - val variant_abs: string * typ * term -> string * term - val variant_abs': string * typ * term -> string * term + val print_abs: string * typ * term -> string * term val dependent_tr': string * string -> term list -> term val antiquote_tr': string -> term -> term val quote_tr': string -> term -> term val quote_antiquote_tr': string -> string -> string -> string * (Proof.context -> term list -> term) val update_name_tr': term -> term val get_idents: Proof.context -> {structs: string list, fixes: string list} val put_idents: {structs: string list, fixes: string list} -> Proof.context -> Proof.context val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list val pure_parse_translation: (string * (Proof.context -> term list -> term)) list val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list end; structure Syntax_Trans: SYNTAX_TRANS = struct structure Syntax = Lexicon.Syntax; (* print mode *) val bracketsN = "brackets"; val no_bracketsN = "no_brackets"; fun no_brackets () = find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (print_mode_value ()) = SOME no_bracketsN; val type_bracketsN = "type_brackets"; val no_type_bracketsN = "no_type_brackets"; fun no_type_brackets () = find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (print_mode_value ()) <> SOME type_bracketsN; (** parse (ast) translations **) (* strip_positions *) fun strip_positions_ast_tr [ast] = Ast.strip_positions ast | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts); (* constify *) fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] = Ast.Appl [c, constify_ast_tr [ast1], ast2] | constify_ast_tr [Ast.Variable c] = Ast.Constant c | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts); (* type syntax *) fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty] | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts); fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys) | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts); fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\<^type>fun" (Ast.unfold_ast "_types" dom, cod) | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts); (* application *) fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args) | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts); fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args) | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts); (* abstraction *) fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty] | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts); fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body) | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts); fun absfree_proper (x, T) t = if Name.is_internal x then error ("Illegal internal variable in abstraction: " ^ quote x) else absfree (x, T) t; fun abs_tr [Free x, t] = absfree_proper x t | abs_tr [Const ("_idtdummy", T), t] = absdummy T t | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT | abs_tr ts = raise TERM ("abs_tr", ts); (* binder *) fun mk_binder_tr (syn, name) = let fun err ts = raise TERM ("binder_tr: " ^ syn, ts) fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]] | binder_tr [x, t] = Syntax.const name $ (abs_tr [x, t] handle TERM _ => err [x, t]) | binder_tr ts = err ts; in (syn, fn _ => binder_tr) end; (* type propositions *) fun mk_type ty = Syntax.const "_constrain" $ Syntax.const "\<^const>Pure.type" $ (Syntax.const "\<^type>itself" $ ty); fun ofclass_tr [ty, cls] = cls $ mk_type ty | ofclass_tr ts = raise TERM ("ofclass_tr", ts); fun sort_constraint_tr [ty] = Syntax.const "\<^const>Pure.sort_constraint" $ mk_type ty | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts); (* meta propositions *) fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\<^type>prop" | aprop_tr ts = raise TERM ("aprop_tr", ts); (* meta implication *) fun bigimpl_ast_tr (asts as [asms, concl]) = let val prems = (case Ast.unfold_ast_p "_asms" asms of (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm'] | _ => raise Ast.AST ("bigimpl_ast_tr", asts)) in Ast.fold_ast_p "\<^const>Pure.imp" (prems, concl) end | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts); (* type/term reflection *) fun type_tr [ty] = mk_type ty | type_tr ts = raise TERM ("type_tr", ts); (* quote / antiquote *) fun antiquote_tr name = let fun tr i ((t as Const (c, _)) $ u) = if c = name then tr i u $ Bound i else tr i t $ tr i u | tr i (t $ u) = tr i t $ tr i u | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t) | tr _ a = a; in tr 0 end; fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t)); fun quote_antiquote_tr quoteN antiquoteN name = let fun tr [t] = Syntax.const name $ quote_tr antiquoteN t | tr ts = raise TERM ("quote_tr", ts); in (quoteN, fn _ => tr) end; (* corresponding updates *) fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) else list_comb (c $ update_name_tr [t] $ (Lexicon.fun_type $ (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts) | update_name_tr ts = raise TERM ("update_name_tr", ts); (* indexed syntax *) structure Idents = Proof_Data ( type T = {structs: string list, fixes: string list}; fun init _ : T = {structs = [], fixes = []}; ); val get_idents = Idents.get; val put_idents = Idents.put; fun indexdefault_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]] | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts); fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"] | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts); fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts; fun index_tr [t] = t | index_tr ts = raise TERM ("index_tr", ts); fun struct_tr ctxt [Const ("_indexdefault", _)] = (case #structs (get_idents ctxt) of x :: _ => Syntax.const (Lexicon.mark_fixed x) | _ => error "Illegal reference to implicit structure") | struct_tr _ ts = raise TERM ("struct_tr", ts); (** print (ast) translations **) (* types *) fun non_typed_tr' f ctxt _ ts = f ctxt ts; (* type syntax *) fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f]) | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f] | tappl_ast_tr' (f, ty :: tys) = Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f]; fun fun_ast_tr' asts = if no_brackets () orelse no_type_brackets () then raise Match else (case Ast.unfold_ast_p "\<^type>fun" (Ast.Appl (Ast.Constant "\<^type>fun" :: asts)) of (dom as _ :: _ :: _, cod) => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod] | _ => raise Match); (* application *) fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f]) | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args]; fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f]) | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args]; (* partial eta-contraction before printing *) fun eta_abs (Abs (a, T, t)) = (case eta_abs t of t' as Const ("_aprop", _) $ _ => Abs (a, T, t') | t' as f $ u => (case eta_abs u of Bound 0 => if Term.is_dependent f then Abs (a, T, t') else incr_boundvars ~1 f | _ => Abs (a, T, t')) | t' => Abs (a, T, t')) | eta_abs t = t; val eta_contract = Config.declare_option_bool ("eta_contract", \<^here>); fun eta_contr ctxt = Config.get ctxt eta_contract ? eta_abs; (* abstraction *) fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T); fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T); fun bound_vars vars body = subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body); fun strip_abss vars_of body_of tm = let val vars = vars_of tm; val body = body_of tm; val rev_new_vars = Term.rename_wrt_term body vars; fun subst (x, T) b = if Name.is_internal x andalso not (Term.is_dependent b) then (Const ("_idtdummy", T), incr_boundvars ~1 b) else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b)); val (rev_vars', body') = fold_map subst rev_new_vars body; in (rev rev_vars', body') end; fun abs_tr' ctxt tm = uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t)) (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); fun atomic_abs_tr' (x, T, t) = let val [xT] = Term.rename_wrt_term t [(x, T)] in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end; fun abs_ast_tr' asts = (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of ([], _) => raise Ast.AST ("abs_ast_tr'", asts) | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); fun const_abs_tr' t = (case eta_abs t of Abs (_, _, t') => if Term.is_dependent t' then raise Match else incr_boundvars ~1 t' | _ => raise Match); (* binders *) fun mk_binder_tr' (name, syn) = let fun mk_idts [] = raise Match (*abort translation*) | mk_idts [idt] = idt | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts; fun tr' t = let val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; in Syntax.const syn $ mk_idts xs $ bd end; fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts) | binder_tr' [] = raise Match; in (name, fn _ => binder_tr') end; fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts => let val (x, t) = atomic_abs_tr' abs in list_comb (Syntax.const syn $ x $ t, ts) end); fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts => let val (x, t) = atomic_abs_tr' abs in list_comb (Syntax.const syn $ x $ A $ t, ts) end); (* idtyp constraints *) fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] = Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs] | idtyp_ast_tr' _ _ = raise Match; (* meta implication *) fun impl_ast_tr' asts = if no_brackets () then raise Match else (case Ast.unfold_ast_p "\<^const>Pure.imp" (Ast.Appl (Ast.Constant "\<^const>Pure.imp" :: asts)) of (prems as _ :: _ :: _, concl) => let val (asms, asm) = split_last prems; val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]); in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end | _ => raise Match); (* dependent / nondependent quantifiers *) -fun var_abs mark (x, T, b) = +fun print_abs (x, T, b) = let val (x', _) = Name.variant x (Term.declare_term_names b Name.context) - in (x', subst_bound (mark (x', T), b)) end; - -val variant_abs = var_abs Free; -val variant_abs' = var_abs mark_bound_abs; + in (x', subst_bound (mark_bound_abs (x', T), b)) end; fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = if Term.is_dependent B then - let val (x', B') = variant_abs' (x, dummyT, B); + let val (x', B') = print_abs (x, dummyT, B); in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts) | dependent_tr' _ _ = raise Match; (* quote / antiquote *) fun antiquote_tr' name = let fun tr' i (t $ u) = if u aconv Bound i then Syntax.const name $ tr' i t else tr' i t $ tr' i u | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t) | tr' i a = if a aconv Bound i then raise Match else a; in tr' 0 end; fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t) | quote_tr' _ _ = raise Match; fun quote_antiquote_tr' quoteN antiquoteN name = let fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts) | tr' _ = raise Match; in (name, fn _ => tr') end; (* corresponding updates *) local fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T | upd_type _ = dummyT; fun upd_tr' (x_upd, T) = (case try (unsuffix "_update") x_upd of SOME x => (x, upd_type T) | NONE => raise Match); in fun update_name_tr' (Free x) = Free (upd_tr' x) | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x) | update_name_tr' (Const x) = Const (upd_tr' x) | update_name_tr' _ = raise Match; end; (* indexed syntax *) fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast | index_ast_tr' _ = raise Match; fun struct_ast_tr' ctxt [Ast.Constant "_indexdefault"] = (case #structs (get_idents ctxt) of x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x] | _ => raise Match) | struct_ast_tr' _ _ = raise Match; (** Pure translations **) val pure_parse_ast_translation = [("_strip_positions", fn _ => strip_positions_ast_tr), ("_constify", fn _ => constify_ast_tr), ("_tapp", fn _ => tapp_ast_tr), ("_tappl", fn _ => tappl_ast_tr), ("_bracket", fn _ => bracket_ast_tr), ("_appl", fn _ => appl_ast_tr), ("_applC", fn _ => applC_ast_tr), ("_lambda", fn _ => lambda_ast_tr), ("_idtyp", fn _ => idtyp_ast_tr), ("_bigimpl", fn _ => bigimpl_ast_tr), ("_indexdefault", fn _ => indexdefault_ast_tr), ("_indexvar", fn _ => indexvar_ast_tr), ("_struct", fn _ => struct_ast_tr)]; val pure_parse_translation = [("_abs", fn _ => abs_tr), ("_aprop", fn _ => aprop_tr), ("_ofclass", fn _ => ofclass_tr), ("_sort_constraint", fn _ => sort_constraint_tr), ("_TYPE", fn _ => type_tr), ("_update_name", fn _ => update_name_tr), ("_index", fn _ => index_tr), ("_struct", struct_tr)]; val pure_print_ast_translation = [("\<^type>fun", fn _ => fun_ast_tr'), ("_abs", fn _ => abs_ast_tr'), ("_idts", fn _ => idtyp_ast_tr' "_idts"), ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"), ("\<^const>Pure.imp", fn _ => impl_ast_tr'), ("_index", fn _ => index_ast_tr'), ("_struct", struct_ast_tr')]; end; structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans; open Basic_Syntax_Trans;