source: Papers/polymorphic-variants-2012/Variants2.agda @ 3454

Last change on this file since 3454 was 2552, checked in by mulligan, 7 years ago

Some different ideas, don't seem to be working out well.

File size: 2.5 KB
Line 
1module Variants2 where
2
3  open import Data.Bool
4  open import Data.Empty
5  open import Data.List hiding ([_])
6  open import Data.Nat
7  open import Data.Product
8  open import Data.Sum
9  open import Data.Unit
10
11  open import Function
12
13  open import Relation.Binary.PropositionalEquality
14
15  module StdLib where
16
17    toSet : Bool  Set
18    toSet true  = ⊤
19    toSet false = ⊥
20
21  module VariantMachinery (α : Set) (τ : Set) (↑_ : α  τ) (_≈_ : τ  τ  Bool) where
22
23    infixr 5 _▸_
24
25    data Variants : Set where
26      [_] : τ  Variants
27      _▸_ : τ  Variants  Variants
28
29    _∈_ : τ  Variants  Bool
30    e ∈ [ y ]    = e ≈ y
31    e ∈ (x ▸ xs) with e ≈ x
32    ... | true  = true
33    ... | false = e ∈ xs
34
35    -- Intuition: valid pattern matches must match at most these tags.
36    [<_] : Variants  Set
37    [< n ] = Σ α (λ x  StdLib.toSet $ (↑ x) ∈ n)
38
39    -- Intuition: valid pattern matches must match at least these tags.
40    [>_] : Variants  Set
41    [> [ y ]  ] = Σ α (λ x  StdLib.toSet $ (↑ x) ≈ y)
42    [> y ▸ ys ] = Σ α (λ x  StdLib.toSet $ (↑ x) ≈ y) ⊎ [> ys ]
43
44  module Test where
45
46    data Size : Set where
47      four    : Size
48      seven   : Size
49      eight   : Size
50      eleven  : Size
51      sixteen : Size
52
53    data Tag : Set where
54      `four    : Tag
55      `seven   : Tag
56      `eight   : Tag
57      `eleven  : Tag
58      `sixteen : Tag
59
60    _≈_ : Tag  Tag  Bool
61    `four    ≈ `four    = true
62    `four    ≈ _        = false
63    `seven   ≈ `seven   = true
64    `seven   ≈ _        = false
65    `eight   ≈ `eight   = true
66    `eight   ≈ _        = false
67    `eleven  ≈ `eleven  = true
68    `eleven  ≈ _        = false
69    `sixteen ≈ `sixteen = true
70    `sixteen ≈ _        = false
71
72     : Size  Tag
73    ↑ four    = `four
74    ↑ seven   = `seven
75    ↑ eight   = `eight
76    ↑ eleven  = `eleven
77    ↑ sixteen = `sixteen
78
79    open VariantMachinery Size Tag ↑ _≈_
80
81    Bit : Set
82    Bit = Bool
83
84    private
85
86      postulate
87        assertFalse : {α : Set}  α
88
89      Vect : Set  Set
90      Vect α = List Bit
91
92    Sizes : Set
93    Sizes = [< `four ▸ `seven ▸ `eight ▸ `eleven ▸ [ `sixteen ] ]
94
95    Nibble : Set
96    Nibble = Vect [< [ `four ] ]
97
98    toNibble : Bool  Bool  Bool  Bool  Nibble
99    toNibble b1 b2 b3 b4 = b1 ∷ b2 ∷ b3 ∷ b4 ∷ []
100
101    fromNibble : Nibble  (Bool × Bool × Bool × Bool)
102    fromNibble (b1 ∷ b2 ∷ b3 ∷ b4 ∷ []) = (b1 , b2 , b3 , b4)
103    fromNibble _                        = assertFalse
104
105   
Note: See TracBrowser for help on using the repository browser.