WIP: add dedukti output (not functional yet)

.merlin

@@ -1,12 +1,14 @@
 S sat
 S smt
 S solver
-S util
 S backend
+S util
+S util/smtlib
 
 B _build/
 B _build/sat
 B _build/smt
 B _build/solver
 B _build/util
+B _build/smtlib
 B _build/backend

backend/dedukti.ml

@@ -16,7 +16,7 @@ module type Arg = sig
   val context : Format.formatter -> proof -> unit
 end
 
-module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type proof := S.proof) = struct
+module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type lemma := S.lemma and type proof := S.proof) = struct
 
   let pp_nl fmt = Format.fprintf fmt "@\n"
   let fprintf fmt format = Format.kfprintf pp_nl fmt format

backend/dedukti.mli

@@ -14,6 +14,9 @@ end
 
 module Make :
   functor(S : Res.S) ->
-  functor(A : Arg with type formula := S.St.formula and type proof := S.proof) ->
+  functor(A : Arg
+          with type formula := S.St.formula
+           and type lemma := S.lemma
+           and type proof := S.proof) ->
     S with type t := S.proof
 (** Functor to generate a backend to output proofs for the dedukti type checker. *)

main.ml

@@ -22,6 +22,7 @@ type sat_input =
 
 type sat_output =
   | Standard (* Only output problem status *)
+  | Dedukti
   | Dot
 
 type solver =
@@ -39,6 +40,7 @@ let input_list = [
 ]
 let output_list = [
   "dot", Dot;
+  "dk", Dedukti;
 ]
 let solver_list = [
   "smt", Smt;
@@ -96,14 +98,19 @@ let print format = match !output with
   | Dot ->
     Format.fprintf std "/* ";
     Format.kfprintf (fun fmt -> Format.fprintf fmt " */@.") std format
+  | Dedukti ->
+    Format.fprintf std "(; ";
+    Format.kfprintf (fun fmt -> Format.fprintf fmt " ;)@.") std format
 
 let print_proof proof = match !output with
   | Standard -> ()
-  | Dot -> Smt.print_proof std proof
+  | Dot -> Smt.print_dot std proof
+  | Dedulti -> Smt.print_dedukti std proof
 
 let print_mcproof proof = match !output with
   | Standard -> ()
-  | Dot -> Mcsat.print_proof std proof
+  | Dot -> Mcsat.print_dot std proof
+  | Dedulti -> Mcsat.print_dedukti std proof
 
 let rec print_cl fmt = function
   | [] -> Format.fprintf fmt "[]"
@@ -121,15 +128,15 @@ let print_mclause l =
 
 let print_cnf cnf = match !output with
   | Standard -> print_lcl cnf
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 let print_unsat_core u = match !output with
   | Standard -> print_lclause u
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 let print_mc_unsat_core u = match !output with
   | Standard -> print_mclause u
-  | Dot -> ()
+  | Dot | Dedukti -> ()
 
 (* Arguments parsing *)
 let file = ref ""

smt/smt.ml

@@ -67,8 +67,14 @@ module Make(Dummy:sig end) = struct
       let print_atom = St.print_atom
       let lemma_info () = "Proof", Some "PURPLE", []
     end)
+  module Dedukti = Dedukti.Make(Proof)(struct
+      let print _ _ = ()
+      let prove _ _ = ()
+      let context _ _ = ()
+    end)
 
   let print_clause = St.print_clause
-  let print_proof = Dot.print
+  let print_dot = Dot.print
+  let print_dedulti = Dedukti.print
 
 end

smt/smt.mli

@@ -12,7 +12,10 @@ module Make(Dummy: sig end) : sig
   val print_clause : Format.formatter -> St.clause -> unit
   (** Print the clause on the given formatter. *)
 
-  val print_proof : Format.formatter -> Proof.proof -> unit
+  val print_dot : Format.formatter -> Proof.proof -> unit
+  (** Print the given proof in dot format. *)
+
+  val print_dedukti : Format.formatter -> Proof.proof -> unit
   (** Print the given proof in dot format. *)
 
 end