# HG changeset patch # User wenzelm # Date 1681813417 -7200 # Node ID 1156aa9db7f5b4ec55601791ba655ead96a2e3bb # Parent 6ea0030b9ee9285ad3ed098eb38fb6551c806ac0 backout 4a174bea55e2; diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Doc/Implementation/Logic.thy Tue Apr 18 12:23:37 2023 +0200 @@ -949,7 +949,7 @@ text %mlref \ \begin{mldecls} - @{define_ML Thm.extra_shyps: "thm -> Sortset.T"} \\ + @{define_ML Thm.extra_shyps: "thm -> sort list"} \\ @{define_ML Thm.strip_shyps: "thm -> thm"} \\ \end{mldecls} @@ -971,7 +971,7 @@ theorem (in empty) false: False using bad by blast -ML_val \\<^assert> (Sortset.dest (Thm.extra_shyps @{thm false}) = [\<^sort>\empty\])\ +ML_val \\<^assert> (Thm.extra_shyps @{thm false} = [\<^sort>\empty\])\ text \ Thanks to the inference kernel managing sort hypothesis according to their diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/HOL/Matrix_LP/Compute_Oracle/compute.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML Tue Apr 18 12:23:37 2023 +0200 @@ -17,7 +17,7 @@ val make_with_cache : machine -> theory -> term list -> thm list -> computer val theory_of : computer -> theory val hyps_of : computer -> term list - val shyps_of : computer -> Sortset.T + val shyps_of : computer -> sort list (* ! *) val update : computer -> thm list -> unit (* ! *) val update_with_cache : computer -> term list -> thm list -> unit @@ -169,12 +169,13 @@ fun default_naming i = "v_" ^ string_of_int i datatype computer = Computer of - (theory * Encode.encoding * term list * Sortset.T * prog * unit Unsynchronized.ref * naming) + (theory * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) option Unsynchronized.ref fun theory_of (Computer (Unsynchronized.ref (SOME (thy,_,_,_,_,_,_)))) = thy fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps -fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shypset,_,_,_)))) = shypset +fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) +fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding @@ -187,7 +188,7 @@ fun ref_of (Computer r) = r -datatype cthm = ComputeThm of term list * Sortset.T * term +datatype cthm = ComputeThm of term list * sort list * term fun thm2cthm th = (if not (null (Thm.tpairs_of th)) then raise Make "theorems may not contain tpairs" else (); @@ -219,11 +220,11 @@ (n, vars, AbstractMachine.PConst (c, args@[pb])) end - fun thm2rule (encoding, hyptable, shypset) th = + fun thm2rule (encoding, hyptable, shyptable) th = let val (ComputeThm (hyps, shyps, prop)) = th val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable - val shypset = Sortset.merge (shyps, shypset) + val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) val (a, b) = Logic.dest_equals prop handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)") @@ -269,15 +270,15 @@ fun rename_guard (AbstractMachine.Guard (a,b)) = AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) in - ((encoding, hyptable, shypset), (map rename_guard prems, pattern, rename 0 vars right)) + ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right)) end - val ((encoding, hyptable, shypset), rules) = + val ((encoding, hyptable, shyptable), rules) = fold_rev (fn th => fn (encoding_hyptable, rules) => let val (encoding_hyptable, rule) = thm2rule encoding_hyptable th in (encoding_hyptable, rule::rules) end) - ths ((encoding, Termtab.empty, Sortset.empty), []) + ths ((encoding, Termtab.empty, Sorttab.empty), []) fun make_cache_pattern t (encoding, cache_patterns) = let @@ -298,9 +299,9 @@ fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - val shypset = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shypset shypset + val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - in (thy, encoding, Termtab.keys hyptable, shypset, prog, stamp, default_naming) end + in (thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end fun make_with_cache machine thy cache_patterns raw_thms = Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) @@ -334,19 +335,23 @@ Termtab.keys (add hyps2 (add hyps1 Termtab.empty)) end +fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab + +fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) + val (_, export_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\compute\, fn (thy, hyps, shyps, prop) => let - fun remove_term t = Sortset.subtract (Sortset.build (Sortset.insert_term t)) + val shyptab = add_shyps shyps Sorttab.empty + fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab + fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - val shyps = Sortset.fold (fn s => has_witness s ? Sortset.remove s) shyps shyps - val shyps = - if Sortset.is_empty shyps then Sortset.empty - else fold remove_term (prop::hyps) shyps + val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab + val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) val _ = - if not (Sortset.is_empty shyps) then + if not (null shyps) then raise Compute ("dangling sort hypotheses: " ^ - commas (map (Syntax.string_of_sort_global thy) (Sortset.dest shyps))) + commas (map (Syntax.string_of_sort_global thy) shyps)) else () in Thm.global_cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) @@ -374,7 +379,7 @@ val t = infer_types naming encoding ty t val eq = Logic.mk_equals (t', t) in - export_thm thy (hyps_of computer) (shyps_of computer) eq + export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq end (* --------- Simplify ------------ *) @@ -382,7 +387,7 @@ datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int | Prem of AbstractMachine.term datatype theorem = Theorem of theory * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table - * prem list * AbstractMachine.term * term list * Sortset.T + * prem list * AbstractMachine.term * term list * sort list exception ParamSimplify of computer * theorem @@ -614,7 +619,7 @@ val th = update_varsubst varsubst th val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th - val th = update_shyps (Sortset.merge (shyps_of_theorem th, shyps_of_theorem th')) th + val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th in update_theory thy th end @@ -631,9 +636,10 @@ fun runprem p = run (prem2term p) val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th)) val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th) - val shyps = Sortset.merge (shyps_of_theorem th, shyps_of computer) + val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer)) in export_thm (theory_of_theorem th) hyps shyps prop end end + diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/HOL/Matrix_LP/Compute_Oracle/linker.ML --- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Tue Apr 18 12:23:37 2023 +0200 @@ -365,12 +365,12 @@ (!changed, result) end -datatype cthm = ComputeThm of term list * Sortset.T * term +datatype cthm = ComputeThm of term list * sort list * term fun thm2cthm th = ComputeThm (Thm.hyps_of th, Thm.shyps_of th, Thm.prop_of th) val cthm_ord' = - prod_ord (prod_ord (list_ord Term_Ord.term_ord) Sortset.ord) Term_Ord.term_ord + prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/HOL/Types_To_Sets/internalize_sort.ML --- a/src/HOL/Types_To_Sets/internalize_sort.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML Tue Apr 18 12:23:37 2023 +0200 @@ -31,7 +31,7 @@ val thy = Thm.theory_of_thm thm; val tvar = Thm.typ_of ctvar; - val (ucontext, _) = Logic.unconstrainT Sortset.empty (Thm.prop_of thm); + val (ucontext, _) = Logic.unconstrainT [] (Thm.prop_of thm); fun is_proper_class thy = can (Axclass.get_info thy); (* trick by FH *) fun reduce_to_non_proper_sort (TVar (name, sort)) = diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/Thy/export_theory.ML Tue Apr 18 12:23:37 2023 +0200 @@ -264,7 +264,7 @@ in ((sorts @ typargs, args, prop), proof) end; fun standard_prop_of thm = - standard_prop Name.context (Sortset.dest (Thm.extra_shyps thm)) (Thm.full_prop_of thm); + standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm); val encode_prop = let open XML.Encode Term_XML.Encode diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/envir.ML --- a/src/Pure/envir.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/envir.ML Tue Apr 18 12:23:37 2023 +0200 @@ -17,7 +17,7 @@ val empty: int -> env val init: env val merge: env * env -> env - val insert_sorts: env -> Sortset.T -> Sortset.T + val insert_sorts: env -> sort list -> sort list val genvars: string -> env * typ list -> env * term list val genvar: string -> env * typ -> env * term val lookup1: tenv -> indexname * typ -> term option @@ -94,7 +94,7 @@ (*NB: type unification may invent new sorts*) (* FIXME tenv!? *) -val insert_sorts = Vartab.fold (Sortset.insert_typ o #2 o #2) o type_env; +val insert_sorts = Vartab.fold (Sorts.insert_typ o #2 o #2) o type_env; (*Generate a list of distinct variables. Increments index to make them distinct from ALL present variables. *) diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/logic.ML Tue Apr 18 12:23:37 2023 +0200 @@ -66,7 +66,7 @@ map_atyps: typ -> typ, constraints: ((typ * class) * term) list, outer_constraints: (typ * class) list}; - val unconstrainT: Sortset.T -> term -> unconstrain_context * term + val unconstrainT: sort list -> term -> unconstrain_context * term val protectC: term val protect: term -> term val unprotect: term -> term @@ -365,7 +365,7 @@ fun unconstrainT shyps prop = let val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []); - val extra = Sortset.dest (fold (Sortset.remove o #2) present shyps); + val extra = fold (Sorts.remove_sort o #2) present shyps; val n = length present; val (names1, names2) = Name.invent Name.context Name.aT (n + length extra) |> chop n; diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/more_thm.ML Tue Apr 18 12:23:37 2023 +0200 @@ -57,7 +57,7 @@ val undeclared_hyps: Context.generic -> thm -> term list val check_hyps: Context.generic -> thm -> thm val declare_term_sorts: term -> Proof.context -> Proof.context - val extra_shyps': Proof.context -> thm -> Sortset.T + val extra_shyps': Proof.context -> thm -> sort list val check_shyps: Proof.context -> thm -> thm val weaken_sorts': Proof.context -> cterm -> cterm val elim_implies: thm -> thm -> thm @@ -253,8 +253,8 @@ structure Hyps = Proof_Data ( - type T = {checked_hyps: bool, hyps: Termset.T, shyps: Sortset.T}; - fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = Sortset.empty}; + type T = {checked_hyps: bool, hyps: Termset.T, shyps: sort Ord_List.T}; + fun init _ : T = {checked_hyps = true, hyps = Termset.empty, shyps = []}; ); fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => @@ -299,19 +299,19 @@ fun declare_term_sorts t = map_hyps (fn (checked_hyps, hyps, shyps) => - (checked_hyps, hyps, Sortset.insert_term t shyps)); + (checked_hyps, hyps, Sorts.insert_term t shyps)); fun extra_shyps' ctxt th = - Sortset.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); + Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); fun check_shyps ctxt raw_th = let val th = Thm.strip_shyps raw_th; val extra_shyps = extra_shyps' ctxt th; in - if Sortset.is_empty extra_shyps then th + if null extra_shyps then th else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: - Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) (Sortset.dest extra_shyps))))) + Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) end; val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; @@ -718,7 +718,7 @@ |> perhaps (try Thm.strip_shyps); val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; - val extra_shyps = Sortset.dest (extra_shyps' ctxt th); + val extra_shyps = extra_shyps' ctxt th; val tags = Thm.get_tags th; val tpairs = Thm.tpairs_of th; diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 18 12:23:37 2023 +0200 @@ -136,7 +136,7 @@ val abstract_rule_proof: string * term -> proof -> proof val combination_proof: term -> term -> term -> term -> proof -> proof -> proof val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list -> - Sortset.T -> proof -> proof + sort list -> proof -> proof val of_sort_proof: Sorts.algebra -> (class * class -> proof) -> (string * class list list * class -> proof) -> @@ -177,19 +177,19 @@ val export_proof_boxes: proof_body list -> unit val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body val thm_proof: theory -> (class * class -> proof) -> - (string * class list list * class -> proof) -> string * Position.T -> Sortset.T -> + (string * class list list * class -> proof) -> string * Position.T -> sort list -> term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof val unconstrain_thm_proof: theory -> (class * class -> proof) -> - (string * class list list * class -> proof) -> Sortset.T -> term -> + (string * class list list * class -> proof) -> sort list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof - val get_identity: Sortset.T -> term list -> term -> proof -> + val get_identity: sort list -> term list -> term -> proof -> {serial: serial, theory_name: string, name: string} option - val get_approximative_name: Sortset.T -> term list -> term -> proof -> string + val get_approximative_name: sort list -> term list -> term -> proof -> string type thm_id = {serial: serial, theory_name: string} val make_thm_id: serial * string -> thm_id val thm_header_id: thm_header -> thm_id val thm_id: thm -> thm_id - val get_id: Sortset.T -> term list -> term -> proof -> thm_id option + val get_id: sort list -> term list -> term -> proof -> thm_id option val this_id: thm_id option -> thm_id -> bool val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} -> proof list -> (thm_header * proof) list (*exception MIN_PROOF*) @@ -1086,7 +1086,7 @@ fun strip_shyps_proof algebra present witnessed extra prf = let - val replacements = present @ witnessed @ map (`Logic.dummy_tfree) (Sortset.dest extra); + val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra; fun get_replacement S = replacements |> get_first (fn (T', S') => if Sorts.sort_le algebra (S', S) then SOME T' else NONE); @@ -1182,7 +1182,7 @@ fun const_proof mk name prop = let val args = prop_args prop; - val ({outer_constraints, ...}, prop1) = Logic.unconstrainT Sortset.empty prop; + val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop; val head = mk (name, prop1, NONE); in proof_combP (proof_combt' (head, args), map PClass outer_constraints) end; diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/sorts.ML Tue Apr 18 12:23:37 2023 +0200 @@ -14,6 +14,16 @@ signature SORTS = sig + val make: sort list -> sort Ord_List.T + val subset: sort Ord_List.T * sort Ord_List.T -> bool + val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T + val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T + val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T + val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T + val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T + val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T + val insert_term: term -> sort Ord_List.T -> sort Ord_List.T + val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T type algebra val classes_of: algebra -> serial Graph.T val arities_of: algebra -> (class * sort list) list Symtab.table @@ -59,6 +69,35 @@ structure Sorts: SORTS = struct + +(** ordered lists of sorts **) + +val make = Ord_List.make Term_Ord.sort_ord; +val subset = Ord_List.subset Term_Ord.sort_ord; +val union = Ord_List.union Term_Ord.sort_ord; +val subtract = Ord_List.subtract Term_Ord.sort_ord; + +val remove_sort = Ord_List.remove Term_Ord.sort_ord; +val insert_sort = Ord_List.insert Term_Ord.sort_ord; + +fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss + | insert_typ (TVar (_, S)) Ss = insert_sort S Ss + | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss +and insert_typs [] Ss = Ss + | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss); + +fun insert_term (Const (_, T)) Ss = insert_typ T Ss + | insert_term (Free (_, T)) Ss = insert_typ T Ss + | insert_term (Var (_, T)) Ss = insert_typ T Ss + | insert_term (Bound _) Ss = Ss + | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss) + | insert_term (t $ u) Ss = insert_term t (insert_term u Ss); + +fun insert_terms [] Ss = Ss + | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); + + + (** order-sorted algebra **) (* diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/term_ord.ML Tue Apr 18 12:23:37 2023 +0200 @@ -224,38 +224,6 @@ structure Termset = Set(Termtab.Key); -structure Sortset: -sig - include SET - val insert_typ: typ -> T -> T - val insert_typs: typ list -> T -> T - val insert_term: term -> T -> T - val insert_terms: term list -> T -> T -end = -struct - -structure Set = Set(Sorttab.Key); -open Set; - -fun insert_typ (TFree (_, S)) Ss = insert S Ss - | insert_typ (TVar (_, S)) Ss = insert S Ss - | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss -and insert_typs [] Ss = Ss - | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss); - -fun insert_term (Const (_, T)) Ss = insert_typ T Ss - | insert_term (Free (_, T)) Ss = insert_typ T Ss - | insert_term (Var (_, T)) Ss = insert_typ T Ss - | insert_term (Bound _) Ss = Ss - | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss) - | insert_term (t $ u) Ss = insert_term t (insert_term u Ss); - -fun insert_terms [] Ss = Ss - | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); - -end; - structure Var_Graph = Graph(Vartab.Key); -structure Sort_Graph = Graph(Sorttab.Key); structure Typ_Graph = Graph(Typtab.Key); structure Term_Graph = Graph(Termtab.Key); diff -r 6ea0030b9ee9 -r 1156aa9db7f5 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Apr 18 12:10:00 2023 +0200 +++ b/src/Pure/thm.ML Tue Apr 18 12:23:37 2023 +0200 @@ -69,7 +69,7 @@ val theory_name: thm -> string val maxidx_of: thm -> int val maxidx_thm: thm -> int -> int - val shyps_of: thm -> Sortset.T + val shyps_of: thm -> sort Ord_List.T val hyps_of: thm -> term list val prop_of: thm -> term val tpairs_of: thm -> (term * term) list @@ -98,7 +98,7 @@ val join_transfer_context: Proof.context * thm -> Proof.context * thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm - val weaken_sorts: Sortset.T -> cterm -> cterm + val weaken_sorts: sort list -> cterm -> cterm val proof_bodies_of: thm list -> proof_body list val proof_body_of: thm -> proof_body val proof_of: thm -> proof @@ -108,7 +108,7 @@ val expose_proof: theory -> thm -> unit val future: thm future -> cterm -> thm val thm_deps: thm -> Proofterm.thm Ord_List.T - val extra_shyps: thm -> Sortset.T + val extra_shyps: thm -> sort list val strip_shyps: thm -> thm val derivation_closed: thm -> bool val derivation_name: thm -> string @@ -189,7 +189,7 @@ (** certified types **) -datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: Sortset.T}; +datatype ctyp = Ctyp of {cert: Context.certificate, T: typ, maxidx: int, sorts: sort Ord_List.T}; fun typ_of (Ctyp {T, ...}) = T; @@ -197,7 +197,7 @@ let val T = Sign.certify_typ thy raw_T; val maxidx = Term.maxidx_of_typ T; - val sorts = Sortset.build (Sortset.insert_typ T); + val sorts = Sorts.insert_typ T []; in Ctyp {cert = Context.Certificate thy, T = T, maxidx = maxidx, sorts = sorts} end; val ctyp_of = global_ctyp_of o Proof_Context.theory_of; @@ -219,7 +219,7 @@ val dest_ctyp1 = dest_ctypN 1; fun join_certificate_ctyp (Ctyp {cert, ...}) cert0 = Context.join_certificate (cert0, cert); -fun insert_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sortset.merge (sorts0, sorts); +fun union_sorts_ctyp (Ctyp {sorts, ...}) sorts0 = Sorts.union sorts0 sorts; fun maxidx_ctyp (Ctyp {maxidx, ...}) maxidx0 = Int.max (maxidx0, maxidx); fun make_ctyp (Ctyp {cert, T, maxidx = _, sorts = _}) cargs = @@ -232,7 +232,7 @@ Ctyp { cert = fold join_certificate_ctyp cargs cert, maxidx = fold maxidx_ctyp cargs ~1, - sorts = Sortset.build (fold insert_sorts_ctyp cargs), + sorts = fold union_sorts_ctyp cargs [], T = if length args = length cargs then Type (a, As) else err ()} | _ => err ()) end; @@ -243,7 +243,7 @@ (*certified terms with checked typ, maxidx, and sorts*) datatype cterm = - Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: Sortset.T}; + Cterm of {cert: Context.certificate, t: term, T: typ, maxidx: int, sorts: sort Ord_List.T}; exception CTERM of string * cterm list; @@ -259,7 +259,7 @@ fun global_cterm_of thy tm = let val (t, T, maxidx) = Sign.certify_term thy tm; - val sorts = Sortset.build (Sortset.insert_term t); + val sorts = Sorts.insert_term t []; in Cterm {cert = Context.Certificate thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end; val cterm_of = global_cterm_of o Proof_Context.theory_of; @@ -345,7 +345,7 @@ t = f $ x, T = rty, maxidx = Int.max (maxidx1, maxidx2), - sorts = Sortset.merge (sorts1, sorts2)} + sorts = Sorts.union sorts1 sorts2} else raise CTERM ("apply: types don't agree", [cf, cx]) | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]); @@ -356,7 +356,7 @@ Cterm {cert = join_certificate0 (ct1, ct2), t = t, T = T1 --> T2, maxidx = Int.max (maxidx1, maxidx2), - sorts = Sortset.merge (sorts1, sorts2)} + sorts = Sorts.union sorts1 sorts2} end; fun lambda t u = lambda_name ("", t) u; @@ -430,7 +430,7 @@ tags: Properties.T, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) constraints: constraint Ord_List.T, (*implicit proof obligations for sort constraints*) - shyps: Sortset.T, (*sort hypotheses*) + shyps: sort Ord_List.T, (*sort hypotheses*) hyps: term Ord_List.T, (*hypotheses*) tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) @@ -544,7 +544,7 @@ (Term_Ord.fast_term_ord o apply2 prop_of ||| list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 tpairs_of ||| list_ord Term_Ord.fast_term_ord o apply2 hyps_of - ||| Sortset.ord o apply2 shyps_of); + ||| list_ord Term_Ord.sort_ord o apply2 shyps_of); (* implicit theory context *) @@ -658,7 +658,7 @@ val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct1, ct2], [], NONE); val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty); - val sorts = Sortset.merge (sorts1, sorts2); + val sorts = Sorts.union sorts1 sorts2; fun mk_cTinst ((a, i), (S, T)) = (((a, i), S), Ctyp {T = T, cert = cert, maxidx = maxidx2, sorts = sorts}); fun mk_ctinst ((x, i), (U, t)) = @@ -719,17 +719,18 @@ tags = tags, maxidx = maxidx, constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union sorts shyps, hyps = insert_hyps A hyps, tpairs = tpairs, prop = prop}) end; -fun weaken_sorts more_sorts ct = +fun weaken_sorts raw_sorts ct = let val Cterm {cert, t, T, maxidx, sorts} = ct; val thy = theory_of_cterm ct; - val sorts' = Sortset.fold (Sortset.insert o Sign.certify_sort thy) more_sorts sorts; + val more_sorts = Sorts.make (map (Sign.certify_sort thy) raw_sorts); + val sorts' = Sorts.union sorts more_sorts; in Cterm {cert = cert, t = t, T = T, maxidx = maxidx, sorts = sorts'} end; @@ -816,7 +817,7 @@ val _ = null constraints orelse err "bad sort constraints"; val _ = null tpairs orelse err "bad flex-flex constraints"; val _ = null hyps orelse err "bad hyps"; - val _ = Sortset.subset (shyps, orig_shyps) orelse err "bad shyps"; + val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps"; val _ = forall_promises (fn j => i <> j) promises orelse err "bad dependencies"; val _ = join_promises (dest_promises promises); in thm end; @@ -854,7 +855,7 @@ val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); val cert = Context.Certificate thy; val maxidx = maxidx_of_term prop; - val shyps = Sortset.build (Sortset.insert_term prop); + val shyps = Sorts.insert_term prop []; in Thm (der, {cert = cert, tags = [], maxidx = maxidx, @@ -1019,13 +1020,13 @@ (*Dangling sort constraints of a thm*) fun extra_shyps (th as Thm (_, {shyps, ...})) = - Sortset.subtract (Sortset.build (fold_terms {hyps = true} Sortset.insert_term th)) shyps; + Sorts.subtract (fold_terms {hyps = true} Sorts.insert_term th []) shyps; (*Remove extra sorts that are witnessed by type signature information*) -fun strip_shyps (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = - solve_constraints ( - if Sortset.is_empty shyps then thm - else +fun strip_shyps thm = + (case thm of + Thm (_, {shyps = [], ...}) => thm + | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) => let val thy = theory_of_thm thm; @@ -1037,29 +1038,30 @@ val present = (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; - val extra = fold (Sortset.remove o #2) present shyps; - val witnessed = Sign.witness_sorts thy present (Sortset.dest extra); - val non_witnessed = - fold (Sortset.remove o #2) witnessed extra |> Sortset.dest |> map (`minimize); + val extra = fold (Sorts.remove_sort o #2) present shyps; + val witnessed = Sign.witness_sorts thy present extra; + val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); val extra' = non_witnessed |> map_filter (fn (S, _) => if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S) - |> Sortset.make; + |> Sorts.make; val constrs' = non_witnessed |> maps (fn (S1, S2) => - let val S0 = the (Sortset.get_first (fn S => if le (S, S1) then SOME S else NONE) extra') + let val S0 = the (find_first (fn S => le (S, S1)) extra') in rel (S0, S1) @ rel (S1, S2) end); val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints; - val shyps' = fold (Sortset.insert o #2) present extra'; + val shyps' = fold (Sorts.insert_sort o #2) present extra'; in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) - end); + end) + |> solve_constraints; + (*** Closed theorems with official name ***) @@ -1209,7 +1211,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union sorts shyps, hyps = remove_hyps A hyps, tpairs = tpairs, prop = Logic.mk_implies (A, prop)}); @@ -1236,7 +1238,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraintsA constraints, - shyps = Sortset.merge (shypsA, shyps), + shyps = Sorts.union shypsA shyps, hyps = union_hyps hypsA hyps, tpairs = union_tpairs tpairsA tpairs, prop = B}) @@ -1268,7 +1270,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))}); @@ -1297,7 +1299,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Term.betapply (A, t)}) @@ -1361,7 +1363,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, - shyps = Sortset.merge (shyps1, shyps2), + shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = eq $ t1 $ t2}) @@ -1433,7 +1435,7 @@ tags = [], maxidx = maxidx, constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union sorts shyps, hyps = hyps, tpairs = tpairs, prop = Logic.mk_equals @@ -1473,7 +1475,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, - shyps = Sortset.merge (shyps1, shyps2), + shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (f $ t, g $ u)})) @@ -1501,7 +1503,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, - shyps = Sortset.merge (shyps1, shyps2), + shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = Logic.mk_equals (A, B)}) @@ -1530,7 +1532,7 @@ tags = [], maxidx = Int.max (maxidx1, maxidx2), constraints = union_constraints constraints1 constraints2, - shyps = Sortset.merge (shyps1, shyps2), + shyps = Sorts.union shyps1 shyps2, hyps = union_hyps hyps1 hyps2, tpairs = union_tpairs tpairs1 tpairs2, prop = B}) @@ -1644,7 +1646,7 @@ val add_instT_cert = add_cert (fn Ctyp {cert, ...} => cert); val add_inst_cert = add_cert (fn Cterm {cert, ...} => cert); -fun add_sorts sorts_of (_, c) sorts = Sortset.merge (sorts_of c, sorts); +fun add_sorts sorts_of (_, c) sorts = Sorts.union (sorts_of c) sorts; val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts); val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts); @@ -1811,7 +1813,7 @@ tags = [], maxidx = maxidx_of_term prop', constraints = [], - shyps = Sortset.make [[]], (*potentially redundant*) + shyps = [[]], (*potentially redundant*) hyps = [], tpairs = [], prop = prop'}) @@ -1863,7 +1865,7 @@ in if not (null (hyps_of thm)) then err "theorem may not contain hypotheses" - else if not (Sortset.is_empty (extra_shyps thm)) then + else if not (null (extra_shyps thm)) then err "theorem may not contain sort hypotheses" else if not (null (tpairs_of thm)) then err "theorem may not contain flex-flex pairs" @@ -1899,7 +1901,7 @@ tags = [], maxidx = maxidx + inc, constraints = constraints, - shyps = Sortset.merge (sorts, shyps), + shyps = Sorts.union shyps sorts, (*sic!*) hyps = hyps, tpairs = map (apply2 lift_abs) tpairs, prop = Logic.list_implies (map lift_all As, lift_all B)}) @@ -2191,7 +2193,7 @@ {tags = [], maxidx = Envir.maxidx_of env, constraints = constraints', - shyps = Envir.insert_sorts env (Sortset.merge (shyps1, shyps2)), + shyps = Envir.insert_sorts env (Sorts.union shyps1 shyps2), hyps = union_hyps hyps1 hyps2, tpairs = ntpairs, prop = Logic.list_implies normp,