Commit faad9851 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Still missing

parent 19d51a76
......@@ -111,6 +111,22 @@ let rec type_check env ty : sterm -> tterm = function
tcast (Tvar (x, tyl)) tyl ty',
ty',
tyr), tyr)
| Strue ty' -> (match ty with
| Stbool ty when eq ty ty' -> Ttrue ty
| _ -> Format.eprintf "Type error: error while checking true %s against %s,
expected Bool %s.@."
(string_of_sty ty') (string_of_sty ty) (string_of_sty ty');
exit 1)
| Sfalse ty' -> (match ty with
| Stbool ty when eq ty ty' -> Tfalse ty
| _ -> Format.eprintf "Type error: error while checking false %s against %s,
expected Bool %s.@."
(string_of_sty ty') (string_of_sty ty) (string_of_sty ty');
exit 1)
| Sif (b, t, e) -> Tif (type_check env (Stbool ty) b,
type_check env ty t,
type_check env ty e,
ty)
| Sobj [] -> let _ = type_check_object env ty [] in Tobj ([], ty)
| Sobj ((_, m) :: _ as ll) ->
let bty = type_meth_binder m in
......@@ -182,6 +198,15 @@ and type_term env : sterm -> tterm = function
| Sabst (x, ty, body) ->
let tbody = type_term ((x, ty) :: env) body in
Tabst (x, ty, tbody, infer tbody)
| Strue ty -> Ttrue ty
| Sfalse ty -> Tfalse ty
| Sif (b, t, e) ->
let tb = type_term env b in
let tyb = infer tb in
(match tyb with
| Stbool ty -> Tif (tb, type_check env ty t, type_check env ty e, ty)
| _ -> Format.eprintf "Type error: error while inferring the type of %s,
expecting a boolean.@." (string_of_sterm b); exit 1)
| Sobj [] -> Tobj ([], Stlist [])
| Sobj ((_, m) :: _ as ll) ->
let ty = type_meth_binder m in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment