@@ -14,6 +14,93 @@ import Data.List
1414import Data.Either
1515import Debug.Trace
1616
17+import Control.Monad.State
18+
19+-- Generate the LHSes which are missing from a case tree
20+-- Eliminate the ones which cannot be well typed
21+
22+genMissing :: [Name] -> SC -> Idris [PTerm]
23+genMissing args sc = do sc' <- expandTree sc
24+ iputStrLn (show sc')
25+ gm (map (\x -> P Bound x Erased) args) sc'
26+
27+gm :: [TT Name] -> SC -> Idris [PTerm]
28+gm args (Case n alts) = do m <- mapM (gmAlt args n) alts
29+ return (concat m)
30+gm args (STerm tm) = do iputStrLn ("Covered: " ++ show args)
31+ return []
32+gm args (UnmatchedCase _) = do iputStrLn ("Missing: " ++ show args)
33+ return []
34+
35+gmAlt args n (ConCase cn t cargs sc)
36+ = do let args' = map (subst n (mkApp (P Bound cn Erased)
37+ (map (\x -> P Bound x Erased) cargs))) args
38+ gm args' sc
39+gmAlt args n (ConstCase c sc)
40+ = do let args' = map (subst n (Constant c)) args
41+ gm args' sc
42+gmAlt args n (DefaultCase sc)
43+ = do gm args sc
44+
45+getDefault (DefaultCase sc : _) = sc
46+getDefault (_ : cs) = getDefault cs
47+getDefault [] = UnmatchedCase ""
48+
49+dropDefault (DefaultCase sc : rest) = dropDefault rest
50+dropDefault (c : cs) = c : dropDefault cs
51+dropDefault [] = []
52+
53+expandTree :: SC -> Idris SC
54+expandTree (Case n alts) = do i <- get
55+ as <- expandAlts i (dropDefault alts) (getDefault alts)
56+ alts' <- mapM expandTreeA as
57+ return (Case n alts')
58+ where expandTreeA (ConCase n i ns sc) = do sc' <- expandTree sc
59+ return (ConCase n i ns sc')
60+ expandTreeA (ConstCase i sc) = do sc' <- expandTree sc
61+ return (ConstCase i sc')
62+ expandTreeA (DefaultCase sc) = do sc' <- expandTree sc
63+ return (DefaultCase sc')
64+expandTree t = return t
65+
66+expandAlts :: IState -> [CaseAlt] -> SC -> Idris [CaseAlt]
67+expandAlts i all@(ConstCase c _ : alts) def
68+ = return $ all ++ [DefaultCase def]
69+expandAlts i all@(ConCase n _ _ _ : alts) def
70+ | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)
71+ = do let tyn = getTy n (tt_ctxt i)
72+ case lookupCtxt Nothing tyn (idris_datatypes i) of
73+ (TI ns : _) -> do let ps = map mkPat ns
74+ return $ addAlts ps (altsFor all) all
75+ _ -> return all
76+ where
77+ altsFor [] = []
78+ altsFor (ConCase n _ _ _ : alts) = n : altsFor alts
79+ altsFor (_ : alts) = altsFor alts
80+
81+ addAlts [] got alts = alts
82+ addAlts ((n, arity) : ps) got alts
83+ | n `elem` got = addAlts ps got alts
84+ | otherwise = addAlts ps got (alts ++ [ConCase n (-1) (argList arity) def])
85+
86+ argList i = take i (map (\x -> (MN x "ign")) [0..])
87+
88+ getTy n ctxt = case lookupTy Nothing n ctxt of
89+ (t : _) -> case unApply (getRetTy t) of
90+ (P _ tyn _, _) -> tyn
91+ x -> error $ "Can't happen getTy 1 " ++ show (n, x)
92+ _ -> error "Can't happen getTy 2"
93+
94+ mkPat x = case lookupCtxt Nothing x (idris_implicits i) of
95+ (pargs : _)
96+ -> (x, length pargs)
97+ _ -> error "Can't happen - genAll"
98+expandAlts i alts def = return alts
99+
100+
101+
102+-- OLD STUFF: probably broken...
103+
17104-- Given a list of LHSs, generate a extra clauses which cover the remaining
18105-- cases. The ones which haven't been provided are marked 'absurd' so that the
19106-- checker will make sure they can't happen.