# HG changeset patch # User wenzelm # Date 1564418679 -7200 # Node ID 52435af442a66890ff9f0ba818376e7d032987d9 # Parent 4abd07cd034f41750c269ce3b3c66bd306cd6284# Parent 03cfef16ddb4551080f8d546fa65a7a92cbb177d merged diff -r 4abd07cd034f -r 52435af442a6 src/HOL/Types_To_Sets/internalize_sort.ML --- a/src/HOL/Types_To_Sets/internalize_sort.ML Mon Jul 29 16:26:06 2019 +0200 +++ b/src/HOL/Types_To_Sets/internalize_sort.ML Mon Jul 29 18:44:39 2019 +0200 @@ -31,14 +31,14 @@ val thy = Thm.theory_of_thm thm; val tvar = Thm.typ_of ctvar; - val ((_, assms, 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 diff -r 4abd07cd034f -r 52435af442a6 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Jul 29 16:26:06 2019 +0200 +++ b/src/Pure/Proof/extraction.ML Mon Jul 29 18:44:39 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') = + 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; diff -r 4abd07cd034f -r 52435af442a6 src/Pure/Proof/reconstruct.ML diff -r 4abd07cd034f -r 52435af442a6 src/Pure/logic.ML --- a/src/Pure/logic.ML Mon Jul 29 16:26:06 2019 +0200 +++ b/src/Pure/logic.ML Mon Jul 29 18:44:39 2019 +0200 @@ -56,8 +56,14 @@ 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 -> - ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term + type unconstrain_context = + {present_map: (typ * typ) list, + constraints_map: (sort * typ) list, + atyp_map: typ -> typ, + map_atyps: typ -> typ, + constraints: ((typ * class) * term) list, + outer_constraints: (typ * class) list}; + val unconstrainT: sort list -> term -> unconstrain_context * term val protectC: term val protect: term -> term val unprotect: term -> term @@ -339,6 +345,14 @@ (* internalized sort constraints *) +type unconstrain_context = + {present_map: (typ * typ) list, + constraints_map: (sort * typ) list, + atyp_map: typ -> typ, + map_atyps: 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 []); @@ -362,19 +376,25 @@ | NONE => raise TYPE ("Dangling type variable", [T], []))); 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 - |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map) - |> curry list_implies (map snd constraints); - in ((atyp_map, constraints, outer_constraints), prop') end; + val map_atyps = Term.map_atyps (Type.strip_sorts o atyp_map); + val ucontext = + {present_map = present_map, + constraints_map = constraints_map, + atyp_map = atyp_map, + map_atyps = map_atyps, + constraints = constraints, + outer_constraints = outer_constraints}; + val prop' = prop + |> Term.map_types map_atyps + |> curry list_implies (map #2 constraints); + in (ucontext, prop') end; diff -r 4abd07cd034f -r 52435af442a6 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Jul 29 16:26:06 2019 +0200 +++ b/src/Pure/proofterm.ML Mon Jul 29 18:44:39 2019 +0200 @@ -54,8 +54,9 @@ val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T val all_oracles_of: proof_body -> oracle Ord_List.T val approximate_proof_body: proof -> proof_body - val no_proof_body: proof_body + val no_proof_body: proof -> proof_body val no_thm_proofs: proof -> proof + val no_body_proofs: proof -> proof val encode: proof XML.Encode.T val encode_body: proof_body XML.Encode.T @@ -310,8 +311,8 @@ proof = prf} end; -val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof}; -val no_body = Future.value no_proof_body; +fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof}; +val no_body = Future.value (no_proof_body MinProof); fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body)) | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) @@ -320,6 +321,14 @@ | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 | no_thm_proofs a = a; +fun no_body_proofs (PThm (i, (a, body))) = + PThm (i, (a, Future.value (no_proof_body (join_proof body)))) + | no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf) + | no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) + | no_body_proofs (prf % t) = no_body_proofs prf % t + | no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 + | no_body_proofs a = a; + (** XML data representation **) @@ -1670,38 +1679,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,11 +1718,7 @@ val prop = Logic.list_implies (hyps, concl); val args = prop_args prop; - val ((atyp_map, constraints, outer_constraints), 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; + val (ucontext, prop1) = Logic.unconstrainT shyps prop; val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; val body0 = @@ -1737,7 +1732,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') = @@ -1753,9 +1748,11 @@ val head = PThm (i, ((name, prop1, NONE, open_proof), body')); val proof = - if unconstrain - then proof_combt' (head, args1) - else proof_combP (proof_combt' (head, args), argsP); + if unconstrain then + proof_combt' (head, (map o Option.map o Term.map_types) (#map_atyps ucontext) args) + else + proof_combP (proof_combt' (head, args), + map OfClass (#outer_constraints ucontext) @ map Hyp hyps); in (pthm, proof) end; in