wenzelm@42243: (* Title: Pure/Syntax/syntax_phases.ML wenzelm@42241: Author: Makarius wenzelm@42241: wenzelm@42243: Main phases of inner syntax processing, with standard implementations wenzelm@42243: of parse/unparse operations. wenzelm@42241: *) wenzelm@42241: wenzelm@42243: signature SYNTAX_PHASES = wenzelm@42242: sig wenzelm@45427: val decode_sort: term -> sort wenzelm@45427: val decode_typ: term -> typ wenzelm@42242: val decode_term: Proof.context -> wenzelm@44736: Position.report list * term Exn.result -> Position.report list * term Exn.result wenzelm@42242: val parse_ast_pattern: Proof.context -> string * string -> Ast.ast wenzelm@42247: val term_of_typ: Proof.context -> typ -> term wenzelm@45429: val print_checks: Proof.context -> unit wenzelm@45429: val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> wenzelm@45429: Context.generic -> Context.generic wenzelm@45429: val term_check: int -> string -> (Proof.context -> term list -> term list) -> wenzelm@45429: Context.generic -> Context.generic wenzelm@45429: val typ_uncheck: int -> string -> (Proof.context -> typ list -> typ list) -> wenzelm@45429: Context.generic -> Context.generic wenzelm@45429: val term_uncheck: int -> string -> (Proof.context -> term list -> term list) -> wenzelm@45429: Context.generic -> Context.generic wenzelm@45444: val typ_check': int -> string -> wenzelm@45444: (typ list -> Proof.context -> (typ list * Proof.context) option) -> wenzelm@45444: Context.generic -> Context.generic wenzelm@45444: val term_check': int -> string -> wenzelm@45444: (term list -> Proof.context -> (term list * Proof.context) option) -> wenzelm@45444: Context.generic -> Context.generic wenzelm@45444: val typ_uncheck': int -> string -> wenzelm@45444: (typ list -> Proof.context -> (typ list * Proof.context) option) -> wenzelm@45444: Context.generic -> Context.generic wenzelm@45444: val term_uncheck': int -> string -> wenzelm@45444: (term list -> Proof.context -> (term list * Proof.context) option) -> wenzelm@45444: Context.generic -> Context.generic wenzelm@42242: end wenzelm@42242: wenzelm@42243: structure Syntax_Phases: SYNTAX_PHASES = wenzelm@42241: struct wenzelm@42241: wenzelm@42298: (** markup logical entities **) wenzelm@42298: wenzelm@42298: fun markup_class ctxt c = wenzelm@42379: [Name_Space.markup (Type.class_space (Proof_Context.tsig_of ctxt)) c]; wenzelm@42298: wenzelm@42298: fun markup_type ctxt c = wenzelm@42379: [Name_Space.markup (Type.type_space (Proof_Context.tsig_of ctxt)) c]; wenzelm@42298: wenzelm@42298: fun markup_const ctxt c = wenzelm@42379: [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; wenzelm@42298: wenzelm@42298: fun markup_free ctxt x = wenzelm@45666: [if can Name.dest_skolem x then Isabelle_Markup.skolem else Isabelle_Markup.free] @ wenzelm@42493: (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x wenzelm@42493: then [Variable.markup_fixed ctxt x] wenzelm@42493: else []); wenzelm@42298: wenzelm@45666: fun markup_var xi = [Markup.name (Term.string_of_vname xi) Isabelle_Markup.var]; wenzelm@42298: wenzelm@45412: fun markup_bound def ps (name, id) = wenzelm@45666: let val entity = Isabelle_Markup.entity Isabelle_Markup.boundN name in wenzelm@45666: Isabelle_Markup.bound :: wenzelm@45412: map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps wenzelm@45412: end; wenzelm@42298: wenzelm@42298: fun markup_entity ctxt c = wenzelm@42360: (case Syntax.lookup_const (Proof_Context.syn_of ctxt) c of wenzelm@42298: SOME "" => [] wenzelm@42298: | SOME b => markup_entity ctxt b wenzelm@42298: | NONE => c |> Lexicon.unmark wenzelm@42298: {case_class = markup_class ctxt, wenzelm@42298: case_type = markup_type ctxt, wenzelm@42298: case_const = markup_const ctxt, wenzelm@42298: case_fixed = markup_free ctxt, wenzelm@42298: case_default = K []}); wenzelm@42298: wenzelm@42298: wenzelm@42298: wenzelm@42242: (** decode parse trees **) wenzelm@42242: wenzelm@45427: (* decode_sort *) wenzelm@42242: wenzelm@45427: fun decode_sort tm = wenzelm@42242: let wenzelm@45427: fun err () = raise TERM ("decode_sort: bad encoding of classes", [tm]); wenzelm@42242: wenzelm@42242: fun class s = Lexicon.unmark_class s handle Fail _ => err (); wenzelm@42242: wenzelm@42242: fun classes (Const (s, _)) = [class s] wenzelm@42242: | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs wenzelm@42242: | classes _ = err (); wenzelm@42242: wenzelm@42242: fun sort (Const ("_topsort", _)) = [] wenzelm@42242: | sort (Const (s, _)) = [class s] wenzelm@42242: | sort (Const ("_sort", _) $ cs) = classes cs wenzelm@42242: | sort _ = err (); wenzelm@42242: in sort tm end; wenzelm@42242: wenzelm@42242: wenzelm@45427: (* decode_typ *) wenzelm@42242: wenzelm@45427: fun decode_typ tm = wenzelm@45427: let wenzelm@45427: fun err () = raise TERM ("decode_typ: bad encoding of type", [tm]); wenzelm@42242: wenzelm@45427: fun typ (Free (x, _)) = TFree (x, dummyS) wenzelm@45427: | typ (Var (xi, _)) = TVar (xi, dummyS) wenzelm@45427: | typ (Const ("_tfree",_) $ (t as Free _)) = typ t wenzelm@45427: | typ (Const ("_tvar",_) $ (t as Var _)) = typ t wenzelm@45427: | typ (Const ("_ofsort", _) $ Free (x, _) $ s) = TFree (x, decode_sort s) wenzelm@45427: | typ (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ s) = wenzelm@45427: TFree (x, decode_sort s) wenzelm@45427: | typ (Const ("_ofsort", _) $ Var (xi, _) $ s) = TVar (xi, decode_sort s) wenzelm@45427: | typ (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ s) = wenzelm@45427: TVar (xi, decode_sort s) wenzelm@45427: | typ (Const ("_dummy_ofsort", _) $ s) = TFree ("'_dummy_", decode_sort s) wenzelm@45427: | typ t = wenzelm@42242: let wenzelm@42242: val (head, args) = Term.strip_comb t; wenzelm@42242: val a = wenzelm@42242: (case head of wenzelm@42242: Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ()) wenzelm@42242: | _ => err ()); wenzelm@45427: in Type (a, map typ args) end; wenzelm@45427: in typ tm end; wenzelm@42242: wenzelm@42242: wenzelm@42242: (* parsetree_to_ast *) wenzelm@42242: wenzelm@46126: fun parsetree_to_ast ctxt raw trf parsetree = wenzelm@42242: let wenzelm@44736: val reports = Unsynchronized.ref ([]: Position.report list); wenzelm@44735: fun report pos = Position.store_reports reports [pos]; wenzelm@42242: wenzelm@42242: fun trans a args = wenzelm@42242: (case trf a of wenzelm@42242: NONE => Ast.mk_appl (Ast.Constant a) args wenzelm@42242: | SOME f => f ctxt args); wenzelm@42242: wenzelm@42282: fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) = wenzelm@42242: let wenzelm@42470: val pos = Lexicon.pos_of_token tok; wenzelm@42470: val c = Proof_Context.read_class ctxt (Lexicon.str_of_token tok) wenzelm@42470: handle ERROR msg => error (msg ^ Position.str_of pos); wenzelm@42470: val _ = report pos (markup_class ctxt) c; wenzelm@42282: in [Ast.Constant (Lexicon.mark_class c)] end wenzelm@42282: | asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) = wenzelm@42242: let wenzelm@42470: val pos = Lexicon.pos_of_token tok; wenzelm@42470: val Type (c, _) = wenzelm@42470: Proof_Context.read_type_name_proper ctxt false (Lexicon.str_of_token tok) wenzelm@42470: handle ERROR msg => error (msg ^ Position.str_of pos); wenzelm@42470: val _ = report pos (markup_type ctxt) c; wenzelm@42282: in [Ast.Constant (Lexicon.mark_type c)] end wenzelm@42410: | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) = wenzelm@46126: if raw then [ast_of pt] wenzelm@46126: else wenzelm@45453: [Ast.Appl [Ast.Constant "_constrain", ast_of pt, wenzelm@45453: Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]] wenzelm@42282: | asts_of (Parser.Node (a, pts)) = wenzelm@42282: let wenzelm@42282: val _ = pts |> List.app wenzelm@42282: (fn Parser.Node _ => () | Parser.Tip tok => wenzelm@42282: if Lexicon.valued_token tok then () wenzelm@42298: else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a); wenzelm@42282: in [trans a (maps asts_of pts)] end wenzelm@42282: | asts_of (Parser.Tip tok) = wenzelm@42282: if Lexicon.valued_token tok wenzelm@42282: then [Ast.Variable (Lexicon.str_of_token tok)] wenzelm@42282: else [] wenzelm@42282: wenzelm@42282: and ast_of pt = wenzelm@42282: (case asts_of pt of wenzelm@42282: [ast] => ast wenzelm@42282: | asts => raise Ast.AST ("parsetree_to_ast: malformed parsetree", asts)); wenzelm@42242: wenzelm@42242: val ast = Exn.interruptible_capture ast_of parsetree; wenzelm@42242: in (! reports, ast) end; wenzelm@42242: wenzelm@42242: wenzelm@42242: (* ast_to_term *) wenzelm@42242: wenzelm@42242: fun ast_to_term ctxt trf = wenzelm@42242: let wenzelm@42242: fun trans a args = wenzelm@42242: (case trf a of wenzelm@42476: NONE => Term.list_comb (Syntax.const a, args) wenzelm@42242: | SOME f => f ctxt args); wenzelm@42242: wenzelm@42242: fun term_of (Ast.Constant a) = trans a [] wenzelm@42242: | term_of (Ast.Variable x) = Lexicon.read_var x wenzelm@42242: | term_of (Ast.Appl (Ast.Constant a :: (asts as _ :: _))) = wenzelm@42242: trans a (map term_of asts) wenzelm@42242: | term_of (Ast.Appl (ast :: (asts as _ :: _))) = wenzelm@42242: Term.list_comb (term_of ast, map term_of asts) wenzelm@42242: | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]); wenzelm@42242: in term_of end; wenzelm@42242: wenzelm@42242: wenzelm@42242: (* decode_term -- transform parse tree into raw term *) wenzelm@42242: wenzelm@44736: fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result wenzelm@43761: | decode_term ctxt (reports0, Exn.Res tm) = wenzelm@42242: let wenzelm@42250: fun get_const a = wenzelm@42360: ((true, #1 (Term.dest_Const (Proof_Context.read_const_proper ctxt false a))) wenzelm@42360: handle ERROR _ => (false, Consts.intern (Proof_Context.consts_of ctxt) a)); wenzelm@42360: val get_free = Proof_Context.intern_skolem ctxt; wenzelm@42250: wenzelm@42242: val reports = Unsynchronized.ref reports0; wenzelm@44735: fun report ps = Position.store_reports reports ps; wenzelm@42242: wenzelm@42242: fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) = wenzelm@42264: (case Term_Position.decode_position typ of wenzelm@45445: SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t) wenzelm@45427: | NONE => Type.constraint (decode_typ typ) (decode ps qs bs t)) wenzelm@42242: | decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) = wenzelm@42264: (case Term_Position.decode_position typ of wenzelm@45445: SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t) wenzelm@45427: | NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t)) wenzelm@42242: | decode _ qs bs (Abs (x, T, t)) = wenzelm@42242: let wenzelm@45412: val id = serial (); wenzelm@45412: val _ = report qs (markup_bound true qs) (x, id); wenzelm@45412: in Abs (x, T, decode [] [] ((qs, (x, id)) :: bs) t) end wenzelm@42242: | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u wenzelm@42242: | decode ps _ _ (Const (a, T)) = wenzelm@42242: (case try Lexicon.unmark_fixed a of wenzelm@42282: SOME x => (report ps (markup_free ctxt) x; Free (x, T)) wenzelm@42242: | NONE => wenzelm@42242: let wenzelm@42242: val c = wenzelm@42242: (case try Lexicon.unmark_const a of wenzelm@42242: SOME c => c wenzelm@42242: | NONE => snd (get_const a)); wenzelm@42282: val _ = report ps (markup_const ctxt) c; wenzelm@42242: in Const (c, T) end) wenzelm@42242: | decode ps _ _ (Free (a, T)) = wenzelm@42242: (case (get_free a, get_const a) of wenzelm@42282: (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T)) wenzelm@42282: | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T)) wenzelm@42242: | (_, (false, c)) => wenzelm@42242: if Long_Name.is_qualified c wenzelm@42282: then (report ps (markup_const ctxt) c; Const (c, T)) wenzelm@42282: else (report ps (markup_free ctxt) c; Free (c, T))) wenzelm@42242: | decode ps _ _ (Var (xi, T)) = (report ps markup_var xi; Var (xi, T)) wenzelm@42242: | decode ps _ bs (t as Bound i) = wenzelm@42242: (case try (nth bs) i of wenzelm@45412: SOME (qs, (x, id)) => (report ps (markup_bound false qs) (x, id); t) wenzelm@42242: | NONE => t); wenzelm@42242: wenzelm@42242: val tm' = Exn.interruptible_capture (fn () => decode [] [] [] tm) (); wenzelm@42242: in (! reports, tm') end; wenzelm@42242: wenzelm@42242: wenzelm@42242: wenzelm@42242: (** parse **) wenzelm@42242: wenzelm@42242: (* results *) wenzelm@42242: wenzelm@43761: fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results; wenzelm@42242: fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results; wenzelm@42242: wenzelm@46512: fun report_result ctxt pos ambig_msgs results = wenzelm@42242: (case (proper_results results, failed_results results) of wenzelm@44736: ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn) wenzelm@44736: | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x) wenzelm@46512: | _ => wenzelm@46512: if null ambig_msgs then wenzelm@46512: error ("Parse error: ambiguous syntax" ^ Position.str_of pos) wenzelm@46512: else error (cat_lines ambig_msgs)); wenzelm@42242: wenzelm@42242: wenzelm@42249: (* parse raw asts *) wenzelm@42242: wenzelm@42242: fun parse_asts ctxt raw root (syms, pos) = wenzelm@42242: let wenzelm@42360: val syn = Proof_Context.syn_of ctxt; wenzelm@42253: val ast_tr = Syntax.parse_ast_translation syn; wenzelm@42242: wenzelm@42251: val toks = Syntax.tokenize syn raw syms; wenzelm@44736: val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks); wenzelm@42242: wenzelm@45641: val pts = Syntax.parse syn root (filter Lexicon.is_proper toks) wenzelm@42242: handle ERROR msg => wenzelm@42242: error (msg ^ wenzelm@45666: implode wenzelm@45666: (map (Markup.markup Isabelle_Markup.report o Lexicon.reported_token_range ctxt) toks)); wenzelm@42242: val len = length pts; wenzelm@42242: wenzelm@42242: val limit = Config.get ctxt Syntax.ambiguity_limit; wenzelm@46512: val ambig_msgs = wenzelm@46512: if len <= 1 then [] wenzelm@46506: else wenzelm@46512: [cat_lines wenzelm@46512: (("Ambiguous input" ^ Position.str_of (Position.reset_range pos) ^ wenzelm@46512: "\nproduces " ^ string_of_int len ^ " parse trees" ^ wenzelm@46512: (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: wenzelm@46512: map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))]; wenzelm@46512: wenzelm@46512: in (ambig_msgs, map (parsetree_to_ast ctxt raw ast_tr) pts) end; wenzelm@42242: wenzelm@46506: fun parse_tree ctxt root input = wenzelm@42242: let wenzelm@42360: val syn = Proof_Context.syn_of ctxt; wenzelm@42253: val tr = Syntax.parse_translation syn; wenzelm@42255: val parse_rules = Syntax.parse_rules syn; wenzelm@46512: val (ambig_msgs, asts) = parse_asts ctxt false root input; wenzelm@46512: val results = wenzelm@46512: (map o apsnd o Exn.maps_result) wenzelm@46512: (Ast.normalize ctxt parse_rules #> Exn.interruptible_capture (ast_to_term ctxt tr)) asts; wenzelm@46512: in (ambig_msgs, results) end; wenzelm@42242: wenzelm@42242: wenzelm@42249: (* parse logical entities *) wenzelm@42242: wenzelm@42241: fun parse_failed ctxt pos msg kind = wenzelm@42241: cat_error msg ("Failed to parse " ^ kind ^ wenzelm@45666: Markup.markup Isabelle_Markup.report wenzelm@45666: (Context_Position.reported_text ctxt pos Isabelle_Markup.bad "")); wenzelm@42241: wenzelm@43731: fun parse_sort ctxt = wenzelm@45666: Syntax.parse_token ctxt Term_XML.Decode.sort Isabelle_Markup.sort wenzelm@43731: (fn (syms, pos) => wenzelm@46506: parse_tree ctxt "sort" (syms, pos) wenzelm@46512: |> uncurry (report_result ctxt pos) wenzelm@45427: |> decode_sort wenzelm@43731: |> Type.minimize_sort (Proof_Context.tsig_of ctxt) wenzelm@43731: handle ERROR msg => parse_failed ctxt pos msg "sort"); wenzelm@42241: wenzelm@43731: fun parse_typ ctxt = wenzelm@45666: Syntax.parse_token ctxt Term_XML.Decode.typ Isabelle_Markup.typ wenzelm@43731: (fn (syms, pos) => wenzelm@46506: parse_tree ctxt "type" (syms, pos) wenzelm@46512: |> uncurry (report_result ctxt pos) wenzelm@45427: |> decode_typ wenzelm@43731: handle ERROR msg => parse_failed ctxt pos msg "type"); wenzelm@42241: wenzelm@43731: fun parse_term is_prop ctxt = wenzelm@42241: let wenzelm@42281: val (markup, kind, root, constrain) = wenzelm@42281: if is_prop wenzelm@45666: then (Isabelle_Markup.prop, "proposition", "prop", Type.constraint propT) wenzelm@45666: else (Isabelle_Markup.term, "term", Config.get ctxt Syntax.root, I); wenzelm@43731: val decode = constrain o Term_XML.Decode.term; wenzelm@42249: in wenzelm@43731: Syntax.parse_token ctxt decode markup wenzelm@43731: (fn (syms, pos) => wenzelm@43731: let wenzelm@46512: val (ambig_msgs, results) = parse_tree ctxt root (syms, pos) ||> map (decode_term ctxt); wenzelm@46506: val parsed_len = length (proper_results results); wenzelm@42249: wenzelm@46512: val ambiguity_warning = Config.get ctxt Syntax.ambiguity_warning; wenzelm@43731: val limit = Config.get ctxt Syntax.ambiguity_limit; wenzelm@42249: wenzelm@43731: (*brute-force disambiguation via type-inference*) wenzelm@43761: fun check t = (Syntax.check_term ctxt (constrain t); Exn.Res t) wenzelm@43731: handle exn as ERROR _ => Exn.Exn exn; wenzelm@42249: wenzelm@43731: val results' = wenzelm@46506: if parsed_len > 1 then wenzelm@43731: (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result) wenzelm@43731: check results wenzelm@43731: else results; wenzelm@43731: val reports' = fst (hd results'); wenzelm@42249: wenzelm@43731: val errs = map snd (failed_results results'); wenzelm@43731: val checked = map snd (proper_results results'); wenzelm@46506: val checked_len = length checked; wenzelm@42249: wenzelm@43731: val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt); wenzelm@43731: in wenzelm@46506: if checked_len = 0 then wenzelm@46512: report_result ctxt pos [] wenzelm@46512: [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msgs @ errs)))] wenzelm@46506: else if checked_len = 1 then wenzelm@46512: (if parsed_len > 1 andalso ambiguity_warning then wenzelm@43731: Context_Position.if_visible ctxt warning wenzelm@46512: (cat_lines (ambig_msgs @ wenzelm@46512: ["Fortunately, only one parse tree is type correct" ^ wenzelm@46512: Position.str_of (Position.reset_range pos) ^ wenzelm@46512: ",\nbut you may still want to disambiguate your grammar or your input."])) wenzelm@46512: else (); report_result ctxt pos [] results') wenzelm@43731: else wenzelm@46512: report_result ctxt pos [] wenzelm@46512: [(reports', Exn.Exn (ERROR (cat_lines (ambig_msgs @ wenzelm@46512: (("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^ wenzelm@46506: (if checked_len <= limit then "" wenzelm@46506: else " (" ^ string_of_int limit ^ " displayed)") ^ ":") :: wenzelm@43731: map show_term (take limit checked))))))] wenzelm@43731: end handle ERROR msg => parse_failed ctxt pos msg kind) wenzelm@42249: end; wenzelm@42241: wenzelm@42241: wenzelm@42242: (* parse_ast_pattern *) wenzelm@42242: wenzelm@42242: fun parse_ast_pattern ctxt (root, str) = wenzelm@42242: let wenzelm@42360: val syn = Proof_Context.syn_of ctxt; wenzelm@42242: wenzelm@42242: fun constify (ast as Ast.Constant _) = ast wenzelm@42242: | constify (ast as Ast.Variable x) = wenzelm@42298: if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x wenzelm@42298: then Ast.Constant x wenzelm@42242: else ast wenzelm@42242: | constify (Ast.Appl asts) = Ast.Appl (map constify asts); wenzelm@42242: wenzelm@42242: val (syms, pos) = Syntax.read_token str; wenzelm@42242: in wenzelm@42242: parse_asts ctxt true root (syms, pos) wenzelm@46512: |> uncurry (report_result ctxt pos) wenzelm@42242: |> constify wenzelm@42242: end; wenzelm@42242: wenzelm@42242: wenzelm@42242: wenzelm@42245: (** encode parse trees **) wenzelm@42245: wenzelm@42245: (* term_of_sort *) wenzelm@42245: wenzelm@42245: fun term_of_sort S = wenzelm@42245: let wenzelm@42476: val class = Syntax.const o Lexicon.mark_class; wenzelm@42245: wenzelm@42245: fun classes [c] = class c wenzelm@42476: | classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs; wenzelm@42245: in wenzelm@42245: (case S of wenzelm@42476: [] => Syntax.const "_topsort" wenzelm@42245: | [c] => class c wenzelm@42476: | cs => Syntax.const "_sort" $ classes cs) wenzelm@42245: end; wenzelm@42245: wenzelm@42245: wenzelm@42245: (* term_of_typ *) wenzelm@42245: wenzelm@42247: fun term_of_typ ctxt ty = wenzelm@42245: let wenzelm@42247: val show_sorts = Config.get ctxt show_sorts; wenzelm@42247: wenzelm@42245: fun of_sort t S = wenzelm@42476: if show_sorts then Syntax.const "_ofsort" $ t $ term_of_sort S wenzelm@42245: else t; wenzelm@42245: wenzelm@42245: fun term_of (Type (a, Ts)) = wenzelm@42476: Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts) wenzelm@42245: | term_of (TFree (x, S)) = wenzelm@42290: if is_some (Term_Position.decode x) then Syntax.free x wenzelm@42476: else of_sort (Syntax.const "_tfree" $ Syntax.free x) S wenzelm@42476: | term_of (TVar (xi, S)) = of_sort (Syntax.const "_tvar" $ Syntax.var xi) S; wenzelm@42245: in term_of ty end; wenzelm@42245: wenzelm@42245: wenzelm@42245: (* simple_ast_of *) wenzelm@42245: wenzelm@42245: fun simple_ast_of ctxt = wenzelm@42245: let wenzelm@42245: val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?"; wenzelm@42245: fun ast_of (Const (c, _)) = Ast.Constant c wenzelm@42245: | ast_of (Free (x, _)) = Ast.Variable x wenzelm@42245: | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi)) wenzelm@42245: | ast_of (t as _ $ _) = wenzelm@42245: let val (f, args) = strip_comb t wenzelm@42245: in Ast.mk_appl (ast_of f) (map ast_of args) end wenzelm@42408: | ast_of (Bound i) = Ast.Appl [Ast.Constant "_loose", Ast.Variable ("B." ^ string_of_int i)] wenzelm@42245: | ast_of (Abs _) = raise Fail "simple_ast_of: Abs"; wenzelm@42245: in ast_of end; wenzelm@42245: wenzelm@42245: wenzelm@42245: (* sort_to_ast and typ_to_ast *) wenzelm@42245: wenzelm@42245: fun ast_of_termT ctxt trf tm = wenzelm@42245: let wenzelm@42245: val ctxt' = Config.put show_sorts false ctxt; wenzelm@42245: fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t wenzelm@42245: | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t wenzelm@42245: | ast_of (Const (a, _)) = trans a [] wenzelm@42245: | ast_of (t as _ $ _) = wenzelm@42245: (case strip_comb t of wenzelm@42245: (Const (a, _), args) => trans a args wenzelm@42245: | (f, args) => Ast.Appl (map ast_of (f :: args))) wenzelm@42245: | ast_of t = simple_ast_of ctxt t wenzelm@42254: and trans a args = ast_of (trf a ctxt' dummyT args) wenzelm@42254: handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); wenzelm@42245: in ast_of tm end; wenzelm@42245: wenzelm@42245: fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (term_of_sort S); wenzelm@42247: fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (term_of_typ ctxt T); wenzelm@42245: wenzelm@42245: wenzelm@42245: (* term_to_ast *) wenzelm@42245: wenzelm@42252: fun term_to_ast idents is_syntax_const ctxt trf tm = wenzelm@42245: let wenzelm@42245: val show_types = wenzelm@42245: Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse wenzelm@42245: Config.get ctxt show_all_types; wenzelm@42245: val show_structs = Config.get ctxt show_structs; wenzelm@42245: val show_free_types = Config.get ctxt show_free_types; wenzelm@42245: val show_all_types = Config.get ctxt show_all_types; wenzelm@42245: wenzelm@42245: val {structs, fixes} = idents; wenzelm@42245: wenzelm@42249: fun mark_atoms ((t as Const (c, _)) $ u) = wenzelm@42294: if member (op =) Syntax.token_markers c wenzelm@42245: then t $ u else mark_atoms t $ mark_atoms u wenzelm@42245: | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u wenzelm@42245: | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t) wenzelm@42245: | mark_atoms (t as Const (c, T)) = wenzelm@42252: if is_syntax_const c then t wenzelm@42245: else Const (Lexicon.mark_const c, T) wenzelm@42245: | mark_atoms (t as Free (x, T)) = wenzelm@42245: let val i = find_index (fn s => s = x) structs + 1 in wenzelm@42245: if i = 0 andalso member (op =) fixes x then wenzelm@42245: Const (Lexicon.mark_fixed x, T) wenzelm@42245: else if i = 1 andalso not show_structs then wenzelm@42476: Syntax.const "_struct" $ Syntax.const "_indexdefault" wenzelm@42476: else Syntax.const "_free" $ t wenzelm@42245: end wenzelm@42245: | mark_atoms (t as Var (xi, T)) = wenzelm@42288: if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T) wenzelm@42476: else Syntax.const "_var" $ t wenzelm@42245: | mark_atoms a = a; wenzelm@42245: wenzelm@42245: fun prune_typs (t_seen as (Const _, _)) = t_seen wenzelm@42245: | prune_typs (t as Free (x, ty), seen) = wenzelm@42245: if ty = dummyT then (t, seen) wenzelm@42290: else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen) wenzelm@42245: else (t, t :: seen) wenzelm@42245: | prune_typs (t as Var (xi, ty), seen) = wenzelm@42245: if ty = dummyT then (t, seen) wenzelm@42290: else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen) wenzelm@42245: else (t, t :: seen) wenzelm@42245: | prune_typs (t_seen as (Bound _, _)) = t_seen wenzelm@42245: | prune_typs (Abs (x, ty, t), seen) = wenzelm@42245: let val (t', seen') = prune_typs (t, seen); wenzelm@42245: in (Abs (x, ty, t'), seen') end wenzelm@42245: | prune_typs (t1 $ t2, seen) = wenzelm@42245: let wenzelm@42245: val (t1', seen') = prune_typs (t1, seen); wenzelm@42245: val (t2', seen'') = prune_typs (t2, seen'); wenzelm@42245: in (t1' $ t2', seen'') end; wenzelm@42245: wenzelm@42245: fun ast_of tm = wenzelm@42245: (case strip_comb tm of wenzelm@42284: (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts) wenzelm@42245: | ((c as Const ("_free", _)), Free (x, T) :: ts) => wenzelm@42290: Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) wenzelm@42245: | ((c as Const ("_var", _)), Var (xi, T) :: ts) => wenzelm@42290: Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts) wenzelm@42245: | ((c as Const ("_bound", _)), Free (x, T) :: ts) => wenzelm@42290: Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts) wenzelm@42245: | (Const ("_idtdummy", T), ts) => wenzelm@42476: Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts) wenzelm@42245: | (const as Const (c, T), ts) => wenzelm@42245: if show_all_types wenzelm@42245: then Ast.mk_appl (constrain const T) (map ast_of ts) wenzelm@42245: else trans c T ts wenzelm@42245: | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts)) wenzelm@42245: wenzelm@42254: and trans a T args = ast_of (trf a ctxt T args) wenzelm@42254: handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) wenzelm@42245: wenzelm@42245: and constrain t T = wenzelm@42245: if show_types andalso T <> dummyT then wenzelm@42248: Ast.Appl [Ast.Constant "_constrain", simple_ast_of ctxt t, wenzelm@42247: ast_of_termT ctxt trf (term_of_typ ctxt T)] wenzelm@42245: else simple_ast_of ctxt t; wenzelm@42245: in wenzelm@42245: tm wenzelm@42284: |> Syntax_Trans.prop_tr' wenzelm@42245: |> show_types ? (#1 o prune_typs o rpair []) wenzelm@42245: |> mark_atoms wenzelm@42245: |> ast_of wenzelm@42245: end; wenzelm@42245: wenzelm@42245: wenzelm@42245: wenzelm@42242: (** unparse **) wenzelm@42242: wenzelm@42245: local wenzelm@42245: wenzelm@42267: fun free_or_skolem ctxt x = wenzelm@42267: let wenzelm@42267: val m = wenzelm@42267: if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt wenzelm@45666: then Isabelle_Markup.fixed x wenzelm@45666: else Isabelle_Markup.hilite; wenzelm@42267: in wenzelm@42267: if can Name.dest_skolem x wenzelm@45666: then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x) wenzelm@45666: else ([m, Isabelle_Markup.free], x) wenzelm@42267: end; wenzelm@42267: wenzelm@42267: fun var_or_skolem s = wenzelm@42267: (case Lexicon.read_variable s of wenzelm@42267: SOME (x, i) => wenzelm@42267: (case try Name.dest_skolem x of wenzelm@45666: NONE => (Isabelle_Markup.var, s) wenzelm@45666: | SOME x' => (Isabelle_Markup.skolem, Term.string_of_vname (x', i))) wenzelm@45666: | NONE => (Isabelle_Markup.var, s)); wenzelm@42267: wenzelm@42267: fun unparse_t t_to_ast prt_t markup ctxt t = wenzelm@42245: let wenzelm@42360: val syn = Proof_Context.syn_of ctxt; wenzelm@42267: wenzelm@45666: fun token_trans "_tfree" x = SOME (Pretty.mark_str (Isabelle_Markup.tfree, x)) wenzelm@45666: | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x)) wenzelm@42267: | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x)) wenzelm@45666: | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x)) wenzelm@45666: | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x)) wenzelm@42267: | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x)) wenzelm@45666: | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x)) wenzelm@45666: | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x)) wenzelm@42267: | token_trans _ _ = NONE; wenzelm@42267: wenzelm@42301: fun markup_extern c = wenzelm@42301: (case Syntax.lookup_const syn c of wenzelm@42301: SOME "" => ([], c) wenzelm@42301: | SOME b => markup_extern b wenzelm@42301: | NONE => c |> Lexicon.unmark wenzelm@43548: {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x), wenzelm@43552: case_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x), wenzelm@43552: case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x), wenzelm@42301: case_fixed = fn x => free_or_skolem ctxt x, wenzelm@42301: case_default = fn x => ([], x)}); wenzelm@42245: in wenzelm@42255: t_to_ast ctxt (Syntax.print_translation syn) t wenzelm@42255: |> Ast.normalize ctxt (Syntax.print_rules syn) wenzelm@42267: |> prt_t ctxt (Syntax.prtabs syn) (Syntax.print_ast_translation syn) token_trans markup_extern wenzelm@42253: |> Pretty.markup markup wenzelm@42245: end; wenzelm@42245: wenzelm@42245: in wenzelm@42245: wenzelm@45666: val unparse_sort = unparse_t sort_to_ast Printer.pretty_typ_ast Isabelle_Markup.sort; wenzelm@45666: val unparse_typ = unparse_t typ_to_ast Printer.pretty_typ_ast Isabelle_Markup.typ; wenzelm@42241: wenzelm@42241: fun unparse_term ctxt = wenzelm@42241: let wenzelm@42360: val thy = Proof_Context.theory_of ctxt; wenzelm@42360: val syn = Proof_Context.syn_of ctxt; wenzelm@42360: val idents = Local_Syntax.idents_of (Proof_Context.syntax_of ctxt); wenzelm@42241: in wenzelm@42298: unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn)) wenzelm@42267: (Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy))) wenzelm@45666: Isabelle_Markup.term ctxt wenzelm@42241: end; wenzelm@42241: wenzelm@42249: end; wenzelm@42249: wenzelm@42241: wenzelm@42245: wenzelm@42245: (** translations **) wenzelm@42245: wenzelm@42245: (* type propositions *) wenzelm@42245: wenzelm@42247: fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] = wenzelm@42476: Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T wenzelm@42247: | type_prop_tr' ctxt T [t] = wenzelm@42476: Syntax.const "_ofclass" $ term_of_typ ctxt T $ t wenzelm@42245: | type_prop_tr' _ T ts = raise TYPE ("type_prop_tr'", [T], ts); wenzelm@42245: wenzelm@42245: wenzelm@42245: (* type reflection *) wenzelm@42245: wenzelm@42247: fun type_tr' ctxt (Type ("itself", [T])) ts = wenzelm@42476: Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts) wenzelm@42245: | type_tr' _ _ _ = raise Match; wenzelm@42245: wenzelm@42245: wenzelm@42245: (* type constraints *) wenzelm@42245: wenzelm@42247: fun type_constraint_tr' ctxt (Type ("fun", [T, _])) (t :: ts) = wenzelm@42476: Term.list_comb (Syntax.const "_constrain" $ t $ term_of_typ ctxt T, ts) wenzelm@42245: | type_constraint_tr' _ _ _ = raise Match; wenzelm@42245: wenzelm@42245: wenzelm@42295: (* authentic syntax *) wenzelm@42295: wenzelm@42295: fun const_ast_tr intern ctxt [Ast.Variable c] = wenzelm@42295: let wenzelm@42360: val Const (c', _) = Proof_Context.read_const_proper ctxt false c; wenzelm@42295: val d = if intern then Lexicon.mark_const c' else c; wenzelm@42295: in Ast.Constant d end wenzelm@42470: | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T as Ast.Variable pos]] = wenzelm@42470: (Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T] wenzelm@42470: handle ERROR msg => wenzelm@42470: error (msg ^ Position.str_of (the_default Position.none (Term_Position.decode pos)))) wenzelm@42295: | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts); wenzelm@42295: wenzelm@42295: wenzelm@42245: (* setup translations *) wenzelm@42245: wenzelm@42245: val _ = Context.>> (Context.map_theory wenzelm@42295: (Sign.add_advanced_trfuns wenzelm@42295: ([("_context_const", const_ast_tr true), wenzelm@42295: ("_context_xconst", const_ast_tr false)], [], [], []) #> wenzelm@42295: Sign.add_advanced_trfunsT wenzelm@42245: [("_type_prop", type_prop_tr'), wenzelm@42245: ("\\<^const>TYPE", type_tr'), wenzelm@42245: ("_type_constraint_", type_constraint_tr')])); wenzelm@42245: wenzelm@42245: wenzelm@42245: wenzelm@42382: (** check/uncheck **) wenzelm@42382: wenzelm@45429: (* context-sensitive (un)checking *) wenzelm@45429: wenzelm@45429: type key = int * bool; wenzelm@45429: wenzelm@45429: structure Checks = Generic_Data wenzelm@45429: ( wenzelm@45429: type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option; wenzelm@45429: type T = wenzelm@45429: ((key * ((string * typ check) * stamp) list) list * wenzelm@45429: (key * ((string * term check) * stamp) list) list); wenzelm@45429: val empty = ([], []); wenzelm@45429: val extend = I; wenzelm@45429: fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T = wenzelm@45429: (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2), wenzelm@45429: AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2)); wenzelm@45429: ); wenzelm@45429: wenzelm@45429: fun print_checks ctxt = wenzelm@45429: let wenzelm@45429: fun split_checks checks = wenzelm@45429: List.partition (fn ((_, un), _) => not un) checks wenzelm@45429: |> pairself (map (fn ((i, _), fs) => (i, map (fst o fst) fs)) wenzelm@45429: #> sort (int_ord o pairself fst)); wenzelm@45429: fun pretty_checks kind checks = wenzelm@45429: checks |> map (fn (i, names) => Pretty.block wenzelm@45429: [Pretty.str (kind ^ " (stage " ^ signed_string_of_int i ^ "):"), wenzelm@45429: Pretty.brk 1, Pretty.strs names]); wenzelm@45429: wenzelm@45429: val (typs, terms) = Checks.get (Context.Proof ctxt); wenzelm@45429: val (typ_checks, typ_unchecks) = split_checks typs; wenzelm@45429: val (term_checks, term_unchecks) = split_checks terms; wenzelm@45429: in wenzelm@45429: pretty_checks "typ_checks" typ_checks @ wenzelm@45429: pretty_checks "term_checks" term_checks @ wenzelm@45429: pretty_checks "typ_unchecks" typ_unchecks @ wenzelm@45429: pretty_checks "term_unchecks" term_unchecks wenzelm@45429: end |> Pretty.chunks |> Pretty.writeln; wenzelm@45429: wenzelm@45429: wenzelm@45429: local wenzelm@45429: wenzelm@45429: fun context_check which (key: key) name f = wenzelm@45429: Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ())))); wenzelm@45429: wenzelm@45429: fun simple_check eq f xs ctxt = wenzelm@45429: let val xs' = f ctxt xs wenzelm@45429: in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end; wenzelm@45429: wenzelm@45429: in wenzelm@45429: wenzelm@45444: fun typ_check' stage = context_check apfst (stage, false); wenzelm@45444: fun term_check' stage = context_check apsnd (stage, false); wenzelm@45444: fun typ_uncheck' stage = context_check apfst (stage, true); wenzelm@45444: fun term_uncheck' stage = context_check apsnd (stage, true); wenzelm@45429: wenzelm@45444: fun typ_check key name f = typ_check' key name (simple_check (op =) f); wenzelm@45444: fun term_check key name f = term_check' key name (simple_check (op aconv) f); wenzelm@45444: fun typ_uncheck key name f = typ_uncheck' key name (simple_check (op =) f); wenzelm@45444: fun term_uncheck key name f = term_uncheck' key name (simple_check (op aconv) f); wenzelm@45429: wenzelm@45429: end; wenzelm@45429: wenzelm@45429: wenzelm@45429: local wenzelm@45429: wenzelm@45429: fun check_stage fs = perhaps_loop (perhaps_apply (map uncurry fs)); wenzelm@45429: fun check_all fs = perhaps_apply (map check_stage fs); wenzelm@45429: wenzelm@45429: fun check which uncheck ctxt0 xs0 = wenzelm@45429: let wenzelm@45429: val funs = which (Checks.get (Context.Proof ctxt0)) wenzelm@45429: |> map_filter (fn ((i, u), fs) => if uncheck = u then SOME (i, map (snd o fst) fs) else NONE) wenzelm@45429: |> Library.sort (int_ord o pairself fst) |> map snd wenzelm@45429: |> not uncheck ? map rev; wenzelm@45429: in #1 (perhaps (check_all funs) (xs0, ctxt0)) end; wenzelm@45429: wenzelm@45429: val apply_typ_check = check fst false; wenzelm@45429: val apply_term_check = check snd false; wenzelm@45429: val apply_typ_uncheck = check fst true; wenzelm@45429: val apply_term_uncheck = check snd true; wenzelm@45429: wenzelm@45429: in wenzelm@45429: wenzelm@45423: fun check_typs ctxt = wenzelm@45453: Proof_Context.prepare_sorts ctxt #> wenzelm@45429: apply_typ_check ctxt #> wenzelm@45427: Term_Sharing.typs (Proof_Context.theory_of ctxt); wenzelm@45423: wenzelm@45445: fun check_terms ctxt raw_ts = wenzelm@45445: let wenzelm@45448: val (ts, ps) = raw_ts wenzelm@45453: |> Term.burrow_types (Proof_Context.prepare_sorts ctxt) wenzelm@45448: |> Type_Infer_Context.prepare_positions ctxt; wenzelm@45445: val tys = map (Logic.mk_type o snd) ps; wenzelm@45448: val (ts', tys') = ts @ tys wenzelm@45445: |> apply_term_check ctxt wenzelm@45445: |> chop (length ts); wenzelm@45445: val _ = wenzelm@45445: map2 (fn (pos, _) => fn ty => wenzelm@45445: if Position.is_reported pos then wenzelm@45666: Markup.markup (Position.markup pos Isabelle_Markup.typing) wenzelm@45445: (Syntax.string_of_typ ctxt (Logic.dest_type ty)) wenzelm@45445: else "") ps tys' wenzelm@45445: |> implode |> Output.report wenzelm@45445: in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; wenzelm@45423: wenzelm@42382: fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt; wenzelm@42382: wenzelm@45429: val uncheck_typs = apply_typ_uncheck; wenzelm@45429: val uncheck_terms = apply_term_uncheck; wenzelm@45429: wenzelm@45429: end; wenzelm@45429: wenzelm@45429: wenzelm@45429: (* standard phases *) wenzelm@45429: wenzelm@45429: val _ = Context.>> wenzelm@45429: (typ_check 0 "standard" Proof_Context.standard_typ_check #> wenzelm@45429: term_check 0 "standard" wenzelm@45429: (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #> wenzelm@45429: term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #> wenzelm@45429: term_uncheck 0 "standard" Proof_Context.standard_term_uncheck); wenzelm@42382: wenzelm@42382: wenzelm@42382: wenzelm@42242: (** install operations **) wenzelm@42242: wenzelm@42241: val _ = Syntax.install_operations wenzelm@42241: {parse_sort = parse_sort, wenzelm@42241: parse_typ = parse_typ, wenzelm@42281: parse_term = parse_term false, wenzelm@42281: parse_prop = parse_term true, wenzelm@42241: unparse_sort = unparse_sort, wenzelm@42241: unparse_typ = unparse_typ, wenzelm@42382: unparse_term = unparse_term, wenzelm@42382: check_typs = check_typs, wenzelm@42382: check_terms = check_terms, wenzelm@42382: check_props = check_props, wenzelm@42382: uncheck_typs = uncheck_typs, wenzelm@42382: uncheck_terms = uncheck_terms}; wenzelm@42241: wenzelm@42241: end;