Changeset 2544


Ignore:
Timestamp:
Dec 7, 2012, 5:52:23 PM (7 years ago)
Author:
mulligan
Message:

More added, painful crash course in learning Agda. Seem to have the hang of it now.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Papers/polymorphic-variants-2012/Variants.agda

    r2542 r2544  
    44  open import Data.Empty
    55  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 (_≟_)
    89
    910  open import Function
    1011
    11   open import Relation.Binary.PropositionalEquality
     12  open import Relation.Nullary
     13  open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉)
    1214
    1315  -- The following is ported from `test.ma'.
    … …  
    1820    _⊗_ : Expression α → Expression α → Expression α
    1921
    20   data Tag : Set where
    21     literal : Tag
    22     plus    : Tag
    23     times   : Tag
     22  module MissingStandardLibrary where
    2423
    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 = ⊥
    3027
    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
    3531
    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 ()
    4037
    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
    4640
    47   -- The following is ported from `variants.ma'.
     41    _≈_ : Bool → Bool → Bool
     42    true  ≈ c = c
     43    false ≈ c = not c
    4844
    49   toSet : Bool → Set
    50   toSet true  = ⊤
    51   toSet false = ⊥
     45    ≈-reflexive : (b : Bool) → b ≈ b ≡ true
     46    ≈-reflexive true  = refl
     47    ≈-reflexive false = refl
    5248
    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
    5654
    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
    6157
    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.