Skip to content

Commit 2e6a11e

Browse files
lyonel2017strub
lyonel2017
authored and
strub
committed
Tactic to call Coq (interactively or not) on goals via Why3.
Example : require import AllCore. lemma test : forall x y, x + 2 * y <= 4 && 2 * x + y <= 4 => x + y < 3. proof. coq edit "test" (). qed. This can be proven using Lia.lia in the coq script. Once the coq script is working, replace `edit` with `check` or `fix` to check only the script, or check the script and run the editor if it fails.
1 parent 96f356b commit 2e6a11e

16 files changed

Lines changed: 457 additions & 48 deletions

‎src/ecCoq.ml‎

Lines changed: 243 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,243 @@
1+
(* -------------------------------------------------------------------- *)
2+
open EcUtils
3+
open EcLocation
4+
open EcFol
5+
open EcEnv
6+
open EcProvers
7+
8+
(* -------------------------------------------------------------------- *)
9+
module WCall_provers = Why3.Call_provers
10+
module WConf = Why3.Whyconf
11+
module WDriver = Why3.Driver
12+
module WEnv = Why3.Env
13+
module WTask = Why3.Task
14+
15+
(* -------------------------------------------------------------------- *)
16+
type coqenv = {
17+
config : WConf.config;
18+
main : WConf.main;
19+
driver : WDriver.driver;
20+
cnfprv : WConf.config_prover;
21+
prover : WConf.prover;
22+
}
23+
24+
(* -------------------------------------------------------------------- *)
25+
let call_prover_task ~(coqenv : coqenv) (call : WCall_provers.prover_call) =
26+
EcUtils.try_finally
27+
(fun () ->
28+
match (Why3.Call_provers.wait_on_call call).pr_answer with
29+
| Valid -> Some `Valid
30+
| Invalid -> Some `Invalid
31+
| _ -> None)
32+
(fun () ->
33+
WCall_provers.interrupt_call ~config:coqenv.main call)
34+
35+
(* -------------------------------------------------------------------- *)
36+
let run_batch ~(script : string) ~(coqenv : coqenv) (task : WTask.task) =
37+
let config = Why3.Whyconf.get_main coqenv.config in
38+
let config_mem = Why3.Whyconf.memlimit config in
39+
let config_time = Why3.Whyconf.timelimit config in
40+
let limit =
41+
Why3.Call_provers.{
42+
limit_time = config_time;
43+
limit_steps = 0;
44+
limit_mem = config_mem;
45+
}
46+
in
47+
let command =
48+
Why3.Whyconf.get_complete_command
49+
coqenv.cnfprv ~with_steps:false in
50+
let call =
51+
Why3.Driver.prove_task_prepared
52+
~old:script ~inplace:true
53+
~command ~limit ~config coqenv.driver task
54+
in call_prover_task ~coqenv call
55+
56+
(* -------------------------------------------------------------------- *)
57+
let editor_command ~(coqenv : coqenv) : string =
58+
try
59+
let editors = Why3.Whyconf.get_editors coqenv.config in
60+
let editors =
61+
Why3.Whyconf.Meditor.filter
62+
(fun _ a -> a.Why3.Whyconf.editor_name = "Emacs/ProofGeneral/Coq")
63+
editors
64+
in
65+
let _, ed = Why3.Whyconf.Meditor.max_binding editors in
66+
String.concat " " (ed.editor_command :: ed.editor_options)
67+
68+
with Not_found ->
69+
Why3.Whyconf.(default_editor (get_main coqenv.config))
70+
71+
(* -------------------------------------------------------------------- *)
72+
let script_file ~(name : string located) ~(ext : string) =
73+
let { pl_loc = loc; pl_desc = name; } = name in
74+
let file = loc.loc_fname in
75+
let path = Filename.dirname file in
76+
let path =
77+
if Filename.is_relative path then
78+
Filename.concat (Sys.getcwd ()) path
79+
else path in
80+
let path = Filename.concat path ".interactive" in
81+
let name =
82+
if String.is_empty name then
83+
let name = Filename.basename file in
84+
let name = Filename.remove_extension name in
85+
let l, r = loc.loc_start in
86+
Format.sprintf "%s-%d-%d" name l r
87+
else name
88+
in
89+
Format.sprintf "%s/%s%s" path name ext
90+
91+
(* -------------------------------------------------------------------- *)
92+
let update_script
93+
~(script : string)
94+
~(coqenv : coqenv)
95+
(task : WTask.task)
96+
=
97+
let backup = Format.sprintf "%s~" script in
98+
Sys.rename script backup;
99+
100+
let old = open_in backup in
101+
EcUtils.try_finally
102+
(fun () ->
103+
IO.pp_to_file ~filename:script
104+
(fun fmt -> ignore @@
105+
Why3.Driver.print_task_prepared ~old coqenv.driver fmt task))
106+
(fun () -> close_in old)
107+
108+
(* -------------------------------------------------------------------- *)
109+
let editor
110+
~(script : string)
111+
~(merge : bool)
112+
~(coqenv : coqenv)
113+
(task : WTask.task)
114+
=
115+
if merge then update_script ~script ~coqenv task;
116+
let command = editor_command ~coqenv in
117+
let config = WConf.get_main coqenv.config in
118+
let call = WCall_provers.call_editor ~command ~config script in
119+
ignore @@ call_prover_task ~coqenv call
120+
121+
(* -------------------------------------------------------------------- *)
122+
let prepare
123+
~(name : string located)
124+
~(coqenv : coqenv)
125+
(task : WTask.task)
126+
=
127+
let ext = Why3.Driver.file_of_task coqenv.driver "S" "T" task in
128+
let ext = Filename.extension ext in
129+
let script = script_file ~name ~ext in
130+
131+
if Sys.file_exists script then
132+
(script, true)
133+
else begin
134+
EcUtils.makedirs (Filename.dirname script);
135+
EcUtils.IO.pp_to_file ~filename:script
136+
(fun fmt -> ignore @@
137+
Why3.Driver.print_task_prepared coqenv.driver fmt task);
138+
(script, false)
139+
end
140+
141+
(* -------------------------------------------------------------------- *)
142+
let interactive
143+
~(name : string located)
144+
~(coqmode : coq_mode)
145+
~(coqenv : coqenv)
146+
(task : WTask.task)
147+
=
148+
let script, merge = prepare ~name ~coqenv task in
149+
150+
if merge then
151+
update_script ~script ~coqenv task;
152+
match coqmode with
153+
| Check ->
154+
run_batch ~script ~coqenv task
155+
156+
| Edit ->
157+
editor ~script ~merge ~coqenv task;
158+
run_batch ~script ~coqenv task
159+
160+
| Fix -> begin
161+
match run_batch ~script ~coqenv task with
162+
| Some `Valid as answer ->
163+
answer
164+
| _ ->
165+
editor ~script ~merge ~coqenv task;
166+
run_batch ~script ~coqenv task
167+
end
168+
169+
(* -------------------------------------------------------------------- *)
170+
let is_trivial (t : Why3.Task.task) =
171+
let goal = Why3.Task.task_goal_fmla t in
172+
Why3.Term.t_equal goal Why3.Term.t_true
173+
174+
(* -------------------------------------------------------------------- *)
175+
let build_proof_task
176+
~(notify : notify option)
177+
~(name : string located)
178+
~(coqmode : coq_mode)
179+
~(config : WConf.config)
180+
~(env : WEnv.env)
181+
(task : WTask.task)
182+
=
183+
let exception CoqNotFound in
184+
185+
try
186+
let coqenv =
187+
let (prover, cnfprv) =
188+
let fp = Why3.Whyconf.parse_filter_prover "Coq" in
189+
let provers = Why3.Whyconf.filter_provers config fp in
190+
begin
191+
match Why3.Whyconf.Mprover.is_empty provers with
192+
| false -> Why3.Whyconf.Mprover.max_binding provers
193+
| true -> raise CoqNotFound
194+
end
195+
in
196+
let main = Why3.Whyconf.get_main config in
197+
let driver =
198+
Why3.Driver.load_driver_for_prover
199+
main env cnfprv
200+
in { config; main; driver; cnfprv; prover; } in
201+
202+
let task = Why3.Driver.prepare_task coqenv.driver task in
203+
204+
if is_trivial task then
205+
Some `Valid
206+
else
207+
interactive ~name ~coqmode ~coqenv task
208+
209+
with
210+
| CoqNotFound ->
211+
notify |> oiter (fun notify -> notify `Critical (lazy (
212+
Format.asprintf "Prover Coq not installed or not configured"
213+
)));
214+
None
215+
216+
| exn ->
217+
notify |> oiter (fun notify -> notify `Critical (lazy (
218+
Format.asprintf "[Why3 Error] %a" Why3.Exn_printer.exn_printer exn
219+
)));
220+
None
221+
222+
(* -------------------------------------------------------------------- *)
223+
let check
224+
~(loc : EcLocation.t)
225+
~(name : string)
226+
?(notify : notify option)
227+
(pi : prover_infos)
228+
?(coqmode : coq_mode = Edit)
229+
(hyps : LDecl.hyps)
230+
(concl : form)
231+
=
232+
EcProvers.maybe_start_why3_server pi;
233+
234+
let config = EcProvers.get_w3_conf () in
235+
let env = EcProvers.get_w3_env () in
236+
let ec_env, hyps, tenv, decl = EcSmt.init hyps concl in
237+
238+
let execute_task toadd =
239+
let task = EcSmt.make_task tenv toadd decl in
240+
let result =
241+
build_proof_task ~notify ~name:(mk_loc loc name) ~coqmode ~config ~env task in
242+
Option.map (fun r -> r = `Valid) result
243+
in EcSmt.select ec_env pi hyps concl execute_task

‎src/ecCoq.mli‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
(* -------------------------------------------------------------------- *)
2+
open EcFol
3+
open EcEnv
4+
open EcProvers
5+
6+
(* -------------------------------------------------------------------- *)
7+
val check :
8+
loc:EcLocation.t
9+
-> name:string
10+
-> ?notify:notify
11+
-> prover_infos
12+
-> ?coqmode:coq_mode
13+
-> LDecl.hyps
14+
-> form
15+
-> bool

‎src/ecHiGoal.ml‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,21 @@ let process_smt ?loc (ttenv : ttenv) pi (tc : tcenv1) =
147147
| `Report ->
148148
t_seq (t_simplify ~delta:`No) (t_smt ~mode:(`Report loc) pi) tc
149149

150+
(* -------------------------------------------------------------------- *)
151+
152+
let process_coq ~loc ~name (ttenv : ttenv) coqmode pi (tc : tcenv1) =
153+
let pi = ttenv.tt_provers pi in
154+
155+
match ttenv.tt_smtmode with
156+
| `Admit ->
157+
t_admit tc
158+
159+
| (`Sloppy | `Strict) as mode ->
160+
t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode coqmode pi) tc
161+
162+
| `Report ->
163+
t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode:(`Report (Some loc)) coqmode pi) tc
164+
150165
(* -------------------------------------------------------------------- *)
151166
let process_clear symbols tc =
152167
let hyps = FApi.tc1_hyps tc in

‎src/ecHiGoal.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,7 @@ val process_generalize : ?doeq:bool -> genpattern list -> backward
7373
val process_move : ?doeq:bool -> ppterm list -> prevert -> backward
7474
val process_clear : psymbol list -> backward
7575
val process_smt : ?loc:EcLocation.t -> ttenv -> pprover_infos -> backward
76+
val process_coq : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward
7677
val process_apply : implicits:bool -> apply_t * prevert option -> backward
7778
val process_delta : und_delta:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward
7879
val process_rewrite : ttenv -> ?target:psymbol -> rwarg list -> backward

‎src/ecHiTacticals.ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) =
154154
| Pwlog (ids, b, f) -> process_wlog ~suff:b ids f
155155
| Pgenhave gh -> process_genhave ttenv gh
156156
| Prwnormal _ -> assert false
157+
| Pcoq (m, n, pi) -> process_coq ~loc:(loc t) ~name:n.pl_desc ttenv m pi
157158
in
158159
tx tc
159160

‎src/ecLexer.mll‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@
106106
"trivial" , TRIVIAL ; (* KW: tactic *)
107107
"auto" , AUTO ; (* KW: tactic *)
108108

109+
109110
(* Other tactics *)
110111
"idtac" , IDTAC ; (* KW: tactic *)
111112
"move" , MOVE ; (* KW: tactic *)
@@ -119,6 +120,10 @@
119120
"exact" , EXACT ; (* KW: bytac *)
120121
"assumption" , ASSUMPTION ; (* KW: bytac *)
121122
"smt" , SMT ; (* KW: bytac *)
123+
"coq" , COQ ; (* KW: bytac *)
124+
"check" , CHECK ; (* KW: bytac *)
125+
"edit" , EDIT ; (* KW: bytac *)
126+
"fix" , FIX ; (* KW: bytac *)
122127
"by" , BY ; (* KW: bytac *)
123128
"reflexivity" , REFLEX ; (* KW: bytac *)
124129
"done" , DONE ; (* KW: bytac *)

‎src/ecLowGoal.ml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2435,6 +2435,35 @@ let t_smt ~(mode:smtmode) pi tc =
24352435
then FApi.xmutate1 tc `Smt []
24362436
else error ()
24372437

2438+
(* -------------------------------------------------------------------- *)
2439+
let t_coq
2440+
~(loc : EcLocation.t)
2441+
~(name : string)
2442+
~(mode : smtmode)
2443+
(coqmode : EcProvers.coq_mode option)
2444+
(pi : EcProvers.prover_infos)
2445+
(tc : tcenv1)
2446+
=
2447+
let error () =
2448+
match mode with
2449+
| `Sloppy ->
2450+
tc_error !!tc ~catchable:true "cannot prove goal"
2451+
| `Strict ->
2452+
tc_error !!tc ~catchable:false "cannot prove goal (strict)"
2453+
| `Report loc ->
2454+
EcEnv.notify (FApi.tc1_env tc) `Critical
2455+
"%s: Coq call failed"
2456+
(loc |> omap EcLocation.tostring |> odfl "unknown");
2457+
t_admit tc
2458+
in
2459+
2460+
let env, hyps, concl = FApi.tc1_eflat tc in
2461+
let notify = (fun lvl (lazy s) -> EcEnv.notify env lvl "%s" s) in
2462+
2463+
if EcCoq.check ~loc ~name ~notify ?coqmode pi hyps concl
2464+
then FApi.xmutate1 tc `Smt []
2465+
else error ()
2466+
24382467
(* -------------------------------------------------------------------- *)
24392468
let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(depth = 1) (tc : tcenv1) =
24402469
let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in

‎src/ecLowGoal.mli‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -321,6 +321,14 @@ type smtmode = [`Sloppy | `Strict | `Report of EcLocation.t option]
321321

322322
val t_smt: mode:smtmode -> prover_infos -> FApi.backward
323323

324+
val t_coq:
325+
loc:EcLocation.t
326+
-> name:string
327+
-> mode:smtmode
328+
-> coq_mode option
329+
-> prover_infos
330+
-> FApi.backward
331+
324332
(* -------------------------------------------------------------------- *)
325333
val t_solve :
326334
?canfail:bool

0 commit comments

Comments
 (0)