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.

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

Cswb #590

Closed
wants to merge 9 commits into from
Closed

Cswb #590

Changes from 1 commit
Commits
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
Prev Previous commit
Next Next commit
wip
Tragicus committed Feb 7, 2024
commit 44b52f3887d64a86abf34e1322d52c4c571e9506
24 changes: 13 additions & 11 deletions apps/coercion/src/coq_elpi_coercion_hook.mlg
Original file line number Diff line number Diff line change
@@ -28,17 +28,19 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
state, (loc, qatts), gls
in
let cprogram, _ = get_and_compile program in
match run ~static_check:false cprogram (`Fun query) with
| API.Execute.Success solution ->
let gls = Evar.Set.singleton goal_evar in
let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
if Evd.is_defined sigma goal_evar
then let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t)
else None
| API.Execute.NoMoreSteps
| API.Execute.Failure -> None
| exception (Coq_elpi_utils.LtacFail (level, msg)) -> None
match Interp.get_and_compile program with
| None -> None
| Some (cprogram, _) ->
match Interp.run ~static_check:false cprogram (`Fun query) with
| API.Execute.Success solution ->
let gls = Evar.Set.singleton goal_evar in
let sigma, _, _ = Coq_elpi_HOAS.solution2evd sigma solution gls in
if Evd.is_defined sigma goal_evar
then let t = if retype then Retyping.get_type_of env sigma goal else expected in Some (sigma, goal, t)
else None
| API.Execute.NoMoreSteps
| API.Execute.Failure -> None
| exception (Coq_elpi_utils.LtacFail (level, msg)) -> None

let add_coercion_hook =
let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in
2 changes: 1 addition & 1 deletion apps/tc/elpi/solver.elpi
Original file line number Diff line number Diff line change
@@ -90,4 +90,4 @@ solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
)
(GL = [seal G]).

main _.
main _.
2 changes: 2 additions & 0 deletions coq-builtin.elpi
Original file line number Diff line number Diff line change
@@ -1395,6 +1395,8 @@ external pred coq.sigma.print .
% If Ty is provided, then
% the inferred type is unified (see unify-leq) with it.
% Universe constraints are put in the constraint store.
% Supported attributes:
% - @no-tc! (default false, do not infer typeclasses)
external pred coq.typecheck i:term, o:term, o:diagnostic.

% [coq.typecheck-ty Ty U Diagnostic] typchecks a type Ty returning its
38 changes: 21 additions & 17 deletions src/coq_elpi_builtins.ml
Original file line number Diff line number Diff line change
@@ -90,17 +90,18 @@ let with_pp_options o f =
Detyping.print_evar_arguments := print_evar_arguments;
raise reraise

let with_no_tc ~no_tc f sigma =
if no_tc then
let typeclass_evars = Evd.get_typeclass_evars sigma in
let sigma = Evd.set_typeclass_evars sigma Evar.Set.empty in
let with_no_tc ~no_tc env f sigma =
let sigma, rc = if no_tc then
let typeclass_evars = Evd.get_typeclass_evars sigma in
let sigma = Evd.set_typeclass_evars sigma Evar.Set.empty in
let sigma, rc = f sigma in
let typeclass_evars = Evar.Set.filter (fun x ->
try ignore (Evd.find_undefined sigma x); true
with Not_found -> false) typeclass_evars in
try ignore (Evd.find_undefined sigma x); true
with Not_found -> false) typeclass_evars in
let sigma = Evd.set_typeclass_evars sigma typeclass_evars in
sigma, rc
else f sigma
else f sigma in
sigma, rc

let pr_econstr_env options env sigma t =
with_pp_options options.pp (fun () ->
@@ -3149,21 +3150,24 @@ is equivalent to Elpi Export TacName.|})))),
Full (proof_context,
{|typchecks a term T returning its type Ty. If Ty is provided, then
the inferred type is unified (see unify-leq) with it.
Universe constraints are put in the constraint store.|})))),
Universe constraints are put in the constraint store.
Supported attributes:
- @no-tc! (default false, do not infer typeclasses)|})))),
(fun t ety diag ~depth proof_context _ state ->
let no_tc = if proof_context.options.no_tc = Some true then true else false in
try
let sigma = get_sigma state in
let sigma, ty = Typing.type_of proof_context.env sigma t in
let sigma, ty = with_no_tc ~no_tc proof_context.env (fun sigma -> Typing.type_of proof_context.env sigma t) sigma in
match ety with
| Data ety ->
let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in
let state, assignments = set_current_sigma ~depth state sigma in
state, ?: None +! B.mkOK, assignments
let sigma = Evarconv.unify proof_context.env sigma ~with_ho:true Conversion.CUMUL ty ety in
let state, assignments = set_current_sigma ~depth state sigma in
(state, ?: None +! B.mkOK, assignments)
| NoData ->
let flags = Evarconv.default_flags_of TransparentState.full in
let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in
let state, assignments = set_current_sigma ~depth state sigma in
state, !: ty +! B.mkOK, assignments
let flags = Evarconv.default_flags_of TransparentState.full in
let sigma = Evarconv.solve_unif_constraints_with_heuristics ~flags ~with_ho:true proof_context.env sigma in
let state, assignments = set_current_sigma ~depth state sigma in
(state, !: ty +! B.mkOK, assignments)
with Pretype_errors.PretypeError (env, sigma, err) ->
match diag with
| Data B.OK ->
@@ -3613,7 +3617,7 @@ Supported attributes:
let open Proofview in let open Notations in
let focused_tac =
Unsafe.tclSETGOALS [with_empty_state goal] <*> tactic in
with_no_tc ~no_tc (fun sigma ->
with_no_tc ~no_tc proof_context.env (fun sigma ->
let _, pv = init sigma [] in
let (), pv, _, _ =
let vernac_state = Vernacstate.freeze_full_state () in