source: Papers/polymorphic-variants-2012/Variants.agda @ 2542

Last change on this file since 2542 was 2542, checked in by mulligan, 7 years ago

Trying an Agda port of the polymorphic variants implementation to see how tedious it is. Major stumbling block at the moment is the lack of coercions. Suggested solution is to use type classes, but this doesn't seem very nice either.

File size: 2.0 KB
Line 
1module Variants where
2
3  open import Data.Bool
4  open import Data.Empty
5  open import Data.List
6  open import Data.Nat
7  open import Data.Unit
8
9  open import Function
10
11  open import Relation.Binary.PropositionalEquality
12
13  -- The following is ported from `test.ma'.
14
15  data Expression (α : Set) : Set where
16       : ℕ  Expression α
17    _⊕_ : Expression α  Expression α  Expression α
18    _⊗_ : Expression α  Expression α  Expression α
19
20  data Tag : Set where
21    literal : Tag
22    plus    : Tag
23    times   : Tag
24
25  _≈_ : Tag  Tag  Bool
26  literal ≈ literal = true
27  plus    ≈ plus    = true
28  times   ≈ times   = true
29  _       ≈ _       = false
30
31  toTag : {α : Set}  Expression α  Tag
32  toTag (↑ _)   = literal
33  toTag (_ ⊕ _) = plus
34  toTag (_ ⊗ _) = times
35
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
40
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
46
47  -- The following is ported from `variants.ma'.
48
49  toSet : Bool  Set
50  toSet true  = ⊤
51  toSet false = ⊥
52
53  _∈_ : {α : Set}  Expression α  List Tag  Bool
54  tag ∈ []        = false
55  tag ∈ (x ∷ xs) = (toTag tag ≈ x) ∨ (tag ∈ xs)
56
57  record Subexpression (α : Set) (l : List Tag) : Set where
58    field
59      element   : Expression α
60      ∈-element : toSet $ element ∈ l
61
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 = ?
Note: See TracBrowser for help on using the repository browser.