66 lines
1.4 KiB
Idris
66 lines
1.4 KiB
Idris
module Main
|
||
|
||
import public Quox.Name
|
||
import public Quox.Syntax
|
||
import public Quox.Equal
|
||
import public Quox.Pretty
|
||
import public Quox.Typechecker
|
||
|
||
import Data.Nat
|
||
import Data.Vect
|
||
import Data.List
|
||
import Control.ANSI
|
||
|
||
|
||
private
|
||
text : PrettyOpts -> List String
|
||
text _ =
|
||
["",
|
||
#" ___ ___ _____ __ __"#,
|
||
#"/ _ `/ // / _ \\ \ /"#,
|
||
#"\_, /\_,_/\___/_\_\"#,
|
||
#" /_/"#,
|
||
""]
|
||
|
||
private
|
||
qtuwu : PrettyOpts -> List String
|
||
qtuwu opts =
|
||
if opts.unicode then
|
||
[#" ___,-´⎠ "#,
|
||
#"(·`──´ ◡ -´⎠"#,
|
||
#" \⋀/───´⎞/`──´ "#,
|
||
#" ⋃────,-₎ ⎞ "#,
|
||
#" (‾‾) ⎟ "#,
|
||
#" (‾‾‾) ⎟ "#]
|
||
else
|
||
[#" ___,-´/ "#,
|
||
#"(.`--´ u -´/"#,
|
||
#" \/\/--´|/`--´ "#,
|
||
#" U----,-, \ "#,
|
||
#" (--) | "#,
|
||
#" (---) | "#]
|
||
|
||
private
|
||
join1 : PrettyOpts -> String -> String -> String
|
||
join1 opts l r =
|
||
if opts.color then
|
||
" " <+> show (colored Green l) <+> " " <+> show (colored Magenta r)
|
||
else
|
||
" " <+> l <+> " " <+> r
|
||
|
||
export
|
||
banner : PrettyOpts -> String
|
||
banner opts = unlines $ zipWith (join1 opts) (qtuwu opts) (text opts)
|
||
|
||
export
|
||
tm : Term 1 2
|
||
tm =
|
||
(Pi 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 defPrettyOpts
|
||
prettyTermDef tm
|
||
prettyTermDef $ pushSubstsT tm
|