1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
type kind =
ARROW of kind * kind
| TYP
type tycon =
| TyVar of int
| FUN
| LIST
| STRING
type typ =
TyForall of kind * typ
| TyApp of tycon * typ list
type exp =
| AbsTm of typ * exp
| Var of int
| App of exp * exp
| String of string
| AbsTy of kind * exp
| AppTy of exp * typ
type ttyp =
| TTyFun of ttyp * ttyp
| TTyList of ttyp
| TTyString
| TTyAny
| TTyVar of int
| TTyForall of ttyp
type texp =
| TAbsTm of ttyp * texp
| TVar of int
| TApp of texp * texp
| TString of string
| TLetTy of texp * texp
| TCast of texp * ttyp
| TAppTy of texp * ttyp
| TAbsTy of texp
let (-->) x y = TyApp (FUN, [x;y])
let (--->) x y = TTyFun (x,y)
let rec trans_kind = function
ARROW (k1,k2) -> (trans_kind k1 ---> trans_kind k2)
| TYP -> (TTyForall TANY ---> TTyAny)
let rec trans_typ_arg_aux = function
(* TyForall (k,ty) -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty)) ??? *)
| TyApp (TyVar tv, args) -> failwith "unreduced"
| ty -> TAbsTm (trans_kind k, TAbsTy (trans_typ ty))failwith "unreduced"
|
let rec trans_typ_arg env = function
| TyApp (FUN, []) ->
TAbsTm
(trans_kind TYP,
TLetTy (TVar 0,
TAbsTm
(trans_kind TYP,
TLetTy (TVar 0,
TAbsTm
(TTyForall TANY,
TAppTy (TVar 0, TTyFun (TTyVar 0, TTyVar 1)))))))
| TyApp (TyVar tv, args) ->
try List.assoc (tv,args) env
with Not_found -> failwith "trans_typ: unreduced type variable"
| ty -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, trans_typ env ty))
(*
| TyApp (STRING, []) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyString))
| TyApp (FUN, [l;r]) -> TAbsTm (TTyForall TANY, TAppTy (TVar 0, TTyFun (trans_typ l, trans_typ r)))
*)
let rec trans_typ env = function
TyForall (k,ty) -> (trans_kind k ---> TTyAny)
| TyApp (TyVar tv, args) ->
try List.assoc (tv,args) env
with Not_found -> failwith "trans_typ: unreduced type variable"
| TyApp (FUN, [l;r]) -> TTyFun (trans_typ env l, trans_typ env r)
| TyApp (STRING, []) -> TTyString
| _ -> failwith "trans_typ: badly formed input type"
let rec trans_exp env = function
| AbsTm (ty,e) -> TAbsTm(trans_typ ty, trans_exp e)
| Var n -> TVar n
| App (l,r) -> TApp(trans_exp l, trans_exp r)
| String s -> TString s
| AbsTy (k,e) -> TAbsTm(trans_kind k, reduce env e)
| AppTy (tm,ty) -> TAppTy(trans_exp tm, trans_typ_arg env ty)
open Format;;
let rec pp_print_exp pps = function
L e -> fprintf pps "\
|
