# HG changeset patch # User wenzelm # Date 1302038081 -7200 # Node ID 39261908e12f349142d651dcd83b8a4d7e490760 # Parent dd8029f71e1c6c073d53575b45bcf5adfb4e5b64 moved decode/parse operations to standard_syntax.ML; tuned; diff -r dd8029f71e1c -r 39261908e12f src/HOL/Tools/record.ML --- 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; diff -r dd8029f71e1c -r 39261908e12f src/Pure/Isar/isar_cmd.ML --- 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; diff -r dd8029f71e1c -r 39261908e12f src/Pure/Isar/proof_context.ML --- 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; diff -r dd8029f71e1c -r 39261908e12f src/Pure/Syntax/standard_syntax.ML --- 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, diff -r dd8029f71e1c -r 39261908e12f src/Pure/Syntax/syn_trans.ML --- 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; diff -r dd8029f71e1c -r 39261908e12f src/Pure/Syntax/syntax.ML --- 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 **) diff -r dd8029f71e1c -r 39261908e12f src/Pure/Syntax/type_ext.ML --- 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 **)