From f15c687dd973a6fa3f7fb4dd8b3f86491d2ee1fc Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 27 Jun 2024 18:42:44 +0200 Subject: [PATCH 1/3] [tc] Abstract type of overridden classes set --- .../tc/src/coq_elpi_class_tactics_takeover.ml | 60 +++++++++++++------ 1 file changed, 42 insertions(+), 18 deletions(-) diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/coq_elpi_class_tactics_takeover.ml index 00f09ed48..3fb018f66 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/coq_elpi_class_tactics_takeover.ml @@ -1571,13 +1571,44 @@ let elpi_fails program_name = "Please report this inconvenience to the authors of the program." ])) +module type M = sig + type elt + type t + val empty : t + val diff : t -> t -> t + val union : t -> t -> t + val add : elt -> t -> t + val gr2elt : Names.GlobRef.t -> elt + val mem : elt -> t -> bool + val strs2set : Libnames.qualid list -> t +end + +(* Set of overridden class *) +module OSet : M = struct + module M = GRSet + + type t = M.t + type elt = M.elt + let empty = M.empty + let diff = M.diff + let union = M.union + let add = M.add + let mem = M.mem + let gr2elt (x: Names.GlobRef.t) : elt = x + + let strs2set x = + let add_str x = add (str2gr x) in + let grl2set grl = List.fold_right add_str grl empty in + grl2set x + +end module Modes = struct (** override_mode *) type omode = - | AllButFor of GRSet.t - | Only of GRSet.t + | AllButFor of OSet.t + | Only of OSet.t type action = | Set of omode @@ -1587,21 +1618,19 @@ module Modes = struct let omodes = ref (CSMap.empty : omode CSMap.t) let create_solver_omode solver = - omodes := CSMap.add solver (Only GRSet.empty) !omodes + omodes := CSMap.add solver (Only OSet.empty) !omodes let takeover (qname, new_mode,c) = let name = qname2str qname in if c then create_solver_omode name else - let add_str x = GRSet.add (str2gr x) in - let grl2set grl = List.fold_right add_str grl GRSet.empty in let old_mode = CSMap.find name !omodes in let new_mode = match old_mode, new_mode with | _, Set(mode) -> mode - | AllButFor s, Add grl -> AllButFor (GRSet.diff s (grl2set grl)) - | AllButFor s, Rm grl -> AllButFor (GRSet.union s (grl2set grl)) - | Only s, Add grl -> Only (GRSet.union s (grl2set grl)) - | Only s, Rm grl -> Only (GRSet.diff s (grl2set grl)) + | AllButFor s, Add grl -> AllButFor (OSet.diff s (OSet.strs2set grl)) + | AllButFor s, Rm grl -> AllButFor (OSet.union s (OSet.strs2set grl)) + | Only s, Add grl -> Only (OSet.union s (OSet.strs2set grl)) + | Only s, Rm grl -> Only (OSet.diff s (OSet.strs2set grl)) in omodes := CSMap.set name new_mode !omodes @@ -1643,9 +1672,7 @@ module Solver = struct let ei = Evd.find_undefined sigma i in let ty = Evd.evar_concl ei in match Typeclasses.class_of_constr env sigma ty with - | Some (_,(((cl: typeclass),_),_)) -> - let cl_impl = cl.Typeclasses.cl_impl in - GRSet.mem cl_impl classes + | Some (_,((cl,_),_)) -> OSet.mem (OSet.gr2elt cl.cl_impl) classes | None -> default let covered omode env sigma s = @@ -1669,15 +1696,12 @@ end let set_solver_mode kind qname (l: Libnames.qualid list) = let cache_solver_mode = Modes.cache_solver_mode in - let empty = GRSet.empty in match kind with | AAdd -> Lib.add_leaf (cache_solver_mode (qname, Add l, false)) | ARm -> Lib.add_leaf (cache_solver_mode (qname, Rm l, false)) - | AAll -> Lib.add_leaf (cache_solver_mode (qname, Set (AllButFor empty), false)) - | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only empty), false)) - | ASet -> let set = ref empty in - List.iter (fun x -> set := GRSet.add (str2gr x) !set) l; - Lib.add_leaf (cache_solver_mode (qname, Set (Only !set), false)) + | AAll -> Lib.add_leaf (cache_solver_mode (qname, Set (AllButFor OSet.empty), false)) + | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false)) + | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only (OSet.strs2set l)), false)) let solver_register l = Lib.add_leaf (Solver.cache_solver (l, Create)); From ae7347691e73fe4f51b54c899b5ca8ec112bafe1 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 1 Jul 2024 15:59:11 +0200 Subject: [PATCH 2/3] [TC] bug fix: conversion str2gr should not be done in the cache this avoids a bug source reproducible with tests/test_import/f2.v --- .../tc/src/coq_elpi_class_tactics_takeover.ml | 28 +++++++++---------- apps/tc/tests/test_import/f1.v | 4 +++ apps/tc/tests/test_import/f2.v | 1 + 3 files changed, 19 insertions(+), 14 deletions(-) create mode 100644 apps/tc/tests/test_import/f1.v create mode 100644 apps/tc/tests/test_import/f2.v diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/coq_elpi_class_tactics_takeover.ml index 3fb018f66..035809037 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/coq_elpi_class_tactics_takeover.ml @@ -1580,7 +1580,8 @@ module type M = sig val add : elt -> t -> t val gr2elt : Names.GlobRef.t -> elt val mem : elt -> t -> bool - val strs2set : Libnames.qualid list -> t + val of_qualid_list : Libnames.qualid list -> t + end (* Set of overridden class *) @@ -1596,11 +1597,9 @@ module OSet : M = struct let mem = M.mem let gr2elt (x: Names.GlobRef.t) : elt = x - let strs2set x = - let add_str x = add (str2gr x) in - let grl2set grl = List.fold_right add_str grl empty in - grl2set x - + let of_qualid_list (x: Libnames.qualid list) : t = + let add s x = add (Coq_elpi_utils.locate_simple_qualid x) s in + List.fold_left add empty x end module Modes = struct @@ -1612,8 +1611,8 @@ module Modes = struct type action = | Set of omode - | Add of Libnames.qualid list - | Rm of Libnames.qualid list + | Add of OSet.t + | Rm of OSet.t let omodes = ref (CSMap.empty : omode CSMap.t) @@ -1627,10 +1626,10 @@ module Modes = struct let new_mode = match old_mode, new_mode with | _, Set(mode) -> mode - | AllButFor s, Add grl -> AllButFor (OSet.diff s (OSet.strs2set grl)) - | AllButFor s, Rm grl -> AllButFor (OSet.union s (OSet.strs2set grl)) - | Only s, Add grl -> Only (OSet.union s (OSet.strs2set grl)) - | Only s, Rm grl -> Only (OSet.diff s (OSet.strs2set grl)) + | AllButFor s, Add grl -> AllButFor (OSet.diff s grl) + | AllButFor s, Rm grl -> AllButFor (OSet.union s grl) + | Only s, Add grl -> Only (OSet.union s grl) + | Only s, Rm grl -> Only (OSet.diff s grl) in omodes := CSMap.set name new_mode !omodes @@ -1695,17 +1694,18 @@ end let set_solver_mode kind qname (l: Libnames.qualid list) = + let l = OSet.of_qualid_list l in let cache_solver_mode = Modes.cache_solver_mode in match kind with | AAdd -> Lib.add_leaf (cache_solver_mode (qname, Add l, false)) | ARm -> Lib.add_leaf (cache_solver_mode (qname, Rm l, false)) | AAll -> Lib.add_leaf (cache_solver_mode (qname, Set (AllButFor OSet.empty), false)) | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false)) - | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only (OSet.strs2set l)), false)) + | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only l), false)) let solver_register l = Lib.add_leaf (Solver.cache_solver (l, Create)); - Lib.add_leaf (Modes.cache_solver_mode (l, Add [], true)) + Lib.add_leaf (Modes.cache_solver_mode (l, Add OSet.empty, true)) let solver_activate l = Lib.add_leaf (Solver.cache_solver (l, Activate)) diff --git a/apps/tc/tests/test_import/f1.v b/apps/tc/tests/test_import/f1.v new file mode 100644 index 000000000..de8f271bc --- /dev/null +++ b/apps/tc/tests/test_import/f1.v @@ -0,0 +1,4 @@ +From elpi.apps Require Export tc. +From Coq Require Export Morphisms. + +Elpi TC Solver Override TC.Solver Rm Proper ProperProxy. diff --git a/apps/tc/tests/test_import/f2.v b/apps/tc/tests/test_import/f2.v new file mode 100644 index 000000000..efa2686e9 --- /dev/null +++ b/apps/tc/tests/test_import/f2.v @@ -0,0 +1 @@ +From elpi.apps.tc.tests.test_import Require Import f1. \ No newline at end of file From d082ec1e53ff84f24246812cb141f0b8e96c04f3 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 1 Jul 2024 20:19:42 +0200 Subject: [PATCH 3/3] [TC] correct shelf goal + raise Not_found if no solution lemma_with_max_impl.v tests the correct behavior Fixes #18 --- .../tc/src/coq_elpi_class_tactics_takeover.ml | 4 +- apps/tc/tests/lemma_with_max_impl.v | 63 +++++++++++++++++++ 2 files changed, 65 insertions(+), 2 deletions(-) create mode 100644 apps/tc/tests/lemma_with_max_impl.v diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/coq_elpi_class_tactics_takeover.ml index 035809037..74bd03471 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/coq_elpi_class_tactics_takeover.ml @@ -1655,11 +1655,11 @@ module Solver = struct match Coq_elpi_vernacular.Interp.run ~static_check:false cprogram (`Fun query) with | API.Execute.Success solution -> let sigma, sub_goals, to_shelve = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:true sigma solution (Evar.Set.of_list goals) in - let sigma = Evd.shelve sigma (sub_goals @ to_shelve) in + let sigma = Evd.shelve sigma sub_goals in sub_goals = [], sigma | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> elpi_fails program - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> elpi_fails program + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> raise Not_found } type action = diff --git a/apps/tc/tests/lemma_with_max_impl.v b/apps/tc/tests/lemma_with_max_impl.v new file mode 100644 index 000000000..02260a4a4 --- /dev/null +++ b/apps/tc/tests/lemma_with_max_impl.v @@ -0,0 +1,63 @@ +From elpi.apps Require Import tc. + +Class A (n : nat). +Instance a : A 0 := {}. + +Class B (n : nat). + +Class C (n : nat). +Instance b x: C x := {}. + +Lemma foo: forall (x n: nat) `{A x} `{C n}, True -> B n. Admitted. +Lemma bar: forall (n: nat) `{A n}, True -> B n. Admitted. + +Goal exists n, B n. +Proof. + eexists. + (* Note: `{A x} and `{C n} are solved with x = 0, n remains a hole *) + (* Moreover, True remains as active goal + a shelved goal remain for n *) + refine (foo _ _ _). + auto. + Unshelve. + constructor. +Qed. + +Goal exists x, B x. +Proof. + eexists. + (* Note: `{A x} is solved with x = 0 *) + refine (bar _ _). + auto. +Qed. + + +Goal exists x, C x. +Proof. + eexists. + apply _. + Unshelve. + constructor. +Qed. + +Class Decision (P : Type). + +Goal forall (A : Type) (P1: A -> Prop), + exists (P : A -> A -> A -> Prop), forall z y , (forall x, Decision (P1 x)) + -> forall x, Decision (P z y x). +Proof. + eexists; intros. + apply _. + Unshelve. + auto. +Qed. + +Elpi Tactic A. +Elpi Accumulate lp:{{ + msolve L _ :- coq.ltac.fail _ "[TC] fail to solve" L. +}}. +Goal exists n, B n. + eexists. + Fail apply _. +Abort. + +