Class `Gen_goal.map`Source


  constraint
    'c =
    < visit_'i : 'd -> 'g -> 'h
    ; visit_'v : 'd -> 'i -> 'j
    ; visit_Add : 'd -> ibinop
    ; visit_All : 'd -> quant
    ; visit_And : 'd -> lbinop
    ; visit_Block : 'd -> ('i, 'g) block -> ('j, 'h) prim_fml
    ; visit_BoxJoin : 
      'd ->
      ('i, 'g) exp ->
      ('i, 'g) exp list ->
      ('j, 'h) prim_exp
    ; visit_Card : 'd -> ('i, 'g) exp -> ('j, 'h) prim_iexp
    ; visit_Compr : 
      'd ->
      ('i, 'g) sim_binding list ->
      ('i, 'g) block ->
      ('j, 'h) prim_exp
    ; visit_Diff : 'd -> rbinop
    ; visit_F : 'd -> lunop
    ; visit_FIte : 
      'd ->
      ('i, 'g) fml ->
      ('i, 'g) fml ->
      ('i, 'g) fml ->
      ('j, 'h) prim_fml
    ; visit_False : 'd -> ('j, 'h) prim_fml
    ; visit_G : 'd -> lunop
    ; visit_Gt : 'd -> icomp_op
    ; visit_Gte : 'd -> icomp_op
    ; visit_H : 'd -> lunop
    ; visit_IBin : 
      'd ->
      ('i, 'g) iexp ->
      ibinop ->
      ('i, 'g) iexp ->
      ('j, 'h) prim_iexp
    ; visit_IComp : 
      'd ->
      ('i, 'g) iexp ->
      icomp_op ->
      ('i, 'g) iexp ->
      ('j, 'h) prim_fml
    ; visit_IEq : 'd -> icomp_op
    ; visit_INEq : 'd -> icomp_op
    ; visit_IUn : 'd -> iunop -> ('i, 'g) iexp -> ('j, 'h) prim_iexp
    ; visit_Iden : 'd -> ('j, 'h) prim_exp
    ; visit_Ident : 'd -> 'g -> ('j, 'h) prim_exp
    ; visit_Iff : 'd -> lbinop
    ; visit_Imp : 'd -> lbinop
    ; visit_In : 'd -> comp_op
    ; visit_Inter : 'd -> rbinop
    ; visit_Join : 'd -> rbinop
    ; visit_LBin : 
      'd ->
      ('i, 'g) fml ->
      lbinop ->
      ('i, 'g) fml ->
      ('j, 'h) prim_fml
    ; visit_LProj : 'd -> rbinop
    ; visit_LUn : 'd -> lunop -> ('i, 'g) fml -> ('j, 'h) prim_fml
    ; visit_Let : 
      'd ->
      ('i, 'g) binding list ->
      ('i, 'g) block ->
      ('j, 'h) prim_fml
    ; visit_Lone : 'd -> quant
    ; visit_Lt : 'd -> icomp_op
    ; visit_Lte : 'd -> icomp_op
    ; visit_Neg : 'd -> iunop
    ; visit_No : 'd -> quant
    ; visit_None_ : 'd -> ('j, 'h) prim_exp
    ; visit_Not : 'd -> lunop
    ; visit_NotIn : 'd -> comp_op
    ; visit_Num : 'd -> int -> ('j, 'h) prim_iexp
    ; visit_O : 'd -> lunop
    ; visit_One : 'd -> quant
    ; visit_Or : 'd -> lbinop
    ; visit_Over : 'd -> rbinop
    ; visit_P : 'd -> lunop
    ; visit_Prime : 'd -> ('i, 'g) exp -> ('j, 'h) prim_exp
    ; visit_Prod : 'd -> rbinop
    ; visit_Qual : 'd -> rqualify -> ('i, 'g) exp -> ('j, 'h) prim_fml
    ; visit_Quant : 
      'd ->
      quant ->
      ('i, 'g) sim_binding list ->
      ('i, 'g) block ->
      ('j, 'h) prim_fml
    ; visit_R : 'd -> lbinop
    ; visit_RBin : 
      'd ->
      ('i, 'g) exp ->
      rbinop ->
      ('i, 'g) exp ->
      ('j, 'h) prim_exp
    ; visit_RComp : 
      'd ->
      ('i, 'g) exp ->
      comp_op ->
      ('i, 'g) exp ->
      ('j, 'h) prim_fml
    ; visit_REq : 'd -> comp_op
    ; visit_RIte : 
      'd ->
      ('i, 'g) fml ->
      ('i, 'g) exp ->
      ('i, 'g) exp ->
      ('j, 'h) prim_exp
    ; visit_RLone : 'd -> rqualify
    ; visit_RNEq : 'd -> comp_op
    ; visit_RNo : 'd -> rqualify
    ; visit_ROne : 'd -> rqualify
    ; visit_RProj : 'd -> rbinop
    ; visit_RSome : 'd -> rqualify
    ; visit_RTClos : 'd -> runop
    ; visit_RUn : 'd -> runop -> ('i, 'g) exp -> ('j, 'h) prim_exp
    ; visit_Run : 'd -> (('i, 'g) block * bool option) -> ('j, 'h) t
    ; visit_S : 'd -> lbinop
    ; visit_Some_ : 'd -> quant
    ; visit_Sub : 'd -> ibinop
    ; visit_T : 'd -> lbinop
    ; visit_TClos : 'd -> runop
    ; visit_Transpose : 'd -> runop
    ; visit_True : 'd -> ('j, 'h) prim_fml
    ; visit_U : 'd -> lbinop
    ; visit_Union : 'd -> rbinop
    ; visit_Univ : 'd -> ('j, 'h) prim_exp
    ; visit_X : 'd -> lunop
    ; visit_binding : 'd -> ('i, 'g) binding -> 'j * ('j, 'h) exp
    ; visit_block : 'd -> ('i, 'g) block -> ('j, 'h) block
    ; visit_comp_op : 'd -> comp_op -> comp_op
    ; visit_disj : 'd -> disj -> disj
    ; visit_exp : 'd -> ('i, 'g) exp -> ('j, 'h) exp
    ; visit_fml : 'd -> ('i, 'g) fml -> ('j, 'h) fml
    ; visit_ibinop : 'd -> ibinop -> ibinop
    ; visit_icomp_op : 'd -> icomp_op -> icomp_op
    ; visit_iexp : 'd -> ('i, 'g) iexp -> ('j, 'h) iexp
    ; visit_iunop : 'd -> iunop -> iunop
    ; visit_lbinop : 'd -> lbinop -> lbinop
    ; visit_lunop : 'd -> lunop -> lunop
    ; visit_prim_exp : 'd -> ('i, 'g) prim_exp -> ('j, 'h) prim_exp
    ; visit_prim_fml : 'd -> ('i, 'g) prim_fml -> ('j, 'h) prim_fml
    ; visit_prim_iexp : 'd -> ('i, 'g) prim_iexp -> ('j, 'h) prim_iexp
    ; visit_quant : 'd -> quant -> quant
    ; visit_rbinop : 'd -> rbinop -> rbinop
    ; visit_rqualify : 'd -> rqualify -> rqualify
    ; visit_runop : 'd -> runop -> runop
    ; visit_sim_binding : 
      'd ->
      ('i, 'g) sim_binding ->
      disj * 'j list * ('j, 'h) exp
    ; visit_t : 'd -> ('i, 'g) t -> ('j, 'h) t.. >

method virtual visit_'i : 'd -> 'g -> 'h

method virtual visit_'v : 'd -> 'i -> 'j

method visit_Add : 'd -> ibinop

method visit_All : 'd -> quant

method visit_And : 'd -> lbinop

method visit_Block : 'd -> ('i, 'g) block -> ('j, 'h) prim_fml

method visit_BoxJoin : 'd ->
  ('i, 'g) exp ->
  ('i, 'g) exp list ->
  ('j, 'h) prim_exp

method visit_Card : 'd -> ('i, 'g) exp -> ('j, 'h) prim_iexp

method visit_Compr : 'd ->
  ('i, 'g) sim_binding list ->
  ('i, 'g) block ->
  ('j, 'h) prim_exp

method visit_Diff : 'd -> rbinop

method visit_F : 'd -> lunop

method visit_FIte : 'd ->
  ('i, 'g) fml ->
  ('i, 'g) fml ->
  ('i, 'g) fml ->
  ('j, 'h) prim_fml

method visit_False : 'd -> ('j, 'h) prim_fml

method visit_G : 'd -> lunop

method visit_Gt : 'd -> icomp_op

method visit_Gte : 'd -> icomp_op

method visit_H : 'd -> lunop

method visit_IBin : 'd ->
  ('i, 'g) iexp ->
  ibinop ->
  ('i, 'g) iexp ->
  ('j, 'h) prim_iexp

method visit_IComp : 'd ->
  ('i, 'g) iexp ->
  icomp_op ->
  ('i, 'g) iexp ->
  ('j, 'h) prim_fml

method visit_IEq : 'd -> icomp_op

method visit_INEq : 'd -> icomp_op

method visit_IUn : 'd -> iunop -> ('i, 'g) iexp -> ('j, 'h) prim_iexp

method visit_Iden : 'd -> ('j, 'h) prim_exp

method visit_Ident : 'd -> 'g -> ('j, 'h) prim_exp

method visit_Iff : 'd -> lbinop

method visit_Imp : 'd -> lbinop

method visit_In : 'd -> comp_op

method visit_Inter : 'd -> rbinop

method visit_Join : 'd -> rbinop

method visit_LBin : 'd ->
  ('i, 'g) fml ->
  lbinop ->
  ('i, 'g) fml ->
  ('j, 'h) prim_fml

method visit_LProj : 'd -> rbinop

method visit_LUn : 'd -> lunop -> ('i, 'g) fml -> ('j, 'h) prim_fml

method visit_Let : 'd ->
  ('i, 'g) binding list ->
  ('i, 'g) block ->
  ('j, 'h) prim_fml

method visit_Lone : 'd -> quant

method visit_Lt : 'd -> icomp_op

method visit_Lte : 'd -> icomp_op

method visit_Neg : 'd -> iunop

method visit_No : 'd -> quant

method visit_None_ : 'd -> ('j, 'h) prim_exp

method visit_Not : 'd -> lunop

method visit_NotIn : 'd -> comp_op

method visit_Num : 'd -> int -> ('j, 'h) prim_iexp

method visit_O : 'd -> lunop

method visit_One : 'd -> quant

method visit_Or : 'd -> lbinop

method visit_Over : 'd -> rbinop

method visit_P : 'd -> lunop

method visit_Prime : 'd -> ('i, 'g) exp -> ('j, 'h) prim_exp

method visit_Prod : 'd -> rbinop

method visit_Qual : 'd -> rqualify -> ('i, 'g) exp -> ('j, 'h) prim_fml

method visit_Quant : 'd ->
  quant ->
  ('i, 'g) sim_binding list ->
  ('i, 'g) block ->
  ('j, 'h) prim_fml

method visit_R : 'd -> lbinop

method visit_RBin : 'd ->
  ('i, 'g) exp ->
  rbinop ->
  ('i, 'g) exp ->
  ('j, 'h) prim_exp

method visit_RComp : 'd ->
  ('i, 'g) exp ->
  comp_op ->
  ('i, 'g) exp ->
  ('j, 'h) prim_fml

method visit_REq : 'd -> comp_op

method visit_RIte : 'd ->
  ('i, 'g) fml ->
  ('i, 'g) exp ->
  ('i, 'g) exp ->
  ('j, 'h) prim_exp

method visit_RLone : 'd -> rqualify

method visit_RNEq : 'd -> comp_op

method visit_RNo : 'd -> rqualify

method visit_ROne : 'd -> rqualify

method visit_RProj : 'd -> rbinop

method visit_RSome : 'd -> rqualify

method visit_RTClos : 'd -> runop

method visit_RUn : 'd -> runop -> ('i, 'g) exp -> ('j, 'h) prim_exp

method visit_Run : 'd -> (('i, 'g) block * bool option) -> ('j, 'h) t

method visit_S : 'd -> lbinop

method visit_Some_ : 'd -> quant

method visit_Sub : 'd -> ibinop

method visit_T : 'd -> lbinop

method visit_TClos : 'd -> runop

method visit_Transpose : 'd -> runop

method visit_True : 'd -> ('j, 'h) prim_fml

method visit_U : 'd -> lbinop

method visit_Union : 'd -> rbinop

method visit_Univ : 'd -> ('j, 'h) prim_exp

method visit_X : 'd -> lunop

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

method visit_binding : 'd -> ('i, 'g) binding -> 'j * ('j, 'h) exp

method visit_block : 'd -> ('i, 'g) block -> ('j, 'h) block

method private visit_bool : 'env. 'env -> disj -> disj

method private visit_bytes : 'env. 'env -> bytes -> bytes

method private visit_char : 'env. 'env -> char -> char

method visit_comp_op : 'd -> comp_op -> comp_op

method visit_disj : 'd -> disj -> disj

method visit_exp : 'd -> ('i, 'g) exp -> ('j, 'h) exp

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

method visit_fml : 'd -> ('i, 'g) fml -> ('j, 'h) fml

method visit_ibinop : 'd -> ibinop -> ibinop

method visit_icomp_op : 'd -> icomp_op -> icomp_op

method visit_iexp : 'd -> ('i, 'g) iexp -> ('j, 'h) 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 : 'd -> iunop -> iunop

method private visit_lazy_t : 'env 'a 'b. ('env -> 'a -> 'b) ->
  'env ->
  'a lazy_t ->
  'b lazy_t

method visit_lbinop : 'd -> lbinop -> lbinop

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

method visit_lunop : 'd -> lunop -> lunop

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

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

method visit_prim_exp : 'd -> ('i, 'g) prim_exp -> ('j, 'h) prim_exp

method visit_prim_fml : 'd -> ('i, 'g) prim_fml -> ('j, 'h) prim_fml

method visit_prim_iexp : 'd -> ('i, 'g) prim_iexp -> ('j, 'h) prim_iexp

method visit_quant : 'd -> quant -> quant

method visit_rbinop : 'd -> 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_rqualify : 'd -> rqualify -> rqualify

method visit_runop : 'd -> runop -> runop

method visit_sim_binding : 'd ->
  ('i, 'g) sim_binding ->
  disj * 'j list * ('j, 'h) exp

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

method visit_t : 'd -> ('i, 'g) t -> ('j, 'h) t

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Gen_goal/class-map/index.html

Class `Gen_goal.map`Source

package electrod

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Gen_goal/class-map/index.html

Class Gen_goal.mapSource

Class `Gen_goal.map`Source