3b115b2 · Idris-dev · git.iko.soy

decls.mi+9−1

compare with master

unifiedsplit

@@ -17,7 +17,7 @@ data Env : Vect Set n -> Set where

17PLUSTY : Set;

18PLUSTY = Nat -> Nat -> Nat;

19

20−plus : PLUSTY;

20+plus : PLUSTY;

21plus O y = y;

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

23

@@ -38,3 +38,11 @@ tvect = app (test O) (test (S O));

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

39mapPlus = 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+

src/Core/CaseTree.hs+8−4

@@ -37,19 +37,23 @@ data Pat = PCon Name Int [Pat]

37 | PAny

38 deriving Show

39

40+-- If there are repeated variables, take the *last* one (could be name shadowing

41+-- in a where clause, so take the most recent).

42+

40toPats :: Term -> [Pat]

43toPats :: Term -> [Pat]

41−toPats f = map toPat (reverse (getArgs f)) where

44+toPats f = reverse (toPat (getArgs f)) where

42 getArgs (App f a) = a : getArgs f

45 getArgs (App f a) = a : getArgs f

43 getArgs _ = []

46 getArgs _ = []

44

47

45−toPat :: Term -> Pat

48+toPat :: [Term] -> [Pat]

46−toPat tm = evalState (toPat' tm []) []

49+toPat tms = evalState (mapM (\x -> toPat' x []) tms) []

47 where

50 where

48 toPat' (P (DCon t a) n _) args = return $ PCon n t args

51 toPat' (P (DCon t a) n _) args = return $ PCon n t args

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

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

50 if n `elem` ns

53 if n `elem` ns

51 then return PAny

54 then return PAny

55+ else do put (n : ns)

52− else return (PV n)

56+ return (PV n)

53 toPat' (App f a) args = do a' <- toPat' a []

57 toPat' (App f a) args = do a' <- toPat' a []

54 toPat' f (a' : args)

58 toPat' f (a' : args)

55 toPat' (Constant c) args = return $ PConst c

59 toPat' (Constant c) args = return $ PConst c

src/Core/Evaluate.hs+3−2

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

105 evTree :: [Value] -> [(Name, Value)] -> SC -> Maybe Value

106 evTree env amap (UnmatchedCase str) = Nothing

107 evTree env amap (STerm tm)

108+ = let etm = pToVs (map fst amap) tm in

108− = Just $ ev (map snd amap ++ env) (pToVs (map fst amap) tm)

109+ Just $ ev (map snd amap ++ env) etm

109 evTree env amap (Case n alts)

110 evTree env amap (Case n alts)

110 = do v <- lookup n amap

111 = do v <- lookup n amap

111 (altmap, sc) <- chooseAlt v (getValArgs v) alts amap

112 (altmap, sc) <- chooseAlt v (getValArgs v) alts amap

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

125 -- (This is possibly unnecessary since we make unique names and don't

126 -- (This is possibly unnecessary since we make unique names and don't

126 -- allow repeated variables...?)

127 -- allow repeated variables...?)

127 updateAmap newm amap

128 updateAmap newm amap

128− = newm ++ amap --filter (\ (x, _) -> not (elem x (map fst newm))) amap

129+ = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap

129 findTag i [] = Nothing

130 findTag i [] = Nothing

130 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)

131 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)

131 findTag i (_ : xs) = findTag i xs

132 findTag i (_ : xs) = findTag i xs

src/Idris/Delaborate.hs+1−1

@@ -28,7 +28,7 @@ delab ist tm = de [] tm

28

29 mkPApp n args

30 | Just imps <- lookupCtxt n (idris_implicits ist)

31− = PApp (PRef n) (zipWith imp imps args)

31+ = PApp (PRef n) (zipWith imp (imps ++ repeat (PExp undefined)) args)

32 | otherwise = PApp (PRef n) (map PExp args)

33

34 imp (PImp n _) arg = PImp n arg

src/Idris/ElabDecls.hs+2−2

@@ -129,8 +129,8 @@ elabClause info (PClause fname lhs rhs whereblock)

129 info { params = newps,

130 inblock = newb,

131 liftname = (\n -> case lookupCtxt n newb of

132− Nothing -> n

132+ Nothing -> n

133− _ -> MN i (show n)) . l

133+ _ -> MN i (show n)) . l

134 }

135

136elabDecl :: ElabInfo -> PDecl -> Idris ()

src/Idris/REPL.hs+1

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

44 ctxt <- getContext

45 ist <- get

46 let tm' = normalise ctxt [] tm

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

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

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

48 show (delab ist ty))

49 show (delab ist ty))

49process TTShell = do ist <- get

50process TTShell = do ist <- get