Skip to content

Commit 8390862

Browse files
tlringertlringer
committed
finally
1 parent f6cdaa9 commit 8390862

13 files changed

+770
-2
lines changed

‎.gitignore

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
*.mli~
2+
*.ml~
3+
*.aux
4+
*.glob
5+
*.vo
6+
*.vok
7+
*.vos
8+
*.o
9+
*.cmi
10+
*.cmx
11+
*.cmxs
12+
*.d
13+
*.a
14+
*.cmxa
15+
Makefile.coq
16+
Makefile.coq.conf
17+
src/g_tuto*.ml

‎LICENSE

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
This is free and unencumbered software released into the public domain.
2+
3+
Anyone is free to copy, modify, publish, use, compile, sell, or
4+
distribute this software, either in source code form or as a compiled
5+
binary, for any purpose, commercial or non-commercial, and by any
6+
means.
7+
8+
In jurisdictions that recognize copyright laws, the author or authors
9+
of this software dedicate any and all copyright interest in the
10+
software to the public domain. We make this dedication for the benefit
11+
of the public at large and to the detriment of our heirs and
12+
successors. We intend this dedication to be an overt act of
13+
relinquishment in perpetuity of all present and future rights to this
14+
software under copyright law.
15+
16+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
17+
EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
18+
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
19+
IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
20+
OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
21+
ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
22+
OTHER DEALINGS IN THE SOFTWARE.
23+
24+
For more information, please refer to <http://unlicense.org>

‎Makefile

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
ifeq "$(COQBIN)" ""
2+
COQBIN=$(dir $(shell which coqtop))/
3+
endif
4+
5+
%: Makefile.coq
6+
7+
Makefile.coq: _CoqProject
8+
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
9+
10+
tests: all
11+
@$(MAKE) -C tests -s clean
12+
@$(MAKE) -C tests -s all
13+
14+
-include Makefile.coq

‎README.md

+109-2
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,109 @@
1-
# plugin-tutorial
2-
Yet another plugin tutorial, this time as an exercise for 598
1+
This is a fun plugin tutorial for my Proof Automation class!
2+
3+
This tutorial helps familiarize people with plugin development. The goal
4+
is to implement a command with this syntax:
5+
6+
```
7+
Sub src1 src2 ... srcn with dst1 dst2 ... dstn in trm as name.
8+
```
9+
10+
This command substitutes each subterm of `trm` that is definitionally equal to `srci`
11+
with the corresponding term `desti`. Some tests in [./theories/Demo.v](Demo.v) that pass
12+
after implementing `Sub` correctly:
13+
14+
```
15+
(*
16+
* Turn 4 (sugar for (S (S (S (S 0))))) into
17+
* [1; 1; 1; 1] (sugar for (cons 1 (cons 1 ... nil))).
18+
* Do this by substituting the constructors of nat
19+
* with the constructors of lists.
20+
*)
21+
Sub O S with (@nil nat) (cons 1) in 4 as list_4.
22+
Lemma test1:
23+
list_4 = (cons 1 (cons 1 (cons 1 (cons 1 nil)))).
24+
Proof.
25+
reflexivity.
26+
Qed.
27+
28+
(*
29+
* Convert unary natural numbers to binary numbers!
30+
*)
31+
Require Import Coq.NArith.BinNatDef Coq.NArith.BinNat.
32+
Sub O S with N.zero N.succ in 256 as two_fifty_six_binary.
33+
Lemma test2:
34+
two_fifty_six_binary = 256%N.
35+
Proof.
36+
reflexivity.
37+
Qed.
38+
39+
(*
40+
* Convert the addition function of unary into an addition
41+
* function defined over binary!
42+
*)
43+
Sub nat nat_rec O S with N.t N.peano_rec N.zero N.succ in
44+
(fun (n m : nat) =>
45+
nat_rec
46+
(fun _ => nat -> nat)
47+
(fun m => m)
48+
(fun p add_p m => S (add_p m))
49+
n
50+
m)
51+
as add_bin.
52+
53+
Lemma test3:
54+
add_bin 128%N 12%N = 140%N.
55+
Proof.
56+
reflexivity.
57+
Qed.
58+
```
59+
60+
## Prerequisites
61+
62+
If you are not in my Proof Automation class, please first set up
63+
Coq 8.14 and CoqIDE according to [these instructions](https://dependenttyp.es/classes/artifacts/6-languages.html). Please also set up emacs.
64+
65+
If you are in my Proof Automation class, you have already done this :).
66+
67+
## Installation
68+
69+
Configure your opam environment:
70+
71+
```
72+
opam switch 4.12.0
73+
eval $(opam env)
74+
```
75+
76+
Set up OCaml development tools for plugin development:
77+
78+
```
79+
opam install merlin
80+
opam install tuareg
81+
opam user-setup install
82+
eval $(opam env)
83+
```
84+
85+
Add this line to your .emacs to configure emacs to use those development tools:
86+
87+
```
88+
add-to-list 'auto-mode-alist '("\\.mlg$" . tuareg-mode) t)
89+
```
90+
91+
Build the plugin:
92+
93+
```
94+
make .merlin
95+
make
96+
```
97+
98+
You will get an error at the very end when it builds the Coq file, but that's just
99+
because you haven't implemented the command yet :).
100+
101+
## Getting Started
102+
103+
Open [Demo.v](./theories/Demo.v) in CoqIDE, and open [g_tuto1.mlg](./src/g_tuto1.mlg)
104+
in Emacs alongside it. Follow the instructions in [g_tuto1.mlg](./src/g_tuto1.mlg)
105+
to familiarize yourself with plugin development, then implement the `Sub` command.
106+
Have fun!
107+
108+
109+

‎_CoqProject

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
-R theories Tuto1
2+
-I src
3+
4+
theories/Loader.v
5+
theories/Demo.v
6+
7+
src/termutils.mli
8+
src/termutils.ml
9+
src/exercise.mli
10+
src/exercise.ml
11+
src/g_tuto1.mlg
12+
src/tuto1_plugin.mlpack

‎src/exercise.ml

+64
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
open EConstr
2+
open Termutils
3+
4+
(*
5+
* Count the number of occurrences of terms equal to src in trm.
6+
* Make some simplifying assumptions about the format of trm
7+
* (no pattern matching, no fixpoints, no lets, and so on).
8+
*
9+
* I have done this one for you, to help you figure out how to implement sub.
10+
* I tried to use the state monad only when I felt like it added clarity,
11+
* but if you find it confusing, please ask for help.
12+
*)
13+
let rec count env src trm sigma =
14+
let sigma, is_eq = Termutils.equal env src trm sigma in
15+
if is_eq then
16+
sigma, 1
17+
else
18+
match kind sigma trm with
19+
| Constr.Lambda (n, t, b) -> (* fun (n : t) => b *)
20+
let sigma, count_t = count env src t sigma in
21+
let sigma, count_b = count (push_local (n, t) env) src b sigma in
22+
sigma, count_t + count_b
23+
| Constr.Prod (n, t, b) -> (* forall (n : t), b *)
24+
let sigma, count_t = count env src t sigma in
25+
let sigma, count_b = count (push_local (n, t) env) src b sigma in
26+
sigma, count_t + count_b
27+
| Constr.App (f, args) -> (* f args *)
28+
let sigma, count_f = count env src f sigma in
29+
let sigma, count_args =
30+
Termutils.map_state_array
31+
(count env src)
32+
args
33+
sigma
34+
in sigma, Array.fold_left (fun b a -> b + a) count_f count_args
35+
| _ ->
36+
sigma, 0
37+
38+
(*
39+
* Substitute all occurrences of terms equal to src in trm with dst.
40+
* Make some simplifying assumptions about the format of trm
41+
* (no pattern matching, no fixpoints, not lets, and so on).
42+
*
43+
* HINT 1: You will want to use the mkLambda, mkProd, and mkApp functions
44+
* defined in EConstr: https://github.com/coq/coq/blob/v8.14/engine/eConstr.mli
45+
*
46+
* HINT 2: If you are totally stuck, try copying and pasting the body of
47+
* each case of count, then adapting it to return the substituted term
48+
* instead of a number. The function will have almost exactly the same
49+
* structure.
50+
*)
51+
let sub env (src, dst) trm sigma = (*<- you'll need to add "rec" before "sub"*)
52+
let sigma, is_eq = Termutils.equal env src trm sigma in
53+
if is_eq then
54+
sigma, trm (* <- your implementation here *)
55+
else
56+
match kind sigma trm with
57+
| Constr.Lambda (n, t, b) -> (* fun (n : t) => b *)
58+
sigma, trm (* <- your implementation here *)
59+
| Constr.Prod (n, t, b) -> (* prod (n : t) => b *)
60+
sigma, trm (* <- your implementation here *)
61+
| Constr.App (f, args) -> (* f args *)
62+
sigma, trm (* <- your implementation here *)
63+
| _ ->
64+
sigma, trm

‎src/exercise.mli

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
open Evd
2+
open Termutils
3+
open Environ
4+
5+
(*
6+
* Count the number of occurrences of terms equal to src in trm.
7+
* Make some simplifying assumptions about the format of trm
8+
* (no pattern matching, no fixpoints, no lets, and so on).
9+
*
10+
* I have done this one for you, to help you figure out how to implement sub.
11+
*)
12+
val count :
13+
env -> (* environment *)
14+
EConstr.t -> (* src *)
15+
EConstr.t -> (* trm *)
16+
evar_map -> (* state *)
17+
int state (* stateful count *)
18+
19+
(*
20+
* Substitute all occurrences of terms equal to src in trm with dst.
21+
* Make some simplifying assumptions about the format of trm
22+
* (no pattern matching, no fixpoints, not lets, and so on).
23+
*)
24+
val sub :
25+
env -> (* environment *)
26+
(EConstr.t * EConstr.t) -> (* src, dst *)
27+
EConstr.t -> (* trm *)
28+
evar_map -> (* state *)
29+
EConstr.t state (* stateful updated term *)

0 commit comments

Comments
 (0)