git.iko.soy/Idris-dev
on master help sign in
Implement transformation rules

Now the partial evaluator, in its basic form, is working, recursively generating any required definitions from [static] annotations.

commit146858d364b4ed3352b4f1ce6724fe178794433c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Oct 2014, 19:47 (12 years ago) parent869e6ca
3 files changed+59−3
compare with master
unifiedsplit
src/Idris/Elab/Clause.hs+8−2 src/Idris/PartialEval.hs+1 src/Idris/Transforms.hs+50−1
src/Idris/Elab/Clause.hs+8−2
@@ -84,7 +84,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
8484 addIBC (IBCOpt n)
8585
8686 ist <- getIState
87− let tpats = transformPats ist pats_in
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
90+ Nothing -> transformPats ist pats_in
91+ _ -> pats_in
92+
8893 let pats = map (simple_lhs (tt_ctxt ist)) $
8994 doPartialEval ist tpats
9095
@@ -101,6 +106,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
101106 Right (l, r) -> elabPE info fc n r) pats
102107
103108 -- Redo transforms with the newly generated transformations
109+ ist <- getIState
104110 let pats_transformed = transformPats ist pats
105111
106112 -- Summary of what's about to happen: Definitions go:
@@ -326,9 +332,9 @@ elabPE info fc caller r =
326332 show rhs ++ " ==> " ++ show lhs
327333
328334 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy
329− elabTransform info fc False rhs lhs
330335 let def = -- map (\ (lhs, rhs) ->
331336 [PClause fc newnm lhs [] rhs []] --) pats
337+ elabTransform info fc False rhs lhs
332338 elabClauses info fc opts newnm def)
333339 -- if it doesn't work, just don't specialise. Could happen for lots
334340 -- 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
168168-- _ -> []
169169 else []
170170 _ -> []
171+ ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc
171172 ga env (Bind n t sc) = ga (n : env) sc
172173 ga env t = []
173174
src/Idris/Transforms.hs+50−1
@@ -6,6 +6,7 @@ import Idris.AbsSyntax
66import Idris.Core.CaseTree
77import Idris.Core.TT
88
9+import Debug.Trace
910
1011transformPats :: IState -> [Either Term (Term, Term)] ->
1112 [Either Term (Term, Term)]
@@ -19,4 +20,52 @@ applyTransRules :: IState -> Term -> Term
1920applyTransRules ist tm = applyAll (idris_transforms ist) tm
2021
2122applyAll :: 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+