diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 70f4b3956..1349304fe 100644 --- a/libs/contrib/System/Path.idr +++ b/libs/contrib/System/Path.idr @@ -349,7 +349,7 @@ unc = do count (exactly 2) $ match $ PTPunct '\\' server <- match PTText bodySeparator share <- match PTText - Core.pure $ UNC server share + Core.pure $ UNC server share>>>>>>> master -- Example: \\?\server\share private diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index e8fef9066..5676079c8 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -15,6 +15,9 @@ data SExp = SExpList (List SExp) | IntegerAtom Integer | SymbolAtom String +public export +data DocMode = Overview | Full + public export data IDECommand = Interpret String @@ -22,12 +25,25 @@ data IDECommand | TypeOf String (Maybe (Integer, Integer)) | CaseSplit Integer Integer String | AddClause Integer String + -- deprecated: | AddProofClause + | AddMissing Integer String | ExprSearch Integer String (List String) Bool | GenerateDef Integer String | MakeLemma Integer String | MakeCase Integer String | MakeWith Integer String + | DocsFor String (Maybe DocMode) + | Apropos String | Metavariables Integer + | WhoCalls String + | CallsWho String + | BrowseNamespace String + | NormaliseTerm String -- TODO: implement a Binary lib + | ShowTermImplicits String -- and implement Binary (Term) + | HideTermImplicits String -- for these four defintions, + | ElaborateTerm String -- then change String to Term, as in idris1 + | PrintDefinition String + | ReplCompletions String | Version | GetOptions @@ -58,6 +74,8 @@ getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n]) = Just $ CaseSplit l 0 n getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n]) = Just $ AddClause l n +getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n]) + = Just $ AddMissing line n getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n]) = Just $ ExprSearch l n [] False getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, SExpList hs]) @@ -79,8 +97,36 @@ getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n]) = Just $ MakeCase l n getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n]) = Just $ MakeWith l n +getIDECommand (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail)) + = do -- Maybe monad + modeOpt <- case modeTail of + [] => Just Nothing + [SymbolAtom "overview"] => Just $ Just Overview + [SymbolAtom "full" ] => Just $ Just Full + _ => Nothing + Just $ DocsFor n modeOpt +getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n]) + = Just $ Apropos n getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n]) = Just $ Metavariables n +getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n]) + = Just $ WhoCalls n +getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n]) + = Just $ CallsWho n +getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns]) + = Just $ BrowseNamespace ns +getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm]) + = Just $ NormaliseTerm tm +getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm]) + = Just $ ShowTermImplicits tm +getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm]) + = Just $ HideTermImplicits tm +getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm]) + = Just $ ElaborateTerm tm +getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n]) + = Just $ PrintDefinition n +getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n]) + = Just $ ReplCompletions n getIDECommand (SymbolAtom "version") = Just Version getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions getIDECommand _ = Nothing @@ -94,6 +140,7 @@ putIDECommand (TypeOf cmd Nothing) = (SExpList [SymbolAtom "type-of", putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col]) putIDECommand (CaseSplit line col n) = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n]) putIDECommand (AddClause line n) = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n]) +putIDECommand (AddMissing line n) = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n]) putIDECommand (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode]) where getMode : Bool -> SExp @@ -103,7 +150,22 @@ putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate- putIDECommand (MakeLemma line n) = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n]) putIDECommand (MakeCase line n) = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n]) putIDECommand (MakeWith line n) = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n]) +putIDECommand (DocsFor n modeOpt) = let modeTail = case modeOpt of + Nothing => [] + Just Overview => [SymbolAtom "overview"] + Just Full => [SymbolAtom "full"] in + (SExpList (SymbolAtom "docs-for" :: StringAtom n :: modeTail)) +putIDECommand (Apropos n) = (SExpList [SymbolAtom "apropos", StringAtom n]) putIDECommand (Metavariables n) = (SExpList [SymbolAtom "metavariables", IntegerAtom n]) +putIDECommand (WhoCalls n) = (SExpList [SymbolAtom "who-calls", StringAtom n]) +putIDECommand (CallsWho n) = (SExpList [SymbolAtom "calls-who", StringAtom n]) +putIDECommand (BrowseNamespace ns) = (SExpList [SymbolAtom "browse-namespace", StringAtom ns]) +putIDECommand (NormaliseTerm tm) = (SExpList [SymbolAtom "normalise-term", StringAtom tm]) +putIDECommand (ShowTermImplicits tm) = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm]) +putIDECommand (HideTermImplicits tm) = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm]) +putIDECommand (ElaborateTerm tm) = (SExpList [SymbolAtom "elaborate-term", StringAtom tm]) +putIDECommand (PrintDefinition n) = (SExpList [SymbolAtom "print-definition", StringAtom n]) +putIDECommand (ReplCompletions n) = (SExpList [SymbolAtom "repl-completions", StringAtom n]) putIDECommand GetOptions = (SExpList [SymbolAtom "get-options"]) putIDECommand Version = SymbolAtom "version" diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index c7567f70d..84924527f 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -119,49 +119,99 @@ getInput f do inp <- getNChars f (integerToNat (cast num)) pure (pack inp) +||| Do nothing and tell the user to wait for us to implmement this (or join the effort!) +todoCmd : {auto o : Ref ROpts REPLOpts} -> + String -> Core () +todoCmd cmdName = iputStrLn $ cmdName ++ ": command not yet implemented. Hopefully soon!" + +data IDEResult + = REPL REPLResult + | NameList (List Name) + | Term String -- should be a PTerm + metadata, or SExp. + | TTTerm String -- should be a TT Term + metadata, or perhaps SExp + +replWrap : Core REPLResult -> Core IDEResult +replWrap m = pure $ REPL !m + process : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - IDECommand -> Core REPLResult + IDECommand -> Core IDEResult process (Interpret cmd) - = interpret cmd + = replWrap $ interpret cmd process (LoadFile fname _) - = Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname + = replWrap $ Idris.REPL.process (Load fname) >>= outputSyntaxHighlighting fname process (TypeOf n Nothing) - = Idris.REPL.process (Check (PRef replFC (UN n))) + = replWrap $ Idris.REPL.process (Check (PRef replFC (UN n))) process (TypeOf n (Just (l, c))) - = Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n))) + = replWrap $ Idris.REPL.process (Editing (TypeAt (fromInteger l) (fromInteger c) (UN n))) process (CaseSplit l c n) - = Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n))) + = replWrap $ Idris.REPL.process (Editing (CaseSplit False (fromInteger l) (fromInteger c) (UN n))) process (AddClause l n) - = Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (AddClause False (fromInteger l) (UN n))) +process (AddMissing l n) + = do todoCmd "add-missing" + pure $ REPL $ Edited $ DisplayEdit [] process (ExprSearch l n hs all) - = Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) + = replWrap $ Idris.REPL.process (Editing (ExprSearch False (fromInteger l) (UN n) (map UN hs) all)) process (GenerateDef l n) - = Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (GenerateDef False (fromInteger l) (UN n))) process (MakeLemma l n) - = Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeLemma False (fromInteger l) (UN n))) process (MakeCase l n) - = Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeCase False (fromInteger l) (UN n))) process (MakeWith l n) - = Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n))) + = replWrap $ Idris.REPL.process (Editing (MakeWith False (fromInteger l) (UN n))) +process (DocsFor n modeOpt) + = do todoCmd "docs-for" + pure $ REPL $ Printed [] +process (Apropos n) + = do todoCmd "apropros" + pure $ REPL $ Printed [] +process (WhoCalls n) + = do todoCmd "who-calls" + pure $ NameList [] +process (CallsWho n) + = do todoCmd "calls-who" + pure $ NameList [] +process (BrowseNamespace ns) + = do todoCmd "browse-namespace" + pure $ NameList [] +process (NormaliseTerm tm) + = do todoCmd "normalise-term" + pure $ Term tm +process (ShowTermImplicits tm) + = do todoCmd "show-term-implicits" + pure $ Term tm +process (HideTermImplicits tm) + = do todoCmd "hide-term-implicits" + pure $ Term tm +process (ElaborateTerm tm) + = do todoCmd "elaborate-term" + pure $ TTTerm tm +process (PrintDefinition n) + = do todoCmd "print-definition" + pure $ REPL $ Printed [n] +process (ReplCompletions n) + = do todoCmd "repl-completions" + pure $ NameList [] process Version - = Idris.REPL.process ShowVersion + = replWrap $ Idris.REPL.process ShowVersion process (Metavariables _) - = Idris.REPL.process Metavars + = replWrap $ Idris.REPL.process Metavars process GetOptions - = Idris.REPL.process GetOpts + = replWrap $ Idris.REPL.process GetOpts processCatch : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - IDECommand -> Core REPLResult + IDECommand -> Core IDEResult processCatch cmd = do c' <- branch u' <- get UST @@ -175,7 +225,7 @@ processCatch cmd put Syn s' put ROpts o' msg <- perror err - pure $ REPLError msg) + pure $ REPL $ REPLError msg) idePutStrLn : File -> Integer -> String -> Core () idePutStrLn outf i msg @@ -212,41 +262,79 @@ SExpable REPLOpt where sexpName : Name -> SExp -sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [] ] +sexpName n = SExpList [ StringAtom (show n), SExpList [], SExpList [StringAtom "?", SExpList[]]] displayIDEResult : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - File -> Integer -> REPLResult -> Core () -displayIDEResult outf i (REPLError err) = printIDEError outf i err -displayIDEResult outf i (Evaluated x Nothing) = printIDEResultWithHighlight outf i $ StringAtom $ show x -displayIDEResult outf i (Evaluated x (Just y)) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y -displayIDEResult outf i (Printed xs) = printIDEResultWithHighlight outf i $ StringAtom $ showSep "\n" xs -displayIDEResult outf i (TermChecked x y) = printIDEResultWithHighlight outf i $ StringAtom $ show x ++ " : " ++ show y -displayIDEResult outf i (FileLoaded x) = printIDEResult outf i $ SExpList [] -displayIDEResult outf i (ErrorLoadingFile x err) = printIDEError outf i $ "Error loading file " ++ x ++ ": " ++ show err -displayIDEResult outf i (ErrorsBuildingFile x errs) = printIDEError outf i $ "Error(s) building file " ++ x ++ ": " ++ (showSep "\n" $ map show errs) -displayIDEResult outf i NoFileLoaded = printIDEError outf i "No file can be reloaded" -displayIDEResult outf i (CurrentDirectory dir) = printIDEResult outf i $ StringAtom $ "Current working directory is '" ++ dir ++ "'" -displayIDEResult outf i CompilationFailed = printIDEError outf i "Compilation failed" -displayIDEResult outf i (Compiled f) = printIDEResult outf i $ StringAtom $ "File " ++ f ++ " written" -displayIDEResult outf i (ProofFound x) = printIDEResult outf i $ StringAtom $ show x ---displayIDEResult outf i (Missed cases) = printIDEResult outf i $ showSep "\n" $ map handleMissing cases -displayIDEResult outf i (CheckedTotal xs) = printIDEResult outf i $ StringAtom $ showSep "\n" $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs -displayIDEResult outf i (FoundHoles []) = printIDEResult outf i $ SExpList [] -displayIDEResult outf i (FoundHoles xs) = printIDEResult outf i $ holesSexp + File -> Integer -> IDEResult -> Core () +displayIDEResult outf i (REPL $ REPLError err) + = printIDEError outf i err +displayIDEResult outf i (REPL RequestedHelp ) + = printIDEResult outf i + $ StringAtom $ displayHelp +displayIDEResult outf i (REPL $ Evaluated x Nothing) + = printIDEResultWithHighlight outf i + $ StringAtom $ show x +displayIDEResult outf i (REPL $ Evaluated x (Just y)) + = printIDEResultWithHighlight outf i + $ StringAtom $ show x ++ " : " ++ show y +displayIDEResult outf i (REPL $ Printed xs) + = printIDEResultWithHighlight outf i + $ StringAtom $ showSep "\n" xs +displayIDEResult outf i (REPL $ TermChecked x y) + = printIDEResultWithHighlight outf i + $ StringAtom $ show x ++ " : " ++ show y +displayIDEResult outf i (REPL $ FileLoaded x) + = printIDEResult outf i $ SExpList [] +displayIDEResult outf i (REPL $ ErrorLoadingFile x err) + = printIDEError outf i + $ "Error loading file " ++ x ++ ": " ++ show err +displayIDEResult outf i (REPL $ ErrorsBuildingFile x errs) + = printIDEError outf i + $ "Error(s) building file " ++ x ++ ": " ++ + (showSep "\n" $ map show errs) +displayIDEResult outf i (REPL $ NoFileLoaded) + = printIDEError outf i "No file can be reloaded" +displayIDEResult outf i (REPL $ CurrentDirectory dir) + = printIDEResult outf i + $ StringAtom $ "Current working directory is '" ++ dir ++ "'" +displayIDEResult outf i (REPL CompilationFailed) + = printIDEError outf i "Compilation failed" +displayIDEResult outf i (REPL $ Compiled f) + = printIDEResult outf i $ StringAtom + $ "File " ++ f ++ " written" +displayIDEResult outf i (REPL $ ProofFound x) + = printIDEResult outf i + $ StringAtom $ show x +displayIDEResult outf i (REPL $ Missed cases) + = printIDEResult outf i + $ StringAtom $ showSep "\n" + $ map handleMissing cases +displayIDEResult outf i (REPL $ CheckedTotal xs) + = printIDEResult outf i + $ StringAtom $ showSep "\n" + $ map (\ (fn, tot) => (show fn ++ " is " ++ show tot)) xs +displayIDEResult outf i (REPL $ FoundHoles []) + = printIDEResult outf i $ SExpList [] +displayIDEResult outf i (REPL $ FoundHoles xs) + = printIDEResult outf i $ holesSexp where holesSexp : SExp holesSexp = SExpList $ map sexpName xs -displayIDEResult outf i (LogLevelSet k) = printIDEResult outf i $ StringAtom $ "Set loglevel to " ++ show k -displayIDEResult outf i (OptionsSet opts) = printIDEResult outf i optionsSexp +displayIDEResult outf i (REPL $ LogLevelSet k) + = printIDEResult outf i + $ StringAtom $ "Set loglevel to " ++ show k +displayIDEResult outf i (REPL $ OptionsSet opts) + = printIDEResult outf i optionsSexp where optionsSexp : SExp optionsSexp = SExpList $ map toSExp opts -displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp +displayIDEResult outf i (REPL $ VersionIs x) + = printIDEResult outf i versionSExp where semverSexp : SExp semverSexp = case (semVer x) of @@ -258,11 +346,19 @@ displayIDEResult outf i (VersionIs x) = printIDEResult outf i versionSExp versionSExp : SExp versionSExp = SExpList [ semverSexp, tagSexp ] - -displayIDEResult outf i (Edited (DisplayEdit xs)) = printIDEResult outf i $ StringAtom $ showSep "\n" xs -displayIDEResult outf i (Edited (EditError x)) = printIDEError outf i x -displayIDEResult outf i (Edited (MadeLemma lit name pty pappstr)) = - printIDEResult outf i $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr +displayIDEResult outf i (REPL $ Edited (DisplayEdit xs)) + = printIDEResult outf i $ StringAtom $ showSep "\n" xs +displayIDEResult outf i (REPL $ Edited (EditError x)) + = printIDEError outf i x +displayIDEResult outf i (REPL $ Edited (MadeLemma lit name pty pappstr)) + = printIDEResult outf i + $ StringAtom $ (relit lit $ show name ++ " : " ++ show pty ++ "\n") ++ pappstr +displayIDEResult outf i (NameList ns) + = printIDEResult outf i $ SExpList $ map toSExp ns +displayIDEResult outf i (Term t) + = printIDEResult outf i $ StringAtom t +displayIDEResult outf i (TTTerm t) + = printIDEResult outf i $ StringAtom t displayIDEResult outf i _ = pure () @@ -271,8 +367,8 @@ handleIDEResult : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> - File -> Integer -> REPLResult -> Core () -handleIDEResult outf i Exited = idePutStrLn outf i "Bye for now!" + File -> Integer -> IDEResult -> Core () +handleIDEResult outf i (REPL Exited) = idePutStrLn outf i "Bye for now!" handleIDEResult outf i other = displayIDEResult outf i other loop : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/IDEMode/SyntaxHighlight.idr b/src/Idris/IDEMode/SyntaxHighlight.idr index dc04a3a84..2c29585a7 100644 --- a/src/Idris/IDEMode/SyntaxHighlight.idr +++ b/src/Idris/IDEMode/SyntaxHighlight.idr @@ -58,6 +58,7 @@ SExpable Highlight where inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool inFile fname (MkFC file _ _, _) = file == fname +inFile _ (EmptyFC, _) = False ||| Output some data using current dialog index export diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index d7a0b005b..dafbad211 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -177,16 +177,15 @@ stMain opts setOutput (IDEMode 0 stdin stdout) replIDE {c} {u} {m} else do - throw (InternalError "Not implemeted yet") --- let (host, port) = ideSocketModeHostPort opts --- f <- coreLift $ initIDESocketFile host port --- case f of --- Left err => do --- coreLift $ putStrLn err --- coreLift $ exit 1 --- Right file => do --- setOutput (IDEMode 0 file file) --- replIDE {c} {u} {m} + let (host, port) = ideSocketModeHostPort opts + f <- coreLift $ initIDESocketFile host port + case f of + Left err => do + coreLift $ putStrLn err + coreLift $ exitWith (ExitFailure 1) + Right file => do + setOutput (IDEMode 0 file file) + replIDE {c} {u} {m} else do repl {c} {u} {m} showTimeRecord diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index b04ca9970..745533417 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -820,6 +820,7 @@ mutual prompt NormaliseAll = "" prompt Execute = "[exec] " + export handleMissing : MissedResult -> String handleMissing (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs handleMissing (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function" @@ -872,6 +873,7 @@ mutual displayResult (OptionsSet opts) = printResult $ showSep "\n" $ map show opts displayResult _ = pure () + export displayHelp : String displayHelp = showSep "\n" $ map cmdInfo help