electrod 0.1.4 · OCaml Package

constraint 'd = (Var.t, Tuple.t) CCList.Assoc.t

inherit GenGoalRecursor.recursor

method visit_'v : (Var.t * Tuple.t) list -> Elo.var -> Elo.var

method visit_'i : (Var.t * Tuple.t) list -> Elo.ident -> Elo.ident

method build_fml : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Location.t ->
  Ltl.t

method build_Run : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Ltl.t list ->
  Ltl.t list

method build_True : (Var.t * Tuple.t) list -> Ltl.t

method build_False : (Var.t * Tuple.t) list -> Ltl.t

method build_Block : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Ltl.t list ->
  Ltl.t

method build_FIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_Let : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  (Elo.var * (Tuple.t -> Ltl.t)) list ->
  Ltl.t list ->
  Ltl.t

method visit_Quant : (Var.t * Tuple.t) list ->
  GenGoal.quant ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Ltl.t

method build_Quant : (Var.t * Tuple.t) list ->
  G.quant ->
  (Elo.var, Elo.ident) G.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  G.quant ->
  (GenGoal.disj * Elo.var list * (Tuple.t -> Ltl.t)) list ->
  Ltl.t list ->
  Ltl.t

method build_One : (Var.t * Tuple.t) list -> G.quant

method build_Lone : (Var.t * Tuple.t) list -> G.quant

method build_All : (Var.t * Tuple.t) list -> G.quant

method build_No : (Var.t * Tuple.t) list -> G.quant

method build_Some_ : (Var.t * Tuple.t) list -> G.quant

method build_LBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  GenGoal.lbinop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  ((Elo.var, Elo.ident) GenGoal.fml ->
    (Elo.var, Elo.ident) GenGoal.fml ->
    Ltl.t ->
    Ltl.t ->
    Ltl.t) ->
  Ltl.t ->
  Ltl.t

method build_And : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_Iff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_Imp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_U : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_Or : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_R : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_S : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t ->
  Ltl.t

method build_LUn : (Var.t * Tuple.t) list ->
  GenGoal.lunop ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  ((Elo.var, Elo.ident) GenGoal.fml -> Ltl.t -> Ltl.t) ->
  Ltl.t ->
  Ltl.t

method build_X : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_F : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_G : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_H : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_O : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_P : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_Not : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  Ltl.t ->
  Ltl.t

method build_RComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  GenGoal.comp_op ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  ((Elo.var, Elo.ident) G.exp ->
    (Elo.var, Elo.ident) G.exp ->
    (Tuple.t -> Ltl.t) ->
    (Tuple.t -> Ltl.t) ->
    Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_REq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_In : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_NotIn : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_RNEq : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_IComp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.icomp_op ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  Ltl.term ->
  (Ltl.term -> Ltl.term -> Ltl.t) ->
  Ltl.term ->
  Ltl.t

method build_Gt : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_Gte : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_IEq : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_INEq : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_Lt : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_Lte : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.t

method build_Qual : (Var.t * Tuple.t) list ->
  GenGoal.rqualify ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  G.rqualify ->
  (Tuple.t -> Ltl.t) ->
  Ltl.t

method build_RLone : (Var.t * Tuple.t) list -> G.rqualify

method build_RNo : (Var.t * Tuple.t) list -> G.rqualify

method build_ROne : (Var.t * Tuple.t) list -> G.rqualify

method build_RSome : (Var.t * Tuple.t) list -> G.rqualify

method build_exp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  (Tuple.t -> Ltl.t) ->
  Location.t ->
  int option ->
  Tuple.t ->
  Ltl.t

method visit_Compr : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.sim_binding list ->
  (Elo.var, Elo.ident) GenGoal.block ->
  Tuple.t ->
  Ltl.t

method private allocate_sbs_to_tuples : (Var.t * (Elo.var, Elo.ident) G.exp)
                                          Containers.List.t ->
  Atom.t Containers.List.t ->
  Tuple.t list

method build_Compr : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.sim_binding Containers.List.t ->
  (Elo.var, Elo.ident) GenGoal.block ->
  (GenGoal.disj * Elo.var list * (Tuple.t -> Ltl.t)) list ->
  Ltl.t list ->
  Tuple.t ->
  Ltl.t

method build_Iden : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t

method build_BoxJoin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  (Elo.var, Elo.ident) GenGoal.exp list ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) list ->
  Tuple.t ->
  Ltl.t

method build_Ident : (Var.t * Tuple.t) list ->
  Elo.ident ->
  Elo.ident ->
  Tuple.t ->
  Ltl.t

method build_None_ : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t

method build_Univ : (Var.t * Tuple.t) list -> Tuple.t -> Ltl.t

method build_Prime : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_RIte : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.fml ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  (Elo.var, Elo.ident) GenGoal.exp ->
  Ltl.t ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_RBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  GenGoal.rbinop ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  ((Elo.var, Elo.ident) G.exp ->
    (Elo.var, Elo.ident) G.exp ->
    (Tuple.t -> Ltl.t) ->
    (Tuple.t -> Ltl.t) ->
    Tuple.t ->
    Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Union : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Inter : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Join : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_LProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_RProj : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Prod : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Diff : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Over : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_RUn : (Var.t * Tuple.t) list ->
  GenGoal.runop ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  ((Elo.var, Elo.ident) Elo.G.exp -> (Tuple.t -> Ltl.t) -> Tuple.t -> Ltl.t) ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_RTClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_Transpose : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_TClos : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) Elo.G.exp ->
  (Tuple.t -> Ltl.t) ->
  Tuple.t ->
  Ltl.t

method build_iexp : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  Ltl.term ->
  Location.t ->
  Ltl.term

method build_IBin : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  GenGoal.ibinop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  Ltl.term ->
  (Ltl.term -> Ltl.term -> Ltl.term) ->
  Ltl.term ->
  Ltl.term

method build_IUn : (Var.t * Tuple.t) list ->
  GenGoal.iunop ->
  (Elo.var, Elo.ident) GenGoal.iexp ->
  (Ltl.term -> Ltl.term) ->
  Ltl.term ->
  Ltl.term

method build_Num : (Var.t * Tuple.t) list -> int -> int -> Ltl.term

method build_Add : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.term

method build_Neg : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term

method build_Sub : (Var.t * Tuple.t) list -> Ltl.term -> Ltl.term -> Ltl.term

method build_Card : (Var.t * Tuple.t) list ->
  (Elo.var, Elo.ident) G.exp ->
  (Tuple.t -> Ltl.t) ->
  Ltl.term

package electrod