git.iko.soy/Idris-dev
on master help sign in
Primitive conversion and showing
2d6c12eEdwin Brady
lib/prelude.idr+29
compare with master
unifiedsplit
@@ -24,3 +24,32 @@ data Show : Set -> Set where
24show : Show a => a -> String;
24show : Show a => a -> String;
25show {{ShowInstance s}} v = s v;
25show {{ShowInstance s}} v = s v;
26
26
27+instance showNat : Show Nat;
28+instance showNat = ShowInstance show where {
29+ show : Nat -> String;
30+ show O = "O";
31+ show (S k) = "s" ++ show k;
32+}
33+
34+instance showInt : Show Int;
35+instance showInt = ShowInstance show where {
36+ show : Int -> String;
37+ show = prim__intToStr;
38+}
39+
40+instance showFloat : Show Float;
41+instance showFloat = ShowInstance show where {
42+ show : Float -> String;
43+ show = prim__floatToStr;
44+}
45+
46+instance showList : Show a => Show (List a);
47+instance showList = ShowInstance lshow where {
48+ lshow : Show a => List a -> String;
49+ lshow xs = "[" ++ show' xs ++ "]" where {
50+ show' : Show a => List a -> String;
51+ show' Nil = "";
52+ show' (Cons x Nil) = show x;
53+ show' (Cons x xs) = show x ++ ", " ++ show' xs;
54+ }
55+}
src/Idris/Primitives.hs+26−1
@@ -30,7 +30,13 @@ ref = E.ref
30eOp :: EOp -> ([E.Name], ETm)
30eOp :: EOp -> ([E.Name], ETm)
31eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
31eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
32
32
33+strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]
34+intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
35+strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
36+floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]
37+
33primitives =
38primitives =
39+ -- operators
34 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))
40 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))
35 (eOp E.plus_),
41 (eOp E.plus_),
36 Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))
42 Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))
@@ -68,7 +74,16 @@ primitives =
68 Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))
74 Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))
69 (eOp E.gteF_),
75 (eOp E.gteF_),
70 Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))
76 Prim (UN ["prim__concat"]) (ty [StrType, StrType] StrType) 2 (sBin (++))
71− ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")
77+ ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
78+ -- Conversions
79+ Prim (UN ["prim__strToInt"]) (ty [StrType] IType) 1 (c_strToInt)
80+ ([E.name "x"], strToInt (fun "x")),
81+ Prim (UN ["prim__intToStr"]) (ty [IType] StrType) 1 (c_intToStr)
82+ ([E.name "x"], intToStr (fun "x")),
83+ Prim (UN ["prim__strToFloat"]) (ty [StrType] FlType) 1 (c_strToFloat)
84+ ([E.name "x"], strToFloat (fun "x")),
85+ Prim (UN ["prim__floatToStr"]) (ty [FlType] StrType) 1 (c_floatToStr)
86+ ([E.name "x"], floatToStr (fun "x"))
72 ]
87 ]
73
88
74iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
89iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
@@ -86,6 +101,16 @@ bfBin _ _ = Nothing
86sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
101sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
87sBin _ _ = Nothing
102sBin _ _ = Nothing
88
103
104+c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
105+c_intToStr _ = Nothing
106+c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))
107+c_strToInt _ = Nothing
108+
109+c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
110+c_floatToStr _ = Nothing
111+c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))
112+c_strToFloat _ = Nothing
113+
89elabPrim :: Prim -> Idris ()
114elabPrim :: Prim -> Idris ()
90elabPrim (Prim n ty i def epic)
115elabPrim (Prim n ty i def epic)
91 = do updateContext (addOperator n ty i def)
116 = do updateContext (addOperator n ty i def)