{- pretty basic boiler plate code to pretty print
   constructed valleys, result and result's as sanity check -}

module Boiler where

import Prelude
import ConfluencebyZofGeneralisedLocalDeBruijninCoqExtracted

-- show scopes as natural numbers
instance Show Nat where
  show n = show (nat2nat n)
nat2nat O = 0
nat2nat (S n) = 1 + nat2nat n

-- show an empty reduction as the term, and a non-empty as a non-empty sequence of steps
instance Show Ired where
  show (Irrefl l) = show l
  show (Irnred i) = show i

-- show non-empty sequence of steps by showing its first step and for others only their tail
instance Show Inred where
  show r = ishow True r
ishow b (Instep s t _) = (if b then (show s++" -> ") else "")++show t 
ishow b (Intrans i j) = (ishow b i)++" -> "++(ishow False j)

-- show lambda term by showing only positive scopes on top of lambda,application
instance Show Lam where  
  show (Var n) = show n
  show (Abs n l) = (if (n' > 0) then "S"++show (n'-1) else "")++"λ"++show l where n' = nat2nat n
  show (App n a b) =  (if (n' > 0) then "S"++show (n'-1) else "")++"("++show a++" "++show b++")" where n' = nat2nat n