# Changeset 2544 for Papers

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

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

File:
1 edited

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

 r2542 open import Data.Empty open import Data.List open import Data.Nat open import Data.Unit open import Data.Nat hiding (_≟_) open import Data.Sum open import Data.Unit hiding (_≟_) open import Function open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import Relation.Binary.PropositionalEquality renaming ([_] to 〈_〉) -- The following is ported from `test.ma'. _⊗_ : Expression α → Expression α → Expression α data Tag : Set where literal : Tag plus    : Tag times   : Tag module MissingStandardLibrary where _≈_ : Tag → Tag → Bool literal ≈ literal = true plus    ≈ plus    = true times   ≈ times   = true _       ≈ _       = false toSet : Bool → Set toSet true  = ⊤ toSet false = ⊥ toTag : {α : Set} → Expression α → Tag toTag (↑ _)   = literal toTag (_ ⊕ _) = plus toTag (_ ⊗ _) = times not-not-elim : (b : Bool) → not (not b) ≡ b not-not-elim true  = refl not-not-elim false = refl [_holds-for_] : {α : Set} → (Expression α → Set) → Tag → Set [ Q holds-for literal ] = (n : ℕ) → Q \$ ↑ n [ Q holds-for plus ]    = (x y : _) → Q \$ x ⊕ y [ Q holds-for times ]   = (x y : _) → Q \$ x ⊗ y not-self-adjoint₁ : (b c : Bool) → not b ≡ c → b ≡ not c not-self-adjoint₁ true  true  () not-self-adjoint₁ true  false not-b≡c = refl not-self-adjoint₁ false true  not-b≡c = refl not-self-adjoint₁ false false () holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → [ Q holds-for (toTag x) ] → Q x holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y not-self-adjoint₂ : (b c : Bool) → b ≡ not c → not b ≡ c not-self-adjoint₂ b c b≡not-c = sym \$ not-self-adjoint₁ c b \$ sym \$ b≡not-c -- The following is ported from `variants.ma'. _≈_ : Bool → Bool → Bool true  ≈ c = c false ≈ c = not c toSet : Bool → Set toSet true  = ⊤ toSet false = ⊥ ≈-reflexive : (b : Bool) → b ≈ b ≡ true ≈-reflexive true  = refl ≈-reflexive false = refl _∈_ : {α : Set} → Expression α → List Tag → Bool tag ∈ []        = false tag ∈ (x ∷ xs) = (toTag tag ≈ x) ∨ (tag ∈ xs) ≈-true₁ : (b c : Bool) → b ≈ c ≡ true → b ≡ c ≈-true₁ true  true  b≈c-true = refl ≈-true₁ true  false () ≈-true₁ false true  b≈c-true = b≈c-true ≈-true₁ false false b≈c-true = refl record Subexpression (α : Set) (l : List Tag) : Set where field element   : Expression α ∈-element : toSet \$ element ∈ l ≈-true₂ : (b c : Bool) → b ≡ c → b ≈ c ≡ true ≈-true₂ b c b≡c rewrite b≡c = ≈-reflexive c -- Ack!  We have no coercions in Agda. ofQ : {α : Set} → (l : List Tag) → (Q : Subexpression α l → Set) → Expression α → Set ofQ l s e = ? -- Tags, and their equality module Tag where data Tag : Set where literal : Tag plus    : Tag times   : Tag _≈_ : Tag → Tag → Bool literal ≈ literal = true plus    ≈ plus    = true times   ≈ times   = true _       ≈ _       = false _≉_ : Tag → Tag → Bool l ≉ r = not \$ l ≈ r ≈-≉-dual : (l r : Tag) → l ≈ r ≡ not (l ≉ r) ≈-≉-dual l r rewrite MissingStandardLibrary.not-not-elim (l ≈ r) = refl ≈-reflexive : (l : Tag) → l ≈ l ≡ true ≈-reflexive literal = refl ≈-reflexive plus    = refl ≈-reflexive times   = refl ≈-true₁ : (l r : Tag) → l ≈ r ≡ true → l ≡ r ≈-true₁ literal literal l≈r-true = refl ≈-true₁ literal plus    () ≈-true₁ literal times   () ≈-true₁ plus    literal () ≈-true₁ plus    plus    l≈r-true = refl ≈-true₁ plus    times   () ≈-true₁ times   literal () ≈-true₁ times   plus    () ≈-true₁ times   times   l≈r-true = refl ≈-true₂ : (l r : Tag) → l ≡ r → l ≈ r ≡ true ≈-true₂ l r l≡r rewrite l≡r = ≈-reflexive r ≉-true₁ : (l r : Tag) → l ≉ r ≡ true → l ≢ r ≉-true₁ literal literal () ≉-true₁ literal plus    l≉r-true = λ () ≉-true₁ literal times   l≉r-true = λ () ≉-true₁ plus    literal l≉r-true = λ () ≉-true₁ plus    plus    () ≉-true₁ plus    times   l≉r-true = λ () ≉-true₁ times   literal l≉r-true = λ () ≉-true₁ times   plus    l≉r-true = λ () ≉-true₁ times   times   () ≉-true₂ : (l r : Tag) → l ≢ r → l ≉ r ≡ true ≉-true₂ literal literal l≢r = ⊥-elim \$ l≢r refl ≉-true₂ literal plus    l≢r = refl ≉-true₂ literal times   l≢r = refl ≉-true₂ plus    literal l≢r = refl ≉-true₂ plus    plus    l≢r = ⊥-elim \$ l≢r refl ≉-true₂ plus    times   l≢r = refl ≉-true₂ times   literal l≢r = refl ≉-true₂ times   plus    l≢r = refl ≉-true₂ times   times   l≢r = ⊥-elim \$ l≢r refl ≈-≉-decidable : (l r : Tag) → l ≈ r ≡ true ⊎ l ≉ r ≡ true ≈-≉-decidable literal literal = inj₁ refl ≈-≉-decidable literal plus    = inj₂ refl ≈-≉-decidable literal times   = inj₂ refl ≈-≉-decidable plus    literal = inj₂ refl ≈-≉-decidable plus    plus    = inj₁ refl ≈-≉-decidable plus    times   = inj₂ refl ≈-≉-decidable times   literal = inj₂ refl ≈-≉-decidable times   plus    = inj₂ refl ≈-≉-decidable times   times   = inj₁ refl module DeqSet where record DeqSet (α : Set) : Set where constructor mkDeqSet field _≈_           : α → α → Bool _≉_           : α → α → Bool ≈-≉-dual      : (l r : α) → l ≈ r ≡ not (l ≉ r) ≈-true₁       : (l r : α) → l ≈ r ≡ true → l ≡ r ≈-true₂       : (l r : α) → l ≡ r → l ≈ r ≡ true ≉-true₁       : (l r : α) → l ≉ r ≡ true → l ≢ r ≉-true₂       : (l r : α) → l ≢ r → l ≉ r ≡ true ≈-≉-decidable : (l r : α) → l ≈ r ≡ true ⊎ l ≉ r ≡ true Tag-DeqSet : DeqSet Tag.Tag Tag-DeqSet = mkDeqSet Tag._≈_ Tag._≉_ Tag.≈-≉-dual Tag.≈-true₁ Tag.≈-true₂ Tag.≉-true₁ Tag.≉-true₂ Tag.≈-≉-decidable module Random where -- Random stuff Tag-DeqSet : DeqSet.DeqSet Tag.Tag Tag-DeqSet = {!!} toTag : {α : Set} → Expression α → Tag.Tag toTag (↑ _)   = Tag.literal toTag (_ ⊕ _) = Tag.plus toTag (_ ⊗ _) = Tag.times [_holds-for_] : {α : Set} → (Expression α → Set) → Tag.Tag → Set [ Q holds-for Tag.literal ] = (n : ℕ) → Q \$ ↑ n [ Q holds-for Tag.plus ]    = (x y : _) → Q \$ x ⊕ y [ Q holds-for Tag.times ]   = (x y : _) → Q \$ x ⊗ y holds-for-tag-specialise : {α : Set} → (Q : Expression α → Set) → (x : Expression α) → [ Q holds-for (toTag x) ] → Q x holds-for-tag-specialise Q (↑ n)   Q-holds-for-toTag = Q-holds-for-toTag n holds-for-tag-specialise Q (x ⊕ y) Q-holds-for-toTag = Q-holds-for-toTag x y holds-for-tag-specialise Q (x ⊗ y) Q-holds-for-toTag = Q-holds-for-toTag x y -- The following is ported from `variants.ma'. _∈_ : {α : Set} → Expression α → List Tag.Tag → Bool tag ∈ []        = false tag ∈ (x ∷ xs) = (Tag._≈_ (toTag tag) x) ∨ (tag ∈ xs) record Subexpression (α : Set) (l : List Tag.Tag) : Set where field element   : Expression α ∈-element : MissingStandardLibrary.toSet \$ element ∈ l -- The following two functions are coercions in Matita. subexpression : List Tag.Tag → Set → Set subexpression l = λ α → Subexpression α l mkSubexpression : {α : Set} → (l : List Tag.Tag) → (e : Expression α) → MissingStandardLibrary.toSet \$ e ∈ l → Subexpression α l mkSubexpression l e p = record { element = e; ∈-element = p } -- Missing from the Agda standard library, seemingly. member : {α : Set} → (α → α → Bool) → α → List α → Bool member p e []       = false member p e (x ∷ xs) = (p e x) ∨ (member p e xs)
Note: See TracChangeset for help on using the changeset viewer.