(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2015 Guillaume Bury
*)

module type S = Backend_intf.S

module type Arg = sig

  type atom

  type hyp
  type lemma
  type assumption

  val print_atom : Format.formatter -> atom -> unit

  val prove_hyp : Format.formatter -> string -> hyp -> unit
  val prove_lemma : Format.formatter -> string -> lemma -> unit
  val prove_assumption : Format.formatter -> string -> assumption -> unit

end

module Make(S : Res.S)(A : Arg with type atom := S.atom
                                and type hyp := S.clause
                                and type lemma := S.clause
                                and type assumption := S.clause) = struct

  module M = Map.Make(struct
      type t = S.St.atom
      let compare a b = compare a.S.St.aid b.S.St.aid
    end)

  let name c = c.S.St.name
  let name_tmp c = c.S.St.name ^ "_tmp"

  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 "@[<h>%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 pp_clause_intro fmt c =
    let rec aux fmt acc a i =
      if i >= Array.length a then acc
      else begin
        let name = Format.sprintf "A%d" i in
        Format.fprintf fmt "%s@ " name;
        aux fmt (M.add a.(i) name acc) a (i + 1)
      end
    in
    Format.fprintf fmt "intros @[<hov>";
    let m = aux fmt M.empty c.S.St.atoms 0 in
    Format.fprintf fmt "@].@\n";
    m

  let clausify fmt clause =
    Format.fprintf fmt "assert (%s: %a).@\ntauto. clear %s.@\n"
      (name clause) pp_clause clause (name_tmp clause)

  let elim_duplicate fmt goal hyp _ =
    (** Printing info comment in coq *)
    Format.fprintf fmt "(* Eliminating doublons.@\n";
    Format.fprintf fmt "   Goal : %s ; Hyp : %s *)@\n" (name goal) (name hyp);
    (** Use 'assert' to introduce the clause we want to prove *)
    Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
    (** Prove the goal: intro the atoms, then use them with the hyp *)
    let m = pp_clause_intro fmt goal in
    Format.fprintf fmt "exact (%s%a).@\n"
      (name hyp) (fun fmt -> Array.iter (fun atom ->
          Format.fprintf fmt " %s" (M.find atom m))) hyp.S.St.atoms

  let resolution fmt goal hyp1 hyp2 atom =
    let a = S.St.(atom.var.pa) in
    let h1, h2 =
      if Array.memq a hyp1.S.St.atoms then hyp1, hyp2
      else (assert (Array.memq a hyp2.S.St.atoms); hyp2, hyp1)
    in
    (** Print some debug info *)
    Format.fprintf fmt "(* Clausal resolution.@\n";
    Format.fprintf fmt "   Goal : %s ; Hyps : %s, %s *)@\n"
      (name goal) (name h1) (name h2);
    (** use a cut to introduce the clause we want to prove
        *except* if it is the last clause, i.e the empty clause because
                 we already want to prove 'False',
                 no need to introduce it as a subgoal *)
    if Array.length goal.S.St.atoms <> 0 then
        Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
    (** Prove the goal: intro the axioms, then perform resolution *)
    let m = pp_clause_intro fmt goal in
    Format.fprintf fmt "exact (%s%a).@\n"
      (name h1) (fun fmt -> Array.iter (fun b ->
          if b == a then begin
            Format.fprintf fmt " (fun p => %s%a)"
              (name h2) (fun fmt -> (Array.iter (fun c ->
                  if c == a.S.St.neg then
                    Format.fprintf fmt " (fun np => np p)"
                  else
                    Format.fprintf fmt " %s" (M.find c m)))
                ) h2.S.St.atoms
          end else
            Format.fprintf fmt " %s" (M.find b m))
        ) h1.S.St.atoms


  let prove_node t fmt node =
    let clause = node.S.conclusion in
    match node.S.step with
    | S.Hypothesis ->
      A.prove_hyp fmt (name_tmp clause) clause;
      clausify fmt clause
    | S.Assumption ->
      A.prove_assumption fmt (name_tmp clause) clause;
      clausify fmt clause
    | S.Lemma _ ->
      A.prove_lemma fmt (name_tmp clause) clause;
      clausify fmt clause
    | S.Duplicate (p, l) ->
      let c = (S.expand p).S.conclusion in
      elim_duplicate fmt clause c l
    | S.Resolution (p1, p2, a) ->
      let c1 = (S.expand p1).S.conclusion in
      let c2 = (S.expand p2).S.conclusion in
      resolution fmt clause c1 c2 a

  (* Here the main idea is to always try and have exactly
     one goal to prove, i.e False. So each  *)
  let print fmt p =
    let h = S.H.create 4013 in
    let aux () node =
      Format.fprintf fmt "%a@\n@\n" (prove_node h) node
    in
    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n@\n";
    S.fold aux () p

end


module Simple(S : Res.S)
    (A : Arg with type atom := S.St.formula
              and type hyp = S.St.formula list
              and type lemma := S.lemma
              and type assumption := S.St.formula) =
  Make(S)(struct

    (* Some helpers *)
    let lit a = a.S.St.lit

    let get_assumption c =
      match S.to_list c with
      | [ x ] -> x
      | _ -> assert false

    let get_lemma c =
      match c.S.St.cpremise with
      | S.St.Lemma p -> p
      | _ -> assert false

    (* Actual functions *)
    let print_atom fmt a =
      A.print_atom fmt a.S.St.lit

    let prove_hyp fmt name c =
      A.prove_hyp fmt name (List.map lit (S.to_list c))

    let prove_lemma fmt name c =
      A.prove_lemma fmt name (get_lemma c)

    let prove_assumption fmt name c =
      A.prove_assumption fmt name (lit (get_assumption c))

  end)