@@ -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,8 +11,25 @@ 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
@@ -26,7 +44,7 @@ partial_eval ctxt ns tms = mapM peClause tms where
2644 -- If the term is a clause, specialise the right hand side
2745 peClause (Right (lhs, rhs))
2846 = let (rhs', reductions) = specialise ctxt [] (map toLimit ns) rhs in
29− do checkProgress ns reductions
47+ do -- checkProgress ns reductions
3048 return (Right (lhs, rhs'))
3149
3250 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
@@ -118,13 +136,84 @@ concreteClass ist v
118136 _ -> False
119137 | otherwise = False
120138
121−-- | Creates a new clause for a specialised function application
139+mkNewPats :: IState ->
140+ [(Term, Term)] -> -- definition to specialise
141+ [(PEArgType, Term)] -> -- arguments to specialise with
142+ Name -> -- New name
143+ Name -> -- Specialised function name
144+ PTerm -> -- Default lhs
145+ PTerm -> -- Default rhs
146+ PEDecl
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
151+-- in this case
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)
167+ where
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
174+ (lhs, rhs)
175+
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
187+
188+ extend (P _ n _) t sub = (n, t) : sub
189+ extend _ _ sub = sub
190+
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)
194+
195+ mkSubst :: (Term, Term) -> Maybe (Name, Term)
196+ mkSubst (P _ n _, t) = Just (n, t)
197+ mkSubst _ = Nothing
198+
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
122203mkPE_TermDecl :: IState -> Name -> Name ->
123− [(PEArgType, Term)] -> (PTerm, PTerm)
204+ [(PEArgType, Term)] -> PEDecl
124205mkPE_TermDecl ist newname sname ns
125206 = 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
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
213+ newpats where
214+
215+ getPats (ps, _) = map (\(_, lhs, rhs) -> (lhs, rhs)) ps
216+
128217 mkp [] = []
129218 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
130219 mkp (_ : tms) = mkp tms
@@ -137,14 +226,6 @@ mkPE_TermDecl ist newname sname ns
137226 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
138227 deImpArg a = a
139228
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−
148229-- | Get specialised applications for a given function
149230getSpecApps :: IState -> [Name] -> Term ->
150231 [(Name, [(PEArgType, Term)])]