package ego

  1. Overview
  2. Docs

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

Parameters

module L : LANGUAGE
module E : COST with type node := Id.t L.shape

Signature

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.