package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Logtk.TypedSTermSource

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.

Sourcetype location = ParseLocation.t
Sourcetype t
Sourcetype term = t
Sourcetype ty = t
Sourcetype match_cstor = {
  1. cstor_id : ID.t;
  2. cstor_ty : ty;
  3. cstor_args : ty list;
}

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

Sourcetype match_branch = match_cstor * t Var.t list * t
Sourcetype view = private
  1. | Var of t Var.t
    (*

    variable

    *)
  2. | Const of ID.t
    (*

    constant

    *)
  3. | App of t * t list
    (*

    apply term

    *)
  4. | Ite of t * t * t
  5. | Match of t * match_branch list
  6. | Let of (t Var.t * t) list * t
  7. | Bind of Binder.t * t Var.t * t
    (*

    bind variable in term

    *)
  8. | AppBuiltin of Builtin.t * t list
  9. | Multiset of t list
  10. | Record of (string * t) list * t option
    (*

    extensible record

    *)
  11. | Meta of meta_var
    (*

    Unification variable

    *)
Sourceand meta_var = t Var.t * t option ref * [ `Generalize | `BindDefault | `NoBind ]
Sourceval view : t -> view
Sourceval loc : t -> location option
Sourceval ty : t -> t option
Sourceval ty_exn : t -> t
Sourceval head : t -> ID.t option
Sourceval head_exn : t -> ID.t
Sourceval 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
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
include Interfaces.ORD with type t := t
Sourceval compare : t -> t -> int

Constructors

Sourceexception IllFormedTerm of string
Sourceval tType : t
Sourceval prop : t
Sourceval var : ?loc:location -> t Var.t -> t
Sourceval var_of_string : ?loc:location -> ty:t -> string -> t
Sourceval app : ?loc:location -> ty:t -> t -> t list -> t
Sourceval app_whnf : ?loc:location -> ty:t -> t -> t list -> t

application + WHNF

Sourceval const : ?loc:location -> ty:t -> ID.t -> t
Sourceval const_of_cstor : ?loc:location -> match_cstor -> t
Sourceval ite : ?loc:location -> t -> t -> t -> t
Sourceval match_ : ?loc:location -> t -> match_branch list -> t
Sourceval let_ : ?loc:location -> (t Var.t * t) list -> t -> t
Sourceval app_builtin : ?loc:location -> ty:t -> Builtin.t -> t list -> t
Sourceval builtin : ?loc:location -> ty:t -> Builtin.t -> t
Sourceval bind : ?loc:location -> ty:t -> Binder.t -> t Var.t -> t -> t
Sourceval bind_list : ?loc:location -> ty:t -> Binder.t -> t Var.t list -> t -> t
Sourceval multiset : ?loc:location -> ty:t -> t list -> t
Sourceval meta : ?loc:location -> meta_var -> t
Sourceval record : ?loc:location -> ty:t -> (string * t) list -> rest:t Var.t option -> t
Sourceval 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.

Sourceval fun_l : ?loc:location -> t Var.t list -> t -> t
Sourceval of_string : ?loc:location -> ty:t -> string -> t

Make a constant from this string

Sourceval at_loc : ?loc:location -> t -> t
Sourceval with_ty : ty:t -> t -> t
Sourceval map_ty : t -> f:(t -> t) -> t
Sourceval fresh_var : ?loc:location -> ty:t -> unit -> t

fresh free variable with the given type.

Sourceval box_opaque : t -> t

Put a box around this

Specific Views

Sourcemodule Ty : sig ... end
Sourceval sort_ty_vars_first : t Var.t list -> t Var.t list

sort the given list of variables by putting type variables first

Sourcemodule Form : sig ... end

Utils

Sourceval is_var : t -> bool
Sourceval is_meta : t -> bool
Sourceval is_const : t -> bool
Sourceval is_fun : t -> bool
Sourceval is_ground : t -> bool

true iff there is no free variable

Sourceval is_monomorphic : t -> bool

true if there are no type variables

Sourceval 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

Sourceval 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)

Sourceval unfold_binder : Binder.t -> t -> t Var.t list * t

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

Sourceval unfold_fun : t -> t Var.t list * t
Sourceval var_occurs : var:t Var.t -> t -> bool

var_occurs ~var t is true iff var occurs in t

Sourceval as_id_app : t -> (ID.t * Ty.t * t list) option
Sourceval vars : t -> t Var.t list
Sourceval free_vars : t -> t Var.t list
Sourceval free_vars_l : t list -> t Var.t list
Sourceval free_vars_set : t -> t Var.Set.t
Sourceval close_all : ty:t -> Binder.t -> t -> t

Bind all free vars with the symbol

Sourceval 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
Sourceval to_string : t -> string
Sourceval pp_inner : t CCFormat.printer
Sourceval pp_with_ty : t CCFormat.printer
Sourcemodule Set : Iter.Set.S with type elt = term
Sourcemodule Map : Iter.Map.S with type key = term
Sourcemodule Tbl : Hashtbl.S with type key = term
Sourcemodule Seq : sig ... end

Substitutions

Sourcemodule Subst : sig ... end
Sourceval rename : (term, term Var.t) Var.Subst.t -> t -> t

Perform renaming

Sourceval rename_all_vars : t -> t

Rename bound variables

Table of Variables

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

Unification

Sourceexception UnifyFailure of string * (term * term) list * location option
Sourceval pp_stack : (term * term) list CCFormat.printer
Sourcemodule UStack : sig ... end
Sourceval 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

Sourceval 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).

Sourceval 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

Conversion

Sourceval erase : t -> STerm.t

TPTP

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

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct