module Term:sig
..end
Terms and Formulas
type
vsymbol = private {
|
vs_name : |
|
vs_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
type
lsymbol = private {
|
ls_name : |
|
ls_args : |
|
ls_value : |
|
ls_constr : |
|
ls_proj : |
}
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
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
type
pattern = private {
|
pat_node : |
|
pat_vars : |
|
pat_ty : |
}
type
pattern_node =
| |
Pwild |
| |
Pvar of |
| |
Papp of |
| |
Por of |
| |
Pas of |
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
type
quant =
| |
Tforall |
| |
Texists |
type
binop =
| |
Tand |
| |
Tor |
| |
Timplies |
| |
Tiff |
type
term = private {
|
t_node : |
|
t_ty : |
|
t_attrs : |
|
t_loc : |
}
type
term_node =
| |
Tvar of |
| |
Tconst of |
| |
Tapp of |
| |
Tif of |
| |
Tlet of |
| |
Tcase of |
| |
Teps of |
| |
Tquant of |
| |
Tbinop of |
| |
Tnot of |
| |
Ttrue |
| |
Tfalse |
type
term_bound
type
term_branch
type
term_quant
typetrigger =
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
flags enable comparison of the respective feature:
trigger
: triggers in quantified termsattr
: attributesloc
: source locationsconst
: when false, mathematically equal constants are considered equal,
even if written differentlyval 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)
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
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
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
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
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.
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
val ps_ignore : lsymbol
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.
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
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
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
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
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
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
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))
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
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
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.