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

Removed some unused code in coq backend

Browse source
This commit is contained in:
Guillaume Bury 2017-08-22 14:55:21 +02:00
parent 887de5d0af
commit 8eee822ad6
2 changed files with 4 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/backend/coq.ml
View file

@ -7,22 +7,17 @@ module type S = Backend_intf.S
module type Arg = sig module type Arg = sig
type atom
type hyp type hyp
type lemma type lemma
type assumption type assumption
val print_atom : Format.formatter -> atom -> unit
val prove_hyp : Format.formatter -> string -> hyp -> unit val prove_hyp : Format.formatter -> string -> hyp -> unit
val prove_lemma : Format.formatter -> string -> lemma -> unit val prove_lemma : Format.formatter -> string -> lemma -> unit
val prove_assumption : Format.formatter -> string -> assumption -> unit val prove_assumption : Format.formatter -> string -> assumption -> unit
end end
module Make(S : Res.S)(A : Arg with type atom := S.atom module Make(S : Res.S)(A : Arg with type hyp := S.clause
and type hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause) = struct and type assumption := S.clause) = struct
@ -33,22 +28,6 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom
let name c = c.S.St.name let name c = c.S.St.name
let pp_atom fmt a =
if a == S.St.(a.var.pa) then
Format.fprintf fmt "~ %a" A.print_atom a
else
Format.fprintf fmt "~ ~ %a" A.print_atom a.S.St.neg
let pp_clause fmt c =
let rec aux fmt (a, i) =
if i < Array.length a then
Format.fprintf fmt "%a ->@ %a"
pp_atom a.(i) aux (a, i + 1)
else
Format.fprintf fmt "False"
in
Format.fprintf fmt "@[<hov 1>(%a)@]" aux (c.S.St.atoms, 0)
let clause_map c = let clause_map c =
let rec aux acc a i = let rec aux acc a i =
if i >= Array.length a then acc if i >= Array.length a then acc
@ -141,8 +120,7 @@ end
module Simple(S : Res.S) module Simple(S : Res.S)
(A : Arg with type atom := S.St.formula (A : Arg with type hyp = S.St.formula list
and type hyp = S.St.formula list
and type lemma := S.lemma and type lemma := S.lemma
and type assumption := S.St.formula) = and type assumption := S.St.formula) =
Make(S)(struct Make(S)(struct
@ -160,10 +138,6 @@ module Simple(S : Res.S)
| S.St.Lemma p -> p | S.St.Lemma p -> p
| _ -> assert false | _ -> assert false
(* Actual functions *)
let print_atom fmt a =
A.print_atom fmt a.S.St.lit
let prove_hyp fmt name c = let prove_hyp fmt name c =
A.prove_hyp fmt name (List.map lit (S.to_list c)) A.prove_hyp fmt name (List.map lit (S.to_list c))

12
src/backend/coq.mli
View file

@ -15,17 +15,11 @@ module type S = Backend_intf.S
module type Arg = sig module type Arg = sig
(** Term printing for Coq *) (** Term printing for Coq *)
type atom
(** The type of atomic formulas *)
type hyp type hyp
type lemma type lemma
type assumption type assumption
(** The types of hypotheses, lemmas, and assumptions *) (** The types of hypotheses, lemmas, and assumptions *)
val print_atom : Format.formatter -> atom -> unit
(** Print the given atomic formula *)
val prove_hyp : Format.formatter -> string -> hyp -> unit val prove_hyp : Format.formatter -> string -> hyp -> unit
val prove_lemma : Format.formatter -> string -> lemma -> unit val prove_lemma : Format.formatter -> string -> lemma -> unit
val prove_assumption : Format.formatter -> string -> assumption -> unit val prove_assumption : Format.formatter -> string -> assumption -> unit
@ -39,15 +33,13 @@ module type Arg = sig
end end
module Make(S : Res.S)(A : Arg with type atom := S.atom module Make(S : Res.S)(A : Arg with type hyp := S.clause
and type hyp := S.clause
and type lemma := S.clause and type lemma := S.clause
and type assumption := S.clause) : S with type t := S.proof and type assumption := S.clause) : S with type t := S.proof
(** Base functor to output Coq proofs *) (** Base functor to output Coq proofs *)
module Simple(S : Res.S)(A : Arg with type atom := S.St.formula module Simple(S : Res.S)(A : Arg with type hyp = S.St.formula list
and type hyp = S.St.formula list
and type lemma := S.lemma and type lemma := S.lemma
and type assumption := S.St.formula) : S with type t := S.proof and type assumption := S.St.formula) : S with type t := S.proof
(** Simple functo to output Coq proofs *) (** Simple functo to output Coq proofs *)