src/Pure/theory.ML
author haftmann
Tue Sep 18 07:46:00 2007 +0200 (2007-09-18)
changeset 24626 85eceef2edc7
parent 24199 8be734b5f59f
child 24666 9885a86f14a8
permissions -rw-r--r--
introduced generic concepts for theory interpretators
     1 (*  Title:      Pure/theory.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 
     5 Logical theory content: axioms, definitions, oracles.
     6 *)
     7 
     8 signature BASIC_THEORY =
     9 sig
    10   val eq_thy: theory * theory -> bool
    11   val subthy: theory * theory -> bool
    12 end
    13 
    14 signature THEORY =
    15 sig
    16   include BASIC_THEORY
    17   include SIGN_THEORY
    18   val parents_of: theory -> theory list
    19   val ancestors_of: theory -> theory list
    20   val begin_theory: string -> theory list -> theory
    21   val end_theory: theory -> theory
    22   val checkpoint: theory -> theory
    23   val copy: theory -> theory
    24   val rep_theory: theory ->
    25    {axioms: term NameSpace.table,
    26     defs: Defs.T,
    27     oracles: ((theory * Object.T -> term) * stamp) NameSpace.table}
    28   val axiom_space: theory -> NameSpace.T
    29   val axiom_table: theory -> term Symtab.table
    30   val oracle_space: theory -> NameSpace.T
    31   val oracle_table: theory -> ((theory * Object.T -> term) * stamp) Symtab.table
    32   val axioms_of: theory -> (string * term) list
    33   val all_axioms_of: theory -> (string * term) list
    34   val defs_of : theory -> Defs.T
    35   val check_thy: theory -> theory_ref
    36   val deref: theory_ref -> theory
    37   val merge: theory * theory -> theory
    38   val merge_refs: theory_ref * theory_ref -> theory_ref
    39   val merge_list: theory list -> theory
    40   val requires: theory -> string -> string -> unit
    41   val assert_super: theory -> theory -> theory
    42   val cert_axm: theory -> string * term -> string * term
    43   val read_axm: theory -> string * string -> string * term
    44   val add_axioms: (bstring * string) list -> theory -> theory
    45   val add_axioms_i: (bstring * term) list -> theory -> theory
    46   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    47   val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
    48   val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
    49   val add_finals: bool -> string list -> theory -> theory
    50   val add_finals_i: bool -> term list -> theory -> theory
    51   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    52 end
    53 
    54 signature THEORY_INTERPRETATOR =
    55 sig
    56   type T
    57   type interpretator = T list -> theory -> theory
    58   val add_those: T list -> theory -> theory
    59   val all_those: theory -> T list
    60   val add_interpretator: interpretator -> theory -> theory
    61   val init: theory -> theory
    62 end;
    63 
    64 signature THEORY_INTERPRETATOR_KEY =
    65 sig
    66   type T
    67   val eq: T * T -> bool
    68 end;
    69 
    70 structure Theory =
    71 struct
    72 
    73 
    74 (** datatype thy **)
    75 
    76 datatype thy = Thy of
    77  {axioms: term NameSpace.table,
    78   defs: Defs.T,
    79   oracles: ((theory * Object.T -> term) * stamp) NameSpace.table,
    80   consolidate: theory -> theory};
    81 
    82 fun make_thy (axioms, defs, oracles, consolidate) =
    83   Thy {axioms = axioms, defs = defs, oracles = oracles, consolidate = consolidate};
    84 
    85 fun err_dup_axm dup = error ("Duplicate axiom: " ^ quote dup);
    86 fun err_dup_ora dup = error ("Duplicate oracle: " ^ quote dup);
    87 
    88 structure ThyData = TheoryDataFun
    89 (
    90   type T = thy;
    91   val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table, I);
    92   val copy = I;
    93 
    94   fun extend (Thy {axioms, defs, oracles, consolidate}) =
    95     make_thy (NameSpace.empty_table, defs, oracles, consolidate);
    96 
    97   fun merge pp (thy1, thy2) =
    98     let
    99       val Thy {axioms = _, defs = defs1, oracles = oracles1,
   100         consolidate = consolidate1} = thy1;
   101       val Thy {axioms = _, defs = defs2, oracles = oracles2,
   102         consolidate = consolidate2} = thy2;
   103 
   104       val axioms = NameSpace.empty_table;
   105       val defs = Defs.merge pp (defs1, defs2);
   106       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   107         handle Symtab.DUP dup => err_dup_ora dup;
   108       val consolidate = consolidate1 #> consolidate2;
   109     in make_thy (axioms, defs, oracles, consolidate) end;
   110 );
   111 
   112 fun rep_theory thy = ThyData.get thy |> (fn Thy {axioms, defs, oracles, ...} =>
   113   {axioms = axioms, defs = defs, oracles = oracles});
   114 
   115 fun map_thy f = ThyData.map (fn (Thy {axioms, defs, oracles, consolidate}) =>
   116   make_thy (f (axioms, defs, oracles, consolidate)));
   117 
   118 fun map_axioms f = map_thy
   119   (fn (axioms, defs, oracles, consolidate) => (f axioms, defs, oracles, consolidate));
   120 fun map_defs f = map_thy
   121   (fn (axioms, defs, oracles, consolidate) => (axioms, f defs, oracles, consolidate));
   122 fun map_oracles f = map_thy
   123   (fn (axioms, defs, oracles, consolidate) => (axioms, defs, f oracles, consolidate));
   124 
   125 
   126 (* basic operations *)
   127 
   128 val axiom_space = #1 o #axioms o rep_theory;
   129 val axiom_table = #2 o #axioms o rep_theory;
   130 
   131 val oracle_space = #1 o #oracles o rep_theory;
   132 val oracle_table = #2 o #oracles o rep_theory;
   133 
   134 val axioms_of = Symtab.dest o #2 o #axioms o rep_theory;
   135 
   136 val defs_of = #defs o rep_theory;
   137 
   138 fun requires thy name what =
   139   if Context.exists_name name thy then ()
   140   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   141 
   142 
   143 (* interpretators *)
   144 
   145 fun add_consolidate f = map_thy
   146   (fn (axioms, defs, oracles, consolidate) => (axioms, defs, oracles, consolidate #> f));
   147 
   148 fun consolidate thy =
   149   let
   150     val Thy {consolidate, ...} = ThyData.get thy;
   151   in
   152     thy |> consolidate
   153   end;
   154 
   155 
   156 (** type theory **)
   157 
   158 (* context operations *)
   159 
   160 val eq_thy = Context.eq_thy;
   161 val subthy = Context.subthy;
   162 
   163 fun assert_super thy1 thy2 =
   164   if subthy (thy1, thy2) then thy2
   165   else raise THEORY ("Not a super theory", [thy1, thy2]);
   166 
   167 val parents_of = Context.parents_of;
   168 val ancestors_of = Context.ancestors_of;
   169 
   170 val check_thy = Context.check_thy;
   171 val deref = Context.deref;
   172 val merge = Context.merge;
   173 val merge_refs = Context.merge_refs;
   174 
   175 fun merge_list [] = raise THEORY ("Empty merge of theories", [])
   176   | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
   177 
   178 val begin_theory = Sign.local_path o consolidate oo Context.begin_thy Sign.pp;
   179 val end_theory = Context.finish_thy;
   180 val checkpoint = Context.checkpoint_thy;
   181 val copy = Context.copy_thy;
   182 
   183 
   184 (* signature operations *)
   185 
   186 structure SignTheory: SIGN_THEORY = Sign;
   187 open SignTheory;
   188 
   189 
   190 
   191 (** axioms **)
   192 
   193 fun all_axioms_of thy = maps axioms_of (thy :: ancestors_of thy);
   194 
   195 
   196 (* prepare axioms *)
   197 
   198 fun err_in_axm msg name =
   199   cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
   200 
   201 fun cert_axm thy (name, raw_tm) =
   202   let
   203     val (t, T, _) = Sign.certify_prop thy raw_tm
   204       handle TYPE (msg, _, _) => error msg
   205         | TERM (msg, _) => error msg;
   206   in
   207     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   208     (name, Sign.no_vars (Sign.pp thy) t)
   209   end;
   210 
   211 fun read_axm thy (name, str) =
   212   cert_axm thy (name, Sign.read_prop thy str)
   213     handle ERROR msg => err_in_axm msg name;
   214 
   215 
   216 (* add_axioms(_i) *)
   217 
   218 local
   219 
   220 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   221   let
   222     val axms = map (apsnd (Compress.term thy o Logic.varify) o prep_axm thy) raw_axms;
   223     val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
   224       handle Symtab.DUP dup => err_dup_axm dup;
   225   in axioms' end);
   226 
   227 in
   228 
   229 val add_axioms = gen_add_axioms read_axm;
   230 val add_axioms_i = gen_add_axioms cert_axm;
   231 
   232 end;
   233 
   234 
   235 
   236 (** add constant definitions **)
   237 
   238 (* dependencies *)
   239 
   240 fun dependencies thy unchecked is_def name lhs rhs =
   241   let
   242     val pp = Sign.pp thy;
   243     val consts = Sign.consts_of thy;
   244     fun prep const =
   245       let val Const (c, T) = Sign.no_vars pp (Const const)
   246       in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
   247 
   248     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
   249     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
   250       if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
   251     val _ =
   252       if null rhs_extras then ()
   253       else error ("Specification depends on extra type variables: " ^
   254         commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
   255         "\nThe error(s) above occurred in " ^ quote name);
   256   in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end;
   257 
   258 fun add_deps a raw_lhs raw_rhs thy =
   259   let
   260     val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
   261     val name = if a = "" then (#1 lhs ^ " axiom") else a;
   262   in thy |> map_defs (dependencies thy false false name lhs rhs) end;
   263 
   264 
   265 (* check_overloading *)
   266 
   267 fun check_overloading thy overloaded (c, T) =
   268   let
   269     val declT =
   270       (case Sign.const_constraint thy c of
   271         NONE => error ("Undeclared constant " ^ quote c)
   272       | SOME declT => declT);
   273     val T' = Logic.varifyT T;
   274 
   275     fun message txt =
   276       [Pretty.block [Pretty.str "Specification of constant ",
   277         Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)],
   278         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   279   in
   280     if Sign.typ_instance thy (declT, T') then ()
   281     else if Type.raw_instance (declT, T') then
   282       error (Library.setmp show_sorts true
   283         message "imposes additional sort constraints on the constant declaration")
   284     else if overloaded then ()
   285     else warning (message "is strictly less general than the declared type");
   286     (c, T)
   287   end;
   288 
   289 
   290 (* check_def *)
   291 
   292 fun check_def thy unchecked overloaded (bname, tm) defs =
   293   let
   294     val name = Sign.full_name thy bname;
   295     val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
   296     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   297     val _ = check_overloading thy overloaded lhs_const;
   298   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   299   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   300    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   301     Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
   302 
   303 
   304 (* add_defs(_i) *)
   305 
   306 local
   307 
   308 fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
   309   let val axms = map (prep_axm thy) raw_axms in
   310     thy
   311     |> map_defs (fold (check_def thy unchecked overloaded) axms)
   312     |> add_axioms_i axms
   313   end;
   314 
   315 in
   316 
   317 val add_defs_i = gen_add_defs cert_axm;
   318 val add_defs = gen_add_defs read_axm;
   319 
   320 end;
   321 
   322 
   323 (* add_finals(_i) *)
   324 
   325 local
   326 
   327 fun gen_add_finals prep_term overloaded args thy =
   328   let
   329     fun const_of (Const const) = const
   330       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
   331       | const_of _ = error "Attempt to finalize non-constant term";
   332     fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) [];
   333     val finalize = specify o check_overloading thy overloaded o const_of o prep_term thy;
   334   in thy |> map_defs (fold finalize args) end;
   335 
   336 in
   337 
   338 val add_finals = gen_add_finals Sign.read_term;
   339 val add_finals_i = gen_add_finals Sign.cert_term;
   340 
   341 end;
   342 
   343 
   344 
   345 (** add oracle **)
   346 
   347 fun add_oracle (bname, oracle) thy = thy |> map_oracles (fn oracles =>
   348   NameSpace.extend_table (Sign.naming_of thy) [(bname, (oracle, stamp ()))] oracles
   349     handle Symtab.DUP dup => err_dup_ora dup);
   350 
   351 end;
   352 
   353 functor TheoryInterpretatorFun(Key: THEORY_INTERPRETATOR_KEY) : THEORY_INTERPRETATOR =
   354 struct
   355 
   356 open Key;
   357 
   358 type interpretator = T list -> theory -> theory;
   359 
   360 fun apply ips x = fold_rev (fn (_, f) => f x) ips;
   361 
   362 structure InterpretatorData = TheoryDataFun (
   363   type T = ((serial * interpretator) list * T list) * (theory -> theory);
   364   val empty = (([], []), I);
   365   val extend = I;
   366   val copy = I;
   367   fun merge pp (((interpretators1, done1), upd1), ((interpretators2, done2), upd2)) =
   368     let
   369       fun diff (interpretators1 : (serial * interpretator) list, done1)
   370         (interpretators2, done2) = let
   371           val interpretators = subtract (eq_fst (op =)) interpretators1 interpretators2;
   372           val undone = subtract eq done2 done1;
   373         in apply interpretators undone end;
   374       val interpretators = AList.merge (op =) (K true) (interpretators1, interpretators2);
   375       val done = Library.merge eq (done1, done2);
   376       val upd_new = diff (interpretators2, done2) (interpretators1, done1)
   377         #> diff (interpretators1, done1) (interpretators2, done2);
   378       val upd = upd1 #> upd2 #> upd_new;
   379     in ((interpretators, done), upd) end;
   380 );
   381 
   382 fun consolidate thy =
   383   let
   384     val (_, upd) = InterpretatorData.get thy;
   385   in
   386     thy |> upd |> (InterpretatorData.map o apsnd) (K I)
   387   end;
   388 
   389 val init = Theory.add_consolidate consolidate;
   390 
   391 fun add_those xs thy =
   392   let
   393     val ((interpretators, _), _) = InterpretatorData.get thy;
   394   in
   395     thy
   396     |> apply interpretators xs
   397     |> (InterpretatorData.map o apfst o apsnd) (append xs)
   398   end;
   399 
   400 val all_those = snd o fst o InterpretatorData.get;
   401 
   402 fun add_interpretator interpretator thy =
   403   let
   404     val ((interpretators, xs), _) = InterpretatorData.get thy;
   405   in
   406     thy
   407     |> interpretator (rev xs)
   408     |> (InterpretatorData.map o apfst o apfst) (cons (serial (), interpretator))
   409   end;
   410 
   411 end;
   412 
   413 structure Theory: THEORY = Theory;
   414 structure BasicTheory: BASIC_THEORY = Theory;
   415 open BasicTheory;