module Exercise2 where

open import Data.List
open import Data.Nat
open import Logic.Id

-- Natural numbers ------------------------------------------

-- Here is a view on pairs of natural numbers.
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

-- Define the view function
compare : (n m : Nat) -> Compare n m
compare n m = {! !}

-- Now use the view to compute the difference between two numbers
difference : Nat -> Nat -> Nat
difference n m = {! !}

-- Type checking λ-calcus -----------------------------------

-- Exercise: Open up TypeChecker.agda and fill in the gaps.

-- List lookup ----------------------------------------------

-- (Proof-oriented exercise)

open import Data.Bool

-- In TeX mode (M-x set-input-mode TeX) ∈ = \in
data _∈_ {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> x ∈ x :: xs
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs

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)

-- Prove the following (obvious) lemma
lemma-All-∈ : forall {A x xs}{P : A -> Set} -> All P xs -> x ∈ xs -> P x
lemma-All-∈ p i = {! !}

-- (Did the definition look familiar?)

-- We proved that filter computes a sublist of its input. Now let's finish the job.

-- Prove that all elements of filter p xs satisfies p. Doing this without any
-- auxiliary lemmas involves some rather subtle use of with-abstraction.

-- Exercise: Figure out what is going on by replaying the construction of the program
--           and looking at the goal and context in each step.
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

-- Prove that all elements of the input list satisfying the predicate is also in the result.
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 = {! !}


-- Universes ------------------------------------------------

-- From the lecture

open import Data.String
open import Logic.Base

Tag = String

mutual
  data Schema : Set where
    tag : Tag -> List Child -> Schema

  data Child : Set where
    text : Child
    elem : Nat -> Nat -> Schema -> Child

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)

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

-- 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" :: []) :: []) :: [])

-- Exercise: write a function to print xml documents
-- The string concatenation function is called _+++_.
mutual
  printXML : {s : Schema} -> XML s -> String
  printXML xml = {! !}

  printChildren : {kids : List Child} -> All Element kids -> String
  printChildren xs = {! !}