--- 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';
--- 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'),
--- 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')])
+ ([], [], [], [])
[]
([], []);