------------------------------------------------------------------------
-- The Agda standard library
--
-- An example showing how the Debug.Trace module can be used
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --rewriting --guardedness #-}

module README.Debug.Trace where

------------------------------------------------------------------------
-- Sometimes compiled code can contain bugs.

-- Whether caused by the compiler or present in the source code already, they
-- can be hard to track. A primitive debugging technique is to strategically
-- insert calls to tracing functions which will display their String argument
-- upon evaluation.

open import Data.String.Base using (_++_)
open import Debug.Trace

-- We can for instance add tracing messages to make sure an invariant is
-- respected or check in which order evaluation takes place in the backend
-- (which can inform our decision to use, or not, strictness primitives).

-- In the following example, we define a division operation on natural numbers
-- using the original dividend as the termination measure. We:

-- 1. check in the base case that when the fuel runs out then the updated dividend
--    is already zero.

-- 2. wrap the calls to _∸_ and go in respective calls to trace to see when all
--    of these thunks are forced: are we building a big thunk in go's second
--    argument or evaluating it as we go?

open import Data.Maybe.Base
open import Data.Nat.Base
open import Data.Nat.Show using (show)

div : ℕ → ℕ → Maybe ℕ
div m zero = nothing
div m n    = just (go m m) where

  -- invariants: m ≤ fuel
  -- result : m / n
  go : (fuel : ℕ) (m : ℕ) → ℕ
  go zero       m = trace ("Invariant: " ++ show m ++ " should be zero.") zero
  go (suc fuel) m =
    let m′ = trace ("Thunk for step " ++ show fuel ++ " forced") (m ∸ n) in
    trace ("Recursive call for step " ++ show fuel) (suc (go fuel m′))

-- To observe the behaviour of this code, we need to compile it and run it.
-- To run it, we need a main function. We define a very basic one: run div,
-- and display its result if the run was successful.

-- We add two calls to trace to see when div is evaluated and when the returned
-- number is forced (by a call to show).

open import Level using (0ℓ)
open import IO

main : Main
main =
  let r = trace "Call to div" (div  )
      j = λ n → trace "Forcing the result wrapped in just." (putStrLn (show n)) in
  run (maybe′ j (pure _) r)

-- We get the following trace where we can see that checking that the
-- maybe-solution is just-headed does not force the natural number. Once forced,
-- we observe that we indeed build a big thunk on go's second argument (all the
-- recursive calls happen first and then we force the thunks one by one).

-- Call to div
-- Forcing the result wrapped in just.
-- Recursive call for step 3
-- Recursive call for step 2
-- Recursive call for step 1
-- Recursive call for step 0
-- Thunk for step 0 forced
-- Thunk for step 1 forced
-- Thunk for step 2 forced
-- Thunk for step 3 forced
-- Invariant: 0 should be zero.
-- 4

-- We also notice that the result is incorrect: 4/2 is 2 and not 4. We quickly
-- notice that (div m (suc n)) will perform m recursive calls no matter what.
-- And at each call it will put add 1. We can fix this bug by adding a new first
-- equation to go:

-- go fuel zero = zero

-- Running the example again we observe that because we now need to check
-- whether go's second argument is zero, the function is more strict: we see
-- that recursive calls and thunk forcings are interleaved.

-- Call to div
-- Forcing the result wrapped in just.
-- Recursive call for step 3
-- Thunk for step 3 forced
-- Recursive call for step 2
-- Thunk for step 2 forced
-- 2