--- /dev/null
+module InterimReport where
+
+import Level
+
+module Core where
+ data Exists (A : Set) (B : A -> Set) : Set where
+ _,_ : (x : A) -> B x -> Exists A B
+
+ fst : forall {A B} -> Exists A B -> A
+ fst (x , _) = x
+
+ snd : forall {A B} -> (s : Exists A B) -> B (fst s)
+ snd (_ , x) = x
+
+ data Bot : Set where
+
+ absurd : {A : Set} -> Bot -> A
+ absurd ()
+
+ data Top : Set where
+ <> : Top
+
+ data Bool : Set where
+ true : Bool
+ false : Bool
+
+ if_/_then_else_ : forall {a} (x : Bool) ->
+ (P : Bool -> Set a) -> P true -> P false -> P x
+ if true / _ then x else _ = x
+ if false / _ then _ else x = x
+
+ if_then_else_ : forall {a} {P : Bool -> Set a}
+ (x : Bool) -> P true -> P false -> P x
+ if true then x else _ = x
+ if false then _ else y = y
+
+ data W (A : Set) (B : A -> Set) : Set where
+ _<!_ : (a : A) -> (B a -> W A B) -> W A B
+
+ -- Ugh! Comments and definiton stolen from
+ -- <http://www.e-pig.org/epilogue/?p=324>
+ rec : forall {S P}
+ (C : W S P -> Set) -> -- some conclusion we hope holds
+ ((s : S) -> -- given a shape...
+ (f : P s -> W S P) -> -- ...and a bunch of kids…
+ ((p : P s) -> C (f p)) -> -- ...and C for each kid in the bunch…
+ C (s <! f)) -> -- ...does C hold for the node?
+ (x : W S P) -> -- If so, ...
+ C x -- ...C always holds.
+ rec C c (s <! f) = c s f (\ p -> rec C c (f p))
+
+ _\/_ : (A B : Set) -> Set
+ A \/ B = Exists Bool (\ b -> if b then A else B)
+
+ inl : forall {A B} -> A -> A \/ B
+ inl x = true , x
+
+ inr : forall {A B} -> B -> A \/ B
+ inr x = false , x
+
+ case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
+ case {A} {B} {C} x f g =
+ (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
+ (snd x)
+
+ Tr : Bool -> Set
+ Tr b = if b then Top else Bot
+
+ Nat : Set
+ Nat = W Bool Tr
+
+ zero : Nat
+ zero = false <! absurd
+
+ suc : Nat -> Nat
+ suc n = true <! \ _ -> n
+
+ plus : Nat -> Nat -> Nat
+ plus x y =
+ rec (\ _ -> Nat)
+ (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
+ then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
+
+ data _==_ {A : Set} : A -> A -> Set where
+ refl : {x : A} -> x == x
+
+ subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
+ subst refl T t = t
+
+ _/==_ : forall {A} -> A -> A -> Set
+ x /== y = x == y -> Bot
+
+module Ext where
+ data List (A : Set) : Set where
+ nil : List A
+ _::_ : A -> List A -> List A
+
+ data Nat : Set where
+ zero : Nat
+ suc : Nat -> Nat
+
+ data Vec (A : Set) : Nat -> Set where
+ nil : Vec A zero
+ _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
+
+ head : forall {A n} -> Vec A (suc n) -> A
+ head (x :: _) = x
+
+ data Fin : Nat -> Set where
+ fzero : forall {n} -> Fin (suc n)
+ fsuc : forall {n} -> Fin n -> Fin (suc n)
+
+ _!!_ : forall {A n} -> Vec A n -> Fin n -> A
+ (x :: _) !! fzero = x
+ (x :: xs) !! fsuc i = xs !! i
+
+ open Core using (_==_; refl; subst)
+
+ id : {A : Set} -> A -> A
+ id x = x
+
+ map : forall {A B} -> (A -> B) -> List A -> List B
+ map _ nil = nil
+ map f (x :: xs) = f x :: map f xs
+
+ cong : forall {A B} {x y : A} (f : A -> B) -> x == y -> f x == f y
+ cong f refl = refl
+
+ map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
+ map-id==id nil = refl
+ map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)
+
+ _#_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
+ f # g = \ x -> f (g x)
+
+ map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
+ map (f # g) xs == (map f # map g) xs
+ map-#==#-map f g nil = refl
+ map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)
+
+ -- If we could have this...
+ postulate ext : forall {A B} {f g : A -> B} ->
+ ((x : A) -> f x == g x) -> f == g
+
+ map-id==id' : forall {A} -> map {A} id == id
+ map-id==id' = ext map-id==id
+
+ map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
+ map (f # g) == (map f # map g)
+ map-#==#-map' f g = ext (map-#==#-map f g)
\ No newline at end of file
projects / bitonic-mengthesis.git / blobdiff