--- a/src/Pure/sign.ML Tue Jan 18 07:53:35 1994 +0100
+++ b/src/Pure/sign.ML Tue Jan 18 13:46:08 1994 +0100
@@ -1,10 +1,9 @@
(* Title: Pure/sign.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
+ Copyright 1994 University of Cambridge
-The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
-typs under a signature).
+The abstract types "sg" of signatures
*)
signature SIGN =
@@ -14,11 +13,6 @@
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 *
@@ -27,32 +21,18 @@
(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 =
@@ -90,20 +70,20 @@
(*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;
@@ -238,44 +218,12 @@
-(**** 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;
@@ -284,78 +232,5 @@
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;