Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix bug affecting algebra tactics #438

Merged
merged 8 commits into from
Mar 9, 2023
Merged

Fix bug affecting algebra tactics #438

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
19f99cf
test
gares Mar 1, 2023
b3c9d7b
remove useless state component
gares Mar 2, 2023
e51431a
remove useless assert false
gares Mar 2, 2023
b527f22
quotations: use a dedicated environment
gares Mar 2, 2023
cbf7ff6
harder test using abstract
gares Mar 2, 2023
c263128
clarify env rewindin
gares Mar 3, 2023
d035549
API: int/float->uint63/float64
gares Mar 4, 2023
2e9984b
clarify API for side effects
gares Mar 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,10 @@
# Changelog

## UNRELEASED

### API:
- New `coq.int->uint63` and `coq.float->float64`

## [1.17.0] - 13/02/2023

Requires Elpi 1.16.5 and Coq 8.17.
Expand Down
1 change: 1 addition & 0 deletions _CoqProject.test
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 8 additions & 0 deletions coq-builtin.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1066,10 +1066,18 @@ type proj projection -> int -> primitive-value. % primitive projection
% elpi integer I. Fails if it does not fit.
external pred coq.uint63->int i:uint63, o:int.

% [coq.int->uint63 I U] Transforms an elpi integer I into a primitive
% unsigned integer U. Fails if I is negative.
external pred coq.int->uint63 i:int, o:uint63.

% [coq.float64->float F64 F] Transforms a primitive float on 64 bits to an
% elpi one. Currently, it should not fail.
external pred coq.float64->float i:float64, o:float.

% [coq.float->float64 F F64] Transforms an elpi float F to a primitive float
% on 64 bits. Currently, it should not fail.
external pred coq.float->float64 i:float, o:float64.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% API for extra logical objects
Expand Down
67 changes: 34 additions & 33 deletions src/coq_elpi_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 } =
Expand All @@ -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
gares marked this conversation as resolved.
Show resolved Hide resolved
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 =
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)
Expand All @@ -2060,22 +2060,29 @@ 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
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
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"
Expand Down Expand Up @@ -2112,8 +2119,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 =
Expand Down Expand Up @@ -2147,7 +2152,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 =
Expand Down Expand Up @@ -3418,7 +3422,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: *)
9 changes: 2 additions & 7 deletions src/coq_elpi_HOAS.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading