git.iko.soy/Idris-dev
on master help sign in
Fix regression with data declarations in where
992acb4Edwin Brady
idris.cabal+4
compare with master
unifiedsplit
@@ -382,6 +382,10 @@ Extra-source-files:
382 test/totality003/*.idr
382 test/totality003/*.idr
383 test/totality003/expected
383 test/totality003/expected
384
384
385+ test/tutorial001/run
386+ test/tutorial001/*.idr
387+ test/tutorial001/expected
388+
385source-repository head
389source-repository head
386 type: git
390 type: git
387 location: git://github.com/idris-lang/Idris-dev.git
391 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)
1070 (map econ cons)
1070 (map econ cons)
1071 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1071 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1072 econ (doc, argDocs, n, t, fc, fs)
1072 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)
1074expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
1074expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)
1075 = if tn `elem` ns
1075 = if tn `elem` ns
1076 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1076 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))
1077 cdoc (dec cn) conty
1077 cdoc (dec cn) conty
1078 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1078 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)
1079 cdoc (dec cn) conty
1079 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)
1081expandParamsD rhs ist dec ps ns (PParams f params pds)
1081expandParamsD rhs ist dec ps ns (PParams f params pds)
1082 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1082 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1083 (map (expandParamsD True ist dec ps ns) pds)
1083 (map (expandParamsD True ist dec ps ns) pds)
src/Idris/Core/Elaborate.hs+5−2
@@ -625,9 +625,12 @@ no_errors tac err
625 ps' <- get_probs
625 ps' <- get_probs
626 if (length ps' > length ps) then
626 if (length ps' > length ps) then
627 case reverse ps' of
627 case reverse ps' of
628− ((x,y,env,err,_) : _) ->
628+ ((x,y,env,inerr,_) : _) ->
629 let env' = map (\(x, b) -> (x, binderTy b)) env in
629 let env' = map (\(x, b) -> (x, binderTy b)) env in
630+ lift $ tfail $
631+ case err of
630− lift $ tfail $ CantUnify False x y err env' 0
632+ Nothing -> CantUnify False x y inerr env' 0
633+ Just e -> e
631 else return $! ()
634 else return $! ()
632
635
633-- Try a tactic, if it fails, try another
636-- Try a tactic, if it fails, try another
test/README+1
@@ -12,5 +12,6 @@ primitives: Primitive types
12proof: Theorem proving, tactics
12proof: Theorem proving, tactics
13sugar: Syntactic sugar, syntax extensions
13sugar: Syntactic sugar, syntax extensions
14totality: Totality checking
14totality: Totality checking
15+tutorial: Examples from the tutorial
15
16
16reg: Regression tests, covering previous bug fixes
17reg: 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
9+