Module TypedSTerm

module TypedSTerm: sig .. end

Simple Typed Terms

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

type location = ParseLocation.t

type t

type term = t

type view = private

`\|`	`Var of t Var.t`	`(*`	variable	`*)`
`\|`	`Const of ID.t`	`(*`	constant	`*)`
`\|`	`App of t * t list`	`(*`	apply term	`*)`
`\|`	`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	`*)`

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

val view : t -> view

val loc : t -> location option

val ty : t -> t option

val ty_exn : t -> t

val head_exn : t -> ID.t

val deref : t -> t

While t is a bound Meta variable, follow its link

include Interfaces.HASH

include Interfaces.ORD

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 const : ?loc:location -> ty:t -> ID.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 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.

Specific Views

module Ty: sig .. end

module Form: sig .. end

Utils

val is_var : t -> bool

val is_meta : t -> bool

val is_const : 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.

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

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

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

var_occurs ~var t is true iff var occurs in t

val vars : t -> t Var.t list

val free_vars : t -> t Var.t list

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

Bind all free vars with the symbol

include Interfaces.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

Substitutions

module Subst: sig .. end

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.
Raises UnifyFailure if unification fails.

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

st : used for backtracking

subst : substitution for bound variables

val apply_unify : ?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 deref_rec : t -> t

Follow meta-variables links in all subterms

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

Conversion

val erase : t -> STerm.t

TPTP

module TPTP: sig .. end

module ZF: sig .. end