6412ae4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Implement type-of ideslave command, which uses Check in the background

6412ae4Hannes Mehnert13 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

@@ -93,6 +93,7 @@ parseSExp = parse pSExp "(unknown)"

94data IdeSlaveCommand = REPLCompletions String

95 | Interpret String

96+ | TypeOf String

96 | LoadFile String

97 | LoadFile String

97 deriving Show

98 deriving Show

@@ -101,6 +102,7 @@ sexpToCommand (SexpList (x:[])) = se

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

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

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

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

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

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

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

104sexpToCommand _ = Nothing

106sexpToCommand _ = Nothing

105

107

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

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

src/Idris/REPL.hs+18−15

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

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

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

235 ideslave orig [filename]

236+ Just (TypeOf name) ->

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

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

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

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

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

238 ideslave orig mods

240 ideslave orig mods

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

435 case lookupNames n ctxt of

437 case lookupNames n ctxt of

436 ts@(t:_) ->

438 ts@(t:_) ->

437 case lookup t (idris_metavars ist) of

439 case lookup t (idris_metavars ist) of

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

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

441+ Nothing -> ihPrintResult h $

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

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

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

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

441− ihPrintResult h ""

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

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

443 where

445 where

444 showMetavarInfo c imp ist n i

446 showMetavarInfo c imp ist n i

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

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

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

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

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

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

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

449− = do ihputStrLn h $ " " ++

451+ = let current = " " ++

450− (case n of

452+ (case n of

451− MN _ _ -> "_"

453+ MN _ _ -> "_"

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

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

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

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

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

456+ " : " ++ showImp (Just ist) imp c t

457+ in

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

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

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

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

457 putGoal c imp ist g

460 putGoal c imp ist g

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

461+ = "--------------------------------------\n" ++

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

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

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

463+ showImp (Just ist) imp c g

461

464

462

465

463process h fn (Check t)

466process h fn (Check t)

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

470 case tm of

473 case tm of

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

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

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

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

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

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

474

477

475process h fn (DocStr n)

478process h fn (DocStr n)

476 = do i <- getIState

479 = do i <- getIState