Module Libelectrod.Gen_goalSource

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

Sourcetype ('v, 'i) t = private
  1. | Run of ('v, 'i) block * bool option
Sourceand ('v, 'i) fml = {
  1. prim_fml : ('v, 'i) prim_fml;
  2. fml_loc : Location.t;
}
Sourceand ('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
Sourceand ('v, 'i) binding = 'v * ('v, 'i) exp
Sourceand ('v, 'i) sim_binding = disj * 'v list * ('v, 'i) exp
Sourceand disj = bool
Sourceand ('v, 'i) block = ('v, 'i) fml list
Sourceand quant = private
  1. | All
  2. | Some_
  3. | No
  4. | One
  5. | Lone
Sourceand lbinop = private
  1. | And
  2. | Or
  3. | Imp
  4. | Iff
  5. | U
  6. | R
  7. | S
Sourceand lunop = private
  1. | F
  2. | G
  3. | Not
  4. | O
  5. | X
  6. | H
  7. | P
Sourceand comp_op = private
  1. | In
  2. | NotIn
  3. | REq
  4. | RNEq
Sourceand icomp_op = private
  1. | IEq
  2. | INEq
  3. | Lt
  4. | Lte
  5. | Gt
  6. | Gte
Sourceand ('v, 'i) exp = {
  1. prim_exp : ('v, 'i) prim_exp;
  2. exp_loc : Location.t;
  3. arity : int option;
}
Sourceand ('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
Sourceand rqualify = private
  1. | ROne
  2. | RLone
  3. | RSome
  4. | RNo
Sourceand runop = private
  1. | Transpose
  2. | TClos
  3. | RTClos
Sourceand rbinop = private
  1. | Union
  2. | Inter
  3. | Over
  4. | LProj
  5. | RProj
  6. | Prod
  7. | Diff
  8. | Join
Sourceand ('v, 'i) iexp = {
  1. prim_iexp : ('v, 'i) prim_iexp;
  2. iexp_loc : Location.t;
}
Sourceand ('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
Sourceand iunop = private
  1. | Neg
Sourceand ibinop = private
  1. | Add
  2. | Sub
Sourceclass virtual 'c map : object ... end
Sourceclass virtual 'c fold : object ... end
Sourceval true_ : ('a, 'b) prim_fml
Sourceval false_ : ('a, 'b) prim_fml
Sourceval qual : rqualify -> ('a, 'b) exp -> ('a, 'b) prim_fml
Sourceval rcomp : ('a, 'b) exp -> comp_op -> ('a, 'b) exp -> ('a, 'b) prim_fml
Sourceval icomp : ('a, 'b) iexp -> icomp_op -> ('a, 'b) iexp -> ('a, 'b) prim_fml
Sourceval lbinary : ('a, 'b) fml -> lbinop -> ('a, 'b) fml -> ('a, 'b) prim_fml
Sourceval quant : quant -> ('a, 'b) sim_binding list -> ('a, 'b) block -> ('a, 'b) prim_fml
Sourceval lunary : lunop -> ('a, 'b) fml -> ('a, 'b) prim_fml
Sourceval block : ('a, 'b) block -> ('a, 'b) prim_fml
Sourceval fite : ('a, 'b) fml -> ('a, 'b) fml -> ('a, 'b) fml -> ('a, 'b) prim_fml
Sourceval let_ : ('a, 'b) binding list -> ('a, 'b) block -> ('a, 'b) prim_fml
Sourceval all : quant
Sourceval some : quant
Sourceval no_ : quant
Sourceval lone : quant
Sourceval one : quant
Sourceval and_ : lbinop
Sourceval or_ : lbinop
Sourceval impl : lbinop
Sourceval iff : lbinop
Sourceval until : lbinop
Sourceval releases : lbinop
Sourceval since : lbinop
Sourceval not_ : lunop
Sourceval sometime : lunop
Sourceval always : lunop
Sourceval once : lunop
Sourceval next : lunop
Sourceval historically : lunop
Sourceval previous : lunop
Sourceval num : int -> ('a, 'b) prim_iexp
Sourceval none : ('a, 'b) prim_exp
Sourceval univ : ('a, 'b) prim_exp
Sourceval iden : ('a, 'b) prim_exp
Sourceval ident : 'a -> ('b, 'a) prim_exp
Sourceval runary : runop -> ('a, 'b) exp -> ('a, 'b) prim_exp
Sourceval rbinary : ('a, 'b) exp -> rbinop -> ('a, 'b) exp -> ('a, 'b) prim_exp
Sourceval rite : ('a, 'b) fml -> ('a, 'b) exp -> ('a, 'b) exp -> ('a, 'b) prim_exp
Sourceval boxjoin : ('a, 'b) exp -> ('a, 'b) exp list -> ('a, 'b) prim_exp
Sourceval compr : ('a, 'b) sim_binding list -> ('a, 'b) block -> ('a, 'b) prim_exp
Sourceval prime : ('a, 'b) exp -> ('a, 'b) prim_exp
Sourceval in_ : comp_op
Sourceval not_in : comp_op
Sourceval req : comp_op
Sourceval rneq : comp_op
Sourceval ieq : icomp_op
Sourceval ineq : icomp_op
Sourceval lte : icomp_op
Sourceval gte : icomp_op
Sourceval rone : rqualify
Sourceval rsome : rqualify
Sourceval rlone : rqualify
Sourceval rno : rqualify
Sourceval transpose : runop
Sourceval tclos : runop
Sourceval rtclos : runop
Sourceval union : rbinop
Sourceval inter : rbinop
Sourceval over : rbinop
Sourceval lproj : rbinop
Sourceval rproj : rbinop
Sourceval prod : rbinop
Sourceval diff : rbinop
Sourceval join : rbinop
Sourceval card : ('a, 'b) exp -> ('a, 'b) prim_iexp
Sourceval iunary : iunop -> ('a, 'b) iexp -> ('a, 'b) prim_iexp
Sourceval ibinary : ('a, 'b) iexp -> ibinop -> ('a, 'b) iexp -> ('a, 'b) prim_iexp
Sourceval neg : iunop
Sourceval add : ibinop
Sourceval sub : ibinop
Sourceval fml : Location.t -> ('a, 'b) prim_fml -> ('a, 'b) fml
Sourceval exp : int option -> Location.t -> ('a, 'b) prim_exp -> ('a, 'b) exp
Sourceval iexp : Location.t -> ('a, 'b) prim_iexp -> ('a, 'b) iexp
Sourceval run : ('a, 'b) block -> bool option -> ('a, 'b) t
Sourceval get_expected : ('v, 'i) t -> bool option
Sourceval kwd_styled : 'a Fmtc.t -> 'a Fmtc.t
Sourceval pp : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a, 'b) t -> unit
Sourceval pp_fml : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> ('a, 'b) fml Fmtc.t
Sourceval pp_prim_fml : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a, 'b) prim_fml -> unit
Sourceval pp_block : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> ('a, 'b) block Fmtc.t
Sourceval pp_rqualify : Format.formatter -> rqualify -> unit
Sourceval pp_comp_op : Format.formatter -> comp_op -> unit
Sourceval pp_icomp_op : Format.formatter -> icomp_op -> unit
Sourceval pp_lunop : Format.formatter -> lunop -> unit
Sourceval pp_lbinop : Format.formatter -> lbinop -> unit
Sourceval pp_quant : Format.formatter -> quant -> unit
Sourceval pp_binding : sep:unit Fmtc.t -> 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> ('a, 'b) binding Fmtc.t
Sourceval pp_sim_binding : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> ('a, 'b) sim_binding Fmtc.t
Sourceval pp_exp : ?show_arity:disj -> 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> ('a, 'b) exp Fmtc.t
Sourceval pp_prim_exp : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a, 'b) prim_exp -> unit
Sourceval pp_runop : Format.formatter -> runop -> unit
Sourceval pp_rbinop : Format.formatter -> rbinop -> unit
Sourceval pp_iexp : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a, 'b) iexp -> unit
Sourceval pp_prim_iexp : 'a Fmtc.t -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a, 'b) prim_iexp -> unit
Sourceval pp_iunop : Format.formatter -> iunop -> unit
Sourceval pp_ibinop : Format.formatter -> ibinop -> unit