git.iko.soy/Idris-dev
on master help sign in
Purify toPats.
019b608Matus Tejiscak
src/Idris/Core/CaseTree.hs+30−37
compare with master
unifiedsplit
@@ -342,18 +342,20 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
342 getArgs _ = []
342 getArgs _ = []
343
343
344toPat :: Bool -> Bool -> [Term] -> [Pat]
344toPat :: Bool -> Bool -> [Term] -> [Pat]
345−toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
345+toPat reflect tc = map $ toPat' []
346 where
346 where
347− toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]
347+ toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)
348− | n == txt "Delay" = do arg' <- toPat' arg []
348+ | n == txt "Delay"
349− return $ PCon nm t [PAny, PAny, arg']
349+ = PCon nm t [PAny, PAny, toPat' [] arg]
350+
350− toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
351+ toPat' args (P (DCon t a) n _)
351− return $ PCon n t args'
352+ = PCon n t $ map (toPat' []) args
353+
352 -- n + 1
354 -- n + 1
353− toPat' (P _ (UN pabi) _)
355+ toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
354− [p, Constant (BI 1)] | pabi == txt "prim__addBigInt"
356+ | pabi == txt "prim__addBigInt"
355− = do p' <- toPat' p []
357+ = PSuc $ toPat' [] p
356− return $ PSuc p'
358+
357 -- Typecase
359 -- Typecase
358-- toPat' (P (TCon t a) n _) args | tc
360-- toPat' (P (TCon t a) n _) args | tc
359-- = do args' <- mapM (\x -> toPat' x []) args
361-- = do args' <- mapM (\x -> toPat' x []) args
@@ -369,33 +371,24 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
369-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
371-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
370-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
372-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
371--
373--
372−{-
374+
373− toPat' (P Bound n ty) [] = -- trace (show (n, ty)) $
374− do ns <- get
375− if n `elem` ns
376− then return PAny
377− else do put (n : ns)
378− return (PV n ty)
379−-}
380− toPat' (P Bound n ty) [] = do
375+ toPat' [] (P Bound n ty) = PV n ty
381− ns <- get
382− put $ nub (n : ns)
383− return (PV n ty)
384−
385− toPat' (App f a) args = toPat' f (a : args)
376+ toPat' args (App f a) = toPat' (a : args) f
386− toPat' (Constant (AType _)) [] = return PTyPat
377+ toPat' [] (Constant (AType _)) = PTyPat
387− toPat' (Constant StrType) [] = return PTyPat
378+ toPat' [] (Constant StrType) = PTyPat
388− toPat' (Constant PtrType) [] = return PTyPat
379+ toPat' [] (Constant PtrType) = PTyPat
389− toPat' (Constant VoidType) [] = return PTyPat
380+ toPat' [] (Constant VoidType) = PTyPat
390− toPat' (Constant x) [] = return $ PConst x
381+ toPat' [] (Constant x) = PConst x
382+
383+ toPat' [] (Bind n (Pi t) sc)
391− toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
384+ | reflect && noOccurrence n sc
392− = do t' <- toPat' t []
393− sc' <- toPat' sc []
394− return $ PReflected (sUN "->") (t':sc':[])
385+ = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
386+
395− toPat' (P _ n _) args | reflect
387+ toPat' args (P _ n _)
388+ | reflect
396− = do args' <- mapM (\x -> toPat' x []) args
389+ = PReflected n $ map (toPat' []) args
397− return $ PReflected n args'
390+
398− toPat' t _ = return PAny
391+ toPat' _ t = PAny
399
392
400 fixedN IT8 = "Bits8"
393 fixedN IT8 = "Bits8"
401 fixedN IT16 = "Bits16"
394 fixedN IT16 = "Bits16"