git.iko.soy/Idris-dev
on master help sign in
Propagate '%assert_total' to with blocks

Otherwise they don't reduce properly when typechecking

commit170da6187954414f34d63badf860a60458240183 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 13 Oct 2013, 22:27 (13 years ago) parent54a89bf
9 files changed+74
compare with master
unifiedsplit
idris.cabal+9 src/Idris/ElabDecls.hs+5 src/Idris/Parser.hs+1 test/reg023/expected+12 test/reg023/reg023.idr+8 test/reg023/run+3 test/reg024/expected+1 test/reg024/reg024.idr+31 test/reg024/run+4
idris.cabal+9
@@ -165,6 +165,15 @@ Extra-source-files:
165165 test/reg021/run
166166 test/reg021/*.idr
167167 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
168177 test/test001/run
169178 test/test001/*.idr
170179 test/test001/expected
src/Idris/ElabDecls.hs+5
@@ -1010,6 +1010,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
10101010 wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))
10111011 withblock
10121012 logLvl 3 ("with block " ++ show wb)
1013+ -- propagate totality assertion to the new definitions
1014+ when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]
10131015 mapM_ (elabDecl EAll info) wb
10141016
10151017 -- rhs becomes: fname' ps wval
@@ -1501,6 +1503,9 @@ elabDecl' what info (PMutual f ps)
15011503 mapM_ (elabDecl EDefns info) ps
15021504 -- Do totality checking after entire mutual block
15031505 i <- get
1506+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
1507+ updateContext (simplifyCasedef n))
1508+ (map snd (idris_totcheck i))
15041509 mapM_ buildSCG (idris_totcheck i)
15051510 mapM_ checkDeclTotality (idris_totcheck i)
15061511 clear_totcheck
src/Idris/Parser.hs+1
@@ -1030,6 +1030,7 @@ loadSource lidr f
10301030
10311031 toMutual :: PDecl -> PDecl
10321032 toMutual m@(PMutual _ d) = m
1033+ toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)
10331034 toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
10341035 case x of
10351036 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+ Nat
4+with
5+ f Nat
6+
7+Specifically:
8+ Can't unify
9+ Nat
10+ with
11+ f Nat
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