src/Pure/sign.ML
author wenzelm
Wed Feb 09 14:25:29 1994 +0100 (1994-02-09)
changeset 267 ab78019b8ec8
parent 266 3fe01df1a614
child 277 4abe17e92130
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      Pure/sign.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 
     5 The abstract type "sg" of signatures.
     6 
     7 TODO:
     8   a clean modular sequential Sign.extend (using sg_ext list);
     9 *)
    10 
    11 signature SIGN =
    12 sig
    13   structure Symtab: SYMTAB
    14   structure Syntax: SYNTAX
    15   structure Type: TYPE
    16   sharing Symtab = Type.Symtab
    17   local open Type in
    18     type sg
    19     val rep_sg: sg ->
    20       {tsig: type_sig,
    21        const_tab: typ Symtab.table,
    22        syn: Syntax.syntax,
    23        stamps: string ref list}
    24     val subsig: sg * sg -> bool
    25     val eq_sg: sg * sg -> bool
    26     val print_sg: sg -> unit
    27     val pprint_sg: sg -> pprint_args -> unit
    28     val pretty_term: sg -> term -> Syntax.Pretty.T
    29     val pretty_typ: sg -> typ -> Syntax.Pretty.T
    30     val string_of_term: sg -> term -> string
    31     val string_of_typ: sg -> typ -> string
    32     val pprint_term: sg -> term -> pprint_args -> unit
    33     val pprint_typ: sg -> typ -> pprint_args -> unit
    34     val certify_typ: sg -> typ -> typ
    35     val certify_term: sg -> term -> term * typ * int
    36     val read_typ: sg * (indexname -> sort option) -> string -> typ
    37     val extend: sg -> string ->
    38       (class * class list) list * class list *
    39       (string list * int) list *
    40       (string * string list * string) list *
    41       (string list * (sort list * class)) list *
    42       (string list * string) list * Syntax.sext option -> sg
    43     val merge: sg * sg -> sg
    44     val pure: sg
    45   end
    46 end;
    47 
    48 functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
    49 struct
    50 
    51 structure Symtab = Type.Symtab;
    52 structure Syntax = Syntax;
    53 structure Pretty = Syntax.Pretty;
    54 structure Type = Type;
    55 open Type;
    56 
    57 
    58 (** datatype sg **)
    59 
    60 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    61   impossible to forge a signature*)
    62 
    63 datatype sg =
    64   Sg of {
    65     tsig: type_sig,                 (*order-sorted signature of types*)
    66     const_tab: typ Symtab.table,    (*types of constants*)
    67     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    68     stamps: string ref list};       (*unique theory indentifier*)
    69 
    70 fun rep_sg (Sg args) = args;
    71 
    72 
    73 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
    74 
    75 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    76 
    77 
    78 
    79 (** print signature **)
    80 
    81 fun print_sg sg =
    82   let
    83     fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
    84 
    85     fun pretty_sort [cl] = Pretty.str cl
    86       | pretty_sort cls = Pretty.str_list "{" "}" cls;
    87 
    88     fun pretty_subclass (cl, cls) = Pretty.block
    89       [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
    90 
    91     fun pretty_default cls = Pretty.block
    92       [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
    93 
    94     fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
    95 
    96     fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
    97       [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
    98         Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
    99 
   100     fun pretty_arity ty (cl, []) = Pretty.block
   101           [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl]
   102       | pretty_arity ty (cl, srts) = Pretty.block
   103           [Pretty.str (ty ^ " ::"), Pretty.brk 1,
   104             Pretty.list "(" ")" (map pretty_sort srts),
   105             Pretty.brk 1, Pretty.str cl];
   106 
   107     fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
   108 
   109     fun pretty_const syn (c, ty) = Pretty.block
   110       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   111 
   112 
   113     val Sg {tsig, const_tab, syn, stamps} = sg;
   114     val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig;
   115   in
   116     Pretty.writeln (Pretty.strs ("stamps:" :: map ! stamps));
   117     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   118     Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass));
   119     Pretty.writeln (pretty_default default);
   120     Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args));
   121     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   122     Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg)));
   123     Pretty.writeln (Pretty.big_list "consts:"
   124       (map (pretty_const syn) (Symtab.alist_of const_tab)))
   125   end;
   126 
   127 
   128 fun pprint_sg (Sg {stamps, ...}) =
   129   Pretty.pprint (Pretty.str_list "{" "}" (map ! stamps));
   130 
   131 
   132 
   133 (** pretty printing of terms and types **)
   134 
   135 fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
   136 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
   137 
   138 fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
   139 fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
   140 
   141 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   142 fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   143 
   144 
   145 
   146 (** certify types and terms **)
   147 
   148 (*errors are indicated by exception TYPE*)
   149 
   150 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   151 
   152 
   153 (* FIXME -> term.ML (?) *)
   154 fun mapfilter_atoms f (Abs (_, _, t)) = mapfilter_atoms f t
   155   | mapfilter_atoms f (t $ u) = mapfilter_atoms f t @ mapfilter_atoms f u
   156   | mapfilter_atoms f a = (case f a of Some y => [y] | None => []);
   157 
   158 fun certify_term (sg as Sg {tsig, const_tab, ...}) tm =
   159   let
   160     fun valid_const a T =
   161       (case Symtab.lookup (const_tab, a) of
   162         Some U => typ_instance (tsig, T, U)
   163       | _ => false);
   164 
   165     fun atom_err (Const (a, T)) =
   166           if valid_const a T then None
   167           else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   168             quote (string_of_typ sg T))
   169       | atom_err (Var ((x, i), _)) =
   170           if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   171       | atom_err _ = None;
   172 
   173 
   174     val norm_tm =
   175       (case it_term_types (typ_errors tsig) (tm, []) of
   176         [] => map_term_types (norm_typ tsig) tm
   177       | errs => raise_type (cat_lines errs) [] [tm]);
   178   in
   179     (case mapfilter_atoms atom_err norm_tm of
   180       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   181     | errs => raise_type (cat_lines errs) [] [norm_tm])
   182   end;
   183 
   184 
   185 
   186 (** read types **)
   187 
   188 (*read and certify typ wrt a signature; errors are indicated by
   189   exception ERROR (with messages already printed)*)
   190 
   191 fun rd_typ tsig syn sort_of s =
   192   let
   193     val def_sort = defaultS tsig;
   194     val raw_ty =        (*this may raise ERROR, too!*)
   195       Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s;
   196   in
   197     cert_typ tsig raw_ty
   198       handle TYPE (msg, _, _) => error msg
   199   end
   200   handle ERROR => error ("The error(s) above occurred in type " ^ quote s);
   201 
   202 fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s;
   203 
   204 
   205 
   206 (** extend signature **)
   207 
   208 (*errors are indicated by exception ERROR (with messages already printed)*)
   209 
   210 fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
   211   let
   212     fun read_abbr syn (c, vs, rhs_src) =
   213       (c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src)))
   214         handle ERROR => error ("The error(s) above occurred in the rhs " ^
   215           quote rhs_src ^ "\nof type abbreviation " ^ quote c);
   216 
   217     (*reset TVar indices to 0, renaming to preserve distinctness*)
   218     fun zero_tvar_idxs T =
   219       let
   220         val inxSs = typ_tvars T;
   221         val nms' = variantlist (map (#1 o #1) inxSs, []);
   222         val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms');
   223       in
   224         typ_subst_TVars tye T
   225       end;
   226 
   227     (*read and check the type mentioned in a const declaration; zero type var
   228       indices because type inference requires it*)
   229     fun read_const tsig syn (c, s) =
   230       (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
   231         handle ERROR => error ("in declaration of constant " ^ quote c);
   232 
   233 
   234     val Sg {tsig, const_tab, syn, stamps} = sg;
   235     val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
   236       flat (map #1 consts);
   237     val sext = if_none opt_sext Syntax.empty_sext;
   238 
   239     val tsig' = extend_tsig tsig (classes, default, types, arities);
   240     val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs);
   241 
   242     val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
   243       (logical_types tsig1, xconsts, sext);
   244 
   245     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   246       (Syntax.constants sext @ consts));
   247 
   248     val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
   249       Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
   250         handle Symtab.DUPLICATE c
   251           => error ("Constant " ^ quote c ^ " declared twice");
   252 
   253     val stamps1 =
   254       if exists (equal name o !) stamps then
   255         error ("Theory already contains a " ^ quote name ^ " component")
   256       else stamps @ [ref name];
   257   in
   258     Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1}
   259   end;
   260 
   261 
   262 
   263 (** merge signatures **)
   264 
   265 (*errors are indicated by exception TERM*)
   266 
   267 fun check_stamps stamps =
   268   (case duplicates (map ! stamps) of
   269     [] => stamps
   270   | dups => raise_term ("Attempt to merge different versions of theories " ^
   271       commas (map quote dups)) []);
   272 
   273 fun merge (sg1, sg2) =
   274   if subsig (sg2, sg1) then sg1
   275   else if subsig (sg1, sg2) then sg2
   276   else
   277     (*neither is union already; must form union*)
   278     let
   279       val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   280         stamps = stamps1} = sg1;
   281       val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   282         stamps = stamps2} = sg2;
   283 
   284       val tsig = merge_tsigs (tsig1, tsig2);
   285 
   286       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   287         handle Symtab.DUPLICATE c =>
   288           raise_term ("Incompatible types for constant " ^ quote c) [];
   289 
   290       val syn = Syntax.merge (logical_types tsig) syn1 syn2;
   291 
   292       val stamps = check_stamps (merge_lists stamps1 stamps2);
   293     in
   294       Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   295     end;
   296 
   297 
   298 
   299 (** the Pure signature **)
   300 
   301 val sg0 = Sg {tsig = tsig0, const_tab = Symtab.null,
   302   syn = Syntax.type_syn, stamps = []};
   303 
   304 val pure = extend sg0 "Pure"
   305   ([("logic", [])],
   306    ["logic"],
   307    [(["fun"], 2),
   308     (["prop"], 0),
   309     (Syntax.syntax_types, 0)],
   310    [],
   311    [(["fun"],  ([["logic"], ["logic"]], "logic")),
   312     (["prop"], ([], "logic"))],
   313    ([Syntax.constrainC], "'a::{} => 'a") :: Syntax.syntax_consts,
   314    Some Syntax.pure_sext);
   315 
   316 
   317 end;
   318