src/Pure/theory.ML
author wenzelm
Sat Nov 18 19:48:07 2000 +0100 (2000-11-18 ago)
changeset 10494 305b37c8d8a3
parent 10403 2955ee2424ce
child 10930 7c7a7b0e1d0c
permissions -rw-r--r--
improved messages;
     1 (*  Title:      Pure/theory.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4     Copyright   1996  University of Cambridge
     5 
     6 The abstract type "theory" of theories.
     7 *)
     8 
     9 signature BASIC_THEORY =
    10 sig
    11   type theory
    12   exception THEORY of string * theory list
    13   val rep_theory: theory ->
    14     {sign: Sign.sg,
    15       const_deps: unit Graph.T,
    16       axioms: term Symtab.table,
    17       oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    18       parents: theory list,
    19       ancestors: theory list}
    20   val sign_of: theory -> Sign.sg
    21   val is_draft: theory -> bool
    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_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    29     string list -> string * string -> string * term
    30   val read_axm: Sign.sg -> string * string -> string * term
    31   val inferT_axm: Sign.sg -> string * term -> string * term
    32 end
    33 
    34 signature THEORY =
    35 sig
    36   include BASIC_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: string -> 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 * string list * string) 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 * real)) list -> theory -> theory
    69   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    70     -> theory -> theory
    71   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    72   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    73   val add_axioms: (bstring * string) list -> theory -> theory
    74   val add_axioms_i: (bstring * term) list -> theory -> theory
    75   val add_oracle: bstring * (Sign.sg * Object.T -> term) -> theory -> theory
    76   val add_defs: bool -> (bstring * string) list -> theory -> theory
    77   val add_defs_i: bool -> (bstring * term) list -> theory -> theory
    78   val add_path: string -> theory -> theory
    79   val parent_path: theory -> theory
    80   val root_path: theory -> theory
    81   val hide_space: string * xstring list -> theory -> theory
    82   val hide_space_i: string * string list -> theory -> theory
    83   val hide_classes: string list -> theory -> theory
    84   val hide_types: string list -> theory -> theory
    85   val hide_consts: string list -> theory -> theory
    86   val add_name: string -> theory -> theory
    87   val copy: theory -> theory
    88   val prep_ext: theory -> theory
    89   val prep_ext_merge: theory list -> theory
    90   val requires: theory -> string -> string -> unit
    91   val assert_super: theory -> theory -> theory
    92   val pre_pure: theory
    93 end;
    94 
    95 signature PRIVATE_THEORY =
    96 sig
    97   include THEORY
    98   val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
    99     (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> theory -> theory
   100   val print_data: Object.kind -> theory -> unit
   101   val get_data: Object.kind -> (Object.T -> 'a) -> theory -> 'a
   102   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
   103 end;
   104 
   105 
   106 structure Theory: PRIVATE_THEORY =
   107 struct
   108 
   109 
   110 (** datatype theory **)
   111 
   112 (*Note: dependencies are only tracked for non-overloaded constant definitions*)
   113 
   114 datatype theory =
   115   Theory of {
   116     sign: Sign.sg,
   117     const_deps: unit Graph.T,
   118     axioms: term Symtab.table,
   119     oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
   120     parents: theory list,
   121     ancestors: theory list};
   122 
   123 fun make_theory sign const_deps axioms oracles parents ancestors =
   124   Theory {sign = sign, const_deps = const_deps, axioms = axioms, oracles = oracles,
   125     parents = parents, ancestors = ancestors};
   126 
   127 fun rep_theory (Theory args) = args;
   128 
   129 val sign_of = #sign o rep_theory;
   130 val is_draft = Sign.is_draft o sign_of;
   131 val syn_of = #syn o Sign.rep_sg o sign_of;
   132 val parents_of = #parents o rep_theory;
   133 val ancestors_of = #ancestors o rep_theory;
   134 
   135 (*errors involving theories*)
   136 exception THEORY of string * theory list;
   137 
   138 (*compare theories*)
   139 val subthy = Sign.subsig o pairself sign_of;
   140 val eq_thy = Sign.eq_sg o pairself sign_of;
   141 
   142 (*check for some theory*)
   143 fun requires thy name what =
   144   if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then ()
   145   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);
   146 
   147 fun assert_super thy1 thy2 =
   148   if subthy (thy1, thy2) then thy2
   149   else raise THEORY ("Not a super theory", [thy1, thy2]);
   150 
   151 (*partial Pure theory*)
   152 val pre_pure =
   153   make_theory Sign.pre_pure Graph.empty Symtab.empty Symtab.empty [] [];
   154 
   155 
   156 
   157 (** extend theory **)
   158 
   159 (*name spaces*)
   160 val axiomK = "axiom";
   161 val oracleK = "oracle";
   162 
   163 
   164 (* extend logical part of a theory *)
   165 
   166 fun err_dup_axms names =
   167   error ("Duplicate axiom name(s): " ^ commas_quote names);
   168 
   169 fun err_dup_oras names =
   170   error ("Duplicate oracles: " ^ commas_quote names);
   171 
   172 fun ext_theory thy ext_sg ext_deps new_axms new_oras =
   173   let
   174     val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   175     val draft = Sign.is_draft sign;
   176     val axioms' =
   177       Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
   178         handle Symtab.DUPS names => err_dup_axms names;
   179     val oracles' =
   180       Symtab.extend (oracles, new_oras)
   181         handle Symtab.DUPS names => err_dup_oras names;
   182     val (parents', ancestors') =
   183       if draft then (parents, ancestors) else ([thy], thy :: ancestors);
   184   in
   185     make_theory (ext_sg sign) (ext_deps const_deps) axioms' oracles' parents' ancestors'
   186   end;
   187 
   188 
   189 (* extend signature of a theory *)
   190 
   191 fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] [];
   192 
   193 val add_classes      = ext_sign Sign.add_classes;
   194 val add_classes_i    = ext_sign Sign.add_classes_i;
   195 val add_classrel     = ext_sign Sign.add_classrel;
   196 val add_classrel_i   = ext_sign Sign.add_classrel_i;
   197 val add_defsort      = ext_sign Sign.add_defsort;
   198 val add_defsort_i    = ext_sign Sign.add_defsort_i;
   199 val add_types        = ext_sign Sign.add_types;
   200 val add_nonterminals = ext_sign Sign.add_nonterminals;
   201 val add_tyabbrs      = ext_sign Sign.add_tyabbrs;
   202 val add_tyabbrs_i    = ext_sign Sign.add_tyabbrs_i;
   203 val add_arities      = ext_sign Sign.add_arities;
   204 val add_arities_i    = ext_sign Sign.add_arities_i;
   205 val add_consts       = ext_sign Sign.add_consts;
   206 val add_consts_i     = ext_sign Sign.add_consts_i;
   207 val add_syntax       = ext_sign Sign.add_syntax;
   208 val add_syntax_i     = ext_sign Sign.add_syntax_i;
   209 val add_modesyntax   = curry (ext_sign Sign.add_modesyntax);
   210 val add_modesyntax_i = curry (ext_sign Sign.add_modesyntax_i);
   211 val add_trfuns       = ext_sign Sign.add_trfuns;
   212 val add_trfunsT      = ext_sign Sign.add_trfunsT;
   213 val add_tokentrfuns  = ext_sign Sign.add_tokentrfuns;
   214 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
   215 val add_trrules      = ext_sign Sign.add_trrules;
   216 val add_trrules_i    = ext_sign Sign.add_trrules_i;
   217 val add_path         = ext_sign Sign.add_path;
   218 val parent_path      = add_path "..";
   219 val root_path        = add_path "/";
   220 val add_space        = ext_sign Sign.add_space;
   221 val hide_space       = ext_sign Sign.hide_space;
   222 val hide_space_i     = ext_sign Sign.hide_space_i;
   223 val hide_classes     = curry hide_space_i Sign.classK;
   224 val hide_types       = curry hide_space_i Sign.typeK;
   225 val hide_consts      = curry hide_space_i Sign.constK;
   226 val add_name         = ext_sign Sign.add_name;
   227 val copy             = ext_sign (K Sign.copy) ();
   228 val prep_ext         = ext_sign (K Sign.prep_ext) ();
   229 
   230 
   231 
   232 (** add axioms **)
   233 
   234 (* prepare axioms *)
   235 
   236 fun err_in_axm name =
   237   error ("The error(s) above occurred in axiom " ^ quote name);
   238 
   239 fun no_vars tm =
   240   if null (term_vars tm) andalso null (term_tvars tm) then tm
   241   else error "Illegal schematic variable(s) in term";
   242 
   243 fun cert_axm sg (name, raw_tm) =
   244   let
   245     val (t, T, _) = Sign.certify_term sg raw_tm
   246       handle TYPE (msg, _, _) => error msg
   247            | TERM (msg, _) => error msg;
   248   in
   249     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   250     assert (T = propT) "Term not of type prop";
   251     (name, no_vars t)
   252   end;
   253 
   254 (*some duplication of code with read_def_cterm*)
   255 fun read_def_axm (sg, types, sorts) used (name, str) =
   256   let
   257     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
   258     val (t, _) = Sign.infer_types sg types sorts used true (ts, propT);
   259   in cert_axm sg (name, t) end
   260   handle ERROR => err_in_axm name;
   261 
   262 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str;
   263 
   264 fun inferT_axm sg (name, pre_tm) =
   265   let
   266     val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
   267   in (name, no_vars t) end
   268   handle ERROR => err_in_axm name;
   269 
   270 
   271 (* extend axioms of a theory *)
   272 
   273 fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
   274   let
   275     val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
   276     val axioms =
   277       map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
   278     val ext_sg = Sign.add_space (axiomK, map fst axioms);
   279   in ext_theory thy ext_sg I axioms [] end;
   280 
   281 val add_axioms = ext_axms read_axm;
   282 val add_axioms_i = ext_axms cert_axm;
   283 
   284 
   285 (* add oracle **)
   286 
   287 fun add_oracle (raw_name, oracle) (thy as Theory {sign, ...}) =
   288   let
   289     val name = Sign.full_name sign raw_name;
   290     val ext_sg = Sign.add_space (oracleK, [name]);
   291   in ext_theory thy ext_sg I [] [(name, (oracle, stamp ()))] end;
   292 
   293 
   294 
   295 (** add constant definitions **)
   296 
   297 (* clash_types, clash_consts *)
   298 
   299 (*check if types have common instance (ignoring sorts)*)
   300 
   301 fun clash_types ty1 ty2 =
   302   let
   303     val ty1' = Type.varifyT ty1;
   304     val ty2' = incr_tvar (maxidx_of_typ ty1' + 1) (Type.varifyT ty2);
   305   in Type.raw_unify (ty1', ty2') end;
   306 
   307 fun clash_consts (c1, ty1) (c2, ty2) =
   308   c1 = c2 andalso clash_types ty1 ty2;
   309 
   310 
   311 (* clash_defns *)
   312 
   313 fun clash_defn c_ty (name, tm) =
   314   let val (c, ty') = dest_Const (head_of (fst (Logic.dest_equals tm))) in
   315     if clash_consts c_ty (c, ty') then Some (name, ty') else None
   316   end handle TERM _ => None;
   317 
   318 fun clash_defns c_ty axms =
   319   distinct (mapfilter (clash_defn c_ty) axms);
   320 
   321 
   322 (* overloading *)
   323 
   324 datatype overloading = NoOverloading | Useless | Plain;
   325 
   326 fun overloading sg declT defT =
   327   let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
   328     if Sign.typ_instance sg (declT, T) then NoOverloading
   329     else if Sign.typ_instance sg (Type.rem_sorts declT, Type.rem_sorts T) then Useless
   330     else Plain
   331   end;
   332 
   333 
   334 (* dest_defn *)
   335 
   336 fun dest_defn tm =
   337   let
   338     fun err msg = raise TERM (msg, [tm]);
   339 
   340     val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   341       handle TERM _ => err "Not a meta-equality (==)";
   342     val (head, args) = strip_comb lhs;
   343     val c_ty as (c, ty) = dest_Const head
   344       handle TERM _ => err "Head of lhs not a constant";
   345 
   346     fun dest_free (Free (x, _)) = x
   347       | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   348       | dest_free _ = raise Match;
   349 
   350     val show_frees = commas_quote o map dest_free;
   351     val show_tfrees = commas_quote o map fst;
   352 
   353     val lhs_dups = duplicates args;
   354     val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   355     val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   356   in
   357     if not (forall (can dest_free) args) then
   358       err "Arguments (on lhs) must be variables"
   359     else if not (null lhs_dups) then
   360       err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   361     else if not (null rhs_extras) then
   362       err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   363     else if not (null rhs_extrasT) then
   364       err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   365     else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then
   366       err ("Constant to be defined occurs on rhs")
   367     else (c_ty, rhs)
   368   end;
   369 
   370 
   371 (* check_defn *)
   372 
   373 fun err_in_defn sg name msg =
   374   (error_msg msg;
   375     error ("The error(s) above occurred in definition " ^ quote (Sign.full_name sg name)));
   376 
   377 fun cycle_msg namess = "Cyclic dependency of constants:\n" ^
   378   cat_lines (map (space_implode " -> " o map quote o rev) namess);
   379 
   380 fun add_deps (c, cs) deps =
   381   let fun declare (G, x) = Graph.new_node (x, ()) G handle Graph.DUP _ => G
   382   in foldl declare (deps, c :: cs) |> Graph.add_deps_acyclic (c, cs) end;
   383 
   384 
   385 fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
   386   let
   387     fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   388       Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   389 
   390     fun def_txt (c_ty, txt) = Pretty.block
   391       (Pretty.str "Definition of " :: pretty_const c_ty @
   392         (if txt = "" then [] else [Pretty.str txt]));
   393 
   394     fun show_defn c (dfn, ty') = Pretty.block
   395       (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
   396 
   397     val (c_ty as (c, ty), rhs) = dest_defn tm
   398       handle TERM (msg, _) => err_in_defn sg name msg;
   399     val c_decl =
   400       (case Sign.const_type sg c of Some T => T
   401       | None => err_in_defn sg name ("Undeclared constant " ^ quote c));
   402 
   403     val clashed = clash_defns c_ty axms;
   404   in
   405     if not (null clashed) then
   406       err_in_defn sg name (Pretty.string_of (Pretty.chunks
   407         (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
   408     else
   409       (case overloading sg c_decl ty of
   410         NoOverloading =>
   411           (add_deps (c, Term.add_term_consts (rhs, [])) deps
   412               handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess),
   413             def :: axms)
   414       | Useless =>
   415            err_in_defn sg name (Pretty.string_of (Pretty.chunks
   416              [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
   417                  "imposes additional sort constraints on the declared type of the constant"]))
   418       | Plain =>
   419          (if not overloaded then warning (Pretty.string_of (Pretty.chunks
   420            [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see "
   421                ^ quote (Sign.full_name sg name) ^ ")")]))
   422          else (); (deps, def :: axms)))
   423   end;
   424 
   425 
   426 (* add_defs *)
   427 
   428 fun ext_defns prep_axm overloaded raw_axms thy =
   429   let
   430     val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   431     val all_axioms = flat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
   432 
   433     val axms = map (prep_axm sign) raw_axms;
   434     val (const_deps', _) = foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
   435   in
   436     make_theory sign const_deps' axioms oracles parents ancestors
   437     |> add_axioms_i axms
   438   end;
   439 
   440 val add_defs_i = ext_defns cert_axm;
   441 val add_defs = ext_defns read_axm;
   442 
   443 
   444 
   445 (** additional theory data **)
   446 
   447 val init_data = curry (ext_sign Sign.init_data);
   448 fun print_data kind = Sign.print_data kind o sign_of;
   449 fun get_data kind f = Sign.get_data kind f o sign_of;
   450 fun put_data kind f = ext_sign (Sign.put_data kind f);
   451 
   452 
   453 
   454 (** merge theories **)          (*exception ERROR*)
   455 
   456 fun merge_sign (sg, thy) =
   457   Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
   458 
   459 (*merge list of theories from left to right, preparing extend*)
   460 fun prep_ext_merge thys =
   461   if null thys then
   462     error "Merge: no parent theories"
   463   else if exists is_draft thys then
   464     error "Attempt to merge draft theories"
   465   else
   466     let
   467       val sign' =
   468         foldl merge_sign (sign_of (hd thys), tl thys)
   469         |> Sign.prep_ext
   470         |> Sign.add_path "/";
   471 
   472       val depss = map (#const_deps o rep_theory) thys;
   473       val deps' = foldl (Graph.merge_acyclic (K true)) (hd depss, tl depss)
   474         handle Graph.CYCLES namess => error (cycle_msg namess);
   475 
   476       val axioms' = Symtab.empty;
   477 
   478       fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2;
   479       val oracles' =
   480         Symtab.make (gen_distinct eq_ora
   481           (flat (map (Symtab.dest o #oracles o rep_theory) thys)))
   482         handle Symtab.DUPS names => err_dup_oras names;
   483 
   484       val parents' = gen_distinct eq_thy thys;
   485       val ancestors' =
   486         gen_distinct eq_thy (parents' @ flat (map ancestors_of thys));
   487     in
   488       make_theory sign' deps' axioms' oracles' parents' ancestors'
   489     end;
   490 
   491 
   492 end;
   493 
   494 structure BasicTheory: BASIC_THEORY = Theory;
   495 open BasicTheory;