\subsection{Exercises} \begin{comment} \begin{code} module Exercise2 where open import Data.List open import Data.Nat open import Logic.Id \end{code} \end{comment} \NewExercise{Natural numbers} Here is a view on pairs of natural numbers. \begin{code} data Compare : Nat -> Nat -> Set where less : forall {n} k -> Compare n (n + suc k) more : forall {n} k -> Compare (n + suc k) n same : forall {n} -> Compare n n \end{code} \Exercise{Define the view function} \begin{code} compare : (n m : Nat) -> Compare n m compare n m = {! !} \end{code} \Exercise{Now use the view to compute the difference between two numbers} \begin{code} difference : Nat -> Nat -> Nat difference n m = {! !} \end{code} \NewExercise{Type checking λ-calculus} Change the type checker from Section~\ref{Views} to include precise information also in the failing case. \Exercise{Define inequality on types and change the type comparison to include inequality proofs. Hint: to figure out what the constructors of {\tt \_≠\_} should be you can start defining the {\tt \_=?=\_} function and see what you need from {\tt \_≠\_}.} \begin{comment} \begin{code} infixr 30 _→_ data Type : Set where ι : Type -- TeX mode: \iota _→_ : Type -> Type -> Type -- TeX mode: \to \end{code} \end{comment} \begin{code} data _≠_ : Type -> Type -> Set where -- ... data Equal? : Type -> Type -> Set where yes : forall {τ} -> Equal? τ τ no : forall {σ τ} -> σ ≠ τ -> Equal? σ τ _=?=_ : (σ τ : Type) -> Equal? σ τ σ =?= τ = {! !} \end{code} \Exercise{Define a type of illtyped terms and change {\tt infer} to return such a term upon failure. Look to the definition of {\tt infer} for clues to the constructors of {\tt BadTerm}.} \begin{comment} \begin{code} data _∈_ {A : Set}(x : A) : List A -> Set where hd : forall {xs} -> x ∈ x :: xs tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs index : forall {A}{x : A}{xs} -> x ∈ xs -> Nat index hd = zero index (tl p) = suc (index p) Cxt = List Type infixl 80 _$_ data Raw : Set where var : Nat -> Raw _$_ : Raw -> Raw -> Raw lam : Type -> Raw -> Raw data Term (Γ : Cxt) : Type -> Set where var : forall {τ} -> τ ∈ Γ -> Term Γ τ _$_ : forall {σ τ} -> Term Γ (σ → τ) -> Term Γ σ -> Term Γ τ lam : forall σ {τ} -> Term (σ :: Γ) τ -> Term Γ (σ → τ) erase : forall {Γ τ} -> Term Γ τ -> Raw erase (var x) = var (index x) erase (t$ u) = erase t $erase u erase (lam σ t) = lam σ (erase t) \end{code} \end{comment} \begin{code} data BadTerm (Γ : Cxt) : Set where -- ... eraseBad : {Γ : Cxt} -> BadTerm Γ -> Raw eraseBad b = {! !} data Infer (Γ : Cxt) : Raw -> Set where ok : (τ : Type)(t : Term Γ τ) -> Infer Γ (erase t) bad : (b : BadTerm Γ) -> Infer Γ (eraseBad b) infer : (Γ : Cxt)(e : Raw) -> Infer Γ e infer Γ e = {! !} \end{code} \NewExercise{Properties of list functions} \begin{comment} \begin{code} open import Data.Bool \end{code} \end{comment} Remember the following predicates on lists from Section~\ref{Views} \begin{fakecode} data _∈_ {A : Set}(x : A) : List A -> Set where hd : forall {xs} -> x ∈ x :: xs tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs \end{fakecode} \begin{code} infixr 30 _::_ data All {A : Set}(P : A -> Set) : List A -> Set where [] : All P [] _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs) \end{code} \Exercise{Prove the following lemma stating that {\tt All} is sound.} \begin{code} lemma-All-∈ : forall {A x xs}{P : A -> Set} -> All P xs -> x ∈ xs -> P x lemma-All-∈ p i = {! !} \end{code} We proved that filter computes a sublist of its input. Now let's finish the job. \Exercise{Below is the proof that all elements of {\tt filter p xs} satisfies {\tt p}. Doing this without any auxiliary lemmas involves some rather subtle use of with-abstraction. Figure out what is going on by replaying the construction of the program and looking at the goal and context in each step. } \begin{code} lem-filter-sound : {A : Set}(p : A -> Bool)(xs : List A) -> All (satisfies p) (filter p xs) lem-filter-sound p [] = [] lem-filter-sound p (x :: xs) with inspect (p x) lem-filter-sound p (x :: xs) | it y prf with p x | prf lem-filter-sound p (x :: xs) | it .true prf | true | refl = trueIsTrue prf :: lem-filter-sound p xs lem-filter-sound p (x :: xs) | it .false prf | false | refl = lem-filter-sound p xs \end{code} \Exercise{Finally prove {\tt filter} complete, by proving that all elements of the original list satisfying the predicate are present in the result.} \begin{code} lem-filter-complete : {A : Set}(p : A -> Bool)(x : A){xs : List A} -> x ∈ xs -> satisfies p x -> x ∈ filter p xs lem-filter-complete p x el px = {! !} \end{code} \NewExercise{An XML universe} \begin{comment} \begin{code} open import Data.String open import Logic.Base \end{code} \end{comment} Here is simplified universe of XML schemas: % \begin{code} Tag = String mutual data Schema : Set where tag : Tag -> List Child -> Schema data Child : Set where text : Child elem : Nat -> Nat -> Schema -> Child \end{code} % The number arguments to {\tt elem} specifies the minimum and maximum number of repetitions of the subschema. For instance, {\tt elem 0 1 s} would be an optional child and {\tt elem 1 1 s} would be a child which has to be present. To define the decoding function we need a type of lists of between$n$and$m\$ elements. This is the {\tt FList} type below. \begin{code} data BList (A : Set) : Nat -> Set where [] : forall {n} -> BList A n _::_ : forall {n} -> A -> BList A n -> BList A (suc n) data Cons (A B : Set) : Set where _::_ : A -> B -> Cons A B FList : Set -> Nat -> Nat -> Set FList A zero m = BList A m FList A (suc n) zero = False FList A (suc n) (suc m) = Cons A (FList A n m) \end{code} % Now we define the decoding function as a datatype {\tt XML}. % \begin{code} mutual data XML : Schema -> Set where element : forall {kids}(t : Tag) -> All Element kids -> XML (tag t kids) Element : Child -> Set Element text = String Element (elem n m s) = FList (XML s) n m \end{code} \begin{comment} \begin{code} -- Example schema : Schema schema = tag "html" ( elem 0 1 (tag "head" (elem 0 1 (tag "title" (text :: [])) :: [])) :: elem 1 1 (tag "body" (text :: [])) :: [] ) xml : XML schema xml = element "html" ([] :: (element "body" ("Some text" :: []) :: []) :: []) \end{code} \end{comment} \Exercise{Implement a function to print XML documents. The string concatenation function is {\tt \_+++\_}.} \begin{code} mutual printXML : {s : Schema} -> XML s -> String printXML xml = {! !} printChildren : {kids : List Child} -> All Element kids -> String printChildren xs = {! !} \end{code}