Changeset 2550


Ignore:
Timestamp:
Dec 10, 2012, 6:39:57 PM (7 years ago)
Author:
mulligan
Message:

Some new ideas that lead to non-termination...

File:
1 edited

Legend:

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

    r2549 r2550  
    1111  open import Function
    1212
     13  open import Level
     14
    1315  open import Relation.Nullary
    1416  open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉)
     
    1618  -- The following is ported from `test.ma'.
    1719
    18   data Expression (α : Set) : Set where
    19     ↑   : ℕ → Expression α
    20     _⊕_ : Expression α → Expression α → Expression α
    21     _⊗_ : Expression α → Expression α → Expression α
     20  data Expression : Set where
     21    ↑   : ℕ → Expression
     22    _⊕_ : Expression → Expression → Expression
     23    _⊗_ : Expression → Expression → Expression
    2224
    2325  module MissingStandardLibrary where
     
    9193      times   : Tag
    9294
    93     toTag : {α : Set} → Expression α → Tag
     95    toTag : Expression → Tag
    9496    toTag (↑ _)   = literal
    9597    toTag (_ ⊕ _) = plus
     
    235237  module Random where
    236238
     239    _∈_ : Expression → List Tag.Tag → Set
     240    e ∈ [] = ⊥
     241    e ∈ (x ∷ xs) with Tag._≈_ x $ Tag.toTag e
     242    ... | true  = ⊤
     243    ... | false = e ∈ xs
     244
    237245    `_ : List Tag.Tag → Set
    238     ` [] = ?
    239     ` (x ∷ xs) = ?
    240 
    241     test₁ : ` [ Tag.literal ] → ℕ
    242     test₁ = {!!}
     246    ` xs = Σ Expression (λ x → x ∈ xs)
     247
     248    -- XXX: No syntax for list literals?
     249    test₁ : ` (Tag.literal ∷ Tag.plus ∷ []) → ` [ Tag.literal ]
     250    test₁ (↑ y    , tt)     = ↑ y , tt
     251    test₁ (y ⊕ y' , tt)     = ↑ 5 , tt
     252    test₁ (y ⊗ y' , absurd) = ⊥-elim absurd
     253
     254    ⟦_⟧↑ : ` [ Tag.literal ] → ℕ
     255    ⟦ ↑ y    , tt ⟧↑     = y
     256    ⟦ y ⊕ y' , absurd ⟧↑ = ⊥-elim absurd
     257    ⟦ y ⊗ y' , absurd ⟧↑ = ⊥-elim absurd
     258
     259    ⟦_⟧⊕_ : ` [ Tag.plus ] → (Expression → ℕ) → ℕ
     260    ⟦ ↑ y    , absurd ⟧⊕ f = ⊥-elim absurd
     261    ⟦ y ⊕ y' , tt     ⟧⊕ f = f y + f y'
     262    ⟦ y ⊗ y' , absurd ⟧⊕ f = ⊥-elim absurd
     263
     264    ⟦_⟧⊗_ : ` [ Tag.times ] → (Expression → ℕ) → ℕ
     265    ⟦ ↑ y    , absurd ⟧⊗ f = ⊥-elim absurd
     266    ⟦ y ⊕ y' , absurd ⟧⊗ f = ⊥-elim absurd
     267    ⟦ y ⊗ y' , tt     ⟧⊗ f = f y * f y'
     268
     269    ⟦_⟧ : Expression → ℕ
     270    ⟦ ↑ y    ⟧ = ⟦ ↑ y ⟧
     271    ⟦ y ⊕ y' ⟧ = ⟦ y ⊕ y' , tt ⟧⊕ ⟦_⟧
     272    ⟦ y ⊗ y' ⟧ = ⟦ y ⊗ y' , tt ⟧⊗ ⟦_⟧
Note: See TracChangeset for help on using the changeset viewer.