Skip to content

Switch axiom replay to use exact rather than a custom apply variant #1029

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

Open
oskgo wants to merge 1 commit into
base: main
Choose a base branch
from
+13 −24
Open

Switch axiom replay to use exact rather than a custom apply variant #1029

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
22 changes: 0 additions & 22 deletions src/ecHiGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -562,25 +562,6 @@ let process_apply_bwd ~implicits mode (ff : ppterm) (tc : tcenv1) =
with (EcLowGoal.Apply.NoInstance _) as err ->
tc_error_exn !!tc err

(* -------------------------------------------------------------------- *)
let process_exacttype qs (tc : tcenv1) =
let env, hyps, _ = FApi.tc1_eflat tc in
let p =
try EcEnv.Ax.lookup_path (EcLocation.unloc qs) env
with LookupFailure cause ->
tc_error !!tc "%a" EcEnv.pp_lookup_failure cause
in
let tys =
List.map (fun a -> EcTypes.tvar a)
(EcEnv.LDecl.tohyps hyps).h_tvar in
let pt = ptglobal ~tys p in

try
EcLowGoal.t_apply pt tc
with InvalidGoalShape ->
let ppe = EcPrinting.PPEnv.ofenv env in
tc_error !!tc "cannot apply %a@." (EcPrinting.pp_axname ppe) p

(* -------------------------------------------------------------------- *)
let process_apply_fwd ~implicits (pe, hyp) tc =
let module E = struct exception NoInstance end in
Expand Down Expand Up @@ -2048,9 +2029,6 @@ let process_apply ~implicits ((infos, orv) : apply_t * prevert option) tc =
| `Alpha pe ->
process_apply_bwd ~implicits `Alpha pe tc

| `ExactType qs ->
process_exacttype qs tc

| `Top mode ->
let tc = process_apply_top tc in
if mode = `Exact then t_onall process_done tc else tc
Expand Down
1 change: 0 additions & 1 deletion src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1034,7 +1034,6 @@ type apply_info = [
| `Apply of ppterm list * [`Apply|`Exact|`Alpha]
| `Top of [`Apply|`Exact|`Alpha]
| `Alpha of ppterm
| `ExactType of pqsymbol
]

(* -------------------------------------------------------------------- *)
Expand Down
4 changes: 3 additions & 1 deletion src/ecThCloning.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,9 @@ end = struct
(* ------------------------------------------------------------------ *)
let ax_ovrd _oc ((proofs, evc) : state) name ((axd, mode) : ax_override) =
let loc = axd.pl_loc in
let tc = Papply (`ExactType axd, None) in
let tc = FPNamed (axd, None) in
let tc = { fp_mode = `Explicit; fp_head = tc; fp_args = []; } in
let tc = Papply (`Apply ([tc], `Exact), None) in
let tc = mk_loc loc (Plogic tc) in
let pr = { pthp_mode = `Named (name, mode);
pthp_tactic = Some tc; } in
Expand Down
10 changes: 10 additions & 0 deletions tests/clone-parametric-axiom.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
op gen ['a]: bool = true.
Comment thread
oskgo marked this conversation as resolved.
theory T.
axiom ax : gen<:bool>.
end T.
lemma lem: gen<:'a> by done.

clone T as T' with
axiom ax <- lem.
Loading