electrod 1.0.0 · OCaml Package

constraint 'a = stack

inherit Libelectrod.Elo_recursor.recursor

method build_Add : stack -> Ltl.term -> Ltl.term -> Ltl.term

method build_All : stack -> G.quant

method build_And : stack -> ltl -> ltl -> ltl

method build_Block : stack -> ltl list -> ltl

method build_Card : stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Ltl.term

method visit_Compr : stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  Libelectrod.Tuple.t ->
  ltl

method private allocate_sbs_to_tuples : G.exp Containers.List.t ->
  Libelectrod.Tuple.t ->
  Libelectrod.Tuple.t list

method private check_compr_disj : (bool * int * G.exp) list ->
  Libelectrod.Tuple.t list ->
  bool

method build_Compr : stack ->
  (bool * int * Libelectrod.Elo.exp) list ->
  Libelectrod.Elo.fml list ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) list ->
  ltl list ->
  Libelectrod.Tuple.t ->
  ltl

method build_Diff : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_F : stack -> ltl -> ltl

method build_FIte : stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.fml ->
  ltl ->
  ltl ->
  ltl ->
  ltl

method build_False : stack -> ltl

method build_G : stack -> ltl -> ltl

method build_Gt : stack -> Ltl.tcomp

method build_Gte : stack -> Ltl.tcomp

method build_H : stack -> ltl -> ltl

method build_IBin : stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.ibinop ->
  Libelectrod.Elo.iexp ->
  Ltl.term ->
  (Ltl.term -> Ltl.term -> Ltl.term) ->
  Ltl.term ->
  Ltl.term

method build_IComp : stack ->
  Libelectrod.Elo.iexp ->
  Libelectrod.Elo.icomp_op ->
  Libelectrod.Elo.iexp ->
  Ltl.term ->
  Ltl.tcomp ->
  Ltl.term ->
  ltl

method build_IEq : stack -> Ltl.tcomp

method build_INEq : stack -> Ltl.tcomp

method build_IUn : stack ->
  Libelectrod.Elo.iunop ->
  Libelectrod.Elo.iexp ->
  (Ltl.term -> Ltl.term) ->
  Ltl.term ->
  Ltl.term

method build_Iden : stack -> Libelectrod.Tuple.t -> ltl

method build_Iff : stack -> ltl -> ltl -> ltl

method build_Imp : stack -> ltl -> ltl -> ltl

method build_In : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Inter : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Join : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LBin : stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.lbinop ->
  Libelectrod.Elo.fml ->
  ltl ->
  (ltl -> ltl -> ltl) ->
  ltl ->
  ltl

method build_LProj : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_LUn : stack ->
  Libelectrod.Elo.lunop ->
  Libelectrod.Elo.fml ->
  (ltl -> ltl) ->
  ltl ->
  ltl

method build_Lt : stack -> Ltl.tcomp

method build_Lte : stack -> Ltl.tcomp

method build_Name : stack ->
  Libelectrod.Name.t ->
  Libelectrod.Name.t ->
  Libelectrod.Tuple.t ->
  ltl

method build_Neg : stack -> Ltl.term -> Ltl.term

method build_No : stack -> G.quant

method build_None_ : stack -> Libelectrod.Tuple.t -> ltl

method build_Not : stack -> ltl -> ltl

method build_NotIn : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_Num : stack -> int -> int -> Ltl.term

method build_O : stack -> ltl -> ltl

method build_Or : stack -> ltl -> ltl -> ltl

method build_Over : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_P : stack -> ltl -> ltl

method build_Prime : stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Prod : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method visit_Quant : stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  Libelectrod.Elo.fml list ->
  ltl

method build_Quant : stack ->
  Libelectrod.Elo.quant ->
  (bool * int * Libelectrod.Elo.exp) ->
  G.fml list ->
  G.quant ->
  (bool * int * (Libelectrod.Tuple.t -> ltl)) ->
  ltl list ->
  ltl

method build_R : stack -> ltl -> ltl -> ltl

method build_RBin : stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.rbinop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (G.exp ->
    G.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RComp : stack ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.comp_op ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (G.exp ->
    G.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    (Libelectrod.Tuple.t -> ltl) ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_REq : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RIte : stack ->
  Libelectrod.Elo.fml ->
  Libelectrod.Elo.exp ->
  Libelectrod.Elo.exp ->
  ltl ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RNEq : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  ltl

method build_RProj : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RTClos : stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_RUn : stack ->
  Libelectrod.Elo.runop ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Elo.exp ->
    (Libelectrod.Tuple.t -> ltl) ->
    Libelectrod.Tuple.t ->
    ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_S : stack -> ltl -> ltl -> ltl

method build_Some_ : stack -> G.quant

method build_Sub : stack -> Ltl.term -> Ltl.term -> Ltl.term

method build_T : stack -> ltl -> ltl -> ltl

method build_TClos : stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Transpose : stack ->
  Libelectrod.Elo.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_True : stack -> ltl

method build_U : stack -> ltl -> ltl -> ltl

method build_Union : stack ->
  G.exp ->
  G.exp ->
  (Libelectrod.Tuple.t -> ltl) ->
  (Libelectrod.Tuple.t -> ltl) ->
  Libelectrod.Tuple.t ->
  ltl

method build_Univ : stack -> Libelectrod.Tuple.t -> ltl

method build_Var : stack -> int -> int -> Libelectrod.Tuple.t -> ltl

method build_X : stack -> ltl -> ltl

method build_oexp : stack ->
  (Libelectrod.Elo.fml, Libelectrod.Elo.exp, Libelectrod.Elo.iexp)
    Libelectrod.Elo.oexp ->
  (Libelectrod.Tuple.t -> ltl) ->
  int ->
  Libelectrod.Tuple.t ->
  ltl

package electrod