Visitors.reduce
constraint
'b =
< visit_'annot : 'c -> 'd -> 'f
; visit_'label : 'c -> 'g -> 'f
; visit_ALoc : 'c -> Gil_syntax.ALoc.t -> 'f
; visit_And : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
; visit_Impl : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
; visit_Apply : 'c -> string -> Gil_syntax.Expr.t -> 'g option -> 'f
; visit_ApplyLem :
'c ->
string ->
Gil_syntax.Expr.t list ->
string list ->
'f
; visit_Arguments : 'c -> string -> 'f
; visit_Assert : 'c -> Gil_syntax.Formula.t -> 'f
; visit_Assignment : 'c -> string -> Gil_syntax.Expr.t -> 'f
; visit_Assume : 'c -> Gil_syntax.Formula.t -> 'f
; visit_AssumeType : 'c -> Gil_syntax.Expr.t -> Gil_syntax.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 ->
Gil_syntax.Expr.t ->
Gil_syntax.BinOp.t ->
Gil_syntax.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 -> Gil_syntax.Formula.t -> 'f
; visit_Bug : 'c -> 'f
; visit_Call :
'c ->
string ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t list ->
'g option ->
(string * (string * Gil_syntax.Expr.t) list) option ->
'f
; visit_Car : 'c -> 'f
; visit_Cdr : 'c -> 'f
; visit_Constant : 'c -> Gil_syntax.Constant.t -> 'f
; visit_IDiv : 'c -> 'f
; visit_FDiv : 'c -> 'f
; visit_ECall :
'c ->
string ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t list ->
'g option ->
'f
; visit_EList : 'c -> Gil_syntax.Expr.t list -> 'f
; visit_ESet : 'c -> Gil_syntax.Expr.t list -> 'f
; visit_Exists :
'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Expr.t ->
'f
; visit_EForall :
'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Expr.t ->
'f
; visit_Emp : 'c -> 'f
; visit_Empty : 'c -> 'f
; visit_EmptyType : 'c -> 'f
; visit_Epsilon : 'c -> 'f
; visit_Eq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_Equal : 'c -> 'f
; visit_Error : 'c -> 'f
; visit_Fail : 'c -> string -> Gil_syntax.Expr.t list -> 'f
; visit_False : 'c -> 'f
; visit_Fold :
'c ->
string ->
Gil_syntax.Expr.t list ->
(string * (string * Gil_syntax.Expr.t) list) option ->
'f
; visit_ForAll :
'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Formula.t ->
'f
; visit_GA :
'c ->
string ->
Gil_syntax.Expr.t list ->
Gil_syntax.Expr.t list ->
'f
; visit_Wand :
'c ->
(string * Gil_syntax.Expr.t list) ->
(string * Gil_syntax.Expr.t list) ->
'f
; visit_GUnfold : 'c -> string -> 'f
; visit_Goto : 'c -> 'g -> 'f
; visit_GuardedGoto : 'c -> Gil_syntax.Expr.t -> 'g -> 'g -> 'f
; visit_If :
'c ->
Gil_syntax.Expr.t ->
Gil_syntax.LCmd.t list ->
Gil_syntax.LCmd.t list ->
'f
; visit_Invariant : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
; visit_Consume : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
; visit_Produce : 'c -> Gil_syntax.Asrt.t -> 'f
; visit_LAction : 'c -> string -> string -> Gil_syntax.Expr.t list -> 'f
; visit_LList : 'c -> Gil_syntax.Literal.t list -> 'f
; visit_LVar : 'c -> Gil_syntax.LVar.t -> 'f
; visit_LeftShift : 'c -> 'f
; visit_LeftShiftL : 'c -> 'f
; visit_LeftShiftF : 'c -> 'f
; visit_FLess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_FLessEq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_ILess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_ILessEq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_IsInt : 'c -> Gil_syntax.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 -> Gil_syntax.Literal.t -> 'f
; visit_Loc : 'c -> string -> 'f
; visit_LocalTime : 'c -> 'f
; visit_Logic : 'c -> Gil_syntax.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 ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t ->
Gil_syntax.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 -> Gil_syntax.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 -> Gil_syntax.NOp.t -> Gil_syntax.Expr.t list -> 'f
; visit_NoneType : 'c -> 'f
; visit_Nono : 'c -> 'f
; visit_Normal : 'c -> 'f
; visit_Not : 'c -> Gil_syntax.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 -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
; visit_PVar : 'c -> string -> 'f
; visit_PhiAssignment : 'c -> (string * Gil_syntax.Expr.t list) list -> 'f
; visit_Pi : 'c -> 'f
; visit_IPlus : 'c -> 'f
; visit_FPlus : 'c -> 'f
; visit_Pred : 'c -> string -> Gil_syntax.Expr.t list -> 'f
; visit_Pure : 'c -> Gil_syntax.Formula.t -> 'f
; visit_Random : 'c -> 'f
; visit_ReturnError : 'c -> 'f
; visit_ReturnNormal : 'c -> 'f
; visit_SL : 'c -> Gil_syntax.SLCmd.t -> 'f
; visit_SepAssert : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
; visit_SetDiff : 'c -> 'f
; visit_SetInter : 'c -> 'f
; visit_SetMem : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
; visit_SetSub : 'c -> Gil_syntax.Expr.t -> Gil_syntax.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 -> Gil_syntax.Asrt.t -> Gil_syntax.Asrt.t -> 'f
; visit_StrCat : 'c -> 'f
; visit_StrLen : 'c -> 'f
; visit_IntToNum : 'c -> 'f
; visit_NumToInt : 'c -> 'f
; visit_StrLess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.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 -> Gil_syntax.Type.t -> 'f
; visit_TypeOf : 'c -> 'f
; visit_TypeType : 'c -> 'f
; visit_Types : 'c -> (Gil_syntax.Expr.t * Gil_syntax.Type.t) list -> 'f
; visit_UNot : 'c -> 'f
; visit_UTCTime : 'c -> 'f
; visit_UnOp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.Expr.t -> 'f
; visit_IUnaryMinus : 'c -> 'f
; visit_FUnaryMinus : 'c -> 'f
; visit_Undefined : 'c -> 'f
; visit_UndefinedType : 'c -> 'f
; visit_Unfold :
'c ->
string ->
Gil_syntax.Expr.t list ->
(string * string) list option ->
bool ->
'f
; visit_Package :
'c ->
(string * Gil_syntax.Expr.t list) ->
(string * Gil_syntax.Expr.t list) ->
'f
; visit_UnsignedRightShift : 'c -> 'f
; visit_UnsignedRightShiftL : 'c -> 'f
; visit_UnsignedRightShiftF : 'c -> 'f
; visit_assertion : 'c -> Gil_syntax.Asrt.t -> 'f
; visit_bindings : 'c -> (string * (string * Gil_syntax.Expr.t) list) -> 'f
; visit_binop : 'c -> Gil_syntax.BinOp.t -> 'f
; visit_bispec : 'c -> Gil_syntax.BiSpec.t -> 'f
; visit_cmd : 'c -> 'g Gil_syntax.Cmd.t -> 'f
; visit_constant : 'c -> Gil_syntax.Constant.t -> 'f
; visit_expr : 'c -> Gil_syntax.Expr.t -> 'f
; visit_flag : 'c -> Gil_syntax.Flag.t -> 'f
; visit_formula : 'c -> Gil_syntax.Formula.t -> 'f
; visit_lcmd : 'c -> Gil_syntax.LCmd.t -> 'f
; visit_lemma : 'c -> Gil_syntax.Lemma.t -> 'f
; visit_lemma_spec : 'c -> Gil_syntax.Lemma.spec -> 'f
; visit_literal : 'c -> Gil_syntax.Literal.t -> 'f
; visit_macro : 'c -> Gil_syntax.Macro.t -> 'f
; visit_nop : 'c -> Gil_syntax.NOp.t -> 'f
; visit_pred : 'c -> Gil_syntax.Pred.t -> 'f
; visit_proc : 'c -> ('d, 'g) Gil_syntax.Proc.t -> 'f
; visit_single_spec : 'c -> Gil_syntax.Spec.st -> 'f
; visit_slcmd : 'c -> Gil_syntax.SLCmd.t -> 'f
; visit_spec : 'c -> Gil_syntax.Spec.t -> 'f
; visit_typ : 'c -> Gil_syntax.Type.t -> 'f
; visit_unop : 'c -> Gil_syntax.UnOp.t -> 'f.. >
method visit_ALoc : 'c -> Gil_syntax.ALoc.t -> 'f
method visit_And : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
method visit_Impl : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
method visit_Apply : 'c -> string -> Gil_syntax.Expr.t -> 'g option -> 'f
method visit_ApplyLem : 'c ->
string ->
Gil_syntax.Expr.t list ->
string list ->
'f
method visit_Assert : 'c -> Gil_syntax.Formula.t -> 'f
method visit_Assignment : 'c -> string -> Gil_syntax.Expr.t -> 'f
method visit_Assume : 'c -> Gil_syntax.Formula.t -> 'f
method visit_AssumeType : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Type.t -> 'f
method visit_BinOp : 'c ->
Gil_syntax.Expr.t ->
Gil_syntax.BinOp.t ->
Gil_syntax.Expr.t ->
'f
method visit_Branch : 'c -> Gil_syntax.Formula.t -> 'f
method visit_Call : 'c ->
string ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t list ->
'g option ->
(string * (string * Gil_syntax.Expr.t) list) option ->
'f
method visit_Constant : 'c -> Gil_syntax.Constant.t -> 'f
method visit_ECall : 'c ->
string ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t list ->
'g option ->
'f
method visit_EList : 'c -> Gil_syntax.Expr.t list -> 'f
method visit_ESet : 'c -> Gil_syntax.Expr.t list -> 'f
method visit_Exists : 'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Expr.t ->
'f
method visit_EForall : 'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Expr.t ->
'f
method visit_Eq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_Fail : 'c -> string -> Gil_syntax.Expr.t list -> 'f
method visit_Fold : 'c ->
string ->
Gil_syntax.Expr.t list ->
(string * (string * Gil_syntax.Expr.t) list) option ->
'f
method visit_ForAll : 'c ->
(string * Gil_syntax.Type.t option) list ->
Gil_syntax.Formula.t ->
'f
method visit_GA : 'c ->
string ->
Gil_syntax.Expr.t list ->
Gil_syntax.Expr.t list ->
'f
method visit_Wand : 'c ->
(string * Gil_syntax.Expr.t list) ->
(string * Gil_syntax.Expr.t list) ->
'f
method visit_GuardedGoto : 'c -> Gil_syntax.Expr.t -> 'g -> 'g -> 'f
method visit_If : 'c ->
Gil_syntax.Expr.t ->
Gil_syntax.LCmd.t list ->
Gil_syntax.LCmd.t list ->
'f
method visit_Invariant : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
method visit_Consume : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
method visit_Produce : 'c -> Gil_syntax.Asrt.t -> 'f
method visit_LAction : 'c -> string -> string -> Gil_syntax.Expr.t list -> 'f
method visit_LList : 'c -> Gil_syntax.Literal.t list -> 'f
method visit_LVar : 'c -> Gil_syntax.LVar.t -> 'f
method visit_FLess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_FLessEq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_ILess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_ILessEq : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_IsInt : 'c -> Gil_syntax.Expr.t -> 'f
method visit_Lit : 'c -> Gil_syntax.Literal.t -> 'f
method visit_Logic : 'c -> Gil_syntax.LCmd.t -> 'f
method visit_LstSub : 'c ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t ->
Gil_syntax.Expr.t ->
'f
method visit_Macro : 'c -> string -> Gil_syntax.Expr.t list -> 'f
method visit_NOp : 'c -> Gil_syntax.NOp.t -> Gil_syntax.Expr.t list -> 'f
method visit_Not : 'c -> Gil_syntax.Formula.t -> 'f
method visit_Or : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t -> 'f
method visit_PhiAssignment : 'c -> (string * Gil_syntax.Expr.t list) list -> 'f
method visit_Pred : 'c -> string -> Gil_syntax.Expr.t list -> 'f
method visit_Pure : 'c -> Gil_syntax.Formula.t -> 'f
method visit_SL : 'c -> Gil_syntax.SLCmd.t -> 'f
method visit_SepAssert : 'c -> Gil_syntax.Asrt.t -> string list -> 'f
method visit_SetMem : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_SetSub : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_Star : 'c -> Gil_syntax.Asrt.t -> Gil_syntax.Asrt.t -> 'f
method visit_StrLess : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> 'f
method visit_Type : 'c -> Gil_syntax.Type.t -> 'f
method visit_Types : 'c -> (Gil_syntax.Expr.t * Gil_syntax.Type.t) list -> 'f
method visit_UnOp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.Expr.t -> 'f
method visit_Unfold : 'c ->
string ->
Gil_syntax.Expr.t list ->
(string * string) list option ->
bool ->
'f
method visit_Package : 'c ->
(string * Gil_syntax.Expr.t list) ->
(string * Gil_syntax.Expr.t list) ->
'f
method visit_assertion : 'c -> Gil_syntax.Asrt.t -> 'f
method visit_bindings : 'c ->
(string * (string * Gil_syntax.Expr.t) list) ->
'f
method visit_binop : 'c -> Gil_syntax.BinOp.t -> 'f
method visit_bispec : 'c -> Gil_syntax.BiSpec.t -> 'f
method visit_cmd : 'c -> 'g Gil_syntax.Cmd.t -> 'f
method visit_constant : 'c -> Gil_syntax.Constant.t -> 'f
method visit_expr : 'c -> Gil_syntax.Expr.t -> 'f
method visit_flag : 'c -> Gil_syntax.Flag.t -> 'f
method visit_formula : 'c -> Gil_syntax.Formula.t -> 'f
method visit_lcmd : 'c -> Gil_syntax.LCmd.t -> 'f
method visit_lemma : 'c -> Gil_syntax.Lemma.t -> 'f
method visit_lemma_spec : 'c -> Gil_syntax.Lemma.spec -> 'f
method visit_literal : 'c -> Gil_syntax.Literal.t -> 'f
method visit_macro : 'c -> Gil_syntax.Macro.t -> 'f
method visit_nop : 'c -> Gil_syntax.NOp.t -> 'f
method visit_pred : 'c -> Gil_syntax.Pred.t -> 'f
method visit_proc : 'c -> ('d, 'g) Gil_syntax.Proc.t -> 'f
method visit_single_spec : 'c -> Gil_syntax.Spec.st -> 'f
method visit_slcmd : 'c -> Gil_syntax.SLCmd.t -> 'f
method visit_spec : 'c -> Gil_syntax.Spec.t -> 'f
method visit_typ : 'c -> Gil_syntax.Type.t -> 'f
method visit_unop : 'c -> Gil_syntax.UnOp.t -> 'f