fb185aa · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

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

115 return $ normalise ctxt env' tm

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

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

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

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

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

120

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

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

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

85 fh' env path (Bind x b sc)

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

88 fh' _ _ _ = Nothing

89

90 fhB env path (Let t v)

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

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

298 | same h n = return $ GD env b

299 | otherwise

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

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

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

302 | otherwise

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

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

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

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

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

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

338 = do -- binder first

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

340 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

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

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

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

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

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

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

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

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

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

1126 codata :: Bool,

1127 data_opts :: DataOpts,

1128 param_pos :: [Int],

1129− mutual_types :: [Name] }

1129+ mutual_types :: [Name],

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

1131+ }

1130 deriving (Show, Generic)

1132 deriving (Show, Generic)

1131{-!

1133{-!

1132deriving instance Binary TypeInfo

1134deriving instance Binary TypeInfo

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

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

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

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

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

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

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

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

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

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

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

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

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

1699 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

119 | otherwise = do lift $ tfail $ NoSuchVariable n

120 where rigSafe True _ _ n = Nothing

121 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")

122 rigSafe _ _ _ n = Nothing

123 rigSafe _ _ _ n = Nothing

123

124

124 used Rig0 n = []

125 used Rig0 n = []

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

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

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

264 checkBinder (Let t v)

265 checkBinder (Let t v)

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

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

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

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

269 let tv' = normalise ctxt env tv

271 let tv' = normalise ctxt env tv

270 convertsC ctxt env vt tv

272 convertsC ctxt env vt tv

271 convType tcns ctxt env tt

273 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 =

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

509 | sameBinder bx by

510 = 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

512 combine env bnames h1 h2

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

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

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

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

650 OK (_, UType NullType) -> True

651 OK (_, UType AllTypes) -> True

652 _ -> False in

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

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

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

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

655findUnique _ _ _ = []

656

657getUnfolds (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

922 rev <- case ret_fam of

923 P _ rfamn _ ->

924 case lookupCtxt rfamn (idris_datatypes i) of

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

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

926 return (DataErrRev `elem` dopts &&

927 size clhs <= size crhs)

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

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

105 -- be updated when the mutual block is complete

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

108 (idris_datatypes i) })

109 (idris_datatypes i) })

109 addIBC (IBCDef n)

110 addIBC (IBCDef n)

110 addIBC (IBCData n)

111 addIBC (IBCData n)

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

173 liftname = id -- Is this appropriate?

174 liftname = id -- Is this appropriate?

174 }

175 }

175

176

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

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

179+ linearArg _ = False

180+

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

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

177 Type -> -- for unique kind checking

182 Type -> -- for unique kind checking

178 Type -> -- data type's kind

183 Type -> -- data type's kind

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

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

1242 _ -> False

1243 case quoted of

1244 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

1246 if pattern

1247 then if isRaw

1248 then reflectRawQuotePattern unquoteNames (forget q')

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

2831 mapM_ (addIBC . IBCDef . cn) ctors

2832 ctxt <- getContext

2833 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

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

2836 -- otherwise writing the IBC just fails silently!

2837 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

181 let nty' = normalise ctxt [] nty

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

183

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+

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

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

185 -- the name unambiguously)

189 -- the name unambiguously)

186 i <- getIState

190 i <- getIState

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

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

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

193 let corec = case fam of

197 let corec = case fam of

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

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

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

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

196 _ -> False

200 _ -> False

197 _ -> False

201 _ -> False

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

202 -- 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) []

299 OK (_, UType AllTypes) -> True

300 _ -> False in

301 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

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

304 getUniq env us (V i)

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

574hasEmptyPat ctxt tyctxt _ = False

575

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

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

579 f `notElem` env,

580 Just ty_in <- lookupTyExact f (tt_ctxt ist)

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

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

583 where

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

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

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

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

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

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

587 findLinArg _ _ = []

588 findLinArg _ _ = []

588findLinear ist env (App _ f a)

589findLinear ist env (App _ f a)

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

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

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

591findLinear ist _ _ = []

592findLinear ist _ _ = []

592

593

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

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

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

595setLinear 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)

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

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

597setLinear ns tm = tm

598setLinear ns tm = tm

598

599

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+

599

616

src/Idris/IBC.hs+9−7

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

47import System.FilePath

48

49ibcVersion :: Word16

50−ibcVersion = 158

50+ibcVersion = 159

51

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

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

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

2424 return (FnInfo x1)

2425

2426instance Binary TypeInfo where

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

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

2428− put x2

2428+ put x2

2429− put x3

2429+ put x3

2430− put x4

2430+ put x4

2431− put x5

2431+ put x5

2432+ put x6

2432 get = do x1 <- get

2433 get = do x1 <- get

2433 x2 <- get

2434 x2 <- get

2434 x3 <- get

2435 x3 <- get

2435 x4 <- get

2436 x4 <- get

2436 x5 <- get

2437 x5 <- get

2438+ x6 <- get

2437− return (TI x1 x2 x3 x4 x5)

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

2438

2440

2439instance Binary SynContext where

2441instance Binary SynContext where

2440 put x

2442 put x

src/Idris/REPL.hs+1−1

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

1517 ppMissing _ = empty

1518

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

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

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

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

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

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

src/Idris/Reflection.hs+1−1

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

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

827reifyEnv :: Term -> ElabD Env

828reifyEnv 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

830

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

832rawBool :: Bool -> Raw

src/Idris/Termination.hs+2−2

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

185 case unApply (getRetTy ty) of

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

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

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

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

189 ts -> [tyn]

190 checkPositive ms (n, ty)

191 _-> return $ Total []

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

471

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

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

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

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

475 _ -> (False, []) in

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

477 isInductive _ _ = False