Fixpoint3.Interpreter

Type Aliases

type alias Database[r: Eff] = MutMap[RelSym, BPlusTree[Vector[Boxed], Boxed, Static], r] Source

The IDB or result as it is exposed to the Solver. It maps RelSym to an Index, which uses MutMap instead of a BPlusTree.

def interpret(rc: Region[r], input: (RamProgram[r], Boxing[r])): (Database[r], Predicates) \ r Source

Executes the RamProgram in fst(input) using the Boxing in snd(input).