f2a9099 · Idris-dev · git.iko.soy

idris.cabal+1

@@ -633,6 +633,7 @@ Library

633633 , IRTS.Java.Mangling

634634 , IRTS.Java.Pom

635635 , IRTS.Lang

636+ , IRTS.LangOpts

636637 , IRTS.Simplified

637638 , IRTS.System

638639

libs/prelude/IO.idr+6−2

@@ -5,7 +5,9 @@ import Prelude.List

55%access public

66

77||| Idris's primitive IO, for building abstractions on top of

8−abstract data PrimIO a = prim__IO a

8+abstract

9+data PrimIO : Type -> Type where

10+ prim__IO : a -> PrimIO a

911

1012||| A token representing the world, for use in `IO`

1113abstract data World = TheWorld

@@ -15,7 +17,9 @@ WorldRes x = x

1517

1618-- abstract data WorldRes a = MkWR a World

1719

18−abstract data IO a = MkIO (World -> PrimIO (WorldRes a))

20+abstract

21+data IO : Type -> Type where

22+ MkIO : (World -> PrimIO (WorldRes a)) -> IO a

1923

2024abstract

2125prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b

libs/prelude/Prelude/Basics.idr+1−1

@@ -28,7 +28,7 @@ snd (x, y) = y

2828infixl 9 .

2929

3030||| Function composition

31−(.) : (b -> c) -> (a -> b) -> a -> c

31+(.) : {a, b, c : Type*} -> (b -> c) -> (a -> b) -> a -> c

3232(.) f g x = f (g x)

3333

3434||| Takes in the first two arguments in reverse order.

rts/idris_gc.c+11−4

@@ -12,10 +12,14 @@ VAL copy(VM* vm, VAL x) {

1212 switch(GETTY(x)) {

1313 case CON:

1414 ar = CARITY(x);

15− allocCon(cl, vm, CTAG(x), ar, 1);

16− for(i = 0; i < ar; ++i) {

17−// *argptr = copy(vm, *((VAL*)(x->info.c.args)+i)); // recursive version

18− cl->info.c.args[i] = x->info.c.args[i];

15+ if (ar == 0 && CTAG(x) < 256) {

16+ return x;

17+ } else {

18+ allocCon(cl, vm, CTAG(x), ar, 1);

19+ for(i = 0; i < ar; ++i) {

20+ // *argptr = copy(vm, *((VAL*)(x->info.c.args)+i)); // recursive version

21+ cl->info.c.args[i] = x->info.c.args[i];

22+ }

1923 }

2024 break;

2125 case FLOAT:

@@ -147,4 +151,7 @@ void idris_gcInfo(VM* vm, int doGC) {

147151 printf("Final heap use %d\n", (int)(vm->heap.next - vm->heap.heap));

148152 if (doGC) { idris_gc(vm); }

149153 printf("Final heap use after GC %d\n", (int)(vm->heap.next - vm->heap.heap));

154+

155+ printf("Total allocations %d\n", vm->stats.allocations);

156+ printf("Number of collections %d\n", vm->stats.collections);

150157}

rts/idris_main.c+3

@@ -15,6 +15,8 @@ int main(int argc, char* argv[]) {

1515 __idris_argv = argv;

1616

1717 VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1);

18+ initNullaries();

19+

1820 _idris__123_runMain0_125_(vm, NULL);

1921

2022#ifdef IDRIS_DEBUG

@@ -29,5 +31,6 @@ int main(int argc, char* argv[]) {

2931 print_stats(&stats);

3032 }

3133

34+ freeNullaries();

3235 return EXIT_SUCCESS;

3336}

rts/idris_rts.c+33−6

@@ -828,12 +828,16 @@ VAL copyTo(VM* vm, VAL x) {

828828 switch(GETTY(x)) {

829829 case CON:

830830 ar = CARITY(x);

831− allocCon(cl, vm, CTAG(x), ar, 1);

832−

833− argptr = (VAL*)(cl->info.c.args);

834− for(i = 0; i < ar; ++i) {

835− *argptr = copyTo(vm, *((VAL*)(x->info.c.args)+i)); // recursive version

836− argptr++;

831+ if (ar == 0 && CTAG(x) < 256) { // globally allocated

832+ cl = x;

833+ } else {

834+ allocCon(cl, vm, CTAG(x), ar, 1);

835+

836+ argptr = (VAL*)(cl->info.c.args);

837+ for(i = 0; i < ar; ++i) {

838+ *argptr = copyTo(vm, *((VAL*)(x->info.c.args)+i)); // recursive version

839+ argptr++;

840+ }

837841 }

838842 break;

839843 case FLOAT:

@@ -962,6 +966,29 @@ VAL idris_recvMessage(VM* vm) {

962966 return msg;

963967}

964968#endif

969+

970+VAL* nullary_cons;

971+

972+void initNullaries() {

973+ int i;

974+ VAL cl;

975+ nullary_cons = malloc(256 * sizeof(VAL));

976+ for(i = 0; i < 256; ++i) {

977+ cl = malloc(sizeof(Closure));

978+ SETTY(cl, CON);

979+ cl->info.c.tag_arity = i << 8;

980+ nullary_cons[i] = cl;

981+ }

982+}

983+

984+void freeNullaries() {

985+ int i;

986+ for(i = 0; i < 256; ++i) {

987+ free(nullary_cons[i]);

988+ }

989+ free(nullary_cons);

990+}

991+

965992int __idris_argc;

966993char **__idris_argv;

967994

rts/idris_rts.h+11

@@ -214,6 +214,17 @@ void idris_doneAlloc(VM* vm);

214214 SETTY(cl, CON); \

215215 cl->info.c.tag_arity = ((t) << 8) | (a);

216216

217+#define updateCon(cl, old, t, a) \

218+ cl = old; \

219+ SETTY(cl, CON); \

220+ cl->info.c.tag_arity = ((t) << 8) | (a);

221+

222+#define NULL_CON(x) nullary_cons[x]

223+

224+extern VAL* nullary_cons;

225+void initNullaries();

226+void freeNullaries();

227+

217228void* vmThread(VM* callvm, func f, VAL arg);

218229

219230// Copy a structure to another vm's heap

src/IRTS/Bytecode.hs+11−5

@@ -37,7 +37,9 @@ data BC =

3737

3838 -- reg = constructor, where constructor consists of a tag and

3939 -- values from registers, e.g. (cons tag args)

40− | MKCON Reg Int [Reg]

40+ -- the 'Maybe Reg', if set, is a register which can be overwritten

41+ -- (i.e. safe for mutable update), though this can be ignored

42+ | MKCON Reg (Maybe Reg) Int [Reg]

4143

4244 -- Matching on value of reg: usually (but not always) there are

4345 -- constructors, hence "Int" for patterns (that's a tag on which

@@ -67,8 +69,9 @@ data BC =

6769 -- same, perhaps exists just for TCO

6870 | TAILCALL Name

6971

70− -- set reg to (apply string args), 2nd argument could be ignored,

71− -- types could be ignored if they are not required

72+ -- set reg to (apply string args), FLang argument is the language to

73+ -- be called. FType is the foreign language type, which may be used to

74+ -- control marshaling.

7275 | FOREIGNCALL Reg FLang FType String [(FType, Reg)]

7376

7477 -- move this number of elements from TOP to BASE

@@ -136,15 +139,18 @@ bc reg (SLet (Loc i) e sc) r = bc (L i) e False ++ bc reg sc r

136139bc reg (SUpdate (Loc i) sc) r = bc reg sc False ++ [ASSIGN (L i) reg]

137140 ++ clean r

138141-- bc reg (SUpdate x sc) r = bc reg sc r -- can't update, just do it

139−bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r

142+bc reg (SCon atloc i _ vs) r

143+ = MKCON reg (getAllocLoc atloc) i (map getL vs) : clean r

140144 where getL (Loc x) = L x

145+ getAllocLoc (Just (Loc x)) = Just (L x)

146+ getAllocLoc _ = Nothing

141147bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r

142148bc reg (SConst i) r = ASSIGNCONST reg i : clean r

143149bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r

144150 where getL (Loc x) = L x

145151bc reg (SError str) r = [ERROR str]

146152bc reg SNothing r = NULL reg : clean r

147−bc reg (SCase (Loc l) alts) r

153+bc reg (SCase up (Loc l) alts) r

148154 | isConst alts = constCase reg (L l) alts r

149155 | otherwise = conCase True reg (L l) alts r

150156bc reg (SChkCase (Loc l) alts) r

src/IRTS/CodegenC.hs+10−3

@@ -153,9 +153,10 @@ bcc i (ASSIGNCONST l c)

153153 mkConst (B64 x) = "idris_b64const(vm, " ++ show x ++ "ULL)"

154154 mkConst _ = "MKINT(42424242)"

155155bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

156−bcc i (MKCON l tag args)

157− = indent i ++ "allocCon(" ++ creg Tmp ++ ", vm, " ++ show tag ++ "," ++

158− show (length args) ++ ", 0);\n" ++

156+bcc i (MKCON l loc tag []) | tag < 256

157+ = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"

158+bcc i (MKCON l loc tag args)

159+ = indent i ++ alloc loc tag ++

159160 indent i ++ setArgs 0 args ++ "\n" ++

160161 indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"

161162

@@ -165,6 +166,12 @@ bcc i (MKCON l tag args)

165166 setArgs i [] = ""

166167 setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++

167168 "); " ++ setArgs (i + 1) xs

169+ alloc Nothing tag

170+ = "allocCon(" ++ creg Tmp ++ ", vm, " ++ show tag ++ ", " ++

171+ show (length args) ++ ", 0);\n"

172+ alloc (Just old) tag

173+ = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++

174+ show (length args) ++ ");\n"

168175

169176bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++

170177 ", " ++ show a ++ ");\n"

src/IRTS/CodegenJava.hs+2−2

@@ -460,11 +460,11 @@ mkExp pp (SUpdate var newExp) =

460460 mkExp pp newExp

461461

462462-- Objects

463−mkExp pp (SCon conId _ args) =

463+mkExp pp (SCon _ conId _ args) =

464464 mkIdrisObject conId args >>= ppExp pp

465465

466466-- Case expressions

467−mkExp pp (SCase var alts) = mkCase pp True var alts

467+mkExp pp (SCase up var alts) = mkCase pp True var alts

468468mkExp pp (SChkCase var alts) = mkCase pp False var alts

469469

470470-- Projections

src/IRTS/CodegenJavaScript.hs+1−1

@@ -1314,7 +1314,7 @@ translateBC info bc

13141314 | SLIDE n <- bc = jsSLIDE info n

13151315 | REBASE <- bc = jsREBASE info

13161316 | RESERVE n <- bc = jsRESERVE info n

1317− | MKCON r t rs <- bc = jsMKCON info r t rs

1317+ | MKCON r _ t rs <- bc = jsMKCON info r t rs

13181318 | CASE s r c d <- bc = jsCASE info s r c d

13191319 | CONSTCASE r c d <- bc = jsCONSTCASE info r c d

13201320 | PROJECT r l a <- bc = jsPROJECT info r l a

src/IRTS/CodegenLLVM.hs+2−2

@@ -494,7 +494,7 @@ cgExpr (SUpdate (Loc level) expr) = do

494494 modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }

495495 return val

496496cgExpr (SUpdate x expr) = cgExpr expr

497−cgExpr (SCon tag name args) = do

497+cgExpr (SCon _ tag name args) = do

498498 argSlots <- mapM var args

499499 case sequence argSlots of

500500 Nothing -> return Nothing

@@ -511,7 +511,7 @@ cgExpr (SCon tag name args) = do

511511 ptrI8 <- inst $ BitCast con (PointerType (IntegerType 8) (AddrSpace 0)) []

512512 inst' $ simpleCall "llvm.invariant.start" [ConstantOperand $ C.Int 64 (-1), ptrI8]

513513 Just <$> inst (BitCast con (PointerType valueType (AddrSpace 0)) [])

514−cgExpr (SCase inspect alts) = do

514+cgExpr (SCase _ inspect alts) = do

515515 val <- var inspect

516516 case val of

517517 Nothing -> return Nothing

src/IRTS/Compiler.hs+31−16

@@ -3,6 +3,7 @@

33module IRTS.Compiler(compile, generate) where

44

55import IRTS.Lang

6+import IRTS.LangOpts

67import IRTS.Defunctionalise

78import IRTS.Simplified

89import IRTS.CodegenCommon

@@ -65,8 +66,14 @@ compile codegen f tm

6566 defsIn <- mkDecls tm reachableNames

6667 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

6768 -- iputStrLn $ showSep "\n" (map show defs)

68− let (nexttag, tagged) = addTags 65536 (liftAll defs)

69+ -- Inlined top level LDecl made here

70+ let defsInlined = inlineAll defs

71+ let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

72+ defsInlined

73+

74+ let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)

6975 let ctxtIn = addAlist tagged emptyContext

76+

7077 iLOG "Defunctionalising"

7178 let defuns_in = defunctionalise nexttag ctxtIn

7279 logLvl 5 $ show defuns_in

@@ -75,7 +82,7 @@ compile codegen f tm

7582 logLvl 5 $ show defuns

7683 iLOG "Resolving variables for CG"

7784 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

78− let checked = checkDefs defuns (toAlist defuns)

85+ let checked = simplifyDefs defuns (toAlist defuns)

7986 outty <- outputTy

8087 dumpCases <- getDumpCases

8188 dumpDefun <- getDumpDefun

@@ -171,6 +178,7 @@ showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

171178 snRank (CaseN n) = "5" ++ nameRank n

172179 snRank (ElimN n) = "6" ++ nameRank n

173180 snRank (InstanceCtorN n) = "7" ++ nameRank n

181+ snRank (WithN i n) = "8" ++ nameRank n ++ show i

174182

175183isCon (TyDecl _ _) = True

176184isCon _ = False

@@ -194,11 +202,17 @@ mkLDecl n (Function tm _)

194202 = declArgs [] True n <$> irTerm M.empty [] tm

195203

196204mkLDecl n (CaseOp ci _ _ _ pats cd)

197− = declArgs [] (case_inlinable ci) n <$> irTree args sc

205+ = declArgs [] (case_inlinable ci || caseName n) n <$> irTree args sc

198206 where

199207 (args, sc) = cases_runtime cd

200208

201−mkLDecl n (TyDecl (DCon tag arity) _) =

209+ -- Always attempt to inline functions arising from 'case' expressions

210+ caseName (SN (CaseN _)) = True

211+ caseName (SN (WithN _ _)) = True

212+ caseName (NS n _) = caseName n

213+ caseName _ = False

214+

215+mkLDecl n (TyDecl (DCon tag arity _) _) =

202216 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)

203217

204218mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

@@ -281,12 +295,13 @@ irTerm vs env tm@(App f a) = case unApply tm of

281295 x' <- irTerm vs env x

282296 t' <- irTerm vs env t

283297 e' <- irTerm vs env e

284− return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

298+ return (LCase Shared x'

299+ [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'

285300 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

286301 ])

287302

288303 -- data constructor

289− (P (DCon t arity) n _, args) -> do

304+ (P (DCon t arity _) n _, args) -> do

290305 detag <- fgetState (opt_detaggable . ist_optimisation n)

291306 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

292307

@@ -391,7 +406,7 @@ irTerm vs env tm@(App f a) = case unApply tm of

391406

392407 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of

393408 Just (CaseOp ci ty tys def tot cdefs) -> length tys

394− Just (TyDecl (DCon tag ar) _) -> ar

409+ Just (TyDecl (DCon tag ar _) _) -> ar

395410 Just (TyDecl Ref ty) -> length $ getArgTys ty

396411 Just (Operator ty ar op) -> ar

397412 Just def -> error $ "unknown arity: " ++ show (n, def)

@@ -510,10 +525,10 @@ irSC vs (UnmatchedCase str) = return $ LError str

510525irSC vs (ProjCase tm alts) = do

511526 tm' <- irTerm vs [] tm

512527 alts' <- mapM (irAlt vs tm') alts

513− return $ LCase tm' alts'

528+ return $ LCase Shared tm' alts'

514529

515530-- Transform matching on Delay to applications of Force.

516−irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

531+irSC vs (Case up n [ConCase (UN delay) i [_, _, n'] sc])

517532 | delay == txt "Delay"

518533 = do sc' <- irSC vs $ mkForce n' n sc

519534 return $ LLet n' (LForce (LV (Glob n))) sc'

@@ -540,7 +555,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

540555-- Hence, we check whether the variables are used at all

541556-- and erase the casesplit if they are not.

542557--

543−irSC vs (Case n [alt]) = do

558+irSC vs (Case up n [alt]) = do

544559 replacement <- case alt of

545560 ConCase cn a ns sc -> do

546561 detag <- fgetState (opt_detaggable . ist_optimisation cn)

@@ -556,7 +571,7 @@ irSC vs (Case n [alt]) = do

556571 alt' <- irAlt vs (LV (Glob n)) alt

557572 return $ case namesBoundIn alt' `usedIn` subexpr alt' of

558573 [] -> subexpr alt' -- strip the unused top-most case

559− _ -> LCase (LV (Glob n)) [alt']

574+ _ -> LCase up (LV (Glob n)) [alt']

560575 where

561576 namesBoundIn :: LAlt -> [Name]

562577 namesBoundIn (LConCase cn i ns sc) = ns

@@ -584,13 +599,13 @@ irSC vs (Case n [alt]) = do

584599-- This work-around is not entirely optimal; the best approach would be

585600-- to ensure that such case trees don't arise in the first place.

586601--

587−irSC vs (Case n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

602+irSC vs (Case up n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

588603 detag <- fgetState (opt_detaggable . ist_optimisation cn)

589604 if detag

590− then irSC vs (Case n [ConCase cn a ns sc])

591− else LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

605+ then irSC vs (Case up n [ConCase cn a ns sc])

606+ else LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

592607

593−irSC vs sc@(Case n alts) = do

608+irSC vs sc@(Case up n alts) = do

594609 -- check that neither alternative needs the newtype optimisation,

595610 -- see comment above

596611 goneWrong <- or <$> mapM isDetaggable alts

@@ -598,7 +613,7 @@ irSC vs sc@(Case n alts) = do

598613 $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

599614

600615 -- everything okay

601− LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

616+ LCase up (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

602617 where

603618 isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

604619 isDetaggable _ = return False

src/IRTS/Defunctionalise.hs+16−10

@@ -5,6 +5,7 @@ module IRTS.Defunctionalise(module IRTS.Defunctionalise,

55

66import IRTS.Lang

77import Idris.Core.TT

8+import Idris.Core.CaseTree

89

910import Debug.Trace

1011import Data.Maybe

@@ -17,8 +18,8 @@ data DExp = DV LVar

1718 | DLet Name DExp DExp -- name just for pretty printing

1819 | DUpdate Name DExp -- eval expression, then update var with it

1920 | DProj DExp Int

20− | DC Int Name [DExp]

21− | DCase DExp [DAlt]

21+ | DC (Maybe LVar) Int Name [DExp]

22+ | DCase CaseType DExp [DAlt]

2223 | DChkCase DExp [DAlt] -- a case where the type is unknown (for EVAL/APPLY)

2324 | DConst Const

2425 | DForeign FLang FType String [(FType, DExp)]

@@ -99,15 +100,15 @@ addApps defs (n, LFun _ _ args e)

99100 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)

100101 aa env (LForce e) = liftM eEVAL (aa env e)

101102 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)

102− aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)

103+ aa env (LCon loc i n args) = liftM (DC loc i n) (mapM (aa env) args)

103104 aa env (LProj t@(LV (Glob n)) i)

104105 | n `elem` env = do t' <- aa env t

105106 return $ DProj (DUpdate n t') i

106107 aa env (LProj t i) = do t' <- aa env t

107108 return $ DProj t' i

108− aa env (LCase e alts) = do e' <- aa env e

109− alts' <- mapM (aaAlt env) alts

110− return $ DCase e' alts'

109+ aa env (LCase up e alts) = do e' <- aa env e

110+ alts' <- mapM (aaAlt env) alts

111+ return $ DCase up e' alts'

111112 aa env (LConst c) = return $ DConst c

112113 aa env (LForeign l t n args) = liftM (DForeign l t n) (mapM (aaF env) args)

113114 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)

@@ -160,8 +161,8 @@ addApps defs (n, LFun _ _ args e)

160161 | otherwise = preEval xs t

161162

162163 needsEval x (DApp _ _ args) = or (map (needsEval x) args)

163− needsEval x (DC _ _ args) = or (map (needsEval x) args)

164− needsEval x (DCase e alts) = needsEval x e || or (map nec alts)

164+ needsEval x (DC _ _ _ args) = or (map (needsEval x) args)

165+ needsEval x (DCase up e alts) = needsEval x e || or (map nec alts)

165166 where nec (DConCase _ _ _ e) = needsEval x e

166167 nec (DConstCase _ e) = needsEval x e

167168 nec (DDefaultCase e) = needsEval x e

@@ -262,10 +263,15 @@ instance Show DExp where

262263 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++

263264 show' (env ++ [show n]) e

264265 show' env (DUpdate n e) = "!update " ++ show n ++ "(" ++ show' env e ++ ")"

265− show' env (DC i n args) = show n ++ ")" ++ showSep ", " (map (show' env) args) ++ ")"

266+ show' env (DC loc i n args) = atloc loc ++ show n ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"

267+ where atloc Nothing = ""

268+ atloc (Just l) = "@" ++ show (LV l) ++ ":"

266269 show' env (DProj t i) = show t ++ "!" ++ show i

267− show' env (DCase e alts) = "case " ++ show' env e ++ " of {\n\t" ++

270+ show' env (DCase up e alts) = "case" ++ update ++ show' env e ++ " of {\n\t" ++

268271 showSep "\n\t| " (map (showAlt env) alts)

272+ where update = case up of

273+ Shared -> " "

274+ Updatable -> "! "

269275 show' env (DChkCase e alts) = "case' " ++ show' env e ++ " of {\n\t" ++

270276 showSep "\n\t| " (map (showAlt env) alts)

271277 show' env (DConst c) = show c

src/IRTS/DumpBC.hs+3−1

@@ -35,8 +35,10 @@ serializeBC n bc = indent n ++

3535 "ASSIGNCONST " ++ serializeReg a ++ " " ++ show b

3636 UPDATE a b ->

3737 "UPDATE " ++ serializeReg a ++ " " ++ serializeReg b

38− MKCON a b xs ->

38+ MKCON a Nothing b xs ->

3939 "MKCON " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"

40+ MKCON a (Just r) b xs ->

41+ "MKCON@" ++ serializeReg r ++ " " ++ serializeReg a ++ " " ++ show b ++ " [" ++ (interMap xs ", " serializeReg) ++ "]"

4042 CASE safe r cases def ->

4143 "CASE " ++ serializeReg r ++ ":\n" ++ interMap cases "\n" (serializeCase (n + 1)) ++

4244 maybe "" (\def' -> "\n" ++ serializeDefault (n + 1) def') def

src/IRTS/Java/Mangling.hs+2−2

@@ -31,8 +31,8 @@ prefixCallNamespaces name (SFun fname args i e) =

3131 SLet var (prefixCallNamespacesExp name e1) (prefixCallNamespacesExp name e2)

3232 prefixCallNamespacesExp name (SUpdate var e) =

3333 SUpdate var (prefixCallNamespacesExp name e)

34− prefixCallNamespacesExp name (SCase var alts) =

35− SCase var (map (prefixCallNamespacesCase name) alts)

34+ prefixCallNamespacesExp name (SCase up var alts) =

35+ SCase up var (map (prefixCallNamespacesCase name) alts)

3636 prefixCallNamespacesExp name (SChkCase var alts) =

3737 SChkCase var (map (prefixCallNamespacesCase name) alts)

3838 prefixCallNamespacesExp _ exp = exp

src/IRTS/Lang.hs+100−23

@@ -1,15 +1,22 @@

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2+

13module IRTS.Lang where

24

3−import Control.Monad.State hiding (lift)

4−import Idris.Core.TT

5−import Data.List

6−import Debug.Trace

5+import Control.Monad.State hiding (lift)

6+import Control.Applicative hiding (Const)

7+

8+import Idris.Core.TT

9+import Idris.Core.CaseTree

10+

11+import Data.List

12+import Debug.Trace

713

814data Endianness = Native | BE | LE deriving (Show, Eq)

915

1016data LVar = Loc Int | Glob Name

1117 deriving (Show, Eq)

1218

19+-- ASSUMPTION: All variable bindings have unique names here

1320data LExp = LV LVar

1421 | LApp Bool LExp [LExp] -- True = tail call

1522 | LLazyApp Name [LExp] -- True = tail call

@@ -18,8 +25,9 @@ data LExp = LV LVar

1825 | LLet Name LExp LExp -- name just for pretty printing

1926 | LLam [Name] LExp -- lambda, lifted out before compiling

2027 | LProj LExp Int -- projection

21− | LCon Int Name [LExp]

22− | LCase LExp [LAlt]

28+ | LCon (Maybe LVar) -- Location to reallocate, if available

29+ Int Name [LExp]

30+ | LCase CaseType LExp [LAlt]

2331 | LConst Const

2432 | LForeign FLang FType String [(FType, LExp)]

2533 | LOp PrimFn [LExp]

@@ -90,10 +98,13 @@ data FType = FArith ArithTy

9098 | FAny

9199 deriving (Show, Eq)

92100

93−data LAlt = LConCase Int Name [Name] LExp

94− | LConstCase Const LExp

95− | LDefaultCase LExp

96− deriving (Show, Eq)

101+-- FIXME: Why not use this for all the IRs now?

102+data LAlt' e = LConCase Int Name [Name] e

103+ | LConstCase Const e

104+ | LDefaultCase e

105+ deriving (Show, Eq, Functor)

106+

107+type LAlt = LAlt' LExp

97108

98109data LDecl = LFun [LOpt] Name [Name] LExp -- options, name, arg names, def

99110 | LConstructor Name Int Int -- constructor name, tag, arity

@@ -123,9 +134,9 @@ liftAll :: [(Name, LDecl)] -> [(Name, LDecl)]

123134liftAll xs = concatMap (\ (x, d) -> lambdaLift x d) xs

124135

125136lambdaLift :: Name -> LDecl -> [(Name, LDecl)]

126−lambdaLift n (LFun _ _ args e)

137+lambdaLift n (LFun opts _ args e)

127138 = let (e', (LS _ _ decls)) = runState (lift args e) (LS n 0 []) in

128− (n, LFun [] n args e') : decls

139+ (n, LFun opts n args e') : decls

129140lambdaLift n x = [(n, x)]

130141

131142getNextName :: State LiftState Name

@@ -168,11 +179,11 @@ lift env (LLam args e) = do e' <- lift (env ++ args) e

168179 return (LApp False (LV (Glob fn)) (map (LV . Glob) usedArgs))

169180lift env (LProj t i) = do t' <- lift env t

170181 return (LProj t' i)

171−lift env (LCon i n args) = do args' <- mapM (lift env) args

172− return (LCon i n args')

173−lift env (LCase e alts) = do alts' <- mapM liftA alts

174− e' <- lift env e

175− return (LCase e' alts')

182+lift env (LCon loc i n args) = do args' <- mapM (lift env) args

183+ return (LCon loc i n args')

184+lift env (LCase up e alts) = do alts' <- mapM liftA alts

185+ e' <- lift env e

186+ return (LCase up e' alts')

176187 where

177188 liftA (LConCase i n args e) = do e' <- lift (env ++ args) e

178189 return (LConCase i n args e')

@@ -191,6 +202,67 @@ lift env (LOp f args) = do args' <- mapM (lift env) args

191202lift env (LError str) = return $ LError str

192203lift env LNothing = return $ LNothing

193204

205+allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)

206+allocUnique defs p@(n, LConstructor _ _ _) = p

207+allocUnique defs (n, LFun opts fn args e)

208+ = let e' = evalState (findUp e) [] in

209+ (n, LFun opts fn args e')

210+ where

211+ -- Keep track of 'updatable' names in the state, i.e. names whose heap

212+ -- entry may be reused, along with the arity which was there

213+ findUp :: LExp -> State [(Name, Int)] LExp

214+ findUp (LApp t (LV (Glob n)) as)

215+ | Just (LConstructor _ i ar) <- lookupCtxtExact n defs,

216+ ar == length as

217+ = findUp (LCon Nothing i n as)

218+ findUp (LV (Glob n))

219+ | Just (LConstructor _ i 0) <- lookupCtxtExact n defs

220+ = return $ LCon Nothing i n [] -- nullary cons are global, no need to update

221+ findUp (LApp t f as) = LApp t <$> findUp f <*> mapM findUp as

222+ findUp (LLazyApp n as) = LLazyApp n <$> mapM findUp as

223+ findUp (LLazyExp e) = LLazyExp <$> findUp e

224+ findUp (LForce e) = LForce <$> findUp e

225+ -- use assumption that names are unique!

226+ findUp (LLet n val sc) = LLet n <$> findUp val <*> findUp sc

227+ findUp (LLam ns sc) = LLam ns <$> findUp sc

228+ findUp (LProj e i) = LProj <$> findUp e <*> return i

229+ findUp (LCon (Just l) i n es) = LCon (Just l) i n <$> mapM findUp es

230+ findUp (LCon Nothing i n es)

231+ = do avail <- get

232+ v <- findVar [] avail (length es)

233+ LCon v i n <$> mapM findUp es

234+ findUp (LForeign l t s es)

235+ = LForeign l t s <$> mapM (\ (t, e) -> do e' <- findUp e

236+ return (t, e')) es

237+ findUp (LOp o es) = LOp o <$> mapM findUp es

238+ findUp (LCase Updatable e@(LV (Glob n)) as)

239+ = LCase Updatable e <$> mapM (doUpAlt n) as

240+ findUp (LCase t e as)

241+ = LCase t <$> findUp e <*> mapM findUpAlt as

242+ findUp t = return t

243+

244+ findUpAlt (LConCase i t args rhs) = do avail <- get

245+ rhs' <- findUp rhs

246+ put avail

247+ return $ LConCase i t args rhs'

248+ findUpAlt (LConstCase i rhs) = LConstCase i <$> findUp rhs

249+ findUpAlt (LDefaultCase rhs) = LDefaultCase <$> findUp rhs

250+

251+ doUpAlt n (LConCase i t args rhs)

252+ = do avail <- get

253+ put ((n, length args) : avail)

254+ rhs' <- findUp rhs

255+ put avail

256+ return $ LConCase i t args rhs'

257+ doUpAlt n (LConstCase i rhs) = LConstCase i <$> findUp rhs

258+ doUpAlt n (LDefaultCase rhs) = LDefaultCase <$> findUp rhs

259+

260+ findVar _ [] i = return Nothing

261+ findVar acc ((n, l) : ns) i | l == i = do put (reverse acc ++ ns)

262+ return (Just (Glob n))

263+ findVar acc (n : ns) i = findVar (n : acc) ns i

264+

265+

194266-- Return variables in list which are used in the expression

195267

196268usedArg env n | n `elem` env = [n]

@@ -204,9 +276,9 @@ usedIn env (LLazyExp e) = usedIn env e

204276usedIn env (LForce e) = usedIn env e

205277usedIn env (LLet n v e) = usedIn env v ++ usedIn (env \\ [n]) e

206278usedIn env (LLam ns e) = usedIn (env \\ ns) e

207−usedIn env (LCon i n args) = concatMap (usedIn env) args

279+usedIn env (LCon loc i n args) = concatMap (usedIn env) args

208280usedIn env (LProj t i) = usedIn env t

209−usedIn env (LCase e alts) = usedIn env e ++ concatMap (usedInA env) alts

281+usedIn env (LCase up e alts) = usedIn env e ++ concatMap (usedInA env) alts

210282 where usedInA env (LConCase i n ns e) = usedIn env e

211283 usedInA env (LConstCase c e) = usedIn env e

212284 usedInA env (LDefaultCase e) = usedIn env e

@@ -237,12 +309,17 @@ instance Show LExp where

237309

238310 show' env ind (LProj t i) = show t ++ "!" ++ show i

239311

240− show' env ind (LCon i n args)

241− = show n ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"

312+ show' env ind (LCon loc i n args)

313+ = atloc loc ++ show n ++ "(" ++ showSep ", " (map (show' env ind) args) ++ ")"

314+ where atloc Nothing = ""

315+ atloc (Just l) = "@" ++ show (LV l) ++ ":"

242316

243− show' env ind (LCase e alts)

244− = "case " ++ show' env ind e ++ " of \n" ++ fmt alts

317+ show' env ind (LCase up e alts)

318+ = "case" ++ update ++ show' env ind e ++ " of \n" ++ fmt alts

245319 where

320+ update = case up of

321+ Shared -> " "

322+ Updatable -> "! "

246323 fmt [] = ""

247324 fmt [alt]

248325 = "\t" ++ ind ++ "| " ++ showAlt env (ind ++ " ") alt

src/IRTS/LangOpts.hsnew file+80

@@ -0,0 +1,80 @@

1+{-# LANGUAGE PatternGuards, DeriveFunctor #-}

2+

3+module IRTS.LangOpts where

4+

5+import Control.Monad.State hiding (lift)

6+import Control.Applicative hiding (Const)

7+

8+import IRTS.Lang

9+import Idris.Core.TT

10+import Idris.Core.CaseTree

11+import Data.List

12+import Debug.Trace

13+

14+inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]

15+inlineAll lds = let defs = addAlist lds emptyContext in

16+ map (\ (n, def) -> (n, doInline defs def)) lds

17+

18+nextN :: State Int Name

19+nextN = do i <- get

20+ put (i + 1)

21+ return $ sMN i "in"

22+

23+-- Inline inside a declaration. Variables are still Name at this stage.

24+-- Need to preserve uniqueness of variable names in the resulting definition,

25+-- so invent a new name for every variable we encounter

26+doInline :: LDefs -> LDecl -> LDecl

27+doInline defs d = d

28+doInline defs d@(LConstructor _ _ _) = d

29+doInline defs (LFun opts topn args exp)

30+ = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in

31+ LFun opts topn args res

32+ where

33+ inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp

34+ inlineWith done env var@(LV (Glob n))

35+ = case lookup n env of

36+ Just t -> return t

37+ Nothing -> return var

38+ inlineWith done env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith done env) es)

39+ inlineWith done env (LForce e) = LForce <$> inlineWith done env e

40+ inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e

41+ -- Extend the environment for Let and Lam so that bound names aren't

42+ -- expanded with any top level argument definitions they shadow

43+ inlineWith done env (LLet n val sc)

44+ = do n' <- nextN

45+ LLet n' <$> inlineWith done env val <*>

46+ inlineWith done ((n, LV (Glob n')) : env) sc

47+ inlineWith done env (LLam args sc)

48+ = do ns' <- mapM (\n -> do n' <- nextN

49+ return (n, n')) args

50+ LLam (map snd ns') <$>

51+ inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) sc

52+ inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i

53+ inlineWith done env (LCon loc i n es)

54+ = LCon loc i n <$> mapM (inlineWith done env) es

55+ inlineWith done env (LCase ty e alts)

56+ = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts

57+ inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es

58+ -- the interesting case!

59+ inlineWith done env (LApp t (LV (Glob n)) es)

60+ | n `notElem` done,

61+ [LFun opts _ args body] <- lookupCtxt n defs,

62+ Inline `elem` opts,

63+ length es == length args

64+ = do es' <- mapM (inlineWith done env) es

65+ inlineWith (n : done) (zip args es' ++ env) body

66+ inlineWith done env (LApp t f es)

67+ = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es

68+ inlineWith done env (LForeign l t s args)

69+ = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e

70+ return (t, e')) args

71+ inlineWith done env t = return t

72+

73+ inlineWithAlt done env (LConCase i n es rhs)

74+ = do ns' <- mapM (\n -> do n' <- nextN

75+ return (n, n')) es

76+ LConCase i n (map snd ns') <$>

77+ inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs

78+ inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e

79+ inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e

80+

src/IRTS/Simplified.hs+32−26

@@ -1,7 +1,8 @@

1−module IRTS.Simplified where

1+module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where

22

33import IRTS.Defunctionalise

44import Idris.Core.TT

5+import Idris.Core.CaseTree

56import Idris.Core.Typecheck

67import Data.Maybe

78import Control.Monad.State

@@ -15,8 +16,9 @@ data SExp = SV LVar

1516 | SApp Bool Name [LVar]

1617 | SLet LVar SExp SExp

1718 | SUpdate LVar SExp

18− | SCon Int Name [LVar]

19− | SCase LVar [SAlt]

19+ | SCon (Maybe LVar) -- location to reallocate, if available

20+ Int Name [LVar]

21+ | SCase CaseType LVar [SAlt]

2022 | SChkCase LVar [SAlt]

2123 | SProj LVar Int

2224 | SConst Const

@@ -48,7 +50,7 @@ simplify tl (DV (Loc i)) = return (SV (Loc i))

4850simplify tl (DV (Glob x))

4951 = do ctxt <- ldefs

5052 case lookupCtxtExact x ctxt of

51− Just (DConstructor _ t 0) -> return $ SCon t x []

53+ Just (DConstructor _ t 0) -> return $ SCon Nothing t x []

5254 _ -> return $ SV (Glob x)

5355simplify tl (DApp tc n args) = do args' <- mapM sVar args

5456 mkapp (SApp (tl || tc) n) args'

@@ -61,19 +63,19 @@ simplify tl (DLet n v e) = do v' <- simplify False v

6163 return (SLet (Glob n) v' e')

6264simplify tl (DUpdate n e) = do e' <- simplify False e

6365 return (SUpdate (Glob n) e')

64−simplify tl (DC i n args) = do args' <- mapM sVar args

65− mkapp (SCon i n) args'

66+simplify tl (DC loc i n args) = do args' <- mapM sVar args

67+ mkapp (SCon loc i n) args'

6668simplify tl (DProj t i) = do v <- sVar t

6769 case v of

6870 (x, Nothing) -> return (SProj x i)

6971 (Glob x, Just e) ->

7072 return (SLet (Glob x) e (SProj (Glob x) i))

71−simplify tl (DCase e alts) = do v <- sVar e

72− alts' <- mapM (sAlt tl) alts

73− case v of

74− (x, Nothing) -> return (SCase x alts')

75− (Glob x, Just e) ->

76− return (SLet (Glob x) e (SCase (Glob x) alts'))

73+simplify tl (DCase up e alts) = do v <- sVar e

74+ alts' <- mapM (sAlt tl) alts

75+ case v of

76+ (x, Nothing) -> return (SCase up x alts')

77+ (Glob x, Just e) ->

78+ return (SLet (Glob x) e (SCase up (Glob x) alts'))

7779simplify tl (DChkCase e alts)

7880 = do v <- sVar e

7981 alts' <- mapM (sAlt tl) alts

@@ -90,7 +92,7 @@ simplify tl (DError str) = return $ SError str

9092sVar (DV (Glob x))

9193 = do ctxt <- ldefs

9294 case lookupCtxtExact x ctxt of

93− Just (DConstructor _ t 0) -> sVar (DC t x [])

95+ Just (DConstructor _ t 0) -> sVar (DC Nothing t x [])

9496 _ -> return (Glob x, Nothing)

9597sVar (DV x) = return (x, Nothing)

9698sVar e = do e' <- simplify False e

@@ -118,15 +120,15 @@ sAlt tl (DConstCase c e) = do e' <- simplify tl e

118120sAlt tl (DDefaultCase e) = do e' <- simplify tl e

119121 return (SDefaultCase e')

120122

121−checkDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]

122−checkDefs ctxt [] = return []

123−checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)

124− = do xs' <- checkDefs ctxt xs

123+simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]

124+simplifyDefs ctxt [] = return []

125+simplifyDefs ctxt (con@(n, DConstructor _ _ _) : xs)

126+ = do xs' <- simplifyDefs ctxt xs

125127 return xs'

126−checkDefs ctxt ((n, DFun n' args exp) : xs)

128+simplifyDefs ctxt ((n, DFun n' args exp) : xs)

127129 = do let sexp = evalState (simplify True exp) (ctxt, 0)

128130 (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)

129− xs' <- checkDefs ctxt xs

131+ xs' <- simplifyDefs ctxt xs

130132 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')

131133

132134lvar v = do i <- get

@@ -142,7 +144,7 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

142144 Nothing -> case lookupCtxtExact n ctxt of

143145 Just (DConstructor _ i ar) ->

144146 if True -- ar == 0

145− then return (SCon i n [])

147+ then return (SCon Nothing i n [])

146148 else failsc $ "Constructor " ++ show n ++

147149 " has arity " ++ show ar

148150 Just _ -> return (SV (Glob n))

@@ -152,7 +154,7 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

152154 case lookupCtxtExact f ctxt of

153155 Just (DConstructor n tag ar) ->

154156 if True -- (ar == length args)

155− then return $ SCon tag n args'

157+ then return $ SCon Nothing tag n args'

156158 else failsc $ "Constructor " ++ show f ++

157159 " has arity " ++ show ar

158160 Just _ -> return $ SApp tc f args'

@@ -161,22 +163,26 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

161163 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a

162164 return (t, a')) args

163165 return $ SForeign l ty f args'

164− sc env (SCon tag f args)

165− = do args' <- mapM (scVar env) args

166+ sc env (SCon loc tag f args)

167+ = do loc' <- case loc of

168+ Nothing -> return Nothing

169+ Just l -> do l' <- scVar env l

170+ return (Just l')

171+ args' <- mapM (scVar env) args

166172 case lookupCtxtExact f ctxt of

167173 Just (DConstructor n tag ar) ->

168174 if True -- (ar == length args)

169− then return $ SCon tag n args'

175+ then return $ SCon loc' tag n args'

170176 else failsc $ "Constructor " ++ show f ++

171177 " has arity " ++ show ar

172178 _ -> failsc $ "No such constructor " ++ show f

173179 sc env (SProj e i)

174180 = do e' <- scVar env e

175181 return (SProj e' i)

176− sc env (SCase e alts)

182+ sc env (SCase up e alts)

177183 = do e' <- scVar env e

178184 alts' <- mapM (scalt env) alts

179− return (SCase e' alts')

185+ return (SCase up e' alts')

180186 sc env (SChkCase e alts)

181187 = do e' <- scVar env e

182188 alts' <- mapM (scalt env) alts

src/Idris/AbsSyntax.hs+3−3

@@ -228,7 +228,7 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

228228 (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

229229 (P (TCon _ _) n _, Constant _) -> errWhen True

230230 (Constant _, P (TCon _ _) n' _) -> errWhen True

231− (P (DCon _ _) n _, P (DCon _ _) n' _) -> errWhen (n/=n)

231+ (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

232232 _ -> return ()

233233

234234 where errWhen True

@@ -1026,7 +1026,7 @@ getPriority i tm = 1 -- pri tm

10261026 where

10271027 pri (PRef _ n) =

10281028 case lookupP n (tt_ctxt i) of

1029− ((P (DCon _ _) _ _):_) -> 1

1029+ ((P (DCon _ _ _) _ _):_) -> 1

10301030 ((P (TCon _ _) _ _):_) -> 1

10311031 ((P Ref _ _):_) -> 1

10321032 [] -> 0 -- must be locally bound, if it's not an error...

@@ -1474,7 +1474,7 @@ aiFn inpat True qq ist fc f ds []

14741474 imp _ = True

14751475-- allImp [] = False

14761476 allImp xs = all imp xs

1477− constructor (TyDecl (DCon _ _) _) = True

1477+ constructor (TyDecl (DCon _ _ _) _) = True

14781478 constructor _ = False

14791479

14801480 conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

src/Idris/AbsSyntaxTree.hs+3

@@ -713,6 +713,7 @@ data PTerm = PQuote Raw

713713 | PAlternative Bool [PTerm] -- True if only one may work

714714 | PHidden PTerm -- ^ Irrelevant or hidden pattern

715715 | PType -- ^ 'Type' type

716+ | PUniverse Universe -- ^ Some universe

716717 | PGoal FC PTerm Name PTerm

717718 | PConstant Const -- ^ Builtin types

718719 | Placeholder

@@ -1380,6 +1381,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13801381 prettyAs =

13811382 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as

13821383 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1384+ prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

13831385 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

13841386 -- XXX: add pretty for tactics

13851387 prettySe p bnd (PProof ts) =

@@ -1644,6 +1646,7 @@ instance Sized PTerm where

16441646 size (PDisamb _ tm) = size tm

16451647 size (PNoImplicits tm) = size tm

16461648 size PType = 1

1649+ size (PUniverse _) = 1

16471650 size (PConstant const) = 1 + size const

16481651 size Placeholder = 1

16491652 size (PDoBlock dos) = 1 + size dos

src/Idris/Apropos.hs+1−1

@@ -61,7 +61,7 @@ instance Apropos (Binder (TT Name)) where

6161instance Apropos (TT Name) where

6262 isApropos str (P Ref n ty) = isApropos str n || isApropos str ty

6363 isApropos str (P (TCon _ _) n ty) = isApropos str n || isApropos str ty

64− isApropos str (P (DCon _ _) n ty) = isApropos str n || isApropos str ty

64+ isApropos str (P (DCon _ _ _) n ty) = isApropos str n || isApropos str ty

6565 isApropos str (P Bound _ ty) = isApropos str ty

6666 isApropos str (Bind n b tm) = isApropos str b || isApropos str tm

6767 isApropos str (App t1 t2) = isApropos str t1 || isApropos str t2

src/Idris/Core/Binary.hs+25−3

@@ -78,6 +78,9 @@ instance Binary SpecialName where

7878 CaseN x1 -> do putWord8 4; put x1

7979 ElimN x1 -> do putWord8 5; put x1

8080 InstanceCtorN x1 -> do putWord8 6; put x1

81+ WithN x1 x2 -> do putWord8 7

82+ put x1

83+ put x2

8184 get

8285 = do i <- getWord8

8386 case i of

@@ -99,6 +102,9 @@ instance Binary SpecialName where

99102 return (ElimN x1)

100103 6 -> do x1 <- get

101104 return (InstanceCtorN x1)

105+ 7 -> do x1 <- get

106+ x2 <- get

107+ return (WithN x1 x2)

102108 _ -> error "Corrupted binary data for SpecialName"

103109

104110

@@ -275,13 +281,24 @@ instance (Binary b) => Binary (Binder b) where

275281 _ -> error "Corrupted binary data for Binder"

276282

277283

284+instance Binary Universe where

285+ put x = case x of

286+ UniqueType -> putWord8 0

287+ AllTypes -> putWord8 1

288+ get = do i <- getWord8

289+ case i of

290+ 0 -> return UniqueType

291+ 1 -> return AllTypes

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

293+

278294instance Binary NameType where

279295 put x

280296 = case x of

281297 Bound -> putWord8 0

282298 Ref -> putWord8 1

283− DCon x1 x2 -> do putWord8 2

284− put (x1 * 65536 + x2)

299+ DCon x1 x2 x3 -> do putWord8 2

300+ put (x1 * 65536 + x2)

301+ put x3

285302 TCon x1 x2 -> do putWord8 3

286303 put (x1 * 65536 + x2)

287304 get

@@ -290,7 +307,8 @@ instance Binary NameType where

290307 0 -> return Bound

291308 1 -> return Ref

292309 2 -> do x1x2 <- get

293− return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

310+ x3 <- get

311+ return (DCon (x1x2 `div` 65536) (x1x2 `mod` 65536) x3)

294312 3 -> do x1x2 <- get

295313 return (TCon (x1x2 `div` 65536) (x1x2 `mod` 65536))

296314 _ -> error "Corrupted binary data for NameType"

@@ -325,6 +343,8 @@ instance {- (Binary n) => -} Binary (TT Name) where

325343 TType x1 -> do putWord8 7

326344 put x1

327345 Impossible -> putWord8 8

346+ UType x1 -> do putWord8 10

347+ put x1

328348 get

329349 = do i <- getWord8

330350 case i of

@@ -352,5 +372,7 @@ instance {- (Binary n) => -} Binary (TT Name) where

352372 8 -> return Impossible

353373 9 -> do x1 <- get

354374 return (V x1)

375+ 10 -> do x1 <- get

376+ return (UType x1)

355377 _ -> error "Corrupted binary data for TT"

356378

src/Idris/Core/CaseTree.hs+69−74

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

11{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

22

33module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..), ErasureInfo,

4− Phase(..), CaseTree,

4+ Phase(..), CaseTree, CaseType(..),

55 simpleCase, small, namesUsed, findCalls, findUsedArgs,

66 substSC, substAlt, mkForce) where

77

@@ -30,7 +30,7 @@ data CaseDef = CaseDef [Name] !SC [Term]

3030-- allows casing on arbitrary terms, here we choose to maintain the distinction

3131-- in order to allow for better optimisation opportunities.

3232--

33−data SC' t = Case Name [CaseAlt' t] -- ^ invariant: lowest tags first

33+data SC' t = Case CaseType Name [CaseAlt' t] -- ^ invariant: lowest tags first

3434 | ProjCase t [CaseAlt' t] -- ^ special case for projections/thunk-forcing before inspection

3535 | STerm !t

3636 | UnmatchedCase String -- ^ error message

@@ -41,6 +41,9 @@ deriving instance Binary SC'

4141deriving instance NFData SC'

4242!-}

4343

44+data CaseType = Updatable | Shared

45+ deriving (Eq, Ord, Show)

46+

4447type SC = SC' Term

4548

4649data CaseAlt' t = ConCase Name Int [Name] !(SC' t)

@@ -59,8 +62,11 @@ type CaseAlt = CaseAlt' Term

5962instance Show t => Show (SC' t) where

6063 show sc = show' 1 sc

6164 where

62− show' i (Case n alts) = "case " ++ show n ++ " of\n" ++ indent i ++

65+ show' i (Case up n alts) = "case" ++ u ++ show n ++ " of\n" ++ indent i ++

6366 showSep ("\n" ++ indent i) (map (showA i) alts)

67+ where u = case up of

68+ Updatable -> "! "

69+ Shared -> " "

6470 show' i (ProjCase tm alts) = "case " ++ show tm ++ " of " ++

6571 showSep ("\n" ++ indent i) (map (showA i) alts)

6672 show' i (STerm tm) = show tm

@@ -88,7 +94,7 @@ type Clause = ([Pat], (Term, Term))

8894type CS = ([Term], Int, [(Name, Type)])

8995

9096instance TermSize SC where

91− termsize n (Case n' as) = termsize n as

97+ termsize n (Case _ n' as) = termsize n as

9298 termsize n (ProjCase n' as) = termsize n as

9399 termsize n (STerm t) = termsize n t

94100 termsize n _ = 1

@@ -111,7 +117,7 @@ small n args t = let as = findAllUsedArgs t args in

111117

112118namesUsed :: SC -> [Name]

113119namesUsed sc = nub $ nu' [] sc where

114− nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]

120+ nu' ps (Case _ n alts) = nub (concatMap (nua ps) alts) \\ [n]

115121 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

116122 nu' ps (STerm t) = nub $ nut ps t

117123 nu' ps _ = []

@@ -136,7 +142,7 @@ namesUsed sc = nub $ nu' [] sc where

136142

137143findCalls :: SC -> [Name] -> [(Name, [[Name]])]

138144findCalls sc topargs = nub $ nu' topargs sc where

139− nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

145+ nu' ps (Case _ n alts) = nub (concatMap (nua (n : ps)) alts)

140146 nu' ps (ProjCase t alts) = nub $ nut ps t ++ concatMap (nua ps) alts

141147 nu' ps (STerm t) = nub $ nut ps t

142148 nu' ps _ = []

@@ -189,7 +195,7 @@ findUsedArgs :: SC -> [Name] -> [Name]

189195findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

190196

191197findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where

192− nu' (Case n alts) = n : concatMap nua alts

198+ nu' (Case _ n alts) = n : concatMap nua alts

193199 nu' (ProjCase t alts) = directUse t ++ concatMap nua alts

194200 nu' (STerm t) = directUse t

195201 nu' _ = []

@@ -204,7 +210,7 @@ findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where

204210isUsed :: SC -> Name -> Bool

205211isUsed sc n = used sc where

206212

207− used (Case n' alts) = n == n' || or (map usedA alts)

213+ used (Case _ n' alts) = n == n' || or (map usedA alts)

208214 used (ProjCase t alts) = n `elem` freeNames t || or (map usedA alts)

209215 used (STerm t) = n `elem` freeNames t

210216 used _ = False

@@ -276,7 +282,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

276282

277283 acc [] n = Error (Inaccessible n)

278284 acc (PV x t : xs) n | x == n = OK ()

279− acc (PCon _ _ ps : xs) n = acc (ps ++ xs) n

285+ acc (PCon _ _ _ ps : xs) n = acc (ps ++ xs) n

280286 acc (PSuc p : xs) n = acc (p : xs) n

281287 acc (_ : xs) n = acc xs n

282288

@@ -285,7 +291,7 @@ simpleCase tc cover reflect phase fc inacc argtys cs erInfo

285291-- going on).

286292

287293checkSameTypes :: [(Name, Type)] -> SC -> Bool

288−checkSameTypes tys (Case n alts)

294+checkSameTypes tys (Case _ n alts)

289295 = case lookup n tys of

290296 Just t -> and (map (checkAlts t) alts)

291297 _ -> and (map ((checkSameTypes tys).getSC) alts)

@@ -324,7 +330,7 @@ isConstType (B32V _) (AType (ATInt _)) = True

324330isConstType (B64V _) (AType (ATInt _)) = True

325331isConstType _ _ = False

326332

327−data Pat = PCon Name Int [Pat]

333+data Pat = PCon Bool Name Int [Pat]

328334 | PConst Const

329335 | PV Name Type

330336 | PSuc Pat -- special case for n+1 on Integer

@@ -344,34 +350,18 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where

344350toPat :: Bool -> Bool -> [Term] -> [Pat]

345351toPat reflect tc = map $ toPat' []

346352 where

347− toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)

353+ toPat' [_,_,arg](P (DCon t a uniq) nm@(UN n) _)

348354 | n == txt "Delay"

349− = PCon nm t [PAny, PAny, toPat' [] arg]

355+ = PCon uniq nm t [PAny, PAny, toPat' [] arg]

350356

351− toPat' args (P (DCon t a) n _)

352− = PCon n t $ map (toPat' []) args

357+ toPat' args (P (DCon t a uniq) n _)

358+ = PCon uniq n t $ map (toPat' []) args

353359

354360 -- n + 1

355361 toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)

356362 | pabi == txt "prim__addBigInt"

357363 = PSuc $ toPat' [] p

358364

359− -- Typecase

360−-- toPat' (P (TCon t a) n _) args | tc

361−-- = do args' <- mapM (\x -> toPat' x []) args

362−-- return $ PCon n t args'

363−-- toPat' (Constant (AType (ATInt ITNative))) []

364−-- | tc = return $ PCon (UN "Int") 1 []

365−-- toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

366−-- toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

367−-- toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

368−-- toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

369−-- toPat' (Constant (AType (ATInt ITBig))) []

370−-- | tc = return $ PCon (UN "Integer") 6 []

371−-- toPat' (Constant (AType (ATInt (ITFixed n)))) []

372−-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive

373−--

374−

375365 toPat' [] (P Bound n ty) = PV n ty

376366 toPat' args (App f a) = toPat' (a : args) f

377367 toPat' [] (Constant (AType _)) = PTyPat

@@ -405,7 +395,7 @@ isVarPat (PAny : ps , _) = True

405395isVarPat (PTyPat : ps , _) = True

406396isVarPat _ = False

407397

408−isConPat (PCon _ _ _ : ps, _) = True

398+isConPat (PCon _ _ _ _ : ps, _) = True

409399isConPat (PReflected _ _ : ps, _) = True

410400isConPat (PSuc _ : ps, _) = True

411401isConPat (PConst _ : ps, _) = True

@@ -449,18 +439,18 @@ order ns' cs = let patnames = transpose (map (zip ns') (map fst cs))

449439 noClash [] = True

450440 noClash (p : ps) = not (any (clashPat p) ps) && noClash ps

451441

452− clashPat (PCon _ _ _) (PConst _) = True

453− clashPat (PConst _) (PCon _ _ _) = True

454− clashPat (PCon _ _ _) (PSuc _) = True

455− clashPat (PSuc _) (PCon _ _ _) = True

456− clashPat (PCon n i _) (PCon n' i' _) | i == i' = n /= n'

442+ clashPat (PCon _ _ _ _) (PConst _) = True

443+ clashPat (PConst _) (PCon _ _ _ _) = True

444+ clashPat (PCon _ _ _ _) (PSuc _) = True

445+ clashPat (PSuc _) (PCon _ _ _ _) = True

446+ clashPat (PCon _ n i _) (PCon _ n' i' _) | i == i' = n /= n'

457447 clashPat _ _ = False

458448

459449 -- this compares (+isInaccessible, -numberOfCases)

460450 moreDistinct xs ys = compare (snd . fst . head $ xs, numNames [] (map snd ys))

461451 (snd . fst . head $ ys, numNames [] (map snd xs))

462452

463− numNames xs (PCon n _ _ : ps)

453+ numNames xs (PCon _ n _ _ : ps)

464454 | not (Left n `elem` xs) = numNames (Left n : xs) ps

465455 numNames xs (PConst c : ps)

466456 | not (Right c `elem` xs) = numNames (Right c : xs) ps

@@ -497,7 +487,8 @@ data ConType = CName Name Int -- named constructor

497487 | CConst Const -- constant, not implemented yet

498488 deriving (Show, Eq)

499489

500−data Group = ConGroup ConType -- Constructor

490+data Group = ConGroup Bool -- Uniqueness flag

491+ ConType -- Constructor

501492 [([Pat], Clause)] -- arguments and rest of alternative

502493 deriving Show

503494

@@ -507,26 +498,30 @@ conRule (v:vs) cs err = do groups <- groupCons cs

507498

508499caseGroups :: [Name] -> [Group] -> SC -> CaseBuilder SC

509500caseGroups (v:vs) gs err = do g <- altGroups gs

510− return $ Case v (sort g)

501+ return $ Case (getShared gs) v (sort g)

511502 where

503+ getShared (ConGroup True _ _ : _) = Updatable

504+ getShared _ = Shared

505+

512506 altGroups [] = return [DefaultCase err]

513507

514− altGroups (ConGroup (CName n i) args : cs)

508+ altGroups (ConGroup _ (CName n i) args : cs)

515509 = (:) <$> altGroup n i args <*> altGroups cs

516510

517− altGroups (ConGroup (CFn n) args : cs)

511+ altGroups (ConGroup _ (CFn n) args : cs)

518512 = (:) <$> altFnGroup n args <*> altGroups cs

519513

520− altGroups (ConGroup CSuc args : cs)

514+ altGroups (ConGroup _ CSuc args : cs)

521515 = (:) <$> altSucGroup args <*> altGroups cs

522516

523− altGroups (ConGroup (CConst c) args : cs)

517+ altGroups (ConGroup _ (CConst c) args : cs)

524518 = (:) <$> altConstGroup c args <*> altGroups cs

525519

526− altGroup n i args = do inacc <- inaccessibleArgs n

527− (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

528− matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

529− return $ ConCase n i newVars matchCs

520+ altGroup n i args

521+ = do inacc <- inaccessibleArgs n

522+ (newVars, accVars, inaccVars, nextCs) <- argsToAlt inacc args

523+ matchCs <- match (accVars ++ vs ++ inaccVars) nextCs err

524+ return $ ConCase n i newVars matchCs

530525

531526 altFnGroup n args = do (newVars, _, [], nextCs) <- argsToAlt [] args

532527 matchCs <- match (newVars ++ vs) nextCs err

@@ -601,21 +596,21 @@ groupCons cs = gc [] cs

601596 do acc' <- addGroup p ps res acc

602597 gc acc' cs

603598 addGroup p ps res acc = case p of

604− PCon con i args -> return $ addg (CName con i) args (ps, res) acc

599+ PCon uniq con i args -> return $ addg uniq (CName con i) args (ps, res) acc

605600 PConst cval -> return $ addConG cval (ps, res) acc

606− PSuc n -> return $ addg CSuc [n] (ps, res) acc

607− PReflected fn args -> return $ addg (CFn fn) args (ps, res) acc

601+ PSuc n -> return $ addg False CSuc [n] (ps, res) acc

602+ PReflected fn args -> return $ addg False (CFn fn) args (ps, res) acc

608603 pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"

609604

610− addg c conargs res []

611− = [ConGroup c [(conargs, res)]]

612− addg c conargs res (g@(ConGroup c' cs):gs)

613− | c == c' = ConGroup c (cs ++ [(conargs, res)]) : gs

614− | otherwise = g : addg c conargs res gs

605+ addg uniq c conargs res []

606+ = [ConGroup uniq c [(conargs, res)]]

607+ addg uniq c conargs res (g@(ConGroup _ c' cs):gs)

608+ | c == c' = ConGroup uniq c (cs ++ [(conargs, res)]) : gs

609+ | otherwise = g : addg uniq c conargs res gs

615610

616− addConG con res [] = [ConGroup (CConst con) [([], res)]]

617− addConG con res (g@(ConGroup (CConst n) cs) : gs)

618− | con == n = ConGroup (CConst n) (cs ++ [([], res)]) : gs

611+ addConG con res [] = [ConGroup False (CConst con) [([], res)]]

612+ addConG con res (g@(ConGroup False (CConst n) cs) : gs)

613+ | con == n = ConGroup False (CConst n) (cs ++ [([], res)]) : gs

619614-- | otherwise = g : addConG con res gs

620615 addConG con res (g : gs) = g : addConG con res gs

621616

@@ -637,7 +632,7 @@ depatt :: [Name] -> SC -> SC

637632depatt ns tm = dp [] tm

638633 where

639634 dp ms (STerm tm) = STerm (applyMaps ms tm)

640− dp ms (Case x alts) = Case x (map (dpa ms x) alts)

635+ dp ms (Case up x alts) = Case up x (map (dpa ms x) alts)

641636 dp ms sc = sc

642637

643638 dpa ms x (ConCase n i args sc)

@@ -667,7 +662,7 @@ depatt ns tm = dp [] tm

667662-- FIXME: Do this for SucCase too

668663prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

669664 -> SC -> SC

670−prune proj (Case n alts) = case alts' of

665+prune proj (Case up n alts) = case alts' of

671666 [] -> ImpossibleCase

672667

673668 -- Projection transformations prevent us from seeing some uses of ctor fields

@@ -689,7 +684,7 @@ prune proj (Case n alts) = case alts' of

689684 as@[ConCase cn i args sc]

690685 | proj -> let sc' = prune proj sc in

691686 if any (isUsed sc') args

692− then Case n [ConCase cn i args sc']

687+ then Case up n [ConCase cn i args sc']

693688 else sc'

694689

695690 [SucCase cn sc]

@@ -702,9 +697,9 @@ prune proj (Case n alts) = case alts' of

702697 -- Bit of a hack here! The default case will always be 0, make sure

703698 -- it gets caught first.

704699 [s@(SucCase _ _), DefaultCase dc]

705− -> Case n [ConstCase (BI 0) dc, s]

700+ -> Case up n [ConstCase (BI 0) dc, s]

706701

707− as -> Case n as

702+ as -> Case up n as

708703 where

709704 alts' = filter (not . erased) $ map pruneAlt alts

710705

@@ -719,10 +714,10 @@ prune proj (Case n alts) = case alts' of

719714 erased _ = False

720715

721716 projRep :: Name -> Name -> Int -> SC -> SC

722− projRep arg n i (Case x alts) | x == arg

717+ projRep arg n i (Case up x alts) | x == arg

723718 = ProjCase (Proj (P Bound n Erased) i) $ map (projRepAlt arg n i) alts

724− projRep arg n i (Case x alts)

725− = Case x (map (projRepAlt arg n i) alts)

719+ projRep arg n i (Case up x alts)

720+ = Case up x (map (projRepAlt arg n i) alts)

726721 projRep arg n i (ProjCase t alts)

727722 = ProjCase (projRepTm arg n i t) $ map (projRepAlt arg n i) alts

728723 projRep arg n i (STerm t) = STerm (projRepTm arg n i t)

@@ -749,9 +744,9 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

749744stripLambdas x = x

750745

751746substSC :: Name -> Name -> SC -> SC

752−substSC n repl (Case n' alts)

753− | n == n' = Case repl (map (substAlt n repl) alts)

754− | otherwise = Case n' (map (substAlt n repl) alts)

747+substSC n repl (Case up n' alts)

748+ | n == n' = Case up repl (map (substAlt n repl) alts)

749+ | otherwise = Case up n' (map (substAlt n repl) alts)

755750substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t

756751substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

757752substSC n repl ImpossibleCase = ImpossibleCase

@@ -771,11 +766,11 @@ substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

771766mkForce :: Name -> Name -> SC -> SC

772767mkForce = mkForceSC

773768 where

774− mkForceSC n arg (Case x alts) | x == arg

775− = Case n $ map (mkForceAlt n arg) alts

769+ mkForceSC n arg (Case up x alts) | x == arg

770+ = Case up n $ map (mkForceAlt n arg) alts

776771

777− mkForceSC n arg (Case x alts)

778− = Case x (map (mkForceAlt n arg) alts)

772+ mkForceSC n arg (Case up x alts)

773+ = Case up x (map (mkForceAlt n arg) alts)

779774

780775 mkForceSC n arg (ProjCase t alts)

781776 = ProjCase t $ map (mkForceAlt n arg) alts

src/Idris/Core/DeepSeq.hs+4−2

@@ -14,6 +14,7 @@ instance NFData Name where

1414

1515instance NFData SpecialName where

1616 rnf (WhereN x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

17+ rnf (WithN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

1718 rnf (InstanceN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

1819 rnf (ParentN x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

1920 rnf (MethodN x1) = rnf x1 `seq` ()

@@ -85,7 +86,7 @@ instance NFData UExp where

8586instance NFData NameType where

8687 rnf Bound = ()

8788 rnf Ref = ()

88− rnf (DCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

89+ rnf (DCon x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

8990 rnf (TCon x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

9091

9192instance (NFData n) => NFData (TT n) where

@@ -98,9 +99,10 @@ instance (NFData n) => NFData (TT n) where

9899 rnf Erased = ()

99100 rnf Impossible = ()

100101 rnf (TType x1) = rnf x1 `seq` ()

102+ rnf (UType _) = ()

101103

102104instance (NFData t) => NFData (SC' t) where

103− rnf (Case x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

105+ rnf (Case _ x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

104106 rnf (ProjCase x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

105107 rnf (STerm x1) = rnf x1 `seq` ()

106108 rnf (UnmatchedCase x1) = rnf x1 `seq` ()

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

@@ -404,9 +404,9 @@ matchProblems all = processTactic' (MatchProblems all)

404404unifyProblems :: Elab' aux ()

405405unifyProblems = processTactic' UnifyProblems

406406

407−defer :: Name -> Elab' aux ()

408−defer n = do n' <- unique_hole n

409− processTactic' (Defer n')

407+defer :: [Name] -> Name -> Elab' aux ()

408+defer ds n = do n' <- unique_hole n

409+ processTactic' (Defer ds n')

410410

411411deferType :: Name -> Raw -> [Name] -> Elab' aux ()

412412deferType n ty ns = processTactic' (DeferType n ty ns)

src/Idris/Core/Evaluate.hs+21−9

@@ -11,7 +11,8 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

1212 mapDefCtxt,

1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

15+ isUniverse) where

1516

1617import Debug.Trace

1718import Control.Applicative hiding (Const)

@@ -47,6 +48,7 @@ data Value = VP NameType Name Value

4748 | VBLet Int Name Value Value Value

4849 | VApp Value Value

4950 | VType UExp

51+ | VUType Universe

5052 | VErased

5153 | VImpossible

5254 | VConstant Const

@@ -290,7 +292,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

290292 t' <- ev ntimes stk top env t

291293-- tfull' <- reapply ntimes stk top env t' []

292294 return (doProj t' (getValArgs t'))

293− where doProj t' (VP (DCon _ _) _ _, args)

295+ where doProj t' (VP (DCon _ _ _) _ _, args)

294296 | i >= 0 && i < length args = args!!i

295297 doProj t' _ = VProj t' i

296298

@@ -298,6 +300,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

298300 ev ntimes stk top env Erased = return VErased

299301 ev ntimes stk top env Impossible = return VImpossible

300302 ev ntimes stk top env (TType i) = return $ VType i

303+ ev ntimes stk top env (UType u) = return $ VUType u

301304

302305 evApply ntimes stk top env args (VApp f a)

303306 = evApply ntimes stk top env (a:args) f

@@ -393,7 +396,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

393396 evTree ntimes stk top env amap (ProjCase t alts)

394397 = do t' <- ev ntimes stk top env t

395398 doCase ntimes stk top env amap t' alts

396− evTree ntimes stk top env amap (Case n alts)

399+ evTree ntimes stk top env amap (Case _ n alts)

397400 = case lookup n amap of

398401 Just v -> doCase ntimes stk top env amap v alts

399402 _ -> return Nothing

@@ -409,7 +412,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

409412 _ -> return Nothing

410413

411414 conHeaded tm@(App _ _)

412− | (P (DCon _ _) _ _, args) <- unApply tm = True

415+ | (P (DCon _ _ _) _ _, args) <- unApply tm = True

413416 conHeaded t = False

414417

415418 chooseAlt' ntimes stk env _ (f, args) alts amap

@@ -420,7 +423,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

420423 chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->

421424 [(Name, Value)] ->

422425 Eval (Maybe ([(Name, Value)], SC))

423− chooseAlt env _ (VP (DCon i a) _ _, args) alts amap

426+ chooseAlt env _ (VP (DCon i a _) _ _, args) alts amap

424427 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)

425428 | Just v <- findDefault alts = return $ Just (amap, v)

426429 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap

@@ -519,6 +522,7 @@ instance Quote Value where

519522 return (Bind n (Let t' v') sc'')

520523 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)

521524 quote i (VType u) = return $ TType u

525+ quote i (VUType u) = return $ UType u

522526 quote i VErased = return $ Erased

523527 quote i VImpossible = return $ Impossible

524528 quote i (VProj v j) = do v' <- quote i v

@@ -534,6 +538,11 @@ wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

534538wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

535539wknV i t = return t

536540

541+isUniverse :: Term -> Bool

542+isUniverse (TType _) = True

543+isUniverse (UType _) = True

544+isUniverse _ = False

545+

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

538547

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

@@ -573,11 +582,14 @@ convEq ctxt holes topx topy = ceq [] topx topy where

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

574583 put (v, ULE x y : cs)

575584 return True

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

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

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

576588 ceq ps Erased _ = return True

577589 ceq ps _ Erased = return True

578590 ceq ps x y = return False

579591

580− caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'

592+ caseeq ps (Case _ n cs) (Case _ n' cs') = caseeqA ((n,n'):ps) cs cs'

581593 where

582594 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')

583595 = do q1 <- caseeq (zip as as' ++ ps) sc sc'

@@ -780,7 +792,7 @@ addTyDecl n nt ty uctxt

780792 uctxt { definitions = ctxt' }

781793

782794addDatatype :: Datatype Name -> Context -> Context

783−addDatatype (Data n tag ty cons) uctxt

795+addDatatype (Data n tag ty unique cons) uctxt

784796 = let ctxt = definitions uctxt

785797 ty' = normalise uctxt [] ty

786798 ctxt' = addCons 0 cons (addDef n

@@ -791,7 +803,7 @@ addDatatype (Data n tag ty cons) uctxt

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

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

793805 addCons (tag+1) cons (addDef n

794− (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt)

806+ (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)

795807

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

797809addCasedef :: Name -> ErasureInfo -> CaseInfo ->

@@ -916,7 +928,7 @@ isDConName :: Name -> Context -> Bool

916928isDConName n ctxt

917929 = or $ do def <- lookupCtxt n (definitions ctxt)

918930 case tfst def of

919− (TyDecl (DCon _ _) _) -> return True

931+ (TyDecl (DCon _ _ _) _) -> return True

920932 _ -> return False

921933

922934isFnName :: Name -> Context -> Bool

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

@@ -146,7 +146,7 @@ execute tm = do est <- initState

146146 Right tm' -> return tm'

147147

148148ioWrap :: ExecVal -> ExecVal

149−ioWrap tm = mkEApp (EP (DCon 0 2) (sUN "prim__IO") EErased) [EErased, tm]

149+ioWrap tm = mkEApp (EP (DCon 0 2 False) (sUN "prim__IO") EErased) [EErased, tm]

150150

151151ioUnit :: ExecVal

152152ioUnit = ioWrap (EP Ref unitCon EErased)

@@ -171,7 +171,7 @@ doExec env ctxt p@(P Bound n ty) =

171171 case lookup n env of

172172 Nothing -> execFail . Msg $ "not found"

173173 Just tm -> return tm

174−doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

174+doExec env ctxt (P (DCon a b u) n _) = return (EP (DCon a b u) n EErased)

175175doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

176176doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

177177 | otherwise = execFail . Msg $ "env too small"

@@ -349,7 +349,7 @@ execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

349349 Just r -> return (mkEApp r xs')

350350 Nothing -> return (mkEApp f args)

351351

352−execApp env ctxt c@(EP (DCon _ arity) n _) args =

352+execApp env ctxt c@(EP (DCon _ arity _) n _) args =

353353 do let args' = take arity args

354354 let restArgs = drop arity args

355355 execApp env ctxt (mkEApp c args') restArgs

@@ -443,7 +443,7 @@ execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVa

443443execCase' env ctxt amap (UnmatchedCase _) = return Nothing

444444execCase' env ctxt amap (STerm tm) =

445445 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

446−execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

446+execCase' env ctxt amap (Case sh n alts) | Just tm <- lookup n amap =

447447 case chooseAlt tm alts of

448448 Just (newCase, newBindings) ->

449449 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

src/Idris/Core/ProofState.hs+8−7

@@ -75,7 +75,7 @@ data Tactic = Attack

7575 | PatVar Name

7676 | PatBind Name

7777 | Focus Name

78− | Defer Name

78+ | Defer [Name] Name

7979 | DeferType Name Raw [Name]

8080 | Instance Name

8181 | SetInjective Name

@@ -387,12 +387,13 @@ setinj n ctxt env (Bind x b sc)

387387 ps { injective = n : is })

388388 return (Bind x b sc)

389389

390−defer :: Name -> RunTactic

391−defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

392− do action (\ps -> let hs = holes ps in

390+defer :: [Name] -> Name -> RunTactic

391+defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

392+ do let env' = filter (\(n, t) -> n `notElem` dropped) env

393+ action (\ps -> let hs = holes ps in

393394 ps { holes = hs \\ [x] })

394− return (Bind n (GHole (length env) (mkTy (reverse env) t))

395− (mkApp (P Ref n ty) (map getP (reverse env))))

395+ return (Bind n (GHole (length env') (mkTy (reverse env') t))

396+ (mkApp (P Ref n ty) (map getP (reverse env'))))

396397 where

397398 mkTy [] t = t

398399 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

@@ -952,7 +953,7 @@ process t h = tactic (Just h) (mktac t)

952953 mktac (CheckIn r) = check_in r

953954 mktac (EvalIn r) = eval_in r

954955 mktac (Focus n) = focus n

955− mktac (Defer n) = defer n

956+ mktac (Defer ns n) = defer ns n

956957 mktac (DeferType n t a) = deferType n t a

957958 mktac (Instance n) = instanceArg n

958959 mktac (SetInjective n) = setinj n

src/Idris/Core/TT.hs+32−15

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

139139 | CantResolveAlts [Name]

140140 | IncompleteTerm t

141141 | UniverseError

142+ | UniqueError Name

143+ | UniqueKindError Name

142144 | ProgramLineComment

143145 | Inaccessible Name

144146 | NonCollapsiblePostulate Name

@@ -305,6 +307,7 @@ deriving instance NFData Name

305307!-}

306308

307309data SpecialName = WhereN Int Name Name

310+ | WithN Int Name

308311 | InstanceN Name [T.Text]

309312 | ParentN Name T.Text

310313 | MethodN Name

@@ -349,6 +352,7 @@ instance Show Name where

349352

350353instance Show SpecialName where

351354 show (WhereN i p c) = show p ++ ", " ++ show c

355+ show (WithN i n) = "with block in " ++ show n

352356 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

353357 show (MethodN m) = "method " ++ show m

354358 show (ParentN p c) = show p ++ "#" ++ T.unpack c

@@ -364,6 +368,7 @@ showCG (MN _ u) | u == txt "underscore" = "_"

364368showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

365369showCG (SN s) = showCG' s

366370 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

371+ showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i

367372 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

368373 showCG' (MethodN m) = '!':showCG m

369374 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

@@ -594,10 +599,18 @@ constDocs (B32V v) = "A vector of thirty-two-bit values"

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

595600constDocs prim = "Undocumented"

596601

602+data Universe = UniqueType | AllTypes

603+ deriving (Eq, Ord)

604+

605+instance Show Universe where

606+ show UniqueType = "UniqueType"

607+ show AllTypes = "Type*"

608+

597609data Raw = Var Name

598610 | RBind Name (Binder Raw) Raw

599611 | RApp Raw Raw

600612 | RType

613+ | RUType Universe

601614 | RForce Raw

602615 | RConstant Const

603616 deriving (Show, Eq)

@@ -607,6 +620,7 @@ instance Sized Raw where

607620 size (RBind name bind right) = 1 + size bind + size right

608621 size (RApp left right) = 1 + size left + size right

609622 size RType = 1

623+ size (RUType _) = 1

610624 size (RForce raw) = 1 + size raw

611625 size (RConstant const) = size const

612626

@@ -717,7 +731,7 @@ type UCs = (Int, [UConstraint])

717731

718732data NameType = Bound

719733 | Ref

720− | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor

734+ | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

721735 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

722736 deriving (Show, Ord)

723737{-!

@@ -734,7 +748,7 @@ instance Pretty NameType OutputAnnotation where

734748instance Eq NameType where

735749 Bound == Bound = True

736750 Ref == Ref = True

737− DCon _ a == DCon _ b = (a == b) -- ignore tag

751+ DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag

738752 TCon _ a == TCon _ b = (a == b) -- ignore tag

739753 _ == _ = False

740754

@@ -753,6 +767,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

753767 | Erased -- ^ an erased term

754768 | Impossible -- ^ special case for totality checking

755769 | TType UExp -- ^ the type of types at some level

770+ | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

756771 deriving (Ord, Functor)

757772{-!

758773deriving instance Binary TT

@@ -802,6 +817,7 @@ type EnvTT n = [(n, Binder (TT n))]

802817data Datatype n = Data { d_typename :: n,

803818 d_typetag :: Int,

804819 d_type :: (TT n),

820+ d_unique :: Bool,

805821 d_cons :: [(n, TT n)] }

806822 deriving (Show, Functor, Eq)

807823

@@ -823,7 +839,7 @@ instance Eq n => Eq (TT n) where

823839-- constant, the type Type, pi-binding, or an application of an injective

824840-- term.

825841isInjective :: TT n -> Bool

826−isInjective (P (DCon _ _) _ _) = True

842+isInjective (P (DCon _ _ _) _ _) = True

827843isInjective (P (TCon _ _) _ _) = True

828844isInjective (Constant _) = True

829845isInjective (TType x) = True

@@ -1054,18 +1070,18 @@ unList tm = case unApply tm of

10541070-- with the corresponding name. It is an error if there are free de

10551071-- Bruijn indices.

10561072forget :: TT Name -> Raw

1057−forget tm = fe [] tm

1058− where

1059− fe env (P _ n _) = Var n

1060− fe env (V i) = Var (env !! i)

1061− fe env (Bind n b sc) = let n' = uniqueName n env in

1062− RBind n' (fmap (fe env) b)

1063− (fe (n':env) sc)

1064− fe env (App f a) = RApp (fe env f) (fe env a)

1065− fe env (Constant c)

1066− = RConstant c

1067− fe env (TType i) = RType

1068− fe env Erased = RConstant Forgot

1073+forget tm = forgetEnv [] tm

1074+

1075+forgetEnv env (P _ n _) = Var n

1076+forgetEnv env (V i) = Var (env !! i)

1077+forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1078+ RBind n' (fmap (forgetEnv env) b)

1079+ (forgetEnv (n':env) sc)

1080+forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1081+forgetEnv env (Constant c) = RConstant c

1082+forgetEnv env (TType i) = RType

1083+forgetEnv env (UType u) = RUType u

1084+forgetEnv env Erased = RConstant Forgot

10691085

10701086-- | Introduce a 'Bind' into the given term for each element of the

10711087-- given list of (name, binder) pairs.

@@ -1246,6 +1262,7 @@ showEnv' env t dbg = se 10 env t where

12461262 se p env Erased = "[__]"

12471263 se p env Impossible = "[impossible]"

12481264 se p env (TType i) = "Type " ++ show i

1265+ se p env (UType u) = show u

12491266

12501267 sb env n (Lam t) = showb env "\\ " " => " n t

12511268 sb env n (Hole t) = showb env "? " ". " n t

src/Idris/Core/Typecheck.hs+61−27

@@ -47,8 +47,8 @@ errEnv = map (\(x, b) -> (x, binderTy b))

4747

4848isType :: Context -> Env -> Term -> TC ()

4949isType ctxt env tm = isType' (normalise ctxt env tm)

50− where isType' (TType _) = return ()

51− isType' tm = fail (showEnv env tm ++ " is not a TType")

50+ where isType' tm | isUniverse tm = return ()

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

5252

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

5454recheck ctxt env tm orig

@@ -57,10 +57,12 @@ recheck ctxt env tm orig

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

5858 Error e -> Error e

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

60− return (tm, ty, constraints)

60+ do checkUnique ctxt env tm

61+ return (tm, ty, constraints)

6162

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

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

64+check ctxt env tm

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

6466

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

6668check' holes ctxt env top = chk env top where

@@ -79,29 +81,24 @@ check' holes ctxt env top = chk env top where

7981 _ -> normalise ctxt env fty

8082 case fty' of

8183 Bind x (Pi s) t ->

82−-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

83−-- " from " ++ show fv ++ " : " ++ show fty) $

8484 do convertsC ctxt env aty s

85− -- let apty = normalise initContext env

86− -- (Bind x (Let aty av) t)

8785 let apty = simplify initContext env

8886 (Bind x (Let aty av) t)

8987 return (App fv av, apty)

90− t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"

91− -- This rather unpleasant hack is needed because during incomplete

92− -- proofs, variables are locally bound with an explicit name. If we just

93− -- make sure bound names in function types are locally unique, machine

94− -- generated names, we'll be fine.

95− -- NOTE: now replaced with 'uniqueBinders' above

96− where renameBinders i (Bind x (Pi s) t) = Bind (sMN i "binder") (Pi s)

97− (renameBinders (i+1) t)

98− renameBinders i sc = sc

88+ t -> lift $ tfail $ NonFunctionType fv fty

9989 chk env RType

10090 | holes = return (TType (UVal 0), TType (UVal 0))

10191 | otherwise = do (v, cs) <- get

10292 let c = ULT (UVar v) (UVar (v+1))

10393 put (v+2, (c:cs))

10494 return (TType (UVar v), TType (UVar (v+1)))

95+ chk env (RUType u)

96+ | holes = return (UType u, TType (UVal 0))

97+ | otherwise = do -- TODO! (v, cs) <- get

98+ -- let c = ULT (UVar v) (UVar (v+1))

99+ -- put (v+2, (c:cs))

100+ -- return (TType (UVar v), TType (UVar (v+1)))

101+ return (UType u, TType (UVal 0))

105102 chk env (RConstant Forgot) = return (Erased, Erased)

106103 chk env (RConstant c) = return (Constant c, constType c)

107104 where constType (I _) = Constant (AType (ATInt ITNative))

@@ -125,11 +122,17 @@ check' holes ctxt env top = chk env top where

125122 = do (sv, st) <- chk env s

126123 (tv, tt) <- chk ((n, Pi sv) : env) t

127124 (v, cs) <- get

128− let TType su = normalise ctxt env st

129− let TType tu = normalise ctxt env tt

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

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

125+ case (normalise ctxt env st, normalise ctxt env tt) of

126+ (TType su, TType tu) -> do

127+ 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))

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

130+ (UType 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+ (pToV n tv), UType u)

133136 chk env (RBind n b sc)

134137 = do b' <- checkBinder b

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

@@ -140,12 +143,6 @@ check' holes ctxt env top = chk env top where

140143 let tt' = normalise ctxt env tt

141144 lift $ isType ctxt env tt'

142145 return (Lam tv)

143− checkBinder (Pi t)

144− = do (tv, tt) <- chk env t

145− let tv' = normalise ctxt env tv

146− let tt' = normalise ctxt env tt

147− lift $ isType ctxt env tt'

148− return (Pi tv)

149146 checkBinder (Let t v)

150147 = do (tv, tt) <- chk env t

151148 (vv, vt) <- chk env v

@@ -219,3 +216,40 @@ check' holes ctxt env top = chk env top where

219216 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

220217 discharge n (PVTy t) scv sct

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

219+

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

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

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

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

224+ where

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

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

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

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

229+ chkBinders env (Bind n b t)

230+ = do chkBinderName env n b

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

232+ chkBinders env t = return ()

233+

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

235+ chkBinderName env n b

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

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

238+ case kind of

239+ UType UniqueType -> do ns <- get

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

241+ UType AllTypes -> do ns <- get

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

243+ _ -> return ()

244+ chkBinders env (binderTy b)

245+ case b of

246+ Let t v -> chkBinders env v

247+ _ -> return ()

248+

249+ chkName n

250+ = do ns <- get

251+ case lookup n ns of

252+ Nothing -> return ()

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

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

255+

src/Idris/Core/Unify.hs+19−18

@@ -85,12 +85,12 @@ match_unify ctxt env topx topy inj holes from =

8585 -- answer, merely a valid one, so perhaps we're okay.

8686 -- In other words: it may vanish without warning some day :)

8787 un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

88− | (P (DCon _ _) _ _, _) <- unApply x,

88+ | (P (DCon _ _ _) _ _, _) <- unApply x,

8989 holeIn env f || f `elem` holes

9090 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

9191 checkCycle names (f, Bind n' (Lam t) x)

9292 un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

93− | (P (DCon _ _) _ _, _) <- unApply x,

93+ | (P (DCon _ _ _) _ _, _) <- unApply x,

9494 holeIn env f || f `elem` holes

9595 = let n' = uniqueName fn (map fst env) in

9696 checkCycle names (f, Bind n' (Lam t) x)

@@ -265,11 +265,11 @@ unify ctxt env topx topy inj holes usersupp from =

265265-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

266266 Error e -> tfail e

267267 where

268− headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

268+ headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

269269 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

270270 headDiff _ _ = False

271271

272− injective (P (DCon _ _) _ _) = True

272+ injective (P (DCon _ _ _) _ _) = True

273273 injective (P (TCon _ _) _ _) = True

274274-- injective (App f (P _ _ _)) = injective f

275275-- injective (App f (Constant _)) = injective f

@@ -315,13 +315,13 @@ unify ctxt env topx topy inj holes usersupp from =

315315 StateT UInfo

316316 TC [(Name, TT Name)]

317317 un' fn names x y | x == y = return [] -- shortcut

318− un' fn names topx@(P (DCon _ _) x _) topy@(P (DCon _ _) y _)

318+ un' fn names topx@(P (DCon _ _ _) x _) topy@(P (DCon _ _ _) y _)

319319 | x /= y = unifyFail topx topy

320320 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)

321321 | x /= y = unifyFail topx topy

322− un' fn names topx@(P (DCon _ _) x _) topy@(P (TCon _ _) y _)

322+ un' fn names topx@(P (DCon _ _ _) x _) topy@(P (TCon _ _) y _)

323323 = unifyFail topx topy

324− un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _) y _)

324+ un' fn names topx@(P (TCon _ _) x _) topy@(P (DCon _ _ _) y _)

325325 = unifyFail topx topy

326326 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

327327 = unifyFail topx topy

@@ -427,6 +427,7 @@ unify ctxt env topx topy inj holes usersupp from =

427427 sameBinder _ _ = False

428428 un' fn bnames x y

429429 | OK True <- convEq' ctxt holes x y = do sc 1; return []

430+ | isUniverse x && isUniverse y = do sc 1; return []

430431 | otherwise = do UI s f <- get

431432 let r = recoverable (normalise ctxt env x)

432433 (normalise ctxt env y)

@@ -460,13 +461,13 @@ unify ctxt env topx topy inj holes usersupp from =

460461 | otherwise = unifyTmpFail appx appy

461462 where hnormalise [] _ _ t = t

462463 hnormalise ns ctxt env t = normalise ctxt env t

463− checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

464+ checkHeads (P (DCon _ _ _) x _) (P (DCon _ _ _) y _)

464465 | x /= y = unifyFail appx appy

465466 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

466467 | x /= y = unifyFail appx appy

467− checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)

468+ checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)

468469 = unifyFail appx appy

469− checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)

470+ checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)

470471 = unifyFail appx appy

471472 checkHeads _ _ = return []

472473

@@ -492,7 +493,7 @@ unify ctxt env topx topy inj holes usersupp from =

492493 all (\x -> pat x || metavar x) (f : args)

493494 && nub args == args

494495

495− rigid (P (DCon _ _) _ _) = True

496+ rigid (P (DCon _ _ _) _ _) = True

496497 rigid (P (TCon _ _) _ _) = True

497498 rigid t@(P Ref _ _) = inenv t || globmetavar t

498499 rigid (Constant _) = True

@@ -632,15 +633,15 @@ recoverable t@(App _ _) _

632633 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

633634recoverable _ t@(App _ _)

634635 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

635−recoverable (P (DCon _ _) x _) (P (DCon _ _) y _) = x == y

636+recoverable (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x == y

636637recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

637−recoverable (Constant _) (P (DCon _ _) y _) = False

638+recoverable (Constant _) (P (DCon _ _ _) y _) = False

638639recoverable (Constant x) (Constant y) = x == y

639−recoverable (P (DCon _ _) x _) (Constant _) = False

640+recoverable (P (DCon _ _ _) x _) (Constant _) = False

640641recoverable (Constant _) (P (TCon _ _) y _) = False

641642recoverable (P (TCon _ _) x _) (Constant _) = False

642−recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

643−recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

643+recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

644+recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

644645recoverable p@(Constant _) (App f a) = recoverable p f

645646recoverable (App f a) p@(Constant _) = recoverable f p

646647recoverable p@(P _ n _) (App f a) = recoverable p f

@@ -650,10 +651,10 @@ recoverable (App f a) (App f' a')

650651recoverable (App f a) (App f' a')

651652 = recoverable f f' -- && recoverable a a'

652653recoverable f (Bind _ (Pi _) sc)

653− | (P (DCon _ _) _ _, _) <- unApply f = False

654+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

654655 | (P (TCon _ _) _ _, _) <- unApply f = False

655656recoverable (Bind _ (Pi _) sc) f

656− | (P (DCon _ _) _ _, _) <- unApply f = False

657+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

657658 | (P (TCon _ _) _ _, _) <- unApply f = False

658659recoverable (Bind _ (Lam _) sc) f = recoverable sc f

659660recoverable f (Bind _ (Lam _) sc) = recoverable f sc

src/Idris/Coverage.hs+5−5

@@ -206,7 +206,7 @@ genAll i args

206206 otherPats arg = return Placeholder

207207

208208 ops fc n xs o

209− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

209+ | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)

210210 = do xs' <- mapM otherPats (map getExpTm xs)

211211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212212 let tyn = getTy n (tt_ctxt i)

@@ -341,7 +341,7 @@ calcProd i fc topn pats

341341 return (and ok)

342342 _ -> return True -- defined elsewhere, can't call topn

343343

344− cotype (DCon _ _) n ty

344+ cotype (DCon _ _ _) n ty

345345 | (P _ t _, _) <- unApply (getRetTy ty)

346346 = case lookupCtxt t (idris_datatypes i) of

347347 [TI _ True _ _ _] -> True

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

391391 setTotality n t'

392392 addIBC (IBCTotal n t')

393393 return t'

394− [TyDecl (DCon _ _) ty] ->

394+ [TyDecl (DCon _ _ _) ty] ->

395395 case unApply (getRetTy ty) of

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

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

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

558558 | a == t = isInductive (fst (unApply (getRetTy tyn)))

559559 (fst (unApply (getRetTy tyt)))

560560 smaller ty a (ap@(App f s), _)

561− | (P (DCon _ _) n _, args) <- unApply ap

561+ | (P (DCon _ _ _) n _, args) <- unApply ap

562562 = let tyn = getType n in

563563 any (smaller (ty `mplus` Just tyn) a)

564564 (zip args (map toJust (getArgTys tyn)))

@@ -652,7 +652,7 @@ checkMP ist i mp = if i > 0

652652-- = Partial BelieveMe

653653 -- if we get to a constructor, it's fine as long as it's strictly positive

654654 tryPath desc path ((f, _) : es) arg

655− | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

655+ | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)

656656 = case lookupTotal f (tt_ctxt ist) of

657657 [Total _] -> Unchecked -- okay so far

658658 [Partial _] -> Partial (Other [f])

src/Idris/DataOpts.hs+8−7

@@ -72,19 +72,19 @@ instance Optimisable (TT Name) where

7272 applyOpts (P _ (NS (UN fn) mod) _)

7373 | fn == txt "toIntegerNat" && mod == prel

7474 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

75− applyOpts c@(P (DCon t arity) n _)

76− = return $ applyDataOptRT n t arity []

75+ applyOpts c@(P (DCon t arity uniq) n _)

76+ = return $ applyDataOptRT n t arity uniq []

7777 applyOpts t@(App f a)

78− | (c@(P (DCon t arity) n _), args) <- unApply t

79− = applyDataOptRT n t arity <$> mapM applyOpts args

78+ | (c@(P (DCon t arity uniq) n _), args) <- unApply t

79+ = applyDataOptRT n t arity uniq <$> mapM applyOpts args

8080 | otherwise = App <$> applyOpts f <*> applyOpts a

8181 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

8282 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

8383 applyOpts t = return t

8484

8585-- Need to saturate arguments first to ensure that optimisation happens uniformly

86−applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term

87−applyDataOptRT n tag arity args

86+applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term

87+applyDataOptRT n tag arity uniq args

8888 | length args == arity = doOpts n args

8989 | otherwise = let extra = satArgs (arity - length args)

9090 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

@@ -104,4 +104,5 @@ applyDataOptRT n tag arity args

104104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

105105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106106

107− doOpts n args = mkApp (P (DCon tag arity) n Erased) args

107+ doOpts n args = mkApp (P (DCon tag arity uniq) n Erased) args

108+

src/Idris/DeepSeq.hs+1

@@ -214,6 +214,7 @@ instance NFData PTerm where

214214 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

215215 rnf (PHidden x1) = rnf x1 `seq` ()

216216 rnf PType = ()

217+ rnf (PUniverse _) = ()

217218 rnf (PGoal x1 x2 x3 x4)

218219 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

219220 rnf (PConstant x1) = x1 `seq` ()

src/Idris/Delaborate.hs+5

@@ -80,6 +80,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8080 de env _ Erased = Placeholder

8181 de env _ Impossible = Placeholder

8282 de env _ (TType i) = PType

83+ de env _ (UType u) = PUniverse u

8384

8485 dens x | fullname = x

8586 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

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

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

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

225226pprintErr' i UniverseError = text "Universe inconsistency"

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

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

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

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

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

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

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

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

@@ -722,7 +722,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

722722 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

723723 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

724724 logLvl 5 ("New function type " ++ show wtype)

725− let wname = sMN windex (show fname)

725+ let wname = SN (WithN windex fname)

726726

727727 let imps = getImps wtype -- add to implicits context

728728 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

src/Idris/Elab/Data.hs+22−7

@@ -54,7 +54,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

5454 = do let codata = Codata `elem` opts

5555 iLOG (show (fc, doc))

5656 checkUndefined fc n

57− (cty, t, inacc) <- buildType info syn fc [] n t_in

57+ (cty, _, t, inacc) <- buildType info syn fc [] n t_in

5858

5959 addIBC (IBCDef n)

6060 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

@@ -63,7 +63,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

6363 = do let codata = Codata `elem` opts

6464 iLOG (show fc)

6565 undef <- isUndefined fc n

66− (cty, t, inacc) <- buildType info syn fc [] n t_in

66+ (cty, _, t, inacc) <- buildType info syn fc [] n t_in

6767 -- if n is defined already, make sure it is just a type declaration

6868 -- with the same type we've just elaborated

6969 i <- getIState

@@ -71,7 +71,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

7171 -- temporary, to check cons

7272 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

7373 let cnameinfo = cinfo info (map cname dcons)

74− cons <- mapM (elabCon cnameinfo syn n codata) dcons

74+ let unique = case getRetTy cty of

75+ UType UniqueType -> True

76+ _ -> False

77+ cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

7578 ttag <- getName

7679 i <- getIState

7780 let as = map (const Nothing) (getArgTys cty)

@@ -90,7 +93,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

9093 let metainf = DataMI params

9194 addIBC (IBCMetaInformation n metainf)

9295 -- TMP HACK! Make this a data option

93− updateContext (addDatatype (Data n ttag cty cons))

96+ updateContext (addDatatype (Data n ttag cty unique cons))

9497 updateContext (setMetaInformation n metainf)

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

9699-- mapM_ (checkPositive n) cons

@@ -203,12 +206,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

203206-- TODO: the above is a comment from the past;

204207-- forcenames is probably no longer needed

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

206− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

207−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

209+ Type -> -- for kind checking

210+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->

211+ Idris (Name, Type)

212+elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

208213 = do checkUndefined fc n

209− (cty, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

214+ (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

210215 ctxt <- getContext

211216 let cty' = normalise ctxt [] cty

217+ checkUniqueKind ckind expkind

212218

213219 -- Check that the constructor type is, in fact, a part of the family being defined

214220 tyIs n cty'

@@ -250,6 +256,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

250256 | otherwise = getNamePos (i + 1) sc x

251257 getNamePos _ _ _ = Nothing

252258

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 UniqueType) (UType UniqueType) = return ()

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

263+ checkUniqueKind (UType UniqueType) (TType _)

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

265+ checkUniqueKind (UType AllTypes) _ = return ()

266+ checkUniqueKind (TType _) _ = return ()

267+

253268type EliminatorState = StateT (Map.Map String Int) Idris

254269

255270-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

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

@@ -49,7 +49,7 @@ import Data.List.Split (splitOn)

4949import Util.Pretty(pretty, text)

5050

5151buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

52− Idris (Type, PTerm, [(Int, Name)])

52+ Idris (Type, Type, PTerm, [(Int, Name)])

5353buildType info syn fc opts n ty' = do

5454 ctxt <- getContext

5555 i <- getIState

@@ -80,7 +80,7 @@ buildType info syn fc opts n ty' = do

8080 logLvl 5 $ "Rechecking"

8181 logLvl 6 $ show tyT

8282 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

83− (cty, _) <- recheckC fc [] tyT

83+ (cty, ckind) <- recheckC fc [] tyT

8484

8585 -- record the implicit and inaccessible arguments

8686 i <- getIState

@@ -99,7 +99,7 @@ buildType info syn fc opts n ty' = do

9999 setFnInfo n fninfo

100100 addIBC (IBCFnInfo n fninfo)

101101

102− return (cty, ty, inacc)

102+ return (cty, ckind, ty, inacc)

103103 where

104104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

105105 patToImp (Bind n b sc) = Bind n b (patToImp sc)

@@ -121,7 +121,7 @@ elabType' :: Bool -> -- normalise it

121121elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

122122 n = liftname info n_in in -}

123123 do checkUndefined fc n

124− (cty, ty, inacc) <- buildType info syn fc opts n ty'

124+ (cty, _, ty, inacc) <- buildType info syn fc opts n ty'

125125

126126 addStatics n cty ty

127127 let nty = cty -- normalise ctxt [] cty

src/Idris/ElabDecls.hs+3−3

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

122122 p_synEq args = Nothing

123123

124124 nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased

125− vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

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

127− vnRefl = VP (DCon 0 2) eqCon VErased

125+ vnJust = VP (DCon 1 2 False) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

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

127+ vnRefl = VP (DCon 0 2 False) eqCon VErased

128128

129129 synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

130130 (Bind (sUN "b") (Pi (TType (UVar (-3))))

src/Idris/ElabTerm.hs+78−11

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

238238 -> ElabD ()

239239 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

240240 elab' ina PType = do apply RType []; solve

241+ elab' ina (PUniverse u) = do apply (RUType u) []; solve

241242-- elab' (_,_,inty) (PConstant c)

242243-- | constType c && pattern && not reflection && not inty

243244-- = lift $ tfail (Msg "Typecase is not allowed")

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

629630 elab' ina Placeholder = do (h : hs) <- get_holes

630631 movelast h

631632 elab' ina (PMetavar n) = let n' = mkN n in

632− do attack; defer n'; solve

633+ do attack; defer [] n'; solve

633634 where mkN n@(NS _ _) = n

634635 mkN n = case namespace info of

635636 Just xs@(_:_) -> sNS n xs

@@ -683,14 +684,39 @@ elab ist info emode opts fn tm

683684 focus valn

684685 elabE (True, a, inty, qq) scr

685686 args <- get_env

687+ envU <- mapM (getKind args) args

688+ let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts

689+-- ++ allNamesIn scr

690+

691+ -- in the definition we build for the case, only pass through

692+ -- names which are directly used, type class constraints, and

693+ -- variables any of these depend on

694+ -- FIXME: This probably doesn't help us, but leaving it in

695+ -- temporarily (but commented out). If this comment is still

696+ -- here in master, please delete the code!

697+-- let directUse = filter (\n -> usedIn namesUsedInRHS n

698+-- || tcName (binderTy (snd n))) args

699+-- let args' = args -- chaseDeps args (map fst directUse) directUse

700+-- let argsDropped = map fst $

701+-- filter (\(n, _) -> case lookup n args' of

702+-- Nothing -> True

703+-- _ -> False) args

704+

705+ -- Drop the unique arguments used in the scrutinee (since it's

706+ -- not valid to use them again anyway)

707+ let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)

708+ let args' = filter (\(n, _) -> n `notElem` argsDropped) args

709+

686710 cname <- unique_hole' True (mkCaseName fn)

687711 let cname' = mkN cname

688− elab' ina (PMetavar cname')

712+-- elab' ina (PMetavar cname')

713+ attack; defer argsDropped cname'; solve

714+

689715 -- if the scrutinee is one of the 'args' in env, we should

690716 -- inspect it directly, rather than adding it as a new argument

691717 let newdef = PClauses fc [] cname'

692718 (caseBlock fc cname'

693− (map (isScr scr) (reverse args)) opts)

719+ (map (isScr scr) (reverse args')) opts)

694720 -- elaborate case

695721 updateAux (newdef : )

696722 -- if we haven't got the type yet, hopefully we'll get it later!

@@ -704,6 +730,47 @@ elab ist info emode opts fn tm

704730 mkN n = case namespace info of

705731 Just xs@(_:_) -> sNS n xs

706732 _ -> n

733+

734+ isUnique envk n = case lookup n envk of

735+ Just u -> u

736+ _ -> False

737+

738+ getKind env (n, _)

739+ = case lookup n env of

740+ Nothing -> return (n, False) -- can't happen, actually...

741+ Just b ->

742+ do ty <- get_type (forget (binderTy b))

743+ case ty of

744+ UType UniqueType -> return (n, True)

745+ UType AllTypes -> return (n, True)

746+ _ -> return (n, False)

747+

748+ tcName tm | (P _ n _, _) <- unApply tm

749+ = case lookupCtxt n (idris_classes ist) of

750+ [_] -> True

751+ _ -> False

752+ tcName _ = False

753+

754+ usedIn ns (n, b)

755+ = n `elem` ns

756+ || any (\x -> x `elem` ns) (allTTNames (binderTy b))

757+

758+ -- FIXME: This probably doesn't help us here, but leaving

759+ -- it in temporarily... if this comment is still here in master,

760+ -- please delete the code!

761+ chaseDeps env acc [] = filter (\(n, _) -> n `elem` acc) env

762+ chaseDeps env acc ((n,b) : args)

763+ = let ns = allTTNames (binderTy b) in

764+ extendAcc ns acc args

765+ where

766+ extendAcc [] acc args = chaseDeps env acc args

767+ extendAcc (n:ns) acc args

768+ | elem n acc = extendAcc ns acc args

769+ | otherwise = case lookup n env of

770+ Just b -> extendAcc ns (n : acc)

771+ ((n,b) : args)

772+ Nothing -> extendAcc ns acc args

773+

707774 elab' ina (PUnifyLog t) = do unifyLog True

708775 elab' ina t

709776 unifyLog False

@@ -1541,7 +1608,7 @@ reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

15411608reifyTTNameType t@(App _ _)

15421609 = case unApply t of

15431610 (P _ f _, [Constant (I tag), Constant (I num)])

1544− | f == reflm "DCon" -> return $ DCon tag num

1611+ | f == reflm "DCon" -> return $ DCon tag num False -- FIXME: Uniqueness!

15451612 | f == reflm "TCon" -> return $ TCon tag num

15461613 _ -> fail ("Unknown reflection name type: " ++ show t)

15471614reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

@@ -1799,8 +1866,8 @@ reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

17991866reflectNameType :: NameType -> Raw

18001867reflectNameType (Bound) = Var (reflm "Bound")

18011868reflectNameType (Ref) = Var (reflm "Ref")

1802−reflectNameType (DCon x y)

1803− = reflCall "DCon" [RConstant (I x), RConstant (I y)]

1869+reflectNameType (DCon x y _)

1870+ = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

18041871reflectNameType (TCon x y)

18051872 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

18061873

@@ -2098,7 +2165,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

20982165 parts -> ReflectionError errorparts e

20992166

21002167fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2101−fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

2168+fromTTMaybe (App (App (P (DCon _ _ _) (NS (UN just) _) _) ty) tm)

21022169 | just == txt "Just" = Just tm

21032170fromTTMaybe x = Nothing

21042171

@@ -2109,9 +2176,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

21092176-- representation. Not in Idris or ElabD monads because it should be usable

21102177-- from either.

21112178reifyReportPart :: Term -> Either Err ErrorReportPart

2112−reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

2179+reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =

21132180 Right (TextPart msg)

2114−reifyReportPart (App (P (DCon _ _) n _) ttn)

2181+reifyReportPart (App (P (DCon _ _ _) n _) ttn)

21152182 | n == reflm "NamePart" =

21162183 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

21172184 Error e -> Left . InternalMsg $

@@ -2119,7 +2186,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

21192186 show ttn ++

21202187 " when reflecting an error:" ++ show e

21212188 OK (n', _)-> Right $ NamePart n'

2122−reifyReportPart (App (P (DCon _ _) n _) tm)

2189+reifyReportPart (App (P (DCon _ _ _) n _) tm)

21232190 | n == reflm "TermPart" =

21242191 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

21252192 Error e -> Left . InternalMsg $

@@ -2127,7 +2194,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

21272194 show tm ++

21282195 " when reflecting an error:" ++ show e

21292196 OK (tm', _) -> Right $ TermPart tm'

2130−reifyReportPart (App (P (DCon _ _) n _) tm)

2197+reifyReportPart (App (P (DCon _ _ _) n _) tm)

21312198 | n == reflm "SubReport" =

21322199 case unList tm of

21332200 Just xs -> do subParts <- mapM reifyReportPart xs

src/Idris/Erasure.hs+6−6

@@ -281,13 +281,13 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

281281

282282 -- for the purposes of erasure, we can disregard the projection

283283 getDepsSC fn es vs (ProjCase (Proj t i) alts) = getDepsSC fn es vs (ProjCase t alts) -- step

284− getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case n alts) -- base

284+ getDepsSC fn es vs (ProjCase (P _ n _) alts) = getDepsSC fn es vs (Case Shared n alts) -- base

285285

286286 -- other ProjCase's are not supported

287287 getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)

288288

289289 getDepsSC fn es vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) (etaExpand es t)

290− getDepsSC fn es vs (Case n alts)

290+ getDepsSC fn es vs (Case sh n alts)

291291 -- we case-split on this variable, which marks it as used

292292 -- (unless there is exactly one case branch)

293293 -- hence we add a new dependency, whose only precondition is

@@ -370,13 +370,13 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

370370 getDepsTerm vs bs cd app@(App _ _)

371371 | (fun, args) <- unApply app = case fun of

372372 -- instance constructors -> create metamethod deps

373− P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _

373+ P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

374374 -> conditionalDeps ctorName args -- regular data ctor stuff

375375 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

376376

377377 -- ordinary constructors

378378 P (TCon _ _) n _ -> unconditionalDeps args -- does not depend on anything

379− P (DCon _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

379+ P (DCon _ _ _) n _ -> conditionalDeps n args -- depends on whether (n,#) is used

380380

381381 -- mkForeign* calls must be special-cased because they are variadic

382382 -- All arguments must be marked as used, except for the first one,

@@ -469,7 +469,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

469469 -- Get the number of arguments that might be considered for erasure.

470470 getArity :: Name -> Int

471471 getArity (SN (WhereN i' ctorName (MN i field)))

472− | Just (TyDecl (DCon _ _) ty) <- lookupDefExact ctorName ctx

472+ | Just (TyDecl (DCon _ _ _) ty) <- lookupDefExact ctorName ctx

473473 = let argTys = map snd $ getArgTys ty

474474 in if i <= length argTys

475475 then length $ getArgTys (argTys !! i)

@@ -479,7 +479,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

479479

480480 getArity n = case lookupDefExact n ctx of

481481 Just (CaseOp ci ty tys def tot cdefs) -> length tys

482− Just (TyDecl (DCon tag arity) _) -> arity

482+ Just (TyDecl (DCon tag arity _) _) -> arity

483483 Just (TyDecl (Ref) ty) -> length $ getArgTys ty

484484 Just (Operator ty arity op) -> arity

485485 Just df -> error $ "Erasure/getArity: unrecognised entity '"

src/Idris/IBC.hs+24−7

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

3131import Util.Zlib (decompressEither)

3232

3333ibcVersion :: Word8

34−ibcVersion = 78

34+ibcVersion = 79

3535

3636data IBCFile = IBCFile { ver :: Word8,

3737 sourcefile :: FilePath,

@@ -183,8 +183,8 @@ ibc i (IBCDef n) f

183183 = do c' <- updateSC c; r' <- updateSC r

184184 return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))

185185

186− updateSC (Case n alts) = do alts' <- mapM updateAlt alts

187− return (Case n alts')

186+ updateSC (Case up n alts) = do alts' <- mapM updateAlt alts

187+ return (Case up n alts')

188188 updateSC (ProjCase t alts) = do t' <- update t

189189 alts' <- mapM updateAlt alts

190190 return (ProjCase t' alts')

@@ -631,12 +631,24 @@ instance Binary CGInfo where

631631 x4 <- get

632632 x5 <- get

633633 return (CGInfo x1 x2 [] x4 x5)

634+

635+instance Binary CaseType where

636+ put x = case x of

637+ Updatable -> putWord8 0

638+ Shared -> putWord8 1

639+ get = do i <- getWord8

640+ case i of

641+ 0 -> return Updatable

642+ 1 -> return Shared

643+ _ -> error "Corrupted binary data for CaseType"

644+

634645instance Binary SC where

635646 put x

636647 = case x of

637− Case x1 x2 -> do putWord8 0

638− put x1

639− put x2

648+ Case x1 x2 x3 -> do putWord8 0

649+ put x1

650+ put x2

651+ put x3

640652 ProjCase x1 x2 -> do putWord8 1

641653 put x1

642654 put x2

@@ -650,7 +662,8 @@ instance Binary SC where

650662 case i of

651663 0 -> do x1 <- get

652664 x2 <- get

653− return (Case x1 x2)

665+ x3 <- get

666+ return (Case x1 x2 x3)

654667 1 -> do x1 <- get

655668 x2 <- get

656669 return (ProjCase x1 x2)

@@ -1486,6 +1499,8 @@ instance Binary PTerm where

14861499 PDisamb x1 x2 -> do putWord8 37

14871500 put x1

14881501 put x2

1502+ PUniverse x1 -> do putWord8 38

1503+ put x1

14891504

14901505 get

14911506 = do i <- getWord8

@@ -1602,6 +1617,8 @@ instance Binary PTerm where

16021617 37 -> do x1 <- get

16031618 x2 <- get

16041619 return (PDisamb x1 x2)

1620+ 38 -> do x1 <- get

1621+ return (PUniverse x1)

16051622 _ -> error "Corrupted binary data for PTerm"

16061623

16071624instance (Binary t) => Binary (PTactic' t) where

src/Idris/ParseExpr.hs+2

@@ -307,7 +307,9 @@ simpleExpr syn =

307307 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

308308 <|> proofExpr syn

309309 <|> tacticsExpr syn

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

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

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

311313 <|> do c <- constant

312314 fc <- getFC

313315 return (modifyConst syn fc (PConstant c))

src/Idris/ProofSearch.hs+4−4

@@ -59,7 +59,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

5959 where

6060 -- if nothing worked, make a new metavariable

6161 tryAllFns [] | fromProver = cantSolveGoal

62− tryAllFns [] = do attack; defer nroot; solve

62+ tryAllFns [] = do attack; defer [] nroot; solve

6363 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

6464

6565 tryFn (f, args) = do let imps = map isImp args

@@ -75,7 +75,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

7575 if fromProver then cantSolveGoal

7676 else do

7777 mapM_ (\ h -> do focus h

78− attack; defer nroot; solve)

78+ attack; defer [] nroot; solve)

7979 (hs' \\ hs)

8080-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

8181 solve

@@ -96,7 +96,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

9696 toUN t = t

9797

9898 psRec _ 0 | fromProver = cantSolveGoal

99− psRec rec 0 = do attack; defer nroot; solve --fail "Maximum depth reached"

99+ psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"

100100 psRec False d = tryCons d hints

101101 psRec True d = try' (trivial elab ist)

102102 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

@@ -104,7 +104,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

104104 -- if all else fails, make a new metavariable

105105 (if fromProver

106106 then cantSolveGoal

107− else do attack; defer nroot; solve) True) True

107+ else do attack; defer [] nroot; solve) True) True

108108

109109 getFn d Nothing = []

110110 getFn d (Just f) | d < maxDepth-1 = [f]

src/Idris/Transforms.hs+2−2

@@ -25,10 +25,10 @@ instance Transform a => Transform (Binder a) where

2525

2626instance Transform SC where

2727 transform o@(CaseTrans t) sc = trans t sc where

28− trans t (Case n alts) = t (Case n (map (transform o) alts))

28+ trans t (Case up n alts) = t (Case up n (map (transform o) alts))

2929 trans t x = t x

3030 transform o@(TermTrans t) sc = trans t sc where

31− trans t (Case n alts) = Case n (map (transform o) alts)

31+ trans t (Case up n alts) = Case up n (map (transform o) alts)

3232 trans t (STerm tm) = STerm (t tm)

3333 trans t x = x

3434

src/Idris/WhoCalls.hs+2−2

@@ -36,13 +36,13 @@ namesBinder (NLet ty val) = names ty ++ names val

3636namesBinder b = names (binderTy b)

3737

3838occursSC :: Name -> SC -> Bool

39−occursSC n (Case _ alts) = any (occursCaseAlt n) alts

39+occursSC n (Case _ _ alts) = any (occursCaseAlt n) alts

4040occursSC n (ProjCase t alts) = occurs n t || any (occursCaseAlt n) alts

4141occursSC n (STerm t) = occurs n t

4242occursSC n _ = False

4343

4444namesSC :: SC -> [Name]

45−namesSC (Case _ alts) = concatMap namesCaseAlt alts

45+namesSC (Case _ _ alts) = concatMap namesCaseAlt alts

4646namesSC (ProjCase t alts) = names t ++ concatMap namesCaseAlt alts

4747namesSC (STerm t) = names t

4848namesSC _ = []

test/Makefile+1−1

@@ -14,7 +14,7 @@ test_js:

1414 @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node

1515

1616test_llvm:

17− @perl ./runtest.pl without sugar004 io003 buffer001 --codegen llvm

17+ @perl ./runtest.pl without primitives003 sugar004 io003 buffer001 --codegen llvm

1818

1919update:

2020 /usr/bin/env perl ./runtest.pl all -u

test/reg010/expected+1−1

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

1−reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

1+reg010.idr:5:15:When elaborating right hand side of with block in usubst.unsafeSubst:

22Can't unify

33 P x

44with

test/reg018/expected+1−1

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

11reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

22reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

33reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

4−reg018c.idr:19:1:CodataTest.inf is possibly not total due to: {CodataTest.inf19}

4+reg018c.idr:19:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf

55reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/reg028/expected+2−2

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

1−reg028.idr:5:1:tbad.bad is possibly not total due to: {tbad.bad16}

2−reg028a.idr:11:1:tbad.qsort' is possibly not total due to: {tbad.qsort'18}

1+reg028.idr:5:1:tbad.bad is possibly not total due to: with block in tbad.bad

2+reg028a.idr:11:1:tbad.qsort' is possibly not total due to: with block in tbad.qsort'

test/tutorial006/expected+1−1

@@ -10,7 +10,7 @@ When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:

1010 [92mplus[0m [95mn[0m [95mn[0m

1111 with

1212 [92mplus[0m [95mn[0m [95mm[0m

13−tutorial006b.idr:10:10:When elaborating right hand side of Main.parity:

13+tutorial006b.idr:10:10:When elaborating right hand side of with block in Main.parity:

1414Can't unify

1515 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

1616with