@@ -30,6 +30,7 @@ import Idris.Inliner
3030import Idris.CaseSplit
3131import Idris.DeepSeq
3232import Idris.Output
33+import Idris.Interactive
3334import Idris.WhoCalls
3435
3536import Paths_idris
@@ -698,186 +699,18 @@ process h fn (DebugInfo n)
698699 when (not (null cg')) $ do iputStrLn "Call graph:\n"
699700 iputStrLn (show cg')
700701process 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)
703− = do src <- runIO $ readFile fn
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
702+process h fn (CaseSplitAt updatefile l n)
703+ = caseSplitAt h fn updatefile l n
715704process 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
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
705+ = addClauseFrom h fn updatefile l n
734706process 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
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
707+ = addProofClauseFrom h fn updatefile l n
753708process h fn (AddMissing updatefile l n)
754− = do src <- runIO $ readFile fn
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−
709+ = addMissing h fn updatefile l n
797710process h fn (MakeWith updatefile l n)
798− = do src <- runIO $ readFile fn
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−
711+ = makeWith h fn updatefile l n
815712process h fn (DoProofSearch updatefile rec l n hints)
816− = do src <- runIO $ readFile fn
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−
713+ = doProofSearch h fn updatefile rec l n hints
881714process h fn (Spec t)
882715 = do (tm, ty) <- elabVal toplevel False t
883716 ctxt <- getContext