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

git.iko.soy/Idris-dev

Switch on 'elabPE'

Generates a new specialised definition for [static] argument positions which are then elaborated recursively. Not yet transforming from the original call to the specialised definition. Also still need to take more care in how we specialise definitions - however, the mechanics of generating the new definitions is now done. Generating new definitions may fail for various reasons (scoping errors, for example). This is considered safe, and just fails silently, because it just means it's not a specialisable call. Also removed the {static} syntax because it's inconsistent. [static] only works on named pi bindings due to awkwardness in the parser.

commit77b1faf0b8f18bd4fdb9f58a4a34b1cbf869c575 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 26 Nov 2013, 16:24 (13 years ago) parent16847d5

7 files changed+87−57

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5−3 src/Idris/ElabDecls.hs+27−22 src/Idris/ParseExpr.hs+4−10 src/Idris/PartialEval.hs+48−20 test/test001/test001.idr+1−1 test/test014/Resimp.idr+1−1 test/test014/test014.idr+1

src/Idris/AbsSyntax.hs+5−3

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

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

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

881881 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

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

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

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

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

889886 let stpos = staticList statics' tm

890887 i <- getIState

888+ when (not (null statics)) $

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

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

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

892892 addIBC (IBCStatic n)

893893 where

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

899899 else (static, dynamic)

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

901901

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

903+ = nub $ freeArgNames ty

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

903905 concatMap freeNames args

904906

src/Idris/ElabDecls.hs+27−22

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

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

614614 -- definitions for them

615615

616− {-

617616 mapM_ (\ e -> case e of

618617 Left _ -> return ()

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

620− -}

621619

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

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

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

789787 let sa = getSpecApps ist [] r

790788 mapM_ (mkSpecialised ist) sa

791789 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

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

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

799793 -- transformation.

800794

801795 -- Apply that transformation after every PClauses elaboration

802796

803− mkSpecialised ist specapp = do

804− iputStrLn (show specapp)

805− let specTy = getSpecTy ist specapp

797+ mkSpecialised ist specapp_in = do

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

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

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

808801 [] -> True

809802 _ -> False

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

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

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

804+ idrisCatch

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

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

813807 (mapMaybe specName (snd specapp)))]

814− iputStrLn (show specapp)

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

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

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

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

816811 ++ "\n" ++ show opts

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

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

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

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

814+ showImp Nothing True False rhs)

819815 elabType info defaultSyntax "" fc opts newnm specTy

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

821817 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))

822823

823824 specName (ImplicitS, tm)

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

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

840841 -- get the type of a specialised application

841842 getSpecTy ist (n, args)

842843 = case lookupTy n (tt_ctxt ist) of

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

844− trace (show specty) $ mkPE_TyDecl ist args

845− (explicitNames specty)

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

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

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

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

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

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

848850

849851 getSpecClause ist (n, args)

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

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

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

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

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

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

853−

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

857+ showArg (ImplicitS, n) = show n

858+ showArg _ = ""

854859

855860

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

src/Idris/ParseExpr.hs+4−10

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

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

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

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

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

690689 ;

691690 -}

692691

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

709708 symbol "->"

710709 sc <- expr syn

711710 return (bindList (PPi

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

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

712+ <|> (do

713713 reserved "default"

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

715715 script <- simpleExpr syn

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

717717 lchar '}'

718718 symbol "->"

719719 sc <- expr syn

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

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

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

721+ <|> (if implicitAllowed syn then do

728722 xt <- typeDeclList syn

729723 lchar '}'

730724 symbol "->"

src/Idris/PartialEval.hs+48−20

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

99import Core.TT

1010import Core.Evaluate

1111

12+import Control.Monad.State

1213import Debug.Trace

1314

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

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

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

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

2526

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

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

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

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

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

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

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

36+ = st xs sc

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

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

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

3459

3560mkPE_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

61+mkPE_TyDecl ist args ty = mkty args ty

62+ where

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

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

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

66+ | concreteClass ist t = mkty xs sc

67+ | classConstraint ist t

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

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

70+ mkty (_ : xs) t

71+ = mkty xs t

72+ mkty [] t = delab ist t

4673

4774classConstraint ist v

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

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

81108

82109data PEArgType = ImplicitS | ImplicitD

83110 | ExplicitS | ExplicitD

84− deriving Show

111+ | UnifiedD

112+ deriving (Eq, Show)

85113

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

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

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

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

95123 | x = (ExplicitS, tm)

96124 | imparg imp = (ImplicitD, tm)

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

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

98126

99127 imparg (PExp _ _ _ _) = False

100128 imparg _ = True

test/test001/test001.idr+1−1

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

3838 index_first = stop

3939 index_next = pop

4040

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

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

4242 interp env (Var i) = lookup i env

4343 interp env (Val x) = x

4444 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)

119119 ioret : a -> IO a

120120 ioret = return

121121

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

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

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

124124

125125 interp env (Let val scope) k

test/test014/test014.idr+1

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

6464main : IO ()

6565main = run (readH "test")

6666

67+