Ignore:
Timestamp:
Dec 7, 2012, 6:49:40 PM (7 years ago)
Author:
mulligan
Message:

Some more progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/Variants.agda

    r2544 r2546  
    2222  module MissingStandardLibrary where
    2323
     24    -- Lifting Bool into Set
    2425    toSet : Bool → Set
    2526    toSet true  = ⊤
    2627    toSet false = ⊥
    2728
     29    -- Properties of Boolean negation
    2830    not-not-elim : (b : Bool) → not (not b) ≡ b
    2931    not-not-elim true  = refl
     
    3941    not-self-adjoint₂ b c b≡not-c = sym $ not-self-adjoint₁ c b $ sym $ b≡not-c
    4042
     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
    4153    _≈_ : Bool → Bool → Bool
    4254    true  ≈ c = c
     
    6375      plus    : Tag
    6476      times   : Tag
     77
     78    toTag : {α : Set} → Expression α → Tag
     79    toTag (↑ _)   = literal
     80    toTag (_ ⊕ _) = plus
     81    toTag (_ ⊗ _) = times
    6582
    6683    _≈_ : Tag → Tag → Bool
     
    136153        _≈_           : α → α → Bool
    137154        _≉_           : α → α → Bool
    138 
    139155        ≈-≉-dual      : (l r : α) → l ≈ r ≡ not (l ≉ r)
    140156        ≈-true₁       : (l r : α) → l ≈ r ≡ true → l ≡ r
     
    146162    Tag-DeqSet : DeqSet Tag.Tag
    147163    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 !}
    148177 
    149178  module Random where
    150179  -- 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
    159180
    160181    [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set
     
    164185
    165186    holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) →
    166       [ Q holds-for (toTag x) ] → Q x
     187      [ Q holds-for (Tag.toTag x) ] → Q x
    167188    holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n
    168189    holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y
     
    173194    _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool
    174195    tag ∈ []        = false
    175     tag ∈ (x ∷ xs) = (Tag._≈_ (toTag tag) x) ∨ (tag ∈ xs)
     196    tag ∈ (x ∷ xs) = (Tag._≈_ (Tag.toTag tag) x) ∨ (tag ∈ xs)
    176197
    177198    record Subexpression (α : Set) (l : List Tag.Tag) : Set where
Note: See TracChangeset for help on using the changeset viewer.