src/Pure/sign.ML
author nipkow
Tue Jan 04 17:03:52 1994 +0100 (1994-01-04)
changeset 211 7ab45715c0a6
parent 206 0d624d1ba9cc
child 224 d762f9421933
permissions -rw-r--r--
added fake_cterm_of to speed up rewriting
     1 (*  Title:      Pure/sign.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
     7 typs under a signature).
     8 *)
     9 
    10 signature SIGN =
    11 sig
    12   structure Type: TYPE
    13   structure Symtab: SYMTAB
    14   structure Syntax: SYNTAX
    15   sharing Symtab = Type.Symtab
    16   type sg
    17   type cterm
    18   type ctyp
    19   val cfun: (term -> term) -> (cterm -> cterm)
    20   val cterm_of: sg -> term -> cterm
    21   val ctyp_of: sg -> typ -> ctyp
    22   val extend: sg -> string ->
    23         (class * class list) list * class list *
    24         (string list * int) list *
    25         (string * indexname list * string) list *
    26         (string list * (sort list * class)) list *
    27         (string list * string)list * Syntax.sext option -> sg
    28   val merge: sg * sg -> sg
    29   val pure: sg
    30   val read_cterm: sg -> string * typ -> cterm
    31   val read_ctyp: sg -> string -> ctyp
    32   val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
    33                   -> (indexname -> typ option) * (indexname -> sort option)
    34                   -> (string*string)list
    35                   -> (indexname*ctyp)list * (cterm*cterm)list
    36   val read_typ: sg * (indexname -> sort option) -> string -> typ
    37   val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
    38   val rep_ctyp: ctyp -> {T: typ, sign: sg}
    39   val rep_sg: sg -> {tsig: Type.type_sig,
    40                      const_tab: typ Symtab.table,
    41                      syn: Syntax.syntax,
    42                      stamps: string ref list}
    43   val string_of_cterm: cterm -> string
    44   val string_of_ctyp: ctyp -> string
    45   val pprint_cterm: cterm -> pprint_args -> unit
    46   val pprint_ctyp: ctyp -> pprint_args -> unit
    47   val string_of_term: sg -> term -> string
    48   val string_of_typ: sg -> typ -> string
    49   val subsig: sg * sg -> bool
    50   val pprint_term: sg -> term -> pprint_args -> unit
    51   val pprint_typ: sg -> typ -> pprint_args -> unit
    52   val term_of: cterm -> term
    53   val typ_of: ctyp -> typ
    54   val pretty_term: sg -> term -> Syntax.Pretty.T
    55 val fake_cterm_of: sg -> term -> cterm
    56 end;
    57 
    58 functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    59 struct
    60 
    61 structure Type = Type;
    62 structure Symtab = Type.Symtab;
    63 structure Syntax = Syntax;
    64 structure Pretty = Syntax.Pretty
    65 
    66 
    67 (* Signatures of theories. *)
    68 
    69 datatype sg =
    70   Sg of {
    71     tsig: Type.type_sig,            (*order-sorted signature of types*)
    72     const_tab: typ Symtab.table,    (*types of constants*)
    73     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    74     stamps: string ref list};       (*unique theory indentifier*)
    75 
    76 
    77 fun rep_sg (Sg args) = args;
    78 
    79 fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
    80 
    81 fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
    82 
    83 fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
    84 
    85 (*Is constant present in table with more generic type?*)
    86 fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
    87         Some U => Type.typ_instance(tsig,T,U) | _ => false;
    88 
    89 
    90 (*Check a term for errors.  Are all constants and types valid in signature?
    91   Does not check that term is well-typed!*)
    92 fun term_errors (sign as Sg{tsig,const_tab,...}) =
    93 let val showtyp = string_of_typ sign
    94     fun terrs (Const (a,T), errs) =
    95         if valid_const tsig const_tab (a,T)
    96         then Type.type_errors tsig (T,errs)
    97         else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    98       | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    99       | terrs (Var  ((a,i),T), errs) =
   100         if  i>=0  then  Type.type_errors tsig (T,errs)
   101         else  ("Negative index for Var: " ^ a) :: errs
   102       | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
   103       | terrs (Abs (_,T,t), errs) =
   104             Type.type_errors tsig (T,terrs(t,errs))
   105       | terrs (f$t, errs) = terrs(f, terrs (t,errs))
   106 in  terrs  end;
   107 
   108 
   109 
   110 (** The Extend operation **)
   111 
   112 (* Extend a signature: may add classes, types and constants. The "ref" in
   113    stamps ensures that no two signatures are identical -- it is impossible to
   114    forge a signature. *)
   115 
   116 fun extend (Sg {tsig, const_tab, syn, stamps}) name
   117   (classes, default, types, abbr, arities, const_decs, opt_sext) =
   118   let
   119     fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
   120 
   121     fun read_typ tsg sy s =
   122       Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
   123 
   124     fun check_typ tsg sy ty =
   125       (case Type.type_errors tsg (ty, []) of
   126         [] => ty
   127       | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
   128 
   129     (*reset TVar indices to zero, renaming to preserve distinctness*)
   130     fun zero_tvar_indices T =
   131       let
   132         val inxSs = typ_tvars T;
   133         val nms' = variantlist (map (#1 o #1) inxSs, []);
   134         val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
   135       in typ_subst_TVars tye T end;
   136 
   137     (*read and check the type mentioned in a const declaration; zero type var
   138       indices because type inference requires it*)
   139 
   140     fun read_consts tsg sy (cs, s) =
   141       let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
   142       in
   143         (case Type.type_errors tsg (ty, []) of
   144           [] => (cs, ty)
   145         | errs => error (cat_lines (("Error in type of constants " ^
   146             space_implode " " (map quote cs)) :: errs)))
   147       end;
   148 
   149     val tsig' = Type.extend (tsig, classes, default, types, arities);
   150 
   151     fun read_typ_abbr(a,v,s)=
   152       let val T = Type.varifyT(read_typ tsig' syn s)
   153       in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
   154 
   155     val abbr' = map read_typ_abbr abbr;
   156     val tsig'' = Type.add_abbrs(tsig',abbr');
   157 
   158     val read_ty =
   159       (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
   160     val log_types = Type.logical_types tsig'';
   161     val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
   162     val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
   163 
   164     val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
   165 
   166     val const_decs' =
   167       map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
   168   in
   169     Sg {
   170       tsig = tsig'',
   171       const_tab = Symtab.st_of_declist (const_decs', const_tab)
   172         handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   173       syn = syn',
   174       stamps = ref name :: stamps}
   175   end;
   176 
   177 
   178 (* The empty signature *)
   179 
   180 val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
   181   syn = Syntax.type_syn, stamps = []};
   182 
   183 
   184 (* The pure signature *)
   185 
   186 val pure = extend sg0 "Pure"
   187 ([("logic", [])],
   188  ["logic"],
   189  [(["fun"], 2),
   190   (["prop"], 0),
   191   (Syntax.syntax_types, 0)],
   192  [],
   193  [(["fun"],  ([["logic"], ["logic"]], "logic")),
   194   (["prop"], ([], "logic"))],
   195  [([Syntax.constrainC], "'a::logic => 'a")],
   196  Some Syntax.pure_sext);
   197 
   198 
   199 
   200 (** The Merge operation **)
   201 
   202 (*Update table with (a,x) providing any existing asgt to "a" equals x. *)
   203 fun update_eq ((a,x),tab) =
   204     case Symtab.lookup(tab,a) of
   205         None => Symtab.update((a,x), tab)
   206       | Some y => if x=y then tab
   207             else  raise TERM ("Incompatible types for constant: "^a, []);
   208 
   209 (*Combine tables, updating tab2 by tab1 and checking.*)
   210 fun merge_tabs (tab1,tab2) =
   211     Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
   212 
   213 (*Combine tables, overwriting tab2 with tab1.*)
   214 fun smash_tabs (tab1,tab2) =
   215     Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
   216 
   217 (*Combine stamps, checking that theory names are disjoint. *)
   218 fun merge_stamps (stamps1,stamps2) =
   219   let val stamps = stamps1 union stamps2 in
   220   case findrep (map ! stamps) of
   221      a::_ => error ("Attempt to merge different versions of theory: " ^ a)
   222    | [] => stamps
   223   end;
   224 
   225 (*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
   226 fun merge
   227   (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
   228    sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
   229     if stamps2 subset stamps1 then sign1
   230     else if stamps1 subset stamps2 then sign2
   231     else (*neither is union already; must form union*)
   232       let val tsig = Type.merge (tsig1, tsig2);
   233       in
   234         Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
   235           stamps = merge_stamps (stamps1, stamps2),
   236           syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
   237       end;
   238 
   239 
   240 
   241 (**** CERTIFIED TYPES ****)
   242 
   243 
   244 (*Certified typs under a signature*)
   245 datatype ctyp = Ctyp of {sign: sg,  T: typ};
   246 
   247 fun rep_ctyp(Ctyp ctyp) = ctyp;
   248 
   249 fun typ_of (Ctyp{sign,T}) = T;
   250 
   251 fun ctyp_of (sign as Sg{tsig,...}) T =
   252         case Type.type_errors tsig (T,[]) of
   253           [] => Ctyp{sign= sign,T= T}
   254         | errs =>  error (cat_lines ("Error in type:" :: errs));
   255 
   256 (*The only use is a horrible hack in the simplifier!*)
   257 fun read_typ(Sg{tsig,syn,...}, defS) s =
   258     let val term = Syntax.read syn Syntax.typeT s;
   259         val S0 = Type.defaultS tsig;
   260         fun defS0 s = case defS s of Some S => S | None => S0;
   261     in Syntax.typ_of_term defS0 term end;
   262 
   263 fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
   264 
   265 fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
   266 
   267 fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
   268 
   269 
   270 (**** CERTIFIED TERMS ****)
   271 
   272 (*Certified terms under a signature, with checked typ and maxidx of Vars*)
   273 datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
   274 
   275 fun rep_cterm (Cterm args) = args;
   276 
   277 (*Return the underlying term*)
   278 fun term_of (Cterm{sign,t,T,maxidx}) = t;
   279 
   280 (** pretty printing of terms **)
   281 
   282 fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
   283 
   284 fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
   285 
   286 fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
   287 
   288 fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
   289 
   290 fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
   291 
   292 (*Create a cterm by checking a "raw" term with respect to a signature*)
   293 fun cterm_of sign t =
   294   case  term_errors sign (t,[])  of
   295       [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
   296     | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
   297 
   298 fun fake_cterm_of sign t =
   299   Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
   300 
   301 fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
   302 
   303 (*Lexing, parsing, polymorphic typechecking of a term.*)
   304 fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
   305                    (a,T) =
   306   let val showtyp = string_of_typ sign
   307       and showterm = string_of_term sign
   308       fun termerr [] = ""
   309         | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   310         | termerr ts = "\nInvolving these terms:\n" ^
   311                        cat_lines (map showterm ts)
   312       val t = Syntax.read syn T a;
   313       val (t',tye) = Type.infer_types (tsig, const_tab, types,
   314                                        sorts, showtyp, T, t)
   315                   handle TYPE (msg, Ts, ts) =>
   316           error ("Type checking error: " ^ msg ^ "\n" ^
   317                   cat_lines (map showtyp Ts) ^ termerr ts)
   318   in (cterm_of sign t', tye)
   319   end
   320   handle TERM (msg, _) => error ("Error: " ^  msg);
   321 
   322 
   323 fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
   324 
   325 (** reading of instantiations **)
   326 
   327 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   328         | _ => error("Lexical error in variable name " ^ quote (implode cs));
   329 
   330 fun absent ixn =
   331   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   332 
   333 fun inst_failure ixn =
   334   error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   335 
   336 fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
   337 let fun split([],tvs,vs) = (tvs,vs)
   338       | split((sv,st)::l,tvs,vs) = (case explode sv of
   339                   "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   340                 | cs => split(l,tvs,(indexname cs,st)::vs));
   341     val (tvs,vs) = split(insts,[],[]);
   342     fun readT((a,i),st) =
   343         let val ixn = ("'" ^ a,i);
   344             val S = case rsorts ixn of Some S => S | None => absent ixn;
   345             val T = read_typ (sign,sorts) st;
   346         in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   347            else inst_failure ixn
   348         end
   349     val tye = map readT tvs;
   350     fun add_cterm ((cts,tye), (ixn,st)) =
   351         let val T = case rtypes ixn of
   352                       Some T => typ_subst_TVars tye T
   353                     | None => absent ixn;
   354             val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   355             val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   356         in ((cv,ct)::cts,tye2 @ tye) end
   357     val (cterms,tye') = foldl add_cterm (([],tye), vs);
   358 in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   359 
   360 end;
   361