76 lines
1.6 KiB
Idris
76 lines
1.6 KiB
Idris
module Quox
|
||
|
||
import public Quox.Name
|
||
import public Quox.Syntax
|
||
import public Quox.Equal
|
||
import public Quox.Error
|
||
import public Quox.Pretty
|
||
-- import public Quox.Typechecker
|
||
|
||
import Data.Nat
|
||
import Data.Vect
|
||
import Control.ANSI
|
||
|
||
|
||
public export
|
||
record BannerOpts where
|
||
constructor MakeBannerOpts
|
||
unicode, color : Bool
|
||
|
||
public export
|
||
defBannerOpts : BannerOpts
|
||
defBannerOpts = MakeBannerOpts {unicode = True, color = True}
|
||
|
||
private
|
||
text : BannerOpts -> List String
|
||
text _ =
|
||
["",
|
||
#" ___ ___ _____ __ __"#,
|
||
#"/ _ `/ // / _ \\ \ /"#,
|
||
#"\_, /\_,_/\___/_\_\"#,
|
||
#" /_/"#,
|
||
""]
|
||
|
||
private
|
||
qtuwu : BannerOpts -> List String
|
||
qtuwu opts =
|
||
if opts.unicode then
|
||
[#" ___,-´⎠ "#,
|
||
#"(·`──´ ◡ -´⎠"#,
|
||
#" \⋀/───´⎞/`──´ "#,
|
||
#" ⋃────,-₎ ⎞ "#,
|
||
#" (‾‾) ⎟ "#,
|
||
#" (‾‾‾) ⎟ "#]
|
||
else
|
||
[#" ___,-´/ "#,
|
||
#"(.`--´ u -´/"#,
|
||
#" \/\/--´|/`--´ "#,
|
||
#" U----,-, \ "#,
|
||
#" (--) | "#,
|
||
#" (---) | "#]
|
||
|
||
private
|
||
join1 : BannerOpts -> String -> String -> String
|
||
join1 opts l r =
|
||
if opts.color then
|
||
" " <+> show (colored Green l) <+> " " <+> show (colored Magenta r)
|
||
else
|
||
" " <+> l <+> " " <+> r
|
||
|
||
export
|
||
banner : BannerOpts -> String
|
||
banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
|
||
|
||
export
|
||
tm : Term 1 2
|
||
tm =
|
||
(Pi Zero One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
|
||
`DCloT` (K One ::: id))
|
||
`CloT` (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
|
||
|
||
main : IO Unit
|
||
main = do
|
||
putStrLn $ banner defBannerOpts
|
||
prettyTerm tm
|
||
prettyTerm $ pushSubstsT tm
|