25 lines
912 B
Plaintext
25 lines
912 B
Plaintext
module Show where
|
|
|
|
open import Agda.Builtin.List
|
|
open import Agda.Builtin.Maybe
|
|
open import Agda.Builtin.String
|
|
|
|
open import Parse
|
|
|
|
-- result to string
|
|
showResult : {A : Set} → (A → String) → Result A → String
|
|
showResult f (emit nothing rem) = primStringAppend "remainder: " (primStringFromList rem)
|
|
showResult f (emit (just r) []) = primStringAppend "result: " (f r)
|
|
showResult f (emit (just r) xs) = primStringAppend (primStringAppend "result: " (f r)) (primStringAppend ", remainder: " (primStringFromList xs))
|
|
|
|
-- append all of the items in a list
|
|
showList : {V : Set} → (V → String) → List V → String
|
|
showList f [] = ""
|
|
showList f (x ∷ []) = f x
|
|
showList f (x ∷ xs) = primStringAppend (f x) (primStringAppend ", " (showList f xs))
|
|
|
|
-- maybe to definitely a string
|
|
showMaybe : {V : Set} → (V → String) → Maybe V → String
|
|
showMaybe f nothing = "nothing"
|
|
showMaybe f (just v) = f v
|