git.iko.soy/Idris-dev
on master help sign in
More string and char primitives
commitd9834c12f01eda858c8ce5e8eb42388fd83798ea authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 16 Dec 2011, 14:25 (15 years ago) parente06c1c1
4 files changed+48−3
compare with master
unifiedsplit
lib/builtins.idr+20 lib/prelude.idr+1−1 src/Idris/Primitives.hs+25 tutorial/intro.tex+2−2
lib/builtins.idr+20
@@ -107,6 +107,14 @@ instance Eq Float where {
107107 (==) = boolOp prim__eqFloat;
108108}
109109
110+instance Eq Char where {
111+ (==) = boolOp prim__eqChar;
112+}
113+
114+instance Eq String where {
115+ (==) = boolOp prim__eqString;
116+}
117+
110118data Ordering = LT | EQ | GT;
111119
112120class Eq a => Ord a where {
@@ -150,6 +158,18 @@ instance Ord Float where {
150158 GT;
151159}
152160
161+instance Ord Char where {
162+ compare x y = if (x == y) then EQ else
163+ if (boolOp prim__ltChar x y) then LT else
164+ GT;
165+}
166+
167+instance Ord String where {
168+ compare x y = if (x == y) then EQ else
169+ if (boolOp prim__ltString x y) then LT else
170+ GT;
171+}
172+
153173class Eq a => Num a where {
154174 (+) : a -> a -> a;
155175 (-) : a -> a -> a;
lib/prelude.idr+1−1
@@ -136,7 +136,7 @@ putStrLn : String -> IO ();
136136putStrLn x = putStr (x ++ "\n");
137137
138138print : Show a => a -> IO ();
139−print = putStrLn . show;
139+print x = putStrLn (show x);
140140
141141readLine : IO String;
142142readLine = mkForeign (FFun "readStr" Nil FString);
src/Idris/Primitives.hs+25
@@ -53,6 +53,8 @@ strHead x = foreign_ tyChar "strHead" [(x, tyString)]
5353strTail x = foreign_ tyString "strTail" [(x, tyString)]
5454strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]
5555strRev x = foreign_ tyString "strrev" [(x, tyString)]
56+strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
57+strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
5658
5759primitives =
5860 -- operators
@@ -74,6 +76,16 @@ primitives =
7476 (eOp E.gt_),
7577 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
7678 (eOp E.gte_),
79+ Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
80+ (eOp E.eq_),
81+ Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
82+ (eOp E.lt_),
83+ Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
84+ (eOp E.lte_),
85+ Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
86+ (eOp E.gt_),
87+ Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
88+ (eOp E.gte_),
7789 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
7890 (eOpFn tyBigInt tyBigInt "addBig"),
7991 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
@@ -112,6 +124,10 @@ primitives =
112124 (eOp E.gteF_),
113125 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
114126 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
127+ Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
128+ ([E.name "x", E.name "y"], strEq (fun "x") (fun "y")),
129+ Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
130+ ([E.name "x", E.name "y"], strLt (fun "x") (fun "y")),
115131 -- Conversions
116132 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
117133 ([E.name "x"], strToInt (fun "x")),
@@ -166,6 +182,15 @@ bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0
166182 Just $ VConstant (I i)
167183bfBin _ _ = Nothing
168184
185+bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
186+ Just $ VConstant (I i)
187+bcBin _ _ = Nothing
188+
189+bsBin op [VConstant (Str x), VConstant (Str y)]
190+ = let i = (if op x y then 1 else 0) in
191+ Just $ VConstant (I i)
192+bsBin _ _ = Nothing
193+
169194sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
170195sBin _ _ = Nothing
171196
tutorial/intro.tex+2−2
@@ -39,8 +39,8 @@ app : Vect a n -> Vect a m -> Vect a (n + m);
3939\useverb{appendv}
4040
4141
42−This tutorial introduces \Idris{}, a general purpose dependently typed functional
43−programming language.
42+This tutorial introduces \Idris{}, a general purpose functional
43+programming language with dependent types.
4444The goal of the \Idris{} project is to build a dependently typed language suitable
4545for verifable \emph{systems} programming. To this end, \Idris{} is a compiled language
4646which aims to generate efficient executable code. It also has a lightweight foreign