@@ -12,11 +12,14 @@ import Idris.Core.Evaluate
12import Control.Monad.State
12import Control.Monad.State
13import Debug.Trace
13import Debug.Trace
15+-- | Partially evaluates given terms under the given context.
15partial_eval :: Context -> [(Name, Maybe Int)] ->
16partial_eval :: Context -> [(Name, Maybe Int)] ->
16 [Either Term (Term, Term)] ->
17 [Either Term (Term, Term)] ->
17 [Either Term (Term, Term)]
18 [Either Term (Term, Term)]
18partial_eval ctxt ns tms = map peClause tms where
19partial_eval ctxt ns tms = map peClause tms where
20+ -- If the term is not a clause, it is simply kept as is
19 peClause (Left t) = Left t
21 peClause (Left t) = Left t
22+ -- If the term is a clause, specialise the right hand side
20 peClause (Right (lhs, rhs))
23 peClause (Right (lhs, rhs))
21 = let rhs' = specialise ctxt [] (map toLimit ns) rhs in
24 = let rhs' = specialise ctxt [] (map toLimit ns) rhs in
22 Right (lhs, rhs')
25 Right (lhs, rhs')
@@ -24,20 +27,28 @@ partial_eval ctxt ns tms = map peClause tms where
24 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
27 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
25 toLimit (n, Just l) = (n, l)
28 toLimit (n, Just l) = (n, l)
30+-- | Specialises the type of a partially evaluated TT function returning
31+-- a pair of the specialised type and the types of expected arguments.
27specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
32specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
28specType args ty = let (t, args') = runState (unifyEq args ty) [] in
33specType args ty = let (t, args') = runState (unifyEq args ty) [] in
29 (st (map fst args') t, map fst args')
34 (st (map fst args') t, map fst args')
36+ -- Specialise static argument in type by let-binding provided value instead
37+ -- of expecting it as a function argument
31 st ((ExplicitS, v) : xs) (Bind n (Pi t) sc)
38 st ((ExplicitS, v) : xs) (Bind n (Pi t) sc)
32 = Bind n (Let t v) (st xs sc)
39 = Bind n (Let t v) (st xs sc)
33 st ((ImplicitS, v) : xs) (Bind n (Pi t) sc)
40 st ((ImplicitS, v) : xs) (Bind n (Pi t) sc)
34 = Bind n (Let t v) (st xs sc)
41 = Bind n (Let t v) (st xs sc)
42+ -- Erase argument from function type
35 st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)
43 st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)
36 = st xs sc
44 = st xs sc
37 st (_ : xs) (Bind n (Pi t) sc)
46 st (_ : xs) (Bind n (Pi t) sc)
38 = Bind n (Pi t) (st xs sc)
47 = Bind n (Pi t) (st xs sc)
39 st _ t = t
48 st _ t = t
50+ -- Erase implicit dynamic argument if existing argument shares it value,
51+ -- by substituting the value of previous argument
41 unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t) sc)
52 unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t) sc)
42 = do amap <- get
53 = do amap <- get
43 case lookup imp amap of
54 case lookup imp amap of
@@ -57,6 +68,8 @@ specType args ty = let (t, args') = runState (unifyEq args ty) [] in
57 put (args ++ (zip xs (repeat (sUN "_"))))
68 put (args ++ (zip xs (repeat (sUN "_"))))
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'.
60mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
73mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
61mkPE_TyDecl ist args ty = mkty args ty
74mkPE_TyDecl ist args ty = mkty args ty
@@ -71,12 +84,15 @@ mkPE_TyDecl ist args ty = mkty args ty
71 = mkty xs t
84 = mkty xs t
72 mkty [] t = delab ist t
85 mkty [] t = delab ist t
87+-- | Checks if a given argument is a type class constraint argument
74classConstraint ist v
88classConstraint ist v
75 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of
89 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of
76 [_] -> True
90 [_] -> True
77 _ -> False
91 _ -> False
78 | otherwise = False
92 | otherwise = False
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).
80concreteClass ist v
96concreteClass ist v
81 | not (classConstraint ist v) = False
97 | not (classConstraint ist v) = False
82 | (P _ c _, args) <- unApply v = all concrete args
98 | (P _ c _, args) <- unApply v = all concrete args
@@ -88,6 +104,7 @@ concreteClass ist v
88 _ -> False
104 _ -> False
89 | otherwise = False
105 | otherwise = False
107+-- | Creates a new clause for a specialised function application
91mkPE_TermDecl :: IState -> Name -> Name ->
108mkPE_TermDecl :: IState -> Name -> Name ->
92 [(PEArgType, Term)] -> [(PTerm, PTerm)]
109 [(PEArgType, Term)] -> [(PTerm, PTerm)]
93mkPE_TermDecl ist newname sname ns
110mkPE_TermDecl ist newname sname ns
@@ -106,11 +123,15 @@ mkPE_TermDecl ist newname sname ns
106 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
123 deImpArg a@(PImp _ _ _ _ _) = a { getTm = Placeholder }
107 deImpArg a = a
124 deImpArg a = a
126+-- | Data type representing binding-time annotations for partial evaluation of arguments
109−data PEArgType = ImplicitS | ImplicitD
127+data PEArgType = ImplicitS -- ^ Implicit static argument
110− | ExplicitS | ExplicitD
128+ | ImplicitD -- ^ Implicit dynamic argument
111− | UnifiedD
129+ | ExplicitS -- ^ Explicit static argument
130+ | ExplicitD -- ^ Explicit dynamic argument
131+ | UnifiedD -- ^ Erasable dynamic argument (found under unification)
112 deriving (Eq, Show)
132 deriving (Eq, Show)
134+-- | Get specialised applications for a given function
114getSpecApps :: IState -> [Name] -> Term ->
135getSpecApps :: IState -> [Name] -> Term ->
115 [(Name, [(PEArgType, Term)])]
136 [(Name, [(PEArgType, Term)])]
116getSpecApps ist env tm = ga env (explicitNames tm) where
137getSpecApps ist env tm = ga env (explicitNames tm) where