@@ -342,18 +342,20 @@ toPats reflect tc f = reverse (toPat reflect tc (getArgs f)) where
342342 getArgs _ = []
343343
344344toPat :: Bool -> Bool -> [Term] -> [Pat]
345−toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
345+toPat reflect tc = map $ toPat' []
346346 where
347− toPat' (P (DCon t a) nm@(UN n) _) [_,_,arg]
348− | n == txt "Delay" = do arg' <- toPat' arg []
349− return $ PCon nm t [PAny, PAny, arg']
350− toPat' (P (DCon t a) n _) args = do args' <- mapM (\x -> toPat' x []) args
351− return $ PCon n t args'
347+ toPat' [_,_,arg](P (DCon t a) nm@(UN n) _)
348+ | n == txt "Delay"
349+ = PCon nm t [PAny, PAny, toPat' [] arg]
350+
351+ toPat' args (P (DCon t a) n _)
352+ = PCon n t $ map (toPat' []) args
353+
352354 -- n + 1
353− toPat' (P _ (UN pabi) _)
354− [p, Constant (BI 1)] | pabi == txt "prim__addBigInt"
355− = do p' <- toPat' p []
356− return $ PSuc p'
355+ toPat' [p, Constant (BI 1)] (P _ (UN pabi) _)
356+ | pabi == txt "prim__addBigInt"
357+ = PSuc $ toPat' [] p
358+
357359 -- Typecase
358360-- toPat' (P (TCon t a) n _) args | tc
359361-- = do args' <- mapM (\x -> toPat' x []) args
@@ -369,33 +371,24 @@ toPat reflect tc tms = evalState (mapM (\x -> toPat' x []) tms) []
369371-- toPat' (Constant (AType (ATInt (ITFixed n)))) []
370372-- | tc = return $ PCon (UN (fixedN n)) (7 + fromEnum n) [] -- 7-10 inclusive
371373--
372−{-
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
381− ns <- get
382− put $ nub (n : ns)
383− return (PV n ty)
384−
385− toPat' (App f a) args = toPat' f (a : args)
386− toPat' (Constant (AType _)) [] = return PTyPat
387− toPat' (Constant StrType) [] = return PTyPat
388− toPat' (Constant PtrType) [] = return PTyPat
389− toPat' (Constant VoidType) [] = return PTyPat
390− toPat' (Constant x) [] = return $ PConst x
391− toPat' (Bind n (Pi t) sc) [] | reflect && noOccurrence n sc
392− = do t' <- toPat' t []
393− sc' <- toPat' sc []
394− return $ PReflected (sUN "->") (t':sc':[])
395− toPat' (P _ n _) args | reflect
396− = do args' <- mapM (\x -> toPat' x []) args
397− return $ PReflected n args'
398− toPat' t _ = return PAny
374+
375+ toPat' [] (P Bound n ty) = PV n ty
376+ toPat' args (App f a) = toPat' (a : args) f
377+ toPat' [] (Constant (AType _)) = PTyPat
378+ toPat' [] (Constant StrType) = PTyPat
379+ toPat' [] (Constant PtrType) = PTyPat
380+ toPat' [] (Constant VoidType) = PTyPat
381+ toPat' [] (Constant x) = PConst x
382+
383+ toPat' [] (Bind n (Pi t) sc)
384+ | reflect && noOccurrence n sc
385+ = PReflected (sUN "->") [toPat' [] t, toPat' [] sc]
386+
387+ toPat' args (P _ n _)
388+ | reflect
389+ = PReflected n $ map (toPat' []) args
390+
391+ toPat' _ t = PAny
399392
400393 fixedN IT8 = "Bits8"
401394 fixedN IT16 = "Bits16"