41 lines
950 B
Plaintext
41 lines
950 B
Plaintext
{-|
|
|
Create a Preserves dictionary value from a Dhall `Map`
|
|
|
|
See ./render.dhall for an example.
|
|
-}
|
|
let Prelude = ./Prelude.dhall
|
|
|
|
let List/map = Prelude.List.map
|
|
|
|
let Preserves = ./Type.dhall
|
|
|
|
let Preserves/dictionary = ./dictionary.dhall
|
|
|
|
let dictionaryOf
|
|
: ∀(a : Type) →
|
|
(a → Preserves) →
|
|
∀(b : Type) →
|
|
(b → Preserves) →
|
|
Prelude.Map.Type a b →
|
|
Preserves
|
|
= λ(a : Type) →
|
|
λ(key : a → Preserves) →
|
|
λ(b : Type) →
|
|
λ(value : b → Preserves) →
|
|
λ(x : Prelude.Map.Type a b) →
|
|
let ab = Prelude.Map.Entry a b
|
|
|
|
let pp = Prelude.Map.Entry Preserves Preserves
|
|
|
|
in Preserves/dictionary
|
|
( List/map
|
|
ab
|
|
pp
|
|
( λ(x : ab) →
|
|
{ mapKey = key x.mapKey, mapValue = value x.mapValue }
|
|
)
|
|
x
|
|
)
|
|
|
|
in dictionaryOf
|