Merge PR coq#19120: Use algebraic datatypes to signal failure in Conv…

…ersion API

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

checker/mod_checking.ml

@@ -69,8 +69,10 @@ let check_constant_declaration env opac kn cb opacify =
     match body with
     | Some bd ->
       let j = infer env bd in
-      (try conv_leq env j.uj_type ty
-       with NotConvertible -> Type_errors.error_actual_type env j ty)
+      begin match conv_leq env j.uj_type ty with
+      | Result.Ok () -> ()
+      | Result.Error () -> Type_errors.error_actual_type env j ty
+      end
     | None -> ()
   in
   match body with

dev/ci/user-overlays/19120-ppedrot-conversion-no-inner-exception-api.sh

@@ -0,0 +1 @@
+overlay smtcoq https://github.com/ppedrot/smtcoq conversion-no-inner-exception-api 19120

kernel/constant_typing.ml

@@ -111,8 +111,9 @@ let process_universes env = function
 
 let check_primitive_type env op_t u t =
   let inft = Typeops.type_of_prim_or_type env u op_t in
-  try Conversion.default_conv Conversion.CONV env inft t
-  with Conversion.NotConvertible ->
+  match Conversion.default_conv Conversion.CONV env inft t with
+  | Result.Ok () -> ()
+  | Result.Error () ->
     Type_errors.error_incorrect_primitive env (make_judge op_t inft) t
 
 let adjust_primitive_univ_entry p auctx = function

kernel/conversion.ml

@@ -122,15 +122,18 @@ let pure_stack lfts stk =
 (* Conversion utility functions *)
 
 (* functions of this type are called from the kernel *)
-type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
+type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result
 
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:evar_handler ->
-  'a -> 'a -> unit
+  'a -> 'a -> (unit, unit) result
+
+type payload = ..
 
 exception NotConvertible
+exception NotConvertibleTrace of payload
 
 (* Convertibility of sorts *)
 
@@ -145,19 +148,16 @@ type conv_pb =
   | CONV
   | CUMUL
 
-type 'a universe_compare = {
-  (* Might raise NotConvertible *)
-  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
-  compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
+type ('a, 'err) universe_compare = {
+  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
+  compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
   compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
-    UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
+    UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
-type 'a universe_state = 'a * 'a universe_compare
-
-type 'b generic_conversion_function = 'b universe_state -> constr -> constr -> 'b
+type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
 
-type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraints.t
+type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> constr -> constr -> ('a, 'err option) result
 
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare_sorts env pb s0 s1 u, check)
@@ -190,10 +190,24 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
     let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
     if not (Int.equal num_param_arity nargs) then
       (* shortcut, not sure if worth doing, could use perf data *)
-      if UVars.Instance.equal u1 u2 then s else raise MustExpand
+      if UVars.Instance.equal u1 u2 then Result.Ok s else raise MustExpand
     else
       cmp_cumul cv_pb variances u1 u2 s
 
+type 'e conv_tab = {
+  cnv_inf : clos_infos;
+  lft_tab : clos_tab;
+  rgt_tab : clos_tab;
+  err_ret : 'e -> payload;
+}
+(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
+    location contained both in tl and in tr. *)
+
+let fail_check (infos : 'err conv_tab) (state, check) = match state with
+| Result.Ok state -> (state, check)
+| Result.Error None -> raise NotConvertible
+| Result.Error (Some err) -> raise (NotConvertibleTrace (infos.err_ret err))
+
 let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
   convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
     cv_pb ind nargs u1 u2 s, check
@@ -208,7 +222,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
   | Some _ ->
     let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
-      if UVars.Instance.equal u1 u2 then s else raise MustExpand
+      if UVars.Instance.equal u1 u2 then Result.Ok s else raise MustExpand
     else
       (** By invariant, both constructors have a common supertype,
           so they are convertible _at that type_. *)
@@ -225,11 +239,11 @@ let conv_table_key infos ~nargs k1 k2 cuniv =
   match k1, k2 with
   | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
     if UVars.Instance.equal u u' then cuniv
-    else if Int.equal nargs 1 && is_array_type (info_env infos) cst then cuniv
+    else if Int.equal nargs 1 && is_array_type (info_env infos.cnv_inf) cst then cuniv
     else
-      let flex = evaluable_constant cst (info_env infos)
-        && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
-      in convert_instances ~flex u u' cuniv
+      let flex = evaluable_constant cst (info_env infos.cnv_inf)
+        && RedFlags.red_set (info_flags infos.cnv_inf) (RedFlags.fCONST cst)
+      in fail_check infos @@ convert_instances ~flex u u' cuniv
   | VarKey id, VarKey id' when Id.equal id id' -> cuniv
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
@@ -239,14 +253,6 @@ let same_args_size sk1 sk2 =
   if Int.equal n (CClosure.stack_args_size sk2) then n
   else raise NotConvertible
 
-type conv_tab = {
-  cnv_inf : clos_infos;
-  lft_tab : clos_tab;
-  rgt_tab : clos_tab;
-}
-(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
-    location contained both in tl and in tr. *)
-
 (** The same heap separation invariant must hold for the fconstr arguments
     passed to each respective side of the conversion function below. *)
 
@@ -393,7 +399,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                if not (is_empty_stack v1 && is_empty_stack v2) then
                  (* May happen because we convert application right to left *)
                  raise NotConvertible;
-              sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
+              fail_check infos @@ sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
            | (Meta n, Meta m) ->
                if Int.equal n m
                then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -431,10 +437,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FFlex fl1, FFlex fl2) ->
       (try
          let nargs = same_args_size v1 v2 in
-         let cuniv = conv_table_key infos.cnv_inf ~nargs fl1 fl2 cuniv in
+         let cuniv = conv_table_key infos ~nargs fl1 fl2 cuniv in
          let () = if irr_flex infos.cnv_inf fl1 then raise NotConvertible (* trigger the fallback *) in
          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-       with NotConvertible | UGraph.UniverseInconsistency _ ->
+       with NotConvertible | NotConvertibleTrace _ ->
         let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in
         let r2 = unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 in
         match r1, r2 with
@@ -604,12 +610,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
       if Ind.CanOrd.equal ind1 ind2 then
         if UVars.Instance.is_empty u1 || UVars.Instance.is_empty u2 then
-          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          let cuniv = fail_check infos @@ convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
           let nargs = same_args_size v1 v2 in
-          match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+          match fail_check infos @@ convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
           | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
           | exception MustExpand ->
             let env = info_env infos.cnv_inf in
@@ -621,12 +627,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
       if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then
         if UVars.Instance.is_empty u1 || UVars.Instance.is_empty u2 then
-          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          let cuniv = fail_check infos @@ convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
           let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
           let nargs = same_args_size v1 v2 in
-          match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+          match fail_check infos @@ convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
           | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
           | exception MustExpand ->
             let env = info_env infos.cnv_inf in
@@ -710,7 +716,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let nargs = inductive_cumulativity_arguments ind in
         let u1 = CClosure.usubst_instance e1 u1 in
         let u2 = CClosure.usubst_instance e2 u2 in
-        convert_inductives CONV ind nargs u1 u2 cuniv
+        fail_check infos @@ convert_inductives CONV ind nargs u1 u2 cuniv
       in
       let pms1 = mk_clos_vect e1 pms1 in
       let pms2 = mk_clos_vect e2 pms2 in
@@ -722,7 +728,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
       let len = Parray.length_int t1 in
       if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
-      let cuniv = convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
+      let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
       let el1 = el_stack lft1 v1 in
       let el2 = el_stack lft2 v2 in
       let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -789,6 +795,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
                     | None -> convert_instances ~flex:false u1 u2 cu
                     | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
                 in
+                let cu = fail_check infos cu in
                 let pms1 = mk_clos_vect e1 pms1 in
                 let pms2 = mk_clos_vect e2 pms2 in
                 let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in
@@ -876,41 +883,45 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
   convert_list l2r infos lft1 lft2 v1 v2 cuniv
 | _, _ -> raise NotConvertible
 
-let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
-  NewProfile.profile "Conversion" (fun () ->
+let clos_gen_conv (type err) trans cv_pb l2r evars env graph univs t1 t2 =
+  NewProfile.profile "Conversion" begin fun () ->
       let reds = RedFlags.red_add_transparent RedFlags.betaiotazeta trans in
       let infos = create_conv_infos ~univs:graph ~evars reds env in
+      let module Error = struct type payload += Error of err end in
+      let box e = Error.Error e in
       let infos = {
         cnv_inf = infos;
         lft_tab = create_tab ();
         rgt_tab = create_tab ();
+        err_ret = box;
       } in
-      ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs)
-    ()
+      try Result.Ok (ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs)
+      with
+      | NotConvertible -> Result.Error None
+      | NotConvertibleTrace (Error.Error e) -> Result.Error (Some e)
+      | NotConvertibleTrace _ -> assert false
+  end ()
 
 let check_eq univs u u' =
-  if not (UGraph.check_eq_sort univs u u') then raise NotConvertible
+  if UGraph.check_eq_sort univs u u' then Result.Ok univs else Result.Error None
 
 let check_leq univs u u' =
-  if not (UGraph.check_leq_sort univs u u') then raise NotConvertible
+  if UGraph.check_leq_sort univs u u' then Result.Ok univs else Result.Error None
 
-let check_sort_cmp_universes pb s0 s1 univs =
+let checked_sort_cmp_universes _env pb s0 s1 univs =
   match pb with
   | CUMUL -> check_leq univs s0 s1
   | CONV -> check_eq univs s0 s1
 
-let checked_sort_cmp_universes _env pb s0 s1 univs =
-  check_sort_cmp_universes pb s0 s1 univs; univs
-
 let check_convert_instances ~flex:_ u u' univs =
-  if UGraph.check_eq_instances univs u u' then univs
-  else raise NotConvertible
+  if UGraph.check_eq_instances univs u u' then Result.Ok univs
+  else Result.Error None
 
 (* general conversion and inference functions *)
 let check_inductive_instances cv_pb variance u1 u2 univs =
   let qcsts, ucsts = get_cumulativity_constraints cv_pb variance u1 u2 in
-  if Sorts.QConstraints.trivial qcsts && (UGraph.check_constraints ucsts univs) then univs
-  else raise NotConvertible
+  if Sorts.QConstraints.trivial qcsts && (UGraph.check_constraints ucsts univs) then Result.Ok univs
+  else Result.Error None
 
 let checked_universes =
   { compare_sorts = checked_sort_cmp_universes;
@@ -920,14 +931,17 @@ let checked_universes =
 let () =
   let conv infos tab a b =
     try
+      let box = Empty.abort in
       let univs = info_univs infos in
-      let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; } in
+      let infos = { cnv_inf = infos; lft_tab = tab; rgt_tab = tab; err_ret = box } in
       let univs', _ = ccnv CONV false infos el_id el_id a b
           (univs, checked_universes)
       in
       assert (univs==univs');
       true
-      with NotConvertible -> false
+    with
+    | NotConvertible -> false
+    | NotConvertibleTrace _ -> assert false
   in
   CClosure.set_conv conv
 
@@ -937,19 +951,20 @@ let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=defaul
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2
     else eq_constr_univs univs t1 t2
   in
-    if b then ()
-    else
-      let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
-        ()
+    if b then Result.Ok ()
+    else match clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 with
+    | Result.Ok (_ : UGraph.t * (UGraph.t, Empty.t) universe_compare)-> Result.Ok ()
+    | Result.Error None -> Result.Error ()
+    | Result.Error (Some e) -> Empty.abort e
 
 let conv = gen_conv CONV
 let conv_leq = gen_conv CUMUL
 
 let generic_conv cv_pb ~l2r reds env ?(evars=default_evar_handler env) univs t1 t2 =
   let graph = Environ.universes env in
-  let (s, _) =
-    clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
-  in s
+  match clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2 with
+  | Result.Ok (s, _) -> Result.Ok s
+  | Result.Error e -> Result.Error e
 
 let default_conv cv_pb env t1 t2 =
     gen_conv cv_pb env t1 t2

kernel/conversion.mli

@@ -14,29 +14,24 @@ open Environ
 (***********************************************************************
   s conversion functions *)
 
-exception NotConvertible
-
-type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
+type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result
 type 'a extended_conversion_function =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:CClosure.evar_handler ->
-  'a -> 'a -> unit
+  'a -> 'a -> (unit, unit) result
 
 type conv_pb = CONV | CUMUL
 
-type 'a universe_compare = {
-  (* Might raise NotConvertible *)
-  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
-  compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
+type ('a, 'err) universe_compare = {
+  compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
+  compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
   compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
-    UVars.Instance.t -> UVars.Instance.t -> 'a -> 'a;
+    UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
-type 'a universe_state = 'a * 'a universe_compare
-
-type 'b generic_conversion_function = 'b universe_state -> constr -> constr -> 'b
+type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
 
-type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraints.t
+type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> constr -> constr -> ('a, 'err option) result
 
 val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array ->
   UVars.Instance.t -> UVars.Instance.t -> Sorts.QUConstraints.t
@@ -45,27 +40,26 @@ val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int
 val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
 
 val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
-  'a * 'a universe_compare -> 'a * 'a universe_compare
+  'a * ('a, 'err) universe_compare -> ('a, 'err option) result * ('a, 'err) universe_compare
 
 (* [flex] should be true for constants, false for inductive types and
 constructors. *)
 val convert_instances : flex:bool -> UVars.Instance.t -> UVars.Instance.t ->
-  'a * 'a universe_compare -> 'a * 'a universe_compare
+  'a * ('a, 'err) universe_compare -> ('a, 'err option) result * ('a, 'err) universe_compare
 
-(** This function never raise UnivInconsistency. *)
-val checked_universes : UGraph.t universe_compare
+(** This function never returns an non-empty error. *)
+val checked_universes : (UGraph.t, 'err) universe_compare
 
-(** These two functions can only raise NotConvertible *)
+(** These two functions can only fail with unit *)
 val conv : constr extended_conversion_function
 
 val conv_leq : types extended_conversion_function
 
-(** Depending on the universe state functions, this might raise
-  [UniverseInconsistency] in addition to [NotConvertible] (for better error
-  messages). *)
+(** The failure values depend on the universe state functions
+    (for better error messages). *)
 val generic_conv : conv_pb -> l2r:bool
   -> TransparentState.t -> env -> ?evars:CClosure.evar_handler
-  -> 'a generic_conversion_function
+  -> ('a, 'err) generic_conversion_function
 
 val default_conv     : conv_pb -> types kernel_conversion_function
 val default_conv_leq : types kernel_conversion_function