@@ -1,6 +1,10 @@
1−module Idris.PartialEval(partial_eval) where
1+{-# LANGUAGE PatternGuards #-}
2+
3+module Idris.PartialEval(partial_eval, getSpecApps, specType,
4+ mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)) where
25
36import Idris.AbsSyntax
7+import Idris.Delaborate
48
59import Core.TT
610import Core.Evaluate
@@ -18,3 +22,101 @@ partial_eval ctxt ns tms = map peClause tms where
1822
1923 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit
2024 toLimit (n, Just l) = (n, l)
25+
26+specType :: [(PEArgType, Term)] -> Type -> Type
27+specType ((ExplicitS, v) : xs) (Bind n (Pi t) sc)
28+ = Bind n (Let t v) (specType xs sc)
29+specType ((ImplicitS, v) : xs) (Bind n (Pi t) sc)
30+ = Bind n (Let t v) (specType xs sc)
31+specType (_ : xs) (Bind n (Pi t) sc)
32+ = Bind n (Pi t) (specType xs sc)
33+specType _ t = t
34+
35+mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
36+mkPE_TyDecl ist ((ExplicitD, v) : xs) (Bind n (Pi t) sc)
37+ = PPi expl n (delab ist t) (mkPE_TyDecl ist xs sc)
38+mkPE_TyDecl ist ((ImplicitD, v) : xs) (Bind n (Pi t) sc)
39+ | concreteClass ist t = mkPE_TyDecl ist xs sc
40+ | classConstraint ist t
41+ = PPi constraint n (delab ist t) (mkPE_TyDecl ist xs sc)
42+ | otherwise = PPi impl n (delab ist t) (mkPE_TyDecl ist xs sc)
43+mkPE_TyDecl ist (_ : xs) t
44+ = mkPE_TyDecl ist xs t
45+mkPE_TyDecl ist [] t = delab ist t
46+
47+classConstraint ist v
48+ | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of
49+ [_] -> True
50+ _ -> False
51+ | otherwise = False
52+
53+concreteClass ist v
54+ | not (classConstraint ist v) = False
55+ | (P _ c _, args) <- unApply v = all concrete args
56+ | otherwise = False
57+ where concrete (Constant _) = True
58+ concrete tm | (P _ n _, args) <- unApply tm
59+ = case lookupTy n (tt_ctxt ist) of
60+ [_] -> all concrete args
61+ _ -> False
62+ | otherwise = False
63+
64+mkPE_TermDecl :: IState -> Name -> Name ->
65+ [(PEArgType, Term)] -> [(PTerm, PTerm)]
66+mkPE_TermDecl ist newname sname ns
67+ = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))
68+ rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns)) in
69+ [(lhs, rhs)] where
70+ mkp [] = []
71+ mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms
72+ mkp (_ : tms) = mkp tms
73+
74+ eraseImps tm = mapPT deImp tm
75+
76+ deImp (PApp fc t as) = PApp fc t (map deImpArg as)
77+ deImp t = t
78+
79+ deImpArg a@(PImp _ _ _ _ _ _) = a { getTm = Placeholder }
80+ deImpArg a = a
81+
82+data PEArgType = ImplicitS | ImplicitD
83+ | ExplicitS | ExplicitD
84+ deriving Show
85+
86+getSpecApps :: IState -> [Name] -> Term ->
87+ [(Name, [(PEArgType, Term)])]
88+getSpecApps ist env tm = ga env (explicitNames tm) where
89+
90+-- staticArg env True _ tm@(P _ n _) _ | n `elem` env = Just (True, tm)
91+-- staticArg env True _ tm@(App f a) _ | (P _ n _, args) <- unApply tm,
92+-- n `elem` env = Just (True, tm)
93+ staticArg env x imp tm n
94+ | x && imparg imp = (ImplicitS, tm)
95+ | x = (ExplicitS, tm)
96+ | imparg imp = (ImplicitD, tm)
97+ | otherwise = (ExplicitD, (P Ref (MN n "arg") Erased))
98+
99+ imparg (PExp _ _ _ _) = False
100+ imparg _ = True
101+
102+ buildApp env [] [] _ _ = []
103+ buildApp env (s:ss) (i:is) (a:as) (n:ns)
104+ = let s' = staticArg env s i a n
105+ ss' = buildApp env ss is as ns in
106+ (s' : ss')
107+
108+ ga env tm@(App f a) | (P _ n _, args) <- unApply tm =
109+ ga env f ++ ga env a ++
110+ case (lookupCtxt n (idris_statics ist),
111+ lookupCtxt n (idris_implicits ist)) of
112+ ([statics], [imps]) ->
113+ if (length statics == length args && or statics) then
114+ case buildApp env statics imps args [0..] of
115+ args -> [(n, args)]
116+-- _ -> []
117+ else []
118+ _ -> []
119+ ga env (Bind n t sc) = ga (n : env) sc
120+ ga env t = []
121+
122+