fb185aa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check for linearity of constructors

If a type has any linear constructors, it can only be used at multiplicity 1

commitfb185aa2a2ac75b11381b8652eb64b42b59c19a5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 18 Dec 2016, 23:43 (10 years ago) parenta5033e7

14 files changed+66−33

compare with master

unifiedsplit

src/Idris/Core/Execute.hs+1−1 src/Idris/Core/ProofTerm.hs+5−5 src/Idris/Core/TT.hs+4−1 src/Idris/Core/Typecheck.hs+4−2 src/Idris/Core/Unify.hs+1−1 src/Idris/Elab/Clause.hs+3−3 src/Idris/Elab/Data.hs+6−1 src/Idris/Elab/Term.hs+2−2 src/Idris/Elab/Type.hs+5−1 src/Idris/Elab/Utils.hs+22−5 src/Idris/IBC.hs+9−7 src/Idris/REPL.hs+1−1 src/Idris/Reflection.hs+1−1 src/Idris/Termination.hs+2−2

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

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

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

115115 return $ normalise ctxt env' tm

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

117− return (n, Rig0, Let Erased v')

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

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

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

120120

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

@@ -84,7 +84,7 @@ findHole n env t = fh' env Top t where

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

8585 fh' env path (Bind x b sc)

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

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

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

8888 fh' _ _ _ = Nothing

8989

9090 fhB env path (Let t v)

@@ -297,10 +297,10 @@ goal h pt@(PT path env sub ups)

297297 g env (Bind n b@(Guess _ _) sc)

298298 | same h n = return $ GD env b

299299 | otherwise

300− = gb env b `mplus` g ((n, Rig0, b):env) sc

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

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

302302 | otherwise

303− = g ((n, Rig0, b):env) sc `mplus` gb env b

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

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

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

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

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

338338 = do -- binder first

339339 (b', u) <- ulift2 f c env Guess t v

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

341− else do (sc', u) <- atH f c ((n, Rig0, b) : env) sc

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

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

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

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

345345 | otherwise -- scope first

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

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

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

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

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

src/Idris/Core/TT.hs+4−1

@@ -1126,7 +1126,9 @@ data TypeInfo = TI { con_names :: [Name],

11261126 codata :: Bool,

11271127 data_opts :: DataOpts,

11281128 param_pos :: [Int],

1129− mutual_types :: [Name] }

1129+ mutual_types :: [Name],

1130+ linear_con :: Bool -- is there a linear argument?

1131+ }

11301132 deriving (Show, Generic)

11311133{-!

11321134deriving instance Binary TypeInfo

@@ -1691,6 +1693,7 @@ showEnv' env t dbg = se 10 env t where

16911693 sb env n (Pi _ (Just _) t _) = showb env "{" "} -> " n t

16921694 sb env n (Pi Rig1 _ t _) = showb env "(" ") -0 " n t

16931695 sb env n (Pi _ _ t _) = showb env "(" ") -> " n t

1696+ sb env n (PVar Rig0 t) = showb env "pat 0 " ". " n t

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

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

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

src/Idris/Core/Typecheck.hs+4−2

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

119119 | otherwise = do lift $ tfail $ NoSuchVariable n

120120 where rigSafe True _ _ n = Nothing

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

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

122123 rigSafe _ _ _ n = Nothing

123124

124125 used Rig0 n = []

@@ -263,9 +264,10 @@ check' holes tcns ctxt env top

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

264265 checkBinder (Let t v)

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

266− -- May have multiple uses, check at RigW.

267+ -- May have multiple uses, check at RigW

268+ -- (or rather, like an application of a lambda, multiply)

267269 -- (Consider: adding a single use let?)

268− (vv, vt, vns) <- chk RigW u Nothing env v

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

269271 let tv' = normalise ctxt env tv

270272 convertsC ctxt env vt tv

271273 convType tcns ctxt env tt

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

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

508508 un' env fn bnames (Bind x bx sx) (Bind y by sy)

509509 | sameBinder bx by

510510 = do h1 <- uB env bnames bx by

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

511+ h2 <- un' ((x, RigW, bx) : env) False (((x,y),binderTy bx):bnames) sx sy

512512 combine env bnames h1 h2

513513 where sameBinder (Lam _ _) (Lam _ _) = True

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

src/Idris/Elab/Clause.hs+3−3

@@ -650,8 +650,8 @@ findUnique ctxt env (Bind n b sc)

650650 OK (_, UType NullType) -> True

651651 OK (_, UType AllTypes) -> True

652652 _ -> False in

653− if uniq then n : findUnique ctxt ((n, Rig0, b) : env) sc

654− else findUnique ctxt ((n, Rig0, b) : env) sc

653+ if uniq then n : findUnique ctxt ((n, RigW, b) : env) sc

654+ else findUnique ctxt ((n, RigW, b) : env) sc

655655findUnique _ _ _ = []

656656

657657getUnfolds (UnfoldIface n ns : _) = Just (n, ns)

@@ -922,7 +922,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

922922 rev <- case ret_fam of

923923 P _ rfamn _ ->

924924 case lookupCtxt rfamn (idris_datatypes i) of

925− [TI _ _ dopts _ _] ->

925+ [TI _ _ dopts _ _ _] ->

926926 return (DataErrRev `elem` dopts &&

927927 size clhs <= size crhs)

928928 _ -> return False

src/Idris/Elab/Data.hs+6−1

@@ -104,7 +104,8 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

104104 -- TI contains information about mutually declared types - this will

105105 -- be updated when the mutual block is complete

106106 putIState (i { idris_datatypes =

107− addDef n (TI (map fst cons) codata opts params [n])

107+ addDef n (TI (map fst cons) codata opts params [n]

108+ (any linearArg (map snd cons)))

108109 (idris_datatypes i) })

109110 addIBC (IBCDef n)

110111 addIBC (IBCData n)

@@ -173,6 +174,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

173174 liftname = id -- Is this appropriate?

174175 }

175176

177+ linearArg (Bind n (Pi Rig1 _ _ _) sc) = True

178+ linearArg (Bind n (Pi _ _ _ _) sc) = linearArg sc

179+ linearArg _ = False

180+

176181elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

177182 Type -> -- for unique kind checking

178183 Type -> -- data type's kind

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

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

12421242 _ -> False

12431243 case quoted of

12441244 Just q -> do ctxt <- get_context

1245− (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Rig0, Lam Rig0 Erased) | uq <- unquoteNames] (forget q) q

1245+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, RigW, Lam RigW Erased) | uq <- unquoteNames] (forget q) q

12461246 if pattern

12471247 then if isRaw

12481248 then reflectRawQuotePattern unquoteNames (forget q')

@@ -2831,7 +2831,7 @@ processTacticDecls info steps =

28312831 mapM_ (addIBC . IBCDef . cn) ctors

28322832 ctxt <- getContext

28332833 let params = findParams tyn (normalise ctxt [] tyconTy) (map cty ctors)

2834− let typeInfo = TI (map cn ctors) False [] params []

2834+ let typeInfo = TI (map cn ctors) False [] params [] False

28352835 -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.

28362836 -- otherwise writing the IBC just fails silently!

28372837 updateIState $ \i -> i { idris_datatypes =

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

@@ -181,6 +181,10 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

181181 let nty' = normalise ctxt [] nty

182182 logElab 2 $ "Rechecked to " ++ show nty'

183183

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

185+ -- make sure they are use-once

186+ linearCheck fc nty'

187+

184188 -- Add function name to internals (used for making :addclause know

185189 -- the name unambiguously)

186190 i <- getIState

@@ -192,7 +196,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

192196 let (fam, _) = unApply (getRetTy nty')

193197 let corec = case fam of

194198 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

195− [TI _ True _ _ _] -> True

199+ [TI _ True _ _ _ _] -> True

196200 _ -> False

197201 _ -> False

198202 -- Productivity checking now via checking for guarded 'Delay'

src/Idris/Elab/Utils.hs+22−5

@@ -299,7 +299,7 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

299299 OK (_, UType AllTypes) -> True

300300 _ -> False in

301301 do getUniqB env us b

302− getUniq ((n, Rig0, b):env) ((n, uniq):us) sc

302+ getUniq ((n, RigW, b):env) ((n, uniq):us) sc

303303 getUniq env us (App _ f a) = do getUniq env us f; getUniq env us a

304304 getUniq env us (V i)

305305 | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

@@ -574,7 +574,7 @@ hasEmptyPat ctxt tyctxt (Bind n (PVar _ ty) sc)

574574hasEmptyPat ctxt tyctxt _ = False

575575

576576-- Find names which are applied to a function in a Rig1 position

577−findLinear :: IState -> [Name] -> Term -> [Name]

577+findLinear :: IState -> [Name] -> Term -> [(Name, RigCount)]

578578findLinear ist env tm | (P _ f _, args) <- unApply tm,

579579 f `notElem` env,

580580 Just ty_in <- lookupTyExact f (tt_ctxt ist)

@@ -582,7 +582,8 @@ findLinear ist env tm | (P _ f _, args) <- unApply tm,

582582 nub $ concatMap (findLinear ist env) args ++ findLinArg ty args

583583 where

584584 findLinArg (Bind n (Pi c _ _ _) sc) (P _ a _ : as)

585− | Rig1 <- c = a : findLinArg sc as

585+ | Rig0 <- c = (a, c) : findLinArg sc as

586+ | Rig1 <- c = (a, c) : findLinArg sc as

586587 findLinArg (Bind n (Pi _ _ _ _) sc) (a : as) = findLinArg sc as

587588 findLinArg _ _ = []

588589findLinear ist env (App _ f a)

@@ -590,10 +591,26 @@ findLinear ist env (App _ f a)

590591findLinear ist env (Bind n b sc) = findLinear ist (n : env) sc

591592findLinear ist _ _ = []

592593

593−setLinear :: [Name] -> Term -> Term

594+setLinear :: [(Name, RigCount)] -> Term -> Term

594595setLinear ns (Bind n b@(PVar r t) sc)

595− | n `elem` ns = Bind n (PVar Rig1 t) (setLinear ns sc)

596+ | Just r <- lookup n ns = Bind n (PVar r t) (setLinear ns sc)

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

597598setLinear ns tm = tm

598599

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

601+linearCheck :: FC -> Type -> Idris ()

602+linearCheck fc t = do ist <- getIState

603+ checkArgs ist t

604+ where

605+ checkArgs ist (Bind n (Pi RigW _ ty _) sc)

606+ | (P _ f _, _) <- unApply ty

607+ = case lookupCtxtExact f (idris_datatypes ist) of

608+ Just ti | linear_con ti ->

609+ ierror $ At fc $

610+ Msg $ show ty ++ " has a linear constructor, so must have count <= 1"

611+ _ -> return ()

612+ checkArgs ist (Bind n (Pi _ _ _ _) sc)

613+ = checkArgs ist (substV (P Bound n Erased) sc)

614+ checkArgs ist _ = return ()

615+

599616

src/Idris/IBC.hs+9−7

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

4747import System.FilePath

4848

4949ibcVersion :: Word16

50−ibcVersion = 158

50+ibcVersion = 159

5151

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

5353-- different structures/definitions) depending on which phase we're in.

@@ -2424,17 +2424,19 @@ instance Binary FnInfo where

24242424 return (FnInfo x1)

24252425

24262426instance Binary TypeInfo where

2427− put (TI x1 x2 x3 x4 x5) = do put x1

2428− put x2

2429− put x3

2430− put x4

2431− put x5

2427+ put (TI x1 x2 x3 x4 x5 x6) = do put x1

2428+ put x2

2429+ put x3

2430+ put x4

2431+ put x5

2432+ put x6

24322433 get = do x1 <- get

24332434 x2 <- get

24342435 x3 <- get

24352436 x4 <- get

24362437 x5 <- get

2437− return (TI x1 x2 x3 x4 x5)

2438+ x6 <- get

2439+ return (TI x1 x2 x3 x4 x5 x6)

24382440

24392441instance Binary SynContext where

24402442 put x

src/Idris/REPL.hs+1−1

@@ -1517,7 +1517,7 @@ pprintDef asCore n =

15171517 ppMissing _ = empty

15181518

15191519 ppTy :: Bool -> IState -> (Name, TypeInfo) -> Doc OutputAnnotation

1520− ppTy amb ist (n, TI constructors isCodata _ _ _)

1520+ ppTy amb ist (n, TI constructors isCodata _ _ _ _)

15211521 = kwd key <+> prettyName True amb [] n <+> colon <+>

15221522 align (pprintDelabTy ist n) <+> kwd "where" <$>

15231523 indent 2 (vsep (map (ppCon False ist) constructors))

src/Idris/Reflection.hs+1−1

@@ -826,7 +826,7 @@ reflectEnv = foldr consToEnvList emptyEnvList . envBinders

826826-- Reflected environments don't get the RigCount (for the moment, at least)

827827reifyEnv :: Term -> ElabD Env

828828reifyEnv tm = do preEnv <- reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT"))) tm

829− return $ map (\(n, b) -> (n, Rig0, b)) preEnv

829+ return $ map (\(n, b) -> (n, RigW, b)) preEnv

830830

831831-- | Reflect an error into the internal datatype of Idris -- TODO

832832rawBool :: Bool -> Raw

src/Idris/Termination.hs+2−2

@@ -185,7 +185,7 @@ checkTotality path fc n

185185 case unApply (getRetTy ty) of

186186 (P _ tyn _, _) -> do

187187 let ms = case lookupCtxt tyn (idris_datatypes i) of

188− [TI _ _ _ _ xs@(_:_)] -> xs

188+ [TI _ _ _ _ xs@(_:_) _] -> xs

189189 ts -> [tyn]

190190 checkPositive ms (n, ty)

191191 _-> return $ Total []

@@ -471,7 +471,7 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

471471

472472 isInductive (P _ nty _) (P _ nty' _) =

473473 let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of

474− [TI _ x _ _ muts] -> (x, muts)

474+ [TI _ x _ _ muts _] -> (x, muts)

475475 _ -> (False, []) in

476476 (nty == nty' || any (== nty') muts) && not co

477477 isInductive _ _ = False