--- a/src/HOL/Tools/record.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/HOL/Tools/record.ML Tue Apr 05 23:14:41 2011 +0200
@@ -662,7 +662,7 @@
fun get_sort env xi =
the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
in
- Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
+ Standard_Syntax.typ_of_term (get_sort (Standard_Syntax.term_sorts t)) t
end;
--- a/src/Pure/Isar/isar_cmd.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Apr 05 23:14:41 2011 +0200
@@ -161,11 +161,9 @@
fun read_trrules thy raw_rules =
let
val ctxt = ProofContext.init_global thy;
- val type_ctxt = ProofContext.type_context ctxt;
- val syn = ProofContext.syn_of ctxt;
in
raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
- Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
+ Standard_Syntax.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
end;
fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
--- a/src/Pure/Isar/proof_context.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 05 23:14:41 2011 +0200
@@ -67,10 +67,10 @@
val check_tvar: Proof.context -> indexname * sort -> indexname * sort
val check_tfree: Proof.context -> string * sort -> string * sort
val get_sort: Proof.context -> (indexname * sort) list -> indexname -> 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 Exn.result -> Position.reports * term Exn.result
+ type type_context
+ val type_context: Proof.context -> type_context
+ type term_context
+ val term_context: Proof.context -> term_context
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
@@ -670,15 +670,27 @@
in
-fun type_context ctxt : Syntax.type_context =
+type type_context =
+ {get_class: string -> string,
+ get_type: string -> string,
+ markup_class: string -> Markup.T list,
+ markup_type: string -> Markup.T list};
+
+fun type_context ctxt : type_context =
{get_class = read_class ctxt,
get_type = #1 o dest_Type o read_type_name_proper ctxt false,
markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
-fun term_context ctxt : Syntax.term_context =
- {get_sort = get_sort ctxt,
- get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
+type term_context =
+ {get_const: string -> bool * string,
+ get_free: string -> string option,
+ markup_const: string -> Markup.T list,
+ markup_free: string -> Markup.T list,
+ markup_var: indexname -> Markup.T list};
+
+fun term_context ctxt : term_context =
+ {get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
get_free = intern_skolem ctxt (Variable.def_type ctxt false),
markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
@@ -687,8 +699,6 @@
(if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
markup_var = fn xi => [Markup.name (Term.string_of_vname xi) Markup.var]};
-val decode_term = Syntax.decode_term o term_context;
-
end;
--- a/src/Pure/Syntax/standard_syntax.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Syntax/standard_syntax.ML Tue Apr 05 23:14:41 2011 +0200
@@ -4,9 +4,330 @@
Standard implementation of inner syntax operations.
*)
-structure Standard_Syntax: sig end =
+signature STANDARD_SYNTAX =
+sig
+ val term_sorts: term -> (indexname * sort) list
+ val typ_of_term: (indexname -> sort) -> term -> typ
+ val decode_term: Proof.context ->
+ Position.reports * term Exn.result -> Position.reports * term Exn.result
+ val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
+end
+
+structure Standard_Syntax: STANDARD_SYNTAX =
struct
+(** decode parse trees **)
+
+(* sort_of_term *)
+
+fun sort_of_term tm =
+ let
+ fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+ fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+ fun classes (Const (s, _)) = [class s]
+ | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+ | classes _ = err ();
+
+ fun sort (Const ("_topsort", _)) = []
+ | sort (Const (s, _)) = [class s]
+ | sort (Const ("_sort", _) $ cs) = classes cs
+ | sort _ = err ();
+ in sort tm end;
+
+
+(* term_sorts *)
+
+fun term_sorts tm =
+ let
+ val sort_of = sort_of_term;
+
+ fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
+ insert (op =) ((x, ~1), sort_of cs)
+ | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
+ insert (op =) ((x, ~1), sort_of cs)
+ | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
+ insert (op =) (xi, sort_of cs)
+ | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
+ insert (op =) (xi, sort_of cs)
+ | add_env (Abs (_, _, t)) = add_env t
+ | add_env (t1 $ t2) = add_env t1 #> add_env t2
+ | add_env _ = I;
+ in add_env tm [] end;
+
+
+(* typ_of_term *)
+
+fun typ_of_term get_sort tm =
+ let
+ fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+ fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
+ | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
+ | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
+ | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
+ | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
+ | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
+ TFree (x, get_sort (x, ~1))
+ | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
+ | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
+ TVar (xi, get_sort xi)
+ | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+ | typ_of t =
+ let
+ val (head, args) = Term.strip_comb t;
+ val a =
+ (case head of
+ Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+ | _ => err ());
+ in Type (a, map typ_of args) end;
+ in typ_of tm end;
+
+
+(* parsetree_to_ast *)
+
+fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
+
+fun parsetree_to_ast ctxt constrain_pos trf parsetree =
+ let
+ val {get_class, get_type, markup_class, markup_type} = ProofContext.type_context ctxt;
+
+ val reports = Unsynchronized.ref ([]: Position.reports);
+ fun report pos = Position.reports reports [pos];
+
+ fun trans a args =
+ (case trf a of
+ NONE => Ast.mk_appl (Ast.Constant a) args
+ | SOME f => f ctxt args);
+
+ fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
+ let
+ val c = get_class (Lexicon.str_of_token tok);
+ val _ = report (Lexicon.pos_of_token tok) markup_class c;
+ in Ast.Constant (Lexicon.mark_class c) end
+ | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
+ let
+ val c = get_type (Lexicon.str_of_token tok);
+ val _ = report (Lexicon.pos_of_token tok) markup_type c;
+ in Ast.Constant (Lexicon.mark_type c) end
+ | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+ if constrain_pos then
+ Ast.Appl [Ast.Constant "_constrain", ast_of pt,
+ Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
+ else ast_of pt
+ | 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 = Exn.interruptible_capture ast_of parsetree;
+ in (! reports, ast) end;
+
+
+(* ast_to_term *)
+
+fun ast_to_term ctxt trf =
+ let
+ fun trans a args =
+ (case trf a of
+ NONE => Term.list_comb (Lexicon.const a, args)
+ | SOME f => f ctxt args);
+
+ fun term_of (Ast.Constant a) = trans a []
+ | term_of (Ast.Variable x) = Lexicon.read_var x
+ | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
+ trans a (map term_of asts)
+ | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
+ Term.list_comb (term_of ast, map term_of asts)
+ | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
+ in term_of end;
+
+
+(* decode_term -- transform parse tree into raw term *)
+
+fun markup_bound def id =
+ [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
+
+fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+ | decode_term ctxt (reports0, Exn.Result tm) =
+ let
+ val {get_const, get_free, markup_const, markup_free, markup_var} =
+ ProofContext.term_context ctxt;
+ val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
+
+ val reports = Unsynchronized.ref reports0;
+ fun report ps = Position.reports reports ps;
+
+ fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
+ (case Syntax.decode_position_term 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 Syntax.decode_position_term 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 =>
+ 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' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
+ in (! reports, tm') end;
+
+
+
+(** parse **)
+
+(* results *)
+
+fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
+
+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));
+
+
+(* parse_asts *)
+
+fun parse_asts ctxt raw root (syms, pos) =
+ let
+ val {lexicon, gram, parse_ast_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
+
+ val toks = Lexicon.tokenize lexicon raw syms;
+ val _ = List.app (Lexicon.report_token ctxt) toks;
+
+ val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
+ handle ERROR msg =>
+ error (msg ^
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
+ val len = length pts;
+
+ val limit = Config.get ctxt Syntax.ambiguity_limit;
+ val _ =
+ if len <= Config.get ctxt Syntax.ambiguity_level then ()
+ else if not (Config.get ctxt Syntax.ambiguity_enabled) then error (ambiguity_msg pos)
+ else
+ (Context_Position.if_visible ctxt warning (cat_lines
+ (("Ambiguous input" ^ Position.str_of pos ^
+ "\nproduces " ^ string_of_int len ^ " parse trees" ^
+ (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
+ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
+
+ val constrain_pos = not raw andalso Config.get ctxt Syntax.positions;
+ val parsetree_to_ast = parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab);
+ in map parsetree_to_ast pts end;
+
+
+(* read_raw *)
+
+fun read_raw ctxt root input =
+ let
+ val {parse_ruletab, parse_trtab, ...} = Syntax.rep_syntax (ProofContext.syn_of ctxt);
+ val norm = Ast.normalize ctxt (Symtab.lookup_list parse_ruletab);
+ val ast_to_term = ast_to_term ctxt (lookup_tr parse_trtab);
+ in
+ parse_asts ctxt false root input
+ |> (map o apsnd o Exn.maps_result) (norm #> Exn.interruptible_capture ast_to_term)
+ end;
+
+
+(* read sorts *)
+
+fun standard_parse_sort ctxt (syms, pos) =
+ read_raw ctxt "sort" (syms, pos)
+ |> report_result ctxt pos
+ |> sort_of_term;
+
+
+(* read types *)
+
+fun standard_parse_typ ctxt (syms, pos) =
+ read_raw ctxt "type" (syms, pos)
+ |> report_result ctxt pos
+ |> (fn t => typ_of_term (ProofContext.get_sort ctxt (term_sorts t)) t);
+
+
+(* read terms -- brute-force disambiguation via type-inference *)
+
+fun standard_parse_term check ctxt root (syms, pos) =
+ let
+ val results = read_raw ctxt root (syms, pos) |> map (decode_term ctxt);
+
+ val level = Config.get ctxt Syntax.ambiguity_level;
+ val limit = Config.get ctxt Syntax.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 "";
+
+ 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 = Syntax.string_of_term (Config.put Syntax.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;
+
+
+(* standard operations *)
+
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
@@ -14,19 +335,15 @@
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
- val S =
- Syntax.standard_parse_sort ctxt (ProofContext.type_context ctxt)
- (ProofContext.syn_of ctxt) (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg "sort";
+ val S = standard_parse_sort ctxt (syms, pos)
+ handle ERROR msg => parse_failed ctxt pos msg "sort";
in Type.minimize_sort (ProofContext.tsig_of ctxt) S end;
fun parse_typ ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
- val T =
- Syntax.standard_parse_typ ctxt (ProofContext.type_context ctxt)
- (ProofContext.syn_of ctxt) (ProofContext.get_sort ctxt) (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg "type";
+ val T = standard_parse_typ ctxt (syms, pos)
+ handle ERROR msg => parse_failed ctxt pos msg "type";
in T end;
fun parse_term T ctxt text =
@@ -46,14 +363,34 @@
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
- (ProofContext.type_context ctxt) (ProofContext.term_context ctxt)
- (ProofContext.syn_of ctxt) root (syms, pos)
+ val t = standard_parse_term check ctxt root (syms, pos)
handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
+(* parse_ast_pattern *)
+
+fun parse_ast_pattern ctxt (root, str) =
+ let
+ val syn = ProofContext.syn_of ctxt;
+
+ fun constify (ast as Ast.Constant _) = ast
+ | constify (ast as Ast.Variable x) =
+ if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
+ else ast
+ | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
+
+ val (syms, pos) = Syntax.read_token str;
+ in
+ parse_asts ctxt true root (syms, pos)
+ |> report_result ctxt pos
+ |> constify
+ end;
+
+
+
+(** unparse **)
+
fun unparse_sort ctxt =
Syntax.standard_unparse_sort {extern_class = Type.extern_class (ProofContext.tsig_of ctxt)}
ctxt (ProofContext.syn_of ctxt);
@@ -79,6 +416,8 @@
end;
+(** install operations **)
+
val _ = Syntax.install_operations
{parse_sort = parse_sort,
parse_typ = parse_typ,
--- a/src/Pure/Syntax/syn_trans.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Tue Apr 05 23:14:41 2011 +0200
@@ -48,7 +48,6 @@
(string * (term list -> term)) list *
(string * (bool -> typ -> term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list
- type type_context
end;
signature SYN_TRANS =
@@ -58,11 +57,6 @@
val prop_tr': term -> term
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
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 Exn.result
- val ast_to_term: Proof.context ->
- (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
end;
structure Syn_Trans: SYN_TRANS =
@@ -547,67 +541,4 @@
fun struct_trfuns structs =
([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
-
-
-(** parsetree_to_ast **)
-
-type type_context =
- {get_class: string -> string,
- get_type: string -> string,
- markup_class: string -> Markup.T list,
- markup_type: string -> Markup.T list};
-
-fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
- let
- val {get_class, get_type, markup_class, markup_type} = type_context;
-
- val reports = Unsynchronized.ref ([]: Position.reports);
- fun report pos = Position.reports reports [pos];
-
- fun trans a args =
- (case trf a of
- NONE => Ast.mk_appl (Ast.Constant a) args
- | SOME f => f ctxt args);
-
- fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
- let
- val c = get_class (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_class c;
- in Ast.Constant (Lexicon.mark_class c) end
- | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
- let
- val c = get_type (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_type c;
- in Ast.Constant (Lexicon.mark_type c) end
- | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
- if constrain_pos then
- Ast.Appl [Ast.Constant "_constrain", ast_of pt,
- Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
- else ast_of pt
- | 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 = Exn.interruptible_capture ast_of parsetree;
- in (! reports, ast) end;
-
-
-
-(** ast_to_term **)
-
-fun ast_to_term ctxt trf =
- let
- fun trans a args =
- (case trf a of
- NONE => Term.list_comb (Lexicon.const a, args)
- | SOME f => f ctxt args);
-
- fun term_of (Ast.Constant a) = trans a []
- | term_of (Ast.Variable x) = Lexicon.read_var x
- | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) =
- trans a (map term_of asts)
- | term_of (Ast.Appl (ast :: (asts as _ :: _))) =
- Term.list_comb (term_of ast, map term_of asts)
- | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
- in term_of end;
-
end;
--- a/src/Pure/Syntax/syntax.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Apr 05 23:14:41 2011 +0200
@@ -95,7 +95,22 @@
val string_of_sort_global: theory -> sort -> string
val pp: Proof.context -> Pretty.pp
val pp_global: theory -> Pretty.pp
+ type ruletab
type syntax
+ val rep_syntax: syntax ->
+ {input: Syn_Ext.xprod list,
+ lexicon: Scan.lexicon,
+ gram: Parser.gram,
+ consts: string list,
+ prmodes: string list,
+ parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
+ parse_ruletab: ruletab,
+ parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
+ print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+ print_ruletab: ruletab,
+ print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
+ tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
+ prtabs: Printer.prtabs}
val eq_syntax: syntax * syntax -> bool
val is_keyword: syntax -> string -> bool
type mode
@@ -114,20 +129,12 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
- 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
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.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} ->
@@ -394,8 +401,6 @@
(* parse (ast) translations *)
-fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
-
fun err_dup_trfun name c =
error ("More than one " ^ name ^ " for " ^ quote c);
@@ -484,6 +489,7 @@
tokentrtab: (string * (string * ((Proof.context -> string -> Pretty.T) * stamp)) list) list,
prtabs: Printer.prtabs} * stamp;
+fun rep_syntax (Syntax (tabs, _)) = tabs;
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
@@ -700,131 +706,6 @@
val ambiguity_limit =
Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
-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;
- val toks = Lexicon.tokenize lexicon raw syms;
- val _ = List.app (Lexicon.report_token ctxt) toks;
-
- val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
- handle ERROR msg =>
- error (msg ^
- implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
- val len = length pts;
-
- val limit = Config.get ctxt ambiguity_limit;
- val _ =
- if len <= Config.get ctxt ambiguity_level then ()
- else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
- else
- (Context_Position.if_visible ctxt warning (cat_lines
- (("Ambiguous input" ^ Position.str_of pos ^
- "\nproduces " ^ string_of_int len ^ " parse trees" ^
- (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
-
- val constrain_pos = not raw andalso Config.get ctxt positions;
- 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_raw *)
-
-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 sorts *)
-
-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) =
- 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 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 "";
-
- 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;
-
(** prepare translation rules **)
@@ -872,24 +753,6 @@
end;
-(* read_rule_pattern *)
-
-fun read_rule_pattern ctxt type_ctxt syn (root, str) =
- let
- fun constify (ast as Ast.Constant _) = ast
- | constify (ast as Ast.Variable x) =
- if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
- else ast
- | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
-
- val (syms, pos) = read_token str;
- in
- read_asts ctxt type_ctxt syn true root (syms, pos)
- |> report_result ctxt pos
- |> constify
- end;
-
-
(** unparse terms, typs, sorts **)
--- a/src/Pure/Syntax/type_ext.ML Tue Apr 05 18:06:45 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Tue Apr 05 23:14:41 2011 +0200
@@ -6,15 +6,10 @@
signature TYPE_EXT0 =
sig
- val sort_of_term: term -> sort
- val term_sorts: term -> (indexname * sort) list
- val typ_of_term: (indexname -> sort) -> term -> typ
+ val decode_position_term: term -> Position.T option
val is_position: term -> bool
val strip_positions: term -> term
val strip_positions_ast: Ast.ast -> Ast.ast
- type term_context
- 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
@@ -25,7 +20,6 @@
include TYPE_EXT0
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val sortT: typ
val type_ext: Syn_Ext.syn_ext
end;
@@ -34,79 +28,12 @@
(** input utils **)
-(* sort_of_term *)
-
-fun sort_of_term tm =
- let
- fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
-
- fun class s = Lexicon.unmark_class s handle Fail _ => err ();
-
- fun classes (Const (s, _)) = [class s]
- | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
- | classes _ = err ();
-
- fun sort (Const ("_topsort", _)) = []
- | sort (Const (s, _)) = [class s]
- | sort (Const ("_sort", _) $ cs) = classes cs
- | sort _ = err ();
- in sort tm end;
-
-
-(* term_sorts *)
-
-fun term_sorts tm =
- let
- val sort_of = sort_of_term;
-
- fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
- insert (op =) ((x, ~1), sort_of cs)
- | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
- insert (op =) ((x, ~1), sort_of cs)
- | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
- insert (op =) (xi, sort_of cs)
- | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
- insert (op =) (xi, sort_of cs)
- | add_env (Abs (_, _, t)) = add_env t
- | add_env (t1 $ t2) = add_env t1 #> add_env t2
- | add_env _ = I;
- in add_env tm [] end;
-
-
-(* typ_of_term *)
-
-fun typ_of_term get_sort tm =
- let
- fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
-
- fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
- | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
- | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
- | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
- | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
- | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
- TFree (x, get_sort (x, ~1))
- | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
- | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
- TVar (xi, get_sort xi)
- | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
- | typ_of t =
- let
- val (head, args) = Term.strip_comb t;
- val a =
- (case head of
- Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
- | _ => err ());
- in Type (a, map typ_of args) end;
- in typ_of tm end;
-
-
(* positions *)
-fun decode_position (Free (x, _)) = Lexicon.decode_position x
- | decode_position _ = NONE;
+fun decode_position_term (Free (x, _)) = Lexicon.decode_position x
+ | decode_position_term _ = NONE;
-val is_position = is_some o decode_position;
+val is_position = is_some o decode_position_term;
fun strip_positions ((t as Const (c, _)) $ u $ v) =
if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
@@ -124,71 +51,6 @@
| strip_positions_ast ast = ast;
-(* decode_term -- transform parse tree into raw term *)
-
-fun markup_bound def id =
- [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
-
-type term_context =
- {get_sort: (indexname * sort) list -> indexname -> sort,
- get_const: string -> bool * string,
- get_free: string -> string option,
- markup_const: string -> Markup.T list,
- markup_free: string -> Markup.T list,
- markup_var: indexname -> Markup.T list};
-
-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;
-
- 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 =>
- 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' = Exn.interruptible_capture (fn () => decode [] [] [] tm) ();
- in (! reports, tm') end;
-
-
(** output utils **)