endo (gillian.Gillian.Gil_syntax.Visitors.endo)


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

method visit_'annot : 'c -> 'd -> 'd

method visit_'label : 'c -> 'f -> 'f

method visit_ALoc : 'c -> Gil_syntax.Expr.t -> string -> Gil_syntax.Expr.t

method visit_And : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t

method visit_Impl : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t

method visit_Apply : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  Gil_syntax.Expr.t ->
  'f option ->
  'f Gil_syntax.Cmd.t

method visit_ApplyLem : 'c ->
  Gil_syntax.SLCmd.t ->
  string ->
  Gil_syntax.Expr.t list ->
  string list ->
  Gil_syntax.SLCmd.t

method visit_Arguments : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  'f Gil_syntax.Cmd.t

method visit_Assert : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.LCmd.t

method visit_Assignment : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  Gil_syntax.Expr.t ->
  'f Gil_syntax.Cmd.t

method visit_Assume : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.LCmd.t

method visit_AssumeType : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Type.t ->
  Gil_syntax.LCmd.t

method visit_BAnd : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BOr : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BImpl : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BSetMem : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BSetSub : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BinOp : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.BinOp.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

method visit_BitwiseAnd : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseAndL : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseAndF : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseNot : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_BitwiseOr : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseOrL : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseOrF : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseXor : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseXorL : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_BitwiseXorF : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_Bool : 'c -> Gil_syntax.Literal.t -> bool -> Gil_syntax.Literal.t

method visit_BooleanType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Branch : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.LCmd.t

method visit_Bug : 'c -> Gil_syntax.Flag.t -> Gil_syntax.Flag.t

method visit_Call : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t list ->
  'f option ->
  (string * (string * Gil_syntax.Expr.t) list) option ->
  'f Gil_syntax.Cmd.t

method visit_Car : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_Cdr : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_Constant : 'c ->
  Gil_syntax.Literal.t ->
  Gil_syntax.Constant.t ->
  Gil_syntax.Literal.t

method visit_ECall : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t list ->
  'f option ->
  'f Gil_syntax.Cmd.t

method visit_EList : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Expr.t

method visit_ESet : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Expr.t

method visit_Exists : 'c ->
  Gil_syntax.Expr.t ->
  (string * Gil_syntax.Type.t option) list ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

method visit_EForall : 'c ->
  Gil_syntax.Expr.t ->
  (string * Gil_syntax.Type.t option) list ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

method visit_Emp : 'c -> Gil_syntax.Asrt.t -> Gil_syntax.Asrt.t

method visit_Empty : 'c -> Gil_syntax.Literal.t -> Gil_syntax.Literal.t

method visit_EmptyType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Epsilon : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_Eq : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_Equal : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_Error : 'c -> Gil_syntax.Flag.t -> Gil_syntax.Flag.t

method visit_FDiv : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FLessThan : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FLessThanEqual : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FMinus : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FMod : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FPlus : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FTimes : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FUnaryMinus : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_Fail : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  Gil_syntax.Expr.t list ->
  'f Gil_syntax.Cmd.t

method visit_False : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t

method visit_Fold : 'c ->
  Gil_syntax.SLCmd.t ->
  string ->
  Gil_syntax.Expr.t list ->
  (string * (string * Gil_syntax.Expr.t) list) option ->
  Gil_syntax.SLCmd.t

method visit_ForAll : 'c ->
  Gil_syntax.Formula.t ->
  (string * Gil_syntax.Type.t option) list ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t

method visit_GA : 'c ->
  Gil_syntax.Asrt.t ->
  string ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Asrt.t

method visit_Wand : 'c ->
  Gil_syntax.Asrt.t ->
  (string * Gil_syntax.Expr.t list) ->
  (string * Gil_syntax.Expr.t list) ->
  Gil_syntax.Asrt.t

method visit_GUnfold : 'c -> Gil_syntax.SLCmd.t -> string -> Gil_syntax.SLCmd.t

method visit_Goto : 'c -> 'f Gil_syntax.Cmd.t -> 'f -> 'f Gil_syntax.Cmd.t

method visit_GuardedGoto : 'c ->
  'f Gil_syntax.Cmd.t ->
  Gil_syntax.Expr.t ->
  'f ->
  'f ->
  'f Gil_syntax.Cmd.t

method visit_IDiv : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_ILessThan : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_ILessThanEqual : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_IMinus : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_IMod : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_IPlus : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_ITimes : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_IUnaryMinus : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_If : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.LCmd.t list ->
  Gil_syntax.LCmd.t list ->
  Gil_syntax.LCmd.t

method visit_Int : 'c -> Gil_syntax.Literal.t -> Z.t -> Gil_syntax.Literal.t

method visit_IntType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Invariant : 'c ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.Asrt.t ->
  string list ->
  Gil_syntax.SLCmd.t

method visit_Consume : 'c ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.Asrt.t ->
  string list ->
  Gil_syntax.SLCmd.t

method visit_Produce : 'c ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.SLCmd.t

method visit_LAction : 'c ->
  'f Gil_syntax.Cmd.t ->
  string ->
  string ->
  Gil_syntax.Expr.t list ->
  'f Gil_syntax.Cmd.t

method visit_LList : 'c ->
  Gil_syntax.Literal.t ->
  Gil_syntax.Literal.t list ->
  Gil_syntax.Literal.t

method visit_LVar : 'c -> Gil_syntax.Expr.t -> string -> Gil_syntax.Expr.t

method visit_LeftShift : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_LeftShiftL : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_LeftShiftF : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_FLess : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_FLessEq : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_ILess : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_ILessEq : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_IsInt : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_ListType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Lit : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Literal.t ->
  Gil_syntax.Expr.t

method visit_Loc : 'c -> Gil_syntax.Literal.t -> string -> Gil_syntax.Literal.t

method visit_LocalTime : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_Logic : 'c ->
  'f Gil_syntax.Cmd.t ->
  Gil_syntax.LCmd.t ->
  'f Gil_syntax.Cmd.t

method visit_LstCat : 'c -> Gil_syntax.NOp.t -> Gil_syntax.NOp.t

method visit_LstLen : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_LstNth : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_LstRepeat : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_LstRev : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_LstSub : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

method visit_M_abs : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_acos : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_asin : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_atan : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_atan2 : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_M_ceil : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_cos : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_exp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_floor : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_isNaN : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_log : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_pow : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_M_round : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_sgn : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_sin : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_sqrt : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_M_tan : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_Macro : 'c ->
  Gil_syntax.LCmd.t ->
  string ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.LCmd.t

method visit_MaxSafeInteger : 'c ->
  Gil_syntax.Constant.t ->
  Gil_syntax.Constant.t

method visit_Max_float : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_Min_float : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_NOp : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.NOp.t ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Expr.t

method visit_NoneType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Nono : 'c -> Gil_syntax.Literal.t -> Gil_syntax.Literal.t

method visit_Normal : 'c -> Gil_syntax.Flag.t -> Gil_syntax.Flag.t

method visit_Not : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t

method visit_Null : 'c -> Gil_syntax.Literal.t -> Gil_syntax.Literal.t

method visit_NullType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Num : 'c -> Gil_syntax.Literal.t -> float -> Gil_syntax.Literal.t

method visit_NumberType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_ObjectType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Or : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Formula.t

method visit_PVar : 'c -> Gil_syntax.Expr.t -> string -> Gil_syntax.Expr.t

method visit_PhiAssignment : 'c ->
  'f Gil_syntax.Cmd.t ->
  (string * Gil_syntax.Expr.t list) list ->
  'f Gil_syntax.Cmd.t

method visit_Pi : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_Pred : 'c ->
  Gil_syntax.Asrt.t ->
  string ->
  Gil_syntax.Expr.t list ->
  Gil_syntax.Asrt.t

method visit_Pure : 'c ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Asrt.t

method visit_Random : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_ReturnError : 'c -> 'f Gil_syntax.Cmd.t -> 'f Gil_syntax.Cmd.t

method visit_ReturnNormal : 'c -> 'f Gil_syntax.Cmd.t -> 'f Gil_syntax.Cmd.t

method visit_SL : 'c ->
  Gil_syntax.LCmd.t ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.LCmd.t

method visit_SLessThan : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_SepAssert : 'c ->
  Gil_syntax.SLCmd.t ->
  Gil_syntax.Asrt.t ->
  string list ->
  Gil_syntax.SLCmd.t

method visit_SetDiff : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_SetInter : 'c -> Gil_syntax.NOp.t -> Gil_syntax.NOp.t

method visit_SetMem : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_SetSub : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_SetToList : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_SetType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_SetUnion : 'c -> Gil_syntax.NOp.t -> Gil_syntax.NOp.t

method visit_SignedRightShift : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_SignedRightShiftL : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_SignedRightShiftF : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_Skip : 'c -> 'f Gil_syntax.Cmd.t -> 'f Gil_syntax.Cmd.t

method visit_FreshSVar : 'c -> Gil_syntax.LCmd.t -> string -> Gil_syntax.LCmd.t

method visit_Star : 'c ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Asrt.t ->
  Gil_syntax.Asrt.t

method visit_StrCat : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_StrLen : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_IntToNum : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_NumToInt : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_StrLess : 'c ->
  Gil_syntax.Formula.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Formula.t

method visit_StrNth : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_String : 'c ->
  Gil_syntax.Literal.t ->
  string ->
  Gil_syntax.Literal.t

method visit_StringType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_SymbExec : 'c -> Gil_syntax.SLCmd.t -> Gil_syntax.SLCmd.t

method visit_ToInt32Op : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_ToIntOp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_ToNumberOp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_ToStringOp : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_ToUint16Op : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_ToUint32Op : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_True : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t

method visit_Type : 'c ->
  Gil_syntax.Literal.t ->
  Gil_syntax.Type.t ->
  Gil_syntax.Literal.t

method visit_TypeOf : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_TypeType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Types : 'c ->
  Gil_syntax.Asrt.t ->
  (Gil_syntax.Expr.t * Gil_syntax.Type.t) list ->
  Gil_syntax.Asrt.t

method visit_UNot : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t

method visit_UTCTime : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_UnOp : 'c ->
  Gil_syntax.Expr.t ->
  Gil_syntax.UnOp.t ->
  Gil_syntax.Expr.t ->
  Gil_syntax.Expr.t

method visit_Undefined : 'c -> Gil_syntax.Literal.t -> Gil_syntax.Literal.t

method visit_UndefinedType : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method visit_Unfold : 'c ->
  Gil_syntax.SLCmd.t ->
  string ->
  Gil_syntax.Expr.t list ->
  (string * string) list option ->
  bool ->
  Gil_syntax.SLCmd.t

method visit_Package : 'c ->
  Gil_syntax.SLCmd.t ->
  (string * Gil_syntax.Expr.t list) ->
  (string * Gil_syntax.Expr.t list) ->
  Gil_syntax.SLCmd.t

method visit_UnsignedRightShift : 'c ->
  Gil_syntax.BinOp.t ->
  Gil_syntax.BinOp.t

method visit_UnsignedRightShiftL : 'c ->
  Gil_syntax.BinOp.t ->
  Gil_syntax.BinOp.t

method visit_UnsignedRightShiftF : 'c ->
  Gil_syntax.BinOp.t ->
  Gil_syntax.BinOp.t

method private visit_array : 'env 'a. ('env -> 'a -> 'a) ->
  'env ->
  'a array ->
  'a array

method visit_assertion : 'c -> Gil_syntax.Asrt.t -> Gil_syntax.Asrt.t

method visit_bindings : 'c ->
  (string * (string * Gil_syntax.Expr.t) list) ->
  string * (string * Gil_syntax.Expr.t) list

method visit_binop : 'c -> Gil_syntax.BinOp.t -> Gil_syntax.BinOp.t

method visit_bispec : 'c -> Gil_syntax.BiSpec.t -> Gil_syntax.BiSpec.t

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_cmd : 'c -> 'f Gil_syntax.Cmd.t -> 'f Gil_syntax.Cmd.t

method visit_constant : 'c -> Gil_syntax.Constant.t -> Gil_syntax.Constant.t

method visit_expr : 'c -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t

method visit_flag : 'c -> Gil_syntax.Flag.t -> Gil_syntax.Flag.t

method private visit_float : 'env. 'env -> float -> float

method visit_formula : 'c -> Gil_syntax.Formula.t -> Gil_syntax.Formula.t

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 private visit_lazy_t : 'env 'a. ('env -> 'a -> 'a) ->
  'env ->
  'a Stdlib.Lazy.t ->
  'a Stdlib.Lazy.t

method visit_lcmd : 'c -> Gil_syntax.LCmd.t -> Gil_syntax.LCmd.t

method visit_lemma : 'c -> Gil_syntax.Lemma.t -> Gil_syntax.Lemma.t

method visit_lemma_spec : 'c -> Gil_syntax.Lemma.spec -> Gil_syntax.Lemma.spec

method private visit_list : 'env 'a. ('env -> 'a -> 'a) ->
  'env ->
  'a list ->
  'a list

method visit_literal : 'c -> Gil_syntax.Literal.t -> Gil_syntax.Literal.t

method visit_macro : 'c -> Gil_syntax.Macro.t -> Gil_syntax.Macro.t

method private visit_nativeint : 'env. 'env -> nativeint -> nativeint

method visit_nop : 'c -> Gil_syntax.NOp.t -> Gil_syntax.NOp.t

method private visit_option : 'env 'a. ('env -> 'a -> 'a) ->
  'env ->
  'a option ->
  'a option

method visit_pred : 'c -> Gil_syntax.Pred.t -> Gil_syntax.Pred.t

method visit_proc : 'c ->
  ('d, 'f) Gil_syntax.Proc.t ->
  ('d, 'f) Gil_syntax.Proc.t

method private visit_ref : 'env 'a. ('env -> 'a -> 'a) ->
  'env ->
  'a Stdlib.ref ->
  'a Stdlib.ref

method private visit_result : 'env 'a 'e. ('env -> 'a -> 'a) ->
  ('env -> 'e -> 'e) ->
  'env ->
  ('a, 'e) Result.result ->
  ('a, 'e) Result.result

method visit_single_spec : 'c -> Gil_syntax.Spec.st -> Gil_syntax.Spec.st

method visit_slcmd : 'c -> Gil_syntax.SLCmd.t -> Gil_syntax.SLCmd.t

method visit_spec : 'c -> Gil_syntax.Spec.t -> Gil_syntax.Spec.t

method private visit_string : 'env. 'env -> string -> string

method visit_typ : 'c -> Gil_syntax.Type.t -> Gil_syntax.Type.t

method private visit_unit : 'env. 'env -> unit -> unit

method visit_unop : 'c -> Gil_syntax.UnOp.t -> Gil_syntax.UnOp.t