git.iko.soy/Idris-dev
on master help sign in
Float operations
7123e31Edwin Brady
prims.mi+33−10
compare with master
unifiedsplit
@@ -6,6 +6,13 @@ infixl 7 <<, >>;
6infixl 8 +,-,++,+.,-.;
6infixl 8 +,-,++,+.,-.;
7infixl 9 *,/,*.,/.;
7infixl 9 *,/,*.,/.;
8
8
9+intToBool : Int -> Bool;
10+intToBool 0 = False;
11+intToBool x = True;
12+
13+boolOp : {a:Set} -> (a -> a -> Int) -> a -> a -> Bool;
14+boolOp op x y = intToBool (op x y);
15+
9(+) : Int -> Int -> Int;
16(+) : Int -> Int -> Int;
10(+) = prim__addInt;
17(+) = prim__addInt;
11
18
@@ -18,13 +25,6 @@ infixl 9 *,/,*.,/.;
18div : Int -> Int -> Int;
25div : Int -> Int -> Int;
19div = prim__divInt;
26div = prim__divInt;
20
27
21−intToBool : Int -> Bool;
22−intToBool 0 = False;
23−intToBool x = True;
24−
25−boolOp : (Int -> Int -> Int) -> Int -> Int -> Bool;
26−boolOp op x y = intToBool (op x y);
27−
28(==) : Int -> Int -> Bool;
28(==) : Int -> Int -> Bool;
29(==) = boolOp prim__eqInt;
29(==) = boolOp prim__eqInt;
30
30
@@ -40,7 +40,30 @@ boolOp op x y = intToBool (op x y);
40(>=) : Int -> Int -> Bool;
40(>=) : Int -> Int -> Bool;
41(>=) = boolOp prim__gteInt;
41(>=) = boolOp prim__gteInt;
42
42
43−fact : Int -> Int;
43+(+.) : Float -> Float -> Float;
44−fact 0 = 1;
44+(+.) = prim__addFloat;
45−fact n = n * fact (n - 1);
45+
46+(-.) : Float -> Float -> Float;
47+(-.) = prim__subFloat;
48+
49+(*.) : Float -> Float -> Float;
50+(*.) = prim__mulFloat;
51+
52+(/.) : Float -> Float -> Float;
53+(/.) = prim__divFloat;
54+
55+(==.) : Float -> Float -> Bool;
56+(==.) = boolOp prim__eqFloat;
57+
58+(<.) : Float -> Float -> Bool;
59+(<.) = boolOp prim__ltFloat;
60+
61+(<=.) : Float -> Float -> Bool;
62+(<=.) = boolOp prim__lteFloat;
63+
64+(>.) : Float -> Float -> Bool;
65+(>.) = boolOp prim__gtFloat;
66+
67+(>=.) : Float -> Float -> Bool;
68+(>=.) = boolOp prim__gteFloat;
46
69
src/Idris/Parser.hs+2−1
@@ -189,7 +189,8 @@ pConstant = do reserved "Int"; return IType
189 <|> do reserved "Float"; return FlType
189 <|> do reserved "Float"; return FlType
190 <|> do reserved "String"; return StrType
190 <|> do reserved "String"; return StrType
191 <|> do reserved "Ptr"; return PtrType
191 <|> do reserved "Ptr"; return PtrType
192+ <|> try (do f <- float; return $ Fl f)
192− <|> do i <- natural; return $ I (fromInteger i)
193+ <|> try (do i <- natural; return $ I (fromInteger i))
193
194
194table fixes
195table fixes
195 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [] [PConstant (I 0), x])]]
196 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [] [PConstant (I 0), x])]]
src/Idris/Primitives.hs+28−12
@@ -16,21 +16,37 @@ ty [] x = Constant x
16ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
16ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
17
17
18primitives =
18primitives =
19− [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (vBin (+)),
19+ [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+)),
20− Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (vBin (-)),
20+ Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-)),
21− Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (vBin (*)),
21+ Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*)),
22− Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (vBin (div)),
22+ Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div)),
23− Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (bBin (==)),
23+ Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==)),
24− Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (bBin (<)),
24+ Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<)),
25− Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (bBin (<=)),
25+ Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=)),
26− Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (bBin (>)),
26+ Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>)),
27− Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (bBin (>=))
27+ Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=)),
28+ Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+)),
29+ Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-)),
30+ Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*)),
31+ Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/)),
32+ Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==)),
33+ Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),
34+ Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),
35+ Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>)),
36+ Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))
28 ]
37 ]
29
38
30−vBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
39+iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
31−vBin _ _ = Nothing
40+iBin _ _ = Nothing
32
41
33−bBin op = vBin (\x y -> if (op x y) then 1 else 0)
42+biBin op = iBin (\x y -> if (op x y) then 1 else 0)
43+
44+fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
45+fBin _ _ = Nothing
46+
47+bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
48+ Just $ VConstant (I i)
49+bfBin _ _ = Nothing
34
50
35elabPrim :: Prim -> Idris ()
51elabPrim :: Prim -> Idris ()
36elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)
52elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)