clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;
authorwenzelm
Sun, 21 Jul 2024 23:31:32 +0200
changeset 80608 0b8922e351a3
parent 80607 e23aab2df03c
child 80610 628d2e5015e3
clarified export: replaced Proofterm.standard_vars by ZTerm.standard_vars;
src/Pure/Build/export_theory.ML
src/Pure/proofterm.ML
src/Pure/zterm.ML
--- a/src/Pure/Build/export_theory.ML	Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/Build/export_theory.ML	Sun Jul 21 23:31:32 2024 +0200
@@ -65,17 +65,6 @@
       in ([], triple int string int (ass, delim, pri)) end];
 
 
-(* free variables: not declared in the context *)
-
-val is_free = not oo Name.is_declared;
-
-fun add_frees used =
-  fold_aterms (fn Free (x, T) => is_free used x ? insert (op =) (x, T) | _ => I);
-
-fun add_tfrees used =
-  (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
-
-
 (* locales *)
 
 fun locale_content thy loc =
@@ -149,6 +138,22 @@
     val enabled = export_enabled context;
 
 
+    (* recode *)
+
+    val thy_cache = perhaps ZTerm.init_cache thy;
+
+    val ztyp_of = ZTerm.ztyp_cache thy_cache;
+    val zterm_of = ZTerm.zterm_of thy_cache;
+    val zproof_of = Proofterm.proof_to_zproof thy_cache;
+
+    val encode_ztyp = ZTerm.encode_ztyp;
+    val encode_zterm = ZTerm.encode_zterm {typed_vars = true};
+    val encode_term = encode_zterm o zterm_of;
+
+    val encode_standard_zterm = ZTerm.encode_zterm {typed_vars = false};
+    val encode_standard_zproof = ZTerm.encode_zproof {typed_vars = false};
+
+
     (* strict parents *)
 
     val parents = Theory.parents_of thy;
@@ -228,11 +233,9 @@
 
     (* consts *)
 
-    val encode_term = Term_XML.Encode.term consts;
-
     val encode_const =
       let open XML.Encode Term_XML.Encode
-      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_term) bool))) end;
+      in pair encode_syntax (pair (list string) (pair typ (pair (option encode_zterm) bool))) end;
 
     val _ =
       export_entities "consts" Sign.const_space (#constants (Consts.dest consts))
@@ -242,7 +245,8 @@
               val syntax = get_syntax_const thy_ctxt c;
               val U = Logic.unvarifyT_global T;
               val U0 = Term.strip_sortsT U;
-              val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts;
+              fun trim_abbrev t =
+                ZTerm.standard_vars Name.context (zterm_of t, NONE) |> #prop |> ZTerm.strip_sorts;
               val abbrev' = Option.map trim_abbrev abbrev;
               val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
               val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
@@ -253,19 +257,21 @@
 
     fun standard_prop used extra_shyps raw_prop raw_proof =
       let
-        val (prop, proof) = Proofterm.standard_vars used (raw_prop, raw_proof);
-        val args = rev (add_frees used prop []);
-        val typargs = rev (add_tfrees used prop []);
-        val used_typargs = fold (Name.declare o #1) typargs used;
+        val {typargs, args, prop, proof} =
+          ZTerm.standard_vars used (zterm_of raw_prop, Option.map zproof_of raw_proof);
+        val is_free = not o Name.is_declared used;
+        val args' = args |> filter (is_free o #1);
+        val typargs' = typargs |> filter (is_free o #1);
+        val used_typargs = fold (Name.declare o #1) typargs' used;
         val sorts = Name.invent used_typargs Name.aT (length extra_shyps) ~~ extra_shyps;
-      in ((sorts @ typargs, args, prop), proof) end;
+      in ((sorts @ typargs', args', prop), proof) end;
 
     fun standard_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
-      in triple (list (pair string sort)) (list (pair string typ)) encode_term end;
+      in triple (list (pair string sort)) (list (pair string encode_ztyp)) encode_zterm end;
 
     fun encode_axiom used prop =
       encode_prop (#1 (standard_prop used [] prop NONE));
@@ -308,10 +314,8 @@
         val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
-          let
-            open XML.Encode Term_XML.Encode;
-            val encode_proof = Proofterm.encode_standard_proof thy;
-          in triple encode_prop (list Thm_Name.encode) encode_proof end
+          let open XML.Encode Term_XML.Encode
+          in triple encode_prop (list Thm_Name.encode) encode_standard_zproof end
       end;
 
     fun export_thm (thm_id, (thm_name, _)) =
--- a/src/Pure/proofterm.ML	Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 21 23:31:32 2024 +0200
@@ -174,11 +174,6 @@
   val expand_name_empty: thm_header -> Thm_Name.P option
   val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
 
-  val standard_vars: Name.context -> term * proof option -> term * proof option
-  val standard_vars_term: Name.context -> term -> term
-  val add_standard_vars: proof -> (string * typ) list -> (string * typ) list
-  val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
-
   val export_enabled: unit -> bool
   val export_standard_enabled: unit -> bool
   val export_proof_boxes_required: theory -> bool
@@ -2034,107 +2029,6 @@
 
 (** theorems **)
 
-(* standardization of variables for export: only frees and named bounds *)
-
-local
-
-val declare_frees_term = Term.declare_term_frees;
-val declare_frees_term' = fn SOME t => declare_frees_term t | NONE => I;
-val declare_frees_proof = fold_proof_terms declare_frees_term;
-
-fun variant_term bs (Abs (x, T, t)) =
-      let
-        val x' = #1 (Name.variant x (declare_frees_term t bs));
-        val t' = variant_term (Name.declare x' bs) t;
-      in Abs (x', T, t') end
-  | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
-  | variant_term _ t = t;
-
-fun variant_proof bs (Abst (x, T, prf)) =
-      let
-        val x' = #1 (Name.variant x (declare_frees_proof prf bs));
-        val prf' = variant_proof (Name.declare x' bs) prf;
-      in Abst (x', T, prf') end
-  | variant_proof bs (AbsP (x, t, prf)) =
-      let
-        val x' = #1 (Name.variant x (declare_frees_term' t (declare_frees_proof prf bs)));
-        val t' = Option.map (variant_term bs) t;
-        val prf' = variant_proof (Name.declare x' bs) prf;
-      in AbsP (x', t', prf') end
-  | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
-  | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
-  | variant_proof bs (Hyp t) = Hyp (variant_term bs t)
-  | variant_proof _ prf = prf;
-
-val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
-val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
-
-val unvarify_type = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
-val unvarify_term = map_types unvarify_type o Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t);
-val unvarify_proof = map_proof_terms unvarify_term unvarify_type;
-
-fun hidden_types prop proof =
-  let
-    val visible = (fold_types o fold_atyps) (insert (op =)) prop [];
-    val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
-  in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end;
-
-fun standard_hidden_types prop proof =
-  let
-    val hidden = hidden_types prop proof;
-    val idx = Term.maxidx_term prop (maxidx_proof proof ~1) + 1;
-    fun smash T =
-      if member (op =) hidden T then
-        (case Type.sort_of_atyp T of
-          [] => dummyT
-        | S => TVar (("'", idx), S))
-      else T;
-    val smashT = map_atyps smash;
-  in map_proof_terms (map_types smashT) smashT proof end;
-
-fun standard_hidden_terms prop proof =
-  let
-    fun add_unless excluded x =
-      ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x;
-    val visible = fold_aterms (add_unless []) prop [];
-    val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof [];
-    val dummy_term = Term.map_aterms (fn x =>
-      if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x);
-  in proof |> not (null hidden) ? map_proof_terms dummy_term I end;
-
-in
-
-fun standard_vars used (term, opt_proof) =
-  let
-    val proofs = opt_proof
-      |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list;
-    val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []);
-    val used' = used
-      |> used_frees_term term
-      |> fold used_frees_proof proofs;
-    val inst = Term_Subst.zero_var_indexes_inst used' (term :: proof_terms);
-    val term' = term |> Term_Subst.instantiate inst |> unvarify_term |> variant_term Name.context;
-    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof Name.context);
-  in (term', try hd proofs') end;
-
-fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
-
-val add_standard_vars_term = fold_aterms
-  (fn Free (x, T) =>
-    (fn env =>
-      (case AList.lookup (op =) env x of
-        NONE => (x, T) :: env
-      | SOME T' =>
-          if T = T' then env
-          else raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x, [T, T'], [])))
-    | _ => I);
-
-val add_standard_vars = fold_proof_terms add_standard_vars_term;
-
-end;
-
-
 (* PThm nodes *)
 
 fun prune_body body =
@@ -2165,19 +2059,19 @@
 
 local
 
-fun export_proof thy i prop prf =
+fun export_proof thy i prop0 proof0 =
   let
-    val (prop', SOME prf') = standard_vars Name.context (prop, SOME (no_thm_names prf));
-    val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
-    val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
-
-    val xml = (typargs, (args, (prop', prf'))) |>
+    val {typargs, args, prop, proof} =
+      ZTerm.standard_vars Name.context
+        (ZTerm.zterm_of thy prop0, SOME (proof_to_zproof thy (no_thm_names proof0)));
+    val xml = (typargs, (args, (prop, the proof))) |>
       let
         open XML.Encode Term_XML.Encode;
-        val encode_vars = list (pair string typ);
-        val encode_term = encode_standard_term thy;
-        val encode_proof = encode_standard_proof thy;
-      in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
+        val encode_tfrees = list (pair string sort);
+        val encode_frees = list (pair string ZTerm.encode_ztyp);
+        val encode_term = ZTerm.encode_zterm {typed_vars = false};
+        val encode_proof = ZTerm.encode_zproof {typed_vars = false};
+      in pair encode_tfrees (pair encode_frees (pair encode_term encode_proof)) end;
   in
     Export.export_params (Context.Theory thy)
      {theory_name = Context.theory_long_name thy,
--- a/src/Pure/zterm.ML	Sun Jul 21 22:34:25 2024 +0200
+++ b/src/Pure/zterm.ML	Sun Jul 21 23:31:32 2024 +0200
@@ -312,12 +312,16 @@
   val ztyp_dummy: ztyp
   val typ_of_tvar: indexname * sort -> typ
   val typ_of: ztyp -> typ
+  val init_cache: theory -> theory option
+  val exit_cache: theory -> theory option
   val reset_cache: theory -> theory
   val check_cache: theory -> {ztyp: int, typ: int} option
   val ztyp_cache: theory -> typ -> ztyp
   val typ_cache: theory -> ztyp -> typ
   val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
   val zterm_of: theory -> term -> zterm
+  val zterm_dummy_pattern: ztyp -> zterm
+  val zterm_type: ztyp -> zterm
   val term_of: theory -> zterm -> term
   val beta_norm_term_same: zterm Same.operation
   val beta_norm_proof_same: zproof Same.operation
@@ -376,6 +380,8 @@
   val encode_ztyp: ztyp XML.Encode.T
   val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
   val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
+  val standard_vars: Name.context -> zterm * zproof option ->
+    {typargs: (string * sort) list, args: (string * ztyp) list, prop: zterm, proof: zproof option}
 end;
 
 structure ZTerm: ZTERM =
@@ -697,6 +703,8 @@
 fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
 fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
 
+in
+
 fun init_cache thy =
   if is_some (Data.get thy) then NONE
   else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
@@ -706,8 +714,6 @@
     SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
   | NONE => NONE);
 
-in
-
 val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
 
 fun reset_cache thy =
@@ -757,6 +763,9 @@
 
 val zterm_of = #zterm o zterm_cache;
 
+fun zterm_dummy_pattern T = ZConst1 ("Pure.dummy_pattern", T);
+fun zterm_type T = ZConst1 ("Pure.type", T);
+
 fun term_of thy =
   let
     val instance = Consts.instance (Sign.consts_of thy);
@@ -1502,4 +1511,143 @@
 
 end;
 
+
+(* standardization of variables for export: only frees and named bounds *)
+
+local
+
+fun declare_frees_term t = fold_vars (fn ((x, ~1), _) => Name.declare x | _ => I) t;
+val declare_frees_proof = fold_proof {hyps = true} (K I) declare_frees_term;
+
+val (variant_abs_term, variant_abs_proof) =
+  let
+    fun term bs (ZAbs (x, T, t)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_term t bs));
+            val bs' = Name.declare x' bs;
+          in ZAbs (x', T, Same.commit_if (x <> x') (term bs') t) end
+      | term bs (ZApp (t, u)) =
+          (ZApp (term bs t, Same.commit (term bs) u)
+            handle Same.SAME => ZApp (t, term bs u))
+      | term _ _ = raise Same.SAME;
+
+    fun proof bs (ZAbst (x, T, p)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_proof p bs));
+            val bs' = Name.declare x' bs;
+          in ZAbst (x', T, Same.commit_if (x <> x') (proof bs') p) end
+      | proof bs (ZAbsp (x, t, p)) =
+          let
+            val x' = #1 (Name.variant x (declare_frees_term t (declare_frees_proof p bs)));
+            val (t', term_eq) = Same.commit_id (term bs) t;
+            val bs' = Name.declare x' bs;
+          in ZAbsp (x', t', Same.commit_if (x <> x' orelse not term_eq) (proof bs') p) end
+      | proof bs (ZAppt (p, t)) =
+          (ZAppt (proof bs p, Same.commit (term bs) t)
+            handle Same.SAME => ZAppt (p, term bs t))
+      | proof bs (ZAppp (p, q)) =
+          (ZAppp (proof bs p, Same.commit (proof bs) q)
+            handle Same.SAME => ZAppp (p, proof bs q))
+      | proof bs (ZHyp t) = ZHyp (term bs t)
+      | proof _ _ = raise Same.SAME;
+  in (term Name.context, proof Name.context) end;
+
+val used_frees_type = fold_tvars (fn ((a, ~1), _) => Name.declare a | _ => I);
+fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
+val used_frees_proof = fold_proof {hyps = true} used_frees_type used_frees_term;
+
+fun hidden_types prop proof =
+  let
+    val visible = (fold_types o fold_tvars) (insert (op =)) prop [];
+    val add_hiddenT = fold_tvars (fn v => not (member (op =) visible v) ? insert (op =) v);
+  in rev (fold_proof {hyps = true} add_hiddenT (fold_types add_hiddenT) proof []) end;
+
+fun standard_hidden_types prop proof =
+  let
+    val hidden = hidden_types prop proof;
+    val idx = maxidx_term prop (maxidx_proof proof ~1) + 1;
+    fun zvar (v as (_, S)) =
+      if not (member (op =) hidden v) then raise Same.SAME
+      else if null S then ztyp_dummy
+      else ZTVar (("'", idx), S);
+    val typ = map_tvars_same zvar;
+  in proof |> not (null hidden) ? map_proof {hyps = true} typ (map_types typ) end;
+
+fun standard_hidden_terms prop proof =
+  let
+    fun add_unless excluded (ZVar v) = not (member (op =) excluded v) ? insert (op =) v
+      | add_unless _ _ = I;
+    val visible = fold_aterms (add_unless []) prop [];
+    val hidden = fold_proof {hyps = true} (K I) (fold_aterms (add_unless visible)) proof [];
+    fun var (v as (_, T)) =
+      if member (op =) hidden v then zterm_dummy_pattern T else raise Same.SAME;
+    val term = map_vars_same var;
+  in proof |> not (null hidden) ? map_proof {hyps = true} Same.same term end;
+
+fun standard_inst add mk (v as ((x, i), T)) (inst, used) =
+  let
+    val (x', used') = Name.variant_bound x used;
+    val inst' = if x = x' andalso i = ~1 then inst else add (v, mk ((x', ~1), T)) inst;
+  in (inst', used') end;
+
+fun standard_inst_type used prf =
+  let
+    val add_tvars = fold_tvars (fn v => ZTVars.add (v, ()));
+    val (instT, _) =
+      (ZTVars.empty, used) |> ZTVars.fold (standard_inst ZTVars.add ZTVar o #1)
+        (TVars.build (prf |> fold_proof {hyps = true} add_tvars (fold_types add_tvars)));
+  in instantiate_type_same instT end;
+
+fun standard_inst_term used inst_type prf =
+  let
+    val add_vars = fold_vars (fn (x, T) => ZVars.add ((x, Same.commit inst_type T), ()));
+    val (inst, _) =
+      (ZVars.empty, used) |> ZVars.fold (standard_inst ZVars.add ZVar o #1)
+        (ZVars.build (prf |> fold_proof {hyps = true} (K I) add_vars));
+  in instantiate_term_same inst_type inst end;
+
+val typargs_type = fold_tvars (fn ((a, ~1), S) => TFrees.add_set (a, S) | _ => I);
+val typargs_term = fold_types typargs_type;
+val typargs_proof = fold_proof {hyps = true} typargs_type typargs_term;
+
+val add_standard_vars_term = fold_aterms
+  (fn ZVar ((x, ~1), T) =>
+      (fn env =>
+        (case AList.lookup (op =) env x of
+          NONE => (x, T) :: env
+        | SOME T' =>
+            if T = T' then env
+            else
+              raise TYPE ("standard_vars_env: type conflict for variable " ^ quote x,
+                [typ_of T, typ_of T'], [])))
+    | _ => I);
+
+val add_standard_vars = fold_proof {hyps = true} (K I) add_standard_vars_term;
+
+in
+
+fun standard_vars used (prop, opt_prf) =
+  let
+    val prf = the_default ZNop opt_prf
+      |> standard_hidden_types prop
+      |> standard_hidden_terms prop;
+    val prop_prf = ZAppp (ZHyp prop, prf);
+
+    val used' = used |> used_frees_proof prop_prf;
+    val inst_type = standard_inst_type used' prop_prf;
+    val inst_term = standard_inst_term used' inst_type prop_prf;
+    val inst_proof = map_proof_same {hyps = true} inst_type inst_term;
+
+    val prop' = prop |> Same.commit (Same.compose variant_abs_term inst_term);
+    val opt_proof' =
+      if is_none opt_prf then NONE
+      else SOME (prf |> Same.commit (Same.compose variant_abs_proof inst_proof));
+    val proofs' = the_list opt_proof';
+
+    val args = build_rev (add_standard_vars_term prop' #> fold add_standard_vars proofs');
+    val typargs = TFrees.list_set (TFrees.build (typargs_term prop' #> fold typargs_proof proofs'));
+  in {typargs = typargs, args = args, prop = prop', proof = opt_proof'} end;
+
 end;
+
+end;