89dd6ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Check linearity of functions

89dd6aeEdwin Brady10 years ago

CHANGELOG.md+10−2

compare with master

unifiedsplit

@@ -2,14 +2,22 @@

3## Language updates

5+* Language pragmas now required for the less stable existing features, in

5−* New language extensions, in addition to the existing `TypeProviders` and

6+ addition to the existing `TypeProviders` and `ErrorReflection`:

6− `ErrorReflection`:

7 + `ElabReflection`, which must be enabled to use `%runElab`

8 + `UniquenessTypes`, which must be enabled to use `UniqueType`

9 + `DSLNotation`, which must be enabled to define a `dsl` block

10 + `FirstClassReflection`, which must be enabled to define a `%reflection`

11 function

13+* New language extension `LinearTypes`:

14+ + This allows adding a /multiplicity/ to a binder which says how often it

15+ is allowed to be used; either 0 or 1 (if unstated, multiplicity is "many")

16+ + The typing rules follow Conor McBride's paper "I Got Plenty o' Nuttin'"

17+ + This is highly experimental, unfinished, not at all polished. and there

18+ are still lots of details to sort out. Some features don't quite work

19+ properly yet. But it is there to play with for the brave!

20+

13## Tool Updates

21## Tool Updates

15+ Idris' output has been updated to more accurately reflect its

23+ Idris' output has been updated to more accurately reflect its

src/IRTS/Compiler.hs+1−1

@@ -466,7 +466,7 @@ irTerm top vs env tm@(App _ f a) = do

466 | otherwise = n

467

468 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

469− fst4 (x,_,_,_,_) = x

469+ fst4 (x,_,_,_,_,_) = x

470

471irTerm top vs env (P _ n _) = return $ LV (Glob n)

472irTerm top vs env (V i)

src/Idris/ASTUtils.hs+1−1

@@ -148,7 +148,7 @@ opts_idrisCmdline =

148--

149-- This has a terrible name, but I'm not sure of a better one that

150-- isn't confusingly close to tt_ctxt

151−known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation))

151+known_terms :: Field IState (Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation))

152known_terms = Field (definitions . tt_ctxt)

153 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

154

src/Idris/Core/Evaluate.hs+50−32

@@ -16,12 +16,14 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,

16 Def(..), CaseInfo(..), CaseDefs(..),

17 Accessibility(..), Injectivity, Totality(..), PReason(..), MetaInformation(..),

18 Context, initContext, ctxtAlist, next_tvar,

19+ addToCtxt, setAccess, setInjective, setTotal, setRigCount,

19− addToCtxt, setAccess, setInjective, setTotal, setMetaInformation, addCtxtDef, addTyDecl,

20+ setMetaInformation, addCtxtDef, addTyDecl,

20 addDatatype, addCasedef, simplifyCasedef, addOperator,

21 addDatatype, addCasedef, simplifyCasedef, addOperator,

21 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

22 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

22 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

23 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

23 mapDefCtxt, tcReducible,

24 mapDefCtxt, tcReducible,

24 lookupTotal, lookupTotalExact, lookupInjectiveExact,

25 lookupTotal, lookupTotalExact, lookupInjectiveExact,

26+ lookupRigCount, lookupRigCountExact,

25 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

27 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,

26 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,

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

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

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

@@ -866,9 +868,11 @@ data MetaInformation =

866

868

867-- | Contexts used for global definitions and for proof state. They contain

869-- | Contexts used for global definitions and for proof state. They contain

868-- universe constraints and existing definitions.

870-- universe constraints and existing definitions.

871+-- Also store maximum RigCount of the name (can't bind a name at multiplicity

872+-- 1 in a RigW, for example)

869data Context = MkContext {

873data Context = MkContext {

870 next_tvar :: Int,

874 next_tvar :: Int,

871− definitions :: Ctxt (Def, Injectivity, Accessibility, Totality, MetaInformation)

875+ definitions :: Ctxt (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)

872 } deriving (Show, Generic)

876 } deriving (Show, Generic)

873

877

874

878

@@ -878,53 +882,59 @@ initContext = MkContext 0 emptyContext

878

882

879mapDefCtxt :: (Def -> Def) -> Context -> Context

883mapDefCtxt :: (Def -> Def) -> Context -> Context

880mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)

884mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)

881− where f' (!d, i, a, t, m) = f' (f d, i, a, t, m)

885+ where f' (!d, r, i, a, t, m) = f' (f d, r, i, a, t, m)

882

886

883-- | Get the definitions from a context

887-- | Get the definitions from a context

884ctxtAlist :: Context -> [(Name, Def)]

888ctxtAlist :: Context -> [(Name, Def)]

885−ctxtAlist ctxt = map (\(n, (d, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

889+ctxtAlist ctxt = map (\(n, (d, r, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)

886

890

887veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

891veval ctxt env t = evalState (eval False ctxt [] env t []) initEval

888

892

889addToCtxt :: Name -> Term -> Type -> Context -> Context

893addToCtxt :: Name -> Term -> Type -> Context -> Context

890addToCtxt n tm ty uctxt

894addToCtxt n tm ty uctxt

891 = let ctxt = definitions uctxt

895 = let ctxt = definitions uctxt

892− !ctxt' = addDef n (Function ty tm, False, Public, Unchecked, EmptyMI) ctxt in

896+ !ctxt' = addDef n (Function ty tm, RigW, False, Public, Unchecked, EmptyMI) ctxt in

893 uctxt { definitions = ctxt' }

897 uctxt { definitions = ctxt' }

894

898

895setAccess :: Name -> Accessibility -> Context -> Context

899setAccess :: Name -> Accessibility -> Context -> Context

896setAccess n a uctxt

900setAccess n a uctxt

897 = let ctxt = definitions uctxt

901 = let ctxt = definitions uctxt

898− !ctxt' = updateDef n (\ (d, i, _, t, m) -> (d, i, a, t, m)) ctxt in

902+ !ctxt' = updateDef n (\ (d, r, i, _, t, m) -> (d, r, i, a, t, m)) ctxt in

899 uctxt { definitions = ctxt' }

903 uctxt { definitions = ctxt' }

900

904

901setInjective :: Name -> Injectivity -> Context -> Context

905setInjective :: Name -> Injectivity -> Context -> Context

902setInjective n i uctxt

906setInjective n i uctxt

903 = let ctxt = definitions uctxt

907 = let ctxt = definitions uctxt

904− !ctxt' = updateDef n (\ (d, _, a, t, m) -> (d, i, a, t, m)) ctxt in

908+ !ctxt' = updateDef n (\ (d, r, _, a, t, m) -> (d, r, i, a, t, m)) ctxt in

905 uctxt { definitions = ctxt' }

909 uctxt { definitions = ctxt' }

906

910

907setTotal :: Name -> Totality -> Context -> Context

911setTotal :: Name -> Totality -> Context -> Context

908setTotal n t uctxt

912setTotal n t uctxt

909 = let ctxt = definitions uctxt

913 = let ctxt = definitions uctxt

910− !ctxt' = updateDef n (\ (d, i, a, _, m) -> (d, i, a, t, m)) ctxt in

914+ !ctxt' = updateDef n (\ (d, r, i, a, _, m) -> (d, r, i, a, t, m)) ctxt in

915+ uctxt { definitions = ctxt' }

916+

917+setRigCount :: Name -> RigCount -> Context -> Context

918+setRigCount n rc uctxt

919+ = let ctxt = definitions uctxt

920+ !ctxt' = updateDef n (\ (d, _, i, a, t, m) -> (d, rc, i, a, t, m)) ctxt in

911 uctxt { definitions = ctxt' }

921 uctxt { definitions = ctxt' }

912

922

913setMetaInformation :: Name -> MetaInformation -> Context -> Context

923setMetaInformation :: Name -> MetaInformation -> Context -> Context

914setMetaInformation n m uctxt

924setMetaInformation n m uctxt

915 = let ctxt = definitions uctxt

925 = let ctxt = definitions uctxt

916− !ctxt' = updateDef n (\ (d, i, a, t, _) -> (d, i, a, t, m)) ctxt in

926+ !ctxt' = updateDef n (\ (d, r, i, a, t, _) -> (d, r, i, a, t, m)) ctxt in

917 uctxt { definitions = ctxt' }

927 uctxt { definitions = ctxt' }

918

928

919addCtxtDef :: Name -> Def -> Context -> Context

929addCtxtDef :: Name -> Def -> Context -> Context

920addCtxtDef n d c = let ctxt = definitions c

930addCtxtDef n d c = let ctxt = definitions c

921− !ctxt' = addDef n (d, False, Public, Unchecked, EmptyMI) $! ctxt in

931+ !ctxt' = addDef n (d, RigW, False, Public, Unchecked, EmptyMI) $! ctxt in

922 c { definitions = ctxt' }

932 c { definitions = ctxt' }

923

933

924addTyDecl :: Name -> NameType -> Type -> Context -> Context

934addTyDecl :: Name -> NameType -> Type -> Context -> Context

925addTyDecl n nt ty uctxt

935addTyDecl n nt ty uctxt

926 = let ctxt = definitions uctxt

936 = let ctxt = definitions uctxt

927− !ctxt' = addDef n (TyDecl nt ty, False, Public, Unchecked, EmptyMI) ctxt in

937+ !ctxt' = addDef n (TyDecl nt ty, RigW, False, Public, Unchecked, EmptyMI) ctxt in

928 uctxt { definitions = ctxt' }

938 uctxt { definitions = ctxt' }

929

939

930addDatatype :: Datatype Name -> Context -> Context

940addDatatype :: Datatype Name -> Context -> Context

@@ -932,14 +942,14 @@ addDatatype (Data n tag ty unique cons) uctxt

932 = let ctxt = definitions uctxt

942 = let ctxt = definitions uctxt

933 ty' = normalise uctxt [] ty

943 ty' = normalise uctxt [] ty

934 !ctxt' = addCons 0 cons (addDef n

944 !ctxt' = addCons 0 cons (addDef n

935− (TyDecl (TCon tag (arity ty')) ty, True, Public, Unchecked, EmptyMI) ctxt) in

945+ (TyDecl (TCon tag (arity ty')) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt) in

936 uctxt { definitions = ctxt' }

946 uctxt { definitions = ctxt' }

937 where

947 where

938 addCons tag [] ctxt = ctxt

948 addCons tag [] ctxt = ctxt

939 addCons tag ((n, ty) : cons) ctxt

949 addCons tag ((n, ty) : cons) ctxt

940 = let ty' = normalise uctxt [] ty in

950 = let ty' = normalise uctxt [] ty in

941 addCons (tag+1) cons (addDef n

951 addCons (tag+1) cons (addDef n

942− (TyDecl (DCon tag (arity ty') unique) ty, True, Public, Unchecked, EmptyMI) ctxt)

952+ (TyDecl (DCon tag (arity ty') unique) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt)

943

953

944-- FIXME: Too many arguments! Refactor all these Bools.

954-- FIXME: Too many arguments! Refactor all these Bools.

945--

955--

@@ -973,7 +983,7 @@ addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)

973 (args_rt, sc_rt)

983 (args_rt, sc_rt)

974 op = (CaseOp (ci { case_inlinable = inlc })

984 op = (CaseOp (ci { case_inlinable = inlc })

975 ty argtys ps_in ps_ct cdef,

985 ty argtys ps_in ps_ct cdef,

976− False, access, Unchecked, EmptyMI)

986+ RigW, False, access, Unchecked, EmptyMI)

977 in return $ addDef n op ctxt

987 in return $ addDef n op ctxt

978-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

988-- other -> tfail (Msg $ "Error adding case def: " ++ show other)

979 return uctxt { definitions = ctxt' }

989 return uctxt { definitions = ctxt' }

@@ -986,15 +996,15 @@ simplifyCasedef :: Name -> ErasureInfo -> Context -> TC Context

986simplifyCasedef n ei uctxt

996simplifyCasedef n ei uctxt

987 = do let ctxt = definitions uctxt

997 = do let ctxt = definitions uctxt

988 ctxt' <- case lookupCtxt n ctxt of

998 ctxt' <- case lookupCtxt n ctxt of

989− [(CaseOp ci ty atys [] ps _, inj, acc, tot, metainf)] ->

999+ [(CaseOp ci ty atys [] ps _, rc, inj, acc, tot, metainf)] ->

990 return ctxt -- nothing to simplify (or already done...)

1000 return ctxt -- nothing to simplify (or already done...)

991− [(CaseOp ci ty atys ps_in ps cd, inj, acc, tot, metainf)] ->

1001+ [(CaseOp ci ty atys ps_in ps cd, rc, inj, acc, tot, metainf)] ->

992 do let ps_in' = map simpl ps_in

1002 do let ps_in' = map simpl ps_in

993 pdef = map debind ps_in'

1003 pdef = map debind ps_in'

994 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

1004 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei

995 return $ addDef n (CaseOp ci

1005 return $ addDef n (CaseOp ci

996 ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),

1006 ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),

997− inj, acc, tot, metainf) ctxt

1007+ rc, inj, acc, tot, metainf) ctxt

998

1008

999 _ -> return ctxt

1009 _ -> return ctxt

1000 return uctxt { definitions = ctxt' }

1010 return uctxt { definitions = ctxt' }

@@ -1014,10 +1024,10 @@ addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->

1014 Context -> Context

1024 Context -> Context

1015addOperator n ty a op uctxt

1025addOperator n ty a op uctxt

1016 = let ctxt = definitions uctxt

1026 = let ctxt = definitions uctxt

1017− ctxt' = addDef n (Operator ty a op, False, Public, Unchecked, EmptyMI) ctxt in

1027+ ctxt' = addDef n (Operator ty a op, RigW, False, Public, Unchecked, EmptyMI) ctxt in

1018 uctxt { definitions = ctxt' }

1028 uctxt { definitions = ctxt' }

1019

1029

1020−tfst (a, _, _, _, _) = a

1030+tfst (a, _, _, _, _, _) = a

1021

1031

1022lookupNames :: Name -> Context -> [Name]

1032lookupNames :: Name -> Context -> [Name]

1023lookupNames n ctxt

1033lookupNames n ctxt

@@ -1103,10 +1113,10 @@ lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]

1103lookupP_all all exact n ctxt

1113lookupP_all all exact n ctxt

1104 = do (n', def) <- names

1114 = do (n', def) <- names

1105 p <- case def of

1115 p <- case def of

1106− (Function ty tm, inj, a, _, _) -> return (P Ref n' ty, a)

1116+ (Function ty tm, _, inj, a, _, _) -> return (P Ref n' ty, a)

1107− (TyDecl nt ty, _, a, _, _) -> return (P nt n' ty, a)

1117+ (TyDecl nt ty, _, _, a, _, _) -> return (P nt n' ty, a)

1108− (CaseOp _ ty _ _ _ _, inj, a, _, _) -> return (P Ref n' ty, a)

1118+ (CaseOp _ ty _ _ _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)

1109− (Operator ty _ _, inj, a, _, _) -> return (P Ref n' ty, a)

1119+ (Operator ty _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)

1110 case snd p of

1120 case snd p of

1111 Hidden -> if all then return (fst p) else []

1121 Hidden -> if all then return (fst p) else []

1112 Private -> if all then return (fst p) else []

1122 Private -> if all then return (fst p) else []

@@ -1133,28 +1143,36 @@ lookupDefAcc :: Name -> Bool -> Context ->

1133lookupDefAcc n mkpublic ctxt

1143lookupDefAcc n mkpublic ctxt

1134 = map mkp $ lookupCtxt n (definitions ctxt)

1144 = map mkp $ lookupCtxt n (definitions ctxt)

1135 -- io_bind a special case for REPL prettiness

1145 -- io_bind a special case for REPL prettiness

1136− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1146+ where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1137− then (d, Public) else (d, a)

1147+ then (d, Public) else (d, a)

1138

1148

1139lookupDefAccExact :: Name -> Bool -> Context ->

1149lookupDefAccExact :: Name -> Bool -> Context ->

1140 Maybe (Def, Accessibility)

1150 Maybe (Def, Accessibility)

1141lookupDefAccExact n mkpublic ctxt

1151lookupDefAccExact n mkpublic ctxt

1142 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

1152 = fmap mkp $ lookupCtxtExact n (definitions ctxt)

1143 -- io_bind a special case for REPL prettiness

1153 -- io_bind a special case for REPL prettiness

1144− where mkp (d, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1154+ where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))

1145− then (d, Public) else (d, a)

1155+ then (d, Public) else (d, a)

1146

1156

1147lookupTotal :: Name -> Context -> [Totality]

1157lookupTotal :: Name -> Context -> [Totality]

1148lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

1158lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

1149− where mkt (d, inj, a, t, m) = t

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

1150

1160

1151lookupTotalExact :: Name -> Context -> Maybe Totality

1161lookupTotalExact :: Name -> Context -> Maybe Totality

1152lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1162lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1153− where mkt (d, inj, a, t, m) = t

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

1164+

1165+lookupRigCount :: Name -> Context -> [Totality]

1166+lookupRigCount n ctxt = map mkt $ lookupCtxt n (definitions ctxt)

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

1168+

1169+lookupRigCountExact :: Name -> Context -> Maybe RigCount

1170+lookupRigCountExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)

1171+ where mkt (d, rc, inj, a, t, m) = rc

1154

1172

1155lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

1173lookupInjectiveExact :: Name -> Context -> Maybe Injectivity

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

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

1157− where mkt (d, inj, a, t, m) = inj

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

1158

1176

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

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

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

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

@@ -1166,10 +1184,10 @@ tcReducible n ctxt = case lookupTotalExact n ctxt of

1166

1184

1167lookupMetaInformation :: Name -> Context -> [MetaInformation]

1185lookupMetaInformation :: Name -> Context -> [MetaInformation]

1168lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

1186lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)

1169− where mkm (d, inj, a, t, m) = m

1187+ where mkm (d, _, inj, a, t, m) = m

1170

1188

1171lookupNameTotal :: Name -> Context -> [(Name, Totality)]

1189lookupNameTotal :: Name -> Context -> [(Name, Totality)]

1172−lookupNameTotal n = map (\(n, (_, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

1190+lookupNameTotal n = map (\(n, (_, _, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions

1173

1191

1174

1192

1175lookupVal :: Name -> Context -> [Value]

1193lookupVal :: Name -> Context -> [Value]

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

@@ -111,11 +111,11 @@ check' holes tcns ctxt env top

111 Just msg -> lift $ tfail $ Msg msg

112 -- If we're elaborating, we don't want the private names; if we're

113 -- checking an already elaborated term, we do

114− | [P nt n' ty] <- lookupP_all (not holes) False n ctxt

115− = return (P nt n' ty, ty, [])

116− -- If the names are ambiguous, require it to be fully qualified

117 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

114 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

118 = return (P nt n' ty, ty, [])

115 = return (P nt n' ty, ty, [])

116+-- -- If the names are ambiguous, require it to be fully qualified

117+-- | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

118+-- = return (P nt n' ty, ty, [])

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

src/Idris/Elab/Clause.hs+11

@@ -14,6 +14,7 @@ import Idris.Core.CaseTree

14import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.Evaluate

16import Idris.Core.Execute

17+import Idris.Core.WHNF

17import Idris.Core.TT

18import Idris.Core.TT

18import Idris.Core.Typecheck

19import Idris.Core.Typecheck

19import Idris.Coverage

20import Idris.Coverage

@@ -286,6 +287,10 @@ elabClauses info' fc opts n_in cs =

286 Just Public -> mapM_ (checkVisibility fc n Public Public) calls

287 Just Public -> mapM_ (checkVisibility fc n Public Public) calls

287 _ -> return ()

288 _ -> return ()

288 addCalls n calls

289 addCalls n calls

290+ let rig = if linearArg (whnfArgs ctxt [] ty)

291+ then Rig1

292+ else RigW

293+ updateContext (setRigCount n (minRig ctxt rig calls))

289 addIBC (IBCCG n)

294 addIBC (IBCCG n)

290 _ -> return ()

295 _ -> return ()

291 return ()

296 return ()

@@ -378,6 +383,12 @@ elabClauses info' fc opts n_in cs =

378 Just t -> return t

383 Just t -> return t

379 Nothing -> ierror (At fc (Msg "No specialisation achieved"))

384 Nothing -> ierror (At fc (Msg "No specialisation achieved"))

380

385

386+ minRig :: Context -> RigCount -> [Name] -> RigCount

387+ minRig c minr [] = minr

388+ minRig c minr (r : rs) = case lookupRigCountExact r c of

389+ Nothing -> minRig c minr rs

390+ Just rc -> minRig c (min minr rc) rs

391+

381forceWith :: Ctxt OptInfo -> Term -> Term

392forceWith :: Ctxt OptInfo -> Term -> Term

382forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $

393forceWith opts lhs = -- trace (show lhs ++ "\n==>\n" ++ show (force lhs) ++ "\n----") $

383 force lhs

394 force lhs

src/Idris/Elab/Data.hs+3−4

@@ -120,6 +120,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

120 -- TMP HACK! Make this a data option

121 updateContext (addDatatype (Data n ttag cty unique cons))

122 updateContext (setMetaInformation n metainf)

123+ when (any linearArg (map snd cons)) $

124+ updateContext (setRigCount n Rig1)

125+

123 mapM_ totcheck (zip (repeat fc) (map fst cons))

126 mapM_ totcheck (zip (repeat fc) (map fst cons))

124-- mapM_ (checkPositive n) cons

127-- mapM_ (checkPositive n) cons

125

128

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

174 liftname = id -- Is this appropriate?

177 liftname = id -- Is this appropriate?

175 }

178 }

176

179

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

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

179− linearArg _ = False

180−

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

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

182 Type -> -- for unique kind checking

181 Type -> -- for unique kind checking

183 Type -> -- data type's kind

182 Type -> -- data type's kind

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

@@ -16,6 +16,7 @@ import Idris.ASTUtils

16import Idris.Core.CaseTree

17import Idris.Core.Elaborate hiding (Tactic(..))

18import Idris.Core.Evaluate

19+import Idris.Core.WHNF

19import Idris.Core.Execute

20import Idris.Core.Execute

20import Idris.Core.TT

21import Idris.Core.TT

21import Idris.Core.Typecheck

22import Idris.Core.Typecheck

@@ -132,6 +133,10 @@ buildType info syn fc opts n ty' = do

132 let fninfo = FnInfo (param_pos 0 pnames cty)

133 let fninfo = FnInfo (param_pos 0 pnames cty)

133 setFnInfo n fninfo

134 setFnInfo n fninfo

134 addIBC (IBCFnInfo n fninfo)

135 addIBC (IBCFnInfo n fninfo)

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)

135

140

136 return (cty, ckind, ty, inacc)

141 return (cty, ckind, ty, inacc)

137 where

142 where

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

181 let nty' = normalise ctxt [] nty

186 let nty' = normalise ctxt [] nty

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

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

183

188

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−

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

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

189 -- the name unambiguously)

190 -- the name unambiguously)

190 i <- getIState

191 i <- getIState

src/Idris/Elab/Utils.hs+15−7

@@ -602,16 +602,24 @@ setLinear ns tm = tm

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

603linearCheck fc t = do ist <- getIState

604 checkArgs ist t

605− where

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+

606 checkArgs ist (Bind n (Pi RigW _ ty _) sc)

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

607− | (P _ f _, _) <- unApply ty

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

608− = case lookupCtxtExact f (idris_datatypes ist) of

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

609− Just ti | linear_con ti ->

610− ierror $ At fc $

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

612− _ -> return ()

613 checkArgs ist (Bind n (Pi _ _ _ _) sc)

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

614 = checkArgs ist (substV (P Bound n Erased) sc)

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

615 checkArgs ist _ = return ()

618 checkArgs ist _ = return ()

616

619

620+linearArg :: Type -> Bool

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

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

623+linearArg _ = False

624+

617

625

src/Idris/IBC.hs+1−1

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

47import System.FilePath

49ibcVersion :: Word16

50−ibcVersion = 159

50+ibcVersion = 160

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

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

src/Idris/TypeSearch.hs+2−2

@@ -104,8 +104,8 @@ searchPred istate ty1 = matcher where

104 matcher = matchTypesBulk istate maxScore ty1

105

106

107−typeFromDef :: (Def, i, b, c, d) -> Maybe Type

107+typeFromDef :: (Def, r, i, b, c, d) -> Maybe Type

108−typeFromDef (def, _, _, _, _) = get def where

108+typeFromDef (def, _, _, _, _, _) = get def where

109 get :: Def -> Maybe Type

110 get (Function ty _) = Just ty

111 get (TyDecl _ ty) = Just ty