Previous  Up  Next

Module Exp

module Exp: sig .. end
Representation of expressions
type sfn1 =
| Sfn_NOT
| Sfn_item
| Sfn_sorted
| Sfn_hd
| Sfn_tl
| Sfn_set_of_list
| Sfn_can_return
Built-in functions with one argument
type sfn2 =
| Sfn_list_lt
| Sfn_items
| Sfn_subset
| Sfn_once_in_list
| Sfn_set_minus
Built-in functions with two arguments
type sfn =
| Sfn_list
| Sfn_set
| Sfn_AND
| Sfn_OR
| Sfn_XOR
| Sfn_undef
Built-in functions with a variable number of arguments
type sfn_grp =
| Sfn_plus
| Sfn_pos 
type id_internal1 
type id_internal2 
type id_internal3 
type exp = private
| Enum of int
| Eident of id_internal1 * id_internal2 * id_internal3
| Eeq of exp * exp
| Efun1 of sfn1 * exp
| Efun2 of sfn2 * exp * exp
| Efun of sfn * exp list
| Egrp of sfn_grp * int * ie_list (*Abelian groups*)
Canonical expressions
type ie_list = private
| IEnil
| IEcons of exp * int * ie_list 
type subst = exp -> exp
Substitutions

Standard functions


val string_of_sfn1 : sfn1 -> string
val string_of_sfn2 : sfn2 -> string
val string_of_sfn : sfn -> string
val string_of_sfn_grp : sfn_grp -> string

Identifiers


module Id: sig .. end
Identifiers 
module IdSet: Set.S  with type elt = Id.t
module IdMap: Map.S  with type key = Id.t

Expressions


module E: sig .. end
val equal_exp : exp -> exp -> bool
val compare_exp : exp -> exp -> int
val compare_exp_list : exp list -> exp list -> int
val abs_compare_exp : exp -> exp -> int
val mem_exp : exp -> exp list -> bool
val remdup_exp : exp list -> exp list
val existential_id : exp -> bool
return true if exp of the form _x
val exp_fold : (exp -> 'a -> 'a) -> exp -> 'a -> 'a
val ie_fold : (exp -> int -> 'a -> 'a) -> ie_list -> 'a -> 'a
val ie_fold_exp : (exp -> 'a -> 'a) -> ie_list -> 'a -> 'a

Substitutions


val mk_fun_subst : subst -> subst
val mk_id_subst : (Id.t -> exp) -> subst
val mk_subst : (Id.t, exp) Misc.plist -> subst
val mk_single_subst : Id.t -> exp -> subst
val mk_gensym_garb_subst : Id.t -> subst
val mk_gensym_garb_subst_idset : IdSet.t -> subst
val mk_gensym_garb_subst_idset2 : IdSet.t -> subst * subst
val existentials_rename_tonormal_sub : IdSet.t -> subst * subst
Replace existentials with gensym'd normal vars.
val existentials_rename_sub : IdSet.t -> subst
Replace existentials with gensym'd existential vars.
val map_sub : ('a -> 'a) -> 'a list -> 'a list
val map_idset : subst -> IdSet.t -> IdSet.t
val exp_no_s : string -> exp -> bool

Disjoint sets


module Dset: sig .. end
Disjoint sets

Fields


module Fld: sig .. end

Pretty printing


val pp_ident : Format.formatter -> Id.t -> unit
val pp_idset : Format.formatter -> IdSet.t -> unit
val pp_exp : Format.formatter -> exp -> unit
val pp_exp_list : Format.formatter -> exp list -> unit
val pp_fld : Format.formatter -> Fld.t -> unit

Identifier pools


type idpool 
val idpool_new : (string -> Id.t) -> string -> idpool
val idpool_combine : idpool -> 'a list -> ('a, exp) Misc.plist
val idpool_combine2 : idpool -> IdSet.t -> subst * subst
Imprint | Data protection