git.iko.soy/Idris-dev
on master help sign in
Float operations
commit7123e3111430a70ddc1ac6cac1cdf83e504a3a98 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 11 Oct 2011, 15:25 (15 years ago) parenta805f47
3 files changed+63−23
compare with master
unifiedsplit
prims.mi+33−10 src/Idris/Parser.hs+2−1 src/Idris/Primitives.hs+28−12
prims.mi+33−10
@@ -6,6 +6,13 @@ infixl 7 <<, >>;
66infixl 8 +,-,++,+.,-.;
77infixl 9 *,/,*.,/.;
88
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+
916(+) : Int -> Int -> Int;
1017(+) = prim__addInt;
1118
@@ -18,13 +25,6 @@ infixl 9 *,/,*.,/.;
1825div : Int -> Int -> Int;
1926div = prim__divInt;
2027
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−
2828(==) : Int -> Int -> Bool;
2929(==) = boolOp prim__eqInt;
3030
@@ -40,7 +40,30 @@ boolOp op x y = intToBool (op x y);
4040(>=) : Int -> Int -> Bool;
4141(>=) = boolOp prim__gteInt;
4242
43−fact : Int -> Int;
44−fact 0 = 1;
45−fact n = n * fact (n - 1);
43+(+.) : Float -> Float -> Float;
44+(+.) = prim__addFloat;
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;
4669
src/Idris/Parser.hs+2−1
@@ -189,7 +189,8 @@ pConstant = do reserved "Int"; return IType
189189 <|> do reserved "Float"; return FlType
190190 <|> do reserved "String"; return StrType
191191 <|> do reserved "Ptr"; return PtrType
192− <|> do i <- natural; return $ I (fromInteger i)
192+ <|> try (do f <- float; return $ Fl f)
193+ <|> try (do i <- natural; return $ I (fromInteger i))
193194
194195table fixes
195196 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [] [PConstant (I 0), x])]]
src/Idris/Primitives.hs+28−12
@@ -16,21 +16,37 @@ ty [] x = Constant x
1616ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
1717
1818primitives =
19− [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (vBin (+)),
20− Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (vBin (-)),
21− Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (vBin (*)),
22− Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (vBin (div)),
23− Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (bBin (==)),
24− Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (bBin (<)),
25− Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (bBin (<=)),
26− Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (bBin (>)),
27− Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (bBin (>=))
19+ [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+)),
20+ Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-)),
21+ Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*)),
22+ Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div)),
23+ Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==)),
24+ Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<)),
25+ Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=)),
26+ Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>)),
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 (>=))
2837 ]
2938
30−vBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
31−vBin _ _ = Nothing
39+iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
40+iBin _ _ = Nothing
3241
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
3450
3551elabPrim :: Prim -> Idris ()
3652elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)