Skip to content

Commit

Permalink
Use ppInductives from main
Browse files Browse the repository at this point in the history
Don't print BuiltinList as its now declared implicitly
  • Loading branch information
paulcadman committed Aug 9, 2024
1 parent 2d81867 commit 7334f1c
Showing 1 changed file with 15 additions and 1 deletion.
16 changes: 15 additions & 1 deletion src/Juvix/Compiler/Core/Pretty/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -560,7 +560,7 @@ instance PrettyCode InfoTable where

ppInductives :: [InductiveInfo] -> Sem r (Doc Ann)
ppInductives inds = do
inds' <- mapM ppInductive (filter (isNothing . (^. inductiveBuiltin)) inds)
inds' <- mapM ppInductive (filter (shouldPrintInductive . (^. inductiveBuiltin)) inds)
return (vsep inds')
where
ppInductive :: InductiveInfo -> Sem r (Doc Ann)
Expand All @@ -569,6 +569,20 @@ instance PrettyCode InfoTable where
ctrs <- mapM (fmap (<> semi) . ppCode . lookupTabConstructorInfo tbl) (ii ^. inductiveConstructors)
return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line) <> kwSemicolon)

shouldPrintInductive :: Maybe BuiltinType -> Bool
shouldPrintInductive = \case
Just (BuiltinTypeInductive i) -> case i of
BuiltinList -> False
BuiltinMaybe -> False
BuiltinPair -> True
BuiltinPoseidonState -> True
BuiltinEcPoint -> True
BuiltinNat -> False
BuiltinInt -> False
BuiltinBool -> False
Just _ -> False
Nothing -> True

instance PrettyCode AxiomInfo where
ppCode ii = do
name <- ppName KNameAxiom (ii ^. axiomName)
Expand Down

0 comments on commit 7334f1c

Please sign in to comment.