170da61 · Idris-dev · git.iko.soy

idris.cabal+9

compare with master

unifiedsplit

@@ -165,6 +165,15 @@ Extra-source-files:

165 test/reg021/run

166 test/reg021/*.idr

167 test/reg021/expected

168+ test/reg022/run

169+ test/reg022/*.idr

170+ test/reg022/expected

171+ test/reg023/run

172+ test/reg023/*.idr

173+ test/reg023/expected

174+ test/reg024/run

175+ test/reg024/*.idr

176+ test/reg024/expected

168 test/test001/run

177 test/test001/run

169 test/test001/*.idr

178 test/test001/*.idr

170 test/test001/expected

179 test/test001/expected

src/Idris/ElabDecls.hs+5

@@ -1010,6 +1010,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1010 wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))

1011 withblock

1012 logLvl 3 ("with block " ++ show wb)

1013+ -- propagate totality assertion to the new definitions

1014+ when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

1013 mapM_ (elabDecl EAll info) wb

1015 mapM_ (elabDecl EAll info) wb

1014

1016

1015 -- rhs becomes: fname' ps wval

1017 -- rhs becomes: fname' ps wval

@@ -1501,6 +1503,9 @@ elabDecl' what info (PMutual f ps)

1501 mapM_ (elabDecl EDefns info) ps

1503 mapM_ (elabDecl EDefns info) ps

1502 -- Do totality checking after entire mutual block

1504 -- Do totality checking after entire mutual block

1503 i <- get

1505 i <- get

1506+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1507+ updateContext (simplifyCasedef n))

1508+ (map snd (idris_totcheck i))

1504 mapM_ buildSCG (idris_totcheck i)

1509 mapM_ buildSCG (idris_totcheck i)

1505 mapM_ checkDeclTotality (idris_totcheck i)

1510 mapM_ checkDeclTotality (idris_totcheck i)

1506 clear_totcheck

1511 clear_totcheck

src/Idris/Parser.hs+1

@@ -1030,6 +1030,7 @@ loadSource lidr f

1030

1031 toMutual :: PDecl -> PDecl

1032 toMutual m@(PMutual _ d) = m

1033+ toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1033 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in

1034 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in

1034 case x of

1035 case x of

1035 PClauses _ _ _ _ -> r

1036 PClauses _ _ _ _ -> r

test/reg023/expectednew file+12

@@ -0,0 +1,12 @@

1+reg023.idr:7:When elaborating right hand side of bad:

2+Can't unify

3+ [94mNat[0m

4+with

5+ [92mf[0m [94mNat[0m

6+

7+Specifically:

8+ Can't unify

9+ [94mNat[0m

10+ with

11+ [92mf[0m [94mNat[0m

12+

test/reg023/reg023.idrnew file+8

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

1+module Foo

2+

3+f : Type -> Type

4+f x = f x

5+

6+bad : f Nat

7+bad = Z

8+

test/reg023/runnew file+3

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

1+#!/bin/bash

2+idris $@ reg023.idr --check

3+rm -f *.ibc

test/reg024/expectednew file+1

@@ -0,0 +1 @@

1+The answer is 42

test/reg024/reg024.idrnew file+31

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

1+module Main

2+

3+data Format = End | FInt Format | FStr Format | FChar Char Format

4+

5+fromList : List Char -> Format

6+fromList Nil = End

7+fromList ('%' :: 'd' :: cs) = FInt (fromList cs)

8+fromList ('%' :: 's' :: cs) = FStr (fromList cs)

9+fromList (c :: cs) = FChar c (fromList cs)

10+

11+PrintfType : Format -> Type

12+PrintfType End = String

13+PrintfType (FInt rest) = Int -> PrintfType rest

14+PrintfType (FStr rest) = String -> PrintfType rest

15+PrintfType (FChar c rest) = PrintfType rest

16+

17+printf : (fmt: String) -> PrintfType (fromList $ unpack fmt)

18+printf fmt = printFormat (fromList $ unpack fmt) where

19+ printFormat : (fmt: Format) -> PrintfType fmt

20+ printFormat fmt = rec fmt "" where

21+ rec : (f: Format) -> String -> PrintfType f

22+ rec End acc = acc

23+ rec (FInt rest) acc = \i: Int => rec rest (acc ++ (show i))

24+ rec (FStr rest) acc = \s: String => rec rest (acc ++ s)

25+ rec (FChar c rest) acc = rec rest (acc ++ (pack [c]))

26+

27+test : String

28+test = printf "The %s is %d" "answer" 42

29+

30+main : IO ()

31+main = print test

test/reg024/runnew file+4

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

1+#!/bin/bash

2+idris $@ reg024.idr -o reg024

3+./reg024

4+rm -f reg024 *.ibc