* Improved syntax and semantics for Nix expressions.
This commit is contained in:
parent
2b07b0e7eb
commit
3ec5252582
91
src/eval.hh
91
src/eval.hh
|
@ -10,67 +10,62 @@ extern "C" {
|
||||||
using namespace std;
|
using namespace std;
|
||||||
|
|
||||||
|
|
||||||
/* Abstract syntax of Nix values:
|
/* Abstract syntax of Nix expressions.
|
||||||
|
|
||||||
e := Deref(e) -- external expression
|
An expression describes a (partial) state of the file system in a
|
||||||
| Hash(h) -- value reference
|
referentially transparent way. The operational effect of
|
||||||
| Str(s) -- string constant
|
evaluating an expression is that the state described by the
|
||||||
| Bool(b) -- boolean constant
|
expression is realised.
|
||||||
| Var(x) -- variable
|
|
||||||
| App(e, e) -- application
|
|
||||||
| Lam(x, e) -- lambda abstraction
|
|
||||||
| Exec(platform, e, [Arg(e, e)])
|
|
||||||
-- primitive; execute e with args e* on platform
|
|
||||||
;
|
|
||||||
|
|
||||||
TODO: Deref(e) allows computed external expressions, which might be
|
File : String * Content * [Expr] -> Expr
|
||||||
too expressive; perhaps this should be Deref(h).
|
|
||||||
|
|
||||||
Semantics
|
File(path, content, refs) specifies a file object (its full path
|
||||||
|
and contents), along with all file objects referenced by it (that
|
||||||
|
is, that it has pointers to). We assume that all files are
|
||||||
|
self-referential. This prevents us from having to deal with
|
||||||
|
cycles.
|
||||||
|
|
||||||
Each rule given as eval(e) => e', i.e., expression e has a normal
|
Derive : String * Expr * [Expr] * [String] -> Expr
|
||||||
form e'.
|
|
||||||
|
|
||||||
eval(Deref(Hash(h))) => eval(loadExpr(h))
|
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'.
|
||||||
|
|
||||||
eval(Hash(h)) => Hash(h) # idem for Str, Bool
|
Str : String -> Expr
|
||||||
|
|
||||||
eval(App(e1, e2)) => eval(App(e1', e2))
|
A string constant.
|
||||||
where e1' = eval(e1)
|
|
||||||
|
|
||||||
eval(App(Lam(var, body), arg)) =>
|
Tup : Expr * Expr -> Expr
|
||||||
eval(subst(var, arg, body))
|
|
||||||
|
|
||||||
eval(Exec(platform, prog, args)) => Hash(h)
|
Tuples of expressions.
|
||||||
where
|
|
||||||
fn = ... name of the output (random or by hashing expr) ...
|
|
||||||
h =
|
|
||||||
if exec( fn
|
|
||||||
, eval(platform) => Str(...)
|
|
||||||
, getFile(eval(prog))
|
|
||||||
, map(makeArg . eval, args)
|
|
||||||
) then
|
|
||||||
hashPath(fn)
|
|
||||||
else
|
|
||||||
undef
|
|
||||||
... register ...
|
|
||||||
|
|
||||||
makeArg(Arg(Str(nm), (Hash(h), h))) => (nm, getFile(h))
|
Regular : String -> Content
|
||||||
makeArg(Arg(Str(nm), (Str(s), _))) => (nm, s)
|
Directory : [(String, Content)] -> Content
|
||||||
makeArg(Arg(Str(nm), (Bool(True), _))) => (nm, "1")
|
Hash : String -> Content
|
||||||
makeArg(Arg(Str(nm), (Bool(False), _))) => (nm, undef)
|
|
||||||
|
|
||||||
subst(x, e1, e2) is defined as a generic topdown term
|
File content, given either explicitly or implicitly through a cryptographic hash.
|
||||||
traversal of e2, replacing each `Var(x)' with e1, and not
|
|
||||||
descending into `Lam(x, _)'.
|
|
||||||
|
|
||||||
Note: all stored expressions must be closed. !!! ugly
|
The set of expressions in {\em $f$-normal form} is as follows:
|
||||||
|
|
||||||
|
File : String * Content * [FExpr] -> FExpr
|
||||||
|
|
||||||
|
These are completely evaluated Nix expressions.
|
||||||
|
|
||||||
|
The set of expressions in {\em $d$-normal form} is as follows:
|
||||||
|
|
||||||
|
File : String * Content * [DExpr] -> DExpr
|
||||||
|
Derive : String * DExpr * [Tup] * [String] -> DExpr
|
||||||
|
|
||||||
|
Tup : Str * DExpr -> Tup
|
||||||
|
Tup : Str * Str -> Tup
|
||||||
|
|
||||||
|
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.
|
||||||
|
|
||||||
getFile :: Hash -> FileName
|
|
||||||
loadExpr :: Hash -> FileName
|
|
||||||
hashExpr :: Expr -> Hash
|
|
||||||
hashPath :: FileName -> Hash
|
|
||||||
exec :: FileName -> Platform -> FileName -> [(String, String)] -> Status
|
|
||||||
*/
|
*/
|
||||||
|
|
||||||
typedef ATerm Expr;
|
typedef ATerm Expr;
|
||||||
|
|
Loading…
Reference in a new issue