Class Visitors.reduce

constraint 'b = < visit_'annot : 'c -> 'd -> 'f ; visit_'label : 'c -> 'g -> 'f ; visit_ALoc : 'c -> ALoc.t -> 'f ; visit_And : 'c -> Formula.t -> Formula.t -> 'f ; visit_Impl : 'c -> Formula.t -> Formula.t -> 'f ; visit_Apply : 'c -> string -> Expr.t -> 'g option -> 'f ; visit_ApplyLem : 'c -> string -> Expr.t list -> string list -> 'f ; visit_Arguments : 'c -> string -> 'f ; visit_Assert : 'c -> Formula.t -> 'f ; visit_Assignment : 'c -> string -> Expr.t -> 'f ; visit_Assume : 'c -> Formula.t -> 'f ; visit_AssumeType : 'c -> Expr.t -> Type.t -> 'f ; visit_BAnd : 'c -> 'f ; visit_BOr : 'c -> 'f ; visit_BImpl : 'c -> 'f ; visit_BSetMem : 'c -> 'f ; visit_BSetSub : 'c -> 'f ; visit_BinOp : 'c -> Expr.t -> BinOp.t -> Expr.t -> 'f ; visit_BitwiseAnd : 'c -> 'f ; visit_BitwiseAndL : 'c -> 'f ; visit_BitwiseAndF : 'c -> 'f ; visit_BitwiseNot : 'c -> 'f ; visit_BitwiseOr : 'c -> 'f ; visit_BitwiseOrL : 'c -> 'f ; visit_BitwiseOrF : 'c -> 'f ; visit_BitwiseXor : 'c -> 'f ; visit_BitwiseXorL : 'c -> 'f ; visit_BitwiseXorF : 'c -> 'f ; visit_Bool : 'c -> bool -> 'f ; visit_BooleanType : 'c -> 'f ; visit_Branch : 'c -> Formula.t -> 'f ; visit_Bug : 'c -> 'f ; visit_Call : 'c -> string -> Expr.t -> Expr.t list -> 'g option -> (string * (string * Expr.t) list) option -> 'f ; visit_Car : 'c -> 'f ; visit_Cdr : 'c -> 'f ; visit_Constant : 'c -> Constant.t -> 'f ; visit_IDiv : 'c -> 'f ; visit_FDiv : 'c -> 'f ; visit_ECall : 'c -> string -> Expr.t -> Expr.t list -> 'g option -> 'f ; visit_EList : 'c -> Expr.t list -> 'f ; visit_ESet : 'c -> Expr.t list -> 'f ; visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> 'f ; visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> 'f ; visit_Emp : 'c -> 'f ; visit_Empty : 'c -> 'f ; visit_EmptyType : 'c -> 'f ; visit_Epsilon : 'c -> 'f ; visit_Eq : 'c -> Expr.t -> Expr.t -> 'f ; visit_Equal : 'c -> 'f ; visit_Error : 'c -> 'f ; visit_Fail : 'c -> string -> Expr.t list -> 'f ; visit_False : 'c -> 'f ; visit_Fold : 'c -> string -> Expr.t list -> (string * (string * Expr.t) list) option -> 'f ; visit_ForAll : 'c -> (string * Type.t option) list -> Formula.t -> 'f ; visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> 'f ; visit_Wand : 'c -> (string * Expr.t list) -> (string * Expr.t list) -> 'f ; visit_GUnfold : 'c -> string -> 'f ; visit_Goto : 'c -> 'g -> 'f ; visit_GuardedGoto : 'c -> Expr.t -> 'g -> 'g -> 'f ; visit_If : 'c -> Expr.t -> LCmd.t list -> LCmd.t list -> 'f ; visit_Invariant : 'c -> Asrt.t -> string list -> 'f ; visit_Consume : 'c -> Asrt.t -> string list -> 'f ; visit_Produce : 'c -> Asrt.t -> 'f ; visit_LAction : 'c -> string -> string -> Expr.t list -> 'f ; visit_LList : 'c -> Literal.t list -> 'f ; visit_LVar : 'c -> LVar.t -> 'f ; visit_LeftShift : 'c -> 'f ; visit_LeftShiftL : 'c -> 'f ; visit_LeftShiftF : 'c -> 'f ; visit_FLess : 'c -> Expr.t -> Expr.t -> 'f ; visit_FLessEq : 'c -> Expr.t -> Expr.t -> 'f ; visit_ILess : 'c -> Expr.t -> Expr.t -> 'f ; visit_ILessEq : 'c -> Expr.t -> Expr.t -> 'f ; visit_IsInt : 'c -> Expr.t -> 'f ; visit_ILessThan : 'c -> 'f ; visit_ILessThanEqual : 'c -> 'f ; visit_FLessThan : 'c -> 'f ; visit_FLessThanEqual : 'c -> 'f ; visit_SLessThan : 'c -> 'f ; visit_ListType : 'c -> 'f ; visit_Lit : 'c -> Literal.t -> 'f ; visit_Loc : 'c -> string -> 'f ; visit_LocalTime : 'c -> 'f ; visit_Logic : 'c -> LCmd.t -> 'f ; visit_LstCat : 'c -> 'f ; visit_LstLen : 'c -> 'f ; visit_LstNth : 'c -> 'f ; visit_LstRepeat : 'c -> 'f ; visit_LstRev : 'c -> 'f ; visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f ; visit_M_abs : 'c -> 'f ; visit_M_acos : 'c -> 'f ; visit_M_asin : 'c -> 'f ; visit_M_atan : 'c -> 'f ; visit_M_atan2 : 'c -> 'f ; visit_M_ceil : 'c -> 'f ; visit_M_cos : 'c -> 'f ; visit_M_exp : 'c -> 'f ; visit_M_floor : 'c -> 'f ; visit_M_isNaN : 'c -> 'f ; visit_M_log : 'c -> 'f ; visit_M_pow : 'c -> 'f ; visit_M_round : 'c -> 'f ; visit_M_sgn : 'c -> 'f ; visit_M_sin : 'c -> 'f ; visit_M_sqrt : 'c -> 'f ; visit_M_tan : 'c -> 'f ; visit_Macro : 'c -> string -> Expr.t list -> 'f ; visit_Max_float : 'c -> 'f ; visit_MaxSafeInteger : 'c -> 'f ; visit_Min_float : 'c -> 'f ; visit_IMinus : 'c -> 'f ; visit_FMinus : 'c -> 'f ; visit_IMod : 'c -> 'f ; visit_FMod : 'c -> 'f ; visit_NOp : 'c -> NOp.t -> Expr.t list -> 'f ; visit_NoneType : 'c -> 'f ; visit_Nono : 'c -> 'f ; visit_Normal : 'c -> 'f ; visit_Not : 'c -> Formula.t -> 'f ; visit_Null : 'c -> 'f ; visit_NullType : 'c -> 'f ; visit_Int : 'c -> Z.t -> 'f ; visit_Num : 'c -> float -> 'f ; visit_IntType : 'c -> 'f ; visit_NumberType : 'c -> 'f ; visit_ObjectType : 'c -> 'f ; visit_Or : 'c -> Formula.t -> Formula.t -> 'f ; visit_PVar : 'c -> string -> 'f ; visit_PhiAssignment : 'c -> (string * Expr.t list) list -> 'f ; visit_Pi : 'c -> 'f ; visit_IPlus : 'c -> 'f ; visit_FPlus : 'c -> 'f ; visit_Pred : 'c -> string -> Expr.t list -> 'f ; visit_Pure : 'c -> Formula.t -> 'f ; visit_Random : 'c -> 'f ; visit_ReturnError : 'c -> 'f ; visit_ReturnNormal : 'c -> 'f ; visit_SL : 'c -> SLCmd.t -> 'f ; visit_SepAssert : 'c -> Asrt.t -> string list -> 'f ; visit_SetDiff : 'c -> 'f ; visit_SetInter : 'c -> 'f ; visit_SetMem : 'c -> Expr.t -> Expr.t -> 'f ; visit_SetSub : 'c -> Expr.t -> Expr.t -> 'f ; visit_SetToList : 'c -> 'f ; visit_SetType : 'c -> 'f ; visit_SetUnion : 'c -> 'f ; visit_SignedRightShift : 'c -> 'f ; visit_SignedRightShiftL : 'c -> 'f ; visit_SignedRightShiftF : 'c -> 'f ; visit_Skip : 'c -> 'f ; visit_FreshSVar : 'c -> string -> 'f ; visit_Star : 'c -> Asrt.t -> Asrt.t -> 'f ; visit_StrCat : 'c -> 'f ; visit_StrLen : 'c -> 'f ; visit_IntToNum : 'c -> 'f ; visit_NumToInt : 'c -> 'f ; visit_StrLess : 'c -> Expr.t -> Expr.t -> 'f ; visit_StrNth : 'c -> 'f ; visit_String : 'c -> string -> 'f ; visit_StringType : 'c -> 'f ; visit_SymbExec : 'c -> 'f ; visit_ITimes : 'c -> 'f ; visit_FTimes : 'c -> 'f ; visit_ToInt32Op : 'c -> 'f ; visit_ToIntOp : 'c -> 'f ; visit_ToNumberOp : 'c -> 'f ; visit_ToStringOp : 'c -> 'f ; visit_ToUint16Op : 'c -> 'f ; visit_ToUint32Op : 'c -> 'f ; visit_True : 'c -> 'f ; visit_Type : 'c -> Type.t -> 'f ; visit_TypeOf : 'c -> 'f ; visit_TypeType : 'c -> 'f ; visit_Types : 'c -> (Expr.t * Type.t) list -> 'f ; visit_UNot : 'c -> 'f ; visit_UTCTime : 'c -> 'f ; visit_UnOp : 'c -> UnOp.t -> Expr.t -> 'f ; visit_IUnaryMinus : 'c -> 'f ; visit_FUnaryMinus : 'c -> 'f ; visit_Undefined : 'c -> 'f ; visit_UndefinedType : 'c -> 'f ; visit_Unfold : 'c -> string -> Expr.t list -> (string * string) list option -> bool -> 'f ; visit_Package : 'c -> (string * Expr.t list) -> (string * Expr.t list) -> 'f ; visit_UnsignedRightShift : 'c -> 'f ; visit_UnsignedRightShiftL : 'c -> 'f ; visit_UnsignedRightShiftF : 'c -> 'f ; visit_assertion : 'c -> Asrt.t -> 'f ; visit_bindings : 'c -> (string * (string * Expr.t) list) -> 'f ; visit_binop : 'c -> BinOp.t -> 'f ; visit_bispec : 'c -> BiSpec.t -> 'f ; visit_cmd : 'c -> 'g Cmd.t -> 'f ; visit_constant : 'c -> Constant.t -> 'f ; visit_expr : 'c -> Expr.t -> 'f ; visit_flag : 'c -> Flag.t -> 'f ; visit_formula : 'c -> Formula.t -> 'f ; visit_lcmd : 'c -> LCmd.t -> 'f ; visit_lemma : 'c -> Lemma.t -> 'f ; visit_lemma_spec : 'c -> Lemma.spec -> 'f ; visit_literal : 'c -> Literal.t -> 'f ; visit_macro : 'c -> Macro.t -> 'f ; visit_nop : 'c -> NOp.t -> 'f ; visit_pred : 'c -> Pred.t -> 'f ; visit_proc : 'c -> ('d, 'g) Proc.t -> 'f ; visit_single_spec : 'c -> Spec.st -> 'f ; visit_slcmd : 'c -> SLCmd.t -> 'f ; visit_spec : 'c -> Spec.t -> 'f ; visit_typ : 'c -> Type.t -> 'f ; visit_unop : 'c -> UnOp.t -> 'f.. >
method private virtual plus : 'f -> 'f -> 'f
method visit_'annot : 'c -> 'd -> 'f
method visit_'label : 'c -> 'g -> 'f
method visit_ALoc : 'c -> ALoc.t -> 'f
method visit_And : 'c -> Formula.t -> Formula.t -> 'f
method visit_Impl : 'c -> Formula.t -> Formula.t -> 'f
method visit_Apply : 'c -> string -> Expr.t -> 'g option -> 'f
method visit_ApplyLem : 'c -> string -> Expr.t list -> string list -> 'f
method visit_Arguments : 'c -> string -> 'f
method visit_Assert : 'c -> Formula.t -> 'f
method visit_Assignment : 'c -> string -> Expr.t -> 'f
method visit_Assume : 'c -> Formula.t -> 'f
method visit_AssumeType : 'c -> Expr.t -> Type.t -> 'f
method visit_BAnd : 'c -> 'f
method visit_BOr : 'c -> 'f
method visit_BImpl : 'c -> 'f
method visit_BSetMem : 'c -> 'f
method visit_BSetSub : 'c -> 'f
method visit_BinOp : 'c -> Expr.t -> BinOp.t -> Expr.t -> 'f
method visit_BitwiseAnd : 'c -> 'f
method visit_BitwiseAndL : 'c -> 'f
method visit_BitwiseAndF : 'c -> 'f
method visit_BitwiseNot : 'c -> 'f
method visit_BitwiseOr : 'c -> 'f
method visit_BitwiseOrL : 'c -> 'f
method visit_BitwiseOrF : 'c -> 'f
method visit_BitwiseXor : 'c -> 'f
method visit_BitwiseXorL : 'c -> 'f
method visit_BitwiseXorF : 'c -> 'f
method visit_Bool : 'c -> bool -> 'f
method visit_BooleanType : 'c -> 'f
method visit_Branch : 'c -> Formula.t -> 'f
method visit_Bug : 'c -> 'f
method visit_Call : 'c -> string -> Expr.t -> Expr.t list -> 'g option -> (string * (string * Expr.t) list) option -> 'f
method visit_Car : 'c -> 'f
method visit_Cdr : 'c -> 'f
method visit_Constant : 'c -> Constant.t -> 'f
method visit_IDiv : 'c -> 'f
method visit_FDiv : 'c -> 'f
method visit_ECall : 'c -> string -> Expr.t -> Expr.t list -> 'g option -> 'f
method visit_EList : 'c -> Expr.t list -> 'f
method visit_ESet : 'c -> Expr.t list -> 'f
method visit_Exists : 'c -> (string * Type.t option) list -> Expr.t -> 'f
method visit_EForall : 'c -> (string * Type.t option) list -> Expr.t -> 'f
method visit_Emp : 'c -> 'f
method visit_Empty : 'c -> 'f
method visit_EmptyType : 'c -> 'f
method visit_Epsilon : 'c -> 'f
method visit_Eq : 'c -> Expr.t -> Expr.t -> 'f
method visit_Equal : 'c -> 'f
method visit_Error : 'c -> 'f
method visit_Fail : 'c -> string -> Expr.t list -> 'f
method visit_False : 'c -> 'f
method visit_Fold : 'c -> string -> Expr.t list -> (string * (string * Expr.t) list) option -> 'f
method visit_ForAll : 'c -> (string * Type.t option) list -> Formula.t -> 'f
method visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> 'f
method visit_Wand : 'c -> (string * Expr.t list) -> (string * Expr.t list) -> 'f
method visit_GUnfold : 'c -> string -> 'f
method visit_Goto : 'c -> 'g -> 'f
method visit_GuardedGoto : 'c -> Expr.t -> 'g -> 'g -> 'f
method visit_If : 'c -> Expr.t -> LCmd.t list -> LCmd.t list -> 'f
method visit_Invariant : 'c -> Asrt.t -> string list -> 'f
method visit_Consume : 'c -> Asrt.t -> string list -> 'f
method visit_Produce : 'c -> Asrt.t -> 'f
method visit_LAction : 'c -> string -> string -> Expr.t list -> 'f
method visit_LList : 'c -> Literal.t list -> 'f
method visit_LVar : 'c -> LVar.t -> 'f
method visit_LeftShift : 'c -> 'f
method visit_LeftShiftL : 'c -> 'f
method visit_LeftShiftF : 'c -> 'f
method visit_FLess : 'c -> Expr.t -> Expr.t -> 'f
method visit_FLessEq : 'c -> Expr.t -> Expr.t -> 'f
method visit_ILess : 'c -> Expr.t -> Expr.t -> 'f
method visit_ILessEq : 'c -> Expr.t -> Expr.t -> 'f
method visit_IsInt : 'c -> Expr.t -> 'f
method visit_ILessThan : 'c -> 'f
method visit_ILessThanEqual : 'c -> 'f
method visit_FLessThan : 'c -> 'f
method visit_FLessThanEqual : 'c -> 'f
method visit_SLessThan : 'c -> 'f
method visit_ListType : 'c -> 'f
method visit_Lit : 'c -> Literal.t -> 'f
method visit_Loc : 'c -> string -> 'f
method visit_LocalTime : 'c -> 'f
method visit_Logic : 'c -> LCmd.t -> 'f
method visit_LstCat : 'c -> 'f
method visit_LstLen : 'c -> 'f
method visit_LstNth : 'c -> 'f
method visit_LstRepeat : 'c -> 'f
method visit_LstRev : 'c -> 'f
method visit_LstSub : 'c -> Expr.t -> Expr.t -> Expr.t -> 'f
method visit_M_abs : 'c -> 'f
method visit_M_acos : 'c -> 'f
method visit_M_asin : 'c -> 'f
method visit_M_atan : 'c -> 'f
method visit_M_atan2 : 'c -> 'f
method visit_M_ceil : 'c -> 'f
method visit_M_cos : 'c -> 'f
method visit_M_exp : 'c -> 'f
method visit_M_floor : 'c -> 'f
method visit_M_isNaN : 'c -> 'f
method visit_M_log : 'c -> 'f
method visit_M_pow : 'c -> 'f
method visit_M_round : 'c -> 'f
method visit_M_sgn : 'c -> 'f
method visit_M_sin : 'c -> 'f
method visit_M_sqrt : 'c -> 'f
method visit_M_tan : 'c -> 'f
method visit_Macro : 'c -> string -> Expr.t list -> 'f
method visit_Max_float : 'c -> 'f
method visit_MaxSafeInteger : 'c -> 'f
method visit_Min_float : 'c -> 'f
method visit_IMinus : 'c -> 'f
method visit_FMinus : 'c -> 'f
method visit_IMod : 'c -> 'f
method visit_FMod : 'c -> 'f
method visit_NOp : 'c -> NOp.t -> Expr.t list -> 'f
method visit_NoneType : 'c -> 'f
method visit_Nono : 'c -> 'f
method visit_Normal : 'c -> 'f
method visit_Not : 'c -> Formula.t -> 'f
method visit_Null : 'c -> 'f
method visit_NullType : 'c -> 'f
method visit_Int : 'c -> Z.t -> 'f
method visit_Num : 'c -> float -> 'f
method visit_IntType : 'c -> 'f
method visit_NumberType : 'c -> 'f
method visit_ObjectType : 'c -> 'f
method visit_Or : 'c -> Formula.t -> Formula.t -> 'f
method visit_PVar : 'c -> string -> 'f
method visit_PhiAssignment : 'c -> (string * Expr.t list) list -> 'f
method visit_Pi : 'c -> 'f
method visit_IPlus : 'c -> 'f
method visit_FPlus : 'c -> 'f
method visit_Pred : 'c -> string -> Expr.t list -> 'f
method visit_Pure : 'c -> Formula.t -> 'f
method visit_Random : 'c -> 'f
method visit_ReturnError : 'c -> 'f
method visit_ReturnNormal : 'c -> 'f
method visit_SL : 'c -> SLCmd.t -> 'f
method visit_SepAssert : 'c -> Asrt.t -> string list -> 'f
method visit_SetDiff : 'c -> 'f
method visit_SetInter : 'c -> 'f
method visit_SetMem : 'c -> Expr.t -> Expr.t -> 'f
method visit_SetSub : 'c -> Expr.t -> Expr.t -> 'f
method visit_SetToList : 'c -> 'f
method visit_SetType : 'c -> 'f
method visit_SetUnion : 'c -> 'f
method visit_SignedRightShift : 'c -> 'f
method visit_SignedRightShiftL : 'c -> 'f
method visit_SignedRightShiftF : 'c -> 'f
method visit_Skip : 'c -> 'f
method visit_FreshSVar : 'c -> string -> 'f
method visit_Star : 'c -> Asrt.t -> Asrt.t -> 'f
method visit_StrCat : 'c -> 'f
method visit_StrLen : 'c -> 'f
method visit_IntToNum : 'c -> 'f
method visit_NumToInt : 'c -> 'f
method visit_StrLess : 'c -> Expr.t -> Expr.t -> 'f
method visit_StrNth : 'c -> 'f
method visit_String : 'c -> string -> 'f
method visit_StringType : 'c -> 'f
method visit_SymbExec : 'c -> 'f
method visit_ITimes : 'c -> 'f
method visit_FTimes : 'c -> 'f
method visit_ToInt32Op : 'c -> 'f
method visit_ToIntOp : 'c -> 'f
method visit_ToNumberOp : 'c -> 'f
method visit_ToStringOp : 'c -> 'f
method visit_ToUint16Op : 'c -> 'f
method visit_ToUint32Op : 'c -> 'f
method visit_True : 'c -> 'f
method visit_Type : 'c -> Type.t -> 'f
method visit_TypeOf : 'c -> 'f
method visit_TypeType : 'c -> 'f
method visit_Types : 'c -> (Expr.t * Type.t) list -> 'f
method visit_UNot : 'c -> 'f
method visit_UTCTime : 'c -> 'f
method visit_UnOp : 'c -> UnOp.t -> Expr.t -> 'f
method visit_IUnaryMinus : 'c -> 'f
method visit_FUnaryMinus : 'c -> 'f
method visit_Undefined : 'c -> 'f
method visit_UndefinedType : 'c -> 'f
method visit_Unfold : 'c -> string -> Expr.t list -> (string * string) list option -> bool -> 'f
method visit_Package : 'c -> (string * Expr.t list) -> (string * Expr.t list) -> 'f
method visit_UnsignedRightShift : 'c -> 'f
method visit_UnsignedRightShiftL : 'c -> 'f
method visit_UnsignedRightShiftF : 'c -> 'f
method visit_assertion : 'c -> Asrt.t -> 'f
method visit_bindings : 'c -> (string * (string * Expr.t) list) -> 'f
method visit_binop : 'c -> BinOp.t -> 'f
method visit_bispec : 'c -> BiSpec.t -> 'f
method visit_cmd : 'c -> 'g Cmd.t -> 'f
method visit_constant : 'c -> Constant.t -> 'f
method visit_expr : 'c -> Expr.t -> 'f
method visit_flag : 'c -> Flag.t -> 'f
method visit_formula : 'c -> Formula.t -> 'f
method visit_lcmd : 'c -> LCmd.t -> 'f
method visit_lemma : 'c -> Lemma.t -> 'f
method visit_lemma_spec : 'c -> Lemma.spec -> 'f
method visit_literal : 'c -> Literal.t -> 'f
method visit_macro : 'c -> Macro.t -> 'f
method visit_nop : 'c -> NOp.t -> 'f
method visit_pred : 'c -> Pred.t -> 'f
method visit_proc : 'c -> ('d, 'g) Proc.t -> 'f
method visit_single_spec : 'c -> Spec.st -> 'f
method visit_slcmd : 'c -> SLCmd.t -> 'f
method visit_spec : 'c -> Spec.t -> 'f
method visit_typ : 'c -> Type.t -> 'f
method visit_unop : 'c -> UnOp.t -> 'f
method private virtual zero : 'f