blob: 9c11d19c279e473522d2dcf080d4962bae82334d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
Require Import Ltac2.Ltac2.
Import Ltac2.Notations.
(** Test calls to Ltac1 from Ltac2 *)
Ltac2 foo () := ltac1:(discriminate).
Goal true = false -> False.
Proof.
foo ().
Qed.
Goal true = false -> false = true.
Proof.
intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
Qed.
Goal true = false -> false = true.
Proof.
intros H; ltac1:(rewrite H); reflexivity.
Abort.
(** Variables do not cross the compatibility layer boundary. *)
Fail Ltac2 bar nay := ltac1:(discriminate nay).
Fail Ltac2 pose1 (v : constr) :=
ltac1:(pose $v).
(** Variables explicitly crossing the boundary must satisfy typing properties *)
Goal True.
Proof.
(* Wrong type *)
Fail ltac1:(x |- idtac) 0.
(* OK, and runtime has access to variable *)
ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)).
(* Same for ltac1val *)
Fail Ltac1.run (ltac1val:(x |- idtac) 0).
Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
Abort.
(** Test calls to Ltac2 from Ltac1 *)
Set Default Proof Mode "Classic".
Ltac foo := ltac2:(foo ()).
Goal true = false -> False.
Proof.
ltac2:(foo ()).
Qed.
Goal true = false -> False.
Proof.
foo.
Qed.
(** Variables do not cross the compatibility layer boundary. *)
Fail Ltac bar x := ltac2:(foo x).
Ltac mytac tac := idtac "wow".
Goal True.
Proof.
(** Fails because quotation is evaluated eagerly *)
Fail mytac ltac2:(fail).
(** One has to thunk thanks to the idtac trick *)
let t := idtac; ltac2:(fail) in mytac t.
constructor.
Qed.
|
