package electrod

  1. Overview
  2. Docs
Formal analysis for the Electrod formal pivot language

Install 

dune-project
 Dependency

grayswandyr.github.io Readme Changelog MPL-2.0 License Edit opam file Versions (10)

Authors

  1. D
    David Chemouil
  2. J
    Julien Brunel

Maintainers

  1. D
    David Chemouil <david.chemouil+git@onera.fr>

Sources

electrod-0.2.3.tbz
sha256=7371c45e28b84a1955d117ef2c798d545febb87c74f596b6efe24965e4b28f31
sha512=e579db68ac05e30b0985f7d90080a82697de18c12e818d48bd7029cea8844571423f08d5881accbf8a0cbeb7df7de9b5b95ff5fe813330a6c92448a0901cdfe7

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 -> 'y ; build_S : 'd -> 'i ; build_Some_ : 'd -> 'h ; build_Sub : 'd -> 'g ; 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 -> 'y ; visit_S : 'd -> 'i ; visit_Some_ : 'd -> 'h ; visit_Sub : 'd -> 'g ; 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_Add : 'd -> 'g
method virtual build_All : 'd -> 'h
method virtual build_And : 'd -> 'i
method virtual build_Block : 'd -> 'j list -> 'k
method virtual build_BoxJoin : 'd -> 'l -> 'l list -> 'm
method virtual build_Card : 'd -> 'l -> 'n
method virtual build_Compr : 'd -> (disj * 'o list * 'l) list -> 'j list -> 'm
method virtual build_Diff : 'd -> 'p
method virtual build_F : 'd -> 'q
method virtual build_FIte : 'd -> 'j -> 'j -> 'j -> 'k
method virtual build_False : 'd -> 'k
method virtual build_G : 'd -> 'q
method virtual build_Gt : 'd -> 'r
method virtual build_Gte : 'd -> 'r
method virtual build_H : 'd -> 'q
method virtual build_IBin : 'd -> 's -> 'g -> 's -> 'n
method virtual build_IComp : 'd -> 's -> 'r -> 's -> 'k
method virtual build_IEq : 'd -> 'r
method virtual build_INEq : 'd -> 'r
method virtual build_IUn : 'd -> 't -> 's -> 'n
method virtual build_Iden : 'd -> 'm
method virtual build_Ident : 'd -> 'u -> 'm
method virtual build_Iff : 'd -> 'i
method virtual build_Imp : 'd -> 'i
method virtual build_In : 'd -> 'v
method virtual build_Inter : 'd -> 'p
method virtual build_Join : 'd -> 'p
method virtual build_LBin : 'd -> 'j -> 'i -> 'j -> 'k
method virtual build_LProj : 'd -> 'p
method virtual build_LUn : 'd -> 'q -> 'j -> 'k
method virtual build_Let : 'd -> ('o * 'l) list -> 'j list -> 'k
method virtual build_Lone : 'd -> 'h
method virtual build_Lt : 'd -> 'r
method virtual build_Lte : 'd -> 'r
method virtual build_Neg : 'd -> 't
method virtual build_No : 'd -> 'h
method virtual build_None_ : 'd -> 'm
method virtual build_Not : 'd -> 'q
method virtual build_NotIn : 'd -> 'v
method virtual build_Num : 'd -> int -> 'n
method virtual build_O : 'd -> 'q
method virtual build_One : 'd -> 'h
method virtual build_Or : 'd -> 'i
method virtual build_Over : 'd -> 'p
method virtual build_P : 'd -> 'q
method virtual build_Prime : 'd -> 'l -> 'm
method virtual build_Prod : 'd -> 'p
method virtual build_Qual : 'd -> 'w -> 'l -> 'k
method virtual build_Quant : 'd -> 'h -> (disj * 'o list * 'l) list -> 'j list -> 'k
method virtual build_R : 'd -> 'i
method virtual build_RBin : 'd -> 'l -> 'p -> 'l -> 'm
method virtual build_RComp : 'd -> 'l -> 'v -> 'l -> 'k
method virtual build_REq : 'd -> 'v
method virtual build_RIte : 'd -> 'j -> 'l -> 'l -> 'm
method virtual build_RLone : 'd -> 'w
method virtual build_RNEq : 'd -> 'v
method virtual build_RNo : 'd -> 'w
method virtual build_ROne : 'd -> 'w
method virtual build_RProj : 'd -> 'p
method virtual build_RSome : 'd -> 'w
method virtual build_RTClos : 'd -> 'x
method virtual build_RUn : 'd -> 'x -> 'l -> 'm
method virtual build_Run : 'd -> 'j list -> 'y
method virtual build_S : 'd -> 'i
method virtual build_Some_ : 'd -> 'h
method virtual build_Sub : 'd -> 'g
method virtual build_TClos : 'd -> 'x
method virtual build_Transpose : 'd -> 'x
method virtual build_True : 'd -> 'k
method virtual build_U : 'd -> 'i
method virtual build_Union : 'd -> 'p
method virtual build_Univ : 'd -> 'm
method virtual build_X : 'd -> 'q
method virtual build_exp : 'd -> 'm -> Libelectrod.Location.t -> int option -> 'l
method virtual build_fml : 'd -> 'k -> Libelectrod.Location.t -> 'j
method virtual build_iexp : 'd -> 'n -> Libelectrod.Location.t -> 's
method virtual visit_'i : 'd -> 'z -> 'u
method virtual visit_'v : 'd -> 'a1 -> 'o
method visit_Add : 'd -> 'g
method visit_All : 'd -> 'h
method visit_And : 'd -> 'i
method visit_Block : 'd -> ('a1, 'z) block -> 'k
method visit_BoxJoin : 'd -> ('a1, 'z) exp -> ('a1, 'z) exp list -> 'm
method visit_Card : 'd -> ('a1, 'z) exp -> 'n
method visit_Compr : 'd -> ('a1, 'z) sim_binding list -> ('a1, 'z) block -> 'm
method visit_Diff : 'd -> 'p
method visit_F : 'd -> 'q
method visit_FIte : 'd -> ('a1, 'z) fml -> ('a1, 'z) fml -> ('a1, 'z) fml -> 'k
method visit_False : 'd -> 'k
method visit_G : 'd -> 'q
method visit_Gt : 'd -> 'r
method visit_Gte : 'd -> 'r
method visit_H : 'd -> 'q
method visit_IBin : 'd -> ('a1, 'z) iexp -> ibinop -> ('a1, 'z) iexp -> 'n
method visit_IComp : 'd -> ('a1, 'z) iexp -> icomp_op -> ('a1, 'z) iexp -> 'k
method visit_IEq : 'd -> 'r
method visit_INEq : 'd -> 'r
method visit_IUn : 'd -> iunop -> ('a1, 'z) iexp -> 'n
method visit_Iden : 'd -> 'm
method visit_Ident : 'd -> 'z -> 'm
method visit_Iff : 'd -> 'i
method visit_Imp : 'd -> 'i
method visit_In : 'd -> 'v
method visit_Inter : 'd -> 'p
method visit_Join : 'd -> 'p
method visit_LBin : 'd -> ('a1, 'z) fml -> lbinop -> ('a1, 'z) fml -> 'k
method visit_LProj : 'd -> 'p
method visit_LUn : 'd -> lunop -> ('a1, 'z) fml -> 'k
method visit_Let : 'd -> ('a1, 'z) binding list -> ('a1, 'z) block -> 'k
method visit_Lone : 'd -> 'h
method visit_Lt : 'd -> 'r
method visit_Lte : 'd -> 'r
method visit_Neg : 'd -> 't
method visit_No : 'd -> 'h
method visit_None_ : 'd -> 'm
method visit_Not : 'd -> 'q
method visit_NotIn : 'd -> 'v
method visit_Num : 'd -> int -> 'n
method visit_O : 'd -> 'q
method visit_One : 'd -> 'h
method visit_Or : 'd -> 'i
method visit_Over : 'd -> 'p
method visit_P : 'd -> 'q
method visit_Prime : 'd -> ('a1, 'z) exp -> 'm
method visit_Prod : 'd -> 'p
method visit_Qual : 'd -> rqualify -> ('a1, 'z) exp -> 'k
method visit_Quant : 'd -> quant -> ('a1, 'z) sim_binding list -> ('a1, 'z) block -> 'k
method visit_R : 'd -> 'i
method visit_RBin : 'd -> ('a1, 'z) exp -> rbinop -> ('a1, 'z) exp -> 'm
method visit_RComp : 'd -> ('a1, 'z) exp -> comp_op -> ('a1, 'z) exp -> 'k
method visit_REq : 'd -> 'v
method visit_RIte : 'd -> ('a1, 'z) fml -> ('a1, 'z) exp -> ('a1, 'z) exp -> 'm
method visit_RLone : 'd -> 'w
method visit_RNEq : 'd -> 'v
method visit_RNo : 'd -> 'w
method visit_ROne : 'd -> 'w
method visit_RProj : 'd -> 'p
method visit_RSome : 'd -> 'w
method visit_RTClos : 'd -> 'x
method visit_RUn : 'd -> runop -> ('a1, 'z) exp -> 'm
method visit_Run : 'd -> ('a1, 'z) block -> 'y
method visit_S : 'd -> 'i
method visit_Some_ : 'd -> 'h
method visit_Sub : 'd -> 'g
method visit_TClos : 'd -> 'x
method visit_Transpose : 'd -> 'x
method visit_True : 'd -> 'k
method visit_U : 'd -> 'i
method visit_Union : 'd -> 'p
method visit_Univ : 'd -> 'm
method visit_X : 'd -> 'q
method private visit_array : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a array -> 'b array
method visit_binding : 'd -> ('a1, 'z) binding -> 'o * 'l
method visit_block : 'd -> ('a1, 'z) block -> 'j list
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 -> 'v
method visit_disj : 'd -> disj -> disj
method visit_exp : 'd -> ('a1, 'z) exp -> 'l
method private visit_float : 'env. 'env -> float -> float
method visit_fml : 'd -> ('a1, 'z) fml -> 'j
method visit_ibinop : 'd -> ibinop -> 'g
method visit_icomp_op : 'd -> icomp_op -> 'r
method visit_iexp : 'd -> ('a1, 'z) iexp -> 's
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 -> 't
method private visit_lazy_t : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a lazy_t -> 'b lazy_t
method visit_lbinop : 'd -> lbinop -> 'i
method private visit_list : 'env 'a 'b. ('env -> 'a -> 'b) -> 'env -> 'a list -> 'b list
method visit_lunop : 'd -> lunop -> 'q
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 -> ('a1, 'z) prim_exp -> 'm
method visit_prim_fml : 'd -> ('a1, 'z) prim_fml -> 'k
method visit_prim_iexp : 'd -> ('a1, 'z) prim_iexp -> 'n
method visit_quant : 'd -> quant -> 'h
method visit_rbinop : 'd -> rbinop -> 'p
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 -> 'w
method visit_runop : 'd -> runop -> 'x
method visit_sim_binding : 'd -> ('a1, 'z) sim_binding -> disj * 'o list * 'l
method private visit_string : 'env. 'env -> string -> string
method visit_t : 'd -> ('a1, 'z) t -> 'y
method private visit_unit : 'env. 'env -> unit -> unit