37748ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add transformation rules for partial evaluation

37748ceEdwin Brady12 years ago

idris.cabal+1

compare with master

unifiedsplit

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

595 , Idris.Elab.Class

596 , Idris.Elab.Instance

597 , Idris.Elab.Provider

598+ , Idris.Elab.Transform

598 , Idris.Elab.Value

599 , Idris.Elab.Value

599

600

600 , Idris.AbsSyntax

601 , Idris.AbsSyntax

src/Idris/AbsSyntax.hs+17−5

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

111 idris_language_extensions = ErrorReflection : idris_language_extensions i

112 }

113

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

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

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

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

117+addTrans basefn t

115−addTrans t = do i <- getIState

118+ = do i <- getIState

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

120+ Just def -> (t : def)

121+ Nothing -> [t]

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

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

123+ (idris_transforms i) }

117

124

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

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

119addErrRev t = do i <- getIState

126addErrRev t = do i <- getIState

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

1061 let stpos = staticList statics' tm

1068 let stpos = staticList statics' tm

1062 i <- getIState

1069 i <- getIState

1063 when (not (null statics)) $

1070 when (not (null statics)) $

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

1072+ ++ showTmImpls ptm

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

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

1065 ++ "\n" ++ show stnames ++ "\n" ++ show dnames

1074 ++ "\n" ++ show stnames ++ "\n" ++ show dnames

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

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

1067 addIBC (IBCStatic n)

1076 addIBC (IBCStatic n)

1068 where

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

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

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

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

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

1072 else if (not (searchArg p))

1084 else if (not (searchArg p))

src/Idris/AbsSyntaxTree.hs+5−4

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

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

162 idris_tyinfodata :: Ctxt TIData,

163 idris_fninfo :: Ctxt FnInfo,

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

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

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

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

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

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

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

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

170 -- ^ Full application LHS on source line

171 -- ^ Full application LHS on source line

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

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

172 idris_coercions :: [Name],

173 idris_coercions :: [Name],

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

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

175 syntax_rules :: [Syntax],

176 syntax_keywords :: [String],

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

264 | IBCTotal Name Totality

265 | IBCFlags Name [FnOpt]

266 | IBCFnInfo Name FnInfo

267− | IBCTrans (Term, Term)

267+ | IBCTrans Name (Term, Term)

268 | IBCErrRev (Term, Term)

269 | IBCCG Name

270 | IBCDoc Name

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

284idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

285 emptyContext emptyContext emptyContext emptyContext

286 emptyContext emptyContext emptyContext emptyContext

287− emptyContext emptyContext emptyContext

287+ emptyContext emptyContext emptyContext emptyContext

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

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

289 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

291 AutomaticWidth S.empty Nothing Nothing []

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

365 | Warranty

366 | PrintDef Name

367 | PPrint OutputFmt Int PTerm

368+ | TransformInfo Name

368

369

369data OutputFmt = HTMLOutput | LaTeXOutput

370data OutputFmt = HTMLOutput | LaTeXOutput

370

371

src/Idris/Coverage.hs+5−5

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

65 logLvl 5 $ show lhss

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

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

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

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

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

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

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

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

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

77 _ -> repeat (pexp Placeholder)

78 let tryclauses = mkClauses parg all_args

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

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

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

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

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

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

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

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

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

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

85 return new

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

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

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

14import Idris.Primitives

15import Idris.Inliner

16import Idris.PartialEval

17+import Idris.Transforms

17import Idris.DeepSeq

18import Idris.DeepSeq

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

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

19import IRTS.Lang

20import IRTS.Lang

21import Idris.Elab.Type

22import Idris.Elab.Type

23+import Idris.Elab.Transform

22import Idris.Elab.Utils

24import Idris.Elab.Utils

24import Idris.Core.TT

26import Idris.Core.TT

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

48import Data.List.Split (splitOn)

50import Data.List.Split (splitOn)

50import Util.Pretty(pretty, text)

52import Util.Pretty(pretty, text)

53+import Numeric

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

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

53-- top-level definition.

56-- top-level definition.

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

81 addIBC (IBCOpt n)

84 addIBC (IBCOpt n)

83 ist <- getIState

86 ist <- getIState

87+ let tpats = transformPats ist pats_in

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

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

89+ doPartialEval ist tpats

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

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

87 -- show l ++ " = " ++

92 -- show l ++ " = " ++

88 -- show r) pats))

93 -- show r) pats))

89 let tcase = opt_typecase (idris_options ist)

94 let tcase = opt_typecase (idris_options ist)

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

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

98+ -- for partially evaluated definitions

99+ mapM_ (\ e -> case e of

100+ Left _ -> return ()

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

102+

103+ -- Redo transforms with the newly generated transformations

104+ let pats_transformed = transformPats ist pats

105+

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

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

92 --

107 --

93 -- pats_in -> pats -> pdef -> pdef'

108 -- pats_in -> pats -> pdef -> pdef'

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

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

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

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

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

99 -- further inlined to help with totality checking.

114 -- further inlined to help with totality checking.

100− let pdef = map debind pats

115+ let pdef = map debind pats_transformed

101

116

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

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

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

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

104

119

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−

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

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

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

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

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

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

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

120 numArgs <- tclift $ sameLength pdef

128 numArgs <- tclift $ sameLength pdef

121

129

122 case specNames opts of

130 case specNames opts of

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

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

124 _ -> return ()

132 _ -> return ()

125

133

126 erInfo <- getErasureInfo <$> getIState

134 erInfo <- getErasureInfo <$> getIState

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

163 -- then case tot of

171 -- then case tot of

164 -- Total _ -> return ()

172 -- Total _ -> return ()

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

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

166− -- else return ()

167 -- _ -> return ()

174 -- _ -> return ()

168 case tree of

175 case tree of

169 CaseDef _ _ [] -> return ()

176 CaseDef _ _ [] -> return ()

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

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

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

272 sameLength [] = return 0

279 sameLength [] = return 0

273

280

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

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

275− -- user defined transformation rules later)

282+ doPartialEval ist pats =

276− doTransforms ist pats =

277 case specNames opts of

283 case specNames opts of

278 Nothing -> pats

284 Nothing -> pats

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

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

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

285 let sa = getSpecApps ist [] r

291 let sa = getSpecApps ist [] r

286 mapM_ (mkSpecialised ist) sa

292 mapM_ (mkSpecialised ist) sa

287 where

293 where

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

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

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

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

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

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

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

291 -- transformation.

298 -- transformation.

292

299

293− -- Apply that transformation after every PClauses elaboration

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

294

301

295 mkSpecialised ist specapp_in = do

302 mkSpecialised ist specapp_in = do

296 let (specTy, specapp) = getSpecTy ist specapp_in

303 let (specTy, specapp) = getSpecTy ist specapp_in

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

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

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

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

299 [] -> True

306 [] -> True

300 _ -> False

307 _ -> False

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

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

302 idrisCatch

309 idrisCatch

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

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

304 cgns <- getAllNames n

311 cgns <- getAllNames n

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

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

306 mapMaybe specName (snd specapp))]

313 mapMaybe specName (snd specapp))]

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

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

315+ ++ " with " ++ show cgns

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

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

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

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

310 ++ "\n" ++ show opts

318 ++ "\n" ++ show opts

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

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

312− showSep "\n"

320+-- showSep "\n"

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

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

314 (showTmImpls lhs ++ " = " ++

322 (showTmImpls lhs ++ " = " ++

315− showTmImpls rhs)) pats)

323+ showTmImpls rhs) -- pats)

324+

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

326+ show rhs ++ " ==> " ++ show lhs

327+

316 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

328 elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

329+ elabTransform info fc False rhs lhs

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

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

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

318− elabClauses info fc opts newnm def

332+ elabClauses info fc opts newnm def)

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

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

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

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

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

322 -- lifted out).

335 -- lifted out).

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

351

364

352 -- get the clause of a specialised application

365 -- get the clause of a specialised application

353 getSpecClause ist (n, args)

366 getSpecClause ist (n, args)

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

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

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

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

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

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

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

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

358 where showArg (ExplicitS, n) = show n

371 where showArg (ExplicitS, n) = show n

359 showArg (ImplicitS, n) = show n

372 showArg (ImplicitS, n) = show n

360 showArg _ = ""

373 showArg _ = ""

361

374

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

376+ -- function.

377+ qhash :: Int -> String -> String

378+ qhash acc [] = showHex acc ""

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

380+

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

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

363-- possible, otherwise Nothing.

382-- possible, otherwise Nothing.

364

383

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

28import Idris.Elab.Class

29import Idris.Elab.Instance

30import Idris.Elab.Provider

31+import Idris.Elab.Transform

31import Idris.Elab.Value

32import Idris.Elab.Value

33import Idris.Core.TT

34import Idris.Core.TT

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

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

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

142 }

143 }

143

144

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

175

145

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

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

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

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

src/Idris/IBC.hs+5−5

@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)

32import Util.Zlib (decompressEither)

34ibcVersion :: Word8

35−ibcVersion = 81

35+ibcVersion = 82

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

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

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

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

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

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

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

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

67 ibc_coercions :: [Name],

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

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

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

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

234ibc 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 }

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

237ibc i (IBCLineApp fp l t) f

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

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

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

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

492

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

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

494−pTrans ts = mapM_ addTrans ts

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

495

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

497pErrRev ts = mapM_ addErrRev ts

src/Idris/PartialEval.hs+2−2

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

109

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

111mkPE_TermDecl :: IState -> Name -> Name ->

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

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

113mkPE_TermDecl ist newname sname ns

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

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

116− [(lhs, rhs)] where

116+ (lhs, rhs) where

117 mkp [] = []

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

119 mkp (_ : tms) = mkp tms

src/Idris/REPL.hs+20

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

1188 [] -> iPrintError "Not found"

1189 outs -> iRenderResult . vsep $ outs

1190

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

1191

1211

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

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

1193 = do outs <- pprintDef n

1213 = do outs <- pprintDef n

src/Idris/REPLParser.hs+1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Transforms.hs+12−47

@@ -1,57 +1,22 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.Transforms where

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

5import Idris.AbsSyntax

6import Idris.Core.CaseTree

7import Idris.Core.TT

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

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

12−class Transform a where

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

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

11+ [Either Term (Term, Term)]

12+transformPats ist ps = map tClause ps where

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

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

15+ = let rhs' = applyTransRules ist rhs in

16+ Right (lhs, rhs')

15−instance Transform (TT Name) where

18+applyTransRules :: IState -> Term -> Term

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

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

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

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

22+applyAll ts t = t