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