Skip to content

Instantly share code, notes, and snippets.

@peti
Last active November 2, 2017 15:54
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save peti/7a2318dcbba9946862423aea0380859b to your computer and use it in GitHub Desktop.
Save peti/7a2318dcbba9946862423aea0380859b to your computer and use it in GitHub Desktop.
Model the //> operator from https://github.com/NixOS/rfcs/pull/3 in Maude
***(
nix.maude -- experiment with the recursive update operator
The language extension was suggested in https://github.com/NixOS/rfcs/pull/3.
This code lives at https://gist.github.com/peti/7a2318dcbba9946862423aea0380859b.
To evaluate the examples given at the bottom of this code, run the command:
nix-shell -p maude --run "maude -no-banner -batch <nix.maude"
***)
fmod VARIABLE is
sort Variable .
endfm
view Variable from TRIV to VARIABLE is
sort Elt to Variable .
endv
fmod EXPRESSION is
sort Expression .
endfm
view Expression from TRIV to EXPRESSION is
sort Elt to Expression .
endv
fmod NIX is
protecting STRING .
protecting MAP{Variable,Expression} * ( op _|->_ to _=_
, op _,_ to _;_ [prec 121]
) .
sorts Lambda AttrSet .
subsort String Variable Lambda AttrSet < Expression .
op _:_ : Variable Expression -> Lambda .
var AS : AttrSet .
vars M1 M : Map{Variable,Expression} .
var V : Variable .
var E : Expression .
op {} : -> AttrSet .
op {_} : Map{Variable,Expression} -> AttrSet [ctor] .
eq {} = { empty } .
op _//_ : AttrSet AttrSet -> AttrSet [assoc] .
eq AS // { empty } = AS .
eq { M1 } // { V = E ; M } = { insert(V, E, M1) } // {M} .
endfm
fmod RECURSIVE-UPDATE-OPERATOR is
protecting NIX .
vars AS1 AS2 AS : AttrSet .
vars M1 M2 M : Map{Variable,Expression} .
vars V V1 V2 : Variable .
vars E E1 E2 : Expression .
sort RewritePattern .
subsort AttrSet < RewritePattern .
var RWP : RewritePattern .
op _//<_ : AttrSet RewritePattern -> AttrSet .
eq { V = AS ; M } //< { V = RWP } = { V = AS //< RWP ; M } .
eq AS //< { V = E } = AS // { V = E } .
op >:_ : AttrSet -> RewritePattern .
eq AS1 //< >: AS2 = AS2 .
endfm
fmod MAIN is
protecting RECURSIVE-UPDATE-OPERATOR .
ops a b c d e f g h i j k l m n o p q r s t u v w x y z : -> Variable [ctor] .
endfm
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { c = "bar" } == {a = {b = {c = "foo"} ; c = "bar"} ; c = "bar"} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = "bar" } == {a = "bar"} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } // { a = { b = "bar" } } == {a = {b = "bar"}} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = { b = "bar" } } == {a = {b = "bar" ; c = "bar"}} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = { b = { c = "bar" } } } == {a = {b = {c = "bar"} ; c = "bar"}} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = { d = "" } } == {a = {b = {c = "foo"} ; c = "bar" ; d = ""}} .
reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = >: { d = "" } } == {a = {d = ""}} .
*** TODO:
*** reduce ({ foo = a: { a = a; }; } //< { foo = b: { b = >: b + 1; }; }).foo 1 == { a = 1; b = 2; }
*** reduce { a = x: { a = x; }; } //< { a = y: { b = >: y; }; } == { a = z: { a = z; b = z; }; }
*** Examples:
*** reduce { a = { b = { c = "foo" } ; c = "bar" } } //< { a = { b = { c = a : "foo" + a } } } .
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment