@@ -1,7 +1,8 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
3module Idris.PartialEval(partial_eval, getSpecApps, specType,
3module Idris.PartialEval(partial_eval, getSpecApps, specType,
4− mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)) where
4+ mkPE_TyDecl, mkPE_TermDecl, PEArgType(..),
5+ pe_app, pe_def, pe_clauses) where
6import Idris.AbsSyntax
7import Idris.AbsSyntax
7import Idris.Delaborate
8import Idris.Delaborate
@@ -10,8 +11,25 @@ import Idris.Core.TT
10import Idris.Core.Evaluate
11import Idris.Core.Evaluate
12import Control.Monad.State
13import Control.Monad.State
13import Debug.Trace
15import Debug.Trace
17+-- | Data type representing binding-time annotations for partial evaluation of arguments
18+data PEArgType = ImplicitS -- ^ Implicit static argument
19+ | ImplicitD -- ^ Implicit dynamic argument
20+ | ExplicitS -- ^ Explicit static argument
21+ | ExplicitD -- ^ Explicit dynamic argument
22+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)
25+-- | A partially evaluated function. pe_app captures the lhs of the
26+-- new definition, pe_def captures the rhs, and pe_clauses is the
27+-- specialised implementation.
28+data PEDecl = PEDecl { pe_app :: PTerm, -- new application
29+ pe_def :: PTerm, -- old application
30+ pe_clauses :: [(PTerm, PTerm)] -- clauses of new application
15-- | Partially evaluates given terms under the given context.
33-- | Partially evaluates given terms under the given context.
16-- It is an error if partial evaluation fails to make any progress.
34-- It is an error if partial evaluation fails to make any progress.
17-- Making progress is defined as: all of the names given with explicit
35-- Making progress is defined as: all of the names given with explicit
@@ -26,7 +44,7 @@ partial_eval ctxt ns tms = mapM peClause tms where
26 -- If the term is a clause, specialise the right hand side
44 -- If the term is a clause, specialise the right hand side
27 peClause (Right (lhs, rhs))
45 peClause (Right (lhs, rhs))
28 = let (rhs', reductions) = specialise ctxt [] (map toLimit ns) rhs in
46 = let (rhs', reductions) = specialise ctxt [] (map toLimit ns) rhs in
29− do checkProgress ns reductions
47+ do -- checkProgress ns reductions
30 return (Right (lhs, rhs'))
48 return (Right (lhs, rhs'))
32 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
50 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
@@ -118,13 +136,84 @@ concreteClass ist v
118 _ -> False
136 _ -> False
119 | otherwise = False
137 | otherwise = False
139+mkNewPats :: IState ->
140+ [(Term, Term)] -> -- definition to specialise
141+ [(PEArgType, Term)] -> -- arguments to specialise with
143+ Name -> -- Specialised function name
144+ PTerm -> -- Default lhs
145+ PTerm -> -- Default rhs
147+-- If all of the dynamic positions on the lhs are variables (rather than
148+-- patterns or constants) then we can just make a simple definition
149+-- directly applying the specialised function, since we know the
150+-- definition isn't going to block on any of the dynamic arguments
152+mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)
153+ = PEDecl lhs rhs [(lhs, rhs)]
154+ where dynVar ap = case unApply ap of
155+ (_, args) -> dynArgs ns args
156+ dynArgs [] [] = True
157+ -- if Static, doesn't matter what the argument is
158+ dynArgs ((ImplicitS, _) : ns) (a : as) = dynArgs ns as
159+ dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as
160+ -- if Dynamic, it had better be a variable or we'll need to
161+ -- do some more work
162+ dynArgs (_ : ns) (V _ : as) = dynArgs ns as
163+ dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as
164+ dynArgs _ _ = False -- and now we'll get stuck
165+mkNewPats ist d ns newname sname lhs rhs =
166+ PEDecl lhs rhs (map mkClause d)
168+ mkClause :: (Term, Term) -> (PTerm, PTerm)
169+ mkClause (oldlhs, oldrhs)
170+ = let (_, as) = unApply oldlhs
171+ lhs = PApp emptyFC (PRef emptyFC newname)
172+ (mkLHSargs [] ns as)
173+ rhs = mkRHS as oldrhs in
176+ mkLHSargs _ [] [] = []
177+ -- dynamics don't appear if they're implicit
178+ mkLHSargs sub ((ExplicitD, t) : ns) (a : as)
179+ = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as
180+ mkLHSargs sub ((ImplicitD, _) : ns) (a : as)
181+ = mkLHSargs sub ns as
182+ -- statics get dropped in any case
183+ mkLHSargs sub ((ImplicitS, t) : ns) (a : as)
184+ = mkLHSargs (extend a t sub) ns as
185+ mkLHSargs sub ((ExplicitS, t) : ns) (a : as)
186+ = mkLHSargs (extend a t sub) ns as
188+ extend (P _ n _) t sub = (n, t) : sub
189+ extend _ _ sub = sub
191+ mkRHS :: [Term] -> Term -> PTerm
192+ mkRHS as oldrhs = let amap = mapMaybe mkSubst (zip as (map snd ns)) in
193+ delab ist (substNames amap oldrhs)
195+ mkSubst :: (Term, Term) -> Maybe (Name, Term)
196+ mkSubst (P _ n _, t) = Just (n, t)
121−-- | Creates a new clause for a specialised function application
199+-- | Creates a new declaration for a specialised function application.
200+-- Simple version at the moment: just create a version which is a direct
201+-- application of the function to be specialised.
202+-- More complex version to do: specialise the definition clause by clause
122mkPE_TermDecl :: IState -> Name -> Name ->
203mkPE_TermDecl :: IState -> Name -> Name ->
123− [(PEArgType, Term)] -> (PTerm, PTerm)
204+ [(PEArgType, Term)] -> PEDecl
124mkPE_TermDecl ist newname sname ns
205mkPE_TermDecl ist newname sname ns
125 = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))
206 = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))
126− rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns)) in
207+ rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))
208+ patdef = lookupCtxtExact sname (idris_patdefs ist)
209+ newpats = case patdef of
210+ Nothing -> PEDecl lhs rhs [(lhs, rhs)]
211+ Just d -> mkNewPats ist (getPats d) ns
212+ newname sname lhs rhs in
127− (lhs, rhs) where
213+ newpats where
215+ getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps
128 mkp [] = []
217 mkp [] = []
129 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
218 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
130 mkp (_ : tms) = mkp tms
219 mkp (_ : tms) = mkp tms
@@ -137,14 +226,6 @@ mkPE_TermDecl ist newname sname ns
137 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
226 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
138 deImpArg a = a
227 deImpArg a = a
140−-- | Data type representing binding-time annotations for partial evaluation of arguments
141−data PEArgType = ImplicitS -- ^ Implicit static argument
142− | ImplicitD -- ^ Implicit dynamic argument
143− | ExplicitS -- ^ Explicit static argument
144− | ExplicitD -- ^ Explicit dynamic argument
145− | UnifiedD -- ^ Erasable dynamic argument (found under unification)
148-- | Get specialised applications for a given function
229-- | Get specialised applications for a given function
149getSpecApps :: IState -> [Name] -> Term ->
230getSpecApps :: IState -> [Name] -> Term ->
150 [(Name, [(PEArgType, Term)])]
231 [(Name, [(PEArgType, Term)])]