0bc69fb · Idris-dev · git.iko.soy

lib/builtins.idr+1

compare with master

unifiedsplit

@@ -20,6 +20,7 @@ lazy : a -> a;

20lazy x = x; -- compiled specially

21

22believe_me : a -> b; -- compiled specially as id, use with care!

23+believe_me x = prim__believe_me _ _ x;

23

24

24namespace builtins {

25namespace builtins {

25

26

lib/prelude.idr+1

@@ -8,6 +8,7 @@ import prelude.list;

8import prelude.maybe;

9import prelude.either;

10import prelude.vect;

11+import prelude.strings;

11

12

12-- Show and instances

13-- Show and instances

13

14

lib/prelude/strings.idrnew file+34

@@ -0,0 +1,34 @@

1+module prelude.strings;

2+

3+import builtins;

4+

5+-- Some more complex string operations

6+

7+data StrM : String -> Set where

8+ StrNil : StrM ""

9+ | StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs);

10+

11+strHead' : (x : String) -> so (not (x == "")) -> Char;

12+strHead' x p = prim__strHead x;

13+

14+strTail' : (x : String) -> so (not (x == "")) -> String;

15+strTail' x p = prim__strTail x;

16+

17+-- we need the 'believe_me' because the operations are primitives

18+

19+strM : (x : String) -> StrM x;

20+strM x with choose (not (x == "")) {

21+ strM x | (Left p) = believe_me (StrCons (strHead' x p) (strTail' x p));

22+ strM x | (Right p) = believe_me StrNil;

23+}

24+

25+unpack : String -> List Char;

26+unpack s with strM s {

27+ unpack "" | StrNil = [];

28+ unpack (strCons x xs) | (StrCons _ _) = x :: unpack xs;

29+}

30+

31+pack : List Char -> String;

32+pack [] = "";

33+pack (x :: xs) = strCons x (pack xs);

34+

src/Core/CaseTree.hs+3−10

@@ -78,16 +78,9 @@ toPat tc tms = evalState (mapM (\x -> toPat' x []) tms) []

78 else do put (n : ns)

79 return (PV n)

80 toPat' (App f a) args = toPat' f (a : args)

81− toPat' (Constant c) args

81+ toPat' (Constant (I c)) [] = return $ PConst (I c)

82− | isType c = return PAny

83− | otherwise = return $ PConst c

84− toPat' _ _ = return PAny

82+ toPat' _ _ = return PAny

85−

83+

86− isType (I _) = False

87− isType (Fl _) = False

88− isType (Str _) = False

89− isType (Ch _) = False

90− isType _ = True

91

84

92data Partition = Cons [Clause]

85data Partition = Cons [Clause]

93 | Vars [Clause]

86 | Vars [Clause]

src/Core/TT.hs+1−1

@@ -451,7 +451,7 @@ showEnvDbg env t = showEnv' env t True

451

452showEnv' env t dbg = se 10 env t where

453 se p env (P nt n t) = show n

454− -- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

454+ ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

455 se p env (V i) | i < length env = (show $ fst $ env!!i) ++

456 if dbg then "{" ++ show i ++ "}" else ""

457 | otherwise = "!!V " ++ show i ++ "!!"

src/Core/Typecheck.hs+4−4

@@ -20,16 +20,16 @@ convertsC ctxt env x y

20 (finalise (normalise ctxt env y))

21 if c then return ()

22 else fail ("Can't convert between " ++

23− showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

23+ showEnvDbg env (finalise (normalise ctxt env x)) ++ " and " ++

24− showEnv env (finalise (normalise ctxt env y)))

24+ showEnvDbg env (finalise (normalise ctxt env y)))

25

26converts :: Context -> Env -> Term -> Term -> TC ()

27converts ctxt env x y = if (finalise (normalise ctxt env x) ==

28 finalise (normalise ctxt env y))

29 then return ()

30 else fail ("Can't convert between " ++

31− showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

31+ showEnvDbg env (finalise (normalise ctxt env x)) ++ " and " ++

32− showEnv env (finalise (normalise ctxt env y)))

32+ showEnvDbg env (finalise (normalise ctxt env y)))

33

34isSet :: Context -> Env -> Term -> TC ()

35isSet ctxt env tm = isSet' (normalise ctxt env tm)

src/Idris/Compiler.hs+1−3

@@ -13,7 +13,7 @@ import Control.Monad.State

13import Epic.Epic hiding (Term, Type, Name, fn, compile)

14import qualified Epic.Epic as E

15

16−primDefs = [UN "mkForeign", UN "FalseElim", UN "believe_me"]

16+primDefs = [UN "mkForeign", UN "FalseElim"]

17

18compile :: FilePath -> Idris ()

19compile f = do ds <- mkDecls

@@ -61,8 +61,6 @@ instance ToEpic (TT Name) where

61 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm

62 = do arg' <- epic' env arg

63 return $ lazy_ arg'

64− | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm

65− = epic' env arg

66 | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm

64 | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm

67 = epic' env v

65 = epic' env v

68 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

66 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

src/Idris/Parser.hs+3

@@ -886,10 +886,13 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

886 block b [a] = PElabError "Last statement in do block must be an expression"

887 block b (DoBind fc n tm : rest)

888 = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]

889+ block b (DoLet fc n tm : rest)

890+ = PLet n Placeholder tm (block b rest)

889 block b (DoExp fc tm : rest)

891 block b (DoExp fc tm : rest)

890 = PApp fc (PRef fc b)

892 = PApp fc (PRef fc b)

891 [pexp tm,

893 [pexp tm,

892 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

894 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

895+ block b _ = PElabError "Invalid statement in do block"

893expandDo dsl t = t

896expandDo dsl t = t

894

897

895

898

src/Idris/Primitives.hs+11−1

@@ -22,6 +22,10 @@ data Prim = Prim { p_name :: Name,

22ty [] x = Constant x

23ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)

24

25+believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))

26+ (Bind (UN "b") (Pi (Set (UVar (-2))))

27+ (Bind (UN "x") (Pi (V 1)) (V 1)))

28+

25type ETm = E.Term

29type ETm = E.Term

26type EOp = E.Op

30type EOp = E.Op

27

31

@@ -160,9 +164,15 @@ primitives =

160 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

164 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)

161 ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")),

165 ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i")),

162 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

166 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

163− ([E.name "x"], strRev (fun "x"))

167+ ([E.name "x"], strRev (fun "x")),

168+

169+ Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)

170+ ([E.name "a", E.name "b", E.name "x"], fun "x")

164 ]

171 ]

165

172

173+p_believeMe [_,_,x] = Just x

174+p_believeMe _ = Nothing

175+

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

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

167iBin _ _ = Nothing

177iBin _ _ = Nothing

168

178