Skip to content

The Mirror Library (mirror)

Collection of mirror Rel definitions.

Module: rel:mirror

View source
rel:mirror

This module contains the entry points to load the Mirror MetaModel.

Each entry point takes a Config relation which specifies what part of the metamodel to load and through what phase. The dependencies and dependencies_all entry points also accept :extra items of :code and :docstring which respectively add the code_string and docstring properties to the returned metamodel.

The returned metamodel is described by the rel:mirror:metamodel_schema relation.

PhaseName

View source
PhaseName(x)

Members of PhaseName are valid phases for use in the rel:mirror entry point relations.

Parameters

ParameterTypeDescription
xAnyAny value to check whether it is of type PhaseName.

Explanation

Mirror returns metamodel information at different phases during the compilation process. Some of the properties of the metamodel only apply for certain phases of compilation. When this is the case, a rel:mirror:metamodel_schema:Phase is taken as a parameter.

The PhaseName members are used as values with the mirror config’s :entry_point key to limit the phase through which information is gathered and returned. Requesting only an early phase means that nearly all metamodel information will already be available to the compiler and less data will be returned, so it is generally faster to run. Requesting a late phase could cause the compiler to need to evaluate parts of the program to generate the metamodel.

The phases are:

  • :syntax_analysis: Shortly after parsing, when names have been resolved.
  • :simplify: After most desugaring has happened.
  • :type_inference: After types have been inferred and applied. Outlining also happens at this phase and the decls generated during outlining are added to the dependency graph.
  • :front: After front compilation. The decls are now in Back IR form.
  • :eval: At the end of compilation. This may trigger evaluation of queried declarations and their dependencies.

dependencies

View source
dependencies[Name, Config]

Return the metamodel containing the dependency graph of relations and declarations with the outer name Name as per the parameters specified in the Config relation.

Parameters

ParameterTypeDescription
NameRelNameA unary relation of names to find the dependency graph of (must be grounded).
ConfigRelationA binary relation of RelName keys and values describing the parameters to use when loading the metamodel (must be grounded).

Explanation

Name must be a arity one relation of RelName, such as {:model; :variables}.

Mirror Config parameters:

  • :phase: The maximum phase (see rel:mirror:PhaseName) to return information on.
  • :extra: :code and :docstring can be passed as extras. This wil add the code_string and docstring properties to the returned metamodel where available.

The default config is {:phase, :front}. This will set the phase to :front if not specified in the passed Config.

Note: Mirror can only fetch the metamodel of the installed model or base relations.

See rel:mirror:metamodel_schema for details on the returned data.

Examples

def metamodel = rel:mirror:dependencies[:add, {:phase, :syntax_analysis; :extra, :docstring}]
 
with metamodel use model_name, lookup_front_decl, depends_on_decl, docstring
 
def m_add = lookup_front_decl["add"]
 
ic { model_name[m_add]  "rel/stdlib" }
ic { depends_on_decl(m_add, lookup_front_decl["rel_primitive_add"])}
 
// list all of the docstrings in this metamodel
def output(q, doc) = docstring(d, doc) and lookup_front_decl(q, d) from d

See Also

Module: rel:mirror:metamodel_schema.

dependencies_all

View source
dependencies_all[Config]

Return the metamodel containing the dependency graph of all relations and declarations in the database as per the parameters specified in the Config relation.

Parameters

ParameterTypeDescription
ConfigRelationA binary relation of RelName keys and values describing the parameters to use when loading the metamodel (must be grounded).

Explanation

Mirror Config parameters:

  • :phase: The maximum phase (see rel:mirror:PhaseName) to return information on.
  • :extra: :code and :docstring can be passed as extras. This wil add the code_string and docstring properties to the returned metamodel where available.

The default config is {:phase, :front}. This will set the phase to :front if not specified in the passed Config.

Note: Mirror can only fetch the metamodel of the installed model or base relations.

See rel:mirror:metamodel_schema for details on the returned data.

Examples

def insert:q = 1; 2; 3.14; "a"
 
def metamodel = rel:mirror:dependencies_all[{:phase, :eval}]
 
with metamodel use lookup_relation, cardinality_estimate
 
def specialization_count = count[lookup_relation["q"]]
// Be careful on the group by, otherwise the Float and String overloads' cardinalities collapse
def total_cardinality = sum[{id, c: cardinality_estimate(id, c) and lookup_relation("q", id)}]
 
ic { specialization_count  3 }
ic { total_cardinality  4 }

See Also

Module: rel:mirror:metamodel_schema.

list_derived_all

View source
list_derived_all[Config]

Return the metamodel containing all of the derived relations in the dependency graph as per the parameters in Config.

Parameters

ParameterTypeDescription
ConfigRelationA binary relation of RelName keys and values describing the parameters to use when loading the metamodel (must be grounded).

Explanation

Mirror Config parameters:

  • :phase: The maximum phase (see rel:mirror:PhaseName) to return information on.

The default config is {:phase, :front}. This will set the phase to :front if not specified in the passed Config.

Note: Mirror can only fetch the metamodel of the installed model or base relations.

See rel:mirror:metamodel_schema for details on the returned data.

Examples

def metamodel = rel:mirror:list_derived_all[{:phase, :eval}]
 
with metamodel use lookup_relation, cardinality_estimate
 
// find all of the derived relations in the `rel` namespace
def rel_rels(x) = exists(y: lookup_relation(y, x) and regex_match("^rel", y))
 
def output:num_rel_rels = count[rel_rels]
def output:total_card_rel_rels = sum[cardinality_estimate[x] for x in rel_rels]

See Also

Module: rel:mirror:metamodel_schema.

list_base_all

View source
list_base_all[Config]

Return the metamodel containing all of the base relations in the dependency graph as per the parameters in Config.

Parameters

ParameterTypeDescription
ConfigRelationA binary relation of RelName keys and values describing the parameters to use when loading the metamodel (must be grounded).

Explanation

Mirror Config parameters:

  • :phase: The maximum phase (see rel:mirror:PhaseName) to return information on.

The default config is {:phase, :front}. This will set the phase to :front if not specified in the passed Config.

Note: Mirror can only fetch the metamodel of the installed model or base relations.

See rel:mirror:metamodel_schema for details on the returned data.

Examples

def metamodel = rel:mirror:list_base_all[{:phase, :eval}]
 
with metamodel use lookup_relation, cardinality_estimate
 
// find all of the base relations in the `rel` namespace
def rel_rels(x) = exists(y: lookup_relation(y, x) and regex_match("^rel", y))
 
def output:num_rel_rels = count[rel_rels]
def output:total_card_rel_rels = sum[cardinality_estimate[x] for x in rel_rels]

See Also

Module: rel:mirror:metamodel_schema.

Module: rel:mirror:metamodel_schema

View source
rel:mirror:metamodel_schema

The schema of the data returned from the rel:mirror entry point relations. This can be used to create a bound declaration on relations containing the metamodel.

Examples

bound metamodel = rel:mirror:metamodel_schema
def metamodel = rel:mirror:dependencies_all[{}]

qualifier

View source
qualifier(item in Hash, q in String)

Relation, Declaration, and SourceModule all have qualifier strings to map the unique identifier to a string displaying the qualifying prefix of the item. The qualifier is the constant RelName prefix of the item.

Parameters

ParameterTypeDescription
itemHashAn identifier for an entity in the metamodel.
qStringA qualifier for an entity in the metamodel.

Explanation

The corrolary to qualifier is lookup_<item> where the lookup is specialized by the type of the item.

Examples

// qualifier = "person:address"
def person:address = "123 Main St"
 
// qualifier = "cube"
@inline
def cube[n] = n^3
 
// qualifier of decl = "outer:inner:decl"
// qualifier of outer module = "outer"
// qualifier of inner module = "outer:inner"
@outline
module outer[R]
    module inner
        def decl = R + 1
    end
end
 
// qualifier = "a:b"
@inline
def a:b[c in Int, :d] = c + 1
 
// qualifier of decl = "insert:name"
// qualifier of resulting base relation = "name"
def insert:name = "jodie"

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

See Also

lookup_back_decl, lookup_front_decl, lookup_module, and lookup_relation.

Declaration

View source
Declaration(x)

The supertype of Front and Back.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

depends_on_decl

View source
depends_on_decl(p in Phase, x in Declaration, y in Declaration)

A declaration x depends directly on another declaration y at the given phase.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase in the metamodel.
xDeclarationAn identifier for a declaration entity in the metamodel.
yDeclarationAn identifier for a declaration entity in the metamodel.

Entry Points

  • dependencies

code_string

View source
code_string(p in Phase, d in Declaration, s in String)

A pretty printed representation of the code of declartion d at phase p.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase in the metamodel.
dDeclarationAn identifier for a declaration entity in the metamodel.
sStringA string representing code at the given phase of compilation.

Explanation

During compilation the code gets lowered to intermediate representations (IR). These IRs are more rudimentary represntations of Rel than in the source code and are not valid Rel.

Entry Points

  • dependencies (with :extra, :code set in Config)

generated_from

View source
generated_from(d in Delcaration, src_decl in Declaration)

A declaration d was generated during compilation of declaration src_decl.

Parameters

ParameterTypeDescription
dDeclarationAn identifier for a declaration entity in the metamodel.
src_declDeclarationAn identifier for a declaration entity in the metamodel.

Explanation

The compiler generates declarations in various situations:

  • Desugaring (e.g. a bound declartion generates an integrity constraint)
  • Outlining
  • Breaking down a declaration into intermediates

Examples

In the following example, the generated declaration for tc[edge] is generated from the original source declaration tc.

@outline
def tc[E] = E; tc[E].E
 
def reachable = tc[edge]

In the following example, the generated declaration for rel:catalog:ic_violation refers to the original soure delcaration ic foo.

def bar = 1; 2; 3
ic foo(x) { bar(x) implies Int(x) }

Entry Points

  • dependencies

is_recursive

View source
is_recusive(p in Phase, d in Declaration)

Declaration d is recusive at phase p.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase in the metamodel.
dDeclarationAn identifier for a declaration entity in the metamodel.

Entry Points

  • dependencies

Front

View source
Front(x)

The supertype of FrontDeclaration and FrontNativeDeclaration.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

FrontDeclaration

View source
FrontDeclaration(x)

The type check relation for the FrontDeclaration entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

A FrontDeclaration corresponds to a user definition in rel source or a declaration that the compiler generated while compiling that source.

The below are examples of declarations:

  • bound data = RelName, FilePos, Int
  • def values = 1; 2; 3
  • ic { exists(data) }

Entry Points

  • dependencies

FrontNativeDeclaration

View source
FrontNativeDeclaration(x)

The type check relation for the FrontNativeDeclaration entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

Some declarations are built into the compiler and do not refer back to a declaration in the installed model.

The below are examples of natives:

  • rel_primitive_add
  • rel_primitive_round_up

Entry Points

  • dependencies

lookup_front_decl

View source
lookup_front_decl(q in String, x in Front)

Lookup a Front identifier by its qualifier string. See rel:mirror:metamodel_schema:qualifier for more information on qualifiers.

Parameters

ParameterTypeDescription
qStringA qualifier for an entity in the metamodel.
xFrontAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

See Also

qualifier.

docstring

View source
docstring(d in FrontDeclaration, s in String)

The documentation string associated with the front declaration d.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
sStringAn string containing documentation on the declaration.

Entry Points

  • dependencies (with :extra, :docstring set in Config)

to_string

View source
to_string(d in FrontDeclaration, s in String)

A compact string representation of a FrontDeclaration (e.g. “rel/stdlib:6641 intersect”).

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
sStringAn string containing a compact representation of the declaration.

Entry Points

  • dependencies

model_name

View source
model_name(d in FrontDeclaration, s in String)

The name of the model where the declaration is installed.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
sStringAn string containing the name of the model where the declaration is installed.

Entry Points

  • dependencies

is_native

View source
is_native(d in Declaration)

If the declaration is a Rel native (e.g. rel_primitive_add).

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.

Explanation

Currently this is only true for FrontNatieDeclaration.

Entry Points

  • dependencies

in_module

View source
in_module(d in FrontDeclartion, m in SourceModule)

A declaration d was declared in the source module m.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
mSourceModuleAn identifier for a module entity in the metamodel.

Explanation

This will point to the innermost module the declaration was nested in. That module will have a pointer to its parent module if nested.

Entry Points

  • dependencies

See Also

parent_module.

is_inline

View source
is_inline(d in FrontDeclaration)

The declaration d has the attribute @inline.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.

Entry Points

  • dependencies

is_outline

View source
is_outline(d in FrontDeclaration)

The declaration d has the attribute @outline.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.

Entry Points

  • dependencies

is_higher_order

View source
is_higher_order(d in Front)

The declaration d has at least one higher order parameter.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.

Entry Points

  • dependencies

compiles_to

View source
compiles_to(f in Front, b in Back)

The front declaration d compiles to the back declaration b.

Parameters

ParameterTypeDescription
fFrontAn identifier for a front entity in the metamodel.
bBackAn identifier for a back entity in the metamodel.

Entry Points

  • dependencies

Module: range

View source

start:line

View source
range:start:line(d in FrontDeclaration, l in Int)

The line in the source code of the model where declaration d begins.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
lIntThe line number in the source code.

Entry Points

  • dependencies

end:line

View source
range:end:line(d in FrontDeclaration, l in Int)

The line in the source code of the model where declaration d ends.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
lIntThe line number in the source code.

Entry Points

  • dependencies

start:character

View source
range:start:character(d in FrontDeclaration, c in Int)

The character in the line of source code of the model where declaration d begins.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
cIntThe character number in the line in the source code.

Entry Points

  • dependencies

end:character

View source
range:end:character(d in FrontDeclaration, c in Int)

The character in the line of source code of the model where declaration d ends.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
cIntThe character number in the line in the source code.

Entry Points

  • dependencies

Diagnostic

View source
Diagnostic(x)

The type check relation for the Diagnostic entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

generated_diagnostic

View source
generated_diagnostic(d in FrontDeclaration, dx in Diagnostic)

During compilation of declaration d, diagnostic dx was generated.

Parameters

ParameterTypeDescription
dFrontDeclarationAn identifier for a front declaration entity in the metamodel.
dxDiagnosticAn identifier for a diagnostic entity in the metamodel.

Entry Points

  • dependencies

Module: diagnostic

View source

severity

View source
diagnostic:severity(dx in Diagnostic, s in String)

The diagnostic dx has severity s.

Parameters

ParameterTypeDescription
dxDiagnosticAn identifier for a diagnostic entity in the metamodel.
sStringThe severity level of the diagnostic.

Explanation

Severity levels:

  • "exception"
  • "error"
  • "warning"

Entry Points

  • dependencies

code

View source
diagnostic:code(dx in Diagnostic, c in String)

The diagnostic dx has code c.

Parameters

ParameterTypeDescription
dxDiagnosticAn identifier for a diagnostic entity in the metamodel.
cStringThe code of the diagnostic.

Explanation

Sample codes:

  • "UNDEFINED_IDENTIFIER"
  • "UNTYPED_VARIABLE"
  • "EXPERIMENTAL"

Entry Points

  • dependencies

Back

View source
Back(x)

The supertype of BackDeclaration. In the future, other back declaration types will be added here.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

BackDeclaration

View source
BackDeclaration(x)

The type check relation for the BackDeclaration entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

lookup_back_decl

View source
lookup_back_decl(q in String, x in Back)

Lookup a Back identifier by its qualifier string. See rel:mirror:metamodel_schema:qualifier for more information on qualifiers.

Parameters

ParameterTypeDescription
qStringA qualifier for an entity in the metamodel.
xBackAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

See Also

qualifier.

declares

View source
declares(d in Back, r in Relation)

The declaration d declares the relation r.

Parameters

ParameterTypeDescription
dBackAn identifier for a back entity in the metamodel.
rRelationAn identifier for a relation entity in the metamodel.

Entry Points

  • dependencies

depends_on_relation

View source
depends_on_relation(p in Phase, d in Declaration, r in Relation)

The declaration d directly depends on the relation r at phase p.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase in the metamodel.
dDeclarationAn identifier for a declaration entity in the metamodel.
rRelationAn identifier for a relation entity in the metamodel.

Explanation

A FrontDeclaration can depend only on BaseRelation and not on DerivedRelation, as derived relations are not yet known to the compiler at this point. BackDeclaration depends on both BaseRelation and DerivedRelation.

Entry Points

  • dependencies

See Also

Phase, Declaration, and Relation.

SCC

View source
SCC(x)

The type check relation for the SCC entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

An SCC is a Strongly Connected Component, which groups together mutually dependent declarations.

Entry Points

  • dependencies

scc

View source
scc(p in Phase, d in Declaration, s in SCC)

The declaration d is in the strongly connected component s at phase p.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase in the metamodel.
dDeclarationAn identifier for a declaration entity in the metamodel.
sSCCAn identifier for an SCC entity in the metamodel.

Entry Points

  • dependencies

Relation

View source
Relation(x)

The supertype of BaseRelation and DerivedRelation.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

BaseRelation

View source
BaseRelation(x)

The type check relation for the BaseRelation entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

A BaseRelation is a relation which is inserted into the database as a fact.

Entry Points

  • dependencies
  • list_base_all

DerivedRelation

View source
DerivedRelation(x)

The type check relation for the BaseRelation entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

A DerviedRelation is a relation which is derived from logic in the database’s model.

Entry Points

  • dependencies
  • list_derived_all

lookup_relation

View source
lookup_relation(q in String, x in Relation)

Lookup a Relation identifier by its qualifier string. See rel:mirror:metamodel_schema:qualifier for more information on qualifiers.

Parameters

ParameterTypeDescription
qStringA qualifier for an entity in the metamodel.
xRelationAn identifier for an entity in the metamodel.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

See Also

qualifier.

cardinality_estimate

View source
cardinality_estimate(r in Relation, n in Int)

The estimate of the how many tuples are in the relation r in the database.

Parameters

ParameterTypeDescription
xRelationAn identifier for an entity in the metamodel.
nIntAn estimate of the number of tuples in the relation.

Explanation

Cardinality estimate is only available at phase :eval and may be missing on relations generated by the compiler.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

SourceModule

View source
SourceModule(x)

The type check relation for the SourceModule entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

An SourceModule corresponds a declared module in the source model.

Entry Points

  • dependencies

lookup_module

View source
lookup_module(q in String, m in SourceModule)

Lookup a SourceModule identifier by its qualifier string. See rel:mirror:metamodel_schema:qualifier for more information on qualifiers.

Parameters

ParameterTypeDescription
qStringA qualifier for an entity in the metamodel.
xSourceModuleAn identifier for an entity in the metamodel.

Entry Points

  • dependencies

See Also

qualifier.

parent_module

View source
parent_module(m in SourceModule, parent in SourceModule)

The module m is nested direclty inside module parent.

Parameters

ParameterTypeDescription
mSourceModuleA qualifier for a module entity in the metamodel.
parentSourceModuleAn identifier for a module entity in the metamodel.

Entry Points

  • dependencies

docstring

View source
docstring(m in SourceModule, s in String)

The documentation string associated with the source module m.

Parameters

ParameterTypeDescription
mSourceModuleAn identifier for a module entity in the metamodel.
sStringAn string containing documentation on the module.

Entry Points

  • dependencies (with :extra, :docstring set in Config)

Phase

View source
Phase(x)

The type check relation for the Phase entity.

Parameters

ParameterTypeDescription
xHashAn identifier for an entity in the metamodel.

Explanation

A Phase is an entity identifier corresponding to a rel:mirror:PhaseName.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

lookup_phase

View source
lookup_phase(name in rel:mirror:PhaseName, p in Phase)

Lookup a Phase identifier by it’s RelName identifier in rel:mirror:PhaseName.

Parameters

ParameterTypeDescription
namerel:mirror:PhaseNameThe name of a mirror phase.
pPhaseAn identifier for a phase entity in the metamodel.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all

phase_ordinal

View source
phase_ordinal(p in Phase, n in Int)

An integer n representing the order of the phase p in the compilation pipeline.

Parameters

ParameterTypeDescription
pPhaseAn identifier for a phase entity in the metamodel.
nIntThe order of the phase during compilation.

Entry Points

  • dependencies
  • list_base_all
  • list_derived_all
Was this doc helpful?