Add linear Lam

Get linearity status of 'Lam' from the function type - there's currently
no explicit syntax for it.

src/IRTS/Compiler.hs

@@ -473,7 +473,7 @@ irTerm top vs env (V i)
     | i >= 0 && i < length env = return $ LV (Glob (env!!i))
     | otherwise = ifail $ "bad de bruijn index: " ++ show i
 
-irTerm top vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
+irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) sc
   where
     n' = uniqueName n env
 

src/Idris/AbsSyntaxTree.hs

@@ -1624,7 +1624,7 @@ getInferTerm (App _ (App _ _ _) tm) = tm
 getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
 
 getInferType (Bind n b sc)  = Bind n (toTy b) $ getInferType sc
-  where toTy (Lam t)        = Pi RigW Nothing t (TType (UVar [] 0))
+  where toTy (Lam r t)      = Pi r Nothing t (TType (UVar [] 0))
         toTy (PVar _ t)     = PVTy t
         toTy b              = b
 getInferType (App _ (App _ _ ty) _) = ty

src/Idris/Apropos.hs

@@ -72,7 +72,7 @@ instance Apropos Def where
   isApropos str (CaseOp _ ty ty' _ _ _) = isApropos str ty
 
 instance Apropos (Binder (TT Name)) where
-  isApropos str (Lam ty)      = str == T.pack "\\" || isApropos str ty
+  isApropos str (Lam _ ty)    = str == T.pack "\\" || isApropos str ty
   isApropos str (Pi _ _ ty _) = str == T.pack "->" || isApropos str ty
   isApropos str (Let ty val)  = str == T.pack "let" || isApropos str ty || isApropos str val
   isApropos str (NLet ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

src/Idris/Core/Binary.hs

@@ -515,8 +515,9 @@ instance Binary ImplicitInfo where
 instance (Binary b) => Binary (Binder b) where
         put x
           = case x of
-                Lam x1 -> do putWord8 0
-                             put x1
+                Lam x1 x2 -> do putWord8 0
+                                put x1
+                                put x2
                 Pi x1 x2 x3 x4 -> do putWord8 1
                                      put x1
                                      put x2
@@ -546,7 +547,8 @@ instance (Binary b) => Binary (Binder b) where
           = do i <- getWord8
                case i of
                    0 -> do x1 <- get
-                           return (Lam x1)
+                           x2 <- get
+                           return (Lam x1 x2)
                    1 -> do x1 <- get
                            x2 <- get
                            x3 <- get

src/Idris/Core/CaseTree.hs

@@ -823,7 +823,7 @@ prune proj (Case up n alts) = case alts' of
 prune _ t = t
 
 stripLambdas :: CaseDef -> CaseDef
-stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)
+stripLambdas (CaseDef ns (STerm (Bind x (Lam _ _) sc)) tm)
     = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
 stripLambdas x = x
 

src/Idris/Core/Evaluate.hs

@@ -403,7 +403,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
             = reapply ntimes stk top env f (a : args)
     reapply ntimes stk top env v args = return v
 
-    apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
+    apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)
          = do a' <- sc a
               app <- apply ntimes stk top env a' as
               wknV 1 app
@@ -636,13 +636,13 @@ convEq ctxt holes topx topy = ceq [] topx topy where
         | x `elem` holes || y `elem` holes = return True
         | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
         | otherwise = sameDefs ps x y
-    ceq ps x (Bind n (Lam t) (App _ y (V 0)))
+    ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))
           = ceq ps x (substV (P Bound n t) y)
-    ceq ps (Bind n (Lam t) (App _ x (V 0))) y
+    ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y
           = ceq ps (substV (P Bound n t) x) y
-    ceq ps x (Bind n (Lam t) (App _ y (P Bound n' _)))
+    ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
         | n == n' = ceq ps x y
-    ceq ps (Bind n (Lam t) (App _ x (P Bound n' _))) y
+    ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
         | n == n' = ceq ps x y
 
     ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y

src/Idris/Core/Execute.hs

@@ -91,7 +91,7 @@ toTT (EBind n b body) = do n' <- newN n
                            body' <- body $ EP Bound n' EErased
                            b' <- fixBinder b
                            Bind n' b' <$> toTT body'
-    where fixBinder (Lam t)       = Lam     <$> toTT t
+    where fixBinder (Lam rig t)    = Lam rig  <$> toTT t
           fixBinder (Pi rig i t k) = Pi rig i <$> toTT t <*> toTT k
           fixBinder (Let t1 t2)   = Let     <$> toTT t1 <*> toTT t2
           fixBinder (NLet t1 t2)  = NLet    <$> toTT t1 <*> toTT t2

src/Idris/Core/ProofState.hs

@@ -657,12 +657,12 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
        (tyv, tyt) <- lift $ check ctxt env ty
 --        ns <- lift $ unify ctxt env tyv t'
        case t' of
-           Bind y (Pi _ _ s _) t -> let t' = updsubst y (P Bound n s) t in
-                                      do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
-                                         ps <- get
-                                         let (uh, uns) = unified ps
---                                          put (ps { unified = (uh, uns ++ ns) })
-                                         return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
+           Bind y (Pi rig _ s _) t -> let t' = updsubst y (P Bound n s) t in
+                                        do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
+                                           ps <- get
+                                           let (uh, uns) = unified ps
+--                                            put (ps { unified = (uh, uns ++ ns) })
+                                           return $ Bind n (Lam rig tyv) (Bind x (Hole t') (P Bound x t'))
            _ -> lift $ tfail $ CantIntroduce t'
 introTy ty n ctxt env _ = fail "Can't introduce here."
 
@@ -672,15 +672,15 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
                     x@(Bind y (Pi _ _ s _) _) -> x
                     _ -> normalise ctxt env t
        case t' of
-           Bind y (Pi _ _ s _) t ->
+           Bind y (Pi rig _ s _) t ->
                let n = case mn of
                       Just name -> name
                       Nothing -> y
                -- It's important that this be subst and not updsubst,
                -- because we want to substitute even in portions of
                -- terms that we know do not contain holes.
                    t' = subst y (P Bound n s) t
-               in return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
+               in return $ Bind n (Lam rig s) (Bind x (Hole t') (P Bound x t'))
            _ -> lift $ tfail $ CantIntroduce t'
 intro n ctxt env _ = fail "Can't introduce here."
 
@@ -725,7 +725,7 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
        let tmt' = normalise ctxt env tmt
        case unApply tmt' of
          (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
-            do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
+            do let p = Bind rname (Lam RigW lt) (mkP (P Bound rname lt) r l t)
                let newt = mkP l r l t
                let sc = forget $ (Bind x (Hole newt)
                                        (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
                          Var nm -> uniqueNameCtxt ctxt nm currentNames
                          _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
              let tmvar = P Bound tmnm tmt'
-             prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
+             prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam RigW tmt') (mkP tmvar tmv tmvar t)
              consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
              let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
                                                         (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
           makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
           replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
                                                                         let var = P Bound idnm idxt
-                                                                        return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
+                                                                        return $ Bind idnm (Lam RigW idxt) (mkP var idxv var t)) prop $ zip idnms idxs
 casetac tm induction ctxt env _ = fail $ "Can't do " ++ (if induction then "induction" else "case analysis") ++ " here"
 
 

src/Idris/Core/TT.hs

@@ -853,7 +853,8 @@ deriving instance Binary ImplicitInfo
 -- | All binding forms are represented in a uniform fashion. This type only represents
 -- the types of bindings (and their values, if any); the attached identifiers are part
 -- of the 'Bind' constructor for the 'TT' type.
-data Binder b = Lam   { binderTy  :: !b {-^ type annotation for bound variable-}}
+data Binder b = Lam   { binderCount :: RigCount,
+                        binderTy  :: !b {-^ type annotation for bound variable-}}
                 -- ^ A function binding
               | Pi    { binderCount :: RigCount,
                         binderImpl :: Maybe ImplicitInfo,
@@ -900,7 +901,7 @@ deriving instance Binary Binder
 !-}
 
 instance Sized a => Sized (Binder a) where
-  size (Lam ty) = 1 + size ty
+  size (Lam _ ty) = 1 + size ty
   size (Pi _ _ ty _) = 1 + size ty
   size (Let ty val) = 1 + size ty + size val
   size (NLet ty val) = 1 + size ty + size val
@@ -914,8 +915,8 @@ fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
 fmapMB f (Let t v)   = liftM2 Let (f t) (f v)
 fmapMB f (NLet t v)  = liftM2 NLet (f t) (f v)
 fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
-fmapMB f (Lam t)     = liftM Lam (f t)
-fmapMB f (Pi c i t k)  = liftM2 (Pi c i) (f t) (f k)
+fmapMB f (Lam c t)   = liftM (Lam c) (f t)
+fmapMB f (Pi c i t k) = liftM2 (Pi c i) (f t) (f k)
 fmapMB f (Hole t)    = liftM Hole (f t)
 fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)
 fmapMB f (PVar c t)    = liftM (PVar c) (f t)
@@ -1632,7 +1633,7 @@ prettyEnv env t = prettyEnv' env t False
     prettySe p env (UType u) debug = text (show u)
 
     -- Render a `Binder` and its name
-    prettySb env n (Lam t) = prettyB env "λ" "=>" n t
+    prettySb env n (Lam _ t) = prettyB env "λ" "=>" n t
     prettySb env n (Hole t) = prettyB env "?defer" "." n t
     prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t
     prettySb env n (Pi Rig0 _ t _) = prettyB env "(" ") ->" n t
@@ -1682,7 +1683,8 @@ showEnv' env t dbg = se 10 env t where
     se p env (TType i) = "Type " ++ show i
     se p env (UType u) = show u
 
-    sb env n (Lam t)  = showb env "\\ " " => " n t
+    sb env n (Lam Rig1 t)  = showb env "\\ 1 " " => " n t
+    sb env n (Lam _ t)  = showb env "\\ " " => " n t
     sb env n (Hole t) = showb env "? " ". " n t
     sb env n (GHole i ns t) = showb env "?defer " ". " n t
     sb env n (Pi Rig1 (Just _) t _)   = showb env "{" "} -o " n t
@@ -1795,7 +1797,7 @@ pprintTT bound tm = pp startPrec bound tm
                             text "Type"
     pp p bound (UType u) = text (show u)
 
-    ppb p bound n (Lam ty) sc =
+    ppb p bound n (Lam rig ty) sc =
       bracket p startPrec . group . align . hang 2 $
       text "λ" <+> bindingOf n False <+> text "." <> line <> sc
     ppb p bound n (Pi rig _ ty k) sc =
@@ -1884,8 +1886,8 @@ pprintRaw bound (RBind n b body) =
        , ppb b
        , pprintRaw (n:bound) body]
   where
-    ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $
-                   text "Lam" <$> pprintRaw bound ty
+    ppb (Lam _ ty) = enclose lparen rparen . group . align . hang 2 $
+                     text "Lam" <$> pprintRaw bound ty
     ppb (Pi _ _ ty k) = enclose lparen rparen . group . align . hang 2 $
                         vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]
     ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs

@@ -226,8 +226,8 @@ check' holes tcns ctxt env top
       where mkUniquePi kv (Bind n (Pi rig i s k) sc)
                     = let k' = smaller kv k in
                           Bind n (Pi rig i s k') (mkUniquePi k' sc)
-            mkUniquePi kv (Bind n (Lam t) sc)
-                    = Bind n (Lam (mkUniquePi kv t)) (mkUniquePi kv sc)
+            mkUniquePi kv (Bind n (Lam rig t) sc)
+                    = Bind n (Lam rig (mkUniquePi kv t)) (mkUniquePi kv sc)
             mkUniquePi kv (Bind n (Let t v) sc)
                     = Bind n (Let (mkUniquePi kv t) v) (mkUniquePi kv sc)
             mkUniquePi kv t = t
@@ -245,6 +245,7 @@ check' holes tcns ctxt env top
            discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)
     where getCount (Pi rig _ _ _) = rigMult rigc rig
           getCount (PVar rig _) = rigMult rigc rig
+          getCount (Lam rig _) = rigMult rigc rig
           getCount _ = rigMult rigc RigW
 
           checkUsageOK Rig0 _ = return ()
@@ -255,11 +256,11 @@ check' holes tcns ctxt env top
                        else lift $ tfail $ Msg $ "There are " ++ (show used) ++ 
                               " uses of linear name " ++ show n
 
-          checkBinder (Lam t)
+          checkBinder (Lam rig t)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                  let tv' = normalise ctxt env tv
                  convType tcns ctxt env tt
-                 return (Lam tv, tt, [])
+                 return (Lam rig tv, tt, [])
           checkBinder (Let t v)
             = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t
                  -- May have multiple uses, check at RigW.
@@ -310,8 +311,8 @@ check' holes tcns ctxt env top
                  convType tcns ctxt env tt
                  return (PVTy tv, tt, [])
 
-          discharge n (Lam t) bt scv sct ns
-            = return (Bind n (Lam t) scv, Bind n (Pi RigW Nothing t bt) sct, ns)
+          discharge n (Lam r t) bt scv sct ns
+            = return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)
           discharge n (Pi r i t k) bt scv sct ns
             = return (Bind n (Pi r i t k) scv, sct, ns)
           discharge n (Let t v) bt scv sct ns