c55895d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix universe errors, update tests

commitc55895d70520b9d6ed89e6c7d577cdd758b703aa authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Aug 2014, 20:31 (12 years ago) parent7e7368d

10 files changed+64−17

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Core/Typecheck.hs+4−4 src/Idris/ElabDecls.hs+7−7 src/Idris/Primitives.hs+1−1 test/quasiquote001/expected+3−3 test/unique001/expected+13−1 test/unique002/expected+4−1 test/unique003/expected+4 test/unique003/run+3 test/unique003/unique003.idr+22

idris.cabal+3

@@ -513,6 +513,9 @@ Extra-source-files:

513513 test/unique002/run

514514 test/unique002/*.idr

515515 test/unique002/expected

516+ test/unique003/run

517+ test/unique003/*.idr

518+ test/unique003/expected

516519

517520source-repository head

518521 type: git

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

@@ -69,7 +69,7 @@ check ctxt env tm

6969 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

7070

7171check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

72−check' holes ctxt env top = chk (TType (UVar 0)) env top where

72+check' holes ctxt env top = chk (TType (UVar (-5))) env top where

7373

7474 smaller (UType NullType) _ = UType NullType

7575 smaller _ (UType NullType) = UType NullType

@@ -140,11 +140,11 @@ check' holes ctxt env top = chk (TType (UVar 0)) env top where

140140 case (normalise ctxt env st, normalise ctxt env tt) of

141141 (TType su, TType tu) -> do

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

143− let k' = u `smaller` st `smaller` kv `smaller` TType (UVar v)

143+ let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u

144144 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

145145 (pToV n tv), k')

146146 (un, un') ->

147− let k' = u `smaller` st `smaller` kv `smaller` un `smaller` un' in

147+ let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in

148148 return (Bind n (Pi (uniqueBinders (map fst env) sv) k')

149149 (pToV n tv), k')

150150

@@ -284,11 +284,11 @@ checkUnique borrowed ctxt env tm

284284 -- Must be safe whether we evaluate the scope or binder first

285285 -- (Surely there is a tidier rule than this...?)

286286 st <- get

287− chkBinders ((n, b) : env) t

288287 chkBinders env (binderTy b)

289288 case b of

290289 Let t v -> chkBinders env v

291290 _ -> return ()

291+ chkBinders ((n, b) : env) t

292292-- put st

293293-- chkBinders env (binderTy b)

294294-- case b of

src/Idris/ElabDecls.hs+7−7

@@ -103,9 +103,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

103103

104104 p_believeMe [_,_,x] = Just x

105105 p_believeMe _ = Nothing

106− believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))) (TType (UVar 0)))

107− (Bind (sUN "b") (Pi (TType (UVar (-2))) (TType (UVar 0)))

108− (Bind (sUN "x") (Pi (V 1) (TType (UVar 0))) (V 1)))

106+ believeTy = Bind (sUN "a") (Pi (TType (UVar (-2))) (TType (UVar (-1))))

107+ (Bind (sUN "b") (Pi (TType (UVar (-2))) (TType (UVar (-1))))

108+ (Bind (sUN "x") (Pi (V 1) (TType (UVar (-1)))) (V 1)))

109109 elabBelieveMe

110110 = do let prim__believe_me = sUN "prim__believe_me"

111111 updateContext (addOperator prim__believe_me believeTy 3 p_believeMe)

@@ -126,10 +126,10 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

126126 vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

127127 vnRefl = VP (DCon 0 2 False) eqCon VErased

128128

129− synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))) (TType (UVar 0)))

130− (Bind (sUN "b") (Pi (TType (UVar (-3))) (TType (UVar 0)))

131− (Bind (sUN "x") (Pi (V 1) (TType (UVar 0)))

132− (Bind (sUN "y") (Pi (V 1) (TType (UVar 0)))

129+ synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))) (TType (UVar (-2))))

130+ (Bind (sUN "b") (Pi (TType (UVar (-3))) (TType (UVar (-2))))

131+ (Bind (sUN "x") (Pi (V 1) (TType (UVar (-2))))

132+ (Bind (sUN "y") (Pi (V 1) (TType (UVar (-2))))

133133 (mkApp nMaybe [mkApp (P (TCon 0 4) eqTy Erased)

134134 [V 3, V 2, V 1, V 0]]))))

135135 elabSynEq

src/Idris/Primitives.hs+1−1

@@ -26,7 +26,7 @@ data Prim = Prim { p_name :: Name,

2626

2727ty :: [Const] -> Const -> Type

2828ty [] x = Constant x

29−ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t) (TType (UVar 0))) (ty ts x)

29+ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t) (TType (UVar (-3)))) (ty ts x)

3030

3131total, partial, iopartial :: Totality

3232total = Total []

test/quasiquote001/expected+3−3

@@ -1,5 +1,5 @@

1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6))))))

1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 10))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 10))))))

22--------------

3−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 110))) (TType (UVar 112))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 114))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 116)))))

3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 190))) (TType (UVar 192))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 194))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 196)))))

44--------------

5−(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 36))) (Bind (MN 0 "B") (Pi (TType (UVar 38))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 28))) (Bind (MN 1 "B") (Pi (TType (UVar 30))) (TType (UVar 32))))) (V 3)) (V 2))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110))))

5+(App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190)))) (App (App (App (App (P (DCon 0 4) (MN 0 "__MkPair") (Bind (MN 0 "A") (Pi (TType (UVar 64))) (Bind (MN 0 "B") (Pi (TType (UVar 68))) (Bind (MN 0 "a") (Pi (V 1)) (Bind (MN 0 "b") (Pi (V 1)) (App (App (P (TCon 0 0) (MN 0 "__Pair") (Bind (MN 1 "A") (Pi (TType (UVar 52))) (Bind (MN 1 "B") (Pi (TType (UVar 56))) (TType (UVar 60))))) (V 3)) (V 2))))))) (TType (UVar 184))) (TType (UVar 186))) (TType (UVar 190))) (TType (UVar 190))))

test/unique001/expected+13−1

@@ -1,7 +1,19 @@

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

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

3338,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

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

5+unique001a.idr:38:11:Can't convert

6+ [94mInt[0m -> [94mString[0m

7+with

8+ UniqueType ([94mInt[0m -> [94mString[0m)

9+unique001a.idr:49:12:Can't convert

10+ [94mInt[0m -> [94mString[0m

11+with

12+ UniqueType ([94mInt[0m -> [94mString[0m)

13+unique001a.idr:60:12:Can't convert

14+ UniqueType ([94mInt[0m -> [94mString[0m)

15+with

16+ [94mInt[0m -> [94mString[0m

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

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

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

test/unique002/expected+4−1

@@ -1,2 +1,5 @@

11unique002.idr:15:5:Unique name xs is used more than once

2−unique002a.idr:15:5:Unique name xs is used more than once

2+unique002a.idr:15:5:Can't convert

3+ [94mInt[0m -> [94mString[0m

4+with

5+ UniqueType ([94mInt[0m -> [94mString[0m)

test/unique003/expectednew file+4

@@ -0,0 +1,4 @@

1+unique003.idr:18:5:Can't convert

2+ [94mInt[0m -> [94mString[0m

3+with

4+ UniqueType ([94mInt[0m -> [94mString[0m)

test/unique003/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ unique003.idr --check

3+rm -f *.ibc

test/unique003/unique003.idrnew file+22

@@ -0,0 +1,22 @@

1+module Main

3+data UList : Type -> UniqueType where

4+ Nil : UList a

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

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

8+showU xs = "[" ++ showU' xs ++ "]" where

9+ showU' : Borrowed (UList a) -> String

10+ showU' [] = ""

11+ showU' [x] = show x

12+ showU' (x :: xs) = show x ++ ", " ++ showU' xs

13+

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

15+free xs = ""

16+

17+foo : UList Int -> IO ()

18+foo xs = do let f = \x : Int => showU xs -- can't build this in unique context

19+ putStrLn (f 10)

20+ putStrLn $ free xs

21+ putStrLn (f 10)

22+ return ()