940da80 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -6,6 +6,7 @@ New in 0.9.13:

6* Command line option -e (or --eval) to evaluate expressions without loading the

7 REPL. This is useful for writing more portable tests.

8* Many more of the basic functions and datatypes are documented.

9+* Removed javascript lib in favor of idris-hackers/iQuery

9

10

10Internal changes

11Internal changes

11

12

CONTRIBUTORS+1

@@ -8,6 +8,7 @@ Edwin Brady

8David Raymond Christiansen

9Jason Dagit

10Simon Fowler

11+Google

11Cezar Ionescu

12Cezar Ionescu

12Irene Knapp

13Irene Knapp

13Shea Levy

14Shea Levy

idris.cabal+3−5

@@ -103,11 +103,6 @@ Extra-source-files:

103 libs/oldeffects/Effect/*.idr

104 libs/oldeffects/*.idr

105

106− libs/javascript/*.idr

107− libs/javascript/JavaScript/*.idr

108− libs/javascript/Makefile

109− libs/javascript/javascript.ipkg

110−

111 llvm/*.c

106 llvm/*.c

112 llvm/Makefile

107 llvm/Makefile

113

108

@@ -237,6 +232,9 @@ Extra-source-files:

237 test/reg041/run

232 test/reg041/run

238 test/reg041/*.idr

233 test/reg041/*.idr

239 test/reg041/expected

234 test/reg041/expected

235+ test/reg042/run

236+ test/reg042/*.idr

237+ test/reg042/expected

240

238

241 test/basic001/run

239 test/basic001/run

242 test/basic001/*.idr

240 test/basic001/*.idr

libs/Makefile−3

@@ -2,19 +2,16 @@ build:

2 $(MAKE) -C prelude build

3 $(MAKE) -C base build

4 $(MAKE) -C effects build

5− $(MAKE) -C javascript build

6

5

7

6

8install:

7install:

9 $(MAKE) -C prelude install

8 $(MAKE) -C prelude install

10 $(MAKE) -C base install

9 $(MAKE) -C base install

11 $(MAKE) -C effects install

10 $(MAKE) -C effects install

12− $(MAKE) -C javascript install

13

11

14clean:

12clean:

15 $(MAKE) -C prelude clean

13 $(MAKE) -C prelude clean

16 $(MAKE) -C base clean

14 $(MAKE) -C base clean

17 $(MAKE) -C effects clean

15 $(MAKE) -C effects clean

18− $(MAKE) -C javascript clean

19

16

20.PHONY: build install clean

17.PHONY: build install clean

libs/base/Data/Complex.idr+2−2

@@ -62,8 +62,8 @@ conjugate (r:+i) = (r :+ (0-i))

62-- We can't do "instance Num a => Num (Complex a)" because

63-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float

64instance Num (Complex Float) where

65− (+) (a:+b) (c:+d) = ((a+b):+(c+d))

65+ (+) (a:+b) (c:+d) = ((a+c):+(b+d))

66− (-) (a:+b) (c:+d) = ((a-b):+(c-d))

66+ (-) (a:+b) (c:+d) = ((a-c):+(b-d))

67 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))

68 fromInteger x = (fromInteger x:+0)

69 abs (a:+b) = (magnitude (a:+b):+0)

libs/base/Data/Erased.idrnew file+29

@@ -0,0 +1,29 @@

1+module Data.Erased

2+

3+%access public

4+%default total

5+

6+||| The erasure monad.

7+|||

8+||| Used when explicit modelling of erasure in the type system is needed.

9+data Erased : Type -> Type where

10+

11+ ||| Construct an erased value from any value.

12+ Erase : .(x : a) -> Erased a

13+

14+instance Functor Erased where

15+ map f (Erase x) = Erase (f x)

16+

17+instance Applicative Erased where

18+ pure = Erase

19+ (<$>) (Erase f) (Erase x) = Erase (f x)

20+

21+instance Monad Erased where

22+ (>>=) (Erase x) f = f x

23+

24+||| Project the erased value out of the monad.

25+|||

26+||| This is usable only in types and other erased contexts,

27+||| where it won't cause erasure violations.

28+unerase : Erased a -> a

29+unerase (Erase x) = x

libs/base/base.ipkg+1−1

@@ -22,7 +22,7 @@ modules = System,

22 Data.SortedMap, Data.SortedSet, Data.BoundedList,

23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

25− Data.Rel, Data.Buffer,

25+ Data.Rel, Data.Buffer, Data.Erased,

26

27 Control.Isomorphism, Control.Isomorphism.Primitives,

28 Control.Monad.Identity,

libs/effects/Effect/Random.idr+15−1

@@ -16,18 +16,32 @@ using (m : Type -> Type)

16RND : EFFECT

17RND = MkEff Integer Random

18

19+||| Generates a random Integer in a given range

19rndInt : Integer -> Integer -> { [RND] } Eff m Integer

20rndInt : Integer -> Integer -> { [RND] } Eff m Integer

20rndInt lower upper = do v <- getRandom

21rndInt lower upper = do v <- getRandom

21 return (v `prim__sremBigInt` (upper - lower) + lower)

22 return (v `prim__sremBigInt` (upper - lower) + lower)

22

23

24+||| Generate a random number in Fin (S `k`)

25+|||

26+||| Note that rndFin k takes values 0, 1, ..., k.

23rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

27rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

24−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)

28+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))

25 return (toFin v)

29 return (toFin v)

26 where toFin : Integer -> Fin (S k)

30 where toFin : Integer -> Fin (S k)

27 toFin x = case integerToFin x (S k) of

31 toFin x = case integerToFin x (S k) of

28 Just v => v

32 Just v => v

29 Nothing => toFin (assert_smaller x (x - cast (S k)))

33 Nothing => toFin (assert_smaller x (x - cast (S k)))

30

34

35+||| Select a random element from a vector

36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a

37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)

38+

39+||| Select a random element from a list, or Nothing if the list is empty

40+rndSelect : List a -> { [RND] } Eff IO (Maybe a)

41+rndSelect [] = return Nothing

42+rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

43+

44+||| Sets the random seed

31srand : Integer -> { [RND] } Eff m ()

45srand : Integer -> { [RND] } Eff m ()

32srand n = setSeed n

46srand n = setSeed n

33

47

libs/javascript/JavaScript.idrdeleted−104

@@ -1,104 +0,0 @@

1−module JavaScript

2−

3−%access public

4−

5−private

6−isUndefined : Ptr -> IO Bool

7−isUndefined p = do

8− res <- mkForeign (

9− FFun "%0 === undefined" [FPtr] FString) p

10− if res == "false"

11− then (return False)

12− else (return True)

13−

14−--------------------------------------------------------------------------------

15−-- Events

16−--------------------------------------------------------------------------------

17−abstract

18−data Event : Type where

19− MkEvent : Ptr -> Event

20−

21−--------------------------------------------------------------------------------

22−-- Elements

23−--------------------------------------------------------------------------------

24−abstract

25−data Element : Type where

26− MkElem : Ptr -> Element

27−

28−setText : Element -> String -> IO ()

29−setText (MkElem p) s =

30− mkForeign (FFun "%0.textContent=%1" [FPtr, FString] FUnit) p s

31−

32−

33−setOnClick : Element -> (Event -> IO Bool) -> IO ()

34−setOnClick (MkElem e) f =

35− mkForeign (

36− FFun "%0['onclick']=%1" [ FPtr

37− , FFunction (FAny Event) (FAny (IO Bool))

38− ] FUnit) e f

39−--------------------------------------------------------------------------------

40−-- Nodelists

41−--------------------------------------------------------------------------------

42−abstract

43−data NodeList : Type where

44− MkNodeList : Ptr -> NodeList

45−

46−elemAt : NodeList -> Nat -> IO (Maybe Element)

47−elemAt (MkNodeList p) i = do

48− e <- mkForeign (FFun "%0.item(%1)" [FPtr, FInt] FPtr) p (

49− prim__truncBigInt_Int (cast i)

50− )

51− d <- isUndefined e

52− if d

53− then return $ Just (MkElem e)

54− else return Nothing

55−

56−--------------------------------------------------------------------------------

57−-- Intervals

58−--------------------------------------------------------------------------------

59−abstract

60−data Interval : Type where

61− MkInterval : Ptr -> Interval

62−

63−setInterval : (() -> IO ()) -> Float -> IO Interval

64−setInterval f t = do

65− e <- mkForeign (

66− FFun "setInterval(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr

67− ) f t

68− return (MkInterval e)

69−

70−clearInterval : Interval -> IO ()

71−clearInterval (MkInterval p) =

72− mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p

73−

74−--------------------------------------------------------------------------------

75−-- Timeouts

76−--------------------------------------------------------------------------------

77−data Timeout : Type where

78− MkTimeout : Ptr -> Timeout

79−

80−setTimeout : (() -> IO ()) -> Float -> IO Timeout

81−setTimeout f t = do

82− e <- mkForeign (

83− FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr

84− ) f t

85− return (MkTimeout e)

86−

87−clearTimeout : Timeout -> IO ()

88−clearTimeout (MkTimeout p) =

89− mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p

90−

91−--------------------------------------------------------------------------------

92−-- Basic IO

93−--------------------------------------------------------------------------------

94−alert : String -> IO ()

95−alert msg =

96− mkForeign (FFun "alert(%0)" [FString] FUnit) msg

97−

98−--------------------------------------------------------------------------------

99−-- DOM

100−--------------------------------------------------------------------------------

101−query : String -> IO NodeList

102−query q = do

103− e <- mkForeign (FFun "document.querySelectorAll(%0)" [FString] FPtr) q

104− return (MkNodeList e)

libs/javascript/JavaScript/JSON.idrdeleted−44

@@ -1,44 +0,0 @@

1−module JSON

2−

3−import Data.SortedMap

4−

5−data JSONType : Type where

6− JSONArray : (n : Nat) -> Vect n JSONType -> JSONType

7− JSONString : JSONType

8− JSONNumber : JSONType

9− JSONBool : JSONType

10− JSONObject : SortedMap String JSONType -> JSONType

11− JSONNull : JSONType

12−

13−mutual

14− using (ts : Vect n JSONType, fs : SortedMap String JSONType)

15− namespace JArray

16− data JArray : (n : Nat) -> Vect n JSONType -> Type where

17− Nil : JArray 0 []

18− (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)

19−

20− namespace JObject

21− data JObject : SortedMap String JSONType -> Type where

22− Nil : JObject empty

23− (::) : (f : (String, JSON t)) ->

24− JObject fs ->

25− JObject (insert (fst f) t fs)

26−

27− data JSON : JSONType -> Type where

28− JSString : String -> JSON JSONString

29− JSNumber : Float -> JSON JSONNumber

30− JSBool : Bool -> JSON JSONBool

31− JSNull : JSON JSONNull

32− JSArray : JArray n ts -> JSON (JSONArray n ts)

33− JSObject : JObject fs -> JSON (JSONObject fs)

34−

35−index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)

36−index fZ (JSArray (x :: xs)) = x

37−index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)

38−

39−(++) : JSON (JSONArray m ts1) ->

40− JSON (JSONArray n ts2) ->

41− JSON (JSONArray (m + n) (ts1 ++ ts2))

42−(++) (JSArray []) ys = ys

43−(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)

44− | (JSArray as) = JSArray (x :: as)

libs/javascript/Makefiledeleted−14

@@ -1,14 +0,0 @@

1−IDRIS := idris

2−

3−build:

4− $(IDRIS) --build javascript.ipkg

5−

6−install:

7− $(IDRIS) --install javascript.ipkg

8−

9−clean:

10− $(IDRIS) --clean javascript.ipkg

11−

12−rebuild: clean build

13−

14−.PHONY: build install clean rebuild

libs/javascript/javascript.ipkgdeleted−5

@@ -1,5 +0,0 @@

1−package javascript

2−

3−opts = "--nobasepkgs -i ../prelude -i ../base"

4−modules = JavaScript, JavaScript.JSON

5−

src/IRTS/Compiler.hs+126−47

@@ -262,20 +262,67 @@ irTerm vs env tm@(App f a) = case unApply tm of

262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'

263 ])

264

265+ -- data constructor

265 (P (DCon t arity) n _, args) -> do

266 (P (DCon t arity) n _, args) -> do

266 detag <- fgetState (opt_detaggable . ist_optimisation n)

267 detag <- fgetState (opt_detaggable . ist_optimisation n)

267 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

268 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

268

269

269− when (length args > arity) $

270+ let isNewtype = length used == 1 && detag

270− ifail ("oversaturated data ctor: " ++ show tm)

271−

272− let args' = [a | (i,a) <- zip [0..] args, i `elem` used]

271+ let argsPruned = [a | (i,a) <- zip [0..] args, i `elem` used]

273− if length args' == 1 && detag -- detaggable

272+

273+ -- The following code removes fields from data constructors

274+ -- and performs the newtype optimisation.

275+ --

276+ -- The general rule here is:

277+ -- Everything we get as input is not touched by erasure,

278+ -- so it conforms to the official arities and types

279+ -- and we can reason about it like it's plain TT.

280+ --

281+ -- It's only the data that leaves this point that's erased

282+ -- and possibly no longer typed as the original TT version.

283+ --

284+ -- Especially, underapplied constructors must yield functions

285+ -- even if all the remaining arguments are erased

286+ -- (the resulting function *will* be applied, to NULLs).

287+ --

288+ -- This will probably need rethinking when we get erasure from functions.

289+

290+ -- "padLams" will wrap our term in LLam-bdas and give us

291+ -- the "list of future unerased args" coming from these lambdas.

292+ --

293+ -- We can do whatever we like with the list of unerased args,

294+ -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.

295+ let padLams = padLambdas used (length args) arity

296+

297+ case compare arity (length args) of

298+

299+ -- overapplied

300+ GT -> ifail ("overapplied data constructor: " ++ show tm)

301+

302+ -- exactly saturated

303+ EQ | isNewtype

274− then irTerm vs env (head args') -- newtype

304+ -> irTerm vs env (head argsPruned)

275− else irCon vs env (length used) n args'

305+

276−

306+ | otherwise -- not newtype, plain data ctor

307+ -> buildApp (LV $ Glob n) argsPruned

308+

309+ -- not saturated, underapplied

310+ LT | isNewtype -- newtype

311+ , length argsPruned == 1 -- and we already have the value

312+ -> padLams . (\tm [] -> tm) -- the [] asserts there are no unerased args

313+ <$> irTerm vs env (head argsPruned)

314+

315+ | isNewtype -- newtype but the value is not among args yet

316+ -> return . padLams $ \[vn] -> LApp False (LV $ Glob n) [LV $ Glob vn]

317+

318+ -- not a newtype, just apply to a constructor

319+ | otherwise

320+ -> padLams . applyToNames <$> buildApp (LV $ Glob n) argsPruned

321+

322+ -- type constructor

277 (P (TCon t a) n _, args) -> return LNothing

323 (P (TCon t a) n _, args) -> return LNothing

278

324

325+ -- a name applied to arguments

279 (P _ n _, args) -> do

326 (P _ n _, args) -> do

280 ist <- getIState

327 ist <- getIState

281 case lookup n (idris_scprims ist) of

328 case lookup n (idris_scprims ist) of

@@ -296,29 +343,44 @@ irTerm vs env tm@(App f a) = case unApply tm of

296 <*> mapM (irTerm vs env) args

343 <*> mapM (irTerm vs env) args

297

344

298 where

345 where

346+ buildApp :: LExp -> [Term] -> Idris LExp

347+ buildApp e [] = return e

348+ buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs

349+

350+ applyToNames :: LExp -> [Name] -> LExp

351+ applyToNames tm [] = tm

352+ applyToNames tm ns = LApp False tm $ map (LV . Glob) ns

353+

354+ padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp

355+ padLambdas used startIdx endSIdx mkTerm

356+ = LLam allNames $ mkTerm nonerasedNames

357+ where

358+ allNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1]]

359+ nonerasedNames = [sMN i "sat" | i <- [startIdx .. endSIdx-1], i `elem` used]

360+

299 applyName :: Name -> IState -> [Term] -> Idris LExp

361 applyName :: Name -> IState -> [Term] -> Idris LExp

300 applyName n ist args =

362 applyName n ist args =

301 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)

363 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)

302− where

364+ where

303− erase (i, x)

365+ erase (i, x)

304− | i >= arity || i `elem` used = x

366+ | i >= arity || i `elem` used = x

305− | otherwise = Erased

367+ | otherwise = Erased

306−

368+

307− arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of

369+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of

308− Just (CaseOp ci ty tys def tot cdefs) -> length tys

370+ Just (CaseOp ci ty tys def tot cdefs) -> length tys

309− Just (TyDecl (DCon tag ar) _) -> ar

371+ Just (TyDecl (DCon tag ar) _) -> ar

310− Just (TyDecl Ref ty) -> length $ getArgTys ty

372+ Just (TyDecl Ref ty) -> length $ getArgTys ty

311− Just (Operator ty ar op) -> ar

373+ Just (Operator ty ar op) -> ar

312− Just def -> error $ "unknown arity: " ++ show (n, def)

374+ Just def -> error $ "unknown arity: " ++ show (n, def)

313− Nothing -> 0 -- no definition, probably local name => can't erase anything

375+ Nothing -> 0 -- no definition, probably local name => can't erase anything

314−

376+

315− -- name for purposes of usage info lookup

377+ -- name for purposes of usage info lookup

316− uName

378+ uName

317− | Just n' <- viMethod =<< M.lookup n vs = n'

379+ | Just n' <- viMethod =<< M.lookup n vs = n'

318− | otherwise = n

380+ | otherwise = n

319−

381+

320− used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

382+ used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)

321− fst4 (x,_,_,_) = x

383+ fst4 (x,_,_,_) = x

322

384

323irTerm vs env (P _ n _) = return $ LV (Glob n)

385irTerm vs env (P _ n _) = return $ LV (Glob n)

324irTerm vs env (V i)

386irTerm vs env (V i)

@@ -345,24 +407,6 @@ irTerm vs env (TType _) = return $ LNothing

345irTerm vs env Erased = return $ LNothing

407irTerm vs env Erased = return $ LNothing

346irTerm vs env Impossible = return $ LNothing

408irTerm vs env Impossible = return $ LNothing

347

409

348−irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp

349−irCon vs env arity n args

350− | length args > arity

351− = error $ "oversaturated data constructor: " ++ show (n, args)

352−

353− -- saturated

354− | length args == arity

355− = buildApp (LV (Glob n)) args

356−

357− -- undersaturated, wrap in lambdas

358− | otherwise

359− = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]

360− extraTs = [P Bound n undefined | n <- extraNs]

361− in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)

362− where

363− buildApp e [] = return e

364− buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs

365−

366doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp

410doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp

367doForeign vs env (_ : fgn : args)

411doForeign vs env (_ : fgn : args)

368 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

412 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

@@ -470,6 +514,7 @@ irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

470--

514--

471-- Hence, we check whether the variables are used at all

515-- Hence, we check whether the variables are used at all

472-- and erase the casesplit if they are not.

516-- and erase the casesplit if they are not.

517+--

473irSC vs (Case n [alt]) = do

518irSC vs (Case n [alt]) = do

474 replacement <- case alt of

519 replacement <- case alt of

475 ConCase cn a ns sc -> do

520 ConCase cn a ns sc -> do

@@ -498,7 +543,41 @@ irSC vs (Case n [alt]) = do

498 subexpr (LConstCase _ e) = e

543 subexpr (LConstCase _ e) = e

499 subexpr (LDefaultCase e) = e

544 subexpr (LDefaultCase e) = e

500

545

546+-- FIXME: When we have a non-singleton case-tree of the form

547+--

548+-- case {e0} of

549+-- C(x) => ...

550+-- ... => ...

551+--

552+-- and C is detaggable (the only constructor of the family), we can be sure

553+-- that the first branch will be always taken -- so we add special handling

554+-- to remove the dead default branch.

555+--

556+-- If we don't do so and C is newtype-optimisable, we will miss this newtype

557+-- transformation and the resulting code will probably segfault.

558+--

559+-- This work-around is not entirely optimal; the best approach would be

560+-- to ensure that such case trees don't arise in the first place.

561+--

562+irSC vs (Case n alts@[ConCase cn a ns sc, DefaultCase sc']) = do

563+ detag <- fgetState (opt_detaggable . ist_optimisation cn)

564+ if detag

565+ then irSC vs (Case n [ConCase cn a ns sc])

501−irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

566+ else LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

567+

568+irSC vs sc@(Case n alts) = do

569+ -- check that neither alternative needs the newtype optimisation,

570+ -- see comment above

571+ goneWrong <- or <$> mapM isDetaggable alts

572+ when goneWrong

573+ $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

574+

575+ -- everything okay

576+ LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts

577+ where

578+ isDetaggable (ConCase cn _ _ _) = fgetState $ opt_detaggable . ist_optimisation cn

579+ isDetaggable _ = return False

580+

502irSC vs ImpossibleCase = return LNothing

581irSC vs ImpossibleCase = return LNothing

503

582

504irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

583irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt

src/Idris/CaseSplit.hs+7−4

@@ -361,16 +361,19 @@ getProofClause l fn fp

361

362mkWith :: String -> Name -> String

363mkWith str n = let str' = replaceRHS str "with (_)"

364− newpat = " " ++

365− replaceRHS str "| with_pat = ?" ++ show n ++ "_rhs" in

366− str' ++ "\n" ++ newpat

364+ in str' ++ "\n" ++ newpat str

367

365

368 where replaceRHS [] str = str

366 where replaceRHS [] str = str

369 replaceRHS ('?':'=': rest) str = str

367 replaceRHS ('?':'=': rest) str = str

370− replaceRHS ('=': rest) str

368+ replaceRHS ('=': rest) str

371 | not ('=' `elem` rest) = str

369 | not ('=' `elem` rest) = str

372 replaceRHS (x : rest) str = x : replaceRHS rest str

370 replaceRHS (x : rest) str = x : replaceRHS rest str

373

371

372+ newpat ('>':patstr) = '>':newpat patstr

373+ newpat patstr =

374+ " " ++

375+ replaceRHS patstr "| with_pat = ?" ++ show n ++ "_rhs"

376+

374-- Replace _ with names in missing clauses

377-- Replace _ with names in missing clauses

375

378

376nameMissing :: [PTerm] -> Idris [PTerm]

379nameMissing :: [PTerm] -> Idris [PTerm]

src/Idris/Core/Elaborate.hs+1

@@ -646,6 +646,7 @@ no_errors tac err

646 Error _ -> lift $ Error e

647 OK (a, s') -> do put s'

648 return a

649+ unifyProblems

649 ps' <- get_probs

650 ps' <- get_probs

650 if (length ps' > length ps) then

651 if (length ps' > length ps) then

651 case reverse ps' of

652 case reverse ps' of

src/Idris/Core/ProofState.hs+3−2

@@ -817,8 +817,9 @@ mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)

817mergeNotunified env ns = mnu ns [] [] where

818 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)

819 mnu ((n, t):ns) ns_acc ps_acc

820− | Just t' <- lookup n ns = mnu ns ((n,t) : ns_acc)

820+ | Just t' <- lookup n ns, t /= t'

821+ = mnu ns ((n,t') : ns_acc)

821− ((t,t',env,Msg "", [],Match) : ps_acc)

822+ ((t,t',env,Msg "", [],Unify) : ps_acc)

822 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

823 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc

823

824

824updateNotunified [] nu = nu

825updateNotunified [] nu = nu

src/Idris/ElabTerm.hs+2−2

@@ -1187,8 +1187,8 @@ reifyApp _ t [x]

1187reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)

1188reifyApp ist t [Constant (Str n), x]

1189 | t == reflm "GoalType" = liftM (GoalType n) (reify ist x)

1190−reifyApp _ t [Constant (Str n)]

1190+reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)

1191− | t == reflm "Intro" = return $ Intro [sUN n]

1191+reifyApp _ t [n] | t == reflm "Induction" = liftM Induction (reifyTTName n)

1192reifyApp ist t [t']

1193 | t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')

1194reifyApp ist t [t']

src/Idris/ParseExpr.hs+45−33

@@ -54,14 +54,22 @@ fullExpr syn = do x <- expr syn

54 return $ debindApp syn (desugar syn i x)

55

56

57−{- |Parses an expression

57+{- | Parses an expression

58@

59− Expr ::= Expr';

59+ Expr ::= Pi

60@

61−-}

61+ -}

62expr :: SyntaxInfo -> IdrisParser PTerm

63+expr = pi

64+

65+{- | Parses an expression with possible operator applied

66+@

67+ OpExpr ::= {- Expression Parser with Operators based on Expr' -};

68+@

69+-}

70+opExpr :: SyntaxInfo -> IdrisParser PTerm

63−expr syn = do i <- get

71+opExpr syn = do i <- get

64− buildExpressionParser (table (idris_infixes i)) (expr' syn)

72+ buildExpressionParser (table (idris_infixes i)) (expr' syn)

65

73

66{- | Parses either an internally defined expression or

74{- | Parses either an internally defined expression or

67 a user-defined one

75 a user-defined one

@@ -70,16 +78,10 @@ Expr' ::= "External (User-defined) Syntax"

70 | InternalExpr;

78 | InternalExpr;

71@

79@

72 -}

80 -}

73−expr' syn = doexpr' syn

74−-- = do l <- restOfLine

75−-- f <- getFC

76−-- e <- trace (show (f, l)) $ doexpr' syn

77−-- return e

78−

79−doexpr' :: SyntaxInfo -> IdrisParser PTerm

81+expr' :: SyntaxInfo -> IdrisParser PTerm

80−doexpr' syn = try (externalExpr syn)

82+expr' syn = try (externalExpr syn)

81− <|> internalExpr syn

83+ <|> internalExpr syn

82− <?> "expression"

84+ <?> "expression"

83

85

84{- | Parses a user-defined expression -}

86{- | Parses a user-defined expression -}

85externalExpr :: SyntaxInfo -> IdrisParser PTerm

87externalExpr :: SyntaxInfo -> IdrisParser PTerm

@@ -197,7 +199,6 @@ InternalExpr ::=

197 | QuoteGoal

199 | QuoteGoal

198 | Let

200 | Let

199 | RewriteTerm

201 | RewriteTerm

200− | Pi

201 | CaseExpr

202 | CaseExpr

202 | DoBlock

203 | DoBlock

203 | App

204 | App

@@ -214,7 +215,6 @@ internalExpr syn =

214 <|> quoteGoal syn

215 <|> quoteGoal syn

215 <|> let_ syn

216 <|> let_ syn

216 <|> rewriteTerm syn

217 <|> rewriteTerm syn

217− <|> try (pi syn)

218 <|> doBlock syn

219 <|> caseExpr syn

220 <|> app syn

@@ -363,7 +363,7 @@ bracketed' syn =

363 return (PDPair fc TypeOrTerm (PRef fc ln) lty r))

364 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

365 -- No prefix operators! (bit of a hack here...)

366− if (o == "-" || o == "!")

366+ if (o == "-" || o == "!")

367 then fail "minus not allowed in section"

368 else return $ PLam (sMN 1000 "ARG") Placeholder

369 (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

@@ -754,11 +754,16 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;

754{- | Parses a dependent type signature

755

756@

757−Pi ::=

757+Pi ::= PiOpts Static? Pi'

758− '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

758+@

759− | '|'? Static? '{' TypeDeclList '}' '->' Expr

759+

760+@

761+Pi' ::=

762+ OpExpr ('->' Pi)?

763+ | '(' TypeDeclList ')' '->' Pi

764+ | '{' TypeDeclList '}' '->' Pi

760− | '{' 'auto' TypeDeclList '}' '->' Expr

765+ | '{' 'auto' TypeDeclList '}' '->' Pi

761− | '{' 'default' TypeDeclList '}' '->' Expr

766+ | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi

762 ;

767 ;

763@

768@

764 -}

769 -}

@@ -767,37 +772,44 @@ pi :: SyntaxInfo -> IdrisParser PTerm

767pi syn =

772pi syn =

768 do opts <- piOpts syn

773 do opts <- piOpts syn

769 st <- static

774 st <- static

770− (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

775+ (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

771 symbol "->"

776 symbol "->"

772 sc <- expr syn

777 sc <- expr syn

773 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

778 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

774− lchar '{'

775− (do reserved "auto"

779+ (do try (lchar '{' *> reserved "auto")

776 when (st == Static) $ fail "auto type constraints can not be lazy or static"

780 when (st == Static) $ fail "auto type constraints can not be lazy or static"

777 xt <- typeDeclList syn

781 xt <- typeDeclList syn

778 lchar '}'

782 lchar '}'

779 symbol "->"

783 symbol "->"

780 sc <- expr syn

784 sc <- expr syn

781 return (bindList (PPi

785 return (bindList (PPi

782− (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

786+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc)) <|> (do

783− <|> (do

784− reserved "default"

787+ try (lchar '{' *> reserved "default")

785 when (st == Static) $ fail "default tactic constraints can not be lazy or static"

788 when (st == Static) $ fail "default tactic constraints can not be lazy or static"

786 script <- simpleExpr syn

789 script <- simpleExpr syn

787 xt <- typeDeclList syn

790 xt <- typeDeclList syn

788 lchar '}'

791 lchar '}'

789 symbol "->"

792 symbol "->"

790 sc <- expr syn

793 sc <- expr syn

791− return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

794+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

792 <|> (if implicitAllowed syn then do

795 <|> (if implicitAllowed syn then do

793− xt <- typeDeclList syn

796+ xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

794− lchar '}'

795 symbol "->"

797 symbol "->"

796 sc <- expr syn

798 sc <- expr syn

797 return (bindList (PPi (Imp opts st False)) xt sc)

799 return (bindList (PPi (Imp opts st False)) xt sc)

798 else do fail "no implicit arguments allowed here"))

800 else do fail "no implicit arguments allowed here"))

801+ <|> (do x <- opExpr syn

802+ (do symbol "->"

803+ sc <- expr syn

804+ return (PPi (Exp opts st False) (sUN "__pi_arg") x sc))

805+ <|> return x)

799 <?> "dependent type signature"

806 <?> "dependent type signature"

800

807

808+{- | Parses Possible Options for Pi Expressions

809+@

810+ PiOpts ::= '.'?

811+@

812+-}

801piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

813piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

802piOpts syn | implicitAllowed syn =

814piOpts syn | implicitAllowed syn =

803 lchar '.' *> return [InaccessibleArg]

815 lchar '.' *> return [InaccessibleArg]

@@ -1079,7 +1091,7 @@ Static ::=

1079@

1091@

1080-}

1092-}

1081static :: IdrisParser Static

1093static :: IdrisParser Static

1082−static = do lchar '['; reserved "static"; lchar ']'; return Static

1094+static = do reserved "[static]"; return Static

1083 <|> return Dynamic

1095 <|> return Dynamic

1084 <?> "static modifier"

1096 <?> "static modifier"

1085

1097

src/Idris/ParseOps.hs+1−2

@@ -38,8 +38,7 @@ table fixes

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft],

41+ [binary "=" PEq AssocLeft]]

42− [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43 where

42 where

44 flatten :: PTerm -> PTerm -- flatten application

43 flatten :: PTerm -> PTerm -- flatten application

45 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

src/Idris/Prover.hs+1

@@ -85,6 +85,7 @@ prove opt ctxt lit n ty

85 [([], P Ref n ty, ptm)]

86 [([], P Ref n ty, ptm')] ty)

87 solveDeferred n

88+

88elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

89elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

89elabStep st e = case runStateT eCheck st of

90elabStep st e = case runStateT eCheck st of

90 OK (a, st') -> return (a, st')

91 OK (a, st') -> return (a, st')

src/Idris/REPL.hs+5−4

@@ -900,14 +900,15 @@ process h fn (RmProof n')

900

901process h fn' (AddProof prf)

902 = do fn <- do

903+ let fn'' = takeWhile (/= ' ') fn'

903− ex <- runIO $ doesFileExist fn'

904+ ex <- runIO $ doesFileExist fn''

904− let fnExt = fn' <.> "idr"

905+ let fnExt = fn'' <.> "idr"

905 exExt <- runIO $ doesFileExist fnExt

906 exExt <- runIO $ doesFileExist fnExt

906 if ex

907 if ex

907− then return fn'

908+ then return fn''

908 else if exExt

909 else if exExt

909 then return fnExt

910 then return fnExt

910− else ifail $ "Neither \""++fn'++"\" nor \""++fnExt++"\" exist"

911+ else ifail $ "Neither \""++fn''++"\" nor \""++fnExt++"\" exist"

911 let fb = fn ++ "~"

912 let fb = fn ++ "~"

912 runIO $ copyFile fn fb -- make a backup in case something goes wrong!

913 runIO $ copyFile fn fb -- make a backup in case something goes wrong!

913 prog <- runIO $ readFile fb

914 prog <- runIO $ readFile fb

test/reg042/expectednew file+1

@@ -0,0 +1 @@

1+7

test/reg042/reg042.idrnew file+24

@@ -0,0 +1,24 @@

1+-- This regtest tests for incorrect erasure from underapplied data constructors.

2+

3+data T : Type where

4+ C : Nat -> Nat -> Nat -> T

5+

6+data Q : Type where

7+ D : (Nat -> T) -> Q

8+

9+-- The bug was here: (C 3 4) would compile to plain data,

10+-- not to a function that would expect another (albeit erased) argument.

11+f : Q

12+f = D (C 3 4)

13+

14+proj : Nat -> Q -> Nat -> T

15+proj Z (D f) = f

16+proj (S n) q = proj n q

17+

18+g : T -> Nat

19+g (C x y z) = x + y

20+

21+-- Here, we'd apply the not-a-function to the erased argument 4,

22+-- which would make the program go wrong.

23+main : IO ()

24+main = print $ g (proj 3 f 4)

test/reg042/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ reg042 -o reg042 --warnreach

3+./reg042

4+rm -f reg042 *.ibc