Module Imandra_surface.Term
type const
=
|
Const_nativeint of nativeint
|
Const_int32 of int32
|
Const_int64 of int64
|
Const_float of float
|
Const_char of char
|
Const_string of string
|
Const_z of Z.t
|
Const_q of Q.t
type rec_flag
= Syn_term.rec_flag
=
|
Recursive
|
Nonrecursive
type var
= Var.t
type t
=
|
Const of const * Type.t
|
If of Type.t * t * t * t
|
Let of
{
ty : Type.t;
flg : rec_flag;
bs : t binding list;
body : t;
}
|
Apply of
{
ty : Type.t;
f : t;
l : t list;
}
|
Fun of
{
ty : Type.t;
v : Var.t;
body : t;
}
|
Ident of Var.t
|
Construct of
{
c : Uid.t;
ty : Type.t;
l : t list;
}
|
Destruct of
{
c : Uid.t;
data_ty : Type.t;
ty : Type.t;
i : int;
t : t;
}
|
Is_a of
{
c : Uid.t;
data_ty : Type.t;
t : t;
}
|
Tuple of
{
ty : Type.t;
l : t list;
}
|
Field of
{
ty : Type.t;
rec_ty : Type.t;
f : Uid.t;
t : t;
}
|
Tuple_field of
{
ty : Type.t;
tup_ty : Type.t;
i : int;
t : t;
}
|
Record of
{
ty : Type.t;
rows : (Uid.t * t) list;
rest : t option;
}
|
Bool of bool
|
Temp of Uid.t * Type.t
and 't binding
= Var.t * 't
type term
= t
type fo_pattern
=
|
FO_any
|
FO_bool of bool
|
FO_const of const
|
FO_var of Var.t
|
FO_app of Var.t * fo_pattern list
|
FO_cstor of Uid.t option * Type.t * fo_pattern list
|
FO_destruct of Uid.t option * Type.t * int * fo_pattern
|
FO_is_a of Uid.t * Type.t * fo_pattern
Patterns used for rewriting
module Syn : Syn_term.S with type const = const and type id = Uid.t and type var = Var.t and type ty = Type.t
generic transformation
val rename : Var.t Imandra_surface.Var.Map.t -> Var.t -> Var.t Imandra_surface.Var.Map.t * Var.t
val rename_t : t Imandra_surface.Var.Map.t -> Var.t -> t Imandra_surface.Var.Map.t * Var.t
val map : f:('b_acc -> t -> t) -> ty:('b_acc -> Type.t -> Type.t) -> bind:('b_acc -> Var.t -> 'b_acc * Var.t) -> 'b_acc -> t -> t
Generic map on terms. It doesn't perform recursion by itself, but applies
f
to immediate subterms. When traversing a binder,bind b_acc v
is called to obtain a new local environment and a renamed variable.Example: to rename variables we can write the following code. It traverses most terms using
map
(to traverse one level), but has a special case for variables. Also note howbind
is called on every binder (lambdas, lets, …) to update the substitution and yield a fresh copy of the variable.let rec rename subst t = match t with | Ident v -> Var.Map.find v subst | _ -> map subst t ~f:rename ~bind:(fun subst v -> let v' = Var.copy v in Var.Map.add v v', v')
val fold : f:('b_acc -> 'acc -> t -> 'acc) -> ?fty:('b_acc -> 'acc -> Type.t -> 'acc) -> bind:('b_acc -> Var.t -> 'b_acc) -> 'b_acc -> 'acc -> t -> 'acc
Generic fold on terms.
'b_acc
is a local binding environment that is updated when we traverse binders
val iter : f:('b_acc -> t -> unit) -> ?fty:('b_acc -> Type.t -> unit) -> bind:('b_acc -> Var.t -> 'b_acc) -> 'b_acc -> t -> unit
val chash_const : const Imandra_util.Chash.hasher
val chash : cb_id_f:(Uid.t -> unit) -> cb_id_ty:(Uid.t -> unit) -> ?local:Uid.Chash_map.t -> t Imandra_util.Chash.hasher
helpers
val mk_apply : ty:Type.t -> t -> t list -> t
val apply : t -> t list -> t
"smart" constructor for applications
val apply_beta_reduce : t -> t list -> t
val bool : bool -> t
val true_ : t
val false_ : t
val var : Var.t -> t
val implies : t -> t -> t
val or_ : t -> t -> t
val and_ : t -> t -> t
val or_l : t list -> t
val and_l : t list -> t
val eq : ty:Type.t -> t -> t -> t
val not_ : t -> t
val of_int : Z.t -> t
val ite : t -> t -> t -> t
val if_ : t -> t -> t -> t
val is_a : c:Uid.t -> data_ty:Type.t -> t -> t
val let_ : flg:rec_flag -> t binding list -> t -> t
val construct : c:Uid.t -> ty:Type.t -> t list -> t
val record : ty:Type.t -> (Uid.t * t) list -> rest:t option -> t
val tuple : ty:Type.t -> t list -> t
val destruct : data_ty:Type.t -> ty:Type.t -> c:Uid.t -> int -> t -> t
val field : rec_ty:Type.t -> ty:Type.t -> f:Uid.t -> t -> t
val tuple_field : tup_ty:Type.t -> ty:Type.t -> int -> t -> t
val fun_ : ty:Type.t -> Var.t -> t -> t
val fun_l : Var.t list -> t -> t
val int : Z.t -> t
val of_int : int -> t
val inst_of_term : ?rename:Var.t Imandra_surface.Var.Map.t -> t_subst:t Imandra_surface.Var.Map.t -> Type.subst -> t -> t
val apply_subst : t Imandra_surface.Var.Map.t -> t -> t
Basic application of a term substitution
val subst : was:t -> is:t -> t -> t
val frees_of_term : ?bound:Imandra_surface.Var.Set.t -> ?init:Imandra_surface.Var.Set.t -> t -> Imandra_surface.Var.Set.t
val frees_of_terms : ?bound:Imandra_surface.Var.Set.t -> ?init:Imandra_surface.Var.Set.t -> t list -> Imandra_surface.Var.Set.t
val all_ty_vars : t -> Imandra_surface.Type.Var.Set.t
val open_fun : t -> Var.t list * t
open_fun (fun x y -> body)
returns[x;y], body
val equal : t -> t -> bool
val hash : t -> int
val equal_constant : const -> const -> bool
val compare_constant : const -> const -> int
val hash_constant : const -> int
val equal_syntactic_approx : ?bound:Imandra_surface.Var.Set.t -> t -> t -> bool
Are the term syntactically equal, modulo alpha-renaming? This is an under-approximation, there are some complicated terms for which it might fail. However,
equal_syntactic_approx t u = true
implies thatt
andu
are indeed syntactically equiv.- parameter bound
set of bound variables (ie variables that are allowed to change)
val ambiguous_ids : t -> Imandra_surface.Uid.Set.t
ambiguous_ids t
returns a sets
of IDs that occur int
, and such that for eachid in s
, there isid' in s, id' ≠ id
wherename id = name id'
. For example,s
might contain two distinct IDs with name "f", which is ambiguous when printed
val size : t -> int
Printers
val pp_const : const CCFormat.printer
val pp_const_ocaml : const CCFormat.printer
val string_of_const : const -> string
val string_of_const_ocaml : const -> string
val print_fo_pattern : fo_pattern CCFormat.printer
module PP_syn : Syn_term.PP with module T = Syn
module PP_syn_ocaml : Syn_term.PP with module T = Syn
val print : t CCFormat.printer
Default pretty printer
val to_string : t -> string
Default pretty printer
val print_with : pp_ident_ty:bool -> expand_lambda:bool -> t CCFormat.printer
Default pretty printer
val to_string_with : pp_ident_ty:bool -> expand_lambda:bool -> t -> string
Default pretty printer
val print_as_value : Stdlib.Format.formatter -> t -> unit
val to_string_as_value : t -> string
val to_doc_str : t -> Imandra_document.Document.t
Render as string, wrap
val to_doc_str_with : expand_lambda:bool -> t -> Imandra_document.Document.t
Render as string, wrap
Render as string, wrap
val to_doc : ?expand_lambda:bool -> ?txt:bool -> t -> Imandra_document.Document.t
Render as string, wrap
as nested divs
Term-based models
module Model : sig ... end