992acb4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix regression with data declarations in where

Also, start adding tests for examples from the tutorial (we need to cover it all, really).

commit992acb426b9fe3beb048749f735c675a670ac513 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 10 Mar 2014, 20:47 (13 years ago) parentfdb46c7

7 files changed+24−4

compare with master

unifiedsplit

idris.cabal+4 src/Idris/AbsSyntax.hs+2−2 src/Idris/Core/Elaborate.hs+5−2 test/README+1 test/tutorial001/expected test/tutorial001/run+3 test/tutorial001/tutorial001.idr+9

idris.cabal+4

@@ -382,6 +382,10 @@ Extra-source-files:

382382 test/totality003/*.idr

383383 test/totality003/expected

384384

385+ test/tutorial001/run

386+ test/tutorial001/*.idr

387+ test/tutorial001/expected

388+

385389source-repository head

386390 type: git

387391 location: git://github.com/idris-lang/Idris-dev.git

src/Idris/AbsSyntax.hs+2−2

@@ -1070,14 +1070,14 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

10701070 (map econ cons)

10711071 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

10721072 econ (doc, argDocs, n, t, fc, fs)

1073− = (doc, argDocs, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1073+ = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

10741074expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

10751075 = if tn `elem` ns

10761076 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

10771077 cdoc (dec cn) conty

10781078 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

10791079 cdoc (dec cn) conty

1080− where conty = piBindp impl ps (expandParams dec ps ns [] cty)

1080+ where conty = piBindp expl ps (expandParams dec ps ns [] cty)

10811081expandParamsD rhs ist dec ps ns (PParams f params pds)

10821082 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

10831083 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/Core/Elaborate.hs+5−2

@@ -625,9 +625,12 @@ no_errors tac err

625625 ps' <- get_probs

626626 if (length ps' > length ps) then

627627 case reverse ps' of

628− ((x,y,env,err,_) : _) ->

628+ ((x,y,env,inerr,_) : _) ->

629629 let env' = map (\(x, b) -> (x, binderTy b)) env in

630− lift $ tfail $ CantUnify False x y err env' 0

630+ lift $ tfail $

631+ case err of

632+ Nothing -> CantUnify False x y inerr env' 0

633+ Just e -> e

631634 else return $! ()

632635

633636-- Try a tactic, if it fails, try another

test/README+1

@@ -12,5 +12,6 @@ primitives: Primitive types

1212proof: Theorem proving, tactics

1313sugar: Syntactic sugar, syntax extensions

1414totality: Totality checking

15+tutorial: Examples from the tutorial

1516

1617reg: Regression tests, covering previous bug fixes

test/tutorial001/expectednew file

No changes to the content.

test/tutorial001/runnew file+3

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

1+#!/usr/bin/env bash

2+idris --check tutorial001.idr

3+rm -f *.ibc

test/tutorial001/tutorial001.idrnew file+9

@@ -0,0 +1,9 @@

1+foo : Int -> Int

2+foo x = case isLT of

3+ Yes => x*2

4+ No => x*4

5+ where

6+ data MyLT = Yes | No

7+ isLT : MyLT

8+ isLT = if x < 20 then Yes else No