58f3f68 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:edwinb/Idris-dev

commit58f3f68e08efc82429e4d31711f295a57a3038e7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Jun 2013, 00:07 (13 years ago) parentc7fded1 115783c

11 files changed+167−16

compare with master

unifiedsplit

lib/Data/HVect.idr+63 lib/Data/Vect.idr+32 lib/Prelude/Vect.idr+4 lib/base.ipkg+1−1 src/Core/CoreParser.hs+10−7 src/Core/Evaluate.hs+1−1 src/IRTS/CodegenC.hs+1−1 src/Idris/Primitives.hs+45−6 test/test028/expected+1 test/test028/run+4 test/test028/test028.idr+5

lib/Data/HVect.idrnew file+63

@@ -0,0 +1,63 @@

1+module Data.HVect

3+import Data.Vect

5+%access public

6+%default total

8+using (k : Nat, ts : Vect Type k)

9+ data HVect : Vect Type k -> Type where

10+ Nil : HVect []

11+ (::) : t -> HVect ts -> HVect (t::ts)

12+

13+ index : (i : Fin k) -> HVect ts -> index i ts

14+ index fO (x::xs) = x

15+ index (fS j) (x::xs) = index j xs

16+

17+ deleteAt : {us : Vect Type (S l)} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

18+ deleteAt fO (x::xs) = xs

19+ deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs

20+ deleteAt _ [] impossible

21+

22+ replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

23+ replaceAt fO y (x::xs) = y::xs

24+ replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs

25+

26+ updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)

27+ updateAt fO f (x::xs) = f x :: xs

28+ updateAt (fS j) f (x::xs) = x :: updateAt j f xs

29+

30+ (++) : {us : Vect Type l} -> HVect ts -> HVect us -> HVect (ts ++ us)

31+ (++) [] ys = ys

32+ (++) (x::xs) ys = x :: (xs ++ ys)

33+

34+ instance Eq (HVect []) where

35+ [] == [] = True

36+

37+ instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where

38+ (x::xs) == (y::ys) = x == y && xs == ys

39+

40+ class Shows (k : Nat) (ts : Vect Type k) where

41+ shows : HVect ts -> Vect String k

42+

43+ instance Shows O [] where

44+ shows [] = []

45+

46+ instance (Show t, Shows k ts) => Shows (S k) (t::ts) where

47+ shows (x::xs) = show x :: shows xs

48+

49+ instance (Shows k ts) => Show (HVect ts) where

50+ show xs = show (shows xs)

51+

52+ get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t

53+ get {p = Here} (x::xs) = x

54+ get {p = There p'} (x::xs) = get {p = p'} xs

55+

56+ put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts

57+ put {p = Here} y (x::xs) = y :: xs

58+ put {p = There p'} y (x::xs) = x :: put {p = p'} y xs

59+

60+ update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)

61+ update {p = Here} f (x::xs) = f x :: xs

62+ update {p = There p'} f (x::xs) = x :: update {p = p'} f xs

63+

lib/Data/Vect.idrnew file+32

@@ -0,0 +1,32 @@

1+module Data.Vect

3+import Language.Reflection

5+%access public

6+%default total

8+--------------------------------------------------------------------------------

9+-- Elem

10+--------------------------------------------------------------------------------

11+

12+data Elem : a -> Vect a k -> Type where

13+ Here : {xs : Vect a k} -> Elem x (x::xs)

14+ There : {xs : Vect a k} -> Elem x xs -> Elem x (y::xs)

15+

16+findElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic

17+findElem O ctxt goal = Refine "Here" `Seq` Solve

18+findElem (S n) ctxt goal = GoalType "Elem" (Try (Refine "Here" `Seq` Solve) (Refine "There" `Seq` (Solve `Seq` findElem n ctxt goal)))

19+

20+replaceElem : (xs : Vect t k) -> Elem x xs -> (y : t) -> (ys : Vect t k ** Elem y ys)

21+replaceElem (x::xs) Here y = (y :: xs ** Here)

22+replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)

23+ | (ys ** yinys) = (x :: ys ** There yinys)

24+

25+replaceByElem : (xs : Vect t k) -> Elem x xs -> t -> Vect t k

26+replaceByElem (x::xs) Here y = y :: xs

27+replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y

28+

29+mapElem : {xs : Vect t k} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)

30+mapElem Here = Here

31+mapElem (There e) = There (mapElem e)

32+

lib/Prelude/Vect.idr+4

@@ -41,6 +41,10 @@ deleteAt fO (x::xs) = xs

4141deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

4242deleteAt _ [] impossible

4343

44+replaceAt : Fin n -> t -> Vect t n -> Vect t n

45+replaceAt fO y (x::xs) = y::xs

46+replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs

47+

4448--------------------------------------------------------------------------------

4549-- Subvectors

4650--------------------------------------------------------------------------------

lib/base.ipkg+1−1

@@ -25,7 +25,7 @@ modules = Builtins, Prelude, IO, System,

2525 Data.Bits, Data.Mod2,

2626 Data.Z, Data.Sign,

2727 Data.SortedMap, Data.SortedSet, Data.BoundedList,

28− Data.Vect.Quantifiers,

28+ Data.Vect, Data.HVect, Data.Vect.Quantifiers,

2929

3030 Control.Monad.Identity, Control.Monad.State, Control.Category,

3131 Control.Arrow,

src/Core/CoreParser.hs+10−7

@@ -57,13 +57,16 @@ lexWS = do i <- getInput

5757 where

5858

5959 simpleSpace = skipMany1 (satisfy isSpace)

60− oneLineComment = do try (do string ("--")

61− satisfy (\x -> x /= '|' && x /= '^'))

62− skipMany (satisfy (/= '\n'))

63− return ()

64− multiLineComment = do try (do string "{-"

65− satisfy (\x -> x /= '|' && x /= '^'))

66− inCommentMulti

60+ oneLineComment =

61+ try (void $ string "--\n") <|>

62+ do try (do string "--"

63+ satisfy (\x -> x /= '|' && x /= '^'))

64+ skipMany (satisfy (/= '\n'))

65+ multiLineComment =

66+ try (void $ string "{--}") <|>

67+ do try (do string "{-"

68+ satisfy (\x -> x /= '|' && x /= '^'))

69+ inCommentMulti

6770

6871 inCommentMulti

6972 = do{ try (string "-}") ; return () }

src/Core/Evaluate.hs+1−1

@@ -174,7 +174,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

174174 | i < length env && i >= 0 = return $ env !! i

175175 | otherwise = return $ VV i

176176 ev ntimes stk top env (Bind n (Let t v) sc)

177− | not simpl -- || vinstances 0 sc < 2

177+ | not simpl -- - || vinstances 0 sc < 2

178178 = do v' <- ev ntimes stk top env v --(finalise v)

179179 sc' <- ev ntimes stk top (v' : env) sc

180180 wknV (-1) sc'

src/IRTS/CodegenC.hs+1−1

@@ -352,7 +352,7 @@ doOp v (LZExt from to) [x]

352352 | intTyWidth from < intTyWidth to = bitCoerce v "Z" from to x

353353doOp v (LTrunc ITNative to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

354354doOp v (LTrunc from ITNative) [x] = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (intTyWidth from) ++ ")"

355−doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, mpz_get_ui(GETMPZ(" ++ creg x ++ "))"

355+doOp v (LTrunc ITBig to) [x] = v ++ "idris_b" ++ show (intTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"

356356doOp v (LTrunc from to) [x]

357357 | intTyWidth from > intTyWidth to = bitCoerce v "T" from to x

358358

src/Idris/Primitives.hs+45−6

@@ -22,16 +22,20 @@ data Prim = Prim { p_name :: Name,

2222 p_total :: Totality

2323 }

2424

25+ty :: [Const] -> Const -> Type

2526ty [] x = Constant x

2627ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

2728

29+believeTy :: Type

2830believeTy = Bind (UN "a") (Pi (TType (UVar (-2))))

2931 (Bind (UN "b") (Pi (TType (UVar (-2))))

3032 (Bind (UN "x") (Pi (V 1)) (V 1)))

3133

34+total, partial :: Totality

3235total = Total []

33−partial = Partial NotCovering

36+partial = Partial NotCovering

3437

38+primitives :: [Prim]

3539primitives =

3640 -- operators

3741 [Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))

@@ -138,7 +142,7 @@ primitives =

138142 (1, LFloatStr) total,

139143

140144 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)

141− (1, LFExp) total,

145+ (1, LFExp) total,

142146 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)

143147 (1, LFLog) total,

144148 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)

@@ -181,6 +185,7 @@ primitives =

181185 (3, LNoOp) partial -- ahem

182186 ] ++ concatMap intOps [IT8, IT16, IT32, IT64, ITBig, ITNative]

183187

188+intOps :: IntTy -> [Prim]

184189intOps ity =

185190 [ iCmp ity "lt" (bCmp ity (<)) LLt total

186191 , iCmp ity "lte" (bCmp ity (<=)) LLe total

@@ -216,50 +221,67 @@ intTyName ITNative = "Int"

216221intTyName ITBig = "BigInt"

217222intTyName sized = "B" ++ show (intTyWidth sized)

218223

224+iCmp, iBinOp, iUnOp :: IntTy -> String -> ([Value] -> Maybe Value) -> (IntTy -> PrimFn) -> Totality -> Prim

219225iCmp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) IType) 2 impl (2, irop ity) totality

220226iBinOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty (replicate 2 $ intTyToConst ity) (intTyToConst ity)) 2 impl (2, irop ity) totality

221227iUnOp ity op impl irop totality = Prim (UN $ "prim__" ++ op ++ intTyName ity) (ty [intTyToConst ity] (intTyToConst ity)) 1 impl (1, irop ity) totality

228+

229+iCoerce :: IntTy -> IntTy -> String -> (IntTy -> IntTy -> [Value] -> Maybe Value) -> (IntTy -> IntTy -> PrimFn) -> Prim

222230iCoerce from to op impl irop =

223231 Prim (UN $ "prim__" ++ op ++ intTyName from ++ "_" ++ intTyName to)

224232 (ty [intTyToConst from] (intTyToConst to)) 1 (impl from to) (1, irop from to) total

225233

234+p_believeMe :: [a] -> Maybe a

226235p_believeMe [_,_,x] = Just x

227236p_believeMe _ = Nothing

228237

238+iUn :: (Int -> Int) -> [Value] -> Maybe Value

229239iUn op [VConstant (I x)] = Just $ VConstant (I (op x))

230240iUn _ _ = Nothing

231241

242+iBin :: (Int -> Int -> Int) -> [Value] -> Maybe Value

232243iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

233244iBin _ _ = Nothing

234245

246+bBin :: (Integer -> Integer -> Integer) -> [Value] -> Maybe Value

235247bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

236248bBin _ _ = Nothing

237249

250+bBini :: (Integer -> Integer -> Int) -> [Value] -> Maybe Value

238251bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))

239252bBini _ _ = Nothing

240253

254+biBin :: (Int -> Int -> Bool) -> [Value] -> Maybe Value

241255biBin op = iBin (\x y -> if (op x y) then 1 else 0)

256+

257+bbBin :: (Integer -> Integer -> Bool) -> [Value] -> Maybe Value

242258bbBin op = bBini (\x y -> if (op x y) then 1 else 0)

243259

260+fBin :: (Double -> Double -> Double) -> [Value] -> Maybe Value

244261fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))

245262fBin _ _ = Nothing

246263

264+bfBin :: (Double -> Double -> Bool) -> [Value] -> Maybe Value

247265bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in

248266 Just $ VConstant (I i)

249267bfBin _ _ = Nothing

250268

269+bcBin :: (Char -> Char -> Bool) -> [Value] -> Maybe Value

251270bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in

252271 Just $ VConstant (I i)

253272bcBin _ _ = Nothing

254273

255−bsBin op [VConstant (Str x), VConstant (Str y)]

274+bsBin :: (String -> String -> Bool) -> [Value] -> Maybe Value

275+bsBin op [VConstant (Str x), VConstant (Str y)]

256276 = let i = (if op x y then 1 else 0) in

257277 Just $ VConstant (I i)

258278bsBin _ _ = Nothing

259279

280+sBin :: (String -> String -> String) -> [Value] -> Maybe Value

260281sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))

261282sBin _ _ = Nothing

262283

284+bsrem :: IntTy -> [Value] -> Maybe Value

263285bsrem IT8 [VConstant (B8 x), VConstant (B8 y)]

264286 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int8)))

265287bsrem IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -271,6 +293,7 @@ bsrem IT64 [VConstant (B64 x), VConstant (B64 y)]

271293bsrem ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `rem` y))

272294bsrem _ _ = Nothing

273295

296+bsdiv :: IntTy -> [Value] -> Maybe Value

274297bsdiv IT8 [VConstant (B8 x), VConstant (B8 y)]

275298 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int8)))

276299bsdiv IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -282,6 +305,7 @@ bsdiv IT64 [VConstant (B64 x), VConstant (B64 y)]

282305bsdiv ITNative [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (x `div` y))

283306bsdiv _ _ = Nothing

284307

308+bashr :: IntTy -> [Value] -> Maybe Value

285309bashr IT8 [VConstant (B8 x), VConstant (B8 y)]

286310 = Just $ VConstant (B8 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int8)))

287311bashr IT16 [VConstant (B16 x), VConstant (B16 y)]

@@ -320,6 +344,7 @@ bCmp ITBig op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (if (op

320344bCmp ITNative op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (if (op x y) then 1 else 0))

321345bCmp _ _ _ = Nothing

322346

347+toInt :: Integral a => IntTy -> a -> Value

323348toInt IT8 x = VConstant (B8 (fromIntegral x))

324349toInt IT16 x = VConstant (B16 (fromIntegral x))

325350toInt IT32 x = VConstant (B32 (fromIntegral x))

@@ -327,6 +352,7 @@ toInt IT64 x = VConstant (B64 (fromIntegral x))

327352toInt ITBig x = VConstant (BI (fromIntegral x))

328353toInt ITNative x = VConstant (I (fromIntegral x))

329354

355+intToInt :: IntTy -> IntTy -> [Value] -> Maybe Value

330356intToInt IT8 out [VConstant (B8 x)] = Just $ toInt out x

331357intToInt IT16 out [VConstant (B16 x)] = Just $ toInt out x

332358intToInt IT32 out [VConstant (B32 x)] = Just $ toInt out x

@@ -335,12 +361,14 @@ intToInt ITBig out [VConstant (BI x)] = Just $ toInt out x

335361intToInt ITNative out [VConstant (I x)] = Just $ toInt out x

336362intToInt _ _ _ = Nothing

337363

364+zext :: IntTy -> IntTy -> [Value] -> Maybe Value

338365zext from ITBig val = intToInt from ITBig val

339366zext ITBig _ _ = Nothing

340367zext from to val

341368 | intTyWidth from < intTyWidth to = intToInt from to val

342369zext _ _ _ = Nothing

343370

371+sext :: IntTy -> IntTy -> [Value] -> Maybe Value

344372sext IT8 out [VConstant (B8 x)] = Just $ toInt out (fromIntegral x :: Int8)

345373sext IT16 out [VConstant (B16 x)] = Just $ toInt out (fromIntegral x :: Int16)

346374sext IT32 out [VConstant (B32 x)] = Just $ toInt out (fromIntegral x :: Int32)

@@ -348,6 +376,7 @@ sext IT64 out [VConstant (B64 x)] = Just $ toInt out (fromIntegral x :: Int64)

348376sext ITBig _ _ = Nothing

349377sext from to val = intToInt from to val

350378

379+trunc :: IntTy -> IntTy -> [Value] -> Maybe Value

351380trunc ITBig to val = intToInt ITBig to val

352381trunc _ ITBig _ = Nothing

353382trunc from to val | intTyWidth from > intTyWidth to = intToInt from to val

@@ -362,25 +391,31 @@ getInt [VConstant (I x)] = Just . toInteger $ x

362391getInt [VConstant (BI x)] = Just x

363392getInt _ = Nothing

364393

394+intToStr :: [Value] -> Maybe Value

365395intToStr val | Just i <- getInt val = Just $ VConstant (Str (show i))

366396intToStr _ = Nothing

367397

398+strToInt :: IntTy -> [Value] -> Maybe Value

368399strToInt ity [VConstant (Str x)] = case reads x of

369400 [(n,"")] -> Just $ toInt ity (n :: Integer)

370401 _ -> Just $ VConstant (I 0)

371402strToInt _ _ = Nothing

372403

404+intToFloat :: [Value] -> Maybe Value

373405intToFloat val | Just i <- getInt val = Just $ VConstant (Fl (fromIntegral i))

374406intToFloat _ = Nothing

375407

408+floatToInt :: IntTy -> [Value] -> Maybe Value

376409floatToInt ity [VConstant (Fl x)] = Just $ toInt ity (truncate x :: Integer)

377410floatToInt _ _ = Nothing

378411

412+c_intToChar :: [Value] -> Maybe Value

379413c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))

380414c_intToChar _ = Nothing

381415c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))

382416c_charToInt _ = Nothing

383417

418+c_floatToStr :: [Value] -> Maybe Value

384419c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

385420c_floatToStr _ = Nothing

386421c_strToFloat [VConstant (Str x)] = case reads x of

@@ -388,9 +423,11 @@ c_strToFloat [VConstant (Str x)] = case reads x of

388423 _ -> Just $ VConstant (Fl 0)

389424c_strToFloat _ = Nothing

390425

426+p_fPrim :: (Double -> Double) -> [Value] -> Maybe Value

391427p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))

392428p_fPrim f _ = Nothing

393429

430+p_floatExp, p_floatLog, p_floatSin, p_floatCos, p_floatTan, p_floatASin, p_floatACos, p_floatATan, p_floatSqrt, p_floatFloor, p_floatCeil :: [Value] -> Maybe Value

394431p_floatExp = p_fPrim exp

395432p_floatLog = p_fPrim log

396433p_floatSin = p_fPrim sin

@@ -403,13 +440,14 @@ p_floatSqrt = p_fPrim sqrt

403440p_floatFloor = p_fPrim (fromInteger . floor)

404441p_floatCeil = p_fPrim (fromInteger . ceiling)

405442

443+p_strLen, p_strHead, p_strTail, p_strIndex, p_strCons, p_strRev :: [Value] -> Maybe Value

406444p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))

407445p_strLen _ = Nothing

408446p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)

409447p_strHead _ = Nothing

410448p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)

411449p_strTail _ = Nothing

412−p_strIndex [VConstant (Str xs), VConstant (I i)]

450+p_strIndex [VConstant (Str xs), VConstant (I i)]

413451 | i < length xs = Just $ VConstant (Ch (xs!!i))

414452p_strIndex _ = Nothing

415453p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))

@@ -417,17 +455,18 @@ p_strCons _ = Nothing

417455p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))

418456p_strRev _ = Nothing

419457

458+p_cantreduce :: a -> Maybe b

420459p_cantreduce _ = Nothing

421460

422461elabPrim :: Prim -> Idris ()

423−elabPrim (Prim n ty i def sc tot)

462+elabPrim (Prim n ty i def sc tot)

424463 = do updateContext (addOperator n ty i def)

425464 setTotality n tot

426465 i <- getIState

427466 putIState i { idris_scprims = (n, sc) : idris_scprims i }

428467

429468elabPrims :: Idris ()

430−elabPrims = do mapM_ (elabDecl EAll toplevel)

469+elabPrims = do mapM_ (elabDecl EAll toplevel)

431470 (map (PData "" defaultSyntax (FC "builtin" 0) False)

432471 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

433472 mapM_ elabPrim primitives

test/test028/expectednew file+1

@@ -0,0 +1 @@

1+hello, world!

test/test028/runnew file+4

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

1+#!/bin/bash

2+idris $@ test028.idr -o test028

3+./test028

4+rm -f test028 test028.ibc

test/test028/test028.idrnew file+5

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

1+{--}

2+module Main

3+--

4+main : IO ()

5+main = print "hello, world!"