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

src/Core/Unify.hs+3−3

compare with master

unifiedsplit

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

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

26 Injs, Fails)

27unify ctxt env topx topy

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

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

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

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

30− _ ->

30+ -- _ ->

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

32 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

src/IRTS/Compiler.hs+4

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

51 let checked = checkDefs defuns (toAlist defuns)

52 dumpC <- getDumpC

53 dumpCases <- getDumpCases

54+ dumpDefun <- getDumpDefun

54 case dumpCases of

55 case dumpCases of

55 Nothing -> return ()

56 Nothing -> return ()

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

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

57 liftIO $ writeFile f (showCaseTrees cs)

58 liftIO $ writeFile f (showCaseTrees cs)

59+ case dumpDefun of

60+ Nothing -> return ()

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

58 iLOG "Building output"

62 iLOG "Building output"

59 case checked of

63 case checked of

60 OK c -> case target of

64 OK c -> case target of

src/IRTS/Defunctionalise.hs+9−1

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

174

175instance Show DExp where

176 show e = show' [] e where

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

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

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

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

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

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

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

238 tagLT i (DDefaultCase _) = False

239

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

5import IRTS.Defunctionalise

6

7inline :: 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

9

20

src/Idris/AbsSyntax.hs+7

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

206 findC (DumpC x : _) = Just x

207 findC (_ : xs) = findC xs

208

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+

209getDumpCases :: Idris (Maybe FilePath)

216getDumpCases :: Idris (Maybe FilePath)

210getDumpCases = do i <- get

217getDumpCases = do i <- get

211 return $ findC (opt_cmdline (idris_options i))

218 return $ findC (opt_cmdline (idris_options i))

src/Idris/AbsSyntaxTree.hs+1

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

185 | Pkg String

186 | BCAsm String

187 | DumpC String

188+ | DumpDefun String

188 | DumpCases String

189 | DumpCases String

189 | FOVM String

190 | FOVM String

190 deriving (Show, Eq)

191 deriving (Show, Eq)

src/Idris/ElabTerm.hs+2

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

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

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

242 solve)

243+ -- ptm <- get_term

244+ -- elog (show ptm)

243 ivs' <- get_instances

245 ivs' <- get_instances

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

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

245 mapM_ (\n -> do focus n

247 mapM_ (\n -> do focus n

src/Idris/REPL.hs+1

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

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

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

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

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

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

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

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

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

418

419