package electrod

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

Definition of the type for Electrod models.

module G = GenGoal
type var =
  1. | BVar of Var.t
val bound_var : Var.t -> var
val equal_var : var -> var -> bool
type ident =
  1. | Var of Var.t
  2. | Name of Name.t
val var_ident : Var.t -> ident
val name_ident : Name.t -> ident
val var_ident_of_bound_var : var -> ident
val equal_ident : ident -> ident -> bool
type goal = (var, ident) G.t
type t = {
  1. file : string option;
  2. domain : Domain.t;
  3. instance : Instance.t;
  4. sym : Symmetry.t list;
  5. invariants : (var, ident) G.fml list;
  6. goal : goal;
}
val make : string option -> Domain.t -> Instance.t -> Symmetry.t list -> (var, ident) G.fml list -> goal -> t
val pp_var : Format.formatter -> var -> unit
val pp_ident : Format.formatter -> ident -> unit
val pp_goal : Format.formatter -> (var, ident) G.t -> unit
val pp_fml : (var, ident) G.fml Fmtc.t
val pp_prim_fml : Format.formatter -> (var, ident) G.prim_fml -> unit
val pp_exp : Format.formatter -> (var, ident) G.exp -> unit
val pp_prim_exp : Format.formatter -> (var, ident) G.prim_exp -> unit
val pp_iexp : Format.formatter -> (var, ident) G.iexp -> unit
val pp_prim_iexp : Format.formatter -> (var, ident) G.prim_iexp -> unit
val pp_block : Format.formatter -> (var, ident) G.block -> unit
val pp_sim_binding : Format.formatter -> (var, ident) G.sim_binding -> unit
val pp : Format.formatter -> t -> unit
val substitute : < visit_'i : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> ident -> ident ; visit_'v : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> var -> var ; visit_Add : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.ibinop ; visit_All : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant ; visit_And : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_Block : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.block -> (var, ident) G.prim_fml ; visit_BoxJoin : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> (var, ident) G.exp list -> (var, ident) G.prim_exp ; visit_Card : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> (var, ident) G.prim_iexp ; visit_Compr : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.sim_binding list -> (var, ident) G.block -> (var, ident) G.prim_exp ; visit_Diff : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_F : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_FIte : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.fml -> (var, ident) G.fml -> (var, ident) G.fml -> (var, ident) G.prim_fml ; visit_False : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_fml ; visit_G : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_Gt : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_Gte : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_H : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_IBin : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.iexp -> G.ibinop -> (var, ident) G.iexp -> (var, ident) G.prim_iexp ; visit_IComp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.iexp -> G.icomp_op -> (var, ident) G.iexp -> (var, ident) G.prim_fml ; visit_IEq : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_INEq : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_IUn : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.iunop -> (var, ident) G.iexp -> (var, ident) G.prim_iexp ; visit_Iden : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_exp ; visit_Ident : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> ident -> (var, ident) G.prim_exp ; visit_Iff : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_Imp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_In : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.comp_op ; visit_Inter : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_Join : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_LBin : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.fml -> G.lbinop -> (var, ident) G.fml -> (var, ident) G.prim_fml ; visit_LProj : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_LUn : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop -> (var, ident) G.fml -> (var, ident) G.prim_fml ; visit_Let : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.binding list -> (var, ident) G.block -> (var, ident) G.prim_fml ; visit_Lone : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant ; visit_Lt : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_Lte : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op ; visit_Neg : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.iunop ; visit_No : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant ; visit_None_ : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_exp ; visit_Not : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_NotIn : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.comp_op ; visit_Num : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> int -> (var, ident) G.prim_iexp ; visit_O : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_One : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant ; visit_Or : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_Over : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_P : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_Prime : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> (var, ident) G.prim_exp ; visit_Prod : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_Qual : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify -> (var, ident) G.exp -> (var, ident) G.prim_fml ; visit_Quant : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant -> (var, ident) G.sim_binding list -> (var, ident) G.block -> (var, ident) G.prim_fml ; visit_R : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_RBin : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> G.rbinop -> (var, ident) G.exp -> (var, ident) G.prim_exp ; visit_RComp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> G.comp_op -> (var, ident) G.exp -> (var, ident) G.prim_fml ; visit_REq : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.comp_op ; visit_RIte : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.fml -> (var, ident) G.exp -> (var, ident) G.exp -> (var, ident) G.prim_exp ; visit_RLone : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify ; visit_RNEq : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.comp_op ; visit_RNo : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify ; visit_ROne : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify ; visit_RProj : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_RSome : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify ; visit_RTClos : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.runop ; visit_RUn : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.runop -> (var, ident) G.exp -> (var, ident) G.prim_exp ; visit_Run : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.block -> (var, ident) G.t ; visit_S : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_Some_ : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant ; visit_Sub : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.ibinop ; visit_TClos : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.runop ; visit_Transpose : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.runop ; visit_True : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_fml ; visit_U : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop ; visit_Union : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop ; visit_Univ : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_exp ; visit_X : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop ; visit_binding : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.binding -> var * (var, ident) G.exp ; visit_block : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.block -> (var, ident) G.block ; visit_comp_op : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.comp_op -> G.comp_op ; visit_disj : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.disj -> G.disj ; visit_exp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.exp -> (var, ident) G.exp ; visit_fml : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.fml -> (var, ident) G.fml ; visit_ibinop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.ibinop -> G.ibinop ; visit_icomp_op : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.icomp_op -> G.icomp_op ; visit_iexp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.iexp -> (var, ident) G.iexp ; visit_iunop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.iunop -> G.iunop ; visit_lbinop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lbinop -> G.lbinop ; visit_lunop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.lunop -> G.lunop ; visit_prim_exp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_exp -> (var, ident) G.prim_exp ; visit_prim_fml : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_fml -> (var, ident) G.prim_fml ; visit_prim_iexp : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.prim_iexp -> (var, ident) G.prim_iexp ; visit_quant : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.quant -> G.quant ; visit_rbinop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rbinop -> G.rbinop ; visit_rqualify : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.rqualify -> G.rqualify ; visit_runop : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> G.runop -> G.runop ; visit_sim_binding : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.sim_binding -> G.disj * var list * (var, ident) G.exp ; visit_t : (Var.t, (var, ident) G.prim_exp) CCList.Assoc.t -> (var, ident) G.t -> (var, ident) G.t >
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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