whyml: impose exhaustive pattern matching

src/core/decl.ml

@@ -675,18 +675,17 @@ let find_prop_decl kn pr =
   | Dprop (k,_,f) -> k,f
   | Dtype _ | Ddata _ | Dparam _ | Dlogic _ -> assert false
 
-exception NonExhaustiveCase of pattern list * term
-
-let rec check_matchT kn () t = match t.t_node with
-  | Tcase (t1,bl) ->
-      let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
-      let find_constructors kn ts = List.map fst (find_constructors kn ts) in
-      ignore (try Pattern.CompileTerm.compile (find_constructors kn) [t1] bl
-      with Pattern.NonExhaustive p -> raise (NonExhaustiveCase (p,t)));
-      t_fold (check_matchT kn) () t
-  | _ -> t_fold (check_matchT kn) () t
-
-let check_match kn d = decl_fold (check_matchT kn) () d
+let check_match kn d =
+  let rec check () t = match t.t_node with
+    | Tcase (t1,bl) ->
+        let find ts = List.map fst (find_constructors kn ts) in
+        let bl = List.map (fun b -> let p,t = t_open_branch b in [p],t) bl in
+        let try3 f = match t.t_loc with Some l -> Loc.try3 l f | None -> f in
+        ignore (try3 Pattern.CompileTerm.compile find [t1] bl);
+        t_fold check () t
+    | _ -> t_fold check () t
+  in
+  decl_fold check () d
 
 exception NonFoundedTypeDecl of tysymbol
 

src/core/decl.mli

@@ -180,7 +180,6 @@ val merge_known : known_map -> known_map -> known_map
 exception KnownIdent of ident
 exception UnknownIdent of ident
 exception RedeclaredIdent of ident
-exception NonExhaustiveCase of pattern list * term
 exception NonFoundedTypeDecl of tysymbol
 
 val find_constructors : known_map -> tysymbol -> constructor list

src/core/pretty.ml

@@ -539,8 +539,8 @@ let () = Exn_printer.register
       fprintf fmt "The symbol %a is not a constructor"
         print_ls ls
   | Pattern.NonExhaustive pl ->
-      fprintf fmt "Non-exhaustive pattern list:@\n@[<hov 2>%a@]"
-        (print_list newline print_pat) pl
+      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
+        print_pat (List.hd pl)
   | Decl.BadConstructor ls ->
       fprintf fmt "Bad constructor symbol: %a" print_ls ls
   | Decl.BadRecordField ls ->
@@ -588,9 +588,6 @@ let () = Exn_printer.register
         id.id_string
   | Decl.NoTerminationProof ls ->
       fprintf fmt "Cannot prove the termination of %a" print_ls ls
-  | Decl.NonExhaustiveCase (pl, e) ->
-      fprintf fmt "Pattern @[%a@] is not covered in expression:@\n  @[%a@]"
-        (print_list comma print_pat) pl print_term e
   | _ -> raise exn
   end
 

src/whyml/mlw_decl.ml

@@ -308,20 +308,42 @@ let pd_vars pd = match pd.pd_node with
       Mid.map (fun _ -> ()) varm
   | PDtype _ | PDdata _ | PDexn _ -> Sid.empty
 
-let known_add_decl lkn0 kn0 decl =
-  let kn = Mid.map (const decl) decl.pd_news in
+let known_add_decl lkn0 kn0 d =
+  let kn = Mid.map (const d) d.pd_news in
   let check id decl0 _ =
-    if pd_equal decl0 decl
+    if pd_equal decl0 d
     then raise (KnownIdent id)
-    else raise (RedeclaredIdent id)
-  in
+    else raise (RedeclaredIdent id) in
   let kn = Mid.union check kn0 kn in
-  let unk = Mid.set_diff (pd_vars decl) kn in
+  let unk = Mid.set_diff (pd_vars d) kn in
   let unk = Mid.set_diff unk lkn0 in
   if Sid.is_empty unk then kn
   else raise (UnknownIdent (Sid.choose unk))
 
-(* TODO: known_add_decl must check pattern matches for exhaustiveness *)
+let check_match lkn d =
+  let rec checkE () e = match e.e_node with
+    | Ecase (e1,bl) ->
+        let typ = ty_of_ity (vtv_of_expr e1).vtv_ity in
+        let tye = ty_of_ity (vtv_of_expr e).vtv_ity in
+        let t_p = t_var (create_vsymbol (id_fresh "x") typ) in
+        let t_e = t_var (create_vsymbol (id_fresh "y") tye) in
+        let bl = List.map (fun (pp,_) -> [pp.ppat_pattern], t_e) bl in
+        let try3 f = match e.e_loc with Some l -> Loc.try3 l f | None -> f in
+        let find ts = List.map fst (Decl.find_constructors lkn ts) in
+        ignore (try3 Pattern.CompileTerm.compile find [t_p] bl);
+        e_fold checkE () e
+    | _ -> e_fold checkE () e
+  in
+  match d.pd_node with
+  | PDrec { rec_defn = fdl } ->
+      List.iter (fun fd -> checkE () fd.fun_lambda.l_expr) fdl
+  | PDlet { let_expr = e } -> checkE () e
+  | PDval _ | PDtype _ | PDdata _ | PDexn _ -> ()
+
+let known_add_decl lkn kn d =
+  let kn = known_add_decl lkn kn d in
+  check_match lkn d;
+  kn
 
 let rec find_td its1 = function
   | (its2,csl,inv) :: _ when its_equal its1 its2 -> csl,inv