1.1 --- a/src/Pure/Syntax/syn_trans.ML Wed Jun 29 15:13:41 2005 +0200
1.2 +++ b/src/Pure/Syntax/syn_trans.ML Wed Jun 29 15:13:42 2005 +0200
1.3 @@ -21,6 +21,7 @@
1.4 val mark_bound: string -> term
1.5 val mark_boundT: string * typ -> term
1.6 val variant_abs': string * typ * term -> string * term
1.7 + exception TRANSLATION_FAIL of exn * string
1.8 end;
1.9
1.10 signature SYN_TRANS1 =
1.11 @@ -49,8 +50,10 @@
1.12 val prop_tr': term -> term
1.13 val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
1.14 val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
1.15 - val pts_to_asts: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree list -> Ast.ast list
1.16 - val asts_to_terms: (string -> (term list -> term) option) -> Ast.ast list -> term list
1.17 + val pts_to_asts: theory -> (string -> (theory -> Ast.ast list -> Ast.ast) option) ->
1.18 + Parser.parsetree list -> Ast.ast list
1.19 + val asts_to_terms: theory -> (string -> (theory -> term list -> term) option) ->
1.20 + Ast.ast list -> term list
1.21 end;
1.22
1.23 structure SynTrans: SYN_TRANS =
1.24 @@ -113,9 +116,7 @@
1.25
1.26 fun binder_tr (*sy*) [idts, body] = tr (idts, body)
1.27 | binder_tr (*sy*) ts = raise TERM ("binder_tr", ts);
1.28 - in
1.29 - (sy, binder_tr)
1.30 - end;
1.31 + in (sy, binder_tr) end;
1.32
1.33
1.34 (* meta propositions *)
1.35 @@ -131,15 +132,14 @@
1.36
1.37 (* meta implication *)
1.38
1.39 -fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
1.40 - Ast.fold_ast_p "==>" (Ast.unfold_ast2 "_asms" "_asm" asms, concl)
1.41 +fun bigimpl_ast_tr (*"_bigimpl"*) (asts as [asms, concl]) =
1.42 + let val prems =
1.43 + (case Ast.unfold_ast_p "_asms" asms of
1.44 + (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
1.45 + | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
1.46 + in Ast.fold_ast_p "==>" (prems, concl) end
1.47 | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
1.48
1.49 -(*
1.50 -fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
1.51 - Ast.fold_ast_p "==>" (Ast.unfold_ast "_asms" asms, concl)
1.52 - | bigimpl_ast_tr (*"_bigimpl"*) asts = raise Ast.AST ("bigimpl_ast_tr", asts);
1.53 -*)
1.54
1.55 (* type reflection *)
1.56
1.57 @@ -337,9 +337,7 @@
1.58 | tr' Ts (t as t1 $ t2) =
1.59 (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
1.60 then I else aprop) (tr' Ts t1 $ tr' Ts t2);
1.61 - in
1.62 - tr' [] tm
1.63 - end;
1.64 + in tr' [] tm end;
1.65
1.66 fun mk_ofclass_tr' show_sorts (*"_mk_ofclass"*) T [t] =
1.67 Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
1.68 @@ -352,19 +350,13 @@
1.69 if TypeExt.no_brackets () then raise Match
1.70 else
1.71 (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
1.72 - (asms as _ :: _ :: _, concl)
1.73 - => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast2 "_asms" "_asm" asms, concl]
1.74 + (prems as _ :: _ :: _, concl) =>
1.75 + let
1.76 + val (asms, asm) = split_last prems;
1.77 + val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
1.78 + in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
1.79 | _ => raise Match);
1.80
1.81 -(*
1.82 -fun impl_ast_tr' (*"==>"*) asts =
1.83 - if TypeExt.no_brackets () then raise Match
1.84 - else
1.85 - (case Ast.unfold_ast_p "==>" (Ast.Appl (Ast.Constant "==>" :: asts)) of
1.86 - (asms as _ :: _ :: _, concl)
1.87 - => Ast.Appl [Ast.Constant "_bigimpl", Ast.fold_ast "_asms" asms, concl]
1.88 - | _ => raise Match);
1.89 -*)
1.90
1.91 (* meta conjunction *)
1.92
1.93 @@ -432,7 +424,6 @@
1.94 [(case Lexicon.read_nat s of
1.95 SOME i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
1.96 | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
1.97 -;
1.98
1.99 fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
1.100 the_struct' structs "1"
1.101 @@ -467,14 +458,16 @@
1.102
1.103 (** pts_to_asts **)
1.104
1.105 -exception TRANSLATION of string * exn;
1.106 +exception TRANSLATION_FAIL of exn * string;
1.107
1.108 -fun pts_to_asts trf pts =
1.109 +fun pts_to_asts thy trf pts =
1.110 let
1.111 fun trans a args =
1.112 (case trf a of
1.113 NONE => Ast.mk_appl (Ast.Constant a) args
1.114 - | SOME f => f args handle exn => raise TRANSLATION (a, exn));
1.115 + | SOME f => transform_failure (fn exn =>
1.116 + TRANSLATION_FAIL (exn, "Error in parse ast translation for " ^ quote a))
1.117 + (fn () => f thy args) ());
1.118
1.119 (*translate pt bottom-up*)
1.120 fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
1.121 @@ -483,23 +476,20 @@
1.122 val exn_results = map (capture ast_of) pts;
1.123 val exns = List.mapPartial get_exn exn_results;
1.124 val results = List.mapPartial get_result exn_results
1.125 - in
1.126 - (case (results, exns) of
1.127 - ([], TRANSLATION (a, exn) :: _) =>
1.128 - (writeln ("Error in parse ast translation for " ^ quote a); raise exn)
1.129 - | _ => results)
1.130 - end;
1.131 + in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
1.132
1.133
1.134
1.135 (** asts_to_terms **)
1.136
1.137 -fun asts_to_terms trf asts =
1.138 +fun asts_to_terms thy trf asts =
1.139 let
1.140 fun trans a args =
1.141 (case trf a of
1.142 NONE => Term.list_comb (Lexicon.const a, args)
1.143 - | SOME f => f args handle exn => raise TRANSLATION (a, exn));
1.144 + | SOME f => transform_failure (fn exn =>
1.145 + TRANSLATION_FAIL (exn, "Error in parse translation for " ^ quote a))
1.146 + (fn () => f thy args) ());
1.147
1.148 fun term_of (Ast.Constant a) = trans a []
1.149 | term_of (Ast.Variable x) = Lexicon.read_var x
1.150 @@ -512,11 +502,6 @@
1.151 val exn_results = map (capture term_of) asts;
1.152 val exns = List.mapPartial get_exn exn_results;
1.153 val results = List.mapPartial get_result exn_results
1.154 - in
1.155 - (case (results, exns) of
1.156 - ([], TRANSLATION (a, exn) :: _) =>
1.157 - (writeln ("Error in parse translation for " ^ quote a); raise exn)
1.158 - | _ => results)
1.159 - end;
1.160 + in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
1.161
1.162 end;