@@ -1,7 +1,8 @@
11{-# LANGUAGE PatternGuards #-}
22
33module 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
56
67import Idris.AbsSyntax
78import Idris.Delaborate
@@ -10,12 +11,32 @@ import Idris.Core.TT
1011import Idris.Core.Evaluate
1112
1213import Control.Monad.State
14+import Data.Maybe
1315import Debug.Trace
1416
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)
23+ deriving (Eq, Show)
24+
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
31+ }
32+
1533-- | Partially evaluates given terms under the given context.
1634-- It is an error if partial evaluation fails to make any progress.
1735-- Making progress is defined as: all of the names given with explicit
18−-- reduction limits must have reduced at least once.
36+-- reduction limits (in practice, the function being specialised)
37+-- must have reduced at least once.
38+-- If we don't do this, we might end up making an infinite function after
39+-- applying the transformation.
1940partial_eval :: Context ->
2041 [(Name, Maybe Int)] ->
2142 [Either Term (Term, Term)] ->
@@ -35,7 +56,7 @@ partial_eval ctxt ns tms = mapM peClause tms where
3556 checkProgress ns [] = return ()
3657 checkProgress ns ((n, r) : rs)
3758 | Just (Just start) <- lookup n ns
38− = if r < start then checkProgress ns rs else Nothing
59+ = if start <= 1 || r < start then checkProgress ns rs else Nothing
3960 | otherwise = checkProgress ns rs
4061
4162-- | Specialises the type of a partially evaluated TT function returning
@@ -118,13 +139,89 @@ concreteClass ist v
118139 _ -> False
119140 | otherwise = False
120141
121−-- | Creates a new clause for a specialised function application
142+mkNewPats :: IState ->
143+ [(Term, Term)] -> -- definition to specialise
144+ [(PEArgType, Term)] -> -- arguments to specialise with
145+ Name -> -- New name
146+ Name -> -- Specialised function name
147+ PTerm -> -- Default lhs
148+ PTerm -> -- Default rhs
149+ PEDecl
150+-- If all of the dynamic positions on the lhs are variables (rather than
151+-- patterns or constants) then we can just make a simple definition
152+-- directly applying the specialised function, since we know the
153+-- definition isn't going to block on any of the dynamic arguments
154+-- in this case
155+mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)
156+ = PEDecl lhs rhs [(lhs, rhs)]
157+ where dynVar ap = case unApply ap of
158+ (_, args) -> dynArgs ns args
159+ dynArgs _ [] = True -- can definitely reduce from here
160+ -- if Static, doesn't matter what the argument is
161+ dynArgs ((ImplicitS, _) : ns) (a : as) = dynArgs ns as
162+ dynArgs ((ExplicitS, _) : ns) (a : as) = dynArgs ns as
163+ -- if Dynamic, it had better be a variable or we'll need to
164+ -- do some more work
165+ dynArgs (_ : ns) (V _ : as) = dynArgs ns as
166+ dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as
167+ dynArgs _ _ = False -- and now we'll get stuck
168+mkNewPats ist d ns newname sname lhs rhs =
169+ PEDecl lhs rhs (map mkClause d)
170+ where
171+ mkClause :: (Term, Term) -> (PTerm, PTerm)
172+ mkClause (oldlhs, oldrhs)
173+ = let (_, as) = unApply oldlhs
174+ lhsargs = mkLHSargs [] ns as
175+ lhs = PApp emptyFC (PRef emptyFC newname) lhsargs
176+ rhs = PApp emptyFC (PRef emptyFC sname)
177+ (mkRHSargs ns lhsargs) in
178+ (lhs, rhs)
179+
180+ mkLHSargs _ [] [] = []
181+ -- dynamics don't appear if they're implicit
182+ mkLHSargs sub ((ExplicitD, t) : ns) (a : as)
183+ = pexp (delab ist (substNames sub a)) : mkLHSargs sub ns as
184+ mkLHSargs sub ((ImplicitD, _) : ns) (a : as)
185+ = mkLHSargs sub ns as
186+ mkLHSargs sub ((UnifiedD, _) : ns) (a : as)
187+ = mkLHSargs sub ns as
188+ -- statics get dropped in any case
189+ mkLHSargs sub ((ImplicitS, t) : ns) (a : as)
190+ = mkLHSargs (extend a t sub) ns as
191+ mkLHSargs sub ((ExplicitS, t) : ns) (a : as)
192+ = mkLHSargs (extend a t sub) ns as
193+ mkLHSargs sub _ [] = [] -- no more LHS
194+
195+ extend (P _ n _) t sub = (n, t) : sub
196+ extend _ _ sub = sub
197+
198+ mkRHSargs ((ExplicitS, t) : ns) as = pexp (delab ist t) : mkRHSargs ns as
199+ mkRHSargs ((ExplicitD, t) : ns) (a : as) = a : mkRHSargs ns as
200+ mkRHSargs (_ : ns) as = mkRHSargs ns as
201+ mkRHSargs _ _ = []
202+
203+ mkSubst :: (Term, Term) -> Maybe (Name, Term)
204+ mkSubst (P _ n _, t) = Just (n, t)
205+ mkSubst _ = Nothing
206+
207+-- | Creates a new declaration for a specialised function application.
208+-- Simple version at the moment: just create a version which is a direct
209+-- application of the function to be specialised.
210+-- More complex version to do: specialise the definition clause by clause
122211mkPE_TermDecl :: IState -> Name -> Name ->
123− [(PEArgType, Term)] -> (PTerm, PTerm)
212+ [(PEArgType, Term)] -> PEDecl
124213mkPE_TermDecl ist newname sname ns
125214 = 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
127− (lhs, rhs) where
215+ rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))
216+ patdef = lookupCtxtExact sname (idris_patdefs ist)
217+ newpats = case patdef of
218+ Nothing -> PEDecl lhs rhs [(lhs, rhs)]
219+ Just d -> mkNewPats ist (getPats d) ns
220+ newname sname lhs rhs in
221+ newpats where
222+
223+ getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps
224+
128225 mkp [] = []
129226 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
130227 mkp (_ : tms) = mkp tms
@@ -137,14 +234,6 @@ mkPE_TermDecl ist newname sname ns
137234 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
138235 deImpArg a = a
139236
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)
146− deriving (Eq, Show)
147−
148237-- | Get specialised applications for a given function
149238getSpecApps :: IState -> [Name] -> Term ->
150239 [(Name, [(PEArgType, Term)])]
@@ -167,19 +256,22 @@ getSpecApps ist env tm = ga env (explicitNames tm) where
167256 = let s' = staticArg env s i a n
168257 ss' = buildApp env ss is as ns in
169258 (s' : ss')
170−
171− ga env tm@(App f a) | (P _ n _, args) <- unApply tm =
172− ga env f ++ ga env a ++
173− case (lookupCtxt n (idris_statics ist),
174− lookupCtxt n (idris_implicits ist)) of
175− ([statics], [imps]) ->
176− if (length statics == length args && or statics) then
177−-- trace (show (n, statics, imps, args)) $
178− case buildApp env statics imps args [0..] of
179− args -> [(n, args)]
180−-- _ -> []
181− else []
182− _ -> []
259+
260+ -- if we have a *defined* function that has static arguments,
261+ -- it will become a specialised application
262+ ga env tm@(App f a) | (P _ n _, args) <- unApply tm,
263+ n `notElem` map fst (idris_metavars ist) =
264+ ga env f ++ ga env a ++
265+ case (lookupCtxt n (idris_statics ist),
266+ lookupCtxt n (idris_implicits ist)) of
267+ ([statics], [imps]) ->
268+ if (length statics == length args && or statics) then
269+-- trace (show (n, statics, imps, args)) $
270+ case buildApp env statics imps args [0..] of
271+ args -> [(n, args)]
272+-- _ -> []
273+ else []
274+ _ -> []
183275 ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc
184276 ga env (Bind n t sc) = ga (n : env) sc
185277 ga env t = []