package electrod

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

Install 

dune-project
 Dependency

github.com 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.9.0.tbz
sha256=b2263601350f2ffe3cb1671d8bdd256729986b248c1ec39e84ec76a2f2b8408c
sha512=f4c0e7a196c7a14fff51e7f0cc6f91ed8b3df965523d878ab507320f9771ec69efddb31252ff9763ed2f92bc8c369cea73ca20edebbc3c9ff327fe500f33bdf0

doc/electrod.libelectrod/Libelectrod/Gen_goal_recursor/class-recursor/index.html

Class Gen_goal_recursor.recursorSource

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