Fix bug affecting algebra tactics

_CoqProject.test

@@ -27,6 +27,7 @@ tests/test_tactic.v
 tests/test_elaborator.v
 tests/test_ltac.v
 tests/test_ltac2.v
+tests/test_ltac3.v
 tests/test_cache_async.v
 tests/test_COQ_ELPI_ATTRIBUTES.v
 tests/perf_calls.v

src/coq_elpi_HOAS.ml

@@ -752,21 +752,19 @@ let in_elpi_primitive ~depth state i =
 
 (* {{{ HOAS : Evd.evar_map -> elpi *************************************** *)
 
-let command_mode =
-  S.declare ~name:"coq-elpi:command-mode"
-    ~init:(fun () -> true)
-    ~start:(fun x -> x)
-    ~pp:(fun fmt b -> Format.fprintf fmt "%b" b)
-
 module CoqEngine_HOAS : sig 
 
   val show_coq_engine : ?with_univs:bool -> coq_engine -> string
 
   val engine : coq_engine S.component
 
-  val from_env_keep_univ_of_sigma : Environ.env -> Evd.evar_map -> coq_engine
   val from_env_sigma : Environ.env -> Evd.evar_map -> coq_engine
 
+  (* when the env changes under the hood, we can adapt sigma or drop it but keep
+     its constraints *)
+  val from_env_keep_univ_of_sigma : env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+  val from_env_keep_univ_and_sigma : env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+
 end = struct
 
  let pp_coq_engine ?with_univs fmt { sigma } =
@@ -782,10 +780,18 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un
 
  let from_env env = from_env_sigma env (Evd.from_env env)
 
- let from_env_keep_univ_of_sigma env sigma0 =
+ let from_env_keep_univ_and_sigma ~env0 ~env sigma0 =
+   assert(env0 != env);
    let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
-   let sigma = Evd.from_ctx (UState.demote_global_univs env uctx) in
-   from_env_sigma env sigma
+   let uctx = UState.demote_global_univs env uctx in
+   from_env_sigma env (Evd.set_universe_context sigma0 uctx)
+
+let from_env_keep_univ_of_sigma ~env0 ~env sigma0 =
+   assert(env0 != env);
+   let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in
+  let uctx = UState.demote_global_univs env uctx in
+  from_env_sigma env (Evd.from_ctx uctx)
+
  let init () = from_env (Global.env ())
 
  let engine : coq_engine S.component =
@@ -1992,11 +1998,13 @@ and create_evar_unknown ~calldepth syntactic_constraints (coq_ctx : 'a coq_conte
 
   let state, (k, kty) = S.update_return engine state (fun ({ sigma } as e) ->
     let sigma, (ty, _) = Evarutil.new_type_evar ~naming:(Namegen.IntroFresh (Names.Id.of_string "e")) env sigma Evd.univ_rigid in
+    let ty_key, _ = EConstr.destEvar sigma ty in
     if on_ty then
-      { e with sigma }, (fst (EConstr.destEvar sigma ty), None)
+      { e with sigma }, (ty_key, None)
     else
       let sigma, t = Evarutil.new_evar ~typeclass_candidate:false ~naming:(Namegen.IntroFresh (Names.Id.of_string "e")) env sigma ty in
-      { e with sigma }, (fst (EConstr.destEvar sigma t), Some (fst (EConstr.destEvar sigma ty)))) in
+      let t_key, _ = EConstr.destEvar sigma t in
+      { e with sigma }, (t_key, Some ty_key)) in
   (*let state = S.update UVMap.uvmap state (UVMap.add elpi_evk k) in*)
   let state, gls_kty =
     match kty with
@@ -2043,14 +2051,6 @@ let lp2constr syntactic_constraints coq_ctx ~depth state t =
 
 (* ********************************* }}} ********************************** *)
 
-let push_env state name =
-  let open Context.Rel.Declaration in
-  S.update engine state (fun ({ global_env } as x) ->
-     { x with global_env = Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,C.mkProp)) global_env })
-let pop_env state =
-  S.update engine state (fun ({ global_env } as x) ->
-     { x with global_env = Environ.pop_rel_context 1 global_env })
-
 let set_sigma state sigma = S.update engine state (fun x -> { x with sigma })
 
 (* We reset the evar map since it depends on the env in which it was created *)
@@ -2060,22 +2060,31 @@ let grab_global_env state =
   if env == env0 then state
   else
     if Environ.universes env0 == Environ.universes env then
-      let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (Evd.from_ctx (Evd.evar_universe_context (get_sigma state)))) in
-      let state = UVMap.empty state in
+      let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (get_sigma state)) in
+      (*let state = UVMap.empty state in*)
       state  
     else
-      let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_of_sigma env (get_sigma state)) in
-      let state = UVMap.empty state in
+      let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_and_sigma ~env0 ~env (get_sigma state)) in
+      (*let state = UVMap.empty state in*)
       state
-let grab_global_env_drop_univs state =
+let grab_global_env_drop_univs_and_sigma state =
+  let env0 = get_global_env state in
   let env = Global.env () in
-  if env == get_global_env state then state
+  if env == env0 then state
   else
     let state = S.set engine state (CoqEngine_HOAS.from_env_sigma env (Evd.from_env env)) in
     let state = UVMap.empty state in
     state
 
-
+let grab_global_env_drop_sigma state =
+  let env0 = get_global_env state in
+  let env = Global.env () in
+  if env == env0 then state
+  else
+    let state = S.set engine state (CoqEngine_HOAS.from_env_keep_univ_of_sigma ~env0 ~env (get_sigma state)) in
+    let state = UVMap.empty state in
+    state
+
 
 let solvec = E.Constants.declare_global_symbol "solve"
 let msolvec = E.Constants.declare_global_symbol "msolve"
@@ -2112,8 +2121,6 @@ let sealed_goal2lp ~depth ~args ~in_elpi_tac_arg state k =
 
 let solvegoal2query sigma goals loc args ~in_elpi_tac_arg ~depth:calldepth state =
 
-  let state = S.set command_mode state false in (* tactic mode *)
-
   let state = S.set engine state (from_env_sigma (get_global_env state) sigma) in
 
   let state, gl, gls =
@@ -2147,7 +2154,6 @@ let customtac2query sigma goals loc text ~depth:calldepth state =
     let env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env in
     if not (Evd.is_undefined sigma goal) then
       err Pp.(str (Printf.sprintf "Evar %d is not a goal" (Evar.repr goal)));
-    let state = S.set command_mode state false in (* tactic mode *)
     let state = S.set engine state (from_env_sigma env sigma) in
     let state, elpi_goal_evar, elpi_raw_goal_evar, evar_decls = in_elpi_evar ~calldepth goal  state in
     let evar_concl, goal_ctx, goal_env =
@@ -3418,7 +3424,4 @@ let in_elpi_module_type (x : Declarations.module_type_body) = in_elpi_modty x
 
 (* ********************************* }}} ********************************** *)
 
-let command_mode = S.get command_mode
-
-
 (* vim:set foldmethod=marker: *)

src/coq_elpi_HOAS.mli

@@ -255,21 +255,16 @@ val body_of_constant :
   State.t -> Names.Constant.t -> Univ.Instance.t option ->
   State.t * EConstr.t option * Univ.Instance.t option
 
-val command_mode : State.t -> bool
 val grab_global_env : State.t -> State.t
-val grab_global_env_drop_univs : State.t -> State.t
+val grab_global_env_drop_univs_and_sigma : State.t -> State.t
+val grab_global_env_drop_sigma : State.t -> State.t
 
 val mk_decl : depth:int -> Name.t -> ty:term -> term
 (* Adds an Arg for the normal form with ctx_len context entry vars in scope *)
 
 val mk_def :
   depth:int -> Name.t -> bo:term -> ty:term -> term
 
-(* Push a name with a dummy type (just for globalization to work) and
- * pop it back *)
-val push_env : State.t -> Names.Name.t -> State.t
-val pop_env : State.t -> State.t
-
 val get_global_env : State.t -> Environ.env
 val get_sigma : State.t -> Evd.evar_map
 val update_sigma : State.t -> (Evd.evar_map -> Evd.evar_map) -> State.t

src/coq_elpi_builtins.ml

@@ -114,15 +114,15 @@ let on_global_state ?(abstract_exception=false) ?options api thunk = (); (fun st
     Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
   let state, result, gls = thunk state in
   match options with
-  | Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls
+  | Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
   | _ -> Coq_elpi_HOAS.grab_global_env state, result, gls)
 
 (* This is for stuff that is not monotonic in the env, eg section closing *)
 let on_global_state_does_rewind_env api thunk = (); (fun state ->
   if State.get tactic_mode state then
     Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
   let state, result, gls = thunk state in
-  Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls)
+  Coq_elpi_HOAS.grab_global_env_drop_sigma state, result, gls)
 
 let warn_if_contains_univ_levels ~depth t =
   let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
@@ -1988,7 +1988,7 @@ coq.env.begin-module Name MP :-
   MLCode(Pred("coq.env.end-module",
     Out(modpath, "ModPath",
     Full(unit_ctx, "end the current module that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state "coq.env.end-module" (fun state ->
+  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module" (fun state ->
      let mp = Declaremods.end_module () in
      state, !: mp, []))),
   DocAbove);
@@ -2023,7 +2023,7 @@ coq.env.begin-module-type Name :-
   MLCode(Pred("coq.env.end-module-type",
     Out(modtypath, "ModTyPath",
     Full(unit_ctx, "end the current module type that becomes known as ModPath *E*")),
-  (fun _ ~depth _ _ -> on_global_state "coq.env.end-module-type" (fun state ->
+  (fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module-type" (fun state ->
      let mp = Declaremods.end_modtype () in
      state, !: mp, []))),
   DocAbove);
@@ -3476,7 +3476,6 @@ fold_left over the terms, letin body comes before the type).
            proofview pv in
 
        Declare.Internal.export_side_effects (Evd.eval_side_effects sigma);
-       let sigma = Evd.drop_side_effects sigma in
 
        let state, assignments = set_current_sigma ~depth state sigma in
        state, !: subgoals, assignments

src/coq_elpi_glob_quotation.ml

@@ -28,7 +28,7 @@ let get_ctx, set_ctx, _update_ctx =
   let bound_vars =
     S.declare ~name:"coq-elpi:glob-quotation-bound-vars"
       ~init:(fun () -> None)
-      ~pp:(fun fmt -> function Some (x,_) -> () | None -> assert false)
+      ~pp:(fun fmt -> function Some (x,_) -> () | None -> ())
       ~start:(fun x -> x)
        in
   S.(get bound_vars, set bound_vars, update bound_vars)
@@ -58,6 +58,19 @@ let is_restricted_name =
   let rex = Str.regexp "_elpi_restricted_[0-9]+_" in
   fun s -> Str.(string_match rex (Id.to_string s) 0)
 
+
+let glob_environment : Environ.env S.component =
+  S.declare ~name:"coq-elpi:glob-environment"
+    ~pp:(fun _ _ -> ()) ~init:Global.env ~start:(fun _ -> Global.env ())
+
+let push_env state name =
+  let open Context.Rel.Declaration in
+  S.update glob_environment state (Environ.push_rel (LocalAssum(Context.make_annot name Sorts.Relevant,Constr.mkProp)))
+let pop_env state =
+  S.update glob_environment state (Environ.pop_rel_context 1)
+
+let get_glob_env state = S.get glob_environment state
+
 (* XXX: I don't get why we use a coq_ctx here *)
 let under_ctx name ty bo gterm2lp ~depth state x =
   let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
@@ -129,7 +142,7 @@ let noglsk f ~depth state = let state, x = f ~depth state in state, x, ()
 let rec gterm2lp ~depth state x =
   debug Pp.(fun () ->
       str"gterm2lp: depth=" ++ int depth ++
-      str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
+      str " term=" ++Printer.pr_glob_constr_env (get_glob_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
   | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p ->
       let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
@@ -160,7 +173,7 @@ let rec gterm2lp ~depth state x =
       let state, s = API.RawQuery.mk_Arg state ~name:(Printf.sprintf "type_%d" !type_gen) ~args:[] in
       state, in_elpi_flex_sort s
   | GSort(UNamed u) ->
-      let env = get_global_env state in
+      let env = get_glob_env state in
       in_elpi_sort ~depth state (sort_name env (get_sigma state) u)
   | GSort(_) -> nYI "(glob)HOAS for Type@{i j}"
 
@@ -270,7 +283,7 @@ let rec gterm2lp ~depth state x =
 
   | GCases(_, oty, [ t, (as_name, oind) ], bs) ->
       let open Declarations in
-      let env = get_global_env state in
+      let env = get_glob_env state in
       let ind, args_name =
         match oind with
         | Some {CAst.v=ind, arg_names} -> ind, arg_names
@@ -378,7 +391,7 @@ let coq_quotation ~depth state loc src =
   in
   let glob =
     try
-      Constrintern.intern_constr (get_global_env state) (get_sigma state) ce
+      Constrintern.intern_constr (get_glob_env state) (get_sigma state) ce
     with e ->
       CErrors.user_err
         Pp.(str(API.Ast.Loc.show loc) ++str":" ++ spc() ++ CErrors.print_no_report e)

tests/test_ltac3.v

@@ -0,0 +1,24 @@
+
+From elpi Require Export elpi.
+From Coq Require Import ssreflect ssrfun ssrbool.
+
+Ltac ltac_foo := cut True; [ idtac | abstract (exact I) ].
+
+Record fooType := Foo { sort :> Type; }.
+Canonical unit_fooType := Foo unit.
+
+Elpi Tactic fail_foo.
+Elpi Accumulate lp:{{
+
+pred solve i:goal, o:list sealed-goal.
+solve (goal _ _ _ _ [_] as G) GS :-
+  coq.ltac.call "ltac_foo" [] G GS.
+
+}}.
+Elpi Typecheck.
+
+Goal nat.
+Proof.
+elpi fail_foo ([the fooType of unit : Type]).
+exact (fun _ => 0).
+Qed.