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

Quick access to the type of this term.

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 that t and u 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 set s of IDs that occur in t, and such that for each id in s, there is id' in s, id' ≠ id where name 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