@@ -54,8 +54,7 @@ compile target f tm
5454 dumpDefun <- getDumpDefun
5555 case dumpCases of
5656 Nothing -> return ()
57− Just f -> do cs <- getCaseTrees (concat used)
58− liftIO $ writeFile f (showCaseTrees cs)
57+ Just f -> liftIO $ writeFile f (showCaseTrees tagged)
5958 case dumpDefun of
6059 Nothing -> return ()
6160 Just f -> liftIO $ writeFile f (dumpDefuns defuns)
@@ -99,18 +98,13 @@ mkDecls t used
9998 decls <- mapM build ds
10099 return decls
101100
102−getCaseTrees :: [Name] -> Idris [(Name, Def)]
103−getCaseTrees used
104− = do i <- getIState
105− let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
106− return ds
107−
108−showCaseTrees :: [(Name, Def)] -> String
101+showCaseTrees :: [(Name, LDecl)] -> String
109102showCaseTrees ds = showSep "\n\n" (map showCT ds)
110103 where
111− showCT (n, CaseOp _ _ _ _ _ args sc)
112− = show n ++ " " ++ showSep " " (map show args) ++ " = " ++ show sc
113− showCT (n, _) = ""
104+ showCT (n, LFun f args lexp)
105+ = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
106+ ++ show lexp
107+ showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
114108
115109isCon (TyDecl _ _) = True
116110isCon _ = False