electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
Module Libelectrod . Elo
constraint 'c = < visit_'exp : 'env -> exp -> exp ; visit_'fml : 'env -> fml -> fml ; visit_'iexp : 'env -> iexp -> iexp ; visit_Add : 'env -> ibinop ; visit_All : 'env -> quant ; visit_And : 'env -> lbinop ; visit_Block : 'env -> fml list -> ( fml, exp, iexp ) ofml ; visit_Card : 'env -> exp -> ( fml, exp, iexp ) oiexp ; visit_Compr : 'env -> (bool * int * exp) list -> fml list -> ( fml, exp, iexp ) prim_oexp ; visit_Diff : 'env -> rbinop ; visit_F : 'env -> lunop ; visit_FIte : 'env -> fml -> fml -> fml -> ( fml, exp, iexp ) ofml ; visit_False : 'env -> ( fml, exp, iexp ) ofml ; visit_G : 'env -> lunop ; visit_Gt : 'env -> icomp_op ; visit_Gte : 'env -> icomp_op ; visit_H : 'env -> lunop ; visit_IBin : 'env -> iexp -> ibinop -> iexp -> ( fml, exp, iexp ) oiexp ; visit_IComp : 'env -> iexp -> icomp_op -> iexp -> ( fml, exp, iexp ) ofml ; visit_IEq : 'env -> icomp_op ; visit_INEq : 'env -> icomp_op ; visit_IUn : 'env -> iunop -> iexp -> ( fml, exp, iexp ) oiexp ; visit_Iden : 'env -> ( fml, exp, iexp ) prim_oexp ; visit_Iff : 'env -> lbinop ; visit_Imp : 'env -> lbinop ; visit_In : 'env -> comp_op ; visit_Inter : 'env -> rbinop ; visit_Join : 'env -> rbinop ; visit_LBin : 'env -> fml -> lbinop -> fml -> ( fml, exp, iexp ) ofml ; visit_LProj : 'env -> rbinop ; visit_LUn : 'env -> lunop -> fml -> ( fml, exp, iexp ) ofml ; visit_Lt : 'env -> icomp_op ; visit_Lte : 'env -> icomp_op ; visit_Name : 'env -> Libelectrod.Name.t -> ( fml, exp, iexp ) prim_oexp ; visit_Neg : 'env -> iunop ; visit_No : 'env -> quant ; visit_None_ : 'env -> ( fml, exp, iexp ) prim_oexp ; visit_Not : 'env -> lunop ; visit_NotIn : 'env -> comp_op ; visit_Num : 'env -> int -> ( fml, exp, iexp ) oiexp ; visit_O : 'env -> lunop ; visit_Or : 'env -> lbinop ; visit_Over : 'env -> rbinop ; visit_P : 'env -> lunop ; visit_Prime : 'env -> exp -> ( fml, exp, iexp ) prim_oexp ; visit_Prod : 'env -> rbinop ; visit_Quant : 'env -> quant -> (bool * int * exp) -> fml list -> ( fml, exp, iexp ) ofml ; visit_R : 'env -> lbinop ; visit_RBin : 'env -> exp -> rbinop -> exp -> ( fml, exp, iexp ) prim_oexp ; visit_RComp : 'env -> exp -> comp_op -> exp -> ( fml, exp, iexp ) ofml ; visit_REq : 'env -> comp_op ; visit_RIte : 'env -> fml -> exp -> exp -> ( fml, exp, iexp ) prim_oexp ; visit_RNEq : 'env -> comp_op ; visit_RProj : 'env -> rbinop ; visit_RTClos : 'env -> runop ; visit_RUn : 'env -> runop -> exp -> ( fml, exp, iexp ) prim_oexp ; visit_S : 'env -> lbinop ; visit_Some_ : 'env -> quant ; visit_Sub : 'env -> ibinop ; visit_T : 'env -> lbinop ; visit_TClos : 'env -> runop ; visit_Transpose : 'env -> runop ; visit_True : 'env -> ( fml, exp, iexp ) ofml ; visit_U : 'env -> lbinop ; visit_Union : 'env -> rbinop ; visit_Univ : 'env -> ( fml, exp, iexp ) prim_oexp ; visit_Var : 'env -> int -> ( fml, exp, iexp ) prim_oexp ; visit_X : 'env -> lunop ; visit_comp_op : 'env -> comp_op -> comp_op ; visit_exp : 'env -> exp -> exp ; visit_fml : 'env -> fml -> fml ; visit_ibinop : 'env -> ibinop -> ibinop ; visit_icomp_op : 'env -> icomp_op -> icomp_op ; visit_iexp : 'env -> iexp -> iexp ; visit_iunop : 'env -> iunop -> iunop ; visit_lbinop : 'env -> lbinop -> lbinop ; visit_lunop : 'env -> lunop -> lunop ; visit_oexp : 'env -> ( fml, exp, iexp ) oexp -> ( fml, exp, iexp ) oexp ; visit_ofml : 'env -> ( fml, exp, iexp ) ofml -> ( fml, exp, iexp ) ofml ; visit_oiexp : 'env -> ( fml, exp, iexp ) oiexp -> ( fml, exp, iexp ) oiexp ; visit_prim_oexp : 'env -> ( fml, exp, iexp ) prim_oexp -> ( fml, exp, iexp ) prim_oexp ; visit_quant : 'env -> quant -> quant ; visit_rbinop : 'env -> rbinop -> rbinop ; visit_runop : 'env -> runop -> runop.. >
method visit_'exp : 'env -> exp -> exp
method visit_'fml : 'env -> fml -> fml
method visit_'iexp : 'env -> iexp -> iexp
method visit_Add : 'env -> ibinop
method visit_All : 'env -> quant
method visit_And : 'env -> lbinop
method visit_Block : 'env -> fml list -> ( fml, exp, iexp ) ofml
method visit_Card : 'env -> exp -> ( fml, exp, iexp ) oiexp
method visit_Compr : 'env -> (bool * int * exp) list -> fml list -> ( fml, exp, iexp ) prim_oexp
method visit_Diff : 'env -> rbinop
method visit_F : 'env -> lunop
method visit_FIte : 'env -> fml -> fml -> fml -> ( fml, exp, iexp ) ofml
method visit_False : 'env -> ( fml, exp, iexp ) ofml
method visit_G : 'env -> lunop
method visit_Gt : 'env -> icomp_op
method visit_Gte : 'env -> icomp_op
method visit_H : 'env -> lunop
method visit_IBin : 'env -> iexp -> ibinop -> iexp -> ( fml, exp, iexp ) oiexp
method visit_IComp : 'env -> iexp -> icomp_op -> iexp -> ( fml, exp, iexp ) ofml
method visit_IEq : 'env -> icomp_op
method visit_INEq : 'env -> icomp_op
method visit_IUn : 'env -> iunop -> iexp -> ( fml, exp, iexp ) oiexp
method visit_Iden : 'env -> ( fml, exp, iexp ) prim_oexp
method visit_Iff : 'env -> lbinop
method visit_Imp : 'env -> lbinop
method visit_In : 'env -> comp_op
method visit_Inter : 'env -> rbinop
method visit_Join : 'env -> rbinop
method visit_LBin : 'env -> fml -> lbinop -> fml -> ( fml, exp, iexp ) ofml
method visit_LProj : 'env -> rbinop
method visit_LUn : 'env -> lunop -> fml -> ( fml, exp, iexp ) ofml
method visit_Lt : 'env -> icomp_op
method visit_Lte : 'env -> icomp_op
method visit_Name : 'env -> Libelectrod.Name.t -> ( fml, exp, iexp ) prim_oexp
method visit_Neg : 'env -> iunop
method visit_No : 'env -> quant
method visit_None_ : 'env -> ( fml, exp, iexp ) prim_oexp
method visit_Not : 'env -> lunop
method visit_NotIn : 'env -> comp_op
method visit_Num : 'env -> int -> ( fml, exp, iexp ) oiexp
method visit_O : 'env -> lunop
method visit_Or : 'env -> lbinop
method visit_Over : 'env -> rbinop
method visit_P : 'env -> lunop
method visit_Prime : 'env -> exp -> ( fml, exp, iexp ) prim_oexp
method visit_Prod : 'env -> rbinop
method visit_Quant : 'env -> quant -> (bool * int * exp) -> fml list -> ( fml, exp, iexp ) ofml
method visit_R : 'env -> lbinop
method visit_RBin : 'env -> exp -> rbinop -> exp -> ( fml, exp, iexp ) prim_oexp
method visit_RComp : 'env -> exp -> comp_op -> exp -> ( fml, exp, iexp ) ofml
method visit_REq : 'env -> comp_op
method visit_RIte : 'env -> fml -> exp -> exp -> ( fml, exp, iexp ) prim_oexp
method visit_RNEq : 'env -> comp_op
method visit_RProj : 'env -> rbinop
method visit_RTClos : 'env -> runop
method visit_RUn : 'env -> runop -> exp -> ( fml, exp, iexp ) prim_oexp
method visit_S : 'env -> lbinop
method visit_Some_ : 'env -> quant
method visit_Sub : 'env -> ibinop
method visit_T : 'env -> lbinop
method visit_TClos : 'env -> runop
method visit_Transpose : 'env -> runop
method visit_True : 'env -> ( fml, exp, iexp ) ofml
method visit_U : 'env -> lbinop
method visit_Union : 'env -> rbinop
method visit_Univ : 'env -> ( fml, exp, iexp ) prim_oexp
method visit_Var : 'env -> int -> ( fml, exp, iexp ) prim_oexp
method visit_X : 'env -> lunop
method private visit_array : 'env 'a 'b. ( 'env -> 'a -> 'b ) -> 'env -> 'a array -> 'b array
method private visit_bool : 'env. 'env -> bool -> bool
method private visit_bytes : 'env. 'env -> bytes -> bytes
method private visit_char : 'env. 'env -> char -> char
method visit_comp_op : 'env -> comp_op -> comp_op
method visit_exp : 'env -> exp -> exp
method private visit_float : 'env. 'env -> float -> float
method visit_fml : 'env -> fml -> fml
method visit_ibinop : 'env -> ibinop -> ibinop
method visit_icomp_op : 'env -> icomp_op -> icomp_op
method visit_iexp : 'env -> iexp -> iexp
method private visit_int : 'env. 'env -> int -> int
method private visit_int32 : 'env. 'env -> int32 -> int32
method private visit_int64 : 'env. 'env -> int64 -> int64
method visit_iunop : 'env -> iunop -> iunop
method private visit_lazy_t : 'env 'a 'b. ( 'env -> 'a -> 'b ) -> 'env -> 'a lazy_t -> 'b lazy_t
method visit_lbinop : 'env -> lbinop -> lbinop
method private visit_list : 'env 'a 'b. ( 'env -> 'a -> 'b ) -> 'env -> 'a list -> 'b list
method visit_lunop : 'env -> lunop -> lunop
method private visit_nativeint : 'env. 'env -> nativeint -> nativeint
method visit_oexp : 'env -> ( fml, exp, iexp ) oexp -> ( fml, exp, iexp ) oexp
method visit_ofml : 'env -> ( fml, exp, iexp ) ofml -> ( fml, exp, iexp ) ofml
method visit_oiexp : 'env -> ( fml, exp, iexp ) oiexp -> ( fml, exp, iexp ) oiexp
method private visit_option : 'env 'a 'b. ( 'env -> 'a -> 'b ) -> 'env -> 'a option -> 'b option
method visit_prim_oexp : 'env -> ( fml, exp, iexp ) prim_oexp -> ( fml, exp, iexp ) prim_oexp
method visit_quant : 'env -> quant -> quant
method visit_rbinop : 'env -> rbinop -> rbinop
method private visit_ref : 'env 'a 'b. ( 'env -> 'a -> 'b ) -> 'env -> 'a ref -> 'b ref
method private visit_result : 'env 'a 'b 'e 'f. ( 'env -> 'a -> 'b ) -> ( 'env -> 'e -> 'f ) -> 'env -> ( 'a, 'e ) result -> ( 'b, 'f ) result
method visit_runop : 'env -> runop -> runop
method private visit_string : 'env. 'env -> string -> string
method private visit_unit : 'env. 'env -> unit -> unit