--- a/src/Pure/Proof/extraction.ML Fri Jun 07 15:20:01 2024 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jun 07 23:53:31 2024 +0200
@@ -11,7 +11,7 @@
val add_realizes_eqns : string list -> theory -> theory
val add_typeof_eqns_i : ((term * term) list * (term * term)) list -> theory -> theory
val add_typeof_eqns : string list -> theory -> theory
- val add_realizers_i : (string * (string list * term * Proofterm.proof)) list
+ val add_realizers_i : (Thm_Name.T * (string list * term * Proofterm.proof)) list
-> theory -> theory
val add_realizers : (thm * (string list * string * string)) list
-> theory -> theory
@@ -118,8 +118,11 @@
val change_types = Proofterm.change_types o SOME;
-fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
-fun corr_name s vs = extr_name s vs ^ "_correctness";
+fun extr_name ((name, i): Thm_Name.T) vs =
+ (Long_Name.append "extr" (space_implode "_" (name :: vs)), i);
+
+fun corr_name thm_name vs =
+ extr_name thm_name vs |>> suffix "_correctness";
fun msg d s = writeln (Symbol.spaces d ^ s);
@@ -202,16 +205,16 @@
typeof_eqns : rules,
types : (string * ((term -> term option) list *
(term -> typ -> term -> typ -> term) option)) list,
- realizers : (string list * (term * proof)) list Symtab.table,
+ realizers : (string list * (term * proof)) list Thm_Name.Table.table,
defs : thm list,
- expand : string list,
+ expand : Thm_Name.T list,
prep : (theory -> proof -> proof) option}
val empty =
{realizes_eqns = empty_rules,
typeof_eqns = empty_rules,
types = [],
- realizers = Symtab.empty,
+ realizers = Thm_Name.Table.empty,
defs = [],
expand = [],
prep = NONE};
@@ -224,7 +227,7 @@
{realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
types = AList.merge (op =) (K true) (types1, types2),
- realizers = Symtab.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
+ realizers = Thm_Name.Table.merge_list (eq_set (op =) o apply2 #1) (realizers1, realizers2),
defs = Library.merge Thm.eq_thm (defs1, defs2),
expand = Library.merge (op =) (expand1, expand2),
prep = if is_some prep1 then prep1 else prep2};
@@ -319,7 +322,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
- realizers = fold (Symtab.cons_list o prep_rlz thy) rs realizers,
+ realizers = fold (Thm_Name.Table.cons_list o prep_rlz thy) rs realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -335,8 +338,8 @@
val rd = Proof_Syntax.read_proof thy' true false;
in fn (thm, (vs, s1, s2)) =>
let
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_realizers: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_realizers: unnamed theorem" else ();
val prop = Thm.unconstrainT thm |> Thm.prop_of |>
Pattern.rewrite_term thy' (map (Logic.dest_equals o Thm.prop_of) defs) [];
val vars = vars_of prop;
@@ -357,7 +360,7 @@
val r = Logic.list_implies (shyps,
fold_rev Logic.all (map (get_var_type r') vars) r');
val prf = Proofterm.reconstruct_proof thy' r (rd s2);
- in (name, (vs, (t, prf))) end
+ in (thm_name, (vs, (t, prf))) end
end;
val add_realizers_i = gen_add_realizers
@@ -411,8 +414,8 @@
val {realizes_eqns, typeof_eqns, types, realizers,
defs, expand, prep} = ExtractionData.get thy;
- val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
+ val thm_name = Thm.derivation_name thm;
+ val _ = if Thm_Name.is_empty thm_name then error "add_expand_thm: unnamed theorem" else ();
in
thy |> ExtractionData.put
(if is_def then
@@ -425,7 +428,7 @@
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
realizers = realizers, defs = defs,
- expand = insert (op =) name expand, prep = prep})
+ expand = insert (op =) thm_name expand, prep = prep})
end;
fun extraction_expand is_def =
@@ -508,8 +511,9 @@
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc [];
- fun expand_name ({name, ...}: Proofterm.thm_header) =
- if name = "" orelse member (op =) expand name then SOME "" else NONE;
+ fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+ if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
+ then SOME Thm_Name.empty else NONE;
val prep = the_default (K I) prep thy' o
Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
Proofterm.expand_proof thy' expand_name;
@@ -539,7 +543,8 @@
(T, Sign.defaultS thy)) tye;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
- fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
+ fun filter_thm_name (a: Thm_Name.T) =
+ map_filter (fn (b, x) => if a = b then SOME x else NONE);
fun app_rlz_rews Ts vs t =
strip_abs (length Ts)
@@ -618,7 +623,7 @@
| corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
- val {pos, theory_name, name, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -629,14 +634,16 @@
else snd (extr d vs ts Ts hs prf0 defs)
in
if T = nullT andalso realizes_null vs' prop aconv prop then (prf0, defs)
- else (case Symtab.lookup realizers name of
- NONE => (case find vs' (find' name defs') of
+ else (case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs') of
NONE =>
let
val _ = T = nullT orelse error "corr: internal error";
- val _ = msg d ("Building correctness proof for " ^ quote name ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Building correctness proof for " ^
+ quote (Thm_Name.short thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (corr_prf0, defs'') = corr (d + 1) vs' [] [] []
(rev shyps) NONE prf' prf' defs';
@@ -644,7 +651,7 @@
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name name vs') corr_prop
+ (corr_name thm_name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf' =
Proofterm.proof_combP
@@ -656,15 +663,16 @@
mkabsp shyps
in
(Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs),
- (name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
+ (thm_name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'')
end
| SOME (_, (_, prf')) =>
(Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs'))
| SOME rs => (case find vs' rs of
SOME (_, prf') => (Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs), defs')
| NONE => error ("corr: no realizer for instance of theorem " ^
- quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
- (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
+ quote (Thm_Name.short thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy'
+ (Envir.beta_norm (Proofterm.prop_of (Proofterm.proof_combt (prf0, ts)))))))
end
| corr d vs ts Ts hs cs _ (prf0 as PAxm (s, prop, SOME Ts')) _ defs =
@@ -674,7 +682,7 @@
in
if etype_of thy' vs' [] prop = nullT andalso
realizes_null vs' prop aconv prop then (prf0, defs)
- else case find vs' (Symtab.lookup_list realizers s) of
+ else case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (_, prf) => (Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye),
defs)
| NONE => error ("corr: no realizer for instance of axiom " ^
@@ -719,19 +727,20 @@
| extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
- val {pos, theory_name, name = s, prop, ...} = thm_header;
+ val {pos, theory_name, thm_name, prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case Symtab.lookup realizers s of
- NONE => (case find vs' (find' s defs) of
+ case Thm_Name.Table.lookup realizers thm_name of
+ NONE => (case find vs' (filter_thm_name thm_name defs) of
NONE =>
let
- val _ = msg d ("Extracting " ^ quote s ^
- (if null vs' then ""
- else " (relevant variables: " ^ commas_quote vs' ^ ")"));
+ val _ =
+ msg d ("Extracting " ^ quote (Thm_Name.short thm_name) ^
+ (if null vs' then ""
+ else " (relevant variables: " ^ commas_quote vs' ^ ")"));
val prf' = prep (Proofterm.reconstruct_proof thy' prop prf);
val (t, defs') = extr (d + 1) vs' [] [] [] prf' defs;
val (corr_prf, defs'') = corr (d + 1) vs' [] [] []
@@ -743,7 +752,7 @@
val args' = filter (fn v => Logic.occs (v, nt)) args;
val t' = mkabs args' nt;
val T = fastype_of t';
- val cname = extr_name s vs';
+ val cname = Thm_Name.short (extr_name thm_name vs');
val c = Const (cname, T);
val u = mkabs args (list_comb (c, args'));
val eqn = Logic.mk_equals (c, t');
@@ -764,7 +773,7 @@
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
Proofterm.thm_header (serial ()) pos theory_name
- (corr_name s vs') corr_prop
+ (corr_name thm_name vs') corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
@@ -775,13 +784,14 @@
mkabsp shyps
in
(subst_TVars tye' u,
- (s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
+ (thm_name, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'')
end
| SOME ((_, u), _) => (subst_TVars tye' u, defs))
| SOME rs => (case find vs' rs of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of theorem " ^
- quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
+ quote (Thm_Name.short thm_name) ^ ":\n" ^
+ Syntax.string_of_term_global thy' (Envir.beta_norm
(Proofterm.prop_of (Proofterm.proof_combt (prf0, ts))))))
end
@@ -790,7 +800,7 @@
val (vs', tye) = find_inst prop Ts ts vs;
val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
in
- case find vs' (Symtab.lookup_list realizers s) of
+ case find vs' (Thm_Name.Table.lookup_list realizers (s, 0)) of
SOME (t, _) => (subst_TVars tye' t, defs)
| NONE => error ("extr: no realizer for instance of axiom " ^
quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
@@ -805,26 +815,27 @@
val prop = Thm.prop_of thm;
val prf = Thm.proof_of thm;
val name = Thm.derivation_name thm;
- val _ = name <> "" orelse error "extraction: unnamed theorem";
+ val _ = if Thm_Name.is_empty name then error "extraction: unnamed theorem" else ();
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
- quote name ^ " has no computational content")
+ quote (Thm_Name.short name) ^ " has no computational content")
in Proofterm.reconstruct_proof thy' prop prf end;
val defs =
fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
thm_vss [];
- fun add_def (s, (vs, ((t, u)))) thy =
+ fun add_def (name, (vs, ((t, u)))) thy =
let
val ft = Type.legacy_freeze t;
val fu = Type.legacy_freeze u;
val head = head_of (strip_abs_body fu);
- val b = Binding.qualified_name (extr_name s vs);
+ val b = Binding.qualified_name (Thm_Name.short (extr_name name vs));
in
thy
|> Sign.add_consts [(b, fastype_of ft, NoSyn)]
|> Global_Theory.add_def
- (Binding.qualified_name (Thm.def_name (extr_name s vs)), Logic.mk_equals (head, ft))
+ (Binding.qualified_name (Thm.def_name (Thm_Name.short (extr_name name vs))),
+ Logic.mk_equals (head, ft))
|-> (fn def_thm =>
Spec_Rules.add_global b Spec_Rules.equational
[Thm.term_of (Thm.lhs_of def_thm)] [def_thm]
@@ -836,7 +847,7 @@
val corr_prop = Proofterm.prop_of prf;
in
thy
- |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
+ |> Global_Theory.store_thm (Binding.qualified_name (Thm_Name.short (corr_name s vs)),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
(Proof_Checker.thm_of_proof thy
@@ -845,7 +856,7 @@
end;
fun add_def_and_corr (s, (vs, ((t, u), (prf, _)))) thy =
- if is_none (Sign.const_type thy (extr_name s vs))
+ if is_none (Sign.const_type thy (Thm_Name.short (extr_name s vs)))
then
thy
|> not (t = nullt) ? add_def (s, (vs, ((t, u))))