src/Pure/sign.ML
author lcp
Tue Jan 18 13:46:08 1994 +0100 (1994-01-18)
changeset 229 4002c4cd450c
parent 224 d762f9421933
child 251 c9b984c0a674
permissions -rw-r--r--
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field
of a theorem to be regarded as a cterm -- avoids expensive calls to
cterm_of.
     1 (*  Title:      Pure/sign.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 The abstract types "sg" of signatures
     7 *)
     8 
     9 signature SIGN =
    10 sig
    11   structure Type: TYPE
    12   structure Symtab: SYMTAB
    13   structure Syntax: SYNTAX
    14   sharing Symtab = Type.Symtab
    15   type sg
    16   val extend: sg -> string ->
    17         (class * class list) list * class list *
    18         (string list * int) list *
    19         (string * indexname list * string) list *
    20         (string list * (sort list * class)) list *
    21         (string list * string)list * Syntax.sext option -> sg
    22   val merge: sg * sg -> sg
    23   val pure: sg
    24   val read_typ: sg * (indexname -> sort option) -> string -> typ
    25   val rep_sg: sg -> {tsig: Type.type_sig,
    26                      const_tab: typ Symtab.table,
    27                      syn: Syntax.syntax,
    28                      stamps: string ref list}
    29   val string_of_term: sg -> term -> string
    30   val string_of_typ: sg -> typ -> string
    31   val subsig: sg * sg -> bool
    32   val pprint_term: sg -> term -> pprint_args -> unit
    33   val pprint_typ: sg -> typ -> pprint_args -> unit
    34   val pretty_term: sg -> term -> Syntax.Pretty.T
    35   val term_errors: sg -> term -> string list
    36 end;
    37 
    38 functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    39 struct
    40 
    41 structure Type = Type;
    42 structure Symtab = Type.Symtab;
    43 structure Syntax = Syntax;
    44 structure Pretty = Syntax.Pretty
    45 
    46 
    47 (* Signatures of theories. *)
    48 
    49 datatype sg =
    50   Sg of {
    51     tsig: Type.type_sig,            (*order-sorted signature of types*)
    52     const_tab: typ Symtab.table,    (*types of constants*)
    53     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    54     stamps: string ref list};       (*unique theory indentifier*)
    55 
    56 
    57 fun rep_sg (Sg args) = args;
    58 
    59 fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
    60 
    61 fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
    62 
    63 fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
    64 
    65 (*Is constant present in table with more generic type?*)
    66 fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
    67         Some U => Type.typ_instance(tsig,T,U) | _ => false;
    68 
    69 
    70 (*Check a term for errors.  Are all constants and types valid in signature?
    71   Does not check that term is well-typed!*)
    72 fun term_errors (sign as Sg{tsig,const_tab,...}) =
    73   let val showtyp = string_of_typ sign
    74       fun terrs (Const (a,T), errs) =
    75 	  if valid_const tsig const_tab (a,T)
    76 	  then Type.type_errors tsig (T,errs)
    77 	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    78 	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    79 	| terrs (Var  ((a,i),T), errs) =
    80 	  if  i>=0  then  Type.type_errors tsig (T,errs)
    81 	  else  ("Negative index for Var: " ^ a) :: errs
    82 	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    83 	| terrs (Abs (_,T,t), errs) =
    84 	      Type.type_errors tsig (T,terrs(t,errs))
    85 	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
    86   in  fn t => terrs(t,[])  end;
    87 
    88 
    89 
    90 (** The Extend operation **)
    91 
    92 (* Extend a signature: may add classes, types and constants. The "ref" in
    93    stamps ensures that no two signatures are identical -- it is impossible to
    94    forge a signature. *)
    95 
    96 fun extend (Sg {tsig, const_tab, syn, stamps}) name
    97   (classes, default, types, abbr, arities, const_decs, opt_sext) =
    98   let
    99     fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
   100 
   101     fun read_typ tsg sy s =
   102       Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
   103 
   104     fun check_typ tsg sy ty =
   105       (case Type.type_errors tsg (ty, []) of
   106         [] => ty
   107       | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
   108 
   109     (*reset TVar indices to zero, renaming to preserve distinctness*)
   110     fun zero_tvar_indices T =
   111       let
   112         val inxSs = typ_tvars T;
   113         val nms' = variantlist (map (#1 o #1) inxSs, []);
   114         val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
   115       in typ_subst_TVars tye T end;
   116 
   117     (*read and check the type mentioned in a const declaration; zero type var
   118       indices because type inference requires it*)
   119 
   120     fun read_consts tsg sy (cs, s) =
   121       let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
   122       in
   123         (case Type.type_errors tsg (ty, []) of
   124           [] => (cs, ty)
   125         | errs => error (cat_lines (("Error in type of constants " ^
   126             space_implode " " (map quote cs)) :: errs)))
   127       end;
   128 
   129     val tsig' = Type.extend (tsig, classes, default, types, arities);
   130 
   131     fun read_typ_abbr(a,v,s)=
   132       let val T = Type.varifyT(read_typ tsig' syn s)
   133       in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
   134 
   135     val abbr' = map read_typ_abbr abbr;
   136     val tsig'' = Type.add_abbrs(tsig',abbr');
   137 
   138     val read_ty =
   139       (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
   140     val log_types = Type.logical_types tsig'';
   141     val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
   142     val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
   143 
   144     val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
   145 
   146     val const_decs' =
   147       map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
   148   in
   149     Sg {
   150       tsig = tsig'',
   151       const_tab = Symtab.st_of_declist (const_decs', const_tab)
   152         handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   153       syn = syn',
   154       stamps = ref name :: stamps}
   155   end;
   156 
   157 
   158 (* The empty signature *)
   159 
   160 val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
   161   syn = Syntax.type_syn, stamps = []};
   162 
   163 
   164 (* The pure signature *)
   165 
   166 val pure = extend sg0 "Pure"
   167 ([("logic", [])],
   168  ["logic"],
   169  [(["fun"], 2),
   170   (["prop"], 0),
   171   (Syntax.syntax_types, 0)],
   172  [],
   173  [(["fun"],  ([["logic"], ["logic"]], "logic")),
   174   (["prop"], ([], "logic"))],
   175  [([Syntax.constrainC], "'a::logic => 'a")],
   176  Some Syntax.pure_sext);
   177 
   178 
   179 
   180 (** The Merge operation **)
   181 
   182 (*Update table with (a,x) providing any existing asgt to "a" equals x. *)
   183 fun update_eq ((a,x),tab) =
   184     case Symtab.lookup(tab,a) of
   185         None => Symtab.update((a,x), tab)
   186       | Some y => if x=y then tab
   187             else  raise TERM ("Incompatible types for constant: "^a, []);
   188 
   189 (*Combine tables, updating tab2 by tab1 and checking.*)
   190 fun merge_tabs (tab1,tab2) =
   191     Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
   192 
   193 (*Combine tables, overwriting tab2 with tab1.*)
   194 fun smash_tabs (tab1,tab2) =
   195     Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
   196 
   197 (*Combine stamps, checking that theory names are disjoint. *)
   198 fun merge_stamps (stamps1,stamps2) =
   199   let val stamps = stamps1 union stamps2 in
   200   case findrep (map ! stamps) of
   201      a::_ => error ("Attempt to merge different versions of theory: " ^ a)
   202    | [] => stamps
   203   end;
   204 
   205 (*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
   206 fun merge
   207   (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
   208    sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
   209     if stamps2 subset stamps1 then sign1
   210     else if stamps1 subset stamps2 then sign2
   211     else (*neither is union already; must form union*)
   212       let val tsig = Type.merge (tsig1, tsig2);
   213       in
   214         Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
   215           stamps = merge_stamps (stamps1, stamps2),
   216           syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
   217       end;
   218 
   219 
   220 
   221 fun read_typ(Sg{tsig,syn,...}, defS) s =
   222     let val term = Syntax.read syn Syntax.typeT s;
   223         val S0 = Type.defaultS tsig;
   224         fun defS0 s = case defS s of Some S => S | None => S0;
   225     in Syntax.typ_of_term defS0 term end;
   226 
   227 (** pretty printing of terms **)
   228 
   229 fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
   230 
   231 fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
   232 
   233 fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
   234 
   235 end;
   236