8531634 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Set up more partial evaluation machinery

8531634Edwin Brady13 years ago

src/Core/Evaluate.hs+4−4

compare with master

unifiedsplit

@@ -151,7 +151,7 @@ usable True n ns

151 case lookup n ls of

152 Just 0 -> return (False, ns)

153 Just i -> return (True, ns)

154− _ -> return (False, ns)

154+ _ -> return (True, ns)

155usable False n ns

156 = case lookup n ns of

157 Just 0 -> return (False, ns)

@@ -203,7 +203,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

203 | otherwise

204 = do (u, ntimes) <- usable spec n ntimes_in

205 if u then

206− do let val = lookupDefAcc n atRepl ctxt

206+ do let val = lookupDefAcc n (spec || atRepl) ctxt

207 case val of

208 [(Function _ tm, Public)] ->

209 ev ntimes (n:stk) True env tm

@@ -279,7 +279,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

279 = apply ntimes stk top env f args

280

281 reapply ntimes stk top env f@(VP Ref n ty) args

282− = let val = lookupDefAcc n atRepl ctxt in

282+ = let val = lookupDefAcc n (spec || atRepl) ctxt in

283 case val of

284 [(CaseOp ci _ _ _ cd, acc)] ->

285 let (ns, tree) = getCases cd in

@@ -305,7 +305,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

305 | otherwise

306 = do (u, ntimes) <- usable spec n ntimes_in

307 if u then

308− do let val = lookupDefAcc n atRepl ctxt

308+ do let val = lookupDefAcc n (spec || atRepl) ctxt

309 case val of

310 [(CaseOp ci _ _ _ cd, acc)]

311 | acc == Public -> -- unoptimised version

src/Core/TT.hs+1

@@ -293,6 +293,7 @@ tcname _ = False

293

294implicitable (NS n _) = implicitable n

295implicitable (UN (x:xs)) = isLower x

296+implicitable (MN _ _) = True

296implicitable _ = False

297implicitable _ = False

297

298

298nsroot (NS n _) = n

299nsroot (NS n _) = n

src/Idris/AbsSyntax.hs+17−3

@@ -883,11 +883,13 @@ getPriority i tm = 1 -- pri tm

883addStatics :: Name -> Term -> PTerm -> Idris ()

884addStatics n tm ptm =

885 do let (statics, dynamics) = initStatics tm ptm

886− let stnames = nub $ concatMap freeNames (map snd statics)

886+ let stnames = nub $ concatMap freeArgNames (map snd statics)

887− let dnames = nub $ concatMap freeNames (map snd dynamics)

887+ let dnames = nub $ concatMap freeArgNames (map snd dynamics)

888 when (not (null statics)) $

889 logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics

890 ++ "\n" ++ show stnames ++ "\n" ++ show dnames

891+ -- also get the arguments which are 'uniquely inferrable' from

892+ -- statics (see sec 4.2 of "Scrapping Your Inefficient Engine")

891 let statics' = nub $ map fst statics ++

893 let statics' = nub $ map fst statics ++

892 filter (\x -> not (elem x dnames)) stnames

894 filter (\x -> not (elem x dnames)) stnames

893 let stpos = staticList statics' tm

895 let stpos = staticList statics' tm

@@ -898,9 +900,21 @@ addStatics n tm ptm =

898 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)

900 initStatics (Bind n (Pi ty) sc) (PPi p _ _ s)

899 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

901 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

900 if pstatic p == Static then ((n, ty) : static, dynamic)

902 if pstatic p == Static then ((n, ty) : static, dynamic)

903+ else if (not (searchArg p))

901− else (static, (n, ty) : dynamic)

904+ then (static, (n, ty) : dynamic)

905+ else (static, dynamic)

902 initStatics t pt = ([], [])

906 initStatics t pt = ([], [])

903

907

908+ freeArgNames tm = let (_, args) = unApply tm in

909+ concatMap freeNames args

910+

911+ -- if a name appears in a type class or tactic implicit index, it doesn't

912+ -- affect its 'uniquely inferrable' from a static status since these are

913+ -- resolved by searching.

914+ searchArg (Constraint _ _ _) = True

915+ searchArg (TacImp _ _ _ _) = True

916+ searchArg _ = False

917+

904 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

918 staticList sts (Bind n (Pi _) sc) = (n `elem` sts) : staticList sts sc

905 staticList _ _ = []

919 staticList _ _ = []

906

920

src/Idris/ElabDecls.hs+69−4

@@ -593,7 +593,17 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

593 -- further inlined to help with totality checking.

594 let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats

595

596− logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef

596+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pats

597+ logLvl 5 $ "Initial typechecked pattern def:\n" ++ show pdef

598+

599+ -- Look for 'static' names and generate new specialised

600+ -- definitions for them

601+

602+ {- Not fully implemented yet!

603+ mapM_ (\ e -> case e of

604+ Left _ -> return ()

605+ Right (l, r) -> elabPE info fc r) pats

606+ -}

597

607

598 -- TODO: Inlining on initial definition happens here.

608 -- TODO: Inlining on initial definition happens here.

599

609

@@ -747,12 +757,67 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

747 -- user defined transformation rules later)

757 -- user defined transformation rules later)

748 doTransforms ist pats =

758 doTransforms ist pats =

749 case specNames opts of

759 case specNames opts of

750− Nothing -> pats

760+ Nothing -> pats

751− Just ns -> partial_eval (tt_ctxt ist) ns pats

761+ Just ns -> partial_eval (tt_ctxt ist) ns pats

762+

763+-- Find 'static' applications in a term and partially evaluate them

764+elabPE :: ElabInfo -> FC -> Term -> Idris ()

765+elabPE info fc r =

766+ do ist <- getIState

767+ let sa = getSpecApps ist [] r

768+ mapM_ (mkSpecialised ist) sa

769+ where

770+ mkSpecialised ist specapp = do

771+ let specTy = getSpecTy ist specapp

772+ let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp

773+ let undef = case lookupDef newnm (tt_ctxt ist) of

774+ [] -> True

775+ _ -> False

776+ when (undef && all (concreteArg ist) (snd specapp)) $ do

777+ let opts = [Specialise ((n, Nothing) :

778+ (mapMaybe specName (snd specapp)))]

779+ iputStrLn (show specapp)

780+ iputStrLn $ "PE definition type : " ++ (show specTy)

781+ ++ "\n" ++ show opts

782+ iputStrLn $ "PE definition " ++ show newnm ++ ":\n" ++

783+ (show lhs ++ " = " ++ show rhs)

784+ elabType info defaultSyntax "" fc opts newnm specTy

785+ let def = [PClause fc newnm lhs [] rhs []]

786+ elabClauses info fc opts newnm def

787+

788+ specName (ImplicitS, tm)

789+ | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

790+ specName (ExplicitS, tm)

791+ | (P Ref n _, _) <- unApply tm = Just (n, Just 1)

792+ specName _ = Nothing

793+

794+ concreteArg ist (ImplicitS, tm) = concreteTm ist tm

795+ concreteArg ist (ExplicitS, tm) = concreteTm ist tm

796+ concreteArg ist _ = True

797+

798+ concreteTm ist tm | (P _ n _, _) <- unApply tm =

799+ case lookupTy n (tt_ctxt ist) of

800+ [] -> False

801+ _ -> True

802+ concreteTm ist _ = False

803+

804+ -- get the type of a specialised application

805+ getSpecTy ist (n, args)

806+ = case lookupTy n (tt_ctxt ist) of

807+ [ty] -> let specty = normalise (tt_ctxt ist) [] (specType args ty) in

808+ trace (show specty) $ mkPE_TyDecl ist args

809+ (explicitNames specty)

810+-- (normalise (tt_ctxt ist) [] (specType args ty))

811+ _ -> error "Can't happen (getSpecTy)"

812+

813+ getSpecClause ist (n, args)

814+ = let newnm = UN (show (nsroot n) ++ "__spectest") in -- UN (show n ++ show (map snd args)) in

815+ (n, newnm, mkPE_TermDecl ist newnm n args)

816+

817+

752

818

753-- Elaborate a value, returning any new bindings created (this will only

819-- Elaborate a value, returning any new bindings created (this will only

754-- happen if elaborating as a pattern clause)

820-- happen if elaborating as a pattern clause)

755−

756elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

821elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

757elabValBind info aspat tm_in

822elabValBind info aspat tm_in

758 = do ctxt <- getContext

823 = do ctxt <- getContext

src/Idris/PartialEval.hs+103−1

@@ -1,6 +1,10 @@

1+{-# LANGUAGE PatternGuards #-}

1−module Idris.PartialEval(partial_eval) where

3+module Idris.PartialEval(partial_eval, getSpecApps, specType,

4+ mkPE_TyDecl, mkPE_TermDecl, PEArgType(..)) where

3import Idris.AbsSyntax

6import Idris.AbsSyntax

7+import Idris.Delaborate

5import Core.TT

9import Core.TT

6import Core.Evaluate

10import Core.Evaluate

@@ -18,3 +22,101 @@ partial_eval ctxt ns tms = map peClause tms where

19 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

23 toLimit (n, Nothing) = (n, 65536) -- somewhat arbitrary reduction limit

20 toLimit (n, Just l) = (n, l)

24 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+