electrod 1.0.0 (latest) · OCaml Package

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

| Run of ('v, 'i) block * bool option

and ('v, 'i) fml = {

prim_fml : ('v, 'i) prim_fml;
fml_loc : Location.t;

}

and ('v, 'i) prim_fml = private

| True
| False
| Qual of rqualify * ('v, 'i) exp
| RComp of ('v, 'i) exp * comp_op * ('v, 'i) exp
| IComp of ('v, 'i) iexp * icomp_op * ('v, 'i) iexp
| LUn of lunop * ('v, 'i) fml
| LBin of ('v, 'i) fml * lbinop * ('v, 'i) fml
| Quant of quant * ('v, 'i) sim_binding list * ('v, 'i) block
| Let of ('v, 'i) binding list * ('v, 'i) block
| FIte of ('v, 'i) fml * ('v, 'i) fml * ('v, 'i) fml
| 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

| All
| Some_
| No
| One
| Lone

and lbinop = private

| And
| Or
| Imp
| Iff
| U
| R
| S
| T

and lunop = private

| F
| G
| Not
| O
| X
| H
| P

and comp_op = private

| In
| NotIn
| REq
| RNEq

and icomp_op = private

| IEq
| INEq
| Lt
| Lte
| Gt
| Gte

and ('v, 'i) exp = {

prim_exp : ('v, 'i) prim_exp;
exp_loc : Location.t;
arity : int option;

}

and ('v, 'i) prim_exp = private

| None_
| Univ
| Iden
| Ident of 'i
| RUn of runop * ('v, 'i) exp
| RBin of ('v, 'i) exp * rbinop * ('v, 'i) exp
| RIte of ('v, 'i) fml * ('v, 'i) exp * ('v, 'i) exp
| BoxJoin of ('v, 'i) exp * ('v, 'i) exp list
| Compr of ('v, 'i) sim_binding list * ('v, 'i) block
| Prime of ('v, 'i) exp

and rqualify = private

| ROne
| RLone
| RSome
| RNo

and runop = private

| Transpose
| TClos
| RTClos

and rbinop = private

| Union
| Inter
| Over
| LProj
| RProj
| Prod
| Diff
| Join

and ('v, 'i) iexp = {

prim_iexp : ('v, 'i) prim_iexp;
iexp_loc : Location.t;

}

and ('v, 'i) prim_iexp = private

| Num of int
| Card of ('v, 'i) exp
| IUn of iunop * ('v, 'i) iexp
| IBin of ('v, 'i) iexp * ibinop * ('v, 'i) iexp

and iunop = private

| Neg

and ibinop = private

| Add
| 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 ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'b) t ->
  unit

val pp_fml : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  ('a, 'b) fml Fmtc.t

val pp_prim_fml : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'b) prim_fml ->
  unit

val pp_block : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  ('a, 'b) block Fmtc.t

val pp_rqualify : Stdlib.Format.formatter -> rqualify -> unit

val pp_comp_op : Stdlib.Format.formatter -> comp_op -> unit

val pp_icomp_op : Stdlib.Format.formatter -> icomp_op -> unit

val pp_lunop : Stdlib.Format.formatter -> lunop -> unit

val pp_lbinop : Stdlib.Format.formatter -> lbinop -> unit

val pp_quant : Stdlib.Format.formatter -> quant -> unit

val pp_binding : 
  sep:unit Fmtc.t ->
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  ('a, 'b) binding Fmtc.t

val pp_sim_binding : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  ('a, 'b) sim_binding Fmtc.t

val pp_exp : 
  ?show_arity:disj ->
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  ('a, 'b) exp Fmtc.t

val pp_prim_exp : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'b) prim_exp ->
  unit

val pp_runop : Stdlib.Format.formatter -> runop -> unit

val pp_rbinop : Stdlib.Format.formatter -> rbinop -> unit

val pp_iexp : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'b) iexp ->
  unit

val pp_prim_iexp : 
  'a Fmtc.t ->
  (Stdlib.Format.formatter -> 'b -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'b) prim_iexp ->
  unit

val pp_iunop : Stdlib.Format.formatter -> iunop -> unit

val pp_ibinop : Stdlib.Format.formatter -> ibinop -> unit

package electrod