Module `Logtk.TypedSTerm`

Simple Typed Terms

Similar to STerm, but this time the terms are properly scoped (using Var) and typed.

These terms are suitable for many preprocessing transformations, including CNF.

They can be obtained from STerm.t using TypeInference.

type location = ParseLocation.t

type t

type term = t

type ty = t

type match_cstor = {

cstor_id : ID.t;
cstor_ty : ty;
cstor_args : ty list;

}

a constructor of given type, applied to a list of type argumentss

type match_branch = match_cstor * t Var.t list * t

type view = private

| Var of t Var.t
(*
variable
*)
| Const of ID.t
(*
constant
*)
| App of t * t list
(*
apply term
*)
| Ite of t * t * t
| Match of t * match_branch list
| Let of (t Var.t * t) list * t
| Bind of Binder.t * t Var.t * t
(*
bind variable in term
*)
| AppBuiltin of Builtin.t * t list
| Multiset of t list
| Record of (string * t) list * t option
(*
extensible record
*)
| Meta of meta_var
(*
Unification variable
*)

and meta_var =
  t Var.t * t option ref * [ `Generalize | `BindDefault | `NoBind ]

val view : t -> view

val loc : t -> location option

val ty : t -> t option

val ty_exn : t -> t

val head : t -> ID.t option

val head_exn : t -> ID.t

raises Not_found
if not an application/const

val deref : t -> t

While t is a bound Meta variable, follow its link

include Interfaces.HASH with type t := t

include Interfaces.EQ with type t := t

val equal : t -> t -> bool

val hash : t -> int

include Interfaces.ORD with type t := t

val compare : t -> t -> int

Constructors

exception IllFormedTerm of string

val tType : t

val prop : t

val var : ?loc:location -> t Var.t -> t

val var_of_string : ?loc:location -> ty:t -> string -> t

val app : ?loc:location -> ty:t -> t -> t list -> t

val app_whnf : ?loc:location -> ty:t -> t -> t list -> t

application + WHNF

val const : ?loc:location -> ty:t -> ID.t -> t

val const_of_cstor : ?loc:location -> match_cstor -> t

val ite : ?loc:location -> t -> t -> t -> t

val match_ : ?loc:location -> t -> match_branch list -> t

val let_ : ?loc:location -> (t Var.t * t) list -> t -> t

val app_builtin : ?loc:location -> ty:t -> Builtin.t -> t list -> t

val builtin : ?loc:location -> ty:t -> Builtin.t -> t

val bind : ?loc:location -> ty:t -> Binder.t -> t Var.t -> t -> t

val bind_list : ?loc:location -> ty:t -> Binder.t -> t Var.t list -> t -> t

val multiset : ?loc:location -> ty:t -> t list -> t

val meta : ?loc:location -> meta_var -> t

val record : 
  ?loc:location ->
  ty:t ->
  (string * t) list ->
  rest:t Var.t option ->
  t

val record_flatten : 
  ?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 fun_l : ?loc:location -> t Var.t list -> t -> t

val of_string : ?loc:location -> ty:t -> string -> t

Make a constant from this string

val at_loc : ?loc:location -> t -> t

val with_ty : ty:t -> t -> t

val map_ty : t -> f:(t -> t) -> t

val fresh_var : ?loc:location -> ty:t -> unit -> t

fresh free variable with the given type.

val box_opaque : t -> t

Put a box around this

Specific Views

module Ty : sig ... end

val sort_ty_vars_first : t Var.t list -> t Var.t list

sort the given list of variables by putting type variables first

module Form : sig ... end

Utils

val is_var : t -> bool

val is_meta : t -> bool

val is_const : t -> bool

val is_fun : t -> bool

val is_ground : t -> bool

true iff there is no free variable

val is_monomorphic : t -> bool

true if there are no type variables

val is_subterm : strict:bool -> t -> of_:t -> bool

is_subterm a ~of_:b is true if a is a subterm of b.

parameter strict
if true, a must be a strict subterm of b, that is, not b itself

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 unfold_binder : Binder.t -> t -> t Var.t list * t

unfold_binder b (b v1 (b v2... (b vn t))) returns [v1,...,vn], t

val unfold_fun : t -> t Var.t list * t

val var_occurs : var:t Var.t -> t -> bool

var_occurs ~var t is true iff var occurs in t

val as_id_app : t -> (ID.t * Ty.t * t list) option

val vars : t -> t Var.t list

val free_vars : t -> t Var.t list

val free_vars_l : t list -> t Var.t list

val free_vars_set : t -> t Var.Set.t

val close_all : ty:t -> Binder.t -> t -> t

Bind all free vars with the symbol

val close_with_vars : ?binder:Binder.t -> t list -> t -> t

val map : 
  f:('a -> t -> t) ->
  bind:('a -> ty Var.t -> 'a * ty Var.t) ->
  'a ->
  t ->
  t

Generic non-recursive map

include Interfaces.PRINT with type t := t

val pp : t CCFormat.printer

val to_string : t -> string

val pp_inner : t CCFormat.printer

val pp_with_ty : t CCFormat.printer

val pp_in : Output_format.t -> t CCFormat.printer

module Set : Iter.Set.S with type elt = term

module Map : Iter.Map.S with type key = term

module Tbl : Hashtbl.S with type key = term

module Seq : sig ... end

Substitutions

module Subst : sig ... end

val rename : (term, term Var.t) Var.Subst.t -> t -> t

Perform renaming

val rename_all_vars : t -> t

Rename bound variables

Table of Variables

module Var_tbl : CCHashtbl.S with type key = t Var.t

Unification

exception UnifyFailure of string * (term * term) list * location option

val pp_stack : (term * term) list CCFormat.printer

module UStack : sig ... end

val unify : 
  ?allow_open:bool ->
  ?loc:location ->
  ?st:UStack.t ->
  ?subst:Subst.t ->
  term ->
  term ->
  unit

unifies destructively the two given terms, by modifying references that occur under Meta. Regular variables are not modified.

parameter allow_open
if true, metas can be unified to terms with free variables (default false)

parameter st
used for backtracking

parameter subst
substitution for bound variables

raises UnifyFailure
if unification fails.

val apply_unify : 
  ?gen_fresh_meta:(unit -> meta_var) ->
  ?allow_open:bool ->
  ?loc:location ->
  ?st:UStack.t ->
  ?subst:Subst.t ->
  t ->
  t list ->
  t

apply_unify f_ty args compute the type of a function of type f_ty, when applied to parameters args. The first elements of args might be interpreted as types, the other ones as terms (whose types are unified against expected types).

val app_infer : ?st:UStack.t -> ?subst:Subst.t -> t -> t list -> t

app_infer f l computes the type ty of f l, and return app ~ty f l

raises UnifyFailure
if types do not correspond

val try_alpha_renaming : t -> t -> Subst.t option

val simplify_formula : t -> t

val depth : t -> int

Conversion

val erase : t -> STerm.t

TPTP

module TPTP : sig ... end

module TPTP_THF : sig ... end

module ZF : sig ... end

package logtk

Module Logtk.TypedSTerm