77b1faf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Switch on 'elabPE'

77b1fafEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+5−3

compare with master

unifiedsplit

@@ -879,15 +879,15 @@ addStatics n tm ptm =

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

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

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

882− when (not (null statics)) $

883− logLvl 7 $ show n ++ " " ++ show statics ++ "\n" ++ show dynamics

884− ++ "\n" ++ show stnames ++ "\n" ++ show dnames

885 -- also get the arguments which are 'uniquely inferrable' from

882 -- also get the arguments which are 'uniquely inferrable' from

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

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

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

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

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

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

889 let stpos = staticList statics' tm

886 let stpos = staticList statics' tm

890 i <- getIState

887 i <- getIState

888+ when (not (null statics)) $

889+ logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics

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

891 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

892 addIBC (IBCStatic n)

893 where

@@ -899,6 +899,8 @@ addStatics n tm ptm =

899 else (static, dynamic)

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

901

902+ freeArgNames (Bind n (Pi ty) sc)

903+ = nub $ freeArgNames ty

902 freeArgNames tm = let (_, args) = unApply tm in

904 freeArgNames tm = let (_, args) = unApply tm in

903 concatMap freeNames args

905 concatMap freeNames args

904

906

src/Idris/ElabDecls.hs+27−22

@@ -613,11 +613,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

613 -- Look for 'static' names and generate new specialised

614 -- definitions for them

615

616− {-

617 mapM_ (\ e -> case e of

616 mapM_ (\ e -> case e of

618 Left _ -> return ()

617 Left _ -> return ()

619 Right (l, r) -> elabPE info fc n r) pats

618 Right (l, r) -> elabPE info fc n r) pats

620− -}

621

619

622 -- NOTE: Need to store original definition so that proofs which

620 -- NOTE: Need to store original definition so that proofs which

623 -- rely on its structure aren't affected by any changes to the

621 -- rely on its structure aren't affected by any changes to the

@@ -789,36 +787,39 @@ elabPE info fc caller r =

789 let sa = getSpecApps ist [] r

787 let sa = getSpecApps ist [] r

790 mapM_ (mkSpecialised ist) sa

788 mapM_ (mkSpecialised ist) sa

791 where

789 where

792− -- TODO: Freeze the newly defined name, make sure it never gets

793− -- reduced when specialising (not quite the same as an 'abstract' name

794− -- so may need a new class (public/abstract/private/specialised)

795−

796− -- Add a PTerm level transformation rule, which is basically the

790+ -- TODO: Add a PTerm level transformation rule, which is basically the

797 -- new definition in reverse (before specialising it).

791 -- new definition in reverse (before specialising it).

798 -- RHS => LHS where implicit arguments are left blank in the

792 -- RHS => LHS where implicit arguments are left blank in the

799 -- transformation.

793 -- transformation.

800

794

801 -- Apply that transformation after every PClauses elaboration

795 -- Apply that transformation after every PClauses elaboration

802

796

803− mkSpecialised ist specapp = do

797+ mkSpecialised ist specapp_in = do

804− iputStrLn (show specapp)

798+ let (specTy, specapp) = getSpecTy ist specapp_in

805− let specTy = getSpecTy ist specapp

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

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

807 let undef = case lookupDef newnm (tt_ctxt ist) of

800 let undef = case lookupDef newnm (tt_ctxt ist) of

808 [] -> True

801 [] -> True

809 _ -> False

802 _ -> False

810− iputStrLn $ show (newnm, map (concreteArg ist) (snd specapp))

803+ logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))

804+ idrisCatch

811− when (undef && all (concreteArg ist) (snd specapp)) $ do

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

812 let opts = [Specialise ((n, Nothing) :

806 let opts = [Specialise ((n, Nothing) :

813 (mapMaybe specName (snd specapp)))]

807 (mapMaybe specName (snd specapp)))]

814− iputStrLn (show specapp)

808+ logLvl 3 $ "Specialising application: " ++ show specapp

809+ logLvl 2 $ "New name: " ++ show newnm

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

810+ iLOG $ "PE definition type : " ++ (show specTy)

816 ++ "\n" ++ show opts

811 ++ "\n" ++ show opts

817− iputStrLn $ "PE definition " ++ show newnm ++ ":\n" ++

812+ logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++

818− (show lhs ++ " = " ++ show rhs)

813+ (showImp Nothing True False lhs ++ " = " ++

814+ showImp Nothing True False rhs)

819 elabType info defaultSyntax "" fc opts newnm specTy

815 elabType info defaultSyntax "" fc opts newnm specTy

820 let def = [PClause fc newnm lhs [] rhs []]

816 let def = [PClause fc newnm lhs [] rhs []]

821 elabClauses info fc opts newnm def

817 elabClauses info fc opts newnm def

818+ logLvl 1 $ "Specialised " ++ show newnm)

819+ -- if it doesn't work, just don't specialise. Could happen for lots

820+ -- of valid reasons (e.g. local variables in scope which can't be

821+ -- lifted out).

822+ (\e -> logLvl 4 $ "Couldn't specialise: " ++ (pshow ist e))

822

823

823 specName (ImplicitS, tm)

824 specName (ImplicitS, tm)

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

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

@@ -840,17 +841,21 @@ elabPE info fc caller r =

840 -- get the type of a specialised application

841 -- get the type of a specialised application

841 getSpecTy ist (n, args)

842 getSpecTy ist (n, args)

842 = case lookupTy n (tt_ctxt ist) of

843 = case lookupTy n (tt_ctxt ist) of

844+ [ty] -> let (specty_in, args') = specType args (explicitNames ty)

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

845+ specty = normalise (tt_ctxt ist) [] (finalise specty_in)

844− trace (show specty) $ mkPE_TyDecl ist args

845− (explicitNames specty)

846+ t = mkPE_TyDecl ist args' (explicitNames specty) in

847+ (t, (n, args'))

846-- (normalise (tt_ctxt ist) [] (specType args ty))

848-- (normalise (tt_ctxt ist) [] (specType args ty))

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

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

848

850

849 getSpecClause ist (n, args)

851 getSpecClause ist (n, args)

850− = let newnm = UN (show (nsroot n) ++ "_" ++ show (nsroot caller) ++

852+ = let newnm = UN ("__"++show (nsroot n) ++ "_" ++

853+ showSep "_" (map showArg args)) in

851− "__spectest") in -- UN (show n ++ show (map snd args)) in

854+ -- UN (show n ++ show (map snd args)) in

852 (n, newnm, mkPE_TermDecl ist newnm n args)

855 (n, newnm, mkPE_TermDecl ist newnm n args)

853−

856+ where showArg (ExplicitS, n) = show n

857+ showArg (ImplicitS, n) = show n

858+ showArg _ = ""

854

859

855

860

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

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

src/Idris/ParseExpr.hs+4−10

@@ -686,7 +686,6 @@ Pi ::=

686 | '|'? Static? '{' TypeDeclList '}' '->' Expr

687 | '{' 'auto' TypeDeclList '}' '->' Expr

688 | '{' 'default' TypeDeclList '}' '->' Expr

689− | '{' 'static' '}' Expr' '->' Expr

690 ;

689 ;

691 -}

690 -}

692

691

@@ -709,7 +708,8 @@ pi syn =

709 symbol "->"

708 symbol "->"

710 sc <- expr syn

709 sc <- expr syn

711 return (bindList (PPi

710 return (bindList (PPi

712− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do

711+ (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))

712+ <|> (do

713 reserved "default"

714 when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"

715 script <- simpleExpr syn

@@ -717,14 +717,8 @@ pi syn =

717 lchar '}'

718 symbol "->"

719 sc <- expr syn

720− return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do

720+ return (bindList (PPi (TacImp False Dynamic script "")) xt sc))

721− reserved "static"

722− lchar '}'

723− t <- expr' syn

724− symbol "->"

725− sc <- expr syn

726− return (PPi (Exp False Static "" False) (MN 42 "__pi_arg") t sc)) <|> (

727− if implicitAllowed syn then do

721+ <|> (if implicitAllowed syn then do

728 xt <- typeDeclList syn

722 xt <- typeDeclList syn

729 lchar '}'

723 lchar '}'

730 symbol "->"

724 symbol "->"

src/Idris/PartialEval.hs+48−20

@@ -9,6 +9,7 @@ import Idris.Delaborate

9import Core.TT

10import Core.Evaluate

12+import Control.Monad.State

12import Debug.Trace

13import Debug.Trace

14partial_eval :: Context -> [(Name, Maybe Int)] ->

15partial_eval :: Context -> [(Name, Maybe Int)] ->

@@ -23,26 +24,52 @@ partial_eval ctxt ns tms = map peClause tms where

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

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

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

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

26−specType :: [(PEArgType, Term)] -> Type -> Type

27+specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])

28+specType args ty = let (t, args') = runState (unifyEq args ty) [] in

29+ (st (map fst args') t, map fst args')

30+ where

27−specType ((ExplicitS, v) : xs) (Bind n (Pi t) sc)

31+ st ((ExplicitS, v) : xs) (Bind n (Pi t) sc)

28− = Bind n (Let t v) (specType xs sc)

32+ = Bind n (Let t v) (st xs sc)

29−specType ((ImplicitS, v) : xs) (Bind n (Pi t) sc)

33+ st ((ImplicitS, v) : xs) (Bind n (Pi t) sc)

30− = Bind n (Let t v) (specType xs sc)

34+ = Bind n (Let t v) (st xs sc)

35+ st ((UnifiedD, _) : xs) (Bind n (Pi t) sc)

36+ = st xs sc

31−specType (_ : xs) (Bind n (Pi t) sc)

37+ st (_ : xs) (Bind n (Pi t) sc)

32− = Bind n (Pi t) (specType xs sc)

38+ = Bind n (Pi t) (st xs sc)

33−specType _ t = t

39+ st _ t = t

40+

41+ unifyEq (imp@(ImplicitD, v) : xs) (Bind n (Pi t) sc)

42+ = do amap <- get

43+ case lookup imp amap of

44+ Just n' ->

45+ do put (amap ++ [((UnifiedD, Erased), n)])

46+ sc' <- unifyEq xs (subst n (P Bound n' Erased) sc)

47+ return (Bind n (Pi t) sc') -- erase later

48+ _ -> do put (amap ++ [(imp, n)])

49+ sc' <- unifyEq xs sc

50+ return (Bind n (Pi t) sc')

51+ unifyEq (x : xs) (Bind n (Pi t) sc)

52+ = do args <- get

53+ put (args ++ [(x, n)])

54+ sc' <- unifyEq xs sc

55+ return (Bind n (Pi t) sc')

56+ unifyEq xs t = do args <- get

57+ put (args ++ (zip xs (repeat (UN "_"))))

58+ return t

35mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

60mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

61+mkPE_TyDecl ist args ty = mkty args ty

62+ where

36−mkPE_TyDecl ist ((ExplicitD, v) : xs) (Bind n (Pi t) sc)

63+ mkty ((ExplicitD, v) : xs) (Bind n (Pi t) sc)

37− = PPi expl n (delab ist t) (mkPE_TyDecl ist xs sc)

64+ = PPi expl n (delab ist t) (mkty xs sc)

38−mkPE_TyDecl ist ((ImplicitD, v) : xs) (Bind n (Pi t) sc)

65+ mkty ((ImplicitD, v) : xs) (Bind n (Pi t) sc)

39− | concreteClass ist t = mkPE_TyDecl ist xs sc

66+ | concreteClass ist t = mkty xs sc

40− | classConstraint ist t

67+ | classConstraint ist t

41− = PPi constraint n (delab ist t) (mkPE_TyDecl ist xs sc)

68+ = PPi constraint n (delab ist t) (mkty xs sc)

42− | otherwise = PPi impl n (delab ist t) (mkPE_TyDecl ist xs sc)

69+ | otherwise = PPi impl n (delab ist t) (mkty xs sc)

43−mkPE_TyDecl ist (_ : xs) t

70+ mkty (_ : xs) t

44− = mkPE_TyDecl ist xs t

71+ = mkty xs t

45−mkPE_TyDecl ist [] t = delab ist t

72+ mkty [] t = delab ist t

47classConstraint ist v

74classConstraint ist v

48 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of

75 | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of

@@ -81,7 +108,8 @@ mkPE_TermDecl ist newname sname ns

108

82data PEArgType = ImplicitS | ImplicitD

109data PEArgType = ImplicitS | ImplicitD

83 | ExplicitS | ExplicitD

110 | ExplicitS | ExplicitD

111+ | UnifiedD

84− deriving Show

112+ deriving (Eq, Show)

113

86getSpecApps :: IState -> [Name] -> Term ->

114getSpecApps :: IState -> [Name] -> Term ->

87 [(Name, [(PEArgType, Term)])]

115 [(Name, [(PEArgType, Term)])]

@@ -94,7 +122,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

94 | x && imparg imp = (ImplicitS, tm)

122 | x && imparg imp = (ImplicitS, tm)

95 | x = (ExplicitS, tm)

123 | x = (ExplicitS, tm)

96 | imparg imp = (ImplicitD, tm)

124 | imparg imp = (ImplicitD, tm)

97− | otherwise = (ExplicitD, (P Ref (MN n "arg") Erased))

125+ | otherwise = (ExplicitD, (P Ref (UN (show n ++ "arg")) Erased))

126

99 imparg (PExp _ _ _ _) = False

127 imparg (PExp _ _ _ _) = False

100 imparg _ = True

128 imparg _ = True

test/test001/test001.idr+1−1

@@ -38,7 +38,7 @@ using (G : Vect n Ty)

38 index_first = stop

39 index_next = pop

41− interp : Env G -> {static} Expr G t -> interpTy t

41+ interp : Env G -> [static] (e : Expr G t) -> interpTy t

42 interp env (Var i) = lookup i env

43 interp env (Val x) = x

44 interp env (Lam sc) = \x => interp (x :: env) sc

test/test014/Resimp.idr+1−1

@@ -119,7 +119,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

119 ioret : a -> IO a

120 ioret = return

121

122− interp : Env gam -> {static} Res gam gam' t ->

122+ interp : Env gam -> [static] (e : Res gam gam' t) ->

123 (Env gam' -> interpTy t -> IO u) -> IO u

124

125 interp env (Let val scope) k

test/test014/test014.idr+1

@@ -64,3 +64,4 @@ readH fn = res (do let x = open fn Reading

64main : IO ()

65main = run (readH "test")

67+