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
|