Adapt to coq/coq#18624 (Tac2ffi / Tac2val split) (#149)

* Add separate files for v8.20

Everything except Makefile changes done with
```
for i in $(git ls-files "*.v819"); do cp $i ${i/v819/v820}; git add ${i/v819/v820}; done
```

* Adapt to coq/coq#18624 (Tac2ffi / Tac2val split)

Makefile.local.common

@@ -34,8 +34,13 @@ ifneq (,$(filter 8.18%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v818
 ML_DESCRIPTION := "Coq v8.18"
 else
+ifneq (,$(filter 8.19%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v819
 ML_DESCRIPTION := "Coq v8.19"
+else
+EXPECTED_EXT:=.v820
+ML_DESCRIPTION := "Coq v8.20"
+endif 
 endif
 endif
 endif

src/Rewriter/Util/Tactics2/Constr.v.v820

@@ -0,0 +1,100 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Require Rewriter.Util.Tactics2.Array.
+Require Rewriter.Util.Tactics2.Proj.
+Require Rewriter.Util.Tactics2.Option.
+Require Import Rewriter.Util.Tactics2.Iterate.
+Local Set Warnings Append "-masking-absolute-name".
+Require Import Rewriter.Util.plugins.Ltac2Extra.
+Import Ltac2.Constr.
+Import Ltac2.Bool.
+
+Ltac2 is_sort(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Sort _ => true
+  | _ => false
+  end.
+
+Module Unsafe.
+  Export Ltac2.Constr.Unsafe.
+
+  Ltac2 rec kind_nocast_gen kind (x : constr) :=
+    let k := kind x in
+    match k with
+    | Cast x _ _ => kind_nocast_gen kind x
+    | _ => k
+    end.
+
+  Ltac2 kind_nocast (x : constr) : kind := kind_nocast_gen kind x.
+
+  Module Case.
+    Ltac2 iter_invert (f : constr -> unit) (ci : case_invert) : unit :=
+      match ci with
+      | NoInvert => ()
+      | CaseInvert indices => Array.iter f indices
+      end.
+  End Case.
+
+  (** [iter f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+  Ltac2 iter (f : constr -> unit) (c : constr) : unit :=
+    match kind c with
+    | Rel _ => () | Meta _ => () | Var _ => () | Sort _ => () | Constant _ _ => () | Ind _ _ => ()
+    | Constructor _ _ => () | Uint63 _ => () | Float _ => ()
+    | Cast c _ t => f c; f t
+    | Prod b c => f (Binder.type b); f c
+    | Lambda b c => f (Binder.type b); f c
+    | LetIn b t c => f (Binder.type b); f t; f c
+    | App c l => f c; Array.iter f l
+    | Evar _ l => () (* not possible to iter in Ltac2... *)
+    | Case _ x iv y bl
+      => Array.iter f bl;
+         Case.iter_invert f iv;
+         match x with (x,_) => f x end;
+         f y
+    | Proj _p _ c => f c
+    | Fix _ _ tl bl =>
+        Array.iter (fun b => f (Binder.type b)) tl;
+        Array.iter f bl
+    | CoFix _ tl bl =>
+        Array.iter (fun b => f (Binder.type b)) tl;
+        Array.iter f bl
+    | Array _u t def ty =>
+        Array.iter f t; f def; f ty
+    end.
+
+  (** [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+  Ltac2 iter_with_binders (g : 'a -> 'a) (f : 'a -> constr -> unit) (n : 'a) (c : constr) : unit :=
+    match kind c with
+    | Rel _ => () | Meta _ => () | Var _ => () | Sort _ => () | Constant _ _ => () | Ind _ _ => ()
+    | Constructor _ _ => () | Uint63 _ => () | Float _ => ()
+    | Cast c _ t => f n c; f n t
+    | Prod b c => f n (Binder.type b); f (g n) c
+    | Lambda b c => f n (Binder.type b); f (g n) c
+    | LetIn b t c => f n (Binder.type b); f n t; f (g n) c
+    | App c l => f n c; Array.iter (f n) l
+    | Evar _ l => () (* not possible to iter in Ltac2... *)
+    | Case _ x iv y bl
+      => Array.iter (f n) bl;
+         Case.iter_invert (f n) iv;
+         match x with (x,_) => f n x end;
+         f n y
+    | Proj _p _ c => f n c
+    | Fix _ _ tl bl =>
+        Array.iter (fun b => f n (Binder.type b)) tl;
+        Array.iter (f (iterate g (Array.length tl) n)) bl
+    | CoFix _ tl bl =>
+        Array.iter (fun b => f n (Binder.type b)) tl;
+        Array.iter (f (iterate g (Array.length tl) n)) bl
+    | Array _u t def ty =>
+        Array.iter (f n) t; f n def; f n ty
+    end.
+End Unsafe.
+Import Unsafe.
+
+Ltac2 equal_nounivs : constr -> constr -> bool := Ltac2.Constr.equal_nounivs.

src/Rewriter/Util/Tactics2/DestCase.v.v820

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_case (kind) ].
+Ltac2 destCase (c : constr) :=
+  let k := kind c in
+  match k with
+  | Case a b c d e => let (b,_) := b in (a, b, c, d, e)
+  | _ => Control.throw (Not_a_case k)
+  end.

src/Rewriter/Util/Tactics2/DestProj.v.v820

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_proj (kind) ].
+Ltac2 destProj (c : constr) :=
+  let k := kind c in
+  match k with
+  | Proj p r v => (p, r, v)
+  | _ => Control.throw (Not_a_proj k)
+  end.

src/Rewriter/Util/Tactics2/Proj.v.v820

@@ -0,0 +1,5 @@
+Require Import Ltac2.Ltac2.
+Require Export Ltac2.Proj.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.
+Import Constr.Unsafe.

src/Rewriter/Util/plugins/Ltac2Extra.v.v820

@@ -0,0 +1,10 @@
+Require Import Ltac2.Ltac2.
+
+Declare ML Module "coq-rewriter.ltac2_extra".
+
+Module Ltac2.
+  Module Constr.
+    Export Ltac2.Constr.
+    Ltac2 @ external equal_nounivs : constr -> constr -> bool := "coq-rewriter.ltac2_extra" "constr_equal_nounivs".
+  End Constr.
+End Ltac2.

src/Rewriter/Util/plugins/RewriterBuild.v.v820

@@ -0,0 +1,10 @@
+Require Import Rewriter.Util.plugins.RewriterBuildRegistry.
+
+Declare ML Module "coq-rewriter.rewriter_build".
+
+Ltac Rewrite_lhs_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_lhs_for verified_rewriter_package.
+Ltac Rewrite_rhs_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_rhs_for verified_rewriter_package.
+Ltac Rewrite_for verified_rewriter_package := RewriteRules.Tactic.Rewrite_for verified_rewriter_package.
+
+Export Pre.RewriteRuleNotations.
+Export IdentifiersGenerateProofs.Compilers.pattern.ProofTactic.Settings.

src/Rewriter/Util/plugins/RewriterBuildRegistry.v.v820

@@ -0,0 +1,20 @@
+Require Export Rewriter.Util.plugins.RewriterBuildRegistryImports.
+
+Register Basic.GoalType.package_with_args as rewriter.basic_package_with_args.type.
+Register Basic.GoalType.base_elim_with_args as rewriter.base_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.ident_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.pattern_ident_elim_with_args.type.
+Register Basic.GoalType.ident_elim_with_args as rewriter.raw_ident_elim_with_args.type.
+Register ScrapedData.t_with_args as rewriter.scraped_data_with_args.type.
+Register rules_proofsT_with_args as rewriter.rules_proofs_with_args.type.
+Register InductiveHList.nil as rewriter.ident_list.nil.
+Register RewriteRules.GoalType.VerifiedRewriter_with_ind_args as rewriter.verified_rewriter_with_args.type.
+
+Ltac make_base_elim_with_args := Basic.PrintBase.make_base_elim.
+Ltac make_ident_elim_with_args := Basic.PrintIdent.make_ident_elim.
+Ltac make_pattern_ident_elim_with_args := Basic.PrintIdent.make_pattern_ident_elim.
+Ltac make_raw_ident_elim_with_args := Basic.PrintIdent.make_raw_ident_elim.
+Ltac make_basic_package_with_args := Basic.Tactic.make_package.
+Ltac make_scraped_data_with_args := Basic.ScrapeTactics.make_scrape_data.
+Ltac make_verified_rewriter_with_args := RewriteRules.Tactic.make_rewriter_all.
+Ltac make_rules_proofs_with_args := Basic.ScrapeTactics.make_rules_proofsT_with_args.

src/Rewriter/Util/plugins/StrategyTactic.v.v820

@@ -0,0 +1,35 @@
+Declare ML Module "coq-rewriter.strategy_tactic".
+
+(*
+(* TEST: *)
+
+Definition id0 {A} (x : A) := x.
+Definition id1 {A} (x : A) := x.
+Definition id2 {A} (x : A) := id1 x.
+Definition id3 {A} (x : A) := id1 x.
+Definition id4 := id1 O.
+
+(* Works locally *)
+Goal exists x : nat, id0 x = id4.
+Proof.
+  strategy 1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 O) end.
+  Undo.
+  strategy -1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+  reflexivity.
+Abort.
+
+(* works globally *)
+Goal exists x : nat, id0 x = id4.
+Proof.
+  strategy -1000 [id0];
+    eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+  reflexivity.
+Defined.
+
+Goal exists x : nat, id0 x = id4.
+Proof.
+  eexists; lazymatch goal with |- ?x = ?y => unify x y; constr_eq x (id0 id4) end.
+Abort.
+*)

src/Rewriter/Util/plugins/definition_by_tactic.ml.v820

@@ -0,0 +1,17 @@
+open Ltac_plugin
+
+let make_definition_by_tactic sigma ~poly (name : Names.Id.t) (ty : EConstr.t) (tac : unit Proofview.tactic) =
+  let cinfo = Declare.CInfo.make ~name ~typ:ty () in
+  let info = Declare.Info.make ~poly () in
+  let lemma = Declare.Proof.start ~cinfo ~info sigma in
+  let lemma, _ = Declare.Proof.by tac lemma in
+  let ids = Declare.Proof.save_regular ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None in
+  match ids with
+  | [Names.GlobRef.ConstRef cst] -> cst
+  | _ -> CErrors.user_err (Pp.str "Internal error in make_definition_by_tactic")
+
+let vernac_make_definition_by_tactic ~poly (name : Names.Id.t) (ty : Constrexpr.constr_expr) tac =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, ty) = Constrintern.interp_constr_evars env sigma ty in
+  ignore(make_definition_by_tactic sigma ~poly name ty (Tacinterp.interp tac))

src/Rewriter/Util/plugins/definition_by_tactic.mli.v820

@@ -0,0 +1,11 @@
+open Ltac_plugin
+
+val make_definition_by_tactic
+  : Evd.evar_map
+  -> poly:bool
+  -> Names.Id.t
+  -> EConstr.t
+  -> unit Proofview.tactic
+  -> Names.Constant.t
+
+val vernac_make_definition_by_tactic : poly:bool -> Names.Id.t -> Constrexpr.constr_expr -> Tacexpr.raw_tactic_expr -> unit

src/Rewriter/Util/plugins/definition_by_tactic_plugin.mlg.v820

@@ -0,0 +1,22 @@
+{
+
+open Stdarg
+open Ltac_plugin
+open Tacarg
+open Definition_by_tactic
+
+}
+
+DECLARE PLUGIN "coq-rewriter.definition_by_tactic"
+
+VERNAC COMMAND EXTEND DefinitionViaTactic CLASSIFIED AS SIDEFF
+  | [ "Make" "Definition" ":" constr(ty) ":=" tactic(tac) ] -> {
+    let poly = false in
+    let name = Namegen.next_global_ident_away (Names.Id.of_string "Unnamed_thm") Names.Id.Set.empty in
+    vernac_make_definition_by_tactic ~poly name ty tac
+  }
+  | [ "Make" "Definition" ident(name) ":" constr(ty) ":=" tactic(tac) ] -> {
+    let poly = false in
+    vernac_make_definition_by_tactic ~poly name ty tac
+  }
+END

src/Rewriter/Util/plugins/definition_by_tactic_plugin.mllib.v820

@@ -0,0 +1,2 @@
+Definition_by_tactic
+Definition_by_tactic_plugin

src/Rewriter/Util/plugins/inductive_from_elim.ml.v820

@@ -0,0 +1,82 @@
+open Constr
+open Genredexpr
+open Names
+open Context
+open Entries
+
+let rec make_constructor_types env sigma (avoid : Id.Set.t) (body : EConstr.t) =
+  match EConstr.kind sigma body with
+  | Prod (cname, cty, body) ->
+    if EConstr.Vars.noccurn sigma 1 body
+    then (* the rest does not depend on this term, so we treat it as a constructor *)
+      (* We pass the empty set on the inner next_name because we care about avoiding other constructor names, which we treat as extra global identifiers *)
+      let cname = Namegen.next_global_ident_away (Namegen.next_name_away cname.binder_name Id.Set.empty) avoid in
+      let avoid = Id.Set.add cname avoid in
+      let dummy_arg = EConstr.mkProp in
+      let (sigma, avoid, rest_ctors) = make_constructor_types env sigma avoid (EConstr.Vars.subst1 dummy_arg body) in
+      (sigma, avoid, (cname, cty) :: rest_ctors)
+    else
+      (* the rest does depend on this argument, so we treat it as part of the final conclusion, and consider ourselves done *)
+      (sigma, avoid, [])
+  | Var _ ->
+    (* we are at the end of the inductive chain *)
+    (sigma, avoid, [])
+  | _ ->
+    CErrors.user_err Pp.(str "Invalid non-arrow component of eliminator type:" ++ Printer.pr_econstr_env env sigma body)
+
+let make_inductive_from_elim sigma (name : Names.Id.t option) (elim_ty : EConstr.t) =
+  let env = Global.env () in
+  let (hnffun, _) = Redexpr.reduction_of_red_expr env Hnf in
+  let (sigma, elim_ty) = hnffun env sigma elim_ty in
+  match EConstr.kind sigma elim_ty with
+  | Prod (ind_name, ind_ty, body) ->
+    (* If the user gives a name explicitly, we use exactly that name;
+       if the user gives a name via a binder name, we are more fuzzy
+       and search for the next free global identifier *)
+    let name = match name with
+      | Some name -> name
+      | None -> Namegen.next_global_ident_away (Namegen.next_name_away ind_name.binder_name Id.Set.empty) Id.Set.empty
+    in
+    let body = EConstr.Vars.subst1 (EConstr.mkVar name) body in
+    let (sigma, _, ctor_types) = make_constructor_types env sigma (Id.Set.singleton name) body in
+    let ctor_type_to_constr cty =
+      EConstr.to_constr sigma (EConstr.Vars.subst_var sigma name cty)
+    in
+    let univs, ubinders = Evd.check_univ_decl ~poly:false sigma UState.default_univ_decl in
+    let uctx = match univs with
+    | UState.Monomorphic_entry ctx ->
+      let () = Global.push_context_set ~strict:true ctx in
+      Entries.Monomorphic_ind_entry
+    | UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
+    in
+    let mie = {
+      mind_entry_record = None;
+      mind_entry_finite = Declarations.Finite;
+      mind_entry_params = [];
+      mind_entry_inds = [{
+          mind_entry_typename = name;
+          mind_entry_arity = EConstr.to_constr sigma ind_ty;
+          mind_entry_consnames = List.map (fun (cname, cty) -> cname) ctor_types;
+          mind_entry_lc = List.map (fun (cname, cty) -> ctor_type_to_constr cty) ctor_types
+        }];
+      mind_entry_universes = uctx;
+      mind_entry_variance = None;
+      mind_entry_private = None;
+    } in
+    let sigma =
+      let uctx = Evd.evar_universe_context sigma in
+      let uctx = UState.demote_seff_univs (fst (Evd.universe_context_set sigma)) uctx in
+      Evd.set_universe_context sigma uctx
+    in
+    (sigma,
+     (DeclareInd.declare_mutual_inductive_with_eliminations
+        mie (univs, UnivNames.empty_binders) [([], List.map (fun _ -> []) ctor_types)],
+      0))
+  | _ ->
+    CErrors.user_err Pp.(str "Invalid non-arrow eliminator type:" ++ Printer.pr_econstr_env env sigma elim_ty)
+
+let vernac_make_inductive_from_elim name elim_ty =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let (sigma, elim_ty) = Constrintern.interp_constr_evars env sigma elim_ty in
+  ignore(make_inductive_from_elim sigma name elim_ty)

src/Rewriter/Util/plugins/inductive_from_elim.mli.v820

@@ -0,0 +1,3 @@
+val make_inductive_from_elim : Evd.evar_map -> Names.Id.t option -> EConstr.t -> Evd.evar_map * Names.inductive
+
+val vernac_make_inductive_from_elim : Names.Id.t option -> Constrexpr.constr_expr -> unit

src/Rewriter/Util/plugins/inductive_from_elim_plugin.mlg.v820

@@ -0,0 +1,17 @@
+{
+
+open Stdarg
+open Inductive_from_elim
+
+}
+
+DECLARE PLUGIN "coq-rewriter.inductive_from_elim"
+
+VERNAC COMMAND EXTEND InductiveViaElim CLASSIFIED AS SIDEFF
+  | [ "Make" "Inductive" "From" "Elim" "Type" constr(elim_ty) ] -> {
+    vernac_make_inductive_from_elim None elim_ty
+  }
+  | [ "Make" ident(name) ":=" "Inductive" "From" "Elim" "Type" constr(elim_ty) ] -> {
+    vernac_make_inductive_from_elim (Some name) elim_ty
+  }
+END

src/Rewriter/Util/plugins/inductive_from_elim_plugin.mllib.v820

@@ -0,0 +1,2 @@
+Inductive_from_elim
+Inductive_from_elim_plugin