Package Description Semantics

Imported from Trac wiki; be wary of outdated information or markup mishaps.

A Semantics for Package Description Files

The following is an attempt to give a semantics to Cabal's package description file. We will construct a function that, given an assignment for all configuration flags in the package and a set of all packages available in the environment returns whether the function is buildable or not.

We start with a slightly abstracted syntax of the package description file, that removes some of the boring details we don't care about here.

A flag assignment consists of a flag name and a boolean value.

flag-assign ::= flag-name := ( "true" | "false" )

A package consists of a package name and a version.

package ::= package-name "-" version

version ::= number ("." number) 

A dependency consists of a package name and a range of possible versions. Ther also is a special value denoting the impossible dependency (this is implemented by specifying "buildable: False").

dependency ::= package-name version-range | "impossible"

version-range ::= "any" 
               | (">" | ">=" | "==" | "<=" | "<" ) version 
               | version-range "&&" version-range
               | version range "||" version-range

A package consists of a sequence of conditional sections. A conditional-section consists of a sequence of field descriptions either denoting package data or dependencies. Additionally, it may contain nested conditional sections. Order does not matter.

package ::= cond-section+

cond-section ::= "if" condition "then"
                     dep-field* data-field* cond-section*  -- non-empty
                 "else"
                     dep-field* data-field* cond-section* 

A condition is a boolean formula possibly containing flag variables (but not more).

condition ::= "true" | "false" | flag-name 
           | "!" condition
           | condition "&&" condition 
           | condition "||" condition

A real package description will contain some global options and library and executable sections, but we can just use "if true ..." to model that in this format.

A dependency field lists a number of dependencies, a data field is describes the final package after flags have been resolved. It is not actually needed, but it is affected by the choice of flags, so we keep it here.

data-field ::= data  -- we don't care about the actual contents here

dep-field ::= dependency+

env ::= flags x packages

-- returns whether the package is buildable and what packages we can choose from
buildable :: env -> package -> ((packages x data) + fail)
buildable env sects = mconcat (map (eval env) (map sectBuildable sects))

sectBuildable :: cond-section -> [(condition x dependency* x data)]
sectBuildable ("if" cond "then" deps1 data1 sects1 "else" deps2 data2 sects2) =
    (cond, deps1, data1) : 
    (!cond, deps1, data1) :
    map (\(c,deps,data) -> (cond /\ c, deps, data)) 
        (map sectBuildable (sects1 ++ sects2))

eval :: env -> (condition x dependency* x data) -> (packages x data) + fail
eval (fs,ps) (cond, deps, data)
  | evalCond fs cond = case evalDeps ps deps of
                         {}  -> fail
                         ps' -> (ps', data)
  | otherwise        = fail

evalCond :: flags -> condition -> bool
evalCond fs c = case c of
  flag -> lookup flag fs
  ... -- usual boolean rules

evalDeps :: packages -> dependency* -> packages + fail
evalDeps ps deps = foldl filterPs ps deps
  where filterPs ps dep = -- if deps removes all possibilities fail
                          -- otherwise filter packages