2d6c12e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Primitive conversion and showing

commit2d6c12efa08b38463f476f166c01a17aee6ad6ce authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 5 Nov 2011, 10:49 (15 years ago) parent77194b9

2 files changed+55−1

compare with master

unifiedsplit

lib/prelude.idr+29 src/Idris/Primitives.hs+26−1

lib/prelude.idr+29

@@ -24,3 +24,32 @@ data Show : Set -> Set where

2424show : Show a => a -> String;

2525show {{ShowInstance s}} v = s v;

2626

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

3030eOp :: EOp -> ([E.Name], ETm)

3131eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))

3232

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+

3338primitives =

39+ -- operators

3440 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))

3541 (eOp E.plus_),

3642 Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-))

@@ -68,7 +74,16 @@ primitives =

6874 Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))

6975 (eOp E.gteF_),

7076 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"))

7287 ]

7388

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

@@ -86,6 +101,16 @@ bfBin _ _ = Nothing

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

87102sBin _ _ = Nothing

88103

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+

89114elabPrim :: Prim -> Idris ()

90115elabPrim (Prim n ty i def epic)

91116 = do updateContext (addOperator n ty i def)