44ec9a2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1582 from edwinb/partial-eval

Partial evaluation

commit44ec9a2faa71f6ad9d902bc99d23d442ae3f70e9 authorEdwin Brady <edwin.brady@gmail.com> dateSat 4 Oct 2014, 20:57 (12 years ago) parentb65a1c2 146858d

12 files changed+272−129

compare with master

unifiedsplit

idris.cabal+1 src/Idris/AbsSyntax.hs+17−5 src/Idris/AbsSyntaxTree.hs+5−4 src/Idris/Coverage.hs+5−5 src/Idris/Elab/Clause.hs+54−29 src/Idris/Elab/Transform.hs+98 src/Idris/ElabDecls.hs+1−31 src/Idris/IBC.hs+4−4 src/Idris/PartialEval.hs+3−2 src/Idris/REPL.hs+20 src/Idris/REPLParser.hs+1 src/Idris/Transforms.hs+63−49

idris.cabal+1

@@ -595,6 +595,7 @@ Library

595595 , Idris.Elab.Class

596596 , Idris.Elab.Instance

597597 , Idris.Elab.Provider

598+ , Idris.Elab.Transform

598599 , Idris.Elab.Value

599600

600601 , Idris.AbsSyntax

src/Idris/AbsSyntax.hs+17−5

@@ -111,9 +111,16 @@ addLangExt ErrorReflection = do i <- getIState

111111 idris_language_extensions = ErrorReflection : idris_language_extensions i

112112 }

113113

114−addTrans :: (Term, Term) -> Idris ()

115−addTrans t = do i <- getIState

116− putIState $ i { idris_transforms = t : idris_transforms i }

114+-- Transforms are organised by the function being applied on the lhs of the

115+-- transform, to make looking up appropriate transforms quicker

116+addTrans :: Name -> (Term, Term) -> Idris ()

117+addTrans basefn t

118+ = do i <- getIState

119+ let t' = case lookupCtxtExact basefn (idris_transforms i) of

120+ Just def -> (t : def)

121+ Nothing -> [t]

122+ putIState $ i { idris_transforms = addDef basefn t'

123+ (idris_transforms i) }

117124

118125addErrRev :: (Term, Term) -> Idris ()

119126addErrRev t = do i <- getIState

@@ -1061,12 +1068,17 @@ addStatics n tm ptm =

10611068 let stpos = staticList statics' tm

10621069 i <- getIState

10631070 when (not (null statics)) $

1064− logLvl 5 $ show n ++ " " ++ show statics' ++ "\n" ++ show dynamics

1071+ logLvl 2 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

1072+ ++ showTmImpls ptm

1073+ ++ show statics' ++ "\n" ++ show dynamics

10651074 ++ "\n" ++ show stnames ++ "\n" ++ show dnames

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

10671076 addIBC (IBCStatic n)

10681077 where

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

1078+ initStatics (Bind n (Pi ty _) sc) (PPi p n' t s)

1079+ | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in

1080+ (static, (n, ty) : dynamic)

1081+ initStatics (Bind n (Pi ty _) sc) (PPi p n' _ s)

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

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

10721084 else if (not (searchArg p))

src/Idris/AbsSyntaxTree.hs+5−4

@@ -161,6 +161,7 @@ data IState = IState {

161161 idris_docstrings :: Ctxt (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]),

162162 idris_tyinfodata :: Ctxt TIData,

163163 idris_fninfo :: Ctxt FnInfo,

164+ idris_transforms :: Ctxt [(Term, Term)],

164165 idris_totcheck :: [(FC, Name)], -- names to check totality on

165166 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

166167 idris_totcheckfail :: [(FC, String)],

@@ -170,7 +171,6 @@ data IState = IState {

170171 -- ^ Full application LHS on source line

171172 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

172173 idris_coercions :: [Name],

173− idris_transforms :: [(Term, Term)],

174174 idris_errRev :: [(Term, Term)],

175175 syntax_rules :: [Syntax],

176176 syntax_keywords :: [String],

@@ -264,7 +264,7 @@ data IBCWrite = IBCFix FixDecl

264264 | IBCTotal Name Totality

265265 | IBCFlags Name [FnOpt]

266266 | IBCFnInfo Name FnInfo

267− | IBCTrans (Term, Term)

267+ | IBCTrans Name (Term, Term)

268268 | IBCErrRev (Term, Term)

269269 | IBCCG Name

270270 | IBCDoc Name

@@ -284,8 +284,8 @@ idrisInit :: IState

284284idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

285285 emptyContext emptyContext emptyContext emptyContext

286286 emptyContext emptyContext emptyContext emptyContext

287− emptyContext emptyContext emptyContext

288− [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

287+ emptyContext emptyContext emptyContext emptyContext

288+ [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

289289 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

290290 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

291291 AutomaticWidth S.empty Nothing Nothing []

@@ -365,6 +365,7 @@ data Command = Quit

365365 | Warranty

366366 | PrintDef Name

367367 | PPrint OutputFmt Int PTerm

368+ | TransformInfo Name

368369

369370data OutputFmt = HTMLOutput | LaTeXOutput

370371

src/Idris/Coverage.hs+5−5

@@ -65,7 +65,7 @@ genClauses fc n xs given

6565 logLvl 5 $ show lhss

6666 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

6767 logLvl 10 $ show argss ++ "\n" ++ show all_args

68− logLvl 1 $ "Original: \n" ++

68+ logLvl 3 $ "Original: \n" ++

6969 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

7070 -- add an infinite supply of explicit arguments to update the possible

7171 -- cases for (the return type may be variadic, or function type, so

@@ -76,11 +76,11 @@ genClauses fc n xs given

7676 p ++ repeat (PExp 0 [] (sMN 0 "gcarg") Placeholder)

7777 _ -> repeat (pexp Placeholder)

7878 let tryclauses = mkClauses parg all_args

79− logLvl 2 $ show (length tryclauses) ++ " initially to check"

80− logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)

79+ logLvl 3 $ show (length tryclauses) ++ " initially to check"

80+ logLvl 2 $ showSep "\n" (map (showTm i) tryclauses)

8181 let new = filter (noMatch i) (nub tryclauses)

82− logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

83− logLvl 3 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

82+ logLvl 2 $ show (length new) ++ " clauses to check for impossibility"

83+ logLvl 4 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

8484-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

8585 return new

8686-- return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Elab/Clause.hs+54−29

@@ -14,11 +14,13 @@ import Idris.Providers

1414import Idris.Primitives

1515import Idris.Inliner

1616import Idris.PartialEval

17+import Idris.Transforms

1718import Idris.DeepSeq

1819import Idris.Output (iputStrLn, pshow, iWarn)

1920import IRTS.Lang

2021

2122import Idris.Elab.Type

23+import Idris.Elab.Transform

2224import Idris.Elab.Utils

2325

2426import Idris.Core.TT

@@ -48,6 +50,7 @@ import Data.Char(isLetter, toLower)

4850import Data.List.Split (splitOn)

4951

5052import Util.Pretty(pretty, text)

53+import Numeric

5154

5255-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

5356-- top-level definition.

@@ -81,13 +84,31 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

8184 addIBC (IBCOpt n)

8285

8386 ist <- getIState

84− let pats = map (simple_lhs (tt_ctxt ist)) $ doTransforms ist pats_in

87+ -- Don't apply rules if this is a partial evaluation definition,

88+ -- or we'll make something that just runs itself!

89+ let tpats = case specNames opts of

90+ Nothing -> transformPats ist pats_in

91+ _ -> pats_in

92+

93+ let pats = map (simple_lhs (tt_ctxt ist)) $

94+ doPartialEval ist tpats

8595

8696 -- logLvl 3 (showSep "\n" (map (\ (l,r) ->

8797 -- show l ++ " = " ++

8898 -- show r) pats))

8999 let tcase = opt_typecase (idris_options ist)

90100

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

102+ -- definitions for them, as well as generating rewrite rules

103+ -- for partially evaluated definitions

104+ mapM_ (\ e -> case e of

105+ Left _ -> return ()

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

107+

108+ -- Redo transforms with the newly generated transformations

109+ ist <- getIState

110+ let pats_transformed = transformPats ist pats

111+

91112 -- Summary of what's about to happen: Definitions go:

92113 --

93114 -- pats_in -> pats -> pdef -> pdef'

@@ -97,18 +118,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

97118 -- pdef is the compile-time pattern definition.

98119 -- This will get further optimised for run-time, and, separately,

99120 -- further inlined to help with totality checking.

100− let pdef = map debind pats

121+ let pdef = map debind pats_transformed

101122

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

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

104125

105− -- Look for 'static' names and generate new specialised

106− -- definitions for them

107−

108− mapM_ (\ e -> case e of

109− Left _ -> return ()

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

111−

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

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

114128 -- inliner. Just use the inlined version to generate pdef' and to

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

120134 numArgs <- tclift $ sameLength pdef

121135

122136 case specNames opts of

123− Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

137+ Just _ -> logLvl 1 $ "Partially evaluated:\n" ++ show pats

124138 _ -> return ()

125139

126140 erInfo <- getErasureInfo <$> getIState

@@ -163,7 +177,6 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

163177 -- then case tot of

164178 -- Total _ -> return ()

165179 -- t -> tclift $ tfail (At fc (Msg (show n ++ " is " ++ show t)))

166− -- else return ()

167180 -- _ -> return ()

168181 case tree of

169182 CaseDef _ _ [] -> return ()

@@ -271,9 +284,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

271284 else tfail (At fc (Msg "Clauses have differing numbers of arguments "))

272285 sameLength [] = return 0

273286

274− -- apply all transformations (just specialisation for now, add

275− -- user defined transformation rules later)

276− doTransforms ist pats =

287+ -- Partially evaluate, if the definition is marked as specialisable

288+ doPartialEval ist pats =

277289 case specNames opts of

278290 Nothing -> pats

279291 Just ns -> partial_eval (tt_ctxt ist) ns pats

@@ -285,38 +297,45 @@ elabPE info fc caller r =

285297 let sa = getSpecApps ist [] r

286298 mapM_ (mkSpecialised ist) sa

287299 where

288− -- TODO: Add a PTerm level transformation rule, which is basically the

300+ -- Make a specialised version of the application, and

301+ -- add a PTerm level transformation rule, which is basically the

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

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

291304 -- transformation.

292305

293− -- Apply that transformation after every PClauses elaboration

306+ -- Transformation rules are applied after every PClause elaboration

294307

295308 mkSpecialised ist specapp_in = do

296309 let (specTy, specapp) = getSpecTy ist specapp_in

297− let (n, newnm, pats) = getSpecClause ist specapp

310+ let (n, newnm, (lhs, rhs)) = getSpecClause ist specapp

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

299312 [] -> True

300313 _ -> False

301− logLvl 5 $ show (newnm, map (concreteArg ist) (snd specapp))

314+ logLvl 3 $ show (newnm, map (concreteArg ist) (snd specapp))

302315 idrisCatch

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

304317 cgns <- getAllNames n

305318 let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++

306319 mapMaybe specName (snd specapp))]

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

308− logLvl 2 $ "New name: " ++ show newnm

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

321+ ++ " with " ++ show cgns

322+ logLvl 3 $ "New name: " ++ show newnm

323+ logLvl 3 $ "PE definition type : " ++ (show specTy)

310324 ++ "\n" ++ show opts

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

312− showSep "\n"

313− (map (\ (lhs, rhs) ->

325+ logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++

326+-- showSep "\n"

327+-- (map (\ (lhs, rhs) ->

314328 (showTmImpls lhs ++ " = " ++

315− showTmImpls rhs)) pats)

329+ showTmImpls rhs) -- pats)

330+

331+ logLvl 2 $ show n ++ " transformation rule: " ++

332+ show rhs ++ " ==> " ++ show lhs

333+

316334 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

317− let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

318− elabClauses info fc opts newnm def

319− logLvl 2 $ "Specialised " ++ show newnm)

335+ let def = -- map (\ (lhs, rhs) ->

336+ [PClause fc newnm lhs [] rhs []] --) pats

337+ elabTransform info fc False rhs lhs

338+ elabClauses info fc opts newnm def)

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

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

322341 -- lifted out).

@@ -351,14 +370,20 @@ elabPE info fc caller r =

351370

352371 -- get the clause of a specialised application

353372 getSpecClause ist (n, args)

354− = let newnm = sUN ("__"++show (nsroot n) ++ "_" ++

355− showSep "_" (map showArg args)) in

373+ = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++

374+ qhash 0 (showSep "_" (map showArg args))) in

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

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

358377 where showArg (ExplicitS, n) = show n

359378 showArg (ImplicitS, n) = show n

360379 showArg _ = ""

361380

381+ -- TMP for readability! This is obviously a really bad hashing

382+ -- function.

383+ qhash :: Int -> String -> String

384+ qhash acc [] = showHex acc ""

385+ qhash acc (x:xs) = qhash (fromEnum x + acc) xs

386+

362387-- checks if the clause is a possible left hand side. Returns the term if

363388-- possible, otherwise Nothing.

364389

src/Idris/Elab/Transform.hsnew file+98

@@ -0,0 +1,98 @@

1+{-# LANGUAGE PatternGuards #-}

2+module Idris.Elab.Transform where

4+import Idris.AbsSyntax

5+import Idris.ASTUtils

6+import Idris.DSL

7+import Idris.Error

8+import Idris.Delaborate

9+import Idris.Imports

10+import Idris.ElabTerm

11+import Idris.Coverage

12+import Idris.DataOpts

13+import Idris.Providers

14+import Idris.Primitives

15+import Idris.Inliner

16+import Idris.PartialEval

17+import Idris.DeepSeq

18+import Idris.Output (iputStrLn, pshow, iWarn)

19+import IRTS.Lang

20+

21+import Idris.Elab.Utils

22+

23+import Idris.Core.TT

24+import Idris.Core.Elaborate hiding (Tactic(..))

25+import Idris.Core.Evaluate

26+import Idris.Core.Execute

27+import Idris.Core.Typecheck

28+import Idris.Core.CaseTree

29+

30+import Idris.Docstrings

31+

32+import Prelude hiding (id, (.))

33+import Control.Category

34+

35+import Control.Applicative hiding (Const)

36+import Control.DeepSeq

37+import Control.Monad

38+import Control.Monad.State.Strict as State

39+import Data.List

40+import Data.Maybe

41+import Debug.Trace

42+

43+import qualified Data.Map as Map

44+import qualified Data.Set as S

45+import qualified Data.Text as T

46+import Data.Char(isLetter, toLower)

47+import Data.List.Split (splitOn)

48+

49+import Util.Pretty(pretty, text)

50+

51+elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

52+elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53+ = do ctxt <- getContext

54+ i <- getIState

55+ let lhs = addImplPat i lhs_in

56+ ((lhs', dlhs, []), _) <-

57+ tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

58+ (erun fc (buildTC i info ELHS [] (sUN "transform")

59+ (infTerm lhs)))

60+ let lhs_tm = orderPats (getInferTerm lhs')

61+ let lhs_ty = getInferType lhs'

62+ let newargs = pvars i lhs_tm

63+

64+ (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm

65+ logLvl 3 ("Transform LHS " ++ show clhs_tm)

66+ let rhs = addImplBound i (map fst newargs) rhs_in

67+ ((rhs', defer), _) <-

68+ tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

69+ (do pbinds i lhs_tm

70+ setNextName

71+ erun fc (build i info ERHS [] (sUN "transform") rhs)

72+ erun fc $ psolve lhs_tm

73+ tt <- get_term

74+ return (runState (collectDeferred Nothing tt) []))

75+ (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

76+ logLvl 3 ("Transform RHS " ++ show crhs_tm)

77+ -- Types must always convert

78+ case converts ctxt [] clhs_ty crhs_ty of

79+ OK _ -> return ()

80+ Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

81+ -- In safe mode, values must convert (Thinks: This is probably not

82+ -- useful as is, perhaps it should require a proof of equality instead)

83+ when safe $ case converts ctxt [] clhs_tm crhs_tm of

84+ OK _ -> return ()

85+ Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

86+

87+ case unApply (depat clhs_tm) of

88+ (P _ tfname _, _) -> do addTrans tfname (clhs_tm, crhs_tm)

89+ addIBC (IBCTrans tf (clhs_tm, crhs_tm))

90+ _ -> ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

91+

92+ where

93+ depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc)

94+ depat x = x

95+

96+elabTransform info fc safe lhs_in rhs_in

97+ = ierror (At fc (Msg "Invalid transformation rule (must be function application)"))

98+

src/Idris/ElabDecls.hs+1−31

@@ -28,6 +28,7 @@ import Idris.Elab.Record

2828import Idris.Elab.Class

2929import Idris.Elab.Instance

3030import Idris.Elab.Provider

31+import Idris.Elab.Transform

3132import Idris.Elab.Value

3233

3334import Idris.Core.TT

@@ -141,37 +142,6 @@ elabPrims = do mapM_ (elabDecl' EAll recinfo)

141142 idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i

142143 }

143144

144−elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

145−elabTransform info fc safe lhs_in rhs_in

146− = do ctxt <- getContext

147− i <- getIState

148− let lhs = addImplPat i lhs_in

149− ((lhs', dlhs, []), _) <-

150− tclift $ elaborate ctxt (sMN 0 "transLHS") infP []

151− (erun fc (buildTC i info ELHS [] (sUN "transform")

152− (infTerm lhs)))

153− let lhs_tm = orderPats (getInferTerm lhs')

154− let lhs_ty = getInferType lhs'

155− let newargs = pvars i lhs_tm

156−

157− (clhs_tm, clhs_ty) <- recheckC fc [] lhs_tm

158− logLvl 3 ("Transform LHS " ++ show clhs_tm)

159− let rhs = addImplBound i (map fst newargs) rhs_in

160− ((rhs', defer), _) <-

161− tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty []

162− (do pbinds i lhs_tm

163− setNextName

164− erun fc (build i info ERHS [] (sUN "transform") rhs)

165− erun fc $ psolve lhs_tm

166− tt <- get_term

167− return (runState (collectDeferred Nothing tt) []))

168− (crhs_tm, crhs_ty) <- recheckC fc [] rhs'

169− logLvl 3 ("Transform RHS " ++ show crhs_tm)

170− when safe $ case converts ctxt [] clhs_tm crhs_tm of

171− OK _ -> return ()

172− Error e -> ierror (At fc (CantUnify False clhs_tm crhs_tm e [] 0))

173− addTrans (clhs_tm, crhs_tm)

174− addIBC (IBCTrans (clhs_tm, crhs_tm))

175145

176146elabDecls :: ElabInfo -> [PDecl] -> Idris ()

177147elabDecls info ds = do mapM_ (elabDecl EAll info) ds

src/Idris/IBC.hs+4−4

@@ -62,7 +62,7 @@ data IBCFile = IBCFile { ver :: Word8,

6262 ibc_cg :: [(Name, CGInfo)],

6363 ibc_defs :: [(Name, Def)],

6464 ibc_docstrings :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))],

65− ibc_transforms :: [(Term, Term)],

65+ ibc_transforms :: [(Name, (Term, Term))],

6666 ibc_errRev :: [(Term, Term)],

6767 ibc_coercions :: [Name],

6868 ibc_lineapps :: [(FilePath, Int, PTerm)],

@@ -232,7 +232,7 @@ ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

232232ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

233233ibc i (IBCFnInfo n a) f = return f { ibc_fninfo = (n,a) : ibc_fninfo f }

234234ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

235−ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

235+ibc i (IBCTrans n t) f = return f { ibc_transforms = (n, t) : ibc_transforms f }

236236ibc i (IBCErrRev t) f = return f { ibc_errRev = t : ibc_errRev f }

237237ibc i (IBCLineApp fp l t) f

238238 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

@@ -490,8 +490,8 @@ pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

490490pCoercions :: [Name] -> Idris ()

491491pCoercions ns = mapM_ (\ n -> addCoercion n) ns

492492

493−pTrans :: [(Term, Term)] -> Idris ()

494−pTrans ts = mapM_ addTrans ts

493+pTrans :: [(Name, (Term, Term))] -> Idris ()

494+pTrans ts = mapM_ (\ (n, t) -> addTrans n t) ts

495495

496496pErrRev :: [(Term, Term)] -> Idris ()

497497pErrRev ts = mapM_ addErrRev ts

src/Idris/PartialEval.hs+3−2

@@ -109,11 +109,11 @@ concreteClass ist v

109109

110110-- | Creates a new clause for a specialised function application

111111mkPE_TermDecl :: IState -> Name -> Name ->

112− [(PEArgType, Term)] -> [(PTerm, PTerm)]

112+ [(PEArgType, Term)] -> (PTerm, PTerm)

113113mkPE_TermDecl ist newname sname ns

114114 = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))

115115 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns)) in

116− [(lhs, rhs)] where

116+ (lhs, rhs) where

117117 mkp [] = []

118118 mkp ((ExplicitD, tm) : tms) = delab ist tm : mkp tms

119119 mkp (_ : tms) = mkp tms

@@ -168,6 +168,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

168168-- _ -> []

169169 else []

170170 _ -> []

171+ ga env (Bind n (Let t v) sc) = ga env v ++ ga (n : env) sc

171172 ga env (Bind n t sc) = ga (n : env) sc

172173 ga env t = []

173174

src/Idris/REPL.hs+20

@@ -1188,6 +1188,26 @@ process fn (PrintDef n) =

11881188 [] -> iPrintError "Not found"

11891189 outs -> iRenderResult . vsep $ outs

11901190

1191+-- Show relevant transformation rules for the name 'n'

1192+process fn (TransformInfo n)

1193+ = do i <- getIState

1194+ let ts = lookupCtxt n (idris_transforms i)

1195+ let res = map (showTrans i) ts

1196+ iRenderResult . vsep $ concat res

1197+ where showTrans :: IState -> [(Term, Term)] -> [Doc OutputAnnotation]

1198+ showTrans i [] = []

1199+ showTrans i ((lhs, rhs) : ts)

1200+ = let ppTm tm = annotate (AnnTerm [] tm) .

1201+ pprintPTerm (ppOptionIst i) [] [] [] .

1202+ delab i $ tm

1203+ ts' = showTrans i ts in

1204+ ppTm lhs <+> text " ==> " <+> ppTm rhs : ts'

1205+

1206+-- iRenderOutput (pretty lhs)

1207+-- iputStrLn " ==> "

1208+-- iPrintTermWithType (pprintDelab i rhs)

1209+-- iputStrLn "---------------"

1210+-- showTrans i ts

11911211

11921212process fn (PPrint fmt width (PRef _ n))

11931213 = do outs <- pprintDef n

src/Idris/REPLParser.hs+1

@@ -41,6 +41,7 @@ pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit

4141 <|> do c <- cmd ["d", "def"]; fnNameArg c Defn

4242 <|> do c <- cmd ["total"]; fnNameArg c TotCheck

4343 <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef

44+ <|> do c <- cmd ["transinfo"]; fnNameArg c TransformInfo

4445 <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls

4546 <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho

4647 <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo

src/Idris/Transforms.hs+63−49

@@ -1,57 +1,71 @@

11{-# LANGUAGE PatternGuards #-}

3−module Idris.Transforms where

3+module Idris.Transforms(transformPats, applyTransRules) where

55import Idris.AbsSyntax

66import Idris.Core.CaseTree

77import Idris.Core.TT

9−data TTOpt = TermTrans (TT Name -> TT Name) -- term transform

10− | CaseTrans (SC -> SC) -- case expression transform

11−

12−class Transform a where

13− transform :: TTOpt -> a -> a

14−

15−instance Transform (TT Name) where

16− transform o@(TermTrans t) tm = trans t tm where

17− trans t (Bind n b tm) = t $ Bind n (transform o b) (trans t tm)

18− trans t (App f a) = t $ App (trans t f) (trans t a)

19− trans t tm = t tm

20− transform _ tm = tm

21−

22−instance Transform a => Transform (Binder a) where

23− transform t (Let ty v) = Let (transform t ty) (transform t v)

24− transform t b = b { binderTy = transform t (binderTy b) }

25−

26−instance Transform SC where

27− transform o@(CaseTrans t) sc = trans t sc where

28− trans t (Case up n alts) = t (Case up n (map (transform o) alts))

29− trans t x = t x

30− transform o@(TermTrans t) sc = trans t sc where

31− trans t (Case up n alts) = Case up n (map (transform o) alts)

32− trans t (STerm tm) = STerm (t tm)

33− trans t x = x

34−

35−instance Transform CaseAlt where

36− transform o (ConCase n i ns sc) = ConCase n i ns (transform o sc)

37− transform o (ConstCase c sc) = ConstCase c (transform o sc)

38− transform o (DefaultCase sc) = DefaultCase (transform o sc)

39−

40−natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

41−

42−zname = sNS (sUN "Z") ["Nat","Prelude"]

43−sname = sNS (sUN "S") ["Nat","Prelude"]

44−

45−zero :: TT Name -> TT Name

46−zero (P _ n _) | n == zname

47− = Constant (BI 0)

48−zero x = x

49−

50−suc :: TT Name -> TT Name

51−suc (App (P _ s _) a) | s == sname

52− = mkApp (P Ref (sUN "prim__addBigInt") Erased) [Constant (BI 1), a]

53−suc x = x

54−

55−natcase :: SC -> SC

56−natcase = undefined

9+import Debug.Trace

10+

11+transformPats :: IState -> [Either Term (Term, Term)] ->

12+ [Either Term (Term, Term)]

13+transformPats ist ps = map tClause ps where

14+ tClause (Left t) = Left t -- not a clause, leave it alone

15+ tClause (Right (lhs, rhs)) -- apply transforms on RHS

16+ = let rhs' = applyTransRules ist rhs in

17+ Right (lhs, rhs')

18+

19+applyTransRules :: IState -> Term -> Term

20+applyTransRules ist tm = applyAll (idris_transforms ist) tm

21+

22+applyAll :: Ctxt [(Term, Term)] -> Term -> Term

23+applyAll ts ap@(App f a)

24+ | (P _ fn ty, args) <- unApply ap

25+ = case lookupCtxtExact fn ts of

26+ Just rules -> case applyFnRules rules ap of

27+ Just tm' -> tm'

28+ _ -> App (applyAll ts f) (applyAll ts a)

29+ Nothing -> App (applyAll ts f) (applyAll ts a)

30+applyAll ts (Bind n b sc) = Bind n (fmap (applyAll ts) b) (applyAll ts sc)

31+applyAll ts t = t

32+

33+applyFnRules :: [(Term, Term)] -> Term -> Maybe Term

34+applyFnRules [] tm = Nothing

35+applyFnRules (r : rs) tm | Just tm' <- applyRule r tm = Just tm'

36+ | otherwise = applyFnRules rs tm

37+

38+applyRule :: (Term, Term) -> Term -> Maybe Term

39+applyRule (lhs, rhs) tm

40+ | Just ms <- matchTerm lhs tm

41+-- = trace ("SUCCESS " ++ show ms ++ "\n FROM\n" ++ show lhs ++

42+-- "\n" ++ show rhs

43+-- ++ "\n" ++ show tm) $

44+ = Just $ depat ms rhs

45+ | otherwise = Nothing

46+ where depat ms (Bind n (PVar t) sc)

47+ = case lookup n ms of

48+ Just tm -> depat ms (instantiate tm sc)

49+ _ -> depat ms sc -- no occurrence? Shouldn't happen

50+ depat ms tm = tm

51+

52+matchTerm :: Term -> Term -> Maybe [(Name, Term)]

53+matchTerm lhs tm = matchVars [] lhs tm

54+ where

55+ matchVars acc (Bind n (PVar t) sc) tm

56+ = matchVars (n : acc) (instantiate (P Bound n t) sc) tm

57+ matchVars acc sc tm

58+ = -- trace (show acc ++ ": " ++ show (sc, tm)) $

59+ doMatch acc sc tm

60+

61+ doMatch :: [Name] -> Term -> Term -> Maybe [(Name, Term)]

62+ doMatch ns (P _ n _) tm

63+ | n `elem` ns = return [(n, tm)]

64+ doMatch ns (App f a) (App f' a')

65+ = do fm <- doMatch ns f f'

66+ am <- doMatch ns a a'

67+ return (fm ++ am)

68+ doMatch ns x y | x == y = return []

69+ | otherwise = Nothing

70+

5771