Module LogtkPrologTerm

module LogtkPrologTerm: sig .. end

Prolog-like Terms

.

Those terms are not hashconsed, nor do they use De Bruijn indices. Their simplicity make them good for heavy AST transformations, output of parsing, etc.

Terms are only compared, hashsed, etc. by their "term" component (the algebraic variant). Additional fields (location...) are ignored for almost every operation.


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