package electrod
Formal analysis for the Electrod formal pivot language
Install
Dune Dependency
Authors
Maintainers
Sources
electrod-1.0.0.tbz
sha256=4da251e58d97c797d6e940e586d225a09715777fbb1b25c5527a6a2e1e3c2d58
sha512=89c45ebd0d3401b17eac4217289ed21ec87135ab5fa62bf63b2bed1ad1435a381e3434582c2ec99c2e6d8d87ce23cecfa7ba14d76234493992ae06879b808dd2
doc/electrod.libelectrod/Libelectrod/Gen_goal/class-fold/index.html
Class Gen_goal.foldSource
constraint
'c =
< build_Add : 'd -> 'g
; build_All : 'd -> 'h
; build_And : 'd -> 'i
; build_Block : 'd -> 'j list -> 'k
; build_BoxJoin : 'd -> 'l -> 'l list -> 'm
; build_Card : 'd -> 'l -> 'n
; build_Compr : 'd -> (disj * 'o list * 'l) list -> 'j list -> 'm
; build_Diff : 'd -> 'p
; build_F : 'd -> 'q
; build_FIte : 'd -> 'j -> 'j -> 'j -> 'k
; build_False : 'd -> 'k
; build_G : 'd -> 'q
; build_Gt : 'd -> 'r
; build_Gte : 'd -> 'r
; build_H : 'd -> 'q
; build_IBin : 'd -> 's -> 'g -> 's -> 'n
; build_IComp : 'd -> 's -> 'r -> 's -> 'k
; build_IEq : 'd -> 'r
; build_INEq : 'd -> 'r
; build_IUn : 'd -> 't -> 's -> 'n
; build_Iden : 'd -> 'm
; build_Ident : 'd -> 'u -> 'm
; build_Iff : 'd -> 'i
; build_Imp : 'd -> 'i
; build_In : 'd -> 'v
; build_Inter : 'd -> 'p
; build_Join : 'd -> 'p
; build_LBin : 'd -> 'j -> 'i -> 'j -> 'k
; build_LProj : 'd -> 'p
; build_LUn : 'd -> 'q -> 'j -> 'k
; build_Let : 'd -> ('o * 'l) list -> 'j list -> 'k
; build_Lone : 'd -> 'h
; build_Lt : 'd -> 'r
; build_Lte : 'd -> 'r
; build_Neg : 'd -> 't
; build_No : 'd -> 'h
; build_None_ : 'd -> 'm
; build_Not : 'd -> 'q
; build_NotIn : 'd -> 'v
; build_Num : 'd -> int -> 'n
; build_O : 'd -> 'q
; build_One : 'd -> 'h
; build_Or : 'd -> 'i
; build_Over : 'd -> 'p
; build_P : 'd -> 'q
; build_Prime : 'd -> 'l -> 'm
; build_Prod : 'd -> 'p
; build_Qual : 'd -> 'w -> 'l -> 'k
; build_Quant : 'd -> 'h -> (disj * 'o list * 'l) list -> 'j list -> 'k
; build_R : 'd -> 'i
; build_RBin : 'd -> 'l -> 'p -> 'l -> 'm
; build_RComp : 'd -> 'l -> 'v -> 'l -> 'k
; build_REq : 'd -> 'v
; build_RIte : 'd -> 'j -> 'l -> 'l -> 'm
; build_RLone : 'd -> 'w
; build_RNEq : 'd -> 'v
; build_RNo : 'd -> 'w
; build_ROne : 'd -> 'w
; build_RProj : 'd -> 'p
; build_RSome : 'd -> 'w
; build_RTClos : 'd -> 'x
; build_RUn : 'd -> 'x -> 'l -> 'm
; build_Run : 'd -> ('j list * bool option) -> 'y
; build_S : 'd -> 'i
; build_Some_ : 'd -> 'h
; build_Sub : 'd -> 'g
; build_T : 'd -> 'i
; build_TClos : 'd -> 'x
; build_Transpose : 'd -> 'x
; build_True : 'd -> 'k
; build_U : 'd -> 'i
; build_Union : 'd -> 'p
; build_Univ : 'd -> 'm
; build_X : 'd -> 'q
; build_exp : 'd -> 'm -> Libelectrod.Location.t -> int option -> 'l
; build_fml : 'd -> 'k -> Libelectrod.Location.t -> 'j
; build_iexp : 'd -> 'n -> Libelectrod.Location.t -> 's
; visit_'i : 'd -> 'z -> 'u
; visit_'v : 'd -> 'a1 -> 'o
; visit_Add : 'd -> 'g
; visit_All : 'd -> 'h
; visit_And : 'd -> 'i
; visit_Block : 'd -> ('a1, 'z) block -> 'k
; visit_BoxJoin : 'd -> ('a1, 'z) exp -> ('a1, 'z) exp list -> 'm
; visit_Card : 'd -> ('a1, 'z) exp -> 'n
; visit_Compr : 'd -> ('a1, 'z) sim_binding list -> ('a1, 'z) block -> 'm
; visit_Diff : 'd -> 'p
; visit_F : 'd -> 'q
; visit_FIte : 'd -> ('a1, 'z) fml -> ('a1, 'z) fml -> ('a1, 'z) fml -> 'k
; visit_False : 'd -> 'k
; visit_G : 'd -> 'q
; visit_Gt : 'd -> 'r
; visit_Gte : 'd -> 'r
; visit_H : 'd -> 'q
; visit_IBin : 'd -> ('a1, 'z) iexp -> ibinop -> ('a1, 'z) iexp -> 'n
; visit_IComp : 'd -> ('a1, 'z) iexp -> icomp_op -> ('a1, 'z) iexp -> 'k
; visit_IEq : 'd -> 'r
; visit_INEq : 'd -> 'r
; visit_IUn : 'd -> iunop -> ('a1, 'z) iexp -> 'n
; visit_Iden : 'd -> 'm
; visit_Ident : 'd -> 'z -> 'm
; visit_Iff : 'd -> 'i
; visit_Imp : 'd -> 'i
; visit_In : 'd -> 'v
; visit_Inter : 'd -> 'p
; visit_Join : 'd -> 'p
; visit_LBin : 'd -> ('a1, 'z) fml -> lbinop -> ('a1, 'z) fml -> 'k
; visit_LProj : 'd -> 'p
; visit_LUn : 'd -> lunop -> ('a1, 'z) fml -> 'k
; visit_Let : 'd -> ('a1, 'z) binding list -> ('a1, 'z) block -> 'k
; visit_Lone : 'd -> 'h
; visit_Lt : 'd -> 'r
; visit_Lte : 'd -> 'r
; visit_Neg : 'd -> 't
; visit_No : 'd -> 'h
; visit_None_ : 'd -> 'm
; visit_Not : 'd -> 'q
; visit_NotIn : 'd -> 'v
; visit_Num : 'd -> int -> 'n
; visit_O : 'd -> 'q
; visit_One : 'd -> 'h
; visit_Or : 'd -> 'i
; visit_Over : 'd -> 'p
; visit_P : 'd -> 'q
; visit_Prime : 'd -> ('a1, 'z) exp -> 'm
; visit_Prod : 'd -> 'p
; visit_Qual : 'd -> rqualify -> ('a1, 'z) exp -> 'k
; visit_Quant :
'd ->
quant ->
('a1, 'z) sim_binding list ->
('a1, 'z) block ->
'k
; visit_R : 'd -> 'i
; visit_RBin : 'd -> ('a1, 'z) exp -> rbinop -> ('a1, 'z) exp -> 'm
; visit_RComp : 'd -> ('a1, 'z) exp -> comp_op -> ('a1, 'z) exp -> 'k
; visit_REq : 'd -> 'v
; visit_RIte : 'd -> ('a1, 'z) fml -> ('a1, 'z) exp -> ('a1, 'z) exp -> 'm
; visit_RLone : 'd -> 'w
; visit_RNEq : 'd -> 'v
; visit_RNo : 'd -> 'w
; visit_ROne : 'd -> 'w
; visit_RProj : 'd -> 'p
; visit_RSome : 'd -> 'w
; visit_RTClos : 'd -> 'x
; visit_RUn : 'd -> runop -> ('a1, 'z) exp -> 'm
; visit_Run : 'd -> (('a1, 'z) block * bool option) -> 'y
; visit_S : 'd -> 'i
; visit_Some_ : 'd -> 'h
; visit_Sub : 'd -> 'g
; visit_T : 'd -> 'i
; visit_TClos : 'd -> 'x
; visit_Transpose : 'd -> 'x
; visit_True : 'd -> 'k
; visit_U : 'd -> 'i
; visit_Union : 'd -> 'p
; visit_Univ : 'd -> 'm
; visit_X : 'd -> 'q
; visit_binding : 'd -> ('a1, 'z) binding -> 'o * 'l
; visit_block : 'd -> ('a1, 'z) block -> 'j list
; visit_comp_op : 'd -> comp_op -> 'v
; visit_disj : 'd -> disj -> disj
; visit_exp : 'd -> ('a1, 'z) exp -> 'l
; visit_fml : 'd -> ('a1, 'z) fml -> 'j
; visit_ibinop : 'd -> ibinop -> 'g
; visit_icomp_op : 'd -> icomp_op -> 'r
; visit_iexp : 'd -> ('a1, 'z) iexp -> 's
; visit_iunop : 'd -> iunop -> 't
; visit_lbinop : 'd -> lbinop -> 'i
; visit_lunop : 'd -> lunop -> 'q
; visit_prim_exp : 'd -> ('a1, 'z) prim_exp -> 'm
; visit_prim_fml : 'd -> ('a1, 'z) prim_fml -> 'k
; visit_prim_iexp : 'd -> ('a1, 'z) prim_iexp -> 'n
; visit_quant : 'd -> quant -> 'h
; visit_rbinop : 'd -> rbinop -> 'p
; visit_rqualify : 'd -> rqualify -> 'w
; visit_runop : 'd -> runop -> 'x
; visit_sim_binding : 'd -> ('a1, 'z) sim_binding -> disj * 'o list * 'l
; visit_t : 'd -> ('a1, 'z) t -> 'y.. >method virtual build_Compr : 'd -> (disj * 'o list * 'l) list -> 'j list -> 'mmethod virtual build_Quant : 'd ->
'h ->
(disj * 'o list * 'l) list ->
'j list ->
'kmethod virtual build_exp : 'd ->
'm ->
Libelectrod.Location.t ->
int option ->
'lmethod virtual build_fml : 'd -> 'k -> Libelectrod.Location.t -> 'jmethod virtual build_iexp : 'd -> 'n -> Libelectrod.Location.t -> 'smethod visit_Block : 'd -> ('a1, 'z) block -> 'kmethod visit_Card : 'd -> ('a1, 'z) exp -> 'nmethod visit_Compr : 'd -> ('a1, 'z) sim_binding list -> ('a1, 'z) block -> 'mmethod visit_Prime : 'd -> ('a1, 'z) exp -> 'mmethod visit_Quant : 'd ->
quant ->
('a1, 'z) sim_binding list ->
('a1, 'z) block ->
'kmethod visit_Run : 'd -> (('a1, 'z) block * bool option) -> 'ymethod visit_binding : 'd -> ('a1, 'z) binding -> 'o * 'lmethod visit_block : 'd -> ('a1, 'z) block -> 'j listmethod visit_comp_op : 'd -> comp_op -> 'vmethod visit_exp : 'd -> ('a1, 'z) exp -> 'lmethod visit_fml : 'd -> ('a1, 'z) fml -> 'jmethod visit_ibinop : 'd -> ibinop -> 'gmethod visit_icomp_op : 'd -> icomp_op -> 'rmethod visit_iexp : 'd -> ('a1, 'z) iexp -> 'smethod visit_iunop : 'd -> iunop -> 'tmethod visit_lbinop : 'd -> lbinop -> 'imethod visit_lunop : 'd -> lunop -> 'qmethod visit_prim_exp : 'd -> ('a1, 'z) prim_exp -> 'mmethod visit_prim_fml : 'd -> ('a1, 'z) prim_fml -> 'kmethod visit_prim_iexp : 'd -> ('a1, 'z) prim_iexp -> 'nmethod visit_quant : 'd -> quant -> 'hmethod visit_rbinop : 'd -> rbinop -> 'pmethod visit_rqualify : 'd -> rqualify -> 'wmethod visit_runop : 'd -> runop -> 'xmethod visit_sim_binding : 'd -> ('a1, 'z) sim_binding -> disj * 'o list * 'lmethod visit_t : 'd -> ('a1, 'z) t -> 'y