# HG changeset patch # User wenzelm # Date 1302119741 -7200 # Node ID 4821a2a91548f3aa7f1c7dfaa154b220c7de1ee7 # Parent 611856e8cb1e8130a09d528f17bf1ec1350eadb4 moved type syntax translations to syn_trans.ML; diff -r 611856e8cb1e -r 4821a2a91548 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Apr 06 18:36:28 2011 +0200 +++ b/src/Pure/Syntax/printer.ML Wed Apr 06 21:55:41 2011 +0200 @@ -180,7 +180,7 @@ (*default applications: prefix / postfix*) val appT = - if type_mode then Type_Ext.tappl_ast_tr' + if type_mode then Syn_Trans.tappl_ast_tr' else if curried then Syn_Trans.applC_ast_tr' else Syn_Trans.appl_ast_tr'; diff -r 611856e8cb1e -r 4821a2a91548 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Wed Apr 06 18:36:28 2011 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Wed Apr 06 21:55:41 2011 +0200 @@ -33,6 +33,8 @@ signature SYN_TRANS1 = sig include SYN_TRANS0 + val no_brackets: unit -> bool + val no_type_brackets: unit -> bool val non_typed_tr': (term list -> term) -> typ -> term list -> term val non_typed_tr'': ('a -> term list -> term) -> 'a -> typ -> term list -> term val constrainAbsC: string @@ -52,6 +54,7 @@ signature SYN_TRANS = sig include SYN_TRANS1 + val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val abs_tr': Proof.context -> term -> term val prop_tr': term -> term val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast @@ -61,6 +64,23 @@ structure Syn_Trans: SYN_TRANS = struct +(* 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 **) @@ -76,6 +96,18 @@ | 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) @@ -247,6 +279,22 @@ fun non_typed_tr'' f x _ ts = f x 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]) @@ -387,7 +435,7 @@ (* meta implication *) fun impl_ast_tr' (*"==>"*) asts = - if Type_Ext.no_brackets () then raise Match + if no_brackets () then raise Match else (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of (prems as _ :: _ :: _, concl) => @@ -484,6 +532,9 @@ val pure_trfuns = ([("_strip_positions", strip_positions_ast_tr), ("_constify", constify_ast_tr), + ("_tapp", tapp_ast_tr), + ("_tappl", tappl_ast_tr), + ("_bracket", bracket_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr), ("_lambda", lambda_ast_tr), @@ -503,7 +554,8 @@ ("_update_name", update_name_tr), ("_index", index_tr)], ([]: (string * (term list -> term)) list), - [("_abs", abs_ast_tr'), + [("\\<^type>fun", fun_ast_tr'), + ("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), ("_pttrns", idtyp_ast_tr' "_pttrns"), ("\\<^const>==>", impl_ast_tr'), diff -r 611856e8cb1e -r 4821a2a91548 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Apr 06 18:36:28 2011 +0200 +++ b/src/Pure/Syntax/type_ext.ML Wed Apr 06 21:55:41 2011 +0200 @@ -10,14 +10,11 @@ val is_position: term -> bool val strip_positions: term -> term val strip_positions_ast: Ast.ast -> Ast.ast - val no_brackets: unit -> bool - val no_type_brackets: unit -> bool end; signature TYPE_EXT = sig include TYPE_EXT0 - val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val type_ext: Syn_Ext.syn_ext end; @@ -52,53 +49,6 @@ (** the type 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 *) - -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); - - -(* print ast translations *) - -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' (*"\\<^type>fun"*) 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); - - -(* type_ext *) - fun typ c = Type (c, []); val class_nameT = typ "class_name"; @@ -135,9 +85,7 @@ Mfix ("'(_')", typeT --> typeT, "", [0], max_pri), Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)] ["_type_prop"] - (map Syn_Ext.mk_trfun - [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)], - [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')]) + ([], [], [], []) [] ([], []);