simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-26 11:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Change coq backend requirements

Browse source 
Remove the automatic clausification encoding of the coq backend, which
was slow because of the 'tauto' tactic. It was particularly a problem
for long problems, since the tauto tactic would take longer each time
because of the new hypotheses. The buren is now on the hands of the
functor argument, which hopefully should be able to do it better.
This commit is contained in:
Guillaume Bury 2017-08-16 11:49:51 +02:00
parent bd5fa2426b
commit 887de5d0af
2 changed files with 8 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/backend/coq.ml
View file

@ -32,7 +32,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
end)
let name c = c.S.St.name
let name_tmp c = c.S.St.name ^ "_tmp"
let pp_atom fmt a =
if a == S.St.(a.var.pa) then
@ -60,12 +59,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
in
aux M.empty c.S.St.atoms 0
let clausify fmt clause =
Format.fprintf fmt "(* Encoding theory clause %s into: %s *)@\n"
(name_tmp clause) (name clause);
Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n"
(name clause) pp_clause clause (name_tmp clause)
let clause_iter m format fmt clause =
let aux atom = Format.fprintf fmt format (M.find atom m) in
Array.iter aux clause.S.St.atoms
@ -121,14 +114,11 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let clause = node.S.conclusion in
match node.S.step with
| S.Hypothesis ->
A.prove_hyp fmt (name_tmp clause) clause;
clausify fmt clause
A.prove_hyp fmt (name clause) clause
| S.Assumption ->
A.prove_assumption fmt (name_tmp clause) clause;
clausify fmt clause
A.prove_assumption fmt (name clause) clause
| S.Lemma _ ->
A.prove_lemma fmt (name_tmp clause) clause;
clausify fmt clause
A.prove_lemma fmt (name clause) clause
| S.Duplicate (p, l) ->
let c = (S.expand p).S.conclusion in
elim_duplicate fmt clause c l

6
src/backend/coq.mli
View file

@ -31,7 +31,11 @@ module type Arg = sig
val prove_assumption : Format.formatter -> string -> assumption -> unit
(** Proving function for hypotheses, lemmas and assumptions.
[prove_x fmt name x] should prove [x], and be such that after
executing it, [x] is among the coq hypotheses under the name [name]. *)
executing it, [x] is among the coq hypotheses under the name [name].
The hypothesis should be the encoding of the given clause, i.e
for a clause [a \/ not b \/ c], the proved hypothesis should be:
[ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
one in the atoms array of the clause. *)
end