A pretty printer for
Elaborator Reflection (not yet - currently a very ugly printer).
| |
%language ElabReflection
implementation Show TTName where
show (UN s) = "`{{"++s++"}}"
show (NS t a) = "{"++(show t)++"."++(show a)++"}"
show (MN i s) = "{"++s++"_"++(show i)++"}"
show (SN sn) = "TTName special name"
implementation Show TTUExp where
show (UVar s i) = "ext="++s++"#"++(show i)
show (UVal i) = "U"++(show i)
-- You must turn on the UniquenessTypes extension to use UniqueType or AnyType
--implementation Show Universe where
-- show NullType = "Universe:NullType"
-- show UniqueType = "Universe:UniqueType"
-- show AllTypes = "Universe:AllTypes"
implementation Show Const where
show (I a) = show a
show (BI a) = show a
show (Fl a) = show a
show (Ch a) = show a
show (Str a) = show a
show (B8 a) = show a
show (B16 a) = show a
show (B32 a) = show a
show (B64 a) = show a
show (AType a) = "AType"
show StrType = "StrType"
show VoidType = "VoidType"
show Forgot = "Forgot"
show WorldType = "WorldType"
show TheWorld = "TheWorld"
implementation Show NameType where
show Bound = "NameType just bound by intro"
show Ref = "NameType de Bruijn indexed"
show (DCon i1 i2) = "{NameType data constructor i1="++(show i1)++" i2"++(show i2)++"}"
show (TCon i1 i2) = "{type const tag="++(show i1)++","++(show i2)++"}"
mutual
implementation Show TT where
show (P ty nm tt) = "{TT:Parameter name ref
NameType=" ++ (show ty)++
"
TTName="++ (show nm)++"
TT="++ (show tt)++"
}"
show (V i) = "{TT:de Bruijn index="++ (show i)++"}"
show (Bind ttn b tt) = "{TT:Bind
name=" ++ (show ttn)++"
binder=" ++
(show b)++"
tt=" ++ (show tt)++"
}"
show (App tt1 tt2) = "{TT:App
tt1=" ++ (show tt1)++"
tt2=" ++ (show tt2)++"
}"
show (TConst c) = "{TT:TConst c=" ++ (show c)++"}"
show Erased = "{TT:Erased}"
show (TType t) = "{TT:TType
tt="++ (show t)++"
}"
show UType = "{TT:UType}"
implementation Show (Binder TT) where
show (Lam ty) =
let
s : String = case ty of
P typ nm tt => "{λ ("++(show nm)++":"++(show typ)++
")."++(show tt)++"
}"
_ => "{Binder Lam:
arg type="++(show ty)++"
}"
in
s
show (Pi ty kind) =
let
s : String = case ty of
P typ nm tt => "{Π ("++(show nm)++":"++(show typ)++
")."++(show tt)++"
}"
_ => "{Binder Pi:
arg type="++(show ty)++"
kind="++(show kind)++"
}"
in
s
show (Let ty val) = "{Binder Let:
arg type="++(show ty)++"
val="++(show val)++"
}"
show (Hole ty) = "{Binder Hole:
arg type="++(show ty)++"
}"
show (GHole ty) = "{Binder GHole:
arg type="++(show ty)++"
}"
idNat : Nat -> Nat
idNat = %runElab (do
intro `{{x}}
fill (Var `{{x}})
--debugMessage [TextPart (show (!getGuess))]
solve
debugMessage [TextPart ("getEnv=" ++show (!getEnv)++
"
getGoal="++show (!getGoal)++
"
getHoles="++show (!getHoles))]
) |
