Changeset 2544
- Timestamp:
- Dec 7, 2012, 5:52:23 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/Variants.agda
r2542 r2544 4 4 open import Data.Empty 5 5 open import Data.List 6 open import Data.Nat 7 open import Data.Unit 6 open import Data.Nat hiding (_≟_) 7 open import Data.Sum 8 open import Data.Unit hiding (_≟_) 8 9 9 10 open import Function 10 11 11 open import Relation.Binary.PropositionalEquality 12 open import Relation.Nullary 13 open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉) 12 14 13 15 -- The following is ported from `test.ma'. … … 18 20 _⊗_ : Expression α → Expression α → Expression α 19 21 20 data Tag : Set where 21 literal : Tag 22 plus : Tag 23 times : Tag 22 module MissingStandardLibrary where 24 23 25 _≈_ : Tag → Tag → Bool 26 literal ≈ literal = true 27 plus ≈ plus = true 28 times ≈ times = true 29 _ ≈ _ = false 24 toSet : Bool → Set 25 toSet true = ⊤ 26 toSet false = ⊥ 30 27 31 toTag : {α : Set} → Expression α → Tag 32 toTag (↑ _) = literal 33 toTag (_ ⊕ _) = plus 34 toTag (_ ⊗ _) = times 28 not-not-elim : (b : Bool) → not (not b) ≡ b 29 not-not-elim true = refl 30 not-not-elim false = refl 35 31 36 [_holds-for_] : {α : Set} → (Expression α → Set) → Tag → Set 37 [ Q holds-for literal ] = (n : ℕ) → Q $ ↑ n 38 [ Q holds-for plus ] = (x y : _) → Q $ x ⊕ y 39 [ Q holds-for times ] = (x y : _) → Q $ x ⊗ y 32 not-self-adjoint₁ : (b c : Bool) → not b ≡ c → b ≡ not c 33 not-self-adjoint₁ true true () 34 not-self-adjoint₁ true false not-b≡c = refl 35 not-self-adjoint₁ false true not-b≡c = refl 36 not-self-adjoint₁ false false () 40 37 41 holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → 42 [ Q holds-for (toTag x) ] → Q x 43 holds-for-tag-specialise Q (↑ n) Q-holds-for-toTag = Q-holds-for-toTag n 44 holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y 45 holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y 38 not-self-adjoint₂ : (b c : Bool) → b ≡ not c → not b ≡ c 39 not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c 46 40 47 -- The following is ported from `variants.ma'. 41 _≈_ : Bool → Bool → Bool 42 true ≈ c = c 43 false ≈ c = not c 48 44 49 toSet : Bool → Set50 toSet true = ⊤51 toSet false = ⊥45 ≈-reflexive : (b : Bool) → b ≈ b ≡ true 46 ≈-reflexive true = refl 47 ≈-reflexive false = refl 52 48 53 _∈_ : {α : Set} → Expression α → List Tag → Bool 54 tag ∈ [] = false 55 tag ∈ (x ∷ xs) = (toTag tag ≈ x) ∨ (tag ∈ xs) 49 ≈-true₁ : (b c : Bool) → b ≈ c ≡ true → b ≡ c 50 ≈-true₁ true true b≈c-true = refl 51 ≈-true₁ true false () 52 ≈-true₁ false true b≈c-true = b≈c-true 53 ≈-true₁ false false b≈c-true = refl 56 54 57 record Subexpression (α : Set) (l : List Tag) : Set where 58 field 59 element : Expression α 60 ∈-element : toSet $ element ∈ l 55 ≈-true₂ : (b c : Bool) → b ≡ c → b ≈ c ≡ true 56 ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c 61 57 62 -- Ack! We have no coercions in Agda. 63 ofQ : {α : Set} → (l : List Tag) → (Q : Subexpression α l → Set) → Expression α → Set 64 ofQ l s e = ? 58 -- Tags, and their equality 59 module Tag where 60 61 data Tag : Set where 62 literal : Tag 63 plus : Tag 64 times : Tag 65 66 _≈_ : Tag → Tag → Bool 67 literal ≈ literal = true 68 plus ≈ plus = true 69 times ≈ times = true 70 _ ≈ _ = false 71 72 _≉_ : Tag → Tag → Bool 73 l ≉ r = not $ l ≈ r 74 75 ≈-≉-dual : (l r : Tag) → l ≈ r ≡ not (l ≉ r) 76 ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl 77 78 ≈-reflexive : (l : Tag) → l ≈ l ≡ true 79 ≈-reflexive literal = refl 80 ≈-reflexive plus = refl 81 ≈-reflexive times = refl 82 83 ≈-true₁ : (l r : Tag) → l ≈ r ≡ true → l ≡ r 84 ≈-true₁ literal literal l≈r-true = refl 85 ≈-true₁ literal plus () 86 ≈-true₁ literal times () 87 ≈-true₁ plus literal () 88 ≈-true₁ plus plus l≈r-true = refl 89 ≈-true₁ plus times () 90 ≈-true₁ times literal () 91 ≈-true₁ times plus () 92 ≈-true₁ times times l≈r-true = refl 93 94 ≈-true₂ : (l r : Tag) → l ≡ r → l ≈ r ≡ true 95 ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r 96 97 ≉-true₁ : (l r : Tag) → l ≉ r ≡ true → l ≢ r 98 ≉-true₁ literal literal () 99 ≉-true₁ literal plus l≉r-true = λ () 100 ≉-true₁ literal times l≉r-true = λ () 101 ≉-true₁ plus literal l≉r-true = λ () 102 ≉-true₁ plus plus () 103 ≉-true₁ plus times l≉r-true = λ () 104 ≉-true₁ times literal l≉r-true = λ () 105 ≉-true₁ times plus l≉r-true = λ () 106 ≉-true₁ times times () 107 108 ≉-true₂ : (l r : Tag) → l ≢ r → l ≉ r ≡ true 109 ≉-true₂ literal literal l≢r = ⊥-elim $ l≢r refl 110 ≉-true₂ literal plus l≢r = refl 111 ≉-true₂ literal times l≢r = refl 112 ≉-true₂ plus literal l≢r = refl 113 ≉-true₂ plus plus l≢r = ⊥-elim $ l≢r refl 114 ≉-true₂ plus times l≢r = refl 115 ≉-true₂ times literal l≢r = refl 116 ≉-true₂ times plus l≢r = refl 117 ≉-true₂ times times l≢r = ⊥-elim $ l≢r refl 118 119 ≈-≉-decidable : (l r : Tag) → l ≈ r ≡ true ⊎ l ≉ r ≡ true 120 ≈-≉-decidable literal literal = inj₁ refl 121 ≈-≉-decidable literal plus = inj₂ refl 122 ≈-≉-decidable literal times = inj₂ refl 123 ≈-≉-decidable plus literal = inj₂ refl 124 ≈-≉-decidable plus plus = inj₁ refl 125 ≈-≉-decidable plus times = inj₂ refl 126 ≈-≉-decidable times literal = inj₂ refl 127 ≈-≉-decidable times plus = inj₂ refl 128 ≈-≉-decidable times times = inj₁ refl 129 130 module DeqSet where 131 132 record DeqSet (α : Set) : Set where 133 constructor 134 mkDeqSet 135 field 136 _≈_ : α → α → Bool 137 _≉_ : α → α → Bool 138 139 ≈-≉-dual : (l r : α) → l ≈ r ≡ not (l ≉ r) 140 ≈-true₁ : (l r : α) → l ≈ r ≡ true → l ≡ r 141 ≈-true₂ : (l r : α) → l ≡ r → l ≈ r ≡ true 142 ≉-true₁ : (l r : α) → l ≉ r ≡ true → l ≢ r 143 ≉-true₂ : (l r : α) → l ≢ r → l ≉ r ≡ true 144 ≈-≉-decidable : (l r : α) → l ≈ r ≡ true ⊎ l ≉ r ≡ true 145 146 Tag-DeqSet : DeqSet Tag.Tag 147 Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable 148 149 module Random where 150 -- Random stuff 151 152 Tag-DeqSet : DeqSet.DeqSet Tag.Tag 153 Tag-DeqSet = {!!} 154 155 toTag : {α : Set} → Expression α → Tag.Tag 156 toTag (↑ _) = Tag.literal 157 toTag (_ ⊕ _) = Tag.plus 158 toTag (_ ⊗ _) = Tag.times 159 160 [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set 161 [ Q holds-for Tag.literal ] = (n : ℕ) → Q $ ↑ n 162 [ Q holds-for Tag.plus ] = (x y : _) → Q $ x ⊕ y 163 [ Q holds-for Tag.times ] = (x y : _) → Q $ x ⊗ y 164 165 holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → 166 [ Q holds-for (toTag x) ] → Q x 167 holds-for-tag-specialise Q (↑ n) Q-holds-for-toTag = Q-holds-for-toTag n 168 holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y 169 holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y 170 171 -- The following is ported from `variants.ma'. 172 173 _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool 174 tag ∈ [] = false 175 tag ∈ (x ∷ xs) = (Tag._≈_ (toTag tag) x) ∨ (tag ∈ xs) 176 177 record Subexpression (α : Set) (l : List Tag.Tag) : Set where 178 field 179 element : Expression α 180 ∈-element : MissingStandardLibrary.toSet $ element ∈ l 181 182 -- The following two functions are coercions in Matita. 183 subexpression : List Tag.Tag → Set → Set 184 subexpression l = λ α → Subexpression α l 185 186 mkSubexpression : {α : Set} → (l : List Tag.Tag) → (e : Expression α) → 187 MissingStandardLibrary.toSet $ e ∈ l → Subexpression α l 188 mkSubexpression l e p = record { element = e; ∈-element = p } 189 190 -- Missing from the Agda standard library, seemingly. 191 member : {α : Set} → (α → α → Bool) → α → List α → Bool 192 member p e [] = false 193 member p e (x ∷ xs) = (p e x) ∨ (member p e xs)
Note: See TracChangeset
for help on using the changeset viewer.