git.iko.soy/Idris-dev
on master help sign in
Fix bug in generation of case functions
947c2b3Edwin Brady
lib/prelude/list.idr+6−8
compare with master
unifiedsplit
@@ -40,17 +40,15 @@ map f (x :: xs) = f x :: map f xs;
40
40
41mapMaybe : (a -> Maybe b) -> List a -> List b;
41mapMaybe : (a -> Maybe b) -> List a -> List b;
42mapMaybe f [] = [];
42mapMaybe f [] = [];
43−mapMaybe f (x :: xs) with f x {
43+mapMaybe f (x :: xs) = case f x of {
44− | Nothing = mapMaybe f xs;
44+ Nothing => mapMaybe f xs
45− | Just v = v :: mapMaybe f xs;
45+ | Just v => v :: mapMaybe f xs
46−}
46+ };
47
47
48filter : (y -> Bool) -> List y -> List y;
48filter : (y -> Bool) -> List y -> List y;
49filter pred [] = [];
49filter pred [] = [];
50−filter pred (x :: xs) with (pred x, filter pred xs) {
50+filter pred (x :: xs) = if (pred x) then (x :: filter pred xs)
51− | (True, fxs) = x :: fxs;
51+ else (filter pred xs);
52− | (False, fxs) = fxs;
53−}
54
52
55elem : Eq a => a -> List a -> Bool;
53elem : Eq a => a -> List a -> Bool;
56elem x [] = False;
54elem x [] = False;
src/Idris/AbsSyntax.hs+3−1
@@ -1040,7 +1040,9 @@ aiFn ist fc f as
1040 -- This is where namespaces get resolved by adding PAlternative
1040 -- This is where namespaces get resolved by adding PAlternative
1041 = case lookupCtxtName Nothing f (idris_implicits ist) of
1041 = case lookupCtxtName Nothing f (idris_implicits ist) of
1042 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1042 [(f',ns)] -> mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1043+ [] -> if f `elem` idris_metavars ist
1044+ then PApp fc (PRef fc f) as
1043− [] -> mkPApp fc 1 (PRef fc f) as
1045+ else mkPApp fc 1 (PRef fc f) as
1044 alts -> PAlternative $
1046 alts -> PAlternative $
1045 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1047 map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')
1046 (insertImpl ns as)) alts
1048 (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
49 ds <- checkDef fc ((n, nty):defer)
49 ds <- checkDef fc ((n, nty):defer)
50 addIBC (IBCDef n)
50 addIBC (IBCDef n)
51 addDeferred ds
51 addDeferred ds
52− mapM_ (elabDecl' info) is
52+ mapM_ (elabCaseBlock info) is
53
53
54elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
54elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
55elabData info syn fc (PDatadecl n t_in dcons)
55elabData info syn fc (PDatadecl n t_in dcons)
@@ -63,7 +63,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
63 (erun fc (build i info False n t))
63 (erun fc (build i info False n t))
64 def' <- checkDef fc defer
64 def' <- checkDef fc defer
65 addDeferred def'
65 addDeferred def'
66− mapM_ (elabDecl' info) is
66+ mapM_ (elabCaseBlock info) is
67 (cty, _) <- recheckC ctxt fc [] t'
67 (cty, _) <- recheckC ctxt fc [] t'
68 logLvl 2 $ "---> " ++ show cty
68 logLvl 2 $ "---> " ++ show cty
69 updateContext (addTyDecl n cty) -- temporary, to check cons
69 updateContext (addTyDecl n cty) -- temporary, to check cons
@@ -85,7 +85,7 @@ elabCon info syn (n, t_in, fc)
85 logLvl 2 $ "Rechecking " ++ show t'
85 logLvl 2 $ "Rechecking " ++ show t'
86 def' <- checkDef fc defer
86 def' <- checkDef fc defer
87 addDeferred def'
87 addDeferred def'
88− mapM_ (elabDecl' info) is
88+ mapM_ (elabCaseBlock info) is
89 ctxt <- getContext
89 ctxt <- getContext
90 (cty, _) <- recheckC ctxt fc [] t'
90 (cty, _) <- recheckC ctxt fc [] t'
91 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
91 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
@@ -95,8 +95,8 @@ elabCon info syn (n, t_in, fc)
95elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
95elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
96elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
96elabClauses info fc opts n_in cs_in = let n = liftname info n_in in
97 do let cs = genClauses cs_in
97 do let cs = genClauses cs_in
98− solveDeferred n
99 pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs
98 pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs
99+ solveDeferred n
100 let pats = mapMaybe id pats_in
100 let pats = mapMaybe id pats_in
101 logLvl 3 (showSep "\n" (map (\ (l,r) ->
101 logLvl 3 (showSep "\n" (map (\ (l,r) ->
102 show l ++ " = " ++
102 show l ++ " = " ++
@@ -192,7 +192,7 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)
192 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
192 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
193 def' <- checkDef fc defer
193 def' <- checkDef fc defer
194 addDeferred def'
194 addDeferred def'
195− mapM_ (elabDecl' info) is
195+ mapM_ (elabCaseBlock info) is
196 ctxt <- getContext
196 ctxt <- getContext
197 logLvl 5 $ "Rechecking"
197 logLvl 5 $ "Rechecking"
198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'
198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'
@@ -242,7 +242,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)
242 return (tt, d, is))
242 return (tt, d, is))
243 def' <- checkDef fc defer
243 def' <- checkDef fc defer
244 addDeferred def'
244 addDeferred def'
245− mapM_ (elabDecl' info) is
245+ mapM_ (elabCaseBlock info) is
246 (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')
246 (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')
247 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
247 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
248 windex <- getName
248 windex <- getName
@@ -278,7 +278,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)
278 return (tt, d, is))
278 return (tt, d, is))
279 def' <- checkDef fc defer
279 def' <- checkDef fc defer
280 addDeferred def'
280 addDeferred def'
281− mapM_ (elabDecl' info) is
281+ mapM_ (elabCaseBlock info) is
282 (crhs, crhsty) <- recheckC ctxt fc [] rhs'
282 (crhs, crhsty) <- recheckC ctxt fc [] rhs'
283 return $ Just (clhs, crhs)
283 return $ Just (clhs, crhs)
284 where
284 where
@@ -585,6 +585,9 @@ elabDecl' info (PInstance s f cs n ps t ds)
585 elabInstance info s f cs n ps t ds
585 elabInstance info s f cs n ps t ds
586elabDecl' info (PDirective i) = i
586elabDecl' info (PDirective i) = i
587
587
588+elabCaseBlock info d@(PClauses f o n ps)
589+ = elabDecl' info d
590+
588-- elabDecl' info (PImport i) = loadModule i
591-- elabDecl' info (PImport i) = loadModule i
589
592
590
593
src/Idris/ElabTerm.hs+5−3
@@ -241,7 +241,7 @@ elab ist info pattern tcgen fn tm
241 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args
241 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args
242 -- elaborate case
242 -- elaborate case
243 updateAux (newdef : )
243 updateAux (newdef : )
244− solve -- trace (show newdef) solve
244+ solve
245 where mkCaseName (NS n ns) = NS (mkCaseName n) ns
245 where mkCaseName (NS n ns) = NS (mkCaseName n) ns
246 mkCaseName (UN x) = UN (x ++ "_case")
246 mkCaseName (UN x) = UN (x ++ "_case")
247 mkCaseName (MN i x) = MN i (x ++ "_case")
247 mkCaseName (MN i x) = MN i (x ++ "_case")
@@ -249,9 +249,11 @@ elab ist info pattern tcgen fn tm
249
249
250 caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]
250 caseBlock :: FC -> Name -> [(Name, Binder Term)] -> [(PTerm, PTerm)] -> [PClause]
251 caseBlock fc n env opts
251 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
253 map (mkClause args) opts
253 map (mkClause args) opts
254+ where -- mkarg (MN _ _) = Placeholder
255+ mkarg n = PRef fc n
254− where mkClause args (l, r)
256+ mkClause args (l, r)
255 = PClause n (PApp fc (PRef fc n)
257 = PClause n (PApp fc (PRef fc n)
256 (map pexp args ++ [pexp l])) [] r []
258 (map pexp args ++ [pexp l])) [] r []
257
259