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

git.iko.soy/Idris-dev

Added prelude.strings, made believe_me primitive

commit0bc69fbfd323877b32ae2cd159367985ea008c30 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 17 Dec 2011, 18:17 (15 years ago) parent124f0e4

9 files changed+59−19

compare with master

unifiedsplit

lib/builtins.idr+1 lib/prelude.idr+1 lib/prelude/strings.idr+34 src/Core/CaseTree.hs+3−10 src/Core/TT.hs+1−1 src/Core/Typecheck.hs+4−4 src/Idris/Compiler.hs+1−3 src/Idris/Parser.hs+3 src/Idris/Primitives.hs+11−1

lib/builtins.idr+1

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

2020lazy x = x; -- compiled specially

2121

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

23+believe_me x = prim__believe_me _ _ x;

2324

2425namespace builtins {

2526

lib/prelude.idr+1

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

88import prelude.maybe;

99import prelude.either;

1010import prelude.vect;

11+import prelude.strings;

1112

1213-- Show and instances

1314

lib/prelude/strings.idrnew file+34

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

1+module prelude.strings;

3+import builtins;

5+-- Some more complex string operations

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) []

7878 else do put (n : ns)

7979 return (PV n)

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

81− toPat' (Constant c) args

82− | isType c = return PAny

83− | otherwise = return $ PConst c

84− toPat' _ _ = return PAny

85−

86− isType (I _) = False

87− isType (Fl _) = False

88− isType (Str _) = False

89− isType (Ch _) = False

90− isType _ = True

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

82+ toPat' _ _ = return PAny

83+

9184

9285data Partition = Cons [Clause]

9386 | Vars [Clause]

src/Core/TT.hs+1−1

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

451451

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

453453 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 ""

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

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

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

src/Core/Typecheck.hs+4−4

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

2020 (finalise (normalise ctxt env y))

2121 if c then return ()

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

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

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

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

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

2525

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

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

2828 finalise (normalise ctxt env y))

2929 then return ()

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

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

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

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

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

3333

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

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

src/Idris/Compiler.hs+1−3

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

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

1414import qualified Epic.Epic as E

1515

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

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

1717

1818compile :: FilePath -> Idris ()

1919compile f = do ds <- mkDecls

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

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

6262 = do arg' <- epic' env arg

6363 return $ lazy_ arg'

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

65− = epic' env arg

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

6765 = epic' env v

6866 | (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

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

887887 block b (DoBind fc n tm : rest)

888888 = 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)

889891 block b (DoExp fc tm : rest)

890892 = PApp fc (PRef fc b)

891893 [pexp tm,

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

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

893896expandDo dsl t = t

894897

895898

src/Idris/Primitives.hs+11−1

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

2222ty [] x = Constant x

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

2424

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+

2529type ETm = E.Term

2630type EOp = E.Op

2731

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

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

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

162166 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")

164171 ]

165172

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

174+p_believeMe _ = Nothing

175+

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

167177iBin _ _ = Nothing

168178