Necessary changes to accomodate type abbreviations.
authornipkow
Tue Dec 21 16:26:40 1993 +0100 (1993-12-21)
changeset 20039a931cc6558
parent 199 ac55692ab41f
child 201 9e41c6cec27c
Necessary changes to accomodate type abbreviations.
src/Pure/sign.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/sign.ML	Tue Dec 21 14:47:29 1993 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Dec 21 16:26:40 1993 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val extend: sg -> string ->
     1.5          (class * class list) list * class list *
     1.6          (string list * int) list *
     1.7 +        (string * indexname list * string) list *
     1.8          (string list * (sort list * class)) list *
     1.9          (string list * string)list * Syntax.sext option -> sg
    1.10    val merge: sg * sg -> sg
    1.11 @@ -52,7 +53,7 @@
    1.12    val pretty_term: sg -> term -> Syntax.Pretty.T
    1.13  end;
    1.14  
    1.15 -functor SignFun(structure Type: TYPE and Syntax: SYNTAX): SIGN =
    1.16 +functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
    1.17  struct
    1.18  
    1.19  structure Type = Type;
    1.20 @@ -85,18 +86,18 @@
    1.21  (*Check a term for errors.  Are all constants and types valid in signature?
    1.22    Does not check that term is well-typed!*)
    1.23  fun term_errors (sign as Sg{tsig,const_tab,...}) =
    1.24 -let val showtyp = string_of_typ sign;
    1.25 +let val showtyp = string_of_typ sign
    1.26      fun terrs (Const (a,T), errs) =
    1.27          if valid_const tsig const_tab (a,T)
    1.28 -        then Type.type_errors (tsig,showtyp) (T,errs)
    1.29 +        then Type.type_errors tsig (T,errs)
    1.30          else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
    1.31 -      | terrs (Free (_,T), errs) = Type.type_errors (tsig,showtyp) (T,errs)
    1.32 +      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
    1.33        | terrs (Var  ((a,i),T), errs) =
    1.34 -        if  i>=0  then  Type.type_errors (tsig,showtyp) (T,errs)
    1.35 +        if  i>=0  then  Type.type_errors tsig (T,errs)
    1.36          else  ("Negative index for Var: " ^ a) :: errs
    1.37        | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
    1.38        | terrs (Abs (_,T,t), errs) =
    1.39 -            Type.type_errors(tsig,showtyp)(T,terrs(t,errs))
    1.40 +            Type.type_errors tsig (T,terrs(t,errs))
    1.41        | terrs (f$t, errs) = terrs(f, terrs (t,errs))
    1.42  in  terrs  end;
    1.43  
    1.44 @@ -109,7 +110,7 @@
    1.45     forge a signature. *)
    1.46  
    1.47  fun extend (Sg {tsig, const_tab, syn, stamps}) name
    1.48 -  (classes, default, types, arities, const_decs, opt_sext) =
    1.49 +  (classes, default, types, abbr, arities, const_decs, opt_sext) =
    1.50    let
    1.51      fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
    1.52  
    1.53 @@ -117,7 +118,7 @@
    1.54        Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
    1.55  
    1.56      fun check_typ tsg sy ty =
    1.57 -      (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.58 +      (case Type.type_errors tsg (ty, []) of
    1.59          [] => ty
    1.60        | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
    1.61  
    1.62 @@ -135,32 +136,34 @@
    1.63      fun read_consts tsg sy (cs, s) =
    1.64        let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
    1.65        in
    1.66 -        (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
    1.67 +        (case Type.type_errors tsg (ty, []) of
    1.68            [] => (cs, ty)
    1.69          | errs => error (cat_lines (("Error in type of constants " ^
    1.70              space_implode " " (map quote cs)) :: errs)))
    1.71        end;
    1.72  
    1.73 -
    1.74 -    (* FIXME abbr *)
    1.75      val tsig' = Type.extend (tsig, classes, default, types, arities);
    1.76  
    1.77 -    (* FIXME *)
    1.78 -    fun expand_typ _ ty = ty;
    1.79 +    fun read_typ_abbr(a,v,s)=
    1.80 +      let val T = Type.varifyT(read_typ tsig' syn s)
    1.81 +      in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
    1.82 +
    1.83 +    val abbr' = map read_typ_abbr abbr;
    1.84 +    val tsig'' = Type.add_abbrs(tsig',abbr');
    1.85  
    1.86      val read_ty =
    1.87 -      (expand_typ tsig') o (check_typ tsig' syn) o (read_typ tsig' syn);
    1.88 -    val log_types = Type.logical_types tsig';
    1.89 +      (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
    1.90 +    val log_types = Type.logical_types tsig'';
    1.91      val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
    1.92      val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
    1.93  
    1.94      val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
    1.95  
    1.96      val const_decs' =
    1.97 -      map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
    1.98 +      map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
    1.99    in
   1.100      Sg {
   1.101 -      tsig = tsig',
   1.102 +      tsig = tsig'',
   1.103        const_tab = Symtab.st_of_declist (const_decs', const_tab)
   1.104          handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
   1.105        syn = syn',
   1.106 @@ -182,6 +185,7 @@
   1.107   [(["fun"], 2),
   1.108    (["prop"], 0),
   1.109    (Syntax.syntax_types, 0)],
   1.110 + [],
   1.111   [(["fun"],  ([["logic"], ["logic"]], "logic")),
   1.112    (["prop"], ([], "logic"))],
   1.113   [([Syntax.constrainC], "'a::logic => 'a")],
   1.114 @@ -241,7 +245,7 @@
   1.115  fun typ_of (Ctyp{sign,T}) = T;
   1.116  
   1.117  fun ctyp_of (sign as Sg{tsig,...}) T =
   1.118 -        case Type.type_errors (tsig,string_of_typ sign) (T,[]) of
   1.119 +        case Type.type_errors tsig (T,[]) of
   1.120            [] => Ctyp{sign= sign,T= T}
   1.121          | errs =>  error (cat_lines ("Error in type:" :: errs));
   1.122  
   1.123 @@ -341,12 +345,10 @@
   1.124                        Some T => typ_subst_TVars tye T
   1.125                      | None => absent ixn;
   1.126              val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
   1.127 -        in ((ixn,T,ct)::cts,tye2 @ tye) end
   1.128 +            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
   1.129 +        in ((cv,ct)::cts,tye2 @ tye) end
   1.130      val (cterms,tye') = foldl add_cterm (([],tye), vs);
   1.131 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
   1.132 -    map (fn (ixn,T,ct)=> (cterm_of sign (Var(ixn,typ_subst_TVars tye' T)), ct))
   1.133 -        cterms)
   1.134 -end;
   1.135 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
   1.136  
   1.137  end;
   1.138  
     2.1 --- a/src/Pure/thm.ML	Tue Dec 21 14:47:29 1993 +0100
     2.2 +++ b/src/Pure/thm.ML	Tue Dec 21 16:26:40 1993 +0100
     2.3 @@ -38,6 +38,7 @@
     2.4    val extend_theory: theory -> string
     2.5  	-> (class * class list) list * sort
     2.6  	   * (string list * int)list
     2.7 +           * (string * indexname list * string) list
     2.8  	   * (string list * (sort list * class))list
     2.9  	   * (string list * string)list * Sign.Syntax.sext option
    2.10  	-> (string*string)list -> theory
    2.11 @@ -419,7 +420,6 @@
    2.12  	    (Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs))
    2.13    end;
    2.14  
    2.15 -
    2.16  (*Instantiation of Vars
    2.17  		      A
    2.18  	     --------------------
    2.19 @@ -471,7 +471,6 @@
    2.20             raise THM("instantiate: incompatible signatures",0,[th])
    2.21         | TYPE _ => raise THM("instantiate: type conflict", 0, [th]);
    2.22  
    2.23 -
    2.24  (*The trivial implication A==>A, justified by assume and forall rules.
    2.25    A can contain Vars, not so for assume!   *)
    2.26  fun trivial ct : thm = 
     3.1 --- a/src/Pure/type.ML	Tue Dec 21 14:47:29 1993 +0100
     3.2 +++ b/src/Pure/type.ML	Tue Dec 21 16:26:40 1993 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title: 	Types and Sorts
     3.5 +    Author:	Tobias Nipkow & Lawrence C Paulson
     3.6      ID:         $Id$
     3.7 -    Author:	Tobias Nipkow & Lawrence C Paulson
     3.8  
     3.9  Maybe type classes should go in a separate module?
    3.10  *)
    3.11 @@ -10,7 +10,16 @@
    3.12  sig
    3.13    structure Symtab:SYMTAB
    3.14    type type_sig
    3.15 +  val rep_tsig: type_sig ->
    3.16 +    {classes: class list, default: sort,
    3.17 +      subclass: (class * class list) list,
    3.18 +      args: (string * int) list,
    3.19 +      coreg: (string * (class * sort list) list) list,
    3.20 +      abbr: (string * (indexname list * typ) ) list}
    3.21    val defaultS: type_sig -> sort
    3.22 +  val add_abbrs : type_sig * (string * (indexname list * typ)) list
    3.23 +                    -> type_sig
    3.24 +  val expand_typ: type_sig -> typ -> typ 
    3.25    val extend: type_sig * (class * class list)list * sort *
    3.26  	      (string list * int)list *
    3.27  	      (string list * (sort list * class))list -> type_sig
    3.28 @@ -23,14 +32,9 @@
    3.29    val logical_type: type_sig -> string -> bool
    3.30    val logical_types: type_sig -> string list
    3.31    val merge: type_sig * type_sig -> type_sig
    3.32 -  val rep_tsig: type_sig ->
    3.33 -      {classes: class list, default: sort,
    3.34 -       subclass: (class * class list) list,
    3.35 -       args: (string * int) list,
    3.36 -       coreg: (string * (class * sort list) list) list}
    3.37    val thaw_vars: typ -> typ
    3.38    val tsig0: type_sig
    3.39 -  val type_errors: type_sig * (typ->string) -> typ * string list -> string list
    3.40 +  val type_errors: type_sig -> typ * string list -> string list
    3.41    val typ_instance: type_sig * typ * typ -> bool
    3.42    val typ_match: type_sig -> (indexname*typ)list * (typ*typ) ->
    3.43  		 (indexname*typ)list
    3.44 @@ -41,7 +45,7 @@
    3.45    exception TYPE_MATCH;
    3.46  end;
    3.47  
    3.48 -functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) : TYPE =
    3.49 +functor TypeFun(structure Symtab:SYMTAB and Syntax:SYNTAX) (*: TYPE*) = 
    3.50  struct
    3.51  structure Symtab = Symtab
    3.52  
    3.53 @@ -74,7 +78,8 @@
    3.54  	    default: sort,
    3.55  	    subclass: (class * class list) list,
    3.56  	    args: (string * int) list,
    3.57 -	    coreg: (string * (class * domain) list) list };
    3.58 +	    coreg: (string * (class * domain) list) list,
    3.59 +            abbr: (string * (indexname list * typ) ) list };
    3.60  
    3.61  (* classes: a list of all declared classes;
    3.62     default: the default sort attached to all unconstrained TVars
    3.63 @@ -87,15 +92,18 @@
    3.64     coreg: a two-fold association list of all type arities; (t,al) means that
    3.65            type constructor t has the arities in al; an element (c,ss) of al
    3.66            represents the arity (ss)c
    3.67 +   abbr: an association list of type abbreviations
    3.68  *)
    3.69  
    3.70  fun rep_tsig (TySg comps) = comps;
    3.71 + 
    3.72  
    3.73  val tsig0 = TySg{classes = [],
    3.74  		 default = [],
    3.75  		 subclass = [],
    3.76  		 args = [],
    3.77 -		 coreg = []};
    3.78 +		 coreg = [],
    3.79 +                 abbr = []};
    3.80  
    3.81  fun undcl_class (s) = error("Class " ^ s ^ " has not been declared");
    3.82  
    3.83 @@ -129,7 +137,6 @@
    3.84  fun logical_types (tsig as TySg {args, ...}) =
    3.85    filter (logical_type tsig) (map #1 args);
    3.86  
    3.87 -
    3.88  (* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
    3.89     S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1
    3.90     with C1 <= C2 (according to an association list 'a')
    3.91 @@ -207,6 +214,14 @@
    3.92  
    3.93  fun cod_above (a,w,ars) = min_filter a (fn w' => lew a (w,w')) ars;
    3.94  
    3.95 +(*Instantiation of type variables in types*)
    3.96 +(*Pre: instantiations obey restrictions! *)
    3.97 +fun inst_typ tye =
    3.98 +  let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
    3.99 +        | inst(T as TFree _) = T
   3.100 +        | inst(T as TVar(v,_)) =
   3.101 +            (case assoc(tye,v) of Some U => inst U | None => T)
   3.102 +  in inst end;
   3.103  
   3.104  (* 'least_sort' returns for a given type its maximum sort:
   3.105     - type variables, free types: the sort brought with
   3.106 @@ -214,11 +229,13 @@
   3.107                      arguments if the type is declared in 'coreg' of the 
   3.108                      given type signature  *) 
   3.109  
   3.110 -fun least_sort (tsig as TySg{subclass,coreg,...}) =
   3.111 +fun least_sort (tsig as TySg{subclass,coreg,abbr,...}) =
   3.112    let fun ls(T as Type(a,Ts)) =
   3.113 -	  let val ars = case assoc (coreg,a) of Some(ars) => ars
   3.114 -			      | None => raise TYPE(undcl_type a,[T],[]);
   3.115 -	  in cod_above(subclass,map ls Ts,ars) end
   3.116 +            (case assoc(abbr,a) of
   3.117 +               Some(v,U) => ls(inst_typ(v~~Ts) U)
   3.118 +             | None => (case assoc (coreg,a) of
   3.119 +                          Some(ars) => cod_above(subclass,map ls Ts,ars)
   3.120 +			| None => raise TYPE(undcl_type a,[T],[])))
   3.121  	| ls(TFree(a,S)) = S
   3.122  	| ls(TVar(a,S)) = S
   3.123    in ls end;
   3.124 @@ -240,17 +257,41 @@
   3.125  (*Instantiation of type variables in terms *)
   3.126  fun inst_term_tvars(tsig,tye) = map_term_types (inst_typ_tvars(tsig,tye));
   3.127  
   3.128 +
   3.129 +(* expand1_typ *)
   3.130 +
   3.131 +fun expand1_typ(abbr,a,Ts) =
   3.132 +         ( case assoc(abbr,a) of Some(v,U) => Some(inst_typ(v~~Ts) U)
   3.133 +                               | None      => None );
   3.134 +
   3.135 +(* expand_typ *)
   3.136 +
   3.137 +fun expand_typ(tsig as TySg{abbr,...}) =
   3.138 +  let fun exptyp(Type(a,Ts)) =
   3.139 +           ( case assoc(abbr,a) of
   3.140 +             Some (v,U) => exptyp(inst_typ(v~~Ts) U)
   3.141 +           | None       => Type(a, map exptyp Ts)    )
   3.142 +        | exptyp(T) = T
   3.143 +  in exptyp end;
   3.144 +
   3.145  exception TYPE_MATCH;
   3.146  
   3.147  (* Typ matching
   3.148     typ_match(ts,s,(U,T)) = s' <=> s'(U)=T and s' is an extension of s *)
   3.149 -fun typ_match tsig =
   3.150 +fun typ_match (tsig as TySg{abbr,...}) =
   3.151  let fun tm(subs, (TVar(v,S), T)) = (case assoc(subs,v) of
   3.152  		None => ( (v, (check_has_sort(tsig,T,S); T))::subs
   3.153  			handle TYPE _ => raise TYPE_MATCH )
   3.154 -	      | Some(U) => if U=T then subs else raise TYPE_MATCH)
   3.155 -      | tm(subs, (Type(a,Ts), Type(b,Us))) =
   3.156 -	if a<>b then raise TYPE_MATCH
   3.157 +	      | Some(U) => if expand_typ tsig U = expand_typ tsig T
   3.158 +                           then subs
   3.159 +                           else raise TYPE_MATCH)
   3.160 +      | tm(subs, (T as Type(a,Ts), U as Type(b,Us))) =
   3.161 +        if a<>b then
   3.162 +            (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of
   3.163 +                             (None,None) => raise TYPE_MATCH
   3.164 +                           | (None,Some(U)) => tm(subs,(T,U))
   3.165 +                           | (Some(T),None) => tm(subs,(T,U))
   3.166 +                           | (Some(T),Some(U)) => tm(subs,(T,U)))
   3.167  	else foldl tm (subs, Ts~~Us)
   3.168        | tm(subs, (TFree(x), TFree(y))) =
   3.169  	if x=y then subs else raise TYPE_MATCH
   3.170 @@ -267,28 +308,27 @@
   3.171  
   3.172  fun twice(a) = error("Type constructor " ^a^ " has already been declared.");
   3.173  
   3.174 +fun tyab_conflict(a) = error("Canīt declare type "^(quote a)^"!\nAn abbreviation with this name exists already.");
   3.175 +
   3.176  (*Is the type valid? Accumulates error messages in "errs".*)
   3.177 -fun type_errors (tsig as TySg{classes,subclass,args,...},
   3.178 -                 string_of_typ) (T,errs) =
   3.179 -let fun class_err([],errs) = errs
   3.180 -     |  class_err(S::Ss,errs) = 
   3.181 -          if S mem classes then class_err (Ss,errs)
   3.182 -	  else class_err (Ss,("Class " ^ S ^ " has not been declared") :: errs)
   3.183 -    fun errors(Type(c,Us), errs) =
   3.184 +fun type_errors (tsig as TySg{classes,args,abbr,...}) =
   3.185 +  let fun class_err(errs,C) =
   3.186 +            if C mem classes then errs
   3.187 +	    else ("Class " ^ quote C ^ " has not been declared") :: errs
   3.188 +      val sort_err = foldl class_err
   3.189 +      fun errors(Type(c,Us), errs) =
   3.190  	let val errs' = foldr errors (Us,errs)
   3.191 +            fun nargs n = if n=length(Us) then errs'
   3.192 +		          else ("Wrong number of arguments: " ^ c) :: errs'
   3.193  	in case assoc(args,c) of
   3.194 -	     None => (undcl_type c) :: errs
   3.195 -	   | Some(n) => if n=length(Us) then errs'
   3.196 -		        else ("Wrong number of arguments: " ^ c) :: errs
   3.197 +	     Some(n) => nargs n
   3.198 +	   | None => (case assoc(abbr,c) of
   3.199 +                        Some(v,_) => nargs(length v)
   3.200 +                      | None => (undcl_type c) :: errs)
   3.201  	end
   3.202 -      | errors(TFree(_,S), errs) = class_err(S,errs)
   3.203 -      | errors(TVar(_,S), errs) = class_err(S,errs);
   3.204 -in case errors(T,[]) of
   3.205 -     [] => ((least_sort tsig T; errs)
   3.206 -	    handle TYPE(_,[U],_) => ("Ill-formed type: " ^ string_of_typ U)
   3.207 -				    :: errs)
   3.208 -   | errs' => errs'@errs
   3.209 -end;
   3.210 +      | errors(TFree(_,S), errs) = sort_err(errs,S)
   3.211 +      | errors(TVar(_,S), errs) = sort_err(errs,S)
   3.212 +  in errors end;
   3.213  
   3.214  
   3.215  (* 'add_class' adds a new class to the list of all existing classes *) 
   3.216 @@ -418,21 +458,61 @@
   3.217        fun ext (s,l) = (s, foldl (check (map #1 l)) (l,l));
   3.218    in map ext coreg end;
   3.219  
   3.220 -fun add_types(ac,(ts,n)) =
   3.221 -  let fun add_type((args,coreg),t) = case assoc(args,t) of
   3.222 -          Some _ => twice(t) | None => ((t,n)::args,(t,[])::coreg)
   3.223 +fun add_types(aca,(ts,n)) =
   3.224 +  let fun add_type((args,coreg,abbr),t) = case assoc(args,t) of
   3.225 +          Some _ => twice(t) 
   3.226 +        | None => (case assoc(abbr,t) of Some _ => tyab_conflict(t)
   3.227 +                                       | None => ((t,n)::args,(t,[])::coreg,abbr))
   3.228    in if n<0
   3.229       then error("Type constructor cannot have negative number of arguments")
   3.230 -     else foldl add_type (ac,ts)
   3.231 +     else foldl add_type (aca,ts)
   3.232    end;
   3.233  
   3.234 +(* check_abbr *)
   3.235 +
   3.236 +fun check_abbr( (a,(vs,U)), tsig as TySg{abbr,args,...} ) =
   3.237 +  let val (ndxname,_) = split_list(add_typ_tvars(U,[]))
   3.238 +      fun err_abbr a = ("ERROR in abbreviation "^ quote a)
   3.239 +  in if not( (ndxname subset vs) andalso (vs subset ndxname) )
   3.240 +     then [err_abbr a,("Not the same set of variables on lhs and rhs")]
   3.241 +     else
   3.242 +      (case findrep(vs) of
   3.243 +        (v,_)::_ => [err_abbr a,("Variable "^v^" occurs twice on lhs")]
   3.244 +        |[] =>
   3.245 +       (case assoc(args,a) of
   3.246 +         Some _ => [err_abbr a,("A type with this name exists already")]
   3.247 +        |None => 
   3.248 +          (case assoc(abbr,a) of
   3.249 +            Some _ => [err_abbr a,("An abbreviation with this name exists already")]
   3.250 +           |None =>
   3.251 +             (case type_errors (tsig) (U,[]) of
   3.252 +               []  => []
   3.253 +              |errs => (err_abbr a) :: errs
   3.254 +             )
   3.255 +           )
   3.256 +         )
   3.257 +        )
   3.258 +  end;
   3.259 +
   3.260 +(* add_abbrs *)
   3.261 +
   3.262 +fun add_abbr (tsig as TySg{classes,default,subclass,args,coreg,abbr},
   3.263 +                newabbr) =
   3.264 +  case check_abbr (newabbr,tsig) of
   3.265 +     []   => TySg{classes=classes,default=default,subclass=subclass,args=args,
   3.266 +                  coreg=coreg, abbr = (newabbr) :: abbr}
   3.267 +   | errs => error(cat_lines errs) ;
   3.268 +
   3.269 +val add_abbrs = foldl add_abbr;
   3.270 +
   3.271 +
   3.272  (* 'extend' takes the above described check- and extend-functions to
   3.273     extend a given type signature with new classes and new type declarations *)
   3.274  
   3.275 -fun extend (TySg{classes,default,subclass,args,coreg},
   3.276 +fun extend (TySg{classes,default,subclass,args,coreg,abbr},
   3.277              newclasses,newdefault,types,arities) =
   3.278  let val (classes',subclass') = extend_classes(classes,subclass,newclasses);
   3.279 -    val (args',coreg') = foldl add_types ((args,coreg),types);
   3.280 +    val (args',coreg',_) = foldl add_types ((args,coreg,abbr),types);
   3.281      val old_coreg = map #1 coreg;
   3.282      fun is_old(c) = if c mem old_coreg then () else undcl_type_err(c);
   3.283      fun is_new(c) = if c mem old_coreg then twice(c) else ();
   3.284 @@ -441,7 +521,7 @@
   3.285      val coreg''' = close (coreg'',subclass');
   3.286      val default' = if null newdefault then default else newdefault;
   3.287  in TySg{classes=classes', default=default',subclass=subclass', args=args',
   3.288 -	coreg=coreg'''} end;
   3.289 +	coreg=coreg''',abbr=abbr} end;
   3.290  
   3.291  
   3.292  (* 'assoc_union' merges two association lists if the contents associated
   3.293 @@ -477,21 +557,30 @@
   3.294        Some(m) => if m=n then args else varying_decls(t)
   3.295      | None => (t,n)::args;
   3.296  
   3.297 +fun merge_abbrs(abbr1,abbr2) =
   3.298 +  let val abbru = abbr1 union abbr2
   3.299 +      val names = map fst abbru
   3.300 +  in ( case findrep names of
   3.301 +        []   => abbru
   3.302 +       |a::_ => error("ERROR in Type.merge: abbreviation "^a^" declared twice") ) end;
   3.303 +
   3.304  (* 'merge' takes the above declared functions to merge two type signatures *)
   3.305  
   3.306  fun merge(TySg{classes=classes1,default=default1,subclass=subclass1,args=args1,
   3.307 -           coreg=coreg1},
   3.308 +           coreg=coreg1,abbr=abbr1},
   3.309  	  TySg{classes=classes2,default=default2,subclass=subclass2,args=args2,
   3.310 -           coreg=coreg2}) =
   3.311 +           coreg=coreg2,abbr=abbr2}) =
   3.312    let val classes' = classes1 union classes2;
   3.313        val subclass' = trcl (assoc_union (subclass1,subclass2));
   3.314        val args' = foldl merge_args (args1,args2)
   3.315        val coreg' = merge_coreg classes' subclass' (coreg1,coreg2);
   3.316 -      val default' = min_sort subclass' (default1 @ default2)
   3.317 +      val default' = min_sort subclass' (default1 @ default2);
   3.318 +      val abbr' = merge_abbrs(abbr1, abbr2);
   3.319    in TySg{classes=classes' , default=default',subclass=subclass', args=args',
   3.320 -	  coreg=coreg'} 
   3.321 +	  coreg=coreg' , abbr = abbr' } 
   3.322    end;
   3.323  
   3.324 +
   3.325  (**** TYPE INFERENCE ****)
   3.326  
   3.327  (*
   3.328 @@ -535,7 +624,6 @@
   3.329  *)
   3.330  
   3.331  fun gen_tyvar(S) = TVar(("'a", new_tvar_inx()),S);
   3.332 -fun new_id_type(a) = TVar(("'"^a, new_tvar_inx()),[]);
   3.333  
   3.334  (*Occurs check: type variable occurs in type?*)
   3.335  fun occ v tye =
   3.336 @@ -589,9 +677,8 @@
   3.337  
   3.338  (* Order-sorted Unification of Types (U)  *)
   3.339  
   3.340 -
   3.341  (* Precondition: both types are well-formed w.r.t. type constructor arities *)
   3.342 -fun unify (tsig as TySg{subclass,coreg,...}) = 
   3.343 +fun unify (tsig as TySg{subclass,coreg,abbr,...}) = 
   3.344    let fun unif ((T,U),tye) =
   3.345          case (devar(T,tye), devar(U,tye)) of
   3.346  	  (T as TVar(v,S1), U as TVar(w,S2)) =>
   3.347 @@ -604,19 +691,17 @@
   3.348               if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
   3.349          | (U, T as TVar (v,S)) =>
   3.350               if occ v tye U then raise TUNIFY else W ((U,S),tsig,(v,U)::tye)
   3.351 -        | (Type(a,Ts),Type(b,Us)) =>
   3.352 -	     if a<>b then raise TUNIFY else foldr unif (Ts~~Us,tye)
   3.353 +        | (T as Type(a,Ts),U as Type(b,Us)) =>
   3.354 +             if a<>b then
   3.355 +                 (case (expand1_typ(abbr,a,Ts), expand1_typ(abbr,b,Us)) of
   3.356 +                             (None,None) => raise TUNIFY
   3.357 +                           | (None,Some(U)) => unif((T,U),tye)
   3.358 +                           | (Some(T),None) => unif((T,U),tye)
   3.359 +                           | (Some(T),Some(U)) => unif((T,U),tye))
   3.360 +             else foldr unif (Ts~~Us,tye)
   3.361          | (T,U) => if T=U then tye else raise TUNIFY
   3.362    in unif end;
   3.363  
   3.364 -(*Instantiation of type variables in types*)
   3.365 -(*Pre: instantiations obey restrictions! *)
   3.366 -fun inst_typ tye =
   3.367 -  let fun inst(Type(a,Ts)) = Type(a, map inst Ts)
   3.368 -        | inst(T as TFree _) = T
   3.369 -        | inst(T as TVar(v,_)) =
   3.370 -            (case assoc(tye,v) of Some U => inst U | None => T)
   3.371 -  in inst end;
   3.372  
   3.373  (*Type inference for polymorphic term*)
   3.374  fun infer tsig =
   3.375 @@ -654,8 +739,9 @@
   3.376  
   3.377  (*Find type of ident.  If not in table then use ident's name for tyvar
   3.378    to get consistent typing.*)
   3.379 +fun new_id_type a = TVar(("'"^a,new_tvar_inx()),[]);
   3.380  fun type_of_ixn(types,ixn as (a,_)) =
   3.381 -      case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
   3.382 +	case types ixn of Some T => freeze_vars T | None => TVar(("'"^a,~1),[]);
   3.383  
   3.384  fun constrain(term,T) = Const(Syntax.constrainC,T-->T) $ term;
   3.385  fun constrainAbs(Abs(a,_,body),T) = Abs(a,T,body);
   3.386 @@ -689,7 +775,7 @@
   3.387        fun prepareT(typ) =
   3.388  	let val T = Syntax.typ_of_term defS0 typ;
   3.389  	    val T' = freeze_vars T
   3.390 -	in case type_errors (tsig,string_of_typ) (T,[]) of
   3.391 +	in case type_errors (tsig) (T,[]) of
   3.392  	     [] => T'
   3.393  	   | errs => raise TYPE(cat_lines errs,[T],[])
   3.394  	end