f2a9099 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

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

633 , IRTS.Java.Mangling

634 , IRTS.Java.Pom

635 , IRTS.Lang

636+ , IRTS.LangOpts

636 , IRTS.Simplified

637 , IRTS.Simplified

637 , IRTS.System

638 , IRTS.System

638

639

libs/prelude/IO.idr+6−2

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

5%access public

6

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

9

11

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

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

11abstract data World = TheWorld

13abstract data World = TheWorld

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

15

17

16-- abstract data WorldRes a = MkWR a World

18-- abstract data WorldRes a = MkWR a World

17

19

20+abstract

21+data IO : Type -> Type where

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

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

19

23

20abstract

24abstract

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

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

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

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

28infixl 9 .

29

30||| Function composition

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

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

32(.) f g x = f (g x)

33

34||| 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) {

12 switch(GETTY(x)) {

13 case CON:

14 ar = CARITY(x);

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

16+ return x;

17+ } else {

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

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

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

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

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

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

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

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

22+ }

19 }

23 }

20 break;

24 break;

21 case FLOAT:

25 case FLOAT:

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

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

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

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

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

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

153 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);

150}

157}

rts/idris_main.c+3

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

15 __idris_argv = argv;

16

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

18+ initNullaries();

19+

18 _idris__123_runMain0_125_(vm, NULL);

20 _idris__123_runMain0_125_(vm, NULL);

19

21

20#ifdef IDRIS_DEBUG

22#ifdef IDRIS_DEBUG

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

29 print_stats(&stats);

31 print_stats(&stats);

30 }

32 }

31

33

34+ freeNullaries();

32 return EXIT_SUCCESS;

35 return EXIT_SUCCESS;

33}

36}

rts/idris_rts.c+33−6

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

828 switch(GETTY(x)) {

829 case CON:

830 ar = CARITY(x);

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

832+ cl = x;

833+ } else {

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

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

832−

835+

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

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

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

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

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

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

836− argptr++;

839+ argptr++;

840+ }

837 }

841 }

838 break;

842 break;

839 case FLOAT:

843 case FLOAT:

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

962 return msg;

966 return msg;

963}

967}

964#endif

968#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+

965int __idris_argc;

992int __idris_argc;

966char **__idris_argv;

993char **__idris_argv;

967

994

rts/idris_rts.h+11

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

214 SETTY(cl, CON); \

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

216

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+

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

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

218

229

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

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

src/IRTS/Bytecode.hs+11−5

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

37

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

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

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

40− | MKCON Reg Int [Reg]

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

41

43

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

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

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

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

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

67 -- same, perhaps exists just for TCO

69 -- same, perhaps exists just for TCO

68 | TAILCALL Name

70 | TAILCALL Name

69

71

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

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

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

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

74+ -- control marshaling.

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

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

73

76

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

77 -- 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

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

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

137 ++ clean r

140 ++ clean r

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

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

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

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

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

140 where getL (Loc x) = L x

144 where getL (Loc x) = L x

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

146+ getAllocLoc _ = Nothing

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

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

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

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

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

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

144 where getL (Loc x) = L x

150 where getL (Loc x) = L x

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

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

146bc reg SNothing r = NULL reg : clean r

152bc reg SNothing r = NULL reg : clean r

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

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

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

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

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

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

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

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

src/IRTS/CodegenC.hs+10−3

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

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

154 mkConst _ = "MKINT(42424242)"

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

156−bcc i (MKCON l tag args)

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

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

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

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

158+bcc i (MKCON l loc tag args)

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

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

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

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

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

161

162

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

165 setArgs i [] = ""

166 setArgs i [] = ""

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

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

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

168 "); " ++ 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"

168

175

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

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

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

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

src/IRTS/CodegenJava.hs+2−2

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

460 mkExp pp newExp

461

462-- Objects

463−mkExp pp (SCon conId _ args) =

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

464 mkIdrisObject conId args >>= ppExp pp

465

466-- 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

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

469

470-- Projections

src/IRTS/CodegenJavaScript.hs+1−1

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

1314 | SLIDE n <- bc = jsSLIDE info n

1315 | REBASE <- bc = jsREBASE info

1316 | 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

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

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

1320 | 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

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

495 return val

496cgExpr (SUpdate x expr) = cgExpr expr

497−cgExpr (SCon tag name args) = do

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

498 argSlots <- mapM var args

499 case sequence argSlots of

500 Nothing -> return Nothing

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

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

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

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

514−cgExpr (SCase inspect alts) = do

514+cgExpr (SCase _ inspect alts) = do

515 val <- var inspect

516 case val of

517 Nothing -> return Nothing

src/IRTS/Compiler.hs+31−16

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

3module IRTS.Compiler(compile, generate) where

4

5import IRTS.Lang

6+import IRTS.LangOpts

6import IRTS.Defunctionalise

7import IRTS.Defunctionalise

7import IRTS.Simplified

8import IRTS.Simplified

8import IRTS.CodegenCommon

9import IRTS.CodegenCommon

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

65 defsIn <- mkDecls tm reachableNames

66 defsIn <- mkDecls tm reachableNames

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

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

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

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

69+ -- Inlined top level LDecl made here

70+ let defsInlined = inlineAll defs

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

72+ defsInlined

73+

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

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

69 let ctxtIn = addAlist tagged emptyContext

75 let ctxtIn = addAlist tagged emptyContext

76+

70 iLOG "Defunctionalising"

77 iLOG "Defunctionalising"

71 let defuns_in = defunctionalise nexttag ctxtIn

78 let defuns_in = defunctionalise nexttag ctxtIn

72 logLvl 5 $ show defuns_in

79 logLvl 5 $ show defuns_in

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

75 logLvl 5 $ show defuns

82 logLvl 5 $ show defuns

76 iLOG "Resolving variables for CG"

83 iLOG "Resolving variables for CG"

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

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

78− let checked = checkDefs defuns (toAlist defuns)

85+ let checked = simplifyDefs defuns (toAlist defuns)

79 outty <- outputTy

86 outty <- outputTy

80 dumpCases <- getDumpCases

87 dumpCases <- getDumpCases

81 dumpDefun <- getDumpDefun

88 dumpDefun <- getDumpDefun

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

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

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

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

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

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

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

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

174

182

175isCon (TyDecl _ _) = True

183isCon (TyDecl _ _) = True

176isCon _ = False

184isCon _ = False

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

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

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

195

203

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

204mkLDecl 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

198 where

206 where

199 (args, sc) = cases_runtime cd

207 (args, sc) = cases_runtime cd

200

208

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+

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

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

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

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

203

217

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

218mkLDecl 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

281 x' <- irTerm vs env x

295 x' <- irTerm vs env x

282 t' <- irTerm vs env t

296 t' <- irTerm vs env t

283 e' <- irTerm vs env e

297 e' <- irTerm vs env e

298+ return (LCase Shared x'

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

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

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

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

286 ])

301 ])

287

302

288 -- data constructor

303 -- data constructor

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

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

290 detag <- fgetState (opt_detaggable . ist_optimisation n)

305 detag <- fgetState (opt_detaggable . ist_optimisation n)

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

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

292

307

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

391

406

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

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

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

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

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

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

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

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

396 Just (Operator ty ar op) -> ar

411 Just (Operator ty ar op) -> ar

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

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

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

510irSC vs (ProjCase tm alts) = do

525irSC vs (ProjCase tm alts) = do

511 tm' <- irTerm vs [] tm

526 tm' <- irTerm vs [] tm

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

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

513− return $ LCase tm' alts'

528+ return $ LCase Shared tm' alts'

514

529

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

530-- 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])

517 | delay == txt "Delay"

532 | delay == txt "Delay"

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

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

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

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

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

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

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

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

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

542--

557--

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

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

544 replacement <- case alt of

559 replacement <- case alt of

545 ConCase cn a ns sc -> do

560 ConCase cn a ns sc -> do

546 detag <- fgetState (opt_detaggable . ist_optimisation cn)

561 detag <- fgetState (opt_detaggable . ist_optimisation cn)

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

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

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

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

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

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

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

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

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

560 where

575 where

561 namesBoundIn :: LAlt -> [Name]

576 namesBoundIn :: LAlt -> [Name]

562 namesBoundIn (LConCase cn i ns sc) = ns

577 namesBoundIn (LConCase cn i ns sc) = ns

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

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

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

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

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

586--

601--

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

588 detag <- fgetState (opt_detaggable . ist_optimisation cn)

603 detag <- fgetState (opt_detaggable . ist_optimisation cn)

589 if detag

604 if detag

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

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

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

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

592

607

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

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

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

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

595 -- see comment above

610 -- see comment above

596 goneWrong <- or <$> mapM isDetaggable alts

611 goneWrong <- or <$> mapM isDetaggable alts

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

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

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

599

614

600 -- everything okay

615 -- 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

602 where

617 where

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

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

604 isDetaggable _ = return False

619 isDetaggable _ = return False

src/IRTS/Defunctionalise.hs+16−10

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

5

6import IRTS.Lang

7import Idris.Core.TT

8+import Idris.Core.CaseTree

8

9

9import Debug.Trace

10import Debug.Trace

10import Data.Maybe

11import Data.Maybe

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

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

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

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

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

19 | DProj DExp Int

20 | DProj DExp Int

20− | DC Int Name [DExp]

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

21− | DCase DExp [DAlt]

22+ | DCase CaseType DExp [DAlt]

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

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

23 | DConst Const

24 | DConst Const

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

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

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

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

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

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

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

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

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

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

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

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

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

105 return $ DProj (DUpdate n t') i

106 return $ DProj (DUpdate n t') i

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

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

107 return $ DProj t' i

108 return $ DProj t' i

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

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

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

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

110− return $ DCase e' alts'

111+ return $ DCase up e' alts'

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

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

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

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

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

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

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

160 | otherwise = preEval xs t

161 | otherwise = preEval xs t

161

162

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

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

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

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

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

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

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

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

166 nec (DConstCase _ e) = needsEval x e

167 nec (DConstCase _ e) = needsEval x e

167 nec (DDefaultCase e) = needsEval x e

168 nec (DDefaultCase e) = needsEval x e

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

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

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

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

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

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

265 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) ++ ":"

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

269 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" ++

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

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

272+ where update = case up of

273+ Shared -> " "

274+ Updatable -> "! "

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

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

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

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

271 show' env (DConst c) = show c

277 show' env (DConst c) = show c

src/IRTS/DumpBC.hs+3−1

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

35 "ASSIGNCONST " ++ serializeReg a ++ " " ++ show b

36 UPDATE a b ->

37 "UPDATE " ++ serializeReg a ++ " " ++ serializeReg b

38− MKCON a b xs ->

38+ MKCON a Nothing b xs ->

39 "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) ++ "]"

40 CASE safe r cases def ->

42 CASE safe r cases def ->

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

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

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

44 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) =

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

32 prefixCallNamespacesExp name (SUpdate var e) =

33 SUpdate var (prefixCallNamespacesExp name e)

34− prefixCallNamespacesExp name (SCase var alts) =

34+ prefixCallNamespacesExp name (SCase up var alts) =

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

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

36 prefixCallNamespacesExp name (SChkCase var alts) =

37 SChkCase var (map (prefixCallNamespacesCase name) alts)

38 prefixCallNamespacesExp _ exp = exp

src/IRTS/Lang.hs+100−23

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

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

2+

1module IRTS.Lang where

3module IRTS.Lang where

2

4

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

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

6+import Control.Applicative hiding (Const)

7+

4−import Idris.Core.TT

8+import Idris.Core.TT

9+import Idris.Core.CaseTree

10+

5−import Data.List

11+import Data.List

6−import Debug.Trace

12+import Debug.Trace

7

13

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

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

9

15

10data LVar = Loc Int | Glob Name

16data LVar = Loc Int | Glob Name

11 deriving (Show, Eq)

17 deriving (Show, Eq)

12

18

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

13data LExp = LV LVar

20data LExp = LV LVar

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

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

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

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

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

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

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

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

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

20 | LProj LExp Int -- projection

27 | LProj LExp Int -- projection

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

21− | LCon Int Name [LExp]

29+ Int Name [LExp]

22− | LCase LExp [LAlt]

30+ | LCase CaseType LExp [LAlt]

23 | LConst Const

31 | LConst Const

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

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

25 | LOp PrimFn [LExp]

33 | LOp PrimFn [LExp]

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

90 | FAny

98 | FAny

91 deriving (Show, Eq)

99 deriving (Show, Eq)

92

100

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

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

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

94− | LConstCase Const LExp

103+ | LConstCase Const e

95− | LDefaultCase LExp

104+ | LDefaultCase e

96− deriving (Show, Eq)

105+ deriving (Show, Eq, Functor)

106+

107+type LAlt = LAlt' LExp

97

108

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

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

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

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

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

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

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

124

135

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

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

126−lambdaLift n (LFun _ _ args e)

137+lambdaLift n (LFun opts _ args e)

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

138 = 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

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

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

130

141

131getNextName :: State LiftState Name

142getNextName :: State LiftState Name

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

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

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

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

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

170 return (LProj t' i)

181 return (LProj t' i)

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

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

172− return (LCon i n args')

183+ return (LCon loc i n args')

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

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

174− e' <- lift env e

185+ e' <- lift env e

175− return (LCase e' alts')

186+ return (LCase up e' alts')

176 where

187 where

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

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

178 return (LConCase i n args e')

189 return (LConCase i n args e')

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

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

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

192lift env LNothing = return $ LNothing

203lift env LNothing = return $ LNothing

193

204

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+

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

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

195

267

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

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

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

204usedIn env (LForce e) = usedIn env e

276usedIn env (LForce e) = usedIn env e

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

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

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

278usedIn 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

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

280usedIn 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

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

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

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

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

212 usedInA env (LDefaultCase e) = usedIn env e

284 usedInA env (LDefaultCase e) = usedIn env e

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

237

309

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

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

239

311

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

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

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

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

314+ where atloc Nothing = ""

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

242

316

243− show' env ind (LCase e alts)

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

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

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

245 where

319 where

320+ update = case up of

321+ Shared -> " "

322+ Updatable -> "! "

246 fmt [] = ""

323 fmt [] = ""

247 fmt [alt]

324 fmt [alt]

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

325 = "\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

2

3import IRTS.Defunctionalise

4import Idris.Core.TT

5+import Idris.Core.CaseTree

5import Idris.Core.Typecheck

6import Idris.Core.Typecheck

6import Data.Maybe

7import Data.Maybe

7import Control.Monad.State

8import Control.Monad.State

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

15 | SApp Bool Name [LVar]

16 | SApp Bool Name [LVar]

16 | SLet LVar SExp SExp

17 | SLet LVar SExp SExp

17 | SUpdate LVar SExp

18 | SUpdate LVar SExp

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

18− | SCon Int Name [LVar]

20+ Int Name [LVar]

19− | SCase LVar [SAlt]

21+ | SCase CaseType LVar [SAlt]

20 | SChkCase LVar [SAlt]

22 | SChkCase LVar [SAlt]

21 | SProj LVar Int

23 | SProj LVar Int

22 | SConst Const

24 | SConst Const

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

48simplify tl (DV (Glob x))

50simplify tl (DV (Glob x))

49 = do ctxt <- ldefs

51 = do ctxt <- ldefs

50 case lookupCtxtExact x ctxt of

52 case lookupCtxtExact x ctxt of

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

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

52 _ -> return $ SV (Glob x)

54 _ -> return $ SV (Glob x)

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

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

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

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

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

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

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

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

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

63 return (SUpdate (Glob n) e')

65 return (SUpdate (Glob n) e')

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

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

65− mkapp (SCon i n) args'

67+ mkapp (SCon loc i n) args'

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

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

67 case v of

69 case v of

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

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

69 (Glob x, Just e) ->

71 (Glob x, Just e) ->

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

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

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

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

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

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

73− case v of

75+ case v of

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

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

75− (Glob x, Just e) ->

77+ (Glob x, Just e) ->

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

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

77simplify tl (DChkCase e alts)

79simplify tl (DChkCase e alts)

78 = do v <- sVar e

80 = do v <- sVar e

79 alts' <- mapM (sAlt tl) alts

81 alts' <- mapM (sAlt tl) alts

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

90sVar (DV (Glob x))

92sVar (DV (Glob x))

91 = do ctxt <- ldefs

93 = do ctxt <- ldefs

92 case lookupCtxtExact x ctxt of

94 case lookupCtxtExact x ctxt of

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

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

94 _ -> return (Glob x, Nothing)

96 _ -> return (Glob x, Nothing)

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

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

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

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

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

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

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

119 return (SDefaultCase e')

121 return (SDefaultCase e')

120

122

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

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

122−checkDefs ctxt [] = return []

124+simplifyDefs ctxt [] = return []

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

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

124− = do xs' <- checkDefs ctxt xs

126+ = do xs' <- simplifyDefs ctxt xs

125 return xs'

127 return xs'

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

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

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

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

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

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

129− xs' <- checkDefs ctxt xs

131+ xs' <- simplifyDefs ctxt xs

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

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

131

133

132lvar v = do i <- get

134lvar v = do i <- get

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

142 Nothing -> case lookupCtxtExact n ctxt of

144 Nothing -> case lookupCtxtExact n ctxt of

143 Just (DConstructor _ i ar) ->

145 Just (DConstructor _ i ar) ->

144 if True -- ar == 0

146 if True -- ar == 0

145− then return (SCon i n [])

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

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

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

147 " has arity " ++ show ar

149 " has arity " ++ show ar

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

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

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

152 case lookupCtxtExact f ctxt of

154 case lookupCtxtExact f ctxt of

153 Just (DConstructor n tag ar) ->

155 Just (DConstructor n tag ar) ->

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

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

155− then return $ SCon tag n args'

157+ then return $ SCon Nothing tag n args'

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

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

157 " has arity " ++ show ar

159 " has arity " ++ show ar

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

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

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

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

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

162 return (t, a')) args

164 return (t, a')) args

163 return $ SForeign l ty f args'

165 return $ SForeign l ty f args'

164− sc env (SCon tag f 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')

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

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

166 case lookupCtxtExact f ctxt of

172 case lookupCtxtExact f ctxt of

167 Just (DConstructor n tag ar) ->

173 Just (DConstructor n tag ar) ->

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

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

169− then return $ SCon tag n args'

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

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

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

171 " has arity " ++ show ar

177 " has arity " ++ show ar

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

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

173 sc env (SProj e i)

179 sc env (SProj e i)

174 = do e' <- scVar env e

180 = do e' <- scVar env e

175 return (SProj e' i)

181 return (SProj e' i)

176− sc env (SCase e alts)

182+ sc env (SCase up e alts)

177 = do e' <- scVar env e

183 = do e' <- scVar env e

178 alts' <- mapM (scalt env) alts

184 alts' <- mapM (scalt env) alts

179− return (SCase e' alts')

185+ return (SCase up e' alts')

180 sc env (SChkCase e alts)

186 sc env (SChkCase e alts)

181 = do e' <- scVar env e

187 = do e' <- scVar env e

182 alts' <- mapM (scalt env) alts

188 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

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

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

230 (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)

232 _ -> return ()

233

234 where errWhen True

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

1026 where

1027 pri (PRef _ n) =

1028 case lookupP n (tt_ctxt i) of

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

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

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

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

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

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

1474 imp _ = True

1475-- allImp [] = False

1476 allImp xs = all imp xs

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

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

1478 constructor _ = False

1479

1480 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

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

714 | PHidden PTerm -- ^ Irrelevant or hidden pattern

715 | PType -- ^ 'Type' type

716+ | PUniverse Universe -- ^ Some universe

716 | PGoal FC PTerm Name PTerm

717 | PGoal FC PTerm Name PTerm

717 | PConstant Const -- ^ Builtin types

718 | PConstant Const -- ^ Builtin types

718 | Placeholder

719 | Placeholder

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

1380 prettyAs =

1381 prettyAs =

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

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

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

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

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

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

1384 -- XXX: add pretty for tactics

1386 -- XXX: add pretty for tactics

1385 prettySe p bnd (PProof ts) =

1387 prettySe p bnd (PProof ts) =

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

1644 size (PDisamb _ tm) = size tm

1646 size (PDisamb _ tm) = size tm

1645 size (PNoImplicits tm) = size tm

1647 size (PNoImplicits tm) = size tm

1646 size PType = 1

1648 size PType = 1

1649+ size (PUniverse _) = 1

1647 size (PConstant const) = 1 + size const

1650 size (PConstant const) = 1 + size const

1648 size Placeholder = 1

1651 size Placeholder = 1

1649 size (PDoBlock dos) = 1 + size dos

1652 size (PDoBlock dos) = 1 + size dos

src/Idris/Apropos.hs+1−1

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

61instance Apropos (TT Name) where

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

63 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

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

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

67 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

78 CaseN x1 -> do putWord8 4; put x1

79 ElimN x1 -> do putWord8 5; put x1

80 InstanceCtorN x1 -> do putWord8 6; put x1

81+ WithN x1 x2 -> do putWord8 7

82+ put x1

83+ put x2

81 get

84 get

82 = do i <- getWord8

85 = do i <- getWord8

83 case i of

86 case i of

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

99 return (ElimN x1)

102 return (ElimN x1)

100 6 -> do x1 <- get

103 6 -> do x1 <- get

101 return (InstanceCtorN x1)

104 return (InstanceCtorN x1)

105+ 7 -> do x1 <- get

106+ x2 <- get

107+ return (WithN x1 x2)

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

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

103

109

104

110

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

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

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

276

282

277

283

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+

278instance Binary NameType where

294instance Binary NameType where

279 put x

295 put x

280 = case x of

296 = case x of

281 Bound -> putWord8 0

297 Bound -> putWord8 0

282 Ref -> putWord8 1

298 Ref -> putWord8 1

283− DCon x1 x2 -> do putWord8 2

299+ DCon x1 x2 x3 -> do putWord8 2

284− put (x1 * 65536 + x2)

300+ put (x1 * 65536 + x2)

301+ put x3

285 TCon x1 x2 -> do putWord8 3

302 TCon x1 x2 -> do putWord8 3

286 put (x1 * 65536 + x2)

303 put (x1 * 65536 + x2)

287 get

304 get

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

290 0 -> return Bound

307 0 -> return Bound

291 1 -> return Ref

308 1 -> return Ref

292 2 -> do x1x2 <- get

309 2 -> do x1x2 <- get

310+ x3 <- get

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

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

294 3 -> do x1x2 <- get

312 3 -> do x1x2 <- get

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

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

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

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

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

325 TType x1 -> do putWord8 7

343 TType x1 -> do putWord8 7

326 put x1

344 put x1

327 Impossible -> putWord8 8

345 Impossible -> putWord8 8

346+ UType x1 -> do putWord8 10

347+ put x1

328 get

348 get

329 = do i <- getWord8

349 = do i <- getWord8

330 case i of

350 case i of

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

352 8 -> return Impossible

372 8 -> return Impossible

353 9 -> do x1 <- get

373 9 -> do x1 <- get

354 return (V x1)

374 return (V x1)

375+ 10 -> do x1 <- get

376+ return (UType x1)

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

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

356

378

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

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

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

2

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

4− Phase(..), CaseTree,

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

5 simpleCase, small, namesUsed, findCalls, findUsedArgs,

6 substSC, substAlt, mkForce) where

7

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

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

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

32--

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

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

35 | STerm !t

36 | UnmatchedCase String -- ^ error message

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

41deriving instance NFData SC'

42!-}

43

44+data CaseType = Updatable | Shared

45+ deriving (Eq, Ord, Show)

46+

44type SC = SC' Term

47type SC = SC' Term

45

48

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

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

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

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

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

60 show sc = show' 1 sc

63 show sc = show' 1 sc

61 where

64 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 ++

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

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

67+ where u = case up of

68+ Updatable -> "! "

69+ Shared -> " "

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

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

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

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

66 show' i (STerm tm) = show tm

72 show' i (STerm tm) = show tm

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

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

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

89

95

90instance TermSize SC where

96instance TermSize SC where

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

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

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

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

93 termsize n (STerm t) = termsize n t

99 termsize n (STerm t) = termsize n t

94 termsize n _ = 1

100 termsize n _ = 1

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

111

117

112namesUsed :: SC -> [Name]

118namesUsed :: SC -> [Name]

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

119namesUsed 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]

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

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

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

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

117 nu' ps _ = []

123 nu' ps _ = []

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

136

142

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

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

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

144findCalls 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)

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

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

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

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

142 nu' ps _ = []

148 nu' ps _ = []

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

189findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

195findUsedArgs sc topargs = nub (findAllUsedArgs sc topargs)

190

196

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

197findAllUsedArgs 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

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

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

194 nu' (STerm t) = directUse t

200 nu' (STerm t) = directUse t

195 nu' _ = []

201 nu' _ = []

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

204isUsed :: SC -> Name -> Bool

210isUsed :: SC -> Name -> Bool

205isUsed sc n = used sc where

211isUsed sc n = used sc where

206

212

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

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

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

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

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

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

210 used _ = False

216 used _ = False

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

276

282

277 acc [] n = Error (Inaccessible n)

283 acc [] n = Error (Inaccessible n)

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

284 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

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

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

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

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

282

288

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

285-- going on).

291-- going on).

286

292

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

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

288−checkSameTypes tys (Case n alts)

294+checkSameTypes tys (Case _ n alts)

289 = case lookup n tys of

295 = case lookup n tys of

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

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

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

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

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

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

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

325isConstType _ _ = False

331isConstType _ _ = False

326

332

327−data Pat = PCon Name Int [Pat]

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

328 | PConst Const

334 | PConst Const

329 | PV Name Type

335 | PV Name Type

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

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

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

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

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

345toPat reflect tc = map $ toPat' []

351toPat reflect tc = map $ toPat' []

346 where

352 where

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

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

348 | n == txt "Delay"

354 | n == txt "Delay"

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

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

350

356

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

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

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

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

353

359

354 -- n + 1

360 -- n + 1

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

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

356 | pabi == txt "prim__addBigInt"

362 | pabi == txt "prim__addBigInt"

357 = PSuc $ toPat' [] p

363 = PSuc $ toPat' [] p

358

364

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−

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

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

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

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

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

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

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

405isVarPat (PTyPat : ps , _) = True

395isVarPat (PTyPat : ps , _) = True

406isVarPat _ = False

396isVarPat _ = False

407

397

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

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

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

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

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

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

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

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

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

449 noClash [] = True

439 noClash [] = True

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

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

451

441

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

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

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

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

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

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

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

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

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

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

457 clashPat _ _ = False

447 clashPat _ _ = False

458

448

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

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

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

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

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

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

462

452

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

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

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

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

465 numNames xs (PConst c : ps)

455 numNames xs (PConst c : ps)

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

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

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

497 | CConst Const -- constant, not implemented yet

487 | CConst Const -- constant, not implemented yet

498 deriving (Show, Eq)

488 deriving (Show, Eq)

499

489

490+data Group = ConGroup Bool -- Uniqueness flag

500−data Group = ConGroup ConType -- Constructor

491+ ConType -- Constructor

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

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

502 deriving Show

493 deriving Show

503

494

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

507

498

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

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

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

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

510− return $ Case v (sort g)

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

511 where

502 where

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

504+ getShared _ = Shared

505+

512 altGroups [] = return [DefaultCase err]

506 altGroups [] = return [DefaultCase err]

513

507

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

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

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

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

516

510

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

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

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

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

519

513

520− altGroups (ConGroup CSuc args : cs)

514+ altGroups (ConGroup _ CSuc args : cs)

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

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

522

516

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

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

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

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

525

519

520+ altGroup n i args

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

521+ = do inacc <- inaccessibleArgs n

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

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

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

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

529− return $ ConCase n i newVars matchCs

524+ return $ ConCase n i newVars matchCs

530

525

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

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

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

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

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

601 do acc' <- addGroup p ps res acc

596 do acc' <- addGroup p ps res acc

602 gc acc' cs

597 gc acc' cs

603 addGroup p ps res acc = case p of

598 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

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

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

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

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

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

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

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

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

609

604

610− addg c conargs res []

605+ addg uniq c conargs res []

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

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

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

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

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

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

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

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

615

610

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

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

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

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

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

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

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

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

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

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

621

616

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

637depatt ns tm = dp [] tm

632depatt ns tm = dp [] tm

638 where

633 where

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

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

641 dp ms sc = sc

636 dp ms sc = sc

642

637

643 dpa ms x (ConCase n i args sc)

638 dpa ms x (ConCase n i args sc)

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

667-- FIXME: Do this for SucCase too

662-- FIXME: Do this for SucCase too

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

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

669 -> SC -> SC

664 -> SC -> SC

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

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

671 [] -> ImpossibleCase

666 [] -> ImpossibleCase

672

667

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

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

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

689 as@[ConCase cn i args sc]

684 as@[ConCase cn i args sc]

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

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

691 if any (isUsed sc') args

686 if any (isUsed sc') args

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

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

693 else sc'

688 else sc'

694

689

695 [SucCase cn sc]

690 [SucCase cn sc]

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

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

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

703 -- it gets caught first.

698 -- it gets caught first.

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

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

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

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

706

701

707− as -> Case n as

702+ as -> Case up n as

708 where

703 where

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

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

710

705

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

719 erased _ = False

714 erased _ = False

720

715

721 projRep :: Name -> Name -> Int -> SC -> SC

716 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

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

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

724− projRep arg n i (Case x alts)

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

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

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

726 projRep arg n i (ProjCase t alts)

721 projRep arg n i (ProjCase t alts)

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

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

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

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

749stripLambdas x = x

744stripLambdas x = x

750

745

751substSC :: Name -> Name -> SC -> SC

746substSC :: Name -> Name -> SC -> SC

752−substSC n repl (Case n' alts)

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

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

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

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

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

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

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

756substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

751substSC n repl (UnmatchedCase errmsg) = UnmatchedCase errmsg

757substSC n repl ImpossibleCase = ImpossibleCase

752substSC n repl ImpossibleCase = ImpossibleCase

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

771mkForce :: Name -> Name -> SC -> SC

766mkForce :: Name -> Name -> SC -> SC

772mkForce = mkForceSC

767mkForce = mkForceSC

773 where

768 where

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

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

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

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

776

771

777− mkForceSC n arg (Case x alts)

772+ mkForceSC n arg (Case up x alts)

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

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

779

774

780 mkForceSC n arg (ProjCase t alts)

775 mkForceSC n arg (ProjCase t alts)

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

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

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

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

14

15instance NFData SpecialName where

16 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` ()

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

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

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

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

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

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

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

85instance NFData NameType where

86instance NFData NameType where

86 rnf Bound = ()

87 rnf Bound = ()

87 rnf Ref = ()

88 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` ()

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

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

90

91

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

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

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

98 rnf Erased = ()

99 rnf Erased = ()

99 rnf Impossible = ()

100 rnf Impossible = ()

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

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

102+ rnf (UType _) = ()

101

103

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

104instance (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` ()

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

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

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

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

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

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

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

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

404unifyProblems :: Elab' aux ()

405unifyProblems = processTactic' UnifyProblems

406

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

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

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

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

409− processTactic' (Defer n')

409+ processTactic' (Defer ds n')

410

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

412deferType 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,

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

12 mapDefCtxt,

13 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

15

16

16import Debug.Trace

17import Debug.Trace

17import Control.Applicative hiding (Const)

18import Control.Applicative hiding (Const)

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

47 | VBLet Int Name Value Value Value

48 | VBLet Int Name Value Value Value

48 | VApp Value Value

49 | VApp Value Value

49 | VType UExp

50 | VType UExp

51+ | VUType Universe

50 | VErased

52 | VErased

51 | VImpossible

53 | VImpossible

52 | VConstant Const

54 | VConstant Const

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

290 t' <- ev ntimes stk top env t

292 t' <- ev ntimes stk top env t

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

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

292 return (doProj t' (getValArgs t'))

294 return (doProj t' (getValArgs t'))

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

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

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

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

295 doProj t' _ = VProj t' i

297 doProj t' _ = VProj t' i

296

298

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

298 ev ntimes stk top env Erased = return VErased

300 ev ntimes stk top env Erased = return VErased

299 ev ntimes stk top env Impossible = return VImpossible

301 ev ntimes stk top env Impossible = return VImpossible

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

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

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

301

304

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

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

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

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

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

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

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

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

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

395 doCase ntimes stk top env amap t' alts

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

397 = case lookup n amap of

400 = case lookup n amap of

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

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

399 _ -> return Nothing

402 _ -> return Nothing

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

409 _ -> return Nothing

412 _ -> return Nothing

410

413

411 conHeaded tm@(App _ _)

414 conHeaded tm@(App _ _)

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

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

413 conHeaded t = False

416 conHeaded t = False

414

417

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

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

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

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

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

421 [(Name, Value)] ->

424 [(Name, Value)] ->

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

425 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

522 quote i VErased = return $ Erased

526 quote i VErased = return $ Erased

523 quote i VImpossible = return $ Impossible

527 quote i VImpossible = return $ Impossible

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

528 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

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

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

535wknV i t = return t

539wknV i t = return t

536

540

541+isUniverse :: Term -> Bool

542+isUniverse (TType _) = True

543+isUniverse (UType _) = True

544+isUniverse _ = False

545+

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

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

538

547

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

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

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

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

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

574 put (v, ULE x y : cs)

583 put (v, ULE x y : cs)

575 return True

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

576 ceq ps Erased _ = return True

588 ceq ps Erased _ = return True

577 ceq ps _ Erased = return True

589 ceq ps _ Erased = return True

578 ceq ps x y = return False

590 ceq ps x y = return False

579

591

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'

581 where

593 where

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

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

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

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

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

780 uctxt { definitions = ctxt' }

792 uctxt { definitions = ctxt' }

781

793

782addDatatype :: Datatype Name -> Context -> Context

794addDatatype :: Datatype Name -> Context -> Context

783−addDatatype (Data n tag ty cons) uctxt

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

784 = let ctxt = definitions uctxt

796 = let ctxt = definitions uctxt

785 ty' = normalise uctxt [] ty

797 ty' = normalise uctxt [] ty

786 ctxt' = addCons 0 cons (addDef n

798 ctxt' = addCons 0 cons (addDef n

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

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

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

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

804 = let ty' = normalise uctxt [] ty in

793 addCons (tag+1) cons (addDef n

805 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)

795

807

796-- FIXME: Too many arguments! Refactor all these Bools.

808-- FIXME: Too many arguments! Refactor all these Bools.

797addCasedef :: Name -> ErasureInfo -> CaseInfo ->

809addCasedef :: Name -> ErasureInfo -> CaseInfo ->

@@ -916,7 +928,7 @@ isDConName :: Name -> Context -> Bool

916isDConName n ctxt

928isDConName n ctxt

917 = or $ do def <- lookupCtxt n (definitions ctxt)

929 = or $ do def <- lookupCtxt n (definitions ctxt)

918 case tfst def of

930 case tfst def of

919− (TyDecl (DCon _ _) _) -> return True

931+ (TyDecl (DCon _ _ _) _) -> return True

920 _ -> return False

932 _ -> return False

921

933

922isFnName :: Name -> Context -> Bool

934isFnName :: Name -> Context -> Bool

src/Idris/Core/Execute.hs+4−4

@@ -146,7 +146,7 @@ execute tm = do est <- initState

146 Right tm' -> return tm'

147

148ioWrap :: 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]

150

151ioUnit :: ExecVal

152ioUnit = ioWrap (EP Ref unitCon EErased)

@@ -171,7 +171,7 @@ doExec env ctxt p@(P Bound n ty) =

171 case lookup n env of

172 Nothing -> execFail . Msg $ "not found"

173 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)

175doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

176doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

177 | otherwise = execFail . Msg $ "env too small"

@@ -349,7 +349,7 @@ execApp env ctxt f@(EP _ fp _) args@(ty:fn:xs) | fp == mkfprim

349 Just r -> return (mkEApp r xs')

350 Nothing -> return (mkEApp f args)

351

352−execApp env ctxt c@(EP (DCon _ arity) n _) args =

352+execApp env ctxt c@(EP (DCon _ arity _) n _) args =

353 do let args' = take arity args

354 let restArgs = drop arity args

355 execApp env ctxt (mkEApp c args') restArgs

@@ -443,7 +443,7 @@ execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVa

443execCase' env ctxt amap (UnmatchedCase _) = return Nothing

444execCase' env ctxt amap (STerm tm) =

445 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 =

447 case chooseAlt tm alts of

448 Just (newCase, newBindings) ->

449 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

75 | PatVar Name

76 | PatBind Name

77 | Focus Name

78− | Defer Name

78+ | Defer [Name] Name

79 | DeferType Name Raw [Name]

80 | Instance Name

81 | SetInjective Name

@@ -387,12 +387,13 @@ setinj n ctxt env (Bind x b sc)

387 ps { injective = n : is })

388 return (Bind x b sc)

389

390−defer :: Name -> RunTactic

390+defer :: [Name] -> Name -> RunTactic

391−defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

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

392− do action (\ps -> let hs = holes ps in

393+ action (\ps -> let hs = holes ps in

393 ps { holes = hs \\ [x] })

394 ps { holes = hs \\ [x] })

394− return (Bind n (GHole (length env) (mkTy (reverse env) t))

395+ return (Bind n (GHole (length env') (mkTy (reverse env') t))

395− (mkApp (P Ref n ty) (map getP (reverse env))))

396+ (mkApp (P Ref n ty) (map getP (reverse env'))))

396 where

397 where

397 mkTy [] t = t

398 mkTy [] t = t

398 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)

399 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)

952 mktac (CheckIn r) = check_in r

953 mktac (CheckIn r) = check_in r

953 mktac (EvalIn r) = eval_in r

954 mktac (EvalIn r) = eval_in r

954 mktac (Focus n) = focus n

955 mktac (Focus n) = focus n

955− mktac (Defer n) = defer n

956+ mktac (Defer ns n) = defer ns n

956 mktac (DeferType n t a) = deferType n t a

957 mktac (DeferType n t a) = deferType n t a

957 mktac (Instance n) = instanceArg n

958 mktac (Instance n) = instanceArg n

958 mktac (SetInjective n) = setinj n

959 mktac (SetInjective n) = setinj n

src/Idris/Core/TT.hs+32−15

@@ -139,6 +139,8 @@ data Err' t

139 | CantResolveAlts [Name]

140 | IncompleteTerm t

141 | UniverseError

142+ | UniqueError Name

143+ | UniqueKindError Name

142 | ProgramLineComment

144 | ProgramLineComment

143 | Inaccessible Name

145 | Inaccessible Name

144 | NonCollapsiblePostulate Name

146 | NonCollapsiblePostulate Name

@@ -305,6 +307,7 @@ deriving instance NFData Name

305!-}

307!-}

306

308

307data SpecialName = WhereN Int Name Name

309data SpecialName = WhereN Int Name Name

310+ | WithN Int Name

308 | InstanceN Name [T.Text]

311 | InstanceN Name [T.Text]

309 | ParentN Name T.Text

312 | ParentN Name T.Text

310 | MethodN Name

313 | MethodN Name

@@ -349,6 +352,7 @@ instance Show Name where

349

352

350instance Show SpecialName where

353instance Show SpecialName where

351 show (WhereN i p c) = show p ++ ", " ++ show c

354 show (WhereN i p c) = show p ++ ", " ++ show c

355+ show (WithN i n) = "with block in " ++ show n

352 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

356 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl

353 show (MethodN m) = "method " ++ show m

357 show (MethodN m) = "method " ++ show m

354 show (ParentN p c) = show p ++ "#" ++ T.unpack c

358 show (ParentN p c) = show p ++ "#" ++ T.unpack c

@@ -364,6 +368,7 @@ showCG (MN _ u) | u == txt "underscore" = "_"

364showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

368showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

365showCG (SN s) = showCG' s

369showCG (SN s) = showCG' s

366 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

370 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

371+ showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i

367 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

372 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

368 showCG' (MethodN m) = '!':showCG m

373 showCG' (MethodN m) = '!':showCG m

369 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

374 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

@@ -594,10 +599,18 @@ constDocs (B32V v) = "A vector of thirty-two-bit values"

594constDocs (B64V v) = "A vector of sixty-four-bit values"

599constDocs (B64V v) = "A vector of sixty-four-bit values"

595constDocs prim = "Undocumented"

600constDocs prim = "Undocumented"

596

601

602+data Universe = UniqueType | AllTypes

603+ deriving (Eq, Ord)

604+

605+instance Show Universe where

606+ show UniqueType = "UniqueType"

607+ show AllTypes = "Type*"

608+

597data Raw = Var Name

609data Raw = Var Name

598 | RBind Name (Binder Raw) Raw

610 | RBind Name (Binder Raw) Raw

599 | RApp Raw Raw

611 | RApp Raw Raw

600 | RType

612 | RType

613+ | RUType Universe

601 | RForce Raw

614 | RForce Raw

602 | RConstant Const

615 | RConstant Const

603 deriving (Show, Eq)

616 deriving (Show, Eq)

@@ -607,6 +620,7 @@ instance Sized Raw where

607 size (RBind name bind right) = 1 + size bind + size right

620 size (RBind name bind right) = 1 + size bind + size right

608 size (RApp left right) = 1 + size left + size right

621 size (RApp left right) = 1 + size left + size right

609 size RType = 1

622 size RType = 1

623+ size (RUType _) = 1

610 size (RForce raw) = 1 + size raw

624 size (RForce raw) = 1 + size raw

611 size (RConstant const) = size const

625 size (RConstant const) = size const

612

626

@@ -717,7 +731,7 @@ type UCs = (Int, [UConstraint])

717

731

718data NameType = Bound

732data NameType = Bound

719 | Ref

733 | Ref

720− | DCon {nt_tag :: Int, nt_arity :: Int} -- ^ Data constructor

734+ | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor

721 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

735 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor

722 deriving (Show, Ord)

736 deriving (Show, Ord)

723{-!

737{-!

@@ -734,7 +748,7 @@ instance Pretty NameType OutputAnnotation where

734instance Eq NameType where

748instance Eq NameType where

735 Bound == Bound = True

749 Bound == Bound = True

736 Ref == Ref = True

750 Ref == Ref = True

737− DCon _ a == DCon _ b = (a == b) -- ignore tag

751+ DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag

738 TCon _ a == TCon _ b = (a == b) -- ignore tag

752 TCon _ a == TCon _ b = (a == b) -- ignore tag

739 _ == _ = False

753 _ == _ = False

740

754

@@ -753,6 +767,7 @@ data TT n = P NameType n (TT n) -- ^ named references with type

753 | Erased -- ^ an erased term

767 | Erased -- ^ an erased term

754 | Impossible -- ^ special case for totality checking

768 | Impossible -- ^ special case for totality checking

755 | TType UExp -- ^ the type of types at some level

769 | TType UExp -- ^ the type of types at some level

770+ | UType Universe -- ^ Uniqueness type universe (disjoint from TType)

756 deriving (Ord, Functor)

771 deriving (Ord, Functor)

757{-!

772{-!

758deriving instance Binary TT

773deriving instance Binary TT

@@ -802,6 +817,7 @@ type EnvTT n = [(n, Binder (TT n))]

802data Datatype n = Data { d_typename :: n,

817data Datatype n = Data { d_typename :: n,

803 d_typetag :: Int,

818 d_typetag :: Int,

804 d_type :: (TT n),

819 d_type :: (TT n),

820+ d_unique :: Bool,

805 d_cons :: [(n, TT n)] }

821 d_cons :: [(n, TT n)] }

806 deriving (Show, Functor, Eq)

822 deriving (Show, Functor, Eq)

807

823

@@ -823,7 +839,7 @@ instance Eq n => Eq (TT n) where

823-- constant, the type Type, pi-binding, or an application of an injective

839-- constant, the type Type, pi-binding, or an application of an injective

824-- term.

840-- term.

825isInjective :: TT n -> Bool

841isInjective :: TT n -> Bool

826−isInjective (P (DCon _ _) _ _) = True

842+isInjective (P (DCon _ _ _) _ _) = True

827isInjective (P (TCon _ _) _ _) = True

843isInjective (P (TCon _ _) _ _) = True

828isInjective (Constant _) = True

844isInjective (Constant _) = True

829isInjective (TType x) = True

845isInjective (TType x) = True

@@ -1054,18 +1070,18 @@ unList tm = case unApply tm of

1054-- with the corresponding name. It is an error if there are free de

1070-- with the corresponding name. It is an error if there are free de

1055-- Bruijn indices.

1071-- Bruijn indices.

1056forget :: TT Name -> Raw

1072forget :: TT Name -> Raw

1057−forget tm = fe [] tm

1073+forget tm = forgetEnv [] tm

1058− where

1074+

1059− fe env (P _ n _) = Var n

1075+forgetEnv env (P _ n _) = Var n

1060− fe env (V i) = Var (env !! i)

1076+forgetEnv env (V i) = Var (env !! i)

1061− fe env (Bind n b sc) = let n' = uniqueName n env in

1077+forgetEnv env (Bind n b sc) = let n' = uniqueName n env in

1062− RBind n' (fmap (fe env) b)

1078+ RBind n' (fmap (forgetEnv env) b)

1063− (fe (n':env) sc)

1079+ (forgetEnv (n':env) sc)

1064− fe env (App f a) = RApp (fe env f) (fe env a)

1080+forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)

1065− fe env (Constant c)

1081+forgetEnv env (Constant c) = RConstant c

1066− = RConstant c

1067− fe env (TType i) = RType

1082+forgetEnv env (TType i) = RType

1083+forgetEnv env (UType u) = RUType u

1068− fe env Erased = RConstant Forgot

1084+forgetEnv env Erased = RConstant Forgot

1069

1085

1070-- | Introduce a 'Bind' into the given term for each element of the

1086-- | Introduce a 'Bind' into the given term for each element of the

1071-- given list of (name, binder) pairs.

1087-- given list of (name, binder) pairs.

@@ -1246,6 +1262,7 @@ showEnv' env t dbg = se 10 env t where

1246 se p env Erased = "[__]"

1262 se p env Erased = "[__]"

1247 se p env Impossible = "[impossible]"

1263 se p env Impossible = "[impossible]"

1248 se p env (TType i) = "Type " ++ show i

1264 se p env (TType i) = "Type " ++ show i

1265+ se p env (UType u) = show u

1249

1266

1250 sb env n (Lam t) = showb env "\\ " " => " n t

1267 sb env n (Lam t) = showb env "\\ " " => " n t

1251 sb env n (Hole t) = showb env "? " ". " n t

1268 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))

47

48isType :: Context -> Env -> Term -> TC ()

49isType ctxt env tm = isType' (normalise ctxt env tm)

50− where isType' (TType _) = return ()

50+ where isType' tm | isUniverse tm = return ()

51− isType' tm = fail (showEnv env tm ++ " is not a TType")

51+ | otherwise = fail (showEnv env tm ++ " is not a Type")

52

53recheck :: Context -> Env -> Raw -> Term -> TC (Term, Type, UCs)

54recheck ctxt env tm orig

@@ -57,10 +57,12 @@ recheck ctxt env tm orig

57 Error (IncompleteTerm _) -> Error $ IncompleteTerm orig

58 Error e -> Error e

59 OK ((tm, ty), constraints) ->

60+ do checkUnique ctxt env tm

60− return (tm, ty, constraints)

61+ return (tm, ty, constraints)

61

62

62check :: Context -> Env -> Raw -> TC (Term, Type)

63check :: Context -> Env -> Raw -> TC (Term, Type)

64+check ctxt env tm

63−check ctxt env tm = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

65+ = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

64

66

65check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

67check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

66check' holes ctxt env top = chk env top where

68check' holes ctxt env top = chk env top where

@@ -79,29 +81,24 @@ check' holes ctxt env top = chk env top where

79 _ -> normalise ctxt env fty

81 _ -> normalise ctxt env fty

80 case fty' of

82 case fty' of

81 Bind x (Pi s) t ->

83 Bind x (Pi s) t ->

82−-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

83−-- " from " ++ show fv ++ " : " ++ show fty) $

84 do convertsC ctxt env aty s

85− -- let apty = normalise initContext env

86− -- (Bind x (Let aty av) t)

87 let apty = simplify initContext env

85 let apty = simplify initContext env

88 (Bind x (Let aty av) t)

86 (Bind x (Let aty av) t)

89 return (App fv av, apty)

87 return (App fv av, apty)

90− t -> lift $ tfail $ NonFunctionType fv fty -- "Can't apply a non-function type"

88+ t -> lift $ tfail $ NonFunctionType fv fty

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

99 chk env RType

89 chk env RType

100 | holes = return (TType (UVal 0), TType (UVal 0))

90 | holes = return (TType (UVal 0), TType (UVal 0))

101 | otherwise = do (v, cs) <- get

91 | otherwise = do (v, cs) <- get

102 let c = ULT (UVar v) (UVar (v+1))

92 let c = ULT (UVar v) (UVar (v+1))

103 put (v+2, (c:cs))

93 put (v+2, (c:cs))

104 return (TType (UVar v), TType (UVar (v+1)))

94 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))

105 chk env (RConstant Forgot) = return (Erased, Erased)

102 chk env (RConstant Forgot) = return (Erased, Erased)

106 chk env (RConstant c) = return (Constant c, constType c)

103 chk env (RConstant c) = return (Constant c, constType c)

107 where constType (I _) = Constant (AType (ATInt ITNative))

104 where constType (I _) = Constant (AType (ATInt ITNative))

@@ -125,11 +122,17 @@ check' holes ctxt env top = chk env top where

125 = do (sv, st) <- chk env s

122 = do (sv, st) <- chk env s

126 (tv, tt) <- chk ((n, Pi sv) : env) t

123 (tv, tt) <- chk ((n, Pi sv) : env) t

127 (v, cs) <- get

124 (v, cs) <- get

128− let TType su = normalise ctxt env st

125+ case (normalise ctxt env st, normalise ctxt env tt) of

129− let TType tu = normalise ctxt env tt

126+ (TType su, TType tu) -> do

130− when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

127+ 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))

128+ return (Bind n (Pi (uniqueBinders (map fst env) sv))

132 (pToV n tv), TType (UVar v))

129 (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)

133 chk env (RBind n b sc)

136 chk env (RBind n b sc)

134 = do b' <- checkBinder b

137 = do b' <- checkBinder b

135 (scv, sct) <- chk ((n, b'):env) sc

138 (scv, sct) <- chk ((n, b'):env) sc

@@ -140,12 +143,6 @@ check' holes ctxt env top = chk env top where

140 let tt' = normalise ctxt env tt

143 let tt' = normalise ctxt env tt

141 lift $ isType ctxt env tt'

144 lift $ isType ctxt env tt'

142 return (Lam tv)

145 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)

149 checkBinder (Let t v)

146 checkBinder (Let t v)

150 = do (tv, tt) <- chk env t

147 = do (tv, tt) <- chk env t

151 (vv, vt) <- chk env v

148 (vv, vt) <- chk env v

@@ -219,3 +216,40 @@ check' holes ctxt env top = chk env top where

219 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

216 = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)

220 discharge n (PVTy t) scv sct

217 discharge n (PVTy t) scv sct

221 = return (Bind n (PVTy t) scv, sct)

218 = 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 =

85 -- answer, merely a valid one, so perhaps we're okay.

86 -- In other words: it may vanish without warning some day :)

87 un names x tm@(App (P _ f (Bind fn (Pi t) sc)) a)

88− | (P (DCon _ _) _ _, _) <- unApply x,

88+ | (P (DCon _ _ _) _ _, _) <- unApply x,

89 holeIn env f || f `elem` holes

90 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

91 checkCycle names (f, Bind n' (Lam t) x)

92 un names tm@(App (P _ f (Bind fn (Pi t) sc)) a) x

93− | (P (DCon _ _) _ _, _) <- unApply x,

93+ | (P (DCon _ _ _) _ _, _) <- unApply x,

94 holeIn env f || f `elem` holes

95 = let n' = uniqueName fn (map fst env) in

96 checkCycle names (f, Bind n' (Lam t) x)

@@ -265,11 +265,11 @@ unify ctxt env topx topy inj holes usersupp from =

265-- Error e@(CantUnify False _ _ _ _ _) -> tfail e

266 Error e -> tfail e

267 where

268− headDiff (P (DCon _ _) x _) (P (DCon _ _) y _) = x /= y

268+ headDiff (P (DCon _ _ _) x _) (P (DCon _ _ _) y _) = x /= y

269 headDiff (P (TCon _ _) x _) (P (TCon _ _) y _) = x /= y

270 headDiff _ _ = False

271

272− injective (P (DCon _ _) _ _) = True

272+ injective (P (DCon _ _ _) _ _) = True

273 injective (P (TCon _ _) _ _) = True

274-- injective (App f (P _ _ _)) = injective f

275-- injective (App f (Constant _)) = injective f

@@ -315,13 +315,13 @@ unify ctxt env topx topy inj holes usersupp from =

315 StateT UInfo

316 TC [(Name, TT Name)]

317 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 _)

319 | x /= y = unifyFail topx topy

320 un' fn names topx@(P (TCon _ _) x _) topy@(P (TCon _ _) y _)

321 | 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 _)

323 = 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 _)

325 = unifyFail topx topy

326 un' fn names topx@(Constant _) topy@(P (TCon _ _) y _)

327 = unifyFail topx topy

@@ -427,6 +427,7 @@ unify ctxt env topx topy inj holes usersupp from =

427 sameBinder _ _ = False

428 un' fn bnames x y

429 | OK True <- convEq' ctxt holes x y = do sc 1; return []

430+ | isUniverse x && isUniverse y = do sc 1; return []

430 | otherwise = do UI s f <- get

431 | otherwise = do UI s f <- get

431 let r = recoverable (normalise ctxt env x)

432 let r = recoverable (normalise ctxt env x)

432 (normalise ctxt env y)

433 (normalise ctxt env y)

@@ -460,13 +461,13 @@ unify ctxt env topx topy inj holes usersupp from =

460 | otherwise = unifyTmpFail appx appy

461 | otherwise = unifyTmpFail appx appy

461 where hnormalise [] _ _ t = t

462 where hnormalise [] _ _ t = t

462 hnormalise ns ctxt env t = normalise ctxt env t

463 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 _)

464 | x /= y = unifyFail appx appy

465 | x /= y = unifyFail appx appy

465 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

466 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

466 | x /= y = unifyFail appx appy

467 | x /= y = unifyFail appx appy

467− checkHeads (P (DCon _ _) x _) (P (TCon _ _) y _)

468+ checkHeads (P (DCon _ _ _) x _) (P (TCon _ _) y _)

468 = unifyFail appx appy

469 = unifyFail appx appy

469− checkHeads (P (TCon _ _) x _) (P (DCon _ _) y _)

470+ checkHeads (P (TCon _ _) x _) (P (DCon _ _ _) y _)

470 = unifyFail appx appy

471 = unifyFail appx appy

471 checkHeads _ _ = return []

472 checkHeads _ _ = return []

472

473

@@ -492,7 +493,7 @@ unify ctxt env topx topy inj holes usersupp from =

492 all (\x -> pat x || metavar x) (f : args)

493 all (\x -> pat x || metavar x) (f : args)

493 && nub args == args

494 && nub args == args

494

495

495− rigid (P (DCon _ _) _ _) = True

496+ rigid (P (DCon _ _ _) _ _) = True

496 rigid (P (TCon _ _) _ _) = True

497 rigid (P (TCon _ _) _ _) = True

497 rigid t@(P Ref _ _) = inenv t || globmetavar t

498 rigid t@(P Ref _ _) = inenv t || globmetavar t

498 rigid (Constant _) = True

499 rigid (Constant _) = True

@@ -632,15 +633,15 @@ recoverable t@(App _ _) _

632 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

633 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

633recoverable _ t@(App _ _)

634recoverable _ t@(App _ _)

634 | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy'" = False

635 | (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

636recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

637recoverable (P (TCon _ _) x _) (P (TCon _ _) y _) = x == y

637−recoverable (Constant _) (P (DCon _ _) y _) = False

638+recoverable (Constant _) (P (DCon _ _ _) y _) = False

638recoverable (Constant x) (Constant y) = x == y

639recoverable (Constant x) (Constant y) = x == y

639−recoverable (P (DCon _ _) x _) (Constant _) = False

640+recoverable (P (DCon _ _ _) x _) (Constant _) = False

640recoverable (Constant _) (P (TCon _ _) y _) = False

641recoverable (Constant _) (P (TCon _ _) y _) = False

641recoverable (P (TCon _ _) x _) (Constant _) = False

642recoverable (P (TCon _ _) x _) (Constant _) = False

642−recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

643+recoverable (P (DCon _ _ _) x _) (P (TCon _ _) y _) = False

643−recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

644+recoverable (P (TCon _ _) x _) (P (DCon _ _ _) y _) = False

644recoverable p@(Constant _) (App f a) = recoverable p f

645recoverable p@(Constant _) (App f a) = recoverable p f

645recoverable (App f a) p@(Constant _) = recoverable f p

646recoverable (App f a) p@(Constant _) = recoverable f p

646recoverable p@(P _ n _) (App f a) = recoverable p f

647recoverable p@(P _ n _) (App f a) = recoverable p f

@@ -650,10 +651,10 @@ recoverable (App f a) (App f' a')

650recoverable (App f a) (App f' a')

651recoverable (App f a) (App f' a')

651 = recoverable f f' -- && recoverable a a'

652 = recoverable f f' -- && recoverable a a'

652recoverable f (Bind _ (Pi _) sc)

653recoverable f (Bind _ (Pi _) sc)

653− | (P (DCon _ _) _ _, _) <- unApply f = False

654+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

654 | (P (TCon _ _) _ _, _) <- unApply f = False

655 | (P (TCon _ _) _ _, _) <- unApply f = False

655recoverable (Bind _ (Pi _) sc) f

656recoverable (Bind _ (Pi _) sc) f

656− | (P (DCon _ _) _ _, _) <- unApply f = False

657+ | (P (DCon _ _ _) _ _, _) <- unApply f = False

657 | (P (TCon _ _) _ _, _) <- unApply f = False

658 | (P (TCon _ _) _ _, _) <- unApply f = False

658recoverable (Bind _ (Lam _) sc) f = recoverable sc f

659recoverable (Bind _ (Lam _) sc) f = recoverable sc f

659recoverable f (Bind _ (Lam _) sc) = recoverable f sc

660recoverable f (Bind _ (Lam _) sc) = recoverable f sc

src/Idris/Coverage.hs+5−5

@@ -206,7 +206,7 @@ genAll i args

206 otherPats arg = return Placeholder

207

208 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)

210 = do xs' <- mapM otherPats (map getExpTm xs)

211 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

212 let tyn = getTy n (tt_ctxt i)

@@ -341,7 +341,7 @@ calcProd i fc topn pats

341 return (and ok)

342 _ -> return True -- defined elsewhere, can't call topn

343

344− cotype (DCon _ _) n ty

344+ cotype (DCon _ _ _) n ty

345 | (P _ t _, _) <- unApply (getRetTy ty)

346 = case lookupCtxt t (idris_datatypes i) of

347 [TI _ True _ _ _] -> True

@@ -391,7 +391,7 @@ checkTotality path fc n

391 setTotality n t'

392 addIBC (IBCTotal n t')

393 return t'

394− [TyDecl (DCon _ _) ty] ->

394+ [TyDecl (DCon _ _ _) ty] ->

395 case unApply (getRetTy ty) of

396 (P _ tyn _, _) -> do

397 let ms = case lookupCtxt tyn (idris_datatypes i) of

@@ -558,7 +558,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

558 | a == t = isInductive (fst (unApply (getRetTy tyn)))

559 (fst (unApply (getRetTy tyt)))

560 smaller ty a (ap@(App f s), _)

561− | (P (DCon _ _) n _, args) <- unApply ap

561+ | (P (DCon _ _ _) n _, args) <- unApply ap

562 = let tyn = getType n in

563 any (smaller (ty `mplus` Just tyn) a)

564 (zip args (map toJust (getArgTys tyn)))

@@ -652,7 +652,7 @@ checkMP ist i mp = if i > 0

652-- = Partial BelieveMe

653 -- if we get to a constructor, it's fine as long as it's strictly positive

654 tryPath desc path ((f, _) : es) arg

655− | [TyDecl (DCon _ _) _] <- lookupDef f (tt_ctxt ist)

655+ | [TyDecl (DCon _ _ _) _] <- lookupDef f (tt_ctxt ist)

656 = case lookupTotal f (tt_ctxt ist) of

657 [Total _] -> Unchecked -- okay so far

658 [Partial _] -> Partial (Other [f])

src/Idris/DataOpts.hs+8−7

@@ -72,19 +72,19 @@ instance Optimisable (TT Name) where

72 applyOpts (P _ (NS (UN fn) mod) _)

73 | fn == txt "toIntegerNat" && mod == prel

74 = return (App (P Ref (sNS (sUN "id") ["Basics","Prelude"]) Erased) Erased)

75− applyOpts c@(P (DCon t arity) n _)

75+ applyOpts c@(P (DCon t arity uniq) n _)

76− = return $ applyDataOptRT n t arity []

76+ = return $ applyDataOptRT n t arity uniq []

77 applyOpts t@(App f a)

78− | (c@(P (DCon t arity) n _), args) <- unApply t

78+ | (c@(P (DCon t arity uniq) n _), args) <- unApply t

79− = applyDataOptRT n t arity <$> mapM applyOpts args

79+ = applyDataOptRT n t arity uniq <$> mapM applyOpts args

80 | otherwise = App <$> applyOpts f <*> applyOpts a

81 applyOpts (Bind n b t) = Bind n <$> applyOpts b <*> applyOpts t

82 applyOpts (Proj t i) = Proj <$> applyOpts t <*> pure i

83 applyOpts t = return t

84

85-- Need to saturate arguments first to ensure that optimisation happens uniformly

86−applyDataOptRT :: Name -> Int -> Int -> [Term] -> Term

86+applyDataOptRT :: Name -> Int -> Int -> Bool -> [Term] -> Term

87−applyDataOptRT n tag arity args

87+applyDataOptRT n tag arity uniq args

88 | length args == arity = doOpts n args

89 | otherwise = let extra = satArgs (arity - length args)

90 tm = doOpts n (args ++ map (\n -> P Bound n Erased) extra)

@@ -104,4 +104,5 @@ applyDataOptRT n tag arity args

104 | s == txt "S" && nat == txt "Nat" && prelude == txt "Prelude"

105 = App (App (P Ref (sUN "prim__addBigInt") Erased) k) (Constant (BI 1))

106

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

214 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

215 rnf (PHidden x1) = rnf x1 `seq` ()

216 rnf PType = ()

217+ rnf (PUniverse _) = ()

217 rnf (PGoal x1 x2 x3 x4)

218 rnf (PGoal x1 x2 x3 x4)

218 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

219 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

219 rnf (PConstant x1) = x1 `seq` ()

220 rnf (PConstant x1) = x1 `seq` ()

src/Idris/Delaborate.hs+5

@@ -80,6 +80,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

80 de env _ Erased = Placeholder

81 de env _ Impossible = Placeholder

82 de env _ (TType i) = PType

83+ de env _ (UType u) = PUniverse u

83

84

84 dens x | fullname = x

85 dens x | fullname = x

85 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

86 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

223pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

224pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

224pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

225pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

225pprintErr' i UniverseError = text "Universe inconsistency"

226pprintErr' 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"

226pprintErr' i ProgramLineComment = text "Program line next to comment"

231pprintErr' i ProgramLineComment = text "Program line next to comment"

227pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

232pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"

228pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>

233pprintErr' 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)

722 map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

723 (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

724 logLvl 5 ("New function type " ++ show wtype)

725− let wname = sMN windex (show fname)

725+ let wname = SN (WithN windex fname)

726

727 let imps = getImps wtype -- add to implicits context

728 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)

54 = do let codata = Codata `elem` opts

55 iLOG (show (fc, doc))

56 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

58

59 addIBC (IBCDef n)

60 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)

63 = do let codata = Codata `elem` opts

64 iLOG (show fc)

65 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

67 -- if n is defined already, make sure it is just a type declaration

68 -- with the same type we've just elaborated

69 i <- getIState

@@ -71,7 +71,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

71 -- temporary, to check cons

72 when undef $ updateContext (addTyDecl n (TCon 0 0) cty)

73 let cnameinfo = cinfo info (map cname dcons)

74+ let unique = case getRetTy cty of

75+ UType UniqueType -> True

76+ _ -> False

74− cons <- mapM (elabCon cnameinfo syn n codata) dcons

77+ cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

75 ttag <- getName

78 ttag <- getName

76 i <- getIState

79 i <- getIState

77 let as = map (const Nothing) (getArgTys cty)

80 let as = map (const Nothing) (getArgTys cty)

@@ -90,7 +93,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

90 let metainf = DataMI params

93 let metainf = DataMI params

91 addIBC (IBCMetaInformation n metainf)

94 addIBC (IBCMetaInformation n metainf)

92 -- TMP HACK! Make this a data option

95 -- TMP HACK! Make this a data option

93− updateContext (addDatatype (Data n ttag cty cons))

96+ updateContext (addDatatype (Data n ttag cty unique cons))

94 updateContext (setMetaInformation n metainf)

97 updateContext (setMetaInformation n metainf)

95 mapM_ totcheck (zip (repeat fc) (map fst cons))

98 mapM_ totcheck (zip (repeat fc) (map fst cons))

96-- mapM_ (checkPositive n) cons

99-- mapM_ (checkPositive n) cons

@@ -203,12 +206,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

203-- TODO: the above is a comment from the past;

206-- TODO: the above is a comment from the past;

204-- forcenames is probably no longer needed

207-- forcenames is probably no longer needed

205elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

208elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

209+ Type -> -- for kind checking

206− (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)

210+ (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) ->

211+ Idris (Name, Type)

207−elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

212+elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

208 = do checkUndefined fc n

213 = 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)

210 ctxt <- getContext

215 ctxt <- getContext

211 let cty' = normalise ctxt [] cty

216 let cty' = normalise ctxt [] cty

217+ checkUniqueKind ckind expkind

212

218

213 -- Check that the constructor type is, in fact, a part of the family being defined

219 -- Check that the constructor type is, in fact, a part of the family being defined

214 tyIs n cty'

220 tyIs n cty'

@@ -250,6 +256,15 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

250 | otherwise = getNamePos (i + 1) sc x

256 | otherwise = getNamePos (i + 1) sc x

251 getNamePos _ _ _ = Nothing

257 getNamePos _ _ _ = Nothing

252

258

259+ -- if the constructor is a UniqueType, the datatype must be too

260+ -- (Type* is fine, since that is checked for uniqueness too)

261+ checkUniqueKind (UType 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+

253type EliminatorState = StateT (Map.Map String Int) Idris

268type EliminatorState = StateT (Map.Map String Int) Idris

254

269

255-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

270-- 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)

49import Util.Pretty(pretty, text)

50

51buildType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm ->

52− Idris (Type, PTerm, [(Int, Name)])

52+ Idris (Type, Type, PTerm, [(Int, Name)])

53buildType info syn fc opts n ty' = do

54 ctxt <- getContext

55 i <- getIState

@@ -80,7 +80,7 @@ buildType info syn fc opts n ty' = do

80 logLvl 5 $ "Rechecking"

81 logLvl 6 $ show tyT

82 logLvl 10 $ "Elaborated to " ++ showEnvDbg [] tyT

83− (cty, _) <- recheckC fc [] tyT

83+ (cty, ckind) <- recheckC fc [] tyT

84

85 -- record the implicit and inaccessible arguments

86 i <- getIState

@@ -99,7 +99,7 @@ buildType info syn fc opts n ty' = do

99 setFnInfo n fninfo

100 addIBC (IBCFnInfo n fninfo)

101

102− return (cty, ty, inacc)

102+ return (cty, ckind, ty, inacc)

103 where

104 patToImp (Bind n (PVar t) sc) = Bind n (Pi t) (patToImp sc)

105 patToImp (Bind n b sc) = Bind n b (patToImp sc)

@@ -121,7 +121,7 @@ elabType' :: Bool -> -- normalise it

121elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

122 n = liftname info n_in in -}

123 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'

125

126 addStatics n cty ty

127 let nty = cty -- normalise ctxt [] cty

src/Idris/ElabDecls.hs+3−3

@@ -122,9 +122,9 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

122 p_synEq args = Nothing

123

124 nMaybe = P (TCon 0 2) (sNS (sUN "Maybe") ["Maybe", "Prelude"]) Erased

125− vnJust = VP (DCon 1 2) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

125+ vnJust = VP (DCon 1 2 False) (sNS (sUN "Just") ["Maybe", "Prelude"]) VErased

126− vnNothing = VP (DCon 0 1) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

126+ vnNothing = VP (DCon 0 1 False) (sNS (sUN "Nothing") ["Maybe", "Prelude"]) VErased

127− vnRefl = VP (DCon 0 2) eqCon VErased

127+ vnRefl = VP (DCon 0 2 False) eqCon VErased

128

129 synEqTy = Bind (sUN "a") (Pi (TType (UVar (-3))))

130 (Bind (sUN "b") (Pi (TType (UVar (-3))))

src/Idris/ElabTerm.hs+78−11

@@ -238,6 +238,7 @@ elab ist info emode opts fn tm

238 -> ElabD ()

239 elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

240 elab' ina PType = do apply RType []; solve

241+ elab' ina (PUniverse u) = do apply (RUType u) []; solve

241-- elab' (_,_,inty) (PConstant c)

242-- elab' (_,_,inty) (PConstant c)

242-- | constType c && pattern && not reflection && not inty

243-- | constType c && pattern && not reflection && not inty

243-- = lift $ tfail (Msg "Typecase is not allowed")

244-- = lift $ tfail (Msg "Typecase is not allowed")

@@ -629,7 +630,7 @@ elab ist info emode opts fn tm

629 elab' ina Placeholder = do (h : hs) <- get_holes

630 elab' ina Placeholder = do (h : hs) <- get_holes

630 movelast h

631 movelast h

631 elab' ina (PMetavar n) = let n' = mkN n in

632 elab' ina (PMetavar n) = let n' = mkN n in

632− do attack; defer n'; solve

633+ do attack; defer [] n'; solve

633 where mkN n@(NS _ _) = n

634 where mkN n@(NS _ _) = n

634 mkN n = case namespace info of

635 mkN n = case namespace info of

635 Just xs@(_:_) -> sNS n xs

636 Just xs@(_:_) -> sNS n xs

@@ -683,14 +684,39 @@ elab ist info emode opts fn tm

683 focus valn

684 focus valn

684 elabE (True, a, inty, qq) scr

685 elabE (True, a, inty, qq) scr

685 args <- get_env

686 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+

686 cname <- unique_hole' True (mkCaseName fn)

710 cname <- unique_hole' True (mkCaseName fn)

687 let cname' = mkN cname

711 let cname' = mkN cname

688− elab' ina (PMetavar cname')

712+-- elab' ina (PMetavar cname')

713+ attack; defer argsDropped cname'; solve

714+

689 -- if the scrutinee is one of the 'args' in env, we should

715 -- if the scrutinee is one of the 'args' in env, we should

690 -- inspect it directly, rather than adding it as a new argument

716 -- inspect it directly, rather than adding it as a new argument

691 let newdef = PClauses fc [] cname'

717 let newdef = PClauses fc [] cname'

692 (caseBlock fc cname'

718 (caseBlock fc cname'

693− (map (isScr scr) (reverse args)) opts)

719+ (map (isScr scr) (reverse args')) opts)

694 -- elaborate case

720 -- elaborate case

695 updateAux (newdef : )

721 updateAux (newdef : )

696 -- if we haven't got the type yet, hopefully we'll get it later!

722 -- 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

704 mkN n = case namespace info of

730 mkN n = case namespace info of

705 Just xs@(_:_) -> sNS n xs

731 Just xs@(_:_) -> sNS n xs

706 _ -> n

732 _ -> 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+

707 elab' ina (PUnifyLog t) = do unifyLog True

774 elab' ina (PUnifyLog t) = do unifyLog True

708 elab' ina t

775 elab' ina t

709 unifyLog False

776 unifyLog False

@@ -1541,7 +1608,7 @@ reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref

1541reifyTTNameType t@(App _ _)

1608reifyTTNameType t@(App _ _)

1542 = case unApply t of

1609 = case unApply t of

1543 (P _ f _, [Constant (I tag), Constant (I num)])

1610 (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!

1545 | f == reflm "TCon" -> return $ TCon tag num

1612 | f == reflm "TCon" -> return $ TCon tag num

1546 _ -> fail ("Unknown reflection name type: " ++ show t)

1613 _ -> fail ("Unknown reflection name type: " ++ show t)

1547reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

1614reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)

@@ -1799,8 +1866,8 @@ reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]

1799reflectNameType :: NameType -> Raw

1866reflectNameType :: NameType -> Raw

1800reflectNameType (Bound) = Var (reflm "Bound")

1867reflectNameType (Bound) = Var (reflm "Bound")

1801reflectNameType (Ref) = Var (reflm "Ref")

1868reflectNameType (Ref) = Var (reflm "Ref")

1802−reflectNameType (DCon x y)

1869+reflectNameType (DCon x y _)

1803− = reflCall "DCon" [RConstant (I x), RConstant (I y)]

1870+ = reflCall "DCon" [RConstant (I x), RConstant (I y)] -- FIXME: Uniqueness!

1804reflectNameType (TCon x y)

1871reflectNameType (TCon x y)

1805 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1872 = reflCall "TCon" [RConstant (I x), RConstant (I y)]

1806

1873

@@ -2098,7 +2165,7 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

2098 parts -> ReflectionError errorparts e

2165 parts -> ReflectionError errorparts e

2099

2166

2100fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

2167fromTTMaybe :: 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)

2102 | just == txt "Just" = Just tm

2169 | just == txt "Just" = Just tm

2103fromTTMaybe x = Nothing

2170fromTTMaybe x = Nothing

2104

2171

@@ -2109,9 +2176,9 @@ reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

2109-- representation. Not in Idris or ElabD monads because it should be usable

2176-- representation. Not in Idris or ElabD monads because it should be usable

2110-- from either.

2177-- from either.

2111reifyReportPart :: Term -> Either Err ErrorReportPart

2178reifyReportPart :: 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" =

2113 Right (TextPart msg)

2180 Right (TextPart msg)

2114−reifyReportPart (App (P (DCon _ _) n _) ttn)

2181+reifyReportPart (App (P (DCon _ _ _) n _) ttn)

2115 | n == reflm "NamePart" =

2182 | n == reflm "NamePart" =

2116 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2183 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

2117 Error e -> Left . InternalMsg $

2184 Error e -> Left . InternalMsg $

@@ -2119,7 +2186,7 @@ reifyReportPart (App (P (DCon _ _) n _) ttn)

2119 show ttn ++

2186 show ttn ++

2120 " when reflecting an error:" ++ show e

2187 " when reflecting an error:" ++ show e

2121 OK (n', _)-> Right $ NamePart n'

2188 OK (n', _)-> Right $ NamePart n'

2122−reifyReportPart (App (P (DCon _ _) n _) tm)

2189+reifyReportPart (App (P (DCon _ _ _) n _) tm)

2123 | n == reflm "TermPart" =

2190 | n == reflm "TermPart" =

2124 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2191 case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

2125 Error e -> Left . InternalMsg $

2192 Error e -> Left . InternalMsg $

@@ -2127,7 +2194,7 @@ reifyReportPart (App (P (DCon _ _) n _) tm)

2127 show tm ++

2194 show tm ++

2128 " when reflecting an error:" ++ show e

2195 " when reflecting an error:" ++ show e

2129 OK (tm', _) -> Right $ TermPart tm'

2196 OK (tm', _) -> Right $ TermPart tm'

2130−reifyReportPart (App (P (DCon _ _) n _) tm)

2197+reifyReportPart (App (P (DCon _ _ _) n _) tm)

2131 | n == reflm "SubReport" =

2198 | n == reflm "SubReport" =

2132 case unList tm of

2199 case unList tm of

2133 Just xs -> do subParts <- mapM reifyReportPart xs

2200 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]

281

282 -- for the purposes of erasure, we can disregard the projection

283 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

285

286 -- other ProjCase's are not supported

287 getDepsSC fn es vs (ProjCase t alts) = error $ "ProjCase not supported:\n" ++ show (ProjCase t alts)

288

289 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)

291 -- we case-split on this variable, which marks it as used

292 -- (unless there is exactly one case branch)

293 -- 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]

370 getDepsTerm vs bs cd app@(App _ _)

371 | (fun, args) <- unApply app = case fun of

372 -- instance constructors -> create metamethod deps

373− P (DCon _ _) ctorName@(SN (InstanceCtorN className)) _

373+ P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

374 -> conditionalDeps ctorName args -- regular data ctor stuff

375 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

376

377 -- ordinary constructors

378 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

380

381 -- mkForeign* calls must be special-cased because they are variadic

382 -- 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]

469 -- Get the number of arguments that might be considered for erasure.

470 getArity :: Name -> Int

471 getArity (SN (WhereN i' ctorName (MN i field)))

472− | Just (TyDecl (DCon _ _) ty) <- lookupDefExact ctorName ctx

472+ | Just (TyDecl (DCon _ _ _) ty) <- lookupDefExact ctorName ctx

473 = let argTys = map snd $ getArgTys ty

474 in if i <= length argTys

475 then length $ getArgTys (argTys !! i)

@@ -479,7 +479,7 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]

479

480 getArity n = case lookupDefExact n ctx of

481 Just (CaseOp ci ty tys def tot cdefs) -> length tys

482− Just (TyDecl (DCon tag arity) _) -> arity

482+ Just (TyDecl (DCon tag arity _) _) -> arity

483 Just (TyDecl (Ref) ty) -> length $ getArgTys ty

484 Just (Operator ty arity op) -> arity

485 Just df -> error $ "Erasure/getArity: unrecognised entity '"

src/Idris/IBC.hs+24−7

@@ -31,7 +31,7 @@ import Codec.Compression.Zlib (compress)

31import Util.Zlib (decompressEither)

32

33ibcVersion :: Word8

34−ibcVersion = 78

34+ibcVersion = 79

35

36data IBCFile = IBCFile { ver :: Word8,

37 sourcefile :: FilePath,

@@ -183,8 +183,8 @@ ibc i (IBCDef n) f

183 = do c' <- updateSC c; r' <- updateSC r

184 return (CaseDefs (ts, t) (cs, c') (is, i) (rs, r'))

185

186− updateSC (Case n alts) = do alts' <- mapM updateAlt alts

186+ updateSC (Case up n alts) = do alts' <- mapM updateAlt alts

187− return (Case n alts')

187+ return (Case up n alts')

188 updateSC (ProjCase t alts) = do t' <- update t

189 alts' <- mapM updateAlt alts

190 return (ProjCase t' alts')

@@ -631,12 +631,24 @@ instance Binary CGInfo where

631 x4 <- get

632 x5 <- get

633 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+

634instance Binary SC where

645instance Binary SC where

635 put x

646 put x

636 = case x of

647 = case x of

637− Case x1 x2 -> do putWord8 0

648+ Case x1 x2 x3 -> do putWord8 0

638− put x1

649+ put x1

639− put x2

650+ put x2

651+ put x3

640 ProjCase x1 x2 -> do putWord8 1

652 ProjCase x1 x2 -> do putWord8 1

641 put x1

653 put x1

642 put x2

654 put x2

@@ -650,7 +662,8 @@ instance Binary SC where

650 case i of

662 case i of

651 0 -> do x1 <- get

663 0 -> do x1 <- get

652 x2 <- get

664 x2 <- get

665+ x3 <- get

653− return (Case x1 x2)

666+ return (Case x1 x2 x3)

654 1 -> do x1 <- get

667 1 -> do x1 <- get

655 x2 <- get

668 x2 <- get

656 return (ProjCase x1 x2)

669 return (ProjCase x1 x2)

@@ -1486,6 +1499,8 @@ instance Binary PTerm where

1486 PDisamb x1 x2 -> do putWord8 37

1499 PDisamb x1 x2 -> do putWord8 37

1487 put x1

1500 put x1

1488 put x2

1501 put x2

1502+ PUniverse x1 -> do putWord8 38

1503+ put x1

1489

1504

1490 get

1505 get

1491 = do i <- getWord8

1506 = do i <- getWord8

@@ -1602,6 +1617,8 @@ instance Binary PTerm where

1602 37 -> do x1 <- get

1617 37 -> do x1 <- get

1603 x2 <- get

1618 x2 <- get

1604 return (PDisamb x1 x2)

1619 return (PDisamb x1 x2)

1620+ 38 -> do x1 <- get

1621+ return (PUniverse x1)

1605 _ -> error "Corrupted binary data for PTerm"

1622 _ -> error "Corrupted binary data for PTerm"

1606

1623

1607instance (Binary t) => Binary (PTactic' t) where

1624instance (Binary t) => Binary (PTactic' t) where

src/Idris/ParseExpr.hs+2

@@ -307,7 +307,9 @@ simpleExpr syn =

307 <|> do reserved "elim_for"; fc <- getFC; t <- fnName; return (PRef fc (SN $ ElimN t))

308 <|> proofExpr syn

309 <|> tacticsExpr syn

310+ <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

310 <|> do reserved "Type"; return PType

311 <|> do reserved "Type"; return PType

312+ <|> do reserved "UniqueType"; return $ PUniverse UniqueType

311 <|> do c <- constant

313 <|> do c <- constant

312 fc <- getFC

314 fc <- getFC

313 return (modifyConst syn fc (PConstant c))

315 return (modifyConst syn fc (PConstant c))

src/Idris/ProofSearch.hs+4−4

@@ -59,7 +59,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

59 where

60 -- if nothing worked, make a new metavariable

61 tryAllFns [] | fromProver = cantSolveGoal

62− tryAllFns [] = do attack; defer nroot; solve

62+ tryAllFns [] = do attack; defer [] nroot; solve

63 tryAllFns (f : fs) = try' (tryFn f) (tryAllFns fs) True

64

65 tryFn (f, args) = do let imps = map isImp args

@@ -75,7 +75,7 @@ proofSearch False fromProver depth elab _ nroot [fn] ist

75 if fromProver then cantSolveGoal

76 else do

77 mapM_ (\ h -> do focus h

78− attack; defer nroot; solve)

78+ attack; defer [] nroot; solve)

79 (hs' \\ hs)

80-- (filter (\ (x, y) -> not x) (zip (map fst imps) args))

81 solve

@@ -96,7 +96,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

96 toUN t = t

97

98 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"

100 psRec False d = tryCons d hints

101 psRec True d = try' (trivial elab ist)

102 (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

@@ -104,7 +104,7 @@ proofSearch rec fromProver maxDepth elab fn nroot hints ist

104 -- if all else fails, make a new metavariable

105 (if fromProver

106 then cantSolveGoal

107− else do attack; defer nroot; solve) True) True

107+ else do attack; defer [] nroot; solve) True) True

108

109 getFn d Nothing = []

110 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

25

26instance Transform SC where

27 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))

29 trans t x = t x

30 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)

32 trans t (STerm tm) = STerm (t tm)

33 trans t x = x

34

src/Idris/WhoCalls.hs+2−2

@@ -36,13 +36,13 @@ namesBinder (NLet ty val) = names ty ++ names val

36namesBinder b = names (binderTy b)

37

38occursSC :: Name -> SC -> Bool

39−occursSC n (Case _ alts) = any (occursCaseAlt n) alts

39+occursSC n (Case _ _ alts) = any (occursCaseAlt n) alts

40occursSC n (ProjCase t alts) = occurs n t || any (occursCaseAlt n) alts

41occursSC n (STerm t) = occurs n t

42occursSC n _ = False

43

44namesSC :: SC -> [Name]

45−namesSC (Case _ alts) = concatMap namesCaseAlt alts

45+namesSC (Case _ _ alts) = concatMap namesCaseAlt alts

46namesSC (ProjCase t alts) = names t ++ concatMap namesCaseAlt alts

47namesSC (STerm t) = names t

48namesSC _ = []

test/Makefile+1−1

@@ -14,7 +14,7 @@ test_js:

14 @perl ./runtest.pl without sugar004 reg029 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node

15

16test_llvm:

17− @perl ./runtest.pl without sugar004 io003 buffer001 --codegen llvm

17+ @perl ./runtest.pl without primitives003 sugar004 io003 buffer001 --codegen llvm

18

19update:

20 /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:

2Can't unify

3 P x

4with

test/reg018/expected+1−1

@@ -1,5 +1,5 @@

1reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

3reg018b.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

5reg018d.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}

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: {tbad.qsort'18}

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:

10 [92mplus[0m [95mn[0m [95mn[0m

11 with

12 [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:

14Can't unify

15 [94mParity[0m ([92mplus[0m ([91mS[0m [95mj[0m) ([91mS[0m [95mj[0m))

16with