{-# OPTIONS --no-positivity-check #-} module X6 where ---------------------------------------------------------------------- -- Exercise 6 : Generic induction -- ---------------------------------------------------------------------- -- 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 Maybe (X : Set) : Set where just : X -> Maybe X nothing : Maybe X 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 Diff : Description -> Description Diff (DSigma S D) = DSigma S \ s -> Diff (D s) Diff DPlace = D1 Diff (S D* T) = Diff S D* T D+ S D* Diff T Diff D1 = D0 Focus : Description -> Description Focus D = Diff D D* DPlace layer : (D : Description){X : Set} -> Focus D ! X -> D ! X layer (DSigma S D) ((s , d) , x) = s , layer (D s) (d , x) layer DPlace (c , x) = x layer (S D* T) ((left , s' , t) , x) = layer S (s' , x) , t layer (S D* T) ((right , s , t') , x) = s , layer T (t' , x) layer D1 ((() , _) , x) plug : (D : Description) -> Data D -> Data (LIST (Diff D ! Data D)) -> Data D plug D t [ left , void ] = t plug D t [ right , d' , d's ] = plug D [ layer D (d' , t) ] d's -- EXERCISES {- (6.1) Define the function which decorates each element of a (D ! X) with its context. You may find map quite useful here. You may also find the following useful. -} _<*>_ : {S0 S1 : Set}{T0 : S0 -> Set}{T1 : S1 -> Set} (f : S0 -> S1)(g : {s : S0} -> T0 s -> T1 (f s)) -> Sigma S0 T0 -> Sigma S1 T1 (f <*> g) (s , t) = f s , g t id : {S : Set} -> S -> S id x = x _o_ : {A : Set}{B : A -> Set}{C : (a : A) -> B a -> Set} (f : {a : A}(b : B a) -> C a b)(g : (a : A) -> B a) (a : A) -> C a (g a) (f o g) a = f (g a) decorate : (D : Description){X : Set} -> D ! X -> D ! (Focus D ! X) decorate D d = {! !} {- (6.2*) Generalize decorate to a higher-order function, so that map is not needed. Hint: abstract the map-after-decorate pattern, as used above. -} {- (6.3) Implement a function which focuses on the righmost place in some data, or returns the data unfocused if it has no place. As you can see, the type only permits you to return inl if you have a D with no places! -} rightmost : (D : Description){X : Set} -> D ! X -> (D ! Zero) :+: (Focus D ! X) rightmost D d = {! !} {- (6.4) Implement a function which moves one place to the left, rebuilding the data if there is no place left. -} leftward : (D : Description){X : Set} -> Focus D ! X -> (D ! X) :+: (Focus D ! X) leftward D d'x = {! !} {- (6.5) Implement the mirror images of the above. -} leftmost : (D : Description){X : Set} -> D ! X -> (Focus D ! X) :+: (D ! Zero) leftmost D d = {! !} rightward : (D : Description){X : Set} -> Focus D ! X -> (Focus D ! X) :+: (D ! X) rightward D d'x = {! !} {- The Zipper -} {- Gerard Huet introduced the following representation of a tree separated into a subtree and its context. Let us now write an editor for such structures! -} Zipper : Description -> Set Zipper D = Data D :*: Data (LIST (Diff D ! Data D)) {- (6.6) Implement "cursor" operations for trees, using Maybe to model the possibility that you can't move in a given direction. -} MayMove : Description -> Set MayMove D = Zipper D -> Maybe (Zipper D) moveUp : {D : Description} -> MayMove D -- towards the root moveUp z = {! !} moveDown : {D : Description} -> MayMove D -- to a child moveDown z = {! !} moveLeft : {D : Description} -> MayMove D moveLeft z = {! !} moveRight : {D : Description} -> MayMove D moveRight z = {! !} {- (6.7) Implement the operator which replaces the subtree in focus. -} replace : {D : Description} -> Data D -> MayMove D replace t z = {! !} {- We can model the traces of an editor by recording the moves we make. The index of Edit is the current state. -} after : {X : Set} -> X -> Maybe X -> X after x (just y) = y after x nothing = x data Edit {X : Set}(x : X) : Set where _/_ : (f : X -> Maybe X) -> Edit (after x (f x)) -> Edit x stop : Edit x infixr 30 _/_ {- (6.8) Implement the function which computes the final state of an edit. -} final : {X : Set}(x : X) -> Edit x -> X final x e = {! !} {- (6.9) Play! Interact by refining with / ? then normalizing the goal! -} play : Zipper TREE play = final ([ left , void ] , nil) {! !}