--- a/src/Pure/sign.ML Tue Dec 21 14:47:29 1993 +0100
+++ b/src/Pure/sign.ML Tue Dec 21 16:26:40 1993 +0100
@@ -22,6 +22,7 @@
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
@@ -52,7 +53,7 @@
val pretty_term: sg -> term -> Syntax.Pretty.T
end;
-functor SignFun(structure Type: TYPE and Syntax: SYNTAX): SIGN =
+functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
struct
structure Type = Type;
@@ -85,18 +86,18 @@
(*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;
+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,showtyp) (T,errs)
+ then Type.type_errors tsig (T,errs)
else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
- | terrs (Free (_,T), errs) = Type.type_errors (tsig,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,showtyp) (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,showtyp)(T,terrs(t,errs))
+ Type.type_errors tsig (T,terrs(t,errs))
| terrs (f$t, errs) = terrs(f, terrs (t,errs))
in terrs end;
@@ -109,7 +110,7 @@
forge a signature. *)
fun extend (Sg {tsig, const_tab, syn, stamps}) name
- (classes, default, types, arities, const_decs, opt_sext) =
+ (classes, default, types, abbr, arities, const_decs, opt_sext) =
let
fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
@@ -117,7 +118,7 @@
Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
fun check_typ tsg sy ty =
- (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
+ (case Type.type_errors tsg (ty, []) of
[] => ty
| errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
@@ -135,32 +136,34 @@
fun read_consts tsg sy (cs, s) =
let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
in
- (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
+ (case Type.type_errors tsg (ty, []) of
[] => (cs, ty)
| errs => error (cat_lines (("Error in type of constants " ^
space_implode " " (map quote cs)) :: errs)))
end;
-
- (* FIXME abbr *)
val tsig' = Type.extend (tsig, classes, default, types, arities);
- (* FIXME *)
- fun expand_typ _ ty = ty;
+ fun read_typ_abbr(a,v,s)=
+ let val T = Type.varifyT(read_typ tsig' syn s)
+ in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
+
+ val abbr' = map read_typ_abbr abbr;
+ val tsig'' = Type.add_abbrs(tsig',abbr');
val read_ty =
- (expand_typ tsig') o (check_typ tsig' syn) o (read_typ tsig' syn);
- val log_types = Type.logical_types tsig';
+ (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
+ val log_types = Type.logical_types tsig'';
val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
val const_decs' =
- map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
+ map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
in
Sg {
- tsig = tsig',
+ tsig = tsig'',
const_tab = Symtab.st_of_declist (const_decs', const_tab)
handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
syn = syn',
@@ -182,6 +185,7 @@
[(["fun"], 2),
(["prop"], 0),
(Syntax.syntax_types, 0)],
+ [],
[(["fun"], ([["logic"], ["logic"]], "logic")),
(["prop"], ([], "logic"))],
[([Syntax.constrainC], "'a::logic => 'a")],
@@ -241,7 +245,7 @@
fun typ_of (Ctyp{sign,T}) = T;
fun ctyp_of (sign as Sg{tsig,...}) T =
- case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
+ case Type.type_errors tsig (T,[]) of
[] => Ctyp{sign= sign,T= T}
| errs => error (cat_lines ("Error in type:" :: errs));
@@ -341,12 +345,10 @@
Some T => typ_subst_TVars tye T
| None => absent ixn;
val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
- in ((ixn,T,ct)::cts,tye2 @ tye) end
+ 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',
- map (fn (ixn,T,ct)=> (cterm_of sign (Var(ixn,typ_subst_TVars tye' T)), ct))
- cterms)
-end;
+in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
end;
--- a/src/Pure/type.ML Tue Dec 21 14:47:29 1993 +0100
+++ b/src/Pure/type.ML Tue Dec 21 16:26:40 1993 +0100
@@ -1,6 +1,6 @@
(* Title: Types and Sorts
+ Author: Tobias Nipkow & Lawrence C Paulson
ID: $Id$
- Author: Tobias Nipkow & Lawrence C Paulson
Maybe type classes should go in a separate module?
*)
@@ -10,7 +10,16 @@
sig
structure Symtab:SYMTAB
type type_sig
+ val rep_tsig: type_sig ->
+ {classes: class list, default: sort,
+ subclass: (class * class list) list,
+ args: (string * int) list,
+ coreg: (string * (class * sort list) list) list,
+ abbr: (string * (indexname list * typ) ) list}
val defaultS: type_sig -> sort
+ val add_abbrs : type_sig * (string * (indexname list * typ)) list
+ -> type_sig
+ val expand_typ: type_sig -> typ -> typ
val extend: type_sig * (class * class list)list * sort *
(string list * int)list *
(string list * (sort list * class))list -> type_sig
@@ -23,14 +32,9 @@
val logical_type: type_sig -> string -> bool
val logical_types: type_sig -> string list
val merge: type_sig * type_sig -> type_sig
- val rep_tsig: type_sig ->
- {classes: class list, default: sort,
- subclass: (class * class list) list,
- args: (string * int) list,
- coreg: (string * (class * sort list) list) list}
val thaw_vars: typ -> typ
val tsig0: type_sig
- val type_errors: type_sig * (typ->string) -> typ * string list -> string list
+ val type_errors: type_sig -> typ * string list -> string list
val typ_instance: type_sig * typ * typ -> bool
val typ_match: type_sig -> (indexname*typ)list * (typ*typ) ->
(indexname*typ)list
@@ -41,7 +45,7 @@
exception TYPE_MATCH;
end;
-functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) : TYPE =
+functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) (*: TYPE*) =
struct
structure Symtab = Symtab
@@ -74,7 +78,8 @@
default: sort,
subclass: (class * class list) list,
args: (string * int) list,
- coreg: (string * (class * domain) list) list };
+ coreg: (string * (class * domain) list) list,
+ abbr: (string * (indexname list * typ) ) list };
(* classes: a list of all declared classes;
default: the default sort attached to all unconstrained TVars
@@ -87,15 +92,18 @@
coreg: a two-fold association list of all type arities; (t,al) means that
type constructor t has the arities in al; an element (c,ss) of al
represents the arity (ss)c
+ abbr: an association list of type abbreviations
*)
fun rep_tsig (TySg comps) = comps;
+
val tsig0 = TySg{classes = [],
default = [],
subclass = [],
args = [],
- coreg = []};
+ coreg = [],
+ abbr = []};
fun undcl_class (s) = error("Class " ^ s ^ " has not been declared");
@@ -129,7 +137,6 @@
fun logical_types (tsig as TySg {args, ...}) =
filter (logical_type tsig) (map #1 args);
-
(* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1
with C1 <= C2 (according to an association list 'a')
@@ -207,6 +214,14 @@
fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars;
+(*Instantiation of type variables in types*)
+(*Pre: instantiations obey restrictions! *)
+fun inst_typ tye =
+ let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
+ | inst(T as TFree _) = T
+ | inst(T as TVar(v,_)) =
+ (case assoc(tye,v) of Some U => inst U | None => T)
+ in inst end;
(* 'least_sort' returns for a given type its maximum sort:
- type variables, free types: the sort brought with
@@ -214,11 +229,13 @@
arguments if the type is declared in 'coreg' of the
given type signature *)
-fun least_sort (tsig as TySg{subclass,coreg,...}) =
+fun least_sort (tsig as TySg{subclass,coreg,abbr,...}) =
let fun ls(T as Type(a,Ts)) =
- let val ars = case assoc (coreg,a) of Some(ars) => ars
- | None => raise TYPE(undcl_type a,[T],[]);
- in cod_above(subclass,map ls Ts,ars) end
+ (case assoc(abbr,a) of
+ Some(v,U) => ls(inst_typ(v~~Ts) U)
+ | None => (case assoc (coreg,a) of
+ Some(ars) => cod_above(subclass,map ls Ts,ars)
+ | None => raise TYPE(undcl_type a,[T],[])))
| ls(TFree(a,S)) = S
| ls(TVar(a,S)) = S
in ls end;
@@ -240,17 +257,41 @@
(*Instantiation of type variables in terms *)
fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye));
+
+(* expand1_typ *)
+
+fun expand1_typ(abbr,a,Ts) =
+ ( case assoc(abbr,a) of Some(v,U) => Some(inst_typ(v~~Ts) U)
+ | None => None );
+
+(* expand_typ *)
+
+fun expand_typ(tsig as TySg{abbr,...}) =
+ let fun exptyp(Type(a,Ts)) =
+ ( case assoc(abbr,a) of
+ Some (v,U) => exptyp(inst_typ(v~~Ts) U)
+ | None => Type(a, map exptyp Ts) )
+ | exptyp(T) = T
+ in exptyp end;
+
exception TYPE_MATCH;
(* Typ matching
typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *)
-fun typ_match tsig =
+fun typ_match (tsig as TySg{abbr,...}) =
let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of
None => ( (v, (check_has_sort(tsig,T,S); T))::subs
handle TYPE _ => raise TYPE_MATCH )
- | Some(U) => if U=T then subs else raise TYPE_MATCH)
- | tm(subs, (Type(a,Ts), Type(b,Us))) =
- if a<>b then raise TYPE_MATCH
+ | Some(U) => if expand_typ tsig U = expand_typ tsig T
+ then subs
+ else raise TYPE_MATCH)
+ | tm(subs, (T as Type(a,Ts), U as Type(b,Us))) =
+ if a<>b then
+ (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of
+ (None,None) => raise TYPE_MATCH
+ | (None,Some(U)) => tm(subs,(T,U))
+ | (Some(T),None) => tm(subs,(T,U))
+ | (Some(T),Some(U)) => tm(subs,(T,U)))
else foldl tm (subs, Ts~~Us)
| tm(subs, (TFree(x), TFree(y))) =
if x=y then subs else raise TYPE_MATCH
@@ -267,28 +308,27 @@
fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
+fun tyab_conflict(a) = error("Canīt declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
+
(*Is the type valid? Accumulates error messages in "errs".*)
-fun type_errors (tsig as TySg{classes,subclass,args,...},
- string_of_typ) (T,errs) =
-let fun class_err([],errs) = errs
- | class_err(S::Ss,errs) =
- if S mem classes then class_err (Ss,errs)
- else class_err (Ss,("Class " ^ S ^ " has not been declared") :: errs)
- fun errors(Type(c,Us), errs) =
+fun type_errors (tsig as TySg{classes,args,abbr,...}) =
+ let fun class_err(errs,C) =
+ if C mem classes then errs
+ else ("Class " ^ quote C ^ " has not been declared") :: errs
+ val sort_err = foldl class_err
+ fun errors(Type(c,Us), errs) =
let val errs' = foldr errors (Us,errs)
+ fun nargs n = if n=length(Us) then errs'
+ else ("Wrong number of arguments: " ^ c) :: errs'
in case assoc(args,c) of
- None => (undcl_type c) :: errs
- | Some(n) => if n=length(Us) then errs'
- else ("Wrong number of arguments: " ^ c) :: errs
+ Some(n) => nargs n
+ | None => (case assoc(abbr,c) of
+ Some(v,_) => nargs(length v)
+ | None => (undcl_type c) :: errs)
end
- | errors(TFree(_,S), errs) = class_err(S,errs)
- | errors(TVar(_,S), errs) = class_err(S,errs);
-in case errors(T,[]) of
- [] => ((least_sort tsig T; errs)
- handle TYPE(_,[U],_) => ("Ill-formed type: " ^ string_of_typ U)
- :: errs)
- | errs' => errs'@errs
-end;
+ | errors(TFree(_,S), errs) = sort_err(errs,S)
+ | errors(TVar(_,S), errs) = sort_err(errs,S)
+ in errors end;
(* 'add_class' adds a new class to the list of all existing classes *)
@@ -418,21 +458,61 @@
fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l));
in map ext coreg end;
-fun add_types(ac,(ts,n)) =
- let fun add_type((args,coreg),t) = case assoc(args,t) of
- Some _ => twice(t) | None => ((t,n)::args,(t,[])::coreg)
+fun add_types(aca,(ts,n)) =
+ let fun add_type((args,coreg,abbr),t) = case assoc(args,t) of
+ Some _ => twice(t)
+ | None => (case assoc(abbr,t) of Some _ => tyab_conflict(t)
+ | None => ((t,n)::args,(t,[])::coreg,abbr))
in if n<0
then error("Type constructor cannot have negative number of arguments")
- else foldl add_type (ac,ts)
+ else foldl add_type (aca,ts)
end;
+(* check_abbr *)
+
+fun check_abbr( (a,(vs,U)), tsig as TySg{abbr,args,...} ) =
+ let val (ndxname,_) = split_list(add_typ_tvars(U,[]))
+ fun err_abbr a = ("ERROR in abbreviation "^ quote a)
+ in if not( (ndxname subset vs) andalso (vs subset ndxname) )
+ then [err_abbr a,("Not the same set of variables on lhs and rhs")]
+ else
+ (case findrep(vs) of
+ (v,_)::_ => [err_abbr a,("Variable "^v^" occurs twice on lhs")]
+ |[] =>
+ (case assoc(args,a) of
+ Some _ => [err_abbr a,("A type with this name exists already")]
+ |None =>
+ (case assoc(abbr,a) of
+ Some _ => [err_abbr a,("An abbreviation with this name exists already")]
+ |None =>
+ (case type_errors (tsig) (U,[]) of
+ [] => []
+ |errs => (err_abbr a) :: errs
+ )
+ )
+ )
+ )
+ end;
+
+(* add_abbrs *)
+
+fun add_abbr (tsig as TySg{classes,default,subclass,args,coreg,abbr},
+ newabbr) =
+ case check_abbr (newabbr,tsig) of
+ [] => TySg{classes=classes,default=default,subclass=subclass,args=args,
+ coreg=coreg, abbr = (newabbr) :: abbr}
+ | errs => error(cat_lines errs) ;
+
+val add_abbrs = foldl add_abbr;
+
+
(* 'extend' takes the above described check- and extend-functions to
extend a given type signature with new classes and new type declarations *)
-fun extend (TySg{classes,default,subclass,args,coreg},
+fun extend (TySg{classes,default,subclass,args,coreg,abbr},
newclasses,newdefault,types,arities) =
let val (classes',subclass') = extend_classes(classes,subclass,newclasses);
- val (args',coreg') = foldl add_types ((args,coreg),types);
+ val (args',coreg',_) = foldl add_types ((args,coreg,abbr),types);
val old_coreg = map #1 coreg;
fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c);
fun is_new(c) = if c mem old_coreg then twice(c) else ();
@@ -441,7 +521,7 @@
val coreg''' = close (coreg'',subclass');
val default' = if null newdefault then default else newdefault;
in TySg{classes=classes', default=default',subclass=subclass', args=args',
- coreg=coreg'''} end;
+ coreg=coreg''',abbr=abbr} end;
(* 'assoc_union' merges two association lists if the contents associated
@@ -477,21 +557,30 @@
Some(m) => if m=n then args else varying_decls(t)
| None => (t,n)::args;
+fun merge_abbrs(abbr1,abbr2) =
+ let val abbru = abbr1 union abbr2
+ val names = map fst abbru
+ in ( case findrep names of
+ [] => abbru
+ |a::_ => error("ERROR in Type.merge: abbreviation "^a^" declared twice") ) end;
+
(* 'merge' takes the above declared functions to merge two type signatures *)
fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1,
- coreg=coreg1},
+ coreg=coreg1,abbr=abbr1},
TySg{classes=classes2,default=default2,subclass=subclass2,args=args2,
- coreg=coreg2}) =
+ coreg=coreg2,abbr=abbr2}) =
let val classes' = classes1 union classes2;
val subclass' = trcl (assoc_union (subclass1,subclass2));
val args' = foldl merge_args (args1,args2)
val coreg' = merge_coreg classes' subclass' (coreg1,coreg2);
- val default' = min_sort subclass' (default1 @ default2)
+ val default' = min_sort subclass' (default1 @ default2);
+ val abbr' = merge_abbrs(abbr1, abbr2);
in TySg{classes=classes' , default=default',subclass=subclass', args=args',
- coreg=coreg'}
+ coreg=coreg' , abbr = abbr' }
end;
+
(**** TYPE INFERENCE ****)
(*
@@ -535,7 +624,6 @@
*)
fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S);
-fun new_id_type(a) = TVar(("'"^a, new_tvar_inx()),[]);
(*Occurs check: type variable occurs in type?*)
fun occ v tye =
@@ -589,9 +677,8 @@
(* Order-sorted Unification of Types (U) *)
-
(* Precondition: both types are well-formed w.r.t. type constructor arities *)
-fun unify (tsig as TySg{subclass,coreg,...}) =
+fun unify (tsig as TySg{subclass,coreg,abbr,...}) =
let fun unif ((T,U),tye) =
case (devar(T,tye), devar(U,tye)) of
(T as TVar(v,S1), U as TVar(w,S2)) =>
@@ -604,19 +691,17 @@
if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
| (U, T as TVar (v,S)) =>
if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
- | (Type(a,Ts),Type(b,Us)) =>
- if a<>b then raise TUNIFY else foldr unif (Ts~~Us,tye)
+ | (T as Type(a,Ts),U as Type(b,Us)) =>
+ if a<>b then
+ (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of
+ (None,None) => raise TUNIFY
+ | (None,Some(U)) => unif((T,U),tye)
+ | (Some(T),None) => unif((T,U),tye)
+ | (Some(T),Some(U)) => unif((T,U),tye))
+ else foldr unif (Ts~~Us,tye)
| (T,U) => if T=U then tye else raise TUNIFY
in unif end;
-(*Instantiation of type variables in types*)
-(*Pre: instantiations obey restrictions! *)
-fun inst_typ tye =
- let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
- | inst(T as TFree _) = T
- | inst(T as TVar(v,_)) =
- (case assoc(tye,v) of Some U => inst U | None => T)
- in inst end;
(*Type inference for polymorphic term*)
fun infer tsig =
@@ -654,8 +739,9 @@
(*Find type of ident. If not in table then use ident's name for tyvar
to get consistent typing.*)
+fun new_id_type a = TVar(("'"^a,new_tvar_inx()),[]);
fun type_of_ixn(types,ixn as (a,_)) =
- case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
+ case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term;
fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body);
@@ -689,7 +775,7 @@
fun prepareT(typ) =
let val T = Syntax.typ_of_term defS0 typ;
val T' = freeze_vars T
- in case type_errors (tsig,string_of_typ) (T,[]) of
+ in case type_errors (tsig) (T,[]) of
[] => T'
| errs => raise TYPE(cat_lines errs,[T],[])
end