Merge remote-tracking branch 'origin/sail2' into polymorphic_variants

1 files changed, 77 insertions, 5 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 5ed174ea..47c7e923 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1084,9 +1084,11 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,annot2) as pat2) =
   | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2
   | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) ->
     if id1 = id2 then Some []
-    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound &&
-            Env.lookup_id aid2 (env_of_annot annot2) = Unbound
-           then Some [(id2,id1)] else None
+    else if Env.lookup_id aid1 (env_of_annot annot1) = Unbound
+    then if Env.lookup_id aid2 (env_of_annot annot2) = Unbound
+      then Some [(id2,id1)]
+      else Some []
+    else None
   | P_id id1, _ ->
     if Env.lookup_id id1 (env_of_annot annot1) = Unbound then Some [] else None
   | P_var (pat1,_), P_var (pat2,_) -> subsumes_pat pat1 pat2
@@ -4043,7 +4045,18 @@ let rewrite_defs_realise_mappings (Defs defs) =
 
 
 (* Rewrite to make all pattern matches in Coq output exhaustive.
-   Assumes that guards, vector patterns, etc have been rewritten already. *)
+   Assumes that guards, vector patterns, etc have been rewritten already,
+   and the scattered functions have been merged.
+   Will add escape effect where a default is needed, so effects will
+   need recalculated afterwards.
+
+   Also detects and removes redundant wildcard patterns at the end of the match.
+   (We could do more, but this is sufficient to deal with the code generated by
+   the mappings rewrites.)
+
+   Note: if this naive implementation turns out to be too slow or buggy, we
+   could look at implementing Maranget JFP 17(3), 2007.
+ *)
 
 let opt_coq_warn_nonexhaustive = ref false
 
@@ -4261,12 +4274,38 @@ let process_pexp env =
      raise (Reporting_basic.err_unreachable l
               "Guarded pattern should have been rewritten away")
 
+(* We do some minimal redundancy checking to remove bogus wildcard patterns here *)
+let check_cases process is_wild loc_of cases =
+  let rec aux rps acc = function
+    | [] -> acc, rps
+    | [p] when is_wild p && match rps with [] -> true | _ -> false ->
+      let () = Reporting_basic.print_err false false
+        (loc_of p) "Match checking" "Redundant wildcard clause" in
+      acc, []
+    | h::t -> aux (process rps h) (h::acc) t
+  in
+  let cases, rps = aux [RP_any] [] cases in
+  List.rev cases, rps
+
+let pexp_is_wild = function
+  | (Pat_aux (Pat_exp (P_aux (P_wild,_),_),_)) -> true
+  | _ -> false
+
+let pexp_loc = function
+  | (Pat_aux (Pat_exp (P_aux (_,(l,_)),_),_)) -> l
+  | (Pat_aux (Pat_when (P_aux (_,(l,_)),_,_),_)) -> l
+
+let funcl_is_wild = function
+  | (FCL_aux (FCL_Funcl (_,pexp),_)) -> pexp_is_wild pexp
+
+let funcl_loc (FCL_aux (_,(l,_))) = l
+
 let rewrite_case (e,ann) =
   match e with
   | E_case (e1,cases) ->
      begin
      let env = env_of_annot ann in
-     let rps = List.fold_left (process_pexp env) [RP_any] cases in
+     let cases, rps = check_cases (process_pexp env) pexp_is_wild pexp_loc cases in
      match rps with
      | [] -> E_aux (E_case (e1,cases),ann)
      | (example::_) ->
@@ -4285,6 +4324,37 @@ let rewrite_case (e,ann) =
      end
   | _ -> E_aux (e,ann)
 
+let rewrite_fun rewriters (FD_aux (FD_function (r,t,e,fcls),f_ann)) =
+  let id,fcl_ann =
+    match fcls with
+    | FCL_aux (FCL_Funcl (id,_),ann) :: _ -> id,ann
+    | [] -> raise (Reporting_basic.err_unreachable (fst f_ann)
+                 "Empty function")
+  in
+  let env = env_of_annot fcl_ann in
+  let process_funcl rps (FCL_aux (FCL_Funcl (_,pexp),_)) = process_pexp env rps pexp in
+  let fcls, rps = check_cases process_funcl funcl_is_wild funcl_loc fcls in
+  let fcls' = List.map (function FCL_aux (FCL_Funcl (id,pexp),ann) ->
+                                  FCL_aux (FCL_Funcl (id, rewrite_pexp rewriters pexp),ann))
+                fcls in
+  match rps with
+  | [] -> FD_aux (FD_function (r,t,e,fcls'),f_ann)
+  | (example::_) ->
+     let _ =
+       if !opt_coq_warn_nonexhaustive
+       then Reporting_basic.print_err false false
+              (fst f_ann) "Non-exhaustive matching" ("Example: " ^ string_of_rp example) in
+
+     let l = Parse_ast.Generated Parse_ast.Unknown in
+     let p = P_aux (P_wild, (l, empty_tannot)) in
+     let ann' = mk_tannot env (typ_of_annot fcl_ann) (mk_effect [BE_escape]) in
+     (* TODO: use an expression that specifically indicates a failed pattern match *)
+     let b = E_aux (E_exit (E_aux (E_lit (L_aux (L_unit, l)),(l,empty_tannot))),(l,ann')) in
+     let default = FCL_aux (FCL_Funcl (id,Pat_aux (Pat_exp (p,b),(l,empty_tannot))),fcl_ann) in
+
+     FD_aux (FD_function (r,t,e,fcls'@[default]),f_ann)
+  
+
 let rewrite =
   let alg = { id_exp_alg with e_aux = rewrite_case } in
   rewrite_defs_base
@@ -4381,6 +4451,8 @@ let rewrite_defs_lem = [
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
   ("fix_val_specs", rewrite_fix_val_specs);
+  (* early_return currently breaks the types *)
+  ("recheck_defs", recheck_defs);
   ("remove_blocks", rewrite_defs_remove_blocks);
   ("letbind_effects", rewrite_defs_letbind_effects);
   ("remove_e_assign", rewrite_defs_remove_e_assign);