package electrod

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

Install

Dune 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct