(** [show.lem] exports the typeclass [Show] and associated functions for pretty
  * printing arbitrary values.
  *)

open import Function
open import List
open import Maybe
open import Num
open import String

open import Missing_pervasives

class (Show 'a)
  val show : 'a -> string
end

(** [string_of_bool b] produces a string representation of boolean [b].
  *)
val string_of_bool : bool -> string
let string_of_bool b =
  match b with
    | true  -> "true"
    | false -> "false"
  end

instance (Show bool)
  let show = string_of_bool
end

instance (Show string)
  let show = id
end

(** [string_of_pair p] produces a string representation of pair [p].
  *)
val string_of_pair : forall 'a 'b. Show 'a, Show 'b => ('a * 'b) -> string
let string_of_pair (left, right) =
  "(" ^ show left ^ ", " ^ show right ^ ")"

instance forall 'a 'b. Show 'a, Show 'b => (Show ('a * 'b))
  let show = string_of_pair
end

(** [string_of_list l] produces a string representation of list [l].
  *)
val string_of_list : forall 'a. Show 'a => list 'a -> string
let string_of_list l =
  let result = intercalate "," (List.map show l) in
  let folded = foldr (^) "" result in
    "[" ^ folded ^ "]"

instance forall 'a. Show 'a => (Show (list 'a))
	let show = string_of_list
end

val string_of_maybe : forall 'a. Show 'a => maybe 'a -> string
let string_of_maybe m =
  match m with
    | Nothing -> "Nothing"
    | Just e  -> "Just " ^ show e
  end

instance forall 'a. Show 'a => (Show (maybe 'a))
  let show = string_of_maybe
end

instance (Show nat)
	let show = string_of_nat
end