src/Tools/Metis/src/Literal.sig

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS                                                *)
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

signature Literal =
sig

(* ------------------------------------------------------------------------- *)
(* A type for storing first order logic literals.                            *)
(* ------------------------------------------------------------------------- *)

type polarity = bool

type literal = polarity * Atom.atom

(* ------------------------------------------------------------------------- *)
(* Constructors and destructors.                                             *)
(* ------------------------------------------------------------------------- *)

val polarity : literal -> polarity

val atom : literal -> Atom.atom

val name : literal -> Atom.relationName

val arguments : literal -> Term.term list

val arity : literal -> int

val positive : literal -> bool

val negative : literal -> bool

val negate : literal -> literal

val relation : literal -> Atom.relation

val functions : literal -> NameAritySet.set

val functionNames : literal -> NameSet.set

(* Binary relations *)

val mkBinop : Atom.relationName -> polarity * Term.term * Term.term -> literal

val destBinop : Atom.relationName -> literal -> polarity * Term.term * Term.term

val isBinop : Atom.relationName -> literal -> bool

(* Formulas *)

val toFormula : literal -> Formula.formula

val fromFormula : Formula.formula -> literal

(* ------------------------------------------------------------------------- *)
(* The size of a literal in symbols.                                         *)
(* ------------------------------------------------------------------------- *)

val symbols : literal -> int

(* ------------------------------------------------------------------------- *)
(* A total comparison function for literals.                                 *)
(* ------------------------------------------------------------------------- *)

val compare : literal * literal -> order  (* negative < positive *)

val equal : literal -> literal -> bool

(* ------------------------------------------------------------------------- *)
(* Subterms.                                                                 *)
(* ------------------------------------------------------------------------- *)

val subterm : literal -> Term.path -> Term.term

val subterms : literal -> (Term.path * Term.term) list

val replace : literal -> Term.path * Term.term -> literal

(* ------------------------------------------------------------------------- *)
(* Free variables.                                                           *)
(* ------------------------------------------------------------------------- *)

val freeIn : Term.var -> literal -> bool

val freeVars : literal -> NameSet.set

(* ------------------------------------------------------------------------- *)
(* Substitutions.                                                            *)
(* ------------------------------------------------------------------------- *)

val subst : Subst.subst -> literal -> literal

(* ------------------------------------------------------------------------- *)
(* Matching.                                                                 *)
(* ------------------------------------------------------------------------- *)

val match :  (* raises Error *)
    Subst.subst -> literal -> literal -> Subst.subst

(* ------------------------------------------------------------------------- *)
(* Unification.                                                              *)
(* ------------------------------------------------------------------------- *)

val unify :  (* raises Error *)
    Subst.subst -> literal -> literal -> Subst.subst

(* ------------------------------------------------------------------------- *)
(* The equality relation.                                                    *)
(* ------------------------------------------------------------------------- *)

val mkEq : Term.term * Term.term -> literal

val destEq : literal -> Term.term * Term.term

val isEq : literal -> bool

val mkNeq : Term.term * Term.term -> literal

val destNeq : literal -> Term.term * Term.term

val isNeq : literal -> bool

val mkRefl : Term.term -> literal

val destRefl : literal -> Term.term

val isRefl : literal -> bool

val mkIrrefl : Term.term -> literal

val destIrrefl : literal -> Term.term

val isIrrefl : literal -> bool

(* The following work with both equalities and disequalities *)

val sym : literal -> literal  (* raises Error if given a refl or irrefl *)

val lhs : literal -> Term.term

val rhs : literal -> Term.term

(* ------------------------------------------------------------------------- *)
(* Special support for terms with type annotations.                          *)
(* ------------------------------------------------------------------------- *)

val typedSymbols : literal -> int

val nonVarTypedSubterms : literal -> (Term.path * Term.term) list

(* ------------------------------------------------------------------------- *)
(* Parsing and pretty-printing.                                              *)
(* ------------------------------------------------------------------------- *)

val pp : literal Print.pp

val toString : literal -> string

val fromString : string -> literal

val parse : Term.term Parse.quotation -> literal

end