[funind] Move some exception-based control flow to explicit option typing.

6 files changed, 104 insertions, 76 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5a939b4adf..ca33e4e757 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -941,7 +941,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma =
     try
-      let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
+      let finfos =
+        match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
+        | None -> raise Not_found
+        | Some finfos -> finfos
+      in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
       let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
@@ -953,14 +957,18 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let _ =
         match e with
           | Option.IsNone ->
-              let finfos = find_Function_infos (fst (destConst !evd f)) in
-              update_Function
-                {finfos with
-                   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                                              GlobRef.ConstRef c -> c
-                                            | _ -> CErrors.anomaly (Pp.str "Not a constant.")
-                                         )
-                }
+            let finfos = match find_Function_infos (fst (destConst !evd f)) with
+              | None -> raise Not_found
+              | Some finfos -> finfos
+            in
+            update_Function
+              {finfos with
+               equation_lemma = Some (
+                   match Nametab.locate (qualid_of_ident equation_lemma_id) with
+                   | GlobRef.ConstRef c -> c
+                   | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+                 )
+              }
           | _ -> ()
       in
       (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 730ae48393..66a37435f5 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -495,14 +495,17 @@ let find_induction_principle evd f =
     | Constr.Const c' -> c'
     | _ -> CErrors.user_err Pp.(str "Must be used with a function")
   in
-  let infos = find_Function_infos f_as_constant in
-  match infos.rect_lemma with
-  | None -> raise Not_found
-  | Some rect_lemma ->
-    let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
-    let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
-    evd:=evd';
-    rect_lemma,typ
+  match find_Function_infos f_as_constant with
+  | None ->
+    raise Not_found
+  | Some infos ->
+    match infos.rect_lemma with
+    | None -> raise Not_found
+    | Some rect_lemma ->
+      let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
+      let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+      evd:=evd';
+      rect_lemma,typ
 
 (* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
    is the tactic used to prove correctness lemma.
@@ -1016,12 +1019,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     *)
     let rewrite_tac j ids : Tacmach.tactic =
       let graph_def = graphs.(j) in
-      let infos =
-        try find_Function_infos (fst (destConst (project g) funcs.(j)))
-        with Not_found -> CErrors.user_err Pp.(str "No graph found")
+      let infos = match find_Function_infos (fst (destConst (project g) funcs.(j))) with
+        | None ->
+          CErrors.user_err Pp.(str "No graph found")
+        | Some infos -> infos
       in
-      if infos.is_general
-      || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
+      if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
       then
         let eq_lemma =
           try Option.get (infos).equation_lemma
@@ -1174,9 +1177,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   let first_fun = List.hd funs in
   let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
   let first_fun_kn =
-    try
-      fst (find_Function_infos  (fst first_fun)).graph_ind
-    with Not_found -> raise No_graph_found
+    match find_Function_infos (fst first_fun) with
+    | None -> raise No_graph_found
+    | Some finfos -> fst finfos.graph_ind
   in
   let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
   let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
@@ -1231,12 +1234,15 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos (fst first_fun) in
-    try
-      let equation =  Option.get finfos.equation_lemma in
+    let finfos =
+      match find_Function_infos (fst first_fun) with
+      | None -> raise Not_found
+      | Some finfos -> finfos
+    in
+    match finfos.equation_lemma with
+    | None -> false (* non recursive definition *)
+    | Some equation ->
       Declareops.is_opaque (Global.lookup_constant equation)
-    with Option.IsNone -> (* non recursive definition *)
-      false
   in
   let const = {const with Proof_global.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
@@ -1381,7 +1387,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
             let lemma = fst @@ Lemmas.by
                 (Proofview.V82.tactic (proving_tac i)) lemma in
             let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-            let finfo = find_Function_infos (fst f_as_constant) in
+            let finfo =
+              match find_Function_infos (fst f_as_constant) with
+              | None -> raise Not_found
+              | Some finfo -> finfo
+            in
             (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
             let _,lem_cst_constr = Evd.fresh_global
                 (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
@@ -1443,7 +1453,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
                                (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
                                                         (proving_tac i))) lemma) in
             let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-            let finfo = find_Function_infos (fst f_as_constant) in
+            let finfo =
+              match find_Function_infos (fst f_as_constant) with
+              | None -> raise Not_found
+              | Some finfo -> finfo
+            in
             let _,lem_cst_constr = Evd.fresh_global
                 (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
             let (lem_cst,_) = destConst !evd lem_cst_constr in
@@ -2028,7 +2042,11 @@ let build_case_scheme fa =
   let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
   let first_fun = funs in
   let funs_mp = Constant.modpath first_fun in
-  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
+  let first_fun_kn =
+    match find_Function_infos first_fun with
+    | None -> raise No_graph_found
+    | Some finfos -> fst finfos.graph_ind
+  in
   let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
   let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
   let prop_sort = Sorts.InProp in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2de7be4c67..2937ae5d14 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -52,8 +52,9 @@ let functional_induction with_clean c princl pat =
         | Const (c',u) ->
           let princ_option =
             let finfo = (* we first try to find out a graph on f *)
-              try find_Function_infos c'
-              with Not_found ->
+              match find_Function_infos c' with
+              | Some finfo -> finfo
+              | None ->
                 user_err  (str "Cannot find induction information on "++
                            Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
             in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8471dfd05a..7719705138 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -294,20 +294,16 @@ let find_or_none id =
     )
   with Not_found -> None
 
-
-
 let find_Function_infos f =
-  Cmap_env.find f !from_function
-
+  Cmap_env.find_opt f !from_function
 
 let find_Function_of_graph ind =
-  Indmap.find ind !from_graph
+  Indmap.find_opt ind !from_graph
 
 let update_Function finfo =
   (* Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
 
-
 let add_Function is_general f =
   let f_id = Label.to_id (Constant.label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 0815ca882a..16beaaa3c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -74,8 +74,8 @@ type function_info =
       is_general : bool;
     }
 
-val find_Function_infos : Constant.t -> function_info
-val find_Function_of_graph : inductive -> function_info
+val find_Function_infos : Constant.t -> function_info option
+val find_Function_of_graph : inductive -> function_info option
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> Constant.t -> unit
 val update_Function : function_info -> unit
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 38fdd789a3..d72319d078 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -34,9 +34,10 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
     let ((kn',num) as ind'),u = destInd sigma i in
     if MutInd.equal kn kn'
     then (* We have generated a graph hypothesis so that we must change it if we can *)
-      let info =
-        try find_Function_of_graph ind'
-        with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+      let info = match find_Function_of_graph ind' with
+        | Some info -> info
+        | None ->
+          (* The graphs are mutually recursive but we cannot find one of them !*)
           CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
       in
       (* if we can find a completeness lemma for this function
@@ -108,18 +109,20 @@ let invfun qhyp f  =
     | _ ->
       CErrors.user_err Pp.(str "Not a function")
   in
-  try
-    let finfos = find_Function_infos f in
-    let f_correct = mkConst(Option.get finfos.correctness_lemma)
-    and kn = fst finfos.graph_ind in
-    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
-  with
-  | Not_found -> CErrors.user_err (Pp.str "No graph found")
-  | Option.IsNone  -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
-
-exception NoFunction
+  match find_Function_infos f with
+  | None ->
+    CErrors.user_err (Pp.str "No graph found")
+  | Some finfos ->
+    match finfos.correctness_lemma with
+    | None ->
+      CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
+    | Some f_correct ->
+      let f_correct = mkConst f_correct
+      and kn = fst finfos.graph_ind in
+      Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
 
 let invfun qhyp f =
+  let exception NoFunction in
   match f with
   | Some f -> invfun qhyp f
   | None ->
@@ -132,31 +135,33 @@ let invfun qhyp f =
           let f1,_ = decompose_app sigma args.(1) in
           try
             if not (isConst sigma f1) then raise NoFunction;
-            let finfos = find_Function_infos (fst (destConst sigma f1)) in
+            let finfos = Option.get (find_Function_infos (fst (destConst sigma f1))) in
             let f_correct = mkConst(Option.get finfos.correctness_lemma)
             and kn = fst finfos.graph_ind
             in
             functional_inversion kn hid f1 f_correct
-          with | NoFunction | Option.IsNone | Not_found ->
-          try
-            let f2,_ = decompose_app sigma args.(2) in
-            if not (isConst sigma f2) then raise NoFunction;
-            let finfos = find_Function_infos (fst (destConst sigma f2)) in
-            let f_correct = mkConst(Option.get finfos.correctness_lemma)
-            and kn = fst finfos.graph_ind
-            in
-            functional_inversion kn hid  f2 f_correct
           with
-          | NoFunction ->
-            CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
-          | Option.IsNone  ->
-            if do_observe ()
-            then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
-            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-          | Not_found ->
-            if do_observe ()
-            then CErrors.user_err (Pp.str "No graph found for any side of equality")
-            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+          | NoFunction | Option.IsNone ->
+            let f2,_ = decompose_app sigma args.(2) in
+            if isConst sigma f2 then
+              match find_Function_infos (fst (destConst sigma f2)) with
+              | None ->
+                if do_observe ()
+                then CErrors.user_err (Pp.str "No graph found for any side of equality")
+                else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+              | Some finfos ->
+                match finfos.correctness_lemma with
+                | None ->
+                  if do_observe ()
+                  then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
+                  else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+                | Some f_correct ->
+                  let f_correct = mkConst f_correct
+                  and kn = fst finfos.graph_ind
+                  in
+                  functional_inversion kn hid  f2 f_correct
+            else                (* NoFunction *)
+              CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
         end
       | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
     in