1(*  Title:      Tools/Argo/argo_lit.ML
2    Author:     Sascha Boehme
3
4Representation of literals. Literals are terms with a polarity, either positive or negative.
5A literal for term t with positive polarity is equivalent to t.
6A literal for term t with negative polarity is equivalent to the propositional negation of t.
7*)
8
9signature ARGO_LIT =
10sig
11  datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
12  val literal: Argo_Term.term -> bool -> literal
13  val dest: literal -> Argo_Term.term * bool
14  val term_of: literal -> Argo_Term.term
15  val signed_id_of: literal -> int
16  val signed_expr_of: literal -> Argo_Expr.expr
17  val negate: literal -> literal
18  val eq_id: literal * literal -> bool
19  val eq_lit: literal * literal -> bool
20  val dual_lit: literal * literal -> bool
21end
22
23structure Argo_Lit: ARGO_LIT =
24struct
25
26(* data type *)
27
28datatype literal = Pos of Argo_Term.term | Neg of Argo_Term.term
29
30
31(* operations *)
32
33fun literal t true = Pos t
34  | literal t false = Neg t
35
36fun dest (Pos t) = (t, true)
37  | dest (Neg t) = (t, false)
38
39fun term_of (Pos t) = t
40  | term_of (Neg t) = t
41
42fun signed_id_of (Pos t) = Argo_Term.id_of t
43  | signed_id_of (Neg t) = ~(Argo_Term.id_of t)
44
45fun signed_expr_of (Pos t) = Argo_Term.expr_of t
46  | signed_expr_of (Neg t) = Argo_Expr.mk_not (Argo_Term.expr_of t)
47
48fun id_of (Pos t) = Argo_Term.id_of t
49  | id_of (Neg t) = Argo_Term.id_of t
50
51fun negate (Pos t) = Neg t
52  | negate (Neg t) = Pos t
53
54fun eq_id (lit1, lit2) = (id_of lit1 = id_of lit2)
55
56fun eq_lit (Pos t1, Pos t2) = Argo_Term.eq_term (t1, t2)
57  | eq_lit (Neg t1, Neg t2) = Argo_Term.eq_term (t1, t2)
58  | eq_lit _ = false
59
60fun dual_lit (Pos t1, Neg t2) = Argo_Term.eq_term (t1, t2)
61  | dual_lit (Neg t1, Pos t2) = Argo_Term.eq_term (t1, t2)
62  | dual_lit _ = false
63
64end
65