Module Logtk.TermSource

Terms

Those terms provide a direct presentation of higher-order terms with lambdas in the sense that they make currying possible (as well as applying functions to other terms).

This is as if terms had an `apply` symbol everywhere, but more lightweight.

Types and terms are mixed because it makes application much easier (applying to a type and to a term are the same thing). It might also make dependent typing possible some day.

Term

Sourcetype t = private InnerTerm.t
Sourcetype term = t
Sourcetype var = Type.t HVar.t

Variables are typed with Type.t

Sourcetype view = private
  1. | AppBuiltin of Builtin.t * t list
  2. | DB of int
    (*

    Bound variable (De Bruijn index)

    *)
  3. | Var of var
    (*

    Term variable

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

    Typed constant

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

    Application to a list of terms (cannot be left-nested)

    *)
  6. | Fun of Type.t * t
    (*

    Lambda abstraction

    *)
Sourceval view : t -> view
Sourcemodule Classic : sig ... end
Sourceval subterm : sub:t -> t -> bool

checks whether sub is a (non-strict) subterm of t

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 ty : t -> Type.t

Obtain the type of a term..

Sourcemodule IntMap : Map.S with type key = int
Sourcemodule Set : CCSet.S with type elt = t
Sourcemodule Map : CCMap.S with type key = t
Sourcemodule Tbl : CCHashtbl.S with type key = t
Sourceval hash_mod_alpha : t -> int

Hash invariant w.r.t variable renaming

Sourceval same_l : t list -> t list -> bool

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise. Precondition: both lists have the same length

Sourceval same_l_gen : t list -> t list -> bool

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise. Precondition: both lists have the same length

Constructors

Sourceval var : var -> t
Sourceval var_of_int : ty:Type.t -> int -> t
Sourceval bvar : ty:Type.t -> int -> t

Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.

Sourceval builtin : ty:Type.t -> Builtin.t -> t
Sourceval app_builtin : ty:Type.t -> Builtin.t -> t list -> t
Sourceval const : ty:Type.t -> ID.t -> t

Create a typed constant

Sourceval tyapp : t -> Type.t list -> t

Apply a term to types

  • raises Type.Error

    if types do not match.

Sourceval app : t -> t list -> t

Apply a term to a list of terms

Sourceval app_w_ty : ty:Type.t -> t -> t list -> t

Apply a term to a list of terms

Sourceval app_full : t -> Type.t list -> t list -> t

Apply the term to types, then to terms

Sourceval true_ : t
Sourceval false_ : t
Sourceval fun_ : Type.t -> t -> t
Sourceval fun_l : Type.t list -> t -> t
Sourceval fun_of_fvars : var list -> t -> t

Build a function from a list of free vars + the body. This performs the De Bruijn transformation, and shifts the body.

Sourceval open_fun : t -> Type.t list * t
Sourceval open_fun_offset : offset:int -> t -> var list * t * int

open_fun ~offset (λxy. F) returns [v1,v2], F[v1/x,v2/y], offset+2 where v1 and v2 are fresh variables starting from offset

Sourceval grounding : Type.t -> t

grounding ty is a unique constant of type ty

Sourceval is_var : t -> bool
Sourceval is_appbuiltin : t -> bool
Sourceval is_bvar : t -> bool
Sourceval is_formula : t -> bool
Sourceval is_app : t -> bool
Sourceval is_const : t -> bool
Sourceval is_fun : t -> bool
Sourceval is_app_var : t -> bool
Sourceval is_type : t -> bool

Does it have type tType?

Sourceval in_pfho_fragment : t -> bool
Sourceval in_lfho_fragment : t -> bool
Sourceval is_fo_term : t -> bool
Sourceval is_true_or_false : t -> bool
Sourceval mk_fresh_skolem : var list -> Type.t -> (ID.t * Type.t) * t
Sourceval as_const : t -> ID.t option
Sourceval as_const_exn : t -> ID.t
Sourceval as_var : t -> var option
Sourceval as_var_exn : t -> var
Sourceval as_bvar_exn : t -> int
Sourceval as_app : t -> t * t list

as_app t decomposes t into a head (non-application) and arguments, such as (let f,l = as_app t in app f l) = t

Sourceval as_fun : t -> Type.t list * t

Open functions

Sourceval head_term : t -> t

head_term t = fst (as_app t)

Sourceval head_term_mono : t -> t

head term, but still with type arguments

Sourceval args : t -> t list

args t = snd (as_app t)

Sourceval of_term_unsafe : InnerTerm.t -> t

NOTE: this can break the invariants and make view fail. Only apply with caution.

Sourceval of_term_unsafe_l : InnerTerm.t list -> t list
Sourceval of_ty : Type.t -> t

Upcast from type

Sourceval mk_tmp_cst : counter:int ref -> ty:Type.t -> t
Sourcemodule VarSet : CCSet.S with type elt = var
Sourcemodule VarMap : CCMap.S with type key = var
Sourcemodule VarTbl : CCHashtbl.S with type key = var

Iters

Sourcemodule Seq : sig ... end
Sourceval var_occurs : var:var -> t -> bool

var_occurs ~var t true iff var in t

Sourceval is_ground : t -> bool

is the term ground? (no free vars)

Sourceval is_linear : t -> bool

is the term ground? (no free vars)

is the term linear? (no vars occuring multiple times)

Sourceval monomorphic : t -> bool

is the term linear? (no vars occuring multiple times)

true if the term contains no type var

Sourceval is_beta_reducible : t -> bool
Sourceval has_lambda : t -> bool
Sourceval max_var : VarSet.t -> int

find the maximum variable

Sourceval min_var : VarSet.t -> int

minimum variable

Sourceval add_vars : unit VarTbl.t -> t -> unit

add variables of the term to the set

Sourceval vars : t -> VarSet.t

compute variables of the terms

Sourceval vars_prefix_order : t -> var list

variables in prefix traversal order

Sourceval depth : t -> int

depth of the term

Sourceval head : t -> ID.t option

head ID.t

Sourceval head_exn : t -> ID.t

head ID.t (or Invalid_argument)

Sourceval size : t -> int

Size (number of nodes)

Sourceval simplify_bools : t -> t
Sourceval normalize_bools : t -> t
Sourceval cover_with_terms : ?depth:int -> ?recurse:bool -> t -> t option list -> t list
Sourceval max_cover : t -> t option list -> t
Sourceval weight : ?var:int -> ?sym:(ID.t -> int) -> t -> int

Compute the weight of a term, given a weight for variables and one for ID.ts.

  • parameter var

    unique weight for every variable (default 1)

  • parameter sym

    function from ID.ts to their weight (default const 1)

  • since 0.5.3
Sourceval ho_weight : t -> int
Sourceval ty_vars : t -> Type.VarSet.t

Set of free type variables

Sourceval is_ho_var : t -> bool
Sourceval is_ho_app : t -> bool

is_ho_app (F t1…tn) is true, when F is a variable (of any function type)

Sourceval as_ho_app : t -> (Type.t HVar.t * t list) option

as_ho_app (F t1…tn) = Some (F, [t1…tn])

Sourceval is_ho_pred : t -> bool

is_ho_pred (F t1…tn) is true, when F is a predicate variable

Sourceval is_ho_at_root : t -> bool

is_ho_at_root t returns true if the term t is a higher-order variable, possibly applied (i.e. is_ho_var t || is_ho_app t)

Subterms and Positions

Sourcemodule Pos : sig ... end
Sourceval replace : t -> old:t -> by:t -> t

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

Sourceval replace_m : t -> t Map.t -> t

replace t m syntactically replaces all occurrences of bindings of the map in t, starting from the root

High-level operations

Sourceval symbols : ?init:ID.Set.t -> t -> ID.Set.t

Symbols of the term (keys of signature)

Sourceval contains_symbol : ID.t -> t -> bool

Does the term contain this given ID.t?

Fold

High level fold-like combinators

Sourceval all_positions : ?vars:bool -> ?ty_args:bool -> ?var_args:bool -> ?fun_bodies:bool -> ?pos:Position.t -> t -> t Position.With.t Iter.t

Iterate on all sub-terms with their position.

  • parameter vars

    specifies whether variables are folded on (default false).

  • parameter ty_args

    specifies whether type arguments are folded on (default true).

  • parameter var_args

    specifies whether arguments of applied variables are folded on (default true).

  • parameter fun_bodies

    specifies whether bodies of lambda-expressions are folded on (default true).

  • parameter pos

    the initial position (default empty)

Some AC-utils

Sourcemodule type AC_SPEC = sig ... end
Sourcemodule AC (A : AC_SPEC) : sig ... end

Printing/parsing

Sourceval print_all_types : bool ref

If true, pp will print the types of all annotated terms

include Interfaces.PRINT with type t := t
Sourceval to_string : t -> string
include Interfaces.PRINT_DE_BRUIJN with type t := t and type term := t
Sourcetype print_hook = int -> t CCFormat.printer -> Format.formatter -> t -> bool

User-provided hook that can be used to print terms (for composite cases) before the default printing occurs. The int argument is the De Bruijn depth in the term. A hook takes as arguments the depth and the recursive printing function that it can use to print subterms. A hook should return true if it fired, false to fall back on the default printing.

Sourceval pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
Sourceval add_hook : print_hook -> unit

Hook used by default for printing

Sourceval default_hooks : unit -> print_hook list

List of default hooks

Sourceval debugf : Format.formatter -> t -> unit

debugf printing, with sorts

Formulas

Sourcemodule Form : sig ... end

Arith

Sourcemodule Arith : sig ... end
Sourceval close_quantifier : Builtin.t -> Type.t list -> t -> t
Sourceval has_ho_subterm : t -> bool
Sourcemodule DB : sig ... end

TPTP

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