baaba44 · Idris-dev · git.iko.soy

samples/interp.idr+2−3

@@ -77,7 +77,6 @@ testFac : Int

7777testFac = interp [] eFac 4

7878

7979main : IO ()

80−main = do { print testFac

81− print test }

82−

80+main = do print test

81+ print testFac

8382

src/Core/Elaborate.hs+6−3

@@ -406,13 +406,16 @@ try t1 t2 = do s <- get

406406tryAll :: [(Elab' aux a, String)] -> Elab' aux a

407407tryAll xs = tryAll' [] (fail "Nothing to try") (map fst xs)

408408 where

409+ cantResolve :: Elab' aux a

410+ cantResolve = fail $ "Couldn't resolve alternative: "

411+ ++ showSep ", " (map snd xs)

412+

409413 tryAll' :: [Elab' aux a] -> -- successes

410414 Elab' aux a -> -- last failure

411415 [Elab' aux a] -> -- still to try

412416 Elab' aux a

413− tryAll' [res] _ [] = res

414− tryAll' (_:_) _ [] = fail $ "Couldn't resolve alternative: "

415− ++ showSep ", " (map snd xs)

417+ tryAll' [res] _ [] = res

418+ tryAll' (_:_) _ [] = cantResolve

416419 tryAll' [] f [] = f

417420 tryAll' cs f (x:xs) = do s <- get

418421 case runStateT x s of

src/Core/Evaluate.hs+20−14

@@ -120,7 +120,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

120120 [(Function _ tm, Public)] -> ev True env tm

121121 [(TyDecl nt ty, _)] -> do vty <- ev True env ty

122122 return $ VP nt n vty

123− [(CaseOp inl _ _ [] tree, Public)] ->

123+ [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version

124124 if simpl && (not inl)

125125 then liftM (VP Ref n) (ev top env ty)

126126 else do c <- evCase top env [] [] tree

@@ -162,7 +162,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

162162 apply False env f args

163163 | spec = return $ unload env f args

164164 apply top env (VP Ref n ty) args

165− | [(CaseOp inl _ _ ns tree, Public)] <- lookupDefAcc Nothing n atRepl ctxt

165+ | [(CaseOp inl _ _ ns tree _ _, Public)] <- lookupDefAcc Nothing n atRepl ctxt

166166 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

167167 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

168168 else do c <- evCase top env ns args tree

@@ -309,7 +309,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

309309 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

310310 [Function _ t] -> ev env t

311311 [TyDecl nt ty] -> return $ HP nt n ty

312− [CaseOp inl _ _ [] tree] ->

312+ [CaseOp inl _ _ [] tree _ _] ->

313313 do c <- evCase env [] [] tree

314314 case c of

315315 (Nothing, _, _) -> return $ HP Ref n ty

@@ -339,7 +339,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

339339 app <- apply env sc' as

340340 wknH (-1) app

341341 apply env (HP Ref n ty) args

342− | [CaseOp _ _ _ ns tree] <- lookupDef Nothing n ctxt

342+ | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt

343343 = do c <- evCase env ns args tree

344344 case c of

345345 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args

@@ -439,7 +439,9 @@ spec ctxt statics genv tm = error "spec undefined"

439439data Def = Function Type Term

440440 | TyDecl NameType Type

441441 | Operator Type Int ([Value] -> Maybe Value)

442− | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

442+ | CaseOp Bool Type [(Term, Term)] -- Bool for inlineable

443+ [Name] SC -- Compile time case definition

444+ [Name] SC -- Run time cae definitions

443445{-!

444446deriving instance Binary Def

445447!-}

@@ -448,8 +450,10 @@ instance Show Def where

448450 show (Function ty tm) = "Function: " ++ show (ty, tm)

449451 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

450452 show (Operator ty _ _) = "Operator: " ++ show ty

451− show (CaseOp _ ty ps ns sc) = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

452− show ns ++ " " ++ show sc

453+ show (CaseOp _ ty ps ns sc ns' sc')

454+ = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

455+ show ns ++ " " ++ show sc ++ "\n" ++

456+ show ns' ++ " " ++ show sc'

453457-- We need this for serialising Def. Fortunately, it never gets used because

454458-- we'll never serialise a primitive operator

455459

@@ -516,13 +520,15 @@ addDatatype (Data n tag ty cons) uctxt

516520 addCons (tag+1) cons (addDef n

517521 (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

518522

519−addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

520−addCasedef n alwaysInline tcase ps ty uctxt

523+addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> [(Term, Term)] ->

524+ Type -> Context -> Context

525+addCasedef n alwaysInline tcase ps psrt ty uctxt

521526 = let ctxt = definitions uctxt

522527 ps' = ps -- simpl ps in

523− ctxt' = case simpleCase tcase ps' of

524− CaseDef args sc -> let inl = alwaysInline in

525− addDef n (CaseOp inl ty ps args sc,

528+ ctxt' = case (simpleCase tcase ps', simpleCase tcase psrt) of

529+ (CaseDef args sc, CaseDef args' sc') ->

530+ let inl = alwaysInline in

531+ addDef n (CaseOp inl ty ps args sc args' sc',

526532 Public) ctxt in

527533 uctxt { definitions = ctxt' }

528534 where simpl [] = []

@@ -541,7 +547,7 @@ lookupTy root n ctxt

541547 (Function ty _) -> return ty

542548 (TyDecl _ ty) -> return ty

543549 (Operator ty _ _) -> return ty

544− (CaseOp _ ty _ _ _) -> return ty

550+ (CaseOp _ ty _ _ _ _ _) -> return ty

545551

546552isConName :: Maybe [String] -> Name -> Context -> Bool

547553isConName root n ctxt

@@ -557,7 +563,7 @@ lookupP root n ctxt

557563 p <- case def of

558564 (Function ty tm, a) -> return (P Ref n ty, a)

559565 (TyDecl nt ty, a) -> return (P nt n ty, a)

560− (CaseOp _ ty _ _ _, a) -> return (P Ref n ty, a)

566+ (CaseOp _ ty _ _ _ _ _, a) -> return (P Ref n ty, a)

561567 (Operator ty _ _, a) -> return (P Ref n ty, a)

562568 case snd p of

563569 Hidden -> []

src/Idris/AbsSyntax.hs+1−1

280280 | Compile String | Execute | ExecVal PTerm

281281 | Metavars | Prove Name | AddProof | Universes

282282 | TTShell

283− | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

284284 | NOP

285285

286286-- Parsed declarations

src/Idris/Compiler.hs+5−5

@@ -72,7 +72,7 @@ impossible = int 42424242

7272

7373instance ToEpic Def where

7474 epic (Function tm _) = epic tm

75− epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

75+ epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version

7676 epic _ = return impossible

7777

7878instance ToEpic (TT Name) where

@@ -80,10 +80,10 @@ instance ToEpic (TT Name) where

8080 epic' env tm@(App f a)

8181 | (P _ (UN "mkForeign") _, args) <- unApply tm

8282 = doForeign args

83− | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

83+ | (P _ (UN "lazy") _, [_,arg]) <- unApply tm

8484 = do arg' <- epic' env arg

8585 return $ lazy_ arg'

86− | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm

86+ | (P _ (UN "prim__IO") _, [v]) <- unApply tm

8787 = epic' env v

8888 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

8989 = do v' <- epic' env v

@@ -137,8 +137,8 @@ doForeign (_ : fgn : args)

137137

138138getFTypes :: TT Name -> [E.Type]

139139getFTypes tm = case unApply tm of

140− (nil, [arg]) -> []

141− (cons, [a, (P _ (UN ty) _), xs]) ->

140+ (nil, []) -> []

141+ (cons, [(P _ (UN ty) _), xs]) ->

142142 let rest = getFTypes xs in

143143 mkEty ty : rest

144144

src/Idris/DataOpts.hs+59−9

@@ -15,7 +15,6 @@ import Debug.Trace

1515-- optimisations

1616

1717forceArgs :: Name -> Type -> Idris ()

18−-- forceArgs n t = return ()

1918forceArgs n t = do let fargs = force 0 t

2019 i <- getIState

2120 copt <- case lookupCtxt Nothing n (idris_optimisation i) of

@@ -24,17 +23,18 @@ forceArgs n t = do let fargs = force 0 t

2423 let opts = addDef n (copt { forceable = fargs }) (idris_optimisation i)

2524 putIState (i { idris_optimisation = opts })

2625 addIBC (IBCOpt n)

27− iLOG $ "Forced: " ++ show n ++ " " ++ show fargs

26+ iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++

27+ show t

2828 where

2929 force :: Int -> Term -> [Int]

3030 force i (Bind _ (Pi _) sc)

31− = force (i + 1) $ instantiate (P Bound (MN i "F?") Erased) sc

31+ = force (i + 1) $ instantiate (P Bound (MN i "?") Erased) sc

3232 force _ sc@(App f a)

3333 | (_, args) <- unApply sc

3434 = nub $ concatMap guarded args

3535 force _ _ = []

3636

37− isF (P _ (MN force "F?") _) = Just force

37+ isF (P _ (MN force "?") _) = Just force

3838 isF _ = Nothing

3939

4040 guarded :: Term -> [Int]

@@ -48,17 +48,27 @@ forceArgs n t = do let fargs = force 0 t

4848class Optimisable term where

4949 applyOpts :: term -> Idris term

5050

51+instance (Optimisable a, Optimisable b) => Optimisable (a, b) where

52+ applyOpts (x, y) = do x' <- applyOpts x

53+ y' <- applyOpts y

54+ return (x', y')

55+

56+instance Optimisable a => Optimisable [a] where

57+ applyOpts = mapM applyOpts

58+

5159-- Raw is for compile time optimisation (before type checking)

5260-- Term is for run time optimisation (after type checking, collapsing allowed)

5361

62+-- Compile time: no collapsing

63+

5464instance Optimisable Raw where

5565 applyOpts t@(RApp f a)

5666 | (Var n, args) <- raw_unapply t -- MAGIC HERE

57− = do i <- getIState

67+ = do args' <- mapM applyOpts args

68+ i <- getIState

5869 case lookupCtxt Nothing n (idris_optimisation i) of

59− (oi:_) -> return $ applyDataOpt oi n args

60− _ -> do args' <- mapM applyOpts args

61− return (raw_apply (Var n) args')

70+ (oi:_) -> return $ applyDataOpt oi n args'

71+ _ -> return (raw_apply (Var n) args')

6272 | otherwise = do f' <- applyOpts f

6373 a' <- applyOpts a

6474 return (RApp f' a')

@@ -75,7 +85,6 @@ instance Optimisable t => Optimisable (Binder t) where

7585 applyOpts b = do t' <- applyOpts (binderTy b)

7686 return (b { binderTy = t' })

7787

78−-- Compile time: no collapsing

7988

8089applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

8190applyDataOpt oi n args

@@ -86,3 +95,44 @@ applyDataOpt oi n args

8695 doForce True a = RForce a

8796 doForce False a = a

8897

98+-- Run-time: do everything

99+

100+instance Optimisable (TT Name) where

101+ applyOpts t@(App f a)

102+ | (c@(P (DCon t arity) n _), args) <- unApply t -- MAGIC HERE

103+ = do args' <- mapM applyOpts args

104+ i <- getIState

105+ case lookupCtxt Nothing n (idris_optimisation i) of

106+ (oi:_) -> do return $ applyDataOptRT oi n t arity args'

107+ _ -> return (mkApp c args')

108+ | otherwise = do f' <- applyOpts f

109+ a' <- applyOpts a

110+ return (App f' a')

111+ applyOpts (Bind n b t) = do b' <- applyOpts b

112+ t' <- applyOpts t

113+ return (Bind n b' t')

114+ applyOpts t = return t

115+

116+-- Need to saturate arguments first to ensure that erasure happens uniformly

117+

118+applyDataOptRT :: OptInfo -> Name -> Int -> Int -> [Term] -> Term

119+applyDataOptRT oi n tag arity args

120+ | length args == arity = doOpts n args (collapsible oi) (forceable oi)

121+ | otherwise = let extra = satArgs (arity - length args)

122+ tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

123+ (collapsible oi) (forceable oi) in

124+ bind extra tm

125+ where

126+ satArgs n = map (\i -> MN i "sat") [1..n]

127+

128+ bind [] tm = tm

129+ bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))

130+

131+ doOpts n args True f = Erased

132+ doOpts n args _ forced

133+ = let args' = filter keep (zip (map (\x -> x `elem` forced) [0..])

134+ args) in

135+ mkApp (P (DCon tag (arity - length forced)) n Erased) (map snd args')

136+

137+ keep (forced, _) = not forced

138+

src/Idris/Delaborate.hs+1

@@ -31,6 +31,7 @@ delab' ist tm fullname = de [] tm

3131 = PLet n (de env ty) (de env val) (de (n:env) sc)

3232 de env (Bind n _ sc) = de (n:env) sc

3333 de env (Constant i) = PConstant i

34+ de env Erased = Placeholder

3435 de env (Set i) = PSet

3536

3637 dens x | fullname = x

src/Idris/ElabDecls.hs+7−4

@@ -25,8 +25,8 @@ import Debug.Trace

2525

2626

2727recheckC ctxt fc env t

28− = do t' <- applyOpts (forget t)

29− (tm, ty, cs) <- tclift $ recheck ctxt env t' t

28+ = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

29+ (tm, ty, cs) <- tclift $ recheck ctxt env (forget t) t

3030 addConstraints fc cs

3131 return (tm, ty)

3232

@@ -107,13 +107,16 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

107107 ist <- get

108108 let tcase = opt_typecase (idris_options ist)

109109 let pdef = map debind pats

110− let tree = simpleCase tcase pdef

110+ pdef' <- applyOpts pdef

111+ let tree = simpleCase tcase pdef

112+ let tree' = simpleCase tcase pdef'

111113 tclift $ sameLength pdef

112114 logLvl 3 (show tree)

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

113116 ctxt <- getContext

114117 case lookupTy (namespace info) n ctxt of

115118 [ty] -> do updateContext (addCasedef n (inlinable opts)

116− tcase pdef ty)

119+ tcase pdef pdef' ty)

117120 addIBC (IBCDef n)

118121 [] -> return ()

119122 where

src/Idris/IBC.hs+12−8

@@ -22,7 +22,7 @@ import System.Directory

2222import Paths_idris

2323

2424ibcVersion :: Word8

25−ibcVersion = 5

25+ibcVersion = 6

2626

2727data IBCFile = IBCFile { ver :: Word8,

2828 sourcefile :: FilePath,

@@ -509,12 +509,14 @@ instance Binary Def where

509509 put x1

510510 put x2

511511 put x3

512− CaseOp x1 x2 x3 x4 x5 -> do putWord8 3

513− put x1

514− put x2

515− put x3

516− put x4

517− put x5

512+ CaseOp x1 x2 x3 x4 x5 x6 x7 -> do putWord8 3

513+ put x1

514+ put x2

515+ put x3

516+ put x4

517+ put x5

518+ put x6

519+ put x7

518520 get

519521 = do i <- getWord8

520522 case i of

@@ -533,7 +535,9 @@ instance Binary Def where

533535 x3 <- get

534536 x4 <- get

535537 x5 <- get

536− return (CaseOp x1 x2 x3 x4 x5)

538+ x6 <- get

539+ x7 <- get

540+ return (CaseOp x1 x2 x3 x4 x5 x6 x7)

537541 _ -> error "Corrupted binary data for Def"

538542

539543instance Binary Accessibility where

src/Idris/Prover.hs+4−1

@@ -12,6 +12,7 @@ import Idris.ElabDecls

1212import Idris.ElabTerm

1313import Idris.Parser

1414import Idris.Error

15+import Idris.DataOpts

1516

1617import System.Console.Haskeline

1718import Control.Monad.State

@@ -41,7 +42,9 @@ prove ctxt n ty

4142 let tree = simpleCase False [(P Ref n ty, tm)]

4243 logLvl 3 (show tree)

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

44− updateContext (addCasedef n True False [(P Ref n ty, ptm)] ty)

45+ ptm' <- applyOpts ptm

46+ updateContext (addCasedef n True False [(P Ref n ty, ptm)]

47+ [(P Ref n ty, ptm')] ty)

4548 solveDeferred n

4649

4750elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

src/Idris/REPL.hs+3

@@ -165,6 +165,9 @@ process Universes = do i <- get

165165 OK _ -> iputStrLn "Universes OK"

166166process (Defn n) = do ctxt <- getContext

167167 liftIO $ print (lookupDef Nothing n ctxt)

168+process (Info n) = do i <- get

169+ let oi = lookupCtxt Nothing n (idris_optimisation i)

170+ liftIO $ print oi

168171process (Spec t) = do (tm, ty) <- elabVal toplevel False t

169172 ctxt <- getContext

170173 ist <- get

src/Idris/REPLParser.hs+1

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

3636 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

3737 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

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

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

3940 <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

4041 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

4142 <|> do eof; return NOP