58 lines
1.7 KiB
Idris
58 lines
1.7 KiB
Idris
|
module Quox.Thin.Split
|
||
|
|
|
||
|
|
import public Quox.Thin.Base
|
||
|
|
import public Quox.Thin.View
|
||
|
|
import public Quox.Thin.Eqv
|
||
|
|
import public Quox.Thin.Append
|
||
|
|
import public Quox.Thin.Cover
|
||
|
|
import Data.DPair
|
||
|
|
import Control.Relation
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Chunks m n where
|
||
|
|
constructor MkChunks
|
||
|
|
{leftMask : Nat}
|
||
|
|
{rightMask : Nat}
|
||
|
|
0 left : OPE m (m + n) leftMask
|
||
|
|
0 right : OPE n (m + n) rightMask
|
||
|
|
{auto 0 isCover : Cover [left, right]}
|
||
|
|
%name Chunks chunks
|
||
|
|
|
||
|
|
export
|
||
|
|
chunks : (m, n : Nat) -> Chunks m n
|
||
|
|
chunks 0 0 = MkChunks Stop Stop
|
||
|
|
chunks 0 (S n) =
|
||
|
|
let MkChunks l r = chunks 0 n in
|
||
|
|
MkChunks (Drop l Refl) (Keep r Refl)
|
||
|
|
chunks (S m) n =
|
||
|
|
let MkChunks l r = chunks m n in
|
||
|
|
MkChunks (Keep l Refl) (Drop r Refl)
|
||
|
|
|
||
|
|
-- [todo] the masks here are just ((2 << m) - 1) << n and (2 << n) - 1
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
record SplitAt m n1 n2 (ope : OPE m (n1 + n2) mask) where
|
||
|
|
constructor MkSplitAt
|
||
|
|
{leftMask, rightMask : Nat}
|
||
|
|
{0 leftScope, rightScope : Nat}
|
||
|
|
0 left : OPE leftScope n1 leftMask
|
||
|
|
0 right : OPE rightScope n2 rightMask
|
||
|
|
0 scopePrf : m = leftScope + rightScope
|
||
|
|
0 opePrf : ope `Eqv` (left `app'` right).snd
|
||
|
|
%name SplitAt split
|
||
|
|
|
||
|
|
export
|
||
|
|
splitAt : (n1 : Nat) -> {n2, mask : Nat} -> (0 ope : OPE m (n1 + n2) mask) ->
|
||
|
|
SplitAt m n1 n2 ope
|
||
|
|
splitAt 0 ope = MkSplitAt zero ope Refl reflexive
|
||
|
|
splitAt (S n1) ope with %syntactic (view ope)
|
||
|
|
splitAt (S n1) (Drop ope Refl) | DropV _ ope with %syntactic (splitAt n1 ope)
|
||
|
|
_ | MkSplitAt left right scopePrf opePrf =
|
||
|
|
MkSplitAt (Drop left Refl) right scopePrf (EqvDrop opePrf)
|
||
|
|
splitAt (S n1) (Keep ope Refl) | KeepV _ ope with %syntactic (splitAt n1 ope)
|
||
|
|
_ | MkSplitAt left right scopePrf opePrf =
|
||
|
|
MkSplitAt (Keep left Refl) right (cong S scopePrf) (EqvKeep opePrf)
|