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)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
