Module Generic.MakeExtractor

This functor MakeExtractor allows users to construct an EGraph extraction procedure for a given LANGUAGE and COST system.

Parameters

Signature

val extract : (Id.t L.shape'a'brw) 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.