database2.gr

-- last checked 2019-01-07 by @buggymcbugfix

import Vec

data Patient where
  Patient
    -- (Int    [Private]) -- Patient id
    -- (String [Private]) -- Patient name
    (Int    [Public])  -- Patient age

meanAge : ∀ n : Nat . (Vec (n + 1) Patient) → Int
meanAge xs = meanAge' xs 0 1

meanAge' : ∀ n : Nat . (Vec (n + 1) Patient) -- Patient database
       → Int   -- Count
       → Int   -- Current age sum
       → Int   -- Mean age viewed public
meanAge' xs total n =
  case xs of
    Cons (Patient [age]) Nil → div (age + total) n;
    Cons (Patient [age]) xs  → meanAge' xs (age + total) (n+1)


-- Can only be `Private`
-- names : List Patient → String [Private]
-- names xs =
--   case xs of
--      Next (Patient [_] [name] [_]) xs) →
--         let [allNames] = names xs in [name `stringAppend` allNames];
--      Empty → [""]