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

idris.cabal+1−1

compare with master

unifiedsplit

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

38

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

40 containers, process, transformers, filepath, directory,

41− epic>=0.1.14

41+ epic>=0.9.1

42

43 Extensions: MultiParamTypeClasses, FunctionalDependencies,

44 FlexibleInstances

lib/builtins.idr+37−24

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

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

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

77

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−

102class Eq a where {

78class Eq a where {

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

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

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

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

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

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

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

110}

86}

111

87

88+instance Eq Integer where {

89+ (==) = boolOp prim__eqBigInt;

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

91+}

92+

112instance Eq Float where {

93instance Eq Float where {

113 (==) = boolOp prim__eqFloat;

94 (==) = boolOp prim__eqFloat;

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

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

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

132 GT;

113 GT;

133}

114}

134

115

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+

135div : Int -> Int -> Int;

148div : Int -> Int -> Int;

136div = prim__divInt;

149div = prim__divInt;

137

150

lib/nat.idr+8−8

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

18mult O y = O;

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

20

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−

29instance Eq Nat where {

21instance Eq Nat where {

30 O == O = True;

22 O == O = True;

31 (S x) == (S y) = x == y;

23 (S x) == (S y) = x == y;

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

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

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

36}

28}

37

29

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+

38instance Ord Nat where {

39 compare O O = EQ;

40 compare O (S k) = LT;

lib/prelude.idr+4

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

20 show = prim__intToStr;

21}

22

23+instance Show Integer where {

24+ show = prim__bigIntToStr;

25+}

26+

23instance Show Float where {

27instance Show Float where {

24 show = prim__floatToStr;

28 show = prim__floatToStr;

25}

29}

src/Core/CaseTree.hs+1

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

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

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

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

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

67

68

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

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

69 if n `elem` ns

70 if n `elem` ns

src/Core/CoreParser.hs+1−1

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

23 "infix", "infixl", "infixr", "prefix",

24 "where", "with", "forall", "syntax", "proof",

25 "using", "params", "namespace", "class", "instance",

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

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

27 }

28

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

src/Core/Evaluate.hs+1−1

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

463

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

465addCasedef n alwaysInline tcase ps ty ctxt

466− = let ps' = simpl ps in

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

467 case simpleCase tcase ps' of

468 CaseDef args sc -> let inl = alwaysInline in

469 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

117addAlist [] ctxt = ctxt

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

119

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

122 deriving Eq

123 deriving Eq

123

124

124data Raw = Var Name

125data Raw = Var Name

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

330

331

331instance Show Const where

332instance Show Const where

332 show (I i) = show i

333 show (I i) = show i

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

333 show (Fl f) = show f

335 show (Fl f) = show f

334 show (Ch c) = show c

336 show (Ch c) = show c

335 show (Str s) = show s

337 show (Str s) = show s

336 show IType = "Int"

338 show IType = "Int"

339+ show BIType = "Integer"

337 show FlType = "Float"

340 show FlType = "Float"

338 show ChType = "Char"

341 show ChType = "Char"

339 show StrType = "String"

342 show StrType = "String"

src/Core/Typecheck.hs+1

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

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

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

58 where constType (I _) = Constant IType

59+ constType (BI _) = Constant BIType

59 constType (Fl _) = Constant FlType

60 constType (Fl _) = Constant FlType

60 constType (Ch _) = Constant ChType

61 constType (Ch _) = Constant ChType

61 constType (Str _) = Constant StrType

62 constType (Str _) = Constant StrType

src/Idris/Compiler.hs+2

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

103

104instance ToEpic Const where

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

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

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

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

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

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

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

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

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

111 epic ChType = return $ con_ 3

112 epic ChType = return $ con_ 3

112 epic StrType = return $ con_ 4

113 epic StrType = return $ con_ 4

113 epic PtrType = return $ con_ 5

114 epic PtrType = return $ con_ 5

115+ epic BIType = return $ con_ 6

114

116

115instance ToEpic ([Name], SC) where

117instance ToEpic ([Name], SC) where

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

118 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

550 _ -> True

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

552 elab' (PLam n Placeholder sc)

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

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

554 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

556 elab' (PPi _ n ty sc)

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

558 claim tyn (RSet 0)

src/Idris/Parser.hs+3−1

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

541 return (DoExp fc e))

542

543pConstant :: IParser Const

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Primitives.hs+46

@@ -30,8 +30,15 @@ ref = E.ref

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

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

32

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+

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

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

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

38intToStr 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)]

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

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

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

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

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

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

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

60 (eOp E.gt_),

67 (eOp E.gt_),

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

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

62 (eOp E.gte_),

69 (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"),

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

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

64 (eOp E.plusF_),

89 (eOp E.plusF_),

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

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

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

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

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

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

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

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

112 ([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")),

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

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

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

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

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

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

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

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

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

103iBin _ _ = Nothing

134iBin _ _ = Nothing

104

135

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+

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

142biBin 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)

106

144

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

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

108fBin _ _ = Nothing

146fBin _ _ = Nothing

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

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

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

120c_strToInt _ = Nothing

158c_strToInt _ = Nothing

121

159

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+

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

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

123c_floatToStr _ = Nothing

169c_floatToStr _ = Nothing

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

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