eed3117 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

193

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

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

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

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

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

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

198− else forceArgs ctxt cty'

201+ else forceArgs ctxt tn cty

199

202

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

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

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

204 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

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

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

265 checkUniqueKind _ _ = return ()

268 checkUniqueKind _ _ = return ()

266

269

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

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

268−forceArgs ctxt ty = forceFrom 0 ty

271+forceArgs ctxt tn ty = forceFrom 0 ty

269 where

272 where

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

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

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

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

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

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

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

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

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

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

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

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

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

286 then nub (concatMap findForcePos args)

290 then nub (concatMap findForcePos args)

287 else []

291 else []

test/TestData.hs+2−1

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

222 ( 4, ANY ),

223 ( 5, ANY )]),

224 ("reg", "Regressions",

225+ [ ( 1, ANY ),

225− [ ( 2, ANY ),

226+ ( 2, ANY ),

226 ( 4, ANY ),

227 ( 4, ANY ),

227 ( 5, ANY ),

228 ( 5, ANY ),

228 ( 13, ANY ),

229 ( 13, ANY ),

test/reg001/Area.idrnew file+12

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

1+import TestEx

2+

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

8+

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

2+

3+export

4+data Shape = Triangle Double Double

5+ | Rectangle Double Double

6+ | Circle Double

7+

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