aop
This commit is contained in:
parent
edeb98a73b
commit
73e6009179
2 changed files with 190 additions and 0 deletions
130
src/AOP/Divisoids.agda
Normal file
130
src/AOP/Divisoids.agda
Normal file
|
|
@ -0,0 +1,130 @@
|
|||
open import Relation.Binary.PropositionalEquality
|
||||
open import Data.Product
|
||||
open import Data.Empty
|
||||
|
||||
record Divisoid (X : Set) : Set₁ where
|
||||
field
|
||||
_↝_⊕_ : X → X → X → Set
|
||||
ε : X
|
||||
split-sym : ∀{x a b} → x ↝ a ⊕ b → x ↝ b ⊕ a
|
||||
split-ident₁ : ∀{x y} → x ↝ ε ⊕ y → x ≡ y
|
||||
split-ident₂ : ∀{x} → x ↝ ε ⊕ x
|
||||
split-split : {x a b a₁ b₁ a₂ b₂ : X} → x ↝ a ⊕ b → a ↝ a₁ ⊕ a₂ → b ↝ b₁ ⊕ b₂
|
||||
→ ∃[ x₁ ] ∃[ x₂ ] x ↝ x₁ ⊕ x₂ × x₁ ↝ a₁ ⊕ b₁ × x₂ ↝ a₂ ⊕ b₂
|
||||
|
||||
variable a a₁ b₁ a₂ b₂ b c d x y : X
|
||||
|
||||
split-genL : (x ↝ a ⊕ b) → (a ↝ a₁ ⊕ a₂) → ∃[ q ] (x ↝ a₁ ⊕ q) × (q ↝ a₂ ⊕ b)
|
||||
split-genL x-split a-split with split-split x-split a-split split-ident₂
|
||||
split-genL {x = x} x-split a-split | x₁ , x₂ , x-split' , x₁-split , x₂-split =
|
||||
-- goal: a₁ = a₁ / a₂ = a₂ / b₁ = ε / b₂ = b
|
||||
-- then, q will just be x₂
|
||||
let x₁≡a₁ = split-ident₁ (split-sym x₁-split) in
|
||||
x₂ , subst (λ d → x ↝ d ⊕ x₂) x₁≡a₁ x-split' , x₂-split
|
||||
|
||||
split-genR : x ↝ a ⊕ b → b ↝ c ⊕ d → ∃[ q ] x ↝ q ⊕ d × q ↝ a ⊕ c
|
||||
split-genR x-split b-split with split-split x-split (split-sym split-ident₂) b-split
|
||||
split-genR {x = x} x-split b-split | x₁ , x₂ , x-split' , x₁-split , x₂-split =
|
||||
-- same thing as above
|
||||
let x₂≡d = split-ident₁ x₂-split in
|
||||
x₁ , subst (λ e → x ↝ x₁ ⊕ e) x₂≡d x-split' , x₁-split
|
||||
|
||||
open import Data.Maybe
|
||||
open import Data.Maybe.Properties
|
||||
|
||||
infixl 10 _∙_
|
||||
_∙_ = trans
|
||||
|
||||
record PartialCommMonoid (X : Set) : Set₁ where
|
||||
field
|
||||
_·_ : X → X → Maybe X
|
||||
ε : X
|
||||
_·′_ : Maybe X → Maybe X → Maybe X
|
||||
a ·′ b = a >>= λ x → b >>= (x ·_)
|
||||
field
|
||||
·-comm : ∀{a b} → a · b ≡ b · a
|
||||
·-ident : ∀{x} → ε · x ≡ just x
|
||||
·-assoc : ∀{a b c} → (a · b) ·′ just c ≡ just a ·′ (b · c)
|
||||
variable a a₁ b₁ a₂ b₂ b c d x y : X
|
||||
|
||||
pcm-divis : Divisoid X
|
||||
pcm-divis = record
|
||||
{ _↝_⊕_ = λ x a b → just x ≡ a · b
|
||||
; ε = ε
|
||||
; split-sym = λ p → p ∙ ·-comm
|
||||
; split-ident₁ = split-ident₁
|
||||
; split-ident₂ = sym ·-ident
|
||||
; split-split = split-split
|
||||
} where
|
||||
split-ident₁ : {x y : X} → just x ≡ (ε · y) → x ≡ y
|
||||
split-ident₁ p = just-injective (p ∙ ·-ident)
|
||||
|
||||
split-split : {x a b a₁ b₁ a₂ b₂ : X} → just x ≡ (a · b) → just a ≡ (a₁ · a₂) → just b ≡ (b₁ · b₂) → ∃[ x₁ ] ∃[ x₂ ] just x ≡ (x₁ · x₂) × just x₁ ≡ (a₁ · b₁) × just x₂ ≡ (a₂ · b₂)
|
||||
split-split {x} {a} {b} {a₁} {b₁} {a₂} {b₂} x-split a-split b-split = x₁ , x₂ , xproof , x1w .proj₂ , x2w .proj₂ where
|
||||
-- This is probably the least elegant way to do this
|
||||
|
||||
open import Data.Maybe.Relation.Unary.Any renaming (just to anyjust)
|
||||
open import Data.Unit
|
||||
|
||||
a·b-is-just = subst Is-just x-split (anyjust tt)
|
||||
a₁∙a₂-is-just = subst Is-just a-split (anyjust tt)
|
||||
b₁∙b₂-is-just = subst Is-just b-split (anyjust tt)
|
||||
|
||||
·-all-just : ∀ {a b} → Is-just (a ·′ b) → Is-just a × Is-just b
|
||||
·-all-just {just x} {just y} p = (anyjust tt) , anyjust tt
|
||||
|
||||
·-assoc-just : ∀ {a b c} → Is-just (a · b) → Is-just ((a · b) ·′ just c) → Is-just (b · c) × Is-just (just a ·′ (b · c))
|
||||
·-assoc-just {a} {b} {c} p q =
|
||||
let associated = subst Is-just ·-assoc q in
|
||||
let bcjust = ·-all-just {a = just a} {b = b · c} associated .proj₂ in
|
||||
bcjust , associated
|
||||
|
||||
force-assoc : ∀ {a b c : Maybe X} → Is-just ((a ·′ b) ·′ c) → (a ·′ b) ·′ c ≡ a ·′ (b ·′ c) × Is-just (a ·′ (b ·′ c))
|
||||
force-assoc {a} {b} {c} p = helper p (all-just-ab .proj₁) (all-just-ab .proj₂) (all-just .proj₂) where
|
||||
all-just = ·-all-just {a = a ·′ b} {b = c} p
|
||||
all-just-ab = ·-all-just {a = a} {b = b} (all-just .proj₁)
|
||||
helper : ∀ {a b c} → Is-just ((a ·′ b) ·′ c) → Is-just a → Is-just b → Is-just c → ((a ·′ b) ·′ c) ≡ (a ·′ (b ·′ c)) × Is-just (a ·′ (b ·′ c))
|
||||
helper abcj (anyjust x) (anyjust x₁) (anyjust x₂) = ·-assoc , subst Is-just ·-assoc abcj
|
||||
force-assoc-sym : ∀ {a b c : Maybe X} → Is-just (a ·′ (b ·′ c)) → a ·′ (b ·′ c) ≡ (a ·′ b) ·′ c × Is-just ((a ·′ b) ·′ c)
|
||||
force-assoc-sym {a} {b} {c} p = helper p (all-just .proj₁) (all-just-bc .proj₁) (all-just-bc .proj₂) where
|
||||
all-just = ·-all-just {a = a} {b = b ·′ c} p
|
||||
all-just-bc = ·-all-just {a = b} {b = c} (all-just .proj₂)
|
||||
helper : ∀ {a b c} → Is-just (a ·′ (b ·′ c)) → Is-just a → Is-just b → Is-just c → a ·′ (b ·′ c) ≡ (a ·′ b) ·′ c × Is-just ((a ·′ b) ·′ c)
|
||||
helper abcj (anyjust x) (anyjust x₁) (anyjust x₂) = (sym ·-assoc) , (subst Is-just (sym ·-assoc) abcj)
|
||||
|
||||
[a₁a₂][b₁b₂]-is-just : Is-just ((a₁ · a₂) ·′ (b₁ · b₂))
|
||||
[a₁a₂][b₁b₂]-is-just = subst Is-just (x-split ∙ cong₂ _·′_ a-split b-split) (anyjust tt)
|
||||
|
||||
a₁[a₂[b₁b₂]]-is-just : Is-just (just a₁ ·′ (just a₂ ·′ (b₁ · b₂)))
|
||||
a₁[a₂[b₁b₂]]-is-just = force-assoc {a = just a₁} {b = just a₂} {c = b₁ · b₂} [a₁a₂][b₁b₂]-is-just .proj₂
|
||||
|
||||
a₁[[a₂b₁]b₂]-is-just : Is-just (just a₁ ·′ ((a₂ · b₁) ·′ just b₂))
|
||||
a₁[[a₂b₁]b₂]-is-just = subst (λ x → Is-just (just a₁ ·′ x)) (sym ·-assoc) a₁[a₂[b₁b₂]]-is-just
|
||||
|
||||
a₁[[b₁a₂]b₂]-is-just : Is-just (just a₁ ·′ ((b₁ · a₂) ·′ just b₂))
|
||||
a₁[[b₁a₂]b₂]-is-just = subst (λ x → Is-just (just a₁ ·′ (x ·′ just b₂))) ·-comm a₁[[a₂b₁]b₂]-is-just
|
||||
|
||||
a₁[b₁[a₂b₂]]-is-just : Is-just (just a₁ ·′ (just b₁ ·′ (a₂ · b₂)))
|
||||
a₁[b₁[a₂b₂]]-is-just = subst (λ x → Is-just (just a₁ ·′ x)) ·-assoc a₁[[b₁a₂]b₂]-is-just
|
||||
|
||||
[a₁b₁][a₂b₂]-is-just : Is-just ((a₁ · b₁) ·′ (a₂ · b₂))
|
||||
[a₁b₁][a₂b₂]-is-just = force-assoc-sym {a = just a₁} {b = just b₁} {c = a₂ · b₂} a₁[b₁[a₂b₂]]-is-just .proj₂
|
||||
|
||||
witness2 : ∀ {m : Maybe X} → Is-just m → Σ X (λ x → just x ≡ m)
|
||||
witness2 (anyjust {x = x} _) = x , refl
|
||||
|
||||
xsplit : just x ≡ (a₁ · b₁) ·′ (a₂ · b₂)
|
||||
xsplit = x-split ∙ cong₂ _·′_ a-split b-split
|
||||
∙ force-assoc {a = just a₁} {b = just a₂} {c = b₁ · b₂} [a₁a₂][b₁b₂]-is-just .proj₁
|
||||
∙ cong (just a₁ ·′_) (sym ·-assoc ∙ cong (_·′ just b₂) ·-comm ∙ ·-assoc)
|
||||
∙ force-assoc-sym {a = just a₁} {b = just b₁} {c = a₂ · b₂} a₁[b₁[a₂b₂]]-is-just .proj₁
|
||||
|
||||
just-pieces = ·-all-just {a = a₁ · b₁} {b = a₂ · b₂} [a₁b₁][a₂b₂]-is-just
|
||||
x1w = witness2 (just-pieces .proj₁)
|
||||
x2w = witness2 (just-pieces .proj₂)
|
||||
|
||||
x₁ = x1w .proj₁
|
||||
x₂ = x2w .proj₁
|
||||
|
||||
xproof : just x ≡ x₁ · x₂
|
||||
xproof = subst₂ (λ z1 z2 → just x ≡ (z1 ·′ z2)) (sym (x1w .proj₂)) (sym (x2w .proj₂)) xsplit
|
||||
60
src/AOP/NBE.agda
Normal file
60
src/AOP/NBE.agda
Normal file
|
|
@ -0,0 +1,60 @@
|
|||
module NBE where
|
||||
|
||||
open import Data.Nat
|
||||
|
||||
-- Consider this encoding of natural numbers
|
||||
data SNat : Set where
|
||||
zero : SNat
|
||||
one : SNat
|
||||
add : SNat → SNat → SNat
|
||||
|
||||
variable
|
||||
x x' y y' z z' : SNat
|
||||
|
||||
-- Along with a specification for when two natural numbers are equal
|
||||
data _≈_ : SNat → SNat → Set where
|
||||
add-zero : add zero x ≈ x
|
||||
add-one : add one x ≈ add x one
|
||||
add-any : add (add x y) z ≈ add x (add y z)
|
||||
≈-refl : x ≈ x
|
||||
≈-sym : x ≈ y → y ≈ x
|
||||
≈-trans : x ≈ y → y ≈ z → x ≈ z
|
||||
≈-cong : x ≈ x' → y ≈ y' → add x y ≈ add x' y'
|
||||
|
||||
--
|
||||
-- Our encoding is rather sloppy because it allows
|
||||
-- suboptimal representation of natural numbers.
|
||||
--
|
||||
|
||||
-- observe, for e.g., it alows:
|
||||
zero' : SNat
|
||||
zero' = add zero (add zero zero)
|
||||
|
||||
-- zero' should really just be zero!
|
||||
|
||||
-- observe that the spec agrees:
|
||||
_ : zero' ≈ zero
|
||||
_ = ≈-trans add-zero add-zero
|
||||
|
||||
-- let's write a *correct* optimizer for our sloppy encoding in three phases:
|
||||
--
|
||||
-- 1. evaluation: compiling our sloppy nats into Agda's default and optimal nats
|
||||
-- 2. reification: reconstructing optimal nats in our original encoding
|
||||
-- 3. correctness: prove that optimisation is correct
|
||||
--
|
||||
|
||||
-- phase 1: evaluation
|
||||
eval : SNat → ℕ
|
||||
eval x = {!!}
|
||||
|
||||
-- phase 2: reification
|
||||
reify : ℕ → SNat
|
||||
reify n = {!!}
|
||||
|
||||
-- optimisation is just composition! hurray!
|
||||
optimise : SNat → SNat
|
||||
optimise x = reify (eval x)
|
||||
|
||||
-- phase 3: correctness
|
||||
correct : ∀ x → optimise x ≈ x
|
||||
correct x = {!!}
|
||||
Loading…
Reference in a new issue