14 TyForall of kind * typ
15 | TyApp of tycon * typ list
26 | TTyFun of ttyp * ttyp
34 | TAbsTm of ttyp * texp
38 | TLetTy of texp * texp
39 | TCast of texp * ttyp
41 | TAppTy of texp * ttyp
45 let (-->) x y = TyApp (FUN, [x;y])
46 let (--->) x y = TTyFun (x,y)
48 let rec trans_kind = function
49 ARROW (k1,k2) -> (trans_kind k1 ---> trans_kind k2)
50 | TYP -> (TTyForall TANY ---> TTyAny)
52 let rec trans_typ_arg_aux = function
53 (* TyForall (k,ty) -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty)) ??? *)
54 | TyApp (TyVar tv, args) -> failwith "unreduced"
55 | ty -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty))failwith "unreduced"
57 let rec trans_typ_arg env = function
67 TAppTy (TVar 0, TTyFun (TTyVar 0, TTyVar 1)))))))
68 | TyApp (TyVar tv, args) ->
69 try List.assoc (tv,args) env
70 with Not_found -> failwith "trans_typ: unreduced type variable"
71 | ty -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, trans_typ env ty))
73 | TyApp (STRING, []) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyString))
74 | TyApp (FUN, [l;r]) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyFun (trans_typ l, trans_typ r)))
78 let rec trans_typ env = function
79 TyForall (k,ty) -> (trans_kind k ---> TTyAny)
80 | TyApp (TyVar tv, args) ->
81 try List.assoc (tv,args) env
82 with Not_found -> failwith "trans_typ: unreduced type variable"
83 | TyApp (FUN, [l;r]) -> TTyFun (trans_typ env l, trans_typ env r)
84 | TyApp (STRING, []) -> TTyString
85 | _ -> failwith "trans_typ: badly formed input type"
88 let rec trans_exp env = function
89 | AbsTm (ty,e) -> TAbsTm(trans_typ ty, trans_exp e)
91 | App (l,r) -> TApp(trans_exp l, trans_exp r)
92 | String s -> TString s
93 | AbsTy (k,e) -> TAbsTm(trans_kind k, reduce env e)
94 | AppTy (tm,ty) -> TAppTy(trans_exp tm, trans_typ_arg env ty)
100 let rec pp_print_exp pps = function
101 L e -> fprintf pps "\