module PrimTypes where

data Zero : Set where
record One : Set where
data Two : Set where
  tt : Two
  ff : Two

record Sg (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sg S T
s , t = record {fst = s; snd = t}

open module Sg' {S : Set}{T : S -> Set} = Sg {S} {T}

sp0 : {S : Set}{T : S -> Set}{P : Sg S T -> Set}
      (m : (s : S)(t : T s) -> P (s , t)) -> (p : Sg S T) -> P p
sp0 m p = m (fst p) (snd p)

sp1 : {S : Set}{T : S -> Set}{P : Sg S T -> Set1}
      (m : (s : S)(t : T s) -> P (s , t)) -> (p : Sg S T) -> P p
sp1 m p = m (fst p) (snd p)
record Cont (S : Set) : Set1 where
 field
  Comm : S -> Set
  Resp : (s : S) -> Comm s -> Set
  next : (s : S) -> (c : Comm s) -> Resp s c -> S

open module Cont' {S : Set} = Cont {S}

Fun : {S : Set} -> Cont S -> (S -> Set) -> S -> Set
Fun F X s = Sg (Comm F s) \ c -> (r : Resp F s c) -> X (next F s c r)

_->>_ : {S : Set} -> (S -> Set) -> (S -> Set) -> Set
A ->> B = (s : _) -> A s -> B s

data IMu
  {S : Set}
  (F : Cont S)
  (s : S) : Set where
  con : (c : Comm F s) -> ((r : Resp F s c) -> IMu F (next F s c r)) -> IMu F s

induction : forall {S}(F : Cont S)(P : Sg S (IMu F) -> Set) ->
            ((s : S)(c : Comm F s)(f : (r : Resp F s c) -> IMu F (next F s c r))->
             ((r : Resp F s c) -> P (next F s c r , f r)) -> P (s , con c f)) ->
            {s : S}(x : IMu F s) -> P (s , x)
induction {S} F P p {s} (con c f) = p s c f \ r -> induction F P p (f r)

codata INu
  {S : Set}
  (F : Cont S)
  (s : S) : Set where
  con : (c : Comm F s) -> ((r : Resp F s c) -> INu F (next F s c r)) -> INu F s

out : forall {S}{F : Cont S}{s} -> INu F s -> Fun F (INu F) s
out (con c f) = c , f

command :  forall {S}{F : Cont S}{s} -> INu F s -> Comm F s
command d = fst (out d)

continue :  forall {S}{F : Cont S}{s}(d : INu F s)(r : Resp F s (command d)) ->
            INu F (next F s (command d) r)
continue d = snd (out d)

unfold : forall {S}{F : Cont S}(A : S -> Set) ->
         (A ->> Fun F A) -> A ->> INu F
unfold A g s a = con (fst x) \ r -> unfold A g _ (snd x r) where
  x = g s a