4a3fe0c · Idris-dev · git.iko.soy

CHANGELOG.md+3−1

@@ -5,7 +5,9 @@

55+ In `@`-patterns such as `x@p`, `x` is now in scope on the right-hand side

66 of any definitions in `where` clauses, provided the left-hand side of the

77 definition does not shadow it.

8−

8++ The `LinearTypes` language extension has been revised. It implements the

9+ rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative

10+ Type Theory" and now works with holes and case expressions.

911

1012## Library Updates

1113

libs/prelude/Builtins.idr+2−1

@@ -3,6 +3,7 @@

33%access public export

44%default total

55%language UniquenessTypes

6+%language LinearTypes

67

78||| The canonical single-element type, also known as the trivially

89||| true proposition.

@@ -18,7 +19,7 @@ namespace Builtins

1819 ||| A pair of elements

1920 ||| @a the left element of the pair

2021 ||| @b the right element of the pair

21− MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B

22+ MkPair : {A, B : Type} -> (1 a : A) -> (1 b : B) -> Pair A B

2223

2324 -- Usage hints for erasure analysis

2425 %used MkPair a

src/IRTS/Compiler.hs+1−1

@@ -478,7 +478,7 @@ irTerm top vs env (Bind n (Lam _ _) sc) = LLam [n'] <$> irTerm top vs (n':env) s

478478 where

479479 n' = uniqueName n env

480480

481−irTerm top vs env (Bind n (Let _ v) sc)

481+irTerm top vs env (Bind n (Let _ _ v) sc)

482482 = LLet n <$> irTerm top vs env v <*> irTerm top vs (n : env) sc

483483

484484irTerm top vs env (Bind _ _ _) = return $ LNothing

src/IRTS/Portable.hs+1−1

@@ -320,7 +320,7 @@ instance (ToJSON t) => ToJSON (AppStatus t) where

320320instance (ToJSON t) => ToJSON (Binder t) where

321321 toJSON (Lam rc bty) = object ["Lam" .= (rc, bty)]

322322 toJSON (Pi c i t k) = object ["Pi" .= (c, i, t, k)]

323− toJSON (Let t v) = object ["Let" .= (t, v)]

323+ toJSON (Let rc t v) = object ["Let" .= (t, v)]

324324 toJSON (NLet t v) = object ["NLet" .= (t, v)]

325325 toJSON (Hole t) = object ["Hole" .= (t)]

326326 toJSON (GHole l ns t) = object ["GHole" .= (l, ns, t)]

src/Idris/AbsSyntax.hs+22−15

@@ -143,6 +143,12 @@ addLangExt e = do i <- getIState

143143 idris_language_extensions = e : idris_language_extensions i

144144 }

145145

146+dropLangExt :: LanguageExt -> Idris ()

147+dropLangExt e = do i <- getIState

148+ putIState $ i {

149+ idris_language_extensions = idris_language_extensions i \\ [e]

150+ }

151+

146152-- | Transforms are organised by the function being applied on the lhs

147153-- of the transform, to make looking up appropriate transforms quicker

148154addTrans :: Name -> (Term, Term) -> Idris ()

@@ -1284,11 +1290,11 @@ expandParams dec ps ns infs tm = en 0 tm

12841290 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

12851291 PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))

12861292 | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)

1287− en 0 (PLet fc n nfc ty v s)

1293+ en 0 (PLet fc rc n nfc ty v s)

12881294 | n `elem` (map fst ps ++ ns)

12891295 = let n' = mkShadow n in

1290− PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))

1291− | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)

1296+ PLet fc rc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))

1297+ | otherwise = PLet fc rc n nfc (en 0 ty) (en 0 v) (en 0 s)

12921298 -- FIXME: Should only do this in a type signature!

12931299 en 0 (PDPair f hls p (PRef f' fcs n) t r)

12941300 | n `elem` (map fst ps ++ ns) && t /= Placeholder

@@ -1929,13 +1935,13 @@ addImpl' inpat env infns imp_meths ist ptm

19291935 else let ty' = ai inpat qq env ds ty

19301936 sc' = ai inpat qq ((n, Just ty):env) ds sc in

19311937 PLam fc n nfc ty' sc'

1932− ai inpat qq env ds (PLet fc n nfc ty val sc)

1938+ ai inpat qq env ds (PLet fc rc n nfc ty val sc)

19331939 = if canBeDConName n (tt_ctxt ist)

19341940 then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])

19351941 else let ty' = ai inpat qq env ds ty

19361942 val' = ai inpat qq env ds val

19371943 sc' = ai inpat qq ((n, Just ty):env) ds sc in

1938− PLet fc n nfc ty' val' sc'

1944+ PLet fc rc n nfc ty' val' sc'

19391945 ai inpat qq env ds (PPi p n nfc ty sc)

19401946 = let ty' = ai inpat qq env ds ty

19411947 env' = if n `elem` imp_meths then env

@@ -2345,10 +2351,11 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

23452351 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'

23462352 ms <- match' s s'

23472353 return (mt ++ ms)

2348− match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'

2349− mty <- match' ty ty'

2350− ms <- match' s s'

2351− return (mt ++ mty ++ ms)

2354+ match (PLet _ _ _ _ t ty s) (PLet _ _ _ _ t' ty' s')

2355+ = do mt <- match' t t'

2356+ mty <- match' ty ty'

2357+ ms <- match' s s'

2358+ return (mt ++ mty ++ ms)

23522359 match (PHidden x) (PHidden y)

23532360 | RightOK xs <- match x y = return xs -- to collect variables

23542361 | otherwise = return [] -- Otherwise hidden things are unmatchable

@@ -2401,8 +2408,8 @@ substMatchesShadow nmap shs t = sm shs t where

24012408 PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))

24022409 (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))

24032410 | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)

2404− sm xs (PLet fc x xfc val t sc)

2405− = PLet fc x xfc (sm xs val) (sm xs t) (sm xs sc)

2411+ sm xs (PLet fc rc x xfc val t sc)

2412+ = PLet fc rc x xfc (sm xs val) (sm xs t) (sm xs sc)

24062413 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

24072414 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

24082415 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

@@ -2429,8 +2436,8 @@ shadow n n' t = sm 0 t where

24292436 | otherwise = PLam fc x xfc (sm 0 t) sc

24302437 sm 0 (PPi p x fc t sc) | n /= x = PPi p x fc (sm 0 t) (sm 0 sc)

24312438 | otherwise = PPi p x fc (sm 0 t) sc

2432− sm 0 (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)

2433− | otherwise = PLet fc x xfc (sm 0 t) (sm 0 v) sc

2439+ sm 0 (PLet fc rc x xfc t v sc) | n /= x = PLet fc rc x xfc (sm 0 t) (sm 0 v) (sm 0 sc)

2440+ | otherwise = PLet fc rc x xfc (sm 0 t) (sm 0 v) sc

24342441 sm 0 (PApp f x as) = PApp f (sm 0 x) (map (fmap (sm 0)) as)

24352442 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)

24362443 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)

@@ -2507,7 +2514,7 @@ mkUniqueNames env shadows tm

25072514 ty' <- mkUniq 0 nmap ty

25082515 sc'' <- mkUniq 0 nmap' sc'

25092516 return $! PPi p n' fc ty' sc''

2510− mkUniq 0 nmap (PLet fc n nfc ty val sc)

2517+ mkUniq 0 nmap (PLet fc rc n nfc ty val sc)

25112518 = do env <- get

25122519 (n', sc') <-

25132520 if n `S.member` env

@@ -2519,7 +2526,7 @@ mkUniqueNames env shadows tm

25192526 let nmap' = M.insert n n' nmap

25202527 ty' <- mkUniq 0 nmap ty; val' <- mkUniq 0 nmap val

25212528 sc'' <- mkUniq 0 nmap' sc'

2522− return $! PLet fc n' nfc ty' val' sc''

2529+ return $! PLet fc rc n' nfc ty' val' sc''

25232530 mkUniq 0 nmap (PApp fc t args)

25242531 = do t' <- mkUniq 0 nmap t

25252532 args' <- mapM (mkUniqA 0 nmap) args

src/Idris/AbsSyntaxTree.hs+28−18

@@ -146,6 +146,7 @@ data PPOption = PPOption {

146146 , ppopt_desugarnats :: Bool

147147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings

148148 , ppopt_depth :: Maybe Int

149+ , ppopt_displayrig :: Bool -- ^ whether to display multiplicities in binders

149150 } deriving (Show)

150151

151152

@@ -160,6 +161,7 @@ defaultPPOption = PPOption {

160161 , ppopt_desugarnats = False

161162 , ppopt_pinames = False

162163 , ppopt_depth = Nothing

164+ , ppopt_displayrig = False

163165 }

164166

165167-- | Pretty printing options with the most verbosity.

@@ -169,6 +171,7 @@ verbosePPOption = PPOption {

169171 , ppopt_desugarnats = True

170172 , ppopt_pinames = True

171173 , ppopt_depth = Nothing

174+ , ppopt_displayrig = False

172175 }

173176

174177-- | Get pretty printing options from the big options record.

@@ -178,6 +181,7 @@ ppOption opt = PPOption {

178181 , ppopt_pinames = False

179182 , ppopt_depth = opt_printdepth opt

180183 , ppopt_desugarnats = opt_desugarnats opt

184+ , ppopt_displayrig = False

181185 }

182186

183187-- | Get pretty printing options from an idris state record.

@@ -529,6 +533,8 @@ expl :: Plicity

529533expl = Exp [] Dynamic False RigW

530534expl_param :: Plicity

531535expl_param = Exp [] Dynamic True RigW

536+expl_linear :: Plicity

537+expl_linear = Exp [] Dynamic False Rig1

532538

533539constraint :: Plicity

534540constraint = Constraint [] Static RigW

@@ -949,7 +955,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

949955 | PPatvar FC Name -- ^ A pattern variable

950956 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.

951957 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable

952− | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

958+ | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

953959 | PTyped PTerm PTerm -- ^ Term with explicit type

954960 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

955961 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument

@@ -1019,7 +1025,7 @@ mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n

10191025mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n

10201026mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)

10211027mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1022−mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

1028+mapPTermFC f g (PLet fc rc n fc' t1 t2 t3) = PLet (f fc) rc n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

10231029mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)

10241030mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

10251031mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)

@@ -1046,7 +1052,7 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

10461052 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)

10471053 mapPDoFC (DoBindP fc t1 t2 alts) =

10481054 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

1049− mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1055+ mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

10501056 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

10511057 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)

10521058mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

@@ -1073,7 +1079,7 @@ mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

10731079mapPT f t = f (mpt t) where

10741080 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)

10751081 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)

1076− mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

1082+ mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

10771083 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)

10781084 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

10791085 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)

@@ -1171,7 +1177,7 @@ type PTactic = PTactic' PTerm

11711177data PDo' t = DoExp FC t

11721178 | DoBind FC Name FC t -- ^ second FC is precise name location

11731179 | DoBindP FC t t [(t,t)]

1174− | DoLet FC Name FC t t -- ^ second FC is precise name location

1180+ | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location

11751181 | DoLetP FC t t

11761182 | DoRewrite FC t -- rewrite in do block

11771183 deriving (Eq, Ord, Functor, Data, Generic, Typeable)

@@ -1183,7 +1189,7 @@ instance Sized a => Sized (PDo' a) where

11831189 size (DoExp fc t) = 1 + size fc + size t

11841190 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

11851191 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

1186− size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r

1192+ size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r

11871193 size (DoLetP fc l r) = 1 + size fc + size l + size r

11881194 size (DoRewrite fc h) = 1 + size fc + size h

11891195

@@ -1248,7 +1254,7 @@ highestFC (PInferRef fc _ _) = Just fc

12481254highestFC (PPatvar fc _) = Just fc

12491255highestFC (PLam fc _ _ _ _) = Just fc

12501256highestFC (PPi _ _ _ _ _) = Nothing

1251−highestFC (PLet fc _ _ _ _ _) = Just fc

1257+highestFC (PLet fc _ _ _ _ _ _) = Just fc

12521258highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty

12531259highestFC (PApp fc _ _) = Just fc

12541260highestFC (PAppBind fc _ _) = Just fc

@@ -1279,7 +1285,7 @@ highestFC (PDoBlock lines) =

12791285 getDoFC (DoExp fc t) = fc

12801286 getDoFC (DoBind fc nm nfc t) = fc

12811287 getDoFC (DoBindP fc l r alts) = fc

1282− getDoFC (DoLet fc nm nfc l r) = fc

1288+ getDoFC (DoLet fc rc nm nfc l r) = fc

12831289 getDoFC (DoLetP fc l r) = fc

12841290 getDoFC (DoRewrite fc h) = fc

12851291

@@ -1504,7 +1510,7 @@ inferCon = sMN 0 "__infer"

15041510inferDecl = PDatadecl inferTy primfc

15051511 (PType bi)

15061512 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (

1507− PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))

1513+ PPi expl_linear (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))

15081514 (PRef bi [] inferTy)), bi, [])]

15091515inferOpts = []

15101516

@@ -1673,7 +1679,11 @@ prettyImp impl = pprintPTerm impl [] [] []

16731679

16741680-- | Do the right thing for rendering a term in an IState

16751681prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1676−prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1682+prettyIst ist = pprintPTerm opt [] [] (idris_infixes ist)

1683+ where

1684+ opt = if LinearTypes `elem` idris_language_extensions ist

1685+ then (ppOptionIst ist) { ppopt_displayrig = True }

1686+ else ppOptionIst ist

16771687

16781688-- | Pretty-print a high-level Idris term in some bindings context

16791689-- with infix info.

@@ -1709,16 +1719,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17091719 prettyBindingsOf [n] t = prettyBindingOf n t

17101720 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>

17111721 prettyBindingsOf ns t

1712− prettySe d p bnd (PLet fc n nfc ty v sc) =

1722+ prettySe d p bnd (PLet fc rc n nfc ty v sc) =

17131723 depth d . bracket p startPrec . group . align $

17141724 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>

17151725 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)

17161726 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)

1717− | Rig0 <- rig =

1727+ | Rig0 <- rig, ppopt_displayrig ppo =

17181728 depth d . bracket p startPrec . group $

17191729 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

17201730 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

1721− | Rig1 <- rig =

1731+ | Rig1 <- rig, ppopt_displayrig ppo =

17221732 depth d . bracket p startPrec . group $

17231733 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>

17241734 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc

@@ -1946,7 +1956,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

19461956 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab

19471957 text "no pretty printer for pattern-matching do binding" :

19481958 ppdo bnd dos

1949− ppdo bnd (DoLet _ ln _ ty v : dos) =

1959+ ppdo bnd (DoLet _ _ ln _ ty v : dos) =

19501960 (kwd "let" <+> prettyBindingOf ln False <+>

19511961 (if ty /= Placeholder

19521962 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="

@@ -2234,7 +2244,7 @@ instance Sized PTerm where

22342244 size (PRef fc _ name) = size name

22352245 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy

22362246 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy

2237− size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy

2247+ size (PLet fc _ name nfc ty def bdy) = 1 + size ty + size def + size bdy

22382248 size (PTyped trm ty) = 1 + size trm + size ty

22392249 size (PApp fc name args) = 1 + size args

22402250 size (PAppBind fc name args) = 1 + size args

@@ -2280,7 +2290,7 @@ allNamesIn tm = nub $ ni 0 [] tm

22802290 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f

22812291 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

22822292 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2283− ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

2293+ ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

22842294 ni 0 env (PHidden tm) = ni 0 env tm

22852295 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r

22862296 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

@@ -2311,7 +2321,7 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

23112321 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)

23122322 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]

23132323 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc

2314− ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc

2324+ ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc

23152325 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p

23162326 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r

23172327 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r

@@ -2375,7 +2385,7 @@ implicitNamesIn uvars ist tm

23752385 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

23762386 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

23772387 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2378− ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;

2388+ ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;

23792389 ni 0 env val; ni 0 (n:env) sc

23802390 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

23812391 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

src/Idris/Apropos.hs+1−1

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

7575instance Apropos (Binder (TT Name)) where

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

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

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

78+ isApropos str (Let _ ty val) = str == T.pack "let" || isApropos str ty || isApropos str val

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

8080 isApropos str _ = False -- these shouldn't occur in defined libraries

8181

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

@@ -141,7 +141,7 @@ namesUsed sc = nub $ nu' [] sc where

141141 | otherwise = [n]

142142 nut ps (App _ f a) = nut ps f ++ nut ps a

143143 nut ps (Proj t _) = nut ps t

144− nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

144+ nut ps (Bind n (Let _ t v) sc) = nut ps v ++ nut (n:ps) sc

145145 nut ps (Bind n b sc) = nut (n:ps) sc

146146 nut ps _ = []

147147

@@ -176,7 +176,7 @@ findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where

176176 (S.unions $ map (nut ps) args)

177177 | (P (TCon _ _) n _, _) <- unApply fn = S.empty

178178 | otherwise = S.union (nut ps f) (nut ps a)

179− nut ps (Bind n (Let t v) sc) = S.union (nut ps v) (nut (n:ps) sc)

179+ nut ps (Bind n (Let _ t v) sc) = S.union (nut ps v) (nut (n:ps) sc)

180180 nut ps (Proj t _) = nut ps t

181181 nut ps (Bind n b sc) = nut (n:ps) sc

182182 nut ps _ = S.empty

@@ -188,7 +188,7 @@ findCalls' ignoreasserts sc topargs = S.toList $ nu' topargs sc where

188188

189189directUse :: TT Name -> [Name]

190190directUse (P _ n _) = [n]

191−directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

191+directUse (Bind n (Let _ t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

192192 ++ directUse t

193193directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

194194directUse fn@(App _ f a)

src/Idris/Core/Elaborate.hs+8−7

@@ -437,8 +437,8 @@ introTy ty n = processTactic' (IntroTy ty n)

437437forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()

438438forall n r i t = processTactic' (Forall n r i t)

439439

440−letbind :: Name -> Raw -> Raw -> Elab' aux ()

441−letbind n t v = processTactic' (LetBind n t v)

440+letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux ()

441+letbind n rig t v = processTactic' (LetBind n rig t v)

442442

443443expandLet :: Name -> Term -> Elab' aux ()

444444expandLet n v = processTactic' (ExpandLet n v)

@@ -503,7 +503,7 @@ dotterm = do ES (p, a) s m <- get

503503 = union (foB b)

504504 (findOuter h env (instantiate (P Bound n (binderTy b)) sc))

505505 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)

506− foB (Let t v) = union (findOuter h env t) (findOuter h env v)

506+ foB (Let _ t v) = union (findOuter h env t) (findOuter h env v)

507507 foB b = findOuter h env (binderTy b)

508508 findOuter h env (App _ f a)

509509 = union (findOuter h env f) (findOuter h env a)

@@ -527,10 +527,11 @@ matchProblems all = processTactic' (MatchProblems all)

527527unifyProblems :: Elab' aux ()

528528unifyProblems = processTactic' UnifyProblems

529529

530−defer :: [Name] -> Name -> Elab' aux Name

531−defer ds n = do n' <- unique_hole n

532− processTactic' (Defer ds n')

533− return n'

530+defer :: [Name] -> [Name] -> Name -> Elab' aux Name

531+defer ds ls n

532+ = do n' <- unique_hole n

533+ processTactic' (Defer ds ls n')

534+ return n'

534535

535536deferType :: Name -> Raw -> [Name] -> Elab' aux ()

536537deferType n ty ns = processTactic' (DeferType n ty ns)

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

@@ -66,7 +66,7 @@ data Value = VP NameType Name Value

6666 -- True for Bool indicates safe to reduce

6767 | VBind Bool Name (Binder Value) (Value -> Eval Value)

6868 -- For frozen let bindings when simplifying

69− | VBLet Int Name Value Value Value

69+ | VBLet RigCount Int Name Value Value Value

7070 | VApp Value Value

7171 | VType UExp

7272 | VUType Universe

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

278278 | otherwise = cases_compiletime cd

279279

280280 ev ntimes stk top env (P _ n ty)

281− | Just (Let t v) <- lookupBinder n genv = ev ntimes stk top env v

281+ | Just (Let _ t v) <- lookupBinder n genv = ev ntimes stk top env v

282282 ev ntimes_in stk top env (P Ref n ty)

283283 = do let limit = if simpl then 100 else 10000

284284 (u, ntimes) <- usable spec unfold limit n ntimes_in

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

311311 ev ntimes stk top env (V i)

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

313313 | otherwise = return $ VV i

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

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

315315 | (not (runtime || simpl_inline || unfold)) || occurrences n sc < 2

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

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

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

325325 let vd = nexthole hs

326326 put (hs { nexthole = vd + 1 })

327327 sc' <- ev ntimes stk top ((n, VP Bound (sMN vd "vlet") VErased) : env) sc

328− return $ VBLet vd n t' v' sc'

328+ return $ VBLet c vd n t' v' sc'

329329 ev ntimes stk top env (Bind n (NLet t v) sc)

330330 = do t' <- ev ntimes stk top env (finalise t)

331331 v' <- ev ntimes stk top env (finalise v)

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

333− return $ VBind True n (Let t' v') (\x -> return sc')

333+ return $ VBind True n (Let RigW t' v') (\x -> return sc')

334334 ev ntimes stk top env (Bind n b sc)

335335 = do b' <- vbind env b

336336 let n' = uniqueName n (map fstEnv genv ++ map fst env)

@@ -574,12 +574,12 @@ instance Quote Value where

574574 b' <- quoteB b

575575 liftM (Bind n b') (quote (i+1) sc')

576576 where quoteB t = fmapMB (quote i) t

577− quote i (VBLet vd n t v sc)

577+ quote i (VBLet c vd n t v sc)

578578 = do sc' <- quote i sc

579579 t' <- quote i t

580580 v' <- quote i v

581581 let sc'' = pToV (sMN vd "vlet") (addBinder sc')

582− return (Bind n (Let t' v') sc'')

582+ return (Bind n (Let c t' v') sc'')

583583 quote i (VApp f a) = liftM2 (App MaybeHoles) (quote i f) (quote i a)

584584 quote i (VType u) = return (TType u)

585585 quote i (VUType u) = return (UType u)

@@ -632,7 +632,7 @@ convEq ctxt holes topx topy = ceq [] topx topy where

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

633633 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)

634634 where

635− ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

635+ ceqB ps (Let c v t) (Let c' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

636636 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

637637 ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

638638 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

@@ -1014,7 +1014,7 @@ simplifyCasedef n ufnames umethss ei uctxt

10141014 getNames under f ++ concatMap (getNames under') args

10151015 getNames (Just under) (P _ ref _)

10161016 = if ref `elem` inames then [under] else []

1017− getNames under (Bind n (Let t v) sc)

1017+ getNames under (Bind n (Let c t v) sc)

10181018 = getNames Nothing t ++

10191019 getNames Nothing v ++

10201020 getNames Nothing sc

src/Idris/Core/Execute.hs+5−4

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

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

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

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

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

116+ fixBinder (Let rig t1 t2) = Let rig <$> toTT t1 <*> toTT t2

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

118118 fixBinder (Hole t) = Hole <$> toTT t

119119 fixBinder (GHole i ns t) = GHole i ns <$> toTT t

@@ -134,7 +134,7 @@ toTT (EConstant c) = return (Constant c)

134134toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

135135 return $ normalise ctxt env' tm

136136 where toBinder (n, v) = do v' <- toTT v

137− return (n, RigW, Let Erased v')

137+ return (n, RigW, Let RigW Erased v')

138138toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."

139139toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."

140140toTT (EStringBuf ptr) = execFail $ Msg "Can't convert string buffers back to TT after execution."

@@ -207,8 +207,9 @@ doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)

207207doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

208208doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

209209 | otherwise = execFail . Msg $ "env too small"

210−doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

211− doExec ((n, v'):env) ctxt body

210+doExec env ctxt (Bind n (Let rig t v) body)

211+ = do v' <- doExec env ctxt v

212+ doExec ((n, v'):env) ctxt body

212213doExec env ctxt (Bind n (NLet t v) body) = undefined

213214doExec env ctxt tm@(Bind n b body) = do b' <- forM b (doExec env ctxt)

214215 return $

src/Idris/Core/ProofState.hs+27−23

@@ -31,6 +31,7 @@ import Util.Pretty hiding (fill)

3131import Control.Arrow ((***))

3232import Control.Monad.State.Strict

3333import Data.List

34+import Debug.Trace

3435

3536data ProofState = PS { thname :: Name,

3637 holes :: [Name], -- ^ holes still to be solved

@@ -88,7 +89,7 @@ data Tactic = Attack

8889 | Intro (Maybe Name)

8990 | IntroTy Raw (Maybe Name)

9091 | Forall Name RigCount (Maybe ImplicitInfo) Raw

91− | LetBind Name Raw Raw

92+ | LetBind Name RigCount Raw Raw

9293 | ExpandLet Name Term

9394 | Rewrite Raw

9495 | Induction Raw

@@ -97,7 +98,7 @@ data Tactic = Attack

9798 | PatVar Name

9899 | PatBind Name RigCount

99100 | Focus Name

100− | Defer [Name] Name

101+ | Defer [Name] [Name] Name

101102 | DeferType Name Raw [Name]

102103 | Implementation Name

103104 | AutoArg Name

@@ -128,7 +129,7 @@ instance Show ProofState where

128129 ") -------\n " ++

129130 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"

130131 where showPs env [] = ""

131− showPs env ((n, _, Let t v):bs)

132+ showPs env ((n, _, Let _ t v):bs)

132133 = " " ++ show n ++ " : " ++

133134 showEnv env ({- normalise ctxt env -} t) ++ " = " ++

134135 showEnv env ({- normalise ctxt env -} v) ++

@@ -159,7 +160,7 @@ instance Pretty ProofState OutputAnnotation where

159160 prettyGoal ps b = prettyEnv ps $ binderTy b

160161

161162 prettyPs env [] = empty

162− prettyPs env ((n, _, Let t v):bs) =

163+ prettyPs env ((n, _, Let _ t v):bs) =

163164 nest nestingSize (pretty n <+> colon <+>

164165 prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

165166 nest nestingSize (prettyPs env bs))

@@ -358,9 +359,9 @@ tactic h f = do ps <- get

358359

359360computeLet :: Context -> Name -> Term -> Term

360361computeLet ctxt n tm = cl [] tm where

361− cl env (Bind n' (Let t v) sc)

362+ cl env (Bind n' (Let r t v) sc)

362363 | n' == n = let v' = normalise ctxt env v in

363− Bind n' (Let t v') sc

364+ Bind n' (Let r t v') sc

364365 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, Rig0, b):env) sc)

365366 cl env (App s f a) = App s (cl env f) (cl env a)

366367 cl env t = t

@@ -412,7 +413,7 @@ reorder_claims ctxt env t

412413 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys

413414 | otherwise = y : insertB x ys

414415

415− noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v

416+ noOcc (n, _) (_, Let _ t v) = noOccurrence n t && noOccurrence n v

416417 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v

417418 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)

418419

@@ -459,8 +460,8 @@ setinj n ctxt env (Bind x b sc)

459460 ps { injective = n : is })

460461 return (Bind x b sc)

461462

462−defer :: [Name] -> Name -> RunTactic

463−defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

463+defer :: [Name] -> [Name] -> Name -> RunTactic

464+defer dropped linused n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

464465 do let env' = filter (\(n, _, t) -> n `notElem` dropped) env

465466 action (\ps -> let hs = holes ps in

466467 ps { usedns = n : usedns ps,

@@ -470,10 +471,13 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

470471 (mkApp (P Ref n ty) (map getP (reverse env'))))

471472 where

472473 mkTy [] t = t

473− mkTy ((n,rig,b) : bs) t = Bind n (Pi RigW Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

474+ mkTy ((n,rig,b) : bs) t = Bind n (Pi (setRig rig n) Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

475+

476+ setRig Rig1 n | n `elem` linused = Rig0

477+ setRig rig n = rig

474478

475479 getP (n, rig, b) = P Bound n (binderTy b)

476−defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

480+defer dropped linused n ctxt env _ = fail "Can't defer a non-hole focus."

477481

478482-- as defer, but build the type and application explicitly

479483deferType :: Name -> Raw -> [Name] -> RunTactic

@@ -595,11 +599,11 @@ solve ctxt env (Bind x (Guess ty val) sc)

595599 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)

596600 tryLock hs t@(Bind n (Hole _) sc) = (t, False)

597601 tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)

598− tryLock hs t@(Bind n (Let ty val) sc)

602+ tryLock hs t@(Bind n (Let r ty val) sc)

599603 = let (ty', tyl) = tryLock hs ty

600604 (val', vall) = tryLock hs val

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

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

606+ (Bind n (Let r ty' val') sc', tyl && vall && scl)

603607 tryLock hs t@(Bind n b sc)

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

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

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

611615 case findType x sc of

612616 Just t -> lift $ tfail (CantInferType (show t))

613617 _ -> lift $ tfail (IncompleteTerm h)

614− where findType x (Bind n (Let t v) sc)

618+ where findType x (Bind n (Let r t v) sc)

615619 = findType x v `mplus` findType x sc

616620 findType x (Bind n t sc)

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

@@ -675,13 +679,13 @@ patvar n ctxt env (Bind x (Hole t) sc) =

675679 | otherwise = ps

676680patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm

677681

678−letbind :: Name -> Raw -> Raw -> RunTactic

679−letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

682+letbind :: Name -> RigCount -> Raw -> Raw -> RunTactic

683+letbind n rig ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

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

681685 (valv, valt) <- lift $ check ctxt env val

682686 lift $ isType ctxt env tyt

683− return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))

684−letbind n ty val ctxt env _ = fail "Can't let bind here"

687+ return $ Bind n (Let rig tyv valv) (Bind x (Hole t) (P Bound x t))

688+letbind n rig ty val ctxt env _ = fail "Can't let bind here"

685689

686690expandLet :: Name -> Term -> RunTactic

687691expandLet n v ctxt env tm =

@@ -715,9 +719,9 @@ mkP lt l r (Bind n b sc)

715719 = let b' = mkPB b

716720 sc' = if (r /= sc) then mkP lt l r sc else sc in

717721 Bind n b' sc'

718− where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

719− v' = if (r /= v) then mkP lt l r v else v in

720− Let t' v'

722+ where mkPB (Let c t v) = let t' = if (r /= t) then mkP lt l r t else t

723+ v' = if (r /= v) then mkP lt l r v else v in

724+ Let c t' v'

721725 mkPB b = let ty = binderTy b

722726 ty' = if (r /= ty) then mkP lt l r ty else ty in

723727 b { binderTy = ty' }

@@ -1103,7 +1107,7 @@ process t h = tactic (Just h) (mktac t)

11031107 mktac (Intro n) = intro n

11041108 mktac (IntroTy ty n) = introTy ty n

11051109 mktac (Forall n r i t) = forall n r i t

1106− mktac (LetBind n t v) = letbind n t v

1110+ mktac (LetBind n r t v) = letbind n r t v

11071111 mktac (ExpandLet n b) = expandLet n b

11081112 mktac (Rewrite t) = rewrite t

11091113 mktac (Induction t) = casetac t True

@@ -1114,7 +1118,7 @@ process t h = tactic (Just h) (mktac t)

11141118 mktac (CheckIn r) = check_in r

11151119 mktac (EvalIn r) = eval_in r

11161120 mktac (Focus n) = focus n

1117− mktac (Defer ns n) = defer ns n

1121+ mktac (Defer ns ls n) = defer ns ls n

11181122 mktac (DeferType n t a) = deferType n t a

11191123 mktac (Implementation n)= implementationArg n

11201124 mktac (AutoArg n) = autoArg n

src/Idris/Core/ProofTerm.hs+33−25

@@ -31,8 +31,8 @@ data TermPath = Top

3131

3232-- | A zipper over binders, because terms and binders are mutually defined.

3333data BinderPath = Binder (Binder TermPath)

34− | LetT TermPath Term

35− | LetV Term TermPath

34+ | LetT RigCount TermPath Term

35+ | LetV RigCount Term TermPath

3636 | GuessT TermPath Term

3737 | GuessV Term TermPath

3838 deriving Show

@@ -46,8 +46,8 @@ replaceTop p (AppR s t r) = AppR s t (replaceTop p r)

4646replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc

4747 where

4848 replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)

49− replaceTopB p (LetT t v) = LetT (replaceTop p t) v

50− replaceTopB p (LetV t v) = LetV t (replaceTop p v)

49+ replaceTopB p (LetT c t v) = LetT c (replaceTop p t) v

50+ replaceTopB p (LetV c t v) = LetV c t (replaceTop p v)

5151 replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v

5252 replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)

5353replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

@@ -63,8 +63,8 @@ rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

6363-- | Build a binder from a zipper, given something to put in the hole.

6464rebuildBinder :: Term -> BinderPath -> Binder Term

6565rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p

66−rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t

67−rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)

66+rebuildBinder tm (LetT c p t) = Let c (rebuildTerm tm p) t

67+rebuildBinder tm (LetV c v p) = Let c v (rebuildTerm tm p)

6868rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t

6969rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)

7070

@@ -81,12 +81,12 @@ findHole n env t = fh' env Top t where

8181 | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)

8282 fh' env path (Bind x b sc)

8383 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)

84− | Just (p, env', tm) <- fh' ((x,RigW,b):env) path sc = Just (InScope x b p, env', tm)

84+ | Just (p, env', tm) <- fh' ((x,getRig b,b):env) path sc = Just (InScope x b p, env', tm)

8585 fh' _ _ _ = Nothing

8686

87− fhB env path (Let t v)

88− | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)

89− | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)

87+ fhB env path (Let c t v)

88+ | Just (p, env', tm) <- fh' env path t = Just (LetT c p v, env', tm)

89+ | Just (p, env', tm) <- fh' env path v = Just (LetV c t p, env', tm)

9090 fhB env path (Guess t v)

9191 | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)

9292 | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)

@@ -184,10 +184,10 @@ updateSolvedTerm' xs x = updateSolved' xs x where

184184 if ut then (P nt n ty', True) else (t, False)

185185 updateSolved' xs t = (t, False)

186186

187− updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

188− (v', uv) = updateSolved' xs v in

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

190− else (b, False)

187+ updateSolvedB' xs b@(Let c t v) = let (t', ut) = updateSolved' xs t

188+ (v', uv) = updateSolved' xs v in

189+ if ut || uv then (Let c t' v', True)

190+ else (b, False)

191191 updateSolvedB' xs b@(Guess t v) = let (t', ut) = updateSolved' xs t

192192 (v', uv) = updateSolved' xs v in

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

@@ -226,10 +226,10 @@ updsubst n v tm = fst $ subst' 0 tm

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

227227 subst' i t = (t, False)

228228

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

230− (v', uv) = subst' i v in

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

232− else (b, False)

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

230+ (v', uv) = subst' i v in

231+ if ut || uv then (Let c t' v', True)

232+ else (b, False)

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

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

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

@@ -256,8 +256,8 @@ updateSolvedPath ns (InBind n b sc)

256256 = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

257257 where

258258 updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)

259− updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)

260− updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)

259+ updateSolvedPathB (LetT c p v) = LetT c (updateSolvedPath ns p) (updateSolvedTerm ns v)

260+ updateSolvedPathB (LetV c v p) = LetV c (updateSolvedTerm ns v) (updateSolvedPath ns p)

261261 updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)

262262 updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)

263263updateSolvedPath ns (InScope n (Hole ty) t)

@@ -275,6 +275,13 @@ updateSolved xs pt@(PT path env sub ups)

275275 (updateSolvedTerm xs sub)

276276 (ups ++ xs)

277277

278+getRig :: Binder Term -> RigCount

279+getRig (Pi rig _ _ _) = rig

280+getRig (PVar rig _) = rig

281+getRig (Lam rig _) = rig

282+getRig (Let rig _ _) = rig

283+getRig _ = RigW

284+

278285goal :: Hole -> ProofTerm -> TC Goal

279286goal h pt@(PT path env sub ups)

280287-- | OK ginf <- g env sub = return ginf

@@ -287,12 +294,13 @@ goal h pt@(PT path env sub ups)

287294 = gb env b `mplus` g ((n, RigW, b):env) sc

288295 g env (Bind n b sc) | hole b && same h n = return $ GD env b

289296 | otherwise

290− = g ((n, RigW, b):env) sc `mplus` gb env b

297+ = g ((n, getRig b, b):env) sc `mplus` gb env b

298+

291299 g env (App Complete f a) = fail "Can't find hole"

292300 g env (App _ f a) = g env a `mplus` g env f

293301 g env t = fail "Can't find hole"

294302

295− gb env (Let t v) = g env v `mplus` g env t

303+ gb env (Let c t v) = g env v `mplus` g env t

296304 gb env (Guess t v) = g env v `mplus` g env t

297305 gb env t = g env (binderTy t)

298306

@@ -330,14 +338,14 @@ atHole h f c e pt -- @(PT path env sub)

330338 atH f c env binder@(Bind n b sc)

331339 | hole b && same h n = updated (f c env binder)

332340 | otherwise -- scope first

333− = do (sc', u) <- atH f c ((n, RigW, b) : env) sc

341+ = do (sc', u) <- atH f c ((n, getRig b, b) : env) sc

334342 if u then return (Bind n b sc', True)

335343 else do (b', u) <- atHb f c env b

336344 return (Bind n b' sc', u)

337345 atH tac c env (App s f a) = ulift2 tac c env (App s) f a

338346 atH tac c env t = return (t, False)

339347

340− atHb f c env (Let t v) = ulift2 f c env Let t v

348+ atHb f c env (Let rc t v) = ulift2 f c env (Let rc) t v

341349 atHb f c env (Guess t v) = ulift2 f c env Guess t v

342350 atHb f c env t = do (ty', u) <- atH f c env (binderTy t)

343351 return (t { binderTy = ty' }, u)

@@ -348,7 +356,7 @@ bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath up

348356bound_in_term :: Term -> [Name]

349357bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

350358 where

351− bi (Let t v) = bound_in_term t ++ bound_in_term v

359+ bi (Let c t v) = bound_in_term t ++ bound_in_term v

352360 bi (Guess t v) = bound_in_term t ++ bound_in_term v

353361 bi b = bound_in_term (binderTy b)

354362bound_in_term (App _ f a) = bound_in_term f ++ bound_in_term a

src/Idris/Core/TT.hs+29−25

@@ -844,7 +844,8 @@ data Binder b = Lam { binderCount :: RigCount,

844844 -- flag says whether it was a scoped implicit

845845 -- (i.e. forall bound) in the high level Idris, but

846846 -- otherwise has no relevance in TT.

847− | Let { binderTy :: !b,

847+ | Let { binderCount :: RigCount,

848+ binderTy :: !b,

848849 binderVal :: b {-^ value for bound variable-}}

849850 -- ^ A binding that occurs in a @let@ expression

850851 | NLet { binderTy :: !b,

@@ -882,7 +883,7 @@ deriving instance Binary Binder

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

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

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

885− size (Let ty val) = 1 + size ty + size val

886+ size (Let _ ty val) = 1 + size ty + size val

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

887888 size (Hole ty) = 1 + size ty

888889 size (GHole _ _ ty) = 1 + size ty

@@ -891,7 +892,7 @@ instance Sized a => Sized (Binder a) where

891892 size (PVTy ty) = 1 + size ty

892893

893894fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)

894−fmapMB f (Let t v) = liftM2 Let (f t) (f v)

895+fmapMB f (Let c t v) = liftM2 (Let c) (f t) (f v)

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

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

897898fmapMB f (Lam c t) = liftM (Lam c) (f t)

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

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

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

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

1022− termsize n (Bind n' (Let t v) sc)

1023+ termsize n (Bind n' (Let c t v) sc)

10231024 = let rn = if n == n' then sMN 0 "noname" else n in

10241025 termsize rn v + termsize rn sc

10251026 termsize n (Bind n' b sc)

@@ -1144,7 +1145,7 @@ vinstances :: Int -> TT n -> Int

11441145vinstances i (V x) | i == x = 1

11451146vinstances i (App _ f a) = vinstances i f + vinstances i a

11461147vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc

1147− where instancesB (Let t v) = vinstances i v

1148+ where instancesB (Let c t v) = vinstances i v

11481149 instancesB _ = 0

11491150vinstances i t = 0

11501151

@@ -1271,10 +1272,10 @@ subst n v tm = fst $ subst' 0 tm

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

12721273 subst' i t = (t, False)

12731274

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

1275− (v', uv) = subst' i v in

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

1277− else (b, False)

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

1276+ (v', uv) = subst' i v in

1277+ if ut || uv then (Let c t' v', True)

1278+ else (b, False)

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

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

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

@@ -1321,7 +1322,7 @@ substTerm old new = st where

13211322 eqAlpha as (App _ fx ax) (App _ fy ay) = eqAlpha as fx fy && eqAlpha as ax ay

13221323 eqAlpha as x y = x == y

13231324

1324− eqAlphaB as (Let xt xv) (Let yt yv)

1325+ eqAlphaB as (Let xc xt xv) (Let yc yt yv)

13251326 = eqAlpha as xt yt && eqAlpha as xv yv

13261327 eqAlphaB as (Guess xt xv) (Guess yt yv)

13271328 = eqAlpha as xt yt && eqAlpha as xv yv

@@ -1334,7 +1335,7 @@ occurrences n t = execState (no' 0 t) 0

13341335 no' i (V x) | i == x = do num <- get; put (num + 1)

13351336 no' i (P Bound x _) | n == x = do num <- get; put (num + 1)

13361337 no' i (Bind n b sc) = do noB' i b; no' (i+1) sc

1337− where noB' i (Let t v) = do no' i t; no' i v

1338+ where noB' i (Let c t v) = do no' i t; no' i v

13381339 noB' i (Guess t v) = do no' i t; no' i v

13391340 noB' i b = no' i (binderTy b)

13401341 no' i (App _ f a) = do no' i f; no' i a

@@ -1348,7 +1349,7 @@ noOccurrence n t = no' 0 t

13481349 no' i (V x) = not (i == x)

13491350 no' i (P Bound x _) = not (n == x)

13501351 no' i (Bind n b sc) = noB' i b && no' (i+1) sc

1351− where noB' i (Let t v) = no' i t && no' i v

1352+ where noB' i (Let c t v) = no' i t && no' i v

13521353 noB' i (Guess t v) = no' i t && no' i v

13531354 noB' i b = no' i (binderTy b)

13541355 no' i (App _ f a) = no' i f && no' i a

@@ -1360,7 +1361,7 @@ freeNames :: Eq n => TT n -> [n]

13601361freeNames t = nub $ freeNames' t

13611362 where

13621363 freeNames' (P _ n _) = [n]

1363− freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])

1364+ freeNames' (Bind n (Let c t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])

13641365 ++ freeNames' t

13651366 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])

13661367 freeNames' (App _ f a) = freeNames' f ++ freeNames' a

@@ -1434,8 +1435,8 @@ safeForgetEnv env (Bind n b sc)

14341435 b' <- safeForgetEnvB env b

14351436 sc' <- safeForgetEnv (n':env) sc

14361437 Just $ RBind n' b' sc'

1437− where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)

1438− (safeForgetEnv env v)

1438+ where safeForgetEnvB env (Let c t v) = liftM2 (Let c) (safeForgetEnv env t)

1439+ (safeForgetEnv env v)

14391440 safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)

14401441 (safeForgetEnv env v)

14411442 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)

@@ -1623,7 +1624,8 @@ prettyEnv env t = prettyEnv' env t False

16231624 prettySb env n (PVar Rig1 t) = prettyB env "pat 1 " "." n t

16241625 prettySb env n (PVar _ t) = prettyB env "pat" "." n t

16251626 prettySb env n (PVTy t) = prettyB env "pty" "." n t

1626− prettySb env n (Let t v) = prettyBv env "let" "in" n t v

1627+ prettySb env n (Let Rig1 t v) = prettyBv env "let 1 " "in" n t v

1628+ prettySb env n (Let _ t v) = prettyBv env "let" "in" n t v

16271629 prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v

16281630 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v

16291631

@@ -1651,7 +1653,7 @@ showEnv' env t dbg = se 10 env t where

16511653 = bracket p 2 $ sb env n b ++ se 10 ((n, rig, b):env) sc

16521654 se p env (Bind n b@(Pi rig _ t k) sc)

16531655 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow rig ++ se 10 ((n,Rig0,b):env) sc

1654− where arrow Rig0 = " -> "

1656+ where arrow Rig0 = " 0-> "

16551657 arrow Rig1 = " -o "

16561658 arrow RigW = " -> "

16571659 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,Rig0,b):env) sc

@@ -1676,7 +1678,9 @@ showEnv' env t dbg = se 10 env t where

16761678 sb env n (PVar Rig1 t) = showb env "pat 1 " ". " n t

16771679 sb env n (PVar _ t) = showb env "pat " ". " n t

16781680 sb env n (PVTy t) = showb env "pty " ". " n t

1679− sb env n (Let t v) = showbv env "let " " in " n t v

1681+ sb env n (Let Rig0 t v) = showbv env "let 0 " " in " n t v

1682+ sb env n (Let Rig1 t v) = showbv env "let 1 " " in " n t v

1683+ sb env n (Let _ t v) = showbv env "let " " in " n t v

16801684 sb env n (NLet t v) = showbv env "nlet " " in " n t v

16811685 sb env n (Guess t v) = showbv env "?? " " in " n t v

16821686

@@ -1693,7 +1697,7 @@ pureTerm (App _ f a) = pureTerm f && pureTerm a

16931697pureTerm (Bind n b sc) = notInterfaceName n && pureBinder b && pureTerm sc where

16941698 pureBinder (Hole _) = False

16951699 pureBinder (Guess _ _) = False

1696− pureBinder (Let t v) = pureTerm t && pureTerm v

1700+ pureBinder (Let c t v) = pureTerm t && pureTerm v

16971701 pureBinder t = pureTerm (binderTy t)

16981702

16991703 notInterfaceName (MN _ c) | c == txt "__interface" = False

@@ -1717,7 +1721,7 @@ weakenEnv :: EnvTT n -> EnvTT n

17171721weakenEnv env = wk (length env - 1) env

17181722 where wk i [] = []

17191723 wk i ((n, c, b) : bs) = (n, c, weakenTmB i b) : wk (i - 1) bs

1720− weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)

1724+ weakenTmB i (Let c t v) = Let c (weakenTm i t) (weakenTm i v)

17211725 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)

17221726 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }

17231727

@@ -1728,7 +1732,7 @@ weakenTmEnv i = map (\ (n, c, b) -> (n, c, fmap (weakenTm i) b))

17281732refsIn :: TT Name -> [Name]

17291733refsIn (P _ n _) = [n]

17301734refsIn (Bind n b t) = nub $ nb b ++ refsIn t

1731− where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)

1735+ where nb (Let _ t v) = nub (refsIn t) ++ nub (refsIn v)

17321736 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)

17331737 nb t = refsIn (binderTy t)

17341738refsIn (App s f a) = nub (refsIn f ++ refsIn a)

@@ -1738,7 +1742,7 @@ allTTNames :: Eq n => TT n -> [n]

17381742allTTNames = nub . allNamesIn

17391743 where allNamesIn (P _ n _) = [n]

17401744 allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t

1741− where nb (Let t v) = allNamesIn t ++ allNamesIn v

1745+ where nb (Let _ t v) = allNamesIn t ++ allNamesIn v

17421746 nb (Guess t v) = allNamesIn t ++ allNamesIn v

17431747 nb t = allNamesIn (binderTy t)

17441748 allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a

@@ -1790,7 +1794,7 @@ pprintTT bound tm = pp startPrec bound tm

17901794 where mkArrow Rig1 = text "⇴"

17911795 mkArrow Rig0 = text "⥛"

17921796 mkArrow _ = text "→"

1793− ppb p bound n (Let ty val) sc =

1797+ ppb p bound n (Let _ ty val) sc =

17941798 bracket p startPrec . group . align $

17951799 (group . hang 2) (annotate AnnKeyword (text "let") <+>

17961800 bindingOf n False <+> colon <+>

@@ -1872,8 +1876,8 @@ pprintRaw bound (RBind n b body) =

18721876 text "Lam" <$> pprintRaw bound ty

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

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

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

1876− vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]

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

1880+ vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]

18771881 ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $

18781882 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]

18791883 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $

src/Idris/Core/Typecheck.hs+29−21

@@ -98,7 +98,9 @@ check' holes tcns ctxt env top

9898 astate | holes = MaybeHoles

9999 | otherwise = Complete

100100

101− chk :: RigCount -> -- multiplicity (need enough in context to produce this many of the term)

101+ chk :: RigCount -> -- 'sigma' in Bob Atkey's QTT paper, except that

102+ -- for implementation purposes it could be 0, 1 or omega when

103+ -- checking variable usage.

102104 Type -> -- uniqueness level

103105 Maybe UExp -> -- universe for kind

104106 Env -> Raw -> StateT UCs TC (Term, Type, [Name])

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

118120 where rigSafe True _ _ n = Nothing

119121 rigSafe _ Rig1 RigW n = Just ("Trying to use linear name " ++ show n ++ " in non-linear context")

120122 rigSafe _ Rig0 RigW n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")

123+ rigSafe _ Rig0 Rig1 n = Just ("Trying to use irrelevant name " ++ show n ++ " in relevant context")

121124 rigSafe _ _ _ n = Nothing

122125

123126 used Rig0 n = []

@@ -137,13 +140,13 @@ check' holes tcns ctxt env top

137140 do (v, cs) <- get

138141 put (v+1, ULT (UVar tcns v) v' : cs)

139142 let apty = simplify initContext env

140− (Bind x (Let (TType v') (TType (UVar tcns v))) t)

143+ (Bind x (Let rig (TType v') (TType (UVar tcns v))) t)

141144 return (App Complete fv (TType (UVar tcns v)), apty, fns)

142145 Bind x (Pi rig i s k) t ->

143146 do (av, aty, _) <- chk rigc u Nothing env RType

144147 convertsC ctxt env aty s

145148 let apty = simplify initContext env

146− (Bind x (Let aty av) t)

149+ (Bind x (Let rig aty av) t)

147150 return (App astate fv av, apty, fns)

148151 t -> lift $ tfail $ NonFunctionType fv fty

149152 chk rigc u lvl env ap@(RApp f a)

@@ -156,12 +159,16 @@ check' holes tcns ctxt env top

156159 (rig, uniqueBinders (map fstEnv env) ty)

157160 _ -> (RigW, uniqueBinders (map fstEnv env)

158161 (normalise ctxt env fty)) -- This is an error, caught below...

159− (av, aty, ans) <- chk (rigMult rigc rigf) u Nothing env a

162+ (av, aty, ans_in) <- chk (rigMult rigf rigc) u Nothing env a

163+ -- usage in 'a' doesn't count if the binder has multiplicity 0

164+ let ans = case rigf of

165+ Rig0 -> []

166+ _ -> ans_in

160167 case fty' of

161168 Bind x (Pi rig i s k) t ->

162169 do convertsC ctxt env aty s

163170 let apty = simplify initContext env

164− (Bind x (Let aty av) t)

171+ (Bind x (Let rig aty av) t)

165172 return (App astate fv av, apty, fns ++ ans)

166173 t -> lift $ tfail $ NonFunctionType fv fty

167174 chk rigc u lvl env RType

@@ -195,8 +202,6 @@ check' holes tcns ctxt env top

195202 constType _ = TType (UVal 0)

196203 chk rigc u lvl env (RBind n (Pi rig i s k) t)

197204 = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s

198− when (rig == RigW) $

199− lift $ linearCheckArg ctxt (normalise ctxt env sv)

200205 (v, cs) <- get

201206 (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent

202207 put (v+1, cs)

@@ -218,16 +223,22 @@ check' holes tcns ctxt env top

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

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

220225

221− chk rigc u lvl env (RBind n b sc)

226+ chk rigc_in u lvl env (RBind n b sc)

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

223228 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

224− when (getCount b == RigW) $

225− lift $ linearCheckArg ctxt (normalise ctxt env (binderTy b'))

226229 checkUsageOK (getCount b) scns

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

228− where getCount (Pi rig _ _ _) = rigMult rigc rig

231+ where -- should only check at 0 or 1 (as in Bob's paper) but rigc_in

232+ -- might be RigW, since that's how we check in the Var rule that

233+ -- a linearly bound name is only used in a linear context.

234+ -- So, here, check the scope at multiplicity 1

235+ rigc = case rigc_in of

236+ Rig0 -> Rig0

237+ _ -> Rig1

238+ getCount (Pi rig _ _ _) = rigMult rigc rig

229239 getCount (PVar rig _) = rigMult rigc rig

230240 getCount (Lam rig _) = rigMult rigc rig

241+ getCount (Let rig _ _) = rigMult rigc rig

231242 getCount _ = rigMult rigc RigW

232243

233244 checkUsageOK Rig0 _ = return ()

@@ -242,15 +253,12 @@ check' holes tcns ctxt env top

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

243254 convType tcns ctxt env tt

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

245− checkBinder (Let t v)

256+ checkBinder (Let rig t v)

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

247− -- May have multiple uses, check at RigW

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

249− -- (Consider: adding a single use let?)

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

258+ (vv, vt, vns) <- chk (rigMult rig rigc) u Nothing env v

251259 convertsC ctxt env vt tv

252260 convType tcns ctxt env tt

253− return (Let tv vv, tt, vns)

261+ return (Let rig tv vv, tt, vns)

254262 checkBinder (NLet t v)

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

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

@@ -288,10 +296,10 @@ check' holes tcns ctxt env top

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

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

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

291− discharge n (Let t v) bt scv sct ns

292− = return (Bind n (Let t v) scv, Bind n (Let t v) sct, ns)

299+ discharge n (Let r t v) bt scv sct ns

300+ = return (Bind n (Let r t v) scv, Bind n (Let r t v) sct, ns)

293301 discharge n (NLet t v) bt scv sct ns

294− = return (Bind n (NLet t v) scv, Bind n (Let t v) sct, ns)

302+ = return (Bind n (NLet t v) scv, Bind n (Let RigW t v) sct, ns)

295303 discharge n (Hole t) bt scv sct ns

296304 = return (Bind n (Hole t) scv, sct, ns)

297305 discharge n (GHole i ns t) bt scv sct uns

@@ -339,7 +347,7 @@ checkUnique borrowed ctxt env tm

339347 = do chkBinderName env n b

340348 st <- get

341349 case b of

342− Let t v -> chkBinders env v

350+ Let _ t v -> chkBinders env v

343351 _ -> return ()

344352 chkBinders ((n, Rig0, b) : env) t

345353 chkBinders env t = return ()

src/Idris/Core/Unify.hs+5−4

@@ -130,9 +130,10 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

130130 lift $ tfail err

131131

132132

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

134− h2 <- un bnames vx vy

135− combine bnames h1 h2

133+ uB bnames (Let _ tx vx) (Let _ ty vy)

134+ = do h1 <- un bnames tx ty

135+ h2 <- un bnames vx vy

136+ combine bnames h1 h2

136137 uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty

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

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

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

585586 lift $ tfail err

586587

587588

588− uB env bnames (Let tx vx) (Let ty vy)

589+ uB env bnames (Let _ tx vx) (Let _ ty vy)

589590 = do h1 <- un' env False bnames tx ty

590591 h2 <- un' env False bnames vx vy

591592 sc 1

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

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

8585 | i < length env = let (tm, env') = env !! i in

8686 eval env' stk tm

8787 | otherwise = WV i

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

88+ eval wenv@(WEnv d env) stk (Bind n (Let c t v) sc)

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

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

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

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

9494 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

9595

9696 eval env stk (P nt n ty)

97− | Just (Let t v) <- lookupBinder n genv = eval env stk v

97+ | Just (Let c t v) <- lookupBinder n genv = eval env stk v

9898 eval env stk (P nt n ty) = apply env nt n ty stk

9999 eval env stk (App _ f a) = eval env ((a, env) : stk) f

100100 eval env stk (Constant c) = unload (WConstant c) stk

src/Idris/DSL.hs+10−9

@@ -54,12 +54,12 @@ expandSugar dsl (PLam fc n nfc ty tm)

5454 = PApp fc lam [ pexp (mkTTName fc n)

5555 , pexp (expandSugar dsl (var dsl n tm 0))]

5656expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)

57−expandSugar dsl (PLet fc n nfc ty v tm)

57+expandSugar dsl (PLet fc rc n nfc ty v tm)

5858 | Just letb <- dsl_let dsl

5959 = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

6060 , pexp (expandSugar dsl v)

6161 , pexp (expandSugar dsl (var dsl n tm 0))]

62−expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)

62+expandSugar dsl (PLet fc rc n nfc ty v tm) = PLet fc rc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)

6363expandSugar dsl (PPi p n fc ty tm)

6464 | Just pi <- dsl_pi dsl

6565 = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

@@ -103,8 +103,8 @@ expandSugar dsl (PDoBlock ds)

103103 = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "__bpat") NoFC Placeholder

104104 (PCase fc (PRef fc [] (sMN 0 "__bpat"))

105105 ((p, block b rest) : alts)))]

106− block b (DoLet fc n nfc ty tm : rest)

107− = PLet fc n nfc ty tm (block b rest)

106+ block b (DoLet fc rc n nfc ty tm : rest)

107+ = PLet fc rc n nfc ty tm (block b rest)

108108 block b (DoLetP fc p tm : rest)

109109 = PCase fc tm [(p, block b rest)]

110110 block b (DoRewrite fc h : rest)

@@ -134,10 +134,10 @@ var dsl n t i = v' i t where

134134 | Nothing <- dsl_lambda dsl

135135 = PLam fc n nfc ty (v' i sc)

136136 | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)

137− v' i (PLet fc n nfc ty val sc)

137+ v' i (PLet fc rc n nfc ty val sc)

138138 | Nothing <- dsl_let dsl

139− = PLet fc n nfc (v' i ty) (v' i val) (v' i sc)

140− | otherwise = PLet fc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)

139+ = PLet fc rc n nfc (v' i ty) (v' i val) (v' i sc)

140+ | otherwise = PLet fc rc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)

141141 v' i (PPi p n fc ty sc)

142142 | Nothing <- dsl_pi dsl

143143 = PPi p n fc (v' i ty) (v' i sc)

@@ -200,8 +200,9 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

200200 arg' <- db' arg

201201 return (PWithApp fc t' arg')

202202 db' (PLam fc n nfc ty sc) = return (PLam fc n nfc ty (debind b sc))

203− db' (PLet fc n nfc ty v sc) = do v' <- db' v

204− return (PLet fc n nfc ty v' (debind b sc))

203+ db' (PLet fc rc n nfc ty v sc)

204+ = do v' <- db' v

205+ return (PLet fc rc n nfc ty v' (debind b sc))

205206 db' (PCase fc s opts) = do s' <- db' s

206207 return (PCase fc s' (map (pmap (debind b)) opts))

207208 db' (PPair fc hls p l r) = do l' <- db' l

src/Idris/DataOpts.hs+1−1

@@ -43,7 +43,7 @@ instance Optimisable Raw where

4343

4444-- Erase types (makes ibc smaller, and we don't need them)

4545instance Optimisable (Binder (TT Name)) where

46− applyOpts (Let t v) = Let <$> return Erased <*> applyOpts v

46+ applyOpts (Let r t v) = Let r <$> return Erased <*> applyOpts v

4747 applyOpts b = return (b { binderTy = Erased })

4848

4949instance Optimisable (Binder Raw) where

src/Idris/Delaborate.hs+7−7

@@ -55,13 +55,13 @@ resugar ist = transform flattenDoLet . transform resugarApp

5555 = PConstant fc (BI i)

5656 resugarApp tm = tm

5757

58− flattenDoLet (PLet _ ln _ ty v bdy)

58+ flattenDoLet (PLet _ rc ln _ ty v bdy)

5959 | PDoBlock dos <- flattenDoLet bdy

60− = PDoBlock (DoLet NoFC ln NoFC ty v : dos)

60+ = PDoBlock (DoLet NoFC rc ln NoFC ty v : dos)

6161 flattenDoLet (PDoBlock dos) =

6262 PDoBlock $ concatMap fixExp dos

63− where fixExp (DoExp _ (PLet _ ln _ ty v bdy)) =

64− DoLet NoFC ln NoFC ty v : fixExp (DoExp NoFC bdy)

63+ where fixExp (DoExp _ (PLet _ rc ln _ ty v bdy)) =

64+ DoLet NoFC rc ln NoFC ty v : fixExp (DoExp NoFC bdy)

6565 fixExp d = [d]

6666 flattenDoLet tm = tm

6767

@@ -172,13 +172,13 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

172172 = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)

173173 (de ((n, ty) : tys) ((n,n):env) [] sc)

174174

175− de tys env imps (Bind n (Let ty val) sc)

175+ de tys env imps (Bind n (Let rc ty val) sc)

176176 | docases

177177 , isCaseApp sc

178178 , (P _ cOp _, args) <- unApply sc

179179 , Just caseblock <- delabCase tys env imps val cOp args = caseblock

180180 | otherwise =

181− PLet un n NoFC (de tys env [] ty)

181+ PLet un rc n NoFC (de tys env [] ty)

182182 (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)

183183 de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

184184 de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

@@ -441,7 +441,7 @@ pprintErr' i (IncompleteTerm t)

441441 = getMissing (n : hs) (n : env) sc

442442 getMissing hs env (Bind n (Guess _ _) sc)

443443 = getMissing (n : hs) (n : env) sc

444− getMissing hs env (Bind n (Let t v) sc)

444+ getMissing hs env (Bind n (Let rc t v) sc)

445445 = getMissing hs env t ++

446446 getMissing hs env v ++

447447 getMissing hs (n : env) sc

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

@@ -21,7 +21,7 @@ desugarAs lhs rhs whereblock

2121 (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []

2222

2323 bindOnRight :: PTerm -> [(Name, FC, PTerm)] -> PTerm

24− bindOnRight = foldr (\(n, fc, tm) -> PLet fc n NoFC Placeholder tm)

24+ bindOnRight = foldr (\(n, fc, tm) -> PLet fc RigW n NoFC Placeholder tm)

2525

2626 bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl

2727 bindInWhereDecl pats (PClauses fc opts n clauses)

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

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

509509 concreteTm ist (Constant _) = True

510510 concreteTm ist (Bind n (Lam _ _) sc) = True

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

512− concreteTm ist (Bind n (Let _ _) sc) = concreteTm ist sc

512+ concreteTm ist (Bind n (Let _ _ _) sc) = concreteTm ist sc

513513 concreteTm ist _ = False

514514

515515 -- get the type of a specialised application

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

902902 getVs _ = []

903903 borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a

904904 borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc

905− where borrowedB (Let t v) = nub $ borrowedNames env t ++ borrowedNames env v

905+ where borrowedB (Let _ t v) = nub $ borrowedNames env t ++ borrowedNames env v

906906 borrowedB b = borrowedNames env (binderTy b)

907907 borrowedNames _ _ = []

908908

src/Idris/Elab/Data.hs−2

@@ -99,8 +99,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

9999 -- TMP HACK! Make this a data option

100100 updateContext (addDatatype (Data n ttag cty unique cons))

101101 updateContext (setMetaInformation n metainf)

102− when (any linearArg (map snd cons)) $

103− updateContext (setRigCount n Rig1)

104102

105103 mapM_ totcheck (zip (repeat fc) (map fst cons))

106104-- mapM_ (checkPositive n) cons

src/Idris/Elab/Quasiquote.hs+4−4

@@ -70,10 +70,10 @@ extractDoUnquotes d (DoBind fc n nfc tm)

7070 return (DoBind fc n nfc tm', ex)

7171extractDoUnquotes d (DoBindP fc t t' alts)

7272 = fail "Pattern-matching binds cannot be quasiquoted"

73−extractDoUnquotes d (DoLet fc n nfc v b)

73+extractDoUnquotes d (DoLet fc rc n nfc v b)

7474 = do (v', ex1) <- extractUnquotes d v

7575 (b', ex2) <- extractUnquotes d b

76− return (DoLet fc n nfc v' b', ex1 ++ ex2)

76+ return (DoLet fc rc n nfc v' b', ex1 ++ ex2)

7777extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"

7878extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"

7979

@@ -87,11 +87,11 @@ extractUnquotes n (PPi plicity name fc ty body)

8787 = do (ty', ex1) <- extractUnquotes n ty

8888 (body', ex2) <- extractUnquotes n body

8989 return (PPi plicity name fc ty' body', ex1 ++ ex2)

90−extractUnquotes n (PLet fc name nfc ty val body)

90+extractUnquotes n (PLet fc rc name nfc ty val body)

9191 = do (ty', ex1) <- extractUnquotes n ty

9292 (val', ex2) <- extractUnquotes n val

9393 (body', ex3) <- extractUnquotes n body

94− return (PLet fc name nfc ty' val' body', ex1 ++ ex2 ++ ex3)

94+ return (PLet fc rc name nfc ty' val' body', ex1 ++ ex2 ++ ex3)

9595extractUnquotes n (PTyped tm ty)

9696 = do (tm', ex1) <- extractUnquotes n tm

9797 (ty', ex2) <- extractUnquotes n ty

src/Idris/Elab/Rewrite.hs+6−5

@@ -50,14 +50,14 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

5050 Nothing -> return sc_in

5151 Just t -> do

5252 letn <- getNameFrom (sMN 0 "rewrite_result")

53− return $ PLet fc letn fc t sc_in

53+ return $ PLet fc RigW letn fc t sc_in

5454 (PRef fc [] letn)

5555 tyn <- getNameFrom (sMN 0 "rty")

5656 claim tyn RType

5757 valn <- getNameFrom (sMN 0 "rval")

5858 claim valn (Var tyn)

5959 letn <- getNameFrom (sMN 0 "_rewrite_rule")

60− letbind letn (Var tyn) (Var valn)

60+ letbind letn RigW (Var tyn) (Var valn)

6161 focus valn

6262 elab rule

6363 compute

@@ -95,9 +95,10 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

9595 = let b' = mkPB b

9696 sc' = if (r /= sc) then mkP lt l r sc else sc in

9797 Bind n b' sc'

98− where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

99− v' = if (r /= v) then mkP lt l r v else v in

100− Let t' v'

98+ where mkPB (Let rig t v)

99+ = let t' = if (r /= t) then mkP lt l r t else t

100+ v' = if (r /= v) then mkP lt l r v else v in

101+ Let rig t' v'

101102 mkPB b = let ty = binderTy b

102103 ty' = if (r /= ty) then mkP lt l r ty else ty in

103104 b { binderTy = ty' }

src/Idris/Elab/Term.hs+48−27

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

252252 ptm <- get_term

253253 when pattern $

254254 -- Look for Rig1 (linear) pattern bindings

255− do let pnms = findLinear ist [] ptm

255+ do let pnms = findLinear Rig1 ist [] ptm

256256 update_term (setLinear pnms)

257257 where

258258 pattern = emode == ELHS || emode == EImpossible

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

695695 elabE ec' fc sc

696696 solve

697697 highlightSource nfc (AnnBoundName n False)

698− elab' ina _ tm@(PLet fc n nfc ty val sc)

698+ elab' ina _ tm@(PLet fc rig n nfc ty val sc)

699699 = do attack

700700 ivs <- get_implementations

701701 tyn <- getNameFrom (sMN 0 "letty")

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

703703 valn <- getNameFrom (sMN 0 "letval")

704704 claim valn (Var tyn)

705705 explicit valn

706− letbind n (Var tyn) (Var valn)

706+ letbind n rig (Var tyn) (Var valn)

707707 addPSname n

708708 case ty of

709709 Placeholder -> return ()

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

730730 -- HACK: If the name leaks into its type, it may leak out of

731731 -- scope outside, so substitute in the outer scope.

732732 expandLet n (case lookupBinder n env of

733− Just (Let t v) -> v

733+ Just (Let rig t v) -> v

734734 other -> error ("Value not a let binding: " ++ show other))

735735 solve

736736 highlightSource nfc (AnnBoundName n False)

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

741741 claim tyn RType

742742 valn <- getNameFrom (sMN 0 "letval")

743743 claim valn (Var tyn)

744− letbind n (Var tyn) (Var valn)

744+ letbind n RigW (Var tyn) (Var valn)

745745 focus valn

746746 elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])

747747 env <- get_env

@@ -991,11 +991,13 @@ elab ist info emode opts fn tm

991991 -- When building the metavar application, leave out the unique

992992 -- names which have been used elsewhere in the term, since we

993993 -- won't be able to use them in the resulting application.

994+ env <- get_env

994995 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

996+ let lin_used = getLinearUsed (tt_ctxt ist) ptm

995997 let n' = metavarName (namespace info) n

996998 attack

997999 psns <- getPSnames

998− n' <- defer unique_used n'

1000+ n' <- defer unique_used lin_used n'

9991001 solve

10001002 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

10011003 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

@@ -1016,7 +1018,10 @@ elab ist info emode opts fn tm

10161018 valn <- getNameFrom (sMN 0 "scval")

10171019 scvn <- getNameFrom (sMN 0 "scvar")

10181020 claim valn (Var tyn)

1019− letbind scvn (Var tyn) (Var valn)

1021+ env <- get_env

1022+

1023+ let scrnames = allNamesIn scr

1024+ letbind scvn (letrig scrnames env) (Var tyn) (Var valn)

10201025

10211026 -- Start filling in the scrutinee type, if we can work one

10221027 -- out from the case options

@@ -1047,13 +1052,15 @@ elab ist info emode opts fn tm

10471052 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

10481053

10491054 let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)

1050− (nub $ allNamesIn scr ++ inApp ptm ++

1055+ (nub $ scrnames ++ inApp ptm ++

10511056 inOpts)

1057+ let lin_used = getLinearUsed (tt_ctxt ist) ptm

10521058

10531059 let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args

10541060

1061+ -- trace (show lin_used ++ "\n" ++ show args ++ "\n" ++ show ptm) attack

10551062 attack

1056− cname' <- defer argsDropped (mkN (mkCaseName fc fn))

1063+ cname' <- defer argsDropped lin_used (mkN (mkCaseName fc fn))

10571064 solve

10581065

10591066 -- if the scrutinee is one of the 'args' in env, we should

@@ -1075,6 +1082,17 @@ elab ist info emode opts fn tm

10751082 xs@(_:_) -> sNS n xs

10761083 _ -> n

10771084

1085+ -- If any variables in the scrutinee are in the environment with

1086+ -- multiplicity other than RigW, let bind the scrutinee variable

1087+ -- with the smallest multiplicity

1088+ letrig ns [] = RigW

1089+ letrig ns env = letrig' Rig1 ns env

1090+

1091+ letrig' def ns [] = def

1092+ letrig' def ns ((n, r, _) : env)

1093+ | n `elem` ns = letrig' (rigMult def r) ns env

1094+ | otherwise = letrig' def ns env

1095+

10781096 getScrType [] = Nothing

10791097 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

10801098

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

10921110

10931111 inApp (P _ n _) = [n]

10941112 inApp (App _ f a) = inApp f ++ inApp a

1095− inApp (Bind n (Let _ v) sc) = inApp v ++ inApp sc

1113+ inApp (Bind n (Let _ _ v) sc) = inApp v ++ inApp sc

10961114 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

10971115 inApp (Bind n b sc) = inApp sc

10981116 inApp _ = []

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

11631181 -- Let-bind the result of elaborating the contained term, so that

11641182 -- the hole doesn't disappear

11651183 nTm <- getNameFrom (sMN 0 "quotedTerm")

1166− letbind nTm (Var qTy) (Var qTm)

1184+ letbind nTm RigW (Var qTy) (Var qTm)

11671185

11681186 -- Fill out the goal type, if relevant

11691187 case goalt of

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

12901308 -- In order to intercept the elaborated value, we need to

12911309 -- let-bind it.

12921310 attack

1293− letbind n g (Var n')

1311+ letbind n RigW g (Var n')

12941312 focus n'

12951313 elab' ina fc tm

12961314 env <- get_env

@@ -1319,8 +1337,10 @@ elab ist info emode opts fn tm

13191337 delayElab pri t

13201338 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

13211339

1340+ -- If the variable in the environment is the scrutinee of the case,

1341+ -- and has multiplicity W, keep it available

13221342 isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))

1323− isScr (PRef _ _ n) (n', _, b) = (n', (n == n', b))

1343+ isScr (PRef _ _ n) (n', RigW, b) = (n', (n == n', b))

13241344 isScr _ (n', _, b) = (n', (False, b))

13251345

13261346 caseBlock :: FC -> Name

@@ -1332,8 +1352,8 @@ elab ist info emode opts fn tm

13321352 map (mkClause args) opts

13331353

13341354 where -- Find the variable we want as the scrutinee and mark it as

1335− -- 'True'. If the scrutinee is in the environment, match on that

1336− -- otherwise match on the new argument we're adding.

1355+ -- 'True'. If the scrutinee is available in the environment,

1356+ -- match on that otherwise match on the new argument we're adding.

13371357 findScr ((n, (True, t)) : xs)

13381358 = (n, (True, t)) : scrName n xs

13391359 findScr [(n, (_, t))] = [(n, (True, t))]

@@ -1721,7 +1741,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

17211741 t' <- cd ((n, b) : env) t

17221742 return (Bind n b' t')

17231743 where

1724− cdb (Let t v) = liftM2 Let (cd env t) (cd env v)

1744+ cdb (Let rig t v) = liftM2 (Let rig) (cd env t) (cd env v)

17251745 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

17261746 cdb b = do ty' <- cd env (binderTy b)

17271747 return (b { binderTy = ty' })

@@ -1737,7 +1757,7 @@ case_ ind autoSolve ist fn tm = do

17371757 valn <- getNameFrom (sMN 0 "ival")

17381758 claim valn (Var tyn)

17391759 letn <- getNameFrom (sMN 0 "irule")

1740− letbind letn (Var tyn) (Var valn)

1760+ letbind letn RigW (Var tyn) (Var valn)

17411761 focus valn

17421762 elab ist toplevel ERHS [] (sMN 0 "tac") tm

17431763 env <- get_env

@@ -2115,7 +2135,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

21152135 n' <- reifyTTName n

21162136 ty' <- reifyRaw ty

21172137 tm' <- reifyRaw tm

2118− letbind n' ty' tm'

2138+ letbind n' RigW ty' tm'

21192139 returnUnit

21202140 | n == tacN "Prim__Compute"

21212141 = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit

@@ -2270,9 +2290,10 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

22702290 ptm <- get_term

22712291 -- See documentation above in the elab case for PMetavar

22722292 let unique_used = getUniqueUsed ctxt ptm

2293+ let lin_used = getLinearUsed ctxt ptm

22732294 let mvn = metavarName ns n'

22742295 attack

2275− defer unique_used mvn

2296+ defer unique_used lin_used mvn

22762297 solve

22772298 returnUnit

22782299 | n == tacN "Prim__Fixity"

@@ -2377,7 +2398,7 @@ runTac autoSolve ist perhapsFC fn tac

23772398 valn <- getNameFrom (sMN 0 "eqval")

23782399 claim valn (Var tyn)

23792400 letn <- getNameFrom (sMN 0 "equiv_val")

2380− letbind letn (Var tyn) (Var valn)

2401+ letbind letn RigW (Var tyn) (Var valn)

23812402 focus tyn

23822403 elab ist toplevel ERHS [] (sMN 0 "tac") tm

23832404 focus valn

@@ -2390,7 +2411,7 @@ runTac autoSolve ist perhapsFC fn tac

23902411 valn <- getNameFrom (sMN 0 "rval")

23912412 claim valn (Var tyn)

23922413 letn <- getNameFrom (sMN 0 "rewrite_rule")

2393− letbind letn (Var tyn) (Var valn)

2414+ letbind letn RigW (Var tyn) (Var valn)

23942415 focus valn

23952416 elab ist toplevel ERHS [] (sMN 0 "tac") tm

23962417 rewrite (Var letn)

@@ -2406,7 +2427,7 @@ runTac autoSolve ist perhapsFC fn tac

24062427 valn <- getNameFrom (sMN 0 "letval")

24072428 claim valn (Var tyn)

24082429 letn <- unique_hole n

2409− letbind letn (Var tyn) (Var valn)

2430+ letbind letn RigW (Var tyn) (Var valn)

24102431 focus valn

24112432 elab ist toplevel ERHS [] (sMN 0 "tac") tm

24122433 when autoSolve solveAll

@@ -2417,7 +2438,7 @@ runTac autoSolve ist perhapsFC fn tac

24172438 valn <- getNameFrom (sMN 0 "letval")

24182439 claim valn (Var tyn)

24192440 letn <- unique_hole n

2420− letbind letn (Var tyn) (Var valn)

2441+ letbind letn RigW (Var tyn) (Var valn)

24212442 focus tyn

24222443 elab ist toplevel ERHS [] (sMN 0 "tac") ty

24232444 focus valn

@@ -2443,7 +2464,7 @@ runTac autoSolve ist perhapsFC fn tac

24432464 script <- getNameFrom (sMN 0 "script")

24442465 claim script scriptTy

24452466 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2446− letbind scriptvar scriptTy (Var script)

2467+ letbind scriptvar RigW scriptTy (Var script)

24472468 focus script

24482469 elab ist toplevel ERHS [] (sMN 0 "tac") tm

24492470 (script', _) <- get_type_val (Var scriptvar)

@@ -2475,7 +2496,7 @@ runTac autoSolve ist perhapsFC fn tac

24752496 script <- getNameFrom (sMN 0 "script")

24762497 claim script scriptTy

24772498 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2478− letbind scriptvar scriptTy (Var script)

2499+ letbind scriptvar RigW scriptTy (Var script)

24792500 focus script

24802501 ptm <- get_term

24812502 env <- get_env

@@ -2506,7 +2527,7 @@ runTac autoSolve ist perhapsFC fn tac

25062527 valn <- getNameFrom (sMN 0 "letval")

25072528 claim valn (Var tyn)

25082529 letn <- getNameFrom (sMN 0 "letvar")

2509− letbind letn (Var tyn) (Var valn)

2530+ letbind letn RigW (Var tyn) (Var valn)

25102531 focus valn

25112532 elab ist toplevel ERHS [] (sMN 0 "tac") v

25122533 (value, _) <- get_type_val (Var letn)

@@ -2520,7 +2541,7 @@ runTac autoSolve ist perhapsFC fn tac

25202541 valn <- getNameFrom (sMN 0 "letval")

25212542 claim valn (Var tyn)

25222543 letn <- getNameFrom (sMN 0 "letvar")

2523− letbind letn (Var tyn) (Var valn)

2544+ letbind letn RigW (Var tyn) (Var valn)

25242545 focus valn

25252546 elab ist toplevel ERHS [] (sMN 0 "tac") v

25262547 (value, _) <- get_type_val (Var letn)

src/Idris/Elab/Type.hs−4

@@ -108,10 +108,6 @@ buildType info syn fc opts n ty' = do

108108 setFnInfo n fninfo

109109 addIBC (IBCFnInfo n fninfo)

110110

111− -- If we use any types with linear constructor arguments, we'd better

112− -- make sure they are use-once

113− tcliftAt fc $ linearCheck ctxt (whnfArgs ctxt [] cty)

114−

115111 return (cty, ckind, ty, inacc)

116112 where

117113 patToImp (Bind n (PVar rig t) sc) = Bind n (Pi rig Nothing t (TType (UVar [] 0))) (patToImp sc)

src/Idris/Elab/Utils.hs+74−20

@@ -26,6 +26,7 @@ import Control.Monad.State

2626import Data.List

2727import qualified Data.Map as Map

2828import Data.Maybe

29+import Debug.Trace

2930

3031recheckC = recheckC_borrowing False True []

3132

@@ -286,6 +287,40 @@ paramNames args env (p : ps)

286287 _ -> paramNames args env ps

287288 | otherwise = paramNames args env ps

288289

290+-- Get all the names with multiplicity '1' used in a partial proof term

291+getLinearUsed :: Context -> Term -> [Name]

292+getLinearUsed ctxt tm = execState (getLin [] [] tm) []

293+ where

294+ getLin :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

295+ getLin env us (Bind n b sc)

296+ = do getLinB env us b

297+ let r = getRig b

298+ let lin = case r of

299+ Rig1 -> True

300+ _ -> False

301+ getLin ((n, getRig b, b) : env) ((n, lin) : us) sc

302+ getLin env us (App _ f a) = do getLin env us f; getLin env us a

303+ getLin env us (V i)

304+ | i < length us = if snd (us!!i) then use (fst (us!!1)) else return ()

305+ getLin env us (P _ n _)

306+ | Just u <- lookup n us = if u then use n else return ()

307+ getLin env us _ = return ()

308+

309+ getLinB env us (Let Rig0 t v) = return ()

310+ getLinB env us (Let rig t v) = getLin env us v

311+ getLinB env us (Guess t v) = getLin env us v

312+ getLinB env us (NLet t v) = getLin env us v

313+ getLinB env us b = return ()

314+

315+ use n = do ns <- get; put (n : ns)

316+

317+ getRig :: Binder Term -> RigCount

318+ getRig (Pi rig _ _ _) = rig

319+ getRig (PVar rig _) = rig

320+ getRig (Lam rig _) = rig

321+ getRig (Let rig _ _) = rig

322+ getRig _ = RigW

323+

289324getUniqueUsed :: Context -> Term -> [Name]

290325getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

291326 where

@@ -307,7 +342,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

307342

308343 use n = do ns <- get; put (n : ns)

309344

310− getUniqB env us (Let t v) = getUniq env us v

345+ getUniqB env us (Let rig t v) = getUniq env us v

311346 getUniqB env us (Guess t v) = getUniq env us v

312347-- getUniqB env us (Pi _ _ t v) = do getUniq env us t; getUniq env us v

313348 getUniqB env us (NLet t v) = getUniq env us v

@@ -523,10 +558,10 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

523558 v' <- getPats v

524559 sc' <- getPats sc

525560 return (Bind n (Guess t' v') sc')

526− getPats (Bind n (Let t v) sc) = do t' <- getPats t

527− v' <- getPats v

528− sc' <- getPats sc

529− return (Bind n (Let t' v') sc')

561+ getPats (Bind n (Let rig t v) sc) = do t' <- getPats t

562+ v' <- getPats v

563+ sc' <- getPats sc

564+ return (Bind n (Let rig t' v') sc')

530565 getPats (Bind n (Pi rig i t k) sc) = do t' <- getPats t

531566 k' <- getPats k

532567 sc' <- getPats sc

@@ -574,24 +609,43 @@ hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

574609 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

575610hasEmptyPat ctxt tyctxt _ = False

576611

577−-- Find names which are applied to a function in a Rig1 position

578−findLinear :: IState -> [Name] -> Term -> [(Name, RigCount)]

579−findLinear ist env tm | (P _ f _, args) <- unApply tm,

580− f `notElem` env,

581− Just ty_in <- lookupTyExact f (tt_ctxt ist)

612+-- Find names which are applied to a function in a Rig1/Rig0 position

613+-- 'rig' is the multiplicity of the outer argument. When we go under a

614+-- function application, multiply them (it only needs to be Rig1 if it's

615+-- a linear argument to a linear argument; it needs to be a Rig0 if it's

616+-- Rig0 at any level)

617+findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]

618+findLinear rig ist env tm

619+ | (P _ f _, args) <- unApply tm,

620+ f `notElem` env,

621+ Just ty_in <- lookupTyExact f (tt_ctxt ist)

582622 = let ty = whnfArgs (tt_ctxt ist) [] ty_in in

583− nub $ concatMap (findLinear ist env) args ++ findLinArg ty args

623+ combineRig $ findLinArg ty args

584624 where

585625 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

586− | Rig0 <- c = (a, c) : findLinArg sc as

587− | Rig1 <- c = (a, c) : findLinArg sc as

588− findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)

589− = findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

590− findLinArg _ _ = []

591−findLinear ist env (App _ f a)

592− = nub $ findLinear ist env f ++ findLinear ist env a

593−findLinear ist env (Bind n b sc) = findLinear ist (n : env) sc

594−findLinear ist _ _ = []

626+ = (a, rigMult rig c) : findLinArg sc as

627+ findLinArg (Bind n (Pi c _ _ _) sc) (a : as)

628+ = findLinear (rigMult c rig) ist env a ++

629+ findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

630+ findLinArg ty (a : as)

631+ = findLinear rig ist env a ++ findLinArg ty as

632+ findLinArg _ [] = []

633+

634+ -- If a name is used multiple times in a pattern, take the least restrictive

635+ -- use of it

636+ combineRig [] = []

637+ combineRig ((n, r) : rs)

638+ = let (rs', rig) = findRestrictive n r [] rs in

639+ (n, rig) : combineRig rs'

640+ findRestrictive n r acc [] = (acc, r)

641+ findRestrictive n r acc ((n', r') : rs)

642+ | n == n' = findRestrictive n (max r r') acc rs

643+ | otherwise = findRestrictive n r ((n', r') : acc) rs

644+

645+findLinear rig ist env (App _ f a)

646+ = nub $ findLinear rig ist env f ++ findLinear rig ist env a

647+findLinear rig ist env (Bind n b sc) = findLinear rig ist (n : env) sc

648+findLinear rig ist _ _ = []

595649

596650setLinear :: [(Name, RigCount)] -> Term -> Term

597651setLinear ns (Bind n b@(PVar r t) sc)

src/Idris/ElabDecls.hs+4

@@ -61,7 +61,11 @@ elabPrims = do i <- getIState

6161 let mkdec opt decl docs argdocs =

6262 PData docs argdocs defaultSyntax (fileFC "builtin")

6363 opt decl

64+ -- need to temporarily add linearity for this since the

65+ -- argument may be of restricted type

66+ addLangExt LinearTypes

6467 elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

68+ dropLangExt LinearTypes

6569 -- We don't want the constraints generated by 'Infer' since

6670 -- it's only scaffolding for the elaborator

6771 i <- getIState

src/Idris/Erasure.hs+3−3

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

476476

477477 -- let-bound variables can get partially evaluated

478478 -- it is sufficient just to plug the Cond in when the bound names are used

479− | Let ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body

479+ | Let rig ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body

480480 | NLet ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body

481481 where

482482 var t cd = getDepsTerm vs bs cd t

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

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

530530

531531 -- and we interpret applied lets as lambdas

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

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

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

534534

535535 Proj t i

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

609609 (f, args) = unApply tm

610610

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

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

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

613613 lamToLet' [] tm = tm

614614 lamToLet' vs tm = error $

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

src/Idris/Error.hs+2−2

@@ -100,7 +100,7 @@ warnDisamb ist (PInferRef _ _ _) = return ()

100100warnDisamb ist (PPatvar _ _) = return ()

101101warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

102102warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

103−warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b

103+warnDisamb ist (PLet _ _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b

104104warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t

105105warnDisamb ist (PApp _ t args) = warnDisamb ist t >>

106106 mapM_ (warnDisamb ist . getTm) args

@@ -129,7 +129,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

129129 wStep (DoBind _ _ _ x) = warnDisamb ist x

130130 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

131131 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

132− wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

132+ wStep (DoLet _ _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

133133 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

134134 wStep (DoRewrite _ h) = warnDisamb ist h

135135warnDisamb ist (PIdiom _ x) = warnDisamb ist x

src/Idris/IBC.hs+18−6

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

4040import System.FilePath

4141

4242ibcVersion :: Word16

43−ibcVersion = 163

43+ibcVersion = 164

4444

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

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

@@ -100,6 +100,7 @@ data IBCFile = IBCFile {

100100 , ibc_access :: ![(Name, Accessibility)]

101101 , ibc_fragile :: ![(Name, String)]

102102 , ibc_constraints :: ![(FC, UConstraint)]

103+ , ibc_langexts :: ![LanguageExt]

103104 }

104105 deriving Show

105106{-!

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

107108!-}

108109

109110initIBC :: IBCFile

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

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

111112

112113hasValidIBCVersion :: FilePath -> Idris Bool

113114hasValidIBCVersion fp = do

@@ -206,7 +207,8 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

206207 makeEntry "ibc_total" (ibc_total i),

207208 makeEntry "ibc_injective" (ibc_injective i),

208209 makeEntry "ibc_access" (ibc_access i),

209− makeEntry "ibc_fragile" (ibc_fragile i)]

210+ makeEntry "ibc_fragile" (ibc_fragile i),

211+ makeEntry "ibc_langexts" (ibc_langexts i)]

210212-- TODO: Put this back in shortly after minimising/pruning constraints

211213-- makeEntry "ibc_constraints" (ibc_constraints i)]

212214

@@ -221,7 +223,8 @@ writeIBC src f

221223 iReport 2 $ "Writing IBC for: " ++ show f

222224 i <- getIState

223225 resetNameIdx

224− ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

226+ ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src,

227+ ibc_langexts = idris_language_extensions i })

225228 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

226229 writeArchive f ibcf

227230 logIBC 2 "Written")

@@ -238,7 +241,8 @@ writePkgIndex f

238241 logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++

239242 show (map snd imps)

240243 resetNameIdx

241− let ibcf = initIBC { ibc_imports = imps }

244+ let ibcf = initIBC { ibc_imports = imps,

245+ ibc_langexts = idris_language_extensions i }

242246 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

243247 writeArchive f ibcf

244248 logIBC 2 "Written")

@@ -430,6 +434,7 @@ process reexp phase archive fn = do

430434 processAccess reexp phase archive

431435 processFragile archive

432436 processConstraints archive

437+ processLangExts phase archive

433438

434439timestampOlder :: FilePath -> FilePath -> Idris ()

435440timestampOlder src ibc = do

@@ -705,7 +710,7 @@ processDefs ar = do

705710 sc' <- update sc

706711 return $ Bind n b' sc'

707712 where

708− updateB (Let t v) = liftM2 Let (update' t) (update' v)

713+ updateB (Let rig t v) = liftM2 (Let rig) (update' t) (update' v)

709714 updateB b = do

710715 ty' <- update' (binderTy b)

711716 return (b { binderTy = ty' })

@@ -833,6 +838,13 @@ processMetaVars ar = do

833838 ns <- getEntry [] "ibc_metavars" ar

834839 updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

835840

841+-- We only want the language extensions when reading the top level thing

842+processLangExts :: IBCPhase -> Archive -> Idris ()

843+processLangExts (IBC_REPL True) ar

844+ = do ds <- getEntry [] "ibc_langexts" ar

845+ mapM_ addLangExt ds

846+processLangExts _ _ = return ()

847+

836848----- For Cheapskate and docstrings

837849

838850instance Binary a => Binary (D.Docstring a)

src/Idris/IdrisDoc.hs+2−2

@@ -279,7 +279,7 @@ extractPTermNames (PInferRef _ _ n) = [n]

279279extractPTermNames (PPatvar _ n) = [n]

280280extractPTermNames (PLam _ n _ p1 p2) = n : concatMap extract [p1, p2]

281281extractPTermNames (PPi _ n _ p1 p2) = n : concatMap extract [p1, p2]

282−extractPTermNames (PLet _ n _ p1 p2 p3) = n : concatMap extract [p1, p2, p3]

282+extractPTermNames (PLet _ _ n _ p1 p2 p3) = n : concatMap extract [p1, p2, p3]

283283extractPTermNames (PTyped p1 p2) = concatMap extract [p1, p2]

284284extractPTermNames (PApp _ p pas) = let names = concatMap extractPArg pas

285285 in (extract p) ++ names

@@ -330,7 +330,7 @@ extractPDo (DoBind _ n _ p) = n : extract p

330330extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

331331 ps' = ps1 ++ ps2

332332 in concatMap extract (p1 : p2 : ps')

333−extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]

333+extractPDo (DoLet _ _ n _ p1 p2) = n : concatMap extract [p1, p2]

334334extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

335335extractPDo (DoRewrite _ p) = extract p

336336

src/Idris/Inliner.hs+1−1

@@ -29,7 +29,7 @@ inlineTerm ist tm = inl tm where

2929 inl orig@(P _ n _) = inlApp n [] orig

3030 inl orig@(App _ f a)

3131 | (P _ fn _, args) <- unApply orig = inlApp fn args orig

32− inl (Bind n (Let t v) sc) = Bind n (Let t (inl v)) (inl sc)

32+ inl (Bind n (Let rc t v) sc) = Bind n (Let rc t (inl v)) (inl sc)

3333 inl (Bind n b sc) = Bind n b (inl sc)

3434 inl tm = tm

3535

src/Idris/Interactive.hs+1−1

@@ -261,7 +261,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

261261 else iPrintResult newmv

262262 where dropCtxt 0 sc = sc

263263 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc

264− dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc

264+ dropCtxt i (PLet _ _ _ _ _ _ sc) = dropCtxt (i - 1) sc

265265 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc

266266 dropCtxt _ t = t

267267

src/Idris/Main.hs+2−2

@@ -157,10 +157,10 @@ idrisMain opts =

157157

158158 mapM_ addPkgDir pkgdirs

159159 elabPrims

160− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL True)

160+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins" (IBC_REPL False)

161161 addAutoImport "Builtins"

162162 return ()

163− when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL True)

163+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude" (IBC_REPL False)

164164 addAutoImport "Prelude"

165165 return ()

166166 when (runrepl && not idesl) initScript

src/Idris/Parser.hs+6−6

@@ -501,8 +501,8 @@ syntaxRule syn

501501 n' <- gensym n

502502 body' <- fixBind 0 ((n,n'):rens) body

503503 return $ (PPi plic n' nfc ty' body')

504− fixBind 0 rens (PLet fc n nfc ty val body)

505− | n `elem` userNames = liftM3 (PLet fc n nfc)

504+ fixBind 0 rens (PLet fc rig n nfc ty val body)

505+ | n `elem` userNames = liftM3 (PLet fc rig n nfc)

506506 (fixBind 0 rens ty)

507507 (fixBind 0 rens val)

508508 (fixBind 0 rens body)

@@ -511,7 +511,7 @@ syntaxRule syn

511511 val' <- fixBind 0 rens val

512512 n' <- gensym n

513513 body' <- fixBind 0 ((n,n'):rens) body

514− return $ PLet fc n' nfc ty' val' body'

514+ return $ PLet fc rig n' nfc ty' val' body'

515515 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =

516516 return $ PMatchApp fc n'

517517 -- Also rename resolved quotations, to allow syntax rules to

@@ -1104,10 +1104,10 @@ rhs syn n = do lchar '='

11041104 n' :: Name

11051105 n' = mkN n

11061106 addLet :: FC -> Name -> PTerm -> PTerm

1107− addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)

1107+ addLet fc nm (PLet fc' rig n nfc ty val r) = PLet fc' rig n nfc ty val (addLet fc nm r)

11081108 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)

11091109 where addLetC (l, r) = (l, addLet fc nm r)

1110− addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))

1110+ addLet fc nm r = (PLet fc RigW (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))

11111111

11121112{-|Parses a function clause

11131113

@@ -1171,7 +1171,7 @@ clause syn

11711171 return x,

11721172 do terminator

11731173 return ([], [])]

1174− let capp = PLet fc (sMN 0 "match") NoFC

1174+ let capp = PLet fc RigW (sMN 0 "match") NoFC

11751175 ty

11761176 (PMatchApp fc n)

11771177 (PRef fc [] (sMN 0 "match"))

src/Idris/Parser/Expr.hs+6−6

@@ -190,9 +190,9 @@ updateSynMatch = update

190190 = let (n', nfc') = updateB ns (n, fc)

191191 in PPi (updTacImp ns p) n' nfc'

192192 (update ns ty) (update (dropn n ns) sc)

193− update ns (PLet fc n nfc ty val sc)

193+ update ns (PLet fc rc n nfc ty val sc)

194194 = let (n', nfc') = updateB ns (n, nfc)

195− in PLet fc n' nfc' (update ns ty)

195+ in PLet fc rc n' nfc' (update ns ty)

196196 (update ns val) (update (dropn n ns) sc)

197197 update ns (PApp fc t args)

198198 = PApp fc (update ns t) (map (fmap (update ns)) args)

@@ -217,7 +217,7 @@ updateSynMatch = update

217217 where upd :: [(Name, SynMatch)] -> PDo -> PDo

218218 upd ns (DoExp fc t) = DoExp fc (update ns t)

219219 upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)

220− upd ns (DoLet fc n nfc ty t) = DoLet fc n nfc (update ns ty) (update ns t)

220+ upd ns (DoLet fc rc n nfc ty t) = DoLet fc rc n nfc (update ns ty) (update ns t)

221221 upd ns (DoBindP fc i t ts)

222222 = DoBindP fc (update ns i) (update ns t)

223223 (map (\(l,r) -> (update ns l, update ns r)) ts)

@@ -669,7 +669,7 @@ app syn = do f <- simpleExpr syn

669669 (do try $ reservedOp "<=="

670670 fc <- getFC

671671 ff <- fst <$> fnName

672− return (PLet fc (sMN 0 "match") NoFC

672+ return (PLet fc RigW (sMN 0 "match") NoFC

673673 f

674674 (PMatchApp fc ff)

675675 (PRef fc [] (sMN 0 "match")))

@@ -995,7 +995,7 @@ let_ syn = try (do kw <- reservedFC "let"

995995 <?> "let binding"

996996 where buildLets [] sc = sc

997997 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

998− = PLet fc n nfc ty v (buildLets ls sc)

998+ = PLet fc RigW n nfc ty v (buildLets ls sc)

999999 buildLets ((fc, pat, ty, v, alts) : ls) sc

10001000 = PCase fc v ((pat, buildLets ls sc) : alts)

10011001

@@ -1349,7 +1349,7 @@ do_ syn

13491349 fc <- getFC

13501350 e <- expr syn

13511351 highlightP kw AnnKeyword

1352− return (DoLet fc i ifc ty e))

1352+ return (DoLet fc RigW i ifc ty e))

13531353 <|> try (do kw <- reservedFC "let"

13541354 i <- expr' syn

13551355 reservedOp "="

src/Idris/PartialEval.hs+7−7

@@ -94,12 +94,12 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

9494 where

9595 -- Specialise static argument in type by let-binding provided value instead

9696 -- of expecting it as a function argument

97− st ((ExplicitS, v) : xs) (Bind n (Pi _ _ t _) sc)

98− = Bind n (Let t v) (st xs sc)

99− st ((ImplicitS _, v) : xs) (Bind n (Pi _ _ t _) sc)

100− = Bind n (Let t v) (st xs sc)

101− st ((ConstraintS, v) : xs) (Bind n (Pi _ _ t _) sc)

102− = Bind n (Let t v) (st xs sc)

97+ st ((ExplicitS, v) : xs) (Bind n (Pi rc _ t _) sc)

98+ = Bind n (Let rc t v) (st xs sc)

99+ st ((ImplicitS _, v) : xs) (Bind n (Pi rc _ t _) sc)

100+ = Bind n (Let rc t v) (st xs sc)

101+ st ((ConstraintS, v) : xs) (Bind n (Pi rc _ t _) sc)

102+ = Bind n (Let rc t v) (st xs sc)

103103 -- Erase argument from function type

104104 st ((UnifiedD, _) : xs) (Bind n (Pi _ _ t _) sc)

105105 = st xs sc

@@ -364,7 +364,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

364364-- _ -> []

365365 else []

366366 _ -> []

367− ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc

367+ ga env (Bind n (Let rc t v) sc) = ga env v ++ ga (n : env) sc

368368 ga env (Bind n t sc) = ga (n : env) sc

369369 ga env t = []

370370

src/Idris/ProofSearch.hs+4−4

@@ -139,7 +139,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]

139139 where

140140 -- if nothing worked, make a new metavariable

141141 tryAllFns [] | fromProver = cantSolveGoal

142− tryAllFns [] = do attack; defer [] nroot; solve

142+ tryAllFns [] = do attack; defer [] [] nroot; solve

143143 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

144144

145145 tryFn (f, args) = do let imps = map isImp args

@@ -155,7 +155,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]

155155 if fromProver then cantSolveGoal

156156 else do

157157 mapM_ (\ h -> do focus h

158− attack; defer [] nroot; solve)

158+ attack; defer [] [] nroot; solve)

159159 (hs' \\ hs)

160160-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

161161 solve

@@ -242,7 +242,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

242242 -- that's no use)

243243 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()

244244 psRec _ 0 locs tys | fromProver = cantSolveGoal

245− psRec rec 0 locs tys = do attack; defer [] nroot; solve --fail "Maximum depth reached"

245+ psRec rec 0 locs tys = do attack; defer [] [] nroot; solve --fail "Maximum depth reached"

246246 psRec False d locs tys = tryCons d locs tys hints

247247 psRec True d locs tys

248248 = do compute

@@ -258,7 +258,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

258258 -- if all else fails, make a new metavariable

259259 (if fromProver

260260 then fail "cantSolveGoal"

261− else do attack; defer [] nroot; solve) True) True

261+ else do attack; defer [] [] nroot; solve) True) True

262262

263263 -- get recursive function name. Only user given names make sense.

264264 getFn d (Just f) | d < maxDepth-1 && usersname f = [f]

src/Idris/Prover.hs+4−4

@@ -181,7 +181,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

181181 | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs

182182 prettyPs all g bnd ((n@(MN _ _), _, _) : bs)

183183 | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs

184− prettyPs all g bnd ((n, _, Let t v) : bs) =

184+ prettyPs all g bnd ((n, _, Let rig t v) : bs) =

185185 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

186186 align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs

187187 prettyPs all g bnd ((n, _, b) : bs) =

@@ -350,13 +350,13 @@ elabloop info fn d prompt prf e prev h env

350350 DoLetP {} -> ifail "Pattern-matching let not supported here"

351351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

352352 DoBindP {} -> ifail "Pattern-matching <- not supported here"

353− DoLet fc i ifc Placeholder expr ->

353+ DoLet fc rig i ifc Placeholder expr ->

354354 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

355355 ctxt <- getContext

356356 let tm' = normaliseAll ctxt [] tm

357357 ty' = normaliseAll ctxt [] ty

358358 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

359− DoLet fc i ifc ty expr ->

359+ DoLet fc rig i ifc ty expr ->

360360 do (tm, ty) <- elabVal (recinfo proverfc) ERHS

361361 (PApp NoFC (PRef NoFC [] (sUN "the"))

362362 [ pexp (inLets ist env ty)

@@ -402,7 +402,7 @@ elabloop info fn d prompt prf e prev h env

402402 -- the elaborator with a custom environment here to avoid the

403403 -- delab step.

404404 inLets :: IState -> [(Name, Type, Term)] -> PTerm -> PTerm

405− inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)

405+ inLets ist lets tm = foldr (\(n, ty, v) b -> PLet NoFC RigW n NoFC (delab ist ty) (delab ist v) b) tm (reverse lets)

406406

407407

408408

src/Idris/REPL.hs+8−2

@@ -994,11 +994,12 @@ process fn (Check (PRef _ _ n))

994994 putTy ppo ist i [] (delab ist (errReverse ist ty'))

995995 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

996996 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

997− putTy ppo ist i bnd (PPi _ n _ t sc)

997+ putTy ppo ist i bnd (PPi p n _ t sc)

998998 = let current = case n of

999999 MN _ _ -> text ""

10001000 UN nm | ('_':'_':_) <- str nm -> text ""

1001− _ -> text " " <>

1001+ _ -> countOf (pcount p)

1002+ (LinearTypes `elem` idris_language_extensions ist) <+>

10021003 bindingOf n False

10031004 <+> colon

10041005 <+> align (tPretty bnd ist t)

@@ -1011,6 +1012,11 @@ process fn (Check (PRef _ _ n))

10111012 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

10121013 align (tPretty bnd ist g)

10131014

1015+ -- Only display count if linear types extension is enabled

1016+ countOf Rig0 True = text "0"

1017+ countOf Rig1 True = text "1"

1018+ countOf _ _ = text " "

1019+

10141020 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

10151021

10161022

src/Idris/Reflection.hs+6−6

@@ -313,7 +313,7 @@ reifyTTBinderApp reif f [t]

313313reifyTTBinderApp reif f [t, k]

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

315315reifyTTBinderApp reif f [x, y]

316− | f == reflm "Let" = liftM2 Let (reif x) (reif y)

316+ | f == reflm "Let" = liftM2 (Let RigW) (reif x) (reif y)

317317reifyTTBinderApp reif f [t]

318318 | f == reflm "Hole" = liftM Hole (reif t)

319319reifyTTBinderApp reif f [t]

@@ -533,9 +533,9 @@ reflectRawQuotePattern unq (RBind n b sc) =

533533 focus scH; reflectRawQuotePattern unq sc

534534 focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b

535535 where freeNamesR (Var n) = [n]

536− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

537− freeNamesR body \\ [n],

538− freeNamesR t]

536+ freeNamesR (RBind n (Let rc t v) body) = concat [freeNamesR v,

537+ freeNamesR body \\ [n],

538+ freeNamesR t]

539539 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

540540 (freeNamesR body \\ [n])

541541 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

@@ -583,7 +583,7 @@ reflectBinderQuotePattern q ty unq (Pi _ _ t k)

583583 fill $ reflCall "Pi" [ty, Var t', Var k']

584584 solve

585585 focus t'; q unq t

586−reflectBinderQuotePattern q ty unq (Let x y)

586+reflectBinderQuotePattern q ty unq (Let rc x y)

587587 = do x' <- claimTy (sMN 0 "ty") ty; movelast x';

588588 y' <- claimTy (sMN 0 "v")ty; movelast y';

589589 fill $ reflCall "Let" [ty, Var x', Var y']

@@ -748,7 +748,7 @@ reflectBinderQuote q ty unq (Lam _ t)

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

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

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

751−reflectBinderQuote q ty unq (Let x y)

751+reflectBinderQuote q ty unq (Let rc x y)

752752 = reflCall "Let" [Var ty, q unq x, q unq y]

753753reflectBinderQuote q ty unq (NLet x y)

754754 = reflCall "Let" [Var ty, q unq x, q unq y]

src/Idris/Termination.hs+2−2

@@ -77,7 +77,7 @@ checkIfGuarded n

7777 allGuarded names i _ = True

7878

7979 guardedTerm names i (P _ v _) = v `elem` names || guard v i

80− guardedTerm names i (Bind n (Let t v) sc)

80+ guardedTerm names i (Bind n (Let rig t v) sc)

8181 = guardedTerm names i v && guardedTerm names i sc

8282 guardedTerm names i (Bind n b sc) = False

8383 guardedTerm names i ap@(App _ _ _)

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

364364 notPartial _ = True

365365 findCalls cases guarded (App _ f a) pvs pargs

366366 = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

367− findCalls cases guarded (Bind n (Let t v) e) pvs pargs

367+ findCalls cases guarded (Bind n (Let rig t v) e) pvs pargs

368368 = findCalls cases Unguarded t pvs pargs ++

369369 findCalls cases Unguarded v pvs pargs ++

370370 -- Substitute in the scope since this might reveal some useful

src/Idris/TypeSearch.hs+1−1

@@ -153,7 +153,7 @@ usedVars :: Ord n => TT n -> Map n (TT n, Bool)

153153usedVars = f True where

154154 f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t

155155 f b (Bind n binder t2) = (M.delete n (f b t2) `M.union`) $ case binder of

156− Let t v -> f b t `M.union` f b v

156+ Let rig t v -> f b t `M.union` f b v

157157 Guess t v -> f b t `M.union` f b v

158158 bind -> f b (binderTy bind)

159159 f b (App _ t1 t2) = f b t1 `M.union` f (b && isInjective t1) t2

src/Idris/WhoCalls.hs+2−2

@@ -31,12 +31,12 @@ names (Proj t _) = names t

3131names _ = []

3232

3333occursBinder :: Name -> Binder Term -> Bool

34−occursBinder n (Let ty val) = occurs n ty || occurs n val

34+occursBinder n (Let rc ty val) = occurs n ty || occurs n val

3535occursBinder n (NLet ty val) = occurs n ty || occurs n val

3636occursBinder n b = occurs n (binderTy b)

3737

3838namesBinder :: Binder Term -> [Name]

39−namesBinder (Let ty val) = names ty ++ names val

39+namesBinder (Let rc ty val) = names ty ++ names val

4040namesBinder (NLet ty val) = names ty ++ names val

4141namesBinder b = names (binderTy b)

4242