back to simple 'defs' (cf. revision 1.79);
authorwenzelm
Thu Sep 29 00:58:59 2005 +0200 (2005-09-29)
changeset 17706e534e39f3531
parent 17705 a5d146aca659
child 17707 bc0270e9d27f
back to simple 'defs' (cf. revision 1.79);
prep_const: Compress.type;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Thu Sep 29 00:58:58 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Thu Sep 29 00:58:59 2005 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    val sign_of: theory -> theory    (*obsolete*)
     1.5    val rep_theory: theory ->
     1.6     {axioms: term NameSpace.table,
     1.7 -    defs: Defs.graph,
     1.8 +    defs: Defs.T,
     1.9      oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}
    1.10    val parents_of: theory -> theory list
    1.11    val ancestors_of: theory -> theory list
    1.12 @@ -38,7 +38,7 @@
    1.13    val oracle_space: theory -> NameSpace.T
    1.14    val axioms_of: theory -> (string * term) list
    1.15    val all_axioms_of: theory -> (string * term) list
    1.16 -  val defs_of : theory -> Defs.graph
    1.17 +  val defs_of : theory -> Defs.T
    1.18    val self_ref: theory -> theory_ref
    1.19    val deref: theory_ref -> theory
    1.20    val merge: theory * theory -> theory                     (*exception TERM*)
    1.21 @@ -95,7 +95,7 @@
    1.22  
    1.23  datatype thy = Thy of
    1.24   {axioms: term NameSpace.table,
    1.25 -  defs: Defs.graph,
    1.26 +  defs: Defs.T,
    1.27    oracles: ((theory * Object.T -> term) * stamp) NameSpace.table};
    1.28  
    1.29  fun make_thy (axioms, defs, oracles) =
    1.30 @@ -119,7 +119,7 @@
    1.31        val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
    1.32  
    1.33        val axioms = NameSpace.empty_table;
    1.34 -      val defs = Defs.merge pp defs1 defs2;
    1.35 +      val defs = Defs.merge pp (defs1, defs2);
    1.36        val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
    1.37          handle Symtab.DUPS dups => err_dup_oras dups;
    1.38      in make_thy (axioms, defs, oracles) end;
    1.39 @@ -224,6 +224,9 @@
    1.40  
    1.41  (** add constant definitions **)
    1.42  
    1.43 +fun prep_const thy (c, T) = (c, Compress.typ thy (Type.varifyT T));
    1.44 +
    1.45 +
    1.46  (* check_overloading *)
    1.47  
    1.48  fun check_overloading thy overloaded (c, T) =
    1.49 @@ -296,17 +299,15 @@
    1.50      fun prt_const (c, T) =
    1.51       [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.52        Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
    1.53 -    fun declared (c, _) = (c, Sign.the_const_type thy c);
    1.54  
    1.55      val _ = no_vars pp tm;
    1.56 +    val name = Sign.full_name thy bname;
    1.57      val (const, rhs) = dest_def pp tm handle TERM (msg, _) => error msg;
    1.58      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    1.59      val _ = check_overloading thy overloaded const;
    1.60    in
    1.61 -    defs
    1.62 -    |> Defs.declare thy (declared const)
    1.63 -    |> fold (Defs.declare thy o declared) rhs_consts
    1.64 -    |> Defs.define thy const (Sign.full_name thy bname) rhs_consts
    1.65 +    defs |> Defs.define (Sign.the_const_type thy)
    1.66 +      name (prep_const thy const) (map (prep_const thy) rhs_consts)
    1.67    end
    1.68    handle ERROR => error (Pretty.string_of (Pretty.block
    1.69     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.70 @@ -336,27 +337,20 @@
    1.71  
    1.72  local
    1.73  
    1.74 -fun gen_add_finals prep_term overloaded raw_terms thy =
    1.75 +fun gen_add_finals prep_term overloaded args thy =
    1.76    let
    1.77 -    val pp = Sign.pp thy;
    1.78 -    fun finalize tm =
    1.79 -      let
    1.80 -        val _ = no_vars pp tm;
    1.81 -        val const as (c, _) =
    1.82 -          (case tm of Const x => x
    1.83 -          | Free _ => error "Attempt to finalize variable (or undeclared constant)"
    1.84 -          | _ => error "Attempt to finalize non-constant term")
    1.85 -          |> check_overloading thy overloaded;
    1.86 -      in Defs.declare thy (c, Sign.the_const_type thy c) #> Defs.finalize thy const end;
    1.87 -  in thy |> map_defs (fold (finalize o prep_term thy) raw_terms) end;
    1.88 -
    1.89 -fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT;
    1.90 -fun cert_term thy = #1 o Sign.certify_term (Sign.pp thy) thy;
    1.91 +    fun const_of (Const const) = const
    1.92 +      | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
    1.93 +      | const_of _ = error "Attempt to finalize non-constant term";
    1.94 +    fun specify (c, T) = Defs.define (Sign.the_const_type thy) (c ^ " axiom") (c, T) [];
    1.95 +    val finalize = specify o check_overloading thy overloaded o
    1.96 +      const_of o no_vars (Sign.pp thy) o prep_term thy;
    1.97 +  in thy |> map_defs (fold finalize args) end;
    1.98  
    1.99  in
   1.100  
   1.101 -val add_finals = gen_add_finals read_term;
   1.102 -val add_finals_i = gen_add_finals cert_term;
   1.103 +val add_finals = gen_add_finals Sign.read_term;
   1.104 +val add_finals_i = gen_add_finals Sign.cert_term;
   1.105  
   1.106  end;
   1.107