3c641ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added --dumpdefuns flag

commit3c641ae4ac27323190b65004b826af929db3b1cb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 17 Oct 2012, 14:41 (14 years ago) parent9469ba8

8 files changed+39−5

compare with master

unifiedsplit

src/Core/Unify.hs+3−3 src/IRTS/Compiler.hs+4 src/IRTS/Defunctionalise.hs+9−1 src/IRTS/Inliner.hs+12−1 src/Idris/AbsSyntax.hs+7 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+2 src/Idris/REPL.hs+1

src/Core/Unify.hs+3−3

@@ -25,9 +25,9 @@ data UInfo = UI Int Injs Fails

2525unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

2626 Injs, Fails)

2727unify ctxt env topx topy

28− = case runStateT (un' False [] topx topy) (UI 0 [] []) of

29− OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30− _ ->

28+ = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of

29+ -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30+ -- _ ->

3131 -- trace ("Unifying " ++ show (topx, topy)) $

3232 let topxn = normalise ctxt env topx

3333 topyn = normalise ctxt env topy in

src/IRTS/Compiler.hs+4

@@ -51,10 +51,14 @@ compile target f tm

5151 let checked = checkDefs defuns (toAlist defuns)

5252 dumpC <- getDumpC

5353 dumpCases <- getDumpCases

54+ dumpDefun <- getDumpDefun

5455 case dumpCases of

5556 Nothing -> return ()

5657 Just f -> do cs <- getCaseTrees (concat used)

5758 liftIO $ writeFile f (showCaseTrees cs)

59+ case dumpDefun of

60+ Nothing -> return ()

61+ Just f -> liftIO $ writeFile f (dumpDefuns defuns)

5862 iLOG "Building output"

5963 case checked of

6064 OK c -> case target of

src/IRTS/Defunctionalise.hs+9−1

@@ -174,7 +174,7 @@ mkUnderCon n missing = MN missing ("U_" ++ show n)

174174

175175instance Show DExp where

176176 show e = show' [] e where

177− show' env (DV (Loc i)) = env!!i

177+ show' env (DV (Loc i)) = "var " ++ env!!i

178178 show' env (DV (Glob n)) = show n

179179 show' env (DApp _ e args) = show e ++ "(" ++

180180 showSep ", " (map (show' env) args) ++")"

@@ -237,3 +237,11 @@ groupsOf x xs = let (batch, rest) = span (tagLT (x + tagHead xs)) xs in

237237 tagLT i (DConCase j _ _ _) = i < j

238238 tagLT i (DDefaultCase _) = False

239239

240+dumpDefuns :: DDefs -> String

241+dumpDefuns ds = showSep "\n" $ map showDef (toAlist ds)

242+ where showDef (x, DFun fn args exp)

243+ = show fn ++ "(" ++ showSep ", " (map show args) ++ ") = \n\t" ++

244+ show exp ++ "\n"

245+ showDef (x, DConstructor n t a) = "Constructor " ++ show n ++ " " ++ show t

246+

247+

src/IRTS/Inliner.hs+12−1

@@ -5,5 +5,16 @@ import Core.TT

55import IRTS.Defunctionalise

77inline :: DDefs -> DDefs

8−inline xs = xs

8+inline xs = let sep = toAlist xs

9+ inls = map (inl xs) sep in

10+ addAlist inls emptyContext

11+

12+inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)

13+inl ds d@(n, DFun n' args exp)

14+ = case evalD ds exp of

15+ Just exp' -> (n, DFun n' args exp')

16+ _ -> d

17+inl ds d = d

18+

19+evalD _ e = Just e

920

src/Idris/AbsSyntax.hs+7

@@ -206,6 +206,13 @@ getDumpC = do i <- get

206206 findC (DumpC x : _) = Just x

207207 findC (_ : xs) = findC xs

208208

209+getDumpDefun :: Idris (Maybe FilePath)

210+getDumpDefun = do i <- get

211+ return $ findC (opt_cmdline (idris_options i))

212+ where findC [] = Nothing

213+ findC (DumpDefun x : _) = Just x

214+ findC (_ : xs) = findC xs

215+

209216getDumpCases :: Idris (Maybe FilePath)

210217getDumpCases = do i <- get

211218 return $ findC (opt_cmdline (idris_options i))

src/Idris/AbsSyntaxTree.hs+1

@@ -185,6 +185,7 @@ data Opt = Filename String

185185 | Pkg String

186186 | BCAsm String

187187 | DumpC String

188+ | DumpDefun String

188189 | DumpCases String

189190 | FOVM String

190191 deriving (Show, Eq)

src/Idris/ElabTerm.hs+2

@@ -240,6 +240,8 @@ elab ist info pattern tcgen fn tm

240240 (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)

241241 mkSpecialised ist fc f (map getTm args') tm

242242 solve)

243+ -- ptm <- get_term

244+ -- elog (show ptm)

243245 ivs' <- get_instances

244246 when (not pattern || (ina && not tcgen)) $

245247 mapM_ (\n -> do focus n

src/Idris/REPL.hs+1

@@ -413,6 +413,7 @@ parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

413413parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

414414parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

415415parseArgs ("--dumpc":n:ns) = DumpC n : (parseArgs ns)

416+parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

416417parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

417418parseArgs (n:ns) = Filename n : (parseArgs ns)

418419