66f4f9e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Extend split/splitOnLine to cope with 'where/with'

Main interface is via 'splitOnLine'. Give a source line, and a variable name, provides information of what each variable should be updated to in resulting pattern clauses, in the following form: [[(name_a1, pattern_a1), (name_b1, pattern_b1), ...], [(name_a2, pattern_a2), (name_b2, pattern_b2), ...], ... [(name_an, pattern_an), (name_bn, pattern_bn), ...]] where the name expands into 'n' possible patterns, and the names 'name_a', 'name_b' etc need to be expanded to 'pattern_a', 'pattern_b' etc in the resulting patterns (due e.g. to dependency). An interactive editor should probably just use this information to do a textual replacement on the original pattern, expanding into 'n' new patterns.

commit66f4f9ea8624996065cde6abcc4358a4f1ae96f9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 27 Oct 2013, 14:25 (13 years ago) parent8c19e30

8 files changed+118−50

compare with master

unifiedsplit

src/Core/Evaluate.hs+1−1 src/Idris/AbsSyntax.hs+9−10 src/Idris/AbsSyntaxTree.hs+7−6 src/Idris/CaseSplit.hs+75−21 src/Idris/ElabDecls.hs+13−6 src/Idris/IBC.hs+6−6 src/Idris/REPL.hs+4 src/Idris/REPLParser.hs+3

src/Core/Evaluate.hs+1−1

@@ -10,7 +10,7 @@ module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

1010 addDatatype, addCasedef, simplifyCasedef, addOperator,

1111 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

1212 lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

13− Value(..), Quote(..), evalState, initEval) where

13+ Value(..), Quote(..), initEval) where

1414

1515import Debug.Trace

1616import Control.Monad.State

src/Idris/AbsSyntax.hs+9−10

@@ -235,17 +235,16 @@ getName = do i <- getIState;

235235 putIState $ (i { idris_name = idx + 1 })

236236 return idx

237237

238−addInternalName :: FilePath -> Int -> Name -> Int -> Idris ()

239−addInternalName fp l n w

238+addInternalApp :: FilePath -> Int -> PTerm -> Idris ()

239+addInternalApp fp l t

240240 = do i <- getIState

241− putIState (i { idris_linename = ((fp, l), (n, w)) : idris_linename i })

242−

243−getInternalName :: FilePath -> Int -> Name -- ^ default name

244− -> Idris (Name, Int)

245−getInternalName fp l n = do i <- getIState

246− case lookup (fp, l) (idris_linename i) of

247− Nothing -> return (n, 0)

248− Just n' -> return n'

241+ putIState (i { idris_lineapps = ((fp, l), t) : idris_lineapps i })

242+

243+getInternalApp :: FilePath -> Int -> Idris PTerm

244+getInternalApp fp l = do i <- getIState

245+ case lookup (fp, l) (idris_lineapps i) of

246+ Just n' -> return n'

247+ -- TODO: What if it's not there?

249248

250249checkUndefined :: FC -> Name -> Idris ()

251250checkUndefined fc n

src/Idris/AbsSyntaxTree.hs+7−6

@@ -100,9 +100,8 @@ data IState = IState {

100100 idris_log :: String,

101101 idris_options :: IOption,

102102 idris_name :: Int,

103− idris_linename :: [((FilePath, Int), (Name, Int))],

104− -- ^ internal name for function defined on that line,

105− -- number of 'with' arguments

103+ idris_lineapps :: [((FilePath, Int), PTerm)],

104+ -- ^ Full application LHS on source line

106105 idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

107106 idris_coercions :: [Name],

108107 idris_transforms :: [(Term, Term)],

@@ -179,7 +178,7 @@ data IBCWrite = IBCFix FixDecl

179178 | IBCDoc Name

180179 | IBCCoercion Name

181180 | IBCDef Name -- i.e. main context

182− | IBCLineName FilePath Int Name Int

181+ | IBCLineApp FilePath Int PTerm

183182 deriving Show

184183

185184idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

@@ -240,6 +239,7 @@ data Command = Quit

240239 | DebugInfo Name

241240 | Search PTerm

242241 | CaseSplit Name PTerm

242+ | CaseSplitAt Int Name

243243 | SetOpt Opt

244244 | UnsetOpt Opt

245245 | NOP

@@ -416,13 +416,14 @@ deriving instance Binary PDecl'

416416--

417417-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)

418418--

419−-- 2. The list of patterns

419+-- 2. The list of extra 'with' patterns

420420--

421421-- 3. The right-hand side

422422--

423423-- 4. The where block (PDecl' t)

424+

424425data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

425− | PWith FC Name t [t] t [PDecl' t]

426+ | PWith FC Name t [t] t [PDecl' t]

426427 | PClauseR FC [t] t [PDecl' t]

427428 | PWithR FC [t] t [PDecl' t]

428429 deriving Functor

src/Idris/CaseSplit.hs+75−21

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

11{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split) where

3+module Idris.CaseSplit(split, splitOnLine) where

55-- splitting a variable in a pattern clause

@@ -8,14 +8,22 @@ import Idris.AbsSyntax

88import Idris.ElabDecls

99import Idris.ElabTerm

1010import Idris.Delaborate

11+import Idris.Parser

1112import Idris.Error

1213

1314import Core.TT

15+import Core.Typecheck

1416import Core.Evaluate

1517

1618import Data.Maybe

1719import Control.Monad

18−import Control.Monad.State

20+import Control.Monad.State.Strict

21+

22+import Text.Parser.Combinators

23+import Text.Parser.Char(anyChar)

24+import Text.Trifecta(Result(..), parseString)

25+import Text.Trifecta.Delta

26+import qualified Data.ByteString.UTF8 as UTF8

1927

2028{-

2129

@@ -31,9 +39,12 @@ Always take the "more specific" argument when there is a discrepancy, i.e.

3139names over '_', patterns over names, etc.

3240-}

3341

34−split :: Name -> PTerm -> Idris [PTerm]

42+-- Given a variable to split, and a term application, return a list of

43+-- variable updates

44+split :: Name -> PTerm -> Idris [[(Name, PTerm)]]

3545split n t'

3646 = do (tm, ty, pats) <- elabValBind toplevel True t'

47+ logLvl 4 ("Elaborated:\n" ++ show tm ++ " : " ++ show ty ++ "\n" ++ show pats)

3748 ist <- getIState

3849-- iputStrLn (show (delab ist tm) ++ " : " ++ show (delab ist ty))

3950-- iputStrLn (show pats)

@@ -43,25 +54,48 @@ split n t'

4354 Nothing -> fail $ show n ++ " is not a pattern variable"

4455 Just ty ->

4556 do let splits = findPats ist ty

57+ iLOG ("New patterns " ++ show splits)

4658 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

59+ logLvl 4 ("Trying " ++ showSep "\n" (map show newPats_in))

4760 newPats <- mapM elabNewPat newPats_in

48− logLvl 5 (showSep "\n" (map show (t : mapMaybe id newPats)))

49− logLvl 5 "----"

50− let newPats' = evalState (mapM (mergePat ctxt t)

51− (mapMaybe id newPats))

52− []

53− return newPats'

54−

55−mergePat :: Context -> PTerm -> PTerm -> State [(Name, Name)] PTerm

61+ logLvl 3 ("Original:\n" ++ show t)

62+ logLvl 3 ("Split:\n" ++

63+ (showSep "\n" (map show (mapMaybe id newPats))))

64+ logLvl 3 "----"

65+ let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)

66+ iLOG ("Name updates " ++ showSep "\n"

67+ (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

68+ return (map snd newPats')

69+

70+data MergeState = MS { namemap :: [(Name, Name)],

71+ updates :: [(Name, PTerm)] }

72+

73+addUpdate n tm = do ms <- get

74+ put (ms { updates = ((n, tm) : updates ms) } )

75+

76+mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

77+mergeAllPats ctxt t [] = []

78+mergeAllPats ctxt t (p : ps)

79+ = let (p', MS _ u) = runState (mergePat ctxt t p) (MS [] [])

80+ ps' = mergeAllPats ctxt t ps in

81+ ((p, u) : ps')

82+

83+mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm

5684-- If any names are unified, make sure they stay unified. Always prefer

5785-- user provided name (first pattern)

86+mergePat ctxt (PPatvar fc n) new

87+ = mergePat ctxt (PRef fc n) new

88+mergePat ctxt old (PPatvar fc n)

89+ = mergePat ctxt old (PRef fc n)

5890mergePat ctxt orig@(PRef fc n) new@(PRef _ n')

59− | isConName n' ctxt = return new

91+ | isConName n' ctxt = do addUpdate n new;

92+ return new

6093 | otherwise

61− = do nmap <- get

62− case lookup n' nmap of

63− Just x -> return (PRef fc x)

64− Nothing -> do put ((n', n) : nmap)

94+ = do ms <- get

95+ case lookup n' (namemap ms) of

96+ Just x -> do addUpdate n (PRef fc x)

97+ return (PRef fc x)

98+ Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })

6599 return (PRef fc n)

66100mergePat ctxt (PApp _ _ args) (PApp fc f args')

67101 = do newArgs <- zipWithM mergeArg args args'

@@ -72,15 +106,17 @@ mergePat ctxt (PApp _ _ args) (PApp fc f args')

72106 return (y { machine_inf = machine_inf x,

73107 getTm = tm' })

74108 _ -> return (y { getTm = tm' })

75−mergePat ctxt (PRef fc n) t = tidy t

109+mergePat ctxt (PRef fc n) t = do tm <- tidy t

110+ addUpdate n tm

111+ return tm

76112mergePat ctxt x y = return y

77113

78114mergeUserImpl :: PTerm -> PTerm -> PTerm

79115mergeUserImpl x y = x

80116

81117tidy orig@(PRef fc n)

82− = do nmap <- get

83− case lookup n nmap of

118+ = do ms <- get

119+ case lookup n (namemap ms) of

84120 Just x -> return (PRef fc x)

85121 Nothing -> case n of

86122 (UN _) -> return orig

@@ -118,6 +154,8 @@ findPats ist t = [Placeholder]

118154replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm

119155replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

120156 where subst :: PTerm -> PTerm

157+ subst orig@(PPatvar _ v) | v == n = t

158+ | otherwise = Placeholder

121159 subst orig@(PRef _ v) | v == n = t

122160 | isConName v ctxt = orig

123161 subst (PRef _ _) = Placeholder

@@ -128,5 +166,21 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

128166

129167replaceVar ctxt n t pat = pat

130168

131−

132−

169+splitOnLine :: Int -- ^ line number

170+ -> Name -- ^ variable

171+ -> FilePath -- ^ name of file

172+ -> String -- ^ file contents

173+ -> Idris [[(Name, PTerm)]]

174+splitOnLine l n fn inp = do

175+-- let (before, later) = splitAt (l-1) (lines inp)

176+-- i <- getIState

177+ cl <- getInternalApp fn l

178+ logLvl 3 ("Working with " ++ showImp Nothing True False cl)

179+ tms <- split n cl

180+-- iputStrLn (showSep "\n" (map show tms))

181+ return tms -- "" -- not yet done...

182+

183+getFnName (PClause _ n _ _ _ _) = n

184+getFnName (PWith _ n _ _ _ _) = n

185+

186+

src/Idris/ElabDecls.hs+13−6

@@ -801,6 +801,7 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

801801elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

802802 = do let tcgen = Dictionary `elem` opts

803803 ctxt <- getContext

804+

804805 -- Build the LHS as an "Infer", and pull out its type and

805806 -- pattern bindings

806807 i <- getIState

@@ -815,6 +816,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

815816 let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))

816817 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)

817818 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

819+

820+ addInternalApp (fc_fname fc) (fc_line fc) lhs

821+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) lhs)

822+

818823 ((lhs', dlhs, []), _) <-

819824 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

820825 (errAt "left hand side of " fname

@@ -956,7 +961,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

956961 -- Build the LHS as an "Infer", and pull out its type and

957962 -- pattern bindings

958963 i <- getIState

959− let lhs = addImplPat i lhs_in

964+ let lhs = addImplPat i lhs_in

960965 logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

961966 ((lhs', dlhs, []), _) <-

962967 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

@@ -1009,8 +1014,6 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10091014 (substTerm wargval (P Bound (MN 0 "warg") wargtype) ret_ty)

10101015 logLvl 3 ("New function type " ++ show wtype)

10111016 let wname = MN windex (show fname)

1012− addInternalName (fc_fname fc) (fc_line fc) wname (length withs)

1013− addIBC (IBCLineName (fc_fname fc) (fc_line fc) wname (length withs))

10141017

10151018 let imps = getImps wtype -- add to implicits context

10161019 putIState (i { idris_implicits = addDef wname imps (idris_implicits i) })

@@ -1080,10 +1083,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

10801083 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

10811084 Right mvars ->

10821085 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

1083− return $ PWith fc wname lhs ws wval withs'

1086+ return $ PWith fc wname lhs ws wval withs'

10841087 mkAux wname toplhs ns ns' c

10851088 = ifail $ show fc ++ "badly formed with clause"

10861089

1090+ addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

1091+ addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

1092+

10871093 updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

10881094 = let ns = map (keepMvar (map fst mvars) fc') ns_in

10891095 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

@@ -1448,8 +1454,9 @@ decorateid decorate (PTy doc s f o n t) = PTy doc s f o (decorate n) t

14481454decorateid decorate (PClauses f o n cs)

14491455 = PClauses f o (decorate n) (map dc cs)

14501456 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

1451− dc (PWith fc n t as w ds) = PWith fc (decorate n) (dappname t) as w

1452− (map (decorateid decorate) ds)

1457+ dc (PWith fc n t as w ds)

1458+ = PWith fc (decorate n) (dappname t) as w

1459+ (map (decorateid decorate) ds)

14531460 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

14541461 dappname t = t

14551462

src/Idris/IBC.hs+6−6

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

5151 ibc_docstrings :: [(Name, String)],

5252 ibc_transforms :: [(Term, Term)],

5353 ibc_coercions :: [Name],

54− ibc_linenames :: [(FilePath, Int, Name, Int)]

54+ ibc_lineapps :: [(FilePath, Int, PTerm)]

5555 }

5656 deriving Show

5757{-!

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

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

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

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

138−ibc i (IBCLineName fp l n w) f

139− = return f { ibc_linenames = (fp,l,n, w) : ibc_linenames f }

138+ibc i (IBCLineApp fp l t) f

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

140140

141141process :: IBCFile -> FilePath -> Idris ()

142142process i fn

@@ -171,7 +171,7 @@ process i fn

171171 pDocs (ibc_docstrings i)

172172 pCoercions (ibc_coercions i)

173173 pTrans (ibc_transforms i)

174− pLineNames (ibc_linenames i)

174+ pLineApps (ibc_lineapps i)

175175

176176timestampOlder :: FilePath -> FilePath -> IO ()

177177timestampOlder src ibc = do srct <- getModificationTime src

@@ -316,8 +316,8 @@ pCoercions ns = mapM_ (\ n -> addCoercion n) ns

316316pTrans :: [(Term, Term)] -> Idris ()

317317pTrans ts = mapM_ addTrans ts

318318

319−pLineNames :: [(FilePath, Int, Name, Int)] -> Idris ()

320−pLineNames ls = mapM_ (\ (f, i, n, w) -> addInternalName f i n w) ls

319+pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

320+pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

321321

322322----- Generated by 'derive'

323323

src/Idris/REPL.hs+4

@@ -426,6 +426,10 @@ process fn (Search t) = iPrintError "Not implemented"

426426process fn (CaseSplit n t)

427427 = do tms <- split n t

428428 iputStrLn (showSep "\n" (map show tms))

429+process fn (CaseSplitAt l n)

430+ = do src <- runIO $ readFile fn

431+ res <- splitOnLine l n fn src

432+ iputStrLn (showSep "\n" (map show res))

429433process fn (Spec t) = do (tm, ty) <- elabVal toplevel False t

430434 ctxt <- getContext

431435 ist <- getIState

src/Idris/REPLParser.hs+3

@@ -70,6 +70,9 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

7070 <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))

7171 <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))

7272 <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))

73+ <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

74+ l <- P.natural; n <- P.name;

75+ return (CaseSplitAt (fromInteger l) n))

7376 <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

7477 n <- P.name;

7578 t <- P.fullExpr defaultSyntax;