Queries

After the Fixen solver computes the fixed point, application code needs a way to inspect the results. Queries declare the interface between the generated Fixen module and the surrounding Haskell code, specifying which relations can be queried and which arguments serve as inputs versus outputs.

Queries operate on the solved fact database, i.e., the result of running solve (or reSolve) with initial facts. Initial facts are the input to the solver; query results are the output.

Query Declarations

Queries are declared with the query keyword:

query distTo: DistTo + -

This declares a query named distTo on the DistTo relation. The modes (+ and -) specify that the first argument is an input and the second is an output.

Query Modes

Each argument of a queried relation has a mode:

Mode	Symbol	Meaning
Input	+	The argument is instantiated by the caller (a ground value to match against)
Output	-	The argument is produced by the query (a value to be computed)

The mode determines the type signature of the generated Haskell function. Modes correspond to the argument positions in the relation declaration. For query distTo: DistTo + - where DistTo: Vertex, Dist:

• First argument (Vertex): + = input (caller provides the vertex)
• Second argument (Dist): - = output (solver returns distances)

The generated Haskell function would have the signature:

distanceTo :: Vertex -> Database -> [Fact]

Example: Reachability Queries

query pathsFrom : Path + -
query pathsTo   : Path - +
query allPaths  : Path - -

These generate three Haskell functions:

-- Find all paths starting from a given vertex
pathsFrom :: Vertex -> Database -> [Fact]

-- Find all paths ending at a given vertex
pathsTo :: Vertex -> Database -> [Fact]

-- Retrieve all paths in the database
allPaths :: Database -> [Fact]

Using Queries in Application Code

After compiling a Fixen program, the generated module exports the query functions. Application code uses them to interact with the solved database. An example is shown in the driver module of the graph reachability example.

module Main where

import Reachability

main :: IO ()
main = do
  let edges = [ Edge "Paris" "Tokyo"
              , Edge "Tokyo" "New York" ]
  let solved_database = solve edges
  print (allPaths solved_database)

Queries on Ordered Sorts

The inputs to queries describe the least values of an argument that each result must have. With subsumption, this includes facts whose arguments are larger than the supplied inputs. For example, in shortest paths, given a query reachableIn: DistTo - + and a singular fact DistTo "a" 5 in the database, running the reachableIn query with distance 10 gives DistTo "a" 5 instead of DistTo "a" 10, since DistTo "a" 5 is in the database and subsumes DistTo "a" 10. In other words, queries give the most precise information about the facts in the database.

Queries on Multi-Phase Programs

The examples above all operate on single-phase programs. As shown in the complete example of the reduced product of the interval and parity analyses, on multi-phase programs, the result of fixed-point solving is an interpretation, which is a tuple of fact databases. In multi-phase programs, queries receive an interpretation and a phase selector instead of a database. For instance, on a two-phase setup, the following queries:

query stateBeforeP : StateBeforeP + -
query stateBeforeI : StateBeforeI + -

will generate:

-- Find all parity states with a given label
stateBeforeP :: Label -> Interpretation -> Phase -> [Fact]

-- Find all interval states with a given label
stateBeforeI :: Label -> Interpretation -> Phase -> [Fact]

The Phase datatype is also generated by Fixen. For a two-phase program, the Phase datatype is defined as

data Phase = Phase0 | Phase1 deriving (Eq, Show, Ord)

Summary

• Queries declare how application code can inspect the solved fact database.
• Each query has a name and a list of modes (+ for input, - for output).
• Modes determine the Haskell function signature: input arguments become function parameters.
• Multiple queries can be declared for the same relation with different mode patterns.
• Queries operate on the database/interpretation returned by solve or reSolve.