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

git.iko.soy/Idris-dev

on master help sign in

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

66f4f9eEdwin Brady13 years ago

src/Core/Evaluate.hs+1−1

compare with master

unifiedsplit

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

10 addDatatype, addCasedef, simplifyCasedef, addOperator,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,

12 lookupTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

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

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

15import Debug.Trace

16import Control.Monad.State

src/Idris/AbsSyntax.hs+9−10

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

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

236 return idx

237

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

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

239−addInternalName fp l n w

239+addInternalApp fp l t

240 = do i <- getIState

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

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

242−

242+

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

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

244− -> Idris (Name, Int)

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

244+getInternalApp fp l = do i <- getIState

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

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

247− Nothing -> return (n, 0)

248− Just n' -> return n'

246+ Just n' -> return n'

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

249

248

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

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

251checkUndefined fc n

250checkUndefined fc n

src/Idris/AbsSyntaxTree.hs+7−6

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

100 idris_log :: String,

101 idris_options :: IOption,

102 idris_name :: Int,

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

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

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

104+ -- ^ Full application LHS on source line

105− -- number of 'with' arguments

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

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

107 idris_coercions :: [Name],

106 idris_coercions :: [Name],

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

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

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

179 | IBCDoc Name

178 | IBCDoc Name

180 | IBCCoercion Name

179 | IBCCoercion Name

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

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

182− | IBCLineName FilePath Int Name Int

181+ | IBCLineApp FilePath Int PTerm

183 deriving Show

182 deriving Show

184

183

185idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

184idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

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

240 | DebugInfo Name

239 | DebugInfo Name

241 | Search PTerm

240 | Search PTerm

242 | CaseSplit Name PTerm

241 | CaseSplit Name PTerm

242+ | CaseSplitAt Int Name

243 | SetOpt Opt

244 | UnsetOpt Opt

245 | NOP

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

416--

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

418--

419−-- 2. The list of patterns

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

420--

421-- 3. The right-hand side

422--

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

424+

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

425data 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]

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

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

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

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

428 deriving Functor

429 deriving Functor

src/Idris/CaseSplit.hs+75−21

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

1{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split) where

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

5-- splitting a variable in a pattern clause

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

8import Idris.ElabDecls

9import Idris.ElabTerm

10import Idris.Delaborate

11+import Idris.Parser

11import Idris.Error

12import Idris.Error

13import Core.TT

14import Core.TT

15+import Core.Typecheck

14import Core.Evaluate

16import Core.Evaluate

16import Data.Maybe

18import Data.Maybe

17import Control.Monad

19import 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

20{-

28{-

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

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

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

32-}

40-}

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

43+-- variable updates

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

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

35split n t'

45split n t'

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

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

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

37 ist <- getIState

48 ist <- getIState

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

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

39-- iputStrLn (show pats)

50-- iputStrLn (show pats)

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

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

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

44 Just ty ->

55 Just ty ->

45 do let splits = findPats ist ty

56 do let splits = findPats ist ty

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

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

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

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

47 newPats <- mapM elabNewPat newPats_in

60 newPats <- mapM elabNewPat newPats_in

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

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

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

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

49− logLvl 5 "----"

64+ logLvl 3 "----"

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

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

51− (mapMaybe id newPats))

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

52− []

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

53− return newPats'

68+ return (map snd newPats')

54−

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+

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

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

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

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

57-- user provided name (first pattern)

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

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

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

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

59− | isConName n' ctxt = return new

92+ return new

60 | otherwise

93 | otherwise

61− = do nmap <- get

94+ = do ms <- get

62− case lookup n' nmap of

95+ case lookup n' (namemap ms) of

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

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

97+ return (PRef fc x)

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

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

65 return (PRef fc n)

99 return (PRef fc n)

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

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

67 = do newArgs <- zipWithM mergeArg args args'

101 = do newArgs <- zipWithM mergeArg args args'

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

72 return (y { machine_inf = machine_inf x,

106 return (y { machine_inf = machine_inf x,

73 getTm = tm' })

107 getTm = tm' })

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

108 _ -> 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

76mergePat ctxt x y = return y

112mergePat ctxt x y = return y

113

78mergeUserImpl :: PTerm -> PTerm -> PTerm

114mergeUserImpl :: PTerm -> PTerm -> PTerm

79mergeUserImpl x y = x

115mergeUserImpl x y = x

116

81tidy orig@(PRef fc n)

117tidy orig@(PRef fc n)

82− = do nmap <- get

118+ = do ms <- get

83− case lookup n nmap of

119+ case lookup n (namemap ms) of

84 Just x -> return (PRef fc x)

120 Just x -> return (PRef fc x)

85 Nothing -> case n of

121 Nothing -> case n of

86 (UN _) -> return orig

122 (UN _) -> return orig

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

118replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm

154replaceVar :: Context -> Name -> PTerm -> PTerm -> PTerm

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

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

120 where subst :: PTerm -> PTerm

156 where subst :: PTerm -> PTerm

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

158+ | otherwise = Placeholder

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

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

122 | isConName v ctxt = orig

160 | isConName v ctxt = orig

123 subst (PRef _ _) = Placeholder

161 subst (PRef _ _) = Placeholder

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

128

166

129replaceVar ctxt n t pat = pat

167replaceVar ctxt n t pat = pat

130

168

131−

169+splitOnLine :: Int -- ^ line number

132−

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

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

802 = do let tcgen = Dictionary `elem` opts

803 ctxt <- getContext

804+

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

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

805 -- pattern bindings

806 -- pattern bindings

806 i <- getIState

807 i <- getIState

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

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

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

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

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

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

818 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+

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

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

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

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

820 (errAt "left hand side of " fname

825 (errAt "left hand side of " fname

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

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

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

957 -- pattern bindings

962 -- pattern bindings

958 i <- getIState

963 i <- getIState

959− let lhs = addImplPat i lhs_in

964+ let lhs = addImplPat i lhs_in

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

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

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

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

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

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

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

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

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

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

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

1011 let wname = MN windex (show fname)

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

1014

1017

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

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

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

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

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

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

1081 Right mvars ->

1084 Right mvars ->

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

1085 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'

1084 mkAux wname toplhs ns ns' c

1087 mkAux wname toplhs ns ns' c

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

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

1086

1089

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+

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

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

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

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

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

1095 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

1448decorateid decorate (PClauses f o n cs)

1454decorateid decorate (PClauses f o n cs)

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

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

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

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

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

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

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

1452− (map (decorateid decorate) ds)

1459+ (map (decorateid decorate) ds)

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

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

1454 dappname t = t

1461 dappname t = t

1455

1462

src/Idris/IBC.hs+6−6

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

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

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

53 ibc_coercions :: [Name],

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

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

55 }

56 deriving Show

57{-!

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

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

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

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

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

138+ibc i (IBCLineApp fp l t) f

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

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

140

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

142process i fn

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

171 pDocs (ibc_docstrings i)

172 pCoercions (ibc_coercions i)

173 pTrans (ibc_transforms i)

174− pLineNames (ibc_linenames i)

174+ pLineApps (ibc_lineapps i)

175

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

177timestampOlder src ibc = do srct <- getModificationTime src

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

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

317pTrans ts = mapM_ addTrans ts

318

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

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

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

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

321

322----- Generated by 'derive'

323

src/Idris/REPL.hs+4

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

426process fn (CaseSplit n t)

427 = do tms <- split n t

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

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

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

430 ctxt <- getContext

434 ctxt <- getContext

431 ist <- getIState

435 ist <- getIState

src/Idris/REPLParser.hs+3

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

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

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

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

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

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

74 n <- P.name;

77 n <- P.name;

75 t <- P.fullExpr defaultSyntax;

78 t <- P.fullExpr defaultSyntax;