--- a/src/Pure/sign.ML Tue Oct 21 17:48:06 1997 +0200
+++ b/src/Pure/sign.ML Tue Oct 21 18:09:13 1997 +0200
@@ -18,14 +18,20 @@
signature SIGN =
sig
type sg
+ type sg_ref
val rep_sg: sg ->
- {tsig: Type.type_sig,
+ {id: string ref, (* FIXME hide!? *)
+ self: sg_ref,
+ tsig: Type.type_sig,
const_tab: typ Symtab.table,
syn: Syntax.syntax,
path: string list,
spaces: (string * NameSpace.T) list,
data: Data.T,
- stamps: string ref list}
+ stamps: string ref list} (* FIXME hide!? *)
+ val tsig_of: sg -> Type.type_sig
+ val deref: sg_ref -> sg
+ val self_ref: sg -> sg_ref
val subsig: sg * sg -> bool
val eq_sg: sg * sg -> bool
val same_sg: sg * sg -> bool
@@ -108,9 +114,9 @@
val get_data: sg -> string -> exn
val put_data: string * exn -> sg -> sg
val print_data: sg -> string -> unit
- val prep_ext: sg -> sg
+ val merge_refs: sg_ref * sg_ref -> sg_ref
+ val make_draft: sg -> sg
val merge: sg * sg -> sg
- val nontriv_merge: sg * sg -> sg
val proto_pure: sg
val pure: sg
val cpure: sg
@@ -121,22 +127,55 @@
structure Sign : SIGN =
struct
+
(** datatype sg **)
datatype sg =
Sg of {
+ id: string ref, (*id*)
+ self: sg_ref, (*mutable self reference*)
tsig: Type.type_sig, (*order-sorted signature of types*)
const_tab: typ Symtab.table, (*type schemes of constants*)
syn: Syntax.syntax, (*syntax for parsing and printing*)
path: string list, (*current name space entry prefix*)
spaces: (string * NameSpace.T) list, (*name spaces for consts, types etc.*)
data: Data.T, (*additional data*)
- stamps: string ref list}; (*unique theory indentifier*)
+ stamps: string ref list} (*unique theory indentifier*)
(*the "ref" in stamps ensures that no two signatures are identical
-- it is impossible to forge a signature*)
+and sg_ref =
+ SgRef of sg ref option;
+(*make signature*)
+fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
+ Sg {id = id, self = self, tsig = tsig, const_tab = const_tab, syn = syn,
+ path = path, spaces = spaces, data = data, stamps = stamps};
+
+(*dest signature*)
fun rep_sg (Sg args) = args;
val tsig_of = #tsig o rep_sg;
+val self_ref = #self o rep_sg;
+
+fun get_data (Sg {data, ...}) = Data.get data;
+fun print_data (Sg {data, ...}) = Data.print data;
+
+
+(*show stamps*)
+fun stamp_names stamps = rev (map ! stamps);
+
+fun pretty_sg (Sg {stamps, ...}) = Pretty.str_list "{" "}" (stamp_names stamps);
+val pprint_sg = Pretty.pprint o pretty_sg;
+
+
+(* signature id *)
+
+fun deref (SgRef (Some (ref sg))) = sg
+ | deref (SgRef None) = sys_error "Sign.deref";
+
+fun check_stale (sg as Sg {id, self = SgRef (Some (ref (Sg {id = id', ...}))), ...}) =
+ if id = id' then sg
+ else raise TERM ("Stale signature: " ^ Pretty.str_of (pretty_sg sg), [])
+ | check_stale _ = sys_error "Sign.check_stale";
(* inclusion and equality *)
@@ -157,28 +196,62 @@
if x = y then fast_sub (xs, ys)
else fast_sub (x :: xs, ys);
in
- fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
- s1 = s2 orelse subset_stamp (s1, s2);
+ fun eq_sg (sg1 as Sg {id = id1, ...}, sg2 as Sg {id = id2, ...}) =
+ (check_stale sg1; check_stale sg2; id1 = id2);
- fun fast_subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
- s1 = s2 orelse fast_sub (s1, s2);
+ fun subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
+ eq_sg (sg1, sg2) orelse subset_stamp (s1, s2);
- fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
- s1 = s2 orelse (subset_stamp (s1, s2) andalso subset_stamp (s2, s1));
+ fun fast_subsig (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
+ eq_sg (sg1, sg2) orelse fast_sub (s1, s2);
end;
(*test if same theory names are contained in signatures' stamps,
i.e. if signatures belong to same theory but not necessarily to the
same version of it*)
-fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
- eq_set_string (pairself (map (op !)) (s1, s2));
+fun same_sg (sg1 as Sg {stamps = s1, ...}, sg2 as Sg {stamps = s2, ...}) =
+ eq_sg (sg1, sg2) orelse eq_set_string (pairself (map (op !)) (s1, s2));
(*test for drafts*)
fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
| is_draft _ = false;
+(* build signature *)
+
+fun ext_stamps stamps (id as ref name) =
+ let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
+ if exists (equal name o !) stmps then
+ error ("Theory already contains a " ^ quote name ^ " component")
+ else id :: stmps
+ end;
+
+fun create_sign self stamps name (syn, tsig, ctab, (path, spaces), data) =
+ let
+ val id = ref name;
+ val sign =
+ make_sign (id, self, tsig, ctab, syn, path, spaces, data, ext_stamps stamps id);
+ in
+ (case self of
+ SgRef (Some r) => r := sign
+ | _ => sys_error "Sign.create_sign");
+ sign
+ end;
+
+fun extend_sign extfun name decls
+ (sg as Sg {id = _, self, tsig, const_tab, syn, path, spaces, data, stamps}) =
+ let
+ val _ = check_stale sg;
+ val (self', data') =
+ if is_draft sg then (self, data)
+ else (SgRef (Some (ref sg)), Data.prep_ext data);
+ in
+ create_sign self' stamps name
+ (extfun (syn, tsig, const_tab, (path, spaces), data') decls)
+ end;
+
+
(* consts *)
fun const_type (Sg {const_tab, ...}) c = Symtab.lookup (const_tab, c);
@@ -320,6 +393,7 @@
val intern_tycons = intrn_tycons o spaces_of;
fun full_name (Sg {path, ...}) = full path;
+
end;
@@ -368,8 +442,6 @@
(** print signature **)
-fun stamp_names stamps = rev (map ! stamps);
-
fun print_sg sg =
let
fun prt_cls c = pretty_sort sg [c];
@@ -405,7 +477,7 @@
fun pretty_const (c, ty) = Pretty.block
[prt_const c, Pretty.str " ::", Pretty.brk 1, prt_typ ty];
- val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
+ val Sg {id = _, self = _, tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
val {classes, classrel, default, tycons, abbrs, arities} =
Type.rep_tsig tsig;
@@ -424,12 +496,6 @@
end;
-fun pretty_sg (Sg {stamps, ...}) =
- Pretty.str_list "{" "}" (stamp_names stamps);
-
-val pprint_sg = Pretty.pprint o pretty_sg;
-
-
(** read types **) (*exception ERROR*)
@@ -598,18 +664,18 @@
(* add default sort *)
-fun ext_defsort int (syn, tsig, ctab, (path, spaces)) S =
+fun ext_defsort int (syn, tsig, ctab, (path, spaces), data) S =
(syn, Type.ext_tsig_defsort tsig (if int then intrn_sort spaces S else S),
- ctab, (path, spaces));
+ ctab, (path, spaces), data);
(* add type constructors *)
-fun ext_types (syn, tsig, ctab, (path, spaces)) types =
+fun ext_types (syn, tsig, ctab, (path, spaces), data) types =
let val decls = decls_of path Syntax.type_name types in
(Syntax.extend_type_gram syn types,
Type.ext_tsig_types tsig decls, ctab,
- (path, add_names spaces typeK (map fst decls)))
+ (path, add_names spaces typeK (map fst decls)), data)
end;
@@ -619,7 +685,7 @@
(t, vs, read_raw_typ syn tsig spaces (K None) rhs_src)
handle ERROR => error ("in type abbreviation " ^ t);
-fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces)) abbrs =
+fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
let
fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
val syn' = Syntax.extend_type_gram syn (map mfix_of abbrs);
@@ -630,7 +696,7 @@
val spaces' = add_names spaces typeK (map #1 abbrs');
val decls = map (rd_abbr syn' tsig spaces') abbrs';
in
- (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'))
+ (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data)
end;
fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
@@ -639,7 +705,7 @@
(* add type arities *)
-fun ext_arities int (syn, tsig, ctab, (path, spaces)) arities =
+fun ext_arities int (syn, tsig, ctab, (path, spaces), data) arities =
let
fun intrn_arity (c, Ss, S) =
(intrn spaces typeK c, map (intrn_sort spaces) Ss, intrn_sort spaces S);
@@ -647,7 +713,7 @@
val tsig' = Type.ext_tsig_arities tsig (intrn arities);
val log_types = Type.logical_types tsig';
in
- (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces))
+ (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
end;
@@ -667,7 +733,7 @@
(c, read_raw_typ syn tsig spaces (K None) ty_src, mx)
handle ERROR => err_in_const (const_name path c mx);
-fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces)) raw_consts =
+fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab, (path, spaces), data) raw_consts =
let
fun prep_const (c, ty, mx) =
(c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
@@ -682,7 +748,7 @@
(Syntax.extend_const_gram syn prmode consts, tsig,
Symtab.extend_new (ctab, decls)
handle Symtab.DUPS cs => err_dup_consts cs,
- (path, add_names spaces constK (map fst decls)))
+ (path, add_names spaces constK (map fst decls)), data)
end;
val ext_consts_i = ext_cnsts no_read false ("", true);
@@ -706,7 +772,7 @@
end;
-fun ext_classes int (syn, tsig, ctab, (path, spaces)) classes =
+fun ext_classes int (syn, tsig, ctab, (path, spaces), data) classes =
let
val names = map fst classes;
val consts =
@@ -720,62 +786,51 @@
in
ext_consts_i
(Syntax.extend_consts syn names,
- Type.ext_tsig_classes tsig classes', ctab, (path, spaces'))
+ Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
consts
end;
(* add to classrel *)
-fun ext_classrel int (syn, tsig, ctab, (path, spaces)) pairs =
+fun ext_classrel int (syn, tsig, ctab, (path, spaces), data) pairs =
let val intrn = if int then map (pairself (intrn_class spaces)) else I in
- (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces))
+ (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data)
end;
(* add to syntax *)
-fun ext_syn extfun (syn, tsig, ctab, names) args =
- (extfun syn args, tsig, ctab, names);
+fun ext_syn extfun (syn, tsig, ctab, names, data) args =
+ (extfun syn args, tsig, ctab, names, data);
(* add to path *)
-fun ext_path (syn, tsig, ctab, (path, spaces)) elem =
+fun ext_path (syn, tsig, ctab, (path, spaces), data) elem =
let
val path' =
if elem = ".." andalso not (null path) then fst (split_last path)
else if elem = "/" then []
else path @ NameSpace.unpack elem;
in
- (syn, tsig, ctab, (path', spaces))
+ (syn, tsig, ctab, (path', spaces), data)
end;
(* add to name space *)
-fun ext_space (syn, tsig, ctab, (path, spaces)) (kind, names) =
- (syn, tsig, ctab, (path, add_names spaces kind names));
+fun ext_space (syn, tsig, ctab, (path, spaces), data) (kind, names) =
+ (syn, tsig, ctab, (path, add_names spaces kind names), data);
-(* build signature *)
+(* signature data *)
-fun ext_stamps stamps name =
- let
- val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
- in
- if exists (equal name o !) stmps then
- error ("Theory already contains a " ^ quote name ^ " component")
- else ref name :: stmps
- end;
+fun ext_init_data (syn, tsig, ctab, names, data) (kind, e, ext, mrg, prt) =
+ (syn, tsig, ctab, names, Data.init data kind e ext mrg prt);
-fun make_sign (syn, tsig, ctab, (path, spaces)) data stamps name =
- Sg {tsig = tsig, const_tab = ctab, syn = syn, path = path, spaces = spaces,
- data = data, stamps = ext_stamps stamps name};
-
-fun extend_sign extfun name decls
- (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
- make_sign (extfun (syn, tsig, const_tab, (path, spaces)) decls) data stamps name;
+fun ext_put_data (syn, tsig, ctab, names, data) (kind, e) =
+ (syn, tsig, ctab, names, Data.put data kind e);
(* the external interfaces *)
@@ -804,49 +859,48 @@
val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
val add_path = extend_sign ext_path "#";
val add_space = extend_sign ext_space "#";
+val init_data = extend_sign ext_init_data "#";
+val put_data = extend_sign ext_put_data "#";
fun add_name name sg = extend_sign K name () sg;
val make_draft = add_name "#";
-(* additional signature data *)
-fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
- make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
+(** merge signatures **) (*exception TERM*)
-fun init_data (kind, e, ext, mrg, prt) =
- map_data (fn d => Data.init d kind e ext mrg prt);
+(* merge of sg_refs -- trivial only *)
-fun get_data (Sg {data, ...}) = Data.get data;
-fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
-fun print_data (Sg {data, ...}) kind = Data.print data kind;
-
-(*prepare extension*)
-fun prep_ext sg =
- map_data Data.prep_ext sg |> add_path "/";
+fun merge_refs (sgr1 as SgRef (Some (ref sg1)),
+ sgr2 as SgRef (Some (ref sg2))) =
+ if fast_subsig (sg2, sg1) then sgr1
+ else if fast_subsig (sg1, sg2) then sgr2
+ else if subsig (sg2, sg1) then sgr1
+ else if subsig (sg1, sg2) then sgr2
+ else raise TERM ("Attempt to do non-trivial merge of signatures", [])
+ | merge_refs _ = sys_error "Sign.merge_refs";
-(** merge signatures **) (*exception TERM*)
+(* proper merge *)
-fun merge_aux triv_only (sg1, sg2) =
- if fast_subsig (sg2, sg1) then sg1
- else if fast_subsig (sg1, sg2) then sg2
- else if subsig (sg2, sg1) then sg1
+fun merge_aux (sg1, sg2) =
+ if subsig (sg2, sg1) then sg1
else if subsig (sg1, sg2) then sg2
else if is_draft sg1 orelse is_draft sg2 then
- raise TERM ("Illegal merge of draft signatures", [])
- else if triv_only then
- raise TERM ("Illegal non-trivial merge of signatures", [])
+ raise TERM ("Attempt to merge draft signatures", [])
else
(*neither is union already; must form union*)
let
- val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
+ val Sg {id = _, self = _, tsig = tsig1, const_tab = const_tab1, syn = syn1,
path = _, spaces = spaces1, data = data1, stamps = stamps1} = sg1;
- val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
+ val Sg {id = _, self = _, tsig = tsig2, const_tab = const_tab2, syn = syn2,
path = _, spaces = spaces2, data = data2, stamps = stamps2} = sg2;
+ val id = ref "";
+ val self_ref = ref sg1; (*dummy value*)
+ val self = SgRef (Some self_ref);
val stamps = merge_rev_lists stamps1 stamps2;
val _ =
(case duplicates (stamp_names stamps) of
@@ -855,13 +909,12 @@
^ commas_quote dups, []));
val tsig = Type.merge_tsigs (tsig1, tsig2);
-
val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
handle Symtab.DUPS cs =>
raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
-
val syn = Syntax.merge_syntaxes syn1 syn2;
+ val path = [];
val kinds = distinct (map fst (spaces1 @ spaces2));
val spaces =
kinds ~~
@@ -869,25 +922,27 @@
(map (space_of spaces1) kinds, map (space_of spaces2) kinds);
val data = Data.merge (data1, data2);
+
+ val sign = make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps);
in
- Sg {tsig = tsig, const_tab = const_tab, syn = syn,
- path = [], spaces = spaces, data = data, stamps = stamps}
+ self_ref := sign; sign
end;
-fun gen_merge triv sgs =
- (case handle_error (merge_aux triv) sgs of
+fun merge sg1_sg2 =
+ (case handle_error merge_aux sg1_sg2 of
OK sg => sg
| Error msg => raise TERM (msg, []));
-val merge = gen_merge true;
-val nontriv_merge = gen_merge false;
-
(** the Pure signature **)
+val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
+ Symtab.null, Syntax.pure_syn, [], [], Data.empty, []);
+
val proto_pure =
- make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], [])) Data.empty [] "#"
+ create_sign (SgRef (Some (ref dummy_sg))) [] "#"
+ (Syntax.pure_syn, Type.tsig0, Symtab.null, ([], []), Data.empty)
|> add_types
(("fun", 2, NoSyn) ::
("prop", 0, NoSyn) ::
--- a/src/Pure/thm.ML Tue Oct 21 17:48:06 1997 +0200
+++ b/src/Pure/thm.ML Tue Oct 21 18:09:13 1997 +0200
@@ -86,6 +86,7 @@
val crep_thm : thm -> {sign: Sign.sg, der: deriv, maxidx: int,
shyps: sort list, hyps: cterm list,
prop: cterm}
+ val sign_of_thm : thm -> Sign.sg
val stamps_of_thm : thm -> string ref list
val transfer : theory -> thm -> thm
val tpairs_of : thm -> (term * term) list
@@ -177,16 +178,17 @@
(*certified typs under a signature*)
-datatype ctyp = Ctyp of {sign: Sign.sg, T: typ};
+datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
-fun rep_ctyp (Ctyp args) = args;
+(* FIXME tune!? *)
+fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
fun typ_of (Ctyp {T, ...}) = T;
fun ctyp_of sign T =
- Ctyp {sign = sign, T = Sign.certify_typ sign T};
+ Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
fun read_ctyp sign s =
- Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s};
+ Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
@@ -194,60 +196,63 @@
(*certified terms under a signature, with checked typ and maxidx of Vars*)
-datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int};
+datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
-fun rep_cterm (Cterm args) = args;
+(* FIXME tune!? *)
+fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
+ {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
+
fun term_of (Cterm {t, ...}) = t;
-fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T};
+fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
(*create a cterm by checking a "raw" term with respect to a signature*)
fun cterm_of sign tm =
let val (t, T, maxidx) = Sign.certify_term sign tm
- in Cterm {sign = sign, t = t, T = T, maxidx = maxidx}
+ in Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
end;
-fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t);
+fun cterm_fun f (Cterm {sign_ref, t, ...}) = cterm_of (Sign.deref sign_ref) (f t);
exception CTERM of string;
(*Destruct application in cterms*)
-fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) =
+fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
let val typeA = fastype_of A;
val typeB =
case typeA of Type("fun",[S,T]) => S
| _ => error "Function type expected in dest_comb";
in
- (Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA},
- Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB})
+ (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
+ Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
end
| dest_comb _ = raise CTERM "dest_comb";
(*Destruct abstraction in cterms*)
-fun dest_abs (Cterm {sign, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
+fun dest_abs (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
let val (y,N) = variant_abs (x,ty,M)
- in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)},
- Cterm {sign = sign, T = S, maxidx = maxidx, t = N})
+ in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
+ Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
end
| dest_abs _ = raise CTERM "dest_abs";
(*Makes maxidx precise: it is often too big*)
-fun adjust_maxidx (ct as Cterm {sign, T, t, maxidx, ...}) =
+fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
if maxidx = ~1 then ct
- else Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t};
+ else Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
(*Form cterm out of a function and an argument*)
-fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
- (Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) =
- if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty,
+fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
+ (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
+ if T = dty then Cterm{t=f$x, sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
maxidx=Int.max(maxidx1, maxidx2)}
else raise CTERM "capply: types don't agree"
| capply _ _ = raise CTERM "capply: first arg is not a function"
-fun cabs (Cterm {t=Free(a,ty), sign=sign1, T=T1, maxidx=maxidx1})
- (Cterm {t=t2, sign=sign2, T=T2, maxidx=maxidx2}) =
- Cterm {t=absfree(a,ty,t2), sign=Sign.merge(sign1,sign2),
+fun cabs (Cterm {t=Free(a,ty), sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
+ (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
+ Cterm {t=absfree(a,ty,t2), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2),
T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)}
| cabs _ _ = raise CTERM "cabs: first arg is not a free variable";
@@ -262,7 +267,7 @@
handle TYPE (msg, _, _) => error msg;
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
val (_, t', tye) =
- Sign.infer_types sign types sorts used freeze (ts, T');
+ Sign.infer_types sign types sorts used freeze (ts, T');
val ct = cterm_of sign t'
handle TYPE (msg, _, _) => error msg
| TERM (msg, _) => error msg;
@@ -384,19 +389,22 @@
(*** Meta theorems ***)
datatype thm = Thm of
- {sign: Sign.sg, (*signature for hyps and prop*)
- der: deriv, (*derivation*)
- maxidx: int, (*maximum index of any Var or TVar*)
- shyps: sort list, (*sort hypotheses*)
- hyps: term list, (*hypotheses*)
- prop: term}; (*conclusion*)
+ {sign_ref: Sign.sg_ref, (*mutable reference to signature*)
+ der: deriv, (*derivation*)
+ maxidx: int, (*maximum index of any Var or TVar*)
+ shyps: sort list, (*sort hypotheses*)
+ hyps: term list, (*hypotheses*)
+ prop: term}; (*conclusion*)
-fun rep_thm (Thm args) = args;
+(* FIXME tune!? *)
+fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+ {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
+ shyps = shyps, hyps = hyps, prop = prop};
(*Version of rep_thm returning cterms instead of terms*)
-fun crep_thm (Thm {sign, der, maxidx, shyps, hyps, prop}) =
- let fun ctermf max t = Cterm{sign=sign, t=t, T=propT, maxidx=max};
- in {sign=sign, der=der, maxidx=maxidx, shyps=shyps,
+fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+ let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
+ in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
hyps = map (ctermf ~1) hyps,
prop = ctermf maxidx prop}
end;
@@ -405,21 +413,23 @@
exception THM of string * int * thm list;
-val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm;
+fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
+val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm;
(*merge signatures of two theorems; raise exception if incompatible*)
-fun merge_thm_sgs (th1, th2) =
- Sign.merge (pairself (#sign o rep_thm) (th1, th2))
- handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
+fun merge_thm_sgs
+ (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
+ Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
-(*transfer thm to super theory*)
+(*transfer thm to super theory (non-destructive)*)
fun transfer thy thm =
let
- val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
+ val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
+ val sign = Sign.deref sign_ref;
val sign' = #sign (rep_theory thy);
in
if Sign.subsig (sign, sign') then
- Thm {sign = sign', der = der, maxidx = maxidx,
+ Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
shyps = shyps, hyps = hyps, prop = prop}
else raise THM ("transfer: not a super theory", 0, [thm])
end;
@@ -439,8 +449,8 @@
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
(*the statement of any thm is a cterm*)
-fun cprop_of (Thm {sign, maxidx, prop, ...}) =
- Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop};
+fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
+ Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
@@ -491,11 +501,11 @@
(*preserve sort contexts of rule premises and substituted types*)
fun fix_shyps thms Ts thm =
let
- val Thm {sign, der, maxidx, hyps, prop, ...} = thm;
+ val Thm {sign_ref, der, maxidx, hyps, prop, ...} = thm;
val shyps =
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, [])));
in
- Thm {sign = sign,
+ Thm {sign_ref = sign_ref,
der = der, (*No new derivation, as other rules call this*)
maxidx = maxidx,
shyps = shyps, hyps = hyps, prop = prop}
@@ -509,12 +519,12 @@
(*remove extra sorts that are known to be syntactically non-empty*)
fun strip_shyps thm =
let
- val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
+ val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
val sorts = add_thm_sorts (thm, []);
- val maybe_empty = not o Sign.nonempty_sort sign sorts;
+ val maybe_empty = not o Sign.nonempty_sort (Sign.deref sign_ref) sorts;
val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps;
in
- Thm {sign = sign, der = der, maxidx = maxidx,
+ Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
shyps =
(if eq_set_sort (shyps',sorts) orelse
not (!force_strip_shyps) then shyps'
@@ -536,7 +546,7 @@
[] => thm
| xshyps =>
let
- val Thm {sign, der, maxidx, shyps, hyps, prop} = thm;
+ val Thm {sign_ref, der, maxidx, shyps, hyps, prop} = thm;
val shyps' = ins_sort (logicS, shyps \\ xshyps);
val used_names = foldr add_term_tfree_names (prop :: hyps, []);
val names =
@@ -546,7 +556,7 @@
fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S;
val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps));
in
- Thm {sign = sign,
+ Thm {sign_ref = sign_ref,
der = infer_derivs (Implies_intr_shyps, [der]),
maxidx = maxidx,
shyps = shyps',
@@ -566,7 +576,7 @@
let val {sign, new_axioms, parents, ...} = rep_theory thy
in case Symtab.lookup (new_axioms, name) of
Some t => fix_shyps [] []
- (Thm {sign = sign,
+ (Thm {sign_ref = Sign.self_ref sign,
der = infer_derivs (Axiom(theory,name), []),
maxidx = maxidx_of_term t,
shyps = [],
@@ -586,8 +596,8 @@
(Symtab.dest (#new_axioms (rep_theory thy)));
(*Attach a label to a theorem to make proof objects more readable*)
-fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) =
- Thm {sign = sign,
+fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+ Thm {sign_ref = sign_ref,
der = Join (Theorem name, [der]),
maxidx = maxidx,
shyps = shyps,
@@ -597,8 +607,8 @@
(*Compression of theorems -- a separate rule, not integrated with the others,
as it could be slow.*)
-fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) =
- Thm {sign = sign,
+fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+ Thm {sign_ref = sign_ref,
der = der, (*No derivation recorded!*)
maxidx = maxidx,
shyps = shyps,
@@ -612,9 +622,9 @@
(*Check that term does not contain same var with different typing/sorting.
If this check must be made, recalculate maxidx in hope of preventing its
recurrence.*)
-fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s =
+fun nodup_Vars (thm as Thm{sign_ref, der, maxidx, shyps, hyps, prop}) s =
(Sign.nodup_Vars prop;
- Thm {sign = sign,
+ Thm {sign_ref = sign_ref,
der = der,
maxidx = maxidx_of_term prop,
shyps = shyps,
@@ -629,13 +639,13 @@
(*The assumption rule A|-A in a theory*)
fun assume ct : thm =
- let val {sign, t=prop, T, maxidx} = rep_cterm ct
+ let val Cterm {sign_ref, t=prop, T, maxidx} = ct
in if T<>propT then
raise THM("assume: assumptions must have type prop", 0, [])
else if maxidx <> ~1 then
raise THM("assume: assumptions may not contain scheme variables",
maxidx, [])
- else Thm{sign = sign,
+ else Thm{sign_ref = sign_ref,
der = infer_derivs (Assume ct, []),
maxidx = ~1,
shyps = add_term_sorts(prop,[]),
@@ -650,12 +660,12 @@
-------
A ==> B
*)
-fun implies_intr cA (thB as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
- let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA
+fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
+ let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
in if T<>propT then
raise THM("implies_intr: assumptions must have type prop", 0, [thB])
else fix_shyps [thB] []
- (Thm{sign = Sign.merge (sign,signA),
+ (Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),
der = infer_derivs (Implies_intr cA, [der]),
maxidx = Int.max(maxidxA, maxidx),
shyps = [],
@@ -673,13 +683,13 @@
*)
fun implies_elim thAB thA : thm =
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA
- and Thm{sign, der, maxidx, hyps, prop,...} = thAB;
+ and Thm{sign_ref, der, maxidx, hyps, prop,...} = thAB;
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA])
in case prop of
imp$A$B =>
if imp=implies andalso A aconv propA
then fix_shyps [thAB, thA] []
- (Thm{sign= merge_thm_sgs(thAB,thA),
+ (Thm{sign_ref= merge_thm_sgs(thAB,thA),
der = infer_derivs (Implies_elim, [der,derA]),
maxidx = Int.max(maxA,maxidx),
shyps = [],
@@ -694,10 +704,10 @@
-----
!!x.A
*)
-fun forall_intr cx (th as Thm{sign,der,maxidx,hyps,prop,...}) =
+fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
let val x = term_of cx;
fun result(a,T) = fix_shyps [th] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Forall_intr cx, [der]),
maxidx = maxidx,
shyps = [],
@@ -717,14 +727,14 @@
------
A[t/x]
*)
-fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm =
- let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct
+fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) : thm =
+ let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
in case prop of
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
if T<>qary then
raise THM("forall_elim: type mismatch", 0, [th])
else let val thm = fix_shyps [th] []
- (Thm{sign= Sign.merge(sign,signt),
+ (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
der = infer_derivs (Forall_elim ct, [der]),
maxidx = Int.max(maxidx, maxt),
shyps = [],
@@ -744,7 +754,7 @@
(* Definition of the relation =?= *)
val flexpair_def = fix_shyps [] []
- (Thm{sign= Sign.proto_pure,
+ (Thm{sign_ref= Sign.self_ref Sign.proto_pure,
der = Join(Axiom(pure_thy, "flexpair_def"), []),
shyps = [],
hyps = [],
@@ -754,9 +764,9 @@
(*The reflexivity rule: maps t to the theorem t==t *)
fun reflexive ct =
- let val {sign, t, T, maxidx} = rep_cterm ct
+ let val Cterm {sign_ref, t, T, maxidx} = ct
in fix_shyps [] []
- (Thm{sign= sign,
+ (Thm{sign_ref= sign_ref,
der = infer_derivs (Reflexive ct, []),
shyps = [],
hyps = [],
@@ -769,11 +779,11 @@
----
u==t
*)
-fun symmetric (th as Thm{sign,der,maxidx,shyps,hyps,prop}) =
+fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
case prop of
(eq as Const("==",_)) $ t $ u =>
(*no fix_shyps*)
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (Symmetric, [der]),
maxidx = maxidx,
shyps = shyps,
@@ -795,7 +805,7 @@
if not (u aconv u') then err"middle term"
else let val thm =
fix_shyps [th1, th2] []
- (Thm{sign= merge_thm_sgs(th1,th2),
+ (Thm{sign_ref= merge_thm_sgs(th1,th2),
der = infer_derivs (Transitive, [der1, der2]),
maxidx = Int.max(max1,max2),
shyps = [],
@@ -810,10 +820,10 @@
(*Beta-conversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *)
fun beta_conversion ct =
- let val {sign, t, T, maxidx} = rep_cterm ct
+ let val Cterm {sign_ref, t, T, maxidx} = ct
in case t of
Abs(_,_,bodt) $ u => fix_shyps [] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Beta_conversion ct, []),
maxidx = maxidx,
shyps = [],
@@ -827,7 +837,7 @@
------------
f == g
*)
-fun extensional (th as Thm{sign, der, maxidx,shyps,hyps,prop}) =
+fun extensional (th as Thm{sign_ref, der, maxidx,shyps,hyps,prop}) =
case prop of
(Const("==",_)) $ (f$x) $ (g$y) =>
let fun err(msg) = raise THM("extensional: "^msg, 0, [th])
@@ -841,7 +851,7 @@
then err"variable free in functions" else ()
| _ => err"not a variable");
(*no fix_shyps*)
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (Extensional, [der]),
maxidx = maxidx,
shyps = shyps,
@@ -856,13 +866,13 @@
------------
%x.t == %x.u
*)
-fun abstract_rule a cx (th as Thm{sign,der,maxidx,hyps,prop,...}) =
+fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
let val x = term_of cx;
val (t,u) = Logic.dest_equals prop
handle TERM _ =>
raise THM("abstract_rule: premise not an equality", 0, [th])
fun result T = fix_shyps [th] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Abstract_rule (a,cx), [der]),
maxidx = maxidx,
shyps = [],
@@ -900,7 +910,7 @@
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) =>
let val _ = chktypes (f,t)
val thm = (*no fix_shyps*)
- Thm{sign = merge_thm_sgs(th1,th2),
+ Thm{sign_ref = merge_thm_sgs(th1,th2),
der = infer_derivs (Combination, [der1, der2]),
maxidx = Int.max(max1,max2),
shyps = union_sort(shyps1,shyps2),
@@ -930,7 +940,7 @@
if A aconv A' andalso B aconv B'
then
(*no fix_shyps*)
- Thm{sign = merge_thm_sgs(th1,th2),
+ Thm{sign_ref = merge_thm_sgs(th1,th2),
der = infer_derivs (Equal_intr, [der1, der2]),
maxidx = Int.max(max1,max2),
shyps = union_sort(shyps1,shyps2),
@@ -954,7 +964,7 @@
Const("==",_) $ A $ B =>
if not (prop2 aconv A) then err"not equal" else
fix_shyps [th1, th2] []
- (Thm{sign= merge_thm_sgs(th1,th2),
+ (Thm{sign_ref= merge_thm_sgs(th1,th2),
der = infer_derivs (Equal_elim, [der1, der2]),
maxidx = Int.max(max1,max2),
shyps = [],
@@ -969,9 +979,9 @@
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps.
Repeated hypotheses are discharged only once; fold cannot do this*)
-fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) =
+fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, prop}) =
implies_intr_hyps (*no fix_shyps*)
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Implies_intr_hyps, [der]),
maxidx = maxidx,
shyps = shyps,
@@ -983,7 +993,7 @@
Instantiates the theorem and deletes trivial tpairs.
Resulting sequence may contain multiple elements if the tpairs are
not all flex-flex. *)
-fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) =
+fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, prop,...}) =
let fun newthm env =
if Envir.is_empty env then th
else
@@ -993,7 +1003,7 @@
val distpairs = filter (not o op aconv) tpairs
val newprop = Logic.list_flexpairs(distpairs, horn)
in fix_shyps [th] (env_codT env)
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Flexflex_rule env, [der]),
maxidx = maxidx_of_term newprop,
shyps = [],
@@ -1002,7 +1012,7 @@
end;
val (tpairs,_) = Logic.strip_flexpairs prop
in Sequence.maps newthm
- (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
+ (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
end;
(*Instantiation of Vars
@@ -1015,31 +1025,33 @@
fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
(*For instantiate: process pair of cterms, merge theories*)
-fun add_ctpair ((ct,cu), (sign,tpairs)) =
- let val {sign=signt, t=t, T= T, ...} = rep_cterm ct
- and {sign=signu, t=u, T= U, ...} = rep_cterm cu
- in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs)
- else raise TYPE("add_ctpair", [T,U], [t,u])
+fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
+ let val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
+ and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu
+ in
+ if T=U then
+ (Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu)), (t,u)::tpairs)
+ else raise TYPE("add_ctpair", [T,U], [t,u])
end;
-fun add_ctyp ((v,ctyp), (sign',vTs)) =
- let val {T,sign} = rep_ctyp ctyp
- in (Sign.merge(sign,sign'), (v,T)::vTs) end;
+fun add_ctyp ((v,ctyp), (sign_ref',vTs)) =
+ let val Ctyp {T,sign_ref} = ctyp
+ in (Sign.merge_refs(sign_ref,sign_ref'), (v,T)::vTs) end;
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...].
Instantiates distinct Vars by terms of same type.
Normalizes the new theorem! *)
fun instantiate ([], []) th = th
- | instantiate (vcTs,ctpairs) (th as Thm{sign,der,maxidx,hyps,prop,...}) =
- let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[]));
- val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[]));
+ | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,prop,...}) =
+ let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
+ val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
val newprop =
Envir.norm_term (Envir.empty 0)
(subst_atomic tpairs
- (Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop))
+ (Type.inst_term_tvars(Sign.tsig_of (Sign.deref newsign_ref),vTs) prop))
val newth =
fix_shyps [th] (map snd vTs)
- (Thm{sign = newsign,
+ (Thm{sign_ref = newsign_ref,
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]),
maxidx = maxidx_of_term newprop,
shyps = [],
@@ -1059,11 +1071,11 @@
(*The trivial implication A==>A, justified by assume and forall rules.
A can contain Vars, not so for assume! *)
fun trivial ct : thm =
- let val {sign, t=A, T, maxidx} = rep_cterm ct
+ let val Cterm {sign_ref, t=A, T, maxidx} = ct
in if T<>propT then
raise THM("trivial: the term must have type prop", 0, [])
else fix_shyps [] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Trivial ct, []),
maxidx = maxidx,
shyps = [],
@@ -1074,12 +1086,12 @@
(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
fun class_triv thy c =
let val sign = sign_of thy;
- val Cterm {t, maxidx, ...} =
+ val Cterm {sign_ref, t, maxidx, ...} =
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
in
fix_shyps [] []
- (Thm {sign = sign,
+ (Thm {sign_ref = sign_ref,
der = infer_derivs (Class_triv(thy,c), []),
maxidx = maxidx,
shyps = [],
@@ -1089,10 +1101,10 @@
(* Replace all TFrees not in the hyps by new TVars *)
-fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) =
+fun varifyT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
let val tfrees = foldr add_term_tfree_names (hyps,[])
in let val thm = (*no fix_shyps*)
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (VarifyT, [der]),
maxidx = Int.max(0,maxidx),
shyps = shyps,
@@ -1104,10 +1116,10 @@
end;
(* Replace all TVars by new TFrees *)
-fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) =
+fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,prop}) =
let val (prop',_) = Type.freeze_thaw prop
in (*no fix_shyps*)
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (FreezeT, [der]),
maxidx = maxidx_of_term prop',
shyps = shyps,
@@ -1130,15 +1142,15 @@
(*Increment variables and parameters of orule as required for
resolution with goal i of state. *)
fun lift_rule (state, i) orule =
- let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign=ssign,...} = state
+ let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop)
handle TERM _ => raise THM("lift_rule", i, [orule,state])
- val ct_Bi = Cterm {sign=ssign, maxidx=smax, T=propT, t=Bi}
+ val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
- val (Thm{sign, der, maxidx,shyps,hyps,prop}) = orule
+ val (Thm{sign_ref, der, maxidx,shyps,hyps,prop}) = orule
val (tpairs,As,B) = Logic.strip_horn prop
in (*no fix_shyps*)
- Thm{sign = merge_thm_sgs(state,orule),
+ Thm{sign_ref = merge_thm_sgs(state,orule),
der = infer_derivs (Lift_rule(ct_Bi, i), [der]),
maxidx = maxidx+smax+1,
shyps=union_sort(sshyps,shyps),
@@ -1150,11 +1162,11 @@
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
fun assumption i state =
- let val Thm{sign,der,maxidx,hyps,prop,...} = state;
+ let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) =
fix_shyps [state] (env_codT env)
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Assumption (i, Some env), [der]),
maxidx = maxidx,
shyps = [],
@@ -1167,18 +1179,18 @@
fun addprfs [] = Sequence.null
| addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull
(Sequence.mapp newth
- (Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs))
+ (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
(addprfs apairs)))
in addprfs (Logic.assum_pairs Bi) end;
(*Solve subgoal Bi of proof state B1...Bn/C by assumption.
Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
fun eq_assumption i state =
- let val Thm{sign,der,maxidx,hyps,prop,...} = state;
+ let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
in if exists (op aconv) (Logic.assum_pairs Bi)
then fix_shyps [state] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Assumption (i,None), [der]),
maxidx = maxidx,
shyps = [],
@@ -1190,7 +1202,7 @@
(*For rotate_tac: fast rotation of assumptions of subgoal i*)
fun rotate_rule k i state =
- let val Thm{sign,der,maxidx,hyps,prop,shyps} = state;
+ let val Thm{sign_ref,der,maxidx,hyps,prop,shyps} = state;
val (tpairs, Bs, Bi, C) = dest_state(state,i)
val params = Logic.strip_params Bi
and asms = Logic.strip_assums_hyp Bi
@@ -1204,7 +1216,7 @@
List.take(asms, m),
concl))
else raise THM("rotate_rule", m, [state])
- in Thm{sign = sign,
+ in Thm{sign_ref = sign_ref,
der = infer_derivs (Rotate_rule (k,i), [der]),
maxidx = maxidx,
shyps = shyps,
@@ -1220,7 +1232,7 @@
The names in cs, if distinct, are used for the innermost parameters;
preceding parameters may be renamed to make all params distinct.*)
fun rename_params_rule (cs, i) state =
- let val Thm{sign,der,maxidx,hyps,...} = state
+ let val Thm{sign_ref,der,maxidx,hyps,...} = state
val (tpairs, Bs, Bi, C) = dest_state(state,i)
val iparams = map #1 (Logic.strip_params Bi)
val short = length iparams - length cs
@@ -1237,7 +1249,7 @@
a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a);
state)
| [] => fix_shyps [state] []
- (Thm{sign = sign,
+ (Thm{sign_ref = sign_ref,
der = infer_derivs (Rename_params_rule(cs,i), [der]),
maxidx = maxidx,
shyps = [],
@@ -1342,7 +1354,8 @@
(*How many hyps to skip over during normalization*)
and nlift = Logic.count_prems(strip_all_body Bi,
if eres_flg then ~1 else 0)
- val sign = merge_thm_sgs(state,orule);
+ val sign_ref = merge_thm_sgs(state,orule);
+ val sign = Sign.deref sign_ref;
(** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
let val normt = Envir.norm_term env;
@@ -1361,7 +1374,7 @@
(ntps, map normt (Bs @ As), normt C)
end
val th = (*tuned fix_shyps*)
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (Bicompose(match, eres_flg,
1 + length Bs, nsubgoal, env),
[rder,sder]),
@@ -1452,8 +1465,12 @@
fun trace_warning a = if ! trace_simp then warning a else ();
fun trace_term a sign t = if ! trace_simp then prtm a sign t else ();
fun trace_term_warning a sign t = if ! trace_simp then prtm_warning a sign t else ();
-fun trace_thm a (Thm {sign, prop, ...}) = trace_term a sign prop;
-fun trace_thm_warning a (Thm {sign, prop, ...}) = trace_term_warning a sign prop;
+
+fun trace_thm a (Thm {sign_ref, prop, ...}) =
+ trace_term a (Sign.deref sign_ref) prop;
+
+fun trace_thm_warning a (Thm {sign_ref, prop, ...}) =
+ trace_term_warning a (Sign.deref sign_ref) prop;
@@ -1545,8 +1562,9 @@
(* mk_rrule *)
-fun mk_rrule (thm as Thm {sign, prop, ...}) =
+fun mk_rrule (thm as Thm {sign_ref, prop, ...}) =
let
+ val sign = Sign.deref sign_ref;
val prems = Logic.strip_imp_prems prop;
val concl = Logic.strip_imp_concl prop;
val (lhs, rhs) = Logic.dest_equals concl handle TERM _ =>
@@ -1562,13 +1580,13 @@
fun add_simp
(mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
- thm as Thm {sign, prop, ...}) =
+ thm as Thm {sign_ref, prop, ...}) =
(case mk_rrule thm of
None => mss
| Some (rrule as {lhs, ...}) =>
(trace_thm "Adding rewrite rule:" thm;
mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT =>
- (prtm_warning "ignoring duplicate rewrite rule" sign prop; rules),
+ (prtm_warning "ignoring duplicate rewrite rule" (Sign.deref sign_ref) prop; rules),
congs, procs, bounds, prems, mk_rews, termless)));
val add_simps = foldl add_simp;
@@ -1580,12 +1598,12 @@
fun del_simp
(mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
- thm as Thm {sign, prop, ...}) =
+ thm as Thm {sign_ref, prop, ...}) =
(case mk_rrule thm of
None => mss
| Some (rrule as {lhs, ...}) =>
mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE =>
- (prtm_warning "rewrite rule not in simpset" sign prop; rules),
+ (prtm_warning "rewrite rule not in simpset" (Sign.deref sign_ref) prop; rules),
congs, procs, bounds, prems, mk_rews, termless));
val del_simps = foldl del_simp;
@@ -1628,8 +1646,9 @@
(* add_simprocs *)
fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
- (name, lhs as Cterm {sign, t, ...}, proc, id)) =
- (trace_term ("Adding simplification procedure " ^ name ^ " for:") sign t;
+ (name, lhs as Cterm {sign_ref, t, ...}, proc, id)) =
+ (trace_term ("Adding simplification procedure " ^ name ^ " for:")
+ (Sign.deref sign_ref) t;
mk_mss (rules, congs,
Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
handle Net.INSERT => (trace_warning "ignored duplicate"; procs),
@@ -1690,12 +1709,12 @@
*)
type prover = meta_simpset -> thm -> thm option;
-type termrec = (Sign.sg * term list) * term;
+type termrec = (Sign.sg_ref * term list) * term;
type conv = meta_simpset -> termrec -> termrec;
-fun check_conv (thm as Thm{shyps,hyps,prop,sign,der,maxidx,...}, prop0, ders) =
+fun check_conv (thm as Thm{shyps,hyps,prop,sign_ref,der,maxidx,...}, prop0, ders) =
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm;
- trace_term "Should have proved" sign prop0;
+ trace_term "Should have proved" (Sign.deref sign_ref) prop0;
None)
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
in case prop of
@@ -1722,8 +1741,9 @@
(* mk_procrule *)
-fun mk_procrule (thm as Thm {sign, prop, ...}) =
+fun mk_procrule (thm as Thm {sign_ref, prop, ...}) =
let
+ val sign = Sign.deref sign_ref;
val prems = Logic.strip_imp_prems prop;
val concl = Logic.strip_imp_concl prop;
val (lhs, _) = Logic.dest_equals concl handle TERM _ =>
@@ -1748,15 +1768,17 @@
(4) simplification procedures
*)
-fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, prems, ...})
+fun rewritec (prover,sign_reft) (mss as Mss{rules, procs, mk_rews, termless, prems, ...})
(shypst,hypst,maxt,t,ders) =
let
- val tsigt = #tsig(Sign.rep_sg signt);
- fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
- let val unit = if Sign.subsig(sign,signt) then ()
- else (trace_thm_warning "rewrite rule from different theory"
- thm;
- raise Pattern.MATCH)
+ val signt = Sign.deref sign_reft;
+ val tsigt = Sign.tsig_of signt;
+ fun rew {thm as Thm{sign_ref,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
+ let
+ val _ =
+ if Sign.subsig (Sign.deref sign_ref, signt) then ()
+ else (trace_thm_warning "rewrite rule from different theory" thm;
+ raise Pattern.MATCH);
val rprop = if maxt = ~1 then prop
else Logic.incr_indexes([],maxt+1) prop;
val rlhs = if maxt = ~1 then lhs
@@ -1766,12 +1788,12 @@
val hyps' = union_term(hyps,hypst);
val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
val maxidx' = maxidx_of_term prop'
- val ct' = Cterm{sign = signt, (*used for deriv only*)
+ val ct' = Cterm{sign_ref = sign_reft, (*used for deriv only*)
t = prop',
T = propT,
maxidx = maxidx'}
val der' = infer_derivs (RewriteC ct', [der]);
- val thm' = Thm{sign = signt,
+ val thm' = Thm{sign_ref = sign_reft,
der = der',
shyps = shyps',
hyps = hyps',
@@ -1829,11 +1851,12 @@
(* conversion to apply a congruence rule to a term *)
-fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) =
- let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong
- val unit = if Sign.subsig(sign,signt) then ()
+fun congc (prover,sign_reft) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) =
+ let val signt = Sign.deref sign_reft;
+ val tsig = Sign.tsig_of signt;
+ val Thm{sign_ref,der,shyps,hyps,maxidx,prop,...} = cong
+ val _ = if Sign.subsig(Sign.deref sign_ref,signt) then ()
else error("Congruence rule from different theory")
- val tsig = #tsig(Sign.rep_sg signt)
val rprop = if maxt = ~1 then prop
else Logic.incr_indexes([],maxt+1) prop;
val rlhs = if maxt = ~1 then lhs
@@ -1844,11 +1867,11 @@
val prop' = ren_inst(insts,rprop,rlhs,t);
val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst))
val maxidx' = maxidx_of_term prop'
- val ct' = Cterm{sign = signt, (*used for deriv only*)
+ val ct' = Cterm{sign_ref = sign_reft, (*used for deriv only*)
t = prop',
T = propT,
maxidx = maxidx'}
- val thm' = Thm{sign = signt,
+ val thm' = Thm{sign_ref = sign_reft,
der = infer_derivs (CongC ct', [der]),
shyps = shyps',
hyps = union_term(hyps,hypst),
@@ -1865,15 +1888,15 @@
-fun bottomc ((simprem,useprem),prover,sign) =
+fun bottomc ((simprem,useprem),prover,sign_ref) =
let fun botc fail mss trec =
(case subc mss trec of
some as Some(trec1) =>
- (case rewritec (prover,sign) mss trec1 of
+ (case rewritec (prover,sign_ref) mss trec1 of
Some(trec2) => botc false mss trec2
| None => some)
| None =>
- (case rewritec (prover,sign) mss trec of
+ (case rewritec (prover,sign_ref) mss trec of
Some(trec2) => botc false mss trec2
| None => if fail then None else Some(trec)))
@@ -1926,7 +1949,7 @@
Const(a,_) =>
(case assoc_string(congs,a) of
None => appc()
- | Some(cong) => (congc (prover mss,sign) cong trec
+ | Some(cong) => (congc (prover mss,sign_ref) cong trec
handle Pattern.MATCH => appc() ) )
| _ => appc()
end)
@@ -1941,8 +1964,8 @@
if not useprem then mss else
if maxidx1 <> ~1 then (trace_term_warning
"Cannot add premise as rewrite rule because it contains (type) unknowns:"
- sign s1; mss)
- else let val thm = assume (Cterm{sign=sign, t=s1,
+ (Sign.deref sign_ref) s1; mss)
+ else let val thm = assume (Cterm{sign_ref=sign_ref, t=s1,
T=propT, maxidx=maxidx1})
in add_simps(add_prems(mss,[thm]), mk_rews thm) end
val (shyps2,hyps2,maxidx2,u1,ders2) =
@@ -1968,19 +1991,19 @@
(* FIXME: check that #bounds(mss) does not "occur" in ct alread *)
fun rewrite_cterm mode mss prover ct =
- let val {sign, t, T, maxidx} = rep_cterm ct;
+ let val Cterm {sign_ref, t, T, maxidx} = ct;
val (shyps,hyps,maxu,u,ders) =
- bottomc (mode,prover,sign) mss
+ bottomc (mode,prover, sign_ref) mss
(add_term_sorts(t,[]), [], maxidx, t, []);
val prop = Logic.mk_equals(t,u)
in
- Thm{sign = sign,
+ Thm{sign_ref = sign_ref,
der = infer_derivs (Rewrite_cterm ct, ders),
maxidx = Int.max (maxidx,maxu),
shyps = shyps,
hyps = hyps,
prop = prop}
- end
+ end;
@@ -1997,13 +2020,14 @@
in
fn (sign, exn) =>
let
- val sign' = Sign.merge (sg, sign);
+ val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
+ val sign' = Sign.deref sign_ref';
val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
in
if T <> propT then
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else fix_shyps [] []
- (Thm {sign = sign',
+ (Thm {sign_ref = sign_ref',
der = Join (Oracle (thy, name, sign, exn), []),
maxidx = maxidx,
shyps = [],