Fixpoint3.TypeInfo

This module defines and offers an interface for dealing with the types of the Datalog engine.

A Type is uniquely defined by its UnifiedTypePos which is computed by typeDatalog.

This module has a tight coupling with Compiler since we must assign functional predicates their identifiers in same order. It also has a tight coupling with Lowering, which assumes that a Type is the same as a UnifiedTypePoss.

Type Aliases

type alias RelType = Vector[Type]§ Source

The type of a relation is simply a vector of its types.

type alias Type = UnifiedTypePos§ Source

As far as we are concerned a Type is simply a description of where its boxing/unboxing information is saved.

type alias TypeInformation = Vector[RelType]§ Source

The type of a program is a vector where position i stores the type of the relation with predicate PredSym(_, i).

For functional predicates the vector contains the types of the functional predicates in the same order they are met by the compiler.

Definitions

def expandTypeInfoToProv(typeInfo: TypeInformation, predicates: Predicates): TypeInformation§ Source

Expands typeInfo to include the provenance annotations types.

def expandTypeToProv(relType: RelType): RelType§ Source

Expands relType to include the provenance annotations types.

def getType(id: Int64, index: Int32, typeInfo: TypeInformation): Type§ Source

Returns the type of the index'th value of the relation with predicate PredSym(_, id).

def getTypeOf(id: Int64, typeInfo: TypeInformation): RelType§ Source

Returns the type of the relation with predicate PredSym(_, id).

def provType(): Type§ Source

Returns the type of provenance annotations.

def typeDatalog(d: Datalog, pseudoStratums: PseudoStrataOrder[r], predicates: Predicates, withProv: Bool): TypeInformation \ r

§ Source

Returns the type information of d

For functional predicates the vector returned vector contains the types of the functional predicates in the same order they are met by the compiler.