Module Logtk.STermSource

Simple Terms

.

Simple terms, that are not hashconsed, nor typed.

Those do not use De Bruijn indices for variable binding, but simply names (scoping is done later). 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.

Sourcetype location = ParseLocation.t
Sourcetype var =
  1. | V of string
  2. | Wildcard
Sourcetype t = private {
  1. term : view;
  2. loc : location option;
}
Sourceand match_branch =
  1. | Match_case of string * var list * t
  2. | Match_default of t
Sourceand view =
  1. | Var of var
    (*

    variable

    *)
  2. | Const of string
    (*

    constant

    *)
  3. | AppBuiltin of Builtin.t * t list
  4. | App of t * t list
    (*

    apply term

    *)
  5. | Ite of t * t * t
  6. | Match of t * match_branch list
  7. | Let of (var * t) list * t
  8. | Bind of Binder.t * typed_var list * t
    (*

    bind n variables

    *)
  9. | List of t list
    (*

    special constructor for lists

    *)
  10. | Record of (string * t) list * var option
    (*

    extensible record

    *)
Sourceand typed_var = var * t option
Sourcetype term = t
Sourceval view : t -> view
Sourceval loc : t -> location option
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int
Sourceval var : ?loc:location -> string -> t
Sourceval v_wild : t

wildcard

Sourceval mk_var : ?loc:location -> var -> t
Sourceval app : ?loc:location -> t -> t list -> t
Sourceval app_const : ?loc:location -> string -> t list -> t
Sourceval builtin : ?loc:location -> Builtin.t -> t
Sourceval app_builtin : ?loc:location -> Builtin.t -> t list -> t
Sourceval const : ?loc:location -> string -> t
Sourceval bind : ?loc:location -> Binder.t -> typed_var list -> t -> t
Sourceval ite : ?loc:location -> t -> t -> t -> t
Sourceval match_ : ?loc:location -> t -> match_branch list -> t
Sourceval let_ : ?loc:location -> (var * t) list -> t -> t
Sourceval list_ : ?loc:location -> t list -> t
Sourceval nil : t
Sourceval record : ?loc:location -> (string * t) list -> rest:var option -> t
Sourceval at_loc : loc:location -> t -> t
Sourceval wildcard : t
Sourceval is_app : t -> bool
Sourceval is_var : t -> bool
Sourceval true_ : t
Sourceval false_ : t
Sourceval and_ : ?loc:location -> t list -> t
Sourceval or_ : ?loc:location -> t list -> t
Sourceval not_ : ?loc:location -> t -> t
Sourceval equiv : ?loc:location -> t -> t -> t
Sourceval xor : ?loc:location -> t -> t -> t
Sourceval imply : ?loc:location -> t -> t -> t
Sourceval eq : ?loc:location -> t -> t -> t
Sourceval neq : ?loc:location -> t -> t -> t
Sourceval forall : ?loc:location -> typed_var list -> t -> t
Sourceval exists : ?loc:location -> typed_var list -> t -> t
Sourceval lambda : ?loc:location -> typed_var list -> t -> t
Sourceval int_ : Z.t -> t
Sourceval of_int : int -> t
Sourceval rat : Q.t -> t
Sourceval real : string -> t
Sourceval tType : t
Sourceval term : t
Sourceval prop : t
Sourceval ty_int : t
Sourceval ty_rat : t
Sourceval ty_real : t
Sourceval fun_ty : ?loc:location -> t list -> t -> t
Sourceval forall_ty : ?loc:location -> typed_var list -> t -> t
Sourceval ty_unfold : t -> t list * t
Sourceval unfold_bind : Binder.t -> t -> typed_var list * t
Sourcemodule Set : CCSet.S with type elt = term
Sourcemodule Map : CCMap.S with type key = term
Sourcemodule Tbl : CCHashtbl.S with type key = term
Sourcemodule StringSet : CCSet.S with type elt = string
Sourcemodule Seq : sig ... end
Sourceval ground : t -> bool
Sourceval close_all : Binder.t -> t -> t

Bind all free vars with the symbol

Sourceval subterm : strict:bool -> t -> sub:t -> bool

is sub a (strict?) subterm of the other arg?

Print

include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string

Formats

Sourcemodule TPTP : sig ... end
Sourcemodule ZF : sig ... end

Subst

Sourcemodule StrMap : CCMap.S with type key = string
Sourcetype subst = t StrMap.t
Sourceval empty_subst : subst
Sourceval merge_subst : subst -> subst -> subst

merge a b merges a into b, but favors b in case of conflict

Sourceval apply_subst : subst -> term -> term