electrod

Formal analysis for the Electrod formal pivot language
IN THIS PACKAGE
type ('v, 'i) t = private
| Run of ( 'v, 'i ) block * bool option
and ('v, 'i) fml = {
prim_fml : ( 'v, 'i ) prim_fml;
fml_loc : Location.t;
}
and ('v, 'i) prim_fml = private
| True
| False
| Qual of rqualify * ( 'v, 'i ) exp
| RComp of ( 'v, 'i ) exp * comp_op * ( 'v, 'i ) exp
| IComp of ( 'v, 'i ) iexp * icomp_op * ( 'v, 'i ) iexp
| LUn of lunop * ( 'v, 'i ) fml
| LBin of ( 'v, 'i ) fml * lbinop * ( 'v, 'i ) fml
| Quant of quant * ( 'v, 'i ) sim_binding list * ( 'v, 'i ) block
| Let of ( 'v, 'i ) binding list * ( 'v, 'i ) block
| FIte of ( 'v, 'i ) fml * ( 'v, 'i ) fml * ( 'v, 'i ) fml
| Block of ( 'v, 'i ) block
and ('v, 'i) binding = 'v * ( 'v, 'i ) exp
and ('v, 'i) sim_binding = disj * 'v list * ( 'v, 'i ) exp
and disj = bool
and ('v, 'i) block = ( 'v, 'i ) fml list
and quant = private
| All
| Some_
| No
| One
| Lone
and lbinop = private
| And
| Or
| Imp
| Iff
| U
| R
| S
| T
and lunop = private
| F
| G
| Not
| O
| X
| H
| P
and comp_op = private
| In
| NotIn
| REq
| RNEq
and icomp_op = private
| IEq
| INEq
| Lt
| Lte
| Gt
| Gte
and ('v, 'i) exp = {
prim_exp : ( 'v, 'i ) prim_exp;
exp_loc : Location.t;
arity : int option;
}
and ('v, 'i) prim_exp = private
| None_
| Univ
| Iden
| Ident of 'i
| RUn of runop * ( 'v, 'i ) exp
| RBin of ( 'v, 'i ) exp * rbinop * ( 'v, 'i ) exp
| RIte of ( 'v, 'i ) fml * ( 'v, 'i ) exp * ( 'v, 'i ) exp
| BoxJoin of ( 'v, 'i ) exp * ( 'v, 'i ) exp list
| Compr of ( 'v, 'i ) sim_binding list * ( 'v, 'i ) block
| Prime of ( 'v, 'i ) exp
and rqualify = private
| ROne
| RLone
| RSome
| RNo
and runop = private
| Transpose
| TClos
| RTClos
and rbinop = private
| Union
| Inter
| Over
| LProj
| RProj
| Prod
| Diff
| Join
and ('v, 'i) iexp = {
prim_iexp : ( 'v, 'i ) prim_iexp;
iexp_loc : Location.t;
}
and ('v, 'i) prim_iexp = private
| Num of int
| Card of ( 'v, 'i ) exp
| IUn of iunop * ( 'v, 'i ) iexp
| IBin of ( 'v, 'i ) iexp * ibinop * ( 'v, 'i ) iexp
and iunop = private
| Neg
and ibinop = private
| Add
| Sub
class virtual 'c map : object ... end
class virtual 'c fold : object ... end
val true_ : ( 'a, 'b ) prim_fml
val false_ : ( 'a, 'b ) prim_fml
val qual : rqualify -> ( 'a, 'b ) exp -> ( 'a, 'b ) prim_fml
val rcomp : ( 'a, 'b ) exp -> comp_op -> ( 'a, 'b ) exp -> ( 'a, 'b ) prim_fml
val icomp : ( 'a, 'b ) iexp -> icomp_op -> ( 'a, 'b ) iexp -> ( 'a, 'b ) prim_fml
val lbinary : ( 'a, 'b ) fml -> lbinop -> ( 'a, 'b ) fml -> ( 'a, 'b ) prim_fml
val quant : quant -> ( 'a, 'b ) sim_binding list -> ( 'a, 'b ) block -> ( 'a, 'b ) prim_fml
val lunary : lunop -> ( 'a, 'b ) fml -> ( 'a, 'b ) prim_fml
val block : ( 'a, 'b ) block -> ( 'a, 'b ) prim_fml
val fite : ( 'a, 'b ) fml -> ( 'a, 'b ) fml -> ( 'a, 'b ) fml -> ( 'a, 'b ) prim_fml
val let_ : ( 'a, 'b ) binding list -> ( 'a, 'b ) block -> ( 'a, 'b ) prim_fml
val all : quant
val some : quant
val no_ : quant
val lone : quant
val one : quant
val and_ : lbinop
val or_ : lbinop
val impl : lbinop
val iff : lbinop
val until : lbinop
val releases : lbinop
val triggered : lbinop
val since : lbinop
val not_ : lunop
val eventually : lunop
val always : lunop
val once : lunop
val next : lunop
val historically : lunop
val previous : lunop
val num : int -> ( 'a, 'b ) prim_iexp
val none : ( 'a, 'b ) prim_exp
val univ : ( 'a, 'b ) prim_exp
val iden : ( 'a, 'b ) prim_exp
val ident : 'a -> ( 'b, 'a ) prim_exp
val runary : runop -> ( 'a, 'b ) exp -> ( 'a, 'b ) prim_exp
val rbinary : ( 'a, 'b ) exp -> rbinop -> ( 'a, 'b ) exp -> ( 'a, 'b ) prim_exp
val rite : ( 'a, 'b ) fml -> ( 'a, 'b ) exp -> ( 'a, 'b ) exp -> ( 'a, 'b ) prim_exp
val boxjoin : ( 'a, 'b ) exp -> ( 'a, 'b ) exp list -> ( 'a, 'b ) prim_exp
val compr : ( 'a, 'b ) sim_binding list -> ( 'a, 'b ) block -> ( 'a, 'b ) prim_exp
val prime : ( 'a, 'b ) exp -> ( 'a, 'b ) prim_exp
val in_ : comp_op
val not_in : comp_op
val req : comp_op
val rneq : comp_op
val ieq : icomp_op
val ineq : icomp_op
val lt : icomp_op
val lte : icomp_op
val gt : icomp_op
val gte : icomp_op
val rone : rqualify
val rsome : rqualify
val rlone : rqualify
val rno : rqualify
val transpose : runop
val tclos : runop
val rtclos : runop
val union : rbinop
val inter : rbinop
val over : rbinop
val lproj : rbinop
val rproj : rbinop
val prod : rbinop
val diff : rbinop
val join : rbinop
val card : ( 'a, 'b ) exp -> ( 'a, 'b ) prim_iexp
val iunary : iunop -> ( 'a, 'b ) iexp -> ( 'a, 'b ) prim_iexp
val ibinary : ( 'a, 'b ) iexp -> ibinop -> ( 'a, 'b ) iexp -> ( 'a, 'b ) prim_iexp
val neg : iunop
val add : ibinop
val sub : ibinop
val fml : Location.t -> ( 'a, 'b ) prim_fml -> ( 'a, 'b ) fml
val exp : int option -> Location.t -> ( 'a, 'b ) prim_exp -> ( 'a, 'b ) exp
val iexp : Location.t -> ( 'a, 'b ) prim_iexp -> ( 'a, 'b ) iexp
val run : ( 'a, 'b ) block -> bool option -> ( 'a, 'b ) t
val get_expected : ( 'v, 'i ) t -> bool option
val kwd_styled : 'a Fmtc.t -> 'a Fmtc.t
val pp : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b ) t -> unit
val pp_fml : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> ( 'a, 'b ) fml Fmtc.t
val pp_prim_fml : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b ) prim_fml -> unit
val pp_block : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> ( 'a, 'b ) block Fmtc.t
val pp_rqualify : Format.formatter -> rqualify -> unit
val pp_comp_op : Format.formatter -> comp_op -> unit
val pp_icomp_op : Format.formatter -> icomp_op -> unit
val pp_lunop : Format.formatter -> lunop -> unit
val pp_lbinop : Format.formatter -> lbinop -> unit
val pp_quant : Format.formatter -> quant -> unit
val pp_binding : sep:unit Fmtc.t -> 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> ( 'a, 'b ) binding Fmtc.t
val pp_sim_binding : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> ( 'a, 'b ) sim_binding Fmtc.t
val pp_exp : ?show_arity:disj -> 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> ( 'a, 'b ) exp Fmtc.t
val pp_prim_exp : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b ) prim_exp -> unit
val pp_runop : Format.formatter -> runop -> unit
val pp_rbinop : Format.formatter -> rbinop -> unit
val pp_iexp : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b ) iexp -> unit
val pp_prim_iexp : 'a Fmtc.t -> ( Format.formatter -> 'b -> unit ) -> Format.formatter -> ( 'a, 'b ) prim_iexp -> unit
val pp_iunop : Format.formatter -> iunop -> unit
val pp_ibinop : Format.formatter -> ibinop -> unit