659bc7c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #626 from david-christiansen/hannes-ide

659bc7cEdwin Brady13 years ago

src/Idris/IdeSlave.hs+25−7

compare with master

unifiedsplit

@@ -1,4 +1,4 @@

1−{-# LANGUAGE FlexibleInstances, IncoherentInstances #-}

1+{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

3module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable) where

@@ -73,7 +73,8 @@ pSExp = do xs <- between (char '(') (char ')') (pSExp `sepBy` (char ' '))

73 return (SexpList xs)

74 <|> atom

76+atom = do string "nil"; return (SexpList [])

76−atom = do char ':'; x <- atomC; return x

77+ <|> do char ':'; x <- atomC; return x

77 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

78 <|> do char '"'; xs <- many quotedChar; char '"'; return (StringAtom xs)

78 <|> do ints <- many1 digit

79 <|> do ints <- many1 digit

79 case readDec ints of

80 case readDec ints of

@@ -93,15 +94,32 @@ parseSExp = parse pSExp "(unknown)"

94data IdeSlaveCommand = REPLCompletions String

95data IdeSlaveCommand = REPLCompletions String

95 | Interpret String

96 | Interpret String

97+ | TypeOf String

98+ | CaseSplit Int String

99+ | AddClause Int String

100+ | AddProofClause Int String

101+ | AddMissing Int String

102+ | MakeWithBlock Int String

103+ | ProofSearch Int String [String]

96 | LoadFile String

104 | LoadFile String

97 deriving Show

105 deriving Show

106

99sexpToCommand :: SExp -> Maybe IdeSlaveCommand

107sexpToCommand :: SExp -> Maybe IdeSlaveCommand

100−sexpToCommand (SexpList (x:[])) = sexpToCommand x

108+sexpToCommand (SexpList (x:[])) = sexpToCommand x

101−sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

109+sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

102−sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

110+sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

103−sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

111+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename)

104−sexpToCommand _ = Nothing

112+sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

113+sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

114+sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

115+sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

116+sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

117+sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

118+sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom name, SexpList hintexp]) | Just hints <- getHints hintexp = Just (ProofSearch (fromInteger line) name hints)

119+ where getHints = mapM (\h -> case h of

120+ StringAtom s -> Just s

121+ _ -> Nothing)

122+sexpToCommand _ = Nothing

105

123

106parseMessage :: String -> Either Err (SExp, Integer)

124parseMessage :: String -> Either Err (SExp, Integer)

107parseMessage x = case receiveString x of

125parseMessage x = case receiveString x of

src/Idris/REPL.hs+71−56

@@ -17,7 +17,7 @@ import Idris.UnusedArgs

17import Idris.Docs

18import Idris.Help

19import Idris.Completion

20−import Idris.IdeSlave

20+import qualified Idris.IdeSlave as IdeSlave

21import Idris.Chaser

22import Idris.Imports

23import Idris.Colours

@@ -194,17 +194,17 @@ ideslave :: IState -> [FilePath] -> Idris ()

194ideslave orig mods

195 = do idrisCatch

196 (do l <- runIO $ getLine

197− (sexp, id) <- case parseMessage l of

197+ (sexp, id) <- case IdeSlave.parseMessage l of

198 Left err -> ierror err

199 Right (sexp, id) -> return (sexp, id)

200 i <- getIState

201 putIState $ i { idris_outputmode = (IdeSlave id) }

202+ let fn = case mods of

203+ (f:_) -> f

204+ _ -> ""

202− case sexpToCommand sexp of

205+ case IdeSlave.sexpToCommand sexp of

203− Just (Interpret cmd) ->

206+ Just (IdeSlave.Interpret cmd) ->

204− do let fn = case mods of

205− (f:_) -> f

206− _ -> ""

207− c <- colourise

207+ do c <- colourise

208 case parseCmd i "(input)" cmd of

209 Failure err -> iPrintError $ show (fixColour c err)

210 Success (Prove n') -> do iPrintResult ""

@@ -215,11 +215,11 @@ ideslave orig mods

215 Success cmd -> idrisCatch

216 (ideslaveProcess fn cmd)

217 (\e -> getIState >>= iPrintError . flip pshow e)

218− Just (REPLCompletions str) ->

218+ Just (IdeSlave.REPLCompletions str) ->

219 do (unused, compls) <- replCompletion (reverse str, "")

220− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

220+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

221− runIO $ putStrLn $ convSExp "return" good id

221+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id

222− Just (LoadFile filename) ->

222+ Just (IdeSlave.LoadFile filename) ->

223 do clearErr

224 putIState (orig { idris_options = idris_options i,

225 idris_outputmode = (IdeSlave id) })

@@ -233,6 +233,20 @@ ideslave orig mods

233 Nothing -> iPrintResult $ "loaded " ++ filename

234 Just x -> iPrintError $ "didn't load " ++ filename

235 ideslave orig [filename]

236+ Just (IdeSlave.TypeOf name) ->

237+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))

238+ Just (IdeSlave.CaseSplit line name) ->

239+ process stdout fn (CaseSplitAt False line (UN name))

240+ Just (IdeSlave.AddClause line name) ->

241+ process stdout fn (AddClauseFrom False line (UN name))

242+ Just (IdeSlave.AddProofClause line name) ->

243+ process stdout fn (AddProofClauseFrom False line (UN name))

244+ Just (IdeSlave.AddMissing line name) ->

245+ process stdout fn (AddMissing False line (UN name))

246+ Just (IdeSlave.MakeWithBlock line name) ->

247+ process stdout fn (MakeWith False line (UN name))

248+ Just (IdeSlave.ProofSearch line name hints) ->

249+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))

236 Nothing -> do iPrintError "did not understand")

250 Nothing -> do iPrintError "did not understand")

237 (\e -> do iPrintError $ show e)

251 (\e -> do iPrintError $ show e)

238 ideslave orig mods

252 ideslave orig mods

@@ -435,10 +449,10 @@ process h fn (Check (PRef _ n))

435 case lookupNames n ctxt of

449 case lookupNames n ctxt of

436 ts@(t:_) ->

450 ts@(t:_) ->

437 case lookup t (idris_metavars ist) of

451 case lookup t (idris_metavars ist) of

438− Just (_, i) -> showMetavarInfo c imp ist n i

452+ Just (_, i) -> ihPrintResult h (showMetavarInfo c imp ist n i)

453+ Nothing -> ihPrintResult h $

439− Nothing -> do mapM_ (\n -> ihputStrLn h $ showName (Just ist) [] False c n ++ " : " ++

454+ concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

440− showImp (Just ist) imp c (delabTy ist n)) ts

455+ showImp (Just ist) imp c (delabTy ist n)) $ ts

441− ihPrintResult h ""

442 [] -> ihPrintError h $ "No such variable " ++ show n

456 [] -> ihPrintError h $ "No such variable " ++ show n

443 where

457 where

444 showMetavarInfo c imp ist n i

458 showMetavarInfo c imp ist n i

@@ -446,18 +460,19 @@ process h fn (Check (PRef _ n))

446 (ty:_) -> putTy c imp ist i (delab ist ty)

460 (ty:_) -> putTy c imp ist i (delab ist ty)

447 putTy c imp ist 0 sc = putGoal c imp ist sc

461 putTy c imp ist 0 sc = putGoal c imp ist sc

448 putTy c imp ist i (PPi _ n t sc)

462 putTy c imp ist i (PPi _ n t sc)

449− = do ihputStrLn h $ " " ++

463+ = let current = " " ++

450− (case n of

464+ (case n of

451− MN _ _ -> "_"

465+ MN _ _ -> "_"

452− UN ('_':'_':_) -> "_"

466+ UN ('_':'_':_) -> "_"

453− _ -> showName (Just ist) [] False c n) ++

467+ _ -> showName (Just ist) [] False c n) ++

454− " : " ++ showImp (Just ist) imp c t

468+ " : " ++ showImp (Just ist) imp c t ++ "\n"

469+ in

455− putTy c imp ist (i-1) sc

470+ current ++ putTy c imp ist (i-1) sc

456 putTy c imp ist _ sc = putGoal c imp ist sc

471 putTy c imp ist _ sc = putGoal c imp ist sc

457 putGoal c imp ist g

472 putGoal c imp ist g

458− = do ihputStrLn h $ "--------------------------------------"

473+ = "--------------------------------------\n" ++

459− ihputStrLn h $ showName (Just ist) [] False c n ++ " : "

474+ showName (Just ist) [] False c n ++ " : " ++

460− ++ showImp (Just ist) imp c g

475+ showImp (Just ist) imp c g

461

476

462

477

463process h fn (Check t)

478process h fn (Check t)

@@ -470,7 +485,7 @@ process h fn (Check t)

470 case tm of

485 case tm of

471 TType _ -> ihPrintResult h ("Type : Type 1")

486 TType _ -> ihPrintResult h ("Type : Type 1")

472 _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

487 _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

473− showImp (Just ist) imp c (delab ist ty))

488+ showImp (Just ist) imp c (delab ist ty))

474

489

475process h fn (DocStr n)

490process h fn (DocStr n)

476 = do i <- getIState

491 = do i <- getIState

@@ -544,12 +559,12 @@ process h fn (CaseSplitAt updatefile l n)

544 let (before, (ap : later)) = splitAt (l-1) (lines src)

559 let (before, (ap : later)) = splitAt (l-1) (lines src)

545 res' <- replaceSplits ap res

560 res' <- replaceSplits ap res

546 let new = concat res'

561 let new = concat res'

547− if updatefile then

562+ if updatefile

548− do let fb = fn ++ "~" -- make a backup!

563+ then do let fb = fn ++ "~" -- make a backup!

549− runIO $ writeFile fb (unlines before ++ new ++ unlines later)

564+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)

550− runIO $ copyFile fb fn

565+ runIO $ copyFile fb fn

551− else -- do ihputStrLn h (show res)

566+ else -- do ihputStrLn h (show res)

552− ihputStrLn h new

567+ ihPrintResult h new

553process h fn (AddClauseFrom updatefile l n)

568process h fn (AddClauseFrom updatefile l n)

554 = do src <- runIO $ readFile fn

569 = do src <- runIO $ readFile fn

555 let (before, tyline : later) = splitAt (l-1) (lines src)

570 let (before, tyline : later) = splitAt (l-1) (lines src)

@@ -557,14 +572,14 @@ process h fn (AddClauseFrom updatefile l n)

557 cl <- getClause l n fn

572 cl <- getClause l n fn

558 -- add clause before first blank line in 'later'

573 -- add clause before first blank line in 'later'

559 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

574 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

560− if updatefile then

575+ if updatefile

561− do let fb = fn ++ "~"

576+ then do let fb = fn ++ "~"

562− runIO $ writeFile fb (unlines (before ++ nonblank)

577+ runIO $ writeFile fb (unlines (before ++ nonblank) ++

563− ++ replicate indent ' ' ++

578+ replicate indent ' ' ++

564 cl ++ "\n" ++

579 cl ++ "\n" ++

565− unlines rest)

580+ unlines rest)

566− runIO $ copyFile fb fn

581+ runIO $ copyFile fb fn

567− else ihputStrLn h cl

582+ else ihPrintResult h cl

568 where

583 where

569 getIndent i n [] = 0

584 getIndent i n [] = 0

570 getIndent i n xs | take (length n) xs == n = i

585 getIndent i n xs | take (length n) xs == n = i

@@ -576,14 +591,14 @@ process h fn (AddProofClauseFrom updatefile l n)

576 cl <- getProofClause l n fn

591 cl <- getProofClause l n fn

577 -- add clause before first blank line in 'later'

592 -- add clause before first blank line in 'later'

578 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

593 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

579− if updatefile then

594+ if updatefile

580− do let fb = fn ++ "~"

595+ then do let fb = fn ++ "~"

581− runIO $ writeFile fb (unlines (before ++ nonblank)

596+ runIO $ writeFile fb (unlines (before ++ nonblank) ++

582− ++ replicate indent ' ' ++

597+ replicate indent ' ' ++

583 cl ++ "\n" ++

598 cl ++ "\n" ++

584− unlines rest)

599+ unlines rest)

585− runIO $ copyFile fb fn

600+ runIO $ copyFile fb fn

586− else ihputStrLn h cl

601+ else ihPrintResult h cl

587 where

602 where

588 getIndent i n [] = 0

603 getIndent i n [] = 0

589 getIndent i n xs | take (length n) xs == n = i

604 getIndent i n xs | take (length n) xs == n = i

@@ -600,12 +615,12 @@ process h fn (AddMissing updatefile l n)

600 [] -> return ""

615 [] -> return ""

601 [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms

616 [(_, tms)] -> showNew (show n ++ "_rhs") 1 indent tms

602 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

617 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

603− if updatefile then

618+ if updatefile

604− do let fb = fn ++ "~"

619+ then do let fb = fn ++ "~"

605− runIO $ writeFile fb (unlines (before ++ nonblank) ++

620+ runIO $ writeFile fb (unlines (before ++ nonblank)

606− extras ++ unlines rest)

621+ ++ extras ++ unlines rest)

607− runIO $ copyFile fb fn

622+ runIO $ copyFile fb fn

608− else ihputStrLn h extras

623+ else ihPrintResult h extras

609 where showPat = show . stripNS

624 where showPat = show . stripNS

610 stripNS tm = mapPT dens tm where

625 stripNS tm = mapPT dens tm where

611 dens (PRef fc n) = PRef fc (nsroot n)

626 dens (PRef fc n) = PRef fc (nsroot n)

@@ -626,7 +641,7 @@ process h fn (AddMissing updatefile l n)

626 showPat tm ++ " = ?" ++ nm' ++

641 showPat tm ++ " = ?" ++ nm' ++

627 "\n" ++ rest)

642 "\n" ++ rest)

628 showNew nm i _ [] = return ""

643 showNew nm i _ [] = return ""

629−

644+

630 getIndent i n [] = 0

645 getIndent i n [] = 0

631 getIndent i n xs | take (length n) xs == n = i

646 getIndent i n xs | take (length n) xs == n = i

632 getIndent i n (x : xs) = getIndent (i + 1) n xs

647 getIndent i n (x : xs) = getIndent (i + 1) n xs

@@ -643,7 +658,7 @@ process h fn (MakeWith updatefile l n)

643 ++ with ++ "\n" ++

658 ++ with ++ "\n" ++

644 unlines rest)

659 unlines rest)

645 runIO $ copyFile fb fn

660 runIO $ copyFile fb fn

646− else ihputStrLn h with

661+ else ihPrintResult h with

647process h fn (DoProofSearch updatefile l n hints)

662process h fn (DoProofSearch updatefile l n hints)

648 = do src <- runIO $ readFile fn

663 = do src <- runIO $ readFile fn

649 let (before, tyline : later) = splitAt (l-1) (lines src)

664 let (before, tyline : later) = splitAt (l-1) (lines src)

@@ -675,7 +690,7 @@ process h fn (DoProofSearch updatefile l n hints)

675 updateMeta tyline (show n) newmv ++ "\n"

690 updateMeta tyline (show n) newmv ++ "\n"

676 ++ unlines later)

691 ++ unlines later)

677 runIO $ copyFile fb fn

692 runIO $ copyFile fb fn

678− else ihputStrLn h newmv

693+ else ihPrintResult h newmv

679 where dropCtxt 0 sc = sc

694 where dropCtxt 0 sc = sc

680 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

695 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

681 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

696 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc