switch examples to PartialVecVec
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 17 Feb 2014 10:26:02 +0000 (11:26 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 17 Feb 2014 10:26:02 +0000 (11:26 +0100)
BFFPlug.agda
Examples.agda

index 1d5570c..f463a09 100644 (file)
@@ -12,46 +12,44 @@ open import Relation.Binary using (module DecSetoid)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
 open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
 open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
 open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
-open import Function.Equality using (_⟶_)
+open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 open import Function.LeftInverse using (_RightInverseOf_)
 
 open import Function.LeftInverse using (_RightInverseOf_)
 
+open import Generic using (≡-to-Π)
 import BFF
 import GetTypes
 import Examples
 
 open DecSetoid A using (Carrier)
 import BFF
 import GetTypes
 import Examples
 
 open DecSetoid A using (Carrier)
-open GetTypes.VecVec public using (Get)
-open BFF.VecBFF A public
+open GetTypes.PartialVecVec public using (Get)
+open BFF.PartialVecBFF A public
 
 
-bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)
-bffsameshape G {n} = bff G n
+bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))
+bffsameshape G {i} = bff G i
 
 
-bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l)
-bffplug G sput {n} {m} s v with sput n m
+bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j))
+bffplug G sput {i} {m} s v with sput i m
 ...                        | nothing = nothing
 ...                        | nothing = nothing
-...                        | just l with Get.getlen G l ≟ m
-...                                 | no getlenl≢m  = nothing
-bffplug G sput {n}     s v | just l | yes refl with bff G l s v
+...                        | just j with Get.|gl₂| G j ≟ m
+...                                 | no gl₂j≢m  = nothing
+bffplug G sput {i}     s v | just j | yes refl with bff G j s v
 ...                                            | nothing = nothing
 ...                                            | nothing = nothing
-...                                            | just s′ = just (l , s′)
-
-as-Π : {A B : Set} → (f : A → B) → PropEq A ⟶ PropEq B
-as-Π f = record { _⟨$⟩_ = f; cong = cong f }
+...                                            | just s′ = just (j , s′)
 
 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
 
 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
-f SimpleRightInvOf g = as-Π f RightInverseOf as-Π g
+f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
 
 
-bffinv : (G : Get) → (nelteg : ℕ → ℕ) → nelteg SimpleRightInvOf Get.getlen G → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (nelteg m))
-bffinv G nelteg inv {n} {m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v)
+bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m)))
+bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
-  reverse-put = bffinv reverse' id (λ _ → refl)
+  reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl)
 
   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k))
 
   drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k))
-  drop-put k = bffinv (drop' k) (flip _+_ k) (flip m+n∸n≡m k)
+  drop-put k = bffinv (drop' k) (≡-to-Π (flip _+_ k)) (flip m+n∸n≡m k)
 
   double : ℕ → ℕ
   double zero    = zero
 
   double : ℕ → ℕ
   double zero    = zero
@@ -63,4 +61,4 @@ module InvExamples where
   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
 
   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
 
   sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
-  sieve-put = bffinv sieve' double sieve-inv-len
+  sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
index 5971460..25bdbaa 100644 (file)
@@ -2,18 +2,21 @@ module Examples where
 
 open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
 
 open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉)
 open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_)
+open import Function using (id)
+open import Function.Injection using () renaming (id to id↪)
 
 
+open import Generic using (≡-to-Π)
 import GetTypes
 import FreeTheorems
 
 import GetTypes
 import FreeTheorems
 
-open GetTypes.VecVec using (Get)
-open FreeTheorems.VecVec using (assume-get)
+open GetTypes.PartialVecVec using (Get)
+open FreeTheorems.PartialVecVec using (assume-get)
 
 reverse' : Get
 
 reverse' : Get
-reverse' = assume-get reverse
+reverse' = assume-get id↪ (≡-to-Π id) reverse
 
 double' : Get
 
 double' : Get
-double' = assume-get f
+double' = assume-get id↪ (≡-to-Π g) f
   where g : ℕ → ℕ
         g zero = zero
         g (suc n) = suc (suc (g n))
   where g : ℕ → ℕ
         g zero = zero
         g (suc n) = suc (suc (g n))
@@ -22,24 +25,24 @@ double' = assume-get f
         f (x ∷ v) = x ∷ x ∷ f v
 
 double'' : Get
         f (x ∷ v) = x ∷ x ∷ f v
 
 double'' : Get
-double'' = assume-get (λ v → v ++ v)
+double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v)
 
 take' : ℕ → Get
 
 take' : ℕ → Get
-take' n = assume-get (f n)
+take' n = assume-get id↪ (≡-to-Π _) (f n)
   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
         f n       []       = []
         f zero    (x ∷ xs) = []
         f (suc n) (x ∷ xs) = x ∷ f n xs
 
 drop' : ℕ → Get
   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n)
         f n       []       = []
         f zero    (x ∷ xs) = []
         f (suc n) (x ∷ xs) = x ∷ f n xs
 
 drop' : ℕ → Get
-drop' n = assume-get (f n)
+drop' n = assume-get id↪ (≡-to-Π _) (f n)
   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
         f zero    xs       = xs
         f (suc n) []       = []
         f (suc n) (x ∷ xs) = f n xs
 
 sieve' : Get
   where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n)
         f zero    xs       = xs
         f (suc n) []       = []
         f (suc n) (x ∷ xs) = f n xs
 
 sieve' : Get
-sieve' = assume-get f
+sieve' = assume-get id↪ (≡-to-Π _) f
   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
         f []           = []
         f (x ∷ [])     = x ∷ []
   where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉
         f []           = []
         f (x ∷ [])     = x ∷ []