Source file typeInference.ml
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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
open UtilsLib.Utils
open Lambda
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.typeInference" ~doc:"logs ACGtkLib typeInference events") : Logs.LOG)
module Value =
struct
type t=int
type value = Lambda.stype
let unfold stype _ =
match stype with
| Lambda.Atom _ -> None
| Lambda.LFun (a,b) -> Some (1,[a;b])
| Lambda.Fun (a,b) -> Some (1,[a;b])
| _ -> failwith "Bug: No type inference on these types"
end
module UF=VarUnionFind.UF(Value)
module Type =
struct
exception Not_typable
type typing_env={l_level:int;
nl_level:int;
lvar_typing:int IntMap.t;
nlvar_typing:int IntMap.t;
const_typing:(int*int) IntMap.t;
cst_nbr:int;
type_equations:UF.t;}
let empty_env= {l_level=0;
nl_level=0;
lvar_typing=IntMap.empty;
nlvar_typing=IntMap.empty;
const_typing=IntMap.empty;
cst_nbr=0;
type_equations=UF.empty;}
let type_equation_log _ eq =
Log.debug (fun m -> m "type equation:");
UF.log_content Logs.Debug eq
let rec inference_aux level t ty_var env =
let prefix=String.make (level*3) ' ' in
Log.debug (fun m -> m "%sType inference of %s (currently %d)." prefix (Lambda.raw_to_string t) ty_var);
Log.debug (fun m -> m "%sEquations are:" prefix);
type_equation_log prefix env.type_equations;
let ty,new_env =
match t with
| Lambda.Var i ->
(try
let ty_in_env=IntMap.find (env.nl_level-i-1) env.nlvar_typing in
Log.debug (fun m -> m "%sAdding an equation (variable found in the environment) %d<-->%d" prefix ty_var ty_in_env);
let new_eq=UF.union ty_var ty_in_env env.type_equations in
ty_var,{env with type_equations=new_eq}
with
| Not_found ->
let new_var,new_eq=UF.generate_new_var env.type_equations in
Log.debug (fun m -> m "%sAdding a new variable %d and an equation" prefix new_var);
new_var,{env with nlvar_typing=IntMap.add i new_var env.nlvar_typing; type_equations=new_eq})
| Lambda.LVar i ->
(try
let ty_in_env=IntMap.find (env.l_level-i-1) env.lvar_typing in
Log.debug (fun m -> m "%sAdding an equation (Lvariable found in the environment) %d<-->%d" prefix ty_var ty_in_env);
let new_eq=UF.union ty_var ty_in_env env.type_equations in
ty_var,{env with type_equations=new_eq}
with
| Not_found ->
let new_var,new_eq=UF.generate_new_var env.type_equations in
Log.debug (fun m -> m "%sAdding a new Lvariable %d and an equation" prefix new_var);
new_var,{env with lvar_typing=IntMap.add i new_var env.lvar_typing; type_equations=new_eq})
| Lambda.Const i ->
let new_var,new_eq=UF.generate_new_var env.type_equations in
let new_eq=UF.union ty_var new_var new_eq in
new_var,{env with type_equations=new_eq;const_typing=IntMap.add (env.cst_nbr+1) (new_var,i) env.const_typing;cst_nbr=env.cst_nbr+1}
| Lambda.DConst _ -> failwith "Bug: there should not remain any defined constant when computing the principal type"
| Lambda.Abs (_x,t) ->
Log.debug (fun m -> m "%sType inference of an abstraction:" prefix);
let alpha,new_eq=UF.generate_new_var env.type_equations in
Log.debug (fun m -> m "%sAdded a variable at %d. Equations are:" prefix alpha);
let () = type_equation_log prefix new_eq in
let beta,new_eq=UF.generate_new_var new_eq in
Log.debug (fun m -> m "%sAdded a variable at %d. Equations are:" prefix beta);
let () = type_equation_log prefix new_eq in
let new_const,new_eq=UF.generate_new_constr new_eq (1,[alpha;beta]) in
Log.debug (fun m -> m "%sAdded new const at %d. Equations are:" prefix new_const);
let () = type_equation_log prefix new_eq in
Log.debug (fun m -> m "%sPreparing a Union %d %d." prefix ty_var new_const);
let new_eq=UF.union ty_var new_const new_eq in
Log.debug (fun m -> m "%sAdded a varibale at %d. Equations are:" prefix beta);
type_equation_log prefix new_eq;
let _,new_env=inference_aux (level+1) t beta {env with nl_level=env.nl_level+1;nlvar_typing=IntMap.add env.nl_level alpha env.nlvar_typing;type_equations=new_eq} in
let _is_cyclic,new_eq=UF.cyclic ty_var new_env.type_equations in
ty_var,{env with type_equations=new_eq;const_typing=new_env.const_typing;cst_nbr=new_env.cst_nbr}
| Lambda.LAbs (_x,t) ->
Log.debug (fun m -> m "%sType inference of a linear abstraction:" prefix);
let alpha,new_eq=UF.generate_new_var env.type_equations in
let beta,new_eq=UF.generate_new_var new_eq in
let new_const,new_eq=UF.generate_new_constr new_eq (1,[alpha;beta]) in
let new_eq=UF.union ty_var new_const new_eq in
let _,new_env=inference_aux (level+1) t beta {env with l_level=env.l_level+1;lvar_typing=IntMap.add env.l_level alpha env.lvar_typing;type_equations=new_eq} in
let _is_cyclic,new_eq=UF.cyclic ty_var new_env.type_equations in
ty_var,{env with type_equations=new_eq;const_typing=new_env.const_typing;cst_nbr=new_env.cst_nbr}
| Lambda.App (t,u) ->
let u_type,new_eq=UF.generate_new_var env.type_equations in
let t_type,new_eq=UF.generate_new_constr new_eq (1,[u_type;ty_var]) in
Log.debug (fun m -> m "%sType inference of the parameter in an application:" prefix);
let _u_type,new_env=inference_aux (level+1) u u_type {env with type_equations=new_eq} in
Log.debug (fun m -> m "%sType inference of the functor in an application:" prefix);
let _t_type,new_env=inference_aux (level+1) t t_type new_env in
ty_var,new_env
| _ -> failwith "Bug: No principal typing algorithm for these types" in
let is_cyclic,new_eq=UF.cyclic ty new_env.type_equations in
if is_cyclic then
raise Not_typable
else
ty,{new_env with type_equations=new_eq}
let rec build_type i type_eq =
let (i,v),type_eq = UF.find i type_eq in
match v with
| UF.Link_to j when j=i -> Lambda.Atom(-i)
| UF.Link_to _ -> failwith "Bug: when UF.find returns a Link_to, it should be a Link_to itself"
| UF.Value _ -> failwith "Bug: when performing type inference for principal typing, no type constant should appear"
| UF.Constr (_c,[alpha;beta]) ->
let alpha'=build_type alpha type_eq in
let beta'=build_type beta type_eq in
Lambda.Fun(alpha',beta')
| UF.Constr _ -> failwith "Bug: when performing type inference for principal typing, the only allowd type construction is the arrow"
let inference t =
try
let vars=UF.empty in
let ty,vars=UF.generate_new_var vars in
let ty,env=inference_aux 0 t ty {empty_env with type_equations=vars} in
build_type ty env.type_equations,IntMap.map (fun (ty,i) -> Lambda.Const i,build_type ty env.type_equations) env.const_typing
with
| UF.Union_Failure -> raise Not_typable
end