--- a/NEWS Tue Apr 05 11:44:34 2011 +0200
+++ b/NEWS Tue Apr 05 15:15:33 2011 +0200
@@ -93,6 +93,10 @@
be disabled via the configuration option Syntax.positions, which is
called "syntax_positions" in Isar attribute syntax.
+* Discontinued special treatment of structure Ast: no pervasive
+content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to
+qualified names like Ast.Constant etc.
+
New in Isabelle2011 (January 2011)
--- a/doc-src/Classes/Thy/Setup.thy Tue Apr 05 11:44:34 2011 +0200
+++ b/doc-src/Classes/Thy/Setup.thy Tue Apr 05 15:15:33 2011 +0200
@@ -15,16 +15,16 @@
parse_ast_translation {*
let
- fun alpha_ast_tr [] = Syntax.Variable "'a"
- | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
+ fun alpha_ast_tr [] = Ast.Variable "'a"
+ | alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
fun alpha_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
- | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
- fun beta_ast_tr [] = Syntax.Variable "'b"
- | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+ Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
+ | alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
+ fun beta_ast_tr [] = Ast.Variable "'b"
+ | beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
fun beta_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
- | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
+ Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
+ | beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
in
[(@{syntax_const "_alpha"}, alpha_ast_tr),
(@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
--- a/src/HOL/HOLCF/Cfun.thy Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Tue Apr 05 15:15:33 2011 +0200
@@ -56,9 +56,9 @@
(* cf. Syntax.lambda_ast_tr from src/Pure/Syntax/syn_trans.ML *)
let
fun Lambda_ast_tr [pats, body] =
- Syntax.fold_ast_p @{syntax_const "_cabs"}
- (Syntax.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
- | Lambda_ast_tr asts = raise Syntax.AST ("Lambda_ast_tr", asts);
+ Ast.fold_ast_p @{syntax_const "_cabs"}
+ (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
+ | Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}
@@ -67,12 +67,12 @@
(* cf. Syntax.abs_ast_tr' from src/Pure/Syntax/syn_trans.ML *)
let
fun cabs_ast_tr' asts =
- (case Syntax.unfold_ast_p @{syntax_const "_cabs"}
- (Syntax.Appl (Syntax.Constant @{syntax_const "_cabs"} :: asts)) of
- ([], _) => raise Syntax.AST ("cabs_ast_tr'", asts)
- | (xs, body) => Syntax.Appl
- [Syntax.Constant @{syntax_const "_Lambda"},
- Syntax.fold_ast @{syntax_const "_cargs"} xs, body]);
+ (case Ast.unfold_ast_p @{syntax_const "_cabs"}
+ (Ast.Appl (Ast.Constant @{syntax_const "_cabs"} :: asts)) of
+ ([], _) => raise Ast.AST ("cabs_ast_tr'", asts)
+ | (xs, body) => Ast.Appl
+ [Ast.Constant @{syntax_const "_Lambda"},
+ Ast.fold_ast @{syntax_const "_cargs"} xs, body]);
in [(@{syntax_const "_cabs"}, cabs_ast_tr')] end
*}
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Apr 05 15:15:33 2011 +0200
@@ -442,16 +442,14 @@
(* define syntax for case combinator *)
(* TODO: re-implement case syntax using a parse translation *)
local
- open Syntax
fun syntax c = Syntax.mark_const (fst (dest_Const c))
fun xconst c = Long_Name.base_name (fst (dest_Const c))
- fun c_ast authentic con =
- Constant (if authentic then syntax con else xconst con)
+ fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
fun showint n = string_of_int (n+1)
- fun expvar n = Variable ("e" ^ showint n)
- fun argvar n (m, _) = Variable ("a" ^ showint n ^ "_" ^ showint m)
+ fun expvar n = Ast.Variable ("e" ^ showint n)
+ fun argvar n (m, _) = Ast.Variable ("a" ^ showint n ^ "_" ^ showint m)
fun argvars n args = map_index (argvar n) args
- fun app s (l, r) = mk_appl (Constant s) [l, r]
+ fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r]
val cabs = app "_cabs"
val capp = app @{const_syntax Rep_cfun}
val capps = Library.foldl capp
@@ -460,22 +458,21 @@
fun case1 authentic (n, c) =
app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
- fun when1 n (m, c) =
- if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
- val case_constant = Constant (syntax (case_const dummyT))
+ fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
+ val case_constant = Ast.Constant (syntax (case_const dummyT))
fun case_trans authentic =
- (if authentic then Parse_Print_Rule else Parse_Rule)
- (app "_case_syntax"
- (Variable "x",
- foldr1 (app "_case2") (map_index (case1 authentic) spec)),
- capp (capps (case_constant, map_index arg1 spec), Variable "x"))
+ (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+ (app "_case_syntax"
+ (Ast.Variable "x",
+ foldr1 (app "_case2") (map_index (case1 authentic) spec)),
+ capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
fun one_abscon_trans authentic (n, c) =
- (if authentic then Parse_Print_Rule else Parse_Rule)
- (cabs (con1 authentic n c, expvar n),
- capps (case_constant, map_index (when1 n) spec))
+ (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+ (cabs (con1 authentic n c, expvar n),
+ capps (case_constant, map_index (when1 n) spec))
fun abscon_trans authentic =
map_index (one_abscon_trans authentic) spec
- val trans_rules : ast Syntax.trrule list =
+ val trans_rules : Ast.ast Syntax.trrule list =
case_trans false :: case_trans true ::
abscon_trans false @ abscon_trans true
in
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Apr 05 15:15:33 2011 +0200
@@ -24,12 +24,13 @@
fun trans_rules name2 name1 n mx =
let
val vnames = Name.invents Name.context "a" n
- val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
+ val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
in
[Syntax.Parse_Print_Rule
- (Syntax.mk_appl (Constant name2) (map Variable vnames),
- fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
- vnames (Constant name1))] @
+ (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
+ fold (fn a => fn t =>
+ Ast.mk_appl (Ast.Constant @{const_syntax Rep_cfun}) [t, Ast.Variable a])
+ vnames (Ast.Constant name1))] @
(case mx of
Infix _ => [extra_parse_rule]
| Infixl _ => [extra_parse_rule]
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Apr 05 15:15:33 2011 +0200
@@ -497,33 +497,32 @@
(* syntax translations for pattern combinators *)
local
- open Syntax
fun syntax c = Syntax.mark_const (fst (dest_Const c));
- fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r];
+ fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
val capp = app @{const_syntax Rep_cfun};
val capps = Library.foldl capp
- fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"];
- fun app_pat x = Syntax.mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "_noargs"
+ fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"];
+ fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x];
+ fun args_list [] = Ast.Constant "_noargs"
| args_list xs = foldr1 (app "_args") xs;
fun one_case_trans (pat, (con, args)) =
let
- val cname = Constant (syntax con);
- val pname = Constant (syntax pat);
+ val cname = Ast.Constant (syntax con);
+ val pname = Ast.Constant (syntax pat);
val ns = 1 upto length args;
- val xs = map (fn n => Variable ("x"^(string_of_int n))) ns;
- val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
- val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
+ val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns;
+ val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns;
+ val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns;
in
- [Parse_Rule (app_pat (capps (cname, xs)),
- mk_appl pname (map app_pat xs)),
- Parse_Rule (app_var (capps (cname, xs)),
- app_var (args_list xs)),
- Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
- app "_match" (mk_appl pname ps, args_list vs))]
+ [Syntax.Parse_Rule (app_pat (capps (cname, xs)),
+ Ast.mk_appl pname (map app_pat xs)),
+ Syntax.Parse_Rule (app_var (capps (cname, xs)),
+ app_var (args_list xs)),
+ Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
+ app "_match" (Ast.mk_appl pname ps, args_list vs))]
end;
- val trans_rules : Syntax.ast Syntax.trrule list =
+ val trans_rules : Ast.ast Syntax.trrule list =
maps one_case_trans (pat_consts ~~ spec);
in
val thy = Sign.add_trrules trans_rules thy;
--- a/src/HOL/Import/hol4rews.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML Tue Apr 05 15:15:33 2011 +0200
@@ -610,10 +610,10 @@
end
local
- fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
- | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
- | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
+ fun handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "=="}, _],_,_]] = x
+ | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax all}, _],_]] = x
+ | handle_meta [x as Ast.Appl [Ast.Appl [Ast.Constant "_constrain", Ast.Constant @{const_syntax "==>"}, _],_,_]] = x
+ | handle_meta [x] = Ast.Appl [Ast.Constant @{const_syntax Trueprop}, x]
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]
--- a/src/HOL/Tools/string_syntax.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/HOL/Tools/string_syntax.ML Tue Apr 05 15:15:33 2011 +0200
@@ -16,10 +16,10 @@
(* nibble *)
val mk_nib =
- Syntax.Constant o Syntax.mark_const o
+ Ast.Constant o Syntax.mark_const o
fst o Term.dest_Const o HOLogic.mk_nibble;
-fun dest_nib (Syntax.Constant s) =
+fun dest_nib (Ast.Constant s) =
(case try Syntax.unmark_const s of
NONE => raise Match
| SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
@@ -29,7 +29,7 @@
fun mk_char s =
if Symbol.is_ascii s then
- Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
+ Ast.Appl [Ast.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
else error ("Non-ASCII symbol: " ^ quote s);
val specials = raw_explode "\\\"`'";
@@ -40,44 +40,42 @@
then c else raise Match
end;
-fun dest_char (Syntax.Appl [Syntax.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
+fun dest_char (Ast.Appl [Ast.Constant @{const_syntax Char}, c1, c2]) = dest_chr c1 c2
| dest_char _ = raise Match;
fun syntax_string cs =
- Syntax.Appl
- [Syntax.Constant @{syntax_const "_inner_string"},
- Syntax.Variable (Syntax.implode_xstr cs)];
+ Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
-fun char_ast_tr [Syntax.Variable xstr] =
- (case Syntax.explode_xstr xstr of
- [c] => mk_char c
- | _ => error ("Single character expected: " ^ xstr))
- | char_ast_tr asts = raise AST ("char_ast_tr", asts);
+fun char_ast_tr [Ast.Variable xstr] =
+ (case Syntax.explode_xstr xstr of
+ [c] => mk_char c
+ | _ => error ("Single character expected: " ^ xstr))
+ | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
fun char_ast_tr' [c1, c2] =
- Syntax.Appl [Syntax.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
+ Ast.Appl [Ast.Constant @{syntax_const "_Char"}, syntax_string [dest_chr c1 c2]]
| char_ast_tr' _ = raise Match;
(* string *)
-fun mk_string [] = Syntax.Constant @{const_syntax Nil}
+fun mk_string [] = Ast.Constant @{const_syntax Nil}
| mk_string (c :: cs) =
- Syntax.Appl [Syntax.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
+ Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
-fun string_ast_tr [Syntax.Variable xstr] =
- (case Syntax.explode_xstr xstr of
- [] =>
- Syntax.Appl
- [Syntax.Constant Syntax.constrainC,
- Syntax.Constant @{const_syntax Nil}, Syntax.Constant @{type_syntax string}]
- | cs => mk_string cs)
- | string_ast_tr asts = raise AST ("string_tr", asts);
+fun string_ast_tr [Ast.Variable xstr] =
+ (case Syntax.explode_xstr xstr of
+ [] =>
+ Ast.Appl
+ [Ast.Constant Syntax.constrainC,
+ Ast.Constant @{const_syntax Nil}, Ast.Constant @{type_syntax string}]
+ | cs => mk_string cs)
+ | string_ast_tr asts = raise Ast.AST ("string_tr", asts);
fun list_ast_tr' [args] =
- Syntax.Appl [Syntax.Constant @{syntax_const "_String"},
- syntax_string (map dest_char (Syntax.unfold_ast @{syntax_const "_args"} args))]
+ Ast.Appl [Ast.Constant @{syntax_const "_String"},
+ syntax_string (map dest_char (Ast.unfold_ast @{syntax_const "_args"} args))]
| list_ast_tr' ts = raise Match;
--- a/src/Pure/General/exn.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/General/exn.ML Tue Apr 05 15:15:33 2011 +0200
@@ -11,7 +11,9 @@
val get_exn: 'a result -> exn option
val capture: ('a -> 'b) -> 'a -> 'b result
val release: 'a result -> 'a
+ val flat_result: 'a result result -> 'a result
val map_result: ('a -> 'b) -> 'a result -> 'b result
+ val maps_result: ('a -> 'b result) -> 'a result -> 'b result
exception Interrupt
val interrupt: unit -> 'a
val is_interrupt: exn -> bool
@@ -45,8 +47,13 @@
fun release (Result y) = y
| release (Exn e) = reraise e;
+fun flat_result (Result x) = x
+ | flat_result (Exn e) = Exn e;
+
fun map_result f (Result x) = Result (f x)
- | map_result f (Exn e) = (Exn e);
+ | map_result f (Exn e) = Exn e;
+
+fun maps_result f = flat_result o map_result f;
(* interrupts *)
--- a/src/Pure/Isar/attrib.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Apr 05 15:15:33 2011 +0200
@@ -398,8 +398,8 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Syntax.ast_trace_raw #>
- register_config Syntax.ast_stat_raw #>
+ (register_config Ast.ast_trace_raw #>
+ register_config Ast.ast_stat_raw #>
register_config Syntax.positions_raw #>
register_config Syntax.show_brackets_raw #>
register_config Syntax.show_sorts_raw #>
--- a/src/Pure/Isar/isar_cmd.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Apr 05 15:15:33 2011 +0200
@@ -117,7 +117,7 @@
ML_Lex.read pos txt
|> ML_Context.expression pos
("val parse_ast_translation: (string * (" ^ advancedT a ^
- "Syntax.ast list -> Syntax.ast)) list")
+ "Ast.ast list -> Ast.ast)) list")
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
|> Context.theory_map;
@@ -141,7 +141,7 @@
ML_Lex.read pos txt
|> ML_Context.expression pos
("val print_ast_translation: (string * (" ^ advancedT a ^
- "Syntax.ast list -> Syntax.ast)) list")
+ "Ast.ast list -> Ast.ast)) list")
("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
|> Context.theory_map;
--- a/src/Pure/Isar/proof_context.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 15:15:33 2011 +0200
@@ -67,7 +67,8 @@
val check_tfree: Proof.context -> string * sort -> string * sort
val type_context: Proof.context -> Syntax.type_context
val term_context: Proof.context -> Syntax.term_context
- val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
+ val decode_term: Proof.context ->
+ Position.reports * term Exn.result -> Position.reports * term Exn.result
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
@@ -784,8 +785,8 @@
then default_root else c
| _ => default_root);
- fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
- handle ERROR msg => SOME msg;
+ fun check t = (Syntax.check_term ctxt (Type.constraint T' t); Exn.Result t)
+ handle exn as ERROR _ => Exn.Exn exn;
val t =
Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
root (syms, pos)
@@ -1092,12 +1093,12 @@
local
-fun const_ast_tr intern ctxt [Syntax.Variable c] =
+fun const_ast_tr intern ctxt [Ast.Variable c] =
let
val Const (c', _) = read_const_proper ctxt false c;
val d = if intern then Syntax.mark_const c' else c;
- in Syntax.Constant d end
- | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+ in Ast.Constant d end
+ | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
val typ = Simple_Syntax.read_typ;
--- a/src/Pure/Isar/runtime.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Isar/runtime.ML Tue Apr 05 15:15:33 2011 +0200
@@ -72,9 +72,9 @@
| Fail msg => [raised exn "Fail" [msg]]
| THEORY (msg, thys) =>
[raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
- | Syntax.AST (msg, asts) =>
+ | Ast.AST (msg, asts) =>
[raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+ (if detailed then map (Pretty.string_of o Ast.pretty_ast) asts else []))]
| TYPE (msg, Ts, ts) =>
[raised exn "TYPE" (msg ::
(if detailed then
--- a/src/Pure/Proof/proof_syntax.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Apr 05 15:15:33 2011 +0200
@@ -71,17 +71,20 @@
|> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
- [(Syntax.mk_appl (Constant "_Lam")
- [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
- Syntax.mk_appl (Constant "_Lam")
- [Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
- (Syntax.mk_appl (Constant "_Lam")
- [Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
- Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
- (Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
- (Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
- Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
- [(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
+ [(Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam0")
+ [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.Variable "l",
+ Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
+ (Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam1")
+ [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
+ Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
+ (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
+ (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
+ [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
(**** translation between proof terms and pure terms ****)
--- a/src/Pure/Syntax/ast.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Syntax/ast.ML Tue Apr 05 15:15:33 2011 +0200
@@ -4,21 +4,18 @@
Abstract syntax trees, translation rules, matching and normalization of asts.
*)
-signature AST0 =
+signature AST =
sig
datatype ast =
Constant of string |
Variable of string |
Appl of ast list
+ val mk_appl: ast -> ast list -> ast
exception AST of string * ast list
-end;
-
-signature AST1 =
-sig
- include AST0
- val mk_appl: ast -> ast list -> ast
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
+ val head_of_rule: ast * ast -> string
+ val rule_error: ast * ast -> string option
val fold_ast: string -> ast list -> ast
val fold_ast_p: string -> ast list * ast -> ast
val unfold_ast: string -> ast -> ast list
@@ -27,17 +24,10 @@
val ast_trace: bool Config.T
val ast_stat_raw: Config.raw
val ast_stat: bool Config.T
-end;
-
-signature AST =
-sig
- include AST1
- val head_of_rule: ast * ast -> string
- val rule_error: ast * ast -> string option
val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
end;
-structure Ast : AST =
+structure Ast: AST =
struct
(** abstract syntax trees **)
@@ -53,16 +43,12 @@
Variable of string | (*x, ?x, 'a, ?'a*)
Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
-
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
there are no empty asts or nullary applications; use mk_appl for convenience*)
-
fun mk_appl f [] = f
| mk_appl f args = Appl (f :: args);
-
(*exception for system errors involving asts*)
-
exception AST of string * ast list;
--- a/src/Pure/Syntax/parser.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Apr 05 15:15:33 2011 +0200
@@ -9,7 +9,6 @@
type gram
val empty_gram: gram
val extend_gram: Syn_Ext.xprod list -> gram -> gram
- val make_gram: Syn_Ext.xprod list -> gram
val merge_gram: gram * gram -> gram
val pretty_gram: gram -> Pretty.T list
datatype parsetree =
@@ -54,6 +53,8 @@
lambda productions are stored as normal productions
and also as an entry in "lambdas"*)
+val union_token = union Lexicon.matching_tokens;
+val subtract_token = subtract Lexicon.matching_tokens;
(*productions for which no starting token is
known yet are associated with this token*)
@@ -119,14 +120,14 @@
if forall
(fn Nonterminal (id, _) => member (op =) lambdas' id
| Terminal _ => false) rhs
- then (true, union (op =) lambdas' (connected_with chains' [lhs] [lhs]))
+ then (true, union (op =) (connected_with chains' [lhs] [lhs]) lambdas')
else (false, lambdas');
(*list optional terminal and all nonterminals on which the lookahead
of a production depends*)
fun lookahead_dependency _ [] nts = (NONE, nts)
- | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
- | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
+ | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts)
+ | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts =
if member (op =) lambdas nt then
lookahead_dependency lambdas symbs (nt :: nts)
else (NONE, nt :: nts);
@@ -134,13 +135,11 @@
(*get all known starting tokens for a nonterminal*)
fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
- val token_union = uncurry (union Lexicon.matching_tokens);
-
(*update prods, lookaheads, and lambdas according to new lambda NTs*)
val (added_starts', lambdas') =
let
(*propagate added lambda NT*)
- fun propagate_lambda [] added_starts lambdas= (added_starts, lambdas)
+ fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas)
| propagate_lambda (l :: ls) added_starts lambdas =
let
(*get lookahead for lambda NT*)
@@ -156,11 +155,12 @@
let
val new_lambda = is_none tk andalso subset (op =) (nts, lambdas);
- val new_tks = subtract (op =) l_starts
- ((if is_some tk then [the tk] else []) @
- Library.foldl token_union ([], map starts_for_nt nts));
+ val new_tks =
+ (if is_some tk then [the tk] else [])
+ |> fold (union_token o starts_for_nt) nts
+ |> subtract (op =) l_starts;
- val added_tks' = token_union (new_tks, added_tks);
+ val added_tks' = union_token added_tks new_tks;
val nt_dependencies' = union (op =) nts nt_dependencies;
@@ -244,9 +244,8 @@
val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
val start_tks =
- Library.foldl token_union
- (if is_some start_tk then [the start_tk] else [],
- map starts_for_nt start_nts);
+ (if is_some start_tk then [the start_tk] else [])
+ |> fold (union_token o starts_for_nt) start_nts;
val opt_starts =
(if new_lambda then [NONE]
@@ -256,10 +255,10 @@
(*add lhs NT to list of dependent NTs in lookahead*)
fun add_nts [] = ()
| add_nts (nt :: nts) =
- let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
- if member (op =) old_nts lhs then ()
- else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
- end;
+ let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+ if member (op =) old_nts lhs then ()
+ else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
+ end;
(*add new start tokens to chained NTs' lookahead list;
also store new production for lhs NT*)
@@ -268,7 +267,7 @@
let
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- val new_tks = subtract Lexicon.matching_tokens old_tks start_tks;
+ val new_tks = subtract_token old_tks start_tks;
(*store new production*)
fun store [] prods is_new =
@@ -288,8 +287,10 @@
else (new_prod :: tk_prods, true)
else (new_prod :: tk_prods, true);
- val prods' = prods
- |> is_new' ? AList.update (op =) (tk: Lexicon.token option, tk_prods');
+ val prods' =
+ if is_new' then
+ AList.update (op =) (tk: Lexicon.token option, tk_prods') prods
+ else prods;
in store tks prods' (is_new orelse is_new') end;
val (nt_prods', prod_count', changed) =
@@ -375,17 +376,18 @@
(*associate productions with new lookahead tokens*)
val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods);
- val nt_prods' =
- nt_prods'
- |> (key = SOME unknown_start) ? AList.update (op =) (key, tk_prods');
+ val nt_prods'' =
+ if key = SOME unknown_start then
+ AList.update (op =) (key, tk_prods') nt_prods'
+ else nt_prods';
- val added_tks = subtract Lexicon.matching_tokens old_tks new_tks;
+ val added_tks = subtract_token old_tks new_tks;
in
if null added_tks then
- (Array.update (prods, nt, (lookahead, nt_prods'));
+ (Array.update (prods, nt, (lookahead, nt_prods''));
process_nts nts added)
else
- (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods'));
+ (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods''));
process_nts nts ((nt, added_tks) :: added))
end;
@@ -422,13 +424,14 @@
fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1);
val nt_prods =
- Library.foldl (uncurry (union (op =))) ([], map snd (snd (Vector.sub (prods, tag)))) @
- map prod_of_chain (these (AList.lookup (op =) chains tag));
+ fold (union (op =) o snd) (snd (Vector.sub (prods, tag))) [] @
+ map prod_of_chain (these (AList.lookup (op =) chains tag));
in map (pretty_prod name) nt_prods end;
in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end;
+
(** Operations on gramars **)
val empty_gram =
@@ -465,10 +468,10 @@
delimiters and predefined terms are stored as terminals,
nonterminals are converted to integer tags*)
fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
- | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result =
+ | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result =
symb_of ss nt_count tags
(Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
- | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result =
+ | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result =
let
val (nt_count', tags', new_symb) =
(case Lexicon.predef_term s of
@@ -482,7 +485,7 @@
(*Convert list of productions by invoking symb_of for each of them*)
fun prod_of [] nt_count prod_count tags result =
(nt_count, prod_count, tags, result)
- | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps)
+ | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
nt_count prod_count tags result =
let
val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
@@ -522,8 +525,6 @@
prods = Array.vector prods'}
end;
-fun make_gram xprods = extend_gram xprods empty_gram;
-
(*Merge two grammars*)
fun merge_gram (gram_a, gram_b) =
@@ -551,15 +552,14 @@
val ((nt_count1', tags1'), tag_table) =
let
- val tag_list = Symtab.dest tags2;
-
val table = Array.array (nt_count2, ~1);
+ fun the_nt tag =
+ the (Symtab.get_first (fn (n, t) => if t = tag then SOME n else NONE) tags2);
fun store_tag nt_count tags ~1 = (nt_count, tags)
| store_tag nt_count tags tag =
let
- val (nt_count', tags', tag') =
- get_tag nt_count tags (fst (the (find_first (fn (n, t) => t = tag) tag_list)));
+ val (nt_count', tags', tag') = get_tag nt_count tags (the_nt tag);
val _ = Array.update (table, tag, tag');
in store_tag nt_count' tags' (tag - 1) end;
in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end;
@@ -584,8 +584,7 @@
fun process_nt ~1 result = result
| process_nt nt result =
let
- val nt_prods = Library.foldl (uncurry (union (op =)))
- ([], map snd (snd (Vector.sub (prods2, nt))));
+ val nt_prods = fold (union (op =) o snd) (snd (Vector.sub (prods2, nt))) [];
val lhs_tag = convert_tag nt;
(*convert tags in rhs*)
@@ -627,6 +626,7 @@
end;
+
(** Parser **)
datatype parsetree =
@@ -647,11 +647,11 @@
(*Get all rhss with precedence >= min_prec*)
-fun get_RHS min_prec = filter (fn (_, _, prec:int) => prec >= min_prec);
+fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec);
(*Get all rhss with precedence >= min_prec and < max_prec*)
fun get_RHS' min_prec max_prec =
- filter (fn (_, _, prec:int) => prec >= min_prec andalso prec < max_prec);
+ filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec);
(*Make states using a list of rhss*)
fun mk_states i min_prec lhs_ID rhss =
@@ -660,7 +660,7 @@
(*Add parse tree to list and eliminate duplicates
saving the maximum precedence*)
-fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)])
+fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)])
| conc (t, prec) ((t', prec') :: ts) =
if t = t' then
(SOME prec',
@@ -671,33 +671,25 @@
in (n, (t', prec') :: ts') end;
(*Update entry in used*)
-fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) =
- if A = B then
- let val (n, ts') = conc t ts
- in ((A, (i, ts')) :: used, n) end
- else
- let val (used', n) = update_trees used (A, t)
- in ((B, (i, ts)) :: used', n) end;
+fun update_trees (A, t) used =
+ let
+ val (i, ts) = the (Inttab.lookup used A);
+ val (n, ts') = conc t ts;
+ in (n, Inttab.update (A, (i, ts')) used) end;
(*Replace entry in used*)
-fun update_prec (A: nt_tag, prec) used =
- let
- fun update ((hd as (B, (_, ts))) :: used, used') =
- if A = B
- then used' @ ((A, (prec, ts)) :: used)
- else update (used, hd :: used')
- in update (used, []) end;
+fun update_prec (A, prec) =
+ Inttab.map_entry A (fn (_, ts) => (prec, ts));
-fun getS A max_prec Si =
- filter
- (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
- | _ => false) Si;
-
-fun getS' A max_prec min_prec Si =
- filter
- (fn (_, _, _, Nonterminal (B, prec) :: _, _, _)
- => A = B andalso prec > min_prec andalso prec <= max_prec
- | _ => false) Si;
+fun getS A max_prec NONE Si =
+ filter
+ (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec
+ | _ => false) Si
+ | getS A max_prec (SOME min_prec) Si =
+ filter
+ (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) =>
+ A = B andalso prec > min_prec andalso prec <= max_prec
+ | _ => false) Si;
fun get_states Estate i ii A max_prec =
filter
@@ -706,19 +698,17 @@
(Array.sub (Estate, ii));
-fun movedot_term (A, j, ts, Terminal a :: sa, id, i) c =
- if Lexicon.valued_token c then (A, j, ts @ [Tip c], sa, id, i)
+fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
+ if Lexicon.valued_token c then (A, j, Tip c :: ts, sa, id, i)
else (A, j, ts, sa, id, i);
-fun movedot_nonterm ts (A, j, tss, Nonterminal _ :: sa, id, i) =
- (A, j, tss @ ts, sa, id, i);
+fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) =
+ (A, j, List.revAppend (tt, ts), sa, id, i);
-fun movedot_lambda _ [] = []
- | movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ((t, ki) :: ts) =
- if k <= ki then
- (B, j, tss @ t, sa, id, i) ::
- movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts
- else movedot_lambda (B, j, tss, Nonterminal (A, k) :: sa, id, i) ts;
+fun movedot_lambda [] _ = []
+ | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) =
+ if k <= ki then (B, j, List.revAppend (t, tss), sa, id, i) :: movedot_lambda ts state
+ else movedot_lambda ts state;
(*trigger value for warnings*)
@@ -741,7 +731,7 @@
fun get_prods [] result = result
| get_prods (nt :: nts) result =
let val nt_prods = snd (Vector.sub (prods, nt));
- in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
+ in get_prods nts (token_assoc (nt_prods, tk) @ result) end;
in get_prods (connected_with chains nts nts) [] end;
@@ -755,30 +745,26 @@
(_, _, _, Nonterminal (nt, min_prec) :: _, _, _) =>
let (*predictor operation*)
val (used', new_states) =
- (case AList.lookup (op =) used nt of
+ (case Inttab.lookup used nt of
SOME (used_prec, l) => (*nonterminal has been processed*)
if used_prec <= min_prec then
(*wanted precedence has been processed*)
- (used, movedot_lambda S l)
+ (used, movedot_lambda l S)
else (*wanted precedence hasn't been parsed yet*)
let
val tk_prods = all_prods_for nt;
-
- val States' = mk_states i min_prec nt
- (get_RHS' min_prec used_prec tk_prods);
- in (update_prec (nt, min_prec) used,
- movedot_lambda S l @ States')
- end
-
+ val States' =
+ mk_states i min_prec nt (get_RHS' min_prec used_prec tk_prods);
+ in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end
| NONE => (*nonterminal is parsed for the first time*)
let
val tk_prods = all_prods_for nt;
val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
- in ((nt, (min_prec, [])) :: used, States') end);
+ in (Inttab.update (nt, (min_prec, [])) used, States') end);
- val dummy =
+ val _ =
if not (! warned) andalso
- length (new_states @ States) > Config.get ctxt branching_level then
+ length new_states + length States > Config.get ctxt branching_level then
(Context_Position.if_visible ctxt warning
"Currently parsed expression could be extremely ambiguous";
warned := true)
@@ -789,32 +775,20 @@
| (_, _, _, Terminal a :: _, _, _) => (*scanner operation*)
processS used States
(S :: Si,
- if Lexicon.matching_tokens (a, c) then movedot_term S c :: Sii else Sii)
+ if Lexicon.matching_tokens (a, c) then movedot_term c S :: Sii else Sii)
| (A, prec, ts, [], id, j) => (*completer operation*)
- let val tt = if id = "" then ts else [Node (id, ts)] in
+ let val tt = if id = "" then ts else [Node (id, rev ts)] in
if j = i then (*lambda production?*)
let
- val (used', O) = update_trees used (A, (tt, prec));
- in
- (case O of
- NONE =>
- let
- val Slist = getS A prec Si;
- val States' = map (movedot_nonterm tt) Slist;
- in processS used' (States' @ States) (S :: Si, Sii) end
- | SOME n =>
- if n >= prec then processS used' States (S :: Si, Sii)
- else
- let
- val Slist = getS' A prec n Si;
- val States' = map (movedot_nonterm tt) Slist;
- in processS used' (States' @ States) (S :: Si, Sii) end)
- end
+ val (prec', used') = update_trees (A, (tt, prec)) used;
+ val Slist = getS A prec prec' Si;
+ val States' = map (movedot_nonterm tt) Slist;
+ in processS used' (States' @ States) (S :: Si, Sii) end
else
let val Slist = get_states Estate i j A prec
in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end
end)
- in processS [] states ([], []) end;
+ in processS Inttab.empty states ([], []) end;
fun produce ctxt warned prods tags chains stateset i indata prev_token =
@@ -832,16 +806,16 @@
end
| s =>
(case indata of
- [] => Array.sub (stateset, i)
- | c :: cs =>
- let val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
- in Array.update (stateset, i, si);
- Array.update (stateset, i + 1, sii);
- produce ctxt warned prods tags chains stateset (i + 1) cs c
- end));
+ [] => s
+ | c :: cs =>
+ let
+ val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+ val _ = Array.update (stateset, i, si);
+ val _ = Array.update (stateset, i + 1, sii);
+ in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
-fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l;
+fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
fun earley ctxt prods tags chains startsymbol indata =
let
--- a/src/Pure/Syntax/syn_trans.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Apr 05 15:15:33 2011 +0200
@@ -60,7 +60,7 @@
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val parsetree_to_ast: Proof.context -> type_context -> bool ->
(string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
- Parser.parsetree -> Position.reports * Ast.ast
+ Parser.parsetree -> Position.reports * Ast.ast Exn.result
val ast_to_term: Proof.context ->
(string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
end;
@@ -587,7 +587,7 @@
| ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
| ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
- val ast = ast_of parsetree;
+ val ast = Exn.interruptible_capture ast_of parsetree;
in (! reports, ast) end;
--- a/src/Pure/Syntax/syntax.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 15:15:33 2011 +0200
@@ -7,7 +7,6 @@
signature BASIC_SYNTAX =
sig
- include AST0
include SYN_TRANS0
include MIXFIX0
include PRINTER0
@@ -15,7 +14,6 @@
signature SYNTAX =
sig
- include AST1
include LEXICON0
include SYN_EXT0
include TYPE_EXT0
@@ -116,44 +114,44 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
- val standard_parse_term: (term -> string option) ->
+ val standard_parse_sort: Proof.context -> type_context -> syntax ->
+ Symbol_Pos.T list * Position.T -> sort
+ val standard_parse_typ: Proof.context -> type_context -> syntax ->
+ ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+ val standard_parse_term: (term -> term Exn.result) ->
Proof.context -> type_context -> term_context -> syntax ->
string -> Symbol_Pos.T list * Position.T -> term
- val standard_parse_typ: Proof.context -> type_context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> type_context -> syntax ->
- Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
Parse_Rule of 'a * 'a |
Print_Rule of 'a * 'a |
Parse_Print_Rule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
+ val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> Ast.ast
+ val standard_unparse_sort: {extern_class: string -> xstring} ->
+ Proof.context -> syntax -> sort -> Pretty.T
+ val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> syntax -> typ -> Pretty.T
val standard_unparse_term: {structs: string list, fixes: string list} ->
{extern_class: string -> xstring, extern_type: string -> xstring,
extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
- val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
- Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_sort: {extern_class: string -> xstring} ->
- Proof.context -> syntax -> sort -> Pretty.T
val update_trfuns:
- (string * ((ast list -> ast) * stamp)) list *
+ (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
(string * ((bool -> typ -> term list -> term) * stamp)) list *
- (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
+ (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
val update_advanced_trfuns:
- (string * ((Proof.context -> ast list -> ast) * stamp)) list *
+ (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
- (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
+ (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
syntax -> syntax
val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
val update_const_gram: bool -> (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_trrules: ast trrule list -> syntax -> syntax
- val remove_trrules: ast trrule list -> syntax -> syntax
+ val update_trrules: Ast.ast trrule list -> syntax -> syntax
+ val remove_trrules: Ast.ast trrule list -> syntax -> syntax
end;
structure Syntax: SYNTAX =
@@ -562,7 +560,7 @@
Syntax
({input = input',
lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
- gram = if changed then Parser.make_gram input' else gram,
+ gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram,
consts = consts,
prmodes = prmodes,
parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
@@ -686,17 +684,9 @@
-(** read **)
+(** read **) (* FIXME rename!? *)
-fun some_results f xs =
- let
- val exn_results = map (Exn.interruptible_capture f) xs;
- val exns = map_filter Exn.get_exn exn_results;
- val results = map_filter Exn.get_result exn_results;
- in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
-
-
-(* read_ast *)
+(* configuration options *)
val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
val positions = Config.bool positions_raw;
@@ -712,6 +702,23 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
+
+(* results *)
+
+fun proper_results results = map_filter (fn (y, Exn.Result x) => SOME (y, x) | _ => NONE) results;
+fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
+
+fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
+
+fun report_result ctxt pos results =
+ (case (proper_results results, failed_results results) of
+ ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
+ | ([(reports, x)], _) => (report ctxt reports; x)
+ | _ => error (ambiguity_msg pos));
+
+
+(* read_asts *)
+
fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
let
val {lexicon, gram, parse_ast_trtab, ...} = tabs;
@@ -736,84 +743,87 @@
map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
val constrain_pos = not raw andalso Config.get ctxt positions;
- in
- some_results
- (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
- end;
+ val parsetree_to_ast =
+ Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab);
+ in map parsetree_to_ast pts end;
-(* read *)
+(* read_raw *)
-fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
- let val {parse_ruletab, parse_trtab, ...} = tabs in
- read_asts ctxt type_ctxt syn false root inp
- |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
- |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
+fun read_raw ctxt type_ctxt (syn as Syntax (tabs, _)) root input =
+ let
+ val {parse_ruletab, parse_trtab, ...} = tabs;
+ val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
+ val ast_to_term = Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab);
+ in
+ read_asts ctxt type_ctxt syn false root input
+ |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
end;
-(* read terms *)
-
-fun report_result ctxt (reports, res) =
- (List.app (fn (pos, m) => Context_Position.report ctxt pos m) reports; res);
-
-(*brute-force disambiguation via type-inference*)
-fun disambig ctxt _ [arg] = report_result ctxt arg
- | disambig ctxt check args =
- let
- val level = Config.get ctxt ambiguity_level;
- val limit = Config.get ctxt ambiguity_limit;
-
- val ambiguity = length args;
- fun ambig_msg () =
- if ambiguity > 1 andalso ambiguity <= level then
- "Got more than one parse tree.\n\
- \Retry with smaller syntax_ambiguity_level for more information."
- else "";
+(* read sorts *)
- val errs = Par_List.map_name "Syntax.disambig" (check o snd) args;
- val results = map_filter (fn (arg, NONE) => SOME arg | _ => NONE) (args ~~ errs);
- val len = length results;
-
- val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
- in
- if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
- else if len = 1 then
- (if ambiguity > level then
- Context_Position.if_visible ctxt warning
- "Fortunately, only one parse tree is type correct.\n\
- \You may still want to disambiguate your grammar or your input."
- else (); report_result ctxt (hd results))
- else cat_error (ambig_msg ()) (cat_lines
- (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (show_term o snd) (take limit results)))
- end;
-
-fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
- read ctxt type_ctxt syn root (syms, pos)
- |> map (Type_Ext.decode_term term_ctxt)
- |> disambig ctxt check;
+fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
+ read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos)
+ |> report_result ctxt pos
+ |> Type_Ext.sort_of_term;
(* read types *)
fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
- (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
- [res] =>
- let val t = report_result ctxt res
- in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
- | _ => error (ambiguity_msg pos));
+ read_raw ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos)
+ |> report_result ctxt pos
+ |> (fn t => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t);
-(* read sorts *)
+(* read terms -- brute-force disambiguation via type-inference *)
+
+fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
+ let
+ val results =
+ read_raw ctxt type_ctxt syn root (syms, pos)
+ |> map (Type_Ext.decode_term term_ctxt);
+
+ val level = Config.get ctxt ambiguity_level;
+ val limit = Config.get ctxt ambiguity_limit;
+
+ val ambiguity = length (proper_results results);
+
+ fun ambig_msg () =
+ if ambiguity > 1 andalso ambiguity <= level then
+ "Got more than one parse tree.\n\
+ \Retry with smaller syntax_ambiguity_level for more information."
+ else "";
-fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
- (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
- [res] =>
- let val t = report_result ctxt res
- in Type_Ext.sort_of_term t end
- | _ => error (ambiguity_msg pos));
+ val results' =
+ if ambiguity > 1 then
+ (Par_List.map_name "Syntax.disambig" o apsnd o Exn.maps_result) check results
+ else results;
+ val reports' = fst (hd results');
+
+ val errs = map snd (failed_results results');
+ val checked = map snd (proper_results results');
+ val len = length checked;
+
+ val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
+ in
+ if len = 0 then
+ report_result ctxt pos
+ [(reports', Exn.Exn (Exn.EXCEPTIONS (ERROR (ambig_msg ()) :: errs)))]
+ else if len = 1 then
+ (if ambiguity > level then
+ Context_Position.if_visible ctxt warning
+ "Fortunately, only one parse tree is type correct.\n\
+ \You may still want to disambiguate your grammar or your input."
+ else (); report_result ctxt pos results')
+ else
+ report_result ctxt pos
+ [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg () ::
+ (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
+ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ map show_term (take limit checked))))))]
+ end;
@@ -874,11 +884,9 @@
val (syms, pos) = read_token str;
in
- (case read_asts ctxt type_ctxt syn true root (syms, pos) of
- [res] =>
- let val ast = report_result ctxt res
- in constify ast end
- | _ => error (ambiguity_msg pos))
+ read_asts ctxt type_ctxt syn true root (syms, pos)
+ |> report_result ctxt pos
+ |> constify
end;
@@ -899,16 +907,16 @@
in
-fun standard_unparse_term idents extern =
- unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_sort {extern_class} ctxt syn =
+ unparse_t (K Printer.sort_to_ast)
+ (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+ Markup.sort ctxt syn false;
fun standard_unparse_typ extern ctxt syn =
unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-fun standard_unparse_sort {extern_class} ctxt syn =
- unparse_t (K Printer.sort_to_ast)
- (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
- Markup.sort ctxt syn false;
+fun standard_unparse_term idents extern =
+ unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
end;
@@ -933,16 +941,14 @@
(*export parts of internal Syntax structures*)
-open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer;
end;
structure Basic_Syntax: BASIC_SYNTAX = Syntax;
open Basic_Syntax;
-forget_structure "Ast";
forget_structure "Syn_Ext";
-forget_structure "Parser";
forget_structure "Type_Ext";
forget_structure "Syn_Trans";
forget_structure "Mixfix";
--- a/src/Pure/Syntax/type_ext.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Tue Apr 05 15:15:33 2011 +0200
@@ -13,7 +13,8 @@
val strip_positions: term -> term
val strip_positions_ast: Ast.ast -> Ast.ast
type term_context
- val decode_term: term_context -> Position.reports * term -> Position.reports * term
+ val decode_term: term_context ->
+ Position.reports * term Exn.result -> Position.reports * term Exn.result
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
@@ -136,55 +137,56 @@
markup_free: string -> Markup.T list,
markup_var: indexname -> Markup.T list};
-fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
- let
- val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
- val decodeT = typ_of_term (get_sort (term_sorts tm));
+fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+ | decode_term (term_context: term_context) (reports0, Exn.Result tm) =
+ let
+ val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
+ val decodeT = typ_of_term (get_sort (term_sorts tm));
- val reports = Unsynchronized.ref reports0;
- fun report ps = Position.reports reports ps;
+ val reports = Unsynchronized.ref reports0;
+ fun report ps = Position.reports reports ps;
- fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
- (case decode_position typ of
- SOME p => decode (p :: ps) qs bs t
- | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
- | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
- (case decode_position typ of
- SOME q => decode ps (q :: qs) bs t
- | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
- | decode _ qs bs (Abs (x, T, t)) =
- let
- val id = serial_string ();
- val _ = report qs (markup_bound true) id;
- in Abs (x, T, decode [] [] (id :: bs) t) end
- | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
- | decode ps _ _ (Const (a, T)) =
- (case try Lexicon.unmark_fixed a of
- SOME x => (report ps markup_free x; Free (x, T))
- | NONE =>
+ fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
+ (case decode_position typ of
+ SOME p => decode (p :: ps) qs bs t
+ | NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
+ | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
+ (case decode_position typ of
+ SOME q => decode ps (q :: qs) bs t
+ | NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
+ | decode _ qs bs (Abs (x, T, t)) =
let
- val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => snd (get_const a));
- val _ = report ps markup_const c;
- in Const (c, T) end)
- | decode ps _ _ (Free (a, T)) =
- (case (get_free a, get_const a) of
- (SOME x, _) => (report ps markup_free x; Free (x, T))
- | (_, (true, c)) => (report ps markup_const c; Const (c, T))
- | (_, (false, c)) =>
- if Long_Name.is_qualified c
- then (report ps markup_const c; Const (c, T))
- else (report ps markup_free c; Free (c, T)))
- | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
- | decode ps _ bs (t as Bound i) =
- (case try (nth bs) i of
- SOME id => (report ps (markup_bound false) id; t)
- | NONE => t);
+ val id = serial_string ();
+ val _ = report qs (markup_bound true) id;
+ in Abs (x, T, decode [] [] (id :: bs) t) end
+ | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
+ | decode ps _ _ (Const (a, T)) =
+ (case try Lexicon.unmark_fixed a of
+ SOME x => (report ps markup_free x; Free (x, T))
+ | NONE =>
+ let
+ val c =
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (get_const a));
+ val _ = report ps markup_const c;
+ in Const (c, T) end)
+ | decode ps _ _ (Free (a, T)) =
+ (case (get_free a, get_const a) of
+ (SOME x, _) => (report ps markup_free x; Free (x, T))
+ | (_, (true, c)) => (report ps markup_const c; Const (c, T))
+ | (_, (false, c)) =>
+ if Long_Name.is_qualified c
+ then (report ps markup_const c; Const (c, T))
+ else (report ps markup_free c; Free (c, T)))
+ | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T))
+ | decode ps _ bs (t as Bound i) =
+ (case try (nth bs) i of
+ SOME id => (report ps (markup_bound false) id; t)
+ | NONE => t);
- val tm' = decode [] [] [] tm;
- in (! reports, tm') end;
+ val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+ in (! reports, tm') end;
--- a/src/Pure/pure_setup.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/pure_setup.ML Tue Apr 05 15:15:33 2011 +0200
@@ -30,7 +30,7 @@
toplevel_pp ["Context", "theory"] "Context.pretty_thy";
toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
-toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Syntax", "ast"] "Ast.pretty_ast";
toplevel_pp ["Path", "T"] "Pretty.str o Path.print";
toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
--- a/src/Pure/sign.ML Tue Apr 05 11:44:34 2011 +0200
+++ b/src/Pure/sign.ML Tue Apr 05 15:15:33 2011 +0200
@@ -91,25 +91,25 @@
val primitive_classrel: class * class -> theory -> theory
val primitive_arity: arity -> theory -> theory
val add_trfuns:
- (string * (ast list -> ast)) list *
+ (string * (Ast.ast list -> Ast.ast)) list *
(string * (term list -> term)) list *
(string * (term list -> term)) list *
- (string * (ast list -> ast)) list -> theory -> theory
+ (string * (Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_trfunsT:
(string * (bool -> typ -> term list -> term)) list -> theory -> theory
val add_advanced_trfuns:
- (string * (Proof.context -> ast list -> ast)) list *
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list *
(string * (Proof.context -> term list -> term)) list *
(string * (Proof.context -> term list -> term)) list *
- (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
+ (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_advanced_trfunsT:
(string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
val add_tokentrfuns:
(string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
-> theory -> theory
- val add_trrules: ast Syntax.trrule list -> theory -> theory
- val del_trrules: ast Syntax.trrule list -> theory -> theory
+ val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+ val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val new_group: theory -> theory
val reset_group: theory -> theory
val add_path: string -> theory -> theory