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

CHANGELOG.md+3−1

compare with master

unifiedsplit

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

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

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

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

9

11

10## Library Updates

12## Library Updates

11

13

libs/prelude/Builtins.idr+2−1

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

3%access public export

4%default total

5%language UniquenessTypes

6+%language LinearTypes

6

7

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

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

8||| true proposition.

9||| true proposition.

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

18 ||| A pair of elements

19 ||| A pair of elements

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

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

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

21 ||| @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

22

23

23 -- Usage hints for erasure analysis

24 -- Usage hints for erasure analysis

24 %used MkPair a

25 %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

478 where

479 n' = uniqueName n env

480

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

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

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

483

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

src/IRTS/Portable.hs+1−1

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

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

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

322 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)]

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

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

326 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

143 idris_language_extensions = e : idris_language_extensions i

144 }

145

146+dropLangExt :: LanguageExt -> Idris ()

147+dropLangExt e = do i <- getIState

148+ putIState $ i {

149+ idris_language_extensions = idris_language_extensions i \\ [e]

150+ }

151+

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1289 = let n' = mkShadow n in

1295 = let n' = mkShadow n in

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

1296+ PLet fc rc 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)

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

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

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

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

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

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

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

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

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

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

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

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

1931 PLam fc n nfc ty' sc'

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

1933 = if canBeDConName n (tt_ctxt ist)

1939 = if canBeDConName n (tt_ctxt ist)

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

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

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

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

1936 val' = ai inpat qq env ds val

1942 val' = ai inpat qq env ds val

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

1943 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'

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

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

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

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

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

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

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

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

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

2346 ms <- match' s s'

2352 ms <- match' s s'

2347 return (mt ++ ms)

2353 return (mt ++ ms)

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

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

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

2349− mty <- match' ty ty'

2356+ mty <- match' ty ty'

2350− ms <- match' s s'

2357+ ms <- match' s s'

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

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

2352 match (PHidden x) (PHidden y)

2359 match (PHidden x) (PHidden y)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2415 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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

2507 ty' <- mkUniq 0 nmap ty

2514 ty' <- mkUniq 0 nmap ty

2508 sc'' <- mkUniq 0 nmap' sc'

2515 sc'' <- mkUniq 0 nmap' sc'

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

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

2511 = do env <- get

2518 = do env <- get

2512 (n', sc') <-

2519 (n', sc') <-

2513 if n `S.member` env

2520 if n `S.member` env

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

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

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

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

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

2521 sc'' <- mkUniq 0 nmap' sc'

2528 sc'' <- mkUniq 0 nmap' sc'

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

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

2523 mkUniq 0 nmap (PApp fc t args)

2530 mkUniq 0 nmap (PApp fc t args)

2524 = do t' <- mkUniq 0 nmap t

2531 = do t' <- mkUniq 0 nmap t

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

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

src/Idris/AbsSyntaxTree.hs+28−18

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

146 , ppopt_desugarnats :: Bool

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

148 , ppopt_depth :: Maybe Int

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

149 } deriving (Show)

150 } deriving (Show)

150

151

152

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

160 , ppopt_desugarnats = False

161 , ppopt_desugarnats = False

161 , ppopt_pinames = False

162 , ppopt_pinames = False

162 , ppopt_depth = Nothing

163 , ppopt_depth = Nothing

164+ , ppopt_displayrig = False

163 }

165 }

164

166

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

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

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

169 , ppopt_desugarnats = True

171 , ppopt_desugarnats = True

170 , ppopt_pinames = True

172 , ppopt_pinames = True

171 , ppopt_depth = Nothing

173 , ppopt_depth = Nothing

174+ , ppopt_displayrig = False

172 }

175 }

173

176

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

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

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

178 , ppopt_pinames = False

181 , ppopt_pinames = False

179 , ppopt_depth = opt_printdepth opt

182 , ppopt_depth = opt_printdepth opt

180 , ppopt_desugarnats = opt_desugarnats opt

183 , ppopt_desugarnats = opt_desugarnats opt

184+ , ppopt_displayrig = False

181 }

185 }

182

186

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

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

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

529expl = Exp [] Dynamic False RigW

533expl = Exp [] Dynamic False RigW

530expl_param :: Plicity

534expl_param :: Plicity

531expl_param = Exp [] Dynamic True RigW

535expl_param = Exp [] Dynamic True RigW

536+expl_linear :: Plicity

537+expl_linear = Exp [] Dynamic False Rig1

532

538

533constraint :: Plicity

539constraint :: Plicity

534constraint = Constraint [] Static RigW

540constraint = Constraint [] Static RigW

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

949 | PPatvar FC Name -- ^ A pattern variable

955 | PPatvar FC Name -- ^ A pattern variable

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1027mapPTermFC 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)

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

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

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

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

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

1031mapPTermFC 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)

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

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

1047 mapPDoFC (DoBindP fc t1 t2 alts) =

1053 mapPDoFC (DoBindP fc t1 t2 alts) =

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

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

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

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

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

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

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

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

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

1073mapPT f t = f (mpt t) where

1079mapPT f t = f (mpt t) where

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

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

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

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

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

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

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

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

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

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

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

1171data PDo' t = DoExp FC t

1177data PDo' t = DoExp FC t

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

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

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

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

1175 | DoLetP FC t t

1181 | DoLetP FC t t

1176 | DoRewrite FC t -- rewrite in do block

1182 | DoRewrite FC t -- rewrite in do block

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

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

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

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

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

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

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

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

1191 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

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

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

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

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

1189

1195

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

1248highestFC (PPatvar fc _) = Just fc

1254highestFC (PPatvar fc _) = Just fc

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

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

1250highestFC (PPi _ _ _ _ _) = Nothing

1256highestFC (PPi _ _ _ _ _) = Nothing

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

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

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

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

1253highestFC (PApp fc _ _) = Just fc

1259highestFC (PApp fc _ _) = Just fc

1254highestFC (PAppBind fc _ _) = Just fc

1260highestFC (PAppBind fc _ _) = Just fc

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

1279 getDoFC (DoExp fc t) = fc

1285 getDoFC (DoExp fc t) = fc

1280 getDoFC (DoBind fc nm nfc t) = fc

1286 getDoFC (DoBind fc nm nfc t) = fc

1281 getDoFC (DoBindP fc l r alts) = fc

1287 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

1283 getDoFC (DoLetP fc l r) = fc

1289 getDoFC (DoLetP fc l r) = fc

1284 getDoFC (DoRewrite fc h) = fc

1290 getDoFC (DoRewrite fc h) = fc

1285

1291

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

1504inferDecl = PDatadecl inferTy primfc

1510inferDecl = PDatadecl inferTy primfc

1505 (PType bi)

1511 (PType bi)

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

1512 [(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"))

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

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

1509inferOpts = []

1515inferOpts = []

1510

1516

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

1673

1679

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

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

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

1681prettyIst :: 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

1677

1687

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

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

1679-- with infix info.

1689-- with infix info.

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

1709 prettyBindingsOf [n] t = prettyBindingOf n t

1719 prettyBindingsOf [n] t = prettyBindingOf n t

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

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

1711 prettyBindingsOf ns t

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

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

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

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

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

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

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

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

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

1717− | Rig0 <- rig =

1727+ | Rig0 <- rig, ppopt_displayrig ppo =

1718 depth d . bracket p startPrec . group $

1728 depth d . bracket p startPrec . group $

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

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

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

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

1721− | Rig1 <- rig =

1731+ | Rig1 <- rig, ppopt_displayrig ppo =

1722 depth d . bracket p startPrec . group $

1732 depth d . bracket p startPrec . group $

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

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

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

1734 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

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

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

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

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

1948 ppdo bnd dos

1958 ppdo bnd dos

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

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

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

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

1951 (if ty /= Placeholder

1961 (if ty /= Placeholder

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

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

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

2234 size (PRef fc _ name) = size name

2244 size (PRef fc _ name) = size name

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

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

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

2246 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

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

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

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

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

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

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

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

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

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

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

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

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

2292 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

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

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

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

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

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

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

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

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

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

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

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

2323 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

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

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

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

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

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

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

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

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

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

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

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

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

2387 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;

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

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

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

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

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

2391 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

75instance Apropos (Binder (TT Name)) where

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

77 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

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

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

81

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

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

141 | otherwise = [n]

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

143 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

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

146 nut ps _ = []

147

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

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

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

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

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

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

182 nut ps _ = S.empty

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

188

189directUse :: TT Name -> [Name]

190directUse (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])

192 ++ directUse t

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

194directUse fn@(App _ f a)

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

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

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

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

439

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

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

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

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

442

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

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

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

503 = union (foB b)

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

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

507 foB b = findOuter h env (binderTy b)

508 findOuter h env (App _ f a)

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

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

527unifyProblems :: Elab' aux ()

528unifyProblems = processTactic' UnifyProblems

529

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

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

531+defer ds ls n

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

532+ = do n' <- unique_hole n

532− processTactic' (Defer ds n')

533+ processTactic' (Defer ds ls n')

533− return n'

534+ return n'

534

535

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

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

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

537deferType 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

66 -- True for Bool indicates safe to reduce

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

68 -- For frozen let bindings when simplifying

69− | VBLet Int Name Value Value Value

69+ | VBLet RigCount Int Name Value Value Value

70 | VApp Value Value

71 | VType UExp

72 | VUType Universe

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

278 | otherwise = cases_compiletime cd

279

280 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

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

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

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

311 ev ntimes stk top env (V i)

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

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

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

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

317 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

325 let vd = nexthole hs

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

327 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'

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

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

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

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

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

335 = do b' <- vbind env b

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

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

574 b' <- quoteB b

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

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

578 = do sc' <- quote i sc

579 t' <- quote i t

580 v' <- quote i v

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1018 = getNames Nothing t ++

1019 getNames Nothing v ++

1020 getNames Nothing sc

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

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

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

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

115 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

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

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

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

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

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

135 return $ normalise ctxt env' tm

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

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

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

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

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

140toTT (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)

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

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

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

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

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

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

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

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

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

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

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

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

214 return $

215 return $

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

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

31import Control.Arrow ((***))

32import Control.Monad.State.Strict

33import Data.List

34+import Debug.Trace

34

35

35data ProofState = PS { thname :: Name,

36data ProofState = PS { thname :: Name,

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

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

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

88 | Intro (Maybe Name)

89 | Intro (Maybe Name)

89 | IntroTy Raw (Maybe Name)

90 | IntroTy Raw (Maybe Name)

90 | Forall Name RigCount (Maybe ImplicitInfo) Raw

91 | Forall Name RigCount (Maybe ImplicitInfo) Raw

91− | LetBind Name Raw Raw

92+ | LetBind Name RigCount Raw Raw

92 | ExpandLet Name Term

93 | ExpandLet Name Term

93 | Rewrite Raw

94 | Rewrite Raw

94 | Induction Raw

95 | Induction Raw

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

97 | PatVar Name

98 | PatVar Name

98 | PatBind Name RigCount

99 | PatBind Name RigCount

99 | Focus Name

100 | Focus Name

100− | Defer [Name] Name

101+ | Defer [Name] [Name] Name

101 | DeferType Name Raw [Name]

102 | DeferType Name Raw [Name]

102 | Implementation Name

103 | Implementation Name

103 | AutoArg Name

104 | AutoArg Name

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

128 ") -------\n " ++

129 ") -------\n " ++

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

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

130 where showPs env [] = ""

131 where showPs env [] = ""

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

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

132 = " " ++ show n ++ " : " ++

133 = " " ++ show n ++ " : " ++

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

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

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

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

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

159 prettyGoal ps b = prettyEnv ps $ binderTy b

160 prettyGoal ps b = prettyEnv ps $ binderTy b

160

161

161 prettyPs env [] = empty

162 prettyPs env [] = empty

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

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

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

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

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

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

165 nest nestingSize (prettyPs env bs))

166 nest nestingSize (prettyPs env bs))

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

358

359

359computeLet :: Context -> Name -> Term -> Term

360computeLet :: Context -> Name -> Term -> Term

360computeLet ctxt n tm = cl [] tm where

361computeLet 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)

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

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

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

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

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

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

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

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

366 cl env t = t

367 cl env t = t

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

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

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

413 | otherwise = y : insertB x ys

414 | otherwise = y : insertB x ys

414

415

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

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

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

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

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

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

418

419

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

459 ps { injective = n : is })

460 ps { injective = n : is })

460 return (Bind x b sc)

461 return (Bind x b sc)

461

462

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

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

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

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

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

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

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

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

466 ps { usedns = n : usedns ps,

467 ps { usedns = n : usedns ps,

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

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

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

471 where

472 where

472 mkTy [] t = t

473 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

474

478

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

479 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."

477

481

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

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

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

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

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

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

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

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

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

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

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

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

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

600 (val', vall) = tryLock hs val

604 (val', vall) = tryLock hs val

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

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

603 tryLock hs t@(Bind n b sc)

607 tryLock hs t@(Bind n b sc)

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

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

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

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

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

611 case findType x sc of

615 case findType x sc of

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

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

613 _ -> lift $ tfail (IncompleteTerm h)

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

615 = findType x v `mplus` findType x sc

619 = findType x v `mplus` findType x sc

616 findType x (Bind n t sc)

620 findType x (Bind n t sc)

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

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

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

675 | otherwise = ps

679 | otherwise = ps

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

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

677

681

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

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

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

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

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

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

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

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

682 lift $ isType ctxt env tyt

686 lift $ isType ctxt env tyt

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

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

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

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

685

689

686expandLet :: Name -> Term -> RunTactic

690expandLet :: Name -> Term -> RunTactic

687expandLet n v ctxt env tm =

691expandLet n v ctxt env tm =

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

715 = let b' = mkPB b

719 = let b' = mkPB b

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

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

717 Bind n b' sc'

721 Bind n b' sc'

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

722+ where mkPB (Let c 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

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

720− Let t' v'

724+ Let c t' v'

721 mkPB b = let ty = binderTy b

725 mkPB b = let ty = binderTy b

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

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

723 b { binderTy = ty' }

727 b { binderTy = ty' }

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

1103 mktac (Intro n) = intro n

1107 mktac (Intro n) = intro n

1104 mktac (IntroTy ty n) = introTy ty n

1108 mktac (IntroTy ty n) = introTy ty n

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

1109 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

1107 mktac (ExpandLet n b) = expandLet n b

1111 mktac (ExpandLet n b) = expandLet n b

1108 mktac (Rewrite t) = rewrite t

1112 mktac (Rewrite t) = rewrite t

1109 mktac (Induction t) = casetac t True

1113 mktac (Induction t) = casetac t True

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

1114 mktac (CheckIn r) = check_in r

1118 mktac (CheckIn r) = check_in r

1115 mktac (EvalIn r) = eval_in r

1119 mktac (EvalIn r) = eval_in r

1116 mktac (Focus n) = focus n

1120 mktac (Focus n) = focus n

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

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

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

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

1119 mktac (Implementation n)= implementationArg n

1123 mktac (Implementation n)= implementationArg n

1120 mktac (AutoArg n) = autoArg n

1124 mktac (AutoArg n) = autoArg n

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

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

31

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

33data BinderPath = Binder (Binder TermPath)

34− | LetT TermPath Term

34+ | LetT RigCount TermPath Term

35− | LetV Term TermPath

35+ | LetV RigCount Term TermPath

36 | GuessT TermPath Term

37 | GuessV Term TermPath

38 deriving Show

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

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

47 where

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

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

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

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

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

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

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

53replaceTop 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

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

64rebuildBinder :: Term -> BinderPath -> Binder Term

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

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

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

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

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

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

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

70

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

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

82 fh' env path (Bind x b sc)

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

85 fh' _ _ _ = Nothing

86

87− fhB env path (Let t v)

87+ fhB env path (Let c t v)

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

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 t p, env', tm)

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

90 fhB env path (Guess t v)

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

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

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

185 updateSolved' xs t = (t, False)

186

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

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

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

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

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

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

190− else (b, False)

190+ else (b, False)

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

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

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

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

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

227 subst' i t = (t, False)

228

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

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

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

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

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

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

232− else (b, False)

232+ else (b, False)

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

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

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

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

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

257 where

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

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

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

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

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

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

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

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

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

275 (updateSolvedTerm xs sub)

276 (ups ++ xs)

277

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+

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

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

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

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

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

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

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

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

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

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

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

289 | otherwise

296 | 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+

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

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

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

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

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

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

294

302

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

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

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

297 gb env t = g env (binderTy t)

305 gb env t = g env (binderTy t)

298

306

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

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

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

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

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

332 | otherwise -- scope first

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

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

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

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

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

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

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

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

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

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

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

339

347

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

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

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

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

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

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

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

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

348bound_in_term :: Term -> [Name]

356bound_in_term :: Term -> [Name]

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

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

350 where

358 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

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

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

353 bi b = bound_in_term (binderTy b)

361 bi b = bound_in_term (binderTy b)

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

362bound_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,

844 -- flag says whether it was a scoped implicit

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

846 -- otherwise has no relevance in TT.

847+ | Let { binderCount :: RigCount,

847− | Let { binderTy :: !b,

848+ binderTy :: !b,

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

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

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

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

850 | NLet { binderTy :: !b,

851 | NLet { binderTy :: !b,

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

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

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

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

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

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

885 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

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

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

887 size (Hole ty) = 1 + size ty

888 size (Hole ty) = 1 + size ty

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

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

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

891 size (PVTy ty) = 1 + size ty

892 size (PVTy ty) = 1 + size ty

892

893

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

894fmapMB :: 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1024 termsize rn v + termsize rn sc

1025 termsize rn v + termsize rn sc

1025 termsize n (Bind n' b sc)

1026 termsize n (Bind n' b sc)

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

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

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

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

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

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

1147vinstances 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

1148 instancesB _ = 0

1149 instancesB _ = 0

1149vinstances i t = 0

1150vinstances i t = 0

1150

1151

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

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

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

1272 subst' i t = (t, False)

1273 subst' i t = (t, False)

1273

1274

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

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

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

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

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

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

1277− else (b, False)

1278+ else (b, False)

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

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

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

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

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

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

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

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

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

1322 eqAlpha as x y = x == y

1323 eqAlpha as x y = x == y

1323

1324

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1337 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

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

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

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

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

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

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

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

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

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

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

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

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

1351 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

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

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

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

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

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

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

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

1360freeNames t = nub $ freeNames' t

1361freeNames t = nub $ freeNames' t

1361 where

1362 where

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

1363 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])

1364 ++ freeNames' t

1365 ++ freeNames' t

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

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

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

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

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

1434 b' <- safeForgetEnvB env b

1435 b' <- safeForgetEnvB env b

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

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

1436 Just $ RBind n' b' sc'

1437 Just $ RBind n' b' sc'

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

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

1438− (safeForgetEnv env v)

1439+ (safeForgetEnv env v)

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

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

1440 (safeForgetEnv env v)

1441 (safeForgetEnv env v)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1629

1631

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

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

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

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

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

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

1655 | 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-> "

1655 arrow Rig1 = " -o "

1657 arrow Rig1 = " -o "

1656 arrow RigW = " -> "

1658 arrow RigW = " -> "

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

1659 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

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

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

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

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

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

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

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

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

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

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

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

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

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

1682

1686

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

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

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

1694 pureBinder (Hole _) = False

1698 pureBinder (Hole _) = False

1695 pureBinder (Guess _ _) = False

1699 pureBinder (Guess _ _) = False

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

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

1697 pureBinder t = pureTerm (binderTy t)

1701 pureBinder t = pureTerm (binderTy t)

1698

1702

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

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

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

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

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

1718 where wk i [] = []

1722 where wk i [] = []

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

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

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

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

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

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

1723

1727

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

1728refsIn :: TT Name -> [Name]

1732refsIn :: TT Name -> [Name]

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

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

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

1734refsIn (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)

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

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

1733 nb t = refsIn (binderTy t)

1737 nb t = refsIn (binderTy t)

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

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

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

1738allTTNames = nub . allNamesIn

1742allTTNames = nub . allNamesIn

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

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

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

1744 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

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

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

1743 nb t = allNamesIn (binderTy t)

1747 nb t = allNamesIn (binderTy t)

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

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

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

1790 where mkArrow Rig1 = text "⇴"

1794 where mkArrow Rig1 = text "⇴"

1791 mkArrow Rig0 = text "⥛"

1795 mkArrow Rig0 = text "⥛"

1792 mkArrow _ = text "→"

1796 mkArrow _ = text "→"

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

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

1794 bracket p startPrec . group . align $

1798 bracket p startPrec . group . align $

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

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

1796 bindingOf n False <+> colon <+>

1800 bindingOf n False <+> colon <+>

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

1872 text "Lam" <$> pprintRaw bound ty

1876 text "Lam" <$> pprintRaw bound ty

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

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

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

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

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

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

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

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

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

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

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

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

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

1883 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

98 astate | holes = MaybeHoles

99 | otherwise = Complete

100

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.

102 Type -> -- uniqueness level

104 Type -> -- uniqueness level

103 Maybe UExp -> -- universe for kind

105 Maybe UExp -> -- universe for kind

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

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

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

118 where rigSafe True _ _ n = Nothing

120 where rigSafe True _ _ n = Nothing

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

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

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

122 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")

121 rigSafe _ _ _ n = Nothing

124 rigSafe _ _ _ n = Nothing

122

125

123 used Rig0 n = []

126 used Rig0 n = []

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

137 do (v, cs) <- get

140 do (v, cs) <- get

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

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

139 let apty = simplify initContext env

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

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

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

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

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

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

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

144 convertsC ctxt env aty s

147 convertsC ctxt env aty s

145 let apty = simplify initContext env

148 let apty = simplify initContext env

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

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

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

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

148 t -> lift $ tfail $ NonFunctionType fv fty

151 t -> lift $ tfail $ NonFunctionType fv fty

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

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

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

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

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

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

160 _ -> (RigW, uniqueBinders (map fstEnv env)

158 (normalise ctxt env fty)) -- This is an error, caught below...

161 (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

160 case fty' of

167 case fty' of

161 Bind x (Pi rig i s k) t ->

168 Bind x (Pi rig i s k) t ->

162 do convertsC ctxt env aty s

169 do convertsC ctxt env aty s

163 let apty = simplify initContext env

170 let apty = simplify initContext env

164− (Bind x (Let aty av) t)

171+ (Bind x (Let rig aty av) t)

165 return (App astate fv av, apty, fns ++ ans)

172 return (App astate fv av, apty, fns ++ ans)

166 t -> lift $ tfail $ NonFunctionType fv fty

173 t -> lift $ tfail $ NonFunctionType fv fty

167 chk rigc u lvl env RType

174 chk rigc u lvl env RType

@@ -195,8 +202,6 @@ check' holes tcns ctxt env top

195 constType _ = TType (UVal 0)

202 constType _ = TType (UVal 0)

196 chk rigc u lvl env (RBind n (Pi rig i s k) t)

203 chk rigc u lvl env (RBind n (Pi rig i s k) t)

197 = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s

204 = do (sv, st, sns) <- chk Rig0 u Nothing (envZero env) s

198− when (rig == RigW) $

199− lift $ linearCheckArg ctxt (normalise ctxt env sv)

200 (v, cs) <- get

205 (v, cs) <- get

201 (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent

206 (kv, kt, _) <- chk Rig0 u Nothing (envZero env) k -- no need to validate these constraints, they are independent

202 put (v+1, cs)

207 put (v+1, cs)

@@ -218,16 +223,22 @@ check' holes tcns ctxt env top

218 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

223 return (Bind n (Pi rig i (uniqueBinders (map fstEnv env) sv) k')

219 (pToV n tv), k', sns ++ tns)

224 (pToV n tv), k', sns ++ tns)

220

225

221− chk rigc u lvl env (RBind n b sc)

226+ chk rigc_in u lvl env (RBind n b sc)

222 = do (b', bt', bns) <- checkBinder b

227 = do (b', bt', bns) <- checkBinder b

223 (scv, sct, scns) <- chk rigc (smaller bt' u) Nothing ((n, getCount b, b'):env) sc

228 (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'))

226 checkUsageOK (getCount b) scns

229 checkUsageOK (getCount b) scns

227 discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)

230 discharge n b' bt' (pToV n scv) (pToV n sct) (bns ++ scns)

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

228− where getCount (Pi rig _ _ _) = rigMult rigc rig

238+ getCount (Pi rig _ _ _) = rigMult rigc rig

229 getCount (PVar rig _) = rigMult rigc rig

239 getCount (PVar rig _) = rigMult rigc rig

230 getCount (Lam rig _) = rigMult rigc rig

240 getCount (Lam rig _) = rigMult rigc rig

241+ getCount (Let rig _ _) = rigMult rigc rig

231 getCount _ = rigMult rigc RigW

242 getCount _ = rigMult rigc RigW

232

243

233 checkUsageOK Rig0 _ = return ()

244 checkUsageOK Rig0 _ = return ()

@@ -242,15 +253,12 @@ check' holes tcns ctxt env top

242 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

253 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

243 convType tcns ctxt env tt

254 convType tcns ctxt env tt

244 return (Lam rig tv, tt, [])

255 return (Lam rig tv, tt, [])

245− checkBinder (Let t v)

256+ checkBinder (Let rig t v)

246 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

257 = 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

251 convertsC ctxt env vt tv

259 convertsC ctxt env vt tv

252 convType tcns ctxt env tt

260 convType tcns ctxt env tt

253− return (Let tv vv, tt, vns)

261+ return (Let rig tv vv, tt, vns)

254 checkBinder (NLet t v)

262 checkBinder (NLet t v)

255 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

263 = do (tv, tt, _) <- chk Rig0 u Nothing (envZero env) t

256 (vv, vt, vns) <- chk rigc u Nothing env v

264 (vv, vt, vns) <- chk rigc u Nothing env v

@@ -288,10 +296,10 @@ check' holes tcns ctxt env top

288 = return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)

296 = return (Bind n (Lam r t) scv, Bind n (Pi r Nothing t bt) sct, ns)

289 discharge n (Pi r i t k) bt scv sct ns

297 discharge n (Pi r i t k) bt scv sct ns

290 = return (Bind n (Pi r i t k) scv, sct, ns)

298 = return (Bind n (Pi r i t k) scv, sct, ns)

291− discharge n (Let t v) bt scv sct ns

299+ discharge n (Let r t v) bt scv sct ns

292− = return (Bind n (Let t v) scv, Bind n (Let t v) sct, ns)

300+ = return (Bind n (Let r t v) scv, Bind n (Let r t v) sct, ns)

293 discharge n (NLet t v) bt scv sct ns

301 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)

295 discharge n (Hole t) bt scv sct ns

303 discharge n (Hole t) bt scv sct ns

296 = return (Bind n (Hole t) scv, sct, ns)

304 = return (Bind n (Hole t) scv, sct, ns)

297 discharge n (GHole i ns t) bt scv sct uns

305 discharge n (GHole i ns t) bt scv sct uns

@@ -339,7 +347,7 @@ checkUnique borrowed ctxt env tm

339 = do chkBinderName env n b

347 = do chkBinderName env n b

340 st <- get

348 st <- get

341 case b of

349 case b of

342− Let t v -> chkBinders env v

350+ Let _ t v -> chkBinders env v

343 _ -> return ()

351 _ -> return ()

344 chkBinders ((n, Rig0, b) : env) t

352 chkBinders ((n, Rig0, b) : env) t

345 chkBinders env t = return ()

353 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 =

130 lift $ tfail err

131

132

133− uB bnames (Let tx vx) (Let ty vy) = do h1 <- un bnames tx ty

133+ uB bnames (Let _ tx vx) (Let _ ty vy)

134+ = do h1 <- un bnames tx ty

134− h2 <- un bnames vx vy

135+ h2 <- un bnames vx vy

135− combine bnames h1 h2

136+ combine bnames h1 h2

136 uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty

137 uB bnames (Lam _ tx) (Lam _ ty) = un bnames tx ty

137 uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty

138 uB bnames (Pi r i tx _) (Pi r' i' ty _) = un bnames tx ty

138 uB bnames x y = do UI s f <- get

139 uB bnames x y = do UI s f <- get

@@ -585,7 +586,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

585 lift $ tfail err

586 lift $ tfail err

586

587

588

588− uB env bnames (Let tx vx) (Let ty vy)

589+ uB env bnames (Let _ tx vx) (Let _ ty vy)

589 = do h1 <- un' env False bnames tx ty

590 = do h1 <- un' env False bnames tx ty

590 h2 <- un' env False bnames vx vy

591 h2 <- un' env False bnames vx vy

591 sc 1

592 sc 1

src/Idris/Core/WHNF.hs+2−2

@@ -85,7 +85,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

85 | i < length env = let (tm, env') = env !! i in

86 eval env' stk tm

87 | 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)

89 = eval (WEnv d ((v, wenv) : env)) stk sc

90 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _ _) sc)

91 = eval (WEnv d ((tm, tenv) : env)) stk sc

@@ -94,7 +94,7 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

94 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

95

96 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

98 eval env stk (P nt n ty) = apply env nt n ty stk

99 eval env stk (App _ f a) = eval env ((a, env) : stk) f

100 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)

54 = PApp fc lam [ pexp (mkTTName fc n)

55 , pexp (expandSugar dsl (var dsl n tm 0))]

56expandSugar 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)

58 | Just letb <- dsl_let dsl

59 = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

60 , pexp (expandSugar dsl v)

61 , 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)

63expandSugar dsl (PPi p n fc ty tm)

64 | Just pi <- dsl_pi dsl

65 = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

@@ -103,8 +103,8 @@ expandSugar dsl (PDoBlock ds)

103 = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "__bpat") NoFC Placeholder

104 (PCase fc (PRef fc [] (sMN 0 "__bpat"))

105 ((p, block b rest) : alts)))]

106− block b (DoLet fc n nfc ty tm : rest)

106+ block b (DoLet fc rc n nfc ty tm : rest)

107− = PLet fc n nfc ty tm (block b rest)

107+ = PLet fc rc n nfc ty tm (block b rest)

108 block b (DoLetP fc p tm : rest)

109 = PCase fc tm [(p, block b rest)]

110 block b (DoRewrite fc h : rest)

@@ -134,10 +134,10 @@ var dsl n t i = v' i t where

134 | Nothing <- dsl_lambda dsl

135 = PLam fc n nfc ty (v' i sc)

136 | 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)

138 | Nothing <- dsl_let dsl

139− = PLet fc n nfc (v' i ty) (v' i val) (v' i sc)

139+ = PLet fc rc 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)

140+ | otherwise = PLet fc rc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)

141 v' i (PPi p n fc ty sc)

142 | Nothing <- dsl_pi dsl

143 = 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

200 arg' <- db' arg

201 return (PWithApp fc t' arg')

202 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

203+ db' (PLet fc rc n nfc ty v sc)

204+ = do v' <- db' v

204− return (PLet fc n nfc ty v' (debind b sc))

205+ return (PLet fc rc n nfc ty v' (debind b sc))

205 db' (PCase fc s opts) = do s' <- db' s

206 db' (PCase fc s opts) = do s' <- db' s

206 return (PCase fc s' (map (pmap (debind b)) opts))

207 return (PCase fc s' (map (pmap (debind b)) opts))

207 db' (PPair fc hls p l r) = do l' <- db' l

208 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

43

44-- Erase types (makes ibc smaller, and we don't need them)

45instance 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

47 applyOpts b = return (b { binderTy = Erased })

48

49instance Optimisable (Binder Raw) where

src/Idris/Delaborate.hs+7−7

@@ -55,13 +55,13 @@ resugar ist = transform flattenDoLet . transform resugarApp

55 = PConstant fc (BI i)

56 resugarApp tm = tm

57

58− flattenDoLet (PLet _ ln _ ty v bdy)

58+ flattenDoLet (PLet _ rc ln _ ty v bdy)

59 | PDoBlock dos <- flattenDoLet bdy

60− = PDoBlock (DoLet NoFC ln NoFC ty v : dos)

60+ = PDoBlock (DoLet NoFC rc ln NoFC ty v : dos)

61 flattenDoLet (PDoBlock dos) =

62 PDoBlock $ concatMap fixExp dos

63− where fixExp (DoExp _ (PLet _ ln _ ty v bdy)) =

63+ where fixExp (DoExp _ (PLet _ rc ln _ ty v bdy)) =

64− DoLet NoFC ln NoFC ty v : fixExp (DoExp NoFC bdy)

64+ DoLet NoFC rc ln NoFC ty v : fixExp (DoExp NoFC bdy)

65 fixExp d = [d]

66 flattenDoLet tm = tm

67

@@ -172,13 +172,13 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

172 = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)

173 (de ((n, ty) : tys) ((n,n):env) [] sc)

174

175− de tys env imps (Bind n (Let ty val) sc)

175+ de tys env imps (Bind n (Let rc ty val) sc)

176 | docases

177 , isCaseApp sc

178 , (P _ cOp _, args) <- unApply sc

179 , Just caseblock <- delabCase tys env imps val cOp args = caseblock

180 | otherwise =

181− PLet un n NoFC (de tys env [] ty)

181+ PLet un rc n NoFC (de tys env [] ty)

182 (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)

183 de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

184 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)

441 = getMissing (n : hs) (n : env) sc

442 getMissing hs env (Bind n (Guess _ _) sc)

443 = 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)

445 = getMissing hs env t ++

446 getMissing hs env v ++

447 getMissing hs (n : env) sc

src/Idris/Elab/AsPat.hs+1−1

@@ -21,7 +21,7 @@ desugarAs lhs rhs whereblock

21 (lhs', pats) = runState (collectAs (replaceUnderscore lhs)) []

22

23 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)

25

26 bindInWhereDecl :: [(Name, FC, PTerm)] -> PDecl -> PDecl

27 bindInWhereDecl pats (PClauses fc opts n clauses)

src/Idris/Elab/Clause.hs+2−2

@@ -509,7 +509,7 @@ elabPE info fc caller r =

509 concreteTm ist (Constant _) = True

510 concreteTm ist (Bind n (Lam _ _) sc) = True

511 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

513 concreteTm ist _ = False

514

515 -- 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

902 getVs _ = []

903 borrowedNames env (App _ f a) = nub $ borrowedNames env f ++ borrowedNames env a

904 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

906 borrowedB b = borrowedNames env (binderTy b)

907 borrowedNames _ _ = []

908

src/Idris/Elab/Data.hs−2

@@ -99,8 +99,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

99 -- TMP HACK! Make this a data option

100 updateContext (addDatatype (Data n ttag cty unique cons))

101 updateContext (setMetaInformation n metainf)

102− when (any linearArg (map snd cons)) $

103− updateContext (setRigCount n Rig1)

104

102

105 mapM_ totcheck (zip (repeat fc) (map fst cons))

103 mapM_ totcheck (zip (repeat fc) (map fst cons))

106-- mapM_ (checkPositive n) cons

104-- mapM_ (checkPositive n) cons

src/Idris/Elab/Quasiquote.hs+4−4

@@ -70,10 +70,10 @@ extractDoUnquotes d (DoBind fc n nfc tm)

70 return (DoBind fc n nfc tm', ex)

71extractDoUnquotes d (DoBindP fc t t' alts)

72 = 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)

74 = do (v', ex1) <- extractUnquotes d v

75 (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)

77extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"

78extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"

79

@@ -87,11 +87,11 @@ extractUnquotes n (PPi plicity name fc ty body)

87 = do (ty', ex1) <- extractUnquotes n ty

88 (body', ex2) <- extractUnquotes n body

89 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)

91 = do (ty', ex1) <- extractUnquotes n ty

92 (val', ex2) <- extractUnquotes n val

93 (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)

95extractUnquotes n (PTyped tm ty)

96 = do (tm', ex1) <- extractUnquotes n tm

97 (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

50 Nothing -> return sc_in

51 Just t -> do

52 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

54 (PRef fc [] letn)

55 tyn <- getNameFrom (sMN 0 "rty")

56 claim tyn RType

57 valn <- getNameFrom (sMN 0 "rval")

58 claim valn (Var tyn)

59 letn <- getNameFrom (sMN 0 "_rewrite_rule")

60− letbind letn (Var tyn) (Var valn)

60+ letbind letn RigW (Var tyn) (Var valn)

61 focus valn

62 elab rule

63 compute

@@ -95,9 +95,10 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

95 = let b' = mkPB b

96 sc' = if (r /= sc) then mkP lt l r sc else sc in

97 Bind n b' sc'

98+ where mkPB (Let rig t v)

98− where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

99+ = 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+ v' = if (r /= v) then mkP lt l r v else v in

100− Let t' v'

101+ Let rig t' v'

101 mkPB b = let ty = binderTy b

102 mkPB b = let ty = binderTy b

102 ty' = if (r /= ty) then mkP lt l r ty else ty in

103 ty' = if (r /= ty) then mkP lt l r ty else ty in

103 b { binderTy = ty' }

104 b { binderTy = ty' }

src/Idris/Elab/Term.hs+48−27

@@ -252,7 +252,7 @@ elab ist info emode opts fn tm

252 ptm <- get_term

253 when pattern $

254 -- Look for Rig1 (linear) pattern bindings

255− do let pnms = findLinear ist [] ptm

255+ do let pnms = findLinear Rig1 ist [] ptm

256 update_term (setLinear pnms)

257 where

258 pattern = emode == ELHS || emode == EImpossible

@@ -695,7 +695,7 @@ elab ist info emode opts fn tm

695 elabE ec' fc sc

696 solve

697 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)

699 = do attack

700 ivs <- get_implementations

701 tyn <- getNameFrom (sMN 0 "letty")

@@ -703,7 +703,7 @@ elab ist info emode opts fn tm

703 valn <- getNameFrom (sMN 0 "letval")

704 claim valn (Var tyn)

705 explicit valn

706− letbind n (Var tyn) (Var valn)

706+ letbind n rig (Var tyn) (Var valn)

707 addPSname n

708 case ty of

709 Placeholder -> return ()

@@ -730,7 +730,7 @@ elab ist info emode opts fn tm

730 -- HACK: If the name leaks into its type, it may leak out of

731 -- scope outside, so substitute in the outer scope.

732 expandLet n (case lookupBinder n env of

733− Just (Let t v) -> v

733+ Just (Let rig t v) -> v

734 other -> error ("Value not a let binding: " ++ show other))

735 solve

736 highlightSource nfc (AnnBoundName n False)

@@ -741,7 +741,7 @@ elab ist info emode opts fn tm

741 claim tyn RType

742 valn <- getNameFrom (sMN 0 "letval")

743 claim valn (Var tyn)

744− letbind n (Var tyn) (Var valn)

744+ letbind n RigW (Var tyn) (Var valn)

745 focus valn

746 elabE (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])

747 env <- get_env

@@ -991,11 +991,13 @@ elab ist info emode opts fn tm

991 -- When building the metavar application, leave out the unique

992 -- names which have been used elsewhere in the term, since we

993 -- won't be able to use them in the resulting application.

994+ env <- get_env

994 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

995 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

996+ let lin_used = getLinearUsed (tt_ctxt ist) ptm

995 let n' = metavarName (namespace info) n

997 let n' = metavarName (namespace info) n

996 attack

998 attack

997 psns <- getPSnames

999 psns <- getPSnames

998− n' <- defer unique_used n'

1000+ n' <- defer unique_used lin_used n'

999 solve

1001 solve

1000 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

1002 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

1001 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

1003 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

1016 valn <- getNameFrom (sMN 0 "scval")

1018 valn <- getNameFrom (sMN 0 "scval")

1017 scvn <- getNameFrom (sMN 0 "scvar")

1019 scvn <- getNameFrom (sMN 0 "scvar")

1018 claim valn (Var tyn)

1020 claim valn (Var tyn)

1021+ env <- get_env

1022+

1023+ let scrnames = allNamesIn scr

1019− letbind scvn (Var tyn) (Var valn)

1024+ letbind scvn (letrig scrnames env) (Var tyn) (Var valn)

1020

1025

1021 -- Start filling in the scrutinee type, if we can work one

1026 -- Start filling in the scrutinee type, if we can work one

1022 -- out from the case options

1027 -- out from the case options

@@ -1047,13 +1052,15 @@ elab ist info emode opts fn tm

1047 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1052 let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1048

1053

1049 let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)

1054 let argsDropped = filter (\t -> isUnique envU t || isNotLift args t)

1050− (nub $ allNamesIn scr ++ inApp ptm ++

1055+ (nub $ scrnames ++ inApp ptm ++

1051 inOpts)

1056 inOpts)

1057+ let lin_used = getLinearUsed (tt_ctxt ist) ptm

1052

1058

1053 let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args

1059 let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args

1054

1060

1061+ -- trace (show lin_used ++ "\n" ++ show args ++ "\n" ++ show ptm) attack

1055 attack

1062 attack

1056− cname' <- defer argsDropped (mkN (mkCaseName fc fn))

1063+ cname' <- defer argsDropped lin_used (mkN (mkCaseName fc fn))

1057 solve

1064 solve

1058

1065

1059 -- if the scrutinee is one of the 'args' in env, we should

1066 -- if the scrutinee is one of the 'args' in env, we should

@@ -1075,6 +1082,17 @@ elab ist info emode opts fn tm

1075 xs@(_:_) -> sNS n xs

1082 xs@(_:_) -> sNS n xs

1076 _ -> n

1083 _ -> n

1077

1084

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+

1078 getScrType [] = Nothing

1096 getScrType [] = Nothing

1079 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1097 getScrType (f : os) = maybe (getScrType os) Just (getAppType f)

1080

1098

@@ -1092,7 +1110,7 @@ elab ist info emode opts fn tm

1092

1110

1093 inApp (P _ n _) = [n]

1111 inApp (P _ n _) = [n]

1094 inApp (App _ f a) = inApp f ++ inApp a

1112 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

1096 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

1114 inApp (Bind n (Guess _ v) sc) = inApp v ++ inApp sc

1097 inApp (Bind n b sc) = inApp sc

1115 inApp (Bind n b sc) = inApp sc

1098 inApp _ = []

1116 inApp _ = []

@@ -1163,7 +1181,7 @@ elab ist info emode opts fn tm

1163 -- Let-bind the result of elaborating the contained term, so that

1181 -- Let-bind the result of elaborating the contained term, so that

1164 -- the hole doesn't disappear

1182 -- the hole doesn't disappear

1165 nTm <- getNameFrom (sMN 0 "quotedTerm")

1183 nTm <- getNameFrom (sMN 0 "quotedTerm")

1166− letbind nTm (Var qTy) (Var qTm)

1184+ letbind nTm RigW (Var qTy) (Var qTm)

1167

1185

1168 -- Fill out the goal type, if relevant

1186 -- Fill out the goal type, if relevant

1169 case goalt of

1187 case goalt of

@@ -1290,7 +1308,7 @@ elab ist info emode opts fn tm

1290 -- In order to intercept the elaborated value, we need to

1308 -- In order to intercept the elaborated value, we need to

1291 -- let-bind it.

1309 -- let-bind it.

1292 attack

1310 attack

1293− letbind n g (Var n')

1311+ letbind n RigW g (Var n')

1294 focus n'

1312 focus n'

1295 elab' ina fc tm

1313 elab' ina fc tm

1296 env <- get_env

1314 env <- get_env

@@ -1319,8 +1337,10 @@ elab ist info emode opts fn tm

1319 delayElab pri t

1337 delayElab pri t

1320 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1338 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1321

1339

1340+ -- If the variable in the environment is the scrutinee of the case,

1341+ -- and has multiplicity W, keep it available

1322 isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))

1342 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))

1324 isScr _ (n', _, b) = (n', (False, b))

1344 isScr _ (n', _, b) = (n', (False, b))

1325

1345

1326 caseBlock :: FC -> Name

1346 caseBlock :: FC -> Name

@@ -1332,8 +1352,8 @@ elab ist info emode opts fn tm

1332 map (mkClause args) opts

1352 map (mkClause args) opts

1333

1353

1334 where -- Find the variable we want as the scrutinee and mark it as

1354 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

1355+ -- 'True'. If the scrutinee is available in the environment,

1336− -- otherwise match on the new argument we're adding.

1356+ -- match on that otherwise match on the new argument we're adding.

1337 findScr ((n, (True, t)) : xs)

1357 findScr ((n, (True, t)) : xs)

1338 = (n, (True, t)) : scrName n xs

1358 = (n, (True, t)) : scrName n xs

1339 findScr [(n, (_, t))] = [(n, (True, t))]

1359 findScr [(n, (_, t))] = [(n, (True, t))]

@@ -1721,7 +1741,7 @@ collectDeferred top casenames ctxt tm = cd [] tm

1721 t' <- cd ((n, b) : env) t

1741 t' <- cd ((n, b) : env) t

1722 return (Bind n b' t')

1742 return (Bind n b' t')

1723 where

1743 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)

1725 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1745 cdb (Guess t v) = liftM2 Guess (cd env t) (cd env v)

1726 cdb b = do ty' <- cd env (binderTy b)

1746 cdb b = do ty' <- cd env (binderTy b)

1727 return (b { binderTy = ty' })

1747 return (b { binderTy = ty' })

@@ -1737,7 +1757,7 @@ case_ ind autoSolve ist fn tm = do

1737 valn <- getNameFrom (sMN 0 "ival")

1757 valn <- getNameFrom (sMN 0 "ival")

1738 claim valn (Var tyn)

1758 claim valn (Var tyn)

1739 letn <- getNameFrom (sMN 0 "irule")

1759 letn <- getNameFrom (sMN 0 "irule")

1740− letbind letn (Var tyn) (Var valn)

1760+ letbind letn RigW (Var tyn) (Var valn)

1741 focus valn

1761 focus valn

1742 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1762 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1743 env <- get_env

1763 env <- get_env

@@ -2115,7 +2135,7 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

2115 n' <- reifyTTName n

2135 n' <- reifyTTName n

2116 ty' <- reifyRaw ty

2136 ty' <- reifyRaw ty

2117 tm' <- reifyRaw tm

2137 tm' <- reifyRaw tm

2118− letbind n' ty' tm'

2138+ letbind n' RigW ty' tm'

2119 returnUnit

2139 returnUnit

2120 | n == tacN "Prim__Compute"

2140 | n == tacN "Prim__Compute"

2121 = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit

2141 = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit

@@ -2270,9 +2290,10 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

2270 ptm <- get_term

2290 ptm <- get_term

2271 -- See documentation above in the elab case for PMetavar

2291 -- See documentation above in the elab case for PMetavar

2272 let unique_used = getUniqueUsed ctxt ptm

2292 let unique_used = getUniqueUsed ctxt ptm

2293+ let lin_used = getLinearUsed ctxt ptm

2273 let mvn = metavarName ns n'

2294 let mvn = metavarName ns n'

2274 attack

2295 attack

2275− defer unique_used mvn

2296+ defer unique_used lin_used mvn

2276 solve

2297 solve

2277 returnUnit

2298 returnUnit

2278 | n == tacN "Prim__Fixity"

2299 | n == tacN "Prim__Fixity"

@@ -2377,7 +2398,7 @@ runTac autoSolve ist perhapsFC fn tac

2377 valn <- getNameFrom (sMN 0 "eqval")

2398 valn <- getNameFrom (sMN 0 "eqval")

2378 claim valn (Var tyn)

2399 claim valn (Var tyn)

2379 letn <- getNameFrom (sMN 0 "equiv_val")

2400 letn <- getNameFrom (sMN 0 "equiv_val")

2380− letbind letn (Var tyn) (Var valn)

2401+ letbind letn RigW (Var tyn) (Var valn)

2381 focus tyn

2402 focus tyn

2382 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2403 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2383 focus valn

2404 focus valn

@@ -2390,7 +2411,7 @@ runTac autoSolve ist perhapsFC fn tac

2390 valn <- getNameFrom (sMN 0 "rval")

2411 valn <- getNameFrom (sMN 0 "rval")

2391 claim valn (Var tyn)

2412 claim valn (Var tyn)

2392 letn <- getNameFrom (sMN 0 "rewrite_rule")

2413 letn <- getNameFrom (sMN 0 "rewrite_rule")

2393− letbind letn (Var tyn) (Var valn)

2414+ letbind letn RigW (Var tyn) (Var valn)

2394 focus valn

2415 focus valn

2395 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2416 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2396 rewrite (Var letn)

2417 rewrite (Var letn)

@@ -2406,7 +2427,7 @@ runTac autoSolve ist perhapsFC fn tac

2406 valn <- getNameFrom (sMN 0 "letval")

2427 valn <- getNameFrom (sMN 0 "letval")

2407 claim valn (Var tyn)

2428 claim valn (Var tyn)

2408 letn <- unique_hole n

2429 letn <- unique_hole n

2409− letbind letn (Var tyn) (Var valn)

2430+ letbind letn RigW (Var tyn) (Var valn)

2410 focus valn

2431 focus valn

2411 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2432 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2412 when autoSolve solveAll

2433 when autoSolve solveAll

@@ -2417,7 +2438,7 @@ runTac autoSolve ist perhapsFC fn tac

2417 valn <- getNameFrom (sMN 0 "letval")

2438 valn <- getNameFrom (sMN 0 "letval")

2418 claim valn (Var tyn)

2439 claim valn (Var tyn)

2419 letn <- unique_hole n

2440 letn <- unique_hole n

2420− letbind letn (Var tyn) (Var valn)

2441+ letbind letn RigW (Var tyn) (Var valn)

2421 focus tyn

2442 focus tyn

2422 elab ist toplevel ERHS [] (sMN 0 "tac") ty

2443 elab ist toplevel ERHS [] (sMN 0 "tac") ty

2423 focus valn

2444 focus valn

@@ -2443,7 +2464,7 @@ runTac autoSolve ist perhapsFC fn tac

2443 script <- getNameFrom (sMN 0 "script")

2464 script <- getNameFrom (sMN 0 "script")

2444 claim script scriptTy

2465 claim script scriptTy

2445 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2466 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2446− letbind scriptvar scriptTy (Var script)

2467+ letbind scriptvar RigW scriptTy (Var script)

2447 focus script

2468 focus script

2448 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2469 elab ist toplevel ERHS [] (sMN 0 "tac") tm

2449 (script', _) <- get_type_val (Var scriptvar)

2470 (script', _) <- get_type_val (Var scriptvar)

@@ -2475,7 +2496,7 @@ runTac autoSolve ist perhapsFC fn tac

2475 script <- getNameFrom (sMN 0 "script")

2496 script <- getNameFrom (sMN 0 "script")

2476 claim script scriptTy

2497 claim script scriptTy

2477 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2498 scriptvar <- getNameFrom (sMN 0 "scriptvar" )

2478− letbind scriptvar scriptTy (Var script)

2499+ letbind scriptvar RigW scriptTy (Var script)

2479 focus script

2500 focus script

2480 ptm <- get_term

2501 ptm <- get_term

2481 env <- get_env

2502 env <- get_env

@@ -2506,7 +2527,7 @@ runTac autoSolve ist perhapsFC fn tac

2506 valn <- getNameFrom (sMN 0 "letval")

2527 valn <- getNameFrom (sMN 0 "letval")

2507 claim valn (Var tyn)

2528 claim valn (Var tyn)

2508 letn <- getNameFrom (sMN 0 "letvar")

2529 letn <- getNameFrom (sMN 0 "letvar")

2509− letbind letn (Var tyn) (Var valn)

2530+ letbind letn RigW (Var tyn) (Var valn)

2510 focus valn

2531 focus valn

2511 elab ist toplevel ERHS [] (sMN 0 "tac") v

2532 elab ist toplevel ERHS [] (sMN 0 "tac") v

2512 (value, _) <- get_type_val (Var letn)

2533 (value, _) <- get_type_val (Var letn)

@@ -2520,7 +2541,7 @@ runTac autoSolve ist perhapsFC fn tac

2520 valn <- getNameFrom (sMN 0 "letval")

2541 valn <- getNameFrom (sMN 0 "letval")

2521 claim valn (Var tyn)

2542 claim valn (Var tyn)

2522 letn <- getNameFrom (sMN 0 "letvar")

2543 letn <- getNameFrom (sMN 0 "letvar")

2523− letbind letn (Var tyn) (Var valn)

2544+ letbind letn RigW (Var tyn) (Var valn)

2524 focus valn

2545 focus valn

2525 elab ist toplevel ERHS [] (sMN 0 "tac") v

2546 elab ist toplevel ERHS [] (sMN 0 "tac") v

2526 (value, _) <- get_type_val (Var letn)

2547 (value, _) <- get_type_val (Var letn)

src/Idris/Elab/Type.hs−4

@@ -108,10 +108,6 @@ buildType info syn fc opts n ty' = do

108 setFnInfo n fninfo

109 addIBC (IBCFnInfo n fninfo)

110

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−

115 return (cty, ckind, ty, inacc)

111 return (cty, ckind, ty, inacc)

116 where

112 where

117 patToImp (Bind n (PVar rig t) sc) = Bind n (Pi rig Nothing t (TType (UVar [] 0))) (patToImp sc)

113 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

26import Data.List

27import qualified Data.Map as Map

28import Data.Maybe

29+import Debug.Trace

29

30

30recheckC = recheckC_borrowing False True []

31recheckC = recheckC_borrowing False True []

31

32

@@ -286,6 +287,40 @@ paramNames args env (p : ps)

286 _ -> paramNames args env ps

287 _ -> paramNames args env ps

287 | otherwise = paramNames args env ps

288 | otherwise = paramNames args env ps

288

289

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+

289getUniqueUsed :: Context -> Term -> [Name]

324getUniqueUsed :: Context -> Term -> [Name]

290getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

325getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

291 where

326 where

@@ -307,7 +342,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

307

342

308 use n = do ns <- get; put (n : ns)

343 use n = do ns <- get; put (n : ns)

309

344

310− getUniqB env us (Let t v) = getUniq env us v

345+ getUniqB env us (Let rig t v) = getUniq env us v

311 getUniqB env us (Guess t v) = getUniq env us v

346 getUniqB env us (Guess t v) = getUniq env us v

312-- getUniqB env us (Pi _ _ t v) = do getUniq env us t; getUniq env us v

347-- getUniqB env us (Pi _ _ t v) = do getUniq env us t; getUniq env us v

313 getUniqB env us (NLet t v) = getUniq env us v

348 getUniqB env us (NLet t v) = getUniq env us v

@@ -523,10 +558,10 @@ liftPats tm = let (tm', ps) = runState (getPats tm) [] in

523 v' <- getPats v

558 v' <- getPats v

524 sc' <- getPats sc

559 sc' <- getPats sc

525 return (Bind n (Guess t' v') sc')

560 return (Bind n (Guess t' v') sc')

526− getPats (Bind n (Let t v) sc) = do t' <- getPats t

561+ getPats (Bind n (Let rig t v) sc) = do t' <- getPats t

527− v' <- getPats v

562+ v' <- getPats v

528− sc' <- getPats sc

563+ sc' <- getPats sc

529− return (Bind n (Let t' v') sc')

564+ return (Bind n (Let rig t' v') sc')

530 getPats (Bind n (Pi rig i t k) sc) = do t' <- getPats t

565 getPats (Bind n (Pi rig i t k) sc) = do t' <- getPats t

531 k' <- getPats k

566 k' <- getPats k

532 sc' <- getPats sc

567 sc' <- getPats sc

@@ -574,24 +609,43 @@ hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

574 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

609 = isEmpty ctxt tyctxt ty || hasEmptyPat ctxt tyctxt sc

575hasEmptyPat ctxt tyctxt _ = False

610hasEmptyPat ctxt tyctxt _ = False

576

611

577−-- Find names which are applied to a function in a Rig1 position

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)

578−findLinear :: IState -> [Name] -> Term -> [(Name, RigCount)]

617+findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]

618+findLinear rig ist env tm

579−findLinear ist env tm | (P _ f _, args) <- unApply tm,

619+ | (P _ f _, args) <- unApply tm,

580− f `notElem` env,

620+ f `notElem` env,

581− Just ty_in <- lookupTyExact f (tt_ctxt ist)

621+ Just ty_in <- lookupTyExact f (tt_ctxt ist)

582 = let ty = whnfArgs (tt_ctxt ist) [] ty_in in

622 = let ty = whnfArgs (tt_ctxt ist) [] ty_in in

583− nub $ concatMap (findLinear ist env) args ++ findLinArg ty args

623+ combineRig $ findLinArg ty args

584 where

624 where

585 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

625 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

626+ = (a, rigMult rig c) : findLinArg sc as

588− findLinArg (Bind n (Pi _ _ _ _) sc) (a : as)

627+ findLinArg (Bind n (Pi c _ _ _) sc) (a : as)

628+ = findLinear (rigMult c rig) ist env a ++

589− = findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

629+ findLinArg (whnf (tt_ctxt ist) [] (substV a sc)) as

590− findLinArg _ _ = []

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+

591−findLinear ist env (App _ f a)

645+findLinear rig ist env (App _ f a)

592− = nub $ findLinear ist env f ++ findLinear ist env a

646+ = nub $ findLinear rig ist env f ++ findLinear rig ist env a

593−findLinear ist env (Bind n b sc) = findLinear ist (n : env) sc

647+findLinear rig ist env (Bind n b sc) = findLinear rig ist (n : env) sc

594−findLinear ist _ _ = []

648+findLinear rig ist _ _ = []

595

649

596setLinear :: [(Name, RigCount)] -> Term -> Term

650setLinear :: [(Name, RigCount)] -> Term -> Term

597setLinear ns (Bind n b@(PVar r t) sc)

651setLinear ns (Bind n b@(PVar r t) sc)

src/Idris/ElabDecls.hs+4

@@ -61,7 +61,11 @@ elabPrims = do i <- getIState

61 let mkdec opt decl docs argdocs =

62 PData docs argdocs defaultSyntax (fileFC "builtin")

63 opt decl

64+ -- need to temporarily add linearity for this since the

65+ -- argument may be of restricted type

66+ addLangExt LinearTypes

64 elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

67 elabDecl' EAll (recinfo primfc) (mkdec inferOpts inferDecl emptyDocstring [])

68+ dropLangExt LinearTypes

65 -- We don't want the constraints generated by 'Infer' since

69 -- We don't want the constraints generated by 'Infer' since

66 -- it's only scaffolding for the elaborator

70 -- it's only scaffolding for the elaborator

67 i <- getIState

71 i <- getIState

src/Idris/Erasure.hs+3−3

@@ -476,7 +476,7 @@ buildDepMap ci used externs ctx startNames

476

477 -- let-bound variables can get partially evaluated

478 -- 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

480 | NLet ty t <- bdr = var t cd `union` getDepsTerm vs ((n, const M.empty) : bs) cd body

481 where

482 var t cd = getDepsTerm vs bs cd t

@@ -529,7 +529,7 @@ buildDepMap ci used externs ctx startNames

529 Bind n (Lam _ ty) t -> getDepsTerm vs bs cd (lamToLet app)

530

531 -- 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')

533 Bind n (NLet ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam RigW ty) t) t')

534

535 Proj t i

@@ -609,7 +609,7 @@ buildDepMap ci used externs ctx startNames

609 (f, args) = unApply tm

610

611 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

613 lamToLet' [] tm = tm

614 lamToLet' vs tm = error $

615 "Erasure.hs:lamToLet': unexpected input: "

src/Idris/Error.hs+2−2

@@ -100,7 +100,7 @@ warnDisamb ist (PInferRef _ _ _) = return ()

100warnDisamb ist (PPatvar _ _) = return ()

101warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

102warnDisamb 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

104warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t

105warnDisamb ist (PApp _ t args) = warnDisamb ist t >>

106 mapM_ (warnDisamb ist . getTm) args

@@ -129,7 +129,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

129 wStep (DoBind _ _ _ x) = warnDisamb ist x

130 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

131 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

133 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

134 wStep (DoRewrite _ h) = warnDisamb ist h

135warnDisamb ist (PIdiom _ x) = warnDisamb ist x

src/Idris/IBC.hs+18−6

@@ -40,7 +40,7 @@ import System.Directory

40import System.FilePath

41

42ibcVersion :: Word16

43−ibcVersion = 163

43+ibcVersion = 164

44

45-- | When IBC is being loaded - we'll load different things (and omit

46-- different structures/definitions) depending on which phase we're in.

@@ -100,6 +100,7 @@ data IBCFile = IBCFile {

100 , ibc_access :: ![(Name, Accessibility)]

101 , ibc_fragile :: ![(Name, String)]

102 , ibc_constraints :: ![(FC, UConstraint)]

103+ , ibc_langexts :: ![LanguageExt]

103 }

104 }

104 deriving Show

105 deriving Show

105{-!

106{-!

@@ -107,7 +108,7 @@ deriving instance Binary IBCFile

107!-}

108!-}

108

109

109initIBC :: IBCFile

110initIBC :: IBCFile

110−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] []

111+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] [] [] [] [] [] [] [] [] []

111

112

112hasValidIBCVersion :: FilePath -> Idris Bool

113hasValidIBCVersion :: FilePath -> Idris Bool

113hasValidIBCVersion fp = do

114hasValidIBCVersion fp = do

@@ -206,7 +207,8 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

206 makeEntry "ibc_total" (ibc_total i),

207 makeEntry "ibc_total" (ibc_total i),

207 makeEntry "ibc_injective" (ibc_injective i),

208 makeEntry "ibc_injective" (ibc_injective i),

208 makeEntry "ibc_access" (ibc_access i),

209 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)]

210-- TODO: Put this back in shortly after minimising/pruning constraints

212-- TODO: Put this back in shortly after minimising/pruning constraints

211-- makeEntry "ibc_constraints" (ibc_constraints i)]

213-- makeEntry "ibc_constraints" (ibc_constraints i)]

212

214

@@ -221,7 +223,8 @@ writeIBC src f

221 iReport 2 $ "Writing IBC for: " ++ show f

223 iReport 2 $ "Writing IBC for: " ++ show f

222 i <- getIState

224 i <- getIState

223 resetNameIdx

225 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 })

225 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

228 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

226 writeArchive f ibcf

229 writeArchive f ibcf

227 logIBC 2 "Written")

230 logIBC 2 "Written")

@@ -238,7 +241,8 @@ writePkgIndex f

238 logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++

241 logIBC 2 $ "Writing package index " ++ show f ++ " including\n" ++

239 show (map snd imps)

242 show (map snd imps)

240 resetNameIdx

243 resetNameIdx

241− let ibcf = initIBC { ibc_imports = imps }

244+ let ibcf = initIBC { ibc_imports = imps,

245+ ibc_langexts = idris_language_extensions i }

242 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

246 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

243 writeArchive f ibcf

247 writeArchive f ibcf

244 logIBC 2 "Written")

248 logIBC 2 "Written")

@@ -430,6 +434,7 @@ process reexp phase archive fn = do

430 processAccess reexp phase archive

434 processAccess reexp phase archive

431 processFragile archive

435 processFragile archive

432 processConstraints archive

436 processConstraints archive

437+ processLangExts phase archive

433

438

434timestampOlder :: FilePath -> FilePath -> Idris ()

439timestampOlder :: FilePath -> FilePath -> Idris ()

435timestampOlder src ibc = do

440timestampOlder src ibc = do

@@ -705,7 +710,7 @@ processDefs ar = do

705 sc' <- update sc

710 sc' <- update sc

706 return $ Bind n b' sc'

711 return $ Bind n b' sc'

707 where

712 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)

709 updateB b = do

714 updateB b = do

710 ty' <- update' (binderTy b)

715 ty' <- update' (binderTy b)

711 return (b { binderTy = ty' })

716 return (b { binderTy = ty' })

@@ -833,6 +838,13 @@ processMetaVars ar = do

833 ns <- getEntry [] "ibc_metavars" ar

838 ns <- getEntry [] "ibc_metavars" ar

834 updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

839 updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

835

840

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+

836----- For Cheapskate and docstrings

848----- For Cheapskate and docstrings

837

849

838instance Binary a => Binary (D.Docstring a)

850instance Binary a => Binary (D.Docstring a)

src/Idris/IdrisDoc.hs+2−2

@@ -279,7 +279,7 @@ extractPTermNames (PInferRef _ _ n) = [n]

279extractPTermNames (PPatvar _ n) = [n]

280extractPTermNames (PLam _ n _ p1 p2) = n : concatMap extract [p1, p2]

281extractPTermNames (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]

283extractPTermNames (PTyped p1 p2) = concatMap extract [p1, p2]

284extractPTermNames (PApp _ p pas) = let names = concatMap extractPArg pas

285 in (extract p) ++ names

@@ -330,7 +330,7 @@ extractPDo (DoBind _ n _ p) = n : extract p

330extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

331 ps' = ps1 ++ ps2

332 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]

334extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

335extractPDo (DoRewrite _ p) = extract p

336

src/Idris/Inliner.hs+1−1

@@ -29,7 +29,7 @@ inlineTerm ist tm = inl tm where

29 inl orig@(P _ n _) = inlApp n [] orig

30 inl orig@(App _ f a)

31 | (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)

33 inl (Bind n b sc) = Bind n b (inl sc)

34 inl tm = tm

35

src/Idris/Interactive.hs+1−1

@@ -261,7 +261,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

261 else iPrintResult newmv

262 where dropCtxt 0 sc = sc

263 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

265 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc

266 dropCtxt _ t = t

267

src/Idris/Main.hs+2−2

@@ -157,10 +157,10 @@ idrisMain opts =

157

158 mapM_ addPkgDir pkgdirs

159 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)

161 addAutoImport "Builtins"

162 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)

164 addAutoImport "Prelude"

165 return ()

166 when (runrepl && not idesl) initScript

src/Idris/Parser.hs+6−6

@@ -501,8 +501,8 @@ syntaxRule syn

501 n' <- gensym n

502 body' <- fixBind 0 ((n,n'):rens) body

503 return $ (PPi plic n' nfc ty' body')

504− fixBind 0 rens (PLet fc n nfc ty val body)

504+ fixBind 0 rens (PLet fc rig n nfc ty val body)

505− | n `elem` userNames = liftM3 (PLet fc n nfc)

505+ | n `elem` userNames = liftM3 (PLet fc rig n nfc)

506 (fixBind 0 rens ty)

507 (fixBind 0 rens val)

508 (fixBind 0 rens body)

@@ -511,7 +511,7 @@ syntaxRule syn

511 val' <- fixBind 0 rens val

512 n' <- gensym n

513 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'

515 fixBind 0 rens (PMatchApp fc n) | Just n' <- lookup n rens =

516 return $ PMatchApp fc n'

517 -- Also rename resolved quotations, to allow syntax rules to

@@ -1104,10 +1104,10 @@ rhs syn n = do lchar '='

1104 n' :: Name

1105 n' = mkN n

1106 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)

1108 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)

1109 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))

1111

1112{-|Parses a function clause

1113

@@ -1171,7 +1171,7 @@ clause syn

1171 return x,

1172 do terminator

1173 return ([], [])]

1174− let capp = PLet fc (sMN 0 "match") NoFC

1174+ let capp = PLet fc RigW (sMN 0 "match") NoFC

1175 ty

1176 (PMatchApp fc n)

1177 (PRef fc [] (sMN 0 "match"))

src/Idris/Parser/Expr.hs+6−6

@@ -190,9 +190,9 @@ updateSynMatch = update

190 = let (n', nfc') = updateB ns (n, fc)

191 in PPi (updTacImp ns p) n' nfc'

192 (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)

194 = 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)

196 (update ns val) (update (dropn n ns) sc)

197 update ns (PApp fc t args)

198 = PApp fc (update ns t) (map (fmap (update ns)) args)

@@ -217,7 +217,7 @@ updateSynMatch = update

217 where upd :: [(Name, SynMatch)] -> PDo -> PDo

218 upd ns (DoExp fc t) = DoExp fc (update ns t)

219 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)

221 upd ns (DoBindP fc i t ts)

222 = DoBindP fc (update ns i) (update ns t)

223 (map (\(l,r) -> (update ns l, update ns r)) ts)

@@ -669,7 +669,7 @@ app syn = do f <- simpleExpr syn

669 (do try $ reservedOp "<=="

670 fc <- getFC

671 ff <- fst <$> fnName

672− return (PLet fc (sMN 0 "match") NoFC

672+ return (PLet fc RigW (sMN 0 "match") NoFC

673 f

674 (PMatchApp fc ff)

675 (PRef fc [] (sMN 0 "match")))

@@ -995,7 +995,7 @@ let_ syn = try (do kw <- reservedFC "let"

995 <?> "let binding"

996 where buildLets [] sc = sc

997 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)

999 buildLets ((fc, pat, ty, v, alts) : ls) sc

1000 = PCase fc v ((pat, buildLets ls sc) : alts)

1001

@@ -1349,7 +1349,7 @@ do_ syn

1349 fc <- getFC

1350 e <- expr syn

1351 highlightP kw AnnKeyword

1352− return (DoLet fc i ifc ty e))

1352+ return (DoLet fc RigW i ifc ty e))

1353 <|> try (do kw <- reservedFC "let"

1354 i <- expr' syn

1355 reservedOp "="

src/Idris/PartialEval.hs+7−7

@@ -94,12 +94,12 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in

94 where

95 -- Specialise static argument in type by let-binding provided value instead

96 -- of expecting it as a function argument

97− st ((ExplicitS, v) : xs) (Bind n (Pi _ _ t _) sc)

97+ st ((ExplicitS, v) : xs) (Bind n (Pi rc _ t _) sc)

98− = Bind n (Let t v) (st xs sc)

98+ = Bind n (Let rc t v) (st xs sc)

99− st ((ImplicitS _, v) : xs) (Bind n (Pi _ _ t _) sc)

99+ st ((ImplicitS _, v) : xs) (Bind n (Pi rc _ t _) sc)

100− = Bind n (Let t v) (st xs sc)

100+ = Bind n (Let rc t v) (st xs sc)

101− st ((ConstraintS, v) : xs) (Bind n (Pi _ _ t _) sc)

101+ st ((ConstraintS, v) : xs) (Bind n (Pi rc _ t _) sc)

102− = Bind n (Let t v) (st xs sc)

102+ = Bind n (Let rc t v) (st xs sc)

103 -- Erase argument from function type

104 st ((UnifiedD, _) : xs) (Bind n (Pi _ _ t _) sc)

105 = st xs sc

@@ -364,7 +364,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

364-- _ -> []

365 else []

366 _ -> []

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

368 ga env (Bind n t sc) = ga (n : env) sc

369 ga env t = []

370

src/Idris/ProofSearch.hs+4−4

@@ -139,7 +139,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]

139 where

140 -- if nothing worked, make a new metavariable

141 tryAllFns [] | fromProver = cantSolveGoal

142− tryAllFns [] = do attack; defer [] nroot; solve

142+ tryAllFns [] = do attack; defer [] [] nroot; solve

143 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

144

145 tryFn (f, args) = do let imps = map isImp args

@@ -155,7 +155,7 @@ proofSearch False fromProver ambigok deferonfail depth elab _ nroot psnames [fn]

155 if fromProver then cantSolveGoal

156 else do

157 mapM_ (\ h -> do focus h

158− attack; defer [] nroot; solve)

158+ attack; defer [] [] nroot; solve)

159 (hs' \\ hs)

160-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

161 solve

@@ -242,7 +242,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

242 -- that's no use)

243 psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()

244 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"

246 psRec False d locs tys = tryCons d locs tys hints

247 psRec True d locs tys

248 = do compute

@@ -258,7 +258,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

258 -- if all else fails, make a new metavariable

259 (if fromProver

260 then fail "cantSolveGoal"

261− else do attack; defer [] nroot; solve) True) True

261+ else do attack; defer [] [] nroot; solve) True) True

262

263 -- get recursive function name. Only user given names make sense.

264 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

181 | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs

182 prettyPs all g bnd ((n@(MN _ _), _, _) : bs)

183 | 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) =

185 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

186 align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs

187 prettyPs all g bnd ((n, _, b) : bs) =

@@ -350,13 +350,13 @@ elabloop info fn d prompt prf e prev h env

350 DoLetP {} -> ifail "Pattern-matching let not supported here"

351 DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

352 DoBindP {} -> ifail "Pattern-matching <- not supported here"

353− DoLet fc i ifc Placeholder expr ->

353+ DoLet fc rig i ifc Placeholder expr ->

354 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)

355 ctxt <- getContext

356 let tm' = normaliseAll ctxt [] tm

357 ty' = normaliseAll ctxt [] ty

358 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 ->

360 do (tm, ty) <- elabVal (recinfo proverfc) ERHS

361 (PApp NoFC (PRef NoFC [] (sUN "the"))

362 [ pexp (inLets ist env ty)

@@ -402,7 +402,7 @@ elabloop info fn d prompt prf e prev h env

402 -- the elaborator with a custom environment here to avoid the

403 -- delab step.

404 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)

406

407

408

src/Idris/REPL.hs+8−2

@@ -994,11 +994,12 @@ process fn (Check (PRef _ _ n))

994 putTy ppo ist i [] (delab ist (errReverse ist ty'))

995 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

996 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)

998 = let current = case n of

999 MN _ _ -> text ""

1000 UN nm | ('_':'_':_) <- str nm -> text ""

1001− _ -> text " " <>

1001+ _ -> countOf (pcount p)

1002+ (LinearTypes `elem` idris_language_extensions ist) <+>

1002 bindingOf n False

1003 bindingOf n False

1003 <+> colon

1004 <+> colon

1004 <+> align (tPretty bnd ist t)

1005 <+> align (tPretty bnd ist t)

@@ -1011,6 +1012,11 @@ process fn (Check (PRef _ _ n))

1011 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

1012 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

1012 align (tPretty bnd ist g)

1013 align (tPretty bnd ist g)

1013

1014

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+

1014 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

1020 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

1015

1021

1016

1022

src/Idris/Reflection.hs+6−6

@@ -313,7 +313,7 @@ reifyTTBinderApp reif f [t]

313reifyTTBinderApp reif f [t, k]

314 | f == reflm "Pi" = liftM2 (Pi RigW Nothing) (reif t) (reif k)

315reifyTTBinderApp 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)

317reifyTTBinderApp reif f [t]

318 | f == reflm "Hole" = liftM Hole (reif t)

319reifyTTBinderApp reif f [t]

@@ -533,9 +533,9 @@ reflectRawQuotePattern unq (RBind n b sc) =

533 focus scH; reflectRawQuotePattern unq sc

534 focus bH; reflectBinderQuotePattern reflectRawQuotePattern (Var $ reflm "Raw") unq b

535 where freeNamesR (Var n) = [n]

536− freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

536+ freeNamesR (RBind n (Let rc t v) body) = concat [freeNamesR v,

537− freeNamesR body \\ [n],

537+ freeNamesR body \\ [n],

538− freeNamesR t]

538+ freeNamesR t]

539 freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

540 (freeNamesR body \\ [n])

541 freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

@@ -583,7 +583,7 @@ reflectBinderQuotePattern q ty unq (Pi _ _ t k)

583 fill $ reflCall "Pi" [ty, Var t', Var k']

584 solve

585 focus t'; q unq t

586−reflectBinderQuotePattern q ty unq (Let x y)

586+reflectBinderQuotePattern q ty unq (Let rc x y)

587 = do x' <- claimTy (sMN 0 "ty") ty; movelast x';

588 y' <- claimTy (sMN 0 "v")ty; movelast y';

589 fill $ reflCall "Let" [ty, Var x', Var y']

@@ -748,7 +748,7 @@ reflectBinderQuote q ty unq (Lam _ t)

748 = reflCall "Lam" [Var ty, q unq t]

749reflectBinderQuote q ty unq (Pi _ _ t k)

750 = 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)

752 = reflCall "Let" [Var ty, q unq x, q unq y]

753reflectBinderQuote q ty unq (NLet x y)

754 = reflCall "Let" [Var ty, q unq x, q unq y]

src/Idris/Termination.hs+2−2

@@ -77,7 +77,7 @@ checkIfGuarded n

77 allGuarded names i _ = True

78

79 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)

81 = guardedTerm names i v && guardedTerm names i sc

82 guardedTerm names i (Bind n b sc) = False

83 guardedTerm names i ap@(App _ _ _)

@@ -364,7 +364,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

364 notPartial _ = True

365 findCalls cases guarded (App _ f a) pvs pargs

366 = 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

368 = findCalls cases Unguarded t pvs pargs ++

369 findCalls cases Unguarded v pvs pargs ++

370 -- 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)

153usedVars = f True where

154 f b (P Bound n t) = M.singleton n (t, b) `M.union` f b t

155 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

157 Guess t v -> f b t `M.union` f b v

158 bind -> f b (binderTy bind)

159 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

31names _ = []

32

33occursBinder :: 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

35occursBinder n (NLet ty val) = occurs n ty || occurs n val

36occursBinder n b = occurs n (binderTy b)

37

38namesBinder :: Binder Term -> [Name]

39−namesBinder (Let ty val) = names ty ++ names val

39+namesBinder (Let rc ty val) = names ty ++ names val

40namesBinder (NLet ty val) = names ty ++ names val

41namesBinder b = names (binderTy b)

42