83bb62f · Idris-dev · git.iko.soy

src/IRTS/CodegenC.hs+1−12

compare with master

unifiedsplit

@@ -201,11 +201,7 @@ bcc i (MKCON l loc tag args)

201 = indent i ++ alloc loc tag ++

202 indent i ++ setArgs 0 args ++ "\n" ++

203 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

204−

205−-- "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++

206−-- show (length args) ++ concatMap showArg args ++ ");\n"

207− where showArg r = ", " ++ creg r

208− setArgs i [] = ""

204+ where setArgs i [] = ""

209 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

205 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

210 "); " ++ setArgs (i + 1) xs

206 "); " ++ setArgs (i + 1) xs

211 alloc Nothing tag

207 alloc Nothing tag

@@ -301,13 +297,6 @@ bcc i (CONSTCASE r code def)

301 iCase v (B64 w, bc) =

297 iCase v (B64 w, bc) =

302 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

298 indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"

303 ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

299 ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"

304− showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"

305− ++ concatMap (bcc (i+1)) bc ++

306− indent (i + 1) ++ "break;\n"

307− showDef i Nothing = ""

308− showDef i (Just c) = indent i ++ "default:\n"

309− ++ concatMap (bcc (i+1)) c ++

310− indent (i + 1) ++ "break;\n"

311 showDefS i Nothing = ""

300 showDefS i Nothing = ""

312 showDefS i (Just c) = concatMap (bcc (i+1)) c

301 showDefS i (Just c) = concatMap (bcc (i+1)) c

313

302

src/IRTS/Defunctionalise.hs+1−51

@@ -164,32 +164,6 @@ addApps defs (n, LFun _ _ args e)

164-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as

165 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as

166

167− -- if anything in the DExp is projected from, we'll need to evaluate it,

168− -- but we only want to do it once, rather than every time we project.

169−

170− preEval [] t = t

171− preEval (x : xs) t

172− | needsEval x t = DLet x (DV x) (preEval xs t)

173− | otherwise = preEval xs t

174−

175− needsEval x (DApp _ _ args) = any (needsEval x) args

176− needsEval x (DC _ _ _ args) = any (needsEval x) args

177− needsEval x (DCase up e alts) = needsEval x e || any nec alts

178− where nec (DConCase _ _ _ e) = needsEval x e

179− nec (DConstCase _ e) = needsEval x e

180− nec (DDefaultCase e) = needsEval x e

181− needsEval x (DChkCase e alts) = needsEval x e || any nec alts

182− where nec (DConCase _ _ _ e) = needsEval x e

183− nec (DConstCase _ e) = needsEval x e

184− nec (DDefaultCase e) = needsEval x e

185− needsEval x (DLet n v e)

186− | x == n = needsEval x v

187− | otherwise = needsEval x v || needsEval x e

188− needsEval x (DForeign _ _ args) = any (needsEval x) (map snd args)

189− needsEval x (DOp op args) = any (needsEval x) args

190− needsEval x (DProj (DV x') _) = x == x'

191− needsEval x _ = False

192−

193eEVAL x = DApp False (sMN 0 "EVAL") [x]

167eEVAL x = DApp False (sMN 0 "EVAL") [x]

194

168

195data EvalApply a = EvalCase (Name -> a)

169data EvalApply a = EvalCase (Name -> a)

@@ -221,7 +195,6 @@ toConsA ns (n, i)

221-- (DApp False n (map DV (take i (genArgs 0))))))))

195-- (DApp False n (map DV (take i (genArgs 0))))))))

222 = mkApplyCase n ar i

196 = mkApplyCase n ar i

223 | otherwise = []

197 | otherwise = []

224− where dupdate tlarg x = x

225

198

226mkApplyCase fname n ar | n == ar = []

199mkApplyCase fname n ar | n == ar = []

227mkApplyCase fname n ar

200mkApplyCase fname n ar

@@ -330,30 +303,7 @@ instance Show DExp where

330-- 'max' branches

303-- 'max' branches

331mkBigCase cn max arg branches

304mkBigCase cn max arg branches

332 | length branches <= max = DChkCase arg branches

305 | length branches <= max = DChkCase arg branches

333− | otherwise = -- DChkCase arg branches -- until I think of something...

334− -- divide the branches into groups of at most max (by tag),

335− -- generate a new case and shrink, recursively

336− let bs = sortBy tagOrd branches

337− (all, def) = case (last bs) of

338− DDefaultCase t -> (init all, Just (DDefaultCase t))

339− _ -> (all, Nothing)

340− bss = groupsOf max all

341− cs = map mkCase bss in

342− DChkCase arg branches

306+ | otherwise = DChkCase arg branches

343−

344− where mkCase bs = DChkCase arg bs

345−

346− tagOrd (DConCase t _ _ _) (DConCase t' _ _ _) = compare t t'

347− tagOrd (DConstCase c _) (DConstCase c' _) = compare c c'

348− tagOrd (DDefaultCase _) (DDefaultCase _) = EQ

349−

350− tagOrd (DConCase _ _ _ _) (DDefaultCase _) = LT

351− tagOrd (DConCase _ _ _ _) (DConstCase _ _) = LT

352− tagOrd (DConstCase _ _) (DDefaultCase _) = LT

353−

354− tagOrd (DDefaultCase _) (DConCase _ _ _ _) = GT

355− tagOrd (DConstCase _ _) (DConCase _ _ _ _) = GT

356− tagOrd (DDefaultCase _) (DConstCase _ _) = GT

357

307

358groupsOf :: Int -> [DAlt] -> [[DAlt]]

308groupsOf :: Int -> [DAlt] -> [[DAlt]]

359groupsOf x [] = []

309groupsOf x [] = []

src/IRTS/JavaScript/LangTransforms.hs−5

@@ -44,11 +44,6 @@ deriving instance Data LOpt

44restrictKeys :: Ord k => Map k a -> Set k -> Map k a

45restrictKeys m s = Map.filterWithKey (\k _ -> k `Set.member` s) m

46

47−mapMapListKeys :: Ord k => (a->a) -> [k] -> Map k a -> Map k a

48−mapMapListKeys _ [] x = x

49−mapMapListKeys f (t:r) x = mapMapListKeys f r $ Map.adjust f t x

50−

51−

52extractGlobs :: Map Name LDecl -> LDecl -> [Name]

47extractGlobs :: Map Name LDecl -> LDecl -> [Name]

53extractGlobs defs (LConstructor _ _ _) = []

48extractGlobs defs (LConstructor _ _ _) = []

54extractGlobs defs (LFun _ _ _ e) =

49extractGlobs defs (LFun _ _ _ e) =

src/IRTS/JavaScript/Specialize.hs−11

@@ -59,23 +59,12 @@ constructorOptimizeDB =

59 ]

60 -- constructors

61 where

62− nil = const $ JsArray []

63− cons [h, t] = JsMethod (JsArray [h]) "concat" [t]

64− -- tests

65− --trueTest e = JsUniOp (T.pack "!") $ JsUniOp (T.pack "!") e

66 trueTest = id

62 trueTest = id

67 falseTest e = JsUniOp (T.pack "!") e

63 falseTest e = JsUniOp (T.pack "!") e

68− emptyList e = JsBinOp "===" (JsProp e "length") (JsInt 0)

69− fillList e = JsBinOp ">" (JsProp e "length") (JsInt 0)

70 ltTest e = JsBinOp "<" e (JsInt 0)

64 ltTest e = JsBinOp "<" e (JsInt 0)

71 eqTest e = JsBinOp "===" e (JsInt 0)

65 eqTest e = JsBinOp "===" e (JsInt 0)

72 gtTest e = JsBinOp ">" e (JsInt 0)

66 gtTest e = JsBinOp ">" e (JsInt 0)

73− noneTest e = JsBinOp "===" e JsUndefined

74− notNoneTest e = JsBinOp "!==" e JsUndefined

75 -- projections

67 -- projections

76− justProj x n = x

77− uncons x 1 = JsArrayProj (JsInt 0) x

78− uncons x 2 = JsMethod x "slice" [JsInt 1]

79 cantProj x j = error $ "This type should be projected"

68 cantProj x j = error $ "This type should be projected"

80 item :: String

69 item :: String

81 -> String

70 -> String

src/Idris/AbsSyntax.hs+2−32

@@ -1465,28 +1465,7 @@ expandImplementationScope ist dec ps ns d = d

1465-- * if there's a function type, next (2)

1466-- * finally, everything else (3)

1467getPriority :: IState -> PTerm -> Int

1468−getPriority i tm = 1 -- pri tm

1468+getPriority i tm = 1

1469− where

1470− pri (PRef _ _ n) =

1471− case lookupP n (tt_ctxt i) of

1472− ((P (DCon _ _ _) _ _):_) -> 1

1473− ((P (TCon _ _) _ _):_) -> 1

1474− ((P Ref _ _):_) -> 1

1475− [] -> 0 -- must be locally bound, if it's not an error...

1476− pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

1477− pri (PTrue _ _) = 0

1478− pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))

1479− pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1480− pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

1481− pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))

1482− pri (PTyped l r) = pri l

1483− pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1484− pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1485− pri (PAlternative _ a as) = maximum (map pri as)

1486− pri (PConstant _ _) = 0

1487− pri Placeholder = 1

1488− pri _ = 3

1489−

1490

1469

1491addStatics :: Name -> Term -> PTerm -> Idris ()

1470addStatics :: Name -> Term -> PTerm -> Idris ()

1492addStatics n tm ptm =

1471addStatics n tm ptm =

@@ -2013,9 +1992,6 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []

2013 unqualified (NS _ _) = False

1992 unqualified (NS _ _) = False

2014 unqualified _ = True

1993 unqualified _ = True

2015

1994

2016− constructor (TyDecl (DCon _ _ _) _) = True

2017− constructor _ = False

2018−

2019 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

1995 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

2020

1996

2021 vname (UN n) = True -- non qualified

1997 vname (UN n) = True -- non qualified

@@ -2202,12 +2178,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

2202 -- check will not necessarily fully resolve constructor names,

2178 -- check will not necessarily fully resolve constructor names,

2203 -- and these bare names will otherwise get in the way of

2179 -- and these bare names will otherwise get in the way of

2204 -- impossbility checking.

2180 -- impossbility checking.

2205− | -- Just fn <- getFn f,

2206− canBeDConName fn ctxt

2181+ | canBeDConName fn ctxt

2207 = PApp fc f (fmap (fmap su) args)

2182 = PApp fc f (fmap (fmap su) args)

2208− where getFn (PRef _ _ fn) = Just fn

2209− getFn (PApp _ f args) = getFn f

2210− getFn _ = Nothing

2211 su (PApp fc f args)

2183 su (PApp fc f args)

2212 = PHidden (PApp fc f args)

2184 = PHidden (PApp fc f args)

2213 su (PAlternative ms b alts)

2185 su (PAlternative ms b alts)

@@ -2264,8 +2236,6 @@ findStatics ist tm = let (ns, ss) = fs tm

2264 (ns, ss)

2236 (ns, ss)

2265 fs _ = ([], [])

2237 fs _ = ([], [])

2266

2238

2267− inOne n ns = length (filter id (map (elem n) ns)) == 1

2268−

2269 pos ns ss (PPi p n fc t sc)

2239 pos ns ss (PPi p n fc t sc)

2270 | elem n ss = do sc' <- pos ns ss sc

2240 | elem n ss = do sc' <- pos ns ss sc

2271 spos <- get

2241 spos <- get

src/Idris/AbsSyntaxTree.hs−15

@@ -2200,7 +2200,6 @@ showName ist bnd ppo colour n = case ist of

2200 showbasic (MN i s) = str s

2201 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

2202 showbasic (SN s) = show s

2203− fst3 (x, _, _) = x

2204 colourise n t = let ctxt' = fmap tt_ctxt ist in

2203 colourise n t = let ctxt' = fmap tt_ctxt ist in

2205 case ctxt' of

2204 case ctxt' of

2206 Nothing -> name

2205 Nothing -> name

@@ -2348,20 +2347,6 @@ implicitNamesIn uvars ist tm

2348 addFn n = do (imps, fns) <- get

2347 addFn n = do (imps, fns) <- get

2349 put (imps, n: fns)

2348 put (imps, n: fns)

2350

2349

2351− notCAF [] = False

2352− notCAF (PExp _ _ _ _ : _) = True

2353− notCAF (_ : xs) = notCAF xs

2354−

2355− notHidden (n, _) = case getAccessibility n of

2356− Hidden -> False

2357− Private -> False

2358− _ -> True

2359−

2360− getAccessibility n

2361− = case lookupDefAccExact n False (tt_ctxt ist) of

2362− Just (n,t) -> t

2363− _ -> Public

2364−

2365 ni 0 env (PRef _ _ n@(NS _ _))

2350 ni 0 env (PRef _ _ n@(NS _ _))

2366 | not (n `elem` env)

2351 | not (n `elem` env)

2367 -- Never implicitly bind if there's a namespace

2352 -- Never implicitly bind if there's a namespace

src/Idris/Apropos.hs+1−7

@@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where

11import Idris.AbsSyntax

12import Idris.Core.Evaluate (Def(..), ctxtAlist)

13import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),

14− Type, toAlist)

14+ toAlist)

15import Idris.Docstrings (DocTerm, Docstring, containsText)

16

17import Data.List (intersperse, nub, nubBy)

@@ -104,9 +104,3 @@ instance (Apropos a) => Apropos (Maybe a) where

104

105instance (Apropos a) => Apropos [a] where

106 isApropos str xs = any (isApropos str) xs

107−

108−defType :: Def -> Type

109−defType (Function t _) = t

110−defType (TyDecl _ t) = t

111−defType (Operator t _ _) = t

112−defType (CaseOp _ t _ _ _ _) = t

src/Idris/Chaser.hs−3

@@ -58,9 +58,6 @@ getModuleFiles ts = nub $ execState (modList ts) [] where

58-- when (not (ibc p) || rechk) $

59 mapM_ (modTree (getSrc p : path)) deps

60

61− ibc (IBC _ _) = True

62− ibc _ = False

63−

64 chkReload False p = p

61 chkReload False p = p

65 chkReload True (IBC fn src) = chkReload True src

62 chkReload True (IBC fn src) = chkReload True src

66 chkReload True p = p

63 chkReload True p = p

src/Idris/Completion.hs−5

@@ -67,11 +67,6 @@ metavars :: Idris [String]

67metavars = do i <- get

68 return . map (show . nsroot) $ map fst (filter (\(_, (_,_,_,t,_)) -> not t) (idris_metavars i)) \\ primDefs

69

70−

71−modules :: Idris [String]

72−modules = do i <- get

73− return $ map show $ imported i

74−

75namespaces :: Idris [String]

70namespaces :: Idris [String]

76namespaces = do

71namespaces = do

77 ctxt <- fmap tt_ctxt get

72 ctxt <- fmap tt_ctxt get

src/Idris/Core/CaseTree.hs−57

@@ -268,7 +268,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

268 = return $ CaseDef [] (UnmatchedCase (show fc ++ ":No pattern clauses")) []

269 sc' tc defcase phase fc cs

270 = let proj = phase == RunTime

271− vnames = fstT (head cs)

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

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

273 (avs, toPats reflect tc l, (l, r))) cs

272 (avs, toPats reflect tc l, (l, r))) cs

274 chkPats = mapM chkAccessible pats in

273 chkPats = mapM chkAccessible pats in

@@ -285,10 +284,7 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

285 else return t

284 else return t

286 Error err -> Error (At fc err)

285 Error err -> Error (At fc err)

287 where args = map (\i -> sMN i "e") [0..]

286 where args = map (\i -> sMN i "e") [0..]

288− defaultCase True = STerm Erased

289− defaultCase False = UnmatchedCase "Error"

290 fstT (x, _, _) = x

287 fstT (x, _, _) = x

291− lstT (_, _, x) = x

292

288

293 -- Check that all pattern variables are reachable by a case split

289 -- Check that all pattern variables are reachable by a case split

294 -- Otherwise, they won't make sense on the RHS.

290 -- Otherwise, they won't make sense on the RHS.

@@ -303,48 +299,6 @@ simpleCase tc defcase reflect phase fc inacc argtys cs erInfo

303 acc (PSuc p : xs) n = acc (p : xs) n

299 acc (PSuc p : xs) n = acc (p : xs) n

304 acc (_ : xs) n = acc xs n

300 acc (_ : xs) n = acc xs n

305

301

306−-- For each 'Case', make sure every choice is in the same type family,

307−-- as directed by the variable type (i.e. there is no implicit type casing

308−-- going on).

309−

310−checkSameTypes :: [(Name, Type)] -> SC -> Bool

311−checkSameTypes tys (Case _ n alts)

312− = case lookup n tys of

313− Just t -> and (map (checkAlts t) alts)

314− _ -> and (map ((checkSameTypes tys).getSC) alts)

315− where

316− checkAlts t (ConCase n _ _ sc) = isType n t && checkSameTypes tys sc

317− checkAlts (Constant t) (ConstCase c sc) = isConstType c t && checkSameTypes tys sc

318− checkAlts _ (ConstCase c sc) = False

319− checkAlts _ _ = True

320−

321− getSC (ConCase _ _ _ sc) = sc

322− getSC (FnCase _ _ sc) = sc

323− getSC (ConstCase _ sc) = sc

324− getSC (SucCase _ sc) = sc

325− getSC (DefaultCase sc) = sc

326−checkSameTypes _ _ = True

327−

328−-- FIXME: All we're actually doing here is checking that we haven't arrived

329−-- at a specific constructor for a polymorphic argument. I *think* this

330−-- is sufficient, but if it turns out not to be, fix it!

331−--

332−-- Issue #1718 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1718

333−isType n t | (P (TCon _ _) _ _, _) <- unApply t = True

334−isType n t | (P Ref _ _, _) <- unApply t = True

335−isType n t = False

336−

337−isConstType (I _) (AType (ATInt ITNative)) = True

338−isConstType (BI _) (AType (ATInt ITBig)) = True

339−isConstType (Fl _) (AType ATFloat) = True

340−isConstType (Ch _) (AType (ATInt ITChar)) = True

341−isConstType (Str _) StrType = True

342−isConstType (B8 _) (AType (ATInt _)) = True

343−isConstType (B16 _) (AType (ATInt _)) = True

344−isConstType (B32 _) (AType (ATInt _)) = True

345−isConstType (B64 _) (AType (ATInt _)) = True

346−isConstType _ _ = False

347−

348data Pat = PCon Bool Name Int [Pat]

302data Pat = PCon Bool Name Int [Pat]

349 | PConst Const

303 | PConst Const

350 | PInferred Pat

304 | PInferred Pat

@@ -400,12 +354,6 @@ toPat reflect tc = map $ toPat' []

400

354

401 toPat' _ t = PAny

355 toPat' _ t = PAny

402

356

403− fixedN IT8 = "Bits8"

404− fixedN IT16 = "Bits16"

405− fixedN IT32 = "Bits32"

406− fixedN IT64 = "Bits64"

407−

408−

409data Partition = Cons [Clause]

357data Partition = Cons [Clause]

410 | Vars [Clause]

358 | Vars [Clause]

411 deriving Show

359 deriving Show

@@ -663,9 +611,6 @@ argsToAlt inacc rs@((r, m) : rest) = do

663 where

611 where

664 (acc, inacc) = partitionAcc r

612 (acc, inacc) = partitionAcc r

665

613

666− uniq i (UN n) = MN i n

667− uniq i n = n

668−

669getVar :: String -> CaseBuilder Name

614getVar :: String -> CaseBuilder Name

670getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

615getVar b = do (t, v, ntys) <- get; put (t, v+1, ntys); return (sMN v b)

671

616

@@ -869,5 +814,3 @@ mkForce = mkForceSC

869 = SucCase sn (mkForceSC n arg rhs)

814 = SucCase sn (mkForceSC n arg rhs)

870 mkForceAlt n arg (DefaultCase rhs)

815 mkForceAlt n arg (DefaultCase rhs)

871 = DefaultCase (mkForceSC n arg rhs)

816 = DefaultCase (mkForceSC n arg rhs)

872−

873− forceTm n arg t = subst n arg t

src/Idris/Core/Elaborate.hs−12

@@ -607,9 +607,6 @@ prepare_apply fn imps =

607 lift $ tfail $ TooManyArguments n

608 | otherwise = fail $ "Too many arguments for " ++ show fn

609

610− doClaim ((i, _), n, t) = do claim n t

611− when i (movelast n)

612−

613 mkMN n@(MN i _) = n

610 mkMN n@(MN i _) = n

614 mkMN n@(UN x) = MN 99999 x

611 mkMN n@(UN x) = MN 99999 x

615 mkMN n@(SN s) = sMN 99999 (show s)

612 mkMN n@(SN s) = sMN 99999 (show s)

@@ -666,8 +663,6 @@ apply' fillt fn imps =

666 | i = getNonUnify acc is as

663 | i = getNonUnify acc is as

667 | otherwise = getNonUnify (t : acc) is as

664 | otherwise = getNonUnify (t : acc) is as

668

665

669−-- getNonUnify imps args = map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

670−

671

666

672apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

667apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

673apply2 fn elabs =

668apply2 fn elabs =

@@ -675,7 +670,6 @@ apply2 fn elabs =

675 fill (raw_apply fn (map (Var . snd) args))

670 fill (raw_apply fn (map (Var . snd) args))

676 elabArgs (map snd args) elabs

671 elabArgs (map snd args) elabs

677 ES (p, a) s prev <- get

672 ES (p, a) s prev <- get

678− let (n, hs) = unified p

679 end_unify

673 end_unify

680 solve

674 solve

681 where elabArgs [] [] = return $! ()

675 where elabArgs [] [] = return $! ()

@@ -693,16 +687,10 @@ apply_elab n args =

693 env <- get_env

687 env <- get_env

694 claims <- doClaims (normalise ctxt env ty) args []

688 claims <- doClaims (normalise ctxt env ty) args []

695 prep_fill n (map fst claims)

689 prep_fill n (map fst claims)

696− let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

697 elabClaims [] False claims

690 elabClaims [] False claims

698 complete_fill

691 complete_fill

699 end_unify

692 end_unify

700 where

693 where

701− priOrder Nothing Nothing = EQ

702− priOrder Nothing _ = LT

703− priOrder _ Nothing = GT

704− priOrder (Just (x, _)) (Just (y, _)) = compare x y

705−

706 doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =

694 doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =

707 do n <- unique_hole (mkMN n')

695 do n <- unique_hole (mkMN n')

708 when (null claims) (start_unify n)

696 when (null claims) (start_unify n)

src/Idris/Core/Evaluate.hs−41

@@ -206,16 +206,6 @@ unfold ctxt env ns t

206finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))

207finalEntry (n, r, b) = (n, r, fmap finalise b)

208

209−bindEnv :: EnvTT n -> TT n -> TT n

210−bindEnv [] tm = tm

211−bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)

212−bindEnv ((n, r, b):bs) tm = Bind n b (bindEnv bs tm)

213−

214−unbindEnv :: EnvTT n -> TT n -> TT n

215−unbindEnv [] tm = tm

216−unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

217−unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."

218−

219usable :: Bool -- specialising

209usable :: Bool -- specialising

220 -> Bool -- unfolding only

210 -> Bool -- unfolding only

221 -> Int -- Reduction depth limit (when simplifying/at REPL)

211 -> Int -- Reduction depth limit (when simplifying/at REPL)

@@ -393,22 +383,6 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

393 evApply ntimes stk top env args f

383 evApply ntimes stk top env args f

394 = apply ntimes stk top env f args

384 = apply ntimes stk top env f args

395

385

396− reapply ntimes stk top env f@(VP Ref n ty) args

397− = let val = lookupDefAccExact n (spec || (atRepl && noFree env) || runtime) ctxt in

398− case val of

399− Just (CaseOp ci _ _ _ _ cd, acc) ->

400− let (ns, tree) = getCases cd in

401− do c <- evCase ntimes n (n:stk) top env ns args tree

402− case c of

403− (Nothing, _) -> return $ unload env (VP Ref n ty) args

404− (Just v, rest) -> evApply ntimes stk top env rest v

405− _ -> case args of

406− (a : as) -> return $ unload env f (a : as)

407− [] -> return f

408− reapply ntimes stk top env (VApp f a) args

409− = reapply ntimes stk top env f (a : args)

410− reapply ntimes stk top env v args = return v

411−

412 apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)

386 apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)

413 = do a' <- sc a

387 = do a' <- sc a

414 app <- apply ntimes stk top env a' as

388 app <- apply ntimes stk top env a' as

@@ -741,13 +715,6 @@ convEq ctxt holes topx topy = ceq [] topx topy where

741 (caseeq ((x,y):ps) xdef ydef)

715 (caseeq ((x,y):ps) xdef ydef)

742 _ -> return False

716 _ -> return False

743

717

744−-- SPECIALISATION -----------------------------------------------------------

745−-- We need too much control to be able to do this by tweaking the main

746−-- evaluator

747−

748−spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)

749−spec ctxt statics genv tm = error "spec undefined"

750−

751-- CONTEXTS -----------------------------------------------------------------

718-- CONTEXTS -----------------------------------------------------------------

752

719

753{-| A definition is either a simple function (just an expression with a type),

720{-| A definition is either a simple function (just an expression with a type),

@@ -985,7 +952,6 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

985 CaseDef args_rt sc_rt _) ->

952 CaseDef args_rt sc_rt _) ->

986 let inl = alwaysInline -- tcdict

953 let inl = alwaysInline -- tcdict

987 inlc = (inl || small n args_ct sc_ct) && (not asserted)

954 inlc = (inl || small n args_ct sc_ct) && (not asserted)

988− inlr = inl || small n args_rt sc_rt

989 cdef = CaseDefs (args_ct, sc_ct)

955 cdef = CaseDefs (args_ct, sc_ct)

990 (args_rt, sc_rt)

956 (args_rt, sc_rt)

991 op = (CaseOp (ci { case_inlinable = inlc })

957 op = (CaseOp (ci { case_inlinable = inlc })

@@ -1249,13 +1215,6 @@ linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

1249 tfail $ Msg $ show f ++ " can only appear in a linear binding"

1215 tfail $ Msg $ show f ++ " can only appear in a linear binding"

1250 _ -> return ()

1216 _ -> return ()

1251

1217

1252− checkArgs (Bind n (Pi RigW _ ty _) sc)

1253− = do mapM_ checkNameOK (allTTNames ty)

1254− checkArgs (substV (P Bound n Erased) sc)

1255− checkArgs (Bind n (Pi _ _ _ _) sc)

1256− = checkArgs (substV (P Bound n Erased) sc)

1257− checkArgs _ = return ()

1258−

1259-- Check if a name is reducible in the type checker. Partial definitions

1218-- Check if a name is reducible in the type checker. Partial definitions

1260-- are not reducible (so treated as a constant)

1219-- are not reducible (so treated as a constant)

1261tcReducible :: Name -> Context -> Bool

1220tcReducible :: Name -> Context -> Bool

src/Idris/Core/Execute.hs+2−33

@@ -45,10 +45,6 @@ execute :: Term -> Idris Term

45execute tm = fail "libffi not supported, rebuild Idris with -f FFI"

46#else

47-- else is rest of file

48−readMay :: (Read a) => String -> Maybe a

49−readMay s = case reads s of

50− [(x, "")] -> Just x

51− _ -> Nothing

52

48

53data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

49data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

54

50

@@ -164,9 +160,6 @@ runExec ex st = fst <$> runStateT (runExceptT ex) st

164getExecState :: Exec ExecState

160getExecState :: Exec ExecState

165getExecState = lift get

161getExecState = lift get

166

162

167−putExecState :: ExecState -> Exec ()

168−putExecState = lift . put

169−

170execFail :: Err -> Exec a

163execFail :: Err -> Exec a

171execFail = throwE

164execFail = throwE

172

165

@@ -475,8 +468,8 @@ execForeign env ctxt arity ty fn xs onfail

475execForeign env ctxt arity ty fn xs onfail

468execForeign env ctxt arity ty fn xs onfail

476 = case foreignFromTT arity ty fn xs of

469 = case foreignFromTT arity ty fn xs of

477 Just ffun@(FFun f argTs retT) | length xs >= arity ->

470 Just ffun@(FFun f argTs retT) | length xs >= arity ->

478− do let (args', xs') = (take arity xs, -- foreign args

471+ do let (_, xs') = (take arity xs, -- foreign args

479− drop arity xs) -- rest

472+ drop arity xs) -- rest

480 res <- call ffun (map snd argTs)

473 res <- call ffun (map snd argTs)

481 case res of

474 case res of

482 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

475 Nothing -> fail $ "Could not call foreign function \"" ++ f ++

@@ -704,26 +697,6 @@ foreignFromTT arity ty (EConstant (Str name)) args

704 return $ FFun name argFTyVals (toFDesc ty)

697 return $ FFun name argFTyVals (toFDesc ty)

705foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing

698foreignFromTT arity ty fn args = trace ("failed to construct ffun from " ++ show (ty,fn,args)) Nothing

706

699

707−getFTy :: ExecVal -> Maybe FType

708−getFTy (EApp (EP _ (UN fi) _) (EP _ (UN intTy) _))

709− | fi == txt "FIntT" =

710− case str intTy of

711− "ITNative" -> Just (FArith (ATInt ITNative))

712− "ITChar" -> Just (FArith (ATInt ITChar))

713− "IT8" -> Just (FArith (ATInt (ITFixed IT8)))

714− "IT16" -> Just (FArith (ATInt (ITFixed IT16)))

715− "IT32" -> Just (FArith (ATInt (ITFixed IT32)))

716− "IT64" -> Just (FArith (ATInt (ITFixed IT64)))

717− _ -> Nothing

718−getFTy (EP _ (UN t) _) =

719− case str t of

720− "FFloat" -> Just (FArith ATFloat)

721− "FString" -> Just FString

722− "FPtr" -> Just FPtr

723− "FUnit" -> Just FUnit

724− _ -> Nothing

725−getFTy _ = Nothing

726−

727unEList :: ExecVal -> Maybe [ExecVal]

700unEList :: ExecVal -> Maybe [ExecVal]

728unEList tm = case unApplyV tm of

701unEList tm = case unApplyV tm of

729 (nil, [_]) -> Just []

702 (nil, [_]) -> Just []

@@ -733,10 +706,6 @@ unEList tm = case unApplyV tm of

733 (f, args) -> Nothing

706 (f, args) -> Nothing

734

707

735

708

736−toConst :: Term -> Maybe Const

737−toConst (Constant c) = Just c

738−toConst _ = Nothing

739−

740mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]

709mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]

741mapMaybeM f [] = return []

710mapMaybeM f [] = return []

742mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

711mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

src/Idris/Core/ProofState.hs+10−56

@@ -179,7 +179,6 @@ match_unify' :: Context -> Env ->

179match_unify' ctxt env (topx, xfrom) (topy, yfrom) =

180 do ps <- get

181 let while = while_elaborating ps

182− let dont = dontunify ps

183 let inj = injective ps

182 let inj = injective ps

184 traceWhen (unifylog ps)

183 traceWhen (unifylog ps)

185 ("Matching " ++ show (topx, topy) ++

184 ("Matching " ++ show (topx, topy) ++

@@ -492,15 +491,6 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

492 Nothing -> error ("deferType can't find " ++ show n)

491 Nothing -> error ("deferType can't find " ++ show n)

493deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."

492deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."

494

493

495−regret :: RunTactic

496−regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

497− do action (\ps -> let hs = holes ps in

498− ps { holes = hs \\ [x] })

499− return sc

500−regret ctxt env (Bind x (Hole t) _)

501− = fail $ show x ++ " : " ++ show t ++ " is not solved..."

502−regret _ _ _ = fail "The current focus is not a hole."

503−

504unifyGoal :: Raw -> RunTactic

494unifyGoal :: Raw -> RunTactic

505unifyGoal tm ctxt env h@(Bind x b sc) =

495unifyGoal tm ctxt env h@(Bind x b sc) =

506 do (tmv, _) <- lift $ check ctxt env tm

496 do (tmv, _) <- lift $ check ctxt env tm

@@ -527,14 +517,8 @@ exact _ _ _ _ = fail "Can't fill here."

527fill :: Raw -> RunTactic

517fill :: Raw -> RunTactic

528fill guess ctxt env (Bind x (Hole ty) sc) =

518fill guess ctxt env (Bind x (Hole ty) sc) =

529 do (val, valty) <- lift $ check ctxt env guess

519 do (val, valty) <- lift $ check ctxt env guess

530−-- let valtyn = normalise ctxt env valty

531−-- let tyn = normalise ctxt env ty

532− ns <- unify' ctxt env (valty, Just $ SourceTerm val)

520+ unify' ctxt env (valty, Just $ SourceTerm val)

533− (ty, Just (chkPurpose val ty))

521+ (ty, Just (chkPurpose val ty))

534− ps <- get

535− let (uh, uns) = unified ps

536−-- put (ps { unified = (uh, uns ++ ns) })

537−-- addLog (show (uh, uns ++ ns))

538 return $ Bind x (Guess ty val) sc

522 return $ Bind x (Guess ty val) sc

539 where

523 where

540 -- some expected types show up commonly in errors and indicate a

524 -- some expected types show up commonly in errors and indicate a

@@ -550,14 +534,8 @@ fill _ _ _ _ = fail "Can't fill here."

550match_fill :: Raw -> RunTactic

534match_fill :: Raw -> RunTactic

551match_fill guess ctxt env (Bind x (Hole ty) sc) =

535match_fill guess ctxt env (Bind x (Hole ty) sc) =

552 do (val, valty) <- lift $ check ctxt env guess

536 do (val, valty) <- lift $ check ctxt env guess

553−-- let valtyn = normalise ctxt env valty

554−-- let tyn = normalise ctxt env ty

555− ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)

537+ match_unify' ctxt env (valty, Just $ SourceTerm val)

556− (ty, Just ExpectedType)

538+ (ty, Just ExpectedType)

557− ps <- get

558− let (uh, uns) = unified ps

559−-- put (ps { unified = (uh, uns ++ ns) })

560−-- addLog (show (uh, uns ++ ns))

561 return $ Bind x (Guess ty val) sc

539 return $ Bind x (Guess ty val) sc

562match_fill _ _ _ _ = fail "Can't fill here."

540match_fill _ _ _ _ = fail "Can't fill here."

563

541

@@ -571,11 +549,8 @@ complete_fill :: RunTactic

571complete_fill ctxt env (Bind x (Guess ty val) sc) =

549complete_fill ctxt env (Bind x (Guess ty val) sc) =

572 do let guess = forget val

550 do let guess = forget val

573 (val', valty) <- lift $ check ctxt env guess

551 (val', valty) <- lift $ check ctxt env guess

574− ns <- unify' ctxt env (valty, Just $ SourceTerm val')

552+ unify' ctxt env (valty, Just $ SourceTerm val')

575− (ty, Just ExpectedType)

553+ (ty, Just ExpectedType)

576− ps <- get

577− let (uh, uns) = unified ps

578−-- put (ps { unified = (uh, uns ++ ns) })

579 return $ Bind x (Guess ty val) sc

554 return $ Bind x (Guess ty val) sc

580complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

555complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

581

556

@@ -586,7 +561,6 @@ complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t

586solve :: RunTactic

561solve :: RunTactic

587solve ctxt env (Bind x (Guess ty val) sc)

562solve ctxt env (Bind x (Guess ty val) sc)

588 = do ps <- get

563 = do ps <- get

589− let (uh, uns) = unified ps

590 dropdots <-

564 dropdots <-

591 case lookup x (notunified ps) of

565 case lookup x (notunified ps) of

592 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

566 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $

@@ -603,7 +577,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

603 recents = x : recents ps,

577 recents = x : recents ps,

604 implementations = implementations ps \\ [x],

578 implementations = implementations ps \\ [x],

605 dotted = dropUnified dropdots (dotted ps) })

579 dotted = dropUnified dropdots (dotted ps) })

606− let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

580+ let (locked, _) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

607 return locked

581 return locked

608 where dropUnified ddots [] = []

582 where dropUnified ddots [] = []

609 dropUnified ddots ((x, es) : ds)

583 dropUnified ddots ((x, es) : ds)

@@ -628,7 +602,6 @@ solve ctxt env (Bind x (Guess ty val) sc)

628 (Bind n (Let ty' val') sc', tyl && vall && scl)

602 (Bind n (Let ty' val') sc', tyl && vall && scl)

629 tryLock hs t@(Bind n b sc)

603 tryLock hs t@(Bind n b sc)

630 = let (bt', btl) = tryLock hs (binderTy b)

604 = let (bt', btl) = tryLock hs (binderTy b)

631− (val', vall) = tryLock hs val

632 (sc', scl) = tryLock hs sc in

605 (sc', scl) = tryLock hs sc in

633 (Bind n (b { binderTy = bt' }) sc', btl && scl)

606 (Bind n (b { binderTy = bt' }) sc', btl && scl)

634 tryLock hs t = (t, True)

607 tryLock hs t = (t, True)

@@ -654,13 +627,9 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

654 x@(Bind y (Pi _ _ s _) _) -> x

627 x@(Bind y (Pi _ _ s _) _) -> x

655 _ -> normalise ctxt env t

628 _ -> normalise ctxt env t

656 (tyv, tyt) <- lift $ check ctxt env ty

629 (tyv, tyt) <- lift $ check ctxt env ty

657−-- ns <- lift $ unify ctxt env tyv t'

658 case t' of

630 case t' of

659 Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in

631 Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in

660− do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

632+ do unify' ctxt env (s, Nothing) (tyv, Nothing)

661− ps <- get

662− let (uh, uns) = unified ps

663−-- put (ps { unified = (uh, uns ++ ns) })

664 return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))

633 return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))

665 _ -> lift $ tfail $ CantIntroduce t'

634 _ -> lift $ tfail $ CantIntroduce t'

666introTy ty n ctxt env _ = fail "Can't introduce here."

635introTy ty n ctxt env _ = fail "Can't introduce here."

@@ -758,7 +727,7 @@ casetac :: Raw -> Bool -> RunTactic

758casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

727casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

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

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

760 let tmt' = normalise ctxt env tmt

729 let tmt' = normalise ctxt env tmt

761− let (tacn, tacstr, tactt) = if induction

730+ let (tacn, tacstr, _) = if induction

762 then (ElimN, "eliminator", "Induction")

731 then (ElimN, "eliminator", "Induction")

763 else (CaseN (FC' emptyFC), "case analysis", "Case analysis")

732 else (CaseN (FC' emptyFC), "case analysis", "Case analysis")

764 case unApply tmt' of

733 case unApply tmt' of

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

771 _ -> return []

740 _ -> return []

772 let (params, indicies) = splitTyArgs param_pos tyargs

741 let (params, indicies) = splitTyArgs param_pos tyargs

773 let args = getArgTys elimTy

742 let args = getArgTys elimTy

774− let pmargs = take (length params) args

775 let args' = drop (length params) args

743 let args' = drop (length params) args

776− let propTy = head args'

777 let restargs = init $ tail args'

744 let restargs = init $ tail args'

778 let consargs = take (length restargs - length indicies) restargs

745 let consargs = take (length restargs - length indicies) restargs

779− let indxargs = drop (length restargs - length indicies) restargs

780− let scr = last $ tail args'

781 let indxnames = makeIndexNames indicies

746 let indxnames = makeIndexNames indicies

782 currentNames <- query $ allTTNames . getProofTerm . pterm

747 currentNames <- query $ allTTNames . getProofTerm . pterm

783 let tmnm = case tm of

748 let tmnm = case tm of

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

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

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

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

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

801 tmt'

766 tmt'

802− where scname = sMN 0 "scarg"

803− makeConsArg (nm, ty) = P Bound nm ty

767+ where makeConsArg (nm, ty) = P Bound nm ty

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

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

805 bindConsArgs [] v = v

769 bindConsArgs [] v = v

806 addConsHole (nm, ty) =

770 addConsHole (nm, ty) =

@@ -879,8 +843,6 @@ start_unify :: Name -> RunTactic

879start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })

843start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })

880 return tm

844 return tm

881

845

882−tmap f (a, b, c) = (f a, b, c)

883−

884solve_unified :: RunTactic

846solve_unified :: RunTactic

885solve_unified ctxt env tm =

847solve_unified ctxt env tm =

886 do ps <- get

848 do ps <- get

@@ -929,14 +891,6 @@ updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)

929 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

891 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc

930updateError ns e = e

892updateError ns e = e

931

893

932−updateRes ns [] = []

933−updateRes ns ((x, t) : ts) = (x, updateSolvedTerm ns t) : updateRes ns ts

934−

935−solveInProblems x val [] = []

936−solveInProblems x val ((l, r, env, err) : ps)

937− = ((psubst x val l, psubst x val r,

938− updateEnv [(x, val)] env, err) : solveInProblems x val ps)

939−

940mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)

894mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)

941mergeNotunified env holes ns = mnu ns [] [] where

895mergeNotunified env holes ns = mnu ns [] [] where

942 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

896 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

src/Idris/Core/ProofTerm.hs−10

@@ -195,16 +195,6 @@ updateSolvedTerm' xs x = updateSolved' xs x where

195 updateSolvedB' xs b = let (ty', u) = updateSolved' xs (binderTy b) in

196 if u then (b { binderTy = ty' }, u) else (b, False)

197

198− noneOf ns (P _ n _) | n `elem` ns = False

199− noneOf ns (App s f a) = noneOf ns a && noneOf ns f

200− noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t

201− noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b

202− where

203− noneOfB ns (Let t v) = noneOf ns t && noneOf ns v

204− noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v

205− noneOfB ns b = noneOf ns (binderTy b)

206− noneOf ns _ = True

207−

208-- | As 'subst', in TT, but takes advantage of knowing not to substitute

198-- | As 'subst', in TT, but takes advantage of knowing not to substitute

209-- under Complete applications.

199-- under Complete applications.

210updsubst :: Eq n => n {-^ The id to replace -} ->

200updsubst :: Eq n => n {-^ The id to replace -} ->

src/Idris/Core/TT.hs−18

@@ -79,7 +79,6 @@ import qualified Data.Text as T

79import Data.Traversable (Traversable)

80import Data.Typeable (Typeable)

81import Debug.Trace

82−import Foreign.Storable (sizeOf)

83import GHC.Generics (Generic)

82import GHC.Generics (Generic)

84import Numeric (showIntAtBase)

83import Numeric (showIntAtBase)

85import Numeric.IEEE (IEEE(identicalIEEE))

84import Numeric.IEEE (IEEE(identicalIEEE))

@@ -431,13 +430,6 @@ instance Show a => Show (TC a) where

431tfail :: Err -> TC a

430tfail :: Err -> TC a

432tfail e = Error e

431tfail e = Error e

433

432

434−failMsg :: String -> TC a

435−failMsg str = Error (Msg str)

436−

437−trun :: FC -> TC a -> TC a

438−trun fc (OK a) = OK a

439−trun fc (Error e) = Error (At fc e)

440−

441discard :: Monad m => m a -> m ()

433discard :: Monad m => m a -> m ()

442discard f = f >> return ()

434discard f = f >> return ()

443

435

@@ -510,9 +502,6 @@ deriving instance Binary SpecialName

510sImplementationN :: Name -> [String] -> SpecialName

502sImplementationN :: Name -> [String] -> SpecialName

511sImplementationN n ss = ImplementationN n (map T.pack ss)

503sImplementationN n ss = ImplementationN n (map T.pack ss)

512

504

513−sParentN :: Name -> String -> SpecialName

514−sParentN n s = ParentN n (T.pack s)

515−

516instance Sized Name where

505instance Sized Name where

517 size (UN n) = 1

506 size (UN n) = 1

518 size (NS n els) = 1 + length els

507 size (NS n els) = 1 + length els

@@ -699,13 +688,6 @@ nativeTyWidth IT16 = 16

699nativeTyWidth IT32 = 32

688nativeTyWidth IT32 = 32

700nativeTyWidth IT64 = 64

689nativeTyWidth IT64 = 64

701

690

702−{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}

703−intTyWidth :: IntTy -> Int

704−intTyWidth (ITFixed n) = nativeTyWidth n

705−intTyWidth ITNative = 8 * sizeOf (0 :: Int)

706−intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"

707−intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

708−

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

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

710 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

692 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

711 | AType ArithTy | StrType

693 | AType ArithTy | StrType

src/Idris/Core/Typecheck.hs−31

@@ -205,12 +205,6 @@ check' holes tcns ctxt env top

205 Just v' -> v'

206 (tv, tt, tns) <- chk Rig0 st (Just maxu) ((n, Rig0, Pi Rig0 i sv kv) : envZero env) t

207

208−-- convertsC ctxt env st (TType maxu)

209−-- convertsC ctxt env tt (TType maxu)

210−-- when holes $ put (v, cs)

211−-- return (Bind n (Pi i (uniqueBinders (map fst env) sv) (TType maxu))

212−-- (pToV n tv), TType maxu)

213−

214 case (normalise ctxt env st, normalise ctxt env tt) of

208 case (normalise ctxt env st, normalise ctxt env tt) of

215 (TType su, TType tu) -> do

209 (TType su, TType tu) -> do

216 when (not holes) $ do (v, cs) <- get

210 when (not holes) $ do (v, cs) <- get

@@ -224,21 +218,6 @@ check' holes tcns ctxt env top

224 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

218 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

225 (pToV n tv), k', sns ++ tns)

219 (pToV n tv), k', sns ++ tns)

226

220

227− where mkUniquePi kv (Bind n (Pi rig i s k) sc)

228− = let k' = smaller kv k in

229− Bind n (Pi rig i s k') (mkUniquePi k' sc)

230− mkUniquePi kv (Bind n (Lam rig t) sc)

231− = Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)

232− mkUniquePi kv (Bind n (Let t v) sc)

233− = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

234− mkUniquePi kv t = t

235−

236− -- Kind of the whole thing is the kind of the most unique thing

237− -- in the environment (because uniqueness taints everything...)

238− mostUnique [] k = k

239− mostUnique (Pi _ _ _ pk : es) k = mostUnique es (smaller pk k)

240− mostUnique (_ : es) k = mostUnique es k

241−

242 chk rigc u lvl env (RBind n b sc)

221 chk rigc u lvl env (RBind n b sc)

243 = do (b', bt', bns) <- checkBinder b

222 = do (b', bt', bns) <- checkBinder b

244 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

223 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

@@ -261,7 +240,6 @@ check' holes tcns ctxt env top

261

240

262 checkBinder (Lam rig t)

241 checkBinder (Lam rig t)

263 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

242 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

264− let tv' = normalise ctxt env tv

265 convType tcns ctxt env tt

243 convType tcns ctxt env tt

266 return (Lam rig tv, tt, [])

244 return (Lam rig tv, tt, [])

267 checkBinder (Let t v)

245 checkBinder (Let t v)

@@ -270,14 +248,12 @@ check' holes tcns ctxt env top

270 -- (or rather, like an application of a lambda, multiply)

248 -- (or rather, like an application of a lambda, multiply)

271 -- (Consider: adding a single use let?)

249 -- (Consider: adding a single use let?)

272 (vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v

250 (vv, vt, vns) <- chk (rigMult rigc RigW) u Nothing env v

273− let tv' = normalise ctxt env tv

274 convertsC ctxt env vt tv

251 convertsC ctxt env vt tv

275 convType tcns ctxt env tt

252 convType tcns ctxt env tt

276 return (Let tv vv, tt, vns)

253 return (Let tv vv, tt, vns)

277 checkBinder (NLet t v)

254 checkBinder (NLet t v)

278 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

255 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

279 (vv, vt, vns) <- chk rigc u Nothing env v

256 (vv, vt, vns) <- chk rigc u Nothing env v

280− let tv' = normalise ctxt env tv

281 convertsC ctxt env vt tv

257 convertsC ctxt env vt tv

282 convType tcns ctxt env tt

258 convType tcns ctxt env tt

283 return (NLet tv vv, tt, vns)

259 return (NLet tv vv, tt, vns)

@@ -285,12 +261,10 @@ check' holes tcns ctxt env top

285 | not holes = lift $ tfail (IncompleteTerm undefined)

261 | not holes = lift $ tfail (IncompleteTerm undefined)

286 | otherwise

262 | otherwise

287 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

263 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

288− let tv' = normalise ctxt env tv

289 convType tcns ctxt env tt

264 convType tcns ctxt env tt

290 return (Hole tv, tt, [])

265 return (Hole tv, tt, [])

291 checkBinder (GHole i ns t)

266 checkBinder (GHole i ns t)

292 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

267 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

293− let tv' = normalise ctxt env tv

294 convType tcns ctxt env tt

268 convType tcns ctxt env tt

295 return (GHole i ns tv, tt, [])

269 return (GHole i ns tv, tt, [])

296 checkBinder (Guess t v)

270 checkBinder (Guess t v)

@@ -298,20 +272,15 @@ check' holes tcns ctxt env top

298 | otherwise

272 | otherwise

299 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

273 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

300 (vv, vt, vns) <- chk rigc u Nothing env v

274 (vv, vt, vns) <- chk rigc u Nothing env v

301− let tv' = normalise ctxt env tv

302 convertsC ctxt env vt tv

275 convertsC ctxt env vt tv

303 convType tcns ctxt env tt

276 convType tcns ctxt env tt

304 return (Guess tv vv, tt, vns)

277 return (Guess tv vv, tt, vns)

305 checkBinder (PVar rig t)

278 checkBinder (PVar rig t)

306 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

279 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

307− let tv' = normalise ctxt env tv

308 convType tcns ctxt env tt

280 convType tcns ctxt env tt

309− -- Normalised version, for erasure purposes (it's easier

310− -- to tell if it's a collapsible variable)

311 return (PVar rig tv, tt, [])

281 return (PVar rig tv, tt, [])

312 checkBinder (PVTy t)

282 checkBinder (PVTy t)

313 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

283 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

314− let tv' = normalise ctxt env tv

315 convType tcns ctxt env tt

284 convType tcns ctxt env tt

316 return (PVTy tv, tt, [])

285 return (PVTy tv, tt, [])

317

286

src/Idris/Core/Unify.hs−88

@@ -37,7 +37,6 @@ data FailContext = FailContext { fail_sourceloc :: FC,

37 }

38 deriving (Eq, Show)

39

40−type Injs = [(TT Name, TT Name, TT Name)]

41type Fails = [(TT Name, TT Name, -- unification error

40type Fails = [(TT Name, TT Name, -- unification error

42 Bool, -- ready to retry yet

41 Bool, -- ready to retry yet

43 Env, Err, [FailContext], FailAt)]

42 Env, Err, [FailContext], FailAt)]

@@ -55,10 +54,6 @@ unrecoverable = any bad

55data UInfo = UI Int Fails

54data UInfo = UI Int Fails

56 deriving Show

55 deriving Show

57

56

58−data UResult a = UOK a

59− | UPartOK a

60− | UFail Err

61−

62-- | Smart constructor for unification errors that takes into account the FailContext

57-- | Smart constructor for unification errors that takes into account the FailContext

63cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t

58cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t

64cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

59cantUnify [] r t1 t2 e ctxt i = CantUnify r t1 t2 e ctxt i

@@ -189,16 +184,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

189 | otherwise = checkScope ns (x, tm)

184 | otherwise = checkScope ns (x, tm)

190

185

191 checkScope ns (x, tm) =

186 checkScope ns (x, tm) =

192−-- case boundVs (envPos x 0 env) tm of

193−-- [] -> return [(x, tm)]

194−-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

195−-- (impl ns tm) (errEnv env))

196 let v = highV (-1) tm in

187 let v = highV (-1) tm in

197 if v >= length ns

188 if v >= length ns

198 then lift $ tfail (Msg "SCOPE ERROR")

189 then lift $ tfail (Msg "SCOPE ERROR")

199 else return [(x, bind v ns tm)]

190 else return [(x, bind v ns tm)]

200− where impl [] tm = tm

201− impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

202

191

203 bind i ns tm

192 bind i ns tm

204 | i < 0 = tm

193 | i < 0 = tm

@@ -255,20 +244,6 @@ trimSolutions (topx, xfrom) (topy, yfrom) from env topns = followSols [] (dropPa

255 followSols vs (n : ns) = do ns' <- followSols vs ns

244 followSols vs (n : ns) = do ns' <- followSols vs ns

256 return $ n : ns'

245 return $ n : ns'

257

246

258−expandLets env (x, tm) = (x, doSubst (reverse env) tm)

259− where

260− doSubst [] tm = tm

261− doSubst ((n, Let v t) : env) tm

262− = doSubst env (subst n v tm)

263− doSubst (_ : env) tm

264− = doSubst env tm

265−

266−hasv :: TT Name -> Bool

267−hasv (V x) = True

268−hasv (App _ f a) = hasv f || hasv a

269−hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

270−hasv _ = False

271−

272unify :: Context -> Env ->

247unify :: Context -> Env ->

273 (TT Name, Maybe Provenance) ->

248 (TT Name, Maybe Provenance) ->

274 (TT Name, Maybe Provenance) ->

249 (TT Name, Maybe Provenance) ->

@@ -295,10 +270,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

295-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

270-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

296 Error e -> tfail e

271 Error e -> tfail e

297 where

272 where

298− headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

299− headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

300− headDiff _ _ = False

301−

302 injective (P (DCon _ _ _) _ _) = True

273 injective (P (DCon _ _ _) _ _) = True

303 injective (P (TCon _ _) _ _) = True

274 injective (P (TCon _ _) _ _) = True

304-- injective (P Ref n _)

275-- injective (P Ref n _)

@@ -325,10 +296,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

325 sc i = do UI s f <- get

296 sc i = do UI s f <- get

326 put (UI (s+i) f)

297 put (UI (s+i) f)

327

298

328− errors :: StateT UInfo TC Bool

329− errors = do UI s f <- get

330− return (not (null f))

331−

332 uplus u1 u2 = do UI s f <- get

299 uplus u1 u2 = do UI s f <- get

333 r <- u1

300 r <- u1

334 UI s f' <- get

301 UI s f' <- get

@@ -340,12 +307,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

340 StateT UInfo

307 StateT UInfo

341 TC [(Name, TT Name)]

308 TC [(Name, TT Name)]

342 un = un' env

309 un = un' env

343−-- un fn names x y

344−-- = let (xf, _) = unApply x

345−-- (yf, _) = unApply y in

346−-- if headDiff xf yf then unifyFail x y else

347−-- uplus (un' fn names x y)

348−-- (un' fn names (hnf ctxt env x) (hnf ctxt env y))

349

310

350 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

311 un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->

351 StateT UInfo

312 StateT UInfo

@@ -575,26 +536,11 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

575 = unifyFail appx appy

536 = unifyFail appx appy

576 checkHeads _ _ = return []

537 checkHeads _ _ = return []

577

538

578− numArgs tm = let (f, args) = unApply tm in length args

579−

580 metavarApp tm = let (f, args) = unApply tm in

539 metavarApp tm = let (f, args) = unApply tm in

581 (metavar f &&

540 (metavar f &&

582 all (\x -> metavarApp x) args

541 all (\x -> metavarApp x) args

583 && nub args == args) ||

542 && nub args == args) ||

584 globmetavar tm

543 globmetavar tm

585− metavarArgs tm = let (f, args) = unApply tm in

586− all (\x -> metavar x || inenv x) args

587− && nub args == args

588− metavarApp' tm = let (f, args) = unApply tm in

589− all (\x -> pat x || metavar x) (f : args)

590− && nub args == args

591−

592− rigid (P (DCon _ _ _) _ _) = True

593− rigid (P (TCon _ _) _ _) = True

594− rigid t@(P Ref _ _) = inenv t || globmetavar t

595− rigid (Constant _) = True

596− rigid (App _ f a) = rigid f && rigid a

597− rigid t = not (metavar t) || globmetavar t

598

544

599 globmetavar t = case unApply t of

545 globmetavar t = case unApply t of

600 (P _ x _, _) ->

546 (P _ x _, _) ->

@@ -608,14 +554,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

608 (x `elem` holes || holeIn env x))

554 (x `elem` holes || holeIn env x))

609 || globmetavar t

555 || globmetavar t

610 _ -> False

556 _ -> False

611− pat t = case t of

612− P _ x _ -> x `elem` holes || patIn env x

613− _ -> False

614− inenv t = case t of

615− P _ x _ -> x `elem` (map fstEnv env)

616− _ -> False

617−

618− notFn t = injective t || metavar t || inenv t

619

557

620 injectiveTC t@(P Ref n _) t'@(P Ref n' _)

558 injectiveTC t@(P Ref n _) t'@(P Ref n' _)

621 | Just ni <- lookupInjectiveExact n ctxt,

559 | Just ni <- lookupInjectiveExact n ctxt,

@@ -680,16 +618,10 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

680 | otherwise = checkScope ns (x, tm)

618 | otherwise = checkScope ns (x, tm)

681

619

682 checkScope ns (x, tm) | pureTerm tm =

620 checkScope ns (x, tm) | pureTerm tm =

683−-- case boundVs (envPos x 0 env) tm of

684−-- [] -> return [(x, tm)]

685−-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

686−-- (impl ns tm) (errEnv env))

687 let v = highV (-1) tm in

621 let v = highV (-1) tm in

688 if v >= length ns

622 if v >= length ns

689 then lift $ tfail (Msg "SCOPE ERROR")

623 then lift $ tfail (Msg "SCOPE ERROR")

690 else return [(x, bind v ns tm)]

624 else return [(x, bind v ns tm)]

691− where impl [] tm = tm

692− impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

693 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

625 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

694

626

695 bind i ns tm

627 bind i ns tm

@@ -708,15 +640,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

708 sc 1

640 sc 1

709 combine env bnames as (ns' ++ bs)

641 combine env bnames as (ns' ++ bs)

710

642

711−boundVs :: Int -> Term -> [Int]

712−boundVs i (V j) | j < i = []

713− | otherwise = [j]

714−boundVs i (Bind n b sc) = boundVs (i + 1) sc

715−boundVs i (App _ f x) = let fs = boundVs i f

716− xs = boundVs i x in

717− nub (fs ++ xs)

718−boundVs i _ = []

719−

720highV :: Int -> Term -> Int

643highV :: Int -> Term -> Int

721highV i (V j) | j > i = j

644highV i (V j) | j > i = j

722 | otherwise = i

645 | otherwise = i

@@ -724,11 +647,6 @@ highV i (Bind n b sc) = maximum [i, highV i (binderTy b), (highV i sc - 1)]

724highV i (App _ f x) = max (highV i f) (highV i x)

647highV i (App _ f x) = max (highV i f) (highV i x)

725highV i _ = i

648highV i _ = i

726

649

727−envPos x i [] = 0

728−envPos x i ((y, _) : ys) | x == y = i

729− | otherwise = envPos x (i + 1) ys

730−

731−

732-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

650-- If there are any clashes of constructors, deem it unrecoverable, otherwise some

733-- more work may help.

651-- more work may help.

734-- FIXME: Depending on how overloading gets used, this may cause problems. Better

652-- FIXME: Depending on how overloading gets used, this may cause problems. Better

@@ -794,9 +712,3 @@ holeIn env n = case lookupBinder n env of

794 Just (Hole _) -> True

712 Just (Hole _) -> True

795 Just (Guess _ _) -> True

713 Just (Guess _ _) -> True

796 _ -> False

714 _ -> False

797−

798−patIn :: Env -> Name -> Bool

799−patIn env n = case lookupBinder n env of

800− Just (PVar _ _) -> True

801− Just (PVTy _) -> True

802− _ -> False

src/Idris/Coverage.hs−7

@@ -281,10 +281,6 @@ addMissingConsSt ist (Case t n alts) = liftM (Case t n) (addMissingAlts n alts)

281 collectConsts (ConstCase c sc) = Just c

282 collectConsts _ = Nothing

283

284− hasDefault (DefaultCase (UnmatchedCase _)) = False

285− hasDefault (DefaultCase _) = True

286− hasDefault _ = False

287−

288 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)

284 getConType n = do ty <- lookupTyExact n (tt_ctxt ist)

289 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

285 case unApply (getRetTy (normalise (tt_ctxt ist) [] ty)) of

290 (P _ tyn _, _) -> Just tyn

286 (P _ tyn _, _) -> Just tyn

@@ -333,9 +329,6 @@ trimOverlapping sc = trim [] [] sc

333 trimAlts cs nots vn (DefaultCase sc : rest)

329 trimAlts cs nots vn (DefaultCase sc : rest)

334 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest

330 = DefaultCase (trim cs nots sc) : trimAlts cs nots vn rest

335

331

336− isConMatch c (ConCase cn t args sc) = c == cn

337− isConMatch _ _ = False

338−

339 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]

332 substMatch :: (Name, [Name]) -> [CaseAlt] -> [CaseAlt]

340 substMatch ca [] = []

333 substMatch ca [] = []

341 substMatch (c,args) (ConCase cn t args' sc : _)

334 substMatch (c,args) (ConCase cn t args' sc : _)

src/Idris/DSL.hs+1−2

@@ -167,8 +167,7 @@ var dsl n t i = v' i t where

167 setFC fc t = t

168

169unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

170−unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

170+unIdiom ap pure fc e@(PApp _ _ _) = mkap (getFn e)

171− mkap (getFn e)

172 where

171 where

173 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

172 getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

174 getFn f = (f, [])

173 getFn f = (f, [])

src/Idris/Delaborate.hs+1−8

@@ -191,13 +191,6 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

191 de tys env _ (TType i) = PType un

192 de tys env _ (UType u) = PUniverse un u

193

194− dens x | fullname = x

195− dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

196− [_] -> n -- just one thing

197− [] -> n -- metavariables have no implicits

198− _ -> ns

199− dens n = n

200−

201 deFn tys env (App _ f a) args = deFn tys env f (a:args)

194 deFn tys env (App _ f a) args = deFn tys env f (a:args)

202 deFn tys env (P _ n _) [l,r]

195 deFn tys env (P _ n _) [l,r]

203 | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

196 | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

@@ -353,7 +346,7 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =

353 then text "Unification failure" <$> showSc i sc

346 then text "Unification failure" <$> showSc i sc

354 else empty

347 else empty

355pprintErr' i (CantConvert x_in y_in env) =

348pprintErr' i (CantConvert x_in y_in env) =

356− let (x_ns, y_ns, nms) = renameMNs x_in y_in

349+ let (x_ns, y_ns, _) = renameMNs x_in y_in

357 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

350 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))

358 (delabSugared i (flagUnique y_ns)) in

351 (delabSugared i (flagUnique y_ns)) in

359 text "Type mismatch between" <>

352 text "Type mismatch between" <>

src/Idris/Docs.hs−4

@@ -240,10 +240,6 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

240 updateRef nm (PRef fc _ _) = PRef fc [] nm

241 updateRef _ pt = pt

242

243− isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

244− isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

245− isSubInterface _ = False

246−

247 prettyConstraints =

243 prettyConstraints =

248 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

244 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

249

245

src/Idris/Elab/Clause.hs+4−35

@@ -27,7 +27,6 @@ import Idris.Elab.Transform

27import Idris.Elab.Type

28import Idris.Elab.Utils

29import Idris.Error

30−import Idris.Inliner

31import Idris.Options

30import Idris.Options

32import Idris.Output (iputStrLn, pshow, sendHighlighting)

31import Idris.Output (iputStrLn, pshow, sendHighlighting)

33import Idris.PartialEval

32import Idris.PartialEval

@@ -140,12 +139,6 @@ elabClauses info' fc opts n_in cs =

140 -- optimisation applied to LHS

139 -- optimisation applied to LHS

141 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

140 let pdef = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

142 map debind pats_forced

141 map debind pats_forced

143− -- pdef_cov is the pattern definition without forcing, which

144− -- we feed to the coverage checker (we need to know what the

145− -- programmer wrote before forcing erasure)

146− let pdef_cov

147− = map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) $

148− map debind pats_raw

149 -- pdef_pe is the one which will get further optimised

142 -- pdef_pe is the one which will get further optimised

150 -- for run-time, with no forcing optimisation of the LHS because

143 -- for run-time, with no forcing optimisation of the LHS because

151 -- the affects erasure. Also, it's partially evaluated

144 -- the affects erasure. Also, it's partially evaluated

@@ -160,8 +153,6 @@ elabClauses info' fc opts n_in cs =

160 -- help with later inlinings.

153 -- help with later inlinings.

161

154

162 ist <- getIState

155 ist <- getIState

163− let pdef_inl = inlineDef ist pdef

164−

165 numArgs <- tclift $ sameLength pdef

156 numArgs <- tclift $ sameLength pdef

166

157

167 case specNames opts of

158 case specNames opts of

@@ -184,7 +175,6 @@ elabClauses info' fc opts n_in cs =

184 missing' <- checkPossibles info fc True n missing

175 missing' <- checkPossibles info fc True n missing

185 -- Filter out the ones which match one of the

176 -- Filter out the ones which match one of the

186 -- given cases (including impossible ones)

177 -- given cases (including impossible ones)

187− let clhs = map getLHS pdef

188 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++

178 logElab 2 $ "Must be unreachable (" ++ show (length missing') ++ "):\n" ++

189 showSep "\n" (map showTmImpls missing') ++

179 showSep "\n" (map showTmImpls missing') ++

190 "\nAgainst: " ++

180 "\nAgainst: " ++

@@ -232,7 +222,6 @@ elabClauses info' fc opts n_in cs =

232 logElab 3 $ "Optimised: " ++ show tree'

222 logElab 3 $ "Optimised: " ++ show tree'

233 ctxt <- getContext

223 ctxt <- getContext

234 ist <- getIState

224 ist <- getIState

235− let opt = idris_optimisation ist

236 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

225 putIState (ist { idris_patdefs = addDef n (force pdef_pe, force pmissing)

237 (idris_patdefs ist) })

226 (idris_patdefs ist) })

238 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

227 let caseInfo = CaseInfo (inlinable opts) (inlinable opts) (dictionary opts)

@@ -302,15 +291,6 @@ elabClauses info' fc opts n_in cs =

302 return ()

291 return ()

303

292

304 where

293 where

305− noMatch i cs tm = all (\x -> case trim_matchClause i (delab' i x True True) tm of

306− Right _ -> False

307− Left miss -> True) cs

308− where

309− trim_matchClause i (PApp fcl fl ls) (PApp fcr fr rs)

310− = let args = min (length ls) (length rs) in

311− matchClause i (PApp fcl fl (take args ls))

312− (PApp fcr fr (take args rs))

313−

314 checkUndefined n ctxt = case lookupDef n ctxt of

294 checkUndefined n ctxt = case lookupDef n ctxt of

315 [] -> return ()

295 [] -> return ()

316 [TyDecl _ _] -> return ()

296 [TyDecl _ _] -> return ()

@@ -358,7 +338,7 @@ elabClauses info' fc opts n_in cs =

358

338

359 sameLength ((_, x, _) : xs)

339 sameLength ((_, x, _) : xs)

360 = do l <- sameLength xs

340 = do l <- sameLength xs

361− let (f, as) = unApply x

341+ let (_, as) = unApply x

362 if (null xs || l == length as) then return (length as)

342 if (null xs || l == length as) then return (length as)

363 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

343 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

364 sameLength [] = return 0

344 sameLength [] = return 0

@@ -671,8 +651,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

671 "\n" ++ show ptm

651 "\n" ++ show ptm

672 return (Left ptm, lhs)

652 return (Left ptm, lhs)

673elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)

653elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock_as)

674− = do let tcgen = Dictionary `elem` opts

675− push_estack fname False

654+ = do push_estack fname False

676 ctxt <- getContext

655 ctxt <- getContext

677 let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as

656 let (lhs_in, rhs_in, whereblock) = desugarAs lhs_in_as rhs_in_as whereblock_as

678

657

@@ -903,8 +882,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

903 pinfo info ns ds i

882 pinfo info ns ds i

904 = let newps = params info ++ ns

883 = let newps = params info ++ ns

905 dsParams = map (\n -> (n, map fst newps)) ds

884 dsParams = map (\n -> (n, map fst newps)) ds

906− newb = addAlist dsParams (inblock info)

885+ newb = addAlist dsParams (inblock info) in

907− l = liftname info in

908 info { params = newps,

886 info { params = newps,

909 inblock = newb,

887 inblock = newb,

910 liftname = id -- (\n -> case lookupCtxt n newb of

888 liftname = id -- (\n -> case lookupCtxt n newb of

@@ -953,8 +931,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

953 isOutsideWith _ = True

931 isOutsideWith _ = True

954

932

955elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

933elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

956− = do let tcgen = Dictionary `elem` opts

957− ctxt <- getContext

934+ = do ctxt <- getContext

958 -- Build the LHS as an "Infer", and pull out its type and

935 -- Build the LHS as an "Infer", and pull out its type and

959 -- pattern bindings

936 -- pattern bindings

960 i <- getIState

937 i <- getIState

@@ -1176,9 +1153,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1176 mkAux pn wname toplhs ns ns' c

1153 mkAux pn wname toplhs ns ns' c

1177 = ifail $ show fc ++ ":badly formed with clause"

1154 = ifail $ show fc ++ ":badly formed with clause"

1178

1155

1179− addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1180− addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]

1181−

1182 -- ns, arguments which don't depend on the with argument

1156 -- ns, arguments which don't depend on the with argument

1183 -- ns', arguments which do

1157 -- ns', arguments which do

1184 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

1158 updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

@@ -1202,11 +1176,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1202 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1176 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

1203 = mapPT updateApp tm

1177 = mapPT updateApp tm

1204 where

1178 where

1205− arity (PApp _ _ as) = length as

1206− arity _ = 0

1207−

1208− lhs_arity = arity toplhs

1209−

1210 currentFn fname (PAlternative _ _ as)

1179 currentFn fname (PAlternative _ _ as)

1211 | Just tm <- getApp as = tm

1180 | Just tm <- getApp as = tm

1212 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

1181 where getApp (tm@(PApp _ (PRef _ _ f) _) : as)

src/Idris/Elab/Data.hs+3−20

@@ -42,8 +42,7 @@ warnLC fc n

42

43elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

44elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

45− = do let codata = Codata `elem` opts

46− logElab 1 (show (fc, doc))

45+ = do logElab 1 (show (fc, doc))

47 checkUndefined fc n

46 checkUndefined fc n

48 when (implicitable (nsroot n)) $ warnLC fc n

47 when (implicitable (nsroot n)) $ warnLC fc n

49 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

48 (cty, _, t, inacc) <- buildType info syn fc [] n t_in

@@ -73,7 +72,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

73 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

72 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

74 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

73 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

75 ttag <- getName

74 ttag <- getName

76− let as = map (const (Left (Msg ""))) (getArgTys cty)

77

75

78 ctxt <- getContext

76 ctxt <- getContext

79 let params = findParams n (normalise ctxt [] cty) (map snd cons)

77 let params = findParams n (normalise ctxt [] cty) (map snd cons)

@@ -151,8 +149,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

151 cinfo info ds

149 cinfo info ds

152 = let newps = params info

150 = let newps = params info

153 dsParams = map (\n -> (n, [])) ds

151 dsParams = map (\n -> (n, [])) ds

154− newb = addAlist dsParams (inblock info)

152+ newb = addAlist dsParams (inblock info) in

155− l = liftname info in

156 info { params = newps,

153 info { params = newps,

157 inblock = newb,

154 inblock = newb,

158 liftname = id -- Is this appropriate?

155 liftname = id -- Is this appropriate?

@@ -226,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

226 getTyName (PRef _ _ n) = n == nsroot tn

223 getTyName (PRef _ _ n) = n == nsroot tn

227 getTyName _ = False

224 getTyName _ = False

228

225

229−

230− getNamePos :: Int -> PTerm -> Name -> Maybe Int

231− getNamePos i (PPi _ n _ _ sc) x | n == x = Just i

232− | otherwise = getNamePos (i + 1) sc x

233− getNamePos _ _ _ = Nothing

234−

235 -- if the constructor is a UniqueType, the datatype must be too

226 -- if the constructor is a UniqueType, the datatype must be too

236 -- (AnyType is fine, since that is checked for uniqueness too)

227 -- (AnyType is fine, since that is checked for uniqueness too)

237 -- if hte contructor is AnyType, the datatype must be at least AnyType

228 -- if hte contructor is AnyType, the datatype must be at least AnyType

@@ -339,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do

339 elimLog "Elaborating case function"

330 elimLog "Elaborating case function"

340 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

331 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

341 let (cnstrs, _) = splitPi ty

332 let (cnstrs, _) = splitPi ty

342− let (splittedTy@(pms, idxs)) = splitPms cnstrs

333+ let (pms, idxs) = splitPms cnstrs

343 generalParams <- namePis False pms

334 generalParams <- namePis False pms

344 motiveIdxs <- namePis False idxs

335 motiveIdxs <- namePis False idxs

345 let motive = mkMotive n paramPos generalParams motiveIdxs

336 let motive = mkMotive n paramPos generalParams motiveIdxs

@@ -377,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do

377 elimDeclName :: Name

368 elimDeclName :: Name

378 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

369 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

379

370

380− applyNS :: Name -> [String] -> Name

381− applyNS n [] = n

382− applyNS n ns = sNS n ns

383−

384 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

371 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

385 splitPi = splitPi' []

372 splitPi = splitPi' []

386 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

373 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

@@ -421,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do

421 simpleName (MN i n) = str n ++ show i

408 simpleName (MN i n) = str n ++ show i

422 simpleName n = show n

409 simpleName n = show n

423

410

424− nameSpaces :: Name -> [String]

425− nameSpaces (NS _ ns) = map str ns

426− nameSpaces _ = []

427−

428 freshName :: String -> EliminatorState Name

411 freshName :: String -> EliminatorState Name

429 freshName key = do

412 freshName key = do

430 nameMap <- get

413 nameMap <- get

src/Idris/Elab/Implementation.hs−4

@@ -56,7 +56,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

56 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

57 cs -> tclift $ tfail $ At fc

58 (CantResolveAlts (map fst cs))

59− let constraint = PApp fc (PRef fc [] n) (map pexp ps)

60 let iname = mkiname n (namespace info) ps expn

59 let iname = mkiname n (namespace info) ps expn

61 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

60 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

62 ist <- getIState

61 ist <- getIState

@@ -144,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

144 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

143 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

145 ist <- getIState

144 ist <- getIState

146 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

145 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

147− let wb = wbTys ++ wbVals

148

146

149 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

147 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

150 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

148 logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

@@ -277,8 +275,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

277 mkMethApp ps (n, _, _, ty)

275 mkMethApp ps (n, _, _, ty)

278 = lamBind 0 ty (papp fc (PRef fc [] n)

276 = lamBind 0 ty (papp fc (PRef fc [] n)

279 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

277 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

280− where

281− needed is p = pname p `elem` map pname is

282

278

283 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

279 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

284 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

280 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

src/Idris/Elab/Interface.hs+1−15

@@ -94,8 +94,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

94 ims <- mapM (tdecl impps mnames) mdecls

95 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

96 (filter clause ds)

97− let (methods, imethods)

97+ let imethods = map (\ (x, y, z) -> y) ims

98− = unzip (map (\ (x, y, z) -> (x, y)) ims)

99 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

98 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

100

99

101 addInterface tn (CI cn (map nodoc imethods) defaults idecls

100 addInterface tn (CI cn (map nodoc imethods) defaults idecls

@@ -367,13 +366,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

367 return (PTy doc [] syn fc o m mfc ty',

366 return (PTy doc [] syn fc o m mfc ty',

368 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

367 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

369

368

370− updateIMethod :: [(Name, PTerm)] ->

371− (Name, (a, b, c, d, PTerm)) ->

372− (Name, (a, b, c, d, PTerm))

373− updateIMethod ns tm@(n, (isf, mfc, doc, o, ty))

374− | Just ty' <- lookup (nsroot n) ns = (n, (isf, mfc, doc, o, ty'))

375− | otherwise = tm

376−

377 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

369 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

378 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

370 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

379 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc

371 getMArgs (PPi (Constraint _ _ _) n _ ty sc) = CA : getMArgs sc

@@ -423,12 +415,6 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

423 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

415 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

424 toExp ns e sc = sc

416 toExp ns e sc = sc

425

417

426−-- | Get the method declaration name corresponding to a user-provided name

427−mdec :: Name -> Name

428−mdec (UN n) = SN (MethodN (UN n))

429−mdec (NS x n) = NS (mdec x) n

430−mdec x = x

431−

432-- | Get the docstring corresponding to a member, if one exists

418-- | Get the docstring corresponding to a member, if one exists

433memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

419memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

434memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

420memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

src/Idris/Elab/Record.hs−26

@@ -16,7 +16,6 @@ import Idris.Docstrings

16import Idris.Elab.Data

17import Idris.Error

18import Idris.Output (sendHighlighting)

19−import Idris.Parser.Expr (tryFullExpr)

20

19

21import Control.Monad

20import Control.Monad

22import Data.List

21import Data.List

@@ -212,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

212 isFieldOrParam' :: (Name, a) -> Bool

211 isFieldOrParam' :: (Name, a) -> Bool

213 isFieldOrParam' = isFieldOrParam . fst

212 isFieldOrParam' = isFieldOrParam . fst

214

213

215− isField :: Name -> Bool

216− isField = flip elem fieldNames

217−

218− isField' :: (Name, a, b, c, d, f) -> Bool

219− isField' (n, _, _, _, _, _) = isField n

220−

221− fieldTerms :: [PTerm]

222− fieldTerms = [t | (_, _, _, t, _) <- fields]

223−

224 -- Delabs the TT to PTerm

214 -- Delabs the TT to PTerm

225 -- This is not good.

215 -- This is not good.

226 -- However, for machine generated implicits, there seems to be no PTerm available.

216 -- However, for machine generated implicits, there seems to be no PTerm available.

@@ -239,13 +229,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

239 freeName (NS n s) = NS (freeName n) s

229 freeName (NS n s) = NS (freeName n) s

240 freeName n = n

230 freeName n = n

241

231

242− -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.

243− zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]

244− zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')

245− zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])

246− where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring

247− zipParams _ [] [] = []

248−

249 paramName :: Name -> Name

232 paramName :: Name -> Name

250 paramName (UN n) = sUN ("param_" ++ str n)

233 paramName (UN n) = sUN ("param_" ++ str n)

251 paramName (MN i n) = sMN i ("param_" ++ str n)

234 paramName (MN i n) = sMN i ("param_" ++ str n)

@@ -282,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

282 fieldDep :: Name -> PTerm -> (Name, [Name])

265 fieldDep :: Name -> PTerm -> (Name, [Name])

283 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

266 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

284

267

285− -- | A list of fields depending on another field.

286− dependentFields :: [Name]

287− dependentFields = filter depends fieldNames

288− where

289− depends :: Name -> Bool

290− depends n = case lookup n fieldDependencies of

291− Just xs -> not $ null xs

292− Nothing -> False

293−

294 -- | A list of fields depended on by other fields.

268 -- | A list of fields depended on by other fields.

295 dependedOn :: [Name]

269 dependedOn :: [Name]

296 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

270 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

src/Idris/Elab/Term.hs+1−51

@@ -79,7 +79,6 @@ build :: IState

79 -> ElabD ElabResult

80build ist info emode opts fn tm

81 = do elab ist info emode opts fn tm

82− let tmIn = tm

83 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

82 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

84 [TIPartial] -> True

83 [TIPartial] -> True

85 _ -> False

84 _ -> False

@@ -157,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

157 PTerm ->

156 PTerm ->

158 ElabD ElabResult

157 ElabD ElabResult

159buildTC ist info emode opts fn ns tm

158buildTC ist info emode opts fn ns tm

160− = do let tmIn = tm

161− let inf = case lookupCtxt fn (idris_tyinfodata ist) of

159+ = do let inf = case lookupCtxt fn (idris_tyinfodata ist) of

162 [TIPartial] -> True

160 [TIPartial] -> True

163 _ -> False

161 _ -> False

164 -- set name supply to begin after highest index in tm

162 -- set name supply to begin after highest index in tm

@@ -184,7 +182,6 @@ buildTC ist info emode opts fn ns tm

184 if (log /= "")

182 if (log /= "")

185 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

183 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

186 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

184 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

187− where pattern = emode == ELHS || emode == EImpossible

188

185

189-- | return whether arguments of the given constructor name can be

186-- | return whether arguments of the given constructor name can be

190-- matched on. If they're polymorphic, no, unless the type has beed

187-- matched on. If they're polymorphic, no, unless the type has beed

@@ -241,7 +238,6 @@ elab ist info emode opts fn tm

241 = do let loglvl = opt_logLevel (idris_options ist)

238 = do let loglvl = opt_logLevel (idris_options ist)

242 when (loglvl > 5) $ unifyLog True

239 when (loglvl > 5) $ unifyLog True

243 compute -- expand type synonyms, etc

240 compute -- expand type synonyms, etc

244− let fc = maybe "(unknown)"

245 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

241 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

246 est <- getAux

242 est <- getAux

247 sequence_ (get_delayed_elab est)

243 sequence_ (get_delayed_elab est)

@@ -277,14 +273,6 @@ elab ist info emode opts fn tm

277 Placeholder -> (True, priority arg)

273 Placeholder -> (True, priority arg)

278 tm -> (False, priority arg)

274 tm -> (False, priority arg)

279

275

280− toElab ina arg = case getTm arg of

281− Placeholder -> Nothing

282− v -> Just (priority arg, elabE ina (elabFC info) v)

283−

284− toElab' ina arg = case getTm arg of

285− Placeholder -> Nothing

286− v -> Just (elabE ina (elabFC info) v)

287−

288 mkPat = do hs <- get_holes

276 mkPat = do hs <- get_holes

289 tm <- get_term

277 tm <- get_term

290 case hs of

278 case hs of

@@ -350,18 +338,6 @@ elab ist info emode opts fn tm

350 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

338 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

351 notDelay _ = True

339 notDelay _ = True

352

340

353− local f = do e <- get_env

354− return (f `elem` map fstEnv e)

355−

356− -- | Is a constant a type?

357− constType :: Const -> Bool

358− constType (AType _) = True

359− constType StrType = True

360− constType VoidType = True

361− constType _ = False

362−

363− -- "guarded" means immediately under a constructor, to help find patvars

364−

365 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

341 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

366 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

342 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

367 -> PTerm -- ^ The term to elaborate

343 -> PTerm -- ^ The term to elaborate

@@ -597,13 +573,6 @@ elab ist info emode opts fn tm

597 (P _ n' _, _) -> n == n'

573 (P _ n' _, _) -> n == n'

598 _ -> False

574 _ -> False

599

575

600− showQuick (CantUnify _ (l, _) (r, _) _ _ _)

601− = show (l, r)

602− showQuick (ElaboratingArg _ _ _ e) = showQuick e

603− showQuick (At _ e) = showQuick e

604− showQuick (ProofSearchFail (Msg _)) = "search fail"

605− showQuick _ = "No chance"

606−

607 elab' ina _ (PPatvar fc n) | bindfree

576 elab' ina _ (PPatvar fc n) | bindfree

608 = do patvar n

577 = do patvar n

609 update_term liftPats

578 update_term liftPats

@@ -621,8 +590,6 @@ elab ist info emode opts fn tm

621 = do ty <- goal

590 = do ty <- goal

622 testImplicitWarning fc n ty

591 testImplicitWarning fc n ty

623 let ina = e_inarg ec

592 let ina = e_inarg ec

624− guarded = e_guarded ec

625− inty = e_intype ec

626 ctxt <- get_context

593 ctxt <- get_context

627 env <- get_env

594 env <- get_env

628

595

@@ -884,7 +851,6 @@ elab ist info emode opts fn tm

884 _ -> do mapM_ setInjective (map getTm args)

851 _ -> do mapM_ setInjective (map getTm args)

885 -- maybe more things are solvable now

852 -- maybe more things are solvable now

886 unifyProblems

853 unifyProblems

887− let guarded = isConName f ctxt

888-- trace ("args is " ++ show args) $ return ()

854-- trace ("args is " ++ show args) $ return ()

889 ns <- apply (Var f) (map isph args)

855 ns <- apply (Var f) (map isph args)

890-- trace ("ns is " ++ show ns) $ return ()

856-- trace ("ns is " ++ show ns) $ return ()

@@ -994,10 +960,6 @@ elab ist info emode opts fn tm

994 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

960 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

995 | otherwise = getDets (i + 1) ds as

961 | otherwise = getDets (i + 1) ds as

996

962

997− tacTm (PTactics _) = True

998− tacTm (PProof _) = True

999− tacTm _ = False

1000−

1001 setInjective (PRef _ _ n) = setinj n

963 setInjective (PRef _ _ n) = setinj n

1002 setInjective (PApp _ (PRef _ _ n) _) = setinj n

964 setInjective (PApp _ (PRef _ _ n) _) = setinj n

1003 setInjective _ = return ()

965 setInjective _ = return ()

@@ -1072,7 +1034,6 @@ elab ist info emode opts fn tm

1072 matchProblems True

1034 matchProblems True

1073 args <- get_env

1035 args <- get_env

1074 envU <- mapM (getKind args) args

1036 envU <- mapM (getKind args) args

1075− let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

1076

1037

1077 -- Drop the unique arguments used in the term already

1038 -- Drop the unique arguments used in the term already

1078 -- and in the scrutinee (since it's

1039 -- and in the scrutinee (since it's

@@ -1150,12 +1111,6 @@ elab ist info emode opts fn tm

1150 UType AllTypes -> return (n, True)

1111 UType AllTypes -> return (n, True)

1151 _ -> return (n, False)

1112 _ -> return (n, False)

1152

1113

1153− tcName tm | (P _ n _, _) <- unApply tm

1154− = case lookupCtxt n (idris_interfaces ist) of

1155− [_] -> True

1156− _ -> False

1157− tcName _ = False

1158−

1159 isNotLift env n

1114 isNotLift env n

1160 = case lookupBinder n env of

1115 = case lookupBinder n env of

1161 Just ty ->

1116 Just ty ->

@@ -1164,10 +1119,6 @@ elab ist info emode opts fn tm

1164 _ -> False

1119 _ -> False

1165 _ -> False

1120 _ -> False

1166

1121

1167− usedIn ns (n, b)

1168− = n `elem` ns

1169− || any (\x -> x `elem` ns) (allTTNames (binderTy b))

1170−

1171 elab' ina fc (PUnifyLog t) = do unifyLog True

1122 elab' ina fc (PUnifyLog t) = do unifyLog True

1172 elab' ina fc t

1123 elab' ina fc t

1173 unifyLog False

1124 unifyLog False

@@ -2710,7 +2661,6 @@ processTacticDecls info steps =

2710

2661

2711 RDatatypeDefnInstrs tyn tyconTy ctors ->

2662 RDatatypeDefnInstrs tyn tyconTy ctors ->

2712 do let cn (n, _, _) = n

2663 do let cn (n, _, _) = n

2713− cimpls (_, impls, _) = impls

2714 cty (_, _, t) = t

2664 cty (_, _, t) = t

2715 addIBC (IBCDef tyn)

2665 addIBC (IBCDef tyn)

2716 mapM_ (addIBC . IBCDef . cn) ctors

2666 mapM_ (addIBC . IBCDef . cn) ctors

src/Idris/Elab/Transform.hs−1

@@ -38,7 +38,6 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

38 sendHighlighting highlights

39 updateIState $ \i -> i { idris_name = newGName }

40 let lhs_tm = orderPats (getInferTerm lhs')

41− let lhs_ty = getInferType lhs'

42 let newargs = pvars i lhs_tm

41 let newargs = pvars i lhs_tm

43

42

44 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

43 (clhs_tm_in, clhs_ty) <- recheckC_borrowing False False [] (constraintNS info) fc id [] lhs_tm

src/Idris/Elab/Type.hs−13

@@ -169,11 +169,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

169 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

170

171 let (fam, _) = unApply (getRetTy nty')

172− let corec = case fam of

173− P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

174− [TI _ True _ _ _ _] -> True

175− _ -> False

176− _ -> False

177 -- Productivity checking now via checking for guarded 'Delay'

172 -- Productivity checking now via checking for guarded 'Delay'

178 let opts' = opts -- if corec then (Coinductive : opts) else opts

173 let opts' = opts -- if corec then (Coinductive : opts) else opts

179 let usety = if norm then nty' else nty

174 let usety = if norm then nty' else nty

@@ -224,14 +219,6 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

224 _ -> return ()

219 _ -> return ()

225 return usety

220 return usety

226 where

221 where

227− -- for making an internalapp, we only want the explicit ones, and don't

228− -- want the parameters, so just take the arguments which correspond to the

229− -- user declared explicit ones

230− mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')

231− | e == e' = PPi e n fc ty (mergeTy sc sc')

232− | otherwise = mergeTy sc sc'

233− mergeTy _ sc = sc

234−

235 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

222 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

236

223

237 err = txt "Err"

224 err = txt "Err"

src/Idris/Elab/Utils.hs+1−2

@@ -118,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

118elabCaseBlock info opts d@(PClauses f o n ps)

119 = do addIBC (IBCDef n)

120 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

121− let opts' = nub (o ++ opts)

122 -- propagate totality assertion to the new definitions

121 -- propagate totality assertion to the new definitions

123 let opts' = filter propagatable opts

122 let opts' = filter propagatable opts

124 setFlags n opts'

123 setFlags n opts'

@@ -746,7 +745,7 @@ pruneByType _ _ t _ _ as = as

746-- to it later - just returns 'var' for now. EB)

745-- to it later - just returns 'var' for now. EB)

747isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

746isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

748isPlausible ist var env n ty

747isPlausible ist var env n ty

749− = let (hvar, interfaces) = collectConstraints [] [] ty in

748+ = let (hvar, _) = collectConstraints [] [] ty in

750 case hvar of

749 case hvar of

751 Nothing -> True

750 Nothing -> True

752 Just rth -> var -- trace (show (rth, interfaces)) var

751 Just rth -> var -- trace (show (rth, interfaces)) var

src/Idris/ElabDecls.hs−6

@@ -244,12 +244,6 @@ elabDecl' what info (PParams f ns ps)

244 let nblock = pblock i

245 mapM_ (elabDecl' what info) nblock

246 where

247− pinfo = let ds = concatMap tldeclared ps

248− newps = params info ++ ns

249− dsParams = map (\n -> (n, map fst newps)) ds

250− newb = addAlist dsParams (inblock info) in

251− info { params = newps,

252− inblock = newb }

253 pblock i = map (expandParamsD False i id ns

247 pblock i = map (expandParamsD False i id ns

254 (concatMap tldeclared ps)) ps

248 (concatMap tldeclared ps)) ps

255

249

src/Idris/Erasure.hs−4

@@ -287,7 +287,6 @@ buildDepMap ci used externs ctx startNames

287 -- mini-DSL for postulates

288 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

289 it n is = [(sUN n, Arg i) | i <- is]

290− mn n is = [(MN 0 $ pack n, Arg i) | i <- is]

291

290

292 -- believe_me is special because it does not use all its arguments

291 -- believe_me is special because it does not use all its arguments

293 specialPrims = S.fromList [sUN "prim__believe_me"]

292 specialPrims = S.fromList [sUN "prim__believe_me"]

@@ -624,9 +623,6 @@ buildDepMap ci used externs ctx startNames

624 union :: Deps -> Deps -> Deps

623 union :: Deps -> Deps -> Deps

625 union = M.unionWith (M.unionWith S.union)

624 union = M.unionWith (M.unionWith S.union)

626

625

627− unions :: [Deps] -> Deps

628− unions = M.unionsWith (M.unionWith S.union)

629−

630 unionMap :: (a -> Deps) -> [a] -> Deps

626 unionMap :: (a -> Deps) -> [a] -> Deps

631 unionMap f = M.unionsWith (M.unionWith S.union) . map f

627 unionMap f = M.unionsWith (M.unionWith S.union) . map f

632

628

src/Idris/ErrReverse.hs−11

@@ -12,7 +12,6 @@ module Idris.ErrReverse(errReverse) where

12import Idris.AbsSyntax

13import Idris.Core.Evaluate (unfold)

14import Idris.Core.TT

15−import Util.Pretty

16

15

17import Data.List

16import Data.List

18

17

@@ -72,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)

72 Just (fs ++ as)

71 Just (fs ++ as)

73 -- no matching Binds, for now...

72 -- no matching Binds, for now...

74 match' ns x y = if x == y then Just [] else Nothing

73 match' ns x y = if x == y then Just [] else Nothing

75−

76− -- if the term under a lambda is huge, there's no much point in showing

77− -- it as it won't be very enlightening.

78−

79− elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

80− elideLambdas (Bind n (Lam _ t) sc)

81− | size sc > 200 = P Ref (sUN "...") Erased

82− elideLambdas (Bind n b sc)

83− = Bind n (fmap elideLambdas b) (elideLambdas sc)

84− elideLambdas t = t

src/Idris/IBC.hs+1−12

@@ -51,7 +51,6 @@ data IBCPhase = IBC_Building -- ^ when building the module tree

51data IBCFile = IBCFile {

52 ver :: Word16

53 , sourcefile :: FilePath

54− , ibc_reachablenames :: ![Name]

55 , ibc_imports :: ![(Bool, FilePath)]

54 , ibc_imports :: ![(Bool, FilePath)]

56 , ibc_importdirs :: ![FilePath]

55 , ibc_importdirs :: ![FilePath]

57 , ibc_sourcedirs :: ![FilePath]

56 , ibc_sourcedirs :: ![FilePath]

@@ -108,7 +107,7 @@ deriving instance Binary IBCFile

108!-}

107!-}

109

108

110initIBC :: IBCFile

109initIBC :: IBCFile

111−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

110+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

112

111

113hasValidIBCVersion :: FilePath -> Idris Bool

112hasValidIBCVersion :: FilePath -> Idris Bool

114hasValidIBCVersion fp = do

113hasValidIBCVersion fp = do

@@ -1123,16 +1122,6 @@ instance Binary Accessibility where

1123 3 -> return Hidden

1122 3 -> return Hidden

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

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

1125

1124

1126−safeToEnum :: (Enum a, Bounded a, Integral int) => String -> int -> a

1127−safeToEnum label x' = result

1128− where

1129− x = fromIntegral x'

1130− result

1131− | x < fromEnum (minBound `asTypeOf` result)

1132− || x > fromEnum (maxBound `asTypeOf` result)

1133− = error $ label ++ ": corrupted binary representation in IBC"

1134− | otherwise = toEnum x

1135−

1136instance Binary PReason where

1125instance Binary PReason where

1137 put x

1126 put x

1138 = case x of

1127 = case x of

src/Idris/IdeMode.hs−3

@@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where

176encodeName :: Name -> String

177encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

178

179−decodeName :: String -> Name

180−decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

181−

182encodeTerm :: [(Name, Bool)] -> Term -> String

179encodeTerm :: [(Name, Bool)] -> Term -> String

183encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

180encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

184 (bnd, tm)

181 (bnd, tm)

src/Idris/IdrisDoc.hs−7

@@ -248,13 +248,6 @@ getAccess ist n =

248 [(_, acc)] -> acc

249 _ -> Private

250

251−-- | Simple predicate for whether an NsItem has Docs

252−hasDoc :: NsItem -- ^ The NsItem to test

253− -> Bool -- ^ The result

254−hasDoc (_, Just _, _) = True

255−hasDoc _ = False

256−

257−

258-- | Predicate saying whether a Name possibly may have docs defined

251-- | Predicate saying whether a Name possibly may have docs defined

259-- Without this, getDocs from Idris.Docs may fail a pattern match.

252-- Without this, getDocs from Idris.Docs may fail a pattern match.

260mayHaveDocs :: Name -- ^ The Name to test

253mayHaveDocs :: Name -- ^ The Name to test

src/Idris/Imports.hs+2−2

@@ -29,13 +29,13 @@ pkgIndex :: String -> FilePath

29pkgIndex s = "00" ++ s ++ "-idx.ibc"

30

31srcPath :: FilePath -> FilePath

32−srcPath fp = let (n, ext) = splitExtension fp in

32+srcPath fp = let (_, ext) = splitExtension fp in

33 case ext of

34 ".idr" -> fp

35 _ -> fp ++ ".idr"

36

37lsrcPath :: FilePath -> FilePath

38−lsrcPath fp = let (n, ext) = splitExtension fp in

38+lsrcPath fp = let (_, ext) = splitExtension fp in

39 case ext of

40 ".lidr" -> fp

41 _ -> fp ++ ".lidr"

src/Idris/Interactive.hs+1−3

@@ -382,9 +382,7 @@ makeLemma fn updatefile l n

382 StringAtom lem_app]]]

383 in runIO . hPutStrLn h $ convSExp "return" good n

384

385− where getIndent s = length (takeWhile isSpace s)

386−

387− appArgs skip 0 _ = ""

385+ where appArgs skip 0 _ = ""

388 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

386 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

389 | (thead c /= '_' && n `notElem` skip)

387 | (thead c /= '_' && n `notElem` skip)

390 = " " ++ show n ++ appArgs skip (i - 1) sc

388 = " " ++ show n ++ appArgs skip (i - 1) sc

src/Idris/Package.hs−2

@@ -333,11 +333,9 @@ auditPackage True ipkg = do

333 getIdrisFiles :: FilePath -> IO [FilePath]

334 getIdrisFiles dir = do

335 contents <- getDirectoryContents dir

336− let contents' = filter (\fname -> fname /= "." && fname /= "..") contents

337

336

338 -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

337 -- [ NOTE ] Directory >= 1.2.5.0 introduced `listDirectory` but later versions of directory appear to be causing problems with ghc 7.10.3 and cabal 1.22 in travis. Let's reintroduce the old ranges for directory to be sure.

339

338

340−

341 files <- forM contents (findRest dir)

339 files <- forM contents (findRest dir)

342 return $ filter (isIdrisFile) (concat files)

340 return $ filter (isIdrisFile) (concat files)

343

341

src/Idris/Parser.hs+1−14

@@ -794,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]

794mutual syn =

795 do reservedHL "mutual"

796 openBlock

797− let pvars = syn_params syn

798 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

797 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

799 closeBlock

798 closeBlock

800 fc <- getFC

799 fc <- getFC

@@ -1145,7 +1144,6 @@ clause syn

1145 Just t -> return t

1144 Just t -> return t

1146 Nothing -> fail "Invalid clause"

1145 Nothing -> fail "Invalid clause"

1147 (do r <- rhs syn n

1146 (do r <- rhs syn n

1148− let ctxt = tt_ctxt ist

1149 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1147 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

1150 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1148 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1151 popIndent

1149 popIndent

@@ -1169,8 +1167,6 @@ clause syn

1169 fc <- getFC

1167 fc <- getFC

1170 n_in <- fst <$> fnName; let n = expandNS syn n_in

1168 n_in <- fst <$> fnName; let n = expandNS syn n_in

1171 r <- rhs syn n

1169 r <- rhs syn n

1172− ist <- get

1173− let ctxt = tt_ctxt ist

1174 let wsyn = syn { syn_namespace = [] }

1170 let wsyn = syn { syn_namespace = [] }

1175 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1171 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1176 popIndent

1172 popIndent

@@ -1227,8 +1223,6 @@ clause syn

1227 wargs <- many (wExpr syn)

1223 wargs <- many (wExpr syn)

1228 let capp = PApp fc (PRef nfc [nfc] n) args

1224 let capp = PApp fc (PRef nfc [nfc] n) args

1229 (do r <- rhs syn n

1225 (do r <- rhs syn n

1230− ist <- get

1231− let ctxt = tt_ctxt ist

1232 let wsyn = syn { syn_namespace = [] }

1226 let wsyn = syn { syn_namespace = [] }

1233 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1227 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

1234 popIndent

1228 popIndent

@@ -1573,11 +1567,6 @@ parseImports fname input

1573 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1567 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1574 return ((mdoc, mname, ps, mrk'), annots, i)

1568 return ((mdoc, mname, ps, mrk'), annots, i)

1575

1569

1576− imp m = ImportInfo False (toPath m)

1577− Nothing [] NoFC NoFC

1578− ns = Spl.splitOn "."

1579− toPath = foldl1' (</>) . ns

1580−

1581 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1570 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1582 addPath [] _ = []

1571 addPath [] _ = []

1583 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

1572 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

@@ -1882,8 +1871,6 @@ loadSource lidr f toline

1882

1871

1883{-| Adds names to hide list -}

1872{-| Adds names to hide list -}

1884addHides :: Ctxt Accessibility -> Idris ()

1873addHides :: Ctxt Accessibility -> Idris ()

1885−addHides xs = do i <- getIState

1886− let defh = default_access i

1887− mapM_ doHide (toAlist xs)

1874+addHides xs = mapM_ doHide (toAlist xs)

1888 where doHide (n, a) = do setAccessibility n a

1875 where doHide (n, a) = do setAccessibility n a

1889 addIBC (IBCAccess n a)

1876 addIBC (IBCAccess n a)

src/Idris/Parser/Data.hs−10

@@ -9,7 +9,6 @@ Maintainer : The Idris Community.

9module Idris.Parser.Data where

10

11import Idris.AbsSyntax

12−import Idris.Core.Evaluate

13import Idris.Core.TT

12import Idris.Core.TT

14import Idris.Docstrings

13import Idris.Docstrings

15import Idris.Options

14import Idris.Options

@@ -55,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

55 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

54 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

56 <?> "record type declaration"

55 <?> "record type declaration"

57 where

56 where

58− getRecNames :: SyntaxInfo -> PTerm -> [Name]

59− getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]

60− ++ getRecNames syn sc

61− getRecNames _ _ = []

62−

63 getName (Just (n, _), _, _, _) = Just n

57 getName (Just (n, _), _, _, _) = Just n

64 getName _ = Nothing

58 getName _ = Nothing

65

59

66− toFreeze :: Maybe Accessibility -> Maybe Accessibility

67− toFreeze (Just Frozen) = Just Private

68− toFreeze x = x

69−

70 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

60 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

71 recordBody syn tyn = do

61 recordBody syn tyn = do

72 ist <- get

62 ist <- get

src/Idris/PartialEval.hs−4

@@ -258,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =

258 mkRHSargs (_ : ns) as = mkRHSargs ns as

259 mkRHSargs _ _ = []

260

261− mkSubst :: (Term, Term) -> Maybe (Name, Term)

262− mkSubst (P _ n _, t) = Just (n, t)

263− mkSubst _ = Nothing

264−

265-- | Creates a new declaration for a specialised function application.

261-- | Creates a new declaration for a specialised function application.

266-- Simple version at the moment: just create a version which is a direct

262-- Simple version at the moment: just create a version which is a direct

267-- application of the function to be specialised.

263-- application of the function to be specialised.

src/Idris/Primitives.hs+1−38

@@ -17,7 +17,6 @@ import Data.Bits

17import Data.Char

18import Data.Function (on)

19import Data.Int

20−import Data.Word

21

20

22data Prim = Prim { p_name :: Name,

21data Prim = Prim { p_name :: Name,

23 p_type :: Type,

22 p_type :: Type,

@@ -31,10 +30,9 @@ ty :: [Const] -> Const -> Type

31ty [] x = Constant x

30ty [] x = Constant x

32ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

31ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

33

32

34−total, partial, iopartial :: Totality

33+total, partial :: Totality

35total = Total []

34total = Total []

36partial = Partial NotCovering

35partial = Partial NotCovering

37−iopartial = Partial ExternalIO

38

36

39primitives :: [Prim]

37primitives :: [Prim]

40primitives =

38primitives =

@@ -232,36 +230,6 @@ intConv ity =

232 (1, LFloatInt ity) total

230 (1, LFloatInt ity) total

233 ]

231 ]

234

232

235−bitcastPrim :: ArithTy -> ArithTy -> (ArithTy -> [Const] -> Maybe Const) -> PrimFn -> Prim

236−bitcastPrim from to impl prim =

237− Prim (sUN $ "prim__bitcast" ++ aTyName from ++ "_" ++ aTyName to) (ty [AType from] (AType to)) 1 (impl to)

238− (1, prim) total

239−

240−concatWord8 :: (Word8, Word8) -> Word16

241−concatWord8 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 8)

242−

243−concatWord16 :: (Word16, Word16) -> Word32

244−concatWord16 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 16)

245−

246−concatWord32 :: (Word32, Word32) -> Word64

247−concatWord32 (high, low) = fromIntegral high .|. (fromIntegral low `shiftL` 32)

248−

249−truncWord16 :: Bool -> Word16 -> Word8

250−truncWord16 True x = fromIntegral (x `shiftR` 8)

251−truncWord16 False x = fromIntegral x

252−

253−truncWord32 :: Bool -> Word32 -> Word16

254−truncWord32 True x = fromIntegral (x `shiftR` 16)

255−truncWord32 False x = fromIntegral x

256−

257−truncWord64 :: Bool -> Word64 -> Word32

258−truncWord64 True x = fromIntegral (x `shiftR` 32)

259−truncWord64 False x = fromIntegral x

260−

261−aTyName :: ArithTy -> String

262−aTyName (ATInt t) = intTyName t

263−aTyName ATFloat = "Float"

264−

265iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

233iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

266iCmp ity op self impl irop totality

234iCmp ity op self impl irop totality

267 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

235 = Prim (sUN $ "prim__" ++ op ++ intTyName ity)

@@ -292,11 +260,6 @@ bfBin op [Fl x, Fl y] = let i = (if op x y then 1 else 0) in

292 Just $ I i

260 Just $ I i

293bfBin _ _ = Nothing

261bfBin _ _ = Nothing

294

262

295−bcBin :: (Char -> Char -> Bool) -> [Const] -> Maybe Const

296−bcBin op [Ch x, Ch y] = let i = (if op x y then 1 else 0) in

297− Just $ I i

298−bcBin _ _ = Nothing

299−

300bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

263bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

301bsBin op [Str x, Str y]

264bsBin op [Str x, Str y]

302 = let i = (if op x y then 1 else 0) in

265 = let i = (if op x y then 1 else 0) in

src/Idris/ProofSearch.hs+1−14

@@ -27,7 +27,6 @@ import Control.Monad

27import Control.Monad.State.Strict

28import Data.List

29import qualified Data.Set as S

30−import Debug.Trace

31

30

32-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

31-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

33

32

@@ -49,7 +48,6 @@ trivialHoles psnames ok elab ist

49 tryAll ((x, _, b):xs)

48 tryAll ((x, _, b):xs)

50 = do -- if type of x has any holes in it, move on

49 = do -- if type of x has any holes in it, move on

51 hs <- get_holes

50 hs <- get_holes

52− let badhs = hs -- filter (flip notElem holesOK) hs

53 g <- goal

51 g <- goal

54 -- anywhere but the top is okay for a hole, if holesOK set

52 -- anywhere but the top is okay for a hole, if holesOK set

55 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

53 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

@@ -85,7 +83,6 @@ trivialTCs ok elab ist

85 tryAll ((x, _, b):xs)

83 tryAll ((x, _, b):xs)

86 = do -- if type of x has any holes in it, move on

84 = do -- if type of x has any holes in it, move on

87 hs <- get_holes

85 hs <- get_holes

88− let badhs = hs -- filter (flip notElem holesOK) hs

89 g <- goal

86 g <- goal

90 env <- get_env

87 env <- get_env

91 -- anywhere but the top is okay for a hole, if holesOK set

88 -- anywhere but the top is okay for a hole, if holesOK set

@@ -230,9 +227,6 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

230 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

227 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

231 notHole _ _ = True

228 notHole _ _ = True

232

229

233− inHS hs (P _ n _) = n `elem` hs

234− isHS _ _ = False

235−

236 toUN t@(P nt (MN i n) ty)

230 toUN t@(P nt (MN i n) ty)

237 | ('_':xs) <- str n = t

231 | ('_':xs) <- str n = t

238 | otherwise = P nt (UN n) ty

232 | otherwise = P nt (UN n) ty

@@ -441,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

441 isMeta ns (P _ n _) = n `elem` ns

435 isMeta ns (P _ n _) = n `elem` ns

442 isMeta _ _ = False

436 isMeta _ _ = False

443

437

444− notHole hs (P _ n _, c)

445− | (P _ cn _, _) <- unApply (getRetTy c),

446− n `elem` hs && isConName cn (tt_ctxt ist) = False

447− | Constant _ <- c = not (n `elem` hs)

448− notHole _ _ = True

449−

450 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

438 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

451

439

452 addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn

440 addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn

@@ -484,7 +472,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

484 | otherwise

472 | otherwise

485 = do lams <- introImps

473 = do lams <- introImps

486 t <- goal

474 t <- goal

487− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

488-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

475-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

489-- else do

476-- else do

490 -- if there's a hole in the goal, don't even try

477 -- if there's a hole in the goal, don't even try

@@ -502,7 +489,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

502-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

489-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

503 mapM_ (\ (_,n) -> do focus n

490 mapM_ (\ (_,n) -> do focus n

504 t' <- goal

491 t' <- goal

505− let (tc', ttype) = unApply (getRetTy t')

492+ let (tc', _) = unApply (getRetTy t')

506 let got = fst (unApply (getRetTy t))

493 let got = fst (unApply (getRetTy t))

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

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

508 then depth - 1 else depth

495 then depth - 1 else depth

src/Idris/Prover.hs+1−2

@@ -164,7 +164,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

164 iputGoal rendered

165

166 where

167− (h : hs) = holes ps -- apparently the pattern guards don't give us this

167+ (h : _) = holes ps -- apparently the pattern guards don't give us this

168

169 ppo = ppOptionIst ist

170

@@ -500,7 +500,6 @@ checkType e prf t = do

500 putIState ist { tt_ctxt = ctxt' }

501 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

502 let ppo = ppOptionIst ist

503− ty' = normaliseC ctxt [] ty

504 infixes = idris_infixes ist

503 infixes = idris_infixes ist

505 action = case tm of

504 action = case tm of

506 TType _ ->

505 TType _ ->

src/Idris/REPL.hs+2−17

@@ -402,7 +402,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

402 | (n, (_, i, _, _, _)) <- idris_metavars ist

403 , not (n `elem` primDefs)

404 ]

405− let ppo = ppOptionIst ist

406 -- splitMvs is a list of pairs of names and their split types

405 -- splitMvs is a list of pairs of names and their split types

407 let splitMvs = [ (n, (premises, concl, tm))

406 let splitMvs = [ (n, (premises, concl, tm))

408 | (n, i, ty) <- mvTys ist mvs

407 | (n, i, ty) <- mvTys ist mvs

@@ -420,14 +419,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

420 runIO . hPutStrLn h $

419 runIO . hPutStrLn h $

421 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

420 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

422 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

421 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

423− firstOfThree (x, y, z) = x

424− mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs

425−

426 -- | Split a function type into a pair of premises, conclusion.

422 -- | Split a function type into a pair of premises, conclusion.

427 -- Each maintains both the original and delaborated versions.

423 -- Each maintains both the original and delaborated versions.

428 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

424 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

429 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

425 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

430− let (hs, c, pc) = splitPi ist (i - 1) rest in

426+ let (hs, c, _) = splitPi ist (i - 1) rest in

431 ((n, t, delabTy' ist [] [] t False False True):hs,

427 ((n, t, delabTy' ist [] [] t False False True):hs,

432 c, delabTy' ist [] [] c False False True)

428 c, delabTy' ist [] [] c False False True)

433 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

429 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

@@ -1021,8 +1017,7 @@ process fn (Check t)

1021 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1017 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

1022 ctxt <- getContext

1018 ctxt <- getContext

1023 ist <- getIState

1019 ist <- getIState

1024− let ppo = ppOptionIst ist

1025− ty' = if opt_evaltypes (idris_options ist)

1020+ let ty' = if opt_evaltypes (idris_options ist)

1026 then normaliseC ctxt [] ty

1021 then normaliseC ctxt [] ty

1027 else ty

1022 else ty

1028 case tm of

1023 case tm of

@@ -1127,7 +1122,6 @@ process fn (DebugInfo n)

1127 when (not (null imps)) $ iputStrLn (show imps)

1122 when (not (null imps)) $ iputStrLn (show imps)

1128 let d = lookupDefAcc n False (tt_ctxt i)

1123 let d = lookupDefAcc n False (tt_ctxt i)

1129 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1124 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1130− let cg = lookupCtxtName n (idris_callgraph i)

1131 i <- getIState

1125 i <- getIState

1132 let cg' = lookupCtxtName n (idris_callgraph i)

1126 let cg' = lookupCtxtName n (idris_callgraph i)

1133 sc <- checkSizeChange n

1127 sc <- checkSizeChange n

@@ -1457,12 +1451,6 @@ process fn (TransformInfo n)

1457 ts' = showTrans i ts in

1451 ts' = showTrans i ts in

1458 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

1452 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

1459

1453

1460−-- iRenderOutput (pretty lhs)

1461−-- iputStrLn " ==> "

1462−-- iPrintTermWithType (pprintDelab i rhs)

1463−-- iputStrLn "---------------"

1464−-- showTrans i ts

1465−

1466process fn (PPrint fmt width (PRef _ _ n))

1454process fn (PPrint fmt width (PRef _ _ n))

1467 = do outs <- pprintDef False n

1455 = do outs <- pprintDef False n

1468 iPrintResult =<< renderExternal fmt width (vsep outs)

1456 iPrintResult =<< renderExternal fmt width (vsep outs)

@@ -1470,10 +1458,7 @@ process fn (PPrint fmt width (PRef _ _ n))

1470

1458

1471process fn (PPrint fmt width t)

1459process fn (PPrint fmt width t)

1472 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1460 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1473− ctxt <- getContext

1474 ist <- getIState

1461 ist <- getIState

1475− let ppo = ppOptionIst ist

1476− ty' = normaliseC ctxt [] ty

1477 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1462 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1478

1463

1479

1464

src/Idris/REPL/Parser.hs−2

@@ -178,8 +178,6 @@ namespaceArgCmd names command doc =

178 (names, NamespaceArg, doc, namespaceArg command)

179exprArgCmd names command doc =

180 (names, ExprArg, doc, exprArg command)

181−metavarArgCmd names command doc =

182− (names, MetaVarArg, doc, fnNameArg command)

183optArgCmd names command doc =

181optArgCmd names command doc =

184 (names, OptionArg, doc, optArg command)

182 (names, OptionArg, doc, optArg command)

185proofArgCmd names command doc =

183proofArgCmd names command doc =

src/Idris/Termination.hs+2−9

@@ -142,9 +142,6 @@ checkPositive mut_ns (cn, ty')

142calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

143calcTotality fc n pats

144 = do i <- getIState

145− let opts = case lookupCtxt n (idris_flags i) of

146− [fs] -> fs

147− _ -> []

148 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

145 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

149 (failure : _) -> return failure

146 (failure : _) -> return failure

150 _ -> checkSizeChange n

147 _ -> checkSizeChange n

@@ -301,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

301buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

298buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

302 scgPat (lhs, rhs) = let lhs' = delazy lhs

299 scgPat (lhs, rhs) = let lhs' = delazy lhs

303 rhs' = delazy rhs

300 rhs' = delazy rhs

304− (f, pargs) = unApply (dePat lhs') in

301+ (_, pargs) = unApply (dePat lhs') in

305 findCalls [] Toplevel (dePat rhs') (patvars lhs')

302 findCalls [] Toplevel (dePat rhs') (patvars lhs')

306 (zip pargs [0..])

303 (zip pargs [0..])

307

304

@@ -392,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

392 fccPat cases pvs pargs args g (lhs, rhs)

389 fccPat cases pvs pargs args g (lhs, rhs)

393 = let lhs' = delazy lhs

390 = let lhs' = delazy lhs

394 rhs' = delazy rhs

391 rhs' = delazy rhs

395− (f, pargs_case) = unApply (dePat lhs')

392+ (_, pargs_case) = unApply (dePat lhs')

396 -- pargs is a pair of a term, and the argument position that

393 -- pargs is a pair of a term, and the argument position that

397 -- term appears in. If any of the arguments to the case block

394 -- term appears in. If any of the arguments to the case block

398 -- are also on the lhs, we also want those patterns to appear

395 -- are also on the lhs, we also want those patterns to appear

@@ -544,10 +541,6 @@ checkMP ist topfn i mp = if i > 0

544 collapse paths

541 collapse paths

545 else tryPath 0 [] mp 0

542 else tryPath 0 [] mp 0

546 where

543 where

547− tryPath' d path mp arg

548− = let res = tryPath d path mp arg in

549− trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

550−

551 mkBig (e, d) = (e, 10000)

544 mkBig (e, d) = (e, 10000)

552

545

553 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

546 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

src/Idris/TypeSearch.hs+2−6

@@ -13,8 +13,7 @@ module Idris.TypeSearch (

13 , defaultScoreFunction

14 ) where

15

16−import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,

16+import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)

17− putIState)

18import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

17import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

19 Idris, InterfaceInfo, OutputMode(..), PTerm,

18 Idris, InterfaceInfo, OutputMode(..), PTerm,

20 defaultSyntax, eqTy, implicitAllowed,

19 defaultSyntax, eqTy, implicitAllowed,

@@ -58,7 +57,6 @@ searchByType pkgs pterm = do

58 mapM_ loadPkgIndex pkgs

57 mapM_ loadPkgIndex pkgs

59 pterm' <- addUsingConstraints syn emptyFC pterm

58 pterm' <- addUsingConstraints syn emptyFC pterm

60 pterm'' <- implicit toplevel syn name pterm'

59 pterm'' <- implicit toplevel syn name pterm'

61− let pterm''' = addImpl [] i pterm''

62 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

60 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

63 let names = searchUsing searchPred i ty

61 let names = searchUsing searchPred i ty

64 let names' = take numLimit names

62 let names' = take numLimit names

@@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do

304

302

305isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

303isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

306isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

304isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

307− (clss, args) = unApply ty

305+ (clss, _) = unApply ty

308 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

306 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

309 getInterfaceName _ = []

307 getInterfaceName _ = []

310

308

@@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

358 usedns = map fst startingHoles

356 usedns = map fst startingHoles

359 startingHoles = argNames1 ++ argNames2

357 startingHoles = argNames1 ++ argNames2

360

358

361− startingTypes = [(retTy1, retTy2)]

362−

363

359

364 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

360 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

365 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types

361 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types