git.iko.soy/Idris-dev
on master help sign in
Merge branch 'AddMissingStrLen' of https://github.com/JanBessai/Idris-dev into JanBessai-AddMissingStrLen

Conflicts: test/reg012/run

commitbac75d0c26b1a783ede06afcca7e344cc0bdf905 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 Mar 2013, 09:55 (14 years ago) parentc2061360e6138f
7 files changed+22−1
compare with master
unifiedsplit
lib/Prelude/Strings.idr+3 src/Idris/Primitives.hs+3 test/reg012/run+1−1 test/reg013/expected+3 test/reg013/reg013.idr+8 test/reg013/run+4 tutorial/idris-tutorial.pdf
lib/Prelude/Strings.idr+3
@@ -115,3 +115,6 @@ unwords' ws = (foldr1 addSpace ws)
115115unwords : List String -> String
116116unwords = pack . unwords' . map unpack
117117
118+length : String -> Nat
119+length = fromInteger . prim_lenString
120+
src/Idris/Primitives.hs+3
@@ -332,6 +332,8 @@ primitives =
332332 (2, LStrEq) total,
333333 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
334334 (2, LStrLt) total,
335+ Prim (UN "prim_lenString") (ty [StrType] IType) 1 (p_strLen)
336+ (1, LStrLen) total,
335337 -- Conversions
336338 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
337339 (1, LStrInt) total,
@@ -622,6 +624,7 @@ p_floatSqrt = p_fPrim sqrt
622624p_floatFloor = p_fPrim (fromInteger . floor)
623625p_floatCeil = p_fPrim (fromInteger . ceiling)
624626
627+p_strLen [VConstant (Str xs)] = Just $ VConstant (I (length xs))
625628p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
626629p_strHead _ = Nothing
627630p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
test/reg012/run+1−1
@@ -1,3 +1,3 @@
11#!/bin/bash
22idris $@ reg012.lidr --check
3−rm -f reg012 *.ibc
3+rm -f *.ibc
test/reg013/expectednew file+3
@@ -0,0 +1,3 @@
1+5
2+1
3+0
test/reg013/reg013.idrnew file+8
@@ -0,0 +1,8 @@
1+module Main
2+
3+main : IO ()
4+main = do
5+ print $ prim_lenString "hallo"
6+ print $ prim_lenString "1"
7+ print $ prim_lenString ""
8+
test/reg013/runnew file+4
@@ -0,0 +1,4 @@
1+#!/bin/bash
2+idris $@ reg013.idr -o reg013
3+./reg013
4+rm -f reg013 *.ibc
tutorial/idris-tutorial.pdf

Binary file not shown.