Merge pull request #101 from SkySkimmer/tac2plugin

Adapt to coq/coq#17533 (use correct plugin name in ltac2_extra external)

Makefile.local.common

@@ -23,8 +23,13 @@ ifneq (,$(filter 8.16%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v816
 ML_DESCRIPTION := "Coq v8.16"
 else
+ifneq (,$(filter 8.17%,$(COQ_VERSION)))
 EXPECTED_EXT:=.v817
 ML_DESCRIPTION := "Coq v8.17"
+else
+EXPECTED_EXT:=.v818
+ML_DESCRIPTION := "Coq v8.18"
+endif
 endif
 endif
 

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

@@ -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.v818

@@ -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.v818

@@ -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.v818

@@ -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.v818

@@ -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.v818

@@ -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.v818

@@ -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.v818

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

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

@@ -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 () = DeclareUctx.declare_universe_context ~poly:false 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.v818

@@ -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.v818

@@ -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.v818

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

src/Rewriter/Util/plugins/ltac2_extra.ml.v818

@@ -0,0 +1,19 @@
+open Ltac2_plugin
+open Tac2ffi
+open Tac2expr
+open Proofview.Notations
+
+let pname s = { mltac_plugin = "coq-rewriter.ltac2_extra"; mltac_tactic = s }
+
+let define_primitive name arity f =
+  Tac2env.define_primitive (pname name) (Tac2ffi.mk_closure arity f)
+
+let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
+  f (Tac2ffi.repr_to r0 x) (Tac2ffi.repr_to r1 y)
+end
+
+let () = define2 "constr_equal_nounivs" constr constr begin fun c1 c2 ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let b = EConstr.eq_constr_nounivs sigma c1 c2 in
+  Proofview.tclUNIT (Tac2ffi.of_bool b)
+end

src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg.v818

@@ -0,0 +1 @@
+DECLARE PLUGIN "coq-rewriter.ltac2_extra"

src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib.v818

@@ -0,0 +1,2 @@
+Ltac2_extra
+Ltac2_extra_plugin