Last active
November 2, 2017 15:54
-
-
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
***( | |
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