Using CPS

formula.ml

type formula =
  | False
  | True
  | Atom of string
  | Not of formula
  | And of formula * formula
  | Or of formula * formula

let is_lit = function
  | Atom _ | Not (Atom _) -> true
  | _ -> false

module type S = sig
  val conjuncts : formula -> formula list
  val conjoin : formula list -> formula
  val disjuncts : formula -> formula list
  val disjoin : formula list -> formula
  val rewrite : (formula -> formula) -> formula -> formula
  val simplify : formula -> formula
  val nnf : formula -> formula
  val rawdnf : formula -> formula
  val setdnf : formula -> formula list list
end

module Spec : S = struct

  let rec conjuncts = function
    | And (p,q) -> conjuncts p @ conjuncts q
    | p -> [p]

  let rec conjoin = function
    | [] -> True
    | [p] -> p
    | p::ps -> And (p,conjoin ps)

  let rec disjuncts = function
    | Or (p,q) -> disjuncts p @ disjuncts q
    | p -> [p]

  let rec disjoin = function
    | [] -> False
    | [p] -> p
    | p::ps -> Or (p,disjoin ps)

  let rec rewrite r = function
    | Atom _ as atom -> r atom
    | False -> r False
    | True -> r True
    | Not p -> r (Not (rewrite r p))
    | And (p,q) -> r (And (rewrite r p, rewrite r q))
    | Or (p,q) -> r (Or (rewrite r p, rewrite r q))

  let simplify fm =
    let r = function
      | Not False -> True
      | Not True -> False
      | Not (Not p) -> p
      | And (_,False) | And (False,_) -> False
      | And (p,True) | And (True,p) -> p
      | Or (p,False) | Or (False,p) -> p
      | Or (_,True) | Or (True,_) -> True
      | _ as p -> p
    in
    rewrite r fm

  let nnf fm =
    let rec nnf' = function
      | And (p,q) -> And (nnf' p, nnf' q)
      | Or (p,q) -> Or (nnf' p, nnf' q)
      | Not (Not p) -> nnf' p
      | Not (And (p,q)) -> Or (nnf' (Not p), nnf' (Not q))
      | Not (Or (p,q)) -> And (nnf' (Not p), nnf' (Not q))
      | _ as p -> p
    in
    nnf' (simplify fm)

  let rec distrib = function
    | And(p,(Or(q,r))) -> Or(distrib(And(p,q)),distrib(And(p,r)))
    | And(Or(p,q),r) -> Or(distrib(And(p,r)),distrib(And(q,r)))
    | _ as p -> p

  let rec rawdnf = function
    | And(p,q) -> distrib(And(rawdnf p,rawdnf q))
    | Or(p,q) -> Or(rawdnf p,rawdnf q)
    | _ as p -> p

  let setdnf fm =
    nnf fm |> rawdnf |> disjuncts |> List.map conjuncts

end

module Impl : S = struct

  let conjuncts fm =
    let rec loop ans = function
      | And (p,q)::ps -> loop ans (p::q::ps)
      | p::ps -> loop (p::ans) ps
      | [] -> ans
    in
    loop [] [fm]

  let conjoin = function
    | [] -> True
    | p::ps -> List.fold_left (fun p q -> And (p,q)) p ps

  let disjuncts fm =
    let rec loop ans = function
      | Or (p,q)::ps -> loop ans (p::q::ps)
      | p::ps -> loop (p::ans) ps
      | [] -> ans
    in
    loop [] [fm]

  let disjoin = function
    | [] -> False
    | p::ps -> List.fold_left (fun p q -> Or (p,q)) p ps

  let rec rewritek r fm k =
    match fm with
    | Atom _ as atom -> k (r atom)
    | False -> k (r False)
    | True -> k (r True)
    | Not p ->
      let k' = fun p' -> k (r (Not p')) in
      rewritek r p k'
    | And (p,q) ->
      let k'' = fun p' q'-> k (r (And (p',q'))) in
      let k' = fun p' -> rewritek r q (k'' p') in
      rewritek r p k'
    | Or (p,q) ->
      let k'' = fun p' q'-> k (r (Or (p',q'))) in
      let k' = fun p' -> rewritek r q (k'' p') in
      rewritek r p k'

  let rewrite r fm = rewritek r fm (fun x -> x)

  let simplify =
    let simpl = function
      | Not False -> True
      | Not True -> False
      | Not (Not p) -> p
      | And (_,False) | And (False,_) -> False
      | And (p,True) | And (True,p) -> p
      | Or (p,False) | Or (False,p) -> p
      | Or (_,True) | Or (True,_) -> True
      | _ as p -> p
    in
    rewrite simpl

  let rec nnfk k = function
    | Not (Not p) ->
      nnfk k p
    | And (p,q) ->
      let k'' p' q' = k (And (p',q')) in
      let k' p' = nnfk (k'' p') q in
      nnfk k' p
    | Or (p,q) ->
      let k'' p' q' = k (Or (p',q')) in
      let k' p' = nnfk (k'' p') q in
      nnfk k' p
    | Not (And (p,q)) ->
      let k'' p' q' = k (Or (p',q')) in
      let k' p' = nnfk (k'' p') (Not q) in
      nnfk k' (Not p)
    | Not (Or (p,q)) ->
      let k'' p' q' = k (And (p',q')) in
      let k' p' = nnfk (k'' p') (Not q) in
      nnfk k' (Not p)
    | _ as p -> k p

  let nnf = nnfk (fun x -> x)

  let rec distribk k = function
    | And(p,(Or(q,r))) ->
      let k'' p' q' = k (Or (p',q')) in
      let k' p' = distribk (k'' p') (And (p,q)) in
      distribk k' (And (p,r))
    | And(Or(p,q),r) ->
      let k'' p' q' = k (Or (p',q')) in
      let k' p' = distribk (k'' p') (And (p,r)) in
      distribk k' (And (q,r))
    | p -> k p

  let rec rawdnfk k = function
    | And (p,q) ->
      let k'' p' q' = k (distribk (fun x -> x) (And (p',q'))) in
      let k' p' = rawdnfk (k'' p') q in
      rawdnfk k' p
    | Or (p,q) ->
      let k'' p' q' = k (Or (p',q')) in
      let k' p' = rawdnfk (k'' p') q in
      rawdnfk k' p
    | p -> k p

  let rawdnf = rawdnfk (fun x -> x)

  let setdnf fm =
    nnf fm |> rawdnf |> disjuncts |> List.map conjuncts

end

let p = Atom "p"
let q = Atom "q"
let r = Atom "r"
let s = Atom "s"
let ex = And (And (p, Not False), Not (Not (Or (False,q))))
let ex1 = Spec.simplify ex
let ex2 = Impl.simplify ex