ego
Generic.MakeExtractor
This functor MakeExtractor allows users to construct an EGraph extraction procedure for a given LANGUAGE and COST system.
MakeExtractor
LANGUAGE
COST
module L : LANGUAGE
module E : COST with type node := Id.t L.shape
val extract : (Id.t L.shape, 'a, 'b, rw) egraph -> Id.t -> L.t
extract graph computes an extraction function Id.t -> Sexplib0.Sexp.t to extract concrete terms of the language L from their respective EClasses (specified by Id.t) from the EGraph according to the cost system E.
extract graph
Id.t -> Sexplib0.Sexp.t
L
Id.t
E