module GetTypes where

open import Level using () renaming (zero to ℓ₀)
open import Data.Nat using (ℕ)
open import Data.List using (List ; map)
open import Data.Vec using (Vec) renaming (map to mapV)
open import Function using (_∘_ ; id)
open import Relation.Binary.PropositionalEquality using (_≗_)

open import Structures using (Shaped ; module Shaped)
open import Instances using (VecShaped)

module ListList where
  record Get : Set₁ where
    field
      get : {A : Set} → List A → List A
      free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get

module VecVec where
  record Get : Set₁ where
    field
      getlen : ℕ → ℕ
      get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
      free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get

module PartialVecVec where
  record Get : Set₁ where
    field
      I : Set
      gl₁ : I → ℕ
      gl₂ : I → ℕ
      get : {A : Set} {i : I} → Vec A (gl₁ i) → Vec A (gl₂ i)
      free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ mapV f ≗ mapV f ∘ get

VecVec-to-PartialVecVec : VecVec.Get → PartialVecVec.Get
VecVec-to-PartialVecVec G = record
  { I = ℕ
  ; gl₁ = id
  ; gl₂ = getlen
  ; get = get
  ; free-theorem = free-theorem
  } where open VecVec.Get G

module PartialShapeShape where
  record Get : Set₁ where
    field
      SourceShape : Set
      SourceContainer : Set → SourceShape → Set
      SourceShapeT : Shaped SourceShape SourceContainer

      ViewShape : Set
      ViewContainer : Set → ViewShape → Set
      ViewShapeT : Shaped ViewShape ViewContainer

      I : Set
      gl₁ : I → SourceShape
      gl₂ : I → ViewShape

    open Shaped SourceShapeT using () renaming (fmap to fmapS)
    open Shaped ViewShapeT using () renaming (fmap to fmapV)

    field
      get : {A : Set} {i : I} → SourceContainer A (gl₁ i) → ViewContainer A (gl₂ i)
      free-theorem : {α β : Set} → (f : α → β) → {i : I} → get {_} {i} ∘ fmapS f ≗ fmapV f ∘ get

    open Shaped SourceShapeT public using () renaming (fmap to fmapS)
    open Shaped ViewShapeT public using () renaming (fmap to fmapV)

PartialVecVec-to-PartialShapeShape : PartialVecVec.Get → PartialShapeShape.Get
PartialVecVec-to-PartialShapeShape G = record
  { SourceShapeT = VecShaped
  ; ViewShapeT   = VecShaped
  ; I            = I
  ; gl₁          = gl₁
  ; gl₂          = gl₂
  ; get          = get
  ; free-theorem = free-theorem
  } where open PartialVecVec.Get G