--- a/src/Pure/Tools/codegen_thingol.ML Tue Oct 31 09:29:16 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Oct 31 09:29:17 2006 +0100
@@ -21,7 +21,6 @@
| Context of class list * (vname * int);
datatype itype =
`%% of string * itype list
- | `-> of itype * itype
| ITyVar of vname;
datatype iterm =
IConst of string * (inst list list * itype)
@@ -33,6 +32,7 @@
| ICase of (iterm * itype) * (iterm * iterm) list;
(*(discriminendum term (td), discriminendum type (ty)),
[(selector pattern (p), body term (t))] (bs))*)
+ val `-> : itype * itype -> itype;
val `--> : itype list * itype -> itype;
val `$$ : iterm * iterm list -> iterm;
val `|--> : (vname * itype) list * iterm -> iterm;
@@ -124,7 +124,6 @@
datatype itype =
`%% of string * itype list
- | `-> of itype * itype
| ITyVar of vname;
datatype iterm =
@@ -162,12 +161,13 @@
instance (classs, tyco) inst
*)
+fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
val op `--> = Library.foldr (op `->);
val op `$$ = Library.foldl (op `$);
val op `|--> = Library.foldr (op `|->);
val unfold_fun = unfoldr
- (fn op `-> ty => SOME ty
+ (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
| _ => NONE);
val unfold_app = unfoldl