From 48444b04b208335611cd94cbce0b9e87fb5e6196 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@bedrocksystems.com>
Date: Fri, 12 Apr 2024 13:05:33 +0200
Subject: [PATCH] Fix coq-elpi#618: pick correct initial synterp state in
 interp phase.

---
 src/coq_elpi_vernacular.ml  | 14 +++++++++-----
 src/coq_elpi_vernacular.mli |  4 ++--
 tests/test_synterp.v        | 34 ++++++++++++++++++++++++++++++++++
 3 files changed, 45 insertions(+), 7 deletions(-)

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
index adca0cd3a..409dc6ca1 100644
--- a/src/coq_elpi_vernacular.ml
+++ b/src/coq_elpi_vernacular.ml
@@ -528,6 +528,7 @@ module Synterp = struct
   let run_program loc name ~atts args =
     get_and_compile name |> Option.map (fun (program, raw_args) ->
       let loc = Coq_elpi_utils.of_coq_loc loc in
+      let initial_synterp_state = Vernacstate.Synterp.freeze () in
       let query ~depth state =
         let state, args, gls = EU.map_acc
           (Coq_elpi_arg_HOAS.in_elpi_cmd_synterp ~depth)
@@ -539,7 +540,7 @@ module Synterp = struct
         state, (loc, q), gls in
       try
         let relocate, synterplog = run_and_print ~print:false ~static_check:false name program (`Fun query) in
-        relocate "NewData", synterplog
+        initial_synterp_state, relocate "NewData", synterplog
       with Coq_elpi_builtins_synterp.SynterpAction.Error x -> err x)
 
   let run_in_program ?program query =
@@ -573,11 +574,14 @@ module Interp = struct
         |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign ~strict:true env))
         |> List.map (Coq_elpi_arg_HOAS.Cmd.interp (Ltac_plugin.Tacinterp.default_ist ()) env sigma)
       in
-      let synterplog, synterm =
+      let initial_synterp_state, synterplog, synterm=
         match syndata with
-        | None -> Coq_elpi_builtins_synterp.SynterpAction.RZipper.empty, fun ~target:_ ~depth -> Stdlib.Result.Ok ET.mkDiscard
-        | Some (relocate_term,log) -> log, relocate_term in
-      let initial_synterp_state = Vernacstate.Synterp.freeze () in
+        | None ->
+          let initial_synterp_state = Vernacstate.Synterp.freeze () in
+          initial_synterp_state,
+          Coq_elpi_builtins_synterp.SynterpAction.RZipper.empty,
+          fun ~target:_ ~depth -> Stdlib.Result.Ok ET.mkDiscard
+        | Some (initial_synterp_state,relocate_term,log) -> initial_synterp_state, log, relocate_term in
       let query ~depth state =
         let state, args, gls = EU.map_acc
           (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
diff --git a/src/coq_elpi_vernacular.mli b/src/coq_elpi_vernacular.mli
index 3c8af160c..ce7c05310 100644
--- a/src/coq_elpi_vernacular.mli
+++ b/src/coq_elpi_vernacular.mli
@@ -52,12 +52,12 @@ module type Common = sig
 end
 
 module Synterp : sig include Common
-val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Cmd.raw list -> ((target:Elpi.API.State.t -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option
+val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Cmd.raw list -> (Vernacstate.Synterp.t * (target:Elpi.API.State.t -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option
 val run_in_program : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option
 
 end
 module Interp : sig include Common
-val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> syndata:((target:Elpi.API.State.t -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option -> Cmd.raw list -> unit
+val run_program : Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> syndata:(Vernacstate.Synterp.t * (target:Elpi.API.State.t -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option -> Cmd.raw list -> unit
 val run_in_program : ?program:qualified_name -> syndata:Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option -> Elpi.API.Ast.Loc.t * string -> unit
 end
 
diff --git a/tests/test_synterp.v b/tests/test_synterp.v
index 3e16290ae..4f4ddd72a 100644
--- a/tests/test_synterp.v
+++ b/tests/test_synterp.v
@@ -173,5 +173,39 @@ Elpi Accumulate lp:{{
 }}.
 Elpi foo3.
 
+(* The example below is taken from https://github.com/LPCIC/coq-elpi/issues/618.
+   It tests that the initial synterp state during the interp phase corresponds
+   to the initial synterp state as opposed to the final synterp state. *)
+
+Class c := C {}.
+Definition h : c := C.
+
+Elpi Command ElpiStart.
+#[synterp] Elpi Accumulate lp:{{/*(*/
+    main _ :-
+        coq.env.begin-section "A".
+/*)*/}}.
+Elpi Accumulate lp:{{/*(*/
+    main _ :-
+        coq.env.begin-section "A".
+/*)*/}}.
+Elpi Typecheck.
+Elpi Export ElpiStart.
+
+Elpi Command ElpiTCEnd.
+#[synterp] Elpi Accumulate lp:{{/*(*/
+    main _ :-
+        coq.env.end-section.
+/*)*/}}.
+Elpi Accumulate lp:{{/*(*/
+    main _ :-
+        coq.locate "h" I,
+        @global! => coq.TC.declare-instance I 0,
+        coq.env.end-section.
+/*)*/}}.
+Elpi Typecheck.
+Elpi Export ElpiTCEnd.
 
+ElpiStart.
 
+ElpiTCEnd.