Previous  Up  Next

Module Term

module Term: sig .. end

Terms and Formulas

Terms and Formulas

Variable symbols

type vsymbol = private {
   vs_name : Ident.ident;
   vs_ty : Ty.ty;
} 
module Mvs: Extmap.S  with type key = vsymbol
module Svs: Extset.S  with module M = Mvs
module Hvs: Exthtbl.S  with type key = vsymbol
module Wvs: Weakhtbl.S  with type key = vsymbol
val vs_compare : vsymbol -> vsymbol -> int
val vs_equal : vsymbol -> vsymbol -> bool
val vs_hash : vsymbol -> int
val create_vsymbol : Ident.preid -> Ty.ty -> vsymbol

Function and predicate symbols

type lsymbol = private {
   ls_name : Ident.ident;
   ls_args : Ty.ty list;
   ls_value : Ty.ty option;
   ls_constr : int;
   ls_proj : bool;
} 
module Mls: Extmap.S  with type key = lsymbol
module Sls: Extset.S  with module M = Mls
module Hls: Exthtbl.S  with type key = lsymbol
module Wls: Weakhtbl.S  with type key = lsymbol
val ls_compare : lsymbol -> lsymbol -> int
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol : ?constr:int ->
       ?proj:bool -> Ident.preid -> Ty.ty list -> Ty.ty option -> lsymbol
val create_fsymbol : ?constr:int ->
       ?proj:bool -> Ident.preid -> Ty.ty list -> Ty.ty -> lsymbol

~constr is the number of constructors of the type in which the symbol is a constructor otherwise it must be the default 0.

val create_psymbol : Ident.preid -> Ty.ty list -> lsymbol
val ls_ty_freevars : lsymbol -> Ty.Stv.t

Exceptions

exception EmptyCase
exception DuplicateVar of vsymbol
exception UncoveredVar of vsymbol
exception BadArity of lsymbol * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
exception ConstructorExpected of lsymbol
exception InvalidIntegerLiteralType of Ty.ty
exception InvalidRealLiteralType of Ty.ty
exception InvalidStringLiteralType of Ty.ty

Patterns

type pattern = private {
   pat_node : pattern_node;
   pat_vars : Svs.t;
   pat_ty : Ty.ty;
} 
type pattern_node =
| Pwild
| Pvar of vsymbol
| Papp of lsymbol * pattern list
| Por of pattern * pattern
| Pas of pattern * vsymbol

Smart constructors for patterns

val pat_wild : Ty.ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : lsymbol -> pattern list -> Ty.ty -> pattern
val pat_or : pattern -> pattern -> pattern
val pat_as : pattern -> vsymbol -> pattern

Generic traversal functions

val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool

Terms and Formulas

type quant =
| Tforall
| Texists 
type binop =
| Tand
| Tor
| Timplies
| Tiff 
type term = private {
   t_node : term_node;
   t_ty : Ty.ty option;
   t_attrs : Ident.Sattr.t;
   t_loc : Loc.position option;
} 
type term_node =
| Tvar of vsymbol
| Tconst of Constant.constant
| Tapp of lsymbol * term list
| Tif of term * term * term
| Tlet of term * term_bound
| Tcase of term * term_branch list
| Teps of term_bound
| Tquant of quant * term_quant
| Tbinop of binop * term * term
| Tnot of term
| Ttrue
| Tfalse 
type term_bound 
type term_branch 
type term_quant 
type trigger = term list list 
val term_size : term -> int

term_size t is the size, i.e. the number of term_node constructors occuring in t

val term_branch_size : term_branch -> int

term_branch_size t is the size of the term in the given term branch

Generic term equality

flags enable comparison of the respective feature:

val t_hash_generic : trigger:bool -> attr:bool -> const:bool -> term -> int
val t_compare_generic : trigger:bool ->
       attr:bool -> loc:bool -> const:bool -> term -> term -> int
val t_equal_generic : trigger:bool ->
       attr:bool -> loc:bool -> const:bool -> term -> term -> bool
val mterm_generic : trigger:bool ->
       attr:bool ->
       loc:bool -> const:bool -> (module Extmap.S with type key = term)
val sterm_generic : trigger:bool ->
       attr:bool ->
       loc:bool -> const:bool -> (module Extset.S with type M.key = term)
val hterm_generic : trigger:bool ->
       attr:bool ->
       loc:bool -> const:bool -> (module Exthtbl.S with type key = term)

Term equality modulo alpha-equivalence

val t_equal_strict : term -> term -> bool
val t_compare_strict : term -> term -> int
val t_hash_strict : term -> int
module Mterm_strict: Extmap.S  with type key = term
module Sterm_strict: Extset.S  with type M.key = term
module Hterm_strict: Exthtbl.S  with type key = term

Term equality modulo alpha-equivalence, attributes, triggers, locations, and constant syntax

val t_equal : term -> term -> bool
val t_compare : term -> term -> int
val t_hash : term -> int
module Mterm: Extmap.S  with type key = term
module Sterm: Extset.S  with type M.key = term
module Hterm: Exthtbl.S  with type key = term

Bindings

close bindings

val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
val t_close_quant : vsymbol list -> trigger -> term -> term_quant

open bindings

val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
val t_open_quant : term_quant -> vsymbol list * trigger * term
val t_open_bound_with : term -> term_bound -> term

t_open_bound_with t tb opens the binding tb and immediately replaces the corresponding bound variable with t

val t_clone_bound_id : ?loc:Loc.position -> ?attrs:Ident.Sattr.t -> term_bound -> Ident.preid

open bindings with optimized closing callbacks

val t_open_bound_cb : term_bound ->
       vsymbol * term * (vsymbol -> term -> term_bound)
val t_open_branch_cb : term_branch ->
       pattern * term * (pattern -> term -> term_branch)
val t_open_quant_cb : term_quant ->
       vsymbol list * trigger * term *
       (vsymbol list -> trigger -> term -> term_quant)

retrieve bound identifiers (useful to detect sharing)

val t_peek_bound : term_bound -> Ident.ident
val t_peek_branch : term_branch -> Ident.Sid.t
val t_peek_quant : term_quant -> Ident.ident list

Type checking

exception TermExpected of term
exception FmlaExpected of term
val t_type : term -> Ty.ty

t_type t checks that t is value-typed and returns its type

val t_prop : term -> term

t_prop t checks that t is prop-typed and returns t

val t_ty_check : term -> Ty.ty option -> unit

t_ty_check t ty checks that the type of t is ty

Smart constructors for terms and formulas

val t_app : lsymbol -> term list -> Ty.ty option -> term
val fs_app : lsymbol -> term list -> Ty.ty -> term
val ps_app : lsymbol -> term list -> term
val t_app_infer : lsymbol -> term list -> term
val ls_arg_inst : lsymbol -> term list -> Ty.ty Ty.Mtv.t
val ls_app_inst : lsymbol -> term list -> Ty.ty option -> Ty.ty Ty.Mtv.t
val check_literal : Constant.constant -> Ty.ty -> unit
val t_var : vsymbol -> term
val t_const : Constant.constant -> Ty.ty -> term
val t_if : term -> term -> term -> term
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : term_bound -> term
val t_quant : quant -> term_quant -> term
val t_forall : term_quant -> term
val t_exists : term_quant -> term
val t_binary : binop -> term -> term -> term
val t_and : term -> term -> term
val t_or : term -> term -> term
val t_implies : term -> term -> term
val t_iff : term -> term -> term
val t_not : term -> term
val t_true : term
val t_false : term
val t_nat_const : int -> term

t_nat_const n builds the constant integer term n, n must be non-negative

val t_int_const : BigInt.t -> term
val t_real_const : ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> term
val t_string_const : string -> term
val stop_split : Ident.attribute
val asym_split : Ident.attribute
val t_and_l : term list -> term
val t_or_l : term list -> term
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term
val t_and_asym_l : term list -> term
val t_or_asym_l : term list -> term
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> term -> term
val t_case_close : term -> (pattern * term) list -> term
val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close : vsymbol list -> trigger -> term -> term
val t_exists_close : vsymbol list -> trigger -> term -> term
val t_attr_set : ?loc:Loc.position -> Ident.Sattr.t -> term -> term
val t_attr_add : Ident.attribute -> term -> term
val t_attr_remove : Ident.attribute -> term -> term
val t_attr_copy : term -> term -> term

t_attr_copy src dst returns the term dst with attributes and locations augmented with those of term src

Constructors with propositional simplification

val t_let_close_simp : vsymbol -> term -> term -> term

t_let_close_simp v t1 t2 constructs the term let v=t1 in t2 but if the term t1 is simple enough, then it produces the equivalent term t2[v<-t2] instead.

val t_let_close_simp_keep_var : keep:bool -> vsymbol -> term -> term -> term

t_let_close_simp_keep_var v t1 t2 does the same as t_let_close_simp but when the second term is simple enough and keep is true, it produces the term let v=t1 in t2[v<-t2], keeping thus the variable v even if it is not used after the in

val t_if_simp : term -> term -> term -> term
val t_let_simp : term -> term_bound -> term

similar to t_let_close_simp but on a term_bound

val t_let_simp_keep_var : keep:bool -> term -> term_bound -> term

similar to t_let_close_simp_keep_var but on a term_bound

val t_case_simp : term -> term_branch list -> term
val t_quant_simp : quant -> term_quant -> term
val t_forall_simp : term_quant -> term
val t_exists_simp : term_quant -> term
val t_binary_simp : binop -> term -> term -> term
val t_and_simp : term -> term -> term
val t_and_simp_l : term list -> term
val t_or_simp : term -> term -> term
val t_or_simp_l : term list -> term
val t_implies_simp : term -> term -> term
val t_iff_simp : term -> term -> term
val t_not_simp : term -> term
val t_and_asym_simp : term -> term -> term
val t_and_asym_simp_l : term list -> term
val t_or_asym_simp : term -> term -> term
val t_or_asym_simp_l : term list -> term
val t_case_close_simp : term -> (pattern * term) list -> term
val t_quant_close_simp : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close_simp : vsymbol list -> trigger -> term -> term
val t_exists_close_simp : vsymbol list -> trigger -> term -> term
val t_forall_close_merge : vsymbol list -> term -> term
val t_exists_close_merge : vsymbol list -> term -> term

t_forall_close_merge vs f puts a universal quantifier over f; merges variable lists if f is already universally quantified; reuses triggers of f, if any, otherwise puts no triggers.

Built-in symbols

equality

val ps_equ : lsymbol

equality predicate

val t_equ : term -> term -> term
val t_neq : term -> term -> term
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term

General-purpose 'ignore' predicate

val ps_ignore : lsymbol

Booleans

val fs_bool_true : lsymbol
val fs_bool_false : lsymbol
val t_bool_true : term
val t_bool_false : term
val to_prop : term -> term

to_prop t converts the term t of type bool or prop into a term of type prop. Raises a typing error if t is not a Boolean term.

Tuples

val fs_tuple : int -> lsymbol

n-tuple

val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
val is_fs_tuple_id : Ident.ident -> int option

Higher order

val fs_func_app : lsymbol

higher-order application symbol

val t_func_app : term -> term -> term

value-typed application

val t_pred_app : term -> term -> term

prop-typed application

val t_func_app_l : term -> term list -> term

value-typed application

val t_pred_app_l : term -> term list -> term

prop-typed application

well-founded relations

val ps_acc : lsymbol

acc r x means x is accessible for relation r

val ps_wf : lsymbol

well_founded r means relation r is well-founded, that is, all elements are accessible

Lambda-term manipulation

val t_lambda : vsymbol list -> trigger -> term -> term

t_lambda vl tr e produces a term eps f. (forall vl [tr]. f@vl = e) or eps f. (forall vl [tr]. f@vl = True <-> e if e is prop-typed. If vl is empty, t_lambda returns e or if e then True else False, if e is prop-typed.

val t_open_lambda : term -> vsymbol list * trigger * term

t_open_lambda t returns a triple (vl,tr,e), such that t is equal to t_lambda vl tr e. If t is not a lambda-term, then vl is empty, tr is empty, and e is t. The term e may be prop-typed.

val t_open_lambda_cb : term ->
       vsymbol list * trigger * term *
       (vsymbol list -> trigger -> term -> term)

the same as t_open_lambda but returns additionally an instance of t_lambda that restores the original term if applied to the physically same arguments. Should be used in mapping functions.

val t_is_lambda : term -> bool

t_is_lambda t returns true if t is a lambda-term. Do not use this function if you call t_open_lambda afterwards. Internally, t_is_lambda opens binders itself, so you will pay twice the price. It is better to optimistically call t_open_lambda on any Teps, and handle the generic case if an empty argument list is returned.

val t_closure : lsymbol -> Ty.ty list -> Ty.ty option -> term

t_closure ls tyl oty returns a type-instantiated lambda-term \xx:tyl.(ls xx : oty), or ls : oty if ls is a constant. The length of tyl must be equal to that of ls.ls_args, and oty should be None if and only if ls is a predicate symbol.

val t_app_partial : lsymbol -> term list -> Ty.ty list -> Ty.ty option -> term

t_app_partial ls tl tyl oty produces a closure of ls and applies it to tl using t_func_app. The type signature of the closure is obtained by prepending the list of types of terms in tl to tyl. The resulting list must have the same length as ls.ls_args, and oty should be None if and only if ls is a predicate symbol. If the symbol is fully applied (tyl is empty), the Tapp term is returned. Otherwise, no beta-reduction is performed, in order to preserve the closure.

val t_func_app_beta : term -> term -> term

t_func_app_beta f a applies f to a performing beta-reduction when f is a lambda-term. Always returns a value-typed term, even if f is a lambda-term built on top of a formula.

val t_pred_app_beta : term -> term -> term

t_pred_app_beta f a applies f to a performing beta-reduction when f is a lambda-term. Always returns a formula, even if f is a lambda-term built on top of a bool-typed term.

val t_func_app_beta_l : term -> term list -> term
val t_pred_app_beta_l : term -> term list -> term

Term library

One-level (non-recursive) term traversal

val t_map : (term -> term) -> term -> term
val t_fold : ('a -> term -> 'a) -> 'a -> term -> 'a
val t_iter : (term -> unit) -> term -> unit
val t_map_fold : ('a -> term -> 'a * term) -> 'a -> term -> 'a * term
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool

Special maps

val t_map_simp : (term -> term) -> term -> term

t_map_simp reconstructs the term using simplification constructors

val t_map_sign : (bool -> term -> term) -> bool -> term -> term

t_map_sign passes a polarity parameter, unfolds if-then-else and iff

val t_map_cont : ((term -> 'a) -> term -> 'a) ->
       (term -> 'a) -> term -> 'a

t_map_cont is t_map in continuation-passing style

val list_map_cont : (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b

Trigger traversal

val tr_equal : trigger -> trigger -> bool
val tr_map : (term -> term) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) ->
       'a -> trigger -> 'a * trigger

Traversal with separate functions for value-typed and prop-typed terms

module TermTF: sig .. end

Map/fold over free variables

val t_v_map : (vsymbol -> term) -> term -> term
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val t_v_count : ('a -> vsymbol -> int -> 'a) -> 'a -> term -> 'a
val t_v_occurs : vsymbol -> term -> int

Variable substitution

val t_subst_single : vsymbol -> term -> term -> term

t_subst_single v t1 t2 substitutes variable v in t2 by t1

val t_subst : term Mvs.t -> term -> term

t_subst m t substitutes variables in t by the variable mapping m

val t_ty_subst : Ty.ty Ty.Mtv.t -> term Mvs.t -> term -> term

t_ty_subst mt mv t substitutes simultaneously type variables by mapping mt and term variables by mapping mv in term t

val t_subst_types : Ty.ty Ty.Mtv.t ->
       term Mvs.t -> term -> term Mvs.t * term

t_subst_types mt mv t substitutes type variables of term t by mapping mt. This operation may rename the variables in t, and the same renaming is simultaneously applied to the variables of the substitution mv (both domain and codomain). Example: t_subst_types {'a -> int} {x:'a -> t:'a} (f x) returns ({z:int -> t:int},(f z))

Find free variables and type variables

val t_closed : term -> bool
val t_vars : term -> int Mvs.t
val t_freevars : int Mvs.t -> term -> int Mvs.t
val t_ty_freevars : Ty.Stv.t -> term -> Ty.Stv.t

Map/fold over types and logical symbols in terms and patterns

val t_gen_map : (Ty.ty -> Ty.ty) ->
       (lsymbol -> lsymbol) ->
       vsymbol Mvs.t -> term -> term
val t_s_map : (Ty.ty -> Ty.ty) -> (lsymbol -> lsymbol) -> term -> term
val t_s_fold : ('a -> Ty.ty -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
val t_s_all : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_s_any : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_ty_map : (Ty.ty -> Ty.ty) -> term -> term
val t_ty_fold : ('a -> Ty.ty -> 'a) -> 'a -> term -> 'a

Map/fold over applications in terms (but not in patterns!)

val t_app_map : (lsymbol -> Ty.ty list -> Ty.ty option -> lsymbol) ->
       term -> term
val t_app_fold : ('a -> lsymbol -> Ty.ty list -> Ty.ty option -> 'a) ->
       'a -> term -> 'a

Fold over pattern matching (Requires pattern matching to be compiled)

val t_case_fold : ('a -> Ty.tysymbol -> Ty.ty list -> Ty.ty option -> 'a) ->
       'a -> term -> 'a

Subterm occurrence check and replacement

val t_occurs : term -> term -> bool
val t_replace : term -> term -> term -> term
val remove_unused_in_term : bool -> term -> term

remove_unused_in_term polarity t removes from t the occurrences and uses of symbols marked with attribute Ident.unused_attr. polarity is the polarity of t. Does nothing on sub-terms where polarity cannot be determined, so there might be some unused symbols left.