@@ -17,21 +17,6 @@ import Debug.Trace
1717
1818import Control.Monad.State
1919
20−-- Generate the LHSes which are missing from a case tree
21−-- Eliminate the ones which cannot be well typed
22−
23−genMissing :: Name -> [Name] -> SC -> Idris [PTerm]
24−genMissing fn args sc
25− = do sc' <- expandTree sc
26− logLvl 5 $ "Checking missing cases for " ++
27− show fn ++ "\n" ++ (show sc')
28− (got, missing) <- gm fn (map (\x -> P Bound x Erased) args) sc'
29− return $ filter (\x -> not (x `elem` got)) missing
30−
31−-- Make a term to feed to the pattern matcher from a LHS declared impossible
32−-- (we can't type check it, but we need the case analysis to check for
33−-- covering...)
34−
3520mkPatTm :: PTerm -> Idris Term
3621mkPatTm t = do i <- getIState
3722 let timp = addImpl' True [] [] i t
@@ -48,101 +33,6 @@ mkPatTm t = do i <- getIState
4833 put (v + 1)
4934 return (P Bound (MN v "imp") Erased)
5035
51−mkPTerm :: Name -> [TT Name] -> Idris PTerm
52−mkPTerm f args = do i <- getIState
53− let fapp = mkApp (P Bound f Erased) (map eraseName args)
54− return $ delab i fapp
55− where eraseName (App f a) = App (eraseName f) (eraseName a)
56− eraseName (P _ (MN _ _) _) = Erased
57− eraseName t = t
58−
59−gm :: Name -> [TT Name] -> SC -> Idris ([PTerm], [PTerm])
60−gm fn args (Case n alts) = do m <- mapM (gmAlt fn args n) alts
61− let (got, missing) = unzip m
62− return (concat got, concat missing)
63−gm fn args (STerm tm) = do logLvl 3 ("Covered: " ++ show args)
64− t <- mkPTerm fn args
65− return ([t], [])
66−gm fn args ImpossibleCase = do logLvl 3 ("Impossible: " ++ show args)
67− t <- mkPTerm fn args
68− return ([], [])
69−gm fn args (UnmatchedCase _) = do logLvl 3 ("Missing: " ++ show args)
70− t <- mkPTerm fn args
71− return ([], [t])
72−
73−gmAlt fn args n (ConCase cn t cargs sc)
74− = do let args' = map (subst n (mkApp (P Bound cn Erased)
75− (map (\x -> P Bound x Erased) cargs)))
76− args
77− gm fn args' sc
78−gmAlt fn args n (ConstCase c sc)
79− = do let args' = map (subst n (Constant c)) args
80− gm fn args' sc
81−gmAlt fn args n (DefaultCase sc)
82− = do gm fn args sc
83−
84−getDefault (DefaultCase sc : _) = sc
85−getDefault (_ : cs) = getDefault cs
86−getDefault [] = UnmatchedCase ""
87−
88−dropDefault (DefaultCase sc : rest) = dropDefault rest
89−dropDefault (c : cs) = c : dropDefault cs
90−dropDefault [] = []
91−
92−expandTree :: SC -> Idris SC
93−expandTree (Case n alts) = do i <- getIState
94− as <- expandAlts i (dropDefault alts)
95− (getDefault alts)
96− alts' <- mapM expandTreeA as
97− return (Case n alts')
98− where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc
99− return (ConCase n i ns sc')
100− expandTreeA (ConstCase i sc) = do sc' <- expandTree sc
101− return (ConstCase i sc')
102− expandTreeA (DefaultCase sc) = do sc' <- expandTree sc
103− return (DefaultCase sc')
104−expandTree t = return t
105−
106−expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
107−expandAlts i all@(ConstCase c _ : alts) def
108− = return $ all ++ [DefaultCase def]
109−expandAlts i all@(ConCase n _ _ _ : alts) def
110− | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
111− = do let tyn = getTy n (tt_ctxt i)
112− case lookupCtxt tyn (idris_datatypes i) of
113− (TI ns _ _: _) -> do let ps = map mkPat ns
114− return $ addAlts ps (altsFor all) all
115− _ -> return all
116− where
117− altsFor [] = []
118− altsFor (ConCase n _ _ _ : alts) = n : altsFor alts
119− altsFor (_ : alts) = altsFor alts
120−
121− addAlts [] got alts = alts
122− addAlts ((n, arity) : ps) got alts
123− | n `elem` got = addAlts ps got alts
124− | otherwise = addAlts ps got (alts ++
125− [ConCase n (-1) (argList arity) def])
126−
127− argList i = take i (map (\x -> (MN x "ign")) [0..])
128−
129− getTy n ctxt
130− = case lookupTy n ctxt of
131− (t : _) -> case unApply (getRetTy t) of
132− (P _ tyn _, _) -> tyn
133− x -> error $ "Can't happen getTy 1 " ++ show (n, x)
134− _ -> error "Can't happen getTy 2"
135−
136− mkPat x = case lookupCtxt x (idris_implicits i) of
137− (pargs : _)
138− -> (x, length pargs)
139− _ -> error "Can't happen - genAll"
140−expandAlts i alts def = return alts
141−
142−
143−
144−-- OLD STUFF: probably broken...
145−
14636-- Given a list of LHSs, generate a extra clauses which cover the remaining
14737-- cases. The ones which haven't been provided are marked 'absurd' so that the
14838-- checker will make sure they can't happen.