blob: a8e536fe2c736211d2d746ce74a1c44365e8e88c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
{-# OPTIONS --without-K --safe #-}
module Data.Opaque.List where
import Data.List as L
import Function.Construct.Constant as Const
open import Level using (Level; _⊔_)
open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺)
open import Data.Product using (uncurry′)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Unit.Polymorphic using (⊤)
open import Function using (_⟶ₛ_; Func)
open import Relation.Binary using (Setoid)
open Func
private
variable
a c ℓ : Level
A B : Set a
Aₛ Bₛ : Setoid c ℓ
⊤ₛ : Setoid c ℓ
⊤ₛ = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ }
opaque
List : Set a → Set a
List = L.List
[] : List A
[] = L.[]
_∷_ : A → List A → List A
_∷_ = L._∷_
map : (A → B) → List A → List B
map = L.map
_++_ : List A → List A → List A
_++_ = L._++_
Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ)
Listₛ = PW.setoid
[]ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Listₛ {c} {ℓ} Aₛ
[]ₛ = Const.function ⊤ₛ (Listₛ _) []
∷ₛ : Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ
∷ₛ .to = uncurry′ _∷_
∷ₛ .cong = uncurry′ PW._∷_
mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ
mapₛ f .to = map (to f)
mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys)
++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ
++ₛ .to = uncurry′ _++_
++ₛ .cong = uncurry′ ++⁺
|
