Example.agda

module Example where

loop : Set
loop = loop

_∞_ : Set -> Set -> Set
x ∞ y = x ∞ y

data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

id : Nat -> Nat
id zero = zero
id (succ n) = succ (id n)

bad : Nat -> Nat
bad n = bad n

_+_ : Nat -> Nat -> Nat
zero     + n = n
(succ m) + n = succ (m + n)

bad2 : Nat -> Nat
bad2 (succ x) = bad2 x + bad2 (succ x)
bad2 x        = bad2 x

data Bool : Set where
    true : Bool
    false : Bool

_&&_ : Bool -> Bool -> Bool
true && a = a
false && a = false

mutual

  even : Nat -> Bool
  even zero = true
  even (succ n) = odd n

  odd  : Nat -> Bool
  odd zero = false
  odd (succ n) = even n

data Ty : {_ : Nat} -> Set where
    Base : forall {n} -> Ty {succ n}
    Arr  : forall {n} -> Ty {n} -> Ty {n} -> Ty {succ n}

eqty : forall {n} -> Ty {n} -> Ty {n} -> Bool
eqty Base Base = true
eqty (Arr a b) (Arr a' b') = (eqty a a') && (eqty b b')
eqty _ _ = false

subty : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty Base Base = true
subty (Arr a b) (Arr a' b') = (subty a' a) && (subty b b')
subty _ _ = false
 
-- the following is enough for making it termination check
subty' : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty' Base Base = true
subty' {succ n} (Arr a b) (Arr a' b')
     = (subty' a' a) && (subty' b b')
subty' _ _ = false

subty'' : forall {n} -> Ty {n} -> Ty {n} -> Bool
subty'' Base Base = true
subty'' {succ n} (Arr {.n} a b) (Arr .{n} a'' b'')
     = (subty'' {n} a'' a) && (subty'' {n} b b'')
subty'' _ _ = false


data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

add : Nat × Nat -> Nat
add (zero   , m) = m
add (succ n , m) = succ (add (n , m))

eq : Nat × Nat -> Bool
eq (zero   , zero  ) = true
eq (succ n , succ m) = eq (n , m)
eq _ = false


-- the following should not termination check

mutual

  f : Nat -> Nat -> Nat
  f zero y = zero
  f (succ x) zero = zero
  f (succ x) (succ y) = (g x (succ y)) + (f  (succ (succ x)) y)

  g : Nat -> Nat -> Nat
  g zero y = zero
  g (succ x) zero = zero
  g (succ x) (succ y) = (f (succ x) (succ y)) + (g x (succ (succ y)))


mutual

  badf : Nat ×  Nat -> Nat
  badf (zero , y) = zero
  badf (succ x , zero) = zero
  badf (succ x , succ y) = badg (x , succ y) + badf  (succ (succ x) , y)

  badg : Nat × Nat -> Nat
  badg (zero , y) = zero
  badg (succ x , zero) = zero
  badg (succ x , succ y) = badf (succ x , succ y) +  badg (x , succ (succ y))


-- these are ok, however

mutual

  f' : Nat -> Nat -> Nat
  f' zero y = zero
  f' (succ x) zero = zero
  f' (succ x) (succ y) = (g' x (succ y)) + (f'  (succ (succ x)) y)

  g' : Nat -> Nat -> Nat
  g' zero y = zero
  g' (succ x) zero = zero
  g' (succ x) (succ y) = (f' (succ x) (succ y)) + (g' x (succ y))

-- these are ok, however

bla : Nat
bla = succ (succ zero)

mutual

  f'' : Nat -> Nat -> Nat
  f'' zero y = zero
  f'' (succ x) zero = zero
  f'' (succ x) (succ y) = (g'' x (succ y)) + (f'' bla y)

  g'' : Nat -> Nat -> Nat
  g'' zero y = zero
  g'' (succ x) zero = zero
  g'' (succ x) (succ y) = (f'' (succ x) (succ y)) + (g'' x (succ y))


-- Ackermann

ack : Nat -> Nat -> Nat
ack zero y = succ y
ack (succ x) zero = ack x (succ zero)
ack (succ x) (succ y) = ack x (ack (succ x) y)

ack' : Nat × Nat -> Nat
ack' (zero , y) = succ y
ack' (succ x , zero) = ack' (x , succ zero)
ack' (succ x , succ y) = ack' (x , ack' (succ x , y))

-- Maximum of 3 numbers

max3 : Nat -> Nat -> Nat -> Nat
max3 zero zero z = z
max3 zero y zero = y
max3 x zero zero = x
max3 (succ x) (succ y) zero = succ (max3 x y zero)
max3 (succ x) zero (succ z) = succ (max3 x zero z)
max3 zero (succ y) (succ z) = succ (max3 zero y z)
max3 (succ x) (succ y) (succ z) = succ (max3 x y z)

-- addition of Ordinals

data Ord : Set where
   ozero : Ord
   olim  : (Nat -> Ord) -> Ord

addord : Ord -> Ord -> Ord
addord x ozero = x
addord x (olim f) = olim (\ n -> addord x (f n))

-- Higher-order example which should not pass the termination checker.
-- (Not the current one, anyway.)

foo : Ord -> (Nat -> Ord) -> Ord
foo ozero    g = ozero
foo (olim f) g = olim (\n -> foo (g n) f)

-- Examples checking that a function can be used with several
-- different numbers of arguments on the right-hand side.

const : {a b : Set1} -> a -> b -> a
const x _ = x

ok : Nat -> Nat -> Set
ok zero     y = Nat
ok (succ x) y = const Nat (const (ok x y) (ok x))

notOK : Set -> Set
notOK x = const (notOK Ord) notOK

-- An example which should fail (37 is an arbitrary number):

data ⊤ : Set where
  tt : ⊤

mutual

  foo37 : ⊤ -> ⊤
  foo37 x = bar37 x

  bar37 : ⊤ -> ⊤
  bar37 tt = foo37 tt

-- Some examples involving with.

-- Not OK:

withNo : Nat -> Nat
withNo n with n
withNo n | m = withNo m

-- OK:

withYes : Nat -> Nat
withYes n with n
withYes n | zero   = zero
withYes n | succ m = withYes m

-- Some rather convoluted examples.

-- OK:

number : Nat
number = zero
  where
  data Foo12 : Nat -> Set where
    foo12 : Foo12 number

-- Should the occurrence of number' in the type signature of foo12
-- really be highlighted here?

number' : Nat
number' with zero
number' | x = g12 foo12
  where
  data Foo12 : Nat -> Set where
    foo12 : Foo12 number'
  abstract
    g12 : {i : Nat} -> Foo12 i -> Nat
    g12 foo12 = zero

-- Tests highlighting (but does not type check yet):

-- number'' : Nat
-- number'' with zero
-- number'' | x = g12 (foo12 x)
--   where
--   data Foo12 : Nat -> Set where
--     foo12 : (n : Nat) -> Foo12 (number'' | n)
--   abstract
--     g12 : {i : Nat} -> Foo12 i -> Nat
--     g12 (foo12 n) = n


data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

infixr 50 _::_

-- butlast function
good1 : {A : Set} -> List A -> A 
good1 (a :: []) = a
good1 (a :: b :: bs) = good1 (b :: bs)

infixl 10 _⊕_
postulate
  _⊕_ : {A : Set} -> A -> A -> A  -- non-deterministic choice


-- a funny formulation of insert
-- insert (a :: l)  inserts a into l 
insert : {A : Set} -> List A -> List A
insert [] = []
insert (a :: []) = a :: []
insert (a :: b :: bs) = a :: b :: bs ⊕        -- case a <= b 
                        b :: insert (a :: bs) -- case a > b

-- list flattening
flat : {A : Set} -> List (List A) -> List A
flat [] = []
flat ([] :: ll) = flat ll
flat ((x :: l) :: ll) = x :: flat (l :: ll)


-- leaf-labelled trees

data Tree (A : Set) : Set where
  leaf : A -> Tree A
  node : Tree A -> Tree A -> Tree A

-- flattening (does not termination check)

tflat : {A : Set} -> Tree A -> List A
tflat (leaf a) = a :: []
tflat (node (leaf a) r) = a :: tflat r
tflat (node (node l1 l2) r) = tflat (node l1 (node l2 r))


-- Maximum of 3 numbers
-- mixing tupling and swapping: does not work with structured orders

max3' : Nat × Nat -> Nat -> Nat
max3' (zero , zero) z = z
max3' (zero , y) zero = y
max3' (x , zero) zero = x
max3' (succ x , succ y) zero   = succ (max3' (x , y) zero)
max3' (succ x , zero) (succ z) = succ (max3' (x , z) zero)
max3' (zero , succ y) (succ z) = succ (max3' (y , z) zero)
max3' (succ x , succ y) (succ z) = succ (max3' (z , x) y)