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
module type S = Backend_intf.S
module type Arg = sig
type proof
type lemma
type formula
val pp : Format.formatter -> formula -> unit
val prove : Format.formatter -> lemma -> unit
val context : Format.formatter -> proof -> unit
end
module Make(S : Msat.S)(A : Arg with type formula := S.formula
and type lemma := S.lemma
and type proof := S.proof) = struct
module P = S.Proof
let pp_nl fmt = Format.fprintf fmt "@\n"
let fprintf fmt format = Format.kfprintf pp_nl fmt format
let _clause_name = S.Clause.name
let _pp_clause fmt c =
let rec aux fmt = function
| [] -> ()
| a :: r ->
let f, pos =
if S.Atom.sign a then
S.Atom.formula a, true
else
S.Atom.formula (S.Atom.neg a), false
in
fprintf fmt "%s _b %a ->@ %a"
(if pos then "_pos" else "_neg") A.pp f aux r
in
fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
let context fmt p =
fprintf fmt "(; Embedding ;)";
fprintf fmt "Prop : Type.";
fprintf fmt "_proof : Prop -> Type.";
fprintf fmt "(; Notations for clauses ;)";
fprintf fmt "_pos : Prop -> Prop -> Type.";
fprintf fmt "_neg : Prop -> Prop -> Type.";
fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
A.context fmt p
let pp fmt p =
fprintf fmt "#NAME Proof.";
fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
context fmt p;
()
end