simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fixes to the Coq backend

Browse source 
Formerly, clauses introduced by the theory were left as is, but it
should instead be 'clausified' i.e transformed into what msat expects
(which is an encoding of clauses).
This commit is contained in:
Guillaume Bury 2017-08-09 20:55:27 +02:00
parent 0119d04899
commit 04eb1ec1c5
1 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/backend/coq.ml
View file

@ -32,6 +32,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
end) end)
let name c = c.S.St.name let name c = c.S.St.name
let name_tmp c = c.S.St.name ^ "_or"
let pp_atom fmt a = let pp_atom fmt a =
if a == S.St.(a.var.pa) then if a == S.St.(a.var.pa) then
@ -63,7 +64,9 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
Format.fprintf fmt "@].@\n"; Format.fprintf fmt "@].@\n";
m m
let clausify let clausify fmt clause =
Format.fprintf fmt "assert (%s: %a).@\nintros; try destruct %s; auto. clear %s.@\n"
(name clause) pp_clause clause (name_tmp clause) (name_tmp clause)
let elim_duplicate fmt goal hyp _ = let elim_duplicate fmt goal hyp _ =
(** Printing info comment in coq *) (** Printing info comment in coq *)
@ -94,7 +97,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
Format.fprintf fmt "exact (%s%a).@\n" Format.fprintf fmt "exact (%s%a).@\n"
(name h1) (fun fmt -> Array.iter (fun b -> (name h1) (fun fmt -> Array.iter (fun b ->
if b == a then begin if b == a then begin
Format.fprintf fmt " (fun p => %s%a" Format.fprintf fmt " (fun p => %s%a)"
(name h2) (fun fmt -> (Array.iter (fun c -> (name h2) (fun fmt -> (Array.iter (fun c ->
if c == a.S.St.neg then if c == a.S.St.neg then
Format.fprintf fmt " (fun np => np p)" Format.fprintf fmt " (fun np => np p)"
@ -110,11 +113,14 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let clause = node.S.conclusion in let clause = node.S.conclusion in
match node.S.step with match node.S.step with
| S.Hypothesis -> | S.Hypothesis ->
A.prove_hyp fmt (name clause) clause A.prove_hyp fmt (name_tmp clause) clause;
clausify fmt clause
| S.Assumption -> | S.Assumption ->
A.prove_assumption fmt (name clause) clause A.prove_assumption fmt (name_tmp clause) clause;
clausify fmt clause
| S.Lemma _ -> | S.Lemma _ ->
A.prove_lemma fmt (name clause) clause A.prove_lemma fmt (name_tmp clause) clause;
clausify fmt clause
| S.Duplicate (p, l) -> | S.Duplicate (p, l) ->
let c = (S.expand p).S.conclusion in let c = (S.expand p).S.conclusion in
elim_duplicate fmt clause c l elim_duplicate fmt clause c l
@ -130,7 +136,7 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let aux () node = let aux () node =
Format.fprintf fmt "%a@\n@\n" (prove_node h) node Format.fprintf fmt "%a@\n@\n" (prove_node h) node
in in
Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n"; Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n@\n";
S.fold aux () p S.fold aux () p
end end