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

git.iko.soy/Idris-dev

Fixed pattern matching and delaborator bug

commit3b115b267f1d751f4a17fb45dfe36f0bd9b17aa9 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 13 Oct 2011, 16:35 (15 years ago) parent083fc70

6 files changed+24−10

compare with master

unifiedsplit

decls.mi+9−1 src/Core/CaseTree.hs+8−4 src/Core/Evaluate.hs+3−2 src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+2−2 src/Idris/REPL.hs+1

decls.mi+9−1

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

1717PLUSTY : Set;

1818PLUSTY = Nat -> Nat -> Nat;

1919

20−plus : PLUSTY;

20+plus : PLUSTY;

2121plus O y = y;

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

2323

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

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

3939mapPlus = map (plus (S (S O)));

4040

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]

3737 | PAny

3838 deriving Show

3939

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+

4043toPats :: Term -> [Pat]

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

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

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

4346 getArgs _ = []

4447

45−toPat :: Term -> Pat

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

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

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

4750 where

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

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

5053 if n `elem` ns

5154 then return PAny

52− else return (PV n)

55+ else do put (n : ns)

56+ return (PV n)

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

5458 toPat' f (a' : args)

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

src/Core/Evaluate.hs+3−2

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

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

106106 evTree env amap (UnmatchedCase str) = Nothing

107107 evTree env amap (STerm tm)

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

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

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

109110 evTree env amap (Case n alts)

110111 = do v <- lookup n amap

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

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

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

126127 -- allow repeated variables...?)

127128 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

129130 findTag i [] = Nothing

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

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

src/Idris/Delaborate.hs+1−1

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

2828

2929 mkPApp n args

3030 | 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)

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

3333

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

src/Idris/ElabDecls.hs+2−2

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

129129 info { params = newps,

130130 inblock = newb,

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

132− Nothing -> n

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

132+ Nothing -> n

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

134134 }

135135

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

src/Idris/REPL.hs+1

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

4444 ctxt <- getContext

4545 ist <- get

4646 let tm' = normalise ctxt [] tm

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

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

4849 show (delab ist ty))

4950process TTShell = do ist <- get