a5033e7 · Idris-dev · git.iko.soy

src/IRTS/Compiler.hs+1−1

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

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

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

475475

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

477477 where

478478 n' = uniqueName n env

479479

src/Idris/AbsSyntaxTree.hs+1−1

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

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

16251625

16261626getInferType (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))

16281628 toTy (PVar _ t) = PVTy t

16291629 toTy b = b

16301630getInferType (App _ (App _ _ ty) _) = ty

src/Idris/Apropos.hs+1−1

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

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

7373

7474instance 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

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

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

7878 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

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

516516 put x

517517 = case x of

518− Lam x1 -> do putWord8 0

519− put x1

518+ Lam x1 x2 -> do putWord8 0

519+ put x1

520+ put x2

520521 Pi x1 x2 x3 x4 -> do putWord8 1

521522 put x1

522523 put x2

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

546547 = do i <- getWord8

547548 case i of

548549 0 -> do x1 <- get

549− return (Lam x1)

550+ x2 <- get

551+ return (Lam x1 x2)

550552 1 -> do x1 <- get

551553 x2 <- get

552554 x3 <- get

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

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

823823prune _ t = t

824824

825825stripLambdas :: CaseDef -> CaseDef

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

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

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

828828stripLambdas x = x

829829

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

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

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

404404 reapply ntimes stk top env v args = return v

405405

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)

407407 = do a' <- sc a

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

409409 wknV 1 app

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

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

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

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

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

642642 = 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' _)))

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

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

647647

648648 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

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

9292 b' <- fixBinder b

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

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

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

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

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

9797 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' =

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

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

659659 case t' of

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

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

662− ps <- get

663− let (uh, uns) = unified ps

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

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

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)

662+ ps <- get

663+ let (uh, uns) = unified ps

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

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

666666 _ -> lift $ tfail $ CantIntroduce t'

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

668668

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

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

673673 _ -> normalise ctxt env t

674674 case t' of

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

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

676676 let n = case mn of

677677 Just name -> name

678678 Nothing -> y

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

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

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

682682 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'))

684684 _ -> lift $ tfail $ CantIntroduce t'

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

686686

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

725725 let tmt' = normalise ctxt env tmt

726726 case unApply tmt' of

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

729729 let newt = mkP l r l t

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

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

785785 Var nm -> uniqueNameCtxt ctxt nm currentNames

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

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

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

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

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

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

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

814814 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

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

817817

818818

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

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

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

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

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

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

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

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

857858 -- ^ A function binding

858859 | Pi { binderCount :: RigCount,

859860 binderImpl :: Maybe ImplicitInfo,

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

900901!-}

901902

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

16331634

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

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

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

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

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

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

16831684 se p env (UType u) = show u

16841685

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

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

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

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

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

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

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

17951797 text "Type"

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

17971799

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

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

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

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

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

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

18841886 , ppb b

18851887 , pprintRaw (n:bound) body]

18861888 where

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

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

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

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

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

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

18911893 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

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

227227 = let k' = smaller kv k in

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

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

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

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

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

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

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

233233 mkUniquePi kv t = t

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

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

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

247247 getCount (PVar rig _) = rigMult rigc rig

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

248249 getCount _ = rigMult rigc RigW

249250

250251 checkUsageOK Rig0 _ = return ()

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

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

256257 " uses of linear name " ++ show n

257258

258− checkBinder (Lam t)

259+ checkBinder (Lam rig t)

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

260261 let tv' = normalise ctxt env tv

261262 convType tcns ctxt env tt

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

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

263264 checkBinder (Let t v)

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

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

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

310311 convType tcns ctxt env tt

311312 return (PVTy tv, tt, [])

312313

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

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

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

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

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

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

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

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

141141 h2 <- un bnames vx vy

142142 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

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

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

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

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

204204 bind i ns tm

205205 | i < 0 = tm

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

208208 (P Bound x ty)

209209

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

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

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

452452

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

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

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

455455 tm

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

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

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

458458

459459 substEnv [] tm = tm

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

462462

463463 -- remove any unnecessary lambdas (helps with interface

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

466466 eta ks t = rebind ks t

467467

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

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

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

471471 rebind _ t = t

472472

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

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

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

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

477477

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

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

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

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

485485 = un' env False bnames x y

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

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

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

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

495495 | noOccurrence n y && injectiveApp f

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

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

499499 combine env bnames ux uf

500500

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

502502 | noOccurrence n y && injectiveApp f

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

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

506506 combine env bnames ux uf

507507

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

510510 = do h1 <- uB env bnames bx by

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

512512 combine env bnames h1 h2

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

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

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

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

516516 un' env fn bnames x y

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

642642 h2 <- un' env False bnames vx vy

643643 sc 1

644644 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

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

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

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

679679 bind i ns tm

680680 | i < 0 = tm

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

683683 (P Bound x ty)

684684

685685 combine env bnames as [] = return as

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

766766 | (Constant _) <- f = False

767767 | TType _ <- f = False

768768 | UType _ <- f = False

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

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

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

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

771771recoverable x y = True

772772

773773errEnv :: [(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

9090 | otherwise = WV i

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

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

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

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

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

src/Idris/DataOpts.hs+1−1

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

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

104104

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

107107

108108 -- Nat special cases

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

135135 = case lookup n (idris_metavars ist) of

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

137137 _ -> PRef un [] n

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

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

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

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

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

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

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

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

190190 | 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]

192192 | n == sigmaTy

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

194194 (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 =

528528 [] -> False

529529 _ -> True

530530 concreteTm ist (Constant _) = True

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

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

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

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

534534 concreteTm ist _ = False

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

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

12421242 _ -> False

12431243 case quoted of

12441244 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

12461246 if pattern

12471247 then if isRaw

12481248 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

530530 k' <- getPats k

531531 sc' <- getPats sc

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

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

534− sc' <- getPats sc

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

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

534+ sc' <- getPats sc

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

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

537537 sc' <- getPats sc

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

src/Idris/Erasure.hs+6−6

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

366366 getDepsTerm vs bs cd (Bind n bdr body)

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

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

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

371371

372372 -- let-bound variables can get partially evaluated

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

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

422422

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

425425

426426 -- 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')

428− Bind n (NLet 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 RigW ty) t) t')

429429

430430 Proj t i

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

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

504504 (f, args) = unApply tm

505505

506506 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

508508 lamToLet' [] tm = tm

509509 lamToLet' vs tm = error $

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

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

512512

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

514514 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')

516516 unfoldLams t = ([], t)

517517

518518 union :: Deps -> Deps -> Deps

src/Idris/ErrReverse.hs+1−1

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

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

7171

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

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

7575 elideLambdas (Bind n b sc)

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

src/Idris/IBC.hs+1−1

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

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 157

50+ibcVersion = 158

5151

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

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

314314

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

316316reifyTTBinderApp reif f [t]

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

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

318318reifyTTBinderApp reif f [t, k]

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

320320reifyTTBinderApp reif f [x, y]

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

577577 fill (reflectConstant c); solve

578578

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

580−reflectBinderQuotePattern q ty unq (Lam t)

580+reflectBinderQuotePattern q ty unq (Lam _ t)

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

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

583583 solve

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

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

750750

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

752−reflectBinderQuote q ty unq (Lam t)

752+reflectBinderQuote q ty unq (Lam _ t)

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

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

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