868409a · Idris-dev · git.iko.soy

decls.mideleted−48

compare with master

unifiedsplit

@@ -1,48 +0,0 @@

1−infixl 5 +, - ;

2−infixl 6 *, / ;

3−

4−infixr 7 :: ;

5−

6−data Nat = O | S Nat;

7−data List a = Nil | Cons a (List a);

8−

9−data Vect : Set -> Nat -> Set where

10− VNil : Vect a O

11− | (::) : a -> Vect a k -> Vect a (S k);

12−

13−data Env : Vect Set n -> Set where

14− Empty : Env VNil

15− | Extend : {xs : Vect Set n} -> a -> Env xs -> Env (a :: xs);

16−

17−PLUSTY : Set;

18−PLUSTY = Nat -> Nat -> Nat;

19−

20−plus : PLUSTY;

21−plus O y = y;

22−plus (S k) y = S (plus k y);

23−

24−app : Vect a n -> Vect a m -> Vect a (plus n m);

25−app VNil ys = ys;

26−app (x :: xs) ys = x :: app xs ys;

27−

28−map : (a -> b) -> Vect a n -> Vect b n;

29−map f VNil = VNil;

30−map f (x :: xs) = f x :: map f xs;

31−

32−test : Nat -> Vect Nat (S (S O));

33−test n = n :: n :: VNil;

34−

35−tvect : Vect Nat (S (S (S (S O))));

36−tvect = app (test O) (test (S O));

37−

38−mapPlus : Vect Nat n -> Vect Nat n;

39−mapPlus = map (plus (S (S O)));

40−

41−rev : List a -> List a;

42−rev xs = revAcc Nil xs

43− where {

44− revAcc : List a -> List a -> List a;

45− revAcc acc Nil = acc;

46− revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;

47− }

48−

lib/Makefile+1−1

@@ -1,4 +1,4 @@

1check: .PHONY

2− miniidris --check *.idr

2+ miniidris --noprelude --check *.idr

3

4.PHONY:

lib/prelude.idr+2

@@ -1,4 +1,6 @@

1import nat;

2+import list;

3+import io;

2

4

3data Bool = False | True;

5data Bool = False | True;

4

6

prims.mideleted−71

@@ -1,71 +0,0 @@

1−import nat;

2−

3−data Bool = False | True;

4−

5−infixl 5 ==, /=, ==.;

6−infixl 6 <, <=, >, >=, <., <=., >., >=.;

7−infixl 7 <<, >>;

8−infixl 8 +,-,++,+.,-.;

9−infixl 9 *,/,*.,/.;

10−

11−intToBool : Int -> Bool;

12−intToBool 0 = False;

13−intToBool x = True;

14−

15−boolOp : (a -> a -> Int) -> a -> a -> Bool;

16−boolOp op x y = intToBool (op x y);

17−

18−(+) : Int -> Int -> Int;

19−(+) = prim__addInt;

20−

21−(-) : Int -> Int -> Int;

22−(-) = prim__subInt;

23−

24−(*) : Int -> Int -> Int;

25−(*) = prim__mulInt;

26−

27−div : Int -> Int -> Int;

28−div = prim__divInt;

29−

30−(==) : Int -> Int -> Bool;

31−(==) = boolOp prim__eqInt;

32−

33−(<) : Int -> Int -> Bool;

34−(<) = boolOp prim__ltInt;

35−

36−(<=) : Int -> Int -> Bool;

37−(<=) = boolOp prim__lteInt;

38−

39−(>) : Int -> Int -> Bool;

40−(>) = boolOp prim__gtInt;

41−

42−(>=) : Int -> Int -> Bool;

43−(>=) = boolOp prim__gteInt;

44−

45−(+.) : Float -> Float -> Float;

46−(+.) = prim__addFloat;

47−

48−(-.) : Float -> Float -> Float;

49−(-.) = prim__subFloat;

50−

51−(*.) : Float -> Float -> Float;

52−(*.) = prim__mulFloat;

53−

54−(/.) : Float -> Float -> Float;

55−(/.) = prim__divFloat;

56−

57−(==.) : Float -> Float -> Bool;

58−(==.) = boolOp prim__eqFloat;

59−

60−(<.) : Float -> Float -> Bool;

61−(<.) = boolOp prim__ltFloat;

62−

63−(<=.) : Float -> Float -> Bool;

64−(<=.) = boolOp prim__lteFloat;

65−

66−(>.) : Float -> Float -> Bool;

67−(>.) = boolOp prim__gtFloat;

68−

69−(>=.) : Float -> Float -> Bool;

70−(>=.) = boolOp prim__gteFloat;

71−

src/Core/Evaluate.hs+1−1

@@ -69,7 +69,7 @@ eval ctxt genv tm = ev [] tm where

69 ev env (Bind n (NLet t v) sc)

70 = VBind n (Let (ev env t) (ev env v)) $ (\x -> ev (ev env v : env) sc)

71 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)

72− where vbind env t = fmap (ev env) t

72+ where vbind env t = fmap (ev env) t

73 ev env (App f a) = evApply env [ev env a] (ev env f)

74 ev env (Constant c) = VConstant c

75 ev env (Set i) = VSet i

src/Core/TT.hs+1

@@ -283,6 +283,7 @@ instance Show Const where

283 show FlType = "Float"

284 show ChType = "Char"

285 show StrType = "String"

286+ show PtrType = "Ptr"

286

287

287showEnv env t = showEnv' env t False

288showEnv env t = showEnv' env t False

288showEnvDbg env t = showEnv' env t True

289showEnvDbg env t = showEnv' env t True

src/Idris/ElabDecls.hs+2−2

@@ -79,7 +79,7 @@ elabVal info tm

79 = do ctxt <- getContext

80 logLvl 10 (show tm)

81 (tm', _) <- tclift $ elaborate ctxt (MN 0 "val") infP

82− (build info True (infTerm tm))

82+ (build info False (infTerm tm))

83 logLvl 3 ("Value: " ++ show tm')

84 let vtm = getInferTerm tm'

85 logLvl 2 (show vtm)

@@ -188,7 +188,7 @@ elab info pattern tm = do elab' tm

188 [] -> return ()

189

190 elab' PSet = do fill (RSet 0); solve

191− elab' (PConstant c) = do fill (RConstant c); solve

191+ elab' (PConstant c) = do apply (RConstant c) []; solve

192 elab' (PQuote r) = do fill r; solve

193 elab' (PRef n) | pattern && not (inparamBlock n)

194 = try (do apply (Var n) []; solve)

src/Idris/Parser.hs+5−3

@@ -265,8 +265,10 @@ pConstant = do reserved "Int"; return IType

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

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

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

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

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

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

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

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

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

270

272

271table fixes

273table fixes

272 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

274 = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

@@ -293,7 +295,7 @@ pData :: SyntaxInfo -> IParser PDecl

293pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

295pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

294 reserved "where"

296 reserved "where"

295 ty' <- implicit syn tyn ty

297 ty' <- implicit syn tyn ty

296− cons <- sepBy1 (pConstructor syn) (lchar '|')

298+ cons <- sepBy (pConstructor syn) (lchar '|')

297 lchar ';'

299 lchar ';'

298 return $ PData (PDatadecl tyn ty' cons))

300 return $ PData (PDatadecl tyn ty' cons))

299 <|> do reserved "data"; tyn <- pfName; args <- many iName

301 <|> do reserved "data"; tyn <- pfName; args <- many iName

src/Idris/REPL.hs+2−1

@@ -44,9 +44,10 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel t

44 ctxt <- getContext

45 ist <- get

46 let tm' = normalise ctxt [] tm

47+ let ty' = normalise ctxt [] ty

47 logLvl 3 $ "Raw: " ++ show tm'

48 logLvl 3 $ "Raw: " ++ show tm'

48 iputStrLn (show (delab ist tm') ++ " : " ++

49 iputStrLn (show (delab ist tm') ++ " : " ++

49− show (delab ist ty))

50+ show (delab ist ty'))

50process TTShell = do ist <- get

51process TTShell = do ist <- get

51 let shst = initState (tt_ctxt ist)

52 let shst = initState (tt_ctxt ist)

52 shst' <- lift $ runShell shst

53 shst' <- lift $ runShell shst

test.mideleted−29

@@ -1,29 +0,0 @@

1−data N : Set 0 where

2− | O : N

3− | S : N -> N;

4−

5−one : N = S O;

6−two : N = S (S O);

7−three : N = S two;

8−

9−plus : N -> N -> N;

10−

11−data Parity : N -> Set where

12− | even : (n:N) -> (Parity (plus n n))

13− | odd : (n:N) -> (Parity (S (plus n n)));

14−

15−data Vect : (A:Set 0) -> (n:N) -> Set 0 where

16− | Nil : (A:Set 0) -> (Vect A O)

17− | Cons : (A:Set 0) -> (k:N) -> (a:A) -> (Vect A k) -> (Vect A (S k));

18−

19−vtail : (A:Set 0) -> (k:N) -> (Vect A (S k)) -> (Vect A k);

20−vappend : (A:Set) -> (m:N) -> (n:N) -> (Vect A m) -> (Vect A n) -> (Vect A (plus m n));

21−vadd : (m:N) -> (Vect N m) -> (Vect N m) -> (Vect N m);

22−

23−data Infer : Set 0 where

24− | MkInf : (A : Set) -> A -> Infer;

25−

26−data PClause : Set 0 where

27− | MkP : (A : Set) -> A -> A -> PClause;

28−

29−npar : (n:N) -> (p:Parity n) -> N;

wheres.mideleted−38

@@ -1,38 +0,0 @@

1−data Bool = False | True;

2−

3−infixl 5 ==, /=, ==.;

4−infixl 6 <, <=, >, >=, <., <=., >., >=.;

5−infixl 7 <<, >>;

6−infixl 8 +,-,++,+.,-.;

7−infixl 9 *,/,*.,/.;

8−

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−

16−(+) : Int -> Int -> Int;

17−(+) = prim__addInt;

18−

19−(-) : Int -> Int -> Int;

20−(-) = prim__subInt;

21−

22−(*) : Int -> Int -> Int;

23−(*) = prim__mulInt;

24−

25−data Pair x y = MkPair x y;

26−

27−fact : Int -> Pair Int Int;

28−fact x = factAux 1 x

29− where {

30− factAux : Int -> Int -> Pair Int Int;

31− factAux acc 0 = acc'

32− where {

33− acc' : Pair Int Int;

34− acc' = MkPair acc x;

35− }

36− factAux acc n = factAux (acc * n) (n - 1);

37− }

38−