src/Pure/sign.ML

 (*  Title:      Pure/sign.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
-typs under a signature).
+    Copyright   1994  University of Cambridge
+
+The abstract types "sg" of signatures
 *)
 
 signature SIGN =
 sig
   structure Type: TYPE
   structure Symtab: SYMTAB
   structure Syntax: SYNTAX
   sharing Symtab = Type.Symtab
   type sg
-  type cterm
-  type ctyp
-  val cfun: (term -> term) -> (cterm -> cterm)
-  val cterm_of: sg -> term -> cterm
-  val ctyp_of: sg -> typ -> ctyp
   val extend: sg -> string ->
         (class * class list) list * class list *
         (string list * int) list *
         (string * indexname list * string) list *
         (string list * (sort list * class)) list *
         (string list * string)list * Syntax.sext option -> sg
   val merge: sg * sg -> sg
   val pure: sg
-  val read_cterm: sg -> string * typ -> cterm
-  val read_ctyp: sg -> string -> ctyp
-  val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
-                  -> (indexname -> typ option) * (indexname -> sort option)
-                  -> (string*string)list
-                  -> (indexname*ctyp)list * (cterm*cterm)list
   val read_typ: sg * (indexname -> sort option) -> string -> typ
-  val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
-  val rep_ctyp: ctyp -> {T: typ, sign: sg}
   val rep_sg: sg -> {tsig: Type.type_sig,
                      const_tab: typ Symtab.table,
                      syn: Syntax.syntax,
                      stamps: string ref list}
-  val string_of_cterm: cterm -> string
-  val string_of_ctyp: ctyp -> string
-  val pprint_cterm: cterm -> pprint_args -> unit
-  val pprint_ctyp: ctyp -> pprint_args -> unit
   val string_of_term: sg -> term -> string
   val string_of_typ: sg -> typ -> string
   val subsig: sg * sg -> bool
   val pprint_term: sg -> term -> pprint_args -> unit
   val pprint_typ: sg -> typ -> pprint_args -> unit
-  val term_of: cterm -> term
-  val typ_of: ctyp -> typ
   val pretty_term: sg -> term -> Syntax.Pretty.T
-val fake_cterm_of: sg -> term -> cterm
+  val term_errors: sg -> term -> string list
 end;
 
 functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
 struct
 

 
 
 (*Check a term for errors.  Are all constants and types valid in signature?
   Does not check that term is well-typed!*)
 fun term_errors (sign as Sg{tsig,const_tab,...}) =
-let val showtyp = string_of_typ sign
-    fun terrs (Const (a,T), errs) =
-        if valid_const tsig const_tab (a,T)
-        then Type.type_errors tsig (T,errs)
-        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
-      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
-      | terrs (Var  ((a,i),T), errs) =
-        if  i>=0  then  Type.type_errors tsig (T,errs)
-        else  ("Negative index for Var: " ^ a) :: errs
-      | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
-      | terrs (Abs (_,T,t), errs) =
-            Type.type_errors tsig (T,terrs(t,errs))
-      | terrs (f$t, errs) = terrs(f, terrs (t,errs))
-in  terrs  end;
+  let val showtyp = string_of_typ sign
+      fun terrs (Const (a,T), errs) =
+	  if valid_const tsig const_tab (a,T)
+	  then Type.type_errors tsig (T,errs)
+	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
+	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
+	| terrs (Var  ((a,i),T), errs) =
+	  if  i>=0  then  Type.type_errors tsig (T,errs)
+	  else  ("Negative index for Var: " ^ a) :: errs
+	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
+	| terrs (Abs (_,T,t), errs) =
+	      Type.type_errors tsig (T,terrs(t,errs))
+	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
+  in  fn t => terrs(t,[])  end;
 
 
 
 (** The Extend operation **)
 

           syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
       end;
 
 
 
-(**** CERTIFIED TYPES ****)
-
-
-(*Certified typs under a signature*)
-datatype ctyp = Ctyp of {sign: sg,  T: typ};
-
-fun rep_ctyp(Ctyp ctyp) = ctyp;
-
-fun typ_of (Ctyp{sign,T}) = T;
-
-fun ctyp_of (sign as Sg{tsig,...}) T =
-        case Type.type_errors tsig (T,[]) of
-          [] => Ctyp{sign= sign,T= T}
-        | errs =>  error (cat_lines ("Error in type:" :: errs));
-
 fun read_typ(Sg{tsig,syn,...}, defS) s =
     let val term = Syntax.read syn Syntax.typeT s;
         val S0 = Type.defaultS tsig;
         fun defS0 s = case defS s of Some S => S | None => S0;
     in Syntax.typ_of_term defS0 term end;
 
-fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
-
-fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
-
-fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
-
-
-(**** CERTIFIED TERMS ****)
-
-(*Certified terms under a signature, with checked typ and maxidx of Vars*)
-datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
-
-fun rep_cterm (Cterm args) = args;
-
-(*Return the underlying term*)
-fun term_of (Cterm{sign,t,T,maxidx}) = t;
-
 (** pretty printing of terms **)
 
 fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
 
 fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
 
 fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
 
-fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
-
-fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
-
-(*Create a cterm by checking a "raw" term with respect to a signature*)
-fun cterm_of sign t =
-  case  term_errors sign (t,[])  of
-      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
-    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
-
-(*The only use is a horrible hack in the simplifier!*)
-fun fake_cterm_of sign t =
-  Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
-
-fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
-
-(*Lexing, parsing, polymorphic typechecking of a term.*)
-fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
-                   (a,T) =
-  let val showtyp = string_of_typ sign
-      and showterm = string_of_term sign
-      fun termerr [] = ""
-        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
-        | termerr ts = "\nInvolving these terms:\n" ^
-                       cat_lines (map showterm ts)
-      val t = Syntax.read syn T a;
-      val (t',tye) = Type.infer_types (tsig, const_tab, types,
-                                       sorts, showtyp, T, t)
-                  handle TYPE (msg, Ts, ts) =>
-          error ("Type checking error: " ^ msg ^ "\n" ^
-                  cat_lines (map showtyp Ts) ^ termerr ts)
-  in (cterm_of sign t', tye)
-  end
-  handle TERM (msg, _) => error ("Error: " ^  msg);
-
-
-fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
-
-(** reading of instantiations **)
-
-fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
-        | _ => error("Lexical error in variable name " ^ quote (implode cs));
-
-fun absent ixn =
-  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
-
-fun inst_failure ixn =
-  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
-
-fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
-let fun split([],tvs,vs) = (tvs,vs)
-      | split((sv,st)::l,tvs,vs) = (case explode sv of
-                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
-                | cs => split(l,tvs,(indexname cs,st)::vs));
-    val (tvs,vs) = split(insts,[],[]);
-    fun readT((a,i),st) =
-        let val ixn = ("'" ^ a,i);
-            val S = case rsorts ixn of Some S => S | None => absent ixn;
-            val T = read_typ (sign,sorts) st;
-        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
-           else inst_failure ixn
-        end
-    val tye = map readT tvs;
-    fun add_cterm ((cts,tye), (ixn,st)) =
-        let val T = case rtypes ixn of
-                      Some T => typ_subst_TVars tye T
-                    | None => absent ixn;
-            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
-            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
-        in ((cv,ct)::cts,tye2 @ tye) end
-    val (cterms,tye') = foldl add_cterm (([],tye), vs);
-in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
-
 end;