git.iko.soy/Idris-dev
on master help sign in
Implement transformation rules
146858dEdwin Brady
src/Idris/Elab/Clause.hs+8−2
compare with master
unifiedsplit
@@ -84,7 +84,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
84 addIBC (IBCOpt n)
84 addIBC (IBCOpt n)
85
85
86 ist <- getIState
86 ist <- getIState
87+ -- Don't apply rules if this is a partial evaluation definition,
88+ -- or we'll make something that just runs itself!
89+ let tpats = case specNames opts of
87− let tpats = transformPats ist pats_in
90+ Nothing -> transformPats ist pats_in
91+ _ -> pats_in
92+
88 let pats = map (simple_lhs (tt_ctxt ist)) $
93 let pats = map (simple_lhs (tt_ctxt ist)) $
89 doPartialEval ist tpats
94 doPartialEval ist tpats
90
95
@@ -101,6 +106,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
101 Right (l, r) -> elabPE info fc n r) pats
106 Right (l, r) -> elabPE info fc n r) pats
102
107
103 -- Redo transforms with the newly generated transformations
108 -- Redo transforms with the newly generated transformations
109+ ist <- getIState
104 let pats_transformed = transformPats ist pats
110 let pats_transformed = transformPats ist pats
105
111
106 -- Summary of what's about to happen: Definitions go:
112 -- Summary of what's about to happen: Definitions go:
@@ -326,9 +332,9 @@ elabPE info fc caller r =
326 show rhs ++ " ==> " ++ show lhs
332 show rhs ++ " ==> " ++ show lhs
327
333
328 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
334 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
329− elabTransform info fc False rhs lhs
330 let def = -- map (\ (lhs, rhs) ->
335 let def = -- map (\ (lhs, rhs) ->
331 [PClause fc newnm lhs [] rhs []] --) pats
336 [PClause fc newnm lhs [] rhs []] --) pats
337+ elabTransform info fc False rhs lhs
332 elabClauses info fc opts newnm def)
338 elabClauses info fc opts newnm def)
333 -- if it doesn't work, just don't specialise. Could happen for lots
339 -- if it doesn't work, just don't specialise. Could happen for lots
334 -- of valid reasons (e.g. local variables in scope which can't be
340 -- of valid reasons (e.g. local variables in scope which can't be
src/Idris/PartialEval.hs+1
@@ -168,6 +168,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
168-- _ -> []
168-- _ -> []
169 else []
169 else []
170 _ -> []
170 _ -> []
171+ ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc
171 ga env (Bind n t sc) = ga (n : env) sc
172 ga env (Bind n t sc) = ga (n : env) sc
172 ga env t = []
173 ga env t = []
173
174
src/Idris/Transforms.hs+50−1
@@ -6,6 +6,7 @@ import Idris.AbsSyntax
6import Idris.Core.CaseTree
6import Idris.Core.CaseTree
7import Idris.Core.TT
7import Idris.Core.TT
8
8
9+import Debug.Trace
9
10
10transformPats :: IState -> [Either Term (Term, Term)] ->
11transformPats :: IState -> [Either Term (Term, Term)] ->
11 [Either Term (Term, Term)]
12 [Either Term (Term, Term)]
@@ -19,4 +20,52 @@ applyTransRules :: IState -> Term -> Term
19applyTransRules ist tm = applyAll (idris_transforms ist) tm
20applyTransRules ist tm = applyAll (idris_transforms ist) tm
20
21
21applyAll :: Ctxt [(Term, Term)] -> Term -> Term
22applyAll :: Ctxt [(Term, Term)] -> Term -> Term
22−applyAll ts t = t
23+applyAll ts ap@(App f a)
24+ | (P _ fn ty, args) <- unApply ap
25+ = case lookupCtxtExact fn ts of
26+ Just rules -> case applyFnRules rules ap of
27+ Just tm' -> tm'
28+ _ -> App (applyAll ts f) (applyAll ts a)
29+ Nothing -> App (applyAll ts f) (applyAll ts a)
30+applyAll ts (Bind n b sc) = Bind n (fmap (applyAll ts) b) (applyAll ts sc)
31+applyAll ts t = t
32+
33+applyFnRules :: [(Term, Term)] -> Term -> Maybe Term
34+applyFnRules [] tm = Nothing
35+applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'
36+ | otherwise = applyFnRules rs tm
37+
38+applyRule :: (Term, Term) -> Term -> Maybe Term
39+applyRule (lhs, rhs) tm
40+ | Just ms <- matchTerm lhs tm
41+-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++
42+-- "\n" ++ show rhs
43+-- ++ "\n" ++ show tm) $
44+ = Just $ depat ms rhs
45+ | otherwise = Nothing
46+ where depat ms (Bind n (PVar t) sc)
47+ = case lookup n ms of
48+ Just tm -> depat ms (instantiate tm sc)
49+ _ -> depat ms sc -- no occurrence? Shouldn't happen
50+ depat ms tm = tm
51+
52+matchTerm :: Term -> Term -> Maybe [(Name, Term)]
53+matchTerm lhs tm = matchVars [] lhs tm
54+ where
55+ matchVars acc (Bind n (PVar t) sc) tm
56+ = matchVars (n : acc) (instantiate (P Bound n t) sc) tm
57+ matchVars acc sc tm
58+ = -- trace (show acc ++ ": " ++ show (sc, tm)) $
59+ doMatch acc sc tm
60+
61+ doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]
62+ doMatch ns (P _ n _) tm
63+ | n `elem` ns = return [(n, tm)]
64+ doMatch ns (App f a) (App f' a')
65+ = do fm <- doMatch ns f f'
66+ am <- doMatch ns a a'
67+ return (fm ++ am)
68+ doMatch ns x y | x == y = return []
69+ | otherwise = Nothing
70+
71+