src/Pure/theory.ML
author wenzelm
Tue May 12 18:06:01 1998 +0200 (1998-05-12)
changeset 4912 9ac1c22dfe43
parent 4846 9c072489a9e7
child 4970 8b65444edbb0
permissions -rw-r--r--
fixed comment;
     1 (*  Title:      Pure/theory.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4     Copyright   1996  University of Cambridge
     5 
     6 Theories.
     7 *)
     8 
     9 (*this part made pervasive*)
    10 signature BASIC_THEORY =
    11 sig
    12   type theory
    13   type local_theory
    14   exception THEORY of string * theory list
    15   val rep_theory: theory ->
    16     {sign: Sign.sg,
    17       axioms: term Symtab.table,
    18       oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
    19       parents: theory list,
    20       ancestors: theory list}
    21   val sign_of: theory -> Sign.sg
    22   val syn_of: theory -> Syntax.syntax
    23   val parents_of: theory -> theory list
    24   val ancestors_of: theory -> theory list
    25   val subthy: theory * theory -> bool
    26   val eq_thy: theory * theory -> bool
    27   val cert_axm: Sign.sg -> string * term -> string * term
    28   val read_axm: Sign.sg -> string * string -> string * term
    29   val inferT_axm: Sign.sg -> string * term -> string * term
    30   val merge_theories: string -> theory * theory -> theory
    31 end
    32 
    33 signature THEORY =
    34 sig
    35   include BASIC_THEORY
    36   val apply: (theory -> theory) list -> theory -> theory
    37   val axiomK: string
    38   val oracleK: string
    39   (*theory extension primitives*)
    40   val add_classes: (bclass * xclass list) list -> theory -> theory
    41   val add_classes_i: (bclass * class list) list -> theory -> theory
    42   val add_classrel: (xclass * xclass) list -> theory -> theory
    43   val add_classrel_i: (class * class) list -> theory -> theory
    44   val add_defsort: xsort -> theory -> theory
    45   val add_defsort_i: sort -> theory -> theory
    46   val add_types: (bstring * int * mixfix) list -> theory -> theory
    47   val add_nonterminals: bstring list -> theory -> theory
    48   val add_tyabbrs: (bstring * string list * string * mixfix) list
    49     -> theory -> theory
    50   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list
    51     -> theory -> theory
    52   val add_arities: (xstring * xsort list * xsort) list -> theory -> theory
    53   val add_arities_i: (string * sort list * sort) list -> theory -> theory
    54   val add_consts: (bstring * string * mixfix) list -> theory -> theory
    55   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    56   val add_syntax: (bstring * string * mixfix) list -> theory -> theory
    57   val add_syntax_i: (bstring * typ * mixfix) list -> theory -> theory
    58   val add_modesyntax: string * bool -> (bstring * string * mixfix) list -> theory -> theory
    59   val add_modesyntax_i: string * bool -> (bstring * typ * mixfix) list -> theory -> theory
    60   val add_trfuns:
    61     (string * (Syntax.ast list -> Syntax.ast)) list *
    62     (string * (term list -> term)) list *
    63     (string * (term list -> term)) list *
    64     (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
    65   val add_trfunsT:
    66     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    67   val add_tokentrfuns:
    68     (string * string * (string -> string * int)) list -> theory -> theory
    69   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    70   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    71   val add_axioms: (bstring * string) list -> theory -> theory
    72   val add_axioms_i: (bstring * term) list -> theory -> theory
    73   val add_oracle: bstring * (Sign.sg * object -> term) -> theory -> theory
    74   val add_defs: (bstring * string) list -> theory -> theory
    75   val add_defs_i: (bstring * term) list -> theory -> theory
    76   val add_path: string -> theory -> theory
    77   val parent_path: theory -> theory
    78   val root_path: theory -> theory
    79   val add_space: string * string list -> theory -> theory
    80   val add_name: string -> theory -> theory
    81   val init_data: (string * (object * (object -> object) *
    82     (object * object -> object) * (Sign.sg -> object -> unit))) list -> theory -> theory
    83   val get_data: theory -> string -> object
    84   val put_data: string * object -> theory -> theory
    85   val prep_ext: theory -> theory
    86   val prep_ext_merge: theory list -> theory
    87   val require: theory -> string -> string -> unit
    88   val pre_pure: theory
    89 end;
    90 
    91 
    92 structure Theory: THEORY =
    93 struct
    94 
    95 
    96 (** datatype theory **)
    97 
    98 datatype theory =
    99   Theory of {
   100     sign: Sign.sg,
   101     axioms: term Symtab.table,
   102     oracles: ((Sign.sg * object -> term) * stamp) Symtab.table,
   103     parents: theory list,
   104     ancestors: theory list};
   105 
   106 (*forward definition for Isar proof contexts*)
   107 type local_theory = theory * object Symtab.table;
   108 
   109 fun make_thy sign axms oras parents ancestors =
   110   Theory {sign = sign, axioms = axms, oracles = oras,
   111     parents = parents, ancestors = ancestors};
   112 
   113 fun rep_theory (Theory args) = args;
   114 
   115 val sign_of = #sign o rep_theory;
   116 val syn_of = #syn o Sign.rep_sg o sign_of;
   117 val parents_of = #parents o rep_theory;
   118 val ancestors_of = #ancestors o rep_theory;
   119 
   120 (*errors involving theories*)
   121 exception THEORY of string * theory list;
   122 
   123 (*compare theories*)
   124 val subthy = Sign.subsig o pairself sign_of;
   125 val eq_thy = Sign.eq_sg o pairself sign_of;
   126 
   127 (*check for some named theory*)
   128 fun require thy name what =
   129   if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
   130   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   131 
   132 (*partial Pure theory*)
   133 val pre_pure = make_thy Sign.pre_pure Symtab.empty Symtab.empty [] [];
   134 
   135 (*apply transformers*)
   136 fun apply [] thy = thy
   137   | apply (f :: fs) thy = apply fs (f thy);
   138 
   139 
   140 
   141 (** extend theory **)
   142 
   143 (*name space kinds*)
   144 val axiomK = "axiom";
   145 val oracleK = "oracle";
   146 
   147 
   148 (* extend logical part of a theory *)
   149 
   150 fun err_dup_axms names =
   151   error ("Duplicate axiom name(s) " ^ commas_quote names);
   152 
   153 fun err_dup_oras names =
   154   error ("Duplicate oracles " ^ commas_quote names);
   155 
   156 
   157 fun ext_thy thy sign' new_axms new_oras =
   158   let
   159     val Theory {sign, axioms, oracles, parents, ancestors} = thy;
   160     val draft = Sign.is_draft sign;
   161     val axioms' =
   162       Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
   163         handle Symtab.DUPS names => err_dup_axms names;
   164     val oracles' =
   165       Symtab.extend (oracles, new_oras)
   166         handle Symtab.DUPS names => err_dup_oras names;
   167     val (parents', ancestors') =
   168       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   169   in
   170     make_thy sign' axioms' oracles' parents' ancestors'
   171   end;
   172 
   173 
   174 (* extend signature of a theory *)
   175 
   176 fun ext_sg extfun decls (thy as Theory {sign, ...}) =
   177   ext_thy thy (extfun decls sign) [] [];
   178 
   179 val add_classes      = ext_sg Sign.add_classes;
   180 val add_classes_i    = ext_sg Sign.add_classes_i;
   181 val add_classrel     = ext_sg Sign.add_classrel;
   182 val add_classrel_i   = ext_sg Sign.add_classrel_i;
   183 val add_defsort      = ext_sg Sign.add_defsort;
   184 val add_defsort_i    = ext_sg Sign.add_defsort_i;
   185 val add_types        = ext_sg Sign.add_types;
   186 val add_nonterminals = ext_sg Sign.add_nonterminals;
   187 val add_tyabbrs      = ext_sg Sign.add_tyabbrs;
   188 val add_tyabbrs_i    = ext_sg Sign.add_tyabbrs_i;
   189 val add_arities      = ext_sg Sign.add_arities;
   190 val add_arities_i    = ext_sg Sign.add_arities_i;
   191 val add_consts       = ext_sg Sign.add_consts;
   192 val add_consts_i     = ext_sg Sign.add_consts_i;
   193 val add_syntax       = ext_sg Sign.add_syntax;
   194 val add_syntax_i     = ext_sg Sign.add_syntax_i;
   195 val add_modesyntax   = curry (ext_sg Sign.add_modesyntax);
   196 val add_modesyntax_i = curry (ext_sg Sign.add_modesyntax_i);
   197 val add_trfuns       = ext_sg Sign.add_trfuns;
   198 val add_trfunsT      = ext_sg Sign.add_trfunsT;
   199 val add_tokentrfuns  = ext_sg Sign.add_tokentrfuns;
   200 val add_trrules      = ext_sg Sign.add_trrules;
   201 val add_trrules_i    = ext_sg Sign.add_trrules_i;
   202 val add_path         = ext_sg Sign.add_path;
   203 val parent_path      = add_path "..";
   204 val root_path        = add_path "/";
   205 val add_space        = ext_sg Sign.add_space;
   206 val add_name         = ext_sg Sign.add_name;
   207 val prep_ext         = ext_sg (K Sign.prep_ext) ();
   208 
   209 
   210 
   211 (** add axioms **)
   212 
   213 (* prepare axioms *)
   214 
   215 fun err_in_axm name =
   216   error ("The error(s) above occurred in axiom " ^ quote name);
   217 
   218 fun no_vars tm =
   219   if null (term_vars tm) andalso null (term_tvars tm) then tm
   220   else error "Illegal schematic variable(s) in term";
   221 
   222 fun cert_axm sg (name, raw_tm) =
   223   let
   224     val (t, T, _) = Sign.certify_term sg raw_tm
   225       handle TYPE (msg, _, _) => error msg
   226            | TERM (msg, _) => error msg;
   227   in
   228     assert (T = propT) "Term not of type prop";
   229     (name, no_vars t)
   230   end
   231   handle ERROR => err_in_axm name;
   232 
   233 (*Some duplication of code with read_def_cterm*)
   234 fun read_axm sg (name, str) = 
   235   let
   236     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
   237     val (t, _) = Sign.infer_types sg (K None) (K None) [] true (ts, propT);
   238   in cert_axm sg (name,t) end
   239   handle ERROR => err_in_axm name;
   240 
   241 fun inferT_axm sg (name, pre_tm) =
   242   let
   243     val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
   244   in (name, no_vars t) end
   245   handle ERROR => err_in_axm name;
   246 
   247 
   248 (* extend axioms of a theory *)
   249 
   250 fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
   251   let
   252     val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
   253     val axioms =
   254       map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
   255     val sign' = Sign.add_space (axiomK, map fst axioms) sign;
   256   in
   257     ext_thy thy sign' axioms []
   258   end;
   259 
   260 val add_axioms = ext_axms read_axm;
   261 val add_axioms_i = ext_axms cert_axm;
   262 
   263 
   264 (* add oracle **)
   265 
   266 fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
   267   let
   268     val name = Sign.full_name sign raw_name;
   269     val sign' = Sign.add_space (oracleK, [name]) sign;
   270   in
   271     ext_thy thy sign' [] [(name, (oracle, stamp ()))]
   272   end;
   273 
   274 
   275 
   276 (** add constant definitions **)
   277 
   278 (* all_axioms_of *)
   279 
   280 (*results may contain duplicates!*)
   281 
   282 fun all_axioms_of thy =
   283   flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors_of thy));
   284 
   285 
   286 (* clash_types, clash_consts *)
   287 
   288 (*check if types have common instance (ignoring sorts)*)
   289 
   290 fun clash_types ty1 ty2 =
   291   let
   292     val ty1' = Type.varifyT ty1;
   293     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
   294   in
   295     Type.raw_unify (ty1', ty2')
   296   end;
   297 
   298 fun clash_consts (c1, ty1) (c2, ty2) =
   299   c1 = c2 andalso clash_types ty1 ty2;
   300 
   301 
   302 (* clash_defns *)
   303 
   304 fun clash_defn c_ty (name, tm) =
   305   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
   306     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   307   end handle TERM _ => None;
   308 
   309 fun clash_defns c_ty axms =
   310   distinct (mapfilter (clash_defn c_ty) axms);
   311 
   312 
   313 (* dest_defn *)
   314 
   315 fun dest_defn tm =
   316   let
   317     fun err msg = raise TERM (msg, [tm]);
   318 
   319     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   320       handle TERM _ => err "Not a meta-equality (==)";
   321     val (head, args) = strip_comb lhs;
   322     val (c, ty) = dest_Const head
   323       handle TERM _ => err "Head of lhs not a constant";
   324 
   325     fun occs_const (Const c_ty') = (c_ty' = (c, ty))
   326       | occs_const (Abs (_, _, t)) = occs_const t
   327       | occs_const (t $ u) = occs_const t orelse occs_const u
   328       | occs_const _ = false;
   329 
   330     fun dest_free (Free (x, _)) = x
   331       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   332       | dest_free _ = raise Match;
   333 
   334     val show_frees = commas_quote o map dest_free;
   335     val show_tfrees = commas_quote o map fst;
   336 
   337     val lhs_dups = duplicates args;
   338     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   339     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   340   in
   341     if not (forall (can dest_free) args) then
   342       err "Arguments (on lhs) must be variables"
   343     else if not (null lhs_dups) then
   344       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   345     else if not (null rhs_extras) then
   346       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   347     else if not (null rhs_extrasT) then
   348       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   349     else if occs_const rhs then
   350       err ("Constant to be defined occurs on rhs")
   351     else (c, ty)
   352   end;
   353 
   354 
   355 (* check_defn *)
   356 
   357 fun err_in_defn sg name msg =
   358   (writeln msg; error ("The error(s) above occurred in definition " ^
   359     quote (Sign.full_name sg name)));
   360 
   361 fun check_defn sign (axms, (name, tm)) =
   362   let
   363     fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
   364       [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sign ty]));
   365 
   366     fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
   367     fun show_defns c = cat_lines o map (show_defn c);
   368 
   369     val (c, ty) = dest_defn tm
   370       handle TERM (msg, _) => err_in_defn sign name msg;
   371     val defns = clash_defns (c, ty) axms;
   372   in
   373     if not (null defns) then
   374       err_in_defn sign name ("Definition of " ^ show_const (c, ty) ^
   375         "\nclashes with " ^ show_defns c defns)
   376     else (name, tm) :: axms
   377   end;
   378 
   379 
   380 (* add_defs *)
   381 
   382 fun ext_defns prep_axm raw_axms thy =
   383   let
   384     val axms = map (prep_axm (sign_of thy)) raw_axms;
   385     val all_axms = all_axioms_of thy;
   386   in
   387     foldl (check_defn (sign_of thy)) (all_axms, axms);
   388     add_axioms_i axms thy
   389   end;
   390 
   391 val add_defs_i = ext_defns cert_axm;
   392 val add_defs = ext_defns read_axm;
   393 
   394 
   395 
   396 (** additional theory data **)
   397 
   398 fun init_data ds = foldl (op o) (I, map (ext_sg Sign.init_data) ds);
   399 val get_data = Sign.get_data o sign_of;
   400 val put_data = ext_sg Sign.put_data;
   401 
   402 
   403 
   404 (** merge theories **)		(*exception ERROR*)
   405 
   406 fun merge_sign (sg, thy) =
   407   Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
   408 
   409 (*merge list of theories from left to right, preparing extend*)
   410 fun prep_ext_merge thys =
   411   if null thys then
   412     error "Merge: no parent theories"
   413   else if exists (Sign.is_draft o sign_of) thys then
   414     error "Attempt to merge draft theories"
   415   else
   416     let
   417       val sign' =
   418         foldl merge_sign (sign_of (hd thys), tl thys)
   419         |> Sign.prep_ext
   420         |> Sign.add_path "/";
   421 
   422       val axioms' = Symtab.empty;
   423 
   424       fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   425       val oracles' =
   426         Symtab.make (gen_distinct eq_ora
   427           (flat (map (Symtab.dest o #oracles o rep_theory) thys)))
   428         handle Symtab.DUPS names => err_dup_oras names;
   429 
   430       val parents' = gen_distinct eq_thy thys;
   431       val ancestors' =
   432         gen_distinct eq_thy (parents' @ flat (map ancestors_of thys));
   433     in
   434       make_thy sign' axioms' oracles' parents' ancestors'
   435     end;
   436 
   437 fun merge_theories name (thy1, thy2) =
   438   prep_ext_merge [thy1, thy2]
   439   |> add_name name;
   440 
   441 
   442 end;
   443 
   444 structure BasicTheory: BASIC_THEORY = Theory;
   445 open BasicTheory;