02881b1 · Idris-dev · git.iko.soy

idris.cabal+1

@@ -34,6 +34,7 @@ Executable idris

3434 Idris.Delaborate, Idris.Primitives, Idris.Imports,

3535 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

3636 Idris.Coverage, Idris.IBC, Idris.Unlit,

37+ Idris.DataOpts

3738

3839 Paths_idris

3940

src/Core/Evaluate.hs+3

@@ -31,6 +31,7 @@ data Value = VP NameType Name Value

3131 | VBind Name (Binder Value) (Value -> Eval Value)

3232 | VApp Value Value

3333 | VSet UExp

34+ | VErased

3435 | VConstant Const

3536 | VTmp Int

3637

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

147148 a' <- ev False env a

148149 evApply top env [a'] f'

149150 ev top env (Constant c) = return $ VConstant c

151+ ev top env Erased = return VErased

150152 ev top env (Set i) = return $ VSet i

151153

152154 evApply top env args (VApp f a) =

@@ -259,6 +261,7 @@ instance Quote Value where

259261 where quoteB t = fmapMB (quote i) t

260262 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

261263 quote i (VSet u) = return $ Set u

264+ quote i VErased = return $ Erased

262265 quote i (VConstant c) = return $ Constant c

263266 quote i (VTmp x) = return $ V (i - x - 1)

264267

src/Core/ProofState.hs+1−1

@@ -436,7 +436,7 @@ updateSolved xs t = t

436436processTactic :: Tactic -> ProofState -> TC (ProofState, String)

437437processTactic QED ps = case holes ps of

438438 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)

439− (tm', ty', _) <- recheck (context ps) [] tm

439+ (tm', ty', _) <- recheck (context ps) [] (forget tm) tm

440440 return (ps { done = True, pterm = tm' },

441441 "Proof complete: " ++ showEnv [] tm')

442442 _ -> fail "Still holes to fill."

src/Core/TT.hs+15−2

@@ -173,7 +173,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

173173

174174data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

176− | PtrType

176+ | PtrType | Forgot

177177 deriving Eq

178178{-!

179179deriving instance Binary Const

@@ -183,6 +183,7 @@ data Raw = Var Name

183183 | RBind Name (Binder Raw) Raw

184184 | RApp Raw Raw

185185 | RSet

186+ | RForce Raw

186187 | RConstant Const

187188 deriving (Show, Eq)

188189{-!

@@ -221,6 +222,11 @@ raw_apply :: Raw -> [Raw] -> Raw

221222raw_apply f [] = f

222223raw_apply f (a : as) = raw_apply (RApp f a) as

223224

225+raw_unapply :: Raw -> (Raw, [Raw])

226+raw_unapply t = ua [] t where

227+ ua args (RApp f a) = ua (a:args) f

228+ ua args t = (t, args)

229+

224230data RawFun = RawFun { rtype :: Raw,

225231 rval :: Raw

226232 }

@@ -284,6 +290,7 @@ data TT n = P NameType n (TT n) -- embed type

284290 | Bind n (Binder (TT n)) (TT n)

285291 | App (TT n) (TT n) -- function, function type, arg

286292 | Constant Const

293+ | Erased

287294 | Set UExp

288295 deriving Functor

289296{-!

@@ -305,6 +312,8 @@ instance Eq n => Eq (TT n) where

305312 (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

306313 (==) (Set _) (Set _) = True -- deal with constraints later

307314 (==) (Constant x) (Constant y) = x == y

315+ (==) Erased _ = True

316+ (==) _ Erased = True

308317 (==) _ _ = False

309318

310319convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool

@@ -320,6 +329,8 @@ convEq (Constant x) (Constant y) = return (x == y)

320329convEq (Set x) (Set y) = do (v, cs) <- get

321330 put (v, ULE x y : cs)

322331 return True

332+convEq Erased _ = return True

333+convEq _ Erased = return True

323334convEq _ _ = return False

324335

325336-- A few handy operations on well typed terms:

@@ -418,7 +429,8 @@ forget tm = fe [] tm

418429 fe env (Constant c)

419430 = RConstant c

420431 fe env (Set i) = RSet

421−

432+ fe env Erased = RConstant Forgot

433+

422434bindAll :: [(n, Binder (TT n))] -> TT n -> TT n

423435bindAll [] t =t

424436bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)

@@ -485,6 +497,7 @@ showEnv' env t dbg = se 10 env t where

485497 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

486498 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

487499 se p env (Constant c) = show c

500+ se p env Erased = "[__]"

488501 se p env (Set i) = "Set " ++ show i

489502

490503 sb env n (Lam t) = showb env "\\ " " => " n t

src/Core/Typecheck.hs+8−4

@@ -36,11 +36,11 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)

3636 where isSet' (Set _) = return ()

3737 isSet' tm = fail (showEnv env tm ++ " is not a Set")

3838

39−recheck :: Context -> Env -> Term -> TC (Term, Type, UCs)

40−recheck ctxt env tm

39+recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

40+recheck ctxt env tm orig

4141 = let v = next_tvar ctxt in

42− case runStateT (check' False ctxt env (forget tm)) (v, []) of -- holes banned

43− Error (IncompleteTerm _) -> Error $ IncompleteTerm tm

42+ case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

43+ Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

4444 Error e -> Error e

4545 OK ((tm, ty), constraints) ->

4646 return (tm, ty, constraints)

@@ -77,13 +77,17 @@ check' holes ctxt env top = chk env top where

7777 let c = ULT (UVar v) (UVar (v+1))

7878 put (v+2, (c:cs))

7979 return (Set (UVar v), Set (UVar (v+1)))

80+ chk env (RConstant Forgot) = return (Erased, Erased)

8081 chk env (RConstant c) = return (Constant c, constType c)

8182 where constType (I _) = Constant IType

8283 constType (BI _) = Constant BIType

8384 constType (Fl _) = Constant FlType

8485 constType (Ch _) = Constant ChType

8586 constType (Str _) = Constant StrType

87+ constType Forgot = Erased

8688 constType _ = Set (UVal 0)

89+ chk env (RForce t) = do (_, ty) <- chk env t

90+ return (Erased, ty)

8791 chk env (RBind n (Pi s) t)

8892 = do (sv, st) <- chk env s

8993 (tv, tt) <- chk ((n, Pi sv) : env) t

src/Idris/AbsSyntax.hs+12

@@ -39,6 +39,7 @@ data IState = IState { tt_ctxt :: Context,

3939 idris_implicits :: Ctxt [PArg],

4040 idris_statics :: Ctxt [Bool],

4141 idris_classes :: Ctxt ClassInfo,

42+ idris_optimisation :: Ctxt OptInfo,

4243 idris_log :: String,

4344 idris_options :: IOption,

4445 idris_name :: Int,

@@ -66,6 +67,7 @@ data IBCWrite = IBCFix FixDecl

6667 | IBCImp Name

6768 | IBCStatic Name

6869 | IBCClass Name

70+ | IBCOpt Name

6971 | IBCSyntax Syntax

7072 | IBCKeyword String

7173 | IBCImport FilePath

@@ -77,6 +79,7 @@ data IBCWrite = IBCFix FixDecl

7779 deriving Show

7880

7981idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

82+ emptyContext

8083 "" defaultOpts 6 [] [] [] [] [] [] [] []

8184 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

8285

@@ -521,6 +524,15 @@ data ClassInfo = CI { instanceName :: Name,

521524deriving instance Binary ClassInfo

522525!-}

523526

527+data OptInfo = Optimise { collapsible :: Bool,

528+ forceable :: [Int], -- argument positions

529+ recursive :: [Int] }

530+ deriving Show

531+{-!

532+deriving instance Binary OptInfo

533+!-}

534+

535+

524536-- Syntactic sugar info

525537

526538data DSL = DSL { dsl_bind :: PTerm,

src/Idris/Compiler.hs+1

@@ -107,6 +107,7 @@ instance ToEpic (TT Name) where

107107 a' <- epic' env a

108108 return (f' @@ a')

109109 epic' env (Constant c) = epic c

110+ epic' env Erased = return impossible

110111 epic' env (Set _) = return impossible

111112

112113 epicCon env t arity n args

src/Idris/DataOpts.hsnew file+88

@@ -0,0 +1,88 @@

1+{-# LANGUAGE PatternGuards #-}

2+

3+module Idris.DataOpts where

4+

5+-- Forcing, detagging and collapsing

6+

7+import Idris.AbsSyntax

8+import Core.TT

9+

10+import Data.List

11+import Data.Maybe

12+import Debug.Trace

13+

14+-- Calculate the forceable arguments to a constructor and update the set of

15+-- optimisations

16+

17+forceArgs :: Name -> Type -> Idris ()

18+-- forceArgs n t = return ()

19+forceArgs n t = do let fargs = force 0 t

20+ i <- getIState

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

22+ [] -> return $ Optimise False [] []

23+ (op:_) -> return op

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

25+ putIState (i { idris_optimisation = opts })

26+ addIBC (IBCOpt n)

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

28+ where

29+ force :: Int -> Term -> [Int]

30+ force i (Bind _ (Pi _) sc)

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

32+ force _ sc@(App f a)

33+ | (_, args) <- unApply sc

34+ = nub $ concatMap guarded args

35+ force _ _ = []

36+

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

38+ isF _ = Nothing

39+

40+ guarded :: Term -> [Int]

41+ guarded t@(App f a)

42+ | (P (TCon _ _) _ _, args) <- unApply t

43+ = mapMaybe isF args ++ concatMap guarded args

44+ | (P (DCon _ _) _ _, args) <- unApply t

45+ = mapMaybe isF args ++ concatMap guarded args

46+ guarded t = mapMaybe isF [t]

47+

48+class Optimisable term where

49+ applyOpts :: term -> Idris term

50+

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

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

53+

54+instance Optimisable Raw where

55+ applyOpts t@(RApp f a)

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

57+ = do i <- getIState

58+ 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')

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

63+ a' <- applyOpts a

64+ return (RApp f' a')

65+ applyOpts (RBind n b t) = do b' <- applyOpts b

66+ t' <- applyOpts t

67+ return (RBind n b' t')

68+ applyOpts (RForce t) = applyOpts t

69+ applyOpts t = return t

70+

71+instance Optimisable t => Optimisable (Binder t) where

72+ applyOpts (Let t v) = do t' <- applyOpts t

73+ v' <- applyOpts v

74+ return (Let t' v')

75+ applyOpts b = do t' <- applyOpts (binderTy b)

76+ return (b { binderTy = t' })

77+

78+-- Compile time: no collapsing

79+

80+applyDataOpt :: OptInfo -> Name -> [Raw] -> Raw

81+applyDataOpt oi n args

82+ = let args' = zipWith doForce (map (\x -> x `elem` (forceable oi)) [0..])

83+ args in

84+ raw_apply (Var n) args'

85+ where

86+ doForce True a = RForce a

87+ doForce False a = a

88+

src/Idris/ElabDecls.hs+4−1

@@ -8,6 +8,7 @@ import Idris.Delaborate

88import Idris.Imports

99import Idris.ElabTerm

1010import Idris.Coverage

11+import Idris.DataOpts

1112import Paths_idris

1213

1314import Core.TT

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

2425

2526

2627recheckC ctxt fc env t

27− = do (tm, ty, cs) <- tclift $ recheck ctxt env t

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

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

2830 addConstraints fc cs

2931 return (tm, ty)

3032

@@ -90,6 +92,7 @@ elabCon info syn (n, t_in, fc)

9092 (cty, _) <- recheckC ctxt fc [] t'

9193 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

9294 addIBC (IBCDef n)

95+ forceArgs n cty

9396 return (n, cty)

9497

9598elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

src/Idris/IBC.hs+40−7

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

2222import Paths_idris

2323

2424ibcVersion :: Word8

25−ibcVersion = 4

25+ibcVersion = 5

2626

2727data IBCFile = IBCFile { ver :: Word8,

2828 sourcefile :: FilePath,

@@ -31,6 +31,7 @@ data IBCFile = IBCFile { ver :: Word8,

3131 ibc_fixes :: [FixDecl],

3232 ibc_statics :: [(Name, [Bool])],

3333 ibc_classes :: [(Name, ClassInfo)],

34+ ibc_optimise :: [(Name, OptInfo)],

3435 ibc_syntax :: [Syntax],

3536 ibc_keywords :: [String],

3637 ibc_objs :: [FilePath],

@@ -43,7 +44,7 @@ deriving instance Binary IBCFile

4344!-}

4445

4546initIBC :: IBCFile

46−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] []

47+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] []

4748

4849loadIBC :: FilePath -> Idris ()

4950loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -58,8 +59,9 @@ writeIBC src f

5859 (_:_) -> fail "Can't write ibc when there are unsolved metavariables"

5960 [] -> return ()

6061 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

61− liftIO $ encodeFile f ibcf

62− iLOG $ "Written"

62+ idrisCatch (do liftIO $ encodeFile f ibcf

63+ iLOG "Written")

64+ (\c -> do iLOG $ "Failed " ++ show c)

6365 return ()

6466

6567mkIBC :: [IBCWrite] -> IBCFile -> Idris IBCFile

@@ -81,6 +83,9 @@ ibc i (IBCClass n) f

8183 = case lookupCtxt Nothing n (idris_classes i) of

8284 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

8385 _ -> fail "IBC write failed"

86+ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of

87+ [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

88+ _ -> fail "IBC write failed"

8489ibc i (IBCSyntax n) f = return f { ibc_syntax = n : ibc_syntax f }

8590ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

8691ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

@@ -106,6 +111,7 @@ process i fn

106111 pFixes (ibc_fixes i)

107112 pStatics (ibc_statics i)

108113 pClasses (ibc_classes i)

114+ pOptimise (ibc_optimise i)

109115 pSyntax (ibc_syntax i)

110116 pKeywords (ibc_keywords i)

111117 pObjs (ibc_objs i)

@@ -162,6 +168,13 @@ pClasses cs = mapM_ (\ (n, c) ->

162168 = addDef n c (idris_classes i) }))

163169 cs

164170

171+pOptimise :: [(Name, OptInfo)] -> Idris ()

172+pOptimise cs = mapM_ (\ (n, c) ->

173+ do i <- getIState

174+ putIState (i { idris_optimisation

175+ = addDef n c (idris_optimisation i) }))

176+ cs

177+

165178pSyntax :: [Syntax] -> Idris ()

166179pSyntax s = do i <- getIState

167180 putIState (i { syntax_rules = s ++ syntax_rules i })

@@ -249,6 +262,7 @@ instance Binary Const where

249262 ChType -> putWord8 8

250263 StrType -> putWord8 9

251264 PtrType -> putWord8 10

265+ Forgot -> putWord8 11

252266 get

253267 = do i <- getWord8

254268 case i of

@@ -268,6 +282,7 @@ instance Binary Const where

268282 8 -> return ChType

269283 9 -> return StrType

270284 10 -> return PtrType

285+ 11 -> return Forgot

271286 _ -> error "Corrupted binary data for Const"

272287

273288

@@ -286,6 +301,8 @@ instance Binary Raw where

286301 RSet -> putWord8 3

287302 RConstant x1 -> do putWord8 4

288303 put x1

304+ RForce x1 -> do putWord8 5

305+ put x1

289306 get

290307 = do i <- getWord8

291308 case i of

@@ -301,6 +318,8 @@ instance Binary Raw where

301318 3 -> return RSet

302319 4 -> do x1 <- get

303320 return (RConstant x1)

321+ 5 -> do x1 <- get

322+ return (RForce x1)

304323 _ -> error "Corrupted binary data for Raw"

305324

306325

@@ -400,6 +419,7 @@ instance (Binary n) => Binary (TT n) where

400419 put x1

401420 Set x1 -> do putWord8 5

402421 put x1

422+ Erased -> do putWord8 6

403423 get

404424 = do i <- getWord8

405425 case i of

@@ -420,6 +440,7 @@ instance (Binary n) => Binary (TT n) where

420440 return (Constant x1)

421441 5 -> do x1 <- get

422442 return (Set x1)

443+ 6 -> return Erased

423444 _ -> error "Corrupted binary data for TT"

424445

425446

@@ -530,7 +551,7 @@ instance Binary Accessibility where

530551 _ -> error "Corrupted binary data for Accessibility"

531552

532553instance Binary IBCFile where

533− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

554+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

534555 = do put x1

535556 put x2

536557 put x3

@@ -545,6 +566,7 @@ instance Binary IBCFile where

545566 put x12

546567 put x13

547568 put x14

569+ put x15

548570 get

549571 = do x1 <- get

550572 if x1 == ibcVersion then

@@ -561,7 +583,8 @@ instance Binary IBCFile where

561583 x12 <- get

562584 x13 <- get

563585 x14 <- get

564− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

586+ x15 <- get

587+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

565588 else return (initIBC { ver = x1 })

566589

567590instance Binary Fixity where

@@ -940,7 +963,17 @@ instance Binary ClassInfo where

940963 x4 <- get

941964 return (CI x1 x2 x3 x4)

942965

943−

966+instance Binary OptInfo where

967+ put (Optimise x1 x2 x3)

968+ = do put x1

969+ put x2

970+ put x3

971+ get

972+ = do x1 <- get

973+ x2 <- get

974+ x3 <- get

975+ return (Optimise x1 x2 x3)

976+

944977instance Binary SynContext where

945978 put x

946979 = case x of

src/Idris/Parser.hs+1−1

@@ -64,7 +64,7 @@ loadModule f

6464 LIDR fn -> loadSource True fn

6565 IBC fn src ->

6666 idrisCatch (loadIBC fn)

67− (\c -> do iLOG $ fn ++ " failed"

67+ (\c -> do iLOG $ fn ++ " failed " ++ show c

6868 case src of

6969 IDR sfn -> loadSource False sfn

7070 LIDR sfn -> loadSource True sfn)