eed3117 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Take some more care with forcing

If the forced name is only forceable because we've reduced a name, and that name isn't exported, then we can't actually get the name in other modules! So, check for forceable names before reducing the type, not after. (We could do a bit better than this, in fact, and reduce names which are public export, but there isn't a huge benefit to this at the moment so I'll save it for later.)

commiteed311783bc66473dfcf05da093f08770e70adc6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 14 Mar 2017, 14:32 (10 years ago) parentd3fa352

6 files changed+60−5

compare with master

unifiedsplit

src/Idris/Elab/Data.hs+8−4 test/TestData.hs+2−1 test/reg001/Area.idr+12 test/reg001/TestEx.idr+31 test/reg001/expected+3 test/reg001/run+4

src/Idris/Elab/Data.hs+8−4

@@ -193,9 +193,12 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

193193

194194 -- Check that the constructor type is, in fact, a part of the family being defined

195195 tyIs n cty'

196+ -- Need to calculate forceability from the non-normalised type,

197+ -- because we might not be able to export the definitions which

198+ -- we're normalising which changes the forceability status!

196199 let force = if tn == sUN "Delayed"

197200 then [] -- TMP HACK! Totality checker needs this info

198− else forceArgs ctxt cty'

201+ else forceArgs ctxt tn cty

199202

200203 logElab 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

201204 logElab 5 $ "Inaccessible args: " ++ show inacc

@@ -264,8 +267,8 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

264267 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

265268 checkUniqueKind _ _ = return ()

266269

267−forceArgs :: Context -> Type -> [Int]

268−forceArgs ctxt ty = forceFrom 0 ty

270+forceArgs :: Context -> Name -> Type -> [Int]

271+forceArgs ctxt tn ty = forceFrom 0 ty

269272 where

270273 -- for each argument, substitute in MN pos "FF"

271274 -- then when we look at the return type, if we see MN pos name

@@ -281,7 +284,8 @@ forceArgs ctxt ty = forceFrom 0 ty

281284 -- (FIXME: Actually the real risk is if we erase something a programmer

282285 -- definitely wants, which is particularly the case with 'views'.

283286 -- So perhaps we need a way of marking that in the source?)

284− | (P _ ty _, args) <- unApply sc

287+ | (P _ ty _, args) <- unApply sc,

288+ ty == tn -- Must be the right top level type!

285289 = if null (concatMap (findNonForcePos True) args)

286290 then nub (concatMap findForcePos args)

287291 else []

test/TestData.hs+2−1

@@ -222,7 +222,8 @@ testFamiliesData = [

222222 ( 4, ANY ),

223223 ( 5, ANY )]),

224224 ("reg", "Regressions",

225− [ ( 2, ANY ),

225+ [ ( 1, ANY ),

226+ ( 2, ANY ),

226227 ( 4, ANY ),

227228 ( 5, ANY ),

228229 ( 13, ANY ),

test/reg001/Area.idrnew file+12

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

1+import TestEx

3+area : Shape -> Double

4+area s with (shapeView s)

5+ area (triangle base height) | STriangle = 0.5 * base * height

6+ area (rectangle width height) | SRectangle = width * height

7+ area (circle radius) | SCircle = pi * radius * radius

9+main : IO ()

10+main = do printLn (area (rectangle 2 3))

11+ printLn (area (triangle 2 3))

12+ printLn (area (circle 1))

test/reg001/TestEx.idrnew file+31

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

1+module TestEx

3+export

4+data Shape = Triangle Double Double

5+ | Rectangle Double Double

6+ | Circle Double

8+export

9+triangle : Double -> Double -> Shape

10+triangle = Triangle

11+

12+export

13+rectangle : Double -> Double -> Shape

14+rectangle = Rectangle

15+

16+export

17+circle : Double -> Shape

18+circle = Circle

19+

20+public export

21+data ShapeView : Shape -> Type where

22+ STriangle : ShapeView (triangle base height)

23+ SRectangle : ShapeView (rectangle width height)

24+ SCircle : ShapeView (circle radius)

25+

26+export

27+shapeView : (s : Shape) -> ShapeView s

28+shapeView (Triangle x y) = STriangle

29+shapeView (Rectangle x y) = SRectangle

30+shapeView (Circle x) = SCircle

31+

test/reg001/expectednew file+3

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

1+6

2+3

3+3.141592653589793

test/reg001/runnew file+4

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

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ Area.idr -o reg001

3+./reg001

4+rm -f reg001 *.ibc