bc2bcb6 · Idris-dev · git.iko.soy

idris.cabal+4

compare with master

unifiedsplit

@@ -507,6 +507,10 @@ Extra-source-files:

507 test/tutorial006/*.idr

508 test/tutorial006/expected

509

510+ test/unique001/run

511+ test/unique001/*.idr

512+ test/unique001/expected

513+

510source-repository head

514source-repository head

511 type: git

515 type: git

512 location: git://github.com/idris-lang/Idris-dev.git

516 location: git://github.com/idris-lang/Idris-dev.git

libs/prelude/Builtins.idr+11

@@ -75,6 +75,17 @@ Lazy t = Lazy' LazyEval t

75Inf : Type -> Type

76Inf t = Lazy' LazyCodata t

77

78+namespace Ownership

79+ ||| A read-only version of a unique value

80+ data Borrowed : UniqueType -> NullType where

81+ Read : {a : UniqueType} -> a -> Borrowed a

82+

83+ ||| Make a read-only version of a unique value, which can be passed to another

84+ ||| function without the unique value being consumed.

85+ implicit

86+ lend : {a : UniqueType} -> a -> Borrowed a

87+ lend x = Read x

88+

78par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

89par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

79 -- is better in any case?

90 -- is better in any case?

80par (Delay x) = x

91par (Delay x) = x

rts/idris_rts.h+3−6

@@ -113,9 +113,6 @@ typedef void(*func)(VM*, VAL*);

113#define RVAL (vm->ret)

114#define LOC(x) (*(vm->valstack_base + (x)))

115#define TOP(x) (*(vm->valstack_top + (x)))

116−// Doesn't work! Ordinary assign seems fine though...

117−#define UPDATE(x,y) if (!ISINT(x) && !ISINT(y)) \

118− { (x)->ty = (y)->ty; (x)->info = (y)->info; }

119#define REG1 (vm->reg1)

116#define REG1 (vm->reg1)

120

117

121// Retrieving values

118// Retrieving values

@@ -125,8 +122,8 @@ typedef void(*func)(VM*, VAL*);

125#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

122#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

126#define GETFLOAT(x) (((VAL)(x))->info.f)

123#define GETFLOAT(x) (((VAL)(x))->info.f)

127

124

128−#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )

125+#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )

129−#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )

126+#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )

130

127

131// Already checked it's a CON

128// Already checked it's a CON

132#define CTAG(x) (((x)->info.c.tag_arity) >> 8)

129#define CTAG(x) (((x)->info.c.tag_arity) >> 8)

@@ -148,7 +145,7 @@ typedef intptr_t i_int;

148#define MKINT(x) ((void*)((x)<<1)+1)

145#define MKINT(x) ((void*)((x)<<1)+1)

149#define GETINT(x) ((i_int)(x)>>1)

146#define GETINT(x) ((i_int)(x)>>1)

150#define ISINT(x) ((((i_int)x)&1) == 1)

147#define ISINT(x) ((((i_int)x)&1) == 1)

151−#define ISSTR(x) (((VAL)(x))->ty == STRING)

148+#define ISSTR(x) (GETTY(x) == STRING)

152

149

153#define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))

150#define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))

154#define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))

151#define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))

src/Idris/Core/Binary.hs+2

@@ -285,10 +285,12 @@ instance Binary Universe where

285 put x = case x of

286 UniqueType -> putWord8 0

287 AllTypes -> putWord8 1

288+ NullType -> putWord8 2

288 get = do i <- getWord8

289 get = do i <- getWord8

289 case i of

290 case i of

290 0 -> return UniqueType

291 0 -> return UniqueType

291 1 -> return AllTypes

292 1 -> return AllTypes

293+ 2 -> return NullType

292 _ -> error "Corrupted binary data for Universe"

294 _ -> error "Corrupted binary data for Universe"

293

295

294instance Binary NameType where

296instance Binary NameType where

src/Idris/Core/Evaluate.hs+6−2

@@ -543,6 +543,10 @@ isUniverse (TType _) = True

543isUniverse (UType _) = True

544isUniverse _ = False

545

546+isUsableUniverse :: Term -> Bool

547+isUsableUniverse (UType NullType) = False

548+isUsableUniverse x = isUniverse x

549+

546convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

550convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

547

551

548convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

552convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

@@ -582,8 +586,8 @@ convEq ctxt holes topx topy = ceq [] topx topy where

582 ceq ps (TType x) (TType y) = do (v, cs) <- get

586 ceq ps (TType x) (TType y) = do (v, cs) <- get

583 put (v, ULE x y : cs)

587 put (v, ULE x y : cs)

584 return True

588 return True

585− ceq ps (UType AllTypes) x = return (isUniverse x)

589+ ceq ps (UType AllTypes) x = return (isUsableUniverse x)

586− ceq ps x (UType AllTypes) = return (isUniverse x)

590+ ceq ps x (UType AllTypes) = return (isUsableUniverse x)

587 ceq ps (UType u) (UType v) = return (u == v)

591 ceq ps (UType u) (UType v) = return (u == v)

588 ceq ps Erased _ = return True

592 ceq ps Erased _ = return True

589 ceq ps _ Erased = return True

593 ceq ps _ Erased = return True

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

@@ -139,8 +139,8 @@ data Err' t

139 | CantResolveAlts [Name]

140 | IncompleteTerm t

141 | UniverseError

142− | UniqueError Name

142+ | UniqueError Universe Name

143− | UniqueKindError Name

143+ | UniqueKindError Universe Name

144 | ProgramLineComment

145 | Inaccessible Name

146 | NonCollapsiblePostulate Name

@@ -599,11 +599,12 @@ constDocs (B32V v) = "A vector of thirty-two-bit values"

599constDocs (B64V v) = "A vector of sixty-four-bit values"

600constDocs prim = "Undocumented"

601

602−data Universe = UniqueType | AllTypes

602+data Universe = NullType | UniqueType | AllTypes

603 deriving (Eq, Ord)

604

605instance Show Universe where

606 show UniqueType = "UniqueType"

607+ show NullType = "NullType"

607 show AllTypes = "Type*"

608 show AllTypes = "Type*"

608

609

609data Raw = Var Name

610data Raw = Var Name

src/Idris/Core/Typecheck.hs+52−15

@@ -51,13 +51,17 @@ isType ctxt env tm = isType' (normalise ctxt env tm)

51 | otherwise = fail (showEnv env tm ++ " is not a Type")

52

53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

54+recheck = recheck_borrowing []

55+

56+recheck_borrowing :: [Name] -> Context -> Env -> Raw -> Term ->

57+ TC (Term, Type, UCs)

54−recheck ctxt env tm orig

58+recheck_borrowing bs ctxt env tm orig

55 = let v = next_tvar ctxt in

59 = let v = next_tvar ctxt in

56 case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

60 case runStateT (check' False ctxt env tm) (v, []) of -- holes banned

57 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

61 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

58 Error e -> Error e

62 Error e -> Error e

59 OK ((tm, ty), constraints) ->

63 OK ((tm, ty), constraints) ->

60− do checkUnique ctxt env tm

64+ do checkUnique bs ctxt env tm

61 return (tm, ty, constraints)

65 return (tm, ty, constraints)

62

66

63check :: Context -> Env -> Raw -> TC (Term, Type)

67check :: Context -> Env -> Raw -> TC (Term, Type)

@@ -127,12 +131,14 @@ check' holes ctxt env top = chk env top where

127 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

131 when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

128 return (Bind n (Pi (uniqueBinders (map fst env) sv))

132 return (Bind n (Pi (uniqueBinders (map fst env) sv))

129 (pToV n tv), TType (UVar v))

133 (pToV n tv), TType (UVar v))

130− (UType u, _) ->

134+ (u, u') ->

131− return (Bind n (Pi (uniqueBinders (map fst env) sv))

132− (pToV n tv), UType u)

133− (_, UType u) ->

134 return (Bind n (Pi (uniqueBinders (map fst env) sv))

135 return (Bind n (Pi (uniqueBinders (map fst env) sv))

135− (pToV n tv), UType u)

136+ (pToV n tv), smaller u u')

137+

138+ where smaller (UType NullType) _ = UType NullType

139+ smaller _ (UType NullType) = UType NullType

140+ smaller (UType u) _ = UType u

141+ smaller _ (UType u) = UType u

136 chk env (RBind n b sc)

142 chk env (RBind n b sc)

137 = do b' <- checkBinder b

143 = do b' <- checkBinder b

138 (scv, sct) <- chk ((n, b'):env) sc

144 (scv, sct) <- chk ((n, b'):env) sc

@@ -217,29 +223,57 @@ check' holes ctxt env top = chk env top where

217 discharge n (PVTy t) scv sct

223 discharge n (PVTy t) scv sct

218 = return (Bind n (PVTy t) scv, sct)

224 = return (Bind n (PVTy t) scv, sct)

219

225

226+-- Number of times a name can be used

227+data UniqueUse = Never -- no more times

228+ | Once -- at most once more

229+ | LendOnly -- only under 'lend'

230+ | Many -- unlimited

231+ deriving Eq

232+

220-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

233-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears

221-- in the scope more than once, this is an error.

234-- in the scope more than once, this is an error.

222−checkUnique :: Context -> Env -> Term -> TC ()

235+checkUnique :: [Name] -> Context -> Env -> Term -> TC ()

236+checkUnique borrowed ctxt env tm

223−checkUnique ctxt env tm = evalStateT (chkBinders env (explicitNames tm)) []

237+ = evalStateT (chkBinders env (explicitNames tm)) []

224 where

238 where

239+ isVar (P _ _ _) = True

240+ isVar (V _) = True

241+ isVar _ = False

242+

225− chkBinders :: Env -> Term -> StateT [(Name, Bool)] TC ()

243+ chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()

226 chkBinders env (V i) | length env > i = chkName (fst (env!!i))

244 chkBinders env (V i) | length env > i = chkName (fst (env!!i))

227 chkBinders env (P _ n _) = chkName n

245 chkBinders env (P _ n _) = chkName n

246+ -- 'lending' a unique or nulltype variable doesn't count as a use,

247+ -- but we still can't lend something that's already been used.

248+ chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)

249+ | isVar a && owner == txt "Ownership" &&

250+ (lend == txt "lend" || lend == txt "Read")

251+ = do chkBinders env t -- Check the type normally

252+ st <- get

253+ -- Remove the 'LendOnly' names from the unusable set

254+ put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)

255+ chkBinders env a

256+ put st -- Reset the old state after checking the argument

228 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

257 chkBinders env (App f a) = do chkBinders env f; chkBinders env a

229 chkBinders env (Bind n b t)

258 chkBinders env (Bind n b t)

230 = do chkBinderName env n b

259 = do chkBinderName env n b

231 chkBinders ((n, b) : env) t

260 chkBinders ((n, b) : env) t

232 chkBinders env t = return ()

261 chkBinders env t = return ()

233

262

234− chkBinderName :: Env -> Name -> Binder Term -> StateT [(Name, Bool)] TC ()

263+ chkBinderName :: Env -> Name -> Binder Term ->

264+ StateT [(Name, (UniqueUse, Universe))] TC ()

235 chkBinderName env n b

265 chkBinderName env n b

236 = do let rawty = forgetEnv (map fst env) (binderTy b)

266 = do let rawty = forgetEnv (map fst env) (binderTy b)

237 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

267 (_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?

238 case kind of

268 case kind of

239 UType UniqueType -> do ns <- get

269 UType UniqueType -> do ns <- get

240− put ((n, False) : ns)

270+ if n `elem` borrowed

271+ then put ((n, (LendOnly, NullType)) : ns)

272+ else put ((n, (Once, UniqueType)) : ns)

273+ UType NullType -> do ns <- get

274+ put ((n, (LendOnly, NullType)) : ns)

241 UType AllTypes -> do ns <- get

275 UType AllTypes -> do ns <- get

242− put ((n, False) : ns)

276+ put ((n, (Once, AllTypes)) : ns)

243 _ -> return ()

277 _ -> return ()

244 chkBinders env (binderTy b)

278 chkBinders env (binderTy b)

245 case b of

279 case b of

@@ -250,6 +284,9 @@ checkUnique ctxt env tm = evalStateT (chkBinders env (explicitNames tm)) []

250 = do ns <- get

284 = do ns <- get

251 case lookup n ns of

285 case lookup n ns of

252 Nothing -> return ()

286 Nothing -> return ()

287+ Just (Many, k) -> return ()

253− Just True -> lift $ tfail (UniqueError n)

288+ Just (Never, k) -> lift $ tfail (UniqueError k n)

289+ Just (LendOnly, k) -> lift $ tfail (UniqueError k n)

290+ Just (Once, k) -> put ((n, (Never, k)) :

254− Just False -> put ((n, True) : filter (\x -> fst x /= n) ns)

291+ filter (\x -> fst x /= n) ns)

255

292

src/Idris/Delaborate.hs+7−3

@@ -224,10 +224,14 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

224pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

225pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

226pprintErr' i UniverseError = text "Universe inconsistency"

227+pprintErr' i (UniqueError NullType n)

228+ = text "Borrowed name" <+> annName' n (showbasic n)

229+ <+> text "must not be used on RHS"

227−pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)

230+pprintErr' i (UniqueError _ n) = text "Unique name" <+> annName' n (showbasic n)

228 <+> text "is used more than once"

231 <+> text "is used more than once"

229−pprintErr' i (UniqueKindError n) = text "Constructor" <+> annName' n (showbasic n)

232+pprintErr' i (UniqueKindError k n) = text "Constructor" <+> annName' n (showbasic n)

233+ <+> text ("has a " ++ show k ++ ",")

230− <+> text "has a UniqueType, but the data type deos not"

234+ <+> text "but the data type does not"

231pprintErr' i ProgramLineComment = text "Program line next to comment"

235pprintErr' i ProgramLineComment = text "Program line next to comment"

232pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

236pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

233pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

237pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

src/Idris/Elab/Clause.hs+25−1

@@ -499,6 +499,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

499 then recheckC fc [] lhs_tm

500 else return (lhs_tm, lhs_ty)

501 let clhs = normalise ctxt [] clhs_c

502+ let borrowed = borrowedNames [] clhs

503+

504+ -- These are the names we're not allowed to use on the RHS, because

505+ -- they're UniqueTypes and borrowed from another function.

506+ -- FIXME: There is surely a nicer way than this...

507+ when (not (null borrowed)) $

508+ logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)

502

509

503 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

510 logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

504

511

@@ -572,8 +579,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

572 ctxt <- getContext

579 ctxt <- getContext

573 logLvl 5 $ "Rechecking"

580 logLvl 5 $ "Rechecking"

574 logLvl 6 $ " ==> " ++ show (forget rhs')

581 logLvl 6 $ " ==> " ++ show (forget rhs')

582+

575 (crhs, crhsty) <- if not inf

583 (crhs, crhsty) <- if not inf

576− then recheckC fc [] rhs'

584+ then recheckC_borrowing borrowed fc [] rhs'

577 else return (rhs', clhsty)

585 else return (rhs', clhsty)

578 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

586 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

579 case converts ctxt [] clhsty crhsty of

587 case converts ctxt [] clhsty crhsty of

@@ -610,6 +618,22 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

610 -- _ -> MN i (show n)) . l

618 -- _ -> MN i (show n)) . l

611 }

619 }

612

620

621+ -- Find the variable names which appear under a 'Ownership.Read' so that

622+ -- we know they can't be used on the RHS

623+ borrowedNames :: [Name] -> Term -> [Name]

624+ borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)

625+ | owner == txt "Ownership" &&

626+ (lend == txt "lend" || lend == txt "Read") = getVs arg

627+ where

628+ getVs (V i) = [env!!i]

629+ getVs (App f a) = nub $ getVs f ++ getVs a

630+ getVs _ = []

631+ borrowedNames env (App f a) = nub $ borrowedNames env f ++ borrowedNames env a

632+ borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc

633+ where borrowedB (Let t v) = nub $ borrowedNames env t ++ borrowedNames env v

634+ borrowedB b = borrowedNames env (binderTy b)

635+ borrowedNames _ _ = []

636+

613 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

637 mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []

614 mkLHSapp t = t

638 mkLHSapp t = t

615

639

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

@@ -258,10 +258,13 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

258

259 -- if the constructor is a UniqueType, the datatype must be too

260 -- (Type* is fine, since that is checked for uniqueness too)

261+ checkUniqueKind (UType NullType) (UType NullType) = return ()

262+ checkUniqueKind (UType NullType) _

263+ = tclift $ tfail (At fc (UniqueKindError NullType n))

261 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()

264 checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()

262 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()

265 checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()

263 checkUniqueKind (UType UniqueType) (TType _)

266 checkUniqueKind (UType UniqueType) (TType _)

264− = tclift $ tfail (At fc (UniqueKindError n))

267+ = tclift $ tfail (At fc (UniqueKindError UniqueType n))

265 checkUniqueKind (UType AllTypes) _ = return ()

268 checkUniqueKind (UType AllTypes) _ = return ()

266 checkUniqueKind (TType _) _ = return ()

269 checkUniqueKind (TType _) _ = return ()

267

270

src/Idris/Elab/Utils.hs+4−2

@@ -20,10 +20,12 @@ import Debug.Trace

20

21import qualified Data.Map as Map

22

23−recheckC fc env t

23+recheckC = recheckC_borrowing []

24+

25+recheckC_borrowing bs fc env t

24 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

26 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

25 ctxt <- getContext

27 ctxt <- getContext

26− (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of

28+ (tm, ty, cs) <- tclift $ case recheck_borrowing bs ctxt env (forget t) t of

27 Error e -> tfail (At fc e)

29 Error e -> tfail (At fc e)

28 OK x -> return x

30 OK x -> return x

29 addConstraints fc cs

31 addConstraints fc cs

src/Idris/ParseExpr.hs+1

@@ -310,6 +310,7 @@ simpleExpr syn =

310 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

311 <|> do reserved "Type"; return PType

312 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

313+ <|> do reserved "NullType"; return $ PUniverse NullType

313 <|> do c <- constant

314 <|> do c <- constant

314 fc <- getFC

315 fc <- getFC

315 return (modifyConst syn fc (PConstant c))

316 return (modifyConst syn fc (PConstant c))

test/unique001/expectednew file+8

@@ -0,0 +1,8 @@

1+19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

2+19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END

3+38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END

4+unique001a.idr:23:11:Unique name xs is used more than once

5+unique001b.idr:16:7:Borrowed name xs must not be used on RHS

6+unique001c.idr:49:6:Unique name f is used more than once

7+unique001d.idr:3:7:Borrowed name x must not be used on RHS

8+unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

test/unique001/runnew file+9

@@ -0,0 +1,9 @@

1+#!/usr/bin/env bash

2+idris $@ unique001.idr -o unique001

3+./unique001

4+idris $@ unique001a.idr --check

5+idris $@ unique001b.idr --check

6+idris $@ unique001c.idr --check

7+idris $@ unique001d.idr --check

8+idris $@ unique001e.idr --check

9+rm -f unique001 *.ibc

test/unique001/unique001.idrnew file+31

@@ -0,0 +1,31 @@

1+module Main

2+

3+data UList : Type -> UniqueType where

4+ Nil : UList a

5+ (::) : a -> UList a -> UList a

6+

7+umap : (a -> b) -> UList a -> UList b

8+umap f [] = []

9+umap f (x :: xs) = f x :: umap f xs

10+

11+free : {a : UniqueType} -> a -> String

12+free xs = ""

13+

14+showU : Show a => Borrowed (UList a) -> String

15+showU [] = "END"

16+showU (x :: xs) = show x ++ "," ++ showU xs

17+

18+mkUList : Nat -> UList Int

19+mkUList Z = []

20+mkUList (S k) = cast k :: mkUList k

21+

22+showStuff : UList Int -> IO ()

23+showStuff xs = do

24+ putStrLn (showU xs)

25+ putStrLn (showU xs)

26+ let xs' = umap (*2) xs

27+ putStrLn (showU xs')

28+

29+main : IO ()

30+main = showStuff (mkUList 20)

31+

test/unique001/unique001a.idrnew file+31

@@ -0,0 +1,31 @@

1+module Main

2+

3+data UList : Type -> UniqueType where

4+ Nil : UList a

5+ (::) : a -> UList a -> UList a

6+

7+umap : (a -> b) -> UList a -> UList b

8+umap f [] = []

9+umap f (x :: xs) = f x :: umap f xs

10+

11+free : {a : UniqueType} -> a -> String

12+free xs = ""

13+

14+showU : Show a => Borrowed (UList a) -> String

15+showU [] = "END"

16+showU (x :: xs) = show x ++ "," ++ showU xs

17+

18+mkUList : Nat -> UList Int

19+mkUList Z = []

20+mkUList (S k) = cast k :: mkUList k

21+

22+showStuff : UList Int -> IO ()

23+showStuff xs = do

24+ putStrLn (showU xs)

25+ let xs' = umap (*2) xs

26+ putStrLn (showU xs)

27+ putStrLn (showU xs')

28+

29+main : IO ()

30+main = showStuff (mkUList 20)

31+

test/unique001/unique001b.idrnew file+30

@@ -0,0 +1,30 @@

1+module Main

2+

3+data UList : Type -> UniqueType where

4+ Nil : UList a

5+ (::) : a -> UList a -> UList a

6+

7+umap : (a -> b) -> UList a -> UList b

8+umap f [] = []

9+umap f (x :: xs) = f x :: umap f xs

10+

11+free : {a : UniqueType} -> a -> String

12+free xs = ""

13+

14+showU : Show a => Borrowed (UList a) -> String

15+showU [] = "END"

16+showU (x :: xs) = show x ++ "," ++ free xs

17+

18+mkUList : Nat -> UList Int

19+mkUList Z = []

20+mkUList (S k) = cast k :: mkUList k

21+

22+showStuff : UList Int -> IO ()

23+showStuff xs = do

24+ putStrLn (showU xs)

25+ let xs' = umap (*2) xs

26+ putStrLn (showU xs')

27+

28+main : IO ()

29+main = showStuff (mkUList 20)

30+

test/unique001/unique001c.idrnew file+53

@@ -0,0 +1,53 @@

1+

2+data UList : Type -> UniqueType where

3+ UNil : UList a

4+ UCons : {a : Type} -> a -> UList a -> UList a

5+

6+uapp : UList a -> UList a -> UList a

7+uapp UNil xs = xs

8+uapp (UCons x xs) ys = UCons x (UCons x (uapp xs ys))

9+

10+data UTree : UniqueType where

11+ ULeaf : UTree

12+ UNode : UTree -> Int -> UTree -> UTree

13+

14+data UPair : UniqueType -> UniqueType -> UniqueType where

15+ MkUPair : {a,b:UniqueType} -> a -> b -> UPair a b

16+

17+dup : UTree -> UPair UTree UTree

18+dup ULeaf = MkUPair ULeaf ULeaf

19+dup (UNode l y r) = let MkUPair l1 l2 = dup l

20+ MkUPair r1 r2 = dup r in

21+ MkUPair (UNode l1 y r1) (UNode l2 y r2)

22+

23+data Tree : Type where

24+ Leaf : Tree

25+ Node : Tree -> Int -> Tree -> Tree

26+

27+share : UTree -> Tree

28+share ULeaf = Leaf

29+share (UNode x y z) = Node (share x) y (share z)

30+

31+class UFunctor (f : Type -> Type*) where

32+ fmap : (a -> b) -> f a -> f b

33+

34+instance UFunctor List where

35+ fmap f [] = []

36+ fmap f (x :: xs) = f x :: fmap f xs

37+

38+instance UFunctor UList where

39+ fmap f UNil = UNil

40+ fmap f (UCons x xs) = UCons (f x) (fmap f xs)

41+

42+uconst : {a : Type*} -> a -> b -> a

43+uconst x y = x

44+

45+data MPair : Type* -> Type* -> Type* where

46+ MkMPair : {a, b : Type*} -> a -> b -> MPair a b

47+

48+ndup : {a : UniqueType} -> a -> UPair a a

49+ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

50+

51+

52+

53+

test/unique001/unique001d.idrnew file+3

@@ -0,0 +1,3 @@

1+

2+steal : {a : UniqueType} -> Borrowed a -> a

3+steal x = x