@@ -12,11 +12,14 @@ import Idris.Core.Evaluate
1212import Control.Monad.State
1313import Debug.Trace
1414
15+-- | Partially evaluates given terms under the given context.
1516partial_eval :: Context -> [(Name, Maybe Int)] ->
1617 [Either Term (Term, Term)] ->
1718 [Either Term (Term, Term)]
1819partial_eval ctxt ns tms = map peClause tms where
20+ -- If the term is not a clause, it is simply kept as is
1921 peClause (Left t) = Left t
22+ -- If the term is a clause, specialise the right hand side
2023 peClause (Right (lhs, rhs))
2124 = let rhs' = specialise ctxt [] (map toLimit ns) rhs in
2225 Right (lhs, rhs')
@@ -24,20 +27,28 @@ partial_eval ctxt ns tms = map peClause tms where
2427 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
2528 toLimit (n, Just l) = (n, l)
2629
30+-- | Specialises the type of a partially evaluated TT function returning
31+-- a pair of the specialised type and the types of expected arguments.
2732specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
2833specType args ty = let (t, args') = runState (unifyEq args ty) [] in
2934 (st (map fst args') t, map fst args')
3035 where
36+ -- Specialise static argument in type by let-binding provided value instead
37+ -- of expecting it as a function argument
3138 st ((ExplicitS, v) : xs) (Bind n (Pi t) sc)
3239 = Bind n (Let t v) (st xs sc)
3340 st ((ImplicitS, v) : xs) (Bind n (Pi t) sc)
3441 = Bind n (Let t v) (st xs sc)
42+ -- Erase argument from function type
3543 st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)
3644 = st xs sc
45+ -- Keep types as is
3746 st (_ : xs) (Bind n (Pi t) sc)
3847 = Bind n (Pi t) (st xs sc)
3948 st _ t = t
4049
50+ -- Erase implicit dynamic argument if existing argument shares it value,
51+ -- by substituting the value of previous argument
4152 unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t) sc)
4253 = do amap <- get
4354 case lookup imp amap of
@@ -57,6 +68,8 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in
5768 put (args ++ (zip xs (repeat (sUN "_"))))
5869 return t
5970
71+-- | Creates an Idris type declaration given current state and a specialised TT function application type.
72+-- Can be used in combination with the output of 'specType'.
6073mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
6174mkPE_TyDecl ist args ty = mkty args ty
6275 where
@@ -71,12 +84,15 @@ mkPE_TyDecl ist args ty = mkty args ty
7184 = mkty xs t
7285 mkty [] t = delab ist t
7386
87+-- | Checks if a given argument is a type class constraint argument
7488classConstraint ist v
7589 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of
7690 [_] -> True
7791 _ -> False
7892 | otherwise = False
7993
94+-- | Checks if the given arguments of a type class constraint are all either constants
95+-- or references (i.e. that it doesn't contain any complex terms).
8096concreteClass ist v
8197 | not (classConstraint ist v) = False
8298 | (P _ c _, args) <- unApply v = all concrete args
@@ -88,6 +104,7 @@ concreteClass ist v
88104 _ -> False
89105 | otherwise = False
90106
107+-- | Creates a new clause for a specialised function application
91108mkPE_TermDecl :: IState -> Name -> Name ->
92109 [(PEArgType, Term)] -> [(PTerm, PTerm)]
93110mkPE_TermDecl ist newname sname ns
@@ -106,11 +123,15 @@ mkPE_TermDecl ist newname sname ns
106123 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
107124 deImpArg a = a
108125
109−data PEArgType = ImplicitS | ImplicitD
110− | ExplicitS | ExplicitD
111− | UnifiedD
126+-- | Data type representing binding-time annotations for partial evaluation of arguments
127+data PEArgType = ImplicitS -- ^ Implicit static argument
128+ | ImplicitD -- ^ Implicit dynamic argument
129+ | ExplicitS -- ^ Explicit static argument
130+ | ExplicitD -- ^ Explicit dynamic argument
131+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)
112132 deriving (Eq, Show)
113133
134+-- | Get specialised applications for a given function
114135getSpecApps :: IState -> [Name] -> Term ->
115136 [(Name, [(PEArgType, Term)])]
116137getSpecApps ist env tm = ga env (explicitNames tm) where