8063cfd · Idris-dev · git.iko.soy

src/Core/CaseTree.hs+12−5

compare with master

unifiedsplit

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

2

3−module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

3+module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), Phase(..), CaseTree,

4 simpleCase, small, namesUsed, findCalls, findUsedArgs) where

5

6import Core.TT

@@ -139,11 +139,18 @@ findUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nub $ nu' sc) where

139 nua (ConstCase _ sc) = nu' sc

140 nua (DefaultCase sc) = nu' sc

141

142+data Phase = CompileTime | RunTime

143+ deriving (Show, Eq)

144+

145+-- Generate a simple case tree

146+--

147+

142−simpleCase :: Bool -> Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

148+simpleCase :: Bool -> Bool -> Phase -> FC -> [([Name], Term, Term)] -> TC CaseDef

143−simpleCase tc cover proj fc []

149+simpleCase tc cover phase fc []

144 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

150 = return $ CaseDef [] (UnmatchedCase "No pattern clauses") []

145−simpleCase tc cover proj fc cs

151+simpleCase tc cover phase fc cs

152+ = let proj = phase == RunTime

146− = let pats = map (\ (avs, l, r) ->

153+ pats = map (\ (avs, l, r) ->

147 (avs, reverse (toPats tc l), (l, r))) cs

154 (avs, reverse (toPats tc l), (l, r))) cs

148 chkPats = mapM chkAccessible pats in

155 chkPats = mapM chkAccessible pats in

149 case chkPats of

156 case chkPats of

src/Core/Evaluate.hs+2−2

@@ -691,8 +691,8 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

691 Type -> Context -> Context

692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

693 = let ctxt = definitions uctxt

694− ctxt' = case (simpleCase tcase covering False (FC "" 0) ps,

694+ ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

695− simpleCase tcase covering True (FC "" 0) psrt) of

695+ simpleCase tcase covering RunTime (FC "" 0) psrt) of

696 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

697 let inl = alwaysInline || small sc' in

698 addDef n (CaseOp inl ty ps args sc args' sc',

src/IRTS/CodegenC.hs+1

@@ -1,5 +1,6 @@

1module IRTS.CodegenC where

2

3+import Idris.AbsSyntax

3import IRTS.Bytecode

4import IRTS.Bytecode

4import IRTS.Lang

5import IRTS.Lang

5import IRTS.Simplified

6import IRTS.Simplified

src/IRTS/Compiler.hs+22−1

@@ -46,10 +46,16 @@ compile target f tm

46 iLOG "Inlining"

47 let defuns = inline defuns_in

48 logLvl 5 $ show defuns

49−

49+ iLOG "Resolving variables for CG"

50 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

51 let checked = checkDefs defuns (toAlist defuns)

52 dumpC <- getDumpC

53+ dumpCases <- getDumpCases

54+ case dumpCases of

55+ Nothing -> return ()

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

57+ liftIO $ writeFile f (showCaseTrees cs)

58+ iLOG "Building output"

53 case checked of

59 case checked of

54 OK c -> case target of

60 OK c -> case target of

55 ViaC -> liftIO $ codegenC dumpC c f True hdrs

61 ViaC -> liftIO $ codegenC dumpC c f True hdrs

@@ -67,6 +73,8 @@ compile target f tm

67 mkObj f = f ++ " "

73 mkObj f = f ++ " "

68 mkLib l = "-l" ++ l ++ " "

74 mkLib l = "-l" ++ l ++ " "

69

75

76+

77+

70irMain :: TT Name -> Idris LDecl

78irMain :: TT Name -> Idris LDecl

71irMain tm = do i <- ir tm

79irMain tm = do i <- ir tm

72 return $ LFun (MN 0 "runMain") [] (LForce i)

80 return $ LFun (MN 0 "runMain") [] (LForce i)

@@ -86,6 +94,19 @@ mkDecls t used

86 decls <- mapM build ds

94 decls <- mapM build ds

87 return decls

95 return decls

88

96

97+getCaseTrees :: [Name] -> Idris [(Name, Def)]

98+getCaseTrees used

99+ = do i <- getIState

100+ let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

101+ return ds

102+

103+showCaseTrees :: [(Name, Def)] -> String

104+showCaseTrees ds = showSep "\n\n" (map showCT ds)

105+ where

106+ showCT (n, CaseOp _ _ _ _ _ args sc)

107+ = show n ++ " " ++ showSep " " (map show args) ++ " = " ++ show sc

108+ showCT (n, _) = ""

109+

89isCon (TyDecl _ _) = True

110isCon (TyDecl _ _) = True

90isCon _ = False

111isCon _ = False

91

112

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+getDumpCases :: Idris (Maybe FilePath)

210+getDumpCases = do i <- get

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

212+ where findC [] = Nothing

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

214+ findC (_ : xs) = findC xs

215+

209logLevel :: Idris Int

216logLevel :: Idris Int

210logLevel = do i <- get

217logLevel = do i <- get

211 return (opt_logLevel (idris_options i))

218 return (opt_logLevel (idris_options i))

src/Idris/AbsSyntaxTree.hs+2

@@ -151,6 +151,7 @@ data Command = Quit

151 | HNF PTerm

152 | Defn Name

153 | Info Name

154+ | Missing Name

154 | DebugInfo Name

155 | DebugInfo Name

155 | Search PTerm

156 | Search PTerm

156 | SetOpt Opt

157 | SetOpt Opt

@@ -183,6 +184,7 @@ data Opt = Filename String

183 | Pkg String

184 | Pkg String

184 | BCAsm String

185 | BCAsm String

185 | DumpC String

186 | DumpC String

187+ | DumpCases String

186 | FOVM String

188 | FOVM String

187 deriving (Show, Eq)

189 deriving (Show, Eq)

188

190

src/Idris/Coverage.hs+87

@@ -14,6 +14,93 @@ import Data.List

14import Data.Either

15import Debug.Trace

16

17+import Control.Monad.State

18+

19+-- Generate the LHSes which are missing from a case tree

20+-- Eliminate the ones which cannot be well typed

21+

22+genMissing :: [Name] -> SC -> Idris [PTerm]

23+genMissing args sc = do sc' <- expandTree sc

24+ iputStrLn (show sc')

25+ gm (map (\x -> P Bound x Erased) args) sc'

26+

27+gm :: [TT Name] -> SC -> Idris [PTerm]

28+gm args (Case n alts) = do m <- mapM (gmAlt args n) alts

29+ return (concat m)

30+gm args (STerm tm) = do iputStrLn ("Covered: " ++ show args)

31+ return []

32+gm args (UnmatchedCase _) = do iputStrLn ("Missing: " ++ show args)

33+ return []

34+

35+gmAlt args n (ConCase cn t cargs sc)

36+ = do let args' = map (subst n (mkApp (P Bound cn Erased)

37+ (map (\x -> P Bound x Erased) cargs))) args

38+ gm args' sc

39+gmAlt args n (ConstCase c sc)

40+ = do let args' = map (subst n (Constant c)) args

41+ gm args' sc

42+gmAlt args n (DefaultCase sc)

43+ = do gm args sc

44+

45+getDefault (DefaultCase sc : _) = sc

46+getDefault (_ : cs) = getDefault cs

47+getDefault [] = UnmatchedCase ""

48+

49+dropDefault (DefaultCase sc : rest) = dropDefault rest

50+dropDefault (c : cs) = c : dropDefault cs

51+dropDefault [] = []

52+

53+expandTree :: SC -> Idris SC

54+expandTree (Case n alts) = do i <- get

55+ as <- expandAlts i (dropDefault alts) (getDefault alts)

56+ alts' <- mapM expandTreeA as

57+ return (Case n alts')

58+ where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc

59+ return (ConCase n i ns sc')

60+ expandTreeA (ConstCase i sc) = do sc' <- expandTree sc

61+ return (ConstCase i sc')

62+ expandTreeA (DefaultCase sc) = do sc' <- expandTree sc

63+ return (DefaultCase sc')

64+expandTree t = return t

65+

66+expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]

67+expandAlts i all@(ConstCase c _ : alts) def

68+ = return $ all ++ [DefaultCase def]

69+expandAlts i all@(ConCase n _ _ _ : alts) def

70+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

71+ = do let tyn = getTy n (tt_ctxt i)

72+ case lookupCtxt Nothing tyn (idris_datatypes i) of

73+ (TI ns : _) -> do let ps = map mkPat ns

74+ return $ addAlts ps (altsFor all) all

75+ _ -> return all

76+ where

77+ altsFor [] = []

78+ altsFor (ConCase n _ _ _ : alts) = n : altsFor alts

79+ altsFor (_ : alts) = altsFor alts

80+

81+ addAlts [] got alts = alts

82+ addAlts ((n, arity) : ps) got alts

83+ | n `elem` got = addAlts ps got alts

84+ | otherwise = addAlts ps got (alts ++ [ConCase n (-1) (argList arity) def])

85+

86+ argList i = take i (map (\x -> (MN x "ign")) [0..])

87+

88+ getTy n ctxt = case lookupTy Nothing n ctxt of

89+ (t : _) -> case unApply (getRetTy t) of

90+ (P _ tyn _, _) -> tyn

91+ x -> error $ "Can't happen getTy 1 " ++ show (n, x)

92+ _ -> error "Can't happen getTy 2"

93+

94+ mkPat x = case lookupCtxt Nothing x (idris_implicits i) of

95+ (pargs : _)

96+ -> (x, length pargs)

97+ _ -> error "Can't happen - genAll"

98+expandAlts i alts def = return alts

99+

100+

101+

102+-- OLD STUFF: probably broken...

103+

17-- Given a list of LHSs, generate a extra clauses which cover the remaining

104-- Given a list of LHSs, generate a extra clauses which cover the remaining

18-- cases. The ones which haven't been provided are marked 'absurd' so that the

105-- cases. The ones which haven't been provided are marked 'absurd' so that the

19-- checker will make sure they can't happen.

106-- checker will make sure they can't happen.

src/Idris/ElabDecls.hs+2−2

@@ -268,7 +268,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

268-- return False

269 else return False

270 pdef' <- applyOpts pdef

271− tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover False fc pdef

271+ tree@(CaseDef _ sc _) <- tclift $ simpleCase tcase pcover CompileTime fc pdef

272 ist <- get

273-- let wf = wellFounded ist n sc

274 let tot = if pcover || AssertTotal `elem` opts

@@ -287,7 +287,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

287 iputStrLn $ show fc ++

288 ":warning - Unreachable case: " ++

289 show (delab ist x)) xs

290− tree' <- tclift $ simpleCase tcase pcover True fc pdef'

290+ tree' <- tclift $ simpleCase tcase pcover RunTime fc pdef'

291 logLvl 3 (show tree)

292 logLvl 3 $ "Optimised: " ++ show tree'

293 ctxt <- getContext

src/Idris/Prover.hs+1−1

@@ -46,7 +46,7 @@ prove ctxt lit n ty

46 i <- get

47 let proofs = proof_list i

48 put (i { proof_list = (n, prf) : proofs })

49− let tree = simpleCase False True False (FC "proof" 0) [([], P Ref n ty, tm)]

49+ let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

50 logLvl 3 (show tree)

51 (ptm, pty) <- recheckC (FC "proof" 0) [] tm

52 ptm' <- applyOpts ptm

src/Idris/REPL.hs+9

@@ -323,6 +323,13 @@ process fn (Compile target f)

323 compile target f m

324 where fc = FC "main" 0

325process fn (LogLvl i) = setLogLevel i

326+process fn (Missing n) = do i <- get

327+ case lookupDef Nothing n (tt_ctxt i) of

328+ [CaseOp _ _ _ args t _ _]

329+ -> do tms <- genMissing args t

330+ iputStrLn (show tms)

331+ [] -> iputStrLn $ show n ++ " undefined"

332+ _ -> iputStrLn $ "Ambiguous name"

326process fn Metavars

333process fn Metavars

327 = do ist <- get

334 = do ist <- get

328 let mvs = idris_metavars ist \\ primDefs

335 let mvs = idris_metavars ist \\ primDefs

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

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

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

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

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

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

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

411+parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

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

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

405

413

406help =

414help =

@@ -408,6 +416,7 @@ help =

408 ([""], "", ""),

416 ([""], "", ""),

409 (["<expr>"], "", "Evaluate an expression"),

417 (["<expr>"], "", "Evaluate an expression"),

410 ([":t"], "<expr>", "Check the type of an expression"),

418 ([":t"], "<expr>", "Check the type of an expression"),

419+ ([":miss", ":missing"], "<name>", "Show missing clauses"),

411 ([":i", ":info"], "<name>", "Display information about a type class"),

420 ([":i", ":info"], "<name>", "Display information about a type class"),

412 ([":total"], "<name>", "Check the totality of a name"),

421 ([":total"], "<name>", "Check the totality of a name"),

413 ([":r",":reload"], "", "Reload current file"),

422 ([":r",":reload"], "", "Reload current file"),

src/Idris/REPLParser.hs+1

@@ -44,6 +44,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

44 <|> try (do cmd ["u", "universes"]; eof; return Universes)

45 <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))

46 <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))

47+ <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))

47 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

48 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

48 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

49 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

49 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))

50 <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))