ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 03:34:13 +03:00
Code Issues Projects Releases Wiki Activity

Add Borrowed types

Browse Source 
This allows unique values to be inspected, but not updated or
destroyed. A 'Borrowed' value can be pattern matched, but cannot be used
on the right hand side, nor can any Unique values contained in the
pattern.
This commit is contained in:
Edwin Brady 2014-08-21 22:38:58 +01:00
parent f2a90991f8
commit bc2bcb65ca
19 changed files with 288 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
idris.cabal
View File

@ -507,6 +507,10 @@ Extra-source-files:
test/tutorial006/*.idr
test/tutorial006/expected
test/unique001/run
test/unique001/*.idr
test/unique001/expected
source-repository head
type: git
location: git://github.com/idris-lang/Idris-dev.git

11
libs/prelude/Builtins.idr
View File

@ -75,6 +75,17 @@ Lazy t = Lazy' LazyEval t
Inf : Type -> Type
Inf t = Lazy' LazyCodata t
namespace Ownership
||| A read-only version of a unique value
data Borrowed : UniqueType -> NullType where
Read : {a : UniqueType} -> a -> Borrowed a
||| Make a read-only version of a unique value, which can be passed to another
||| function without the unique value being consumed.
implicit
lend : {a : UniqueType} -> a -> Borrowed a
lend x = Read x
par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
-- is better in any case?
par (Delay x) = x

9
rts/idris_rts.h
View File

@ -113,9 +113,6 @@ typedef void(*func)(VM*, VAL*);
#define RVAL (vm->ret)
#define LOC(x) (*(vm->valstack_base + (x)))
#define TOP(x) (*(vm->valstack_top + (x)))
// Doesn't work! Ordinary assign seems fine though...
#define UPDATE(x,y) if (!ISINT(x) && !ISINT(y)) \
{ (x)->ty = (y)->ty; (x)->info = (y)->info; }
#define REG1 (vm->reg1)
// Retrieving values
@ -125,8 +122,8 @@ typedef void(*func)(VM*, VAL*);
#define GETMPTR(x) (((VAL)(x))->info.mptr->data)
#define GETFLOAT(x) (((VAL)(x))->info.f)
#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )
#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( (x)->ty == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )
#define TAG(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity >> 8 : (-1)) )
#define ARITY(x) (ISINT(x) || x == NULL ? (-1) : ( GETTY(x) == CON ? (x)->info.c.tag_arity & 0x000000ff : (-1)) )
// Already checked it's a CON
#define CTAG(x) (((x)->info.c.tag_arity) >> 8)
@ -148,7 +145,7 @@ typedef intptr_t i_int;
#define MKINT(x) ((void*)((x)<<1)+1)
#define GETINT(x) ((i_int)(x)>>1)
#define ISINT(x) ((((i_int)x)&1) == 1)
#define ISSTR(x) (((VAL)(x))->ty == STRING)
#define ISSTR(x) (GETTY(x) == STRING)
#define INTOP(op,x,y) MKINT((i_int)((((i_int)x)>>1) op (((i_int)y)>>1)))
#define UINTOP(op,x,y) MKINT((i_int)((((uintptr_t)x)>>1) op (((uintptr_t)y)>>1)))

2
src/Idris/Core/Binary.hs
View File

@ -285,10 +285,12 @@ instance Binary Universe where
put x = case x of
UniqueType -> putWord8 0
AllTypes -> putWord8 1
NullType -> putWord8 2
get = do i <- getWord8
case i of
0 -> return UniqueType
1 -> return AllTypes
2 -> return NullType
_ -> error "Corrupted binary data for Universe"
instance Binary NameType where

8
src/Idris/Core/Evaluate.hs
View File

@ -543,6 +543,10 @@ isUniverse (TType _) = True
isUniverse (UType _) = True
isUniverse _ = False
isUsableUniverse :: Term -> Bool
isUsableUniverse (UType NullType) = False
isUsableUniverse x = isUniverse x
convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])
convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool
@ -582,8 +586,8 @@ convEq ctxt holes topx topy = ceq [] topx topy where
ceq ps (TType x) (TType y) = do (v, cs) <- get
put (v, ULE x y : cs)
return True
ceq ps (UType AllTypes) x = return (isUniverse x)
ceq ps x (UType AllTypes) = return (isUniverse x)
ceq ps (UType AllTypes) x = return (isUsableUniverse x)
ceq ps x (UType AllTypes) = return (isUsableUniverse x)
ceq ps (UType u) (UType v) = return (u == v)
ceq ps Erased _ = return True
ceq ps _ Erased = return True

7
src/Idris/Core/TT.hs
View File

@ -139,8 +139,8 @@ data Err' t
| CantResolveAlts [Name]
| IncompleteTerm t
| UniverseError
| UniqueError Name
| UniqueKindError Name
| UniqueError Universe Name
| UniqueKindError Universe Name
| ProgramLineComment
| Inaccessible Name
| NonCollapsiblePostulate Name
@ -599,11 +599,12 @@ constDocs (B32V v) = "A vector of thirty-two-bit values"
constDocs (B64V v) = "A vector of sixty-four-bit values"
constDocs prim = "Undocumented"
data Universe = UniqueType | AllTypes
data Universe = NullType | UniqueType | AllTypes
deriving (Eq, Ord)
instance Show Universe where
show UniqueType = "UniqueType"
show NullType = "NullType"
show AllTypes = "Type*"
data Raw = Var Name

67
src/Idris/Core/Typecheck.hs
View File

@ -51,13 +51,17 @@ isType ctxt env tm = isType' (normalise ctxt env tm)
| otherwise = fail (showEnv env tm ++ " is not a Type")
recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)
recheck ctxt env tm orig
recheck = recheck_borrowing []
recheck_borrowing :: [Name] -> Context -> Env -> Raw -> Term ->
TC (Term, Type, UCs)
recheck_borrowing bs ctxt env tm orig
= let v = next_tvar ctxt in
case runStateT (check' False ctxt env tm) (v, []) of -- holes banned
Error (IncompleteTerm _) -> Error $ IncompleteTerm orig
Error e -> Error e
OK ((tm, ty), constraints) ->
do checkUnique ctxt env tm
do checkUnique bs ctxt env tm
return (tm, ty, constraints)
check :: Context -> Env -> Raw -> TC (Term, Type)
@ -127,12 +131,14 @@ check' holes ctxt env top = chk env top where
when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)
return (Bind n (Pi (uniqueBinders (map fst env) sv))
(pToV n tv), TType (UVar v))
(UType u, _) ->
(u, u') ->
return (Bind n (Pi (uniqueBinders (map fst env) sv))
(pToV n tv), UType u)
(_, UType u) ->
return (Bind n (Pi (uniqueBinders (map fst env) sv))
(pToV n tv), UType u)
(pToV n tv), smaller u u')
where smaller (UType NullType) _ = UType NullType
smaller _ (UType NullType) = UType NullType
smaller (UType u) _ = UType u
smaller _ (UType u) = UType u
chk env (RBind n b sc)
= do b' <- checkBinder b
(scv, sct) <- chk ((n, b'):env) sc
@ -217,29 +223,57 @@ check' holes ctxt env top = chk env top where
discharge n (PVTy t) scv sct
= return (Bind n (PVTy t) scv, sct)
-- Number of times a name can be used
data UniqueUse = Never -- no more times
| Once -- at most once more
| LendOnly -- only under 'lend'
| Many -- unlimited
deriving Eq
-- If any binders are of kind 'UniqueType' or 'AllTypes' and the name appears
-- in the scope more than once, this is an error.
checkUnique :: Context -> Env -> Term -> TC ()
checkUnique ctxt env tm = evalStateT (chkBinders env (explicitNames tm)) []
checkUnique :: [Name] -> Context -> Env -> Term -> TC ()
checkUnique borrowed ctxt env tm
= evalStateT (chkBinders env (explicitNames tm)) []
where
chkBinders :: Env -> Term -> StateT [(Name, Bool)] TC ()
isVar (P _ _ _) = True
isVar (V _) = True
isVar _ = False
chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinders env (V i) | length env > i = chkName (fst (env!!i))
chkBinders env (P _ n _) = chkName n
-- 'lending' a unique or nulltype variable doesn't count as a use,
-- but we still can't lend something that's already been used.
chkBinders env (App (App (P _ (NS (UN lend) [owner]) _) t) a)
| isVar a && owner == txt "Ownership" &&
(lend == txt "lend" || lend == txt "Read")
= do chkBinders env t -- Check the type normally
st <- get
-- Remove the 'LendOnly' names from the unusable set
put (filter (\(n, (ok, _)) -> ok /= LendOnly) st)
chkBinders env a
put st -- Reset the old state after checking the argument
chkBinders env (App f a) = do chkBinders env f; chkBinders env a
chkBinders env (Bind n b t)
= do chkBinderName env n b
chkBinders ((n, b) : env) t
chkBinders env t = return ()
chkBinderName :: Env -> Name -> Binder Term -> StateT [(Name, Bool)] TC ()
chkBinderName :: Env -> Name -> Binder Term ->
StateT [(Name, (UniqueUse, Universe))] TC ()
chkBinderName env n b
= do let rawty = forgetEnv (map fst env) (binderTy b)
(_, kind) <- lift $ check ctxt env rawty -- FIXME: Cache in binder?
case kind of
UType UniqueType -> do ns <- get
put ((n, False) : ns)
if n `elem` borrowed
then put ((n, (LendOnly, NullType)) : ns)
else put ((n, (Once, UniqueType)) : ns)
UType NullType -> do ns <- get
put ((n, (LendOnly, NullType)) : ns)
UType AllTypes -> do ns <- get
put ((n, False) : ns)
put ((n, (Once, AllTypes)) : ns)
_ -> return ()
chkBinders env (binderTy b)
case b of
@ -250,6 +284,9 @@ checkUnique ctxt env tm = evalStateT (chkBinders env (explicitNames tm)) []
= do ns <- get
case lookup n ns of
Nothing -> return ()
Just True -> lift $ tfail (UniqueError n)
Just False -> put ((n, True) : filter (\x -> fst x /= n) ns)
Just (Many, k) -> return ()
Just (Never, k) -> lift $ tfail (UniqueError k n)
Just (LendOnly, k) -> lift $ tfail (UniqueError k n)
Just (Once, k) -> put ((n, (Never, k)) :
filter (\x -> fst x /= n) ns)

10
src/Idris/Delaborate.hs
View File

@ -224,10 +224,14 @@ pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))
pprintErr' i UniverseError = text "Universe inconsistency"
pprintErr' i (UniqueError n) = text "Unique name" <+> annName' n (showbasic n)
pprintErr' i (UniqueError NullType n)
= text "Borrowed name" <+> annName' n (showbasic n)
<+> text "must not be used on RHS"
pprintErr' i (UniqueError _ n) = text "Unique name" <+> annName' n (showbasic n)
<+> text "is used more than once"
pprintErr' i (UniqueKindError n) = text "Constructor" <+> annName' n (showbasic n)
<+> text "has a UniqueType, but the data type deos not"
pprintErr' i (UniqueKindError k n) = text "Constructor" <+> annName' n (showbasic n)
<+> text ("has a " ++ show k ++ ",")
<+> text "but the data type does not"
pprintErr' i ProgramLineComment = text "Program line next to comment"
pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

26
src/Idris/Elab/Clause.hs
View File

@ -499,6 +499,13 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
then recheckC fc [] lhs_tm
else return (lhs_tm, lhs_ty)
let clhs = normalise ctxt [] clhs_c
let borrowed = borrowedNames [] clhs
-- These are the names we're not allowed to use on the RHS, because
-- they're UniqueTypes and borrowed from another function.
-- FIXME: There is surely a nicer way than this...
when (not (null borrowed)) $
logLvl 5 ("Borrowed names on LHS: " ++ show borrowed)
logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
@ -572,8 +579,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
ctxt <- getContext
logLvl 5 $ "Rechecking"
logLvl 6 $ " ==> " ++ show (forget rhs')
(crhs, crhsty) <- if not inf
then recheckC fc [] rhs'
then recheckC_borrowing borrowed fc [] rhs'
else return (rhs', clhsty)
logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
case converts ctxt [] clhsty crhsty of
@ -610,6 +618,22 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
-- _ -> MN i (show n)) . l
}
-- Find the variable names which appear under a 'Ownership.Read' so that
-- we know they can't be used on the RHS
borrowedNames :: [Name] -> Term -> [Name]
borrowedNames env (App (App (P _ (NS (UN lend) [owner]) _) _) arg)
| owner == txt "Ownership" &&
(lend == txt "lend" || lend == txt "Read") = getVs arg
where
getVs (V i) = [env!!i]
getVs (App f a) = nub $ getVs f ++ getVs a
getVs _ = []
borrowedNames env (App f a) = nub $ borrowedNames env f ++ borrowedNames env a
borrowedNames env (Bind n b sc) = nub $ borrowedB b ++ borrowedNames (n:env) sc
where borrowedB (Let t v) = nub $ borrowedNames env t ++ borrowedNames env v
borrowedB b = borrowedNames env (binderTy b)
borrowedNames _ _ = []
mkLHSapp t@(PRef _ _) = trace ("APP " ++ show t) $ PApp fc t []
mkLHSapp t = t

5
src/Idris/Elab/Data.hs
View File

@ -258,10 +258,13 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
-- if the constructor is a UniqueType, the datatype must be too
-- (Type* is fine, since that is checked for uniqueness too)
checkUniqueKind (UType NullType) (UType NullType) = return ()
checkUniqueKind (UType NullType) _
= tclift $ tfail (At fc (UniqueKindError NullType n))
checkUniqueKind (UType UniqueType) (UType UniqueType) = return ()
checkUniqueKind (UType UniqueType) (UType AllTypes) = return ()
checkUniqueKind (UType UniqueType) (TType _)
= tclift $ tfail (At fc (UniqueKindError n))
= tclift $ tfail (At fc (UniqueKindError UniqueType n))
checkUniqueKind (UType AllTypes) _ = return ()
checkUniqueKind (TType _) _ = return ()

6
src/Idris/Elab/Utils.hs
View File

@ -20,10 +20,12 @@ import Debug.Trace
import qualified Data.Map as Map
recheckC fc env t
recheckC = recheckC_borrowing []
recheckC_borrowing bs fc env t
= do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
ctxt <- getContext
(tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
(tm, ty, cs) <- tclift $ case recheck_borrowing bs ctxt env (forget t) t of
Error e -> tfail (At fc e)
OK x -> return x
addConstraints fc cs

1
src/Idris/ParseExpr.hs
View File

@ -310,6 +310,7 @@ simpleExpr syn =
<|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)
<|> do reserved "Type"; return PType
<|> do reserved "UniqueType"; return $ PUniverse UniqueType
<|> do reserved "NullType"; return $ PUniverse NullType
<|> do c <- constant
fc <- getFC
return (modifyConst syn fc (PConstant c))

8
test/unique001/expected Normal file
View File

@ -0,0 +1,8 @@
19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
19,18,17,16,15,14,13,12,11,10,9,8,7,6,5,4,3,2,1,0,END
38,36,34,32,30,28,26,24,22,20,18,16,14,12,10,8,6,4,2,0,END
unique001a.idr:23:11:Unique name xs is used more than once
unique001b.idr:16:7:Borrowed name xs must not be used on RHS
unique001c.idr:49:6:Unique name f is used more than once
unique001d.idr:3:7:Borrowed name x must not be used on RHS
unique001e.idr:4:11:Constructor Main.:: has a UniqueType, but the data type does not

9
test/unique001/run Executable file
View File

@ -0,0 +1,9 @@
#!/usr/bin/env bash
idris $@ unique001.idr -o unique001
./unique001
idris $@ unique001a.idr --check
idris $@ unique001b.idr --check
idris $@ unique001c.idr --check
idris $@ unique001d.idr --check
idris $@ unique001e.idr --check
rm -f unique001 *.ibc

31
test/unique001/unique001.idr Normal file
View File

@ -0,0 +1,31 @@
module Main
data UList : Type -> UniqueType where
Nil : UList a
(::) : a -> UList a -> UList a
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
free : {a : UniqueType} -> a -> String
free xs = ""
showU : Show a => Borrowed (UList a) -> String
showU [] = "END"
showU (x :: xs) = show x ++ "," ++ showU xs
mkUList : Nat -> UList Int
mkUList Z = []
mkUList (S k) = cast k :: mkUList k
showStuff : UList Int -> IO ()
showStuff xs = do
putStrLn (showU xs)
putStrLn (showU xs)
let xs' = umap (*2) xs
putStrLn (showU xs')
main : IO ()
main = showStuff (mkUList 20)

31
test/unique001/unique001a.idr Normal file
View File

@ -0,0 +1,31 @@
module Main
data UList : Type -> UniqueType where
Nil : UList a
(::) : a -> UList a -> UList a
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
free : {a : UniqueType} -> a -> String
free xs = ""
showU : Show a => Borrowed (UList a) -> String
showU [] = "END"
showU (x :: xs) = show x ++ "," ++ showU xs
mkUList : Nat -> UList Int
mkUList Z = []
mkUList (S k) = cast k :: mkUList k
showStuff : UList Int -> IO ()
showStuff xs = do
putStrLn (showU xs)
let xs' = umap (*2) xs
putStrLn (showU xs)
putStrLn (showU xs')
main : IO ()
main = showStuff (mkUList 20)

30
test/unique001/unique001b.idr Normal file
View File

@ -0,0 +1,30 @@
module Main
data UList : Type -> UniqueType where
Nil : UList a
(::) : a -> UList a -> UList a
umap : (a -> b) -> UList a -> UList b
umap f [] = []
umap f (x :: xs) = f x :: umap f xs
free : {a : UniqueType} -> a -> String
free xs = ""
showU : Show a => Borrowed (UList a) -> String
showU [] = "END"
showU (x :: xs) = show x ++ "," ++ free xs
mkUList : Nat -> UList Int
mkUList Z = []
mkUList (S k) = cast k :: mkUList k
showStuff : UList Int -> IO ()
showStuff xs = do
putStrLn (showU xs)
let xs' = umap (*2) xs
putStrLn (showU xs')
main : IO ()
main = showStuff (mkUList 20)

53
test/unique001/unique001c.idr Normal file
View File

@ -0,0 +1,53 @@
data UList : Type -> UniqueType where
UNil : UList a
UCons : {a : Type} -> a -> UList a -> UList a
uapp : UList a -> UList a -> UList a
uapp UNil xs = xs
uapp (UCons x xs) ys = UCons x (UCons x (uapp xs ys))
data UTree : UniqueType where
ULeaf : UTree
UNode : UTree -> Int -> UTree -> UTree
data UPair : UniqueType -> UniqueType -> UniqueType where
MkUPair : {a,b:UniqueType} -> a -> b -> UPair a b
dup : UTree -> UPair UTree UTree
dup ULeaf = MkUPair ULeaf ULeaf
dup (UNode l y r) = let MkUPair l1 l2 = dup l
MkUPair r1 r2 = dup r in
MkUPair (UNode l1 y r1) (UNode l2 y r2)
data Tree : Type where
Leaf : Tree
Node : Tree -> Int -> Tree -> Tree
share : UTree -> Tree
share ULeaf = Leaf
share (UNode x y z) = Node (share x) y (share z)
class UFunctor (f : Type -> Type*) where
fmap : (a -> b) -> f a -> f b
instance UFunctor List where
fmap f [] = []
fmap f (x :: xs) = f x :: fmap f xs
instance UFunctor UList where
fmap f UNil = UNil
fmap f (UCons x xs) = UCons (f x) (fmap f xs)
uconst : {a : Type*} -> a -> b -> a
uconst x y = x
data MPair : Type* -> Type* -> Type* where
MkMPair : {a, b : Type*} -> a -> b -> MPair a b
ndup : {a : UniqueType} -> a -> UPair a a
ndup {a} x = (\f : Int -> a => MkUPair (f 0) (f 1)) (uconst x)

3
test/unique001/unique001d.idr Normal file
View File

@ -0,0 +1,3 @@
steal : {a : UniqueType} -> Borrowed a -> a
steal x = x