quox/src/Quox.idr

66 lines
1.4 KiB
Idris
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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
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 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 defPrettyOpts
prettyTermDef tm
prettyTermDef $ pushSubstsT tm