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