--- a/src/HOL/Types_To_Sets/internalize_sort.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/HOL/Types_To_Sets/internalize_sort.ML Mon Jul 29 11:09:37 2019 +0200
@@ -31,15 +31,14 @@
val thy = Thm.theory_of_thm thm;
val tvar = Thm.typ_of ctvar;
- val {constraints = assms, outer_constraints = classes, ...} =
- Logic.unconstrainT [] (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)) =
TVar (name, Sign.minimize_sort thy (filter_out (is_proper_class thy) (Sign.complete_sort thy sort)))
| reduce_to_non_proper_sort _ = error "not supported";
- val data = (map fst classes) ~~ assms;
+ val data = map #1 (#outer_constraints ucontext) ~~ #constraints ucontext;
val new_tvar = get_first (fn (tvar', ((ren_tvar, _), _)) => if tvar = tvar'
then SOME (reduce_to_non_proper_sort ren_tvar) else NONE) data
--- a/src/Pure/Proof/extraction.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Jul 29 11:09:37 2019 +0200
@@ -365,7 +365,7 @@
fun abs_corr_shyps thy thm vs xs prf =
let
val S = Sign.defaultS thy;
- val {atyp_map, constraints, prop = prop', ...} =
+ val (ucontext, prop') =
Logic.unconstrainT (Thm.shyps_of thm) (Thm.prop_of thm);
val atyps = fold_types (fold_atyps (insert (op =))) (Thm.prop_of thm) [];
val Ts = map_filter (fn ((v, i), _) => if member (op =) vs v then
@@ -374,13 +374,13 @@
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
fun typ_map T = Type.strip_sorts
- (map_atyps (fn U => if member (op =) atyps U then atyp_map U else U) T);
+ (map_atyps (fn U => if member (op =) atyps U then (#atyp_map ucontext) U else U) T);
fun mk_hyp (T, c) = Hyp (Logic.mk_of_class (typ_map T, c));
val xs' = map (map_types typ_map) xs
in
prf |>
Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
- fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
+ fold_rev Proofterm.implies_intr_proof' (map snd (#constraints ucontext)) |>
fold_rev Proofterm.forall_intr_proof' xs' |>
fold_rev Proofterm.implies_intr_proof' constraints'
end;
--- a/src/Pure/Proof/reconstruct.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML Mon Jul 29 11:09:37 2019 +0200
@@ -379,7 +379,7 @@
fun clean_proof_of ctxt full thm =
let
- val {prop, ...} =
+ val (_, prop) =
Logic.unconstrainT (Thm.shyps_of thm)
(Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
in
--- a/src/Pure/logic.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/logic.ML Mon Jul 29 11:09:37 2019 +0200
@@ -56,11 +56,13 @@
val mk_arities: arity -> term list
val mk_arity: string * sort list * class -> term
val dest_arity: term -> string * sort list * class
- val unconstrainT: sort list -> term ->
- {atyp_map: typ -> typ,
+ type unconstrain_context =
+ {present_map: (typ * typ) list,
+ extra_map: (sort * typ) list,
+ atyp_map: typ -> typ,
constraints: ((typ * class) * term) list,
- outer_constraints: (typ * class) list,
- prop: term}
+ outer_constraints: (typ * class) list};
+ val unconstrainT: sort list -> term -> unconstrain_context * term
val protectC: term
val protect: term -> term
val unprotect: term -> term
@@ -342,6 +344,13 @@
(* internalized sort constraints *)
+type unconstrain_context =
+ {present_map: (typ * typ) list,
+ extra_map: (sort * typ) list,
+ atyp_map: typ -> typ,
+ constraints: ((typ * class) * term) list,
+ outer_constraints: (typ * class) list};
+
fun unconstrainT shyps prop =
let
val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []);
@@ -352,37 +361,37 @@
val present_map =
map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1;
- val constraints_map =
- map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @
+ val extra_map =
map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2;
fun atyp_map T =
(case AList.lookup (op =) present_map T of
SOME U => U
| NONE =>
- (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
+ (case AList.lookup (op =) extra_map (Type.sort_of_atyp T) of
SOME U => U
| NONE => raise TYPE ("Dangling type variable", [T], [])));
+ val constraints_map =
+ map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ extra_map;
val constraints =
- maps (fn (_, T as TVar (ai, S)) =>
- map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S)
- constraints_map;
+ constraints_map |> maps (fn (_, T as TVar (ai, S)) =>
+ map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S);
val outer_constraints =
maps (fn (T, S) => map (pair T) S)
(present @ map (fn S => (TFree ("'dummy", S), S)) extra);
- val prop' =
- prop
+ val context =
+ {present_map = present_map,
+ extra_map = extra_map,
+ atyp_map = atyp_map,
+ constraints = constraints,
+ outer_constraints = outer_constraints};
+ val prop' = prop
|> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map)
|> curry list_implies (map snd constraints);
- in
- {atyp_map = atyp_map,
- constraints = constraints,
- outer_constraints = outer_constraints,
- prop = prop'}
- end;
+ in (context, prop') end;
--- a/src/Pure/proofterm.ML Mon Jul 29 10:26:12 2019 +0200
+++ b/src/Pure/proofterm.ML Mon Jul 29 11:09:37 2019 +0200
@@ -1670,38 +1670,28 @@
-(** abstraction over sort constraints **)
-
-fun unconstrainT_prf thy (atyp_map, constraints) =
- let
- fun hyp_map hyp =
- (case AList.lookup (op =) constraints hyp of
- SOME t => Hyp t
- | NONE => raise Fail "unconstrainT_prf: missing constraint");
-
- val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o atyp_map);
- fun ofclass (ty, c) =
- let val ty' = Term.map_atyps atyp_map ty;
- in the_single (of_sort_proof thy hyp_map (ty', [c])) end;
- in
- Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
- #> fold_rev (implies_intr_proof o snd) constraints
- end;
-
-fun unconstrainT_body thy constrs (PBody {oracles, thms, proof}) =
- PBody
- {oracles = oracles, (* FIXME merge (!), unconstrain (!?!) *)
- thms = thms, (* FIXME merge (!) *)
- proof = unconstrainT_prf thy constrs proof};
-
-
-
(** theorems **)
val proof_serial = Counter.make ();
local
+fun unconstrainT_prf thy (ucontext: Logic.unconstrain_context) =
+ let
+ fun hyp_map hyp =
+ (case AList.lookup (op =) (#constraints ucontext) hyp of
+ SOME t => Hyp t
+ | NONE => raise Fail "unconstrainT_prf: missing constraint");
+
+ val typ = Term_Subst.map_atypsT_same (Type.strip_sorts o #atyp_map ucontext);
+ fun ofclass (ty, c) =
+ let val ty' = Term.map_atyps (#atyp_map ucontext) ty;
+ in the_single (of_sort_proof thy hyp_map (ty', [c])) end;
+ in
+ Same.commit (map_proof_same (Term_Subst.map_types_same typ) typ ofclass)
+ #> fold_rev (implies_intr_proof o snd) (#constraints ucontext)
+ end;
+
fun export thy i proof =
if Options.default_bool "export_proofs" then
Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i]))
@@ -1719,12 +1709,11 @@
val prop = Logic.list_implies (hyps, concl);
val args = prop_args prop;
- val {atyp_map, constraints, outer_constraints, prop = prop1, ...} =
- Logic.unconstrainT shyps prop;
+ val (ucontext, prop1) = Logic.unconstrainT shyps prop;
val args1 =
(map o Option.map o Term.map_types o Term.map_atyps)
- (Type.strip_sorts o atyp_map) args;
- val argsP = map OfClass outer_constraints @ map Hyp hyps;
+ (Type.strip_sorts o #atyp_map ucontext) args;
+ val argsP = map OfClass (#outer_constraints ucontext) @ map Hyp hyps;
val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
val body0 =
@@ -1738,7 +1727,7 @@
fun new_prf () =
let
val i = proof_serial ();
- val postproc = unconstrainT_body thy (atyp_map, constraints) #> named ? publish i;
+ val postproc = map_proof_of (unconstrainT_prf thy ucontext) #> named ? publish i;
in (i, fulfill_proof_future thy promises postproc body0) end;
val (i, body') =
@@ -1772,7 +1761,7 @@
(* approximative PThm name *)
fun get_name shyps hyps prop prf =
- let val {prop, ...} = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
+ let val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)) in
(case strip_combt (fst (strip_combP prf)) of
(PThm (_, ((name, prop', _, _), _)), _) => if prop = prop' then name else ""
| _ => "")