Bidirectinnal type-checking

Needed for the PromCell example

typer.ml

@@ -51,8 +51,8 @@ let rec infer : tterm -> sty = function
   | Tconst (_, ty, _) -> ty
   | Tpar t -> infer t
   | Tapp (_, _, _, ty) -> ty
-  | Tabst (x, ty, t, rty) -> Starr (ty, rty)
-  | Tobj (ll, ty) -> ty
+  | Tabst (_, ty, _, rty) -> Starr (ty, rty)
+  | Tobj (_, ty) -> ty
   | Tsel (_, _, ty) -> ty
   | Tupd (_, _, _, ty) -> ty
   | Tcast (_, _, ty) -> ty
@@ -60,53 +60,149 @@ and infer_meth (Tmeth (_, _, _, ty)) = ty
 
 exception Subtype_checking_error of sty * sty
 
+let tcast t ty1 ty2 =
+  if eq ty1 ty2
+  then t
+  else (
+    if subtype ty1 ty2
+    then Tcast (t, ty1, ty2)
+    else raise (Subtype_checking_error (ty1, ty2)))
+
+exception Different_binder_types of ((label * smeth) list)
+
 let dummy_var = (Id "_self")
 
-let rec type_term env : sterm -> tterm = function
+(* type_check env ty t
+   checks that t is typable with type ty
+   and returns a tterm of type ty
+   corresponding to t with casts included. *)
+let rec type_check env ty : sterm -> tterm = function
+  | Svar (x, ty') -> tcast (Tvar (x, ty')) ty' ty
+  | Sconst (x, ty', def) -> tcast (Tconst (x, ty', type_check env ty' def)) ty' ty
+  | Spar t -> Tpar (type_check env ty t)
+  | Sapp (t1, t2) ->
+    (* We don't know what type should be associated with t2
+       so we infer a type for t1 and decompose it as an arrow *)
+    let tt1 = type_term env t1 in
+    let (ty1l, ty1r) = sty_decompose_arrow (infer tt1) in
+    (* Now we check that the application is typable at type ty *)
+    tcast (Tapp (tt1, type_check env ty1l t2, ty1l, ty1r)) ty1r ty
+  | Sabst (x, ty', body) ->
+    (* First decompose ty as an arrow *)
+    let (tyl, tyr) = sty_decompose_arrow ty in
+    if eq ty' tyl then
+      Tabst (x, tyl, type_check ((x, tyl) :: env) tyr body, tyr)
+    else
+      (* We use eta-expansion to cast the variable x. *)
+      Tabst (x, tyl, Tapp (Tabst (x, ty', type_check ((x, ty') :: env) tyr body, tyr),
+                           tcast (Tvar (x, tyl)) tyl ty',
+                           ty',
+                           tyr), tyr)
+  | Sobj [] -> let _ = type_check_object env ty [] in Tobj ([], ty)
+  | Sobj ((_, m) :: _ as ll) ->
+    let bty = type_meth_binder m in
+    let tll = type_check_object env bty ll in
+    tcast (Tobj (tll, bty)) bty ty
+  | Ssel (t, l) ->
+    let tt = type_term env t in
+    let ty1 = (
+      try sty_assoc l (infer tt)
+      with Not_found ->
+        (Format.eprintf "Term %s has no method named %s.@."
+          (string_of_sterm t) (string_of_label l); exit 1))
+    in
+    tcast (Tsel (tt, l, ty1)) ty1 ty
+  | Supd (t, l, m) ->
+    (* Warning, label l could appear in inferred type of t
+       but not in ty. This would be correct.
+       However, the binder in m tells us the expected type
+       which should contain l. *)
+    let ty1 = type_meth_binder m in
+    (* Now get the type that the method should return.
+       and check that the label is OK. *)
+    let rty = (
+      try sty_assoc l ty1
+      with Not_found ->
+        (Format.eprintf "Method %s cannot be associated with label %s: label not found in binder type@."
+           (string_of_smeth m) (string_of_label l); exit 1))
+    in
+    tcast (Tupd (type_check env ty1 t, l, type_check_meth env rty m, ty1)) ty1 ty
+  | Sfupd (t1, l, t2) ->
+    (* Here we have to infer the binder type from t1. *)
+    let tt1 = type_term env t1 in
+    let tty1 = infer tt1 in
+    (* Reduce to regular update case. *)
+    type_check env ty (Supd (t1, l, (Smeth (dummy_var, tty1, t2))))
+
+(* Check that an object has type ty as declared in its binders. *)
+and type_check_object env ty obj =
+  match ty with
+  | Stcid (_, b) -> type_check_object env b obj
+  | Starr _ ->
+    Format.eprintf "Trying to type an object with an arrow type@."; exit 1
+  | Stlist [] -> (
+    match obj with
+    | [] -> []
+    | (l, _) :: _ -> Format.eprintf "Method %s is not required@." (string_of_label l); exit 1)
+  | Stlist ((l, rty) :: lty) -> (
+    match obj with
+    | [] -> Format.eprintf "Missing method %s@." (string_of_label l); exit 1
+    | (l2, _) :: _ when l2 > l -> Format.eprintf "Missing method %s@." (string_of_label l); exit 1
+    | (l2, _) :: _ when l2 < l -> Format.eprintf "Method %s is not required@." (string_of_label l2); exit 1
+    | (_, m) :: ll ->
+      let tm = type_check_meth env rty m in
+      let tll = type_check_object env (Stlist lty) ll in
+      (l, tm) :: tll)
+
+and type_check_meth env rty (Smeth (x, bty, body)) = Tmeth (x, bty, type_check ((x, bty) :: env) rty body, rty)
+
+and type_term env : sterm -> tterm = function
   | Svar (x, ty) -> Tvar (x, ty)
-  | Sconst (x, ty, def) -> Tconst (x, ty, type_term env def)
+  | Sconst (x, ty, def) -> Tconst (x, ty, type_check env ty def)
   | Spar t -> Tpar (type_term env t)
   | Sapp (t1, t2) ->
     let tt1 = type_term env t1 in
-    let tt2 = type_term env t2 in
-    let ty1 = infer tt1 in
-    let (ty1l, ty1r) = sty_decompose_arrow ty1 in
-    let ty2 = infer tt2 in
-    if subtype ty2 ty1l then
-      Tapp (tt1, Tcast (tt2, ty2, ty1l), ty1l, ty1r)
-    else
-      raise (Subtype_checking_error (ty2, ty1l))
+    let (ty1l, ty1r) = sty_decompose_arrow (infer tt1) in
+    Tapp (tt1, type_check env ty1l t2, ty1l, ty1r)
   | Sabst (x, ty, body) ->
     let tbody = type_term ((x, ty) :: env) body in
     Tabst (x, ty, tbody, infer tbody)
-  | Sobj ll ->
-    let tmeths = List.map (fun (l, m) -> (l, type_meth env m)) ll in
-    Tobj (tmeths, Stlist (List.map (fun (l, m) -> (l, infer_meth m)) tmeths))
+  | Sobj [] -> Tobj ([], Stlist [])
+  | Sobj ((_, m) :: _ as ll) ->
+    let ty = type_meth_binder m in
+    Tobj (type_check_object env ty ll, ty)
   | Ssel (t, l) ->
     let tt = type_term env t in
-    let ty = infer tt in
-    Tsel (tt, l, sty_assoc l ty)
+    let ty1 = (
+      try sty_assoc l (infer tt)
+      with Not_found ->
+        Format.eprintf "Term %s has no method named %s.@."
+          (string_of_sterm t) (string_of_label l);
+        exit 1)
+    in
+    Tsel (tt, l, ty1)
   | Supd (t, l, m) ->
-    let tt = type_term env t in
-    let tty = infer tt in
-    let Tmeth (_, ty, _, rty) = type_meth env m in
-    let expected_rty = sty_assoc l ty in
-    if subtype tty ty then (
-      if subtype rty expected_rty then
-        Tupd (tt, l, type_meth env m, tty)
-      else
-        raise (Subtype_checking_error (rty, expected_rty)))
-    else
-      raise (Subtype_checking_error (tty, ty))
+    let ty1 = type_meth_binder m in
+    let rty = (
+      try sty_assoc l ty1
+      with Not_found ->
+        (Format.eprintf "Method %s cannot be associated with label %s: label not found in binder type@."
+          (string_of_smeth m) (string_of_label l); exit 1))
+    in
+    Tupd (type_check env ty1 t, l, type_check_meth env rty m, ty1)
   | Sfupd (t1, l, t2) ->
+    (* Here we have to infer the binder type from t1. *)
     let tt1 = type_term env t1 in
     let tty1 = infer tt1 in
-    let tt2 = type_term env t2 in
-    Tupd (tt1, l, Tmeth (dummy_var, tty1, tt2, infer tt2), tty1)
+    (* Reduce to regular update case. *)
+    type_term env (Supd (t1, l, (Smeth (dummy_var, tty1, t2))))
+
 and type_meth env (Smeth (x, ty, body)) =
   let tbody = type_term ((x, ty) :: env) body in
   (Tmeth (x, ty, tbody, infer tbody))
 
+and type_meth_binder (Smeth (x, ty, body)) = ty
+
 exception Check_failed
 
 let type_line = function