(*  Title:      Tools/Argo/argo_lit.ML
    Author:     Sascha Boehme

Representation of literals. Literals are terms with a polarity, either positive or negative.
A literal for term t with positive polarity is equivalent to t.
A literal for term t with negative polarity is equivalent to the propositional negation of t.
*)

signature ARGO_LIT =
sig
  datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
  val literal: Argo_Term.term -> bool -> literal
  val dest: literal -> Argo_Term.term * bool
  val term_of: literal -> Argo_Term.term
  val signed_id_of: literal -> int
  val signed_expr_of: literal -> Argo_Expr.expr
  val negate: literal -> literal
  val eq_id: literal * literal -> bool
  val eq_lit: literal * literal -> bool
  val dual_lit: literal * literal -> bool
end

structure Argo_Lit: ARGO_LIT =
struct

(* data type *)

datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term


(* operations *)

fun literal t true = Pos t
  | literal t false = Neg t

fun dest (Pos t) = (t, true)
  | dest (Neg t) = (t, false)

fun term_of (Pos t) = t
  | term_of (Neg t) = t

fun signed_id_of (Pos t) = Argo_Term.id_of t
  | signed_id_of (Neg t) = ~(Argo_Term.id_of t)

fun signed_expr_of (Pos t) = Argo_Term.expr_of t
  | signed_expr_of (Neg t) = Argo_Expr.mk_not (Argo_Term.expr_of t)

fun id_of (Pos t) = Argo_Term.id_of t
  | id_of (Neg t) = Argo_Term.id_of t

fun negate (Pos t) = Neg t
  | negate (Neg t) = Pos t

fun eq_id (lit1, lit2) = (id_of lit1 = id_of lit2)

fun eq_lit (Pos t1, Pos t2) = Argo_Term.eq_term (t1, t2)
  | eq_lit (Neg t1, Neg t2) = Argo_Term.eq_term (t1, t2)
  | eq_lit _ = false

fun dual_lit (Pos t1, Neg t2) = Argo_Term.eq_term (t1, t2)
  | dual_lit (Neg t1, Pos t2) = Argo_Term.eq_term (t1, t2)
  | dual_lit _ = false

end