Module LogtkScopedTerm

module LogtkScopedTerm: sig .. end

Scoped Terms

Those terms are not designed to be used directly, but rather to provide a generic backend (implementing De Bruijn indices, subterms, substitutions, etc.) for other more specific representations like LogtkType, LogtkFOTerm, FOLogtkFormula...


type symbol = LogtkSymbol.t 
type t 
Abstract type of term
type term = t 
type view = private 
| Var of int (*
Free variable (integer: mostly useless)
*)
| RigidVar of int (*
Variable that only unifies with other rigid variables
*)
| BVar of int (*
Bound variable (De Bruijn index)
*)
| Bind of symbol * t * t (*
LogtkType, sub-term
*)
| Const of symbol (*
Constant
*)
| Record of (string * t) list * t option (*
Extensible record
*)
| RecordGet of t * string (*
get r name is r.name
*)
| RecordSet of t * string * t (*
set r name t is r.name <- t
*)
| Multiset of t list (*
Multiset of terms
*)
| App of t * t list (*
Uncurried application
*)
| At of t * t (*
Curried application
*)
| SimpleApp of symbol * t list (*
For representing special constructors
*)
val view : t -> view
View on the term's head form
module Kind: sig .. end
val kind : t -> Kind.t
type type_result = 
| NoLogtkType
| HasLogtkType of t
val ty : t -> type_result
LogtkType of the term, if any
val ty_exn : t -> t
Same as LogtkScopedTerm.ty, but fails if the term has no type
Raises Invalid_argument if the type is NoLogtkType
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD

Constructors

Some constructors, such as LogtkScopedTerm.record, may raise LogtkScopedTerm.IllFormedTermif the arguments are ill-formed (several occurrences of a key), or, for variables, if the number is negative

exception IllFormedTerm of string
type nat = int 
val const : kind:Kind.t ->
ty:t -> symbol -> t
val app : kind:Kind.t ->
ty:t ->
t -> t list -> t
val bind : kind:Kind.t ->
ty:t ->
varty:t ->
symbol -> t -> t
val var : kind:Kind.t ->
ty:t -> nat -> t
val rigid_var : kind:Kind.t ->
ty:t -> nat -> t
val bvar : kind:Kind.t ->
ty:t -> nat -> t
val record : kind:Kind.t ->
ty:t ->
(string * t) list ->
rest:t option -> t
val record_get : kind:Kind.t ->
ty:t -> t -> string -> t
val record_set : kind:Kind.t ->
ty:t ->
t -> string -> t -> t
val multiset : kind:Kind.t ->
ty:t -> t list -> t
val at : kind:Kind.t ->
ty:t ->
t -> t -> t
val simple_app : kind:Kind.t ->
ty:t ->
symbol -> t list -> t
val mk_at : kind:Kind.t ->
ty:t ->
t -> t -> t
alias to LogtkScopedTerm.at
val tType : t
The root of the type system. It doesn't have a type. It has kind Kind.LogtkType
val cast : ty:t -> t -> t
Change the type
val change_kind : kind:Kind.t -> t -> t
Change the kind
val is_var : t -> bool
val is_bvar : t -> bool
val is_rigid_var : t -> bool
val is_const : t -> bool
val is_bind : t -> bool
val is_app : t -> bool
val is_record : t -> bool
val is_record_get : t -> bool
val is_record_set : t -> bool
val is_multiset : t -> bool
val is_at : t -> bool
val hashcons_stats : unit -> int * int * int * int * int * int

Flags

be VERY careful with flags. Due to hashconsing, they will be shared between every instance of a term, so only use them for properties that are universal. Only Sys.word_size - 1 flags can exist in a program.
type flag 
val new_flag : unit -> flag
val set_flag : t -> flag -> unit
val get_flag : t -> flag -> bool

Containers


module Map: Sequence.Map.S  with type key = term
module Set: Sequence.Set.S  with type elt = term
module Tbl: sig .. end

De Bruijn indices handling


module DB: sig .. end

High level constructors


val bind_vars : kind:Kind.t ->
ty:t ->
symbol ->
t list -> t -> t
bind several free variables in the term, transforming it to use De Bruijn indices.
ty : return type of the term

Iterators


module Seq: sig .. end

LogtkPositions


module Pos: sig .. end
val replace : t ->
old:t -> by:t -> t
replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

Variables


val close_vars : kind:Kind.t ->
ty:t ->
symbol -> t -> t
Close all free variables of the term using the binding symbol
val ground : t -> bool
true if the term contains no free variables

Misc


val size : t -> int
val depth : t -> int
val head : t -> symbol option
Head symbol, or None if the term is a (bound) variable
val all_positions : ?vars:bool ->
?pos:LogtkPosition.t ->
t ->
'a -> ('a -> t -> LogtkPosition.t -> 'a) -> 'a
Fold on all subterms of the given term, with their position.
Returns the accumulator
vars : if true, also fold on variables Default: false.
pos : the initial position (prefix). Default: empty.

IO


include LogtkInterfaces.PRINT
include LogtkInterfaces.PRINT_DE_BRUIJN
val add_default_hook : print_hook -> unit
Add a print hook that will be used from now on

Misc


val fresh_var : kind:Kind.t ->
ty:t -> unit -> t
fresh_var ~kind ~ty () returns a fresh, unique, NOT HASHCONSED variable that will therefore never be equal to any other variable.
val _var : kind:Kind.t ->
ty:t -> int -> t
Unsafe version of LogtkScopedTerm.var that accepts negative index