4931c20 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added Integer (but an Epic bug prevents them compiling properly)

commit4931c200f75073a26ba460e3cd7e2016be0185c9 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 16 Nov 2011, 00:23 (15 years ago) parente530718

13 files changed+112−40

compare with master

unifiedsplit

idris.cabal+1−1 lib/builtins.idr+37−24 lib/nat.idr+8−8 lib/prelude.idr+4 src/Core/CaseTree.hs+1 src/Core/CoreParser.hs+1−1 src/Core/Evaluate.hs+1−1 src/Core/TT.hs+5−2 src/Core/Typecheck.hs+1 src/Idris/Compiler.hs+2 src/Idris/ElabDecls.hs+2−2 src/Idris/Parser.hs+3−1 src/Idris/Primitives.hs+46

idris.cabal+1−1

@@ -38,7 +38,7 @@ Executable idris

3838

3939 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

4040 containers, process, transformers, filepath, directory,

41− epic>=0.1.14

41+ epic>=0.9.1

4242

4343 Extensions: MultiParamTypeClasses, FunctionalDependencies,

4444 FlexibleInstances

lib/builtins.idr+37−24

@@ -75,30 +75,6 @@ intToBool x = True;

7575boolOp : (a -> a -> Int) -> a -> a -> Bool;

7676boolOp op x y = intToBool (op x y);

7777

78−class Num a where {

79− (+) : a -> a -> a;

80− (-) : a -> a -> a;

81− (*) : a -> a -> a;

82−

83− fromInteger : Int -> a;

84−}

85−

86−instance Num Int where {

87− (+) = prim__addInt;

88− (-) = prim__subInt;

89− (*) = prim__mulInt;

90−

91− fromInteger = id;

92−}

93−

94−instance Num Float where {

95− (+) = prim__addFloat;

96− (-) = prim__subFloat;

97− (*) = prim__mulFloat;

98−

99− fromInteger = prim__intToFloat;

100−}

101−

10278class Eq a where {

10379 (==) : a -> a -> Bool;

10480 (/=) : a -> a -> Bool;

@@ -109,6 +85,11 @@ instance Eq Int where {

10985 (/=) x y = not (x == y);

11086}

11187

88+instance Eq Integer where {

89+ (==) = boolOp prim__eqBigInt;

90+ (/=) x y = not (x == y);

91+}

92+

11293instance Eq Float where {

11394 (==) = boolOp prim__eqFloat;

11495 (/=) x y = not (x == y);

@@ -132,6 +113,38 @@ instance Ord Float where {

132113 GT;

133114}

134115

116+class Eq a => Num a where {

117+ (+) : a -> a -> a;

118+ (-) : a -> a -> a;

119+ (*) : a -> a -> a;

120+

121+ fromInteger : Int -> a;

122+}

123+

124+instance Num Int where {

125+ (+) = prim__addInt;

126+ (-) = prim__subInt;

127+ (*) = prim__mulInt;

128+

129+ fromInteger = id;

130+}

131+

132+instance Num Integer where {

133+ (+) = prim__addBigInt;

134+ (-) = prim__subBigInt;

135+ (*) = prim__mulBigInt;

136+

137+ fromInteger = prim__intToBigInt;

138+}

139+

140+instance Num Float where {

141+ (+) = prim__addFloat;

142+ (-) = prim__subFloat;

143+ (*) = prim__mulFloat;

144+

145+ fromInteger = prim__intToFloat;

146+}

147+

135148div : Int -> Int -> Int;

136149div = prim__divInt;

137150

lib/nat.idr+8−8

@@ -18,14 +18,6 @@ mult : Nat -> Nat -> Nat;

1818mult O y = O;

1919mult (S k) y = plus y (mult k y);

2020

21−instance Num Nat where {

22− (+) = plus;

23− (-) = sub;

24− (*) = mult;

25−

26− fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;

27−}

28−

2921instance Eq Nat where {

3022 O == O = True;

3123 (S x) == (S y) = x == y;

@@ -35,6 +27,14 @@ instance Eq Nat where {

3527 x /= y = not (x == y);

3628}

3729

30+instance Num Nat where {

31+ (+) = plus;

32+ (-) = sub;

33+ (*) = mult;

34+

35+ fromInteger n = if (n > 0) then (S (fromInteger (n-1))) else O;

36+}

37+

3838instance Ord Nat where {

3939 compare O O = EQ;

4040 compare O (S k) = LT;

lib/prelude.idr+4

@@ -20,6 +20,10 @@ instance Show Int where {

2020 show = prim__intToStr;

2121}

2222

23+instance Show Integer where {

24+ show = prim__bigIntToStr;

25+}

26+

2327instance Show Float where {

2428 show = prim__floatToStr;

2529}

src/Core/CaseTree.hs+1

@@ -64,6 +64,7 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

6464 toPat' (Constant ChType) [] | tc = return $ PCon (UN ["Char"]) 3 []

6565 toPat' (Constant StrType) [] | tc = return $ PCon (UN ["String"]) 4 []

6666 toPat' (Constant PtrType) [] | tc = return $ PCon (UN ["Ptr"]) 5 []

67+ toPat' (Constant BIType) [] | tc = return $ PCon (UN ["Integer"]) 6 []

6768

6869 toPat' (P Bound n _) [] = do ns <- get

6970 if n `elem` ns

src/Core/CoreParser.hs+1−1

@@ -23,7 +23,7 @@ idrisDef = haskellDef {

2323 "infix", "infixl", "infixr", "prefix",

2424 "where", "with", "forall", "syntax", "proof",

2525 "using", "params", "namespace", "class", "instance",

26− "Int", "Float", "Char", "String", "Ptr"]

26+ "Int", "Integer", "Float", "Char", "String", "Ptr"]

2727 }

2828

2929iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

src/Core/Evaluate.hs+1−1

@@ -463,7 +463,7 @@ addDatatype (Data n tag ty cons) ctxt

463463

464464addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

465465addCasedef n alwaysInline tcase ps ty ctxt

466− = let ps' = simpl ps in

466+ = let ps' = ps in -- simpl ps in

467467 case simpleCase tcase ps' of

468468 CaseDef args sc -> let inl = alwaysInline in

469469 addDef n (CaseOp inl ty ps args sc) ctxt

src/Core/TT.hs+5−2

@@ -117,8 +117,9 @@ addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

117117addAlist [] ctxt = ctxt

118118addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

119119

120−data Const = I Int | Fl Double | Ch Char | Str String

120+data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

122+ | PtrType

122123 deriving Eq

123124

124125data Raw = Var Name

@@ -330,10 +331,12 @@ instance (Eq n, Show n) => Show (TT n) where

330331

331332instance Show Const where

332333 show (I i) = show i

334+ show (BI i) = show i ++ "L"

333335 show (Fl f) = show f

334336 show (Ch c) = show c

335337 show (Str s) = show s

336338 show IType = "Int"

339+ show BIType = "Integer"

337340 show FlType = "Float"

338341 show ChType = "Char"

339342 show StrType = "String"

src/Core/Typecheck.hs+1

@@ -56,6 +56,7 @@ check ctxt env (RApp f a)

5656check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

5757check ctxt env (RConstant c) = return (Constant c, constType c)

5858 where constType (I _) = Constant IType

59+ constType (BI _) = Constant BIType

5960 constType (Fl _) = Constant FlType

6061 constType (Ch _) = Constant ChType

6162 constType (Str _) = Constant StrType

src/Idris/Compiler.hs+2

@@ -103,6 +103,7 @@ mkEty "FUnit" = tyUnit

103103

104104instance ToEpic Const where

105105 epic (I i) = return (int i)

106+ epic (BI i) = return (bigint i)

106107 epic (Fl f) = return (float f)

107108 epic (Str s) = return (str s)

108109 epic (Ch c) = return (char c)

@@ -111,6 +112,7 @@ instance ToEpic Const where

111112 epic ChType = return $ con_ 3

112113 epic StrType = return $ con_ 4

113114 epic PtrType = return $ con_ 5

115+ epic BIType = return $ con_ 6

114116

115117instance ToEpic ([Name], SC) where

116118 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree

src/Idris/ElabDecls.hs+2−2

@@ -550,9 +550,9 @@ elab ist info pattern tm

550550 _ -> True

551551 elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve

552552 elab' (PLam n Placeholder sc)

553− = do attack; intro (Just n); elabE sc; solve

553+ = do attack; intro (Just n); elabE sc; solve

554554 elab' (PPi _ n Placeholder sc)

555− = do attack; arg n (MN 0 "ty"); elabE sc; solve

555+ = do attack; arg n (MN 0 "ty"); elabE sc; solve

556556 elab' (PPi _ n ty sc)

557557 = do attack; tyn <- unique_hole (MN 0 "ty")

558558 claim tyn (RSet 0)

src/Idris/Parser.hs+3−1

@@ -541,12 +541,14 @@ pDo syn

541541 return (DoExp fc e))

542542

543543pConstant :: IParser Const

544−pConstant = do reserved "Int"; return IType

544+pConstant = do reserved "Integer";return BIType

545+ <|> do reserved "Int"; return IType

545546 <|> do reserved "Char"; return ChType

546547 <|> do reserved "Float"; return FlType

547548 <|> do reserved "String"; return StrType

548549 <|> do reserved "Ptr"; return PtrType

549550 <|> try (do f <- float; return $ Fl f)

551+ <|> try (do i <- natural; lchar 'L'; return $ BI i)

550552 <|> try (do i <- natural; return $ I (fromInteger i))

551553 <|> try (do s <- strlit; return $ Str s)

552554 <|> try (do c <- chlit; return $ Ch c)

src/Idris/Primitives.hs+46

@@ -30,8 +30,15 @@ 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+eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)

34+eOpFn ty rty op = ([E.name "x", E.name "y"],

35+ foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])

36+

3337strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]

3438intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]

39+intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]

40+strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]

41+bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]

3542strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]

3643floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]

3744intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]

@@ -60,6 +67,24 @@ primitives =

6067 (eOp E.gt_),

6168 Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=))

6269 (eOp E.gte_),

70+ Prim (UN ["prim__addBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (+))

71+ (eOpFn tyBigInt tyBigInt "addBig"),

72+ Prim (UN ["prim__subBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (-))

73+ (eOpFn tyBigInt tyBigInt "subBig"),

74+ Prim (UN ["prim__mulBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (*))

75+ (eOpFn tyBigInt tyBigInt "mulBig"),

76+ Prim (UN ["prim__divBigInt"]) (ty [BIType, BIType] BIType) 2 (bBin (div))

77+ (eOpFn tyBigInt tyBigInt "divBig"),

78+ Prim (UN ["prim__eqBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (==))

79+ (eOpFn tyBigInt tyInt "eqBig"),

80+ Prim (UN ["prim__ltBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (<))

81+ (eOpFn tyBigInt tyInt "ltBig"),

82+ Prim (UN ["prim__lteBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (<=))

83+ (eOpFn tyBigInt tyInt "leBig"),

84+ Prim (UN ["prim__gtBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (>))

85+ (eOpFn tyBigInt tyInt "gtBig"),

86+ Prim (UN ["prim__gtBigInt"]) (ty [BIType, BIType] IType) 2 (bbBin (>=))

87+ (eOpFn tyBigInt tyInt "geBig"),

6388 Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+))

6489 (eOp E.plusF_),

6590 Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-))

@@ -85,6 +110,12 @@ primitives =

85110 ([E.name "x"], strToInt (fun "x")),

86111 Prim (UN ["prim__intToStr"]) (ty [IType] StrType) 1 (c_intToStr)

87112 ([E.name "x"], intToStr (fun "x")),

113+ Prim (UN ["prim__intToBigInt"]) (ty [IType] BIType) 1 (c_intToBigInt)

114+ ([E.name "x"], intToBigInt (fun "x")),

115+ Prim (UN ["prim__strToBigInt"]) (ty [StrType] BIType) 1 (c_strToBigInt)

116+ ([E.name "x"], strToBigInt (fun "x")),

117+ Prim (UN ["prim__bigIntToStr"]) (ty [BIType] StrType) 1 (c_bigIntToStr)

118+ ([E.name "x"], bigIntToStr (fun "x")),

88119 Prim (UN ["prim__strToFloat"]) (ty [StrType] FlType) 1 (c_strToFloat)

89120 ([E.name "x"], strToFloat (fun "x")),

90121 Prim (UN ["prim__floatToStr"]) (ty [FlType] StrType) 1 (c_floatToStr)

@@ -102,7 +133,14 @@ primitives =

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

103134iBin _ _ = Nothing

104135

136+bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))

137+bBin _ _ = Nothing

138+

139+bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))

140+bBini _ _ = Nothing

141+

105142biBin op = iBin (\x y -> if (op x y) then 1 else 0)

143+bbBin op = bBini (\x y -> if (op x y) then 1 else 0)

106144

107145fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))

108146fBin _ _ = Nothing

@@ -119,6 +157,14 @@ c_intToStr _ = Nothing

119157c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))

120158c_strToInt _ = Nothing

121159

160+c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))

161+c_intToBigInt _ = Nothing

162+

163+c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))

164+c_bigIntToStr _ = Nothing

165+c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x))

166+c_strToBigInt _ = Nothing

167+

122168c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))

123169c_floatToStr _ = Nothing

124170c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))