src/Pure/sign.ML
changeset 229 4002c4cd450c
parent 224 d762f9421933
child 251 c9b984c0a674
     1.1 --- a/src/Pure/sign.ML	Tue Jan 18 07:53:35 1994 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Jan 18 13:46:08 1994 +0100
     1.3 @@ -1,10 +1,9 @@
     1.4  (*  Title:      Pure/sign.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8 +    Copyright   1994  University of Cambridge
     1.9  
    1.10 -The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
    1.11 -typs under a signature).
    1.12 +The abstract types "sg" of signatures
    1.13  *)
    1.14  
    1.15  signature SIGN =
    1.16 @@ -14,11 +13,6 @@
    1.17    structure Syntax: SYNTAX
    1.18    sharing Symtab = Type.Symtab
    1.19    type sg
    1.20 -  type cterm
    1.21 -  type ctyp
    1.22 -  val cfun: (term -> term) -> (cterm -> cterm)
    1.23 -  val cterm_of: sg -> term -> cterm
    1.24 -  val ctyp_of: sg -> typ -> ctyp
    1.25    val extend: sg -> string ->
    1.26          (class * class list) list * class list *
    1.27          (string list * int) list *
    1.28 @@ -27,32 +21,18 @@
    1.29          (string list * string)list * Syntax.sext option -> sg
    1.30    val merge: sg * sg -> sg
    1.31    val pure: sg
    1.32 -  val read_cterm: sg -> string * typ -> cterm
    1.33 -  val read_ctyp: sg -> string -> ctyp
    1.34 -  val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
    1.35 -                  -> (indexname -> typ option) * (indexname -> sort option)
    1.36 -                  -> (string*string)list
    1.37 -                  -> (indexname*ctyp)list * (cterm*cterm)list
    1.38    val read_typ: sg * (indexname -> sort option) -> string -> typ
    1.39 -  val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
    1.40 -  val rep_ctyp: ctyp -> {T: typ, sign: sg}
    1.41    val rep_sg: sg -> {tsig: Type.type_sig,
    1.42                       const_tab: typ Symtab.table,
    1.43                       syn: Syntax.syntax,
    1.44                       stamps: string ref list}
    1.45 -  val string_of_cterm: cterm -> string
    1.46 -  val string_of_ctyp: ctyp -> string
    1.47 -  val pprint_cterm: cterm -> pprint_args -> unit
    1.48 -  val pprint_ctyp: ctyp -> pprint_args -> unit
    1.49    val string_of_term: sg -> term -> string
    1.50    val string_of_typ: sg -> typ -> string
    1.51    val subsig: sg * sg -> bool
    1.52    val pprint_term: sg -> term -> pprint_args -> unit
    1.53    val pprint_typ: sg -> typ -> pprint_args -> unit
    1.54 -  val term_of: cterm -> term
    1.55 -  val typ_of: ctyp -> typ
    1.56    val pretty_term: sg -> term -> Syntax.Pretty.T
    1.57 -val fake_cterm_of: sg -> term -> cterm
    1.58 +  val term_errors: sg -> term -> string list
    1.59  end;
    1.60  
    1.61  functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    1.62 @@ -90,20 +70,20 @@
    1.63  (*Check a term for errors.  Are all constants and types valid in signature?
    1.64    Does not check that term is well-typed!*)
    1.65  fun term_errors (sign as Sg{tsig,const_tab,...}) =
    1.66 -let val showtyp = string_of_typ sign
    1.67 -    fun terrs (Const (a,T), errs) =
    1.68 -        if valid_const tsig const_tab (a,T)
    1.69 -        then Type.type_errors tsig (T,errs)
    1.70 -        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    1.71 -      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    1.72 -      | terrs (Var  ((a,i),T), errs) =
    1.73 -        if  i>=0  then  Type.type_errors tsig (T,errs)
    1.74 -        else  ("Negative index for Var: " ^ a) :: errs
    1.75 -      | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    1.76 -      | terrs (Abs (_,T,t), errs) =
    1.77 -            Type.type_errors tsig (T,terrs(t,errs))
    1.78 -      | terrs (f$t, errs) = terrs(f, terrs (t,errs))
    1.79 -in  terrs  end;
    1.80 +  let val showtyp = string_of_typ sign
    1.81 +      fun terrs (Const (a,T), errs) =
    1.82 +	  if valid_const tsig const_tab (a,T)
    1.83 +	  then Type.type_errors tsig (T,errs)
    1.84 +	  else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    1.85 +	| terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    1.86 +	| terrs (Var  ((a,i),T), errs) =
    1.87 +	  if  i>=0  then  Type.type_errors tsig (T,errs)
    1.88 +	  else  ("Negative index for Var: " ^ a) :: errs
    1.89 +	| terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    1.90 +	| terrs (Abs (_,T,t), errs) =
    1.91 +	      Type.type_errors tsig (T,terrs(t,errs))
    1.92 +	| terrs (f$t, errs) = terrs(f, terrs (t,errs))
    1.93 +  in  fn t => terrs(t,[])  end;
    1.94  
    1.95  
    1.96  
    1.97 @@ -238,44 +218,12 @@
    1.98  
    1.99  
   1.100  
   1.101 -(**** CERTIFIED TYPES ****)
   1.102 -
   1.103 -
   1.104 -(*Certified typs under a signature*)
   1.105 -datatype ctyp = Ctyp of {sign: sg,  T: typ};
   1.106 -
   1.107 -fun rep_ctyp(Ctyp ctyp) = ctyp;
   1.108 -
   1.109 -fun typ_of (Ctyp{sign,T}) = T;
   1.110 -
   1.111 -fun ctyp_of (sign as Sg{tsig,...}) T =
   1.112 -        case Type.type_errors tsig (T,[]) of
   1.113 -          [] => Ctyp{sign= sign,T= T}
   1.114 -        | errs =>  error (cat_lines ("Error in type:" :: errs));
   1.115 -
   1.116  fun read_typ(Sg{tsig,syn,...}, defS) s =
   1.117      let val term = Syntax.read syn Syntax.typeT s;
   1.118          val S0 = Type.defaultS tsig;
   1.119          fun defS0 s = case defS s of Some S => S | None => S0;
   1.120      in Syntax.typ_of_term defS0 term end;
   1.121  
   1.122 -fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
   1.123 -
   1.124 -fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
   1.125 -
   1.126 -fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
   1.127 -
   1.128 -
   1.129 -(**** CERTIFIED TERMS ****)
   1.130 -
   1.131 -(*Certified terms under a signature, with checked typ and maxidx of Vars*)
   1.132 -datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
   1.133 -
   1.134 -fun rep_cterm (Cterm args) = args;
   1.135 -
   1.136 -(*Return the underlying term*)
   1.137 -fun term_of (Cterm{sign,t,T,maxidx}) = t;
   1.138 -
   1.139  (** pretty printing of terms **)
   1.140  
   1.141  fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
   1.142 @@ -284,78 +232,5 @@
   1.143  
   1.144  fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
   1.145  
   1.146 -fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
   1.147 -
   1.148 -fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
   1.149 -
   1.150 -(*Create a cterm by checking a "raw" term with respect to a signature*)
   1.151 -fun cterm_of sign t =
   1.152 -  case  term_errors sign (t,[])  of
   1.153 -      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
   1.154 -    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
   1.155 -
   1.156 -(*The only use is a horrible hack in the simplifier!*)
   1.157 -fun fake_cterm_of sign t =
   1.158 -  Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t}
   1.159 -
   1.160 -fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
   1.161 -
   1.162 -(*Lexing, parsing, polymorphic typechecking of a term.*)
   1.163 -fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
   1.164 -                   (a,T) =
   1.165 -  let val showtyp = string_of_typ sign
   1.166 -      and showterm = string_of_term sign
   1.167 -      fun termerr [] = ""
   1.168 -        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
   1.169 -        | termerr ts = "\nInvolving these terms:\n" ^
   1.170 -                       cat_lines (map showterm ts)
   1.171 -      val t = Syntax.read syn T a;
   1.172 -      val (t',tye) = Type.infer_types (tsig, const_tab, types,
   1.173 -                                       sorts, showtyp, T, t)
   1.174 -                  handle TYPE (msg, Ts, ts) =>
   1.175 -          error ("Type checking error: " ^ msg ^ "\n" ^
   1.176 -                  cat_lines (map showtyp Ts) ^ termerr ts)
   1.177 -  in (cterm_of sign t', tye)
   1.178 -  end
   1.179 -  handle TERM (msg, _) => error ("Error: " ^  msg);
   1.180 -
   1.181 -
   1.182 -fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
   1.183 -
   1.184 -(** reading of instantiations **)
   1.185 -
   1.186 -fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
   1.187 -        | _ => error("Lexical error in variable name " ^ quote (implode cs));
   1.188 -
   1.189 -fun absent ixn =
   1.190 -  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
   1.191 -
   1.192 -fun inst_failure ixn =
   1.193 -  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
   1.194 -
   1.195 -fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
   1.196 -let fun split([],tvs,vs) = (tvs,vs)
   1.197 -      | split((sv,st)::l,tvs,vs) = (case explode sv of
   1.198 -                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
   1.199 -                | cs => split(l,tvs,(indexname cs,st)::vs));
   1.200 -    val (tvs,vs) = split(insts,[],[]);
   1.201 -    fun readT((a,i),st) =
   1.202 -        let val ixn = ("'" ^ a,i);
   1.203 -            val S = case rsorts ixn of Some S => S | None => absent ixn;
   1.204 -            val T = read_typ (sign,sorts) st;
   1.205 -        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
   1.206 -           else inst_failure ixn
   1.207 -        end
   1.208 -    val tye = map readT tvs;
   1.209 -    fun add_cterm ((cts,tye), (ixn,st)) =
   1.210 -        let val T = case rtypes ixn of
   1.211 -                      Some T => typ_subst_TVars tye T
   1.212 -                    | None => absent ixn;
   1.213 -            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.214 -            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.215 -        in ((cv,ct)::cts,tye2 @ tye) end
   1.216 -    val (cterms,tye') = foldl add_cterm (([],tye), vs);
   1.217 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.218 -
   1.219  end;
   1.220