f7ea42c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1726 from jfdm/fix/lift-fixme-todo

Lifted FIXME and TODOs from Core.

commitf7ea42ceed88ba70889ff12b68157419312d61b7 authorEdwin Brady <edwin.brady@gmail.com> dateMon 24 Nov 2014, 11:17 (12 years ago) parentd8cfafd 18b1e12

8 files changed+132−117

compare with master

unifiedsplit

src/Idris/Core/CaseTree.hs+28−24 src/Idris/Core/Constraints.hs+3−2 src/Idris/Core/Evaluate.hs+15−12 src/Idris/Core/Execute.hs+2−1 src/Idris/Core/ProofState.hs+16−14 src/Idris/Core/TT.hs+8−8 src/Idris/Core/Typecheck.hs+20−18 src/Idris/Core/Unify.hs+40−38

src/Idris/Core/CaseTree.hs+28−24

@@ -41,7 +41,7 @@ deriving instance Binary SC'

4141deriving instance NFData SC'

4242!-}

4343

44−data CaseType = Updatable | Shared

44+data CaseType = Updatable | Shared

4545 deriving (Eq, Ord, Show)

4646

4747type SC = SC' Term

@@ -184,7 +184,7 @@ directUse fn@(App f a)

184184 fce == txt "Force"

185185 = directUse a -- forcing a value counts as a use

186186 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

187− | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

187+ | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

188188 | otherwise = nub $ directUse f ++ directUse a

189189directUse (Proj x i) = nub $ directUse x

190190directUse _ = []

@@ -258,13 +258,15 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

258258 ns = take numargs args

259259 (ns', ps') = order [(n, i `elem` inacc) | (i,n) <- zip [0..] ns] pats

260260 (tree, st) = runCaseBuilder erInfo

261− (match ns' ps' (defaultCase cover))

261+ (match ns' ps' (defaultCase cover))

262262 ([], numargs, [])

263263 t = CaseDef ns (prune proj (depatt ns' tree)) (fstT st) in

264− if proj then return (stripLambdas t)

264+ if proj then return (stripLambdas t)

265265 else return t

266266-- FIXME: This check is not quite right in some cases, and is breaking

267267-- perfectly valid code!

268+--

269+-- Issue #1717 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1717

268270-- if checkSameTypes (lstT st) tree

269271-- then return t

270272-- else Error (At fc (Msg "Typecase is not allowed"))

@@ -311,23 +313,25 @@ checkSameTypes _ _ = True

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

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

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

316+--

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

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

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

316320isType n t = False

317321

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

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

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

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

322−isConstType (Str _) StrType = True

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

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

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

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

327−isConstType (B8V _) (AType (ATInt _)) = True

328−isConstType (B16V _) (AType (ATInt _)) = True

329−isConstType (B32V _) (AType (ATInt _)) = True

330−isConstType (B64V _) (AType (ATInt _)) = True

322+isConstType (I _) (AType (ATInt ITNative)) = True

323+isConstType (BI _) (AType (ATInt ITBig)) = True

324+isConstType (Fl _) (AType ATFloat) = True

325+isConstType (Ch _) (AType (ATInt ITChar)) = True

326+isConstType (Str _) StrType = True

327+isConstType (B8 _) (AType (ATInt _)) = True

328+isConstType (B16 _) (AType (ATInt _)) = True

329+isConstType (B32 _) (AType (ATInt _)) = True

330+isConstType (B64 _) (AType (ATInt _)) = True

331+isConstType (B8V _) (AType (ATInt _)) = True

332+isConstType (B16V _) (AType (ATInt _)) = True

333+isConstType (B32V _) (AType (ATInt _)) = True

334+isConstType (B64V _) (AType (ATInt _)) = True

331335isConstType _ _ = False

332336

333337data Pat = PCon Bool Name Int [Pat]

@@ -430,10 +434,10 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

430434 -- constructor tags between families, and no constructor/constant

431435 -- clash, because otherwise we can't reliable make the

432436 -- case distinction on evaluation

433− (patnames_ord, patnames_rest)

437+ (patnames_ord, patnames_rest)

434438 = Data.List.partition (noClash . map snd) patnames

435439 -- note: sortBy . reverse is not nonsense because sortBy is stable

436− pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

440+ pats' = transpose (sortBy moreDistinct (reverse patnames_ord)

437441 ++ patnames_rest) in

438442 (getNOrder pats', zipWith rebuild pats' cs)

439443 where

@@ -523,7 +527,7 @@ caseGroups (v:vs) gs err = do g <- altGroups gs

523527 altGroups (ConGroup _ (CConst c) args : cs)

524528 = (:) <$> altConstGroup c args <*> altGroups cs

525529

526− altGroup n i args

530+ altGroup n i args

527531 = do inacc <- inaccessibleArgs n

528532 (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

529533 matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

@@ -556,7 +560,7 @@ argsToAlt inacc rs@((r, m) : rest) = do

556560 -- Create names for new variables arising from the given patterns.

557561 getNewVars :: [Pat] -> CaseBuilder [Name]

558562 getNewVars [] = return []

559− getNewVars ((PV n t) : ns) = do v <- getVar "e"

563+ getNewVars ((PV n t) : ns) = do v <- getVar "e"

560564 nsv <- getNewVars ns

561565

562566 -- Record the type of the variable.

@@ -666,6 +670,7 @@ depatt ns tm = dp [] tm

666670 applyMaps ms t = t

667671

668672-- FIXME: Do this for SucCase too

673+-- Issue #1719 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1719

669674prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

670675 -> SC -> SC

671676prune proj (Case up n alts) = case alts' of

@@ -689,9 +694,9 @@ prune proj (Case up n alts) = case alts' of

689694 -- with sc

690695 as@[ConCase cn i args sc]

691696 | proj -> let sc' = prune proj sc in

692− if any (isUsed sc') args

697+ if any (isUsed sc') args

693698 then Case up n [ConCase cn i args sc']

694− else sc'

699+ else sc'

695700

696701 [SucCase cn sc]

697702 | proj

@@ -795,4 +800,3 @@ mkForce = mkForceSC

795800 = DefaultCase (mkForceSC n arg rhs)

796801

797802 forceTm n arg t = subst n arg t

798−

src/Idris/Core/Constraints.hs+3−2

@@ -56,15 +56,16 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs

5656 = Error $ At fc UniverseError

5757 -- FIXME: Make informative

5858 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))

59+ -- Issue #1725 on the issue tracker.

60+ -- https://github.com/idris-lang/Idris-dev/issues/1725

5961 -- if we reach a cycle but we're at the same universe level, it's

6062 -- fine, because they must all be equal, so stop.

6163 | inc == 0 && cv `elem` map fst path

6264 = return ()

63− | otherwise

65+ | otherwise

6466 = case M.lookup cv r of

6567 Nothing -> return ()

6668 Just cs -> mapM_ (next r ((cv, fc):path) inc) cs

6769

6870 next r path inc (ULT l x, fc) = check fc r path (inc + 1) x

6971 next r path inc (ULE l x, fc) = check fc r path inc x

70−

src/Idris/Core/Evaluate.hs+15−12

@@ -8,7 +8,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

88 Context, initContext, ctxtAlist, uconstraints, next_tvar,

99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

11− lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

11+ lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

1212 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

1313 mapDefCtxt,

1414 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,

@@ -92,7 +92,7 @@ normaliseTrace tr ctxt env t

9292

9393-- Return a specialised name, and an updated list of reductions available,

9494-- so that the caller can tell how much specialisation was achieved.

95−specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

95+specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->

9696 (TT Name, [(Name, Int)])

9797specialise ctxt env limits t

9898 = let (tm, st) =

@@ -176,7 +176,7 @@ usable False n ns

176176

177177

178178fnCount :: Int -> Name -> Eval ()

179−fnCount inc n

179+fnCount inc n

180180 = do ES ls num b <- get

181181 case lookup n ls of

182182 Just i -> do put $ ES ((n, (i - inc)) :

@@ -255,7 +255,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

255255 ev ntimes stk top env (V i)

256256 | i < length env && i >= 0 = return $ snd (env !! i)

257257 | otherwise = return $ VV i

258− ev ntimes stk top env (Bind n (Let t v) sc)

258+ ev ntimes stk top env (Bind n (Let t v) sc)

259259 | not runtime || occurrences n sc < 2

260260 = do v' <- ev ntimes stk top env v --(finalise v)

261261 sc' <- ev ntimes stk top ((n, v') : env) sc

@@ -283,7 +283,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

283283 where vbind env t

284284 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

285285 -- block reduction immediately under codata (and not forced)

286− ev ntimes stk top env

286+ ev ntimes stk top env

287287 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)

288288 | dly == txt "Delay" && lco == txt "LazyCodata" && not simpl

289289 = do let (f, _) = unApply arg

@@ -311,7 +311,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

311311 t' <- ev ntimes stk top env t

312312-- tfull' <- reapply ntimes stk top env t' []

313313 return (doProj t' (getValArgs t'))

314− where doProj t' (VP (DCon _ _ _) _ _, args)

314+ where doProj t' (VP (DCon _ _ _) _ _, args)

315315 | i >= 0 && i < length args = args!!i

316316 doProj t' _ = VProj t' i

317317

@@ -338,7 +338,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

338338 _ -> case args of

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

340340 [] -> return f

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

341+ reapply ntimes stk top env (VApp f a) args

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

343343 reapply ntimes stk top env v args = return v

344344

@@ -356,7 +356,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

356356 do let val = lookupDefAcc n (spec || atRepl) ctxt

357357 case val of

358358 [(CaseOp ci _ _ _ _ cd, acc)]

359− | acc /= Frozen || sUN "assert_total" `elem` stk ->

359+ | acc /= Frozen || sUN "assert_total" `elem` stk ->

360360 -- unoptimised version

361361 let (ns, tree) = getCases cd in

362362 if blockSimplify ci n stk

@@ -402,7 +402,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

402402 t <- evTree ntimes stk top env (zip ns args') tree

403403 when spec $ case t of

404404 Nothing -> reinstate n -- Blocked, count n again

405− Just _ -> return ()

405+ Just _ -> return ()

406406-- (zipWith (\n , t) -> (n, t)) ns args') tree

407407 return (t, rest)

408408 | otherwise = return (Nothing, args)

@@ -416,7 +416,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

416416 (amap ++ env) etm

417417 return $ Just etm'

418418 evTree ntimes stk top env amap (ProjCase t alts)

419− = do t' <- ev ntimes stk top env t

419+ = do t' <- ev ntimes stk top env t

420420 doCase ntimes stk top env amap t' alts

421421 evTree ntimes stk top env amap (Case _ n alts)

422422 = case lookup n amap of

@@ -591,10 +591,10 @@ convEq ctxt holes topx topy = ceq [] topx topy where

591591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc

592592

593593 ceq ps (V x) (V y) = return (x == y)

594− ceq ps (V x) (P _ y _)

594+ ceq ps (V x) (P _ y _)

595595 | x >= 0 && length ps > x = return (fst (ps!!x) == y)

596596 | otherwise = return False

597− ceq ps (P _ x _) (V y)

597+ ceq ps (P _ x _) (V y)

598598 | y >= 0 && length ps > y = return (x == snd (ps!!y))

599599 | otherwise = return False

600600 ceq ps (Bind n xb xs) (Bind n' yb ys)

@@ -833,6 +833,9 @@ addDatatype (Data n tag ty unique cons) uctxt

833833 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

834834

835835-- FIXME: Too many arguments! Refactor all these Bools.

836+--

837+-- Issue #1724 on the issue tracker.

838+-- https://github.com/idris-lang/Idris-dev/issues/1724

836839addCasedef :: Name -> ErasureInfo -> CaseInfo ->

837840 Bool -> Bool -> Bool -> Bool ->

838841 [Type] -> -- argument types

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

@@ -525,7 +525,6 @@ call (FFun name argTypes retType) args =

525525 call' (Fun _ h) args FPtr = EPtr <$> (execIO $ callFFI h (retPtr retVoid) (prepArgs args))

526526 call' (Fun _ h) args FUnit = do _ <- execIO $ callFFI h retVoid (prepArgs args)

527527 return $ EP Ref unitCon EErased

528−-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

529528

530529

531530 prepArgs = map prepArg

@@ -536,6 +535,8 @@ call (FFun name argTypes retType) args =

536535 prepArg (EConstant (B64 i)) = argCLong (fromIntegral i)

537536 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

538537 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

538+ -- Issue #1720 on the issue tracker.

539+ -- https://github.com/idris-lang/Idris-dev/issues/1720

539540 prepArg (EConstant (Str s)) = argString s

540541 prepArg (EPtr p) = argPtr p

541542 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

src/Idris/Core/ProofState.hs+16−14

@@ -151,10 +151,10 @@ match_unify' ctxt env topx topy =

151151 let dont = dontunify ps

152152 let inj = injective ps

153153 traceWhen (unifylog ps)

154− ("Matching " ++ show (topx, topy) ++

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

155155 " in " ++ show env ++

156156 "\nHoles: " ++ show (holes ps)

157− ++ "\n"

157+ ++ "\n"

158158 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"

159159 ) $

160160 case match_unify ctxt env topx topy inj (holes ps) while of

@@ -170,7 +170,7 @@ match_unify' ctxt env topx topy =

170170 return []

171171-- traceWhen (unifylog ps)

172172-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++

173−-- "\nSolved: " ++ show u

173+-- "\nSolved: " ++ show u

174174-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)

175175-- -- ++ show (pterm ps)

176176-- ++ "\n----------") $

@@ -203,7 +203,7 @@ unify' ctxt env topx topy =

203203 "\nHoles: " ++ show (holes ps)

204204 ++ "\nInjective: " ++ show (injective ps)

205205 ++ "\n") $

206− lift $ unify ctxt env topx topy inj (holes ps)

206+ lift $ unify ctxt env topx topy inj (holes ps)

207207 (map fst (notunified ps)) while

208208 let notu = filter (\ (n, t) -> case t of

209209 P _ _ _ -> False

@@ -416,7 +416,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

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

417417

418418regret :: RunTactic

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

419+regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

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

421421 ps { holes = hs \\ [x] })

422422 return sc

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

495495 notunified = updateNotunified [(x,val)]

496496 (notunified ps),

497497 instances = instances ps \\ [x] })

498− let tm' = subst x val sc in

498+ let tm' = subst x val sc in

499499 return tm'

500500solve _ _ h@(Bind x t sc)

501501 = do ps <- get

@@ -504,7 +504,7 @@ solve _ _ h@(Bind x t sc)

504504 _ -> lift $ tfail (IncompleteTerm h)

505505 where findType x (Bind n (Let t v) sc)

506506 = findType x v `mplus` findType x sc

507− findType x (Bind n t sc)

507+ findType x (Bind n t sc)

508508 | P _ x' _ <- binderTy t, x == x' = Just n

509509 | otherwise = findType x sc

510510 findType x _ = Nothing

@@ -553,7 +553,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

553553forall n ty ctxt env _ = fail "Can't pi bind here"

554554

555555patvar :: Name -> RunTactic

556−patvar n ctxt env (Bind x (Hole t) sc) =

556+patvar n ctxt env (Bind x (Hole t) sc) =

557557 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

558558 holes ps \\ [x],

559559 solved = Just (x, P Bound n t),

@@ -590,7 +590,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

590590 [lt, l, r, p, tmv, xp]))

591591 (scv, sct) <- lift $ check ctxt env sc

592592 return scv

593− _ -> lift $ tfail (NotEquality tmv tmt')

593+ _ -> lift $ tfail (NotEquality tmv tmt')

594594 where rname = sMN 0 "replaced"

595595rewrite _ _ _ _ = fail "Can't rewrite here"

596596

@@ -769,7 +769,7 @@ updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns e

769769updateError [] err = err

770770updateError ns (At f e) = At f (updateError ns e)

771771updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)

772−updateError ns (ElaboratingArg f a env e)

772+updateError ns (ElaboratingArg f a env e)

773773 = ElaboratingArg f a env (updateError ns e)

774774updateError ns (CantUnify b l r e xs sc)

775775 = CantUnify b (updateSolvedTerm ns l) (updateSolvedTerm ns r) (updateError ns e) xs sc

@@ -777,7 +777,7 @@ updateError ns e = e

777777

778778solveInProblems x val [] = []

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

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

780+ = ((psubst x val l, psubst x val r,

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

782782

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

@@ -785,7 +785,7 @@ mergeNotunified env ns = mnu ns [] [] where

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

786786 mnu ((n, t):ns) ns_acc ps_acc

787787 | Just t' <- lookup n ns, t /= t'

788− = mnu ns ((n,t') : ns_acc)

788+ = mnu ns ((n,t') : ns_acc)

789789 ((t,t',env,CantUnify True t t' (Msg "") [] 0, [],Match) : ps_acc)

790790 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

791791

@@ -796,6 +796,8 @@ updateNotunified ns nu = up nu where

796796 ((n, t') : up nus)

797797

798798-- FIXME: Why not just pass the whole proof state?

799+-- Issue #1716 on the issue tracker.

800+-- https://github.com/idris-lang/Idris-dev/issues/1716

799801updateProblems :: Context -> [(Name, TT Name)] -> Fails -> [Name] -> [Name] -> [Name]

800802 -> ([(Name, TT Name)], Fails)

801803-- updateProblems ctxt [] ps inj holes = ([], ps)

@@ -806,7 +808,7 @@ updateProblems ctxt ns ps inj holes usupp = up ns ps where

806808 y' = updateSolvedTerm ns y

807809 err' = updateError ns err

808810 env' = updateEnv ns env in

809−-- trace ("Updating " ++ show (x',y')) $

811+-- trace ("Updating " ++ show (x',y')) $

810812 case unify ctxt env' x' y' inj holes usupp while of

811813 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

812814 up (ns ++ v) ps

@@ -867,7 +869,7 @@ processTactic (Reorder n) ps

867869 return (ps' { previous = Just ps, plog = "" }, plog ps')

868870processTactic (ComputeLet n) ps

869871 = return (ps { pterm = mkProofTerm $

870− computeLet (context ps) n

872+ computeLet (context ps) n

871873 (getProofTerm (pterm ps)) }, "")

872874processTactic UnifyProblems ps

873875 = let (ns', probs') = updateProblems (context ps) []

src/Idris/Core/TT.hs+8−8

@@ -486,7 +486,7 @@ intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

486486intTyName (ITChar) = "Char"

487487intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

488488

489−data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

489+data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723

490490 deriving (Show, Eq, Ord)

491491{-!

492492deriving instance NFData IntTy

@@ -792,7 +792,7 @@ instance TermSize (TT Name) where

792792 | otherwise = 1

793793 termsize n (V _) = 1

794794 -- for `Bind` terms, we can erroneously declare a term

795− -- "recursive => really big" if the name of the bound

795+ -- "recursive => really big" if the name of the bound

796796 -- variable is the same as the name we're using

797797 -- So generate a different name in that case.

798798 termsize n (Bind n' (Let t v) sc)

@@ -971,19 +971,19 @@ subst n v tm = fst $ subst' 0 tm

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

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

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

974− if ub || usc then (Bind x b' sc', True) else (t, False)

975− subst' i t@(App f a) = let (f', uf) = subst' i f

974+ if ub || usc then (Bind x b' sc', True) else (t, False)

975+ subst' i t@(App f a) = let (f', uf) = subst' i f

976976 (a', ua) = subst' i a in

977977 if uf || ua then (App f' a', True) else (t, False)

978978 subst' i t@(Proj x idx) = let (x', u) = subst' i x in

979979 if u then (Proj x' idx, u) else (t, False)

980980 subst' i t = (t, False)

981981

982− substB' i b@(Let t v) = let (t', ut) = subst' i t

982+ substB' i b@(Let t v) = let (t', ut) = subst' i t

983983 (v', uv) = subst' i v in

984984 if ut || uv then (Let t' v', True)

985985 else (b, False)

986− substB' i b@(Guess t v) = let (t', ut) = subst' i t

986+ substB' i b@(Guess t v) = let (t', ut) = subst' i t

987987 (v', uv) = subst' i v in

988988 if ut || uv then (Guess t' v', True)

989989 else (b, False)

@@ -1090,7 +1090,7 @@ unList tm = case unApply tm of

10901090-- Bruijn indices.

10911091forget :: TT Name -> Raw

10921092forget tm = forgetEnv [] tm

1093−

1093+

10941094forgetEnv :: [Name] -> TT Name -> Raw

10951095forgetEnv env (P _ n _) = Var n

10961096forgetEnv env (V i) = Var (env !! i)

@@ -1384,7 +1384,7 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

13841384 orderPats $ bindPats (reverse ps) tm'

13851385 where

13861386 bindPats [] tm = tm

1387− bindPats ((n, t):ps) tm

1387+ bindPats ((n, t):ps) tm

13881388 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)

13891389 | otherwise = bindPats ps tm

13901390

src/Idris/Core/Typecheck.hs+20−18

@@ -53,7 +53,7 @@ isType ctxt env tm = isType' (normalise ctxt env tm)

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

5454recheck = recheck_borrowing False []

5555

56−recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

56+recheck_borrowing :: Bool -> [Name] -> Context -> Env -> Raw -> Term ->

5757 TC (Term, Type, UCs)

5858recheck_borrowing uniq_check bs ctxt env tm orig

5959 = let v = next_tvar ctxt in

@@ -65,7 +65,7 @@ recheck_borrowing uniq_check bs ctxt env tm orig

6565 return (tm, ty, constraints)

6666

6767check :: Context -> Env -> Raw -> TC (Term, Type)

68−check ctxt env tm

68+check ctxt env tm

6969 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

7070

7171check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

@@ -93,12 +93,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

9393 ty@(Bind x (Pi s k) t) -> ty

9494 _ -> normalise ctxt env fty

9595 case fty' of

96− Bind x (Pi s k) t ->

96+ Bind x (Pi s k) t ->

9797 do convertsC ctxt env aty s

9898 let apty = simplify initContext env

9999 (Bind x (Let aty av) t)

100100 return (App fv av, apty)

101− t -> lift $ tfail $ NonFunctionType fv fty

101+ t -> lift $ tfail $ NonFunctionType fv fty

102102 chk u env RType

103103 | holes = return (TType (UVal 0), TType (UVal 0))

104104 | otherwise = do (v, cs) <- get

@@ -107,7 +107,9 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

107107 return (TType (UVar v), TType (UVar (v+1)))

108108 chk u env (RUType un)

109109 | holes = return (UType un, TType (UVal 0))

110− | otherwise = do -- TODO! (v, cs) <- get

110+ | otherwise = do -- TODO! Issue #1715 on the issue tracker.

111+ -- https://github.com/idris-lang/Idris-dev/issues/1715

112+ -- (v, cs) <- get

111113 -- let c = ULT (UVar v) (UVar (v+1))

112114 -- put (v+2, (c:cs))

113115 -- return (TType (UVar v), TType (UVar (v+1)))

@@ -135,7 +137,6 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

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

136138 (kv, kt) <- chk u env k

137139 (tv, tt) <- chk st ((n, Pi sv kv) : env) t

138−-- let tv = mkUniquePi kv tv_in

139140 (v, cs) <- get

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

141142 (TType su, TType tu) -> do

@@ -148,12 +149,12 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

148149 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149150 (pToV n tv), k')

150151

151− where mkUniquePi kv (Bind n (Pi s k) sc)

152+ where mkUniquePi kv (Bind n (Pi s k) sc)

152153 = let k' = smaller kv k in

153154 Bind n (Pi s k') (mkUniquePi k' sc)

154− mkUniquePi kv (Bind n (Lam t) sc)

155+ mkUniquePi kv (Bind n (Lam t) sc)

155156 = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)

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

157+ mkUniquePi kv (Bind n (Let t v) sc)

157158 = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)

158159 mkUniquePi kv t = t

159160

@@ -257,9 +258,9 @@ data UniqueUse = Never -- no more times

257258-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

258259-- in the scope more than once, this is an error.

259260checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

260−checkUnique borrowed ctxt env tm

261+checkUnique borrowed ctxt env tm

261262 = evalStateT (chkBinders env (explicitNames tm)) []

262− where

263+ where

263264 isVar (P _ _ _) = True

264265 isVar (V _) = True

265266 isVar _ = False

@@ -272,10 +273,10 @@ checkUnique borrowed ctxt env tm

272273 chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

273274 | isVar a && owner == txt "Ownership" &&

274275 (lend == txt "lend" || lend == txt "Read")

275− = do chkBinders env t -- Check the type normally

276+ = do chkBinders env t -- Check the type normally

276277 st <- get

277278 -- Remove the 'LendOnly' names from the unusable set

278− put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

279+ put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

279280 chkBinders env a

280281 put st -- Reset the old state after checking the argument

281282 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

@@ -288,14 +289,16 @@ checkUnique borrowed ctxt env tm

288289 chkBinders ((n, b) : env) t

289290 chkBinders env t = return ()

290291

291− chkBinderName :: Env -> Name -> Binder Term ->

292+ chkBinderName :: Env -> Name -> Binder Term ->

292293 StateT [(Name, (UniqueUse, Universe))] TC ()

293294 chkBinderName env n b

294295 = do let rawty = forgetEnv (map fst env) (binderTy b)

295296 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

297+ -- Issue #1714 on the issue tracker

298+ -- https://github.com/idris-lang/Idris-dev/issues/1714

296299 case kind of

297300 UType UniqueType -> do ns <- get

298− if n `elem` borrowed

301+ if n `elem` borrowed

299302 then put ((n, (LendOnly, NullType)) : ns)

300303 else put ((n, (Once, UniqueType)) : ns)

301304 UType NullType -> do ns <- get

@@ -304,13 +307,12 @@ checkUnique borrowed ctxt env tm

304307 put ((n, (Once, AllTypes)) : ns)

305308 _ -> return ()

306309

307− chkName n

310+ chkName n

308311 = do ns <- get

309312 case lookup n ns of

310313 Nothing -> return ()

311314 Just (Many, k) -> return ()

312315 Just (Never, k) -> lift $ tfail (UniqueError k n)

313316 Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

314− Just (Once, k) -> put ((n, (Never, k)) :

317+ Just (Once, k) -> put ((n, (Never, k)) :

315318 filter (\x -> fst x /= n) ns)

316−

src/Idris/Core/Unify.hs+40−38

@@ -32,7 +32,7 @@ type Injs = [(TT Name, TT Name, TT Name)]

3232type Fails = [(TT Name, TT Name, Env, Err, [FailContext], FailAt)]

3333

3434unrecoverable :: Fails -> Bool

35−unrecoverable = any bad

35+unrecoverable = any bad

3636 where bad (_,_,_, err, _, _) = unrec err

3737

3838 unrec (CantUnify r _ _ _ _ _) = not r

@@ -92,12 +92,12 @@ match_unify ctxt env topx topy inj holes from =

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

9393 holeIn env f || f `elem` holes

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

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

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

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

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

9898 holeIn env f || f `elem` holes

9999 = let n' = uniqueName fn (map fst env) in

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

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

101101

102102 un names tx@(P _ x _) tm

103103 | tx /= tm && holeIn env x || x `elem` holes

@@ -106,12 +106,12 @@ match_unify ctxt env topx topy inj holes from =

106106 | ty /= tm && holeIn env y || y `elem` holes

107107 = do sc 1; checkCycle names (y, tm)

108108 un bnames (V i) (P _ x _)

109− | length bnames > i,

110− fst (fst (bnames!!i)) == x ||

109+ | length bnames > i,

110+ fst (fst (bnames!!i)) == x ||

111111 snd (fst (bnames!!i)) == x = do sc 1; return []

112112 un bnames (P _ x _) (V i)

113113 | length bnames > i,

114− fst (fst (bnames!!i)) == x ||

114+ fst (fst (bnames!!i)) == x ||

115115 snd (fst (bnames!!i)) == x = do sc 1; return []

116116 un bnames (Bind x bx sx) (Bind y by sy) | notHole bx && notHole by

117117 = do h1 <- uB bnames bx by

@@ -124,7 +124,7 @@ match_unify ctxt env topx topy inj holes from =

124124 un names x y

125125 | OK True <- convEq' ctxt holes x y = do sc 1; return []

126126 | otherwise = do UI s f <- get

127− let r = recoverable (normalise ctxt env x)

127+ let r = recoverable (normalise ctxt env x)

128128 (normalise ctxt env y)

129129 let err = cantUnify from r

130130 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -139,7 +139,7 @@ match_unify ctxt env topx topy inj holes from =

139139 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

140140 uB bnames (Pi tx _) (Pi ty _) = un bnames tx ty

141141 uB bnames x y = do UI s f <- get

142− let r = recoverable (normalise ctxt env (binderTy x))

142+ let r = recoverable (normalise ctxt env (binderTy x))

143143 (normalise ctxt env (binderTy y))

144144 let err = cantUnify from r topx topy

145145 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

@@ -152,12 +152,13 @@ match_unify ctxt env topx topy inj holes from =

152152

153153 -- TODO: there's an annoying amount of repetition between this and the

154154 -- main unification function. Consider lifting it out.

155+ -- Issue #1721 on the issue tracker: https://github.com/idris-lang/Idris-dev/issues/1721

155156

156157 sc i = do UI s f <- get

157158 put (UI (s+i) f)

158159

159160 unifyFail x y = do UI s f <- get

160− let r = recoverable (normalise ctxt env x)

161+ let r = recoverable (normalise ctxt env x)

161162 (normalise ctxt env y)

162163 let err = cantUnify from r

163164 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -192,23 +193,23 @@ match_unify ctxt env topx topy inj holes from =

192193 where inst [] tm = tm

193194 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

194195

195− bind i ns tm

196+ bind i ns tm

196197 | i < 0 = tm

197198 | otherwise = let ((x,y),ty) = ns!!i in

198199 App (Bind y (Lam ty) (bind (i-1) ns tm))

199200 (P Bound x ty)

200−

201+

201202renameBinders env (x, t) = (x, renameBindersTm env t)

202203

203204renameBindersTm :: Env -> TT Name -> TT Name

204205renameBindersTm env tm = uniqueBinders (map fst env) tm

205206 where

206207 uniqueBinders env (Bind n b sc)

207− | n `elem` env

208+ | n `elem` env

208209 = let n' = uniqueName n env in

209210 explicitHole $ Bind n' (fmap (uniqueBinders env) b)

210211 (uniqueBinders (n':env) (rename n n' sc))

211− | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

212+ | otherwise = Bind n (fmap (uniqueBinders (n:env)) b)

212213 (uniqueBinders (n:env) sc)

213214 uniqueBinders env (App f a) = App (uniqueBinders env f) (uniqueBinders env a)

214215 uniqueBinders env t = t

@@ -218,7 +219,7 @@ renameBindersTm env tm = uniqueBinders (map fst env) tm

218219 rename n n' (App f a) = App (rename n n' f) (rename n n' a)

219220 rename n n' t = t

220221

221− explicitHole (Bind n (Hole ty) sc)

222+ explicitHole (Bind n (Hole ty) sc)

222223 = Bind n (Hole ty) (instantiate (P Bound n ty) sc)

223224 explicitHole t = t

224225

@@ -227,7 +228,7 @@ trimSolutions ns = followSols (dropPairs ns)

227228 dropPairs (n@(x, P _ x' _) : ns)

228229 | x == x' = dropPairs ns

229230 | otherwise

230− = n : dropPairs

231+ = n : dropPairs

231232 (filter (\t -> case t of

232233 (n, P _ n' _) -> not (n == x' && n' == x)

233234 _ -> True) ns)

@@ -253,14 +254,14 @@ hasv (App f a) = hasv f || hasv a

253254hasv (Bind x b sc) = hasv (binderTy b) || hasv sc

254255hasv _ = False

255256

256−unify :: Context -> Env -> TT Name -> TT Name ->

257+unify :: Context -> Env -> TT Name -> TT Name ->

257258 [Name] -> [Name] -> [Name] -> [FailContext] ->

258259 TC ([(Name, TT Name)], Fails)

259260unify ctxt env topx topy inj holes usersupp from =

260−-- traceWhen (hasv topx || hasv topy)

261+-- traceWhen (hasv topx || hasv topy)

261262-- ("Unifying " ++ show topx ++ "\nAND\n" ++ show topy ++ "\n") $

262263 -- don't bother if topx and topy are different at the head

263− case runStateT (un False [] (renameBindersTm env topx)

264+ case runStateT (un False [] (renameBindersTm env topx)

264265 (renameBindersTm env topy)) (UI 0 []) of

265266 OK (v, UI _ []) -> return (map (renameBinders env) (trimSolutions v),

266267 [])

@@ -271,7 +272,7 @@ unify ctxt env topx topy inj holes usersupp from =

271272 case runStateT (un False [] topxn topyn)

272273 (UI 0 []) of

273274 OK (v, UI _ fails) ->

274− return (map (renameBinders env) (trimSolutions v),

275+ return (map (renameBinders env) (trimSolutions v),

275276 reverse fails)

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

277278 Error e -> tfail e

@@ -287,8 +288,8 @@ unify ctxt env topx topy inj holes usersupp from =

287288 injective (App f a) = injective f -- && injective a

288289 injective _ = False

289290

290−-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

291− injectiveVar (P _ n _) = n `elem` inj

291+-- injectiveVar (P _ (MN _ _) _) = True -- TMP HACK

292+ injectiveVar (P _ n _) = n `elem` inj

292293 injectiveVar (App f a) = injectiveVar f -- && injective a

293294 injectiveVar _ = False

294295

@@ -364,7 +365,7 @@ unify ctxt env topx topy inj holes usersupp from =

364365 then unifyTmpFail xtm tm

365366 else do sc 1

366367 return x

367− | pureTerm tm, not (injective xtm) && injective tm

368+ | pureTerm tm, not (injective xtm) && injective tm

368369 = do checkCycle bnames (x, tm)

369370 unifyTmpFail xtm tm

370371 un' fn bnames tm ytm@(P _ y _)

@@ -378,16 +379,16 @@ unify ctxt env topx topy inj holes usersupp from =

378379 then unifyTmpFail tm ytm

379380 else do sc 1

380381 return x

381− | pureTerm tm, not (injective ytm) && injective tm

382+ | pureTerm tm, not (injective ytm) && injective tm

382383 = do checkCycle bnames (y, tm)

383384 unifyTmpFail tm ytm

384385 un' fn bnames (V i) (P _ x _)

385386 | length bnames > i,

386− fst ((map fst bnames)!!i) == x ||

387+ fst ((map fst bnames)!!i) == x ||

387388 snd ((map fst bnames)!!i) == x = do sc 1; return []

388389 un' fn bnames (P _ x _) (V i)

389390 | length bnames > i,

390− fst ((map fst bnames)!!i) == x ||

391+ fst ((map fst bnames)!!i) == x ||

391392 snd ((map fst bnames)!!i) == x = do sc 1; return []

392393

393394 un' fn names topx@(Bind n (Hole t) sc) y = unifyTmpFail topx y

@@ -417,17 +418,17 @@ unify ctxt env topx topy inj holes usersupp from =

417418 un' fn bnames (App f x) (Bind n (Pi t k) y)

418419 | noOccurrence n y && injectiveApp f

419420 = do ux <- un' False bnames x y

420− uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

421+ uf <- un' False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

421422 (Bind n (Pi t k) (V 1)))

422423 combine bnames ux uf

423−

424+

424425 un' fn bnames (Bind n (Pi t k) y) (App f x)

425426 | noOccurrence n y && injectiveApp f

426427 = do ux <- un' False bnames y x

427− uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

428+ uf <- un' False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar 0)))

428429 (Bind n (Pi t k) (V 1))) f

429430 combine bnames ux uf

430−

431+

431432 un' fn bnames (Bind x bx sx) (Bind y by sy)

432433 | sameBinder bx by

433434 = do h1 <- uB bnames bx by

@@ -438,9 +439,9 @@ unify ctxt env topx topy inj holes usersupp from =

438439 sameBinder _ _ = False

439440 un' fn bnames x y

440441 | OK True <- convEq' ctxt holes x y = do sc 1; return []

441− | isUniverse x && isUniverse y = do sc 1; return []

442+ | isUniverse x && isUniverse y = do sc 1; return []

442443 | otherwise = do UI s f <- get

443− let r = recoverable (normalise ctxt env x)

444+ let r = recoverable (normalise ctxt env x)

444445 (normalise ctxt env y)

445446 let err = cantUnify from r

446447 topx topy (CantUnify r x y (Msg "") (errEnv env) s) (errEnv env) s

@@ -519,7 +520,7 @@ unify ctxt env topx topy inj holes usersupp from =

519520 _ -> False

520521

521522 metavar t = case t of

522− P _ x _ -> (x `notElem` usersupp &&

523+ P _ x _ -> (x `notElem` usersupp &&

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

524525 || globmetavar t

525526 _ -> False

@@ -566,7 +567,7 @@ unify ctxt env topx topy inj holes usersupp from =

566567 uB bnames (Hole tx) (Hole ty) = un' False bnames tx ty

567568 uB bnames (PVar tx) (PVar ty) = un' False bnames tx ty

568569 uB bnames x y = do UI s f <- get

569− let r = recoverable (normalise ctxt env (binderTy x))

570+ let r = recoverable (normalise ctxt env (binderTy x))

570571 (normalise ctxt env (binderTy y))

571572 let err = cantUnify from r topx topy

572573 (CantUnify r (binderTy x) (binderTy y) (Msg "") (errEnv env) s)

@@ -590,9 +591,9 @@ unify ctxt env topx topy inj holes usersupp from =

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

591592 where inst [] tm = tm

592593 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

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

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

594595

595− bind i ns tm

596+ bind i ns tm

596597 | i < 0 = tm

597598 | otherwise = let ((x,y),ty) = ns!!i in

598599 App (Bind y (Lam ty) (bind (i-1) ns tm))

@@ -639,7 +640,9 @@ envPos x i ((y, _) : ys) | x == y = i

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

640641-- rethink overloading properly...

641642-- ASSUMPTION: inputs are in normal form

642−

643+--

644+-- Issue #1722 on the issue tracker https://github.com/idris-lang/Idris-dev/issues/1722

645+--

643646recoverable t@(App _ _) _

644647 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

645648recoverable _ t@(App _ _)

@@ -658,7 +661,7 @@ recoverable (App f a) p@(Constant _) = recoverable f p

658661recoverable p@(P _ n _) (App f a) = recoverable p f

659662recoverable (App f a) p@(P _ _ _) = recoverable f p

660663recoverable (App f a) (App f' a')

661− | f == f' = recoverable a a'

664+ | f == f' = recoverable a a'

662665recoverable (App f a) (App f' a')

663666 = recoverable f f' -- && recoverable a a'

664667recoverable f (Bind _ (Pi _ _) sc)

@@ -685,4 +688,3 @@ patIn env n = case lookup n env of

685688 Just (PVar _) -> True

686689 Just (PVTy _) -> True

687690 _ -> False

688−