commiut

src/lib/ast_util.ml

@@ -1619,7 +1619,11 @@ let destruct_pexp (Pat_aux (pexp, ann)) =
   | Pat_when (pat, guard, exp) -> (pat, Some guard, exp, ann)
 
 let construct_pexp (pat, guard, exp, ann) =
-  match guard with None -> Pat_aux (Pat_exp (pat, exp), ann) | Some guard -> Pat_aux (Pat_when (pat, guard, exp), ann)
+  match guard with 
+  | None -> 
+    Pat_aux (Pat_exp (pat, exp), ann) 
+  | Some guard -> 
+    Pat_aux (Pat_when (pat, guard, exp), ann)
 
 let destruct_mpexp (MPat_aux (mpexp, ann)) =
   match mpexp with MPat_pat mpat -> (mpat, None, ann) | MPat_when (mpat, guard) -> (mpat, Some guard, ann)

src/lib/parse_ast.ml

@@ -383,6 +383,53 @@ and mapcl_aux =
   | MCL_forwards of pexp
   | MCL_backwards of pexp
 
+let rec pat_of_mpat mpat =
+  match mpat with
+  | MP_aux (mpat_aux, l) ->
+      let res =
+        match mpat_aux with
+        | MP_lit lit -> P_lit lit
+        | MP_id id -> P_id id
+        | MP_app (id, mpat_list) -> P_app (id, List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_vector mpat_list -> P_vector (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_vector_concat mpat_list -> P_vector_concat (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_vector_subrange (id, l, r) -> P_vector_subrange (id, l, r)
+        | MP_tuple mpat_list -> P_tuple (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_list mpat_list -> P_list (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_cons (mpat1, mpat2) -> P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2)
+        | MP_string_append mpat_list -> P_string_append (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+        | MP_typ (mp1, atyp) -> P_typ (atyp, pat_of_mpat mp1)
+        | MP_struct id_mpat_list ->
+            let fp_of_id_mpat (id, mpat) = FP_aux (FP_field (id, pat_of_mpat mpat), l) in
+            let fpl = List.map fp_of_id_mpat id_mpat_list in
+            P_struct fpl
+        | MP_as (mpat, id) -> (
+            match pat_of_mpat mpat with P_aux (pat, _id) -> pat
+          )
+      in
+      P_aux (res, l)
+
+let mpat_of_mpexp = function
+  | MPat_aux (mpexp_aux, l) -> (
+      match mpexp_aux with MPat_pat mpat | MPat_when (mpat, _) -> mpat
+    )
+
+let pat_of_pexp = function
+  | Pat_aux (pexp_aux, _l) -> (
+      match pexp_aux with Pat_exp (pat, _exp) -> pat | Pat_when (pat, _e1, _e2) -> pat
+    )
+
+let rec pat_of_mapcl = function
+  | MCL_aux (mapcl_aux, l) -> (
+      match mapcl_aux with
+      | MCL_attribute (_s, _attr_data_option, MCL_aux (mapcl_aux, l)) -> pat_of_mapcl (MCL_aux (mapcl_aux, l))
+      | MCL_doc (_, MCL_aux (mapcl_aux, l)) -> pat_of_mapcl (MCL_aux (mapcl_aux, l))
+      | MCL_bidir (mpexp1, mpexp2) -> pat_of_mpat (mpat_of_mpexp mpexp1)
+      | MCL_forwards_deprecated (mpexp, _exp) -> pat_of_mpat (mpat_of_mpexp mpexp)
+      | MCL_forwards mpexp -> pat_of_pexp mpexp
+      | MCL_backwards mpexp -> pat_of_pexp mpexp
+    )
+
 type mapdef_aux =
   (* mapping definition (bidirectional pattern-match function) *)
   | MD_mapping of id * typschm_opt * mapcl list

src/lib/pattern_completeness.ml

@@ -67,6 +67,7 @@
 
 open Ast
 open Ast_util
+module P = Parse_ast
 module Big_int = Nat_big_num
 
 module IntSet = Util.IntSet
@@ -351,6 +352,7 @@ module Make (C : Config) = struct
     List.iter (fun (_, Columns c) -> prerr_endline (Util.string_of_list ", " _string_of_gpat c)) rs
   [@@@coverage on]
 
+  (* mark *)
   let rec generalize ctx head_exp_typ (P_aux (p_aux, (l, (_, pnum))) as pat) =
     let typ = typ_of_pat pat in
     match p_aux with
@@ -894,6 +896,7 @@ module Make (C : Config) = struct
     | [] -> (have_guard, [])
     | Pat_aux (Pat_exp ((P_aux (_, (l, _)) as pat), _), _) :: cases ->
         let pat, from = number_pat from pat in
+        (* number 在这里进入 *)
         let have_guard, pats = cases_to_pats from have_guard cases in
         (have_guard, (l, pat) :: pats)
     (* We don't consider guarded cases *)
@@ -907,9 +910,33 @@ module Make (C : Config) = struct
     | _, (Pat_aux (Pat_when _, _) as case) :: cases -> case :: update_cases l new_pats cases
     | _, _ -> Reporting.unreachable l __POS__ "Impossible case in update_cases" [@coverage off]
 
-  let is_complete_wildcarded ?(keyword = "match") l ctx cases head_exp_typ =
+  let is_complete_gpats ?(keyword = "match") l ctx have_guard gpats_matrix =
+    let res =
+      match matrix_is_complete l ctx gpats_matrix with
+      | Incomplete (unmatched :: _) ->
+          let guard_info = if have_guard then " by unguarded patterns" else "" in
+          Reporting.warn "Incomplete pattern match statement at" (shrink_loc keyword l)
+            ("The following expression is unmatched" ^ guard_info ^ ": "
+            ^ (string_of_exp unmatched |> Util.yellow |> Util.clear)
+            );
+          false
+      | Incomplete [] -> Reporting.unreachable l __POS__ "Got unmatched pattern matrix without witness" [@coverage off]
+      | Complete cinfo ->
+          (* let wildcarded_pats = List.map (fun (_, pat) -> insert_wildcards cinfo pat) pats in *)
+          List.iter
+            (fun (idx, _) ->
+              if IntSet.mem idx.num cinfo.redundant then
+                Reporting.warn "Redundant case" idx.loc "This match case is never used"
+            )
+            (rows_to_list gpats_matrix);
+          true
+      | Completeness_unknown -> false
+    in
+    res
+
+  let is_complete_pats_wildcarded ?(keyword = "match") l ctx cases pats head_exp_typ =
     try
-      match cases_to_pats 0 false cases with
+      match pats with
       | _, [] -> None
       | have_guard, pats ->
           let matrix =
@@ -944,6 +971,10 @@ module Make (C : Config) = struct
     with (* For now, if any error occurs just report the pattern match is incomplete *)
     | _ -> None
 
+  let is_complete_wildcarded ?(keyword = "match") l ctx cases head_exp_typ =
+    let pats = cases_to_pats 0 false cases in
+    is_complete_pats_wildcarded l ctx cases pats head_exp_typ
+
   let is_complete_funcls_wildcarded ?(keyword = "match") l ctx funcls head_exp_typ =
     let destruct_funcl (FCL_aux (FCL_funcl (id, pexp), annot)) = ((id, annot), pexp) in
     let cases = List.map destruct_funcl funcls in
@@ -953,4 +984,106 @@ module Make (C : Config) = struct
 
   let is_complete ?(keyword = "match") l ctx cases head_exp_typ =
     Option.is_some (is_complete_wildcarded ~keyword l ctx cases head_exp_typ)
+
+  let rec gpat_matrix_of_pats ctx pats head_exp_typ =
+    let mpat_matrix =
+      Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some head_exp_typ) pat])) pats)
+    in
+    mpat_matrix
+
+  (* let mpat_of_mpexp = function
+       | MPat_aux (mpexp_aux, l) -> (
+           match mpexp_aux with MPat_pat mpat | MPat_when (mpat, _) -> mpat
+         )
+
+     let pat_of_pexp = function
+       | Pat_aux (pexp_aux, _l) -> (
+           match pexp_aux with Pat_exp (pat, _exp) -> pat | Pat_when (pat, _e1, _e2) -> pat
+         )
+
+     let rec pat_of_ast_mapcl l = function
+       | MCL_aux (mapcl_aux, _) ->
+           let res =
+             match mapcl_aux with
+             (* | MCL_attribute (_s, _attr_data_option, MCL_aux (mapcl_aux, l)) -> pat_of_mapcl (MCL_aux (mapcl_aux, l)) *)
+             (* | MCL_doc (_, MCL_aux (mapcl_aux, l)) -> pat_of_mapcl (MCL_aux (mapcl_aux, l)) *)
+             | MCL_bidir (mpexp1, mpexp2) -> pat_of_mpat (mpat_of_mpexp mpexp1)
+             (* | MCL_forwards_deprecated (mpexp, _exp) -> pat_of_mpat (mpat_of_mpexp mpexp) *)
+             | MCL_forwards mpexp -> pat_of_pexp mpexp
+             | MCL_backwards mpexp -> pat_of_pexp mpexp
+           in
+           (l, res) *)
+
+  (* let mapcls_to_pats mapcls = List.map (fun (MCL_aux (cl, a)) -> P_aux (P.P_id, a)) mapcls *)
+  let rec pat_of_mpat mpat =
+    match mpat with
+    | MP_aux (mpat_aux, l) ->
+        let res =
+          match mpat_aux with
+          | MP_lit lit -> P_lit lit
+          | MP_id id -> P_id id
+          | MP_app (id, mpat_list) -> P_app (id, List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector mpat_list -> P_vector (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector_concat mpat_list -> P_vector_concat (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_vector_subrange (id, l, r) -> P_vector_subrange (id, l, r)
+          | MP_tuple mpat_list -> P_tuple (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_list mpat_list -> P_list (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_cons (mpat1, mpat2) -> P_cons (pat_of_mpat mpat1, pat_of_mpat mpat2)
+          | MP_string_append mpat_list -> P_string_append (List.map (fun mpat -> pat_of_mpat mpat) mpat_list)
+          | MP_typ (mp1, atyp) -> P_typ (atyp, pat_of_mpat mp1)
+          | MP_struct id_mpat_list ->
+              (* let fp_of_id_mpat (id, mpat) = FP_aux (FP_field (id, pat_of_mpat mpat), l) in *)
+              (* let fpl = List.map fp_of_id_mpat id_mpat_list in *)
+              let fpl = List.map (fun (id, mpat) -> (id, pat_of_mpat mpat)) id_mpat_list in
+              P_struct (fpl, FP_no_wild)
+          | MP_as (mpat, id) -> (
+              match pat_of_mpat mpat with P_aux (pat, _id) -> pat
+            )
+        in
+        P_aux (res, l)
+
+  let pexp_of_mpat pat l =
+    (* make an empty block *)
+    let exp = E_aux (E_block [], l) in
+    Pat_aux (Pat_exp (pat, exp), l)
+
+  let pexp_of_mpexp = function
+    | MPat_aux (mpexp_aux, l) -> (
+        match mpexp_aux with
+        | MPat_when (mpat, exp) -> Pat_aux (Pat_exp (pat_of_mpat mpat, exp), l)
+        | MPat_pat mpat -> pexp_of_mpat (pat_of_mpat mpat) l
+      )
+
+  let rec pexp_funcl_of_mapcl : 'a mapcl -> 'a pexp_funcl = function
+    | MCL_aux (mapcl_aux, l) -> (
+        match mapcl_aux with
+        | MCL_bidir (mpexp1, mpexp2) -> pexp_of_mpexp mpexp1
+        | MCL_forwards pexp ->
+            ( match pexp with
+            | Pat_aux (pexp_aux, annot) -> (
+                match annot with l, t -> ()
+              )
+            );
+            pexp
+        | MCL_backwards pexp -> pexp
+      )
+
+  let rec pexp_of_ast_mapcl = function
+    | MCL_aux (mapcl_aux, _) ->
+        let res =
+          match mapcl_aux with
+          | MCL_bidir (mpexp1, mpexp2) -> pexp_of_mpexp mpexp1
+          | MCL_forwards pexp -> pexp
+          | MCL_backwards pexp -> pexp
+        in
+        res
+
+  let is_complete_mapcls_wildcarded ?(keyword = "match") l ctx mapcls head_exp_typ =
+    let have_guard = false in
+    let cases = List.map pexp_of_ast_mapcl mapcls in
+    let have_guard, pats = cases_to_pats 0 have_guard cases in
+    let matrix =
+      Rows (List.mapi (fun i (l, pat) -> ({ loc = l; num = i }, Columns [generalize ctx (Some head_exp_typ) pat])) pats)
+    in
+    is_complete_gpats l ctx have_guard matrix
 end

src/lib/pattern_completeness.mli

@@ -93,4 +93,7 @@ module Make (C : Config) : sig
   val is_complete_funcls_wildcarded :
     ?keyword:string -> Parse_ast.l -> ctx -> C.t funcl list -> typ -> C.t funcl list option
   val is_complete : ?keyword:string -> Parse_ast.l -> ctx -> C.t pexp list -> typ -> bool
+
+  (* val pexp_of_ast_mapcl : uannot mapcl -> uannot pexp *)
+  val is_complete_mapcls_wildcarded : ?keyword:string -> Parse_ast.l -> ctx -> C.t mapcl list -> typ -> bool
 end

src/lib/type_check.ml

@@ -2095,6 +2095,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
           crule check_exp env exp (app_typ (mk_id "option") [mk_typ_arg (A_typ typ)])
         else irule infer_exp env exp
       in
+      (* inferred_typ *)
       let inferred_typ = typ_of inferred_exp in
       let checked_cases = List.map (fun case -> check_case env inferred_typ case typ) cases in
       let checked_cases, attr_update =
@@ -2105,7 +2106,9 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au
           let ctx = pattern_completeness_ctx env in
           match PC.is_complete_wildcarded l ctx checked_cases completeness_typ with
           | Some wildcarded -> (wildcarded, add_attribute (gen_loc l) "complete" None)
-          | None -> (checked_cases, add_attribute (gen_loc l) "incomplete" None)
+          | None ->
+              Printf.printf "不完整被检查到了😭\n";
+              (checked_cases, add_attribute (gen_loc l) "incomplete" None)
         )
       in
       annot_exp (E_match (inferred_exp, checked_cases)) typ |> update_uannot attr_update
@@ -4346,10 +4349,15 @@ let bind_funcl_arg_typ l env typ =
   | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
 
 let check_funcl env (FCL_aux (FCL_funcl (id, pexp), (def_annot, _))) typ =
+  Printf.printf "check_funcl::begin----------------------------------------------#\n";
   let l = def_annot.loc in
   let typ_arg, typ_ret, env = bind_funcl_arg_typ l env typ in
+  Printf.printf "check_funcl::check_case----------------------------------------------#\n";
   let typed_pexp = check_case env typ_arg pexp typ_ret in
-  FCL_aux (FCL_funcl (id, typed_pexp), (def_annot, mk_expected_tannot env typ (Some typ)))
+  Printf.printf "check_funcl::check_case_done----------------------------------------------#\n";
+  let res = FCL_aux (FCL_funcl (id, typed_pexp), (def_annot, mk_expected_tannot env typ (Some typ))) in
+  Printf.printf "check_funcl::done----------------------------------------------#\n";
+  res
 
 let check_mapcl env (MCL_aux (cl, (def_annot, _))) typ =
   let ignore_errors ~default f = try f () with Type_error _ -> default in
@@ -4551,13 +4559,27 @@ let check_fundef env def_annot (FD_aux (FD_function (recopt, tannot_opt, funcls)
       ([synthesize_val_spec env id quant typ def_annot], Env.add_val_spec id (quant, typ) env)
     else ([], env)
   in
-  let funcls = List.map (fun funcl -> check_funcl funcl_env funcl typ) funcls in
+
+  let funcls =
+    List.map
+      (fun funcl ->
+        let res = check_funcl funcl_env funcl typ in
+        res
+      )
+      funcls
+  in
   let funcls, update_attr =
     if
       Option.is_some (get_def_attribute "complete" def_annot)
       || Option.is_some (get_def_attribute "incomplete" def_annot)
-    then (funcls, fun attrs -> attrs)
-    else check_funcls_complete l funcl_env funcls typ
+    then (
+      Printf.printf "有 [in]complete 标记----------------------------------------------#\n";
+      (funcls, fun attrs -> attrs)
+    )
+    else (
+      Printf.printf "无标记----------------------------------------------#\n";
+      check_funcls_complete l funcl_env funcls typ
+    )
   in
   let def_annot = fix_body_visibility (update_attr def_annot) in
   let env = Env.define_val_spec id env in
@@ -4606,7 +4628,31 @@ let check_mapdef env def_annot (MD_aux (MD_mapping (id, tannot_opt, mapcls), (l,
     else ([], env)
   in
   let mapcl_env = Env.add_typquant l quant env in
+
+  (* check mapcls dup *)
+  (* type infer, uannot -> tannot *)
   let mapcls = List.map (fun mapcl -> check_mapcl mapcl_env mapcl typ) mapcls in
+
+  (* check side complete *)
+  let ctx = pattern_completeness_ctx env in
+
+  (* FIXME: run right side check *)
+  let typ =
+    match typ with
+    | Typ_aux (Typ_bidir (typl, typr), _) -> typl
+    | _ -> typ_error l "Mapping type must be a bi-directional mapping"
+  in
+  Printf.printf "before complete check\n";
+  ignore
+    ( match PC.is_complete_mapcls_wildcarded l ctx mapcls typ with
+    | true ->
+        Printf.printf "hahdha~~~\n";
+        add_attribute (gen_loc l) "complete" None empty_uannot
+    | false ->
+        Printf.printf "🙅‍♀️⭕🥛🛂🔪😭\n";
+        add_attribute (gen_loc l) "incomplete" None empty_uannot
+    );
+
   let def_annot = fix_body_visibility def_annot in
   let env = Env.define_val_spec id env in
   ( vs_def @ [DEF_aux (DEF_mapdef (MD_aux (MD_mapping (id, empty_tannot_opt, mapcls), (l, empty_tannot))), def_annot)],