src/Pure/theory.ML
changeset 16158 2c3565b74b7a
parent 16134 89ea482e1649
child 16190 8382835019d1
     1.1 --- a/src/Pure/theory.ML	Tue May 31 17:52:10 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue May 31 19:32:41 2005 +0200
     1.3 @@ -4,7 +4,6 @@
     1.4  
     1.5  The abstract type "theory" of theories.
     1.6  *)
     1.7 -
     1.8  signature BASIC_THEORY =
     1.9  sig
    1.10    type theory
    1.11 @@ -12,7 +11,6 @@
    1.12    val rep_theory: theory ->
    1.13      {sign: Sign.sg,
    1.14        const_deps: Defs.graph,
    1.15 -      final_consts: typ list Symtab.table,
    1.16        axioms: term Symtab.table,
    1.17        oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    1.18        parents: theory list,
    1.19 @@ -131,14 +129,13 @@
    1.20    Theory of {
    1.21      sign: Sign.sg,
    1.22      const_deps: Defs.graph,
    1.23 -    final_consts: typ list Symtab.table,
    1.24      axioms: term Symtab.table,
    1.25      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    1.26      parents: theory list,
    1.27      ancestors: theory list};
    1.28  
    1.29 -fun make_theory sign const_deps final_consts axioms oracles parents ancestors =
    1.30 -  Theory {sign = sign, const_deps = const_deps, final_consts = final_consts, axioms = axioms,
    1.31 +fun make_theory sign const_deps axioms oracles parents ancestors =
    1.32 +  Theory {sign = sign, const_deps = const_deps, axioms = axioms,
    1.33      oracles = oracles,  parents = parents, ancestors = ancestors};
    1.34  
    1.35  fun rep_theory (Theory args) = args;
    1.36 @@ -167,7 +164,7 @@
    1.37  
    1.38  (*partial Pure theory*)
    1.39  val pre_pure =
    1.40 -  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty Symtab.empty [] [];
    1.41 +  make_theory Sign.pre_pure Defs.empty Symtab.empty Symtab.empty [] [];
    1.42  
    1.43  
    1.44  
    1.45 @@ -186,9 +183,9 @@
    1.46  fun err_dup_oras names =
    1.47    error ("Duplicate oracles: " ^ commas_quote names);
    1.48  
    1.49 -fun ext_theory thy ext_sg ext_deps new_axms new_oras =
    1.50 +fun ext_theory thy ext_sg new_axms new_oras =
    1.51    let
    1.52 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
    1.53 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
    1.54      val draft = Sign.is_draft sign;
    1.55      val axioms' =
    1.56        Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
    1.57 @@ -199,13 +196,13 @@
    1.58      val (parents', ancestors') =
    1.59        if draft then (parents, ancestors) else ([thy], thy :: ancestors);
    1.60    in
    1.61 -    make_theory (ext_sg sign) (ext_deps const_deps) final_consts axioms' oracles' parents' ancestors'
    1.62 +    make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
    1.63    end;
    1.64  
    1.65  
    1.66  (* extend signature of a theory *)
    1.67  
    1.68 -fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) I [] [];
    1.69 +fun ext_sign ext_sg args thy = ext_theory thy (ext_sg args) [] [];
    1.70  
    1.71  val add_classes            = ext_sign Sign.add_classes;
    1.72  val add_classes_i          = ext_sign Sign.add_classes_i;
    1.73 @@ -306,7 +303,7 @@
    1.74      val axioms =
    1.75        map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
    1.76      val ext_sg = Sign.add_space (axiomK, map fst axioms);
    1.77 -  in ext_theory thy ext_sg I axioms [] end;
    1.78 +  in ext_theory thy ext_sg axioms [] end;
    1.79  
    1.80  val add_axioms = ext_axms read_axm;
    1.81  val add_axioms_i = ext_axms cert_axm;
    1.82 @@ -318,7 +315,7 @@
    1.83    let
    1.84      val name = Sign.full_name sign raw_name;
    1.85      val ext_sg = Sign.add_space (oracleK, [name]);
    1.86 -  in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end;
    1.87 +  in ext_theory thy ext_sg [] [(name, (oracle, stamp ()))] end;
    1.88  
    1.89  
    1.90  
    1.91 @@ -421,17 +418,11 @@
    1.92  	end))))
    1.93    end
    1.94  
    1.95 -fun check_defn sg overloaded final_consts ((deps, axms), def as (name, tm)) =
    1.96 +fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
    1.97    let
    1.98      
    1.99      val name = Sign.full_name sg name
   1.100        
   1.101 -    fun is_final (c, ty) =
   1.102 -      case Symtab.lookup(final_consts,c) of
   1.103 -        SOME [] => true
   1.104 -      | SOME tys => exists (curry (Sign.typ_instance sg) ty) tys
   1.105 -      | NONE => false;
   1.106 -
   1.107      fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   1.108        Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   1.109  
   1.110 @@ -446,9 +437,9 @@
   1.111        handle TERM (msg, _) => err_in_defn sg name msg;
   1.112  
   1.113      fun decl deps c = 
   1.114 -        (case Sign.const_type sg c of 
   1.115 -             SOME T => (Defs.declare deps c T handle _ => deps, T)
   1.116 -           | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   1.117 +	(case Sign.const_type sg c of 
   1.118 +	     SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
   1.119 +	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   1.120  
   1.121      val (deps, c_decl) = decl deps c
   1.122  
   1.123 @@ -456,12 +447,6 @@
   1.124      val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
   1.125  
   1.126    in
   1.127 -    if is_final c_ty then
   1.128 -      err_in_defn sg name (Pretty.string_of (Pretty.block
   1.129 -        ([Pretty.str "The constant",Pretty.brk 1] @
   1.130 -         pretty_const c_ty @
   1.131 -         [Pretty.brk 1,Pretty.str "has been declared final"])))
   1.132 -    else
   1.133        (case overloading sg c_decl ty of
   1.134           Useless =>
   1.135             err_in_defn sg name (Pretty.string_of (Pretty.chunks
   1.136 @@ -469,19 +454,24 @@
   1.137                "imposes additional sort constraints on the declared type of the constant"]))   
   1.138         | ov =>
   1.139  	 let 
   1.140 -	     val deps' = Defs.define deps c ty name body
   1.141 +	     val deps' = Defs.define deps c_ty name body
   1.142  		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
   1.143  		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
   1.144                        | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
   1.145                        | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
   1.146 -                          "clashing definitions "^ quote def1 ^" and "^ quote def2)
   1.147 -         in
   1.148 -             ((if ov = Plain andalso not overloaded then
   1.149 -                   warning (Pretty.string_of (Pretty.chunks
   1.150 -                     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   1.151 -               else
   1.152 -                   ()); (deps', def::axms))
   1.153 -         end)
   1.154 +			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
   1.155 +		      | Defs.FINAL cfinal =>
   1.156 +			err_in_defn sg name (Pretty.string_of (Pretty.block
   1.157 +			  ([Pretty.str "The constant",Pretty.brk 1] @
   1.158 +			   pretty_const cfinal @
   1.159 +			   [Pretty.brk 1,Pretty.str "has been declared final"]))) 
   1.160 +	 in
   1.161 +	     ((if ov = Plain andalso not overloaded then
   1.162 +		   warning (Pretty.string_of (Pretty.chunks
   1.163 +		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   1.164 +	       else
   1.165 +		   ()); (deps', def::axms))
   1.166 +	 end)
   1.167    end;
   1.168  
   1.169  
   1.170 @@ -489,13 +479,13 @@
   1.171  
   1.172  fun ext_defns prep_axm overloaded raw_axms thy =
   1.173    let
   1.174 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   1.175 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   1.176      val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
   1.177  
   1.178      val axms = map (prep_axm sign) raw_axms;
   1.179 -    val (const_deps', _) = Library.foldl (check_defn sign overloaded final_consts) ((const_deps, all_axioms), axms);
   1.180 +    val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
   1.181    in
   1.182 -    make_theory sign const_deps' final_consts axioms oracles parents ancestors
   1.183 +    make_theory sign const_deps' axioms oracles parents ancestors
   1.184      |> add_axioms_i axms
   1.185    end;
   1.186  
   1.187 @@ -507,39 +497,29 @@
   1.188  
   1.189  fun ext_finals prep_term overloaded raw_terms thy =
   1.190    let
   1.191 -    val Theory {sign, const_deps, final_consts, axioms, oracles, parents, ancestors} = thy;
   1.192 -    fun mk_final (finals,tm) =
   1.193 -      let
   1.194 -        fun err msg = raise TERM(msg,[tm]);
   1.195 -        val (c,ty) = dest_Const tm
   1.196 -          handle TERM _ => err "Can only make constants final";
   1.197 -        val c_decl =
   1.198 -          (case Sign.const_type sign c of SOME T => T
   1.199 -          | NONE => err ("Undeclared constant " ^ quote c));
   1.200 -        val simple =
   1.201 -          case overloading sign c_decl ty of
   1.202 -            NoOverloading => true
   1.203 -          | Useless => err "Sort restrictions too strong"
   1.204 -          | Plain => if overloaded then false
   1.205 -                     else err "Type is more general than declared";
   1.206 -        val typ_instance = Sign.typ_instance sign;
   1.207 -      in
   1.208 -        if simple then
   1.209 -          (case Symtab.lookup(finals,c) of
   1.210 -            SOME [] => err "Constant already final"
   1.211 -          | _ => Symtab.update((c,[]),finals))
   1.212 -        else
   1.213 -          (case Symtab.lookup(finals,c) of
   1.214 -            SOME [] => err "Constant already completely final"
   1.215 -          | SOME tys => if exists (curry typ_instance ty) tys
   1.216 -                        then err "Instance of constant is already final"
   1.217 -                        else Symtab.update((c,ty::gen_rem typ_instance (tys,ty)),finals)
   1.218 -          | NONE => Symtab.update((c,[ty]),finals))
   1.219 -      end;
   1.220 +    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   1.221 +    fun mk_final (tm, finals) =
   1.222 +	let
   1.223 +            fun err msg = raise TERM(msg,[tm])
   1.224 +            val (c,ty) = dest_Const tm
   1.225 +		handle TERM _ => err "Can only make constants final"
   1.226 +            val c_decl =
   1.227 +		(case Sign.const_type sign c of 
   1.228 +		     SOME T => T
   1.229 +		   | NONE => err ("Undeclared constant " ^ quote c))
   1.230 +	    val _ =
   1.231 +		case overloading sign c_decl ty of
   1.232 +		    NoOverloading => ()
   1.233 +		  | Useless => err "Sort restrictions too strong"
   1.234 +		  | Plain => (if overloaded then () else warning "Type is more general than declared")
   1.235 +	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
   1.236 +	in
   1.237 +	    Defs.finalize finals (c,ty)
   1.238 +	end
   1.239      val consts = map (prep_term sign) raw_terms;
   1.240 -    val final_consts' = Library.foldl mk_final (final_consts,consts);
   1.241 +    val const_deps' = foldl mk_final const_deps consts;
   1.242    in
   1.243 -    make_theory sign const_deps final_consts' axioms oracles parents ancestors
   1.244 +    make_theory sign const_deps' axioms oracles parents ancestors
   1.245    end;
   1.246  
   1.247  local
   1.248 @@ -585,9 +565,6 @@
   1.249        handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
   1.250  	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
   1.251  
   1.252 -    val final_constss = map (#final_consts o rep_theory) thys;
   1.253 -    val final_consts' =
   1.254 -      Library.foldl (Symtab.join (merge_final sign')) (hd final_constss, tl final_constss);
   1.255      val axioms' = Symtab.empty;
   1.256  
   1.257      fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   1.258 @@ -600,7 +577,7 @@
   1.259      val ancestors' =
   1.260        gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   1.261    in
   1.262 -    make_theory sign' deps' final_consts' axioms' oracles' parents' ancestors'
   1.263 +    make_theory sign' deps' axioms' oracles' parents' ancestors'
   1.264    end;
   1.265  
   1.266