Created
January 4, 2023 22:03
-
-
Save necauqua/845c2bd4a4e9c2905ffd7135c22a393e to your computer and use it in GitHub Desktop.
wtf
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
let JSON = | |
https://prelude.dhall-lang.org/JSON/package.dhall | |
sha256:5f98b7722fd13509ef448b075e02b9ff98312ae7a406cf53ed25012dbc9990ac | |
let Expr/Type | |
: Type | |
= ∀(Expr : Type) → | |
∀ ( expr | |
: { ref : Natural → Expr | |
, get : Expr → Natural → Expr | |
, and : Expr → Expr → Expr | |
} | |
) → | |
Expr | |
let exprType = λ(type : Text) → { mapKey = "type", mapValue = JSON.string type } | |
let Expr/toJSON | |
: Expr/Type → JSON.Type | |
= λ(expr : Expr/Type) → | |
expr | |
JSON.Type | |
{ ref = | |
λ(id : Natural) → | |
JSON.object | |
[ exprType "ref" | |
, { mapKey = "id", mapValue = JSON.natural id } | |
] | |
, get = | |
λ(e : JSON.Type) → | |
λ(index : Natural) → | |
JSON.object | |
[ exprType "get" | |
, { mapKey = "expr", mapValue = e } | |
, { mapKey = "index", mapValue = JSON.natural index } | |
] | |
, and = | |
λ(lhs : JSON.Type) → | |
λ(rhs : JSON.Type) → | |
JSON.object | |
[ exprType "and" | |
, { mapKey = "lhs", mapValue = lhs } | |
, { mapKey = "rhs", mapValue = rhs } | |
] | |
} | |
let ref | |
: Natural → Expr/Type | |
= λ(id : Natural) → | |
λ(Expr : Type) → | |
λ ( expr | |
: { ref : Natural → Expr | |
, get : Expr → Natural → Expr | |
, and : Expr → Expr → Expr | |
} | |
) → | |
expr.ref id | |
let get | |
: Expr/Type → Natural → Expr/Type | |
= λ(e : Expr/Type) → | |
λ(index : Natural) → | |
λ(Expr : Type) → | |
λ ( expr | |
: { ref : Natural → Expr | |
, get : Expr → Natural → Expr | |
, and : Expr → Expr → Expr | |
} | |
) → | |
expr.get (e Expr expr) index | |
let and | |
: Expr/Type → Expr/Type → Expr/Type | |
= λ(lhs : Expr/Type) → | |
λ(rhs : Expr/Type) → | |
λ(Expr : Type) → | |
λ ( expr | |
: { ref : Natural → Expr | |
, get : Expr → Natural → Expr | |
, and : Expr → Expr → Expr | |
} | |
) → | |
expr.and (lhs Expr expr) (rhs Expr expr) | |
let items = ref 123 | |
let test = | |
and | |
( and | |
(and (get items 0) (get items 1)) | |
(and (get items 2) (get items 3)) | |
) | |
(and (get items 4) (get items 5)) | |
in JSON.render (Expr/toJSON test) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment