Adapt w.r.t. coq/coq#17955. (#93)

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
 

src/Common/Tactics/HintDbExtra.v.v818

@@ -0,0 +1 @@
+Declare ML Module "coq-fiat-parsers.hint_db_extra_plugin".

src/Common/Tactics/HintDbExtra.v.v819

@@ -0,0 +1 @@
+Declare ML Module "coq-fiat-parsers.hint_db_extra_plugin".

src/Common/Tactics/TransparentAbstract.v.v818

@@ -0,0 +1 @@
+Declare ML Module "coq-fiat-parsers.transparent_abstract_plugin".

src/Common/Tactics/TransparentAbstract.v.v819

@@ -0,0 +1 @@
+Declare ML Module "coq-fiat-parsers.transparent_abstract_plugin".

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

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

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

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

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

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

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

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