0247bde2a8af4e1831e555d55fc82086b2374617
[~helmut/bidiragda.git] / BFF.agda
1 module BFF where
2
3 open import Data.Nat using (ℕ)
4 open import Data.Fin using (Fin)
5 open import Level using () renaming (zero to ℓ₀)
6 import Category.Monad
7 import Category.Functor
8 open import Data.Maybe using (Maybe ; just ; nothing ; maybe′)
9 open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
10 open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
11 open import Data.List using (List ; [] ; _∷_ ; map ; length)
12 open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_)
13 open import Function using (id ; _∘_ ; flip)
14 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
15 open import Function.Injection using (module Injection) renaming (Injection to _↪_)
16 open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
17 open import Relation.Binary.PropositionalEquality using () renaming (setoid to EqSetoid)
18 open Injection using (to)
19
20 open import FinMap
21 open import Generic using (mapMV)
22 import CheckInsert
23 import FreeTheorems
24
25 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
26   open FreeTheorems.VecVec public using (get-type)
27   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
28   open CheckInsert A
29
30   assoc : {n m : ℕ} → Vec (Fin n) m → Vec Carrier m → Maybe (FinMapMaybe n Carrier)
31   assoc []V       []V       = just empty
32   assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b)
33
34   enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n
35   enumerate _ = tabulate id
36
37   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
38   denumerate = flip lookupV
39
40   bff : {getlen : ℕ → ℕ} → (get-type getlen) → ({n : ℕ} → Vec Carrier n → Vec Carrier (getlen n) → Maybe (Vec Carrier n))
41   bff get s v = let s′ = enumerate s
42                     t′ = get s′
43                     g  = fromFunc (denumerate s)
44                     g′ = delete-many t′ g
45                     h  = assoc t′ v
46                     h′ = (flip union g′) <$> h
47                 in h′ >>= flip mapMV s′ ∘ flip lookupV
48
49 module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
50   open FreeTheorems.PartialVecVec public using (get-type)
51   open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq)
52   open CheckInsert A
53
54   open VecBFF A public using (assoc ; enumerate ; denumerate)
55
56   bff : {I : Setoid ℓ₀ ℓ₀} {gl₁ : I ↪ (EqSetoid ℕ)} {gl₂ : I ⟶ EqSetoid ℕ} → get-type gl₁ gl₂ → ({i : Setoid.Carrier I} → Vec Carrier (to gl₁ ⟨$⟩ i) → Vec Carrier (gl₂ ⟨$⟩ i) → Maybe (Vec Carrier (to gl₁ ⟨$⟩ i)))
57   bff get s v = let s′ = enumerate s
58                     t′ = get s′
59                     g  = fromFunc (denumerate s)
60                     g′ = delete-many t′ g
61                     h  = assoc t′ v
62                     h′ = (flip union g′) <$> h
63                 in h′ >>= flip mapMV s′ ∘ flip lookupV