git.iko.soy/Idris-dev
on master help sign in
Move interactive commands to their own module
dae7d7dEdwin Brady
idris.cabal+1
compare with master
unifiedsplit
@@ -540,6 +540,7 @@ Library
540 , Idris.IdrisDoc
540 , Idris.IdrisDoc
541 , Idris.Imports
541 , Idris.Imports
542 , Idris.Inliner
542 , Idris.Inliner
543+ , Idris.Interactive
543 , Idris.Output
544 , Idris.Output
544 , Idris.Parser
545 , Idris.Parser
545 , Idris.ParseHelpers
546 , Idris.ParseHelpers
src/Idris/Interactive.hsnew file+220
@@ -0,0 +1,220 @@
1+module Idris.Interactive(caseSplitAt, addClauseFrom, addProofClauseFrom,
2+ addMissing, makeWith, doProofSearch) where
3+
4+{- Bits and pieces for editing source files interactively, called from
5+ the REPL -}
6+
7+import Idris.Core.TT
8+import Idris.Core.Evaluate
9+import Idris.CaseSplit
10+import Idris.AbsSyntax
11+import Idris.ElabDecls
12+import Idris.Error
13+import Idris.Delaborate
14+import Idris.Output
15+
16+import Util.Pretty
17+import Util.System
18+
19+import System.FilePath
20+import System.Directory
21+import System.IO
22+import Data.Char
23+
24+
25+caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
26+caseSplitAt h fn updatefile l n
27+ = do src <- runIO $ readFile fn
28+ res <- splitOnLine l n fn
29+ iLOG (showSep "\n" (map show res))
30+ let (before, (ap : later)) = splitAt (l-1) (lines src)
31+ res' <- replaceSplits ap res
32+ let new = concat res'
33+ if updatefile
34+ then do let fb = fn ++ "~" -- make a backup!
35+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)
36+ runIO $ copyFile fb fn
37+ else -- do ihputStrLn h (show res)
38+ ihPrintResult h new
39+
40+addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
41+addClauseFrom h fn updatefile l n
42+ = do src <- runIO $ readFile fn
43+ let (before, tyline : later) = splitAt (l-1) (lines src)
44+ let indent = getIndent 0 (show n) tyline
45+ cl <- getClause l n fn
46+ -- add clause before first blank line in 'later'
47+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)
48+ if updatefile
49+ then do let fb = fn ++ "~"
50+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
51+ replicate indent ' ' ++
52+ cl ++ "\n" ++
53+ unlines rest)
54+ runIO $ copyFile fb fn
55+ else ihPrintResult h cl
56+ where
57+ getIndent i n [] = 0
58+ getIndent i n xs | take (length n) xs == n = i
59+ getIndent i n (x : xs) = getIndent (i + 1) n xs
60+
61+addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
62+addProofClauseFrom h fn updatefile l n
63+ = do src <- runIO $ readFile fn
64+ let (before, tyline : later) = splitAt (l-1) (lines src)
65+ let indent = getIndent 0 (show n) tyline
66+ cl <- getProofClause l n fn
67+ -- add clause before first blank line in 'later'
68+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)
69+ if updatefile
70+ then do let fb = fn ++ "~"
71+ runIO $ writeFile fb (unlines (before ++ nonblank) ++
72+ replicate indent ' ' ++
73+ cl ++ "\n" ++
74+ unlines rest)
75+ runIO $ copyFile fb fn
76+ else ihPrintResult h cl
77+ where
78+ getIndent i n [] = 0
79+ getIndent i n xs | take (length n) xs == n = i
80+ getIndent i n (x : xs) = getIndent (i + 1) n xs
81+
82+addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
83+addMissing h fn updatefile l n
84+ = do src <- runIO $ readFile fn
85+ let (before, tyline : later) = splitAt (l-1) (lines src)
86+ let indent = getIndent 0 (show n) tyline
87+ i <- getIState
88+ cl <- getInternalApp fn l
89+ let n' = getAppName cl
90+
91+ extras <- case lookupCtxt n' (idris_patdefs i) of
92+ [] -> return ""
93+ [(_, tms)] -> do tms' <- nameMissing tms
94+ showNew (show n ++ "_rhs") 1 indent tms'
95+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)
96+ if updatefile
97+ then do let fb = fn ++ "~"
98+ runIO $ writeFile fb (unlines (before ++ nonblank)
99+ ++ extras ++ unlines rest)
100+ runIO $ copyFile fb fn
101+ else ihPrintResult h extras
102+ where showPat = show . stripNS
103+ stripNS tm = mapPT dens tm where
104+ dens (PRef fc n) = PRef fc (nsroot n)
105+ dens t = t
106+
107+ nsroot (NS n _) = nsroot n
108+ nsroot (SN (WhereN _ _ n)) = nsroot n
109+ nsroot n = n
110+
111+ getAppName (PApp _ r _) = getAppName r
112+ getAppName (PRef _ r) = r
113+ getAppName _ = n
114+
115+ showNew nm i ind (tm : tms)
116+ = do (nm', i') <- getUniq nm i
117+ rest <- showNew nm i' ind tms
118+ return (replicate ind ' ' ++
119+ showPat tm ++ " = ?" ++ nm' ++
120+ "\n" ++ rest)
121+ showNew nm i _ [] = return ""
122+
123+ getIndent i n [] = 0
124+ getIndent i n xs | take (length n) xs == n = i
125+ getIndent i n (x : xs) = getIndent (i + 1) n xs
126+
127+
128+makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()
129+makeWith h fn updatefile l n
130+ = do src <- runIO $ readFile fn
131+ let (before, tyline : later) = splitAt (l-1) (lines src)
132+ let ind = getIndent tyline
133+ let with = mkWith tyline n
134+ -- add clause before first blank line in 'later',
135+ -- or (TODO) before first line with same indentation as tyline
136+ let (nonblank, rest) = span (\x -> not (all isSpace x) &&
137+ not (ind == getIndent x)) later
138+ if updatefile then
139+ do let fb = fn ++ "~"
140+ runIO $ writeFile fb (unlines (before ++ nonblank)
141+ ++ with ++ "\n" ++
142+ unlines rest)
143+ runIO $ copyFile fb fn
144+ else ihPrintResult h with
145+ where getIndent s = length (takeWhile isSpace s)
146+
147+
148+doProofSearch :: Handle -> FilePath -> Bool -> Bool ->
149+ Int -> Name -> [Name] -> Idris ()
150+doProofSearch h fn updatefile rec l n hints
151+ = do src <- runIO $ readFile fn
152+ let (before, tyline : later) = splitAt (l-1) (lines src)
153+ ctxt <- getContext
154+ mn <- case lookupNames n ctxt of
155+ [x] -> return x
156+ [] -> return n
157+ ns -> ierror (CantResolveAlts (map show ns))
158+ i <- getIState
159+ let (top, envlen, _) = case lookup mn (idris_metavars i) of
160+ Just (t, e, False) -> (t, e, False)
161+ _ -> (Nothing, 0, True)
162+ let fc = fileFC fn
163+ let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))
164+ (ProofSearch rec t hints)]
165+ let def = PClause fc mn (PRef fc mn) [] (body top) []
166+ newmv <- idrisCatch
167+ (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
168+ (tm, ty) <- elabVal toplevel False (PRef fc mn)
169+ ctxt <- getContext
170+ i <- getIState
171+ return . flip displayS "" . renderPretty 1.0 80 $
172+ pprintPTerm defaultPPOption [] [] (idris_infixes i)
173+ (stripNS
174+ (dropCtxt envlen
175+ (delab i (specialise ctxt [] [(mn, 1)] tm)))))
176+ (\e -> return ("?" ++ show n))
177+ if updatefile then
178+ do let fb = fn ++ "~"
179+ runIO $ writeFile fb (unlines before ++
180+ updateMeta False tyline (show n) newmv ++ "\n"
181+ ++ unlines later)
182+ runIO $ copyFile fb fn
183+ else ihPrintResult h newmv
184+ where dropCtxt 0 sc = sc
185+ dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
186+ dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
187+ dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
188+ dropCtxt _ t = t
189+
190+ stripNS tm = mapPT dens tm where
191+ dens (PRef fc n) = PRef fc (nsroot n)
192+ dens t = t
193+
194+ nsroot (NS n _) = nsroot n
195+ nsroot (SN (WhereN _ _ n)) = nsroot n
196+ nsroot n = n
197+
198+ updateMeta brack ('?':cs) n new
199+ | length cs >= length n
200+ = case splitAt (length n) cs of
201+ (mv, c:cs) ->
202+ if ((isSpace c || c == ')' || c == '}') && mv == n)
203+ then addBracket brack new ++ (c : cs)
204+ else '?' : mv ++ c : updateMeta True cs n new
205+ (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
206+ updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
207+ updateMeta brack (c:cs) n new
208+ = c : updateMeta (brack || not (isSpace c)) cs n new
209+ updateMeta brack [] n new = ""
210+
211+ addBracket False new = new
212+ addBracket True new@('(':xs) | last xs == ')' = new
213+ addBracket True new | any isSpace new = '(' : new ++ ")"
214+ | otherwise = new
215+
216+
217+
218+
219+
220+
src/Idris/REPL.hs+8−175
@@ -30,6 +30,7 @@ import Idris.Inliner
30import Idris.CaseSplit
30import Idris.CaseSplit
31import Idris.DeepSeq
31import Idris.DeepSeq
32import Idris.Output
32import Idris.Output
33+import Idris.Interactive
33import Idris.WhoCalls
34import Idris.WhoCalls
34
35
35import Paths_idris
36import Paths_idris
@@ -698,186 +699,18 @@ process h fn (DebugInfo n)
698 when (not (null cg')) $ do iputStrLn "Call graph:\n"
699 when (not (null cg')) $ do iputStrLn "Call graph:\n"
699 iputStrLn (show cg')
700 iputStrLn (show cg')
700process h fn (Search t) = iPrintError "Not implemented"
701process h fn (Search t) = iPrintError "Not implemented"
701−-- FIXME: There is far too much repetition in the cases below!
702−process h fn (CaseSplitAt updatefile l n)
702+process h fn (CaseSplitAt updatefile l n)
703− = do src <- runIO $ readFile fn
703+ = caseSplitAt h fn updatefile l n
704− res <- splitOnLine l n fn
705− iLOG (showSep "\n" (map show res))
706− let (before, (ap : later)) = splitAt (l-1) (lines src)
707− res' <- replaceSplits ap res
708− let new = concat res'
709− if updatefile
710− then do let fb = fn ++ "~" -- make a backup!
711− runIO $ writeFile fb (unlines before ++ new ++ unlines later)
712− runIO $ copyFile fb fn
713− else -- do ihputStrLn h (show res)
714− ihPrintResult h new
715process h fn (AddClauseFrom updatefile l n)
704process h fn (AddClauseFrom updatefile l n)
716− = do src <- runIO $ readFile fn
717− let (before, tyline : later) = splitAt (l-1) (lines src)
718− let indent = getIndent 0 (show n) tyline
719− cl <- getClause l n fn
720− -- add clause before first blank line in 'later'
721− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
722− if updatefile
705+ = addClauseFrom h fn updatefile l n
723− then do let fb = fn ++ "~"
724− runIO $ writeFile fb (unlines (before ++ nonblank) ++
725− replicate indent ' ' ++
726− cl ++ "\n" ++
727− unlines rest)
728− runIO $ copyFile fb fn
729− else ihPrintResult h cl
730− where
731− getIndent i n [] = 0
732− getIndent i n xs | take (length n) xs == n = i
733− getIndent i n (x : xs) = getIndent (i + 1) n xs
734process h fn (AddProofClauseFrom updatefile l n)
706process h fn (AddProofClauseFrom updatefile l n)
735− = do src <- runIO $ readFile fn
736− let (before, tyline : later) = splitAt (l-1) (lines src)
737− let indent = getIndent 0 (show n) tyline
738− cl <- getProofClause l n fn
739− -- add clause before first blank line in 'later'
740− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
741− if updatefile
707+ = addProofClauseFrom h fn updatefile l n
742− then do let fb = fn ++ "~"
743− runIO $ writeFile fb (unlines (before ++ nonblank) ++
744− replicate indent ' ' ++
745− cl ++ "\n" ++
746− unlines rest)
747− runIO $ copyFile fb fn
748− else ihPrintResult h cl
749− where
750− getIndent i n [] = 0
751− getIndent i n xs | take (length n) xs == n = i
752− getIndent i n (x : xs) = getIndent (i + 1) n xs
753process h fn (AddMissing updatefile l n)
708process h fn (AddMissing updatefile l n)
754− = do src <- runIO $ readFile fn
709+ = addMissing h fn updatefile l n
755− let (before, tyline : later) = splitAt (l-1) (lines src)
756− let indent = getIndent 0 (show n) tyline
757− i <- getIState
758− cl <- getInternalApp fn l
759− let n' = getAppName cl
760−
761− extras <- case lookupCtxt n' (idris_patdefs i) of
762− [] -> return ""
763− [(_, tms)] -> do tms' <- nameMissing tms
764− showNew (show n ++ "_rhs") 1 indent tms'
765− let (nonblank, rest) = span (not . all isSpace) (tyline:later)
766− if updatefile
767− then do let fb = fn ++ "~"
768− runIO $ writeFile fb (unlines (before ++ nonblank)
769− ++ extras ++ unlines rest)
770− runIO $ copyFile fb fn
771− else ihPrintResult h extras
772− where showPat = show . stripNS
773− stripNS tm = mapPT dens tm where
774− dens (PRef fc n) = PRef fc (nsroot n)
775− dens t = t
776−
777− nsroot (NS n _) = nsroot n
778− nsroot (SN (WhereN _ _ n)) = nsroot n
779− nsroot n = n
780−
781− getAppName (PApp _ r _) = getAppName r
782− getAppName (PRef _ r) = r
783− getAppName _ = n
784−
785− showNew nm i ind (tm : tms)
786− = do (nm', i') <- getUniq nm i
787− rest <- showNew nm i' ind tms
788− return (replicate ind ' ' ++
789− showPat tm ++ " = ?" ++ nm' ++
790− "\n" ++ rest)
791− showNew nm i _ [] = return ""
792−
793− getIndent i n [] = 0
794− getIndent i n xs | take (length n) xs == n = i
795− getIndent i n (x : xs) = getIndent (i + 1) n xs
796−
797process h fn (MakeWith updatefile l n)
710process h fn (MakeWith updatefile l n)
798− = do src <- runIO $ readFile fn
711+ = makeWith h fn updatefile l n
799− let (before, tyline : later) = splitAt (l-1) (lines src)
800− let ind = getIndent tyline
801− let with = mkWith tyline n
802− -- add clause before first blank line in 'later',
803− -- or (TODO) before first line with same indentation as tyline
804− let (nonblank, rest) = span (\x -> not (all isSpace x) &&
805− not (ind == getIndent x)) later
806− if updatefile then
807− do let fb = fn ++ "~"
808− runIO $ writeFile fb (unlines (before ++ nonblank)
809− ++ with ++ "\n" ++
810− unlines rest)
811− runIO $ copyFile fb fn
812− else ihPrintResult h with
813− where getIndent s = length (takeWhile isSpace s)
814−
815process h fn (DoProofSearch updatefile rec l n hints)
712process h fn (DoProofSearch updatefile rec l n hints)
816− = do src <- runIO $ readFile fn
713+ = doProofSearch h fn updatefile rec l n hints
817− let (before, tyline : later) = splitAt (l-1) (lines src)
818− ctxt <- getContext
819− mn <- case lookupNames n ctxt of
820− [x] -> return x
821− [] -> return n
822− ns -> ierror (CantResolveAlts (map show ns))
823− i <- getIState
824− let (top, envlen, _) = case lookup mn (idris_metavars i) of
825− Just (t, e, False) -> (t, e, False)
826− _ -> (Nothing, 0, True)
827− let fc = fileFC fn
828− let body t = PProof [Try (TSeq Intros (ProofSearch rec t hints))
829− (ProofSearch rec t hints)]
830− let def = PClause fc mn (PRef fc mn) [] (body top) []
831− newmv <- idrisCatch
832− (do elabDecl' EAll toplevel (PClauses fc [] mn [def])
833− (tm, ty) <- elabVal toplevel False (PRef fc mn)
834− ctxt <- getContext
835− i <- getIState
836− return . flip displayS "" . renderPretty 1.0 80 $
837− pprintPTerm defaultPPOption [] [] (idris_infixes i)
838− (stripNS
839− (dropCtxt envlen
840− (delab i (specialise ctxt [] [(mn, 1)] tm)))))
841− (\e -> return ("?" ++ show n))
842− if updatefile then
843− do let fb = fn ++ "~"
844− runIO $ writeFile fb (unlines before ++
845− updateMeta False tyline (show n) newmv ++ "\n"
846− ++ unlines later)
847− runIO $ copyFile fb fn
848− else ihPrintResult h newmv
849− where dropCtxt 0 sc = sc
850− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
851− dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc
852− dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc
853− dropCtxt _ t = t
854−
855− stripNS tm = mapPT dens tm where
856− dens (PRef fc n) = PRef fc (nsroot n)
857− dens t = t
858−
859− nsroot (NS n _) = nsroot n
860− nsroot (SN (WhereN _ _ n)) = nsroot n
861− nsroot n = n
862−
863− updateMeta brack ('?':cs) n new
864− | length cs >= length n
865− = case splitAt (length n) cs of
866− (mv, c:cs) ->
867− if ((isSpace c || c == ')' || c == '}') && mv == n)
868− then addBracket brack new ++ (c : cs)
869− else '?' : mv ++ c : updateMeta True cs n new
870− (mv, []) -> if (mv == n) then addBracket brack new else '?' : mv
871− updateMeta brack ('=':cs) n new = '=':updateMeta False cs n new
872− updateMeta brack (c:cs) n new
873− = c : updateMeta (brack || not (isSpace c)) cs n new
874− updateMeta brack [] n new = ""
875−
876− addBracket False new = new
877− addBracket True new@('(':xs) | last xs == ')' = new
878− addBracket True new | any isSpace new = '(' : new ++ ")"
879− | otherwise = new
880−
881process h fn (Spec t)
714process h fn (Spec t)
882 = do (tm, ty) <- elabVal toplevel False t
715 = do (tm, ty) <- elabVal toplevel False t
883 ctxt <- getContext
716 ctxt <- getContext