From 4500ecbc385203351b17dfa92003ee3c8286b5cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Wed, 6 Sep 2023 17:51:42 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#17955. (#93) --- Makefile | 20 +++++++- src/Common/Tactics/HintDbExtra.v.v818 | 1 + src/Common/Tactics/HintDbExtra.v.v819 | 1 + src/Common/Tactics/TransparentAbstract.v.v818 | 1 + src/Common/Tactics/TransparentAbstract.v.v819 | 1 + .../Tactics/hint_db_extra_plugin.mlg.v818 | 20 ++++++++ .../Tactics/hint_db_extra_plugin.mlg.v819 | 20 ++++++++ .../Tactics/hint_db_extra_tactics.ml.v818 | 50 +++++++++++++++++++ .../Tactics/hint_db_extra_tactics.ml.v819 | 50 +++++++++++++++++++ .../transparent_abstract_plugin.mlg.v818 | 25 ++++++++++ .../transparent_abstract_plugin.mlg.v819 | 25 ++++++++++ .../transparent_abstract_tactics.ml.v818 | 30 +++++++++++ .../transparent_abstract_tactics.ml.v819 | 30 +++++++++++ 13 files changed, 272 insertions(+), 2 deletions(-) create mode 100644 src/Common/Tactics/HintDbExtra.v.v818 create mode 100644 src/Common/Tactics/HintDbExtra.v.v819 create mode 100644 src/Common/Tactics/TransparentAbstract.v.v818 create mode 100644 src/Common/Tactics/TransparentAbstract.v.v819 create mode 100644 src/Common/Tactics/hint_db_extra_plugin.mlg.v818 create mode 100644 src/Common/Tactics/hint_db_extra_plugin.mlg.v819 create mode 100644 src/Common/Tactics/hint_db_extra_tactics.ml.v818 create mode 100644 src/Common/Tactics/hint_db_extra_tactics.ml.v819 create mode 100644 src/Common/Tactics/transparent_abstract_plugin.mlg.v818 create mode 100644 src/Common/Tactics/transparent_abstract_plugin.mlg.v819 create mode 100644 src/Common/Tactics/transparent_abstract_tactics.ml.v818 create mode 100644 src/Common/Tactics/transparent_abstract_tactics.ml.v819 diff --git a/Makefile b/Makefile index a7e0768a..2efec5e1 100644 --- a/Makefile +++ b/Makefile @@ -147,6 +147,20 @@ OTHERFLAGS += -w "-notation-overridden" ML4_OR_MLG := mlg EXTRA_PIPE_SED_FOR_COQPROJECT += | sed 's/@META@/META.coq-fiat-parsers/g' else +ifneq (,$(filter 8.18%,$(COQ_VERSION))) +EXPECTED_EXT:=.v818 +ML_DESCRIPTION := "Coq v8.18" +OTHERFLAGS += -w "-notation-overridden" +ML4_OR_MLG := mlg +EXTRA_PIPE_SED_FOR_COQPROJECT += | sed 's/@META@/META.coq-fiat-parsers/g' +else +ifneq (,$(filter 8.19%,$(COQ_VERSION))) +EXPECTED_EXT:=.v819 +ML_DESCRIPTION := "Coq v8.19" +OTHERFLAGS += -w "-notation-overridden" +ML4_OR_MLG := mlg +EXTRA_PIPE_SED_FOR_COQPROJECT += | sed 's/@META@/META.coq-fiat-parsers/g' +else # >= 8.5 if it exists NOT_EXISTS_LOC_DUMMY_LOC := $(call test_exists_ml_function,Loc.dummy_loc) @@ -157,8 +171,8 @@ ML4_OR_MLG := ml4 else ifdef COQ_VERSION # if not, we're just going to remake the relevant Makefile to include anyway, so we shouldn't error $(warning Unrecognized Coq version $(COQ_VERSION)) -EXPECTED_EXT:=.v817 -ML_DESCRIPTION := "Coq v8.17" +EXPECTED_EXT:=.v819 +ML_DESCRIPTION := "Coq v8.19" OTHERFLAGS += -w "-deprecated-appcontext -notation-overridden" ML4_OR_MLG := mlg EXTRA_PIPE_SED_FOR_COQPROJECT += | sed 's/@META@/META.coq-fiat-parsers/g' @@ -179,6 +193,8 @@ endif endif endif endif +endif +endif ML_COMPATIBILITY_FILES_PATTERN := src/Common/Tactics/hint_db_extra_tactics.ml src/Common/Tactics/hint_db_extra_plugin.@ML4_OR_MLG@ src/Common/Tactics/transparent_abstract_plugin.@ML4_OR_MLG@ src/Common/Tactics/transparent_abstract_tactics.ml src/Common/Tactics/TransparentAbstract.v src/Common/Tactics/HintDbExtra.v diff --git a/src/Common/Tactics/HintDbExtra.v.v818 b/src/Common/Tactics/HintDbExtra.v.v818 new file mode 100644 index 00000000..e2c2194e --- /dev/null +++ b/src/Common/Tactics/HintDbExtra.v.v818 @@ -0,0 +1 @@ +Declare ML Module "coq-fiat-parsers.hint_db_extra_plugin". diff --git a/src/Common/Tactics/HintDbExtra.v.v819 b/src/Common/Tactics/HintDbExtra.v.v819 new file mode 100644 index 00000000..e2c2194e --- /dev/null +++ b/src/Common/Tactics/HintDbExtra.v.v819 @@ -0,0 +1 @@ +Declare ML Module "coq-fiat-parsers.hint_db_extra_plugin". diff --git a/src/Common/Tactics/TransparentAbstract.v.v818 b/src/Common/Tactics/TransparentAbstract.v.v818 new file mode 100644 index 00000000..72d63c04 --- /dev/null +++ b/src/Common/Tactics/TransparentAbstract.v.v818 @@ -0,0 +1 @@ +Declare ML Module "coq-fiat-parsers.transparent_abstract_plugin". diff --git a/src/Common/Tactics/TransparentAbstract.v.v819 b/src/Common/Tactics/TransparentAbstract.v.v819 new file mode 100644 index 00000000..72d63c04 --- /dev/null +++ b/src/Common/Tactics/TransparentAbstract.v.v819 @@ -0,0 +1 @@ +Declare ML Module "coq-fiat-parsers.transparent_abstract_plugin". diff --git a/src/Common/Tactics/hint_db_extra_plugin.mlg.v818 b/src/Common/Tactics/hint_db_extra_plugin.mlg.v818 new file mode 100644 index 00000000..ab3e3e98 --- /dev/null +++ b/src/Common/Tactics/hint_db_extra_plugin.mlg.v818 @@ -0,0 +1,20 @@ +{ + +open Hint_db_extra_tactics +open Stdarg +open Ltac_plugin +open Tacarg + +} + +DECLARE PLUGIN "coq-fiat-parsers.hint_db_extra_plugin" + +TACTIC EXTEND foreach_db + | [ "foreach" "[" ne_preident_list(l) "]" "run" tactic(k) ] -> + { WITH_DB.with_hint_db l k } + END + +TACTIC EXTEND addto_db + | [ "add" constr(name) "to" ne_preident_list(l) ] -> + { WITH_DB.add_resolve_to_db (Hints.hint_constr (name, None)) l } + END diff --git a/src/Common/Tactics/hint_db_extra_plugin.mlg.v819 b/src/Common/Tactics/hint_db_extra_plugin.mlg.v819 new file mode 100644 index 00000000..ab3e3e98 --- /dev/null +++ b/src/Common/Tactics/hint_db_extra_plugin.mlg.v819 @@ -0,0 +1,20 @@ +{ + +open Hint_db_extra_tactics +open Stdarg +open Ltac_plugin +open Tacarg + +} + +DECLARE PLUGIN "coq-fiat-parsers.hint_db_extra_plugin" + +TACTIC EXTEND foreach_db + | [ "foreach" "[" ne_preident_list(l) "]" "run" tactic(k) ] -> + { WITH_DB.with_hint_db l k } + END + +TACTIC EXTEND addto_db + | [ "add" constr(name) "to" ne_preident_list(l) ] -> + { WITH_DB.add_resolve_to_db (Hints.hint_constr (name, None)) l } + END diff --git a/src/Common/Tactics/hint_db_extra_tactics.ml.v818 b/src/Common/Tactics/hint_db_extra_tactics.ml.v818 new file mode 100644 index 00000000..c5cc362f --- /dev/null +++ b/src/Common/Tactics/hint_db_extra_tactics.ml.v818 @@ -0,0 +1,50 @@ +module WITH_DB = + struct + open Tacticals + open Ltac_plugin + + (* Lift a constructor to an ltac value. *) + let to_ltac_val c = Tacinterp.Value.of_constr c + + let with_hint_db dbs tacK = + (* [dbs] : list of hint databases *) + (* [tacK] : tactic to run on a hint *) + Proofview.Goal.enter begin + fun gl -> + let syms = ref [] in + let _ = + List.iter (fun l -> + (* Fetch the searchtable from the database*) + let db = Hints.searchtable_map l in + (* iterate over the hint database, pulling the hint *) + (* list out for each. *) + Hints.Hint_db.iter (fun _ _ hintlist -> + syms := hintlist::!syms) db) dbs in + (* Now iterate over the list of list of hints, *) + List.fold_left + (fun tac hints -> + List.fold_left + (fun tac hint1 -> + Hints.FullHint.run hint1 + (fun hint2 -> + (* match the type of the hint to pull out the lemma *) + match hint2 with + Hints.Give_exact h + | Hints.Res_pf h + | Hints.ERes_pf h -> + let _, lem = Hints.hint_as_term h in + let this_tac = Tacinterp.Value.apply tacK [Tacinterp.Value.of_constr lem] in + tclORELSE this_tac tac + | _ -> tac)) + tac hints) + (tclFAIL (Pp.str "No applicable tactic!")) !syms + end + + let add_resolve_to_db lem db = + Proofview.Goal.enter begin + fun gl -> + let _ = Hints.add_hints ~locality:Hints.Local db (Hints.HintsResolveEntry [({ Typeclasses.hint_priority = Some 1 ; Typeclasses.hint_pattern = None },true,Hints.PathAny,lem)]) in + tclIDTAC + end + +end diff --git a/src/Common/Tactics/hint_db_extra_tactics.ml.v819 b/src/Common/Tactics/hint_db_extra_tactics.ml.v819 new file mode 100644 index 00000000..da53d0b0 --- /dev/null +++ b/src/Common/Tactics/hint_db_extra_tactics.ml.v819 @@ -0,0 +1,50 @@ +module WITH_DB = + struct + open Tacticals + open Ltac_plugin + + (* Lift a constructor to an ltac value. *) + let to_ltac_val c = Tacinterp.Value.of_constr c + + let with_hint_db dbs tacK = + (* [dbs] : list of hint databases *) + (* [tacK] : tactic to run on a hint *) + Proofview.Goal.enter begin + fun gl -> + let syms = ref [] in + let _ = + List.iter (fun l -> + (* Fetch the searchtable from the database*) + let db = Hints.searchtable_map l in + (* iterate over the hint database, pulling the hint *) + (* list out for each. *) + Hints.Hint_db.iter (fun _ _ hintlist -> + syms := hintlist::!syms) db) dbs in + (* Now iterate over the list of list of hints, *) + List.fold_left + (fun tac hints -> + List.fold_left + (fun tac hint1 -> + Hints.FullHint.run hint1 + (fun hint2 -> + (* match the type of the hint to pull out the lemma *) + match hint2 with + Hints.Give_exact h + | Hints.Res_pf h + | Hints.ERes_pf h -> + let _, lem = Hints.hint_as_term h in + let this_tac = Tacinterp.Value.apply tacK [Tacinterp.Value.of_constr lem] in + tclORELSE this_tac tac + | _ -> tac)) + tac hints) + (tclFAIL (Pp.str "No applicable tactic!")) !syms + end + + let add_resolve_to_db lem db = + Proofview.Goal.enter begin + fun gl -> + let _ = Hints.add_hints ~locality:Hints.Local db (Hints.HintsResolveEntry [({ Typeclasses.hint_priority = Some 1 ; Typeclasses.hint_pattern = None }, true, lem)]) in + tclIDTAC + end + +end diff --git a/src/Common/Tactics/transparent_abstract_plugin.mlg.v818 b/src/Common/Tactics/transparent_abstract_plugin.mlg.v818 new file mode 100644 index 00000000..a22f02b4 --- /dev/null +++ b/src/Common/Tactics/transparent_abstract_plugin.mlg.v818 @@ -0,0 +1,25 @@ +{ + +open Transparent_abstract_tactics +open Stdarg +open Ltac_plugin +open Tacarg + +} + +DECLARE PLUGIN "coq-fiat-parsers.transparent_abstract_plugin" + +TACTIC EXTEND transparentabstract +| [ "cache" tactic(tac) "as" ident(name)] +-> { TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) } +END + +TACTIC EXTEND abstracttermas +| [ "cache_term" constr(term) "as" ident(name) "run" tactic(tacK)] -> +{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK } +END + +TACTIC EXTEND abstractterm +| [ "cache_term" constr(term) "run" tactic(tacK) ] -> +{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK } +END diff --git a/src/Common/Tactics/transparent_abstract_plugin.mlg.v819 b/src/Common/Tactics/transparent_abstract_plugin.mlg.v819 new file mode 100644 index 00000000..a22f02b4 --- /dev/null +++ b/src/Common/Tactics/transparent_abstract_plugin.mlg.v819 @@ -0,0 +1,25 @@ +{ + +open Transparent_abstract_tactics +open Stdarg +open Ltac_plugin +open Tacarg + +} + +DECLARE PLUGIN "coq-fiat-parsers.transparent_abstract_plugin" + +TACTIC EXTEND transparentabstract +| [ "cache" tactic(tac) "as" ident(name)] +-> { TRANSPARENT_ABSTRACT.tclTRABSTRACT (Some name) (Tacinterp.tactic_of_value ist tac) } +END + +TACTIC EXTEND abstracttermas +| [ "cache_term" constr(term) "as" ident(name) "run" tactic(tacK)] -> +{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM (Some name) term tacK } +END + +TACTIC EXTEND abstractterm +| [ "cache_term" constr(term) "run" tactic(tacK) ] -> +{ TRANSPARENT_ABSTRACT.tclABSTRACTTERM None term tacK } +END diff --git a/src/Common/Tactics/transparent_abstract_tactics.ml.v818 b/src/Common/Tactics/transparent_abstract_tactics.ml.v818 new file mode 100644 index 00000000..333913e8 --- /dev/null +++ b/src/Common/Tactics/transparent_abstract_tactics.ml.v818 @@ -0,0 +1,30 @@ +module TRANSPARENT_ABSTRACT = + struct + open Names + open Ltac_plugin + + (* Lift a constr to an ltac value. *) + let to_ltac_val c = Tacinterp.Value.of_constr c + + (* Build a new definition for [term] with identifier [id] and call *) + (* the [tacK] tactic with the result. *) + let transparent_abstract_term ~name_op (term : EConstr.constr) tacK = + Proofview.Goal.enter begin + fun gl -> + let termType = Tacmach.pf_get_type_of gl term in + Abstract.cache_term_by_tactic_then ~opaque:false ~name_op + ~goal_type:(Some termType) + (Eauto.e_give_exact term) + (fun lem args -> Tacinterp.Value.apply tacK [to_ltac_val (EConstr.applist (lem, args))]) + end + + (* Default identifier *) + let anon_id = Id.of_string "anonymous" + + let tclTRABSTRACT name_op tac = Abstract.tclABSTRACT ~opaque:false name_op tac + + let tclABSTRACTTERM name_op term tacK = + (* What's the right default goal kind?*) + transparent_abstract_term ~name_op term tacK + + end diff --git a/src/Common/Tactics/transparent_abstract_tactics.ml.v819 b/src/Common/Tactics/transparent_abstract_tactics.ml.v819 new file mode 100644 index 00000000..333913e8 --- /dev/null +++ b/src/Common/Tactics/transparent_abstract_tactics.ml.v819 @@ -0,0 +1,30 @@ +module TRANSPARENT_ABSTRACT = + struct + open Names + open Ltac_plugin + + (* Lift a constr to an ltac value. *) + let to_ltac_val c = Tacinterp.Value.of_constr c + + (* Build a new definition for [term] with identifier [id] and call *) + (* the [tacK] tactic with the result. *) + let transparent_abstract_term ~name_op (term : EConstr.constr) tacK = + Proofview.Goal.enter begin + fun gl -> + let termType = Tacmach.pf_get_type_of gl term in + Abstract.cache_term_by_tactic_then ~opaque:false ~name_op + ~goal_type:(Some termType) + (Eauto.e_give_exact term) + (fun lem args -> Tacinterp.Value.apply tacK [to_ltac_val (EConstr.applist (lem, args))]) + end + + (* Default identifier *) + let anon_id = Id.of_string "anonymous" + + let tclTRABSTRACT name_op tac = Abstract.tclABSTRACT ~opaque:false name_op tac + + let tclABSTRACTTERM name_op term tacK = + (* What's the right default goal kind?*) + transparent_abstract_term ~name_op term tacK + + end