diff --git a/src/Pure/Isar/keyword.ML b/src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML +++ b/src/Pure/Isar/keyword.ML @@ -1,288 +1,292 @@ (* Title: Pure/Isar/keyword.ML Author: Makarius Isar keyword classification. *) signature KEYWORD = sig val diag: string val document_heading: string val document_body: string val document_raw: string val thy_begin: string val thy_end: string val thy_decl: string val thy_decl_block: string val thy_defn: string val thy_stmt: string val thy_load: string val thy_goal: string val thy_goal_defn: string val thy_goal_stmt: string val qed: string val qed_script: string val qed_block: string val qed_global: string val prf_goal: string val prf_block: string val next_block: string val prf_open: string val prf_close: string val prf_chain: string val prf_decl: string val prf_asm: string val prf_asm_goal: string val prf_script: string val prf_script_goal: string val prf_script_asm_goal: string val before_command: string val quasi_command: string type spec = string * string list val no_spec: spec val before_command_spec: spec val quasi_command_spec: spec val document_heading_spec: spec val document_body_spec: spec type keywords val minor_keywords: keywords -> Scan.lexicon val major_keywords: keywords -> Scan.lexicon val no_command_keywords: keywords -> keywords val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords val add_minor_keywords: string list -> keywords -> keywords + val add_major_keywords: string list -> keywords -> keywords val is_keyword: keywords -> string -> bool val is_command: keywords -> string -> bool val is_literal: keywords -> string -> bool val dest_commands: keywords -> string list val command_markup: keywords -> string -> Markup.T option val command_kind: keywords -> string -> string option val command_tags: keywords -> string -> string list val is_vacuous: keywords -> string -> bool val is_diag: keywords -> string -> bool val is_document_heading: keywords -> string -> bool val is_document_body: keywords -> string -> bool val is_document_raw: keywords -> string -> bool val is_document: keywords -> string -> bool val is_theory_end: keywords -> string -> bool val is_theory_load: keywords -> string -> bool val is_theory: keywords -> string -> bool val is_theory_body: keywords -> string -> bool val is_proof: keywords -> string -> bool val is_proof_body: keywords -> string -> bool val is_theory_goal: keywords -> string -> bool val is_proof_goal: keywords -> string -> bool val is_qed: keywords -> string -> bool val is_qed_global: keywords -> string -> bool val is_proof_open: keywords -> string -> bool val is_proof_close: keywords -> string -> bool val is_proof_asm: keywords -> string -> bool val is_improper: keywords -> string -> bool val is_printed: keywords -> string -> bool end; structure Keyword: KEYWORD = struct (** keyword classification **) (* kinds *) val diag = "diag"; val document_heading = "document_heading"; val document_body = "document_body"; val document_raw = "document_raw"; val thy_begin = "thy_begin"; val thy_end = "thy_end"; val thy_decl = "thy_decl"; val thy_decl_block = "thy_decl_block"; val thy_defn = "thy_defn"; val thy_stmt = "thy_stmt"; val thy_load = "thy_load"; val thy_goal = "thy_goal"; val thy_goal_defn = "thy_goal_defn"; val thy_goal_stmt = "thy_goal_stmt"; val qed = "qed"; val qed_script = "qed_script"; val qed_block = "qed_block"; val qed_global = "qed_global"; val prf_goal = "prf_goal"; val prf_block = "prf_block"; val next_block = "next_block"; val prf_open = "prf_open"; val prf_close = "prf_close"; val prf_chain = "prf_chain"; val prf_decl = "prf_decl"; val prf_asm = "prf_asm"; val prf_asm_goal = "prf_asm_goal"; val prf_script = "prf_script"; val prf_script_goal = "prf_script_goal"; val prf_script_asm_goal = "prf_script_asm_goal"; val before_command = "before_command"; val quasi_command = "quasi_command"; val command_kinds = [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; (* specifications *) type spec = string * string list; val no_spec: spec = ("", []); val before_command_spec: spec = (before_command, []); val quasi_command_spec: spec = (quasi_command, []); val document_heading_spec: spec = ("document_heading", ["document"]); val document_body_spec: spec = ("document_body", ["document"]); type entry = {pos: Position.T, id: serial, kind: string, tags: string list}; fun check_spec pos (kind, tags) : entry = if not (member (op =) command_kinds kind) then error ("Unknown outer syntax keyword kind " ^ quote kind) else {pos = pos, id = serial (), kind = kind, tags = tags}; (** keyword tables **) (* type keywords *) datatype keywords = Keywords of {minor: Scan.lexicon, major: Scan.lexicon, commands: entry Symtab.table}; fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; fun make_keywords (minor, major, commands) = Keywords {minor = minor, major = major, commands = commands}; fun map_keywords f (Keywords {minor, major, commands}) = make_keywords (f (minor, major, commands)); val no_command_keywords = map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); (* build keywords *) val empty_keywords = make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); fun merge_keywords (Keywords {minor = minor1, major = major1, commands = commands1}, Keywords {minor = minor2, major = major2, commands = commands2}) = make_keywords (Scan.merge_lexicons (minor1, minor2), Scan.merge_lexicons (major1, major2), Symtab.merge (K true) (commands1, commands2)); val add_keywords = fold (fn ((name, pos), spec as (kind, _)) => map_keywords (fn (minor, major, commands) => if kind = "" orelse kind = before_command orelse kind = quasi_command then let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in (minor', major, commands) end else let val entry = check_spec pos spec; val major' = Scan.extend_lexicon (Symbol.explode name) major; val commands' = Symtab.update (name, entry) commands; in (minor, major', commands') end)); val add_minor_keywords = add_keywords o map (fn name => ((name, Position.none), no_spec)); +val add_major_keywords = + add_keywords o map (fn name => ((name, Position.none), (diag, []))); + (* keyword status *) fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); fun is_command (Keywords {commands, ...}) = Symtab.defined commands; fun is_literal keywords = is_keyword keywords orf is_command keywords; fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; (* command keywords *) fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; fun command_markup keywords name = lookup_command keywords name |> Option.map (fn {pos, id, ...} => Position.make_entity_markup {def = false} id Markup.command_keywordN (name, pos)); fun command_kind keywords = Option.map #kind o lookup_command keywords; fun command_tags keywords name = (case lookup_command keywords name of SOME {tags, ...} => tags | NONE => []); (* command categories *) fun command_category ks = let val tab = Symtab.make_set ks; fun pred keywords name = (case lookup_command keywords name of NONE => false | SOME {kind, ...} => Symtab.defined tab kind); in pred end; val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; val is_diag = command_category [diag]; val is_document_heading = command_category [document_heading]; val is_document_body = command_category [document_body]; val is_document_raw = command_category [document_raw]; val is_document = command_category [document_heading, document_body, document_raw]; val is_theory_end = command_category [thy_end]; val is_theory_load = command_category [thy_load]; val is_theory = command_category [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_theory_body = command_category [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof = command_category [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_proof_body = command_category [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; val is_proof_open = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; val is_proof_asm = command_category [prf_asm, prf_asm_goal]; val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; end; diff --git a/src/Pure/ML/ml_antiquotations.ML b/src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML +++ b/src/Pure/ML/ml_antiquotations.ML @@ -1,467 +1,608 @@ (* Title: Pure/ML/ml_antiquotations.ML Author: Makarius Miscellaneous ML antiquotations. *) signature ML_ANTIQUOTATIONS = sig val make_judgment: Proof.context -> term -> term val dest_judgment: Proof.context -> term -> term + type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list + type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + val instantiate_typ: insts -> typ -> typ + val instantiate_ctyp: cinsts -> ctyp -> ctyp + val instantiate_term: insts -> term -> term + val instantiate_cterm: cinsts -> cterm -> cterm end; structure ML_Antiquotations: ML_ANTIQUOTATIONS = struct (* ML support *) val _ = Theory.setup (ML_Antiquotation.inline \<^binding>\undefined\ (Scan.succeed "(raise General.Match)") #> ML_Antiquotation.inline \<^binding>\assert\ (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> ML_Antiquotation.declaration_embedded \<^binding>\print\ (Scan.lift (Scan.optional Parse.embedded "Output.writeln")) (fn src => fn output => fn ctxt => let val struct_name = ML_Context.struct_name ctxt; val (_, pos) = Token.name_of_src src; val (a, ctxt') = ML_Context.variant "output" ctxt; val env = "val " ^ a ^ ": string -> unit =\n\ \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ ML_Syntax.print_position pos ^ "));\n"; val body = "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; in (K (env, body), ctxt') end) #> ML_Antiquotation.value \<^binding>\rat\ (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); (* formal entities *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\system_option\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> ML_Antiquotation.value_embedded \<^binding>\theory\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) || Scan.succeed "Proof_Context.theory_of ML_context") #> ML_Antiquotation.value_embedded \<^binding>\theory_context\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (Theory.check {long = false} ctxt (name, pos); "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))) #> ML_Antiquotation.inline \<^binding>\context\ (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> ML_Antiquotation.inline_embedded \<^binding>\typ\ (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> ML_Antiquotation.inline_embedded \<^binding>\term\ (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.inline_embedded \<^binding>\prop\ (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); (* schematic variables *) val schematic_input = Args.context -- Scan.lift Parse.embedded_input >> (fn (ctxt, src) => (Proof_Context.set_mode Proof_Context.mode_schematic ctxt, (Syntax.implode_input src, Input.pos_of src))); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\tvar\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_typ ctxt s of TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> ML_Antiquotation.inline_embedded \<^binding>\var\ (schematic_input >> (fn (ctxt, (s, pos)) => (case Syntax.read_term ctxt s of Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v | _ => error ("Schematic variable expected" ^ Position.here pos))))); (* type classes *) fun class syn = Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => Proof_Context.read_class ctxt s |> syn ? Lexicon.mark_class |> ML_Syntax.print_string); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> ML_Antiquotation.inline_embedded \<^binding>\sort\ (Args.context -- Scan.lift Parse.embedded_inner_syntax >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); (* type constructors *) fun type_name kind check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); val res = (case try check (c, decl) of SOME res => res | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\type_name\ (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ (type_name "type" (fn (c, _) => Lexicon.mark_type c))); (* constants *) fun const_name check = Args.context -- Scan.lift (Parse.token Parse.embedded) >> (fn (ctxt, tok) => let val s = Token.inner_syntax_of tok; val (_, pos) = Input.source_content (Token.input_of tok); val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; val res = check (Proof_Context.consts_of ctxt, c) handle TYPE (msg, _, _) => error (msg ^ Position.here pos); in ML_Syntax.print_string res end); val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\const_name\ (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ (const_name (fn (_, c) => Lexicon.mark_const c)) #> ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> ML_Antiquotation.inline_embedded \<^binding>\const\ (Args.context -- Scan.lift (Parse.position Parse.embedded_inner_syntax) -- Scan.optional (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] >> (fn ((ctxt, (raw_c, pos)), Ts) => let val Const (c, _) = Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; val consts = Proof_Context.consts_of ctxt; val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); val _ = length Ts <> n andalso error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); val const = Const (c, Consts.instance consts (c, Ts)); in ML_Syntax.atomic (ML_Syntax.print_term const) end))); (* object-logic judgment *) fun make_judgment ctxt = let val const = Object_Logic.judgment_const ctxt in fn t => Const const $ t end; fun dest_judgment ctxt = let val is_judgment = Object_Logic.is_judgment ctxt; val drop_judgment = Object_Logic.drop_judgment ctxt; in fn t => if is_judgment t then drop_judgment t else raise TERM ("dest_judgment", [t]) end; val _ = Theory.setup (ML_Antiquotation.value \<^binding>\make_judgment\ (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #> ML_Antiquotation.value \<^binding>\dest_judgment\ (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); -(* type/term constructors *) +(* type/term instantiations and constructors *) + +type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list +type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list + +fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts)); +fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts)); + +fun instantiate_term (insts: insts) = + let + val instT = TVars.make (#1 insts); + val instantiateT = Term_Subst.instantiateT instT; + val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts)); + in Term_Subst.instantiate (instT, inst) end; + +fun instantiate_cterm (cinsts: cinsts) = + let + val cinstT = TVars.make (#1 cinsts); + val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT); + val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts)); + in Thm.instantiate_cterm (cinstT, cinst) end; + + +local + +fun make_keywords ctxt = + Thy_Header.get_keywords' ctxt + |> Keyword.no_command_keywords + |> Keyword.add_major_keywords ["typ", "term", "prop", "ctyp", "cterm", "cprop"]; + +val parse_inst = + Parse.position (Parse.type_ident >> pair true || Parse.name >> pair false) -- + (Parse.$$$ "=" |-- Parse.!!! Parse.embedded_ml) >> (fn (((b, a), pos), ml) => (b, ((a, pos), ml))); + +val parse_insts = + Parse.and_list1 parse_inst >> (List.partition #1 #> apply2 (map #2)); + +val ml = ML_Lex.tokenize_no_range; +val ml_range = ML_Lex.tokenize_range; +fun ml_parens x = ml "(" @ x @ ml ")"; +fun ml_bracks x = ml "[" @ x @ ml "]"; +fun ml_commas xs = flat (separate (ml ", ") xs); +val ml_list = ml_bracks o ml_commas; +fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); +val ml_list_pair = ml_list o ListPair.map ml_pair; + +fun get_tfree envT (a, pos) = + (case AList.lookup (op =) envT a of + SOME S => (a, S) + | NONE => error ("Unused type variable " ^ quote a ^ Position.here pos)); + +fun get_free env (x, pos) = + (case AList.lookup (op =) env x of + SOME T => (x, T) + | NONE => error ("Unused variable " ^ quote x ^ Position.here pos)); + +fun make_instT (a, pos) T = + (case try (Term.dest_TVar o Logic.dest_type) T of + NONE => error ("Not a free type variable " ^ quote a ^ Position.here pos) + | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v)); + +fun make_inst (a, pos) t = + (case try Term.dest_Var t of + NONE => error ("Not a free variable " ^ quote a ^ Position.here pos) + | SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v)); + +fun prepare_insts ctxt1 ctxt0 (instT, inst) t = + let + val envT = Term.add_tfrees t []; + val env = Term.add_frees t []; + val freesT = map (Logic.mk_type o TFree o get_tfree envT) instT; + val frees = map (Free o get_free env) inst; + val (t' :: varsT, vars) = + Variable.export_terms ctxt1 ctxt0 (t :: freesT @ frees) + |> chop (1 + length freesT); + val ml_insts = (map2 make_instT instT varsT, map2 make_inst inst vars); + in (ml_insts, t') end; + +fun prepare_ml range (kind, ml1, ml2) ml_val (ml_instT, ml_inst) ctxt = + let + val (ml_name, ctxt') = ML_Context.variant kind ctxt; + val ml_env = ml ("val " ^ ml_name ^ " = ") @ ml ml1 @ ml_parens (ml ml_val) @ ml ";\n"; + fun ml_body (ml_argsT, ml_args) = + ml_parens (ml ml2 @ + ml_pair (ml_list_pair (ml_instT, ml_argsT), ml_list_pair (ml_inst, ml_args)) @ + ml_range range (ML_Context.struct_name ctxt ^ "." ^ ml_name)); + in ((ml_env, ml_body), ctxt') end; + +fun prepare_type range (arg, s) insts ctxt = + let + val T = Syntax.read_typ ctxt s; + val t = Logic.mk_type T; + val ctxt1 = Proof_Context.augment t ctxt; + val (ml_insts, T') = prepare_insts ctxt1 ctxt insts t ||> Logic.dest_type; + in prepare_ml range arg (ML_Syntax.print_typ T') ml_insts ctxt end; + +fun prepare_term read range (arg, (s, fixes)) insts ctxt = + let + val ctxt' = #2 (Proof_Context.add_fixes_cmd fixes ctxt); + val t = read ctxt' s; + val ctxt1 = Proof_Context.augment t ctxt'; + val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t; + in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end; + +fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ"); +fun ctyp_ml kind = (kind, "Thm.ctyp_of ML_context", "ML_Antiquotations.instantiate_ctyp"); +fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term"); +fun cterm_ml kind = (kind, "Thm.cterm_of ML_context", "ML_Antiquotations.instantiate_cterm"); + +fun parse_body range = + (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) -- + Parse.!!! Parse.typ >> prepare_type range || + (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml) + -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range || + (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml) + -- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range; + +val _ = Theory.setup + (ML_Context.add_antiquotation \<^binding>\let\ true + (fn range => fn src => fn ctxt => + let + val (insts, prepare_val) = src + |> Parse.read_embedded_src ctxt (make_keywords ctxt) + ((parse_insts --| Parse.$$$ "in") -- parse_body range); + + val (((ml_env, ml_body), decls), ctxt1) = ctxt + |> prepare_val (apply2 (map #1) insts) + ||>> ML_Context.expand_antiquotes_list (op @ (apply2 (map #2) insts)); + + fun decl' ctxt' = + let val (ml_args_env, ml_args) = split_list (decls ctxt') + in (ml_env @ flat ml_args_env, ml_body (chop (length (#1 insts)) ml_args)) end; + in (decl', ctxt1) end)); + +in end; + local val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; val parse_name = Parse.input Parse.name; val parse_args = Scan.repeat Parse.embedded_ml_underscore; val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) []; fun parse_body b = if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single) else Scan.succeed []; fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" | is_dummy _ = false; val ml = ML_Lex.tokenize_no_range; val ml_range = ML_Lex.tokenize_range; val ml_dummy = ml "_"; fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; fun ml_parens x = ml "(" @ x @ ml ")"; fun ml_bracks x = ml "[" @ x @ ml "]"; fun ml_commas xs = flat (separate (ml ", ") xs); val ml_list = ml_bracks o ml_commas; val ml_string = ml o ML_Syntax.print_string; fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); fun type_antiquotation binding {function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val ((s, type_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function); val pos = Input.pos_of s; val Type (c, Ts) = Proof_Context.read_type_name {proper = true, strict = true} ctxt (Syntax.implode_input s); val n = length Ts; val _ = length type_args = n orelse error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list fn_body ctxt1; fun decl' ctxt' = let val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); val ml1 = ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| T => " @ ml_range range "raise" @ ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") else ml1; in (flat (ml_args_env @ ml_fn_env), ml2) end; in (decl', ctxt2) end); fun const_antiquotation binding {pattern, function} = ML_Context.add_antiquotation binding true (fn range => fn src => fn ctxt => let val (((s, type_args), term_args), fn_body) = src |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_for_args -- parse_body function); val Const (c, T) = Proof_Context.read_const {proper = true, strict = true} ctxt (Syntax.implode_input s); val consts = Proof_Context.consts_of ctxt; val type_paths = Consts.type_arguments consts c; val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); val n = length type_params; val m = length (Term.binder_types T); fun err msg = error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ Position.here (Input.pos_of s)); val _ = length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); val _ = length term_args > m andalso Term.is_Type (Term.body_type T) andalso err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); val (decls1, ctxt1) = ML_Context.expand_antiquotes_list type_args ctxt; val (decls2, ctxt2) = ML_Context.expand_antiquotes_list term_args ctxt1; val (decls3, ctxt3) = ML_Context.expand_antiquotes_list fn_body ctxt2; fun decl' ctxt' = let val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); val relevant = map is_dummy type_args ~~ type_paths; fun relevant_path is = not pattern orelse let val p = rev is in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); fun ml_typ is (Type (d, Us)) = if relevant_path is then ml "Term.Type " @ ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) else ml_dummy | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy | ml_typ _ (TFree _) = raise Match; fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); val ml2 = if function then ml_enclose range (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ ml "| t => " @ ml_range range "raise" @ ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") else ml1; in (ml_env, ml2) end; in (decl', ctxt3) end); val _ = Theory.setup (type_antiquotation \<^binding>\Type\ {function = false} #> type_antiquotation \<^binding>\Type_fn\ {function = true} #> const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); in end; (* special forms *) val _ = Theory.setup (ML_Antiquotation.special_form \<^binding>\try\ "() |> Basics.try" #> ML_Antiquotation.special_form \<^binding>\can\ "() |> Basics.can"); (* basic combinators *) local val parameter = Parse.position Parse.nat >> (fn (n, pos) => if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); fun indices n = map string_of_int (1 upto n); fun empty n = replicate_string n " []"; fun dummy n = replicate_string n " _"; fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); val tuple = enclose "(" ")" o commas; fun tuple_empty n = tuple (replicate n "[]"); fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); in val _ = Theory.setup (ML_Antiquotation.value \<^binding>\map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun map _" ^ empty n ^ " = []\n\ \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ " in map f end")) #> ML_Antiquotation.value \<^binding>\fold\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold _" ^ empty n ^ " a = a\n\ \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold f end")) #> ML_Antiquotation.value \<^binding>\fold_map\ (Scan.lift parameter >> (fn n => "fn f =>\n\ \ let\n\ \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ \ | fold_map f" ^ cons n ^ " a =\n\ \ let\n\ \ val (x, a') = f" ^ vars "x" n ^ " a\n\ \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ \ in (x :: xs, a'') end\n\ \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ " in fold_map f end")) #> ML_Antiquotation.value \<^binding>\split_list\ (Scan.lift parameter >> (fn n => "fn list =>\n\ \ let\n\ \ fun split_list [] =" ^ tuple_empty n ^ "\n\ \ | split_list" ^ tuple_cons n ^ " =\n\ \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ \ in " ^ cons_tuple n ^ "end\n\ \ in split_list list end")) #> ML_Antiquotation.value \<^binding>\apply\ (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> (fn (n, opt_index) => let val cond = (case opt_index of NONE => K true | SOME (index, index_pos) => if 1 <= index andalso index <= n then equal (string_of_int index) else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); in "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) end))); end; (* outer syntax *) val _ = Theory.setup (ML_Antiquotation.value_embedded \<^binding>\keyword\ (Args.context -- Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) >> (fn (ctxt, (name, pos)) => if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); "Parse.$$$ " ^ ML_Syntax.print_string name) else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> ML_Antiquotation.value_embedded \<^binding>\command_keyword\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of SOME markup => (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); end; diff --git a/src/Pure/more_thm.ML b/src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML +++ b/src/Pure/more_thm.ML @@ -1,752 +1,757 @@ (* Title: Pure/more_thm.ML Author: Makarius Further operations on type ctyp/cterm/thm, outside the inference kernel. *) infix aconvc; signature BASIC_THM = sig include BASIC_THM val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val aconvc: cterm * cterm -> bool type attribute = Context.generic * thm -> Context.generic option * thm option end; signature THM = sig include THM val eq_ctyp: ctyp * ctyp -> bool val aconvc: cterm * cterm -> bool val add_tvars: thm -> ctyp TVars.table -> ctyp TVars.table val add_vars: thm -> cterm Vars.table -> cterm Vars.table val dest_funT: ctyp -> ctyp * ctyp val strip_type: ctyp -> ctyp list * ctyp + val instantiate_ctyp: ctyp TVars.table -> ctyp -> ctyp val all_name: Proof.context -> string * cterm -> cterm -> cterm val all: Proof.context -> cterm -> cterm -> cterm val mk_binop: cterm -> cterm -> cterm -> cterm val dest_binop: cterm -> cterm * cterm val dest_implies: cterm -> cterm * cterm val dest_equals: cterm -> cterm * cterm val dest_equals_lhs: cterm -> cterm val dest_equals_rhs: cterm -> cterm val lhs_of: thm -> cterm val rhs_of: thm -> cterm val is_reflexive: thm -> bool val eq_thm: thm * thm -> bool val eq_thm_prop: thm * thm -> bool val eq_thm_strict: thm * thm -> bool val equiv_thm: theory -> thm * thm -> bool val class_triv: theory -> class -> thm val of_sort: ctyp * sort -> thm list val is_dummy: thm -> bool val add_thm: thm -> thm list -> thm list val del_thm: thm -> thm list -> thm list val merge_thms: thm list * thm list -> thm list val item_net: thm Item_Net.T val item_net_intro: thm Item_Net.T val item_net_elim: thm Item_Net.T val declare_hyps: cterm -> Proof.context -> Proof.context val assume_hyps: cterm -> Proof.context -> thm * Proof.context val unchecked_hyps: Proof.context -> Proof.context val restore_hyps: Proof.context -> Proof.context -> Proof.context val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm val forall_intr_name: string * cterm -> thm -> thm val forall_elim_var: int -> thm -> thm val forall_elim_vars: int -> thm -> thm val instantiate_frees: ctyp TFrees.table * cterm Frees.table -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm val forall_intr_frees: thm -> thm val forall_intr_vars: thm -> thm val unvarify_global: theory -> thm -> thm val unvarify_axiom: theory -> string -> thm val rename_params_rule: string list * int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory val add_axiom_global: binding * term -> theory -> (string * thm) * theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory type attribute = Context.generic * thm -> Context.generic option * thm option type binding = binding * attribute list val tag_rule: string * string -> thm -> thm val untag_rule: string -> thm -> thm val is_free_dummy: thm -> bool val tag_free_dummy: thm -> thm val def_name: string -> string val def_name_optional: string -> string -> string val def_binding: Binding.binding -> Binding.binding val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding val make_def_binding: bool -> Binding.binding -> Binding.binding val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic val theory_attributes: attribute list -> thm -> theory -> thm * theory val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag: string * string -> attribute val untag: string -> attribute val kind: string -> attribute val register_proofs: thm list lazy -> theory -> theory val consolidate_theory: theory -> unit val expose_theory: theory -> unit val show_consts: bool Config.T val show_hyps: bool Config.T val show_tags: bool Config.T val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_item: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T val string_of_thm: Proof.context -> thm -> string val string_of_thm_global: theory -> thm -> string end; structure Thm: THM = struct (** basic operations **) (* collecting ctyps and cterms *) val eq_ctyp = op = o apply2 Thm.typ_of; val op aconvc = op aconv o apply2 Thm.term_of; val add_tvars = Thm.fold_atomic_ctyps {hyps = false} Term.is_TVar (fn cT => fn tab => let val v = Term.dest_TVar (Thm.typ_of cT) in tab |> not (TVars.defined tab v) ? TVars.add (v, cT) end); val add_vars = Thm.fold_atomic_cterms {hyps = false} Term.is_Var (fn ct => fn tab => let val v = Term.dest_Var (Thm.term_of ct) in tab |> not (Vars.defined tab v) ? Vars.add (v, ct) end); (* ctyp operations *) fun dest_funT cT = (case Thm.typ_of cT of Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end | T => raise TYPE ("dest_funT", [T], [])); (* ctyp version of strip_type: maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *) fun strip_type cT = (case Thm.typ_of cT of Type ("fun", _) => let val (cT1, cT2) = dest_funT cT; val (cTs, cT') = strip_type cT2 in (cT1 :: cTs, cT') end | _ => ([], cT)); +fun instantiate_ctyp instT cT = + Thm.instantiate_cterm (instT, Vars.empty) (Thm.var (("x", 0), cT)) + |> Thm.ctyp_of_cterm; + (* cterm operations *) fun all_name ctxt (x, t) A = let val T = Thm.typ_of_cterm t; val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT)); in Thm.apply all_const (Thm.lambda_name (x, t) A) end; fun all ctxt t A = all_name ctxt ("", t) A; fun mk_binop c a b = Thm.apply (Thm.apply c a) b; fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); fun dest_implies ct = (case Thm.term_of ct of Const ("Pure.imp", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_implies", [Thm.term_of ct])); fun dest_equals ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => dest_binop ct | _ => raise TERM ("dest_equals", [Thm.term_of ct])); fun dest_equals_lhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); fun dest_equals_rhs ct = (case Thm.term_of ct of Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); val lhs_of = dest_equals_lhs o Thm.cprop_of; val rhs_of = dest_equals_rhs o Thm.cprop_of; (* equality *) fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) handle TERM _ => false; val eq_thm = is_equal o Thm.thm_ord; val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; fun eq_thm_strict ths = eq_thm ths andalso Context.eq_thy_id (apply2 Thm.theory_id ths) andalso op = (apply2 Thm.maxidx_of ths) andalso op = (apply2 Thm.get_tags ths); (* pattern equivalence *) fun equiv_thm thy ths = Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); (* type classes and sorts *) fun class_triv thy c = Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; (* misc operations *) fun is_dummy thm = (case try Logic.dest_term (Thm.concl_of thm) of NONE => false | SOME t => Term.is_dummy_pattern (Term.head_of t)); (* collections of theorems in canonical order *) val add_thm = update eq_thm_prop; val del_thm = remove eq_thm_prop; val merge_thms = merge eq_thm_prop; val item_net = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); val item_net_intro = Item_Net.init eq_thm_prop (single o Thm.concl_of); val item_net_elim = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); (** declared hyps and sort hyps **) structure Hyps = Proof_Data ( type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); (* hyps *) fun declare_hyps raw_ct ctxt = ctxt |> map_hyps (fn (checked_hyps, hyps, shyps) => let val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; in (checked_hyps, hyps', shyps) end); fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); fun restore_hyps ctxt = map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); fun undeclared_hyps context th = Thm.hyps_of th |> filter_out (case context of Context.Theory _ => K false | Context.Proof ctxt => (case Hyps.get ctxt of {checked_hyps = false, ...} => K true | {hyps, ...} => Termtab.defined hyps)); fun check_hyps context th = (case undeclared_hyps context th of [] => th | undeclared => error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" (map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); (* shyps *) fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; (** basic derived rules **) (*Elimination of implication A A \ B ------------ B *) fun elim_implies thA thAB = Thm.implies_elim thAB thA; (* forall_intr_name *) fun forall_intr_name (a, x) th = let val th' = Thm.forall_intr x th; val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); in Thm.renamed_prop prop' th' end; (* forall_elim_var(s) *) local val used_frees = Name.build_context o Thm.fold_terms {hyps = true} Term.declare_term_frees; fun used_vars i = Name.build_context o (Thm.fold_terms {hyps = false} o Term.fold_aterms) (fn Var ((x, j), _) => i = j ? Name.declare x | _ => I); fun dest_all ct used = (case Thm.term_of ct of Const ("Pure.all", _) $ Abs (x, _, _) => let val (x', used') = Name.variant x used; val (v, ct') = Thm.dest_abs_fresh x' (Thm.dest_arg ct); in SOME ((x, Thm.ctyp_of_cterm v), (ct', used')) end | _ => NONE); fun dest_all_list ct used = (case dest_all ct used of NONE => ([], used) | SOME (v, (ct', used')) => let val (vs, used'') = dest_all_list ct' used' in (v :: vs, used'') end); fun forall_elim_vars_list vars i th = let val (vars', _) = (vars, used_vars i th) |-> fold_map (fn (x, T) => fn used => let val (x', used') = Name.variant x used in (Thm.var ((x', i), T), used') end); in fold Thm.forall_elim vars' th end; in fun forall_elim_vars i th = forall_elim_vars_list (#1 (dest_all_list (Thm.cprop_of th) (used_frees th))) i th; fun forall_elim_var i th = let val vars = (case dest_all (Thm.cprop_of th) (used_frees th) of SOME (v, _) => [v] | NONE => raise THM ("forall_elim_var", i, [th])); in forall_elim_vars_list vars i th end; end; (* instantiate frees *) fun instantiate_frees (instT, inst) th = if TFrees.is_empty instT andalso Frees.is_empty inst then th else let val idx = Thm.maxidx_of th + 1; fun index ((a, A), b) = (((a, idx), A), b); val insts = (TVars.build (TFrees.fold (TVars.add o index) instT), Vars.build (Frees.fold (Vars.add o index) inst)); val tfrees = Names.build (TFrees.fold (Names.add_set o #1 o #1) instT); val frees = Names.build (Frees.fold (Names.add_set o #1 o #1) inst); val hyps = Thm.chyps_of th; val inst_cterm = Thm.generalize_cterm (tfrees, frees) idx #> Thm.instantiate_cterm insts; in th |> fold_rev Thm.implies_intr hyps |> Thm.generalize (tfrees, frees) idx |> Thm.instantiate insts |> fold (elim_implies o Thm.assume o inst_cterm) hyps end; (* instantiate by left-to-right occurrence of variables *) fun instantiate' cTs cts thm = let fun err msg = raise TYPE ("instantiate': " ^ msg, map_filter (Option.map Thm.typ_of) cTs, map_filter (Option.map Thm.term_of) cts); fun zip_vars xs ys = zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; val instT = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_tvars thm)) cTs; val thm' = Thm.instantiate (TVars.make instT, Vars.empty) thm; val inst = zip_vars (build_rev (Thm.fold_terms {hyps = false} Term.add_vars thm')) cts; in Thm.instantiate (TVars.empty, Vars.make inst) thm' end; (* implicit generalization over variables -- canonical order *) fun forall_intr_vars th = let val vars = Cterms.build (Cterms.add_vars th) in fold_rev Thm.forall_intr (Cterms.list_set vars) th end; fun forall_intr_frees th = let val fixed = Frees.build (fold Frees.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th)) #> fold Frees.add_frees (Thm.hyps_of th)); val is_fixed = Frees.defined fixed o Term.dest_Free o Thm.term_of; val frees = Cterms.build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Free (fn ct => not (is_fixed ct) ? Cterms.add_set ct)); in fold_rev Thm.forall_intr (Cterms.list_set frees) th end; (* unvarify_global: global schematic variables *) fun unvarify_global thy th = let val prop = Thm.full_prop_of th; val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) handle TERM (msg, _) => raise THM (msg, 0, [th]); val cert = Thm.global_cterm_of thy; val certT = Thm.global_ctyp_of thy; val instT = TVars.build (prop |> (Term.fold_types o Term.fold_atyps) (fn T => fn instT => (case T of TVar (v as ((a, _), S)) => if TVars.defined instT v then instT else TVars.add (v, TFree (a, S)) instT | _ => instT))); val cinstT = TVars.map (K certT) instT; val cinst = Vars.build (prop |> Term.fold_aterms (fn t => fn inst => (case t of Var ((x, i), T) => let val T' = Term_Subst.instantiateT instT T in Vars.add (((x, i), T'), cert (Free ((x, T')))) inst end | _ => inst))); in Thm.instantiate (cinstT, cinst) th end; fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; (* user renaming of parameters in a subgoal *) (*The names, if distinct, are used for the innermost parameters of subgoal i; preceding parameters may be renamed to make all parameters distinct.*) fun rename_params_rule (names, i) st = let val (_, Bs, Bi, C) = Thm.dest_state (st, i); val params = map #1 (Logic.strip_params Bi); val short = length params - length names; val names' = if short < 0 then error "More names than parameters in subgoal!" else Name.variant_list names (take short params) @ names; val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; val Bi' = Logic.list_rename_params names' Bi; in (case duplicates (op =) names of a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) | [] => (case inter (op =) names free_names of a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) end; (* preservation of bound variable names *) fun rename_boundvars pat obj th = (case Term.rename_abs pat obj (Thm.prop_of th) of NONE => th | SOME prop' => Thm.renamed_prop prop' th); (** specification primitives **) (* rules *) fun stripped_sorts thy t = let val tfrees = build_rev (Term.add_tfrees t); val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); val recover = map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) tfrees' tfrees; val strip = map (apply2 TFree) (tfrees ~~ tfrees'); val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; in (strip, recover, t') end; fun add_axiom ctxt (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val (strip, recover, prop') = stripped_sorts thy prop; val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; val thy' = thy |> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold elim_implies of_sorts; in ((axm_name, thm), thy') end; fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = Thm.instantiate (TVars.make recover, Vars.empty) axm' |> unvarify_global thy' |> fold_rev Thm.implies_intr prems; in ((axm_name, thm), thy') end; fun add_def_global unchecked overloaded arg thy = add_def (Defs.global_context thy) unchecked overloaded arg thy; (** theorem tags **) (* add / delete tags *) fun tag_rule tg = Thm.map_tags (insert (op =) tg); fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); (* free dummy thm -- for abstract closure *) val free_dummyN = "free_dummy"; fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; val tag_free_dummy = tag_rule (free_dummyN, ""); (* def_name *) fun def_name c = c ^ "_def"; fun def_name_optional c "" = def_name c | def_name_optional _ name = name; val def_binding = Binding.map_name def_name #> Binding.reset_pos; fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; fun make_def_binding cond b = if cond then def_binding b else Binding.empty; (* unofficial theorem names *) fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) val theoremK = "theorem"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; (** attributes **) (*attributes subsume any kind of rules or context modifiers*) type attribute = Context.generic * thm -> Context.generic option * thm option; type binding = binding * attribute list; fun rule_attribute ths f (x, th) = (NONE, (case find_first is_free_dummy (th :: ths) of SOME th' => SOME th' | NONE => SOME (f x th))); fun declaration_attribute f (x, th) = (if is_free_dummy th then NONE else SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) in (the_default th th', the_default x x') end; fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let fun app [] th x = (th, x) | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; val proof_attributes = apply_attributes Context.Proof Context.the_proof; fun no_attributes x = (x, []); fun simple_fact x = [(x, [])]; fun tag tg = rule_attribute [] (K (tag_rule tg)); fun untag s = rule_attribute [] (K (untag_rule s)); fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); (** forked proofs **) structure Proofs = Theory_Data ( type T = thm list lazy Inttab.table; val empty = Inttab.empty; val merge = Inttab.merge (K true); ); fun reset_proofs thy = if Inttab.is_empty (Proofs.get thy) then NONE else SOME (Proofs.put Inttab.empty thy); val _ = Theory.setup (Theory.at_begin reset_proofs); fun register_proofs ths thy = let val entry = (serial (), Lazy.map_finished (map Thm.trim_context) ths) in (Proofs.map o Inttab.update) entry thy end; fun force_proofs thy = Proofs.get thy |> Inttab.dest |> maps (map (Thm.transfer thy) o Lazy.force o #2); val consolidate_theory = Thm.consolidate o force_proofs; fun expose_theory thy = if Proofterm.export_enabled () then Thm.expose_proofs thy (force_proofs thy) else (); (** print theorems **) (* options *) val show_consts = Config.declare_option_bool ("show_consts", \<^here>); val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); (* pretty_thm etc. *) fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = let val show_tags = Config.get ctxt show_tags; val show_hyps = Config.get ctxt show_hyps; val th = raw_th |> perhaps (try (Thm.transfer' ctxt)) |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; val q = if quote then Pretty.quote else I; val prt_term = q o Syntax.pretty_term ctxt; val hlen = length extra_shyps + length hyps + length tpairs; val hsymbs = if hlen = 0 then [] else if show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ map (Syntax.pretty_sort ctxt) extra_shyps)] else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; val tsymbs = if null tags orelse not show_tags then [] else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; fun pretty_thm_global thy = pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; val string_of_thm = Pretty.string_of oo pretty_thm; val string_of_thm_global = Pretty.string_of oo pretty_thm_global; open Thm; end; structure Basic_Thm: BASIC_THM = Thm; open Basic_Thm;