75 lines
2.2 KiB
Idris
75 lines
2.2 KiB
Idris
|
module Quox.Thin.Cons
|
||
|
|
|
||
|
|
import public Quox.Thin.Base
|
||
|
|
import Quox.Thin.Eqv
|
||
|
|
import Quox.Thin.View
|
||
|
|
import Data.DPair
|
||
|
|
import Control.Relation
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
|
||
|
|
public export
|
||
|
|
data IsHead : (ope : OPE m (S n) mask) -> Bool -> Type where
|
||
|
|
[search ope]
|
||
|
|
DropH : IsHead (Drop ope eq) False
|
||
|
|
KeepH : IsHead (Keep ope eq) True
|
||
|
|
|
||
|
|
public export
|
||
|
|
data IsTail : (full : OPE m (S n) mask) -> OPE m' n mask' -> Type where
|
||
|
|
[search full]
|
||
|
|
DropT : IsTail (Drop ope eq) ope
|
||
|
|
KeepT : IsTail (Keep ope eq) ope
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Uncons (ope : OPE m (S n) mask) where
|
||
|
|
constructor MkUncons
|
||
|
|
0 head : Bool
|
||
|
|
{tailMask : Nat}
|
||
|
|
0 tail : OPE scope n tailMask
|
||
|
|
{auto isHead : IsHead ope head}
|
||
|
|
{auto 0 isTail : IsTail ope tail}
|
||
|
|
|
||
|
|
public export
|
||
|
|
uncons : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Uncons ope
|
||
|
|
uncons ope with %syntactic (view ope)
|
||
|
|
uncons (Drop ope Refl) | DropV _ ope = MkUncons False ope
|
||
|
|
uncons (Keep ope Refl) | KeepV _ ope = MkUncons True ope
|
||
|
|
|
||
|
|
public export
|
||
|
|
head : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Exists $ IsHead ope
|
||
|
|
head ope = Evidence _ (uncons ope).isHead
|
||
|
|
|
||
|
|
public export
|
||
|
|
record Tail (ope : OPE m (S n) mask) where
|
||
|
|
constructor MkTail
|
||
|
|
{tailMask : Nat}
|
||
|
|
0 tail : OPE scope n tailMask
|
||
|
|
{auto 0 isTail : IsTail ope tail}
|
||
|
|
|
||
|
|
public export
|
||
|
|
tail : {n, mask : Nat} -> (0 ope : OPE m (S n) mask) -> Tail ope
|
||
|
|
tail ope = let u = uncons ope in MkTail u.tail @{u.isTail}
|
||
|
|
|
||
|
|
|
||
|
|
export
|
||
|
|
cons : {mask : Nat} -> (head : Bool) -> (0 tail : OPE m n mask) ->
|
||
|
|
Subset Nat (OPE (if head then S m else m) (S n))
|
||
|
|
cons False tail = Element _ $ drop tail
|
||
|
|
cons True tail = Element _ $ keep tail
|
||
|
|
|
||
|
|
export
|
||
|
|
0 consEquiv' : (self : OPE m' (S n) mask') ->
|
||
|
|
(head : Bool) -> (tail : OPE m n mask) ->
|
||
|
|
IsHead self head -> IsTail self tail ->
|
||
|
|
(cons head tail).snd `Eqv` self
|
||
|
|
consEquiv' (Drop tail _) False tail DropH DropT = EqvDrop reflexive
|
||
|
|
consEquiv' (Keep tail _) True tail KeepH KeepT = EqvKeep reflexive
|
||
|
|
|
||
|
|
export
|
||
|
|
0 consEquiv : (full : OPE m' (S n) mask') ->
|
||
|
|
(cons (uncons full).head (uncons full).tail).snd `Eqv` full
|
||
|
|
consEquiv full with %syntactic (uncons full)
|
||
|
|
_ | MkUncons head tail {isHead, isTail} =
|
||
|
|
consEquiv' full head tail isHead isTail
|