a5033e7 · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+1−1

compare with master

unifiedsplit

@@ -473,7 +473,7 @@ irTerm top vs env (V i)

473 | i >= 0 && i < length env = return $ LV (Glob (env!!i))

474 | otherwise = ifail $ "bad de bruijn index: " ++ show i

475

476−irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc

476+irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc

477 where

478 n' = uniqueName n env

479

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1624,7 +1624,7 @@ getInferTerm (App _ (App _ _ _) tm) = tm

1624getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)

1625

1626getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc

1627− where toTy (Lam t) = Pi RigW Nothing t (TType (UVar [] 0))

1627+ where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))

1628 toTy (PVar _ t) = PVTy t

1629 toTy b = b

1630getInferType (App _ (App _ _ ty) _) = ty

src/Idris/Apropos.hs+1−1

@@ -72,7 +72,7 @@ instance Apropos Def where

72 isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty

73

74instance Apropos (Binder (TT Name)) where

75− isApropos str (Lam ty) = str == T.pack "\\" || isApropos str ty

75+ isApropos str (Lam _ ty) = str == T.pack "\\" || isApropos str ty

76 isApropos str (Pi _ _ ty _) = str == T.pack "->" || isApropos str ty

77 isApropos str (Let ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

78 isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

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

@@ -515,8 +515,9 @@ instance Binary ImplicitInfo where

515instance (Binary b) => Binary (Binder b) where

516 put x

517 = case x of

518− Lam x1 -> do putWord8 0

518+ Lam x1 x2 -> do putWord8 0

519− put x1

519+ put x1

520+ put x2

520 Pi x1 x2 x3 x4 -> do putWord8 1

521 Pi x1 x2 x3 x4 -> do putWord8 1

521 put x1

522 put x1

522 put x2

523 put x2

@@ -546,7 +547,8 @@ instance (Binary b) => Binary (Binder b) where

546 = do i <- getWord8

547 = do i <- getWord8

547 case i of

548 case i of

548 0 -> do x1 <- get

549 0 -> do x1 <- get

550+ x2 <- get

549− return (Lam x1)

551+ return (Lam x1 x2)

550 1 -> do x1 <- get

552 1 -> do x1 <- get

551 x2 <- get

553 x2 <- get

552 x3 <- get

554 x3 <- get

src/Idris/Core/CaseTree.hs+1−1

@@ -823,7 +823,7 @@ prune proj (Case up n alts) = case alts' of

823prune _ t = t

824

825stripLambdas :: CaseDef -> CaseDef

826−stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

826+stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)

827 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)

828stripLambdas x = x

829

src/Idris/Core/Evaluate.hs+5−5

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

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

404 reapply ntimes stk top env v args = return v

405

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

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

407 = do a' <- sc a

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

409 wknV 1 app

@@ -636,13 +636,13 @@ convEq ctxt holes topx topy = ceq [] topx topy where

636 | x `elem` holes || y `elem` holes = return True

637 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

638 | otherwise = sameDefs ps x y

639− ceq ps x (Bind n (Lam t) (App _ y (V 0)))

639+ ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))

640 = ceq ps x (substV (P Bound n t) y)

641− ceq ps (Bind n (Lam t) (App _ x (V 0))) y

641+ ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y

642 = ceq ps (substV (P Bound n t) x) y

643− ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))

643+ ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))

644 | n == n' = ceq ps x y

645− ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y

645+ ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y

646 | n == n' = ceq ps x y

647

648 ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y

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

@@ -91,7 +91,7 @@ toTT (EBind n b body) = do n' <- newN n

91 body' <- body $ EP Bound n' EErased

92 b' <- fixBinder b

93 Bind n' b' <$> toTT body'

94− where fixBinder (Lam t) = Lam <$> toTT t

94+ where fixBinder (Lam rig t) = Lam rig <$> toTT t

95 fixBinder (Pi rig i t k) = Pi rig i <$> toTT t <*> toTT k

96 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

97 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

src/Idris/Core/ProofState.hs+11−11

@@ -657,12 +657,12 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

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

658-- ns <- lift $ unify ctxt env tyv t'

659 case t' of

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

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

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

661+ do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)

662− ps <- get

662+ ps <- get

663− let (uh, uns) = unified ps

663+ let (uh, uns) = unified ps

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

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

665− return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))

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

666 _ -> lift $ tfail $ CantIntroduce t'

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

668

@@ -672,7 +672,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

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

673 _ -> normalise ctxt env t

674 case t' of

675− Bind y (Pi _ _ s _) t ->

675+ Bind y (Pi rig _ s _) t ->

676 let n = case mn of

677 Just name -> name

678 Nothing -> y

@@ -680,7 +680,7 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

680 -- because we want to substitute even in portions of

681 -- terms that we know do not contain holes.

682 t' = subst y (P Bound n s) t

683− in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

683+ in return $ Bind n (Lam rig s) (Bind x (Hole t') (P Bound x t'))

684 _ -> lift $ tfail $ CantIntroduce t'

685intro n ctxt env _ = fail "Can't introduce here."

686

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

725 let tmt' = normalise ctxt env tmt

726 case unApply tmt' of

727 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->

728− do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

728+ do let p = Bind rname (Lam RigW lt) (mkP (P Bound rname lt) r l t)

729 let newt = mkP l r l t

730 let sc = forget $ (Bind x (Hole newt)

731 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))

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

785 Var nm -> uniqueNameCtxt ctxt nm currentNames

786 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames

787 let tmvar = P Bound tmnm tmt'

788− prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

788+ prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam RigW tmt') (mkP tmvar tmv tmvar t)

789 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)

790 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

791 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

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

812 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []

813 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

814 let var = P Bound idnm idxt

815− return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

815+ return $ Bind idnm (Lam RigW idxt) (mkP var idxv var t)) prop $ zip idnms idxs

816casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"

817

818

src/Idris/Core/TT.hs+11−9

@@ -853,7 +853,8 @@ deriving instance Binary ImplicitInfo

853-- | All binding forms are represented in a uniform fashion. This type only represents

854-- the types of bindings (and their values, if any); the attached identifiers are part

855-- of the 'Bind' constructor for the 'TT' type.

856+data Binder b = Lam { binderCount :: RigCount,

856−data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}

857+ binderTy :: !b {-^ type annotation for bound variable-}}

857 -- ^ A function binding

858 -- ^ A function binding

858 | Pi { binderCount :: RigCount,

859 | Pi { binderCount :: RigCount,

859 binderImpl :: Maybe ImplicitInfo,

860 binderImpl :: Maybe ImplicitInfo,

@@ -900,7 +901,7 @@ deriving instance Binary Binder

900!-}

901!-}

901

902

902instance Sized a => Sized (Binder a) where

903instance Sized a => Sized (Binder a) where

903− size (Lam ty) = 1 + size ty

904+ size (Lam _ ty) = 1 + size ty

904 size (Pi _ _ ty _) = 1 + size ty

905 size (Pi _ _ ty _) = 1 + size ty

905 size (Let ty val) = 1 + size ty + size val

906 size (Let ty val) = 1 + size ty + size val

906 size (NLet ty val) = 1 + size ty + size val

907 size (NLet ty val) = 1 + size ty + size val

@@ -914,8 +915,8 @@ fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

914fmapMB f (Let t v) = liftM2 Let (f t) (f v)

915fmapMB f (Let t v) = liftM2 Let (f t) (f v)

915fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

916fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)

916fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

917fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)

917−fmapMB f (Lam t) = liftM Lam (f t)

918+fmapMB f (Lam c t) = liftM (Lam c) (f t)

918−fmapMB f (Pi c i t k) = liftM2 (Pi c i) (f t) (f k)

919+fmapMB f (Pi c i t k) = liftM2 (Pi c i) (f t) (f k)

919fmapMB f (Hole t) = liftM Hole (f t)

920fmapMB f (Hole t) = liftM Hole (f t)

920fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

921fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)

921fmapMB f (PVar c t) = liftM (PVar c) (f t)

922fmapMB f (PVar c t) = liftM (PVar c) (f t)

@@ -1632,7 +1633,7 @@ prettyEnv env t = prettyEnv' env t False

1632 prettySe p env (UType u) debug = text (show u)

1633 prettySe p env (UType u) debug = text (show u)

1633

1634

1634 -- Render a `Binder` and its name

1635 -- Render a `Binder` and its name

1635− prettySb env n (Lam t) = prettyB env "λ" "=>" n t

1636+ prettySb env n (Lam _ t) = prettyB env "λ" "=>" n t

1636 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1637 prettySb env n (Hole t) = prettyB env "?defer" "." n t

1637 prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

1638 prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t

1638 prettySb env n (Pi Rig0 _ t _) = prettyB env "(" ") ->" n t

1639 prettySb env n (Pi Rig0 _ t _) = prettyB env "(" ") ->" n t

@@ -1682,7 +1683,8 @@ showEnv' env t dbg = se 10 env t where

1682 se p env (TType i) = "Type " ++ show i

1683 se p env (TType i) = "Type " ++ show i

1683 se p env (UType u) = show u

1684 se p env (UType u) = show u

1684

1685

1686+ sb env n (Lam Rig1 t) = showb env "\\ 1 " " => " n t

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

1687+ sb env n (Lam _ t) = showb env "\\ " " => " n t

1686 sb env n (Hole t) = showb env "? " ". " n t

1688 sb env n (Hole t) = showb env "? " ". " n t

1687 sb env n (GHole i ns t) = showb env "?defer " ". " n t

1689 sb env n (GHole i ns t) = showb env "?defer " ". " n t

1688 sb env n (Pi Rig1 (Just _) t _) = showb env "{" "} -o " n t

1690 sb env n (Pi Rig1 (Just _) t _) = showb env "{" "} -o " n t

@@ -1795,7 +1797,7 @@ pprintTT bound tm = pp startPrec bound tm

1795 text "Type"

1797 text "Type"

1796 pp p bound (UType u) = text (show u)

1798 pp p bound (UType u) = text (show u)

1797

1799

1798− ppb p bound n (Lam ty) sc =

1800+ ppb p bound n (Lam rig ty) sc =

1799 bracket p startPrec . group . align . hang 2 $

1801 bracket p startPrec . group . align . hang 2 $

1800 text "λ" <+> bindingOf n False <+> text "." <> line <> sc

1802 text "λ" <+> bindingOf n False <+> text "." <> line <> sc

1801 ppb p bound n (Pi rig _ ty k) sc =

1803 ppb p bound n (Pi rig _ ty k) sc =

@@ -1884,8 +1886,8 @@ pprintRaw bound (RBind n b body) =

1884 , ppb b

1886 , ppb b

1885 , pprintRaw (n:bound) body]

1887 , pprintRaw (n:bound) body]

1886 where

1888 where

1887− ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $

1889+ ppb (Lam _ ty) = enclose lparen rparen . group . align . hang 2 $

1888− text "Lam" <$> pprintRaw bound ty

1890+ text "Lam" <$> pprintRaw bound ty

1889 ppb (Pi _ _ ty k) = enclose lparen rparen . group . align . hang 2 $

1891 ppb (Pi _ _ ty k) = enclose lparen rparen . group . align . hang 2 $

1890 vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]

1892 vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]

1891 ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

1893 ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs+7−6

@@ -226,8 +226,8 @@ check' holes tcns ctxt env top

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

227 = let k' = smaller kv k in

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

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

229+ mkUniquePi kv (Bind n (Lam rig t) sc)

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

230+ = Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)

231 mkUniquePi kv (Bind n (Let t v) sc)

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

233 mkUniquePi kv t = t

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

245 discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)

246 where getCount (Pi rig _ _ _) = rigMult rigc rig

247 getCount (PVar rig _) = rigMult rigc rig

248+ getCount (Lam rig _) = rigMult rigc rig

248 getCount _ = rigMult rigc RigW

249 getCount _ = rigMult rigc RigW

249

250

250 checkUsageOK Rig0 _ = return ()

251 checkUsageOK Rig0 _ = return ()

@@ -255,11 +256,11 @@ check' holes tcns ctxt env top

255 else lift $ tfail $ Msg $ "There are " ++ (show used) ++

256 else lift $ tfail $ Msg $ "There are " ++ (show used) ++

256 " uses of linear name " ++ show n

257 " uses of linear name " ++ show n

257

258

258− checkBinder (Lam t)

259+ checkBinder (Lam rig t)

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

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

260 let tv' = normalise ctxt env tv

261 let tv' = normalise ctxt env tv

261 convType tcns ctxt env tt

262 convType tcns ctxt env tt

262− return (Lam tv, tt, [])

263+ return (Lam rig tv, tt, [])

263 checkBinder (Let t v)

264 checkBinder (Let t v)

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

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

265 -- May have multiple uses, check at RigW.

266 -- May have multiple uses, check at RigW.

@@ -310,8 +311,8 @@ check' holes tcns ctxt env top

310 convType tcns ctxt env tt

311 convType tcns ctxt env tt

311 return (PVTy tv, tt, [])

312 return (PVTy tv, tt, [])

312

313

313− discharge n (Lam t) bt scv sct ns

314+ discharge n (Lam r t) bt scv sct ns

314− = return (Bind n (Lam t) scv, Bind n (Pi RigW Nothing t bt) sct, ns)

315+ = return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)

315 discharge n (Pi r i t k) bt scv sct ns

316 discharge n (Pi r i t k) bt scv sct ns

316 = return (Bind n (Pi r i t k) scv, sct, ns)

317 = return (Bind n (Pi r i t k) scv, sct, ns)

317 discharge n (Let t v) bt scv sct ns

318 discharge n (Let t v) bt scv sct ns

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

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

140 uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty

141 h2 <- un bnames vx vy

142 combine bnames h1 h2

143− uB bnames (Lam tx) (Lam ty) = un bnames tx ty

143+ uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty

144 uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty

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

146 let r = recoverable (normalise ctxt env (binderTy x))

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

204 bind i ns tm

205 | i < 0 = tm

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

207− App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

207+ App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))

208 (P Bound x ty)

209

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

@@ -451,9 +451,9 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

451 bindLams (a : as) tm = bindLam a (bindLams as tm)

452

453 bindLam (V i) tm = Bind (fstEnv (env !! i))

454− (Lam (binderTy (sndEnv (env !! i))))

454+ (Lam RigW (binderTy (sndEnv (env !! i))))

455 tm

456− bindLam (P _ n ty) tm = Bind n (Lam ty) tm

456+ bindLam (P _ n ty) tm = Bind n (Lam RigW ty) tm

457 bindLam _ tm = error "Can't happen [non rigid bindLam]"

458

459 substEnv [] tm = tm

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

462

463 -- remove any unnecessary lambdas (helps with interface

464 -- resolution later).

465− eta ks (Bind n (Lam ty) sc) = eta ((n, ty) : ks) sc

465+ eta ks (Bind n (Lam r ty) sc) = eta ((n, r, ty) : ks) sc

466 eta ks t = rebind ks t

467

468− rebind ((n, ty) : ks) (App _ f (P _ n' _))

468+ rebind ((n, r, ty) : ks) (App _ f (P _ n' _))

469 | n == n' = eta ks f

470− rebind ((n, ty) : ks) t = rebind ks (Bind n (Lam ty) t)

470+ rebind ((n, r, ty) : ks) t = rebind ks (Bind n (Lam r ty) t)

471 rebind _ t = t

472

473 un' env fn bnames appx@(App _ _ _) appy@(App _ _ _)

@@ -475,13 +475,13 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

475-- = uplus (unApp fn bnames appx appy)

476-- (unifyTmpFail appx appy) -- take the whole lot

477

478− un' env fn bnames x (Bind n (Lam t) (App _ y (P Bound n' _)))

478+ un' env fn bnames x (Bind n (Lam _ t) (App _ y (P Bound n' _)))

479 | n == n' = un' env False bnames x y

480− un' env fn bnames (Bind n (Lam t) (App _ x (P Bound n' _))) y

480+ un' env fn bnames (Bind n (Lam _ t) (App _ x (P Bound n' _))) y

481 | n == n' = un' env False bnames x y

482− un' env fn bnames x (Bind n (Lam t) (App _ y (V 0)))

482+ un' env fn bnames x (Bind n (Lam _ t) (App _ y (V 0)))

483 = un' env False bnames x y

484− un' env fn bnames (Bind n (Lam t) (App _ x (V 0))) y

484+ un' env fn bnames (Bind n (Lam _ t) (App _ x (V 0))) y

485 = un' env False bnames x y

486-- un' env fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

487-- = un' env False ((x,y):bnames) sx sy

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

494 un' env fn bnames (App _ f x) (Bind n (Pi r i t k) y)

495 | noOccurrence n y && injectiveApp f

496 = do ux <- un' env False bnames x y

497− uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

497+ uf <- un' env False bnames f (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))

498 (Bind n (Pi r i t k) (V 1)))

499 combine env bnames ux uf

500

501 un' env fn bnames (Bind n (Pi r i t k) y) (App _ f x)

502 | noOccurrence n y && injectiveApp f

503 = do ux <- un' env False bnames y x

504− uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam (TType (UVar [] 0)))

504+ uf <- un' env False bnames (Bind (sMN 0 "uv") (Lam RigW (TType (UVar [] 0)))

505 (Bind n (Pi r i t k) (V 1))) f

506 combine env bnames ux uf

507

@@ -510,7 +510,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

510 = do h1 <- uB env bnames bx by

511 h2 <- un' ((x, Rig0, bx) : env) False (((x,y),binderTy bx):bnames) sx sy

512 combine env bnames h1 h2

513− where sameBinder (Lam _) (Lam _) = True

513+ where sameBinder (Lam _ _) (Lam _ _) = True

514 sameBinder (Pi _ i _ _) (Pi _ i' _ _) = True

515 sameBinder _ _ = False -- never unify holes/guesses/etc

516 un' env fn bnames x y

@@ -642,7 +642,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

642 h2 <- un' env False bnames vx vy

643 sc 1

644 combine env bnames h1 h2

645− uB env bnames (Lam tx) (Lam ty) = do sc 1; un' env False bnames tx ty

645+ uB env bnames (Lam _ tx) (Lam _ ty) = do sc 1; un' env False bnames tx ty

646 uB env bnames (Pi _ _ tx _) (Pi _ _ ty _) = do sc 1; un' env False bnames tx ty

647 uB env bnames (Hole tx) (Hole ty) = un' env False bnames tx ty

648 uB env bnames (PVar _ tx) (PVar _ ty) = un' env False bnames tx ty

@@ -679,7 +679,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

679 bind i ns tm

680 | i < 0 = tm

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

682− App MaybeHoles (Bind y (Lam ty) (bind (i-1) ns tm))

682+ App MaybeHoles (Bind y (Lam RigW ty) (bind (i-1) ns tm))

683 (P Bound x ty)

684

685 combine env bnames as [] = return as

@@ -766,8 +766,8 @@ recoverable (Bind _ (Pi _ _ _ _) sc) f

766 | (Constant _) <- f = False

767 | TType _ <- f = False

768 | UType _ <- f = False

769−recoverable (Bind _ (Lam _) sc) f = recoverable sc f

769+recoverable (Bind _ (Lam _ _) sc) f = recoverable sc f

770−recoverable f (Bind _ (Lam _) sc) = recoverable f sc

770+recoverable f (Bind _ (Lam _ _) sc) = recoverable f sc

771recoverable x y = True

772

773errEnv :: [(a, r, Binder b)] -> [(a, b)]

src/Idris/Core/WHNF.hs+1−1

@@ -90,7 +90,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

90 | otherwise = WV i

91 eval wenv@(WEnv d env) stk (Bind n (Let t v) sc)

92 = eval (WEnv d ((v, wenv) : env)) stk sc

93− eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)

93+ eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _ _) sc)

94 = eval (WEnv d ((tm, tenv) : env)) stk sc

95 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed

96 =let n' = uniqueName n (map fstEnv genv) in

src/Idris/DataOpts.hs+1−1

@@ -103,7 +103,7 @@ applyDataOptRT n tag arity uniq args

103 satArgs n = map (\i -> sMN i "sat") [1..n]

104

105 bind [] tm = tm

106− bind (n:ns) tm = Bind n (Lam Erased) (pToV n (bind ns tm))

106+ bind (n:ns) tm = Bind n (Lam RigW Erased) (pToV n (bind ns tm))

107

108 -- Nat special cases

109 -- TODO: Would be nice if this was configurable in idris source!

src/Idris/Delaborate.hs+2−2

@@ -135,7 +135,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

135 = case lookup n (idris_metavars ist) of

136 Just (Just _, mi, _, _, _) -> mkMVApp n []

137 _ -> PRef un [] n

138− de env _ (Bind n (Lam ty) sc)

138+ de env _ (Bind n (Lam _ ty) sc)

139 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

140 de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

141 | toplevel_imp impl -- information in 'imps' repeated

@@ -188,7 +188,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

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

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

190 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

191− deFn env (P _ n _) [ty, Bind x (Lam _) r]

191+ deFn env (P _ n _) [ty, Bind x (Lam _ _) r]

192 | n == sigmaTy

193 = PDPair un [] IsType (PRef un [] x) (de env [] ty)

194 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

src/Idris/Elab/Clause.hs+1−1

@@ -528,7 +528,7 @@ elabPE info fc caller r =

528 [] -> False

529 _ -> True

530 concreteTm ist (Constant _) = True

531− concreteTm ist (Bind n (Lam _) sc) = True

531+ concreteTm ist (Bind n (Lam _ _) sc) = True

532 concreteTm ist (Bind n (Pi _ _ _ _) sc) = True

533 concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc

534 concreteTm ist _ = False

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

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

1242 _ -> False

1243 case quoted of

1244 Just q -> do ctxt <- get_context

1245− (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Rig0, Lam Erased) | uq <- unquoteNames] (forget q) q

1245+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Rig0, Lam Rig0 Erased) | uq <- unquoteNames] (forget q) q

1246 if pattern

1247 then if isRaw

1248 then reflectRawQuotePattern unquoteNames (forget q')

src/Idris/Elab/Utils.hs+3−3

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

530 k' <- getPats k

531 sc' <- getPats sc

532 return (Bind n (Pi rig i t' k') sc')

533− getPats (Bind n (Lam t) sc) = do t' <- getPats t

533+ getPats (Bind n (Lam r t) sc) = do t' <- getPats t

534− sc' <- getPats sc

534+ sc' <- getPats sc

535− return (Bind n (Lam t') sc')

535+ return (Bind n (Lam r t') sc')

536 getPats (Bind n (Hole t) sc) = do t' <- getPats t

537 sc' <- getPats sc

538 return (Bind n (Hole t') sc')

src/Idris/Erasure.hs+6−6

@@ -366,7 +366,7 @@ buildDepMap ci used externs ctx startNames

366 getDepsTerm vs bs cd (Bind n bdr body)

367 -- here we just push IM.empty on the de bruijn stack

368 -- the args will be marked as used at the usage site

369− | Lam ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

369+ | Lam _ ty <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

370 | Pi _ _ ty _ <- bdr = getDepsTerm vs ((n, const M.empty) : bs) cd body

371

372 -- let-bound variables can get partially evaluated

@@ -421,11 +421,11 @@ buildDepMap ci used externs ctx startNames

421 V i -> snd (bs !! i) cd `union` unconditionalDeps args

422

423 -- we interpret applied lambdas as lets in order to reuse code here

424− Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet app)

424+ Bind n (Lam _ ty) t -> getDepsTerm vs bs cd (lamToLet app)

425

426 -- and we interpret applied lets as lambdas

427− Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

427+ Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam RigW ty) t) t')

428− Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')

428+ Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam RigW ty) t) t')

429

430 Proj t i

431 -> error $ "cannot[0] analyse projection !" ++ show i ++ " of " ++ show t

@@ -504,7 +504,7 @@ buildDepMap ci used externs ctx startNames

504 (f, args) = unApply tm

505

506 lamToLet' :: [Term] -> Term -> Term

507− lamToLet' (v:vs) (Bind n (Lam ty) tm) = Bind n (Let ty v) $ lamToLet' vs tm

507+ lamToLet' (v:vs) (Bind n (Lam _ ty) tm) = Bind n (Let ty v) $ lamToLet' vs tm

508 lamToLet' [] tm = tm

509 lamToLet' vs tm = error $

510 "Erasure.hs:lamToLet': unexpected input: "

@@ -512,7 +512,7 @@ buildDepMap ci used externs ctx startNames

512

513 -- split "\x_i -> T(x_i)" into [x_i] and T

514 unfoldLams :: Term -> ([Name], Term)

515− unfoldLams (Bind n (Lam ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')

515+ unfoldLams (Bind n (Lam _ ty) t) = let (ns,t') = unfoldLams t in (n:ns, t')

516 unfoldLams t = ([], t)

517

518 union :: Deps -> Deps -> Deps

src/Idris/ErrReverse.hs+1−1

@@ -70,7 +70,7 @@ errReverse ist t = rewrite 5 t -- (elideLambdas t)

70 -- it as it won't be very enlightening.

71

72 elideLambdas (App s f a) = App s (elideLambdas f) (elideLambdas a)

73− elideLambdas (Bind n (Lam t) sc)

73+ elideLambdas (Bind n (Lam _ t) sc)

74 | size sc > 200 = P Ref (sUN "...") Erased

75 elideLambdas (Bind n b sc)

76 = Bind n (fmap elideLambdas b) (elideLambdas sc)

src/Idris/IBC.hs+1−1

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

47import System.FilePath

48

49ibcVersion :: Word16

50−ibcVersion = 157

50+ibcVersion = 158

51

52-- | When IBC is being loaded - we'll load different things (and omit

53-- different structures/definitions) depending on which phase we're in.

src/Idris/Reflection.hs+3−3

@@ -314,7 +314,7 @@ reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)

314

315reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

316reifyTTBinderApp reif f [t]

317− | f == reflm "Lam" = liftM Lam (reif t)

317+ | f == reflm "Lam" = liftM (Lam RigW) (reif t)

318reifyTTBinderApp reif f [t, k]

319 | f == reflm "Pi" = liftM2 (Pi RigW Nothing) (reif t) (reif k)

320reifyTTBinderApp reif f [x, y]

@@ -577,7 +577,7 @@ reflectRawQuotePattern unq (RConstant c) =

577 fill (reflectConstant c); solve

578

579reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> Raw -> [Name] -> Binder a -> ElabD ()

580−reflectBinderQuotePattern q ty unq (Lam t)

580+reflectBinderQuotePattern q ty unq (Lam _ t)

581 = do t' <- claimTy (sMN 0 "ty") ty; movelast t'

582 fill $ reflCall "Lam" [ty, Var t']

583 solve

@@ -749,7 +749,7 @@ reflectBinder :: Binder Term -> Raw

749reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

750

751reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

752−reflectBinderQuote q ty unq (Lam t)

752+reflectBinderQuote q ty unq (Lam _ t)

753 = reflCall "Lam" [Var ty, q unq t]

754reflectBinderQuote q ty unq (Pi _ _ t k)

755 = reflCall "Pi" [Var ty, q unq t, q unq k]