* Normalisation.
This commit is contained in:
parent
3ec5252582
commit
d4c3edfaba
3 changed files with 233 additions and 46 deletions
71
src/eval.hh
71
src/eval.hh
|
|
@ -10,14 +10,14 @@ extern "C" {
|
|||
using namespace std;
|
||||
|
||||
|
||||
/* Abstract syntax of Nix expressions.
|
||||
/* \section{Abstract syntax of Nix expressions}
|
||||
|
||||
An expression describes a (partial) state of the file system in a
|
||||
referentially transparent way. The operational effect of
|
||||
evaluating an expression is that the state described by the
|
||||
expression is realised.
|
||||
|
||||
File : String * Content * [Expr] -> Expr
|
||||
File : Path * Content * [Expr] -> Expr
|
||||
|
||||
File(path, content, refs) specifies a file object (its full path
|
||||
and contents), along with all file objects referenced by it (that
|
||||
|
|
@ -25,12 +25,13 @@ using namespace std;
|
|||
self-referential. This prevents us from having to deal with
|
||||
cycles.
|
||||
|
||||
Derive : String * Expr * [Expr] * [String] -> Expr
|
||||
Derive : String * Path * [Expr] * [Expr] * [Expr] -> Expr
|
||||
|
||||
Derive(platform, builder, ins, outs) specifies the creation of new
|
||||
file objects (in paths declared by `outs') by the execution of a
|
||||
program `builder' on a platform `platform'. This execution takes
|
||||
place in a file system state and in an environment given by `ins'.
|
||||
Derive(platform, builder, ins, outs, env) specifies the creation of
|
||||
new file objects (in paths declared by `outs') by the execution of
|
||||
a program `builder' on a platform `platform'. This execution takes
|
||||
place in a file system state given by `ins'. `env' specifies a
|
||||
mapping of strings to strings.
|
||||
|
||||
Str : String -> Expr
|
||||
|
||||
|
|
@ -40,39 +41,73 @@ using namespace std;
|
|||
|
||||
Tuples of expressions.
|
||||
|
||||
Regular : String -> Content
|
||||
Directory : [(String, Content)] -> Content
|
||||
Hash : String -> Content
|
||||
[ !!! NOT IMPLEMENTED
|
||||
Regular : String -> Content
|
||||
Directory : [(String, Content)] -> Content
|
||||
(this complicates unambiguous normalisation)
|
||||
]
|
||||
CHash : Hash -> Content
|
||||
|
||||
File content, given either explicitly or implicitly through a cryptographic hash.
|
||||
File content, given either in situ, or through an external reference
|
||||
to the file system or url-space decorated with a hash to preserve purity.
|
||||
|
||||
The set of expressions in {\em $f$-normal form} is as follows:
|
||||
DISCUSSION: the idea is that a Regular/Directory is interchangeable
|
||||
with its CHash. This would appear to break referential
|
||||
transparency, e.g., Derive(..., ..., [...CHash(h)...], ...) can
|
||||
only be reduced in a context were the Regular/Directory equivalent
|
||||
of Hash(h) is known. However, CHash should be viewed strictly as a
|
||||
shorthand; that is, when we export an expression containing a
|
||||
CHash, we should also export the file object referenced by that
|
||||
CHash.
|
||||
|
||||
File : String * Content * [FExpr] -> FExpr
|
||||
|
||||
These are completely evaluated Nix expressions.
|
||||
\section{Reduction rules}
|
||||
|
||||
The set of expressions in {\em $d$-normal form} is as follows:
|
||||
...
|
||||
|
||||
|
||||
\section{Normals forms}
|
||||
|
||||
An expression is in {\em weak head normal form} if it is a lambda,
|
||||
a string or boolean value, or a File or Derive value.
|
||||
|
||||
An expression is in {\em $d$-normal form} if it matches the
|
||||
signature FExpr:
|
||||
|
||||
File : String * Content * [DExpr] -> DExpr
|
||||
Derive : String * DExpr * [Tup] * [String] -> DExpr
|
||||
Derive : String * Path * [Tup] * [Tup2] -> DExpr
|
||||
|
||||
Tup : Str * DExpr -> Tup
|
||||
Tup : Str * Str -> Tup
|
||||
|
||||
Tup : Str * Str -> Tup2
|
||||
|
||||
Str : String -> Str
|
||||
|
||||
These are Nix expressions in which the file system result of Derive
|
||||
expressions has not yet been computed. This is useful for, e.g.,
|
||||
querying dependencies.
|
||||
|
||||
An expression is in {\em $f$-normal form} if it matches the
|
||||
signature FExpr:
|
||||
|
||||
File : String * Content * [FExpr] -> FExpr
|
||||
|
||||
These are completely evaluated Nix expressions.
|
||||
|
||||
*/
|
||||
|
||||
typedef ATerm Expr;
|
||||
typedef ATerm Content;
|
||||
|
||||
|
||||
/* Evaluate an expression. */
|
||||
Expr evalValue(Expr e);
|
||||
/* Expression normalisation. */
|
||||
Expr whNormalise(Expr e);
|
||||
Expr dNormalise(Expr e);
|
||||
Expr fNormalise(Expr e);
|
||||
|
||||
/* Realise a $f$-normalised expression in the file system. */
|
||||
void realise(Expr e);
|
||||
|
||||
/* Return a canonical textual representation of an expression. */
|
||||
string printExpr(Expr e);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue