2a70296 · Idris-dev · git.iko.soy

Setup.hs+9−2

@@ -57,6 +57,13 @@ usesGMP flags =

5757 Just False -> False

5858 Nothing -> True

5959

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

62+ case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

6067isRelease :: S.ConfigFlags -> Bool

6168isRelease flags =

6269 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

@@ -176,7 +183,7 @@ getVersion args flags = do

176183 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

177184 return (Just buildinfo, [])

178185

179−idrisBuild _ flags _ local = do

186+idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do

180187 buildStdLib

181188 buildRTS

182189 where

@@ -199,7 +206,7 @@ idrisBuild _ flags _ local = do

199206-- -----------------------------------------------------------------------------

200207-- Copy/Install

201208

202−idrisInstall verbosity copy pkg local = do

209+idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do

203210 installStdLib

204211 installRTS

205212 where

idris.cabal+5

@@ -658,6 +658,11 @@ Flag CI

658658 Default: False

659659 manual: True

660660

661+Flag execonly

662+ Description: Build executables only, skip the libraries and RTS

663+ Default: False

664+ manual: True

665+

661666Library

662667 hs-source-dirs: src

663668 Exposed-modules:

libs/base/Language/Reflection/Utils.idr+1

@@ -272,6 +272,7 @@ instance Show Err where

272272 show (CantResolve tm) = "CantResolve " ++ show tm

273273 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

274274 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

275+ show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

275276 show UniverseError = "UniverseError"

276277 show ProgramLineComment = "ProgramLineComment"

277278 show (Inaccessible n) = "Inaccessible " ++ show n

libs/prelude/Language/Reflection/Errors.idr+1

@@ -31,6 +31,7 @@ data Err = Msg String

3131 | CantResolve TT

3232 | CantResolveAlts (List TTName)

3333 | IncompleteTerm TT

34+ | NoEliminator String TT

3435 | UniverseError

3536 | ProgramLineComment

3637 | Inaccessible TTName

src/Idris/Core/Binary.hs+9−3

@@ -91,8 +91,8 @@ instance Binary a => Binary (Err' a) where

9191 put x

9292 put y

9393 put z

94− put (CantResolve t) = do putWord8 15

95− put t

94+ put (CantResolve _ t) = do putWord8 15

95+ put t

9696 put (CantResolveAlts ns) = do putWord8 16

9797 put ns

9898 put (IncompleteTerm t) = do putWord8 17

@@ -146,6 +146,9 @@ instance Binary a => Binary (Err' a) where

146146 put x1

147147 put x2

148148 put x3

149+ put (NoEliminator s t) = do putWord8 37

150+ put s

151+ put t

149152

150153 get = do i <- getWord8

151154 case i of

@@ -172,7 +175,7 @@ instance Binary a => Binary (Err' a) where

172175 13 -> fmap NoTypeDecl get

173176 14 -> do x <- get ; y <- get ; z <- get

174177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176179 16 -> fmap CantResolveAlts get

177180 17 -> fmap IncompleteTerm get

178181 18 -> return UniverseError

@@ -205,6 +208,9 @@ instance Binary a => Binary (Err' a) where

205208 x2 <- get

206209 x3 <- get

207210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

208214 _ -> error "Corrupted binary data for Err'"

209215----- Generated by 'derive'

210216

src/Idris/Core/DeepSeq.hs+2−1

@@ -80,9 +80,10 @@ instance NFData Err where

8080 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

8181 rnf (NotInjective x1 x2 x3)

8282 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

83− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8484 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

8585 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86+ rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

8687 rnf UniverseError = ()

8788 rnf ProgramLineComment = ()

8889 rnf (Inaccessible x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756756

757757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758758try' t1 t2 proofSearch

759− = do s <- get

760− ps <- get_probs

761− ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

763− OK ((v, _, _), s') -> do put s'

764− return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

767− do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

771− else lift (tfail e2)

772− else lift (tfail e1)

759+ = do s <- get

760+ ps <- get_probs

761+ ulog <- getUnifyLog

762+ case prunStateT 999999 False ps t1 s of

763+ OK ((v, _, _), s') -> do put s'

764+ return $! v

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766+ if recoverableErr e1 then

767+ do case runStateT t2 s of

768+ OK (v, s') -> do put s'; return $! v

769+ Error e2 -> if score e1 >= score e2

770+ then lift (tfail e1)

771+ else lift (tfail e2)

772+ else lift (tfail e1)

773773 where recoverableErr err@(CantUnify r x y _ _ _)

774774 = -- traceWhen r (show err) $

775775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782782 recoverableErr (ElabDebug _ _ _) = False

783783 recoverableErr _ = True

784784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

791+ OK ((v, _, _), s') -> do put s'

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

785801tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

786802tryWhen True a b = try a b

787803tryWhen False a b = a

src/Idris/Core/ProofState.hs+8−5

@@ -681,8 +681,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

681681 (tmv, tmt) <- lift $ check ctxt env tm

682682 let tmt' = normalise ctxt env tmt

683683 let (tacn, tacstr, tactt) = if induction

684− then (ElimN, "an eliminator", "Induction")

685− else (CaseN, "a case function", "Case analysis")

684+ then (ElimN, "eliminator", "Induction")

685+ else (CaseN, "case analysis", "Case analysis")

686686 case unApply tmt' of

687687 (P _ tnm _, tyargs) -> do

688688 case lookupTy (SN (tacn tnm)) ctxt of

@@ -717,9 +717,10 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

717717 (scv, sct) <- lift $ check ctxt env res'

718718 let (scv', _) = specialise ctxt env [] scv

719719 return scv'

720− [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

720+ [] -> lift $ tfail $ NoEliminator tacstr tmt'

721721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

722− _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

722+ _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

723+ tmt'

723724 where scname = sMN 0 "scarg"

724725 makeConsArg (nm, ty) = P Bound nm ty

725726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

@@ -939,7 +940,9 @@ processTactic EndUnify ps

939940 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

940941 (ns'', probs') = updateProblems ps ns' (problems ps)

941942 tm' = updateSolved ns'' (pterm ps) in

942− traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $

943+ traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'') ++ "\n" ++

944+ show (pterm ps) ++ "\n" ++

945+ show tm') $

943946 return (ps { pterm = tm',

944947 unified = (h, []),

945948 problems = probs',

src/Idris/Core/ProofTerm.hs+3

@@ -172,6 +172,9 @@ updateSolvedTerm' xs x = updateSolved' xs x where

172172 else (t, False)

173173 updateSolved' xs t@(P _ n@(MN _ _) _)

174174 | Just v <- lookup n xs = (v, True)

175+ updateSolved' xs t@(P nt n ty)

176+ = let (ty', ut) = updateSolved' xs ty in

177+ if ut then (P nt n ty', True) else (t, False)

175178 updateSolved' xs t = (t, False)

176179

177180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

src/Idris/Core/TT.hs+10−3

@@ -155,9 +155,11 @@ data Err' t

155155 | WithFnType t

156156 | NoTypeDecl Name

157157 | NotInjective t t t

158− | CantResolve t

158+ | CantResolve Bool -- True if postponed, False if fatal

159+ t

159160 | CantResolveAlts [Name]

160161 | IncompleteTerm t

162+ | NoEliminator String t

161163 | UniverseError

162164 | UniqueError Universe Name

163165 | UniqueKindError Universe Name

@@ -231,7 +233,7 @@ instance Sized Err where

231233 size (NoSuchVariable name) = size name

232234 size (NoTypeDecl name) = size name

233235 size (NotInjective l c r) = size l + size c + size r

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235237 size (NoRewriting trm) = size trm

236238 size (CantResolveAlts _) = 1

237239 size (IncompleteTerm trm) = size trm

@@ -246,7 +248,7 @@ instance Sized Err where

246248

247249score :: Err -> Int

248250score (CantUnify _ _ _ m _ s) = s + score m

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250252score (NoSuchVariable _) = 1000

251253score (ProofSearchFail e) = score e

252254score (CantSolveGoal _ _) = 100000

@@ -934,6 +936,7 @@ vinstances i t = 0

934936-- | Replace the outermost (index 0) de Bruijn variable with the given term

935937instantiate :: TT n -> TT n -> TT n

936938instantiate e = subst 0 where

939+ subst i (P nt x ty) = P nt x (subst i ty)

937940 subst i (V x) | i == x = e

938941 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

939942 subst i (App f a) = App (subst i f) (subst i a)

@@ -945,6 +948,7 @@ instantiate e = subst 0 where

945948-- that has been substituted.

946949substV :: TT n -> TT n -> TT n

947950substV x tm = dropV 0 (instantiate x tm) where

951+ subst i (P nt x ty) = P nt x (subst i ty)

948952 dropV i (V x) | x > i = V (x - 1)

949953 | otherwise = V x

950954 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

@@ -1038,6 +1042,9 @@ subst n v tm = fst $ subst' 0 tm

10381042 -- substitution happens...)

10391043 subst' i (V x) | i == x = (v, True)

10401044 subst' i (P _ x _) | n == x = (v, True)

1045+ subst' i t@(P nt x ty)

1046+ = let (ty', ut) = subst' i ty in

1047+ if ut then (P nt x ty', True) else (t, False)

10411048 subst' i t@(Bind x b sc) | x /= n

10421049 = let (b', ub) = substB' i b

10431050 (sc', usc) = subst' (i+1) sc in

src/Idris/Core/Unify.hs+2−2

@@ -100,7 +100,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

100100 | (P (TCon _ _) _ _, _) <- unApply x,

101101 holeIn env f || f `elem` holes

102102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103− checkCycle names (f, Bind n' (Lam t) x)

103+ checkCycle names (f, Bind n' (Lam t) x)

104104 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

105105 | (P (TCon _ _) _ _, _) <- unApply x,

106106 holeIn env f || f `elem` holes

@@ -110,7 +110,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

110110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111111 holeIn env f || f `elem` holes

112112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113− checkCycle names (f, Bind n' (Lam t) x)

113+ checkCycle names (f, Bind n' (Lam t) x)

114114 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

115115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116116 holeIn env f || f `elem` holes

src/Idris/Delaborate.hs+7−1

@@ -289,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

289289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

290290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291291 annTm y (pprintTerm i (delab i y))

292−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

@@ -299,6 +299,12 @@ pprintErr' i (WithFnType ty) =

299299pprintErr' i (CantMatch t) =

300300 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

301301pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

302+pprintErr' i (NoEliminator s t)

303+ = text "No " <> text s <> text " for type " <+>

304+ annTm t (pprintTerm i (delab i t)) <$>

305+ text "Please note that 'induction' is experimental." <$>

306+ text "Only types declared with '%elim' can be used." <$>

307+ text "Consider writing a pattern matching definition instead."

302308pprintErr' i UniverseError = text "Universe inconsistency"

303309pprintErr' i (UniqueError NullType n)

304310 = text "Borrowed name" <+> annName' n (showbasic n)

src/Idris/ElabTerm.hs+48−15

@@ -91,7 +91,7 @@ build ist info emode opts fn tm

9191 mapM_ (\n -> when (n `elem` hs) $

9292 do focus n

9393 g <- goal

94− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

9595 (movelast n)) ivs

9696 ivs <- get_instances

9797 hs <- get_holes

@@ -99,7 +99,7 @@ build ist info emode opts fn tm

9999 mapM_ (\n -> when (n `elem` hs) $

100100 do focus n

101101 g <- goal

102− resolveTC True 7 g fn ist) ivs

102+ resolveTC True True 7 g fn ist) ivs

103103 tm <- get_term

104104 ctxt <- get_context

105105 probs <- get_probs

@@ -350,7 +350,7 @@ elab ist info emode opts fn tm

350350 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

351351 _ -> elab' ina (Just fc) (PRef fc unitCon)

352352 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

353− = do g <- goal; resolveTC False 5 g fn ist

353+ = do g <- goal; resolveTC False False 5 g fn ist

354354 elab' ina fc (PResolveTC fc')

355355 = do c <- getNameFrom (sMN 0 "class")

356356 instanceArg c

@@ -569,7 +569,7 @@ elab ist info emode opts fn tm

569569 g <- goal

570570 hs <- get_holes

571571 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

572− then try (resolveTC True 7 g fn ist)

572+ then try (resolveTC True False 7 g fn ist)

573573 (movelast n)

574574 else movelast n)

575575 (ivs' \\ ivs)

@@ -729,7 +729,7 @@ elab ist info emode opts fn tm

729729 env <- get_env

730730 hs <- get_holes

731731 if all (\n -> not (n `elem` hs)) (freeNames g)

732− then try (resolveTC False 7 g fn ist)

732+ then try (resolveTC False False 7 g fn ist)

733733 (movelast n)

734734 else movelast n)

735735 (ivs' \\ ivs)

@@ -1405,14 +1405,25 @@ proofSearch' ist rec ambigok depth prv top n hints

14051405-- Resolve type classes. This will only pick up 'normal' instances, never

14061406-- named instances (hence using 'tcname' to check it's a generated instance

14071407-- name).

1408−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1408+resolveTC :: Bool -- using default Int

1409+ -> Bool -- allow metavariables in the goal

1410+ -> Int -- depth

1411+ -> Term -- top level goal

1412+ -> Name -- top level function name

1413+ -> IState -> ElabD ()

14091414resolveTC = resTC' []

14101415

1411−resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"

1412−resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True

1413−resTC' tcs defaultOn depth topg fn ist

1414− = do compute

1415− g <- goal

1416+resTC' tcs def mvok 0 topg fn ist = fail $ "Can't resolve type class"

1417+resTC' tcs def mvok 1 topg fn ist = try' (trivial' ist) (resolveTC def mvok 0 topg fn ist) True

1418+resTC' tcs defaultOn mvok depth topg fn ist

1419+ = do compute

1420+ g <- goal

1421+ hs <- get_holes

1422+ let argsok = tcArgsOK g hs

1423+-- trace (show (g,hs,argsok,mvok)) $

1424+ if (not argsok && not mvok)

1425+ then lift $ tfail $ CantResolve True topg

1426+ else do

14161427 ptm <- get_term

14171428 ulog <- getUnifyLog

14181429 hs <- get_holes

@@ -1429,6 +1440,22 @@ resTC' tcs defaultOn depth topg fn ist

14291440 let depth' = if scopeOnly then 2 else depth

14301441 blunderbuss t depth' stk (stk ++ insts)) True

14311442 where

1443+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1444+ = True

1445+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1446+ = let (f, as) = unApply ty in

1447+ not $ any (isMeta hs) as

1448+

1449+ isMeta :: [Name] -> Term -> Bool

1450+ isMeta ns (P _ n _) = n `elem` ns

1451+ isMeta _ _ = False

1452+

1453+ notHole hs (P _ n _, c)

1454+ | (P _ cn _, _) <- unApply c,

1455+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1456+ | Constant _ <- c = not (n `elem` hs)

1457+ notHole _ _ = True

1458+

14321459 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

14331460 | otherwise = (fail "Can't resolve", show n)

14341461

@@ -1456,10 +1483,13 @@ resTC' tcs defaultOn depth topg fn ist

14561483

14571484 blunderbuss t d stk [] = do -- c <- get_env

14581485 -- ps <- get_probs

1459− lift $ tfail $ CantResolve topg

1486+ lift $ tfail $ CantResolve False topg

14601487 blunderbuss t d stk (n:ns)

14611488 | n /= fn && (n `elem` stk || tcname n)

1462− = try' (resolve n d) (blunderbuss t d stk ns) True

1489+ = tryCatch (resolve n d)

1490+ (\e -> case e of

1491+ CantResolve True _ -> lift $ tfail e

1492+ _ -> blunderbuss t d stk ns)

14631493 | otherwise = blunderbuss t d stk ns

14641494

14651495 resolve n depth

@@ -1488,7 +1518,7 @@ resTC' tcs defaultOn depth topg fn ist

14881518 let got = fst (unApply t)

14891519 let depth' = if tc' `elem` tcs

14901520 then depth - 1 else depth

1491− resTC' (got : tcs) defaultOn depth' topg fn ist)

1521+ resTC' (got : tcs) defaultOn mvok depth' topg fn ist)

14921522 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

14931523 -- if there's any arguments left, we've failed to resolve

14941524 hs <- get_holes

@@ -2667,11 +2697,14 @@ reflectErr (NotInjective t1 t2 t3) =

26672697 , reflect t2

26682698 , reflect t3

26692699 ]

2670−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2700+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

26712701reflectErr (CantResolveAlts ss) =

26722702 raw_apply (Var $ reflErrName "CantResolveAlts")

26732703 [rawList (Var $ reflm "TTName") (map reflectName ss)]

26742704reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2705+reflectErr (NoEliminator str t)

2706+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2707+ reflect t]

26752708reflectErr UniverseError = Var $ reflErrName "UniverseError"

26762709reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

26772710reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]