GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 13:01:31 +03:00
Code Issues Projects Releases Wiki Activity

Pretty print with a bit more space, so we can see what's going on.

Browse Source
This commit is contained in:
Iavor Diatchki 2017-08-15 10:52:32 -07:00
parent ca2136fab9
commit b3f605d9f4
1 changed files with 21 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
src/Cryptol/TypeCheck/Parseable.hs
View File

@ -33,14 +33,15 @@ instance ShowParseable Expr where
showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es) showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es)
showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides) showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides)
showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s) showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s)
showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c <+> showParseable t <+> showParseable f) showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c $$ showParseable t $$ showParseable f)
showParseable (EComp _ _ e mss) = parens (text "EComp" <+> showParseable e <+> showParseable mss) showParseable (EComp _ _ e mss) = parens (text "EComp" $$ showParseable e $$ showParseable mss)
showParseable (EVar n) = parens (text "EVar" <+> showParseable n) showParseable (EVar n) = parens (text "EVar" <+> showParseable n)
showParseable (EApp fe ae) = parens (text "EApp" <+> showParseable fe <+> showParseable ae) showParseable (EApp fe ae) = parens (text "EApp" $$ showParseable fe $$ showParseable ae)
showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n <+> showParseable e) showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n $$ showParseable e)
showParseable (EWhere e dclg) = parens (text "EWhere" <+> showParseable e <+> showParseable dclg) showParseable (EWhere e dclg) = parens (text "EWhere" $$ showParseable e $$ showParseable dclg)
showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp <+> showParseable e) showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp
showParseable (ETApp e t) = parens (text "ETApp" <+> showParseable e <+> parens (text "ETyp" <+> showParseable t)) $$ showParseable e)
showParseable (ETApp e t) = parens (text "ETApp" $$ showParseable e $$ parens (text "ETyp" <+> showParseable t))
--NOTE: erase all "proofs" for now (change the following two lines to change that) --NOTE: erase all "proofs" for now (change the following two lines to change that)
showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")" showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")" showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")"
@ -69,23 +70,26 @@ instance ShowParseable Match where
showParseable (Let d) = parens (text "MLet" <+> showParseable d) showParseable (Let d) = parens (text "MLet" <+> showParseable d)
instance ShowParseable Decl where instance ShowParseable Decl where
showParseable d = parens (text "Decl" <+> showParseable (dName d) <+> showParseable (dDefinition d)) showParseable d = parens (text "Decl" <+> showParseable (dName d)
$$ showParseable (dDefinition d))
instance ShowParseable DeclDef where instance ShowParseable DeclDef where
showParseable DPrim = text (show DPrim) showParseable DPrim = text (show DPrim)
showParseable (DExpr e) = parens (text "DExpr" <+> showParseable e) showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e)
instance ShowParseable DeclGroup where instance ShowParseable DeclGroup where
showParseable (Recursive ds) = parens (text "Recursive" <+> showParseable ds) showParseable (Recursive ds) =
showParseable (NonRecursive d) = parens (text "NonRecursive" <+> showParseable d) parens (text "Recursive" $$ showParseable ds)
showParseable (NonRecursive d) =
showParseableList :: (ShowParseable a) => [a] -> Doc parens (text "NonRecursive" $$ showParseable d)
showParseableList [] = empty
showParseableList [x] = showParseable x
showParseableList (x : y) = (showParseable x) <> comma <> showParseableList y
instance (ShowParseable a) => ShowParseable [a] where instance (ShowParseable a) => ShowParseable [a] where
showParseable a = brackets $ showParseableList a showParseable a = case a of
[] -> text "[]"
[x] -> brackets (showParseable x)
x : xs -> text "[" <+> showParseable x $$
vcat [ comma <+> showParseable y | y <- xs ] $$
text "]"
instance (ShowParseable a) => ShowParseable (Maybe a) where instance (ShowParseable a) => ShowParseable (Maybe a) where
showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote