Module Logtk.PrologTerm (.ml)

module PrologTerm: LogtkPrologTerm

type location = LogtkParseLocation.t 
type t = private {
   term : view;
   loc : location option;
}
type view = private 
| Var of string (*
variable
*)
| Int of Z.t (*
integer
*)
| Rat of Q.t (*
rational
*)
| Const of LogtkSymbol.t (*
constant
*)
| Syntactic of LogtkSymbol.t * t list (*
syntactic construct (operator...)
*)
| App of t * t list (*
apply term
*)
| Bind of LogtkSymbol.t * t list * t (*
bind n variables
*)
| List of t list (*
special constructor for lists
*)
| Record of (string * t) list * t option (*
extensible record
*)
| Column of t * t (*
t:t (useful for typing, e.g.)
*)
type term = t 
val view : t -> view
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD
val var : ?loc:location ->
?ty:t -> string -> t
val int_ : Z.t -> t
val of_int : int -> t
val rat : Q.t -> t
val app : ?loc:location ->
t -> t list -> t
val syntactic : ?loc:location ->
LogtkSymbol.t -> t list -> t
val const : ?loc:location -> LogtkSymbol.t -> t
val bind : ?loc:location ->
LogtkSymbol.t ->
t list -> t -> t
val list_ : ?loc:location -> t list -> t
val nil : t
val column : ?loc:location ->
t -> t -> t
val record : ?loc:location ->
(string * t) list ->
rest:t option -> t
val at_loc : loc:location -> t -> t
val wildcard : t
val is_var : t -> bool
module Set: Sequence.Set.S  with type elt = term
module Map: Sequence.Map.S  with type key = term
module Tbl: Hashtbl.S  with type key = term
module Seq: sig .. end
val ground : t -> bool
val close_all : LogtkSymbol.t -> t -> t
Bind all free vars with the symbol
val subterm : strict:bool -> t -> sub:t -> bool
is sub a (strict?) subterm of the other arg?
include LogtkInterfaces.PRINT

Visitor


class virtual ['a] visitor : object .. end
class id_visitor : object .. end
Visitor that maps the subterms into themselves
module TPTP: sig .. end
TPTP constructors and printing