diff --git a/src/Pure/General/basics.ML b/src/Pure/General/basics.ML --- a/src/Pure/General/basics.ML +++ b/src/Pure/General/basics.ML @@ -1,131 +1,135 @@ (* Title: Pure/General/basics.ML Author: Florian Haftmann and Makarius, TU Muenchen Fundamental concepts. *) infix 1 |> |-> |>> ||> ||>> infix 1 #> #-> #>> ##> ##>> signature BASICS = sig (*functions*) val |> : 'a * ('a -> 'b) -> 'b val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd val ` : ('b -> 'a) -> 'b -> 'a * 'b val tap: ('b -> 'a) -> 'b -> 'b (*options*) val is_some: 'a option -> bool val is_none: 'a option -> bool val the: 'a option -> 'a val these: 'a list option -> 'a list val the_list: 'a option -> 'a list val the_default: 'a -> 'a option -> 'a val perhaps: ('a -> 'a option) -> 'a -> 'a val merge_options: 'a option * 'a option -> 'a option + val join_options: ('a * 'a -> 'a) -> 'a option * 'a option -> 'a option val eq_option: ('a * 'b -> bool) -> 'a option * 'b option -> bool (*partiality*) val try: ('a -> 'b) -> 'a -> 'b option val can: ('a -> 'b) -> 'a -> bool (*lists*) val cons: 'a -> 'a list -> 'a list val append: 'a list -> 'a list -> 'a list val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b end; structure Basics: BASICS = struct (* functions *) (*application and structured results*) fun x |> f = f x; fun (x, y) |-> f = f x y; fun (x, y) |>> f = (f x, y); fun (x, y) ||> f = (x, f y); fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end; (*composition and structured results*) fun (f #> g) x = x |> f |> g; fun (f #-> g) x = x |> f |-> g; fun (f #>> g) x = x |> f |>> g; fun (f ##> g) x = x |> f ||> g; fun (f ##>> g) x = x |> f ||>> g; (*result views*) fun `f = fn x => (f x, x); fun tap f = fn x => (f x; x); (* options *) fun is_some (SOME _) = true | is_some NONE = false; fun is_none (SOME _) = false | is_none NONE = true; fun the (SOME x) = x | the NONE = raise Option.Option; fun these (SOME x) = x | these NONE = []; fun the_list (SOME x) = [x] | the_list NONE = [] fun the_default x (SOME y) = y | the_default x NONE = x; fun perhaps f x = the_default x (f x); fun merge_options (x, y) = if is_some x then x else y; +fun join_options f (SOME x, SOME y) = SOME (f (x, y)) + | join_options _ args = merge_options args; + fun eq_option eq (SOME x, SOME y) = eq (x, y) | eq_option _ (NONE, NONE) = true | eq_option _ _ = false; (* partiality *) fun try f x = SOME (f x) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else NONE; fun can f x = is_some (try f x); (* lists *) fun cons x xs = x :: xs; fun append xs ys = xs @ ys; fun fold _ [] y = y | fold f (x :: xs) y = fold f xs (f x y); fun fold_rev _ [] y = y | fold_rev f (x :: xs) y = f x (fold_rev f xs y); fun fold_map _ [] y = ([], y) | fold_map f (x :: xs) y = let val (x', y') = f x y; val (xs', y'') = fold_map f xs y'; in (x' :: xs', y'') end; end; open Basics; diff --git a/src/Pure/Isar/element.ML b/src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML +++ b/src/Pure/Isar/element.ML @@ -1,476 +1,477 @@ (* Title: Pure/Isar/element.ML Author: Makarius Explicit data structures for some Isar language elements, with derived logical operations. *) signature ELEMENT = sig type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list) type obtains = (string, string) obtain list type obtains_i = (typ, term) obtain list datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | Obtains of ('typ, 'term) obtain list type statement = (string, string) stmt type statement_i = (typ, term) stmt datatype ('typ, 'term, 'fact) ctxt = Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | Notes of string * (Attrib.binding * ('fact * Token.src list) list) list | Lazy_Notes of string * (binding * 'fact lazy) type context = (string, string, Facts.ref) ctxt type context_i = (typ, term, thm list) ctxt val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b, pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Token.src -> Token.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt val map_ctxt_attrib: (Token.src -> Token.src) -> ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt val transform_ctxt: morphism -> context_i -> context_i val pretty_stmt: Proof.context -> statement_i -> Pretty.T list val pretty_ctxt: Proof.context -> context_i -> Pretty.T list val pretty_ctxt_no_attribs: Proof.context -> context_i -> Pretty.T list val pretty_statement: Proof.context -> string -> thm -> Pretty.T type witness val prove_witness: Proof.context -> term -> tactic -> witness val witness_proof: (witness list list -> Proof.context -> Proof.context) -> term list list -> Proof.context -> Proof.state val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) -> term list list -> term list -> Proof.context -> Proof.state val witness_local_proof: (witness list list -> Proof.state -> Proof.state) -> string -> term list list -> Proof.context -> Proof.state -> Proof.state val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) -> string -> term list list -> term list -> Proof.context -> Proof.state -> Proof.state val transform_witness: morphism -> witness -> witness val conclude_witness: Proof.context -> witness -> thm val pretty_witness: Proof.context -> witness -> Pretty.T val instantiate_normalize_morphism: ctyp TFrees.table * cterm Frees.table -> morphism val satisfy_morphism: witness list -> morphism val eq_term_morphism: theory -> term list -> morphism option val eq_morphism: theory -> thm list -> morphism option val init: context_i -> Context.generic -> Context.generic val activate_i: context_i -> Proof.context -> context_i * Proof.context val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context end; structure Element: ELEMENT = struct (** language elements **) (* statement *) type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list); type obtains = (string, string) obtain list; type obtains_i = (typ, term) obtain list; datatype ('typ, 'term) stmt = Shows of (Attrib.binding * ('term * 'term list) list) list | Obtains of ('typ, 'term) obtain list; type statement = (string, string) stmt; type statement_i = (typ, term) stmt; (* context *) datatype ('typ, 'term, 'fact) ctxt = Fixes of (binding * 'typ option * mixfix) list | Constrains of (string * 'typ) list | Assumes of (Attrib.binding * ('term * 'term list) list) list | Defines of (Attrib.binding * ('term * 'term list)) list | Notes of string * (Attrib.binding * ('fact * Token.src list) list) list | Lazy_Notes of string * (binding * 'fact lazy); type context = (string, string, Facts.ref) ctxt; type context_i = (typ, term, thm list) ctxt; fun map_ctxt {binding, typ, term, pattern, fact, attrib} = fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) | Constrains xs => Constrains (xs |> map (fn (x, T) => (Variable.check_name (binding (Binding.name x)), typ T))) | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) => ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps))))) | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => ((binding a, map attrib atts), (term t, map pattern ps)))) | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) => ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts))))) | Lazy_Notes (kind, (a, ths)) => Lazy_Notes (kind, (binding a, Lazy.map fact ths)); fun map_ctxt_attrib attrib = map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib}; fun transform_ctxt phi = map_ctxt {binding = Morphism.binding phi, typ = Morphism.typ phi, term = Morphism.term phi, pattern = Morphism.term phi, fact = Morphism.fact phi, attrib = map (Token.transform phi)}; (** pretty printing **) fun pretty_items _ _ [] = [] | pretty_items keyword sep (x :: ys) = Pretty.block [Pretty.keyword2 keyword, Pretty.brk 1, x] :: map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword2 sep, Pretty.brk 1, y]) ys; (* pretty_stmt *) fun pretty_stmt ctxt = let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; val prt_terms = separate (Pretty.keyword2 "and") o map prt_term; val prt_binding = Attrib.pretty_binding ctxt; val prt_name = Proof_Context.pretty_name ctxt; fun prt_show (a, ts) = Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts))); fun prt_var (x, SOME T, _) = Pretty.block [prt_name (Binding.name_of x), Pretty.str " ::", Pretty.brk 1, prt_typ T] | prt_var (x, NONE, _) = prt_name (Binding.name_of x); val prt_vars = separate (Pretty.keyword2 "and") o map prt_var; fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props)) | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props)); in fn Shows shows => pretty_items "shows" "and" (map prt_show shows) | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains) end; (* pretty_ctxt *) fun gen_pretty_ctxt show_attribs ctxt = let val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; val prt_term = Pretty.quote o Syntax.pretty_term ctxt; val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt; val prt_name = Proof_Context.pretty_name ctxt; fun prt_binding (b, atts) = Attrib.pretty_binding ctxt (b, if show_attribs then atts else []); fun prt_fact (ths, atts) = if not show_attribs orelse null atts then map prt_thm ths else Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; fun prt_mixfix NoSyn = [] | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx]; fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" :: Pretty.brk 1 :: prt_typ T :: prt_mixfix mx) | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx); fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); fun prt_asm (a, ts) = Pretty.block (Pretty.breaks (prt_binding a ":" @ map (prt_term o fst) ts)); fun prt_def (a, (t, _)) = Pretty.block (Pretty.breaks (prt_binding a ":" @ [prt_term t])); fun prt_note (a, ths) = Pretty.block (Pretty.breaks (flat (prt_binding a " =" :: map prt_fact ths))); fun notes_kind "" = "notes" | notes_kind kind = "notes " ^ kind; in fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) | Defines defs => pretty_items "defines" "and" (map prt_def defs) | Notes (kind, facts) => pretty_items (notes_kind kind) "and" (map prt_note facts) | Lazy_Notes (kind, (a, ths)) => pretty_items (notes_kind kind) "and" [prt_note ((a, []), [(Lazy.force ths, [])])] end; val pretty_ctxt = gen_pretty_ctxt true; val pretty_ctxt_no_attribs = gen_pretty_ctxt false; (* pretty_statement *) local fun standard_elim ctxt th = (case Object_Logic.elim_concl ctxt th of SOME C => let val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); val insts = (TVars.empty, Vars.make1 (Term.dest_Var C, Thm.cterm_of ctxt thesis)); val th' = Thm.instantiate insts th; in (th', true) end | NONE => (th, false)); fun thm_name ctxt kind th prts = let val head = if Thm.has_name_hint th then Pretty.block [Pretty.keyword1 kind, Pretty.brk 1, Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"] else Pretty.keyword1 kind in Pretty.block (Pretty.fbreaks (head :: prts)) end; fun obtain prop ctxt = let val ((ps, prop'), ctxt') = Variable.focus NONE prop ctxt; fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn); val xs = map (fix o #2) ps; val As = Logic.strip_imp_prems prop'; in ((Binding.empty, (xs, As)), ctxt') end; in fun pretty_statement ctxt kind raw_th = let val (th, is_elim) = standard_elim ctxt (Raw_Simplifier.norm_hhf ctxt raw_th); val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt); val prop = Thm.prop_of th'; val (prems, concl) = Logic.strip_horn prop; val concl_term = Object_Logic.drop_judgment ctxt concl; val (assumes, cases) = chop_suffix (fn prem => is_elim andalso concl aconv Logic.strip_assums_concl prem) prems; val is_thesis = if null cases then K false else fn v => v aconv concl_term; val fixes = rev (fold_aterms (fn v as Free (x, T) => if Variable.is_newly_fixed ctxt' ctxt x andalso not (is_thesis v) then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop []); in pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @ pretty_ctxt ctxt' (Assumes (map (fn t => (Binding.empty_atts, [(t, [])])) assumes)) @ (if null cases then pretty_stmt ctxt' (Shows [(Binding.empty_atts, [(concl, [])])]) else let val (clauses, ctxt'') = fold_map obtain cases ctxt' in pretty_stmt ctxt'' (Obtains clauses) end) end |> thm_name ctxt kind raw_th; end; (** logical operations **) (* witnesses -- hypotheses as protected facts *) datatype witness = Witness of term * thm; val mark_witness = Logic.protect; fun witness_prop (Witness (t, _)) = t; fun witness_hyps (Witness (_, th)) = Thm.hyps_of th; fun map_witness f (Witness witn) = Witness (f witn); fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); fun prove_witness ctxt t tac = Witness (t, Goal.prove ctxt [] [] (mark_witness t) (fn _ => resolve_tac ctxt [Drule.protectI] 1 THEN tac) |> Thm.close_derivation \<^here> |> Thm.trim_context); local val refine_witness = Proof.refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI])))))))); fun gen_witness_proof proof after_qed wit_propss eq_props = let val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss @ [map (rpair []) eq_props]; fun after_qed' thmss = let val (wits, eqs) = split_last ((map o map) (Thm.close_derivation \<^here> #> Thm.trim_context) thmss); in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; in proof after_qed' propss #> refine_witness end; fun proof_local cmd goal_ctxt after_qed propp = let fun after_qed' (result_ctxt, results) state' = after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state'; in Proof.map_context (K goal_ctxt) #> Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) true cmd NONE after_qed' [] [] (map (pair Binding.empty_atts) propp) #> snd end; in fun witness_proof after_qed wit_propss = gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits) wit_propss []; val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE); fun witness_local_proof after_qed cmd wit_propss goal_ctxt = gen_witness_proof (proof_local cmd goal_ctxt) (fn wits => fn _ => after_qed wits) wit_propss []; fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt = gen_witness_proof (proof_local cmd goal_ctxt) after_qed wit_propss eq_props; end; fun conclude_witness ctxt (Witness (_, th)) = Goal.conclude (Thm.transfer' ctxt th) |> Raw_Simplifier.norm_hhf_protect ctxt |> Thm.close_derivation \<^here>; fun pretty_witness ctxt witn = let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in Pretty.block (prt_term (witness_prop witn) :: (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]" (map prt_term (witness_hyps witn))] else [])) end; (* instantiate frees, with beta normalization *) fun instantiate_normalize_morphism insts = Morphism.instantiate_frees_morphism insts $> Morphism.term_morphism "beta_norm" Envir.beta_norm $> Morphism.thm_morphism "beta_conversion" (Conv.fconv_rule (Thm.beta_conversion true)); (* satisfy hypotheses *) local val norm_term = Envir.beta_eta_contract; val norm_conv = Drule.beta_eta_conversion; val norm_cterm = Thm.rhs_of o norm_conv; fun find_witness witns hyp = (case find_first (fn Witness (t, _) => hyp aconv t) witns of NONE => let val hyp' = norm_term hyp in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end | some => some); fun compose_witness (Witness (_, th)) r = let val th' = Goal.conclude (Thm.transfer (Thm.theory_of_thm r) th); val A = Thm.cprem_of r 1; in Thm.implies_elim (Conv.gconv_rule norm_conv 1 r) (Conv.fconv_rule norm_conv (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th')) end; in fun satisfy_thm witns thm = (Thm.chyps_of thm, thm) |-> fold (fn hyp => (case find_witness witns (Thm.term_of hyp) of NONE => I | SOME w => Thm.implies_intr hyp #> compose_witness w)); val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm; end; (* rewriting with equalities *) (* for activating declarations only *) fun eq_term_morphism _ [] = NONE | eq_term_morphism thy props = let + (* FIXME proper morphism context *) fun decomp_simp prop = let val ctxt = Proof_Context.init_global thy; val _ = Logic.no_prems prop orelse error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop); val lhsrhs = Logic.dest_equals prop handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop); in lhsrhs end; val phi = Morphism.morphism "Element.eq_term_morphism" {binding = [], typ = [], - term = [Pattern.rewrite_term thy (map decomp_simp props) []], - fact = [fn _ => error "Illegal application of Element.eq_term_morphism"]}; + term = [K (Pattern.rewrite_term thy (map decomp_simp props) [])], + fact = [fn _ => fn _ => error "Illegal application of Element.eq_term_morphism"]}; in SOME phi end; fun eq_morphism _ [] = NONE | eq_morphism thy thms = let - (* FIXME proper context!? *) + (* FIXME proper morphism context *) fun rewrite th = rewrite_rule (Proof_Context.init_global (Thm.theory_of_thm th)) thms th; val phi = Morphism.morphism "Element.eq_morphism" {binding = [], typ = [], - term = [Raw_Simplifier.rewrite_term thy thms []], - fact = [map rewrite]}; + term = [K (Raw_Simplifier.rewrite_term thy thms [])], + fact = [K (map rewrite)]}; in SOME phi end; (** activate in context **) (* init *) fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2) | init (Constrains _) = I | init (Assumes asms) = Context.map_proof (fn ctxt => let val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms; val (_, ctxt') = ctxt |> fold Proof_Context.augment (maps (map #1 o #2) asms') |> Proof_Context.add_assms Assumption.assume_export asms'; in ctxt' end) | init (Defines defs) = Context.map_proof (fn ctxt => let val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs; val asms = defs' |> map (fn (b, (t, ps)) => let val (_, t') = Local_Defs.cert_def ctxt (K []) t (* FIXME adapt ps? *) in (t', (b, [(t', ps)])) end); val (_, ctxt') = ctxt |> fold Proof_Context.augment (map #1 asms) |> Proof_Context.add_assms Local_Defs.def_export (map #2 asms); in ctxt' end) | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2 | init (Lazy_Notes (kind, ths)) = Attrib.lazy_notes kind ths; (* activate *) fun activate_i elem ctxt = let val elem' = (case (map_ctxt_attrib o map) Token.init_assignable elem of Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) => ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts), (t, ps)))) | e => e); val ctxt' = Context.proof_map (init elem') ctxt; in ((map_ctxt_attrib o map) Token.closure elem', ctxt') end; fun activate raw_elem ctxt = let val elem = raw_elem |> map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = Proof_Context.get_fact ctxt, attrib = Attrib.check_src ctxt} in activate_i elem ctxt end; end; diff --git a/src/Pure/Isar/expression.ML b/src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML +++ b/src/Pure/Isar/expression.ML @@ -1,881 +1,881 @@ (* Title: Pure/Isar/expression.ML Author: Clemens Ballarin, TU Muenchen Locale expressions and user interface layer of locales. *) signature EXPRESSION = sig (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list type 'term rewrites = (Attrib.binding * 'term) list type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list type expression_i = (string, term) expr * (binding * typ option * mixfix) list type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list (* Processing of context statements *) val cert_statement: Element.context_i list -> Element.statement_i -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context val read_statement: Element.context list -> Element.statement -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context (* Declaring locales *) val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val add_locale: binding -> binding -> Bundle.name list -> expression_i -> Element.context_i list -> theory -> string * local_theory val add_locale_cmd: binding -> binding -> (xstring * Position.T) list -> expression -> Element.context list -> theory -> string * local_theory (* Processing of locale expressions *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context end; structure Expression : EXPRESSION = struct datatype ctxt = datatype Element.ctxt; (*** Expressions ***) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list; type 'term rewrites = (Attrib.binding * 'term) list; type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list; type expression_i = (string, term) expr * (binding * typ option * mixfix) list; type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list; (** Internalise locale names in expr **) fun check_expr thy instances = map (apfst (Locale.check thy)) instances; (** Parameters of expression **) (*Sanity check of instantiations and extraction of implicit parameters. The latter only occurs iff strict = false. Positional instantiations are extended to match full length of parameter list of instantiated locale.*) fun parameters_of thy strict (expr, fixed) = let val ctxt = Proof_Context.init_global thy; fun reject_dups message xs = (case duplicates (op =) xs of [] => () | dups => error (message ^ commas dups)); fun parm_eq ((p1, mx1), (p2, mx2)) = p1 = p2 andalso (Mixfix.equal (mx1, mx2) orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); fun params_inst (loc, (prfx, (Positional insts, eqns))) = let val ps = params_loc loc; val d = length ps - length insts; val insts' = if d < 0 then error ("More arguments than parameters in instantiation of locale " ^ quote (Locale.markup_name ctxt loc)) else insts @ replicate d NONE; val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); in (ps', (loc, (prfx, (Positional insts', eqns)))) end | params_inst (loc, (prfx, (Named insts, eqns))) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " (map fst insts); val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps else error (quote p ^ " not a parameter of instantiated expression")); in (ps', (loc, (prfx, (Named insts, eqns)))) end; fun params_expr is = let val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; val fixed' = map (Variable.check_name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] else let val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed'); in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; in (expr', implicit'' @ fixed) end; (** Read instantiation **) (* Parse positional or named instantiation *) local fun prep_inst prep_term ctxt parms (Positional insts) = (insts ~~ parms) |> map (fn (NONE, p) => Free (p, dummyT) | (SOME t, _) => prep_term ctxt t) | prep_inst prep_term ctxt parms (Named insts) = parms |> map (fn p => (case AList.lookup (op =) insts p of SOME t => prep_term ctxt t | NONE => Free (p, dummyT))); in fun parse_inst x = prep_inst Syntax.parse_term x; fun make_inst x = prep_inst (K I) x; end; (* Instantiation morphism *) fun inst_morphism params ((prfx, mandatory), insts') ctxt = let (* parameters *) val parm_types = map #2 params; val type_parms = fold Term.add_tfreesT parm_types []; (* type inference *) val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; val type_parms' = fold Term.add_tvarsT parm_types' []; val checked = (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) val (type_parms'', insts'') = chop (length type_parms') checked; (* context *) val ctxt' = fold Proof_Context.augment checked ctxt; val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; (* instantiation *) val instT = TFrees.build (fold2 (fn v => fn T => not (TFree v = T) ? TFrees.add (v, T)) type_parms (map Logic.dest_type type_parms'')); val cert_inst = Frees.build (fold2 (fn v => fn t => not (Free v = t) ? Frees.add (v, cert t)) (map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) insts''); in (Element.instantiate_normalize_morphism (TFrees.map (K certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; (*** Locale processing ***) (** Parsing **) fun parse_elem prep_typ prep_term ctxt = Element.map_ctxt {binding = I, typ = prep_typ ctxt, term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), fact = I, attrib = I}; fun prepare_stmt prep_prop prep_obtains ctxt stmt = (case stmt of Element.Shows raw_shows => raw_shows |> (map o apsnd o map) (fn (t, ps) => (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) | Element.Obtains raw_obtains => let val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; val obtains = prep_obtains thesis_ctxt thesis raw_obtains; in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); (** Simultaneous type inference: instantiations + elements + statement **) local fun mk_type T = (Logic.mk_type T, []); fun mk_term t = (t, []); fun mk_propp (p, pats) = (Type.constraint propT p, pats); fun dest_type (T, []) = Logic.dest_type T; fun dest_term (t, []) = t; fun dest_propp (p, pats) = (p, pats); fun extract_inst (_, (_, ts)) = map mk_term ts; fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)); fun extract_eqns es = map (mk_term o snd) es; fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs; fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs | extract_elem (Notes _) = [] | extract_elem (Lazy_Notes _) = []; fun restore_elem (Fixes fixes, css) = (fixes ~~ css) |> map (fn ((x, _, mx), cs) => (x, cs |> map dest_type |> try hd, mx)) |> Fixes | restore_elem (Constrains csts, css) = (csts ~~ css) |> map (fn ((x, _), cs) => (x, cs |> map dest_type |> hd)) |> Constrains | restore_elem (Assumes asms, css) = (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes | restore_elem (Defines defs, css) = (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines | restore_elem (elem as Notes _, _) = elem | restore_elem (elem as Lazy_Notes _, _) = elem; fun prep (_, pats) (ctxt, t :: ts) = let val ctxt' = Proof_Context.augment t ctxt in ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), (ctxt', ts)) end; fun check cs ctxt = let val (cs', (ctxt', _)) = fold_map prep cs (ctxt, Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)); in (cs', ctxt') end; in fun check_autofix insts eqnss elems concl ctxt = let val inst_cs = map extract_inst insts; val eqns_cs = map extract_eqns eqnss; val elem_css = map extract_elem elems; val concl_cs = (map o map) mk_propp (map snd concl); (* Type inference *) val (inst_cs' :: eqns_cs' :: css', ctxt') = (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in ((map restore_inst (insts ~~ inst_cs'), map restore_eqns (eqnss ~~ eqns_cs'), map restore_elem (elems ~~ elem_css'), map fst concl ~~ concl_cs'), ctxt') end; end; (** Prepare locale elements **) fun declare_elem prep_var (Fixes fixes) ctxt = let val (vars, _) = fold_map prep_var fixes ctxt in ctxt |> Proof_Context.add_fixes vars |> snd end | declare_elem prep_var (Constrains csts) ctxt = ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd | declare_elem _ (Assumes _) ctxt = ctxt | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt | declare_elem _ (Lazy_Notes _) ctxt = ctxt; (** Finish locale elements **) fun finish_inst ctxt (loc, (prfx, inst)) = let val thy = Proof_Context.theory_of ctxt; val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; in (loc, morph) end; fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => let val x = Binding.name_of binding in (binding, AList.lookup (op =) parms x, mx) end); local fun closeup _ _ false elem = elem | closeup (outer_ctxt, ctxt) parms true elem = let (* FIXME consider closing in syntactic phase -- before type checking *) fun close_frees t = let val rev_frees = Term.fold_aterms (fn Free (x, T) => if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t []; in fold (Logic.all o Free) rev_frees t end; fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in context element"; in (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) | e => e) end; in fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes) | finish_elem _ _ _ (Constrains _) = Constrains [] | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms) | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs) | finish_elem _ _ _ (elem as Notes _) = elem | finish_elem _ _ _ (elem as Lazy_Notes _) = elem; end; (** Process full context statement: instantiations + elements + statement **) (* Interleave incremental parsing and type inference over entire parsed stretch. *) local fun abs_def ctxt = Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; fun prep_full_context_statement parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 = let val thy = Proof_Context.theory_of ctxt1; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let val params = map #1 (Locale.params_of thy loc); val inst' = prep_inst ctxt (map #1 params) inst; val parm_types' = params |> map (#2 #> Logic.varifyT_global #> Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> Type_Infer.paramify_vars); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt; val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 handle ERROR msg => if null eqns then error msg else (Locale.tracing ctxt1 (msg ^ "\nFalling back to reading rewrites clause before activation."); ctxt2); val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns; val eqns' = (prep_eqns ctxt' o map snd) eqns; val eqnss' = [attrss ~~ eqns']; val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt'; val rewrite_morph = eqns' |> map (abs_def ctxt') |> Variable.export_terms ctxt' ctxt |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) |> Morphism.default; val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']; in (i + 1, insts', eqnss', ctxt'') end; fun prep_elem raw_elem ctxt = let val ctxt' = ctxt |> Context_Position.set_visible false |> declare_elem prep_var_elem raw_elem |> Context_Position.restore_visible ctxt; val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem; in (elems', ctxt') end; val fors = fold_map prep_var_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd; val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2); fun prep_stmt elems ctxt = check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; val _ = if fixed_frees then () else (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of [] => () | frees => error ("Illegal free variables in expression: " ^ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); val ((insts, _, elems', concl), ctxt4) = ctxt3 |> init_body |> fold_map prep_elem raw_elems |-> prep_stmt; (* parameters from expression and elements *) val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) (Fixes fors :: elems'); val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4; val fors' = finish_fixes parms fors; val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors'; val deps = map (finish_inst ctxt5) insts; val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'; in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end; in fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) Obtain.cert_obtains Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x; end; (* Context statement: elements + statement *) local fun prep_statement prep activate raw_elems raw_stmt ctxt = let val ((_, _, _, elems, concl), _) = prep {strict = true, do_close = false, fixed_frees = true} ([], []) I raw_elems raw_stmt ctxt; val ctxt' = ctxt |> Proof_Context.set_stmt true |> fold_map activate elems |> #2 |> Proof_Context.restore_stmt ctxt; in (concl, ctxt') end; in fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x; fun read_statement x = prep_statement read_full_context_statement Element.activate x; end; (* Locale declaration: import + elements *) fun fix_params params = Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; local fun prep_declaration prep activate raw_import init_body raw_elems ctxt = let val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) = prep {strict = false, do_close = true, fixed_frees = false} raw_import init_body raw_elems (Element.Shows []) ctxt; val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale"; (* Declare parameters and imported facts *) val ctxt' = ctxt |> fix_params fixed |> fold (Context.proof_map o Locale.activate_facts NONE) deps; val (elems', ctxt'') = ctxt' |> Proof_Context.set_stmt true |> fold_map activate elems ||> Proof_Context.restore_stmt ctxt'; in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end; in fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; fun read_declaration x = prep_declaration read_full_context_statement Element.activate x; end; (* Locale expression to set up a goal *) local fun props_of thy (name, morph) = let val (asm, defs) = Locale.specification_of thy name in map (Morphism.term morph) (the_list asm @ defs) end; fun prep_goal_expression prep expression ctxt = let val thy = Proof_Context.theory_of ctxt; val ((fixed, deps, eqnss, _, _), _) = prep {strict = true, do_close = true, fixed_frees = true} expression I [] (Element.Shows []) ctxt; (* proof obligations *) val propss = map (props_of thy) deps; val eq_propss = (map o map) snd eqnss; val goal_ctxt = ctxt |> fix_params fixed |> (fold o fold) Proof_Context.augment (propss @ eq_propss); val export = Proof_Context.export_morphism goal_ctxt ctxt; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism "Expression.prep_goal" - {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]}; + {binding = [], typ = [K exp_typ], term = [K exp_term], fact = [K exp_fact]}; in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end; in fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; fun read_goal_expression x = prep_goal_expression read_full_context_statement x; end; (*** Locale declarations ***) (* extract specification text *) val norm_term = Envir.beta_norm oo Term.subst_atomic; fun bind_def ctxt eq (env, eqs) = let val _ = Local_Defs.cert_def ctxt (K []) eq; val ((y, T), b) = Local_Defs.abs_def eq; val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of [] => ((Free (y, T), b') :: env, eq :: eqs) | dups => if forall (fn (_, b'') => b' aconv b'') dups then (env, eqs) else err "Attempt to redefine variable") end; (* text has the following structure: (((exts, exts'), (ints, ints')), (xs, env, defs)) where exts: external assumptions (terms in assumes elements) exts': dito, normalised wrt. env ints: internal assumptions (terms in assumptions from insts) ints': dito, normalised wrt. env xs: the free variables in exts' and ints' and rhss of definitions, this includes parameters except defined parameters env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env defs: the equations from the defines elements *) fun eval_text _ _ (Fixes _) text = text | eval_text _ _ (Constrains _) text = text | eval_text _ is_ext (Assumes asms) (((exts, exts'), (ints, ints')), (env, defs)) = let val ts = maps (map #1 o #2) asms; val ts' = map (norm_term env) ts; val spec' = if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) else ((exts, exts'), (ints @ ts, ints' @ ts')); in (spec', (env, defs)) end | eval_text ctxt _ (Defines defs) (spec, binds) = (spec, fold (bind_def ctxt o #1 o #2) defs binds) | eval_text _ _ (Notes _) text = text | eval_text _ _ (Lazy_Notes _) text = text; fun eval_inst ctxt (loc, morph) text = let val thy = Proof_Context.theory_of ctxt; val (asm, defs) = Locale.specification_of thy loc; val asm' = Option.map (Morphism.term morph) asm; val defs' = map (Morphism.term morph) defs; val text' = text |> (if is_some asm then eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])]) else I) |> (if not (null defs) then eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs')) else I) (* FIXME clone from locale.ML *) in text' end; fun eval_elem ctxt elem text = eval_text ctxt true elem text; fun eval ctxt deps elems = let val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [])); val ((spec, (_, defs))) = fold (eval_elem ctxt) elems text'; in (spec, defs) end; (* axiomsN: name of theorem set with destruct rules for locale predicates, also name suffix of delta predicates and assumptions. *) val axiomsN = "axioms"; local (* introN: name of theorems for introduction rules of locale and delta predicates *) val introN = "intro"; fun atomize_spec ctxt ts = let val t = Logic.mk_conjunction_balanced ts; val body = Object_Logic.atomize_term ctxt t; val bodyT = Term.fastype_of body; in if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t)) else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t)) end; (* achieve plain syntax for locale predicates (without "PROP") *) fun aprop_tr' n c = let val c' = Lexicon.mark_const c; fun tr' (_: Proof.context) T args = if T <> dummyT andalso length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args) else raise Match; in (c', tr') end; (* define one predicate including its intro rule and axioms - binding: predicate name - parms: locale parameters - defs: thms representing substitutions from defines elements - ts: terms representing locale assumptions (not normalised wrt. defs) - norm_ts: terms representing locale assumptions (normalised wrt. defs) - thy: the theory *) fun def_pred binding parms defs ts norm_ts thy = let val name = Sign.full_name thy binding; val thy_ctxt = Proof_Context.init_global thy; val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts; val env = Names.build (Names.add_free_names body); val xs = filter (Names.defined env o #1) parms; val Ts = map #2 xs; val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts); val extra_tfrees = TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body) |> TFrees.keys |> map TFree; val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT; val args = map Logic.mk_type extra_tfrees @ map Free xs; val head = Term.list_comb (Const (name, predT), args); val statement = Object_Logic.ensure_propT thy_ctxt head; val ([pred_def], defs_thy) = thy |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name] |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])]; val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head; val intro = Goal.prove_global defs_thy [] norm_ts statement (fn {context = ctxt, ...} => rewrite_goals_tac ctxt [pred_def] THEN compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts)); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness axioms_ctxt t (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1)); in ((statement, intro, axioms), defs_thy) end; in (* main predicate definition function *) fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy = let val ctxt = Proof_Context.init_global thy; val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs; val (a_pred, a_intro, a_axioms, thy2) = if null exts then (NONE, NONE, [], thy) else let val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding; val ((statement, intro, axioms), thy1) = thy |> def_pred abinding parms defs' exts exts'; val ((_, [intro']), thy2) = thy1 |> Sign.qualified_path true abinding |> Global_Theory.note_thms "" ((Binding.name introN, []), [([intro], [Locale.unfold_add])]) ||> Sign.restore_naming thy1; in (SOME statement, SOME intro', axioms, thy2) end; val (b_pred, b_intro, b_axioms, thy4) = if null ints then (NONE, NONE, [], thy2) else let val ((statement, intro, axioms), thy3) = thy2 |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val conclude_witness = Drule.export_without_context o Element.conclude_witness (Proof_Context.init_global thy3); val ([(_, [intro']), _], thy4) = thy3 |> Sign.qualified_path true binding |> Global_Theory.note_thmss "" [((Binding.name introN, []), [([intro], [Locale.intro_add])]), ((Binding.name axiomsN, []), [(map conclude_witness axioms, [])])] ||> Sign.restore_naming thy3; in (SOME statement, SOME intro', axioms, thy4) end; in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy4) end; end; local fun assumes_to_notes (Assumes asms) axms = fold_map (fn (a, spec) => fn axs => let val (ps, qs) = chop (length spec) axs in ((a, [(ps, [])]), qs) end) asms axms |> apfst (curry Notes "") | assumes_to_notes e axms = (e, axms); fun defines_to_notes ctxt (Defines defs) = Notes ("", map (fn (a, (def, _)) => (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)], [(Attrib.internal o K) Locale.witness_add])])) defs) | defines_to_notes _ e = e; val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false; fun gen_add_locale prep_include prep_decl binding raw_predicate_binding raw_includes raw_import raw_body thy = let val name = Sign.full_name thy binding; val _ = Locale.defined thy name andalso error ("Duplicate definition of locale " ^ quote name); val ctxt = Proof_Context.init_global thy; val includes = map (prep_include ctxt) raw_includes; val ((fixed, deps, body_elems, _), (parms, ctxt')) = ctxt |> Bundle.includes includes |> prep_decl raw_import I raw_body; val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms); val extra_tfrees = TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts') |> TFrees.keys; val _ = if null extra_tfrees then () else warning ("Additional type variable(s) in locale specification " ^ Binding.print binding ^ ": " ^ commas (map (Syntax.string_of_typ ctxt' o TFree) extra_tfrees)); val predicate_binding = if Binding.is_empty raw_predicate_binding then binding else raw_predicate_binding; val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_binding parms text thy; val pred_ctxt = Proof_Context.init_global thy'; val a_satisfy = Element.satisfy_morphism a_axioms; val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ maps (fn Fixes fixes => map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems; val asm = if is_some b_statement then b_statement else a_statement; val hyp_spec = filter is_hyp body_elems; val notes = if is_some asm then [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []), [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))], [(Attrib.internal o K) Locale.witness_add])])])] else []; val notes' = body_elems |> map (Element.transform_ctxt (Morphism.transfer_morphism thy')) |> map (defines_to_notes pred_ctxt) |> map (Element.transform_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |> fst |> map (Element.transform_ctxt b_satisfy) |> map_filter (fn Notes notes => SOME notes | _ => NONE); val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val axioms = map (Element.conclude_witness pred_ctxt) b_axioms; val loc_ctxt = thy' |> Locale.register_locale binding (extra_tfrees, params) (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps') |> Named_Target.init includes name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; in val add_locale = gen_add_locale (K I) cert_declaration; val add_locale_cmd = gen_add_locale Bundle.check read_declaration; end; end; diff --git a/src/Pure/assumption.ML b/src/Pure/assumption.ML --- a/src/Pure/assumption.ML +++ b/src/Pure/assumption.ML @@ -1,149 +1,149 @@ (* Title: Pure/assumption.ML Author: Makarius Context assumptions, parameterized by export rules. *) signature ASSUMPTION = sig type export = bool -> cterm list -> (thm -> thm) * (term -> term) val assume_export: export val presume_export: export val assume: Proof.context -> cterm -> thm val assume_hyps: cterm -> Proof.context -> thm * Proof.context val all_assms_of: Proof.context -> cterm list val all_prems_of: Proof.context -> thm list val local_assms_of: Proof.context -> Proof.context -> cterm list val local_prems_of: Proof.context -> Proof.context -> thm list val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context val add_assumes: cterm list -> Proof.context -> thm list * Proof.context val export: bool -> Proof.context -> Proof.context -> thm -> thm val export_term: Proof.context -> Proof.context -> term -> term val export_morphism: Proof.context -> Proof.context -> morphism end; structure Assumption: ASSUMPTION = struct (** basic rules **) type export = bool -> cterm list -> (thm -> thm) * (term -> term); (* [A] : B -------- #A \ B *) fun assume_export is_goal asms = (if is_goal then Drule.implies_intr_protected asms else Drule.implies_intr_list asms, fn t => t); (* [A] : B ------- A \ B *) fun presume_export _ = assume_export false; fun assume ctxt = Raw_Simplifier.norm_hhf ctxt o Thm.assume; fun assume_hyps ct ctxt = let val (th, ctxt') = Thm.assume_hyps ct ctxt in (Raw_Simplifier.norm_hhf ctxt' th, ctxt') end; (** local context data **) datatype data = Data of {assms: (export * cterm list) list, (*assumes: A \ _*) prems: thm list}; (*prems: A |- norm_hhf A*) fun make_data (assms, prems) = Data {assms = assms, prems = prems}; val empty_data = make_data ([], []); structure Data = Proof_Data ( type T = data; fun init _ = empty_data; ); fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems))); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); (* all assumptions *) val all_assumptions_of = #assms o rep_data; val all_assms_of = maps #2 o all_assumptions_of; val all_prems_of = #prems o rep_data; (* local assumptions *) local fun drop_prefix eq (args as (x :: xs, y :: ys)) = if eq (x, y) then drop_prefix eq (xs, ys) else args | drop_prefix _ args = args; fun check_result ctxt kind term_of res = (case res of ([], rest) => rest | (bad :: _, _) => raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^ Syntax.string_of_term ctxt (term_of bad))); in fun local_assumptions_of inner outer = drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner)) |>> maps #2 |> check_result outer "assumption" Thm.term_of; val local_assms_of = maps #2 oo local_assumptions_of; fun local_prems_of inner outer = drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner)) |> check_result outer "premise" Thm.prop_of; end; (* add assumptions *) fun add_assms export new_asms ctxt = let val (new_prems, ctxt') = fold_map assume_hyps new_asms ctxt in ctxt' |> map_data (fn (asms, prems) => (asms @ [(export, new_asms)], prems @ new_prems)) |> pair new_prems end; val add_assumes = add_assms assume_export; (* export *) fun export is_goal inner outer = Raw_Simplifier.norm_hhf_protect_without_context #> fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #> Raw_Simplifier.norm_hhf_protect_without_context; fun export_term inner outer = fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer); fun export_morphism inner outer = let val thm = export false inner outer; val term = export_term inner outer; val typ = Logic.type_map term; in Morphism.morphism "Assumption.export" - {binding = [], typ = [typ], term = [term], fact = [map thm]} + {binding = [], typ = [K typ], term = [K term], fact = [K (map thm)]} end; end; diff --git a/src/Pure/context.ML b/src/Pure/context.ML --- a/src/Pure/context.ML +++ b/src/Pure/context.ML @@ -1,827 +1,836 @@ (* Title: Pure/context.ML Author: Markus Wenzel, TU Muenchen Generic theory contexts with unique identity, arbitrarily typed data, monotonic development graph and history support. Generic proof contexts with arbitrarily typed data. Firm naming conventions: thy, thy', thy1, thy2: theory ctxt, ctxt', ctxt1, ctxt2: Proof.context context: Context.generic *) signature BASIC_CONTEXT = sig type theory exception THEORY of string * theory list structure Proof: sig type context end structure Proof_Context: sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context val get_global: {long: bool} -> theory -> string -> Proof.context end end; signature CONTEXT = sig include BASIC_CONTEXT (*theory data*) type data_kind = int val data_kinds: unit -> (data_kind * Position.T) list (*theory context*) type id = int type theory_id val theory_id: theory -> theory_id val data_timing: bool Unsynchronized.ref val parents_of: theory -> theory list val ancestors_of: theory -> theory list val theory_id_ord: theory_id ord val theory_id_name: {long: bool} -> theory_id -> string val theory_long_name: theory -> string val theory_base_name: theory -> string val theory_name: {long: bool} -> theory -> string val theory_identifier: theory -> id val PureN: string val pretty_thy: theory -> Pretty.T val pretty_abbrev_thy: theory -> Pretty.T val get_theory: {long: bool} -> theory -> string -> theory val eq_thy_id: theory_id * theory_id -> bool val eq_thy: theory * theory -> bool val proper_subthy_id: theory_id * theory_id -> bool val proper_subthy: theory * theory -> bool val subthy_id: theory_id * theory_id -> bool val subthy: theory * theory -> bool val join_thys: theory list -> theory val begin_thy: string -> theory list -> theory val finish_thy: theory -> theory val theory_data_sizeof1: theory -> (Position.T * int) list (*proof context*) val raw_transfer: theory -> Proof.context -> Proof.context (*certificate*) datatype certificate = Certificate of theory | Certificate_Id of theory_id val certificate_theory: certificate -> theory val certificate_theory_id: certificate -> theory_id val eq_certificate: certificate * certificate -> bool val join_certificate: certificate * certificate -> certificate + val join_certificate_theory: theory * theory -> theory (*generic context*) datatype generic = Theory of theory | Proof of Proof.context val theory_tracing: bool Unsynchronized.ref val proof_tracing: bool Unsynchronized.ref val enabled_tracing: unit -> bool val finish_tracing: unit -> {contexts: (generic * Position.T) list, active_contexts: int, active_theories: int, active_proofs: int, total_contexts: int, total_theories: int, total_proofs: int} val cases: (theory -> 'a) -> (Proof.context -> 'a) -> generic -> 'a val mapping: (theory -> theory) -> (Proof.context -> Proof.context) -> generic -> generic val mapping_result: (theory -> 'a * theory) -> (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val the_theory: generic -> theory val the_proof: generic -> Proof.context val map_theory: (theory -> theory) -> generic -> generic val map_proof: (Proof.context -> Proof.context) -> generic -> generic val map_theory_result: (theory -> 'a * theory) -> generic -> 'a * generic val map_proof_result: (Proof.context -> 'a * Proof.context) -> generic -> 'a * generic val theory_map: (generic -> generic) -> theory -> theory val proof_map: (generic -> generic) -> Proof.context -> Proof.context val theory_of: generic -> theory (*total*) val proof_of: generic -> Proof.context (*total*) (*thread data*) val get_generic_context: unit -> generic option val put_generic_context: generic option -> unit val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b val the_generic_context: unit -> generic val the_global_context: unit -> theory val the_local_context: unit -> Proof.context val >> : (generic -> generic) -> unit val >>> : (generic -> 'a * generic) -> 'a end; signature PRIVATE_CONTEXT = sig include CONTEXT structure Theory_Data: sig val declare: Position.T -> Any.T -> ((theory * Any.T) list -> Any.T) -> data_kind val get: data_kind -> (Any.T -> 'a) -> theory -> 'a val put: data_kind -> ('a -> Any.T) -> 'a -> theory -> theory end structure Proof_Data: sig val declare: (theory -> Any.T) -> data_kind val get: data_kind -> (Any.T -> 'a) -> Proof.context -> 'a val put: data_kind -> ('a -> Any.T) -> 'a -> Proof.context -> Proof.context end end; structure Context: PRIVATE_CONTEXT = struct (*** type definitions ***) (* context data *) (*private copy avoids potential conflict of table exceptions*) structure Datatab = Table(type key = int val ord = int_ord); type data_kind = int; val data_kind = Counter.make (); (* theory identity *) type id = int; val new_id = Counter.make (); abstype theory_id = Thy_Id of {id: id, (*identifier*) ids: Intset.T, (*cumulative identifiers -- symbolic body content*) name: string, (*official theory name*) stage: int} (*index for anonymous updates*) with fun rep_theory_id (Thy_Id args) = args; val make_theory_id = Thy_Id; end; (* theory allocation state *) type state = {stage: int} Synchronized.var; fun make_state () : state = Synchronized.var "Context.state" {stage = 0}; fun next_stage (state: state) = Synchronized.change_result state (fn {stage} => (stage + 1, {stage = stage + 1})); (* theory and proof context *) datatype theory = Thy_Undef | Thy of (*allocation state*) state * (*identity*) {theory_id: theory_id, theory_token: theory Unsynchronized.ref, theory_token_pos: Position.T} * (*ancestry*) {parents: theory list, (*immediate predecessors*) ancestors: theory list} * (*all predecessors -- canonical reverse order*) (*data*) Any.T Datatab.table; (*body content*) datatype proof = Prf_Undef | Prf of (*identity*) proof Unsynchronized.ref * (*token*) Position.T * (*token_pos*) theory * (*data*) Any.T Datatab.table; structure Proof = struct type context = proof end; datatype generic = Theory of theory | Proof of Proof.context; (* heap allocations *) val theory_tracing = Unsynchronized.ref false; val proof_tracing = Unsynchronized.ref false; fun enabled_tracing () = ! theory_tracing orelse ! proof_tracing; local fun cons_tokens var token = Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens)); fun finish_tokens var = Synchronized.change_result var (fn (n, tokens) => let val tokens' = filter Unsynchronized.weak_active tokens; val results = map_filter Unsynchronized.weak_peek tokens'; in ((n, results), (n, tokens')) end); fun make_token guard var token0 = if ! guard then let val token = Unsynchronized.ref (! token0); val pos = Position.thread_data (); fun assign res = (token := res; cons_tokens var token; res); in (token, pos, assign) end else (token0, Position.none, I); val theory_tokens = Synchronized.var "theory_tokens" (0, []: theory Unsynchronized.weak_ref list); val proof_tokens = Synchronized.var "proof_tokens" (0, []: proof Unsynchronized.weak_ref list); val theory_token0 = Unsynchronized.ref Thy_Undef; val proof_token0 = Unsynchronized.ref Prf_Undef; in fun theory_token () = make_token theory_tracing theory_tokens theory_token0; fun proof_token () = make_token proof_tracing proof_tokens proof_token0; fun finish_tracing () = let val _ = ML_Heap.full_gc (); val (total_theories, token_theories) = finish_tokens theory_tokens; val (total_proofs, token_proofs) = finish_tokens proof_tokens; fun cons1 (thy as Thy (_, {theory_token_pos, ...}, _, _)) = cons (Theory thy, theory_token_pos) | cons1 _ = I; fun cons2 (ctxt as Prf (_, proof_token_pos, _, _)) = cons (Proof ctxt, proof_token_pos) | cons2 _ = I; val contexts = build (fold cons1 token_theories #> fold cons2 token_proofs); val active_theories = fold (fn (Theory _, _) => Integer.add 1 | _ => I) contexts 0; val active_proofs = fold (fn (Proof _, _) => Integer.add 1 | _ => I) contexts 0; in {contexts = contexts, active_contexts = active_theories + active_proofs, active_theories = active_theories, active_proofs = active_proofs, total_contexts = total_theories + total_proofs, total_theories = total_theories, total_proofs = total_proofs} end; end; (*** theory operations ***) fun rep_theory (Thy args) = args; exception THEORY of string * theory list; val state_of = #1 o rep_theory; val theory_identity = #2 o rep_theory; val theory_id = #theory_id o theory_identity; val identity_of = rep_theory_id o theory_id; val ancestry_of = #3 o rep_theory; val data_of = #4 o rep_theory; fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors}; fun stage_final stage = stage = 0; val theory_id_stage = #stage o rep_theory_id; val theory_id_final = stage_final o theory_id_stage; val theory_id_ord = int_ord o apply2 (#id o rep_theory_id); fun theory_id_name {long} thy_id = let val name = #name (rep_theory_id thy_id) in if long then name else Long_Name.base_name name end; val theory_long_name = #name o identity_of; val theory_base_name = Long_Name.base_name o theory_long_name; fun theory_name {long} = if long then theory_long_name else theory_base_name; val theory_identifier = #id o identity_of; val parents_of = #parents o ancestry_of; val ancestors_of = #ancestors o ancestry_of; (* names *) val PureN = "Pure"; fun display_name thy_id = let val name = theory_id_name {long = false} thy_id; val final = theory_id_final thy_id; in if final then name else name ^ ":" ^ string_of_int (theory_id_stage thy_id) end; fun display_names thy = let val name = display_name (theory_id thy); val ancestor_names = map theory_long_name (ancestors_of thy); in rev (name :: ancestor_names) end; val pretty_thy = Pretty.str_list "{" "}" o display_names; val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); fun pretty_abbrev_thy thy = let val names = display_names thy; val n = length names; val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names; in Pretty.str_list "{" "}" abbrev end; fun get_theory long thy name = if theory_name long thy <> name then (case find_first (fn thy' => theory_name long thy' = name) (ancestors_of thy) of SOME thy' => thy' | NONE => error ("Unknown ancestor theory " ^ quote name)) else if theory_id_final (theory_id thy) then thy else error ("Unfinished theory " ^ quote name); (* identity *) fun merge_ids thys = fold (identity_of #> (fn {id, ids, ...} => fn acc => Intset.merge (acc, ids) |> Intset.insert id)) thys Intset.empty; val eq_thy_id = op = o apply2 (#id o rep_theory_id); val eq_thy = op = o apply2 (#id o identity_of); val proper_subthy_id = apply2 rep_theory_id #> (fn ({id, ...}, {ids, ...}) => Intset.member ids id); val proper_subthy = proper_subthy_id o apply2 theory_id; fun subthy_id p = eq_thy_id p orelse proper_subthy_id p; val subthy = subthy_id o apply2 theory_id; (* consistent ancestors *) fun eq_thy_consistent (thy1, thy2) = eq_thy (thy1, thy2) orelse (theory_base_name thy1 = theory_base_name thy2 andalso raise THEORY ("Duplicate theory name", [thy1, thy2])); fun extend_ancestors thy thys = if member eq_thy_consistent thys thy then raise THEORY ("Duplicate theory node", thy :: thys) else thy :: thys; val merge_ancestors = merge eq_thy_consistent; val eq_ancestry = apply2 ancestry_of #> (fn ({parents, ancestors}, {parents = parents', ancestors = ancestors'}) => eq_list eq_thy (parents, parents') andalso eq_list eq_thy (ancestors, ancestors')); (** theory data **) (* data kinds and access methods *) val data_timing = Unsynchronized.ref false; local type kind = {pos: Position.T, empty: Any.T, merge: (theory * Any.T) list -> Any.T}; val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table); fun the_kind k = (case Datatab.lookup (Synchronized.value kinds) k of SOME kind => kind | NONE => raise Fail "Invalid theory data identifier"); in fun data_kinds () = Datatab.fold_rev (fn (k, {pos, ...}) => cons (k, pos)) (Synchronized.value kinds) []; val invoke_pos = #pos o the_kind; val invoke_empty = #empty o the_kind; fun invoke_merge kind args = if ! data_timing then Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind)) (fn () => #merge kind args) else #merge kind args; fun declare_data pos empty merge = let val k = data_kind (); val kind = {pos = pos, empty = empty, merge = merge}; val _ = Synchronized.change kinds (Datatab.update (k, kind)); in k end; fun lookup_data k thy = Datatab.lookup (data_of thy) k; fun get_data k thy = (case lookup_data k thy of SOME x => x | NONE => invoke_empty k); fun merge_data [] = Datatab.empty | merge_data [thy] = data_of thy | merge_data thys = let fun merge (k, kind) data = (case map_filter (fn thy => lookup_data k thy |> Option.map (pair thy)) thys of [] => data | [(_, x)] => Datatab.default (k, x) data | args => Datatab.update (k, invoke_merge kind args) data); in Datatab.fold merge (Synchronized.value kinds) (data_of (hd thys)) end; end; (** build theories **) (* create theory *) fun create_thy state ids name stage ancestry data = let val theory_id = make_theory_id {id = new_id (), ids = ids, name = name, stage = stage}; val (token, pos, assign) = theory_token (); val identity = {theory_id = theory_id, theory_token = token, theory_token_pos = pos}; in assign (Thy (state, identity, ancestry, data)) end; (* primitives *) val pre_pure_thy = let val state = make_state (); val stage = next_stage state; in create_thy state Intset.empty PureN stage (make_ancestry [] []) Datatab.empty end; local fun change_thy finish f thy = let val {name, stage, ...} = identity_of thy; val Thy (state, _, ancestry, data) = thy; val ancestry' = if stage_final stage then make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)) else ancestry; val ids' = merge_ids [thy]; val stage' = if finish then 0 else next_stage state; val data' = f data; in create_thy state ids' name stage' ancestry' data' end; in val update_thy = change_thy false; val finish_thy = change_thy true I; end; (* join: unfinished theory nodes *) fun join_thys [] = raise List.Empty | join_thys thys = let val thy0 = hd thys; val name0 = theory_long_name thy0; val state0 = state_of thy0; fun ok thy = not (theory_id_final (theory_id thy)) andalso theory_long_name thy = name0 andalso eq_ancestry (thy0, thy); val _ = (case filter_out ok thys of [] => () | bad => raise THEORY ("Cannot join theories", bad)); val stage = next_stage state0; val ids = merge_ids thys; val data = merge_data thys; in create_thy state0 ids name0 stage (ancestry_of thy0) data end; (* merge: finished theory nodes *) fun make_parents thys = let val thys' = distinct eq_thy thys in thys' |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys') end; fun begin_thy name imports = if name = "" then error ("Bad theory name: " ^ quote name) else if null imports then error "Missing theory imports" else let val parents = make_parents imports; val ancestors = Library.foldl1 merge_ancestors (map ancestors_of parents) |> fold extend_ancestors parents; val ancestry = make_ancestry parents ancestors; val state = make_state (); val stage = next_stage state; val ids = merge_ids parents; val data = merge_data parents; in create_thy state ids name stage ancestry data |> tap finish_thy end; (* theory data *) structure Theory_Data = struct val declare = declare_data; fun get k dest thy = dest (get_data k thy); fun put k make x = update_thy (Datatab.update (k, make x)); fun sizeof1 k thy = Datatab.lookup (data_of thy) k |> Option.map ML_Heap.sizeof1; end; fun theory_data_sizeof1 thy = build (data_of thy |> Datatab.fold_rev (fn (k, _) => (case Theory_Data.sizeof1 k thy of NONE => I | SOME n => (cons (invoke_pos k, n))))); (*** proof context ***) (* proof data kinds *) local val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table); fun init_data thy = Synchronized.value kinds |> Datatab.map (fn _ => fn init => init thy); fun init_new_data thy = Synchronized.value kinds |> Datatab.fold (fn (k, init) => fn data => if Datatab.defined data k then data else Datatab.update (k, init thy) data); fun init_fallback k thy = (case Datatab.lookup (Synchronized.value kinds) k of SOME init => init thy | NONE => raise Fail "Invalid proof data identifier"); in fun raw_transfer thy' (ctxt as Prf (_, _, thy, data)) = if eq_thy (thy, thy') then ctxt else if proper_subthy (thy, thy') then let val (token', pos', assign) = proof_token (); val data' = init_new_data thy' data; in assign (Prf (token', pos', thy', data')) end else error "Cannot transfer proof context: not a super theory"; structure Proof_Context = struct fun theory_of (Prf (_, _, thy, _)) = thy; fun init_global thy = let val (token, pos, assign) = proof_token () in assign (Prf (token, pos, thy, init_data thy)) end; fun get_global long thy name = init_global (get_theory long thy name); end; structure Proof_Data = struct fun declare init = let val k = data_kind (); val _ = Synchronized.change kinds (Datatab.update (k, init)); in k end; fun get k dest (Prf (_, _, thy, data)) = (case Datatab.lookup data k of SOME x => x | NONE => init_fallback k thy) |> dest; fun put k make x (Prf (_, _, thy, data)) = let val (token', pos', assign) = proof_token (); val data' = Datatab.update (k, make x) data; in assign (Prf (token', pos', thy, data')) end; end; end; (*** theory certificate ***) datatype certificate = Certificate of theory | Certificate_Id of theory_id; fun certificate_theory (Certificate thy) = thy | certificate_theory (Certificate_Id thy_id) = error ("No content for theory certificate " ^ display_name thy_id); fun certificate_theory_id (Certificate thy) = theory_id thy | certificate_theory_id (Certificate_Id thy_id) = thy_id; fun eq_certificate (Certificate thy1, Certificate thy2) = eq_thy (thy1, thy2) | eq_certificate (Certificate_Id thy_id1, Certificate_Id thy_id2) = eq_thy_id (thy_id1, thy_id2) | eq_certificate _ = false; +fun err_join (thy_id1, thy_id2) = + error ("Cannot join unrelated theory certificates " ^ + display_name thy_id1 ^ " and " ^ display_name thy_id2); + fun join_certificate (cert1, cert2) = let val (thy_id1, thy_id2) = apply2 certificate_theory_id (cert1, cert2) in if eq_thy_id (thy_id1, thy_id2) then (case cert1 of Certificate _ => cert1 | _ => cert2) else if proper_subthy_id (thy_id2, thy_id1) then cert1 else if proper_subthy_id (thy_id1, thy_id2) then cert2 - else - error ("Cannot join unrelated theory certificates " ^ - display_name thy_id1 ^ " and " ^ display_name thy_id2) + else err_join (thy_id1, thy_id2) end; +fun join_certificate_theory (thy1, thy2) = + let val (thy_id1, thy_id2) = apply2 theory_id (thy1, thy2) in + if subthy_id (thy_id2, thy_id1) then thy1 + else if proper_subthy_id (thy_id1, thy_id2) then thy2 + else err_join (thy_id1, thy_id2) + end; (*** generic context ***) fun cases f _ (Theory thy) = f thy | cases _ g (Proof prf) = g prf; fun mapping f g = cases (Theory o f) (Proof o g); fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); val the_theory = cases I (fn _ => error "Ill-typed context: theory expected"); val the_proof = cases (fn _ => error "Ill-typed context: proof expected") I; fun map_theory f = Theory o f o the_theory; fun map_proof f = Proof o f o the_proof; fun map_theory_result f = apsnd Theory o f o the_theory; fun map_proof_result f = apsnd Proof o f o the_proof; fun theory_map f = the_theory o f o Theory; fun proof_map f = the_proof o f o Proof; val theory_of = cases I Proof_Context.theory_of; val proof_of = cases Proof_Context.init_global I; (** thread data **) local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in fun get_generic_context () = Thread_Data.get generic_context_var; val put_generic_context = Thread_Data.put generic_context_var; fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context; fun the_generic_context () = (case get_generic_context () of SOME context => context | _ => error "Unknown context"); val the_global_context = theory_of o the_generic_context; val the_local_context = proof_of o the_generic_context; end; fun >>> f = let val (res, context') = f (the_generic_context ()); val _ = put_generic_context (SOME context'); in res end; nonfix >>; fun >> f = >>> (fn context => ((), f context)); val _ = put_generic_context (SOME (Theory pre_pure_thy)); end; structure Basic_Context: BASIC_CONTEXT = Context; open Basic_Context; (*** type-safe interfaces for data declarations ***) (** theory data **) signature THEORY_DATA'_ARGS = sig type T val empty: T val merge: (theory * T) list -> T end; signature THEORY_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature THEORY_DATA = sig type T val get: theory -> T val put: T -> theory -> theory val map: (T -> T) -> theory -> theory end; functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA = struct type T = Data.T; exception Data of T; val kind = let val pos = Position.thread_data () in Context.Theory_Data.declare pos (Data Data.empty) (Data o Data.merge o map (fn (thy, Data x) => (thy, x))) end; val get = Context.Theory_Data.get kind (fn Data x => x); val put = Context.Theory_Data.put kind Data; fun map f thy = put (f (get thy)) thy; end; functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA = Theory_Data' ( type T = Data.T; val empty = Data.empty; fun merge args = Library.foldl (fn (a, (_, b)) => Data.merge (a, b)) (#2 (hd args), tl args) ); (** proof data **) signature PROOF_DATA_ARGS = sig type T val init: theory -> T end; signature PROOF_DATA = sig type T val get: Proof.context -> T val put: T -> Proof.context -> Proof.context val map: (T -> T) -> Proof.context -> Proof.context end; functor Proof_Data(Data: PROOF_DATA_ARGS): PROOF_DATA = struct type T = Data.T; exception Data of T; val kind = Context.Proof_Data.declare (Data o Data.init); val get = Context.Proof_Data.get kind (fn Data x => x); val put = Context.Proof_Data.put kind Data; fun map f prf = put (f (get prf)) prf; end; (** generic data **) signature GENERIC_DATA_ARGS = sig type T val empty: T val merge: T * T -> T end; signature GENERIC_DATA = sig type T val get: Context.generic -> T val put: T -> Context.generic -> Context.generic val map: (T -> T) -> Context.generic -> Context.generic end; functor Generic_Data(Data: GENERIC_DATA_ARGS): GENERIC_DATA = struct structure Thy_Data = Theory_Data(Data); structure Prf_Data = Proof_Data(type T = Data.T val init = Thy_Data.get); type T = Data.T; fun get (Context.Theory thy) = Thy_Data.get thy | get (Context.Proof prf) = Prf_Data.get prf; fun put x (Context.Theory thy) = Context.Theory (Thy_Data.put x thy) | put x (Context.Proof prf) = Context.Proof (Prf_Data.put x prf); fun map f ctxt = put (f (get ctxt)) ctxt; end; (*hide private interface*) structure Context: CONTEXT = Context; diff --git a/src/Pure/morphism.ML b/src/Pure/morphism.ML --- a/src/Pure/morphism.ML +++ b/src/Pure/morphism.ML @@ -1,186 +1,220 @@ (* Title: Pure/morphism.ML Author: Makarius Abstract morphisms on formal entities. *) infix 1 $> signature BASIC_MORPHISM = sig type morphism type declaration = morphism -> Context.generic -> Context.generic val $> : morphism * morphism -> morphism end signature MORPHISM = sig include BASIC_MORPHISM exception MORPHISM of string * exn + val the_theory: theory option -> theory + val set_context: theory -> morphism -> morphism + val reset_context: morphism -> morphism val morphism: string -> - {binding: (binding -> binding) list, - typ: (typ -> typ) list, - term: (term -> term) list, - fact: (thm list -> thm list) list} -> morphism + {binding: (theory option -> binding -> binding) list, + typ: (theory option -> typ -> typ) list, + term: (theory option -> term -> term) list, + fact: (theory option -> thm list -> thm list) list} -> morphism val is_identity: morphism -> bool + val is_empty: morphism -> bool val pretty: morphism -> Pretty.T val binding: morphism -> binding -> binding val binding_prefix: morphism -> (string * bool) list val typ: morphism -> typ -> typ val term: morphism -> term -> term val fact: morphism -> thm list -> thm list val thm: morphism -> thm -> thm val cterm: morphism -> cterm -> cterm val identity: morphism val default: morphism option -> morphism val compose: morphism -> morphism -> morphism val transform: morphism -> (morphism -> 'a) -> morphism -> 'a val form: (morphism -> 'a) -> 'a val binding_morphism: string -> (binding -> binding) -> morphism + val typ_morphism': string -> (theory -> typ -> typ) -> morphism val typ_morphism: string -> (typ -> typ) -> morphism + val term_morphism': string -> (theory -> term -> term) -> morphism val term_morphism: string -> (term -> term) -> morphism val fact_morphism: string -> (thm list -> thm list) -> morphism val thm_morphism: string -> (thm -> thm) -> morphism val transfer_morphism: theory -> morphism val transfer_morphism': Proof.context -> morphism val transfer_morphism'': Context.generic -> morphism val trim_context_morphism: morphism val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism end; structure Morphism: MORPHISM = struct (* named functions *) -type 'a funs = (string * ('a -> 'a)) list; +type 'a funs = (string * (theory option -> 'a -> 'a)) list; exception MORPHISM of string * exn; -fun app (name, f) x = f x +fun app context (name, f) x = f context x handle exn => if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn); -fun apply fs = fold_rev app fs; + +(* optional context *) + +fun the_theory (SOME thy) = thy + | the_theory NONE = raise Fail "Morphism lacks theory context"; + +fun join_transfer (SOME thy) = Thm.join_transfer thy + | join_transfer NONE = I; + +val join_context = join_options Context.join_certificate_theory; (* type morphism *) datatype morphism = Morphism of - {names: string list, + {context: theory option, + names: string list, binding: binding funs, typ: typ funs, term: term funs, fact: thm list funs}; +type declaration = morphism -> Context.generic -> Context.generic; + fun rep (Morphism args) = args; -type declaration = morphism -> Context.generic -> Context.generic; +fun apply which phi = + let val args = rep phi + in fold_rev (app (#context args)) (which args) end; + +fun put_context context (Morphism {context = _, names, binding, typ, term, fact}) = + Morphism {context = context, names = names, binding = binding, typ = typ, term = term, fact = fact}; + +val set_context = put_context o SOME; +val reset_context = put_context NONE; fun morphism a {binding, typ, term, fact} = Morphism { + context = NONE, names = if a = "" then [] else [a], binding = map (pair a) binding, typ = map (pair a) typ, term = map (pair a) term, fact = map (pair a) fact}; (*syntactic test only!*) -fun is_identity (Morphism {names, binding, typ, term, fact}) = +fun is_identity (Morphism {context = _, names, binding, typ, term, fact}) = null names andalso null binding andalso null typ andalso null term andalso null fact; +fun is_empty phi = is_none (#context (rep phi)) andalso is_identity phi; + fun pretty phi = Pretty.enum ";" "{" "}" (map Pretty.str (rev (#names (rep phi)))); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); -val binding = apply o #binding o rep; +val binding = apply #binding; fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of; -val typ = apply o #typ o rep; -val term = apply o #term o rep; -val fact = apply o #fact o rep; +val typ = apply #typ; +val term = apply #term; +fun fact phi = map (join_transfer (#context (rep phi))) #> apply #fact phi; val thm = singleton o fact; val cterm = Drule.cterm_rule o thm; (* morphism combinators *) val identity = morphism "" {binding = [], typ = [], term = [], fact = []}; val default = the_default identity; fun compose phi1 phi2 = - if is_identity phi1 then phi2 - else if is_identity phi2 then phi1 + if is_empty phi1 then phi2 + else if is_empty phi2 then phi1 else let - val {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1} = rep phi1; - val {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2} = rep phi2; + val {context = context1, names = names1, binding = binding1, + typ = typ1, term = term1, fact = fact1} = rep phi1; + val {context = context2, names = names2, binding = binding2, + typ = typ2, term = term2, fact = fact2} = rep phi2; in Morphism { + context = join_context (context1, context2), names = names1 @ names2, binding = binding1 @ binding2, typ = typ1 @ typ2, term = term1 @ term2, fact = fact1 @ fact2} end; fun phi1 $> phi2 = compose phi2 phi1; fun transform phi f = fn psi => f (phi $> psi); fun form f = f identity; (* concrete morphisms *) -fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []}; -fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []}; -fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []}; -fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]}; -fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]}; +fun binding_morphism a binding = morphism a {binding = [K binding], typ = [], term = [], fact = []}; +fun typ_morphism' a typ = morphism a {binding = [], typ = [typ o the_theory], term = [], fact = []}; +fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []}; +fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []}; +fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []}; +fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]}; +fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]}; val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer; val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; val transfer_morphism'' = transfer_morphism o Context.theory_of; val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; (* instantiate *) fun instantiate_frees_morphism (cinstT, cinst) = if TFrees.is_empty cinstT andalso Frees.is_empty cinst then identity else let val instT = TFrees.map (K Thm.typ_of) cinstT; val inst = Frees.map (K Thm.term_of) cinst; in morphism "instantiate_frees" {binding = [], typ = if TFrees.is_empty instT then [] - else [Term_Subst.instantiateT_frees instT], - term = [Term_Subst.instantiate_frees (instT, inst)], - fact = [map (Thm.instantiate_frees (cinstT, cinst))]} + else [K (Term_Subst.instantiateT_frees instT)], + term = [K (Term_Subst.instantiate_frees (instT, inst))], + fact = [K (map (Thm.instantiate_frees (cinstT, cinst)))]} end; fun instantiate_morphism (cinstT, cinst) = if TVars.is_empty cinstT andalso Vars.is_empty cinst then identity else let val instT = TVars.map (K Thm.typ_of) cinstT; val inst = Vars.map (K Thm.term_of) cinst; in morphism "instantiate" {binding = [], typ = if TVars.is_empty instT then [] - else [Term_Subst.instantiateT instT], - term = [Term_Subst.instantiate (instT, inst)], - fact = [map (Thm.instantiate (cinstT, cinst))]} + else [K (Term_Subst.instantiateT instT)], + term = [K (Term_Subst.instantiate (instT, inst))], + fact = [K (map (Thm.instantiate (cinstT, cinst)))]} end; end; structure Basic_Morphism: BASIC_MORPHISM = Morphism; open Basic_Morphism; diff --git a/src/Pure/variable.ML b/src/Pure/variable.ML --- a/src/Pure/variable.ML +++ b/src/Pure/variable.ML @@ -1,787 +1,788 @@ (* Title: Pure/variable.ML Author: Makarius Fixed type/term variables and polymorphic term abbreviations. *) signature VARIABLE = sig val names_of: Proof.context -> Name.context val binds_of: Proof.context -> (typ * term) Vartab.table val maxidx_of: Proof.context -> int val constraints_of: Proof.context -> typ Vartab.table * sort Vartab.table val is_declared: Proof.context -> string -> bool val check_name: binding -> string val default_type: Proof.context -> string -> typ option val def_type: Proof.context -> bool -> indexname -> typ option val def_sort: Proof.context -> indexname -> sort option val declare_maxidx: int -> Proof.context -> Proof.context val declare_names: term -> Proof.context -> Proof.context val declare_constraints: term -> Proof.context -> Proof.context val declare_internal: term -> Proof.context -> Proof.context val declare_term: term -> Proof.context -> Proof.context val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term -> Proof.context -> Proof.context val unbind_term: indexname -> Proof.context -> Proof.context val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term val lookup_const: Proof.context -> string -> string option val is_const: Proof.context -> string -> bool val declare_const: string * string -> Proof.context -> Proof.context val next_bound: string * typ -> Proof.context -> term * Proof.context val revert_bounds: Proof.context -> term -> term val is_body: Proof.context -> bool val set_body: bool -> Proof.context -> Proof.context val restore_body: Proof.context -> Proof.context -> Proof.context val improper_fixes: Proof.context -> Proof.context val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context val is_improper: Proof.context -> string -> bool val is_fixed: Proof.context -> string -> bool val is_newly_fixed: Proof.context -> Proof.context -> string -> bool val fixed_ord: Proof.context -> string ord val intern_fixed: Proof.context -> string -> string val lookup_fixed: Proof.context -> string -> string option val revert_fixed: Proof.context -> string -> string val markup_fixed: Proof.context -> string -> Markup.T val markup: Proof.context -> string -> Markup.T val markup_entity_def: Proof.context -> string -> Markup.T val dest_fixes: Proof.context -> (string * string) list val add_fixed_names: Proof.context -> term -> string list -> string list val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list val add_newly_fixed: Proof.context -> Proof.context -> term -> (string * typ) list -> (string * typ) list val add_free_names: Proof.context -> term -> string list -> string list val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context val add_fixes: string list -> Proof.context -> string list * Proof.context val add_fixes_direct: string list -> Proof.context -> Proof.context val add_fixes_implicit: term -> Proof.context -> Proof.context val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context val gen_all: Proof.context -> thm -> thm val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list val exportT: Proof.context -> Proof.context -> thm list -> thm list val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof val export: Proof.context -> Proof.context -> thm list -> thm list val export_morphism: Proof.context -> Proof.context -> morphism val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context val import_inst: bool -> term list -> Proof.context -> (typ TVars.table * term Vars.table) * Proof.context val importT_terms: term list -> Proof.context -> term list * Proof.context val import_terms: bool -> term list -> Proof.context -> term list * Proof.context val importT: thm list -> Proof.context -> (ctyp TVars.table * thm list) * Proof.context val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context val import: bool -> thm list -> Proof.context -> ((ctyp TVars.table * cterm Vars.table) * thm list) * Proof.context val import_vars: Proof.context -> thm -> thm val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list val dest_abs: term -> Proof.context -> ((string * typ) * term) * Proof.context val dest_abs_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context val dest_all: term -> Proof.context -> ((string * typ) * term) * Proof.context val dest_all_cterm: cterm -> Proof.context -> (cterm * cterm) * Proof.context val is_bound_focus: Proof.context -> bool val set_bound_focus: bool -> Proof.context -> Proof.context val restore_bound_focus: Proof.context -> Proof.context -> Proof.context val focus_params: binding list option -> term -> Proof.context -> (string list * (string * typ) list) * Proof.context val focus: binding list option -> term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context val focus_cterm: binding list option -> cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context val focus_subgoal: binding list option -> int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context val warn_extra_tfrees: Proof.context -> Proof.context -> unit val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list val polymorphic: Proof.context -> term list -> term list end; structure Variable: VARIABLE = struct (** local context data **) type fixes = (string * bool) Name_Space.table; val empty_fixes: fixes = Name_Space.empty_table Markup.fixedN; datatype data = Data of {names: Name.context, (*type/term variable names*) consts: string Symtab.table, (*consts within the local scope*) bounds: int * ((string * typ) * string) list, (*next index, internal name, type, external name*) fixes: fixes, (*term fixes -- global name space, intern ~> extern*) binds: (typ * term) Vartab.table, (*term bindings*) type_occs: string list Symtab.table, (*type variables -- possibly within term variables*) maxidx: int, (*maximum var index*) constraints: typ Vartab.table * (*type constraints*) sort Vartab.table}; (*default sorts*) fun make_data (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) = Data {names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, type_occs = type_occs, maxidx = maxidx, constraints = constraints}; val empty_data = make_data (Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, Symtab.empty, ~1, (Vartab.empty, Vartab.empty)); structure Data = Proof_Data ( type T = data; fun init _ = empty_data; ); fun map_data f = Data.map (fn Data {names, consts, bounds, fixes, binds, type_occs, maxidx, constraints} => make_data (f (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints))); fun map_names f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (f names, consts, bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_consts f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, f consts, bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_bounds f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, f bounds, fixes, binds, type_occs, maxidx, constraints)); fun map_fixes f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, f fixes, binds, type_occs, maxidx, constraints)); fun map_binds f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, f binds, type_occs, maxidx, constraints)); fun map_type_occs f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, f type_occs, maxidx, constraints)); fun map_maxidx f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, type_occs, f maxidx, constraints)); fun map_constraints f = map_data (fn (names, consts, bounds, fixes, binds, type_occs, maxidx, constraints) => (names, consts, bounds, fixes, binds, type_occs, maxidx, f constraints)); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); val names_of = #names o rep_data; val fixes_of = #fixes o rep_data; val fixes_space = Name_Space.space_of_table o fixes_of; val binds_of = #binds o rep_data; val type_occs_of = #type_occs o rep_data; val maxidx_of = #maxidx o rep_data; val constraints_of = #constraints o rep_data; val is_declared = Name.is_declared o names_of; val check_name = Name_Space.base_name o tap Binding.check; (** declarations **) (* default sorts and types *) fun default_type ctxt x = Vartab.lookup (#1 (constraints_of ctxt)) (x, ~1); fun def_type ctxt pattern xi = let val {binds, constraints = (types, _), ...} = rep_data ctxt in (case Vartab.lookup types xi of NONE => if pattern then NONE else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1) | some => some) end; val def_sort = Vartab.lookup o #2 o constraints_of; (* maxidx *) val declare_maxidx = map_maxidx o Integer.max; (* names *) fun declare_type_names t = map_names (fold_types (fold_atyps Term.declare_typ_names) t) #> map_maxidx (fold_types Term.maxidx_typ t); fun declare_names t = declare_type_names t #> map_names (fold_aterms Term.declare_term_frees t) #> map_maxidx (Term.maxidx_term t); (* type occurrences *) fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T; val decl_type_occs = fold_term_types (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I) | _ => decl_type_occsT); val declare_type_occsT = map_type_occs o fold_types decl_type_occsT; val declare_type_occs = map_type_occs o decl_type_occs; (* constraints *) fun constrain_tvar (xi, raw_S) = let val S = #2 (Term_Position.decode_positionS raw_S) in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; fun declare_constraints t = map_constraints (fn (types, sorts) => let val types' = fold_aterms (fn Free (x, T) => Vartab.update ((x, ~1), T) | Var v => Vartab.update v | _ => I) t types; val sorts' = (fold_types o fold_atyps) (fn TFree (x, S) => constrain_tvar ((x, ~1), S) | TVar v => constrain_tvar v | _ => I) t sorts; in (types', sorts') end) #> declare_type_occsT t #> declare_type_names t; (* common declarations *) fun declare_internal t = declare_names t #> declare_type_occs t #> Thm.declare_term_sorts t; fun declare_term t = declare_internal t #> declare_constraints t; val declare_typ = declare_term o Logic.mk_type; val declare_prf = Proofterm.fold_proof_terms_types declare_internal (declare_internal o Logic.mk_type); val declare_thm = Thm.fold_terms {hyps = true} declare_internal; (* renaming term/type frees *) fun variant_frees ctxt ts frees = let val names = names_of (fold declare_names ts ctxt); val xs = fst (fold_map Name.variant (map #1 frees) names); in xs ~~ map snd frees end; (** term bindings **) fun bind_term ((x, i), t) = let val u = Term.close_schematic_term t; val U = Term.fastype_of u; in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end; val unbind_term = map_binds o Vartab.delete_safe; fun maybe_bind_term (xi, SOME t) = bind_term (xi, t) | maybe_bind_term (xi, NONE) = unbind_term xi; fun expand_binds ctxt = let val binds = binds_of ctxt; val get = fn Var (xi, _) => Vartab.lookup binds xi | _ => NONE; in Envir.beta_norm o Envir.expand_term get end; (** consts **) val lookup_const = Symtab.lookup o #consts o rep_data; val is_const = is_some oo lookup_const; val declare_fixed = map_consts o Symtab.delete_safe; val declare_const = map_consts o Symtab.update; (** bounds **) fun inc_bound (a, T) ctxt = let val b = Name.bound (#1 (#bounds (rep_data ctxt))); val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds)); in (Free (b, T), ctxt') end; fun next_bound a ctxt = let val (x as Free (b, _), ctxt') = inc_bound a ctxt in if Name.is_declared (names_of ctxt') b then inc_bound a ctxt' else (x, ctxt') end; fun revert_bounds ctxt t = (case #2 (#bounds (rep_data ctxt)) of [] => t | bounds => let val names = Term.declare_term_names t (names_of ctxt); val xs = rev (#1 (fold_map Name.variant (rev (map #2 bounds)) names)); fun substs (((b, T), _), x') = let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U)) in [subst T, subst (Type_Annotation.ignore_type T)] end; in Term.subst_atomic (maps substs (bounds ~~ xs)) t end); (** fixes **) (* inner body mode *) val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false); val is_body = Config.apply inner_body; val set_body = Config.put inner_body; val restore_body = set_body o is_body; (* proper mode *) val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true); val improper_fixes = Config.put proper_fixes false; val restore_proper_fixes = Config.put proper_fixes o Config.apply proper_fixes; fun is_improper ctxt x = (case Name_Space.lookup (fixes_of ctxt) x of SOME (_, proper) => not proper | NONE => false); (* specialized name space *) val is_fixed = Name_Space.defined o fixes_of; fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); val fixed_ord = Name_Space.entry_ord o fixes_space; val intern_fixed = Name_Space.intern o fixes_space; fun lookup_fixed ctxt x = let val x' = intern_fixed ctxt x in if is_fixed ctxt x' then SOME x' else NONE end; fun revert_fixed ctxt x = (case Name_Space.lookup (fixes_of ctxt) x of SOME (x', _) => if intern_fixed ctxt x' = x then x' else x | NONE => x); fun markup_fixed ctxt x = Name_Space.markup (fixes_space ctxt) x |> Markup.name (revert_fixed ctxt x); fun markup ctxt x = if is_improper ctxt x then Markup.improper else if Name.is_skolem x then Markup.skolem else Markup.free; val markup_entity_def = Name_Space.markup_def o fixes_space; fun dest_fixes ctxt = Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); (* collect variables *) fun add_free_names ctxt = fold_aterms (fn Free (x, _) => not (is_fixed ctxt x) ? insert (op =) x | _ => I); fun add_frees ctxt = fold_aterms (fn Free (x, T) => not (is_fixed ctxt x) ? insert (op =) (x, T) | _ => I); fun add_fixed_names ctxt = fold_aterms (fn Free (x, _) => is_fixed ctxt x ? insert (op =) x | _ => I); fun add_fixed ctxt = fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I); fun add_newly_fixed ctxt' ctxt = fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I); (* declarations *) local fun err_dups dups = error ("Duplicate fixed variable(s): " ^ commas (map Binding.print dups)); fun new_fixed ((x, x'), pos) ctxt = if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)] else let val proper = Config.get ctxt proper_fixes; val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming) |> Context_Position.set_visible_generic false; in ctxt |> map_fixes (Name_Space.define context true (Binding.make (x', pos), (x, proper)) #> snd #> x <> "" ? Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x') |> declare_fixed x |> declare_constraints (Syntax.free x') end; fun new_fixes names' args = map_names (K names') #> fold new_fixed args #> pair (map (#2 o #1) args); in fun add_fixes_binding bs ctxt = let val _ = (case filter (Name.is_skolem o Binding.name_of) bs of [] => () | bads => error ("Illegal internal Skolem constant(s): " ^ commas (map Binding.print bads))); val _ = (case duplicates (op = o apply2 Binding.name_of) bs of [] => () | dups => err_dups dups); val xs = map check_name bs; val names = names_of ctxt; val (xs', names') = if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem else (xs, fold Name.declare xs names); in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; fun variant_names ctxt raw_xs = let val names = names_of ctxt; val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); in (names', xs ~~ xs') end; fun variant_fixes xs ctxt = let val (names', vs) = variant_names ctxt xs; in ctxt |> new_fixes names' (map (rpair Position.none) vs) end; fun bound_fixes xs ctxt = let val (names', vs) = variant_names ctxt (map #1 xs); val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt; val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys; in ctxt' |> new_fixes names' fixes end; end; val add_fixes = add_fixes_binding o map Binding.name; fun add_fixes_direct xs ctxt = ctxt |> set_body false |> (snd o add_fixes xs) |> restore_body ctxt; fun add_fixes_implicit t ctxt = ctxt |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t [])); (* dummy patterns *) fun fix_dummy_patterns (Const ("Pure.dummy_pattern", T)) ctxt = let val ([x], ctxt') = ctxt |> set_body true |> add_fixes [Name.uu_] ||> restore_body ctxt in (Free (x, T), ctxt') end | fix_dummy_patterns (Abs (x, T, b)) ctxt = let val (b', ctxt') = fix_dummy_patterns b ctxt in (Abs (x, T, b'), ctxt') end | fix_dummy_patterns (t $ u) ctxt = let val (t', ctxt') = fix_dummy_patterns t ctxt; val (u', ctxt'') = fix_dummy_patterns u ctxt'; in (t' $ u', ctxt'') end | fix_dummy_patterns a ctxt = (a, ctxt); (** export -- generalize type/term variables (beware of closure sizes) **) fun gen_all ctxt th = let val i = Thm.maxidx_thm th (maxidx_of ctxt) + 1; fun gen (x, T) = Thm.forall_elim (Thm.cterm_of ctxt (Var ((x, i), T))); in fold gen (Drule.outer_params (Thm.prop_of th)) th end; fun export_inst inner outer = let val declared_outer = is_declared outer; val still_fixed = not o is_newly_fixed inner outer; val gen_fixes = Names.build (fixes_of inner |> Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Names.add_set y)); val type_occs_inner = type_occs_of inner; fun gen_fixesT ts = Names.build (fold decl_type_occs ts type_occs_inner |> Symtab.fold (fn (a, xs) => if declared_outer a orelse exists still_fixed xs then I else Names.add_set a)); in (gen_fixesT, gen_fixes) end; fun exportT_inst inner outer = #1 (export_inst inner outer); fun exportT_terms inner outer = let val mk_tfrees = exportT_inst inner outer; val maxidx = maxidx_of outer; in fn ts => ts |> map (Term_Subst.generalize (mk_tfrees ts, Names.empty) (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) end; fun export_terms inner outer = let val (mk_tfrees, tfrees) = export_inst inner outer; val maxidx = maxidx_of outer; in fn ts => ts |> map (Term_Subst.generalize (mk_tfrees ts, tfrees) (fold Term.maxidx_term ts maxidx + 1)) end; fun export_prf inner outer prf = let val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; val tfrees = mk_tfrees []; val maxidx = maxidx_of outer; val idx = Proofterm.maxidx_proof prf maxidx + 1; val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; val gen_typ = Term_Subst.generalizeT_same tfrees idx; in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; fun gen_export (mk_tfrees, frees) maxidx ths = let val tfrees = mk_tfrees (map Thm.full_prop_of ths); val idx = fold Thm.maxidx_thm ths maxidx + 1; in map (Thm.generalize (tfrees, frees) idx) ths end; fun exportT inner outer = gen_export (exportT_inst inner outer, Names.empty) (maxidx_of outer); fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); fun export_morphism inner outer = let val fact = export inner outer; val term = singleton (export_terms inner outer); val typ = Logic.type_map term; in - Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]} + Morphism.morphism "Variable.export" + {binding = [], typ = [K typ], term = [K term], fact = [K fact]} end; (** import -- fix schematic type/term variables **) fun invent_types Ss ctxt = let val tfrees = Name.invent (names_of ctxt) Name.aT (length Ss) ~~ Ss; val ctxt' = fold (declare_constraints o Logic.mk_type o TFree) tfrees ctxt; in (tfrees, ctxt') end; fun importT_inst ts ctxt = let val tvars = TVars.build (fold TVars.add_tvars ts) |> TVars.list_set; val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt; val instT = TVars.build (fold2 (fn a => fn b => TVars.add (a, TFree b)) tvars tfrees); in (instT, ctxt') end; fun import_inst is_open ts ctxt = let val ren = Name.clean #> (if is_open then I else Name.internal); val (instT, ctxt') = importT_inst ts ctxt; val vars = Vars.build (fold Vars.add_vars ts) |> Vars.list_set |> map (apsnd (Term_Subst.instantiateT instT)); val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt'; val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys); in ((instT, inst), ctxt'') end; fun importT_terms ts ctxt = let val (instT, ctxt') = importT_inst ts ctxt in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end; fun import_terms is_open ts ctxt = let val (inst, ctxt') = import_inst is_open ts ctxt in (map (Term_Subst.instantiate inst) ts, ctxt') end; fun importT ths ctxt = let val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; val ths' = map (Thm.instantiate (instT', Vars.empty)) ths; in ((instT', ths'), ctxt') end; fun import_prf is_open prf ctxt = let val ts = rev (Proofterm.fold_proof_terms_types cons (cons o Logic.mk_type) prf []); val (insts, ctxt') = import_inst is_open ts ctxt; in (Proofterm.instantiate insts prf, ctxt') end; fun import is_open ths ctxt = let val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; val instT' = TVars.map (K (Thm.ctyp_of ctxt')) instT; val inst' = Vars.map (K (Thm.cterm_of ctxt')) inst; val ths' = map (Thm.instantiate (instT', inst')) ths; in (((instT', inst'), ths'), ctxt') end; fun import_vars ctxt th = let val ((_, [th']), _) = ctxt |> set_body false |> import true [th]; in th' end; (* import/export *) fun gen_trade imp exp f ctxt ths = let val ((_, ths'), ctxt') = imp ths ctxt in exp ctxt' ctxt (f ctxt' ths') end; val tradeT = gen_trade importT exportT; val trade = gen_trade (import true) export; (* destruct binders *) local fun gen_dest_abs exn dest term_of arg ctxt = (case term_of arg of Abs (a, T, _) => let val (x, ctxt') = yield_singleton bound_fixes (a, T) ctxt; val res = dest x arg handle Term.USED_FREE _ => raise Fail ("Bad context: clash of fresh free for bound: " ^ Syntax.string_of_term ctxt (Free (x, T)) ^ " vs. " ^ Syntax.string_of_term ctxt' (Free (x, T))); in (res, ctxt') end | _ => raise exn ("dest_abs", [arg])); in val dest_abs = gen_dest_abs TERM Term.dest_abs_fresh I; val dest_abs_cterm = gen_dest_abs CTERM Thm.dest_abs_fresh Thm.term_of; fun dest_all t ctxt = (case t of Const ("Pure.all", _) $ u => dest_abs u ctxt | _ => raise TERM ("dest_all", [t])); fun dest_all_cterm ct ctxt = (case Thm.term_of ct of Const ("Pure.all", _) $ _ => dest_abs_cterm (Thm.dest_arg ct) ctxt | _ => raise CTERM ("dest_all", [ct])); end; (* focus on outermost parameters: \x y z. B *) val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false); val is_bound_focus = Config.apply bound_focus; val set_bound_focus = Config.put bound_focus; val restore_bound_focus = set_bound_focus o is_bound_focus; fun focus_params bindings t ctxt = let val ps = Term.variant_frees t (Term.strip_all_vars t); (*as they are printed :-*) val (xs, Ts) = split_list ps; val (xs', ctxt') = (case bindings of SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt | NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt); val ps' = xs' ~~ Ts; val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps'; in ((xs, ps'), ctxt'') end; fun focus bindings t ctxt = let val ((xs, ps), ctxt') = focus_params bindings t ctxt; val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t); in (((xs ~~ ps), t'), ctxt') end; fun forall_elim_prop t prop = Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t) |> Thm.cprop_of |> Thm.dest_arg; fun focus_cterm bindings goal ctxt = let val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt; val ps' = map (Thm.cterm_of ctxt' o Free) ps; val goal' = fold forall_elim_prop ps' goal; in ((xs ~~ ps', goal'), ctxt') end; fun focus_subgoal bindings i st = let val all_vars = Vars.build (Thm.fold_terms {hyps = false} Vars.add_vars st); in Vars.fold (unbind_term o #1 o #1) all_vars #> Vars.fold (declare_constraints o Var o #1) all_vars #> focus_cterm bindings (Thm.cprem_of st i) end; (** implicit polymorphism **) (* warn_extra_tfrees *) fun warn_extra_tfrees ctxt1 ctxt2 = let fun occs_typ a = Term.exists_subtype (fn TFree (b, _) => a = b | _ => false); fun occs_free a x = (case def_type ctxt1 false (x, ~1) of SOME T => if occs_typ a T then I else cons (a, x) | NONE => cons (a, x)); val occs1 = type_occs_of ctxt1; val occs2 = type_occs_of ctxt2; val extras = Symtab.fold (fn (a, xs) => if Symtab.defined occs1 a then I else fold (occs_free a) xs) occs2 []; val tfrees = map #1 extras |> sort_distinct string_ord; val frees = map #2 extras |> sort_distinct string_ord; in if null extras orelse not (Context_Position.is_visible ctxt2) then () else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^ space_implode " or " (map quote frees)) end; (* polymorphic terms *) fun polymorphic_types ctxt ts = let val ctxt' = fold declare_term ts ctxt; val occs = type_occs_of ctxt; val occs' = type_occs_of ctxt'; val types = Names.build (occs' |> Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else Names.add_set a)); val idx = maxidx_of ctxt' + 1; val Ts' = (fold o fold_types o fold_atyps) (fn T as TFree _ => (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I) | _ => I) ts []; val ts' = map (Term_Subst.generalize (types, Names.empty) idx) ts; in (rev Ts', ts') end; fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts); end;