168 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
168 | DFree of string * int (*free (uninterpreted) dictionary parameters*) |
169 | BVar of int * Univ list (*bound variables, named*) |
169 | BVar of int * Univ list (*bound variables, named*) |
170 | Abs of (int * (Univ list -> Univ)) * Univ list |
170 | Abs of (int * (Univ list -> Univ)) * Univ list |
171 (*abstractions as closures*); |
171 (*abstractions as closures*); |
172 |
172 |
173 fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys |
173 fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys |
174 | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l |
174 | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l |
175 | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys |
175 | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys |
176 | same _ _ = false |
176 | same _ _ = false; |
177 and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys); |
|
178 |
177 |
179 |
178 |
180 (* constructor functions *) |
179 (* constructor functions *) |
181 |
180 |
182 fun abss n f = Abs ((n, f), []); |
181 fun abss n f = Abs ((n, f), []); |