--- a/src/Pure/theory.ML Wed Oct 08 16:02:54 2003 +0200
+++ b/src/Pure/theory.ML Thu Oct 09 18:13:32 2003 +0200
@@ -13,6 +13,7 @@
val rep_theory: theory ->
{sign: Sign.sg,
const_deps: unit Graph.T,
+ final_consts: typ list Symtab.table,
axioms: term Symtab.table,
oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
parents: theory list,
@@ -73,6 +74,8 @@
val add_axioms: (bstring * string) list -> theory -> theory
val add_axioms_i: (bstring * term) list -> theory -> theory
val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
+ val add_finals: bool -> string list -> theory -> theory
+ val add_finals_i: bool -> term list -> theory -> theory
val add_defs: bool -> (bstring * string) list -> theory -> theory
val add_defs_i: bool -> (bstring * term) list -> theory -> theory
val add_path: string -> theory -> theory
@@ -116,14 +119,15 @@
Theory of {
sign: Sign.sg,
const_deps: unit Graph.T,
+ final_consts: typ list Symtab.table,
axioms: term Symtab.table,
oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
parents: theory list,
ancestors: theory list};
-fun make_theory sign const_deps axioms oracles parents ancestors =
- Theory {sign = sign, const_deps = const_deps, axioms = axioms, oracles = oracles,
- parents = parents, ancestors = ancestors};
+fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
+ Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
+ oracles = oracles, parents = parents, ancestors = ancestors};
fun rep_theory (Theory args) = args;
@@ -151,7 +155,7 @@
(*partial Pure theory*)
val pre_pure =
- make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty [] [];
+ make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty Symtab.empty [] [];
@@ -172,7 +176,7 @@
fun ext_theory thy ext_sg ext_deps new_axms new_oras =
let
- val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
+ val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
val draft = Sign.is_draft sign;
val axioms' =
Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
@@ -183,7 +187,7 @@
val (parents', ancestors') =
if draft then (parents, ancestors) else ([thy], thy :: ancestors);
in
- make_theory (ext_sg sign) (ext_deps const_deps) axioms' oracles' parents' ancestors'
+ make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
end;
@@ -386,9 +390,14 @@
let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
in foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
+fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
+ let
+ fun is_final (c, ty) =
+ case Symtab.lookup(final_consts,c) of
+ Some [] => true
+ | Some tys => exists (curry (Sign.typ_instance sg) ty) tys
+ | None => false;
-fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
- let
fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
@@ -410,6 +419,11 @@
if not (null clashed) then
err_in_defn sg name (Pretty.string_of (Pretty.chunks
(def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
+ else if is_final c_ty then
+ err_in_defn sg name (Pretty.string_of (Pretty.block
+ ([Pretty.str "The constant",Pretty.brk 1] @
+ pretty_const c_ty @
+ [Pretty.brk 1,Pretty.str "has been declared final"])))
else
(case overloading sg c_decl ty of
NoOverloading =>
@@ -432,13 +446,13 @@
fun ext_defns prep_axm overloaded raw_axms thy =
let
- val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
+ val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
val axms = map (prep_axm sign) raw_axms;
- val (const_deps', _) = foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
+ val (const_deps', _) = foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
in
- make_theory sign const_deps' axioms oracles parents ancestors
+ make_theory sign const_deps' final_consts axioms oracles parents ancestors
|> add_axioms_i axms
end;
@@ -446,6 +460,66 @@
val add_defs = ext_defns read_axm;
+(* add_finals *)
+
+fun ext_finals prep_term overloaded raw_terms thy =
+ let
+ val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
+ fun mk_final (finals,tm) =
+ let
+ fun err msg = raise TERM(msg,[tm]);
+ val (c,ty) = dest_Const tm
+ handle TERM _ => err "Can only make constants final";
+ val c_decl =
+ (case Sign.const_type sign c of Some T => T
+ | None => err ("Undeclared constant " ^ quote c));
+ val simple =
+ case overloading sign c_decl ty of
+ NoOverloading => true
+ | Useless => err "Sort restrictions too strong"
+ | Plain => if overloaded then false
+ else err "Type is more general than declared";
+ val typ_instance = Sign.typ_instance sign;
+ in
+ if simple then
+ (case Symtab.lookup(finals,c) of
+ Some [] => err "Constant already final"
+ | _ => Symtab.update((c,[]),finals))
+ else
+ (case Symtab.lookup(finals,c) of
+ Some [] => err "Constant already completely final"
+ | Some tys => if exists (curry typ_instance ty) tys
+ then err "Instance of constant is already final"
+ else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
+ | None => Symtab.update((c,[ty]),finals))
+ end;
+ val consts = map (prep_term sign) raw_terms;
+ val final_consts' = foldl mk_final (final_consts,consts);
+ in
+ make_theory sign const_deps final_consts' axioms oracles parents ancestors
+ end;
+
+local
+ fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
+ val cert_term = #1 oo Sign.certify_term;
+in
+val add_finals = ext_finals read_term;
+val add_finals_i = ext_finals cert_term;
+end;
+
+fun merge_final sg =
+ let
+ fun merge_single (tys,ty) =
+ if exists (curry (Sign.typ_instance sg) ty) tys
+ then tys
+ else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
+ fun merge ([],_) = []
+ | merge (_,[]) = []
+ | merge input = foldl merge_single input;
+ in
+ Some o merge
+ end;
+
(** additional theory data **)
@@ -478,6 +552,9 @@
val deps' = foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
handle Graph.CYCLES namess => error (cycle_msg namess);
+ val final_constss = map (#final_consts o rep_theory) thys;
+ val final_consts' = foldl (Symtab.join (merge_final sign')) (hd final_constss,
+ tl final_constss);
val axioms' = Symtab.empty;
fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
@@ -490,7 +567,7 @@
val ancestors' =
gen_distinct eq_thy (parents' @ flat (map ancestors_of thys));
in
- make_theory sign' deps' axioms' oracles' parents' ancestors'
+ make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
end;