a1e13db · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make ChType a member of IntTy ITChar.

This enables back end specific character encoding and unifies some operations. Note that there is no Ord instance, so ``` 'a' + 1 ``` will not work. However ``` prim__addChar 'a' (prim__truncBigInt_Char 1) ``` is now possible and client libraries may feel free to put it to good use (e.g. checking for character ranges).

commita1e13db146b8af55f75f611459c0f1cacf440a01 authorJan Bessai <Jan.Bessai@tu-dortmund.de> dateMon 8 Jul 2013, 19:06 (13 years ago) parentb4689f4

16 files changed+106−49

compare with master

unifiedsplit

effects/Effect/Memory.idr+3−3 lib/IO.idr+6−2 src/Core/CaseTree.hs+1−1 src/Core/Evaluate.hs+2−2 src/Core/Execute.hs+4−3 src/Core/TT.hs+5−4 src/Core/Typecheck.hs+1−1 src/IRTS/CodegenC.hs+36 src/IRTS/CodegenJavaScript.hs+1−2 src/IRTS/CodegenLLVM.hs+2−1 src/IRTS/Compiler.hs+4−2 src/IRTS/LParser.hs+14−3 src/Idris/ElabTerm.hs+2−2 src/Idris/IBC.hs+3−3 src/Idris/Parser.hs+1−1 src/Idris/Primitives.hs+21−19

effects/Effect/Memory.idr+3−3

@@ -48,7 +48,7 @@ do_malloc size with (fromInteger (cast size) == size)

4848private

4949do_memset : Ptr -> Nat -> Bits8 -> Nat -> IO ()

5050do_memset ptr offset c size

51− = mkForeign (FFun "idris_memset" [FPtr, FInt, FChar, FInt] FUnit)

51+ = mkForeign (FFun "idris_memset" [FPtr, FInt, FByte, FInt] FUnit)

5252 ptr (fromInteger $ cast offset) c (fromInteger $ cast size)

5353

5454private

@@ -65,7 +65,7 @@ private

6565do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect Bits8 size)

6666do_peek _ _ O = return (Prelude.Vect.Nil)

6767do_peek ptr offset (S n)

68− = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FChar) ptr (fromInteger $ cast offset)

68+ = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)

6969 bs <- do_peek ptr (S offset) n

7070 Prelude.Monad.return (Prelude.Vect.(::) b bs)

7171

@@ -73,7 +73,7 @@ private

7373do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()

7474do_poke _ _ [] = return ()

7575do_poke ptr offset (b::bs)

76− = do mkForeign (FFun "idris_poke" [FPtr, FInt, FChar] FUnit) ptr (fromInteger $ cast offset) b

76+ = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b

7777 do_poke ptr (S offset) bs

7878

7979instance Handler RawMemory (IOExcept String) where

lib/IO.idr+6−2

@@ -21,7 +21,7 @@ io_return x = prim__IO x

2121run__IO : IO () -> IO ()

2222run__IO v = io_bind v (\v' => io_return v')

2323

24−data IntTy = ITNative | IT8 | IT16 | IT32 | IT64

24+data IntTy = ITChar | ITNative | IT8 | IT16 | IT32 | IT64

2525data FTy = FIntT IntTy

2626 | FFunction FTy FTy

2727 | FFloat

@@ -34,7 +34,10 @@ FInt : FTy

3434FInt = FIntT ITNative

3535

3636FChar : FTy

37−FChar = FIntT IT8

37+FChar = FIntT ITChar

38+

39+FByte : FTy

40+FByte = FIntT IT8

3841

3942FShort : FTy

4043FShort = FIntT IT16

@@ -44,6 +47,7 @@ FLong = FIntT IT64

4447

4548interpFTy : FTy -> Type

4649interpFTy (FIntT ITNative) = Int

50+interpFTy (FIntT ITChar) = Char

4751interpFTy (FIntT IT8) = Bits8

4852interpFTy (FIntT IT16) = Bits16

4953interpFTy (FIntT IT32) = Bits32

src/Core/CaseTree.hs+1−1

@@ -231,7 +231,7 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

231231 toPat' (Constant (AType (ATInt ITNative))) []

232232 | tc = return $ PCon (UN "Int") 1 []

233233 toPat' (Constant (AType ATFloat)) [] | tc = return $ PCon (UN "Float") 2 []

234− toPat' (Constant ChType) [] | tc = return $ PCon (UN "Char") 3 []

234+ toPat' (Constant (AType (ATInt ITChar))) [] | tc = return $ PCon (UN "Char") 3 []

235235 toPat' (Constant StrType) [] | tc = return $ PCon (UN "String") 4 []

236236 toPat' (Constant PtrType) [] | tc = return $ PCon (UN "Ptr") 5 []

237237 toPat' (Constant (AType (ATInt ITBig))) []

src/Core/Evaluate.hs+2−2

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

331331 findConst c (ConstCase c' v : xs) | c == c' = Just v

332332 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

333333 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v

334− findConst ChType (ConCase n 3 [] v : xs) = Just v

334+ findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v

335335 findConst StrType (ConCase n 4 [] v : xs) = Just v

336336 findConst PtrType (ConCase n 5 [] v : xs) = Just v

337337 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v

@@ -524,7 +524,7 @@ eval_hnf ctxt statics genv tm = ev [] tm where

524524 findConst c (ConstCase c' v : xs) | c == c' = Just v

525525 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v

526526 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v

527− findConst ChType (ConCase n 3 [] v : xs) = Just v

527+ findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v

528528 findConst StrType (ConCase n 4 [] v : xs) = Just v

529529 findConst PtrType (ConCase n 5 [] v : xs) = Just v

530530 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v

src/Core/Execute.hs+4−3

@@ -386,7 +386,6 @@ idrisType :: FType -> ExecVal

386386idrisType FUnit = EP Ref unitTy EErased

387387idrisType ft = EConstant (idr ft)

388388 where idr (FArith ty) = AType ty

389− idr FChar = ChType

390389 idr FString = StrType

391390 idr FPtr = PtrType

392391

@@ -419,8 +418,9 @@ call (FFun name argTypes retType) args =

419418 call' (Fun _ h) args (FArith ATFloat) = do

420419 res <- execIO $ callFFI h retCDouble (prepArgs args)

421420 return (EConstant (Fl (realToFrac res)))

422− call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

423− return (EConstant (Ch (castCCharToChar res)))

421+ call' (Fun _ h) args (FArith (ATInt ITChar)) = do

422+ res <- execIO $ callFFI h retCChar (prepArgs args)

423+ return (EConstant (Ch (castCCharToChar res)))

424424 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

425425 hStr <- execIO $ peekCString res

426426-- lift $ free res

@@ -460,6 +460,7 @@ getFTy :: ExecVal -> Maybe FType

460460getFTy (EApp (EP _ (UN "FIntT") _) (EP _ (UN intTy) _)) =

461461 case intTy of

462462 "ITNative" -> Just (FArith (ATInt ITNative))

463+ "ITChar" -> Just (FArith (ATInt ITChar))

463464 "IT8" -> Just (FArith (ATInt (ITFixed IT8)))

464465 "IT16" -> Just (FArith (ATInt (ITFixed IT16)))

465466 "IT32" -> Just (FArith (ATInt (ITFixed IT32)))

src/Core/TT.hs+5−4

@@ -286,7 +286,7 @@ instance Pretty NativeTy where

286286 pretty IT32 = text "Bits32"

287287 pretty IT64 = text "Bits64"

288288

289−data IntTy = ITFixed NativeTy | ITNative | ITBig

289+data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar

290290 | ITVec NativeTy Int

291291 deriving (Show, Eq, Ord)

292292

@@ -296,6 +296,7 @@ data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors

296296instance Pretty ArithTy where

297297 pretty (ATInt ITNative) = text "Int"

298298 pretty (ATInt ITBig) = text "BigInt"

299+ pretty (ATInt ITChar) = text "Char"

299300 pretty (ATInt (ITFixed n)) = pretty n

300301 pretty (ATInt (ITVec e c)) = pretty e <> text "x" <> (text . show $ c)

301302 pretty ATFloat = text "Float"

@@ -310,13 +311,14 @@ nativeTyWidth IT64 = 64

310311intTyWidth :: IntTy -> Int

311312intTyWidth (ITFixed n) = nativeTyWidth n

312313intTyWidth ITNative = 8 * sizeOf (0 :: Int)

314+intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"

313315intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"

314316

315317data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

316318 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64

317319 | B8V (Vector Word8) | B16V (Vector Word16)

318320 | B32V (Vector Word32) | B64V (Vector Word64)

319− | AType ArithTy | ChType | StrType

321+ | AType ArithTy | StrType

320322 | PtrType | VoidType | Forgot

321323 deriving (Eq, Ord)

322324{-!

@@ -333,7 +335,6 @@ instance Pretty Const where

333335 pretty (Ch c) = text . show $ c

334336 pretty (Str s) = text s

335337 pretty (AType a) = pretty a

336− pretty ChType = text "Char"

337338 pretty StrType = text "String"

338339 pretty PtrType = text "Ptr"

339340 pretty VoidType = text "Void"

@@ -781,9 +782,9 @@ instance Show Const where

781782 show (AType ATFloat) = "Float"

782783 show (AType (ATInt ITBig)) = "Integer"

783784 show (AType (ATInt ITNative)) = "Int"

785+ show (AType (ATInt ITChar)) = "Char"

784786 show (AType (ATInt (ITFixed it))) = itBitsName it

785787 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c

786− show ChType = "Char"

787788 show StrType = "String"

788789 show PtrType = "Ptr"

789790 show VoidType = "Void"

src/Core/Typecheck.hs+1−1

@@ -102,7 +102,7 @@ check' holes ctxt env top = chk env top where

102102 where constType (I _) = Constant (AType (ATInt ITNative))

103103 constType (BI _) = Constant (AType (ATInt ITBig))

104104 constType (Fl _) = Constant (AType ATFloat)

105− constType (Ch _) = Constant ChType

105+ constType (Ch _) = Constant (AType (ATInt ITChar))

106106 constType (Str _) = Constant StrType

107107 constType (B8 _) = Constant (AType (ATInt (ITFixed IT8)))

108108 constType (B16 _) = Constant (AType (ATInt (ITFixed IT16)))

src/IRTS/CodegenC.hs+36

@@ -230,6 +230,7 @@ bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); assert(0);

230230

231231

232232c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

233+c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

233234c_irts (FArith (ATInt (ITFixed ity))) l x

234235 = l ++ "idris_b" ++ show (nativeTyWidth ity) ++ "const(vm, " ++ x ++ ")"

235236c_irts FChar l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

@@ -240,6 +241,7 @@ c_irts (FArith ATFloat) l x = l ++ "MKFLOAT(vm, " ++ x ++ ")"

240241c_irts FAny l x = l ++ x

241242

242243irts_c (FArith (ATInt ITNative)) x = "GETINT(" ++ x ++ ")"

244+irts_c (FArith (ATInt ITChar)) x = irts_c (FArith (ATInt ITNative)) x

243245irts_c (FArith (ATInt (ITFixed ity))) x

244246 = "(" ++ x ++ "->info.bits" ++ show (nativeTyWidth ity) ++ ")"

245247irts_c FChar x = "GETINT(" ++ x ++ ")"

@@ -277,6 +279,26 @@ doOp v (LLe (ATInt ITNative)) [l, r] = v ++ "INTOP(<=," ++ creg l ++ ", " ++ cre

277279doOp v (LGt (ATInt ITNative)) [l, r] = v ++ "INTOP(>," ++ creg l ++ ", " ++ creg r ++ ")"

278280doOp v (LGe (ATInt ITNative)) [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

279281

282+doOp v (LPlus (ATInt ITChar)) [l, r] = doOp v (LPlus (ATInt ITNative)) [l, r]

283+doOp v (LMinus (ATInt ITChar)) [l, r] = doOp v (LMinus (ATInt ITNative)) [l, r]

284+doOp v (LTimes (ATInt ITChar)) [l, r] = doOp v (LTimes (ATInt ITNative)) [l, r]

285+doOp v (LUDiv ITChar) [l, r] = doOp v (LUDiv ITNative) [l, r]

286+doOp v (LSDiv (ATInt ITChar)) [l, r] = doOp v (LSDiv (ATInt ITNative)) [l, r]

287+doOp v (LURem ITChar) [l, r] = doOp v (LURem ITNative) [l, r]

288+doOp v (LSRem (ATInt ITChar)) [l, r] = doOp v (LSRem (ATInt ITNative)) [l, r]

289+doOp v (LAnd ITChar) [l, r] = doOp v (LAnd ITNative) [l, r]

290+doOp v (LOr ITChar) [l, r] = doOp v (LOr ITNative) [l, r]

291+doOp v (LXOr ITChar) [l, r] = doOp v (LXOr ITNative) [l, r]

292+doOp v (LSHL ITChar) [l, r] = doOp v (LSHL ITNative) [l, r]

293+doOp v (LLSHR ITChar) [l, r] = doOp v (LLSHR ITNative) [l, r]

294+doOp v (LASHR ITChar) [l, r] = doOp v (LASHR ITNative) [l, r]

295+doOp v (LCompl ITChar) [x] = doOp v (LCompl ITNative) [x]

296+doOp v (LEq (ATInt ITChar)) [l, r] = doOp v (LEq (ATInt ITNative)) [l, r]

297+doOp v (LLt (ATInt ITChar)) [l, r] = doOp v (LLt (ATInt ITNative)) [l, r]

298+doOp v (LLe (ATInt ITChar)) [l, r] = doOp v (LLe (ATInt ITNative)) [l, r]

299+doOp v (LGt (ATInt ITChar)) [l, r] = doOp v (LGt (ATInt ITNative)) [l, r]

300+doOp v (LGe (ATInt ITChar)) [l, r] = doOp v (LGe (ATInt ITNative)) [l, r]

301+

280302doOp v (LPlus ATFloat) [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

281303doOp v (LMinus ATFloat) [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

282304doOp v (LTimes ATFloat) [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"

@@ -346,22 +368,34 @@ doOp v (LSExt (ITFixed from) ITBig) [x]

346368 = v ++ "MKBIGSI(vm, (" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

347369doOp v (LSExt ITNative (ITFixed to)) [x]

348370 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

371+doOp v (LSExt ITChar (ITFixed to)) [x]

372+ = doOp v (LSExt ITNative (ITFixed to)) [x]

349373doOp v (LSExt (ITFixed from) ITNative) [x]

350374 = v ++ "MKINT((i_int)((" ++ signedTy from ++ ")" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ "))"

375+doOp v (LSExt (ITFixed from) ITChar) [x]

376+ = doOp v (LSExt (ITFixed from) ITNative) [x]

351377doOp v (LSExt (ITFixed from) (ITFixed to)) [x]

352378 | nativeTyWidth from < nativeTyWidth to = bitCoerce v "S" from to x

353379doOp v (LZExt ITNative (ITFixed to)) [x]

354380 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ ")"

381+doOp v (LZExt ITChar (ITFixed to)) [x]

382+ = doOp v (LZExt ITNative (ITFixed to)) [x]

355383doOp v (LZExt (ITFixed from) ITNative) [x]

356384 = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

385+doOp v (LZExt (ITFixed from) ITChar) [x]

386+ = doOp v (LZExt (ITFixed from) ITNative) [x]

357387doOp v (LZExt (ITFixed from) ITBig) [x]

358388 = v ++ "MKBIGUI(vm, " ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

359389doOp v (LZExt (ITFixed from) (ITFixed to)) [x]

360390 | nativeTyWidth from < nativeTyWidth to = bitCoerce v "Z" from to x

361391doOp v (LTrunc ITNative (ITFixed to)) [x]

362392 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, GETINT(" ++ creg x ++ "))"

393+doOp v (LTrunc ITChar (ITFixed to)) [x]

394+ = doOp v (LTrunc ITNative (ITFixed to)) [x]

363395doOp v (LTrunc (ITFixed from) ITNative) [x]

364396 = v ++ "MKINT((i_int)" ++ creg x ++ "->info.bits" ++ show (nativeTyWidth from) ++ ")"

397+doOp v (LTrunc (ITFixed from) ITChar) [x]

398+ = doOp v (LTrunc (ITFixed from) ITNative) [x]

365399doOp v (LTrunc ITBig (ITFixed to)) [x]

366400 = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, ISINT(" ++ creg x ++ ") ? GETINT(" ++ creg x ++ ") : mpz_get_ui(GETMPZ(" ++ creg x ++ ")))"

367401doOp v (LTrunc (ITFixed from) (ITFixed to)) [x]

@@ -393,7 +427,9 @@ doOp v LFork [x] = v ++ "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", "

393427doOp v LPar [x] = v ++ creg x -- "MKPTR(vm, vmThread(vm, " ++ cname (MN 0 "EVAL") ++ ", " ++ creg x ++ "))"

394428doOp v LVMPtr [] = v ++ "MKPTR(vm, vm)"

395429doOp v (LChInt ITNative) args = v ++ creg (last args)

430+doOp v (LChInt ITChar) args = doOp v (LChInt ITNative) args

396431doOp v (LIntCh ITNative) args = v ++ creg (last args)

432+doOp v (LIntCh ITChar) args = doOp v (LIntCh ITNative) args

397433doOp v LNoOp args = v ++ creg (last args)

398434doOp _ op _ = "FAIL /* " ++ show op ++ " */"

399435

src/IRTS/CodegenJavaScript.hs+1−2

@@ -144,7 +144,6 @@ translateConstant (Fl f) = show f

144144translateConstant (Ch c) = show c

145145translateConstant (Str s) = show s

146146translateConstant (AType (ATInt ITNative)) = "__IDRRT__.Int"

147−translateConstant ChType = "__IDRRT__.Char"

148147translateConstant StrType = "__IDRRT__.String"

149148translateConstant (AType (ATInt ITBig)) = "__IDRRT__.Integer"

150149translateConstant (AType ATFloat) = "__IDRRT__.Float"

@@ -470,13 +469,13 @@ translateCase _ (SDefaultCase e) =

470469 createIfBlock "true" (translateExpression e)

471470

472471translateCase var (SConstCase ty e)

473− | ChType <- ty = matchHelper "Char"

474472 | StrType <- ty = matchHelper "String"

475473 | PtrType <- ty = matchHelper "Ptr"

476474 | Forgot <- ty = matchHelper "Forgot"

477475 | (AType ATFloat) <- ty = matchHelper "Float"

478476 | (AType (ATInt ITBig)) <- ty = matchHelper "Integer"

479477 | (AType (ATInt ITNative)) <- ty = matchHelper "Int"

478+ | (AType (ATInt ITChar)) <- ty = matchHelper "Char"

480479 where

481480 matchHelper tyName = translateTypeMatch var tyName e

482481

src/IRTS/CodegenLLVM.hs+2−1

@@ -794,7 +794,7 @@ ftyToTy (FArith (ATInt ITBig)) = PointerType mpzTy (AddrSpace 0)

794794ftyToTy (FArith (ATInt (ITFixed ty))) = IntegerType (fromIntegral $ nativeTyWidth ty)

795795ftyToTy (FArith (ATInt (ITVec e c)))

796796 = VectorType (fromIntegral c) (IntegerType (fromIntegral $ nativeTyWidth e))

797−ftyToTy FChar = IntegerType 32

797+ftyToTy (FArith (ATInt ITChar)) = IntegerType 32

798798ftyToTy FString = PointerType (IntegerType 8) (AddrSpace 0)

799799ftyToTy FUnit = VoidType

800800ftyToTy FPtr = PointerType (IntegerType 8) (AddrSpace 0)

@@ -804,6 +804,7 @@ ftyToTy FAny = valueType

804804-- Only use when known not to be ITBig

805805itWidth :: IntTy -> Word32

806806itWidth ITNative = 32

807+itWidth ITChar = 32

807808itWidth (ITFixed x) = fromIntegral $ nativeTyWidth x

808809

809810cgOp :: PrimFn -> [Operand] -> Codegen Operand

src/IRTS/Compiler.hs+4−2

@@ -301,7 +301,8 @@ mkIty' _ = FAny

301301

302302mkIty "FFloat" = FArith ATFloat

303303mkIty "FInt" = mkIntIty "ITNative"

304−mkIty "FChar" = mkIntIty "IT8"

304+mkIty "FChar" = mkIntIty "ITChar"

305+mkIty "FByte" = mkIntIty "IT8"

305306mkIty "FShort" = mkIntIty "IT16"

306307mkIty "FLong" = mkIntIty "IT64"

307308mkIty "FString" = FString

@@ -312,6 +313,7 @@ mkIty "FFunctionIO" = FFunctionIO

312313mkIty x = error $ "Unknown type " ++ x

313314

314315mkIntIty "ITNative" = FArith (ATInt ITNative)

316+mkIntIty "ITChar" = FArith (ATInt ITChar)

315317mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))

316318mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))

317319mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))

@@ -371,7 +373,7 @@ instance ToIR SC where

371373

372374 matchableTy (AType (ATInt ITNative)) = True

373375 matchableTy (AType (ATInt ITBig)) = True

374− matchableTy ChType = True

376+ matchableTy (AType (ATInt ITChar)) = True

375377 matchableTy StrType = True

376378

377379 matchableTy (AType (ATInt (ITFixed IT8))) = True

src/IRTS/LParser.hs+14−3

@@ -97,7 +97,9 @@ optable = [[binary "*" (\x y -> LOp (LTimes (ATInt ITNative)) [x,y]) AssocLeft,

9797 binary "*." (\x y -> LOp (LTimes ATFloat) [x,y]) AssocLeft,

9898 binary "/." (\x y -> LOp (LSDiv ATFloat) [x,y]) AssocLeft,

9999 binary "*:" (\x y -> LOp (LTimes (ATInt ITBig)) [x,y]) AssocLeft,

100− binary "/:" (\x y -> LOp (LSDiv (ATInt ITBig)) [x,y]) AssocLeft

100+ binary "/:" (\x y -> LOp (LSDiv (ATInt ITBig)) [x,y]) AssocLeft,

101+ binary "*," (\x y -> LOp (LTimes (ATInt ITChar)) [x, y]) AssocLeft,

102+ binary "/," (\x y -> LOp (LSDiv (ATInt ITChar)) [x, y]) AssocLeft

101103 ],

102104 [

103105 binary "+" (\x y -> LOp (LPlus (ATInt ITNative)) [x,y]) AssocLeft,

@@ -106,7 +108,9 @@ optable = [[binary "*" (\x y -> LOp (LTimes (ATInt ITNative)) [x,y]) AssocLeft,

106108 binary "+." (\x y -> LOp (LPlus ATFloat) [x,y]) AssocLeft,

107109 binary "-." (\x y -> LOp (LMinus ATFloat) [x,y]) AssocLeft,

108110 binary "+:" (\x y -> LOp (LPlus (ATInt ITBig)) [x,y]) AssocLeft,

109− binary "-:" (\x y -> LOp (LMinus (ATInt ITBig)) [x,y]) AssocLeft

111+ binary "-:" (\x y -> LOp (LMinus (ATInt ITBig)) [x,y]) AssocLeft,

112+ binary "+," (\x y -> LOp (LPlus (ATInt ITChar)) [x,y]) AssocLeft,

113+ binary "-," (\x y -> LOp (LMinus (ATInt ITChar)) [x,y]) AssocLeft

110114 ],

111115 [

112116 binary "==" (\x y -> LOp (LEq (ATInt ITNative)) [x, y]) AssocNone,

@@ -124,7 +128,13 @@ optable = [[binary "*" (\x y -> LOp (LTimes (ATInt ITNative)) [x,y]) AssocLeft,

124128 binary "<:" (\x y -> LOp (LLt (ATInt ITBig)) [x, y]) AssocNone,

125129 binary ">:" (\x y -> LOp (LGt (ATInt ITBig)) [x, y]) AssocNone,

126130 binary "<=:" (\x y -> LOp (LLe (ATInt ITBig)) [x, y]) AssocNone,

127− binary ">=:" (\x y -> LOp (LGe (ATInt ITBig)) [x, y]) AssocNone

131+ binary ">=:" (\x y -> LOp (LGe (ATInt ITBig)) [x, y]) AssocNone,

132+

133+ binary "==," (\x y -> LOp (LEq (ATInt ITChar)) [x, y]) AssocNone,

134+ binary "<," (\x y -> LOp (LLt (ATInt ITChar)) [x, y]) AssocNone,

135+ binary ">," (\x y -> LOp (LGt (ATInt ITChar)) [x, y]) AssocNone,

136+ binary "<=," (\x y -> LOp (LLe (ATInt ITChar)) [x, y]) AssocNone,

137+ binary ">=," (\x y -> LOp (LGe (ATInt ITChar)) [x, y]) AssocNone

128138 ]]

129139

130140binary name f assoc = Infix (do reservedOp name; return f) assoc

@@ -165,6 +175,7 @@ pLExp' = try (do lchar '%'; pCast)

165175pLang = do reserved "C"; return LANG_C

166176

167177pType = do reserved "Int"; return (FArith (ATInt ITNative))

178+ <|> do reserved "Char"; return (FArith (ATInt ITChar))

168179 <|> do reserved "Float"; return (FArith ATFloat)

169180 <|> do reserved "String"; return FString

170181 <|> do reserved "Unit"; return FUnit

src/Idris/ElabTerm.hs+2−2

@@ -1063,7 +1063,7 @@ reifyTTConst :: Term -> ElabD Const

10631063reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))

10641064reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))

10651065reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)

1066−reifyTTConst (P _ n _) | n == reflm "ChType" = return $ ChType

1066+reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar))

10671067reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

10681068reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))

10691069reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))

@@ -1181,7 +1181,7 @@ reflectConstant c@(Str _) = reflCall "Str" [RConstant c]

11811181reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")

11821182reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")

11831183reflectConstant (AType ATFloat) = Var (reflm "FlType")

1184−reflectConstant (ChType) = Var (reflm "ChType")

1184+reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")

11851185reflectConstant (StrType) = Var (reflm "StrType")

11861186reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]

11871187reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]

src/Idris/IBC.hs+3−3

@@ -24,7 +24,7 @@ import Debug.Trace

2424import Paths_idris

2525

2626ibcVersion :: Word8

27−ibcVersion = 30

27+ibcVersion = 31

2828

2929data IBCFile = IBCFile { ver :: Word8,

3030 sourcefile :: FilePath,

@@ -387,7 +387,7 @@ instance Binary Const where

387387 (AType (ATInt ITNative)) -> putWord8 9

388388 (AType (ATInt ITBig)) -> putWord8 10

389389 (AType ATFloat) -> putWord8 11

390− ChType -> putWord8 12

390+ (AType (ATInt ITChar)) -> putWord8 12

391391 StrType -> putWord8 13

392392 PtrType -> putWord8 14

393393 Forgot -> putWord8 15

@@ -422,7 +422,7 @@ instance Binary Const where

422422 9 -> return (AType (ATInt ITNative))

423423 10 -> return (AType (ATInt ITBig))

424424 11 -> return (AType ATFloat)

425− 12 -> return ChType

425+ 12 -> return (AType (ATInt ITChar))

426426 13 -> return StrType

427427 14 -> return PtrType

428428 15 -> return Forgot

src/Idris/Parser.hs+1−1

@@ -1141,7 +1141,7 @@ pIdiom syn

11411141pConstant :: IParser Const

11421142pConstant = do reserved "Integer";return (AType (ATInt ITBig))

11431143 <|> do reserved "Int"; return (AType (ATInt ITNative))

1144− <|> do reserved "Char"; return ChType

1144+ <|> do reserved "Char"; return (AType (ATInt ITChar))

11451145 <|> do reserved "Float"; return (AType ATFloat)

11461146 <|> do reserved "String"; return StrType

11471147 <|> do reserved "Ptr"; return PtrType

src/Idris/Primitives.hs+21−19

@@ -11,6 +11,7 @@ import Core.Evaluate

1111import Data.Bits

1212import Data.Word

1313import Data.Int

14+import Data.Char

1415import qualified Data.Vector.Unboxed as V

1516

1617data Prim = Prim { p_name :: Name,

@@ -32,18 +33,7 @@ partial = Partial NotCovering

3233primitives :: [Prim]

3334primitives =

3435 -- operators

35− [Prim (UN "prim__eqChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (==))

36− (2, LEq (ATInt ITNative)) total,

37− Prim (UN "prim__ltChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (<))

38− (2, LLt (ATInt ITNative)) total,

39− Prim (UN "prim__lteChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (<=))

40− (2, LLe (ATInt ITNative)) total,

41− Prim (UN "prim__gtChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (>))

42− (2, LGt (ATInt ITNative)) total,

43− Prim (UN "prim__gteChar") (ty [ChType, ChType] (AType (ATInt ITNative))) 2 (bcBin (>=))

44− (2, LGe (ATInt ITNative)) total,

45−

46− iCoerce (ITFixed IT8) (ITFixed IT16) "zext" zext LZExt,

36+ [iCoerce (ITFixed IT8) (ITFixed IT16) "zext" zext LZExt,

4737 iCoerce (ITFixed IT8) (ITFixed IT32) "zext" zext LZExt,

4838 iCoerce (ITFixed IT8) (ITFixed IT64) "zext" zext LZExt,

4939 iCoerce (ITFixed IT8) ITBig "zext" zext LZExt,

@@ -60,6 +50,7 @@ primitives =

6050 iCoerce ITNative (ITFixed IT64) "zext" zext LZExt,

6151 iCoerce ITNative (ITFixed IT32) "zext" zext LZExt,

6252 iCoerce ITNative (ITFixed IT16) "zext" zext LZExt,

53+ iCoerce ITChar ITBig "zext" zext LZExt,

6354

6455 iCoerce (ITFixed IT8) (ITFixed IT16) "sext" sext LSExt,

6556 iCoerce (ITFixed IT8) (ITFixed IT32) "sext" sext LSExt,

@@ -79,6 +70,7 @@ primitives =

7970 iCoerce ITNative (ITFixed IT64) "sext" sext LSExt,

8071 iCoerce ITNative (ITFixed IT32) "sext" sext LSExt,

8172 iCoerce ITNative (ITFixed IT16) "sext" sext LSExt,

73+ iCoerce ITChar ITBig "sext" sext LSExt,

8274

8375 iCoerce (ITFixed IT16) (ITFixed IT8) "trunc" trunc LTrunc,

8476 iCoerce (ITFixed IT32) (ITFixed IT8) "trunc" trunc LTrunc,

@@ -98,6 +90,7 @@ primitives =

9890 iCoerce (ITFixed IT64) ITNative "trunc" trunc LTrunc,

9991 iCoerce ITBig ITNative "trunc" trunc LTrunc,

10092 iCoerce ITNative (ITFixed IT64) "trunc" trunc LTrunc,

93+ iCoerce ITBig ITChar "trunc" trunc LTrunc,

10194

10295 Prim (UN "prim__addFloat") (ty [(AType ATFloat), (AType ATFloat)] (AType ATFloat)) 2 (fBin (+))

10396 (2, LPlus ATFloat) total,

@@ -126,9 +119,9 @@ primitives =

126119 Prim (UN "prim_lenString") (ty [StrType] (AType (ATInt ITNative))) 1 (p_strLen)

127120 (1, LStrLen) total,

128121 -- Conversions

129− Prim (UN "prim__charToInt") (ty [ChType] (AType (ATInt ITNative))) 1 (c_charToInt)

130− (1, LChInt ITNative) total,

131− Prim (UN "prim__intToChar") (ty [(AType (ATInt ITNative))] ChType) 1 (c_intToChar)

122+ Prim (UN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)

123+ (1, LChInt ITChar) total,

124+ Prim (UN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)

132125 (1, LIntCh ITNative) total,

133126 Prim (UN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)

134127 (1, LStrFloat) total,

@@ -158,13 +151,13 @@ primitives =

158151 Prim (UN "prim__floatCeil") (ty [(AType ATFloat)] (AType ATFloat)) 1 (p_floatCeil)

159152 (1, LFCeil) total,

160153

161− Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)

154+ Prim (UN "prim__strHead") (ty [StrType] (AType (ATInt ITChar))) 1 (p_strHead)

162155 (1, LStrHead) partial,

163156 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)

164157 (1, LStrTail) partial,

165− Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)

158+ Prim (UN "prim__strCons") (ty [(AType (ATInt ITChar)), StrType] StrType) 2 (p_strCons)

166159 (2, LStrCons) total,

167− Prim (UN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] ChType) 2 (p_strIndex)

160+ Prim (UN "prim__strIndex") (ty [StrType, (AType (ATInt ITNative))] (AType (ATInt ITChar))) 2 (p_strIndex)

168161 (2, LStrIndex) partial,

169162 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

170163 (1, LStrRev) total,

@@ -175,7 +168,7 @@ primitives =

175168 -- Streams

176169 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

177170 (0, LStdIn) partial

178− ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative]

171+ ] ++ concatMap intOps [ITFixed IT8, ITFixed IT16, ITFixed IT32, ITFixed IT64, ITBig, ITNative, ITChar]

179172 ++ concatMap vecOps [ITVec IT8 16, ITVec IT16 8, ITVec IT32 4, ITVec IT64 2]

180173

181174intOps :: IntTy -> [Prim]

@@ -276,6 +269,7 @@ intTyName :: IntTy -> String

276269intTyName ITNative = "Int"

277270intTyName ITBig = "BigInt"

278271intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)

272+intTyName (ITChar) = "Char"

279273intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count

280274

281275iCmp :: IntTy -> String -> Bool -> ([Const] -> Maybe Const) -> (IntTy -> PrimFn) -> Totality -> Prim

@@ -333,6 +327,7 @@ bsrem (ITFixed IT32) [B32 x, B32 y]

333327bsrem (ITFixed IT64) [B64 x, B64 y]

334328 = Just $ B64 (fromIntegral (fromIntegral x `rem` fromIntegral y :: Int64))

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

330+bsrem ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `rem` (ord y))

336331bsrem (ITVec IT8 _) [B8V x, B8V y]

337332 = Just . B8V $

338333 V.zipWith (\n d -> (fromIntegral (fromIntegral n `rem` fromIntegral d :: Int8))) x y

@@ -357,6 +352,7 @@ bsdiv (ITFixed IT32) [B32 x, B32 y]

357352bsdiv (ITFixed IT64) [B64 x, B64 y]

358353 = Just $ B64 (fromIntegral (fromIntegral x `div` fromIntegral y :: Int64))

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

355+bsdiv ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `div` (ord y))

360356bsdiv (ITVec IT8 _) [B8V x, B8V y]

361357 = Just . B8V $

362358 V.zipWith (\n d -> (fromIntegral (fromIntegral n `div` fromIntegral d :: Int8))) x y

@@ -381,6 +377,7 @@ bashr (ITFixed IT32) [B32 x, B32 y]

381377bashr (ITFixed IT64) [B64 x, B64 y]

382378 = Just $ B64 (fromIntegral (fromIntegral x `shiftR` fromIntegral y :: Int64))

383379bashr ITNative [I x, I y] = Just $ I (x `shiftR` y)

380+bashr ITChar [Ch x, Ch y] = Just $ Ch (chr $ (ord x) `shiftR` (ord y))

384381bashr (ITVec IT8 _) [B8V x, B8V y]

385382 = Just . B8V $

386383 V.zipWith (\n d -> (fromIntegral (fromIntegral n `shiftR` fromIntegral d :: Int8))) x y

@@ -402,6 +399,7 @@ bUn (ITFixed IT32) op [B32 x] = Just $ B32 (op x)

402399bUn (ITFixed IT64) op [B64 x] = Just $ B64 (op x)

403400bUn ITBig op [BI x] = Just $ BI (op x)

404401bUn ITNative op [I x] = Just $ I (op x)

402+bUn ITChar op [Ch x] = Just $ Ch (chr $ op (ord x))

405403bUn (ITVec IT8 _) op [B8V x] = Just . B8V $ V.map op x

406404bUn (ITVec IT16 _) op [B16V x] = Just . B16V $ V.map op x

407405bUn (ITVec IT32 _) op [B32V x] = Just . B32V $ V.map op x

@@ -415,6 +413,7 @@ bitBin (ITFixed IT32) op [B32 x, B32 y] = Just $ B32 (op x y)

415413bitBin (ITFixed IT64) op [B64 x, B64 y] = Just $ B64 (op x y)

416414bitBin ITBig op [BI x, BI y] = Just $ BI (op x y)

417415bitBin ITNative op [I x, I y] = Just $ I (op x y)

416+bitBin ITChar op [Ch x, Ch y] = Just $ Ch (chr $ op (ord x) (ord y))

418417bitBin (ITVec IT8 _) op [B8V x, B8V y] = Just . B8V $ V.zipWith op x y

419418bitBin (ITVec IT16 _) op [B16V x, B16V y] = Just . B16V $ V.zipWith op x y

420419bitBin (ITVec IT32 _) op [B32V x, B32V y] = Just . B32V $ V.zipWith op x y

@@ -428,6 +427,7 @@ bCmp (ITFixed IT32) op [B32 x, B32 y] = Just $ I (if (op x y) then 1 else 0)

428427bCmp (ITFixed IT64) op [B64 x, B64 y] = Just $ I (if (op x y) then 1 else 0)

429428bCmp ITBig op [BI x, BI y] = Just $ I (if (op x y) then 1 else 0)

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

430+bCmp ITChar op [Ch x, Ch y] = Just $ I (if (op x y) then 1 else 0)

431431bCmp (ITVec IT8 _) op [B8V x, B8V y]

432432 = Just . B8V . V.map (\b -> if b then -1 else 0) $ V.zipWith op x y

433433bCmp (ITVec IT16 _) op [B16V x, B16V y]

@@ -445,6 +445,7 @@ toInt (ITFixed IT32) x = B32 (fromIntegral x)

445445toInt (ITFixed IT64) x = B64 (fromIntegral x)

446446toInt ITBig x = BI (fromIntegral x)

447447toInt ITNative x = I (fromIntegral x)

448+toInt ITChar x = Ch (chr $ fromIntegral x)

448449

449450intToInt :: IntTy -> IntTy -> [Const] -> Maybe Const

450451intToInt (ITFixed IT8) out [B8 x] = Just $ toInt out x

@@ -453,6 +454,7 @@ intToInt (ITFixed IT32) out [B32 x] = Just $ toInt out x

453454intToInt (ITFixed IT64) out [B64 x] = Just $ toInt out x

454455intToInt ITBig out [BI x] = Just $ toInt out x

455456intToInt ITNative out [I x] = Just $ toInt out x

457+intToInt ITChar out [Ch x] = Just $ toInt out (ord x)

456458intToInt _ _ _ = Nothing

457459

458460zext :: IntTy -> IntTy -> [Const] -> Maybe Const