[rfc] Introduce a new ERASEcast kind for evaluation using verified erasure …

dev/top_printers.ml

@@ -343,6 +343,7 @@ let cast_kind_display k =
   | VMcast -> "VMcast"
   | DEFAULTcast -> "DEFAULTcast"
   | NATIVEcast -> "NATIVEcast"
+  | ERASEcast -> "ERASEcast"
 
 let constr_display csr =
   let rec term_display c = match kind c with

interp/constrexpr_ops.ml

@@ -655,7 +655,7 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
   | CCast (p,Some Constr.DEFAULTcast, t) ->
     CPatCast (coerce_to_cases_pattern_expr p,t)
   | CLambdaN _ | CProdN _ | CSort _ | CLetIn _ | CGeneralization _
-  | CRef (_, Some _) | CCast (_, (Some (VMcast|NATIVEcast) | None), _)
+  | CRef (_, Some _) | CCast (_, (Some (VMcast|NATIVEcast|ERASEcast) | None), _)
   | CFix _ | CCoFix _ | CApp _ | CProj _ | CCases _ | CLetTuple _ | CIf _
   | CPatVar _ | CEvar _
   | CNotation (_,_,(_,_,_,_::_))

kernel/constr.ml

@@ -34,7 +34,7 @@ type existential_key = Evar.t
 type metavariable = int
 
 (* This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | ERASEcast
 
 (* This defines Cases annotations *)
 type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
@@ -1221,6 +1221,7 @@ let hash_cast_kind = function
 | VMcast -> 0
 | NATIVEcast -> 1
 | DEFAULTcast -> 2
+| ERASEcast -> 3
 
 (* Exported hashing fonction on constr, used mainly in plugins.
    Slight differences from [snd (hash_term t)] above: it ignores binders. *)

kernel/constr.mli

@@ -98,7 +98,7 @@ val mkType : Univ.Universe.t -> types
 
 
 (** This defines the strategy to use for verifiying a Cast *)
-type cast_kind = VMcast | NATIVEcast | DEFAULTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast | ERASEcast
 
 (** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the
    type t{_ 2} (that means t2 is declared as the type of t1). *)

kernel/eraseconv.ml

@@ -0,0 +1,75 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Conversion
+
+(** The erase evaluation function can either return an evaluated term or an error if the
+    evaluated term cannot be read back *)
+type erase_evaluation_function =
+  Environ.env -> Constr.t -> types -> (Constr.t, unit) result
+
+let erase_evaluation : erase_evaluation_function option ref = ref None
+
+let install_erase_conv fn =
+  match !erase_evaluation with
+  | None -> erase_evaluation := Some fn
+  | Some _ -> CErrors.anomaly Pp.(str"Attempting to install erasure evaluation twice!")
+
+let evaluate_term env c ty =
+  match !erase_evaluation with
+  | None -> Result.Error ()
+  | Some ev -> ev env c ty
+
+let evaluate_args env ctx args =
+  let open Context.Rel.Declaration in
+  if Int.equal (Array.length args) 0 then args else
+  let newargs = Array.make (Array.length args) args.(0) in
+  let ctx = Vars.smash_rel_context ctx in
+  let rec aux ctx n =
+    match ctx with
+    | LocalAssum (_, ty) :: ctx ->
+      let arg' =
+        match evaluate_term env args.(n) ty with
+        | Result.Ok arg' -> arg'
+        | Result.Error () -> args.(n)
+      in
+      newargs.(n) <- arg';
+      (* ctx is a telescope (reverse context) *)
+      aux (List.rev (Vars.subst1_rel_context arg' (List.rev ctx))) (succ n)
+    | LocalDef _ :: _ -> assert false (* Context is smashed beforehand *)
+    | [] -> ()
+  in
+  let () = aux (List.rev ctx) 0 in
+  newargs
+
+let erase_eval env expected_type =
+  let hd, args = Constr.decompose_app expected_type in
+  match Constr.kind hd with
+  | Ind (ind, u) ->
+    if Array.length args > 0 then
+      let specif = (Inductive.lookup_mind_specif env ind, u) in
+      let indty = Inductive.type_of_inductive specif in
+      let paramsctxt = (fst (fst specif)).Declarations.mind_params_ctxt in
+      let nparams = List.length paramsctxt in
+      let ctx, concl = Term.decompose_prod_n_decls nparams indty in
+      let params, indices = CArray.chop (fst (fst specif)).Declarations.mind_nparams args in
+      let instconcl = Vars.(substl (subst_of_rel_context_instance ctx params) concl) in
+      let indsctx, _ = Term.destArity instconcl in
+      let indices' = evaluate_args env indsctx indices in
+      let newty = Term.appvectc hd (Array.append params indices') in
+      Result.Ok newty
+    else Result.Error ()
+  | _ -> Result.Error ()
+
+let erase_conv pb env ty ty' =
+  match erase_eval env ty' with
+  | Result.Ok newty -> default_conv pb env ty newty
+  | Result.Error () -> Result.Error ()

kernel/eraseconv.mli

@@ -0,0 +1,24 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Constr
+open Conversion
+
+val erase_eval : Environ.env -> Constr.t -> (Constr.t, unit) result
+
+val erase_conv : conv_pb -> types kernel_conversion_function
+
+(** The erase evaluation function can either return an evaluated term or an error if the
+    evaluated term cannot be read back *)
+type erase_evaluation_function =
+  Environ.env -> Constr.t -> types -> (Constr.t, unit) result
+
+(** Link a specific evaluation function. By default it is the function always returning an error. *)
+val install_erase_conv : erase_evaluation_function -> unit

kernel/typeops.ml

@@ -375,6 +375,8 @@ let check_cast env c ct k expected_type =
     | NATIVEcast ->
       let sigma = Genlambda.empty_evars env in
       Nativeconv.native_conv CUMUL sigma env ct expected_type
+    | ERASEcast ->
+      Eraseconv.erase_conv CUMUL env ct expected_type
   in
   match ans with
   | Result.Ok () -> ()

parsing/g_constr.mlg

@@ -180,6 +180,8 @@ GRAMMAR EXTEND Gram
                  { CAst.make ~loc @@ CCast(c1, Some VMcast, c2) }
       | c1 = term; "<<:"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, Some NATIVEcast, c2) }
+      | c1 = term; "<<<:"; c2 = term LEVEL "200" ->
+                 { CAst.make ~loc @@ CCast(c1, Some ERASEcast, c2) }
       | c1 = term; ":>"; c2 = term LEVEL "200" ->
                  { CAst.make ~loc @@ CCast(c1, None, c2) }
       | c1 = term; ":"; c2 = term LEVEL "200" ->

plugins/ltac2/tac2core.ml

@@ -743,6 +743,7 @@ let () =
 let () = define "constr_cast_default" (ret valexpr) (of_cast DEFAULTcast)
 let () = define "constr_cast_vm" (ret valexpr) (of_cast VMcast)
 let () = define "constr_cast_native" (ret valexpr) (of_cast NATIVEcast)
+let () = define "constr_cast_erase" (ret valexpr) (of_cast ERASEcast)
 
 let () =
   define "constr_in_context" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c ->

pretyping/glob_ops.ml

@@ -143,7 +143,8 @@ let cast_kind_eq t1 t2 = let open Constr in match t1, t2 with
   | DEFAULTcast, DEFAULTcast
   | VMcast, VMcast
   | NATIVEcast, NATIVEcast -> true
-  | (DEFAULTcast | VMcast | NATIVEcast), _ -> false
+  | ERASEcast, ERASEcast -> true
+  | (DEFAULTcast | VMcast | NATIVEcast | ERASEcast), _ -> false
 
 let matching_var_kind_eq k1 k2 = match k1, k2 with
 | FirstOrderPatVar ido1, FirstOrderPatVar ido2 -> Id.equal ido1 ido2

pretyping/pretyping.ml

@@ -1528,6 +1528,19 @@ struct
               error_actual_type ?loc !!env sigma cj tval
                 (ConversionFailed (!!env,cty,tval))
           end
+        | Some ERASEcast ->
+            let tval = nf_evar sigma tval in
+            let exp = EConstr.to_constr_opt sigma tval in
+            begin
+              match exp with
+              | Some exp ->
+                (match Eraseconv.erase_eval !!env exp with
+                | Result.Ok newexp -> pretype (mk_tycon (EConstr.of_constr newexp)) env sigma c, tval
+                | Result.Error () -> user_err ?loc Pp.(str"Erasure evaluation failed for type" ++ spc () ++
+                  quote (Termops.Internal.print_constr_env !!env sigma tval)))                  
+              | None -> user_err ?loc Pp.(str"Erasure casts do not support evars in the expected type:" ++
+                  quote (Termops.Internal.print_constr_env !!env sigma tval))
+            end
         | None | Some DEFAULTcast ->
           pretype (mk_tycon tval) env sigma c, tval
       in

printing/ppconstr.ml

@@ -607,6 +607,7 @@ let pr_cast = let open Constr in function
     | Some DEFAULTcast -> str ":"
     | Some VMcast-> str "<:"
     | Some NATIVEcast -> str "<<:"
+    | Some ERASEcast -> str "<<<:"
     | None -> str ":>"
 
 type raw_or_glob_genarg =

test-suite/failure/EraseConv.v

@@ -0,0 +1,2 @@
+Fail Check (2 <<<: nat).
+

user-contrib/Ltac2/Constr.v

@@ -344,6 +344,7 @@ Module Cast.
   Ltac2 @ external default : cast := "rocq-runtime.plugins.ltac2" "constr_cast_default".
   Ltac2 @ external vm : cast := "rocq-runtime.plugins.ltac2" "constr_cast_vm".
   Ltac2 @ external native : cast := "rocq-runtime.plugins.ltac2" "constr_cast_native".
+  Ltac2 @ external erase : cast := "rocq-runtime.plugins.ltac2" "constr_cast_erase".
 
   Ltac2 @ external equal : cast -> cast -> bool := "rocq-runtime.plugins.ltac2" "constr_cast_equal".