Module `Libelectrod.Gen_goal`Source

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

| Run of ('v, 'i) block

Sourceand ('v, 'i) fml = {

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

}

Sourceand ('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

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

| All
| Some_
| No
| One
| Lone

Sourceand lbinop = private

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

Sourceand lunop = private

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

Sourceand comp_op = private

| In
| NotIn
| REq
| RNEq

Sourceand icomp_op = private

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

Sourceand ('v, 'i) exp = {

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

}

Sourceand ('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

Sourceand rqualify = private

| ROne
| RLone
| RSome
| RNo

Sourceand runop = private

| Transpose
| TClos
| RTClos

Sourceand rbinop = private

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

Sourceand ('v, 'i) iexp = {

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

}

Sourceand ('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

Sourceand iunop = private

| Neg

Sourceand ibinop = private

| Add
| 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

Source

val 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 lt : icomp_op

Sourceval lte : icomp_op

Sourceval gt : 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 -> ('a, 'b) t

Sourceval kwd_styled : 'a Fmtc.t -> 'a Fmtc.t

Source

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

Source

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

Source

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

Source

val 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

Source

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

Source

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

Source

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

Source

val 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

Source

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

Source

val 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Gen_goal/index.html

Module `Libelectrod.Gen_goal`Source

package electrod

Install

Dune Dependency

Authors

Maintainers

Sources

doc/electrod.libelectrod/Libelectrod/Gen_goal/index.html

Module Libelectrod.Gen_goalSource

Module `Libelectrod.Gen_goal`Source