Changeset 2546
- Timestamp:
- Dec 7, 2012, 6:49:40 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/Variants.agda
r2544 r2546 22 22 module MissingStandardLibrary where 23 23 24 -- Lifting Bool into Set 24 25 toSet : Bool → Set 25 26 toSet true = ⊤ 26 27 toSet false = ⊥ 27 28 29 -- Properties of Boolean negation 28 30 not-not-elim : (b : Bool) → not (not b) ≡ b 29 31 not-not-elim true = refl … … 39 41 not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c 40 42 43 -- Properties of Boolean disjunction 44 ∨-elim₂ : (b : Bool) → b ∨ true ≡ true 45 ∨-elim₂ true = refl 46 ∨-elim₂ false = refl 47 48 ∨-cases : (b c : Bool) → b ∨ c ≡ true → b ≡ true ⊎ c ≡ true 49 ∨-cases true c b∨c-true = inj₁ refl 50 ∨-cases false c b∨c-true = inj₂ b∨c-true 51 52 -- Boolean equality 41 53 _≈_ : Bool → Bool → Bool 42 54 true ≈ c = c … … 63 75 plus : Tag 64 76 times : Tag 77 78 toTag : {α : Set} → Expression α → Tag 79 toTag (↑ _) = literal 80 toTag (_ ⊕ _) = plus 81 toTag (_ ⊗ _) = times 65 82 66 83 _≈_ : Tag → Tag → Bool … … 136 153 _≈_ : α → α → Bool 137 154 _≉_ : α → α → Bool 138 139 155 ≈-≉-dual : (l r : α) → l ≈ r ≡ not (l ≉ r) 140 156 ≈-true₁ : (l r : α) → l ≈ r ≡ true → l ≡ r … … 146 162 Tag-DeqSet : DeqSet Tag.Tag 147 163 Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable 164 165 _∈_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → α → List α → Bool 166 _∈_ ⦃ DS ⦄ e [] = false 167 _∈_ ⦃ DS ⦄ e (x ∷ xs) = DeqSet._≈_ DS e x ∨ (e ∈ xs) 168 169 _⊂_ : {α : Set} → ⦃ DS : DeqSet α ⦄ → List α → List α → Bool 170 _⊂_ ⦃ DS ⦄ sub sup = all (λ x → x ∈ sup) sub 171 172 x∷xs-⊂-to-∈ : {α : Set} → ⦃ DS : DeqSet α ⦄ → (x : α) → (xs ys : List α) → (x ∷ xs) ⊂ ys ≡ true → x ∈ ys ≡ true 173 x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs [] x∷xs⊂ys = x∷xs⊂ys 174 x∷xs-⊂-to-∈ ⦃ DS ⦄ x xs (x' ∷ xs') x∷xs⊂ys with x ∈ xs' | inspect (λ x → x ∈ xs') $ x 175 ... | true | 〈 p 〉 = MissingStandardLibrary.∨-elim₂ $ DeqSet._≈_ DS x x' 176 ... | false | 〈 p 〉 = {!? $ MissingStandardLibrary.∨-cases ? ? p !} 148 177 149 178 module Random where 150 179 -- Random stuff 151 152 Tag-DeqSet : DeqSet.DeqSet Tag.Tag153 Tag-DeqSet = {!!}154 155 toTag : {α : Set} → Expression α → Tag.Tag156 toTag (↑ _) = Tag.literal157 toTag (_ ⊕ _) = Tag.plus158 toTag (_ ⊗ _) = Tag.times159 180 160 181 [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set … … 164 185 165 186 holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → 166 [ Q holds-for ( toTag x) ] → Q x187 [ Q holds-for (Tag.toTag x) ] → Q x 167 188 holds-for-tag-specialise Q (↑ n) Q-holds-for-toTag = Q-holds-for-toTag n 168 189 holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y … … 173 194 _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool 174 195 tag ∈ [] = false 175 tag ∈ (x ∷ xs) = (Tag._≈_ ( toTag tag) x) ∨ (tag ∈ xs)196 tag ∈ (x ∷ xs) = (Tag._≈_ (Tag.toTag tag) x) ∨ (tag ∈ xs) 176 197 177 198 record Subexpression (α : Set) (l : List Tag.Tag) : Set where
Note: See TracChangeset
for help on using the changeset viewer.