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

src/IRTS/CodegenC.hs+1−12

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

201201 = indent i ++ alloc loc tag ++

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

203203 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 [] = ""

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

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

211207 alloc Nothing tag

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

301297 iCase v (B64 w, bc) =

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

303299 ++ 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"

311300 showDefS i Nothing = ""

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

313302

src/IRTS/Defunctionalise.hs+1−51

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

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

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

166166

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−

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

194168

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

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

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

222196 = mkApplyCase n ar i

223197 | otherwise = []

224− where dupdate tlarg x = x

225198

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

227200mkApplyCase fname n ar

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

330303-- 'max' branches

331304mkBigCase cn max arg branches

332305 | 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

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

306+ | otherwise = DChkCase arg branches

357307

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

359309groupsOf x [] = []

src/IRTS/JavaScript/LangTransforms.hs−5

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

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

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

4646

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−

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

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

5449extractGlobs defs (LFun _ _ _ e) =

src/IRTS/JavaScript/Specialize.hs−11

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

5959 ]

6060 -- constructors

6161 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

6662 trueTest = id

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

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

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

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

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

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

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

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

7567 -- projections

76− justProj x n = x

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

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

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

8069 item :: String

8170 -> String

src/Idris/AbsSyntax.hs+2−32

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

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

14661466-- * finally, everything else (3)

14671467getPriority :: IState -> PTerm -> Int

1468−getPriority i tm = 1 -- pri tm

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−

1468+getPriority i tm = 1

14901469

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

14921471addStatics n tm ptm =

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

20131992 unqualified (NS _ _) = False

20141993 unqualified _ = True

20151994

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

2017− constructor _ = False

2018−

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

20201996

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

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

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

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

22042180 -- impossbility checking.

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

2206− canBeDConName fn ctxt

2181+ | canBeDConName fn ctxt

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

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

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

2210− getFn _ = Nothing

22112183 su (PApp fc f args)

22122184 = PHidden (PApp fc f args)

22132185 su (PAlternative ms b alts)

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

22642236 (ns, ss)

22652237 fs _ = ([], [])

22662238

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

2268−

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

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

22712241 spos <- get

src/Idris/AbsSyntaxTree.hs−15

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

22002200 showbasic (MN i s) = str s

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

22022202 showbasic (SN s) = show s

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

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

22052204 case ctxt' of

22062205 Nothing -> name

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

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

23492348 put (imps, n: fns)

23502349

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−

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

23662351 | not (n `elem` env)

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

src/Idris/Apropos.hs+1−7

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

1111import Idris.AbsSyntax

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

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

14− Type, toAlist)

14+ toAlist)

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

1616

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

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

104104

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

106106 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

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

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

6060

61− ibc (IBC _ _) = True

62− ibc _ = False

63−

6461 chkReload False p = p

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

6663 chkReload True p = p

src/Idris/Completion.hs−5

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

6767metavars = do i <- get

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

6969

70−

71−modules :: Idris [String]

72−modules = do i <- get

73− return $ map show $ imported i

74−

7570namespaces :: Idris [String]

7671namespaces = do

7772 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

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

269269 sc' tc defcase phase fc cs

270270 = let proj = phase == RunTime

271− vnames = fstT (head cs)

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

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

274273 chkPats = mapM chkAccessible pats in

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

285284 else return t

286285 Error err -> Error (At fc err)

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

288− defaultCase True = STerm Erased

289− defaultCase False = UnmatchedCase "Error"

290287 fstT (x, _, _) = x

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

292288

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

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

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

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

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

305301

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−

348302data Pat = PCon Bool Name Int [Pat]

349303 | PConst Const

350304 | PInferred Pat

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

400354

401355 toPat' _ t = PAny

402356

403− fixedN IT8 = "Bits8"

404− fixedN IT16 = "Bits16"

405− fixedN IT32 = "Bits32"

406− fixedN IT64 = "Bits64"

407−

408−

409357data Partition = Cons [Clause]

410358 | Vars [Clause]

411359 deriving Show

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

663611 where

664612 (acc, inacc) = partitionAcc r

665613

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

667− uniq i n = n

668−

669614getVar :: String -> CaseBuilder Name

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

671616

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

869814 = SucCase sn (mkForceSC n arg rhs)

870815 mkForceAlt n arg (DefaultCase rhs)

871816 = 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 =

607607 lift $ tfail $ TooManyArguments n

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

609609

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

611− when i (movelast n)

612−

613610 mkMN n@(MN i _) = n

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

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

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

666663 | i = getNonUnify acc is as

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

668665

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

670−

671666

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

673668apply2 fn elabs =

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

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

676671 elabArgs (map snd args) elabs

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

678− let (n, hs) = unified p

679673 end_unify

680674 solve

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

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

693687 env <- get_env

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

695689 prep_fill n (map fst claims)

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

697690 elabClaims [] False claims

698691 complete_fill

699692 end_unify

700693 where

701− priOrder Nothing Nothing = EQ

702− priOrder Nothing _ = LT

703− priOrder _ Nothing = GT

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

705−

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

707695 do n <- unique_hole (mkMN n')

708696 when (null claims) (start_unify n)

src/Idris/Core/Evaluate.hs−41

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

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

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

208208

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−

219209usable :: Bool -- specialising

220210 -> Bool -- unfolding only

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

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

393383 evApply ntimes stk top env args f

394384 = apply ntimes stk top env f args

395385

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−

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

413387 = do a' <- sc a

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

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

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

742716 _ -> return False

743717

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−

751718-- CONTEXTS -----------------------------------------------------------------

752719

753720{-| 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)

985952 CaseDef args_rt sc_rt _) ->

986953 let inl = alwaysInline -- tcdict

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

988− inlr = inl || small n args_rt sc_rt

989955 cdef = CaseDefs (args_ct, sc_ct)

990956 (args_rt, sc_rt)

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

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

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

12501216 _ -> return ()

12511217

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−

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

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

12611220tcReducible :: Name -> Context -> Bool

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

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

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

4646#else

4747-- 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

5248

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

5450

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

164160getExecState :: Exec ExecState

165161getExecState = lift get

166162

167−putExecState :: ExecState -> Exec ()

168−putExecState = lift . put

169−

170163execFail :: Err -> Exec a

171164execFail = throwE

172165

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

475468execForeign env ctxt arity ty fn xs onfail

476469 = case foreignFromTT arity ty fn xs of

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

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

479− drop arity xs) -- rest

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

472+ drop arity xs) -- rest

480473 res <- call ffun (map snd argTs)

481474 case res of

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

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

704697 return $ FFun name argFTyVals (toFDesc ty)

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

706699

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−

727700unEList :: ExecVal -> Maybe [ExecVal]

728701unEList tm = case unApplyV tm of

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

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

733706 (f, args) -> Nothing

734707

735708

736−toConst :: Term -> Maybe Const

737−toConst (Constant c) = Just c

738−toConst _ = Nothing

739−

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

741710mapMaybeM f [] = return []

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

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

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

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

180180 do ps <- get

181181 let while = while_elaborating ps

182− let dont = dontunify ps

183182 let inj = injective ps

184183 traceWhen (unifylog ps)

185184 ("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' =

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

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

494493

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−

504494unifyGoal :: Raw -> RunTactic

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

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

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

527517fill :: Raw -> RunTactic

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

529519 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)

533− (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))

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

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

538522 return $ Bind x (Guess ty val) sc

539523 where

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

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

550534match_fill :: Raw -> RunTactic

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

552536 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)

556− (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))

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

538+ (ty, Just ExpectedType)

561539 return $ Bind x (Guess ty val) sc

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

563541

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

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

572550 do let guess = forget val

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

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

575− (ty, Just ExpectedType)

576− ps <- get

577− let (uh, uns) = unified ps

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

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

553+ (ty, Just ExpectedType)

579554 return $ Bind x (Guess ty val) sc

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

581556

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

586561solve :: RunTactic

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

588563 = do ps <- get

589− let (uh, uns) = unified ps

590564 dropdots <-

591565 case lookup x (notunified ps) of

592566 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)

603577 recents = x : recents ps,

604578 implementations = implementations ps \\ [x],

605579 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

607581 return locked

608582 where dropUnified ddots [] = []

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

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

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

629603 tryLock hs t@(Bind n b sc)

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

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

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

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

634607 tryLock hs t = (t, True)

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

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

655628 _ -> normalise ctxt env t

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

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

658630 case t' of

659631 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)

661− ps <- get

662− let (uh, uns) = unified ps

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

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

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

665634 _ -> lift $ tfail $ CantIntroduce t'

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

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

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

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

760729 let tmt' = normalise ctxt env tmt

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

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

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

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

764733 case unApply tmt' of

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

771740 _ -> return []

772741 let (params, indicies) = splitTyArgs param_pos tyargs

773742 let args = getArgTys elimTy

774− let pmargs = take (length params) args

775743 let args' = drop (length params) args

776− let propTy = head args'

777744 let restargs = init $ tail args'

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

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

780− let scr = last $ tail args'

781746 let indxnames = makeIndexNames indicies

782747 currentNames <- query $ allTTNames . getProofTerm . pterm

783748 let tmnm = case tm of

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

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

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

801766 tmt'

802− where scname = sMN 0 "scarg"

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

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

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

805769 bindConsArgs [] v = v

806770 addConsHole (nm, ty) =

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

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

880844 return tm

881845

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

883−

884846solve_unified :: RunTactic

885847solve_unified ctxt env tm =

886848 do ps <- get

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

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

930892updateError ns e = e

931893

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−

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

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

942896 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

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

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

197197

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−

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

209199-- under Complete applications.

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

src/Idris/Core/TT.hs−18

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

7979import Data.Traversable (Traversable)

8080import Data.Typeable (Typeable)

8181import Debug.Trace

82−import Foreign.Storable (sizeOf)

8382import GHC.Generics (Generic)

8483import Numeric (showIntAtBase)

8584import Numeric.IEEE (IEEE(identicalIEEE))

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

431430tfail :: Err -> TC a

432431tfail e = Error e

433432

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−

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

442434discard f = f >> return ()

443435

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

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

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

512504

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

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

515−

516505instance Sized Name where

517506 size (UN n) = 1

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

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

699688nativeTyWidth IT32 = 32

700689nativeTyWidth IT64 = 64

701690

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−

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

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

711693 | AType ArithTy | StrType

src/Idris/Core/Typecheck.hs−31

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

205205 Just v' -> v'

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

207207

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−

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

215209 (TType su, TType tu) -> do

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

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

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

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

226220

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−

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

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

244223 (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

261240

262241 checkBinder (Lam rig t)

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

264− let tv' = normalise ctxt env tv

265243 convType tcns ctxt env tt

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

267245 checkBinder (Let t v)

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

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

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

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

273− let tv' = normalise ctxt env tv

274251 convertsC ctxt env vt tv

275252 convType tcns ctxt env tt

276253 return (Let tv vv, tt, vns)

277254 checkBinder (NLet t v)

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

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

280− let tv' = normalise ctxt env tv

281257 convertsC ctxt env vt tv

282258 convType tcns ctxt env tt

283259 return (NLet tv vv, tt, vns)

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

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

286262 | otherwise

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

288− let tv' = normalise ctxt env tv

289264 convType tcns ctxt env tt

290265 return (Hole tv, tt, [])

291266 checkBinder (GHole i ns t)

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

293− let tv' = normalise ctxt env tv

294268 convType tcns ctxt env tt

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

296270 checkBinder (Guess t v)

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

298272 | otherwise

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

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

301− let tv' = normalise ctxt env tv

302275 convertsC ctxt env vt tv

303276 convType tcns ctxt env tt

304277 return (Guess tv vv, tt, vns)

305278 checkBinder (PVar rig t)

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

307− let tv' = normalise ctxt env tv

308280 convType tcns ctxt env tt

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

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

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

312282 checkBinder (PVTy t)

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

314− let tv' = normalise ctxt env tv

315284 convType tcns ctxt env tt

316285 return (PVTy tv, tt, [])

317286

src/Idris/Core/Unify.hs−88

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

3737 }

3838 deriving (Eq, Show)

3939

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

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

4241 Bool, -- ready to retry yet

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

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

5554data UInfo = UI Int Fails

5655 deriving Show

5756

58−data UResult a = UOK a

59− | UPartOK a

60− | UFail Err

61−

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

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

6459cantUnify [] 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 =

189184 | otherwise = checkScope ns (x, tm)

190185

191186 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))

196187 let v = highV (-1) tm in

197188 if v >= length ns

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

199190 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)

202191

203192 bind i ns tm

204193 | i < 0 = tm

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

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

256245 return $ n : ns'

257246

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−

272247unify :: Context -> Env ->

273248 (TT Name, Maybe Provenance) ->

274249 (TT Name, Maybe Provenance) ->

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

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

296271 Error e -> tfail e

297272 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−

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

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

304275-- injective (P Ref n _)

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

325296 sc i = do UI s f <- get

326297 put (UI (s+i) f)

327298

328− errors :: StateT UInfo TC Bool

329− errors = do UI s f <- get

330− return (not (null f))

331−

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

333300 r <- u1

334301 UI s f' <- get

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

340307 StateT UInfo

341308 TC [(Name, TT Name)]

342309 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))

349310

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

351312 StateT UInfo

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

575536 = unifyFail appx appy

576537 checkHeads _ _ = return []

577538

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

579−

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

581540 (metavar f &&

582541 all (\x -> metavarApp x) args

583542 && nub args == args) ||

584543 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

598544

599545 globmetavar t = case unApply t of

600546 (P _ x _, _) ->

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

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

609555 || globmetavar t

610556 _ -> 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

619557

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

621559 | Just ni <- lookupInjectiveExact n ctxt,

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

680618 | otherwise = checkScope ns (x, tm)

681619

682620 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))

687621 let v = highV (-1) tm in

688622 if v >= length ns

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

690624 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)

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

694626

695627 bind i ns tm

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

708640 sc 1

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

710642

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−

720643highV :: Int -> Term -> Int

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

722645 | otherwise = i

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

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

725648highV i _ = i

726649

727−envPos x i [] = 0

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

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

730−

731−

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

733651-- more work may help.

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

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

794712 Just (Hole _) -> True

795713 Just (Guess _ _) -> True

796714 _ -> 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)

281281 collectConsts (ConstCase c sc) = Just c

282282 collectConsts _ = Nothing

283283

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

285− hasDefault (DefaultCase _) = True

286− hasDefault _ = False

287−

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

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

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

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

333329 trimAlts cs nots vn (DefaultCase sc : rest)

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

335331

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

337− isConMatch _ _ = False

338−

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

340333 substMatch ca [] = []

341334 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

167167 setFC fc t = t

168168

169169unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

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

171− mkap (getFn e)

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

172171 where

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

174173 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

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

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

193193

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−

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

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

203196 | 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) =

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

354347 else empty

355348pprintErr' 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

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

358351 (delabSugared i (flagUnique y_ns)) in

359352 text "Type mismatch between" <>

src/Idris/Docs.hs−4

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

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

241241 updateRef _ pt = pt

242242

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−

247243 prettyConstraints =

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

249245

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

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

2727import Idris.Elab.Type

2828import Idris.Elab.Utils

2929import Idris.Error

30−import Idris.Inliner

3130import Idris.Options

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

3332import Idris.PartialEval

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

140139 -- optimisation applied to LHS

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

142141 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

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

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

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

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

160153 -- help with later inlinings.

161154

162155 ist <- getIState

163− let pdef_inl = inlineDef ist pdef

164−

165156 numArgs <- tclift $ sameLength pdef

166157

167158 case specNames opts of

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

184175 missing' <- checkPossibles info fc True n missing

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

186177 -- given cases (including impossible ones)

187− let clhs = map getLHS pdef

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

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

190180 "\nAgainst: " ++

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

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

233223 ctxt <- getContext

234224 ist <- getIState

235− let opt = idris_optimisation ist

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

237226 (idris_patdefs ist) })

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

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

302291 return ()

303292

304293 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−

314294 checkUndefined n ctxt = case lookupDef n ctxt of

315295 [] -> return ()

316296 [TyDecl _ _] -> return ()

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

358338

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

360340 = do l <- sameLength xs

361− let (f, as) = unApply x

341+ let (_, as) = unApply x

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

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

364344 sameLength [] = return 0

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

671651 "\n" ++ show ptm

672652 return (Left ptm, lhs)

673653elabClause 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

676655 ctxt <- getContext

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

678657

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

903882 pinfo info ns ds i

904883 = let newps = params info ++ ns

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

906− newb = addAlist dsParams (inblock info)

907− l = liftname info in

885+ newb = addAlist dsParams (inblock info) in

908886 info { params = newps,

909887 inblock = newb,

910888 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

953931 isOutsideWith _ = True

954932

955933elabClause 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

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

959936 -- pattern bindings

960937 i <- getIState

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

11761153 mkAux pn wname toplhs ns ns' c

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

11781155

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−

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

11831157 -- ns', arguments which do

11841158 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)

12021176 updateWithTerm ist pn wname toplhs ns_in ns_in' tm

12031177 = mapPT updateApp tm

12041178 where

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

1206− arity _ = 0

1207−

1208− lhs_arity = arity toplhs

1209−

12101179 currentFn fname (PAlternative _ _ as)

12111180 | Just tm <- getApp as = tm

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

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

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

4242

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

4444elabData 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))

4746 checkUndefined fc n

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

4948 (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)

7372 rt -> tclift $ tfail (At fc (Elaborating "type constructor " n Nothing (Msg "Not a valid type constructor")))

7473 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

7574 ttag <- getName

76− let as = map (const (Left (Msg ""))) (getArgTys cty)

7775

7876 ctxt <- getContext

7977 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)

151149 cinfo info ds

152150 = let newps = params info

153151 dsParams = map (\n -> (n, [])) ds

154− newb = addAlist dsParams (inblock info)

155− l = liftname info in

152+ newb = addAlist dsParams (inblock info) in

156153 info { params = newps,

157154 inblock = newb,

158155 liftname = id -- Is this appropriate?

@@ -226,12 +223,6 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

226223 getTyName (PRef _ _ n) = n == nsroot tn

227224 getTyName _ = False

228225

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−

235226 -- if the constructor is a UniqueType, the datatype must be too

236227 -- (AnyType is fine, since that is checked for uniqueness too)

237228 -- if hte contructor is AnyType, the datatype must be at least AnyType

@@ -339,7 +330,7 @@ elabCaseFun ind paramPos n ty cons info = do

339330 elimLog "Elaborating case function"

340331 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

341332 let (cnstrs, _) = splitPi ty

342− let (splittedTy@(pms, idxs)) = splitPms cnstrs

333+ let (pms, idxs) = splitPms cnstrs

343334 generalParams <- namePis False pms

344335 motiveIdxs <- namePis False idxs

345336 let motive = mkMotive n paramPos generalParams motiveIdxs

@@ -377,10 +368,6 @@ elabCaseFun ind paramPos n ty cons info = do

377368 elimDeclName :: Name

378369 elimDeclName = if ind then SN . ElimN $ n else SN . CaseN (FC' elimFC) $ n

379370

380− applyNS :: Name -> [String] -> Name

381− applyNS n [] = n

382− applyNS n ns = sNS n ns

383−

384371 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

385372 splitPi = splitPi' []

386373 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

@@ -421,10 +408,6 @@ elabCaseFun ind paramPos n ty cons info = do

421408 simpleName (MN i n) = str n ++ show i

422409 simpleName n = show n

423410

424− nameSpaces :: Name -> [String]

425− nameSpaces (NS _ ns) = map str ns

426− nameSpaces _ = []

427−

428411 freshName :: String -> EliminatorState Name

429412 freshName key = do

430413 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

5656 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

5757 cs -> tclift $ tfail $ At fc

5858 (CantResolveAlts (map fst cs))

59− let constraint = PApp fc (PRef fc [] n) (map pexp ps)

6059 let iname = mkiname n (namespace info) ps expn

6160 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

6261 ist <- getIState

@@ -144,7 +143,6 @@ elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pex

144143 let wbVals_orig = map (decorateid (decorate ns iname)) ds'

145144 ist <- getIState

146145 let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

147− let wb = wbTys ++ wbVals

148146

149147 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

150148 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

277275 mkMethApp ps (n, _, _, ty)

278276 = lamBind 0 ty (papp fc (PRef fc [] n)

279277 (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

280− where

281− needed is p = pname p `elem` map pname is

282278

283279 lamBind i (PPi (Constraint _ _ _) _ _ _ sc) sc'

284280 = 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

9494 ims <- mapM (tdecl impps mnames) mdecls

9595 defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint)

9696 (filter clause ds)

97− let (methods, imethods)

98− = unzip (map (\ (x, y, z) -> (x, y)) ims)

97+ let imethods = map (\ (x, y, z) -> y) ims

9998 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

10099

101100 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

367366 return (PTy doc [] syn fc o m mfc ty',

368367 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []])

369368

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−

377369 getMArgs (PPi (Imp _ _ _ _ _ _) n _ ty sc) = IA n : getMArgs sc

378370 getMArgs (PPi (Exp _ _ _ _) n _ ty sc) = EA n : getMArgs sc

379371 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

423415 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

424416 toExp ns e sc = sc

425417

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−

432418-- | Get the docstring corresponding to a member, if one exists

433419memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

434420memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

src/Idris/Elab/Record.hs−26

@@ -16,7 +16,6 @@ import Idris.Docstrings

1616import Idris.Elab.Data

1717import Idris.Error

1818import Idris.Output (sendHighlighting)

19−import Idris.Parser.Expr (tryFullExpr)

2019

2120import Control.Monad

2221import Data.List

@@ -212,15 +211,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

212211 isFieldOrParam' :: (Name, a) -> Bool

213212 isFieldOrParam' = isFieldOrParam . fst

214213

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−

224214 -- Delabs the TT to PTerm

225215 -- This is not good.

226216 -- 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

239229 freeName (NS n s) = NS (freeName n) s

240230 freeName n = n

241231

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−

249232 paramName :: Name -> Name

250233 paramName (UN n) = sUN ("param_" ++ str n)

251234 paramName (MN i n) = sMN i ("param_" ++ str n)

@@ -282,15 +265,6 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

282265 fieldDep :: Name -> PTerm -> (Name, [Name])

283266 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

284267

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−

294268 -- | A list of fields depended on by other fields.

295269 dependedOn :: [Name]

296270 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))

src/Idris/Elab/Term.hs+1−51

@@ -79,7 +79,6 @@ build :: IState

7979 -> ElabD ElabResult

8080build ist info emode opts fn tm

8181 = do elab ist info emode opts fn tm

82− let tmIn = tm

8382 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

8483 [TIPartial] -> True

8584 _ -> False

@@ -157,8 +156,7 @@ buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

157156 PTerm ->

158157 ElabD ElabResult

159158buildTC 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

162160 [TIPartial] -> True

163161 _ -> False

164162 -- set name supply to begin after highest index in tm

@@ -184,7 +182,6 @@ buildTC ist info emode opts fn ns tm

184182 if (log /= "")

185183 then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

186184 else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

187− where pattern = emode == ELHS || emode == EImpossible

188185

189186-- | return whether arguments of the given constructor name can be

190187-- matched on. If they're polymorphic, no, unless the type has beed

@@ -241,7 +238,6 @@ elab ist info emode opts fn tm

241238 = do let loglvl = opt_logLevel (idris_options ist)

242239 when (loglvl > 5) $ unifyLog True

243240 compute -- expand type synonyms, etc

244− let fc = maybe "(unknown)"

245241 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

246242 est <- getAux

247243 sequence_ (get_delayed_elab est)

@@ -277,14 +273,6 @@ elab ist info emode opts fn tm

277273 Placeholder -> (True, priority arg)

278274 tm -> (False, priority arg)

279275

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−

288276 mkPat = do hs <- get_holes

289277 tm <- get_term

290278 case hs of

@@ -350,18 +338,6 @@ elab ist info emode opts fn tm

350338 notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

351339 notDelay _ = True

352340

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−

365341 elab' :: ElabCtxt -- ^ (in an argument, guarded, in a type, in a quasiquote)

366342 -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

367343 -> PTerm -- ^ The term to elaborate

@@ -597,13 +573,6 @@ elab ist info emode opts fn tm

597573 (P _ n' _, _) -> n == n'

598574 _ -> False

599575

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−

607576 elab' ina _ (PPatvar fc n) | bindfree

608577 = do patvar n

609578 update_term liftPats

@@ -621,8 +590,6 @@ elab ist info emode opts fn tm

621590 = do ty <- goal

622591 testImplicitWarning fc n ty

623592 let ina = e_inarg ec

624− guarded = e_guarded ec

625− inty = e_intype ec

626593 ctxt <- get_context

627594 env <- get_env

628595

@@ -884,7 +851,6 @@ elab ist info emode opts fn tm

884851 _ -> do mapM_ setInjective (map getTm args)

885852 -- maybe more things are solvable now

886853 unifyProblems

887− let guarded = isConName f ctxt

888854-- trace ("args is " ++ show args) $ return ()

889855 ns <- apply (Var f) (map isph args)

890856-- trace ("ns is " ++ show ns) $ return ()

@@ -994,10 +960,6 @@ elab ist info emode opts fn tm

994960 getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as

995961 | otherwise = getDets (i + 1) ds as

996962

997− tacTm (PTactics _) = True

998− tacTm (PProof _) = True

999− tacTm _ = False

1000−

1001963 setInjective (PRef _ _ n) = setinj n

1002964 setInjective (PApp _ (PRef _ _ n) _) = setinj n

1003965 setInjective _ = return ()

@@ -1072,7 +1034,6 @@ elab ist info emode opts fn tm

10721034 matchProblems True

10731035 args <- get_env

10741036 envU <- mapM (getKind args) args

1075− let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

10761037

10771038 -- Drop the unique arguments used in the term already

10781039 -- and in the scrutinee (since it's

@@ -1150,12 +1111,6 @@ elab ist info emode opts fn tm

11501111 UType AllTypes -> return (n, True)

11511112 _ -> return (n, False)

11521113

1153− tcName tm | (P _ n _, _) <- unApply tm

1154− = case lookupCtxt n (idris_interfaces ist) of

1155− [_] -> True

1156− _ -> False

1157− tcName _ = False

1158−

11591114 isNotLift env n

11601115 = case lookupBinder n env of

11611116 Just ty ->

@@ -1164,10 +1119,6 @@ elab ist info emode opts fn tm

11641119 _ -> False

11651120 _ -> False

11661121

1167− usedIn ns (n, b)

1168− = n `elem` ns

1169− || any (\x -> x `elem` ns) (allTTNames (binderTy b))

1170−

11711122 elab' ina fc (PUnifyLog t) = do unifyLog True

11721123 elab' ina fc t

11731124 unifyLog False

@@ -2710,7 +2661,6 @@ processTacticDecls info steps =

27102661

27112662 RDatatypeDefnInstrs tyn tyconTy ctors ->

27122663 do let cn (n, _, _) = n

2713− cimpls (_, impls, _) = impls

27142664 cty (_, _, t) = t

27152665 addIBC (IBCDef tyn)

27162666 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

3838 sendHighlighting highlights

3939 updateIState $ \i -> i { idris_name = newGName }

4040 let lhs_tm = orderPats (getInferTerm lhs')

41− let lhs_ty = getInferType lhs'

4241 let newargs = pvars i lhs_tm

4342

4443 (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

169169 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) (PTyped (PRef fc [] n) ty')) -- (mergeTy ty' (delab i nty')))

170170

171171 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

177172 -- Productivity checking now via checking for guarded 'Delay'

178173 let opts' = opts -- if corec then (Coinductive : opts) else opts

179174 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

224219 _ -> return ()

225220 return usety

226221 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−

235222 ffiexport = sNS (sUN "FFI_Export") ["FFI_Export"]

236223

237224 err = txt "Err"

src/Idris/Elab/Utils.hs+1−2

@@ -118,7 +118,6 @@ elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()

118118elabCaseBlock info opts d@(PClauses f o n ps)

119119 = do addIBC (IBCDef n)

120120 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

121− let opts' = nub (o ++ opts)

122121 -- propagate totality assertion to the new definitions

123122 let opts' = filter propagatable opts

124123 setFlags n opts'

@@ -746,7 +745,7 @@ pruneByType _ _ t _ _ as = as

746745-- to it later - just returns 'var' for now. EB)

747746isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

748747isPlausible ist var env n ty

749− = let (hvar, interfaces) = collectConstraints [] [] ty in

748+ = let (hvar, _) = collectConstraints [] [] ty in

750749 case hvar of

751750 Nothing -> True

752751 Just rth -> var -- trace (show (rth, interfaces)) var

src/Idris/ElabDecls.hs−6

@@ -244,12 +244,6 @@ elabDecl' what info (PParams f ns ps)

244244 let nblock = pblock i

245245 mapM_ (elabDecl' what info) nblock

246246 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 }

253247 pblock i = map (expandParamsD False i id ns

254248 (concatMap tldeclared ps)) ps

255249

src/Idris/Erasure.hs−4

@@ -287,7 +287,6 @@ buildDepMap ci used externs ctx startNames

287287 -- mini-DSL for postulates

288288 (==>) ds rs = (S.fromList ds, M.fromList [(r, S.empty) | r <- rs])

289289 it n is = [(sUN n, Arg i) | i <- is]

290− mn n is = [(MN 0 $ pack n, Arg i) | i <- is]

291290

292291 -- believe_me is special because it does not use all its arguments

293292 specialPrims = S.fromList [sUN "prim__believe_me"]

@@ -624,9 +623,6 @@ buildDepMap ci used externs ctx startNames

624623 union :: Deps -> Deps -> Deps

625624 union = M.unionWith (M.unionWith S.union)

626625

627− unions :: [Deps] -> Deps

628− unions = M.unionsWith (M.unionWith S.union)

629−

630626 unionMap :: (a -> Deps) -> [a] -> Deps

631627 unionMap f = M.unionsWith (M.unionWith S.union) . map f

632628

src/Idris/ErrReverse.hs−11

@@ -12,7 +12,6 @@ module Idris.ErrReverse(errReverse) where

1212import Idris.AbsSyntax

1313import Idris.Core.Evaluate (unfold)

1414import Idris.Core.TT

15−import Util.Pretty

1615

1716import Data.List

1817

@@ -72,13 +71,3 @@ errReverse ist t = rewrite 5 (do_unfold t) -- (elideLambdas t)

7271 Just (fs ++ as)

7372 -- no matching Binds, for now...

7473 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

5151data IBCFile = IBCFile {

5252 ver :: Word16

5353 , sourcefile :: FilePath

54− , ibc_reachablenames :: ![Name]

5554 , ibc_imports :: ![(Bool, FilePath)]

5655 , ibc_importdirs :: ![FilePath]

5756 , ibc_sourcedirs :: ![FilePath]

@@ -108,7 +107,7 @@ deriving instance Binary IBCFile

108107!-}

109108

110109initIBC :: IBCFile

111−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

110+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

112111

113112hasValidIBCVersion :: FilePath -> Idris Bool

114113hasValidIBCVersion fp = do

@@ -1123,16 +1122,6 @@ instance Binary Accessibility where

11231122 3 -> return Hidden

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

11251124

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−

11361125instance Binary PReason where

11371126 put x

11381127 = case x of

src/Idris/IdeMode.hs−3

@@ -176,9 +176,6 @@ instance SExpable OutputAnnotation where

176176encodeName :: Name -> String

177177encodeName n = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ n

178178

179−decodeName :: String -> Name

180−decodeName = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

181−

182179encodeTerm :: [(Name, Bool)] -> Term -> String

183180encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

184181 (bnd, tm)

src/Idris/IdrisDoc.hs−7

@@ -248,13 +248,6 @@ getAccess ist n =

248248 [(_, acc)] -> acc

249249 _ -> Private

250250

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−

258251-- | Predicate saying whether a Name possibly may have docs defined

259252-- Without this, getDocs from Idris.Docs may fail a pattern match.

260253mayHaveDocs :: Name -- ^ The Name to test

src/Idris/Imports.hs+2−2

@@ -29,13 +29,13 @@ pkgIndex :: String -> FilePath

2929pkgIndex s = "00" ++ s ++ "-idx.ibc"

3030

3131srcPath :: FilePath -> FilePath

32−srcPath fp = let (n, ext) = splitExtension fp in

32+srcPath fp = let (_, ext) = splitExtension fp in

3333 case ext of

3434 ".idr" -> fp

3535 _ -> fp ++ ".idr"

3636

3737lsrcPath :: FilePath -> FilePath

38−lsrcPath fp = let (n, ext) = splitExtension fp in

38+lsrcPath fp = let (_, ext) = splitExtension fp in

3939 case ext of

4040 ".lidr" -> fp

4141 _ -> fp ++ ".lidr"

src/Idris/Interactive.hs+1−3

@@ -382,9 +382,7 @@ makeLemma fn updatefile l n

382382 StringAtom lem_app]]]

383383 in runIO . hPutStrLn h $ convSExp "return" good n

384384

385− where getIndent s = length (takeWhile isSpace s)

386−

387− appArgs skip 0 _ = ""

385+ where appArgs skip 0 _ = ""

388386 appArgs skip i (Bind n@(UN c) (Pi _ _ _ _) sc)

389387 | (thead c /= '_' && n `notElem` skip)

390388 = " " ++ show n ++ appArgs skip (i - 1) sc

src/Idris/Package.hs−2

@@ -333,11 +333,9 @@ auditPackage True ipkg = do

333333 getIdrisFiles :: FilePath -> IO [FilePath]

334334 getIdrisFiles dir = do

335335 contents <- getDirectoryContents dir

336− let contents' = filter (\fname -> fname /= "." && fname /= "..") contents

337336

338337 -- [ 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.

339338

340−

341339 files <- forM contents (findRest dir)

342340 return $ filter (isIdrisFile) (concat files)

343341

src/Idris/Parser.hs+1−14

@@ -794,7 +794,6 @@ mutual :: SyntaxInfo -> IdrisParser [PDecl]

794794mutual syn =

795795 do reservedHL "mutual"

796796 openBlock

797− let pvars = syn_params syn

798797 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

799798 closeBlock

800799 fc <- getFC

@@ -1145,7 +1144,6 @@ clause syn

11451144 Just t -> return t

11461145 Nothing -> fail "Invalid clause"

11471146 (do r <- rhs syn n

1148− let ctxt = tt_ctxt ist

11491147 let wsyn = syn { syn_namespace = [], syn_toplevel = False }

11501148 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

11511149 popIndent

@@ -1169,8 +1167,6 @@ clause syn

11691167 fc <- getFC

11701168 n_in <- fst <$> fnName; let n = expandNS syn n_in

11711169 r <- rhs syn n

1172− ist <- get

1173− let ctxt = tt_ctxt ist

11741170 let wsyn = syn { syn_namespace = [] }

11751171 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

11761172 popIndent

@@ -1227,8 +1223,6 @@ clause syn

12271223 wargs <- many (wExpr syn)

12281224 let capp = PApp fc (PRef nfc [nfc] n) args

12291225 (do r <- rhs syn n

1230− ist <- get

1231− let ctxt = tt_ctxt ist

12321226 let wsyn = syn { syn_namespace = [] }

12331227 (wheres, nmap) <- choice [do x <- whereBlock n wsyn

12341228 popIndent

@@ -1573,11 +1567,6 @@ parseImports fname input

15731567 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

15741568 return ((mdoc, mname, ps, mrk'), annots, i)

15751569

1576− imp m = ImportInfo False (toPath m)

1577− Nothing [] NoFC NoFC

1578− ns = Spl.splitOn "."

1579− toPath = foldl1' (</>) . ns

1580−

15811570 addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

15821571 addPath [] _ = []

15831572 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

@@ -1882,8 +1871,6 @@ loadSource lidr f toline

18821871

18831872{-| Adds names to hide list -}

18841873addHides :: 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)

18881875 where doHide (n, a) = do setAccessibility n a

18891876 addIBC (IBCAccess n a)

src/Idris/Parser/Data.hs−10

@@ -9,7 +9,6 @@ Maintainer : The Idris Community.

99module Idris.Parser.Data where

1010

1111import Idris.AbsSyntax

12−import Idris.Core.Evaluate

1312import Idris.Core.TT

1413import Idris.Docstrings

1514import Idris.Options

@@ -55,18 +54,9 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

5554 return $ PRecord doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc syn

5655 <?> "record type declaration"

5756 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−

6357 getName (Just (n, _), _, _, _) = Just n

6458 getName _ = Nothing

6559

66− toFreeze :: Maybe Accessibility -> Maybe Accessibility

67− toFreeze (Just Frozen) = Just Private

68− toFreeze x = x

69−

7060 recordBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe (Name, FC), Docstring (Either Err PTerm))

7161 recordBody syn tyn = do

7262 ist <- get

src/Idris/PartialEval.hs−4

@@ -258,10 +258,6 @@ mkNewPats ist d ns newname sname lhs rhs =

258258 mkRHSargs (_ : ns) as = mkRHSargs ns as

259259 mkRHSargs _ _ = []

260260

261− mkSubst :: (Term, Term) -> Maybe (Name, Term)

262− mkSubst (P _ n _, t) = Just (n, t)

263− mkSubst _ = Nothing

264−

265261-- | Creates a new declaration for a specialised function application.

266262-- Simple version at the moment: just create a version which is a direct

267263-- application of the function to be specialised.

src/Idris/Primitives.hs+1−38

@@ -17,7 +17,6 @@ import Data.Bits

1717import Data.Char

1818import Data.Function (on)

1919import Data.Int

20−import Data.Word

2120

2221data Prim = Prim { p_name :: Name,

2322 p_type :: Type,

@@ -31,10 +30,9 @@ ty :: [Const] -> Const -> Type

3130ty [] x = Constant x

3231ty (t:ts) x = Bind (sMN 0 "T") (Pi RigW Nothing (Constant t) (TType (UVar [] (-3)))) (ty ts x)

3332

34−total, partial, iopartial :: Totality

33+total, partial :: Totality

3534total = Total []

3635partial = Partial NotCovering

37−iopartial = Partial ExternalIO

3836

3937primitives :: [Prim]

4038primitives =

@@ -232,36 +230,6 @@ intConv ity =

232230 (1, LFloatInt ity) total

233231 ]

234232

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−

265233iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

266234iCmp ity op self impl irop totality

267235 = 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

292260 Just $ I i

293261bfBin _ _ = Nothing

294262

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−

300263bsBin :: (String -> String -> Bool) -> [Const] -> Maybe Const

301264bsBin op [Str x, Str y]

302265 = let i = (if op x y then 1 else 0) in

src/Idris/ProofSearch.hs+1−14

@@ -27,7 +27,6 @@ import Control.Monad

2727import Control.Monad.State.Strict

2828import Data.List

2929import qualified Data.Set as S

30−import Debug.Trace

3130

3231-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

3332

@@ -49,7 +48,6 @@ trivialHoles psnames ok elab ist

4948 tryAll ((x, _, b):xs)

5049 = do -- if type of x has any holes in it, move on

5150 hs <- get_holes

52− let badhs = hs -- filter (flip notElem holesOK) hs

5351 g <- goal

5452 -- anywhere but the top is okay for a hole, if holesOK set

5553 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

@@ -85,7 +83,6 @@ trivialTCs ok elab ist

8583 tryAll ((x, _, b):xs)

8684 = do -- if type of x has any holes in it, move on

8785 hs <- get_holes

88− let badhs = hs -- filter (flip notElem holesOK) hs

8986 g <- goal

9087 env <- get_env

9188 -- 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

230227 | (P _ fn _, args@(_:_)) <- unApply fa = fn `notElem` hs

231228 notHole _ _ = True

232229

233− inHS hs (P _ n _) = n `elem` hs

234− isHS _ _ = False

235−

236230 toUN t@(P nt (MN i n) ty)

237231 | ('_':xs) <- str n = t

238232 | otherwise = P nt (UN n) ty

@@ -441,12 +435,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

441435 isMeta ns (P _ n _) = n `elem` ns

442436 isMeta _ _ = False

443437

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−

450438 numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

451439

452440 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

484472 | otherwise

485473 = do lams <- introImps

486474 t <- goal

487− let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

488475-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

489476-- else do

490477 -- 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

502489-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

503490 mapM_ (\ (_,n) -> do focus n

504491 t' <- goal

505− let (tc', ttype) = unApply (getRetTy t')

492+ let (tc', _) = unApply (getRetTy t')

506493 let got = fst (unApply (getRetTy t))

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

508495 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

164164 iputGoal rendered

165165

166166 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

168168

169169 ppo = ppOptionIst ist

170170

@@ -500,7 +500,6 @@ checkType e prf t = do

500500 putIState ist { tt_ctxt = ctxt' }

501501 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

502502 let ppo = ppOptionIst ist

503− ty' = normaliseC ctxt [] ty

504503 infixes = idris_infixes ist

505504 action = case tm of

506505 TType _ ->

src/Idris/REPL.hs+2−17

@@ -402,7 +402,6 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

402402 | (n, (_, i, _, _, _)) <- idris_metavars ist

403403 , not (n `elem` primDefs)

404404 ]

405− let ppo = ppOptionIst ist

406405 -- splitMvs is a list of pairs of names and their split types

407406 let splitMvs = [ (n, (premises, concl, tm))

408407 | (n, i, ty) <- mvTys ist mvs

@@ -420,14 +419,11 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

420419 runIO . hPutStrLn h $

421420 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

422421 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−

426422 -- | Split a function type into a pair of premises, conclusion.

427423 -- Each maintains both the original and delaborated versions.

428424 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

429425 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

431427 ((n, t, delabTy' ist [] [] t False False True):hs,

432428 c, delabTy' ist [] [] c False False True)

433429 splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

@@ -1021,8 +1017,7 @@ process fn (Check t)

10211017 = do (tm, ty) <- elabREPL (recinfo (fileFC "toplevel")) ERHS t

10221018 ctxt <- getContext

10231019 ist <- getIState

1024− let ppo = ppOptionIst ist

1025− ty' = if opt_evaltypes (idris_options ist)

1020+ let ty' = if opt_evaltypes (idris_options ist)

10261021 then normaliseC ctxt [] ty

10271022 else ty

10281023 case tm of

@@ -1127,7 +1122,6 @@ process fn (DebugInfo n)

11271122 when (not (null imps)) $ iputStrLn (show imps)

11281123 let d = lookupDefAcc n False (tt_ctxt i)

11291124 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

1130− let cg = lookupCtxtName n (idris_callgraph i)

11311125 i <- getIState

11321126 let cg' = lookupCtxtName n (idris_callgraph i)

11331127 sc <- checkSizeChange n

@@ -1457,12 +1451,6 @@ process fn (TransformInfo n)

14571451 ts' = showTrans i ts in

14581452 ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

14591453

1460−-- iRenderOutput (pretty lhs)

1461−-- iputStrLn " ==> "

1462−-- iPrintTermWithType (pprintDelab i rhs)

1463−-- iputStrLn "---------------"

1464−-- showTrans i ts

1465−

14661454process fn (PPrint fmt width (PRef _ _ n))

14671455 = do outs <- pprintDef False n

14681456 iPrintResult =<< renderExternal fmt width (vsep outs)

@@ -1470,10 +1458,7 @@ process fn (PPrint fmt width (PRef _ _ n))

14701458

14711459process fn (PPrint fmt width t)

14721460 = do (tm, ty) <- elabVal (recinfo (fileFC "toplevel")) ERHS t

1473− ctxt <- getContext

14741461 ist <- getIState

1475− let ppo = ppOptionIst ist

1476− ty' = normaliseC ctxt [] ty

14771462 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

14781463

14791464

src/Idris/REPL/Parser.hs−2

@@ -178,8 +178,6 @@ namespaceArgCmd names command doc =

178178 (names, NamespaceArg, doc, namespaceArg command)

179179exprArgCmd names command doc =

180180 (names, ExprArg, doc, exprArg command)

181−metavarArgCmd names command doc =

182− (names, MetaVarArg, doc, fnNameArg command)

183181optArgCmd names command doc =

184182 (names, OptionArg, doc, optArg command)

185183proofArgCmd names command doc =

src/Idris/Termination.hs+2−9

@@ -142,9 +142,6 @@ checkPositive mut_ns (cn, ty')

142142calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality

143143calcTotality fc n pats

144144 = do i <- getIState

145− let opts = case lookupCtxt n (idris_flags i) of

146− [fs] -> fs

147− _ -> []

148145 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of

149146 (failure : _) -> return failure

150147 _ -> checkSizeChange n

@@ -301,7 +298,7 @@ buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]

301298buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

302299 scgPat (lhs, rhs) = let lhs' = delazy lhs

303300 rhs' = delazy rhs

304− (f, pargs) = unApply (dePat lhs') in

301+ (_, pargs) = unApply (dePat lhs') in

305302 findCalls [] Toplevel (dePat rhs') (patvars lhs')

306303 (zip pargs [0..])

307304

@@ -392,7 +389,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

392389 fccPat cases pvs pargs args g (lhs, rhs)

393390 = let lhs' = delazy lhs

394391 rhs' = delazy rhs

395− (f, pargs_case) = unApply (dePat lhs')

392+ (_, pargs_case) = unApply (dePat lhs')

396393 -- pargs is a pair of a term, and the argument position that

397394 -- term appears in. If any of the arguments to the case block

398395 -- are also on the lhs, we also want those patterns to appear

@@ -544,10 +541,6 @@ checkMP ist topfn i mp = if i > 0

544541 collapse paths

545542 else tryPath 0 [] mp 0

546543 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−

551544 mkBig (e, d) = (e, 10000)

552545

553546 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

src/Idris/TypeSearch.hs+2−6

@@ -13,8 +13,7 @@ module Idris.TypeSearch (

1313 , defaultScoreFunction

1414 ) where

1515

16−import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,

17− putIState)

16+import Idris.AbsSyntax (addUsingConstraints, getIState, implicit, putIState)

1817import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),

1918 Idris, InterfaceInfo, OutputMode(..), PTerm,

2019 defaultSyntax, eqTy, implicitAllowed,

@@ -58,7 +57,6 @@ searchByType pkgs pterm = do

5857 mapM_ loadPkgIndex pkgs

5958 pterm' <- addUsingConstraints syn emptyFC pterm

6059 pterm'' <- implicit toplevel syn name pterm'

61− let pterm''' = addImpl [] i pterm''

6260 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

6361 let names = searchUsing searchPred i ty

6462 let names' = take numLimit names

@@ -304,7 +302,7 @@ interfaceUnify interfaceInfo ctxt ty tyTry = do

304302

305303isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

306304isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

307− (clss, args) = unApply ty

305+ (clss, _) = unApply ty

308306 getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

309307 getInterfaceName _ = []

310308

@@ -358,8 +356,6 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

358356 usedns = map fst startingHoles

359357 startingHoles = argNames1 ++ argNames2

360358

361− startingTypes = [(retTy1, retTy2)]

362−

363359

364360 startQueueOfQueues :: Q.PQueue Score (info, Q.PQueue Score State)

365361 startQueueOfQueues = Q.fromList $ mapMaybe getStartQueues types