Module LogtkTypedPrologTerm

module LogtkTypedPrologTerm: sig .. end

Prolog-like LogtkTyped Terms

.

These terms are scoped, and possibly typed. LogtkType inference should be performed on them.


type location = LogtkParseLocation.t 
type t 
type term = t 
type view = private 
| Var of string (*
variable
*)
| BVar of string (*
bound variable
*)
| Const of LogtkSymbol.t (*
constant
*)
| App of t * t list (*
apply term
*)
| Bind of LogtkSymbol.t * t * t (*
bind variable in term
*)
| Multiset of t list
| Record of (string * t) list * t option (*
extensible record
*)
val view : t -> view
val loc : t -> location option
val ty : t -> t option
include LogtkInterfaces.HASH
include LogtkInterfaces.ORD

Constructors


exception IllFormedTerm of string
val tType : t
val wildcard : t
val var : ?loc:location ->
?ty:t -> string -> t
val bvar : ?loc:location ->
?ty:t -> string -> t
val app : ?loc:location ->
?ty:t ->
t ->
t list -> t
val const : ?loc:location ->
?ty:t -> LogtkSymbol.t -> t
val bind : ?loc:location ->
?ty:t ->
LogtkSymbol.t ->
t -> t -> t
val bind_list : ?loc:location ->
?ty:t ->
LogtkSymbol.t ->
t list ->
t -> t
val multiset : ?loc:location ->
?ty:t ->
t list -> t
val record : ?loc:location ->
?ty:t ->
(string * t) list ->
rest:t option -> t
Build a record with possibly a row variable.
Raises IllFormedTerm if the rest is not either a record or a variable.
val of_string : ?loc:location ->
?ty:t -> string -> t
val of_int : ?ty:t -> int -> t
val at_loc : ?loc:location ->
t -> t
val with_ty : ?ty:t ->
t -> t
val fresh_var : ?loc:location ->
?ty:t -> unit -> t
fresh free variable with the given type.
val fresh_bvar : ?loc:location ->
?ty:t -> unit -> t

LogtkUtils


val is_var : t -> bool
val is_bvar : t -> bool
val ground : t -> bool
true iff there is no free variable
val closed : t -> bool
closed t is true iff all bound variables of t occur under a binder (i.e. they are actually bound in t)
val vars : t -> t list
val close_all : ?ty:t ->
LogtkSymbol.t -> t -> t
Bind all free vars with the symbol
include LogtkInterfaces.PRINT
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

Visitor


module Visitor: sig .. end

Substitutions, LogtkUnification


type 'a or_error = [ `Error of string | `Ok of 'a ] 
module Subst: sig .. end
val rename : term -> term
Rename all free variables
exception LogtkUnifyFailure of term * term
* Subst.t
val unify : ?subst:Subst.t ->
term ->
term ->
Subst.t or_error
LogtkUnify two terms, might fail
val unify_exn : ?subst:Subst.t ->
term ->
term -> Subst.t
Same as LogtkTypedPrologTerm.unify, but can raise.
Raises LogtkUnifyFailure if the unification fails