Fixpoint3.Phase.RenamePredSyms

Purpose of phase: For PredSym(name, id) we want id to be unique, for the whole program. This phase passes over the Datalog-Ast and replaces the id and after everything is done recreates the old PredSyms for the resulting model.

This is necessary as Flix uses the id-part for generating local predicates, not as unique identifiers.

This purpose of this module is to transform PredSyms defined by (name, id), to PredSyms uniquely defined by their id.

Definitions

def assignUniqueIdentifiersToPredSyms(rc: Region[r], d: Datalog): (Datalog, FixInformation) \ r Source

Maps all PredSyms in d to have unique ids. Returns the resulting program and information which renamePredSyms can use to recreate the original program.

This function expects PredSyms to be defined by their (name, id), while afterwards they will be uniquely defined by their id.

def renamePredSyms(d: Datalog, fixing: FixInformation): Datalog Source

Replaces PredSym(name, id) in d with Map.get(id, fixing).