947c2b3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix bug in generation of case functions

commit947c2b36ce6513a883944c3717be5fb083552830 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 01:51 (15 years ago) parenta328ff1

4 files changed+24−19

compare with master

unifiedsplit

lib/prelude/list.idr+6−8 src/Idris/AbsSyntax.hs+3−1 src/Idris/ElabDecls.hs+10−7 src/Idris/ElabTerm.hs+5−3

lib/prelude/list.idr+6−8

@@ -40,17 +40,15 @@ map f (x :: xs) = f x :: map f xs;

4040

4141mapMaybe : (a -> Maybe b) -> List a -> List b;

4242mapMaybe f [] = [];

43−mapMaybe f (x :: xs) with f x {

44− | Nothing = mapMaybe f xs;

45− | Just v = v :: mapMaybe f xs;

46−}

43+mapMaybe f (x :: xs) = case f x of {

44+ Nothing => mapMaybe f xs

45+ | Just v => v :: mapMaybe f xs

46+ };

4747

4848filter : (y -> Bool) -> List y -> List y;

4949filter pred [] = [];

50−filter pred (x :: xs) with (pred x, filter pred xs) {

51− | (True, fxs) = x :: fxs;

52− | (False, fxs) = fxs;

53−}

50+filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)

51+ else (filter pred xs);

5452

5553elem : Eq a => a -> List a -> Bool;

5654elem x [] = False;

src/Idris/AbsSyntax.hs+3−1

@@ -1040,7 +1040,9 @@ aiFn ist fc f as

10401040 -- This is where namespaces get resolved by adding PAlternative

10411041 = case lookupCtxtName Nothing f (idris_implicits ist) of

10421042 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1043− [] -> mkPApp fc 1 (PRef fc f) as

1043+ [] -> if f `elem` idris_metavars ist

1044+ then PApp fc (PRef fc f) as

1045+ else mkPApp fc 1 (PRef fc f) as

10441046 alts -> PAlternative $

10451047 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

10461048 (insertImpl ns as)) alts

src/Idris/ElabDecls.hs+10−7

@@ -49,7 +49,7 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

4949 ds <- checkDef fc ((n, nty):defer)

5050 addIBC (IBCDef n)

5151 addDeferred ds

52− mapM_ (elabDecl' info) is

52+ mapM_ (elabCaseBlock info) is

5353

5454elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

5555elabData info syn fc (PDatadecl n t_in dcons)

@@ -63,7 +63,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

6363 (erun fc (build i info False n t))

6464 def' <- checkDef fc defer

6565 addDeferred def'

66− mapM_ (elabDecl' info) is

66+ mapM_ (elabCaseBlock info) is

6767 (cty, _) <- recheckC ctxt fc [] t'

6868 logLvl 2 $ "---> " ++ show cty

6969 updateContext (addTyDecl n cty) -- temporary, to check cons

@@ -85,7 +85,7 @@ elabCon info syn (n, t_in, fc)

8585 logLvl 2 $ "Rechecking " ++ show t'

8686 def' <- checkDef fc defer

8787 addDeferred def'

88− mapM_ (elabDecl' info) is

88+ mapM_ (elabCaseBlock info) is

8989 ctxt <- getContext

9090 (cty, _) <- recheckC ctxt fc [] t'

9191 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

@@ -95,8 +95,8 @@ elabCon info syn (n, t_in, fc)

9595elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

9696elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

9797 do let cs = genClauses cs_in

98− solveDeferred n

9998 pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs

99+ solveDeferred n

100100 let pats = mapMaybe id pats_in

101101 logLvl 3 (showSep "\n" (map (\ (l,r) ->

102102 show l ++ " = " ++

@@ -192,7 +192,7 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

192192 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer

193193 def' <- checkDef fc defer

194194 addDeferred def'

195− mapM_ (elabDecl' info) is

195+ mapM_ (elabCaseBlock info) is

196196 ctxt <- getContext

197197 logLvl 5 $ "Rechecking"

198198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

@@ -242,7 +242,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

242242 return (tt, d, is))

243243 def' <- checkDef fc defer

244244 addDeferred def'

245− mapM_ (elabDecl' info) is

245+ mapM_ (elabCaseBlock info) is

246246 (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')

247247 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

248248 windex <- getName

@@ -278,7 +278,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

278278 return (tt, d, is))

279279 def' <- checkDef fc defer

280280 addDeferred def'

281− mapM_ (elabDecl' info) is

281+ mapM_ (elabCaseBlock info) is

282282 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

283283 return $ Just (clhs, crhs)

284284 where

@@ -585,6 +585,9 @@ elabDecl' info (PInstance s f cs n ps t ds)

585585 elabInstance info s f cs n ps t ds

586586elabDecl' info (PDirective i) = i

587587

588+elabCaseBlock info d@(PClauses f o n ps)

589+ = elabDecl' info d

590+

588591-- elabDecl' info (PImport i) = loadModule i

589592

590593

src/Idris/ElabTerm.hs+5−3

@@ -241,7 +241,7 @@ elab ist info pattern tcgen fn tm

241241 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

242242 -- elaborate case

243243 updateAux (newdef : )

244− solve -- trace (show newdef) solve

244+ solve

245245 where mkCaseName (NS n ns) = NS (mkCaseName n) ns

246246 mkCaseName (UN x) = UN (x ++ "_case")

247247 mkCaseName (MN i x) = MN i (x ++ "_case")

@@ -249,9 +249,11 @@ elab ist info pattern tcgen fn tm

249249

250250 caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]

251251 caseBlock fc n env opts

252− = let args = map (PRef fc) (map fst (init env)) in

252+ = let args = map mkarg (map fst (init env)) in

253253 map (mkClause args) opts

254− where mkClause args (l, r)

254+ where -- mkarg (MN _ _) = Placeholder

255+ mkarg n = PRef fc n

256+ mkClause args (l, r)

255257 = PClause n (PApp fc (PRef fc n)

256258 (map pexp args ++ [pexp l])) [] r []

257259