quox/lib/Quox/Thin/Append.idr

28 lines
919 B
Idris
Raw Permalink Normal View History

2023-06-05 10:19:52 -04:00
module Quox.Thin.Append
import public Quox.Thin.Base
import public Quox.Thin.View
import Data.DPair
%default total
public export
app' : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Exists (OPE (m1 + m2) (n1 + n2))
app' Stop ope2 = Evidence _ ope2
app' (Drop ope1 Refl) ope2 = Evidence _ $ Drop (app' ope1 ope2).snd Refl
app' (Keep ope1 Refl) ope2 = Evidence _ $ Keep (app' ope1 ope2).snd Refl
public export
(++) : {n1, n2, mask1, mask2 : Nat} ->
(0 ope1 : OPE m1 n1 mask1) -> (0 ope2 : OPE m2 n2 mask2) ->
Subset Nat (OPE (m1 + m2) (n1 + n2))
ope1 ++ ope2 with %syntactic (view ope1)
Stop ++ ope2 | StopV = Element _ ope2
Drop ope1 Refl ++ ope2 | DropV mask ope1 =
Element _ $ Drop (ope1 ++ ope2).snd Refl
Keep ope1 Refl ++ ope2 | KeepV mask ope1 =
Element _ $ Keep (ope1 ++ ope2).snd Refl
-- [todo] this mask is just (mask1 << n2) | mask2
-- prove it and add %transform