blob: 0ab50934c375a1c37d6945d9ad7502ae7278e8ee (
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
|
module CBPV.Context where
open import Data.Bool using (Bool)
open import Data.List using (List; []; _∷_)
open import Data.String using (String)
import Data.String.Properties as String
open import Relation.Binary.Definitions using (DecidableEquality)
open import CBPV.Type
abstract
Name : Set
Name = String
𝔪 : Name
𝔪 = "𝔪"
record GenNamed (A : Set) : Set where
constructor _:-_
field
name : Name
ofType : A
open GenNamed public
Named : Set
Named = GenNamed ValType
infixl 5 _:<_ _++_ _<><_
data GenContext (A : Set) : Set where
[<] : GenContext A
_:<_ : GenContext A → (ex : GenNamed A) → GenContext A
Context : Set
Context = GenContext ValType
map : {A B : Set} → (A → B) → GenContext A → GenContext B
map f [<] = [<]
map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty)
foldr : {A B : Set} → (A → B → B) → B → GenContext A → B
foldr f z [<] = z
foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ
pattern [<_:-_] x A = [<] :< (x :- A)
pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
_++_ : {A : Set} → GenContext A → GenContext A → GenContext A
Γ ++ [<] = Γ
Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A
Γ <>< [] = Γ
Γ <>< (x ∷ xs) = Γ :< x <>< xs
|
