| 4 |
open Location |
open Location |
| 5 |
open Ast |
open Ast |
| 6 |
|
|
|
exception Pattern of string |
|
| 7 |
exception NonExhaustive of Types.descr |
exception NonExhaustive of Types.descr |
| 8 |
exception MultipleLabel of Types.label |
exception MultipleLabel of Types.label |
| 9 |
exception Constraint of Types.descr * Types.descr * string |
exception Constraint of Types.descr * Types.descr * string |
| 43 |
module StringMap = Map.Make(S) |
module StringMap = Map.Make(S) |
| 44 |
module StringSet = Set.Make(S) |
module StringSet = Set.Make(S) |
| 45 |
|
|
| 46 |
|
type glb = ti StringMap.t |
| 47 |
|
|
| 48 |
let mk' = |
let mk' = |
| 49 |
let counter = ref 0 in |
let counter = ref 0 in |
| 50 |
fun loc -> |
fun loc -> |
| 97 |
| `Star of flat |
| `Star of flat |
| 98 |
| `WeakStar of flat ] |
| `WeakStar of flat ] |
| 99 |
|
|
| 100 |
|
let re_loc = ref noloc |
| 101 |
|
|
| 102 |
let rec propagate vars : regexp -> flat = function |
let rec propagate vars : regexp -> flat = function |
| 103 |
| Epsilon -> `Epsilon |
| Epsilon -> `Epsilon |
| 104 |
| Elem x -> let p = vars x in `Elem (uniq_id (),p) |
| Elem x -> let p = vars x in `Elem (uniq_id (),p) |
| 107 |
| Star r -> `Star (propagate vars r) |
| Star r -> `Star (propagate vars r) |
| 108 |
| WeakStar r -> `WeakStar (propagate vars r) |
| WeakStar r -> `WeakStar (propagate vars r) |
| 109 |
| SeqCapture (v,x) -> |
| SeqCapture (v,x) -> |
| 110 |
let v= mk noloc (Capture v) in |
let v= mk !re_loc (Capture v) in |
| 111 |
propagate (fun p -> mk noloc (And (vars p,v,true))) x |
propagate (fun p -> mk !re_loc (And (vars p,v,true))) x |
| 112 |
|
|
| 113 |
let cup r1 r2 = |
let cup r1 r2 = |
| 114 |
match (r1,r2) with |
match (r1,r2) with |
| 115 |
| (_, `Empty) -> r1 |
| (_, `Empty) -> r1 |
| 116 |
| (`Empty, _) -> r2 |
| (`Empty, _) -> r2 |
| 117 |
| (`Res t1, `Res t2) -> `Res (mk noloc (Or (t1,t2))) |
| (`Res t1, `Res t2) -> `Res (mk !re_loc (Or (t1,t2))) |
| 118 |
|
|
| 119 |
(*TODO: review this compilation schema to avoid explosion when |
(*TODO: review this compilation schema to avoid explosion when |
| 120 |
coding (Optional x) by (Or(Epsilon,x)); memoization ... *) |
coding (Optional x) by (Or(Epsilon,x)); memoization ... *) |
| 133 |
| `Epsilon :: rest -> |
| `Epsilon :: rest -> |
| 134 |
compile fin e rest |
compile fin e rest |
| 135 |
| `Elem (_,p) :: rest -> |
| `Elem (_,p) :: rest -> |
| 136 |
`Res (mk noloc (Prod (p, guard_compile fin rest))) |
`Res (mk !re_loc (Prod (p, guard_compile fin rest))) |
| 137 |
| `Seq (r1,r2) :: rest -> |
| `Seq (r1,r2) :: rest -> |
| 138 |
compile fin e (r1 :: r2 :: rest) |
compile fin e (r1 :: r2 :: rest) |
| 139 |
| `Alt (r1,r2) :: rest -> |
| `Alt (r1,r2) :: rest -> |
| 148 |
with |
with |
| 149 |
Not_found -> |
Not_found -> |
| 150 |
let n = name () in |
let n = name () in |
| 151 |
let v = mk noloc (PatVar n) in |
let v = mk !re_loc (PatVar n) in |
| 152 |
memo := Memo.add seq v !memo; |
memo := Memo.add seq v !memo; |
| 153 |
let d = compile fin (ref Coind.empty) seq in |
let d = compile fin (ref Coind.empty) seq in |
| 154 |
(match d with |
(match d with |
| 158 |
|
|
| 159 |
|
|
| 160 |
let constant_nil v t = |
let constant_nil v t = |
| 161 |
mk noloc (And (t, (mk noloc (Constant (v, Types.Atom Sequence.nil_atom))), true)) |
mk !re_loc |
| 162 |
|
(And (t, |
| 163 |
|
(mk !re_loc (Constant (v, Types.Atom Sequence.nil_atom))), true)) |
| 164 |
|
|
| 165 |
let compile regexp queue : ppat = |
let compile loc regexp queue : ppat = |
| 166 |
|
re_loc := loc; |
| 167 |
let vars = seq_vars StringSet.empty regexp in |
let vars = seq_vars StringSet.empty regexp in |
| 168 |
let fin = StringSet.fold constant_nil vars queue in |
let fin = StringSet.fold constant_nil vars queue in |
| 169 |
let n = guard_compile fin [propagate (fun p -> p) regexp] in |
let n = guard_compile fin [propagate (fun p -> p) regexp] in |
| 170 |
memo := Memo.empty; |
memo := Memo.empty; |
| 171 |
let d = !defs in |
let d = !defs in |
| 172 |
defs := []; |
defs := []; |
| 173 |
mk noloc (Recurs (n,d)) |
mk !re_loc (Recurs (n,d)) |
| 174 |
end |
end |
| 175 |
|
|
| 176 |
let compile_regexp = Regexp.compile |
let compile_regexp = Regexp.compile noloc |
| 177 |
|
|
| 178 |
|
|
| 179 |
let rec compile env { loc = loc; descr = d } : ti = |
let rec compile env { loc = loc; descr = d } : ti = |
| 181 |
| PatVar s -> |
| PatVar s -> |
| 182 |
(try StringMap.find s env |
(try StringMap.find s env |
| 183 |
with Not_found -> |
with Not_found -> |
| 184 |
raise_loc loc (Pattern ("Undefined type variable " ^ s)) |
raise_loc_generic loc ("Undefined type variable " ^ s) |
| 185 |
) |
) |
| 186 |
| Recurs (t, b) -> compile (compile_many env b) t |
| Recurs (t, b) -> compile (compile_many env b) t |
| 187 |
| Regexp (r,q) -> compile env (Regexp.compile r q) |
| Regexp (r,q) -> compile env (Regexp.compile loc r q) |
| 188 |
| Internal t -> cons loc (`Type t) |
| Internal t -> cons loc (`Type t) |
| 189 |
| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2)) |
| Or (t1,t2) -> cons loc (`Or (compile env t1, compile env t2)) |
| 190 |
| And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e)) |
| And (t1,t2,e) -> cons loc (`And (compile env t1, compile env t2,e)) |
| 202 |
List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b; |
List.iter (fun (v,t,x) -> x.descr' <- `Alias (v, compile env t)) b; |
| 203 |
env |
env |
| 204 |
|
|
|
|
|
| 205 |
let comp_fv_seen = ref [] |
let comp_fv_seen = ref [] |
| 206 |
let comp_fv_res = ref [] |
let comp_fv_res = ref [] |
| 207 |
let rec comp_fv s = |
let rec comp_fv s = |
| 240 |
match s.descr' with |
match s.descr' with |
| 241 |
| `Alias (v,x) -> |
| `Alias (v,x) -> |
| 242 |
if List.memq s seen then |
if List.memq s seen then |
| 243 |
raise_loc s.loc' |
raise_loc_generic s.loc' |
| 244 |
(Pattern |
("Unguarded recursion on variable " ^ v ^ " in this type") |
|
("Unguarded recursion on variable " ^ v ^ " in this type")) |
|
| 245 |
else typ (s :: seen) x |
else typ (s :: seen) x |
| 246 |
| `Type t -> t |
| `Type t -> t |
| 247 |
| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2) |
| `Or (s1,s2) -> Types.cup (typ seen s1) (typ seen s2) |
| 270 |
|
|
| 271 |
let rec pat seen s : Patterns.descr = |
let rec pat seen s : Patterns.descr = |
| 272 |
if fv s = [] then Patterns.constr (type_node s) else |
if fv s = [] then Patterns.constr (type_node s) else |
| 273 |
match s.descr' with |
try pat_aux seen s |
| 274 |
|
with Patterns.Error e -> raise_loc_generic s.loc' e |
| 275 |
|
| Location (loc,exn) when loc = noloc -> raise (Location (s.loc', exn)) |
| 276 |
|
|
| 277 |
|
|
| 278 |
|
and pat_aux seen s = match s.descr' with |
| 279 |
| `Alias (v,x) -> |
| `Alias (v,x) -> |
| 280 |
if List.memq s seen then |
if List.memq s seen |
| 281 |
raise_loc s.loc' |
then raise |
| 282 |
(Pattern |
(Patterns.Error |
| 283 |
("Unguarded recursion on variable " ^ v ^ " in this pattern")) |
("Unguarded recursion on variable " ^ v ^ " in this pattern")); |
| 284 |
else pat (s :: seen) x |
pat (s :: seen) x |
| 285 |
| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2) |
| `Or (s1,s2) -> Patterns.cup (pat seen s1) (pat seen s2) |
| 286 |
| `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e |
| `And (s1,s2,e) -> Patterns.cap (pat seen s1) (pat seen s2) e |
| 287 |
| `Diff (s1,s2) when fv s2 = [] -> |
| `Diff (s1,s2) when fv s2 = [] -> |
| 288 |
let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in |
let s2 = Types.cons (Types.neg (Types.descr (type_node s2)))in |
| 289 |
Patterns.cap (pat seen s1) (Patterns.constr s2) true |
Patterns.cap (pat seen s1) (Patterns.constr s2) true |
| 290 |
| `Diff _ -> |
| `Diff _ -> |
| 291 |
raise_loc s.loc' (Pattern "Difference not allowed in patterns") |
raise (Patterns.Error "Difference not allowed in patterns") |
| 292 |
| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2) |
| `Times (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2) |
| 293 |
| `Record (l,false,s) -> Patterns.record l (pat_node s) |
| `Record (l,false,s) -> Patterns.record l (pat_node s) |
| 294 |
| `Record _ -> |
| `Record _ -> |
| 295 |
raise_loc s.loc' |
raise (Patterns.Error "Optional field not allowed in record patterns") |
|
(Pattern "Optional field not allowed in record patterns") |
|
| 296 |
| `Capture x -> Patterns.capture x |
| `Capture x -> Patterns.capture x |
| 297 |
| `Constant (x,c) -> Patterns.constant x c |
| `Constant (x,c) -> Patterns.constant x c |
| 298 |
| `Arrow _ -> |
| `Arrow _ -> |
| 299 |
raise_loc s.loc' (Pattern "Arrow not allowed in patterns") |
raise (Patterns.Error "Arrow not allowed in patterns") |
| 300 |
| `Type _ -> assert false |
| `Type _ -> assert false |
| 301 |
|
|
| 302 |
and pat_node s : Patterns.node = |
and pat_node s : Patterns.node = |
| 309 |
Patterns.define x t; |
Patterns.define x t; |
| 310 |
x |
x |
| 311 |
|
|
|
let global_types = State.ref "Typer.global_types" StringMap.empty |
|
|
|
|
| 312 |
let mk_typ e = |
let mk_typ e = |
| 313 |
if fv e = [] then type_node e |
if fv e = [] then type_node e |
| 314 |
else raise_loc e.loc' (Pattern "Capture variables are not allowed in types") |
else raise_loc_generic e.loc' "Capture variables are not allowed in types" |
| 315 |
|
|
| 316 |
|
|
| 317 |
|
let typ glb e = |
| 318 |
|
mk_typ (compile glb e) |
| 319 |
|
|
| 320 |
let typ e = |
let pat glb e = |
| 321 |
mk_typ (compile !global_types e) |
pat_node (compile glb e) |
| 322 |
|
|
| 323 |
let pat e = |
let register_global_types glb b = |
| 324 |
let e = compile !global_types e in |
let env' = compile_many glb b in |
| 325 |
pat_node e |
List.fold_left |
| 326 |
|
(fun glb (v,{ loc = loc }) -> |
| 327 |
let register_global_types b = |
let t = StringMap.find v env' in |
|
let env = compile_many !global_types b in |
|
|
List.iter (fun (v,_) -> |
|
|
let t = StringMap.find v env in |
|
|
if StringMap.mem v !global_types then |
|
|
raise |
|
|
(Location.Generic ("Multiple definition for type " ^ v)); |
|
|
global_types := StringMap.add v t !global_types; |
|
| 328 |
let d = Types.descr (mk_typ t) in |
let d = Types.descr (mk_typ t) in |
| 329 |
(* let d = Types.normalize d in*) |
(* let d = Types.normalize d in*) |
| 330 |
Types.Print.register_global v d; |
Types.Print.register_global v d; |
| 331 |
() |
if StringMap.mem v glb |
| 332 |
) b |
then raise_loc_generic loc ("Multiple definition for type " ^ v); |
| 333 |
|
StringMap.add v t glb |
| 334 |
|
) glb b |
| 335 |
|
|
| 336 |
|
|
| 337 |
|
|
| 338 |
(* II. Build skeleton *) |
(* II. Build skeleton *) |
| 339 |
|
|
| 340 |
module Fv = StringSet |
module Fv = StringSet |
| 341 |
|
|
| 342 |
let rec expr { loc = loc; descr = d } = |
let rec expr glb { loc = loc; descr = d } = |
| 343 |
let (fv,td) = |
let (fv,td) = |
| 344 |
match d with |
match d with |
|
| DebugTyper t -> (Fv.empty, Typed.DebugTyper (typ t)) |
|
| 345 |
| Forget (e,t) -> |
| Forget (e,t) -> |
| 346 |
let (fv,e) = expr e and t = typ t in |
let (fv,e) = expr glb e and t = typ glb t in |
| 347 |
(fv, Typed.Forget (e,t)) |
(fv, Typed.Forget (e,t)) |
| 348 |
| Var s -> (Fv.singleton s, Typed.Var s) |
| Var s -> (Fv.singleton s, Typed.Var s) |
| 349 |
| Apply (e1,e2) -> |
| Apply (e1,e2) -> |
| 350 |
let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in |
let (fv1,e1) = expr glb e1 and (fv2,e2) = expr glb e2 in |
| 351 |
(Fv.union fv1 fv2, Typed.Apply (e1,e2)) |
(Fv.union fv1 fv2, Typed.Apply (e1,e2)) |
| 352 |
| Abstraction a -> |
| Abstraction a -> |
| 353 |
let iface = List.map (fun (t1,t2) -> (typ t1, typ t2)) a.fun_iface in |
let iface = List.map (fun (t1,t2) -> (typ glb t1, typ glb t2)) |
| 354 |
|
a.fun_iface in |
| 355 |
let t = List.fold_left |
let t = List.fold_left |
| 356 |
(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) |
(fun accu (t1,t2) -> Types.cap accu (Types.arrow t1 t2)) |
| 357 |
Types.any iface in |
Types.any iface in |
| 358 |
let iface = List.map |
let iface = List.map |
| 359 |
(fun (t1,t2) -> (Types.descr t1, Types.descr t2)) |
(fun (t1,t2) -> (Types.descr t1, Types.descr t2)) |
| 360 |
iface in |
iface in |
| 361 |
let (fv0,body) = branches a.fun_body in |
let (fv0,body) = branches glb a.fun_body in |
| 362 |
let fv = match a.fun_name with |
let fv = match a.fun_name with |
| 363 |
| None -> fv0 |
| None -> fv0 |
| 364 |
| Some f -> Fv.remove f fv0 in |
| Some f -> Fv.remove f fv0 in |
| 373 |
) |
) |
| 374 |
| Cst c -> (Fv.empty, Typed.Cst c) |
| Cst c -> (Fv.empty, Typed.Cst c) |
| 375 |
| Pair (e1,e2) -> |
| Pair (e1,e2) -> |
| 376 |
let (fv1,e1) = expr e1 and (fv2,e2) = expr e2 in |
let (fv1,e1) = expr glb e1 and (fv2,e2) = expr glb e2 in |
| 377 |
(Fv.union fv1 fv2, Typed.Pair (e1,e2)) |
(Fv.union fv1 fv2, Typed.Pair (e1,e2)) |
| 378 |
| Dot (e,l) -> |
| Dot (e,l) -> |
| 379 |
let (fv,e) = expr e in |
let (fv,e) = expr glb e in |
| 380 |
(fv, Typed.Dot (e,l)) |
(fv, Typed.Dot (e,l)) |
| 381 |
| RecordLitt r -> |
| RecordLitt r -> |
| 382 |
let fv = ref Fv.empty in |
let fv = ref Fv.empty in |
| 383 |
let r = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in |
let r = List.sort (fun (l1,_) (l2,_) -> compare l1 l2) r in |
| 384 |
let r = List.map |
let r = List.map |
| 385 |
(fun (l,e) -> |
(fun (l,e) -> |
| 386 |
let (fv2,e) = expr e in fv := Fv.union !fv fv2; (l,e)) |
let (fv2,e) = expr glb e in fv := Fv.union !fv fv2; (l,e)) |
| 387 |
r in |
r in |
| 388 |
let rec check = function |
let rec check = function |
| 389 |
| (l1,_) :: (l2,_) :: _ when l1 = l2 -> |
| (l1,_) :: (l2,_) :: _ when l1 = l2 -> |
| 393 |
check r; |
check r; |
| 394 |
(!fv, Typed.RecordLitt r) |
(!fv, Typed.RecordLitt r) |
| 395 |
| Op (op,le) -> |
| Op (op,le) -> |
| 396 |
let (fvs,ltes) = List.split (List.map expr le) in |
let (fvs,ltes) = List.split (List.map (expr glb) le) in |
| 397 |
let fv = List.fold_left Fv.union Fv.empty fvs in |
let fv = List.fold_left Fv.union Fv.empty fvs in |
| 398 |
(fv, Typed.Op (op,ltes)) |
(fv, Typed.Op (op,ltes)) |
| 399 |
| Match (e,b) -> |
| Match (e,b) -> |
| 400 |
let (fv1,e) = expr e |
let (fv1,e) = expr glb e |
| 401 |
and (fv2,b) = branches b in |
and (fv2,b) = branches glb b in |
| 402 |
(Fv.union fv1 fv2, Typed.Match (e, b)) |
(Fv.union fv1 fv2, Typed.Match (e, b)) |
| 403 |
| Map (e,b) -> |
| Map (e,b) -> |
| 404 |
let (fv1,e) = expr e |
let (fv1,e) = expr glb e |
| 405 |
and (fv2,b) = branches b in |
and (fv2,b) = branches glb b in |
| 406 |
(Fv.union fv1 fv2, Typed.Map (e, b)) |
(Fv.union fv1 fv2, Typed.Map (e, b)) |
| 407 |
| Try (e,b) -> |
| Try (e,b) -> |
| 408 |
let (fv1,e) = expr e |
let (fv1,e) = expr glb e |
| 409 |
and (fv2,b) = branches b in |
and (fv2,b) = branches glb b in |
| 410 |
(Fv.union fv1 fv2, Typed.Try (e, b)) |
(Fv.union fv1 fv2, Typed.Try (e, b)) |
| 411 |
in |
in |
| 412 |
fv, |
fv, |
| 415 |
Typed.exp_descr = td; |
Typed.exp_descr = td; |
| 416 |
} |
} |
| 417 |
|
|
| 418 |
and branches b = |
and branches glb b = |
| 419 |
let fv = ref Fv.empty in |
let fv = ref Fv.empty in |
| 420 |
let accept = ref Types.empty in |
let accept = ref Types.empty in |
| 421 |
let b = List.map |
let b = List.map |
| 422 |
(fun (p,e) -> |
(fun (p,e) -> |
| 423 |
let (fv2,e) = expr e in |
let (fv2,e) = expr glb e in |
| 424 |
let p = pat p in |
let p = pat glb p in |
| 425 |
let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in |
let fv2 = List.fold_right Fv.remove (Patterns.fv p) fv2 in |
| 426 |
fv := Fv.union !fv fv2; |
fv := Fv.union !fv fv2; |
| 427 |
accept := Types.cup !accept (Types.descr (Patterns.accept p)); |
accept := Types.cup !accept (Types.descr (Patterns.accept p)); |
| 438 |
} |
} |
| 439 |
) |
) |
| 440 |
|
|
| 441 |
let let_decl p e = |
let let_decl glb p e = |
| 442 |
let (_,e) = expr e in |
let (_,e) = expr glb e in |
| 443 |
{ Typed.let_pat = pat p; |
{ Typed.let_pat = pat glb p; |
| 444 |
Typed.let_body = e; |
Typed.let_body = e; |
| 445 |
Typed.let_compiled = None } |
Typed.let_compiled = None } |
| 446 |
|
|
| 634 |
type_check env e Types.any true |
type_check env e Types.any true |
| 635 |
|
|
| 636 |
and compute_type' loc env = function |
and compute_type' loc env = function |
|
| DebugTyper t -> Types.descr t |
|
| 637 |
| Var s -> |
| Var s -> |
| 638 |
(try Env.find s env |
(try Env.find s env |
| 639 |
with Not_found -> raise_loc loc (UnboundId s) |
with Not_found -> raise_loc loc (UnboundId s) |