The Mirror Library (mirror)

PhaseName

PhaseName(x)

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

Parameters

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

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

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

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

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

list_derived_all[Config]

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

Parameters

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

list_base_all[Config]

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

Parameters

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.

qualifier

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

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

Declaration(x)

The supertype of Front and Back.

Parameters

Entry Points

• dependencies

depends_on_decl

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

Entry Points

• dependencies

code_string

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

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

generated_from(d in Delcaration, src_decl in Declaration)

A declaration d was generated during compilation of declaration src_decl.

Parameters

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

is_recusive(p in Phase, d in Declaration)

Declaration d is recusive at phase p.

Parameters

Entry Points

• dependencies

Front

Front(x)

The supertype of FrontDeclaration and FrontNativeDeclaration.

Parameters

Entry Points

• dependencies

FrontDeclaration

FrontDeclaration(x)

The type check relation for the FrontDeclaration entity.

Parameters

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

FrontNativeDeclaration(x)

The type check relation for the FrontNativeDeclaration entity.

Parameters

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

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

Entry Points

• dependencies

See Also

qualifier.

docstring

docstring(d in FrontDeclaration, s in String)

The documentation string associated with the front declaration d.

Parameters

Entry Points

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

to_string

to_string(d in FrontDeclaration, s in String)

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

Parameters

Entry Points

• dependencies

model_name

model_name(d in FrontDeclaration, s in String)

The name of the model where the declaration is installed.

Parameters

Entry Points

• dependencies

is_native

is_native(d in Declaration)

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

Parameters

Explanation

Currently this is only true for FrontNatieDeclaration.

Entry Points

• dependencies

in_module

in_module(d in FrontDeclartion, m in SourceModule)

A declaration d was declared in the source module m.

Parameters

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

is_inline(d in FrontDeclaration)

The declaration d has the attribute @inline.

Parameters

Entry Points

• dependencies

is_outline

is_outline(d in FrontDeclaration)

The declaration d has the attribute @outline.

Parameters

Entry Points

• dependencies

is_higher_order

is_higher_order(d in Front)

The declaration d has at least one higher order parameter.

Parameters

Entry Points

• dependencies

compiles_to

compiles_to(f in Front, b in Back)

The front declaration d compiles to the back declaration b.

Parameters

Entry Points

• dependencies

Module: range

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

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

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

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

Diagnostic

Diagnostic(x)

The type check relation for the Diagnostic entity.

Parameters

Entry Points

• dependencies

generated_diagnostic

generated_diagnostic(d in FrontDeclaration, dx in Diagnostic)

During compilation of declaration d, diagnostic dx was generated.

Parameters

Entry Points

• dependencies

Module: diagnostic

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

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

Back

Back(x)

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

Parameters

Entry Points

• dependencies

BackDeclaration

BackDeclaration(x)

The type check relation for the BackDeclaration entity.

Parameters

Entry Points

• dependencies

lookup_back_decl

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

Entry Points

• dependencies

See Also

qualifier.

declares

declares(d in Back, r in Relation)

The declaration d declares the relation r.

Parameters

Entry Points

• dependencies

depends_on_relation

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

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

SCC(x)

The type check relation for the SCC entity.

Parameters

Explanation

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

Entry Points

• dependencies

scc

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

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

Parameters

Entry Points

• dependencies

Relation

Relation(x)

The supertype of BaseRelation and DerivedRelation.

Parameters

Entry Points

• dependencies
• list_base_all
• list_derived_all

BaseRelation

BaseRelation(x)

The type check relation for the BaseRelation entity.

Parameters

Explanation

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

Entry Points

• dependencies
• list_base_all

DerivedRelation

DerivedRelation(x)

The type check relation for the BaseRelation entity.

Parameters

Explanation

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

Entry Points

• dependencies
• list_derived_all

lookup_relation

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

Entry Points

• dependencies
• list_base_all
• list_derived_all

See Also

qualifier.

cardinality_estimate

cardinality_estimate(r in Relation, n in Int)

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

Parameters

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

SourceModule(x)

The type check relation for the SourceModule entity.

Parameters

Explanation

An SourceModule corresponds a declared module in the source model.

Entry Points

• dependencies

lookup_module

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

Entry Points

• dependencies

See Also

qualifier.

parent_module

parent_module(m in SourceModule, parent in SourceModule)

The module m is nested direclty inside module parent.

Parameters

Entry Points

• dependencies

docstring

docstring(m in SourceModule, s in String)

The documentation string associated with the source module m.

Parameters

Entry Points

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

Phase

Phase(x)

The type check relation for the Phase entity.

Parameters

Explanation

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

Entry Points

• dependencies
• list_base_all
• list_derived_all

lookup_phase

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

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

Parameters

Entry Points

• dependencies
• list_base_all
• list_derived_all

phase_ordinal

phase_ordinal(p in Phase, n in Int)

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

Parameters

Entry Points

• dependencies
• list_base_all
• list_derived_all