69f73f8 · Idris-dev · git.iko.soy

idris.cabal+2−2

compare with master

unifiedsplit

@@ -14,7 +14,7 @@ Description: Idris is a general purpose language with full dependent types.

14 Dependent types allow types to be predicated on values,

15 meaning that some aspects of a program's behaviour can be

16 specified precisely in the type. The language is closely

17− related to Epigram and Agda. There is a tutorial at

17+ related to Epigram and Agda. There is a tutorial at

18 <http://www.idris-lang.org/documentation>.

19 Features include:

20 .

@@ -462,7 +462,7 @@ Library

462 if os(freebsd)

463 cpp-options: -DFREEBSD

464 build-depends: unix

465− if os(dragonfly)

465+ if os(dragonfly)

466 cpp-options: -DDRAGONFLY

467 build-depends: unix

468 if os(darwin)

libs/prelude/Prelude.idr+3−3

@@ -334,7 +334,7 @@ instance Traversable (Vect n) where

334 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

335

336---- some mathematical operations

337−---- XXX this should probably go some place else,

337+---- XXX this should probably go some place else,

338pow : (Num a) => a -> Nat -> a

339pow x Z = 1

340pow x (S n) = x * (pow x n)

@@ -376,7 +376,7 @@ instance Enum Integer where

376 enumFromThen n inc = n :: enumFromThen (inc + n) inc

377 enumFromTo n m = if n <= m

378 then go (natRange (S (cast {to = Nat} (m - n))))

379− else []

379+ else []

380 where go : List Nat -> List Integer

381 go [] = []

382 go (x :: xs) = n + cast x :: go xs

@@ -392,7 +392,7 @@ instance Enum Int where

392 toNat n = cast n

393 fromNat n = cast n

394 enumFromThen n inc = n :: enumFromThen (inc + n) inc

395− enumFromTo n m = if n <= m

395+ enumFromTo n m = if n <= m

396 then go (natRange (S (cast {to = Nat} (m - n))))

397 else []

398 where go : List Nat -> List Int

src/IRTS/CodegenC.hs+18−1

@@ -10,6 +10,7 @@ import Idris.Core.TT

10import Paths_idris

11import Util.System

12

13+import Numeric

13import Data.Char

14import Data.Char

14import Data.List (intercalate)

15import Data.List (intercalate)

15import System.Process

16import System.Process

@@ -104,6 +105,22 @@ toC f code

104 indent 1 ++ "INITFRAME;\n" ++

105 indent 1 ++ "INITFRAME;\n" ++

105 concatMap (bcc 1) code ++ "}\n\n"

106 concatMap (bcc 1) code ++ "}\n\n"

106

107

108+showCStr :: String -> String

109+showCStr s = '"' : foldr ((++) . showChar) "\"" s

110+ where

111+ showChar :: Char -> String

112+ showChar '"' = "\\\""

113+ showChar '\\' = "\\\\"

114+ showChar c

115+ -- Note: we need the double quotes around the codes because otherwise

116+ -- "\n3" would get encoded as "\x0a3", which is incorrect.

117+ -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.

118+ | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""

119+ | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""

120+ | ord c < 0x7f = [c] -- 0x7f = \DEL

121+ | ord c < 0x100 = "\"\"\\x" ++ showHex (ord c) "\"\""

122+ | otherwise = error $ "non-8-bit character in string literal: " ++ show c

123+

107bcc :: Int -> BC -> String

124bcc :: Int -> BC -> String

108bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

125bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

109bcc i (ASSIGNCONST l c)

126bcc i (ASSIGNCONST l c)

@@ -114,7 +131,7 @@ bcc i (ASSIGNCONST l c)

114 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"

131 | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"

115 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

132 mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"

116 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

133 mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"

117− mkConst (Str s) = "MKSTR(vm, " ++ show s ++ ")"

134+ mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"

118 mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ ")"

135 mkConst (B8 x) = "idris_b8const(vm, " ++ show x ++ ")"

119 mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ ")"

136 mkConst (B16 x) = "idris_b16const(vm, " ++ show x ++ ")"

120 mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ ")"

137 mkConst (B32 x) = "idris_b32const(vm, " ++ show x ++ ")"

src/IRTS/CodegenJavaScript.hs+69−10

@@ -64,6 +64,7 @@ data JS = JSRaw String

64 | JSArray [JS]

65 | JSObject [(String, JS)]

66 | JSString String

67+ | JSChar String

67 | JSNum JSNum

68 | JSNum JSNum

68 | JSAssign JS JS

69 | JSAssign JS JS

69 | JSAlloc String (Maybe JS)

70 | JSAlloc String (Maybe JS)

@@ -153,6 +154,9 @@ compileJS (JSObject fields) =

153compileJS (JSString str) =

154compileJS (JSString str) =

154 show str

155 show str

155

156

157+compileJS (JSChar chr) =

158+ chr

159+

156compileJS (JSNum num)

160compileJS (JSNum num)

157 | JSInt i <- num = show i

161 | JSInt i <- num = show i

158 | JSFloat f <- num = show f

162 | JSFloat f <- num = show f

@@ -170,8 +174,16 @@ compileJS (JSIndex lhs rhs) =

170 compileJS lhs ++ "[" ++ compileJS rhs ++ "]"

174 compileJS lhs ++ "[" ++ compileJS rhs ++ "]"

171

175

172compileJS (JSCond branches) =

176compileJS (JSCond branches) =

173− intercalate " else " $ map createIfBlock branches

177+ intercalate " else " $ map createIfBlock (eliminateDeadBranches branches)

174 where

178 where

179+ eliminateDeadBranches (e@(JSTrue, _):_) = [e]

180+ eliminateDeadBranches (x:xs) = x : eliminateDeadBranches xs

181+ eliminateDeadBranches [] = []

182+

183+ createIfBlock (JSTrue, e) =

184+ "{\n"

185+ ++ "return " ++ compileJS e

186+ ++ ";\n}"

175 createIfBlock (cond, e) =

187 createIfBlock (cond, e) =

176 "if (" ++ compileJS cond ++") {\n"

188 "if (" ++ compileJS cond ++") {\n"

177 ++ "return " ++ compileJS e

189 ++ "return " ++ compileJS e

@@ -233,6 +245,7 @@ jsLet name value body =

233 )

245 )

234 ) [value]

246 ) [value]

235

247

248+

236jsSubst :: String -> JS -> JS -> JS

249jsSubst :: String -> JS -> JS -> JS

237jsSubst var new (JSVar old)

250jsSubst var new (JSVar old)

238 | var == translateVariableName old = new

251 | var == translateVariableName old = new

@@ -260,6 +273,16 @@ jsSubst var new (JSApp (JSIdent "__IDRRT__tailcall") [JSFunction [] (

260 JSReturn $ JSApp (jsSubst var new fun) (map (jsSubst var new) args)

273 JSReturn $ JSApp (jsSubst var new fun) (map (jsSubst var new) args)

261 )]

274 )]

262

275

276+jsSubst var new (JSApp (JSProj (JSFunction args body) "apply") vals)

277+ | var `notElem` args =

278+ JSApp (JSProj (JSFunction args (jsSubst var new body)) "apply") (

279+ map (jsSubst var new) vals

280+ )

281+ | otherwise =

282+ JSApp (JSProj (JSFunction args body) "apply") (

283+ map (jsSubst var new) vals

284+ )

285+

263jsSubst var new (JSApp (JSProj obj field) args) =

286jsSubst var new (JSApp (JSProj obj field) args) =

264 JSApp (JSProj (jsSubst var new obj) field) $ map (jsSubst var new) args

287 JSApp (JSProj (jsSubst var new obj) field) $ map (jsSubst var new) args

265

288

@@ -293,7 +316,38 @@ jsSubst var new (JSCond conds) =

293

316

294jsSubst _ _ js = js

317jsSubst _ _ js = js

295

318

319+

320+isJSConstant :: JS -> Bool

321+isJSConstant js

322+ | JSString _ <- js = True

323+ | JSChar _ <- js = True

324+ | JSNum _ <- js = True

325+ | JSType _ <- js = True

326+

327+ | JSApp (JSIdent "__IDRRT__bigInt") _ <- js = True

328+ | otherwise = False

329+

296inlineJS :: JS -> JS

330inlineJS :: JS -> JS

331+inlineJS (JSApp (JSProj (JSFunction args (JSReturn body)) "apply") [

332+ JSThis,JSProj (JSIdent var) "vars"

333+ ])

334+ | var /= "cse" =

335+ inlineApply args body 0

336+ where

337+ inlineApply [] body _ = body

338+ inlineApply (a:as) body n =

339+ inlineApply as (

340+ jsSubst a (JSIndex (JSProj (JSIdent var) "vars") (JSNum (JSInt n))) body

341+ ) (n + 1)

342+

343+inlineJS (JSApp (JSIdent "__IDR__mEVAL0") [val])

344+ | isJSConstant val = val

345+

346+inlineJS (JSApp (JSIdent "__IDRRT__tailcall") [

347+ JSFunction [] (JSReturn val)

348+ ])

349+ | isJSConstant val = val

350+

297inlineJS (JSApp (JSFunction [] (JSSeq ret)) []) =

351inlineJS (JSApp (JSFunction [] (JSSeq ret)) []) =

298 JSApp (JSFunction [] (JSSeq (map inlineJS ret))) []

352 JSApp (JSFunction [] (JSSeq (map inlineJS ret))) []

299

353

@@ -365,6 +419,9 @@ inlineJS (JSCond cases) =

365inlineJS (JSObject fields) =

419inlineJS (JSObject fields) =

366 JSObject (map (second inlineJS) fields)

420 JSObject (map (second inlineJS) fields)

367

421

422+inlineJS (JSOp op lhs rhs) =

423+ JSOp op (inlineJS lhs) (inlineJS rhs)

424+

368inlineJS js = js

425inlineJS js = js

369

426

370reduceJS :: [JS] -> [JS]

427reduceJS :: [JS] -> [JS]

@@ -536,6 +593,12 @@ reduceLoop reduced (cons, program) =

536 reduceCall funs (JSProj obj field) =

593 reduceCall funs (JSProj obj field) =

537 JSProj (reduceCall funs obj) field

594 JSProj (reduceCall funs obj) field

538

595

596+ reduceCall funs (JSIndex obj idx) =

597+ JSIndex (reduceCall funs obj) (reduceCall funs idx)

598+

599+ reduceCall funs (JSOp op rhs lhs) =

600+ JSOp op (reduceCall funs rhs) (reduceCall funs lhs)

601+

539 reduceCall funs (JSCond conds) =

602 reduceCall funs (JSCond conds) =

540 JSCond $ map (reduceCall funs *** reduceCall funs) conds

603 JSCond $ map (reduceCall funs *** reduceCall funs) conds

541

604

@@ -699,6 +762,9 @@ translateSpecialName name

699translateConstant :: Const -> JS

762translateConstant :: Const -> JS

700translateConstant (I i) = JSNum (JSInt i)

763translateConstant (I i) = JSNum (JSInt i)

701translateConstant (Fl f) = JSNum (JSFloat f)

764translateConstant (Fl f) = JSNum (JSFloat f)

765+translateConstant (Ch '\DEL') = JSChar "'\\u007F'"

766+translateConstant (Ch '\a') = JSChar "'\\u0007'"

767+translateConstant (Ch '\SO') = JSChar "'\\u000E'"

702translateConstant (Ch c) = JSString [c]

768translateConstant (Ch c) = JSString [c]

703translateConstant (Str s) = JSString s

769translateConstant (Str s) = JSString s

704translateConstant (AType (ATInt ITNative)) = JSType JSIntTy

770translateConstant (AType (ATInt ITNative)) = JSType JSIntTy

@@ -800,23 +866,16 @@ translateDeclaration (path, SFun name params stackSize body)

800 JSFunction (p ++ map snd aux) (

866 JSFunction (p ++ map snd aux) (

801 JSSeq $

867 JSSeq $

802 zipWith assignVar [0..] p ++

868 zipWith assignVar [0..] p ++

803− map allocVar [numP .. (numP + stackSize - 1)] ++

804 map assignAux aux ++

869 map assignAux aux ++

805 [JSReturn body]

870 [JSReturn body]

806 )

871 )

807 where

872 where

808− numP :: Int

809− numP = length params

810−

811− allocVar :: Int -> JS

812− allocVar n = JSAlloc (jsVar n) Nothing

813−

814 assignVar :: Int -> String -> JS

873 assignVar :: Int -> String -> JS

815 assignVar n s = JSAlloc (jsVar n) (Just $ JSIdent s)

874 assignVar n s = JSAlloc (jsVar n) (Just $ JSIdent s)

816

875

817 assignAux :: (LVar, String) -> JS

876 assignAux :: (LVar, String) -> JS

818− assignAux (var, val) =

877+ assignAux (Loc var, val) =

819− JSAssign (JSIdent $ translateVariableName var) (JSIdent val)

878+ JSAlloc (jsVar var) (Just $ JSIdent val)

820

879

821 p :: [String]

880 p :: [String]

822 p = map translateName params

881 p = map translateName params

src/Idris/AbsSyntax.hs+6−6

@@ -698,7 +698,7 @@ inferDecl = PDatadecl inferTy

698 PType

699 [("", inferCon, PPi impl (sMN 0 "iType") PType (

700 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

701− (PRef bi inferTy)), bi)]

701+ (PRef bi inferTy)), bi, [])]

702inferOpts = []

703

704infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

@@ -721,7 +721,7 @@ primNames = [unitTy, unitCon,

721unitTy = sMN 0 "__Unit"

722unitCon = sMN 0 "__II"

723unitDecl = PDatadecl unitTy PType

724− [("", unitCon, PRef bi unitTy, bi)]

724+ [("", unitCon, PRef bi unitTy, bi, [])]

725unitOpts = [DefaultEliminator]

726

727falseTy = sMN 0 "__False"

@@ -736,7 +736,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

736 PPi expl (n "a") (PRef bi (n "A")) (

737 PPi expl (n "b") (PRef bi (n "B"))

738 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

739− pexp (PRef bi (n "B"))])))), bi)]

739+ pexp (PRef bi (n "B"))])))), bi, [])]

740 where n a = sMN 0 a

741pairOpts = []

742

@@ -750,7 +750,7 @@ eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

750 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

751 pimp (n "B") Placeholder False,

752 pexp (PRef bi (n "x")),

753− pexp (PRef bi (n "x"))])), bi)]

753+ pexp (PRef bi (n "x"))])), bi, [])]

754 where n a = sMN 0 a

755eqOpts = []

756

@@ -921,8 +921,8 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

921 then PDatadecl (dec n) (piBind ps (expandParams dec ps ns [] ty))

922 (map econ cons)

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

924− econ (doc, n, t, fc)

924+ econ (doc, n, t, fc, fs)

925− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc)

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

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

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

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

src/Idris/AbsSyntaxTree.hs+5−5

@@ -478,7 +478,7 @@ deriving instance NFData PClause'

478-- | Data declaration

479data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

480 d_tcon :: t, -- ^ Type constructor

481− d_cons :: [(String, Name, t, FC)] -- ^ Constructors

481+ d_cons :: [(String, Name, t, FC, [Name])] -- ^ Constructors

482 }

483 -- ^ Data declaration

484 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -505,7 +505,7 @@ declared (PPostulate _ _ _ _ n t) = [n]

505declared (PClauses _ _ n _) = [] -- not a declaration

506declared (PCAF _ n _) = [n]

507declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

508− where fstt (_, a, _, _) = a

508+ where fstt (_, a, _, _, _) = a

509declared (PData _ _ _ _ (PLaterdecl n _)) = [n]

510declared (PParams _ _ ds) = concatMap declared ds

511declared (PNamespace _ ds) = concatMap declared ds

@@ -525,7 +525,7 @@ tldeclared (PPostulate _ _ _ _ n t) = [n]

525tldeclared (PClauses _ _ n _) = [] -- not a declaration

526tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

527tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

528− where fstt (_, a, _, _) = a

528+ where fstt (_, a, _, _, _) = a

529tldeclared (PParams _ _ ds) = []

530tldeclared (PMutual _ ds) = concatMap tldeclared ds

531tldeclared (PNamespace _ ds) = concatMap tldeclared ds

@@ -540,7 +540,7 @@ defined (PPostulate _ _ _ _ n t) = []

540defined (PClauses _ _ n _) = [n] -- not a declaration

541defined (PCAF _ n _) = [n]

542defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

543− where fstt (_, a, _, _) = a

543+ where fstt (_, a, _, _, _) = a

544defined (PData _ _ _ _ (PLaterdecl n _)) = []

545defined (PParams _ _ ds) = concatMap defined ds

546defined (PNamespace _ ds) = concatMap defined ds

@@ -945,7 +945,7 @@ showDImp :: Bool -> PData -> String

945showDImp impl (PDatadecl n ty cons)

946 = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

947 ++ showSep "\n\t| "

948− (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

948+ (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)

949

950getImps :: [PArg] -> [(Name, PTerm)]

951getImps [] = []

src/Idris/Core/CaseTree.hs+1

@@ -157,6 +157,7 @@ directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

157directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

158directUse fn@(App f a)

159 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

160+ | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

160 | otherwise = nub $ directUse f ++ directUse a

161 | otherwise = nub $ directUse f ++ directUse a

161directUse (Proj x i) = nub $ directUse x

162directUse (Proj x i) = nub $ directUse x

162directUse _ = []

163directUse _ = []

src/Idris/DataOpts.hs+6−3

@@ -18,14 +18,16 @@ type ForceMap = M.IntMap Forceability

18

19-- Calculate the forceable arguments to a constructor

20-- and update the set of optimisations.

21−forceArgs :: Name -> Name -> Type -> Idris ()

21+forceArgs :: Name -> Name -> [Int] -> Type -> Idris ()

22−forceArgs typeName n t = do

22+forceArgs typeName n expforce t = do

23 ist <- getIState

24 let fargs = getForcedArgs ist typeName t

25 copt = case lookupCtxt n (idris_optimisation ist) of

26 [] -> Optimise False False [] []

27 op:_ -> op

28− opts = addDef n (copt { forceable = M.toList fargs }) (idris_optimisation ist)

28+ opts = addDef n (copt { forceable = M.toList fargs ++

29+ zip expforce (repeat Unconditional) })

30+ (idris_optimisation ist)

29 putIState (ist { idris_optimisation = opts })

31 putIState (ist { idris_optimisation = opts })

30 addIBC (IBCOpt n)

32 addIBC (IBCOpt n)

31 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

33 iLOG $ "Forced: " ++ show n ++ " " ++ show fargs ++ "\n from " ++ show t

@@ -319,3 +321,4 @@ applyDataOptRT oi n tag arity args

319 where

321 where

320 ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)

322 ctor' = (P (DCon tag (arity - forcedCnt forceMap)) n Erased)

321 args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]

323 args' = [t | (f, t) <- zip (forcedArgSeq oi) args, f /= Just Unconditional]

324+

src/Idris/ElabDecls.hs+24−15

@@ -304,7 +304,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)

304type EliminatorState = StateT (Map.Map String Int) Idris

305

306-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite

307−elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()

307+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] ->

308+ ElabInfo -> EliminatorState ()

308elabEliminator paramPos n ty cons info = do

309elabEliminator paramPos n ty cons info = do

309 elimLog $ "Elaborating eliminator"

310 elimLog $ "Elaborating eliminator"

310 let (cnstrs, _) = splitPi ty

311 let (cnstrs, _) = splitPi ty

@@ -312,7 +313,7 @@ elabEliminator paramPos n ty cons info = do

312 generalParams <- namePis False pms

313 generalParams <- namePis False pms

313 motiveIdxs <- namePis False idxs

314 motiveIdxs <- namePis False idxs

314 let motive = mkMotive n paramPos generalParams motiveIdxs

315 let motive = mkMotive n paramPos generalParams motiveIdxs

315− consTerms <- mapM (\(c@(_,cnm,_,_)) -> do

316+ consTerms <- mapM (\(c@(_,cnm,_,_,_)) -> do

316 name <- freshName $ "elim_" ++ simpleName cnm

317 name <- freshName $ "elim_" ++ simpleName cnm

317 consTerm <- extractConsTerm c generalParams

318 consTerm <- extractConsTerm c generalParams

318 return (name, expl, consTerm)) cons

319 return (name, expl, consTerm)) cons

@@ -469,8 +470,8 @@ elabEliminator paramPos n ty cons info = do

469 splitArgPms _ = ([],[])

470 splitArgPms _ = ([],[])

470

471

472

472− implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]

473+ implicitIndexes :: (String, Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

473− implicitIndexes (cns@(doc, cnm, ty, fc)) = do

474+ implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

474 i <- State.lift getIState

475 i <- State.lift getIState

475 implargs' <- case lookupCtxt cnm (idris_implicits i) of

476 implargs' <- case lookupCtxt cnm (idris_implicits i) of

476 [] -> do fail $ "Error while showing implicits for " ++ show cnm

477 [] -> do fail $ "Error while showing implicits for " ++ show cnm

@@ -484,11 +485,11 @@ elabEliminator paramPos n ty cons info = do

484 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

485 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

485 _ -> return implargs

486 _ -> return implargs

486

487

487− extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

488+ extractConsTerm :: (String, Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

488− extractConsTerm (doc, cnm, ty, fc) generalParameters = do

489+ extractConsTerm (doc, cnm, ty, fc, fs) generalParameters = do

489 let cons' = replaceParams paramPos generalParameters ty

490 let cons' = replaceParams paramPos generalParameters ty

490 let (args, resTy) = splitPi cons'

491 let (args, resTy) = splitPi cons'

491− implidxs <- implicitIndexes (doc, cnm, ty, fc)

492+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

492 consArgs <- namePis True args

493 consArgs <- namePis True args

493 let recArgs = findRecArgs consArgs

494 let recArgs = findRecArgs consArgs

494 let recMotives = map applyRecMotive recArgs

495 let recMotives = map applyRecMotive recArgs

@@ -520,12 +521,12 @@ elabEliminator paramPos n ty cons info = do

520 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

521 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

521 convertImplPi _ = Nothing

522 convertImplPi _ = Nothing

522

523

523− generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

524+ generateEliminatorClauses :: (String, Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

524− generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do

525+ generateEliminatorClauses (doc, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

525 let cons' = replaceParams paramPos generalParameters ty

526 let cons' = replaceParams paramPos generalParameters ty

526 let (args, resTy) = splitPi cons'

527 let (args, resTy) = splitPi cons'

527 i <- State.lift getIState

528 i <- State.lift getIState

528− implidxs <- implicitIndexes (doc, cnm, ty, fc)

529+ implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

529 let (_, generalIdxs') = splitArgPms resTy

530 let (_, generalIdxs') = splitArgPms resTy

530 let generalIdxs = map pexp generalIdxs'

531 let generalIdxs = map pexp generalIdxs'

531 consArgs <- namePis True args

532 consArgs <- namePis True args

@@ -698,7 +699,7 @@ elabTransform info fc safe lhs_in rhs_in

698elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

699elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

699 PTerm -> String -> Name -> PTerm -> Idris ()

700 PTerm -> String -> Name -> PTerm -> Idris ()

700elabRecord info syn doc fc tyn ty cdoc cn cty

701elabRecord info syn doc fc tyn ty cdoc cn cty

701− = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

702+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc, [])])

702 cty' <- implicit syn cn cty

703 cty' <- implicit syn cn cty

703 i <- getIState

704 i <- getIState

704 cty <- case lookupTy cn (tt_ctxt i) of

705 cty <- case lookupTy cn (tt_ctxt i) of

@@ -805,8 +806,8 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

805 return (pn, pfnTy, PClauses fc [] setname [pclause])

806 return (pn, pfnTy, PClauses fc [] setname [pclause])

806

807

807elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

808elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

808− (String, Name, PTerm, FC) -> Idris (Name, Type)

809+ (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

809−elabCon info syn tn codata (doc, n, t_in, fc)

810+elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

810 = do checkUndefined fc n

811 = do checkUndefined fc n

811 ctxt <- getContext

812 ctxt <- getContext

812 i <- getIState

813 i <- getIState

@@ -829,7 +830,10 @@ elabCon info syn tn codata (doc, n, t_in, fc)

829 addIBC (IBCDef n)

830 addIBC (IBCDef n)

830 addDocStr n doc

831 addDocStr n doc

831 addIBC (IBCDoc n)

832 addIBC (IBCDoc n)

833+ let fs = map (getNamePos 0 t) forcenames

834+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of

835+ -- erasing non-forceable things

832− forceArgs tn n cty'

836+ forceArgs tn n (mapMaybe (getNamePos 0 t) forcenames) cty'

833 return (n, cty')

837 return (n, cty')

834 where

838 where

835 tyIs (Bind n b sc) = tyIs sc

839 tyIs (Bind n b sc) = tyIs sc

@@ -841,6 +845,11 @@ elabCon info syn tn codata (doc, n, t_in, fc)

841 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

845 mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

842 mkLazy t = t

846 mkLazy t = t

843

847

848+ getNamePos :: Int -> PTerm -> Name -> Maybe Int

849+ getNamePos i (PPi _ n _ sc) x | n == x = Just i

850+ | otherwise = getNamePos (i + 1) sc x

851+ getNamePos _ _ _ = Nothing

852+

844-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

853-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

845-- top-level definition.

854-- top-level definition.

846elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

855elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

@@ -1628,7 +1637,7 @@ elabClass info syn doc fc constraints tn ps ds

1628 let cty = impbind ps $ conbind constraints

1637 let cty = impbind ps $ conbind constraints

1629 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1638 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

1630 constraint

1639 constraint

1631− let cons = [("", cn, cty, fc)]

1640+ let cons = [("", cn, cty, fc, [])]

1632 let ddecl = PDatadecl tn tty cons

1641 let ddecl = PDatadecl tn tty cons

1633 logLvl 5 $ "Class data " ++ showDImp True ddecl

1642 logLvl 5 $ "Class data " ++ showDImp True ddecl

1634 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1643 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

src/Idris/ParseData.hs+13−9

@@ -49,7 +49,7 @@ record syn = do (doc, acc) <- try (do

49 ty <- typeExpr (allowImp syn)

50 let tyn = expandNS syn tyn_in

51 reserved "where"

52− (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

52+ (cdoc, cn, cty, _, _) <- indentedBlockS (constructor syn)

53 accData acc tyn [cn]

54 let rsyn = syn { syn_namespace = show (nsroot tyn) :

55 syn_namespace syn }

@@ -113,7 +113,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

113 option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

114 reserved "where"

115 cons <- indentedBlock (constructor syn)

116− accData acc tyn (map (\ (_, n, _, _) -> n) cons)

116+ accData acc tyn (map (\ (_, n, _, _, _) -> n) cons)

117 return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

118 args <- many name

119 let ty = bindArgs (map (const PType) args) PType

@@ -133,10 +133,10 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

133 cons <- sepBy1 (simpleConstructor syn) (lchar '|')

134 terminator

135 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

136− cons' <- mapM (\ (doc, x, cargs, cfc) ->

136+ cons' <- mapM (\ (doc, x, cargs, cfc, fs) ->

137 do let cty = bindArgs cargs conty

138− return (doc, x, cty, cfc)) cons

138+ return (doc, x, cty, cfc, fs)) cons

139− accData acc tyn (map (\ (_, n, _, _) -> n) cons')

139+ accData acc tyn (map (\ (_, n, _, _, _) -> n) cons')

140 return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

141 <?> "data type declaration"

142 where

@@ -152,20 +152,24 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

152{- | Parses a type constructor declaration

153 Constructor ::= DocComment? FnName TypeSig;

154-}

155−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)

155+constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC, [Name])

156constructor syn

157 = do doc <- option "" (docComment '|')

158 cn_in <- fnName; fc <- getFC

159 let cn = expandNS syn cn_in

160 lchar ':'

161+ -- FIXME: 'forcenames' is an almighty hack! Need a better way of

162+ -- erasing non-forceable things

163+ fs <- option [] (do lchar '%'; reserved "erase"

164+ sepBy1 name (lchar ','))

161 ty <- typeExpr (allowImp syn)

165 ty <- typeExpr (allowImp syn)

162− return (doc, cn, ty, fc)

166+ return (doc, cn, ty, fc, fs)

163 <?> "constructor"

167 <?> "constructor"

164

168

165{- | Parses a constructor for simple discriminative union data types

169{- | Parses a constructor for simple discriminative union data types

166 SimpleConstructor ::= FnName SimpleExpr* DocComment?

170 SimpleConstructor ::= FnName SimpleExpr* DocComment?

167-}

171-}

168−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)

172+simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC, [Name])

169simpleConstructor syn

173simpleConstructor syn

170 = do cn_in <- fnName

174 = do cn_in <- fnName

171 let cn = expandNS syn cn_in

175 let cn = expandNS syn cn_in

@@ -173,7 +177,7 @@ simpleConstructor syn

173 args <- many (do notEndApp

177 args <- many (do notEndApp

174 simpleExpr syn)

178 simpleExpr syn)

175 doc <- option "" (docComment '^')

179 doc <- option "" (docComment '^')

176− return (doc, cn, args, fc)

180+ return (doc, cn, args, fc, [])

177 <?> "constructor"

181 <?> "constructor"

178

182

179{- | Parses a dsl block declaration

183{- | Parses a dsl block declaration

src/Idris/ParseExpr.hs+1−1

@@ -580,7 +580,7 @@ implicitArg syn = do lchar '{'

580 v <- option (PRef fc n) (do lchar '='

581 expr syn)

582 lchar '}'

583− return (pimp n v False)

583+ return (pimp n v True)

584 <?> "implicit function argument"

585

586{-| Parses a constraint argument (for selecting a named type class instance)

src/Idris/UnusedArgs.hs+2−1

@@ -23,6 +23,7 @@ traceUnused n

23 recused <- mapM (\ (argn, i, (g, j)) ->

24 do u <- used [(n, i)] g j

25 return (argn, u)) fargs

26+ logLvl 4 $ show n ++ " recused TRACE: " ++ show recused

26 let fused = nub $ usedns ++ map fst (filter snd recused)

27 let fused = nub $ usedns ++ map fst (filter snd recused)

27 logLvl 1 $ show n ++ " used args: " ++ show fused

28 logLvl 1 $ show n ++ " used args: " ++ show fused

28 let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)

29 let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)

@@ -50,7 +51,7 @@ used path g j

50 recused <- mapM (\ (argn, j, (g', j')) ->

51 recused <- mapM (\ (argn, j, (g', j')) ->

51 used ((g,j):path) g' j') garg

52 used ((g,j):path) g' j') garg

52 -- used on any route from here, or not used recursively

53 -- used on any route from here, or not used recursively

53− return (directuse || null recused || or recused)

54+ return (directuse || or recused)

54 _ -> return True -- no definition, assume used

55 _ -> return True -- no definition, assume used

55

56

56getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

57getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

test/reg031/expectednew file+1

@@ -0,0 +1 @@

1+[10, -128, -55, -1, 10, 51, 10, 52]

test/reg031/reg031.idrnew file+4

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

1+module Main

2+

3+main : IO ()

4+main = print . map ord . unpack $ "\x0a\x80\xC9\xFF\n3\n4"

test/reg031/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ reg031.idr -o reg031

3+./reg031

4+rm -f *.ibc reg031