module L4 where ---------------------------------------------------------------------- -- Lecture 4 : Shapes and positions ---------------------------------------------------------------------- data List (X : Set) : Set where [l] : List X _:l:_ : X -> List X -> List X infixr 40 _:l:_ data One : Set where void : One data Zero : Set where magic : {X : Set} -> Zero -> X magic () data _:+:_ (S T : Set) : Set where inl : S -> S :+: T inr : T -> S :+: T Somewhere : {X : Set} -> (X -> Set) -> List X -> Set Somewhere P [l] = Zero Somewhere P (x :l: xs) = P x :+: (Somewhere P xs) get : {X : Set}{P : X -> Set}(xs : List X)(i : Somewhere P xs) -> X get [l] () get (x :l: xs) (inl p) = x get (x :l: xs) (inr i) = get xs i data Sigma (S : Set)(T : S -> Set) : Set where _,_ : (s : S)(t : T s) -> Sigma S T _*_ : Set -> Set -> Set S * T = Sigma S \ s -> T get2 : {X : Set}{P : X -> Set}(xs : List X)(i : Somewhere P xs) -> Sigma X P get2 [l] () get2 (x :l: xs) (inl p) = x , p get2 (x :l: xs) (inr i) = get2 xs i ------- data Nat : Set where zero : Nat suc : Nat -> Nat data _^_ (X : Set) : Nat -> Set where [] : X ^ zero _::_ : {n : Nat} -> X -> X ^ n -> X ^ suc n List2 : Set -> Set List2 X = Sigma Nat \ n -> X ^ n [l2] : {X : Set} -> List2 X [l2] = zero , [] _:l2:_ : {X : Set} -> X -> List2 X -> List2 X x :l2: (n , xs) = suc n , (x :: xs) infixr 40 _:l2:_ foldr2 : {X T : Set} -> (X -> T -> T) -> T -> List2 X -> T foldr2 f t (zero , []) = t foldr2 f t (suc n , (x :: xs)) = f x (foldr2 f t (n , xs)) _+2+_ : {X : Set} -> List2 X -> List2 X -> List2 X xs +2+ ys = foldr2 _:l2:_ ys xs --------------------- data Fin : Nat -> Set where fzero : {n : Nat} -> Fin (suc n) fsuc : {n : Nat} -> Fin n -> Fin (suc n) List3 : Set -> Set List3 X = Sigma Nat \ n -> Fin n -> X [l3] : {X : Set} -> List3 X [l3] = zero , none where none : Fin zero -> _ none () _:l3:_ : {X : Set} -> X -> List3 X -> List3 X _:l3:_ x (n , f) = suc n , xf where xf : Fin (suc n) -> _ xf fzero = x xf (fsuc i) = f i {- think about "shape and position" presentations of other containers -} ListShape : Set ListShape = List One ListPosition : ListShape -> Set ListPosition s = Somewhere (\ x -> One) s List4 : Set -> Set List4 X = Sigma ListShape \ s -> ListPosition s -> X [l4] : {X : Set} -> List4 X [l4] = [l] , magic _:l4:_ : {X : Set} -> X -> List4 X -> List4 X _:l4:_ x (s , f) = (void :l: s) , xf where xf : One :+: _ -> _ xf (inl void) = x xf (inr i) = f i