{-# OPTIONS --no-positivity-check #-} module X5 where ---------------------------------------------------------------------- -- Exercise 5 : Generic induction and the container view -- ---------------------------------------------------------------------- -- LIBRARY data Zero : Set where magic : {X : Set} -> Zero -> X magic () data One : Set where void : One data Two : Set where left : Two right : Two data Sigma (S : Set)(T : S -> Set) : Set where _,_ : (s : S)(t : T s) -> Sigma S T infixr 40 _,_ _:*:_ : Set -> Set -> Set S :*: T = Sigma S \ s -> T data _:+:_ (S T : Set) : Set where inl : S -> S :+: T inr : T -> S :+: T case : {S T X : Set} -> (S -> X) -> (T -> X) -> S :+: T -> X case sf tf (inl s) = sf s case sf tf (inr t) = tf t data Description : Set1 where -- that's a set of sets! DSigma : (S : Set) -> (S -> Description) -> Description DPlace : Description _D*_ : Description -> Description -> Description D1 : Description infixr 40 _D*_ _D+_ : Description -> Description -> Description S D+ T = DSigma Two Args where Args : Two -> Description Args left = S Args right = T infixr 30 _D+_ D0 : Description D0 = DSigma Zero Args where Args : Zero -> Description Args () NAT : Description NAT = D1 D+ DPlace TREE : Description TREE = D1 D+ DPlace D* DPlace LIST : Set -> Description LIST X = D1 D+ DSigma X \ _ -> DPlace _!_ : Description -> Set -> Set DSigma S D ! X = Sigma S (\ s -> D s ! X ) DPlace ! X = X (S D* T) ! X = (S ! X) :*: (T ! X) D1 ! X = One data Data (D : Description) : Set where [_] : D ! Data D -> Data D zero : Data NAT zero = [ left , void ] suc : Data NAT -> Data NAT suc n = [ right , n ] nil : {X : Set} -> Data (LIST X) nil = [ left , void ] cons : {X : Set} -> X -> Data (LIST X) -> Data (LIST X) cons x xs = [ right , x , xs ] map : (D : Description){A B : Set} -> (A -> B) -> D ! A -> D ! B map (DSigma S D) f (s , d) = s , map (D s) f d map DPlace f a = f a map (S D* T) f (s , t) = map S f s , map T f t map D1 f d = d [_<|_] : (S : Set)(P : S -> Set) -> Set -> Set [ S <| P ] X = Sigma S \ s -> P s -> X Shape : Description -> Set Shape D = D ! One Positions : (D : Description) -> Shape D -> Set Positions (DSigma S D) (s , d) = Positions (D s) d Positions DPlace d = One Positions (S D* T) (s , t) = Positions S s :+: Positions T t Positions D1 d = Zero -- EXERCISES {- (5.1) Define the constructors for TREE in this style -} leaf : Data TREE leaf = {! !} node : Data TREE -> Data TREE -> Data TREE node s t = {! !} {- (5.2) Check that the following induction principle holds. -} indTREE : (P : Data TREE -> Set) -> P leaf -> ((s t : Data TREE) -> P s -> P t -> P (node s t)) -> (x : Data TREE) -> P x indTREE P pl pn t = {! !} {- (5.3) Define Everywhere and everywhere for (D ! X) in the same style as Exercise 4. -} Everywhere : (D : Description){X : Set} -> (X -> Set) -> D ! X -> Set Everywhere D P dx = {! !} everywhere : (D : Description){X : Set}(P : X -> Set) -> ((x : X) -> P x) -> (xs : D ! X) -> Everywhere D P xs everywhere D P p dx = {! !} {- (5.4*) Implement the induction principle. Hint: it's a bit like fold; it's worth producing a version which the termination checker doesn't like, then transforming it. -} induction : (D : Description)(P : Data D -> Set) -> ((dt : D ! Data D) -> Everywhere D P dt -> P [ dt ]) -> (t : Data D) -> P t induction D P p t = {! !} {- (5.5) Show how to build a D ! X from the corresponding element of [ Shape D <| Positions D ] X -} build : (D : Description){X : Set} -> [ Shape D <| Positions D ] X -> D ! X build D sf = {! !} {- (5.6) Given s : Shape D, show how to build a (D ! Positions D s) where each place holds its own position. -} layout : (D : Description){X : Set}(d1 : Shape D) -> D ! Positions D d1 layout D d1 = {! !} {- (5.7*) Construct the "view" which shows how each element of D ! X is given by some (build D (s , f)) -} data Container (D : Description)(X : Set) : D ! X -> Set where _ X) -> Container D X (build D (s , f)) container : (D : Description)(X : Set)(dx : D ! X) -> Container D X dx container D X d = {! !}