@@ -1,6 +1,6 @@
11{-# LANGUAGE PatternGuards #-}
22
3−module Idris.CaseSplit where
3+module Idris.CaseSplit(split) where
44
55-- splitting a variable in a pattern clause
66
@@ -8,12 +8,125 @@ import Idris.AbsSyntax
88import Idris.ElabDecls
99import Idris.ElabTerm
1010import Idris.Delaborate
11+import Idris.Error
1112
1213import Core.TT
14+import Core.Evaluate
15+
16+import Data.Maybe
17+import Control.Monad
18+import Control.Monad.State
19+
20+{-
21+
22+Given a pattern clause and a variable 'n', elaborate the cluse and find the
23+type of 'n'.
24+
25+Make new pattern clauses by replacing 'n' with all the possibly constructors
26+applied to '_', and replacing all other variables with '_' in order to
27+resolve other dependencies.
28+
29+Finally, merge the generated patterns with the original, by matching.
30+Always take the "more specific" argument when there is a discrepancy, i.e.
31+names over '_', patterns over names, etc.
32+-}
1333
1434split :: Name -> PTerm -> Idris [PTerm]
15−split n t = do (tm, ty, pats) <- elabValBind toplevel True t
16− ist <- getIState
17− iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
18− iputStrLn (show pats)
19− return [t]
35+split n t'
36+ = do (tm, ty, pats) <- elabValBind toplevel True t'
37+ ist <- getIState
38+-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))
39+-- iputStrLn (show pats)
40+ let t = mergeUserImpl (addImpl ist t') (delab ist tm) -- addImplPat ist t'
41+ let ctxt = tt_ctxt ist
42+ case lookup n pats of
43+ Nothing -> fail $ show n ++ " is not a pattern variable"
44+ Just ty ->
45+ do let splits = findPats ist ty
46+ let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
47+ newPats <- mapM elabNewPat newPats_in
48+ logLvl 5 (showSep "\n" (map show (t : mapMaybe id newPats)))
49+ logLvl 5 "----"
50+ let newPats' = evalState (mapM (mergePat ctxt t)
51+ (mapMaybe id newPats))
52+ []
53+ return newPats'
54+
55+mergePat :: Context -> PTerm -> PTerm -> State [(Name, Name)] PTerm
56+-- If any names are unified, make sure they stay unified. Always prefer
57+-- user provided name (first pattern)
58+mergePat ctxt orig@(PRef fc n) new@(PRef _ n')
59+ | isConName n' ctxt = return new
60+ | otherwise
61+ = do nmap <- get
62+ case lookup n' nmap of
63+ Just x -> return (PRef fc x)
64+ Nothing -> do put ((n', n) : nmap)
65+ return (PRef fc n)
66+mergePat ctxt (PApp _ _ args) (PApp fc f args')
67+ = do newArgs <- zipWithM mergeArg args args'
68+ return (PApp fc f newArgs)
69+ where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)
70+ case x of
71+ (PImp _ _ _ _ _ _) ->
72+ return (y { machine_inf = machine_inf x,
73+ getTm = tm' })
74+ _ -> return (y { getTm = tm' })
75+mergePat ctxt (PRef fc n) t = tidy t
76+mergePat ctxt x y = return y
77+
78+mergeUserImpl :: PTerm -> PTerm -> PTerm
79+mergeUserImpl x y = x
80+
81+tidy orig@(PRef fc n)
82+ = do nmap <- get
83+ case lookup n nmap of
84+ Just x -> return (PRef fc x)
85+ Nothing -> case n of
86+ (UN _) -> return orig
87+ _ -> return Placeholder
88+tidy (PApp fc f args)
89+ = do args' <- mapM tidyArg args
90+ return (PApp fc f args')
91+ where tidyArg x = do tm' <- tidy (getTm x)
92+ return (x { getTm = tm' })
93+tidy tm = return tm
94+
95+
96+-- mapPT tidyVar tm
97+-- where tidyVar (PRef _ _) = Placeholder
98+-- tidyVar t = t
99+
100+elabNewPat :: PTerm -> Idris (Maybe PTerm)
101+elabNewPat t = idrisCatch (do (tm, ty) <- elabVal toplevel True t
102+ i <- getIState
103+ return (Just (delab i tm)))
104+ (\e -> return Nothing)
105+
106+findPats :: IState -> Type -> [PTerm]
107+findPats ist t | (P _ n _, _) <- unApply t
108+ = case lookupCtxt n (idris_datatypes ist) of
109+ [ti] -> map genPat (con_names ti)
110+ _ -> [Placeholder]
111+ where genPat n = case lookupCtxt n (idris_implicits ist) of
112+ [args] -> PApp emptyFC (PRef emptyFC n)
113+ (map toPlaceholder args)
114+ _ -> error $ "Can't happen (genPat) " ++ show n
115+ toPlaceholder tm = tm { getTm = Placeholder }
116+findPats ist t = [Placeholder]
117+
118+replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm
119+replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)
120+ where subst :: PTerm -> PTerm
121+ subst orig@(PRef _ v) | v == n = t
122+ | isConName v ctxt = orig
123+ subst (PRef _ _) = Placeholder
124+ subst (PApp fc f pats) = PApp fc f (map substArg pats)
125+ subst x = x
126+
127+ substArg arg = arg { getTm = subst (getTm arg) }
128+
129+replaceVar ctxt n t pat = pat
130+
131+
132+