-
Notifications
You must be signed in to change notification settings - Fork 17
/
fomega.mli
113 lines (76 loc) · 2.19 KB
/
fomega.mli
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
102
103
104
105
106
107
108
109
110
111
112
113
(*
* (c) 2014 Andreas Rossberg
*)
(* Syntax *)
type lab = string
type var = string
type 'a row = (lab * 'a) list
type kind =
| BaseK
| ArrK of kind * kind
| ProdK of kind row
type typ =
| VarT of var
| PrimT of Prim.typ
| ArrT of typ * typ
| ProdT of typ row
| AllT of var * kind * typ
| AnyT of var * kind * typ
| LamT of var * kind * typ
| AppT of typ * typ
| TupT of typ row
| DotT of typ * lab
| RecT of var * kind * typ
| InferT of typ lazy_t * int
type exp =
| VarE of var
| PrimE of Prim.const
| IfE of exp * exp * exp
| LamE of var * typ * exp
| AppE of exp * exp
| TupE of exp row
| DotE of exp * lab
| GenE of var * kind * exp
| InstE of exp * typ
| PackE of typ * exp * typ
| OpenE of exp * var * var * exp
| RollE of exp * typ
| UnrollE of exp
| RecE of var * typ * exp
| LetE of exp * var * exp
exception Error of string
(* Renaming *)
module VarSet : Set.S with type elt = var
val rename : var -> var
val rename_for : VarSet.t -> var -> var
(* Environments *)
type env
val empty : env
val add_typ : var -> kind -> env -> env
val add_val : var -> typ -> env -> env
val lookup_typ : var -> env -> kind (* raise Error *)
val lookup_val : var -> env -> typ (* raise Error *)
(* Substitutions *)
type 'a subst = (var * 'a) list
val subst_typ : typ subst -> typ -> typ
val subst_typ_exp : typ subst -> exp -> exp
val subst_exp : exp subst -> exp -> exp
(* Normalisation and Equality *)
val varT : var * kind -> typ (* eta-long-normal *)
val norm_typ : typ -> typ (* raise Error *) (* beta normalisation *)
val norm_exp : exp -> exp (* raise Error *)
val equal_typ : typ -> typ -> bool (* raise Error *)
val force_typ : typ -> typ
(* Checking *)
val infer_typ : env -> typ -> kind (* raise Error *)
val infer_exp : env -> exp -> typ (* raise Error *)
val check_typ : env -> typ -> kind -> string -> unit (* raise Error *)
val check_exp : env -> exp -> typ -> string -> unit (* raise Error *)
(* Unrolling *)
val unroll_typ : typ -> typ option
(* String conversion *)
val verbose_exp_flag : bool ref
val verbose_typ_flag : bool ref
val string_of_kind : kind -> string
val string_of_typ : typ -> string
val string_of_exp : exp -> string