package electrod

  1. Overview
  2. Docs
package electrod
Legend:
Library
Module
Module type
Parameter
Class
Class type

Implements the type for concrete (Raw) and abstract (Ast) syntax trees, before inference of De Bruijn indices and simplification into Elo trees.

type ('v, 'i) t = private
  1. | Run of ('v, 'i) block * bool option
and ('v, 'i) fml = {
  1. prim_fml : ('v, 'i) prim_fml;
  2. fml_loc : Location.t;
}
and ('v, 'i) prim_fml = private
  1. | True
  2. | False
  3. | Qual of rqualify * ('v, 'i) exp
  4. | RComp of ('v, 'i) exp * comp_op * ('v, 'i) exp
  5. | IComp of ('v, 'i) iexp * icomp_op * ('v, 'i) iexp
  6. | LUn of lunop * ('v, 'i) fml
  7. | LBin of ('v, 'i) fml * lbinop * ('v, 'i) fml
  8. | Quant of quant * ('v, 'i) sim_binding list * ('v, 'i) block
  9. | Let of ('v, 'i) binding list * ('v, 'i) block
  10. | FIte of ('v, 'i) fml * ('v, 'i) fml * ('v, 'i) fml
  11. | 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
  1. | All
  2. | Some_
  3. | No
  4. | One
  5. | Lone
and lbinop = private
  1. | And
  2. | Or
  3. | Imp
  4. | Iff
  5. | U
  6. | R
  7. | S
  8. | T
and lunop = private
  1. | F
  2. | G
  3. | Not
  4. | O
  5. | X
  6. | H
  7. | P
and comp_op = private
  1. | In
  2. | NotIn
  3. | REq
  4. | RNEq
and icomp_op = private
  1. | IEq
  2. | INEq
  3. | Lt
  4. | Lte
  5. | Gt
  6. | Gte
and ('v, 'i) exp = {
  1. prim_exp : ('v, 'i) prim_exp;
  2. exp_loc : Location.t;
  3. arity : int option;
}
and ('v, 'i) prim_exp = private
  1. | None_
  2. | Univ
  3. | Iden
  4. | Ident of 'i
  5. | RUn of runop * ('v, 'i) exp
  6. | RBin of ('v, 'i) exp * rbinop * ('v, 'i) exp
  7. | RIte of ('v, 'i) fml * ('v, 'i) exp * ('v, 'i) exp
  8. | BoxJoin of ('v, 'i) exp * ('v, 'i) exp list
  9. | Compr of ('v, 'i) sim_binding list * ('v, 'i) block
  10. | Prime of ('v, 'i) exp
and rqualify = private
  1. | ROne
  2. | RLone
  3. | RSome
  4. | RNo
and runop = private
  1. | Transpose
  2. | TClos
  3. | RTClos
and rbinop = private
  1. | Union
  2. | Inter
  3. | Over
  4. | LProj
  5. | RProj
  6. | Prod
  7. | Diff
  8. | Join
and ('v, 'i) iexp = {
  1. prim_iexp : ('v, 'i) prim_iexp;
  2. iexp_loc : Location.t;
}
and ('v, 'i) prim_iexp = private
  1. | Num of int
  2. | Card of ('v, 'i) exp
  3. | IUn of iunop * ('v, 'i) iexp
  4. | IBin of ('v, 'i) iexp * ibinop * ('v, 'i) iexp
and iunop = private
  1. | Neg
and ibinop = private
  1. | Add
  2. | 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