f6edbf0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

support for add-missing, make-with-block and proofsearch for ideslave

f6edbf0Hannes Mehnert13 years ago

src/Idris/IdeSlave.hs+20−10

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

@@ -96,18 +97,27 @@ data IdeSlaveCommand = REPLCompletions String

96 | TypeOf String

97 | TypeOf String

97 | CaseSplit Int String

98 | CaseSplit Int String

98 | AddClause Int String

99 | AddClause Int String

100+ | AddMissing Int String

101+ | MakeWithBlock Int String

102+ | ProofSearch Int String [String]

99 | LoadFile String

103 | LoadFile String

100 deriving Show

104 deriving Show

101

105

102sexpToCommand :: SExp -> Maybe IdeSlaveCommand

106sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

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

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

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

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

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

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

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

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

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

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

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

110−sexpToCommand _ = Nothing

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

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

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

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

118+ StringAtom s -> Just s

119+ _ -> Nothing)

120+sexpToCommand _ = Nothing

111

121

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

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

113parseMessage x = case receiveString x of

123parseMessage x = case receiveString x of

src/Idris/REPL.hs+29−23

@@ -239,6 +239,12 @@ ideslave orig mods

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.AddMissing line name) ->

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

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

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

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

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

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

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

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

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

244 ideslave orig mods

250 ideslave orig mods

@@ -567,14 +573,14 @@ process h fn (AddClauseFrom updatefile l n)

567 cl <- getClause l n fn

573 cl <- getClause l n fn

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

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

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

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

570− if updatefile then

576+ if updatefile

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

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

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

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

573− ++ replicate indent ' ' ++

579+ replicate indent ' ' ++

574 cl ++ "\n" ++

580 cl ++ "\n" ++

575− unlines rest)

581+ unlines rest)

576− runIO $ copyFile fb fn

582+ runIO $ copyFile fb fn

577− else ihPrintResult h cl

583+ else ihPrintResult h cl

578 where

584 where

579 getIndent i n [] = 0

585 getIndent i n [] = 0

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

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

@@ -586,14 +592,14 @@ process h fn (AddProofClauseFrom updatefile l n)

586 cl <- getProofClause l n fn

592 cl <- getProofClause l n fn

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

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

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

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

589− if updatefile then

595+ if updatefile

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

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

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

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

592− ++ replicate indent ' ' ++

598+ replicate indent ' ' ++

593 cl ++ "\n" ++

599 cl ++ "\n" ++

594− unlines rest)

600+ unlines rest)

595− runIO $ copyFile fb fn

601+ runIO $ copyFile fb fn

596− else ihputStrLn h cl

602+ else ihPrintResult h cl

597 where

603 where

598 getIndent i n [] = 0

604 getIndent i n [] = 0

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

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

@@ -610,12 +616,12 @@ process h fn (AddMissing updatefile l n)

610 [] -> return ""

616 [] -> return ""

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

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

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

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

613− if updatefile then

619+ if updatefile

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

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

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

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

616− extras ++ unlines rest)

622+ ++ extras ++ unlines rest)

617− runIO $ copyFile fb fn

623+ runIO $ copyFile fb fn

618− else ihputStrLn h extras

624+ else ihPrintResult h extras

619 where showPat = show . stripNS

625 where showPat = show . stripNS

620 stripNS tm = mapPT dens tm where

626 stripNS tm = mapPT dens tm where

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

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

@@ -636,7 +642,7 @@ process h fn (AddMissing updatefile l n)

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

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

637 "\n" ++ rest)

643 "\n" ++ rest)

638 showNew nm i _ [] = return ""

644 showNew nm i _ [] = return ""

639−

645+

640 getIndent i n [] = 0

646 getIndent i n [] = 0

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

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

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

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

@@ -653,7 +659,7 @@ process h fn (MakeWith updatefile l n)

653 ++ with ++ "\n" ++

659 ++ with ++ "\n" ++

654 unlines rest)

660 unlines rest)

655 runIO $ copyFile fb fn

661 runIO $ copyFile fb fn

656− else ihputStrLn h with

662+ else ihPrintResult h with

657process h fn (DoProofSearch updatefile l n hints)

663process h fn (DoProofSearch updatefile l n hints)

658 = do src <- runIO $ readFile fn

664 = do src <- runIO $ readFile fn

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

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

@@ -685,7 +691,7 @@ process h fn (DoProofSearch updatefile l n hints)

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

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

686 ++ unlines later)

692 ++ unlines later)

687 runIO $ copyFile fb fn

693 runIO $ copyFile fb fn

688− else ihputStrLn h newmv

694+ else ihPrintResult h newmv

689 where dropCtxt 0 sc = sc

695 where dropCtxt 0 sc = sc

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

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

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

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