MatchClause

src/TypeInference/Error.ml

@@ -209,7 +209,7 @@ let method_effect_mismatch ~pos ~env eff1 eff2 =
     (Pretty.type_to_string pp_ctx env eff1)
     (Pretty.type_to_string pp_ctx env eff2)
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
-
+*)
 let return_type_mismatch ~pos ~env tp1 tp2 =
   let pp_ctx = Pretty.empty_context () in
   let msg = Printf.sprintf
@@ -226,14 +226,6 @@ let finally_type_mismatch ~pos ~env tp1 tp2 =
     (Pretty.type_to_string pp_ctx env tp2)
   in (pos, msg ^ Pretty.additional_info pp_ctx, [])
 
-let finally_effect_mismatch ~pos ~env eff1 eff2 =
-  let pp_ctx = Pretty.empty_context () in
-  let msg = Printf.sprintf
-    "Finally clause has effect %s, which is not a supereffect of the delimiter's effect %s"
-    (Pretty.type_to_string pp_ctx env eff2)
-    (Pretty.type_to_string pp_ctx env eff1)
-  in (pos, msg ^ Pretty.additional_info pp_ctx, [])
-*)
 let func_not_pure ~pos =
   (pos, "Cannot ensure that this function is pure and always terminates", [])
 

src/TypeInference/Error.mli

@@ -64,14 +64,12 @@ val func_effect_mismatch :
 
 val method_effect_mismatch :
   pos:Position.t -> env:Env.t -> T.effrow -> T.effrow -> t
-
+*)
 val return_type_mismatch :
   pos:Position.t -> env:Env.t -> T.typ -> T.typ -> t
 val finally_type_mismatch :
   pos:Position.t -> env:Env.t -> T.typ -> T.typ -> t
-val finally_effect_mismatch :
-  pos:Position.t -> env:Env.t -> T.effrow -> T.effrow -> t
-*)
+
 val func_not_pure : pos:Position.t -> t
 val impure_handler : pos:Position.t -> t
 (*

src/TypeInference/MatchClause.ml

@@ -3,59 +3,27 @@
  *)
 
 (** Type-inference for match clauses and related constructs *)
-(*
+
 open Common
 open TypeCheckFix
 
-let check_match_clause ~tcfix env tp (cl : S.match_clause) res_tp res_eff =
+let check_match_clause ~tcfix env tp (cl : S.match_clause) res_tp =
   let open (val tcfix : TCFix) in
   match cl.data with
   | Clause(pat, body) ->
-    let scope = Env.scope env in
-    let (env, pat, _, r_eff1) = Pattern.check_type ~env ~scope pat tp in
-    let (body, r_eff2) = check_expr_type env body res_tp res_eff in
-    (pat, body, ret_effect_join r_eff1 r_eff2)
-*)
-let check_match_clauses ~tcfix env tp cls res_tp =
-  (* TODO: not implemented *)
-  begin match None with Some x -> x end
-(*
-  let (r_eff, cls) = List.fold_left_map
-    (fun r_eff1 cl ->
-      let (pat, body, r_eff2) =
-        check_match_clause ~tcfix env tp cl res_tp res_eff in
-      (ret_effect_join r_eff1 r_eff2, (pat, body)))
-    Pure
-    cls
-  in
-  (cls, r_eff)
+    let (env, pat, eff) = Pattern.check_type_ext env pat tp in
+    let er = check_expr_type env body res_tp in
+    (pat, er.er_expr, T.Effect.join eff er.er_effect, er.er_constr)
 
-(* ------------------------------------------------------------------------- *)
-(** Make pattern-matching expression for given non-empty clause list (the
-  meaning of parameters is the same as for [check_match_clauses]). It returns
-  fresh variable [x], and match-expression that matches [x] against given list
-  of clauses. *)
-let make_nonempty_match ~tcfix env tp cls res_tp res_eff =
-  let pos =
-    match cls with
-    | [] -> assert false
-    | cl :: cls ->
-      let p1 = cl.S.pos in
-      let p2 = List.fold_left (fun _ cl -> cl.S.pos) p1 cls in
-      Position.join p1 p2
+let check_match_clauses ~tcfix env tp cls res_tp =
+  let check (eff1, cs1) cl =
+    let (pat, body, eff2, cs2) = check_match_clause ~tcfix env tp cl res_tp in
+    let eff = T.Effect.join eff1 eff2 in
+    let cs = cs1 @ cs2 in
+    ((eff, cs), (pat, body))
   in
-  let (cls, r_eff) = check_match_clauses ~tcfix env tp cls res_tp res_eff in
-  let meff = match_effect r_eff res_eff in
-  let x = Var.fresh () in
-  let body =
-    { T.pos;
-      T.data = T.EMatch({ pos; data = T.EVar x }, cls, res_tp, meff) }
-  in (x, body)
-
-(* ------------------------------------------------------------------------- *)
-let default_clause ~pos res1 res2 =
-  let x = Var.fresh () in
-  (x, res1, { T.pos; T.data = T.EVar x }, res2)
+  let ((eff, cs), cls) = List.fold_left_map check (T.Pure, []) cls in
+  (cls, eff, cs)
 
 let guess_type (type d) env (req : (_, d) request) : _ * (_, d) response =
   match req with
@@ -64,31 +32,48 @@ let guess_type (type d) env (req : (_, d) request) : _ * (_, d) response =
     let tp = Env.fresh_uvar env T.Kind.k_type in
     (tp, Infered tp)
 
-let tr_opt_clauses (type md rd) ~tcfix ~pos env
-  (mtp_req : (_, md) request) cls (rtp_req : (_, rd) request) eff ~on_error :
-    _ * (_, md) response * _ * (_, rd) response =
-  match mtp_req, cls, rtp_req with
-  | Check tp, [], Infer ->
-    default_clause ~pos Checked (Infered tp)
-  | Infer, [], Check tp ->
-    default_clause ~pos (Infered tp) Checked
-  | Infer, [], Infer ->
-    let tp = Env.fresh_uvar env T.Kind.k_type in
-    default_clause ~pos (Infered tp) (Infered tp)
-  | Check tp1, [], Check tp2 ->
-    Error.check_unify_result ~pos (Unification.subtype env tp1 tp2) ~on_error;
-    default_clause ~pos Checked Checked
-  | _ ->
-    let (mtp, mtp_resp) = guess_type env mtp_req in
-    let (rtp, rtp_resp) = guess_type env rtp_req in
-    let (x, body) = make_nonempty_match ~tcfix env mtp cls rtp eff in
-    (x, mtp_resp, body, rtp_resp)
-*)
+let tr_opt_clauses (type dir) ~tcfix ~pos env tp_in cls
+    (rtp_req : (_, dir) request) ~(on_error : pos:_ -> _) :
+    _ * dir expr_result =
+  let x = Var.fresh () in
+  let make data = { T.pos; data } in
+  let x_expr = make (T.EInst(make (T.EVar x), [], [])) in
+  match cls, rtp_req with
+  | [], Infer ->
+    let er =
+      { er_expr   = x_expr;
+        er_type   = Infered tp_in;
+        er_effect = T.Pure;
+        er_constr = []
+      }
+    in (x, er)
+
+  | [], Check tp_out ->
+    Error.check_unify_result ~pos (Unification.subtype env tp_in tp_out)
+      ~on_error:(on_error tp_in tp_out);
+    let er =
+      { er_expr   = x_expr;
+        er_type   = Checked;
+        er_effect = T.Pure;
+        er_constr = []
+      }
+    in (x, er)
+
+  | _ :: _, _ ->
+    let (tp, tp_resp) = guess_type env rtp_req in
+    let (cls, eff, cs) = check_match_clauses ~tcfix env tp_in cls tp in
+    let er =
+      { er_expr   = make (T.EMatch(x_expr, cls, tp, eff));
+        er_type   = tp_resp;
+        er_effect = eff;
+        er_constr = cs
+      }
+    in (x, er)
 
 let tr_return_clauses ~tcfix ~pos env tp_in cls rtp_req =
-  (* TODO: not implemented *)
-  begin match None with Some x -> x end
+  tr_opt_clauses ~tcfix ~pos env tp_in cls rtp_req
+    ~on_error:(Error.return_type_mismatch ~env)
 
 let tr_finally_clauses ~tcfix ~pos env tp_in cls rtp_req =
-  (* TODO: not implemented *)
-  begin match None with Some x -> x end
+  tr_opt_clauses ~tcfix ~pos env tp_in cls rtp_req
+    ~on_error:(Error.finally_type_mismatch ~env)