ad13438 · Idris-dev · git.iko.soy

src/Idris/Core/Evaluate.hs+28−1

compare with master

unifiedsplit

@@ -27,7 +27,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

27 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

28 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

29 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

30− isUniverse) where

30+ isUniverse, linearCheck, linearCheckArg) where

31

32import Idris.Core.CaseTree

33import Idris.Core.TT

@@ -1174,6 +1174,33 @@ lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

1174lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1175 where mkt (d, _, inj, a, t, m) = inj

1176

1177+-- Assume type is at least in whnfArgs form

1178+linearCheck :: Context -> Type -> TC ()

1179+linearCheck ctxt t = checkArgs t

1180+ where

1181+ checkArgs (Bind n (Pi RigW _ ty _) sc)

1182+ = do linearCheckArg ctxt ty

1183+ checkArgs (substV (P Bound n Erased) sc)

1184+ checkArgs (Bind n (Pi _ _ _ _) sc)

1185+ = checkArgs (substV (P Bound n Erased) sc)

1186+ checkArgs _ = return ()

1187+

1188+linearCheckArg :: Context -> Type -> TC ()

1189+linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)

1190+ where

1191+ checkNameOK f

1192+ = case lookupRigCountExact f ctxt of

1193+ Just Rig1 ->

1194+ tfail $ Msg $ show f ++ " can only appear in a linear binding"

1195+ _ -> return ()

1196+

1197+ checkArgs (Bind n (Pi RigW _ ty _) sc)

1198+ = do mapM_ checkNameOK (allTTNames ty)

1199+ checkArgs (substV (P Bound n Erased) sc)

1200+ checkArgs (Bind n (Pi _ _ _ _) sc)

1201+ = checkArgs (substV (P Bound n Erased) sc)

1202+ checkArgs _ = return ()

1203+

1177-- Check if a name is reducible in the type checker. Partial definitions

1204-- Check if a name is reducible in the type checker. Partial definitions

1178-- are not reducible (so treated as a constant)

1205-- are not reducible (so treated as a constant)

1179tcReducible :: Name -> Context -> Bool

1206tcReducible :: Name -> Context -> Bool

src/Idris/Core/Typecheck.hs+5

@@ -12,6 +12,7 @@ Maintainer : The Idris Community.

12module Idris.Core.Typecheck where

13

14import Idris.Core.Evaluate

15+import Idris.Core.WHNF

15import Idris.Core.TT

16import Idris.Core.TT

16

17

17import Control.Monad.State

18import Control.Monad.State

@@ -197,6 +198,8 @@ check' holes tcns ctxt env top

197 constType _ = TType (UVal 0)

198 constType _ = TType (UVal 0)

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

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

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

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

201+ when (rig == RigW) $

202+ lift $ linearCheckArg ctxt (normalise ctxt env sv)

200 (v, cs) <- get

203 (v, cs) <- get

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

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

202 put (v+1, cs)

205 put (v+1, cs)

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

242 chk rigc u lvl env (RBind n b sc)

245 chk rigc u lvl env (RBind n b sc)

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

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

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

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

248+ when (getCount b == RigW) $

249+ lift $ linearCheckArg ctxt (normalise ctxt env (binderTy b'))

245 checkUsageOK (getCount b) scns

250 checkUsageOK (getCount b) scns

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

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

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

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

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

@@ -136,7 +136,7 @@ buildType info syn fc opts n ty' = do

136

137 -- If we use any types with linear constructor arguments, we'd better

138 -- make sure they are use-once

139− linearCheck fc (whnfArgs ctxt [] cty)

139+ tcliftAt fc $ linearCheck ctxt (whnfArgs ctxt [] cty)

140

141 return (cty, ckind, ty, inacc)

142 where

src/Idris/Elab/Utils.hs−19

@@ -598,25 +598,6 @@ setLinear ns (Bind n b@(PVar r t) sc)

598 | otherwise = Bind n b (setLinear ns sc)

599setLinear ns tm = tm

600

601−-- Assume type is at least in whnfArgs form

602−linearCheck :: FC -> Type -> Idris ()

603−linearCheck fc t = do ist <- getIState

604− checkArgs ist t

605− where

606− checkNameOK ist f

607− = case lookupRigCountExact f (tt_ctxt ist) of

608− Just Rig1 ->

609− ierror $ At fc $

610− Msg $ show f ++ " can only appear in a linear binding"

611− _ -> return ()

612−

613− checkArgs ist (Bind n (Pi RigW _ ty _) sc)

614− = do mapM_ (checkNameOK ist) (allTTNames ty)

615− checkArgs ist (substV (P Bound n Erased) sc)

616− checkArgs ist (Bind n (Pi _ _ _ _) sc)

617− = checkArgs ist (substV (P Bound n Erased) sc)

618− checkArgs ist _ = return ()

619−

620linearArg :: Type -> Bool

601linearArg :: Type -> Bool

621linearArg (Bind n (Pi Rig1 _ _ _) sc) = True

602linearArg (Bind n (Pi Rig1 _ _ _) sc) = True

622linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc

603linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc

src/Idris/Error.hs+6

@@ -79,6 +79,12 @@ tclift (Error err@(At fc e)) = do setErrSpan fc; throwError err

79tclift (Error err@(UniverseError fc _ _ _ _)) = do setErrSpan fc; throwError err

80tclift (Error err) = throwError err

81

82+tcliftAt :: FC -> TC a -> Idris a

83+tcliftAt fc (OK v) = return v

84+tcliftAt fc (Error err@(At _ e)) = do setErrSpan fc; throwError err

85+tcliftAt fc (Error err@(UniverseError _ _ _ _ _)) = do setErrSpan fc; throwError err

86+tcliftAt fc (Error err) = do setErrSpan fc; throwError (At fc err)

87+

82tctry :: TC a -> TC a -> Idris a

88tctry :: TC a -> TC a -> Idris a

83tctry tc1 tc2

89tctry tc1 tc2

84 = case tc1 of

90 = case tc1 of