From 3520f7d6fe08be46c465ce1d86f132981503a4dc Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 16 Jul 2019 16:34:57 +0200 Subject: [PATCH 01/20] allow running IDE mode on different network interfaces --- Notes/IDE-mode.md | 1 - src/Idris/CommandLine.idr | 25 +++++++++++++++++---- src/Idris/IDEMode/Main.idr | 18 +++++++-------- src/Idris/IDEMode/REPL.idr | 45 +++++++++++++++++++------------------- src/Idris/Main.idr | 19 ++++++++-------- src/Idris/SetOptions.idr | 11 +++++----- 6 files changed, 67 insertions(+), 52 deletions(-) diff --git a/Notes/IDE-mode.md b/Notes/IDE-mode.md index 056ad5b..02a2947 100644 --- a/Notes/IDE-mode.md +++ b/Notes/IDE-mode.md @@ -40,4 +40,3 @@ Generates a pattern matching definition, if it can find one, for the function declared with the given name, on the given line. It will only return the first definition it finds, as a list of pattern clauses. This works via a combination of case splitting and expression search. - diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index 168bc4a..43c3184 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -1,5 +1,7 @@ module Idris.CommandLine +import Data.String + %default total public export @@ -44,7 +46,7 @@ data CLOpt ||| Whether or not to run in IdeMode (easily parsable for other tools) IdeMode | ||| Whether or not to run IdeMode (using a socket instead of stdin/stdout) - IdeModeSocket | + IdeModeSocket String | ||| Run as a checker for the core language TTImp Yaffle String | Timing | @@ -76,9 +78,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--ide-mode"] [] [IdeMode] (Just "Run the REPL with machine-readable syntax"), - - MkOpt ["--ide-mode-socket"] [] [IdeModeSocket] - (Just "Run the ide socket mode"), + + MkOpt ["--ide-mode-socket"] ["host:port"] (\hp => [IdeModeSocket hp]) + (Just "Run the ide socket mode on given host and port (default: localhost:38398"), MkOpt ["--prefix"] [] [ShowPrefix] (Just "Show installation prefix"), @@ -175,3 +177,18 @@ getCmdOpts = do (_ :: opts) <- getArgs | pure (Left "Invalid command line") pure $ getOpts opts +portPart : String -> Maybe String +portPart p with (not $ p == "") proof prf + portPart p | False = Nothing + portPart p | True = Just $ strTail' p (sym prf) + +||| Extract the host and port to bind the IDE socket to +public export +ideSocketModeHostPort : List CLOpt -> (String, Int) +ideSocketModeHostPort [] = ("localhost", 38398) +ideSocketModeHostPort (IdeModeSocket hp :: _) = + let (h, p) = Strings.break (== ':') hp + port = fromMaybe 38398 (portPart p >>= parsePositive) + host = if h == "" then "localhost" else h + in (host, port) +ideSocketModeHostPort (_ :: rest) = ideSocketModeHostPort rest diff --git a/src/Idris/IDEMode/Main.idr b/src/Idris/IDEMode/Main.idr index d967cc5..4bedee6 100644 --- a/src/Idris/IDEMode/Main.idr +++ b/src/Idris/IDEMode/Main.idr @@ -114,24 +114,25 @@ stMain opts Just f => loadMainFile f doRepl <- postOptions opts - if doRepl - then + if doRepl + then if ide || ideSocket - then - if not ideSocket + then + if not ideSocket then do setOutput (IDEMode 0 stdin stdout) replIDE {c} {u} {m} - else do - f <- coreLift $ initIDESocketFile 38398 + else do + 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} - else do + replIDE {c} {u} {m} + else do iputStrLn "Welcome to Blodwen. Good luck." repl {c} {u} {m} else @@ -178,4 +179,3 @@ locMain opts = coreRun (stMain opts) do putStrLn ("Uncaught error: " ++ show err) exit 1) (\res => pure ()) - diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 44983e5..54868a6 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -43,10 +43,10 @@ socketToFile (MkSocket f _ _ _) = do if !(ferror file) then do pure (Left "Failed to fdopen socket file descriptor") else pure (Right file) - + export -initIDESocketFile : Int -> IO (Either String File) -initIDESocketFile p = do +initIDESocketFile : String -> Int -> IO (Either String File) +initIDESocketFile h p = do osock <- socket AF_INET Stream 0 case osock of Left fail => do @@ -55,9 +55,9 @@ initIDESocketFile p = do exit 1 Right sock => do putStrLn (show p) - res <- bind sock (Just (Hostname "localhost")) p - if res /= 0 - then + res <- bind sock (Just (Hostname h)) p + if res /= 0 + then pure (Left ("Failed to bind socket with error: " ++ show res)) else do res <- listen sock @@ -66,11 +66,11 @@ initIDESocketFile p = do pure (Left ("Failed to listen on socket with error: " ++ show res)) else do res <- accept sock - case res of - Left err => + case res of + Left err => pure (Left ("Failed to accept on socket with error: " ++ show err)) - Right (s, _) => - socketToFile s + Right (s, _) => + socketToFile s getChar : File -> IO Char getChar (FHandle h) = do @@ -83,7 +83,7 @@ getChar (FHandle h) = do putStrLn "Failed to read a character" exit 1 else pure chr - + getFLine : File -> IO String getFLine (FHandle h) = do str <- prim_fread h @@ -95,7 +95,7 @@ getFLine (FHandle h) = do getNChars : File -> Nat -> IO (List Char) getNChars i Z = pure [] getNChars i (S k) - = do x <- getChar i + = do x <- getChar i xs <- getNChars i k pure (x :: xs) @@ -117,10 +117,10 @@ hex 'd' = Just 13 hex 'e' = Just 14 hex 'f' = Just 15 hex _ = Nothing - + toHex : Int -> List Char -> Maybe Int toHex _ [] = Just 0 -toHex m (d :: ds) +toHex m (d :: ds) = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds) -- Read 6 characters. If they're a hex number, read that many characters. @@ -145,7 +145,7 @@ process : {auto c : Ref Ctxt Defs} -> process (Interpret cmd) = do interpret cmd printResult "Done" -process (LoadFile fname toline) +process (LoadFile fname toline) = do opts <- get ROpts put ROpts (record { mainfile = Just fname } opts) resetContext @@ -157,7 +157,7 @@ process (LoadFile fname toline) case errs of [] => printResult $ "Loaded " ++ fname _ => printError $ "Failed to load " ++ fname -process (TypeOf n Nothing) +process (TypeOf n Nothing) = do Idris.REPL.process (Check (PRef replFC (UN n))) pure () process (TypeOf n (Just (l, c))) @@ -170,7 +170,7 @@ process (AddClause l n) = do Idris.REPL.process (Editing (AddClause (fromInteger l) (UN n))) pure () process (ExprSearch l n hs all) - = do Idris.REPL.process (Editing (ExprSearch (fromInteger l) (UN n) + = do Idris.REPL.process (Editing (ExprSearch (fromInteger l) (UN n) (map UN hs) all)) pure () process (GenerateDef l n) @@ -205,7 +205,7 @@ processCatch cmd put ROpts o' emitError err printError "Command failed") - + loop : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> @@ -213,7 +213,7 @@ loop : {auto c : Ref Ctxt Defs} -> {auto o : Ref ROpts REPLOpts} -> Core () loop - = do res <- getOutput + = do res <- getOutput case res of REPL _ => printError "Running idemode but output isn't" IDEMode _ inf outf => do @@ -226,11 +226,11 @@ loop loop Right sexp => case getMsg sexp of - Just (cmd, i) => + Just (cmd, i) => do updateOutput i processCatch cmd - loop - Nothing => + loop + Nothing => do printError "Unrecognised command" loop where @@ -254,4 +254,3 @@ replIDE IDEMode _ inf outf => do send outf (version 2 0) loop - diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index 6bf84f7..8f1f06e 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -122,28 +122,29 @@ stMain opts case fname of Nothing => logTime "Loading prelude" $ readPrelude - Just f => logTime "Loading main file" $ + Just f => logTime "Loading main file" $ loadMainFile f doRepl <- postOptions opts - if doRepl - then + if doRepl + then if ide || ideSocket - then - if not ideSocket + then + if not ideSocket then do setOutput (IDEMode 0 stdin stdout) replIDE {c} {u} {m} - else do - f <- coreLift $ initIDESocketFile 38398 + else do + 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} - else do + replIDE {c} {u} {m} + else do iputStrLn $ "Welcome to Idris 2 version " ++ version ++ ". Enjoy yourself!" repl {c} {u} {m} diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 72eb7c2..af68a93 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -18,7 +18,7 @@ addPkgDir : {auto c : Ref Ctxt Defs} -> String -> Core () addPkgDir p = do defs <- get Ctxt - addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++ + addExtraDir (dir_prefix (dirs (options defs)) ++ dirSep ++ "idris2" ++ dirSep ++ p) -- Options to be processed before type checking @@ -37,7 +37,7 @@ preOptions (SetCG e :: opts) = case getCG e of Just cg => do setCG cg preOptions opts - Nothing => + Nothing => do coreLift $ putStrLn "No such code generator" coreLift $ putStrLn $ "Code generators available: " ++ showSep ", " (map fst availableCGs) @@ -58,11 +58,11 @@ postOptions : {auto c : Ref Ctxt Defs} -> {auto m : Ref MD Metadata} -> List CLOpt -> Core Bool postOptions [] = pure True -postOptions (ExecFn str :: rest) +postOptions (ExecFn str :: rest) = do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str)) postOptions rest pure False -postOptions (CheckOnly :: rest) +postOptions (CheckOnly :: rest) = do postOptions rest pure False postOptions (_ :: rest) = postOptions rest @@ -76,6 +76,5 @@ ideMode (_ :: xs) = ideMode xs export ideModeSocket : List CLOpt -> Bool ideModeSocket [] = False -ideModeSocket (IdeModeSocket :: _) = True +ideModeSocket (IdeModeSocket _ :: _) = True ideModeSocket (_ :: xs) = ideModeSocket xs - From 4f21234c9e8aff25950fb97720cd76f5e5ad0c3f Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Fri, 19 Jul 2019 12:34:15 +0200 Subject: [PATCH 02/20] basic test for --ide-mode how to take care of input termination properly? currently we add the message 'Alas the file is done' in the expected outcome but that's ugly --- src/Idris/IDEMode/REPL.idr | 29 ++++++++++++++++++++++++++++ tests/Main.idr | 20 +++++++++++-------- tests/ideMode/ideMode001/LocType.idr | 7 +++++++ tests/ideMode/ideMode001/expected | 4 ++++ tests/ideMode/ideMode001/input | 1 + tests/ideMode/ideMode001/run | 3 +++ 6 files changed, 56 insertions(+), 8 deletions(-) create mode 100644 tests/ideMode/ideMode001/LocType.idr create mode 100644 tests/ideMode/ideMode001/expected create mode 100644 tests/ideMode/ideMode001/input create mode 100755 tests/ideMode/ideMode001/run diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 54868a6..f56efbc 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -15,6 +15,8 @@ import Core.Options import Core.TT import Core.Unify +import Data.Primitives.Views + import Idris.Desugar import Idris.Error import Idris.ModTree @@ -123,6 +125,33 @@ toHex _ [] = Just 0 toHex m (d :: ds) = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds) +hexDigit : Int -> Char +hexDigit 0 = '0' +hexDigit 1 = '1' +hexDigit 2 = '2' +hexDigit 3 = '3' +hexDigit 4 = '4' +hexDigit 5 = '5' +hexDigit 6 = '6' +hexDigit 7 = '7' +hexDigit 8 = '8' +hexDigit 9 = '9' +hexDigit 10 = 'a' +hexDigit 11 = 'b' +hexDigit 12 = 'c' +hexDigit 13 = 'd' +hexDigit 14 = 'e' +hexDigit 15 = 'f' + +||| Convert a positive integer into a list of (lower case) hexadecimal characters +asHex : Int -> String +asHex n = pack $ asHex' n [] + where + asHex' : Int -> List Char -> List Char + asHex' 0 hex = hex + asHex' n hex with (n `divides` 16) + asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex) + -- Read 6 characters. If they're a hex number, read that many characters. -- Otherwise, just read to newline getInput : File -> IO String diff --git a/tests/Main.idr b/tests/Main.idr index 6ee5930..b271bf3 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -5,7 +5,7 @@ import System %default covering ttimpTests : List String -ttimpTests +ttimpTests = ["basic001", "basic002", "basic003", "basic004", "basic005", "basic006", "coverage001", "coverage002", @@ -53,16 +53,20 @@ typeddTests chezTests : List String chezTests - = ["chez001", "chez002", "chez003", "chez004", + = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", "chez007"] +ideModeTests : List String +ideModeTests + = [ "ideMode001" ] + chdir : String -> IO Bool -chdir dir +chdir dir = do ok <- foreign FFI_C "chdir" (String -> IO Int) dir pure (ok == 0) fail : String -> IO () -fail err +fail err = do putStrLn err exitWith (ExitFailure 1) @@ -79,7 +83,7 @@ runTest dir prog test pure False if (out == exp) then putStrLn "success" - else putStrLn "FAILURE" + else putStrLn $ "FAILURE: found " ++ out chdir "../.." pure (out == exp) @@ -109,16 +113,16 @@ main ttimps <- traverse (runTest "ttimp" idris2) ttimpTests idrs <- traverse (runTest "idris2" idris2) idrisTests typedds <- traverse (runTest "typedd-book" idris2) typeddTests + ideModes <- traverse (runTest "ideMode" idris2) ideModeTests chexec <- findChez chezs <- maybe (do putStrLn "Chez Scheme not found" pure []) (\c => do putStrLn $ "Found Chez Scheme at " ++ c traverse (runTest "chez" idris2) chezTests) chexec - let res = ttimps ++ typedds ++ idrs ++ chezs - putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) + let res = ttimps ++ typedds ++ idrs ++ ideModes ++ chezs + putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) ++ " tests successful") if (any not res) then exitWith (ExitFailure 1) else exitWith ExitSuccess - diff --git a/tests/ideMode/ideMode001/LocType.idr b/tests/ideMode/ideMode001/LocType.idr new file mode 100644 index 0000000..dd8a348 --- /dev/null +++ b/tests/ideMode/ideMode001/LocType.idr @@ -0,0 +1,7 @@ +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +append : Vect n a -> Vect m a -> Vect (n + m) a +append [] ys = ys +append (x :: xs) ys = x :: append xs ys diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected new file mode 100644 index 0000000..22d62d3 --- /dev/null +++ b/tests/ideMode/ideMode001/expected @@ -0,0 +1,4 @@ +000018(:protocol-version 2 0) +000038(:write-string "1/1: Building LocType (LocType.idr)" 1) +00002a(:return (:ok "Loaded LocType.idr" ()) 1) +Alas the file is done, aborting diff --git a/tests/ideMode/ideMode001/input b/tests/ideMode/ideMode001/input new file mode 100644 index 0000000..f079ba3 --- /dev/null +++ b/tests/ideMode/ideMode001/input @@ -0,0 +1 @@ +00001e((:load-file "LocType.idr") 1) diff --git a/tests/ideMode/ideMode001/run b/tests/ideMode/ideMode001/run new file mode 100755 index 0000000..86bdf71 --- /dev/null +++ b/tests/ideMode/ideMode001/run @@ -0,0 +1,3 @@ +$1 --ide-mode < input + +rm -rf build From 72f579aaa936bc5ced82fa59fe7bb431b439d8cb Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 21 Jul 2019 07:14:46 +0200 Subject: [PATCH 03/20] [wip] introduce IDE-mode Client * immediate goal is to be able to write tests against the IDE-mode server * next goal would be to have a REPL talking to a server --- src/Idris/IDEMode/Client.idr | 75 ++++++++++++++++++++++++++++++++++ src/Idris/IDEMode/Commands.idr | 31 ++++++++++++-- src/Idris/IDEMode/REPL.idr | 28 ------------- 3 files changed, 102 insertions(+), 32 deletions(-) create mode 100644 src/Idris/IDEMode/Client.idr diff --git a/src/Idris/IDEMode/Client.idr b/src/Idris/IDEMode/Client.idr new file mode 100644 index 0000000..82fc2f4 --- /dev/null +++ b/src/Idris/IDEMode/Client.idr @@ -0,0 +1,75 @@ +module Idris.IDEMode.Client + +import Data.Primitives.Views +import System +import Idris.IDEMode.Commands +import Idris.Socket +import Idris.Socket.Data +import Idris.IDEMode.REPL + +hexDigit : Int -> Char +hexDigit 0 = '0' +hexDigit 1 = '1' +hexDigit 2 = '2' +hexDigit 3 = '3' +hexDigit 4 = '4' +hexDigit 5 = '5' +hexDigit 6 = '6' +hexDigit 7 = '7' +hexDigit 8 = '8' +hexDigit 9 = '9' +hexDigit 10 = 'a' +hexDigit 11 = 'b' +hexDigit 12 = 'c' +hexDigit 13 = 'd' +hexDigit 14 = 'e' +hexDigit 15 = 'f' + +||| Convert a positive integer into a list of (lower case) hexadecimal characters +asHex : Int -> String +asHex n = pack $ asHex' n [] + where + asHex' : Int -> List Char -> List Char + asHex' 0 hex = hex + asHex' n hex with (n `divides` 16) + asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex) + +connectTo : String -> Int -> IO (Either String Socket) +connectTo host port = do + osock <- socket AF_INET Stream 0 + case osock of + Left fail => do + pure $ Left ("Failed to open client socket " ++ show fail) + Right sock => do + res <- connect sock (Hostname host) port + if res /= 0 + then pure $ Left ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show res) + else pure (Right sock) + +||| Runs an ide-mode client to execute one command against a given server +serialize : IDECommand -> Maybe String +serialize cmd = + let scmd = show $ SExpList [ toSExp cmd, toSExp 1 ] + hexLen = asHex $ cast $ Strings.length scmd + len = case isLTE (length hexLen) 6 of + (Yes _) => Just $ cast (replicate (6 - length hexLen) '0') ++ hexLen + (No _) => Nothing + in (++) <$> len <*> Just scmd + +client : String -> Int -> IDECommand -> IO () +client host port command = do + cnx<- connectTo host port + case cnx of + Left fail => do + putStrLn fail + Right sock => do + let cmdString = serialize command + case cmdString of + Just cmd => do + res <- send sock cmd + case res of + Left err => + putStrLn ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show err) + Right sent => + putStrLn ("Sent " ++ show sent ++ " bytes") + Nothing => putStrLn "Command is too long" diff --git a/src/Idris/IDEMode/Commands.idr b/src/Idris/IDEMode/Commands.idr index ac56125..9b4cba3 100644 --- a/src/Idris/IDEMode/Commands.idr +++ b/src/Idris/IDEMode/Commands.idr @@ -25,7 +25,7 @@ data IDECommand | MakeLemma Integer String | MakeCase Integer String | MakeWith Integer String - + readHints : List SExp -> Maybe (List String) readHints [] = Just [] readHints (StringAtom s :: rest) @@ -46,7 +46,7 @@ getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n]) getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n, IntegerAtom l, IntegerAtom c]) = Just $ TypeOf n (Just (l, c)) -getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c, +getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c, StringAtom n]) = Just $ CaseSplit l c n getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n]) @@ -76,6 +76,25 @@ getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n]) = Just $ MakeWith l n getIDECommand _ = Nothing +export +putIDECommand : IDECommand -> SExp +putIDECommand (Interpret cmd) = (SExpList [SymbolAtom "interpret", StringAtom cmd]) +putIDECommand (LoadFile fname Nothing) = (SExpList [SymbolAtom "load-file", StringAtom fname]) +putIDECommand (LoadFile fname (Just line)) = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line]) +putIDECommand (TypeOf cmd Nothing) = (SExpList [SymbolAtom "type-of", StringAtom cmd]) +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 (ExprSearch line n exprs mode) = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode]) + where + getMode : Bool -> SExp + getMode True = SymbolAtom "all" + getMode False = SymbolAtom "other" +putIDECommand (GenerateDef line n) = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n]) +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]) + export getMsg : SExp -> Maybe (IDECommand, Integer) getMsg (SExpList [cmdexp, IntegerAtom num]) @@ -103,6 +122,10 @@ public export interface SExpable a where toSExp : a -> SExp +export +SExpable IDECommand where + toSExp = putIDECommand + export SExpable SExp where toSExp = id @@ -129,7 +152,7 @@ SExpable Name where export (SExpable a, SExpable b) => SExpable (a, b) where - toSExp (x, y) + toSExp (x, y) = case toSExp y of SExpList xs => SExpList (toSExp x :: xs) y' => SExpList [toSExp x, y'] @@ -151,7 +174,7 @@ hex : File -> Int -> IO () hex (FHandle h) num = foreign FFI_C "fprintf" (Ptr -> String -> Int -> IO ()) h "%06x" num sendLine : File -> String -> IO () -sendLine (FHandle h) st = +sendLine (FHandle h) st = map (const ()) (prim_fwrite h st) export diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index f56efbc..19f43b7 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -15,8 +15,6 @@ import Core.Options import Core.TT import Core.Unify -import Data.Primitives.Views - import Idris.Desugar import Idris.Error import Idris.ModTree @@ -125,32 +123,6 @@ toHex _ [] = Just 0 toHex m (d :: ds) = pure $ !(hex (toLower d)) * m + !(toHex (m*16) ds) -hexDigit : Int -> Char -hexDigit 0 = '0' -hexDigit 1 = '1' -hexDigit 2 = '2' -hexDigit 3 = '3' -hexDigit 4 = '4' -hexDigit 5 = '5' -hexDigit 6 = '6' -hexDigit 7 = '7' -hexDigit 8 = '8' -hexDigit 9 = '9' -hexDigit 10 = 'a' -hexDigit 11 = 'b' -hexDigit 12 = 'c' -hexDigit 13 = 'd' -hexDigit 14 = 'e' -hexDigit 15 = 'f' - -||| Convert a positive integer into a list of (lower case) hexadecimal characters -asHex : Int -> String -asHex n = pack $ asHex' n [] - where - asHex' : Int -> List Char -> List Char - asHex' 0 hex = hex - asHex' n hex with (n `divides` 16) - asHex' (16 * div + rem) hex | DivBy {div} {rem} _ = asHex' div (hexDigit rem :: hex) -- Read 6 characters. If they're a hex number, read that many characters. -- Otherwise, just read to newline From a6610a1a075b6d079385413215318d1bec29153b Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 21 Jul 2019 07:35:20 +0200 Subject: [PATCH 04/20] add very basic and fragile test for ide-mode-socket --- tests/Main.idr | 11 ++++++----- tests/ideMode/ideMode002/LocType.idr | 7 +++++++ tests/ideMode/ideMode002/expected | 3 +++ tests/ideMode/ideMode002/input | 1 + tests/ideMode/ideMode002/run | 6 ++++++ 5 files changed, 23 insertions(+), 5 deletions(-) create mode 100644 tests/ideMode/ideMode002/LocType.idr create mode 100644 tests/ideMode/ideMode002/expected create mode 100644 tests/ideMode/ideMode002/input create mode 100755 tests/ideMode/ideMode002/run diff --git a/tests/Main.idr b/tests/Main.idr index b271bf3..7b87af7 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -58,7 +58,7 @@ chezTests ideModeTests : List String ideModeTests - = [ "ideMode001" ] + = [ "ideMode001", "ideMode002" ] chdir : String -> IO Bool chdir dir @@ -110,9 +110,9 @@ main : IO () main = do [_, idris2] <- getArgs | _ => do putStrLn "Usage: runtests [ttimp path]" - ttimps <- traverse (runTest "ttimp" idris2) ttimpTests - idrs <- traverse (runTest "idris2" idris2) idrisTests - typedds <- traverse (runTest "typedd-book" idris2) typeddTests + -- ttimps <- traverse (runTest "ttimp" idris2) ttimpTests + -- idrs <- traverse (runTest "idris2" idris2) idrisTests + -- typedds <- traverse (runTest "typedd-book" idris2) typeddTests ideModes <- traverse (runTest "ideMode" idris2) ideModeTests chexec <- findChez chezs <- maybe (do putStrLn "Chez Scheme not found" @@ -120,7 +120,8 @@ main (\c => do putStrLn $ "Found Chez Scheme at " ++ c traverse (runTest "chez" idris2) chezTests) chexec - let res = ttimps ++ typedds ++ idrs ++ ideModes ++ chezs + let res = --ttimps ++ typedds ++ idrs ++ + ideModes ++ chezs putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) ++ " tests successful") if (any not res) diff --git a/tests/ideMode/ideMode002/LocType.idr b/tests/ideMode/ideMode002/LocType.idr new file mode 100644 index 0000000..dd8a348 --- /dev/null +++ b/tests/ideMode/ideMode002/LocType.idr @@ -0,0 +1,7 @@ +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + (::) : a -> Vect k a -> Vect (S k) a + +append : Vect n a -> Vect m a -> Vect (n + m) a +append [] ys = ys +append (x :: xs) ys = x :: append xs ys diff --git a/tests/ideMode/ideMode002/expected b/tests/ideMode/ideMode002/expected new file mode 100644 index 0000000..345e631 --- /dev/null +++ b/tests/ideMode/ideMode002/expected @@ -0,0 +1,3 @@ +000018(:protocol-version 2 0) +000038(:write-string "1/1: Building LocType (LocType.idr)" 1) +00002a(:return (:ok "Loaded LocType.idr" ()) 1) diff --git a/tests/ideMode/ideMode002/input b/tests/ideMode/ideMode002/input new file mode 100644 index 0000000..f079ba3 --- /dev/null +++ b/tests/ideMode/ideMode002/input @@ -0,0 +1 @@ +00001e((:load-file "LocType.idr") 1) diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run new file mode 100755 index 0000000..25789e5 --- /dev/null +++ b/tests/ideMode/ideMode002/run @@ -0,0 +1,6 @@ +$1 --ide-mode-socket 0.0.0.0:34567 > /dev/null & +sleep 2 +nc localhost 34567 < input + +kill %1 +rm -rf build From 775c67452a95556fa0e38a18852616c2d1794859 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 27 Jul 2019 17:18:06 +0200 Subject: [PATCH 05/20] reactivate all tests --- tests/Main.idr | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/Main.idr b/tests/Main.idr index 9f2f4a0..2b8c945 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -113,9 +113,9 @@ main : IO () main = do [_, idris2] <- getArgs | _ => do putStrLn "Usage: runtests [ttimp path]" - -- ttimps <- traverse (runTest "ttimp" idris2) ttimpTests - -- idrs <- traverse (runTest "idris2" idris2) idrisTests - -- typedds <- traverse (runTest "typedd-book" idris2) typeddTests + ttimps <- traverse (runTest "ttimp" idris2) ttimpTests + idrs <- traverse (runTest "idris2" idris2) idrisTests + typedds <- traverse (runTest "typedd-book" idris2) typeddTests ideModes <- traverse (runTest "ideMode" idris2) ideModeTests chexec <- findChez chezs <- maybe (do putStrLn "Chez Scheme not found" @@ -123,7 +123,7 @@ main (\c => do putStrLn $ "Found Chez Scheme at " ++ c traverse (runTest "chez" idris2) chezTests) chexec - let res = --ttimps ++ typedds ++ idrs ++ + let res = ttimps ++ typedds ++ idrs ++ ideModes ++ chezs putStrLn (show (length (filter id res)) ++ "/" ++ show (length res) ++ " tests successful") From c49942cfc4ab8d4716374f0f0fabbaccbd086622 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 30 Jul 2019 07:57:44 +0200 Subject: [PATCH 06/20] (hopefully) fix ide-mode-socket test for some reason running idris2 _without_ an input file fails which throws this test in a spin. We start the interpreter in ide mode on a socket loading an empty module without prelude and then request loading a file that does not require Prelude. --- tests/ideMode/ideMode002/Empty.idr | 1 + tests/ideMode/ideMode002/LocType.idr | 7 ------ tests/ideMode/ideMode002/Vect.idr | 34 ++++++++++++++++++++++++++++ tests/ideMode/ideMode002/expected | 4 ++-- tests/ideMode/ideMode002/input | 2 +- tests/ideMode/ideMode002/run | 5 ++-- 6 files changed, 41 insertions(+), 12 deletions(-) create mode 100644 tests/ideMode/ideMode002/Empty.idr delete mode 100644 tests/ideMode/ideMode002/LocType.idr create mode 100644 tests/ideMode/ideMode002/Vect.idr diff --git a/tests/ideMode/ideMode002/Empty.idr b/tests/ideMode/ideMode002/Empty.idr new file mode 100644 index 0000000..b052a4c --- /dev/null +++ b/tests/ideMode/ideMode002/Empty.idr @@ -0,0 +1 @@ +module Empty diff --git a/tests/ideMode/ideMode002/LocType.idr b/tests/ideMode/ideMode002/LocType.idr deleted file mode 100644 index dd8a348..0000000 --- a/tests/ideMode/ideMode002/LocType.idr +++ /dev/null @@ -1,7 +0,0 @@ -data Vect : Nat -> Type -> Type where - Nil : Vect Z a - (::) : a -> Vect k a -> Vect (S k) a - -append : Vect n a -> Vect m a -> Vect (n + m) a -append [] ys = ys -append (x :: xs) ys = x :: append xs ys diff --git a/tests/ideMode/ideMode002/Vect.idr b/tests/ideMode/ideMode002/Vect.idr new file mode 100644 index 0000000..300ac93 --- /dev/null +++ b/tests/ideMode/ideMode002/Vect.idr @@ -0,0 +1,34 @@ +data Nat = Z | S Nat + +plus : Nat -> Nat -> Nat +plus Z y = y +plus (S k) y = S (plus k y) + +data Vect : Nat -> Type -> Type where + Nil : Vect Z a + Cons : a -> Vect k a -> Vect (S k) a + +foldl : (0 b : Nat -> Type) -> + ({k : Nat} -> b k -> a -> b (S k)) -> + b Z -> + Vect n a -> b n +foldl b g z Nil = z +foldl b g z (Cons x xs) = foldl (\i => b (S i)) g (g z x) xs + +reverse : Vect n a -> Vect n a +reverse + = foldl (\m => Vect m a) + (\rev => \x => Cons x rev) Nil + +append : Vect n a -> Vect m a -> Vect (plus n m) a +append Nil ys = ys +append (Cons x xs) ys = Cons x (append xs ys) + +vlength : (n : Nat) -> Vect n a -> Nat +vlength Z Nil = Z +vlength n@_ (Cons x xs) = n -- (vlength _ xs); + +zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c +zipWith f Nil Nil = Nil +-- zipWith f (Cons x xs) Nil impossible +zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys) diff --git a/tests/ideMode/ideMode002/expected b/tests/ideMode/ideMode002/expected index 345e631..0499bc6 100644 --- a/tests/ideMode/ideMode002/expected +++ b/tests/ideMode/ideMode002/expected @@ -1,3 +1,3 @@ 000018(:protocol-version 2 0) -000038(:write-string "1/1: Building LocType (LocType.idr)" 1) -00002a(:return (:ok "Loaded LocType.idr" ()) 1) +000032(:write-string "1/1: Building Vect (Vect.idr)" 1) +000027(:return (:ok "Loaded Vect.idr" ()) 1) diff --git a/tests/ideMode/ideMode002/input b/tests/ideMode/ideMode002/input index f079ba3..fe64178 100644 --- a/tests/ideMode/ideMode002/input +++ b/tests/ideMode/ideMode002/input @@ -1 +1 @@ -00001e((:load-file "LocType.idr") 1) +00001b((:load-file "Vect.idr") 1) diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run index 25789e5..af96f74 100755 --- a/tests/ideMode/ideMode002/run +++ b/tests/ideMode/ideMode002/run @@ -1,6 +1,7 @@ -$1 --ide-mode-socket 0.0.0.0:34567 > /dev/null & +$1 --no-prelude --ide-mode-socket 0.0.0.0:34567 Empty.idr > /dev/null & sleep 2 -nc localhost 34567 < input + +nc -G 5 127.0.0.1 34567 < input kill %1 rm -rf build From 39a5c25fbcc65d91b6e65f7d6f5489d8586c8ee9 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Fri, 2 Aug 2019 17:59:17 +0200 Subject: [PATCH 07/20] remove ide socket mode test because it's hard to make reliable --- tests/ideMode/ideMode002/Empty.idr | 1 - tests/ideMode/ideMode002/Vect.idr | 34 ------------------------------ tests/ideMode/ideMode002/expected | 3 --- tests/ideMode/ideMode002/input | 1 - tests/ideMode/ideMode002/run | 7 ------ 5 files changed, 46 deletions(-) delete mode 100644 tests/ideMode/ideMode002/Empty.idr delete mode 100644 tests/ideMode/ideMode002/Vect.idr delete mode 100644 tests/ideMode/ideMode002/expected delete mode 100644 tests/ideMode/ideMode002/input delete mode 100755 tests/ideMode/ideMode002/run diff --git a/tests/ideMode/ideMode002/Empty.idr b/tests/ideMode/ideMode002/Empty.idr deleted file mode 100644 index b052a4c..0000000 --- a/tests/ideMode/ideMode002/Empty.idr +++ /dev/null @@ -1 +0,0 @@ -module Empty diff --git a/tests/ideMode/ideMode002/Vect.idr b/tests/ideMode/ideMode002/Vect.idr deleted file mode 100644 index 300ac93..0000000 --- a/tests/ideMode/ideMode002/Vect.idr +++ /dev/null @@ -1,34 +0,0 @@ -data Nat = Z | S Nat - -plus : Nat -> Nat -> Nat -plus Z y = y -plus (S k) y = S (plus k y) - -data Vect : Nat -> Type -> Type where - Nil : Vect Z a - Cons : a -> Vect k a -> Vect (S k) a - -foldl : (0 b : Nat -> Type) -> - ({k : Nat} -> b k -> a -> b (S k)) -> - b Z -> - Vect n a -> b n -foldl b g z Nil = z -foldl b g z (Cons x xs) = foldl (\i => b (S i)) g (g z x) xs - -reverse : Vect n a -> Vect n a -reverse - = foldl (\m => Vect m a) - (\rev => \x => Cons x rev) Nil - -append : Vect n a -> Vect m a -> Vect (plus n m) a -append Nil ys = ys -append (Cons x xs) ys = Cons x (append xs ys) - -vlength : (n : Nat) -> Vect n a -> Nat -vlength Z Nil = Z -vlength n@_ (Cons x xs) = n -- (vlength _ xs); - -zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c -zipWith f Nil Nil = Nil --- zipWith f (Cons x xs) Nil impossible -zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys) diff --git a/tests/ideMode/ideMode002/expected b/tests/ideMode/ideMode002/expected deleted file mode 100644 index 0499bc6..0000000 --- a/tests/ideMode/ideMode002/expected +++ /dev/null @@ -1,3 +0,0 @@ -000018(:protocol-version 2 0) -000032(:write-string "1/1: Building Vect (Vect.idr)" 1) -000027(:return (:ok "Loaded Vect.idr" ()) 1) diff --git a/tests/ideMode/ideMode002/input b/tests/ideMode/ideMode002/input deleted file mode 100644 index fe64178..0000000 --- a/tests/ideMode/ideMode002/input +++ /dev/null @@ -1 +0,0 @@ -00001b((:load-file "Vect.idr") 1) diff --git a/tests/ideMode/ideMode002/run b/tests/ideMode/ideMode002/run deleted file mode 100755 index af96f74..0000000 --- a/tests/ideMode/ideMode002/run +++ /dev/null @@ -1,7 +0,0 @@ -$1 --no-prelude --ide-mode-socket 0.0.0.0:34567 Empty.idr > /dev/null & -sleep 2 - -nc -G 5 127.0.0.1 34567 < input - -kill %1 -rm -rf build From c6ba34c770d576d8be08571ea3423296be9dcc37 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Fri, 2 Aug 2019 19:46:58 +0200 Subject: [PATCH 08/20] really remove ide mode socket test --- tests/Main.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/Main.idr b/tests/Main.idr index 4ed51ba..0e864ec 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -64,7 +64,7 @@ chezTests ideModeTests : List String ideModeTests - = [ "ideMode001", "ideMode002" ] + = [ "ideMode001" ] chdir : String -> IO Bool chdir dir From 74a27f3861077e1de5f6fd81bfe799fa0483f63d Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 3 Aug 2019 11:36:54 +0200 Subject: [PATCH 09/20] make Client actually work --- src/Idris/IDEMode/Client.idr | 31 +++++++++++++++++++++++++------ src/Idris/IDEMode/REPL.idr | 1 + 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/src/Idris/IDEMode/Client.idr b/src/Idris/IDEMode/Client.idr index 82fc2f4..0f72e6c 100644 --- a/src/Idris/IDEMode/Client.idr +++ b/src/Idris/IDEMode/Client.idr @@ -3,9 +3,11 @@ module Idris.IDEMode.Client import Data.Primitives.Views import System import Idris.IDEMode.Commands +import Idris.IDEMode.Parser import Idris.Socket import Idris.Socket.Data import Idris.IDEMode.REPL +import Parser.Support hexDigit : Int -> Char hexDigit 0 = '0' @@ -56,6 +58,25 @@ serialize cmd = (No _) => Nothing in (++) <$> len <*> Just scmd + +readOutput : Socket -> IO (Either String SExp) +readOutput sock = do + Right (len, _) <- recv sock 6 | Left err => pure (Left $ "failed to read from socket, error: " ++ show err) + case toHex 1 (reverse $ cast len) of + Nothing => pure $ Left ("expected a length in six-digits hexadecimal, got " ++ len) + Just num => do + Right (msg, _) <- recv sock num | Left err => pure (Left $ "failed to read from socket, error: " ++ show err) + pure $ either (Left . show) Right $ parseSExp msg + +readResult: Socket -> IO () +readResult sock = do + Right output <- readOutput sock | Left err => putStrLn err + case output of + SExpList (SymbolAtom "return" :: rest) => putStrLn $ show (SExpList rest) + res => do + putStrLn (show res) + readResult sock + client : String -> Int -> IDECommand -> IO () client host port command = do cnx<- connectTo host port @@ -66,10 +87,8 @@ client host port command = do let cmdString = serialize command case cmdString of Just cmd => do - res <- send sock cmd - case res of - Left err => - putStrLn ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show err) - Right sent => - putStrLn ("Sent " ++ show sent ++ " bytes") + Right sent <- send sock cmd + | Left err =>putStrLn ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show err) + readResult sock + close sock Nothing => putStrLn "Command is too long" diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index ec80de0..4ad2abc 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -118,6 +118,7 @@ hex 'e' = Just 14 hex 'f' = Just 15 hex _ = Nothing +export toHex : Int -> List Char -> Maybe Int toHex _ [] = Just 0 toHex m (d :: ds) From 6e8b5aa2d2356649abe5470474341d9d888ab20b Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sat, 3 Aug 2019 14:00:44 +0200 Subject: [PATCH 10/20] output test result when diff fails --- libs/network/lib-tests | 1 + 1 file changed, 1 insertion(+) diff --git a/libs/network/lib-tests b/libs/network/lib-tests index 67f84a0..ba494b6 100755 --- a/libs/network/lib-tests +++ b/libs/network/lib-tests @@ -4,6 +4,7 @@ ${IDRIS2} --exec main Echo.idr > build/output if ! [ -z "$(diff build/output expected)" ]; then echo "TEST FAILURE: unexpected build/output" + cat build/output exit 2 else echo "TEST SUCCESS" From c40eabc7e5298b0932616c9b17ededeba08fb2eb Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Tue, 6 Aug 2019 10:46:02 +0200 Subject: [PATCH 11/20] provide a socket-based client REPL --- src/Idris/IDEMode/Client.idr | 89 ++++++++++++++++++++++++++++-------- 1 file changed, 69 insertions(+), 20 deletions(-) diff --git a/src/Idris/IDEMode/Client.idr b/src/Idris/IDEMode/Client.idr index 0f72e6c..5cdc218 100644 --- a/src/Idris/IDEMode/Client.idr +++ b/src/Idris/IDEMode/Client.idr @@ -5,6 +5,8 @@ import System import Idris.IDEMode.Commands import Idris.IDEMode.Parser import Idris.Socket +import Idris.Syntax +import Idris.REPL import Idris.Socket.Data import Idris.IDEMode.REPL import Parser.Support @@ -68,27 +70,74 @@ readOutput sock = do Right (msg, _) <- recv sock num | Left err => pure (Left $ "failed to read from socket, error: " ++ show err) pure $ either (Left . show) Right $ parseSExp msg -readResult: Socket -> IO () -readResult sock = do - Right output <- readOutput sock | Left err => putStrLn err - case output of - SExpList (SymbolAtom "return" :: rest) => putStrLn $ show (SExpList rest) - res => do - putStrLn (show res) - readResult sock +data IDEResult : Type where + IDEReturn : List SExp -> IDEResult + NetworkError : String -> IDEResult + InputError : String -> IDEResult + OutputError : String -> IDEResult -client : String -> Int -> IDECommand -> IO () -client host port command = do - cnx<- connectTo host port - case cnx of - Left fail => do - putStrLn fail - Right sock => do +implementation Show IDEResult where + show (IDEReturn exprs) = unlines $ map show exprs + show (NetworkError reason) = reason + show (InputError reason) = reason + show (OutputError reason) = reason + + +readResult: Socket -> List SExp -> IO IDEResult +readResult sock outputs = do + Right output <- readOutput sock | Left err => pure (OutputError err) + case output of + SExpList (SymbolAtom "return" :: rest) => pure (IDEReturn (SExpList rest :: outputs)) + res => do + readResult sock (res :: outputs) + +execute : Socket -> IDECommand -> IO IDEResult +execute cnx command = do let cmdString = serialize command case cmdString of Just cmd => do - Right sent <- send sock cmd - | Left err =>putStrLn ("Failed to connect to :" ++ host ++ ":" ++ show port ++", " ++ show err) - readResult sock - close sock - Nothing => putStrLn "Command is too long" + Right sent <- send cnx cmd + | Left err => pure (NetworkError ("Failed to send command, error: " ++ show err)) + readResult cnx [] + Nothing => pure $ InputError "Command is too long" + +connect : String -> Int -> IO Socket +connect host port = do + Right sock <- connectTo host port + | Left fail => do + putStrLn $ "fail to connect to " ++ host ++ ":" ++ show port ++", error: " ++ fail + exit 1 + pure sock + +makeIDECommand : REPLCmd -> Either String IDECommand +makeIDECommand (Eval term) = Right $ Interpret (show term) +makeIDECommand (Check term) = Right $ TypeOf (show term) Nothing +makeIDECommand (Load file) = Right $ LoadFile file Nothing +makeIDECommand (Editing (TypeAt line col name)) = Right $ TypeOf (show name) (Just (cast line, cast col)) +makeIDECommand other = Left "Don't know how to interpret command" + +parseCommand : String -> Either String IDECommand +parseCommand = either (Left . show) makeIDECommand . parseRepl + +repl : Socket -> IO () +repl cnx + = do putStr prompt + Right input <- map parseCommand getLine + | Left err => do + putStrLn err + repl cnx + end <- fEOF stdin + if end + then putStrLn "Bye!" + else do + result <- execute cnx input + putStrLn $ show result + repl cnx + + where + prompt : String + prompt = "λ> " + +export +client : String -> Int -> IO () +client host port = connect host port >>= repl From d04333a7f648e86e39818b189bb7c65120307fa5 Mon Sep 17 00:00:00 2001 From: "Keller, Bryn" Date: Tue, 20 Aug 2019 16:24:23 -0700 Subject: [PATCH 12/20] Added note to INSTALL.md to recommend Mac OS X users install Chez from source since homebrew package appears to not support threading --- INSTALL.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/INSTALL.md b/INSTALL.md index b871f1c..d22a5aa 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -24,7 +24,9 @@ Chez Scheme is available to build from source: + https://cisco.github.io/ChezScheme/ -Many popular package managers will provide a binary distribution for Chez. +Many popular package managers will provide a binary distribution for Chez. Note +that homebrew for Mac OS X provides a version without multithreading support, so +Mac OS X users will want to build from source. **Note**: If you install ChezScheme from source files, building it locally, make sure you run `./configure --threads` to build multithreading support in. From 3a33dc3d7dfc4a296b9b5dd903b5a22f7934a18d Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Mon, 26 Aug 2019 17:42:15 +0200 Subject: [PATCH 13/20] add specialised option to listen on different host/port --- src/Idris/CommandLine.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index c31e166..cdf5d52 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -81,8 +81,11 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--ide-mode"] [] [IdeMode] (Just "Run the REPL with machine-readable syntax"), - MkOpt ["--ide-mode-socket"] ["host:port"] (\hp => [IdeModeSocket hp]) - (Just "Run the ide socket mode on given host and port (default: localhost:38398"), + MkOpt ["--ide-mode-socket"] [] [IdeModeSocket "localhost:38398"] + (Just "Run the ide socket mode on default host and port (localhost:38398"), + + MkOpt ["--ide-mode-socket-with"] ["host:port"] (\hp => [IdeModeSocket hp]) + (Just "Run the ide socket mode on given host and port"), MkOpt ["--prefix"] [] [ShowPrefix] (Just "Show installation prefix"), From ba7e0e01d3a79e90a3e219b45ad88e36fdba6eb0 Mon Sep 17 00:00:00 2001 From: lodi Date: Fri, 30 Aug 2019 13:49:36 -0400 Subject: [PATCH 14/20] Fixed #!/usr/bin/env shebang for Chez backend MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit On NixOS, idris2 can't find scheme in the usual locations, so it defaults to generating the following shebang: #!/usr/bin/env scheme --script The `env` program interprets `scheme --script` as one monolithic command, instead of as a command and one argument. /usr/bin/env: ‘scheme --script’: No such file or directory /usr/bin/env: use -[v]S to pass options in shebang lines The -S flag forces `env` to split on whitespace in the intuitive manner. --- src/Compiler/Scheme/Chez.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 8c894f7..c01d5a3 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -29,7 +29,7 @@ findChez Just n => pure n Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] - maybe (pure "/usr/bin/env scheme") pure e + maybe (pure "/usr/bin/env -S scheme") pure e -- Given the chez compiler directives, return a list of pairs of: -- - the library file name From bb246a072a1d0647ed58d478c5169910cb82047d Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 2 Sep 2019 17:10:48 +0100 Subject: [PATCH 15/20] Experimenting with a new FFI Functions can be declared as %foreign with a list of calling conventions, which a backend will work through until it finds one it can understand. Currently implemented only in Chez backend. If this works out, I'll implement it for Racket too, and remove the old primitive functions. There's a bit more boiler plate here than before, but it has the benefit of being more extensible and portable between different back ends. Some examples, pending proper documentation: %foreign "C:puts,libc" "scheme:display" putline : String -> PrimIO () %foreign "C:exp, libm.so.6, math.h" fexp : Double -> Double %foreign "C:initscr, ncurses_glue.so, ncurses.h" prim_initscr : PrimIO () --- libs/prelude/PrimIO.idr | 4 ++ src/Compiler/Common.idr | 24 +++++++ src/Compiler/CompileExpr.idr | 78 ++++++++++++++++---- src/Compiler/Inline.idr | 1 + src/Compiler/Scheme/Chez.idr | 127 ++++++++++++++++++++++++++++++--- src/Compiler/Scheme/Common.idr | 14 ++-- src/Core/Binary.idr | 2 +- src/Core/CompileExpr.idr | 35 ++++++++- src/Core/Context.idr | 8 ++- src/Core/TTC.idr | 87 +++++++++++++++------- src/Idris/Parser.idr | 3 + src/TTImp/ProcessType.idr | 33 ++++++--- src/TTImp/TTImp.idr | 22 +++--- support/chez/support.ss | 1 + support/chicken/support.scm | 1 + support/racket/support.rkt | 1 + 16 files changed, 365 insertions(+), 76 deletions(-) diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 55f719b..6c00710 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -21,6 +21,10 @@ io_bind (MkIO fn) MkIO res = k x' in res w') +public export +PrimIO : Type -> Type +PrimIO a = (1 x : %World) -> IORes a + %extern prim__putStr : String -> (1 x : %World) -> IORes () %extern prim__getStr : (1 x : %World) -> IORes String diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 28dcc57..c68e9e6 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -120,3 +120,27 @@ tmpName = foreign FFI_C "tmpnam" (Ptr -> IO String) null export chmod : String -> Int -> IO () chmod f m = foreign FFI_C "chmod" (String -> Int -> IO ()) f m + +-- Parse a calling convention into a backend/target for the call, and +-- a comma separated list of any other location data. +-- e.g. "scheme:display" - call the scheme function 'display' +-- "C:puts,libc,stdio.h" - call the C function 'puts' which is in +-- the library libc and the header stdio.h +-- Returns Nothing if the string is empty (which a backend can interpret +-- however it likes) +export +parseCC : String -> Maybe (String, List String) +parseCC "" = Nothing +parseCC str + = case span (/= ':') str of + (target, "") => Just (trim target, []) + (target, opts) => Just (trim target, + map trim (getOpts + (assert_total (strTail opts)))) + where + getOpts : String -> List String + getOpts "" = [] + getOpts str + = case span (/= ',') str of + (opt, "") => [opt] + (opt, rest) => opt :: getOpts (assert_total (strTail rest)) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 591761c..2edcea3 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -5,7 +5,9 @@ import public Core.CompileExpr import Core.Context import Core.Env import Core.Name +import Core.Normalise import Core.TT +import Core.Value import Data.NameMap import Data.Vect @@ -27,6 +29,7 @@ numArgs defs (Ref _ _ n) = case !(lookupDefExact n (gamma defs)) of Just (PMDef _ args _ _ _) => pure (length args) Just (ExternDef arity) => pure arity + Just (ForeignDef arity _) => pure arity Just (Builtin {arity} f) => pure arity _ => pure 0 numArgs _ tm = pure 0 @@ -55,12 +58,12 @@ expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars -- No point in applying to anything expandToArity _ (CErased fc) _ = CErased fc -- Overapplied; apply everything as single arguments -expandToArity Z fn args = applyAll fn args +expandToArity Z f args = applyAll f args where applyAll : CExp vars -> List (CExp vars) -> CExp vars applyAll fn [] = fn applyAll fn (a :: args) = applyAll (CApp (getFC fn) fn [a]) args -expandToArity (S k) fn (a :: args) = expandToArity k (addArg fn a) args +expandToArity (S k) f (a :: args) = expandToArity k (addArg f a) args where addArg : CExp vars -> CExp vars -> CExp vars addArg (CApp fc fn args) a = CApp fc fn (args ++ [a]) @@ -270,14 +273,56 @@ mkArgList i (S k) = let (_ ** rec) = mkArgList (i + 1) k in (_ ** ConsArg (MN "arg" i) rec) +data NArgs : Type where + User : Name -> List (Closure []) -> NArgs + NUnit : NArgs + NIORes : Closure [] -> NArgs + +getNArgs : Name -> List (Closure []) -> NArgs +getNArgs (NS _ (UN "IORes")) [arg] = NIORes arg +getNArgs (NS _ (UN "Unit")) [] = NUnit +getNArgs n args = User n args + +nfToCFType : {auto c : Ref Ctxt Defs} -> + NF [] -> Core CFType +nfToCFType (NPrimVal _ IntType) = pure CFInt +nfToCFType (NPrimVal _ StringType) = pure CFString +nfToCFType (NPrimVal _ DoubleType) = pure CFDouble +nfToCFType (NPrimVal _ CharType) = pure CFChar +nfToCFType (NPrimVal _ WorldType) = pure CFWorld +nfToCFType (NTCon _ n _ _ args) + = do defs <- get Ctxt + case getNArgs !(toFullNames n) args of + User un uargs => + do nargs <- traverse (evalClosure defs) uargs + cargs <- traverse nfToCFType nargs + pure (CFUser n cargs) + NUnit => pure CFUnit + NIORes uarg => + do narg <- evalClosure defs uarg + carg <- nfToCFType narg + pure (CFIORes carg) +nfToCFType _ = pure CFUnit + +getCFTypes : {auto c : Ref Ctxt Defs} -> + List CFType -> NF [] -> + Core (List CFType, CFType) +getCFTypes args (NBind fc _ (Pi _ _ ty) sc) + = do aty <- nfToCFType ty + defs <- get Ctxt + sc' <- sc defs (toClosure defaultOpts [] (Erased fc)) + getCFTypes (aty :: args) sc' +getCFTypes args t + = pure (reverse args, !(nfToCFType t)) + toCDef : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> Def -> + NameTags -> Name -> ClosedTerm -> Def -> Core CDef -toCDef tags n None +toCDef tags n ty None = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n)) -toCDef tags n (PMDef _ args _ tree _) +toCDef tags n ty (PMDef _ args _ tree _) = pure $ MkFun _ !(toCExpTree tags n tree) -toCDef tags n (ExternDef arity) +toCDef tags n ty (ExternDef arity) = let (ns ** args) = mkArgList 0 arity in pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args))) where @@ -287,7 +332,11 @@ toCDef tags n (ExternDef arity) getVars : ArgList k ns -> List (Var ns) getVars NoArgs = [] getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest) -toCDef tags n (Builtin {arity} op) +toCDef tags n ty (ForeignDef arity cs) + = do defs <- get Ctxt + (atys, retty) <- getCFTypes [] !(nf defs [] ty) + pure $ MkForeign cs atys retty +toCDef tags n ty (Builtin {arity} op) = let (ns ** args) = mkArgList 0 arity in pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args))) where @@ -297,26 +346,26 @@ toCDef tags n (Builtin {arity} op) getVars : ArgList k ns -> Vect k (Var ns) getVars NoArgs = [] getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest) -toCDef tags n (DCon tag arity) +toCDef tags n ty (DCon tag arity) = case lookup n tags of Just t => pure $ MkCon t arity _ => pure $ MkCon tag arity -toCDef tags n (TCon tag arity _ _ _ _) +toCDef tags n ty (TCon tag arity _ _ _ _) = case lookup n tags of Just t => pure $ MkCon t arity _ => pure $ MkCon tag arity -- We do want to be able to compile these, but also report an error at run time -- (and, TODO: warn at compile time) -toCDef tags n (Hole _ _) +toCDef tags n ty (Hole _ _) = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ show !(getFullName n)) -toCDef tags n (Guess _ _) +toCDef tags n ty (Guess _ _) = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ show !(getFullName n)) -toCDef tags n (BySearch _ _ _) +toCDef tags n ty (BySearch _ _ _) = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ show !(getFullName n)) -toCDef tags n def +toCDef tags n ty def = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ show (!(getFullName n), def)) @@ -333,5 +382,6 @@ compileDef tags n = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n)) - ce <- toCDef tags n !(toFullNames (definition gdef)) + ce <- toCDef tags n (type gdef) + !(toFullNames (definition gdef)) setCompiled n ce diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr index c76ef2e..0a87dc2 100644 --- a/src/Compiler/Inline.idr +++ b/src/Compiler/Inline.idr @@ -58,6 +58,7 @@ unloadApp n args e = unload (drop n args) (CApp (getFC e) e (take n args)) getArity : CDef -> Nat getArity (MkFun args _) = length args getArity (MkCon _ arity) = arity +getArity (MkForeign _ args _) = length args getArity (MkError _) = 0 takeFromStack : EEnv free vars -> Stack free -> (args : List Name) -> diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 8c894f7..fe303e2 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -30,6 +30,15 @@ findChez Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] maybe (pure "/usr/bin/env scheme") pure e + +locate : {auto c : Ref Ctxt Defs} -> + String -> Core (String, String) +locate fname + = do fullname <- catch (findLibraryFile fname) + (\err => -- assume a system library so not + -- in our library path + pure fname) + pure (fname, fullname) -- Given the chez compiler directives, return a list of pairs of: -- - the library file name @@ -43,14 +52,6 @@ findLibs ds = do let libs = mapMaybe (isLib . trim) ds traverse locate (nub libs) where - locate : String -> Core (String, String) - locate fname - = do fullname <- catch (findLibraryFile fname) - (\err => -- assume a system library so not - -- in our library path - pure fname) - pure (fname, fullname) - isLib : String -> Maybe String isLib d = if isPrefixOf "lib" d @@ -119,6 +120,108 @@ mutual chezExtPrim i vs prim args = schExtCommon chezExtPrim i vs prim args +-- Reference label for keeping track of loaded external libraries +data Loaded : Type where + +cftySpec : FC -> CFType -> Core String +cftySpec fc CFUnit = pure "void" +cftySpec fc CFInt = pure "int" +cftySpec fc CFString = pure "string" +cftySpec fc CFDouble = pure "double" +cftySpec fc CFChar = pure "char" +cftySpec fc CFPtr = pure "void*" +cftySpec fc (CFIORes t) = cftySpec fc t +cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ + " to foreign function")) + +cCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> (cfn : String) -> (clib : Maybe String) -> + List (Name, CFType) -> CFType -> Core (String, String) +cCall fc cfn mclib args ret + = do loaded <- get Loaded + lib <- maybe (pure "") + (\clib => + if clib `elem` loaded + then pure "" + else do (fname, fullname) <- locate clib + put Loaded (clib :: loaded) + pure $ "(load-shared-object \"" + ++ escapeQuotes fullname + ++ "\")\n") + mclib + argTypes <- traverse (\a => do s <- cftySpec fc (snd a) + pure (fst a, s)) args + retType <- cftySpec fc ret + let call = "((foreign-procedure #f " ++ show cfn ++ " (" + ++ showSep " " (map snd argTypes) ++ ") " ++ retType ++ ") " + ++ showSep " " (map (schName . fst) argTypes) ++ ")" + + pure (lib, case ret of + CFIORes _ => handleRet retType call + _ => call) + +schemeCall : FC -> (sfn : String) -> + List Name -> CFType -> Core String +schemeCall fc sfn argns ret + = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in + case ret of + CFIORes _ => pure $ mkWorld call + _ => pure call + +-- Use a calling convention to compile a foreign def. +-- Returns any preamble needed for loading libraries, and the body of the +-- function call. +useCC : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String) +useCC fc [] args ret + = throw (GenericMsg fc "No recognised foreign calling convention") +useCC fc (cc :: ccs) args ret + = case parseCC cc of + Nothing => useCC fc ccs args ret + Just ("scheme", [sfn]) => + do body <- schemeCall fc sfn (map fst args) ret + pure ("", body) + Just ("C", [cfn]) => cCall fc cfn Nothing args ret + Just ("C", [cfn, clib]) => cCall fc cfn (Just clib) args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn (Just clib) args ret + _ => useCC fc ccs args ret + +-- For every foreign arg type, return a name, and whether to pass it to the +-- foreign call (we don't pass '%World') +mkArgs : Int -> List CFType -> List (Name, Bool) +mkArgs i [] = [] +mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs +mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs + +schFgnDef : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> Name -> CDef -> Core (String, String) +schFgnDef fc n (MkForeign cs args ret) + = do let argns = mkArgs 0 args + let allargns = map fst argns + let useargns = map fst (filter snd argns) + (load, body) <- useCC fc cs (zip useargns args) ret + defs <- get Ctxt + pure (load, + "(define " ++ schName !(full (gamma defs) n) ++ + " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++ + body ++ "))\n") +schFgnDef _ _ _ = pure ("", "") + +getFgnCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + Name -> Core (String, String) +getFgnCall n + = do defs <- get Ctxt + case !(lookupCtxtExact n (gamma defs)) of + Nothing => throw (InternalError ("Compiling undefined name " ++ show n)) + Just def => case compexpr def of + Nothing => + throw (InternalError ("No compiled definition for " ++ show n)) + Just d => schFgnDef (location def) n d + ||| Compile a TT expression to Chez Scheme compileToSS : Ref Ctxt Defs -> ClosedTerm -> (outfile : String) -> Core () @@ -127,13 +230,17 @@ compileToSS c tm outfile libs <- findLibs ds (ns, tags) <- findUsedNames tm defs <- get Ctxt + l <- newRef {t = List String} Loaded [] + fgndefs <- traverse getFgnCall ns compdefs <- traverse (getScheme chezExtPrim defs) ns - let code = concat compdefs + let code = concat (map snd fgndefs) ++ concat compdefs main <- schExp chezExtPrim 0 [] !(compileExp tags tm) chez <- coreLift findChez support <- readDataFile "chez/support.ss" let scm = schHeader chez (map snd libs) ++ - support ++ code ++ main ++ schFooter + support ++ code ++ + concat (map fst fgndefs) ++ + main ++ schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) coreLift $ chmod outfile 0o755 diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 5b6b94c..48a364b 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -21,6 +21,7 @@ schString s = concatMap okchar (unpack s) then cast c else "C-" ++ show (cast {to=Int} c) +export schName : Name -> String schName (NS ns n) = showSep "-" ns ++ "-" ++ schName n schName (UN n) = schString n @@ -48,6 +49,7 @@ extendSVars {ns} xs vs = extSVars' (cast (length ns)) xs vs extSVars' i [] vs = vs extSVars' i (x :: xs) vs = schName (MN "v" i) :: extSVars' (i + 1) xs vs +export initSVars : (xs : List Name) -> SVars xs initSVars xs = rewrite sym (appendNilRightNeutral xs) in extendSVars xs [] @@ -215,6 +217,12 @@ schConstant WorldType = "#t" schCaseDef : Maybe String -> String schCaseDef Nothing = "" schCaseDef (Just tm) = "(else " ++ tm ++ ")" + +export +schArglist : SVars ns -> String +schArglist [] = "" +schArglist [x] = x +schArglist (x :: xs) = x ++ " " ++ schArglist xs parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CExp vars) -> Core String) mutual @@ -338,11 +346,6 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx = throw (InternalError ("Badly formed external primitive " ++ show prim ++ " " ++ show args)) - schArglist : SVars ns -> String - schArglist [] = "" - schArglist [x] = x - schArglist (x :: xs) = x ++ " " ++ schArglist xs - schDef : {auto c : Ref Ctxt Defs} -> Name -> CDef -> Core String schDef n (MkFun args exp) @@ -351,6 +354,7 @@ parameters (schExtPrim : {vars : _} -> Int -> SVars vars -> ExtPrim -> List (CEx ++ !(schExp 0 vs exp) ++ "))\n" schDef n (MkError exp) = pure $ "(define (" ++ schName !(getFullName n) ++ " . any-args) " ++ !(schExp 0 [] exp) ++ ")\n" + schDef n (MkForeign _ _ _) = pure "" -- compiled by specific back end schDef n (MkCon t a) = pure "" -- Nothing to compile here -- Convert the name to scheme code diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 8b9acbe..5b7714a 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -27,7 +27,7 @@ import Data.Buffer -- TTC files can only be compatible if the version number is the same export ttcVersion : Int -ttcVersion = 6 +ttcVersion = 7 export checkTTCVersion : Int -> Int -> Core () diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index b0d7bcd..1296837 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -8,7 +8,7 @@ import Core.TT import Data.Vect -%default total +%default covering mutual ||| CExp - an expression ready for compiling. @@ -53,12 +53,30 @@ mutual data CConstAlt : List Name -> Type where MkConstAlt : Constant -> CExp vars -> CConstAlt vars +-- Argument type descriptors for foreign function calls +public export +data CFType : Type where + CFUnit : CFType + CFInt : CFType + CFString : CFType + CFDouble : CFType + CFChar : CFType + CFPtr : CFType + CFWorld : CFType + CFIORes : CFType -> CFType + CFUser : Name -> List CFType -> CFType + public export data CDef : Type where -- Normal function definition MkFun : (args : List Name) -> CExp args -> CDef -- Constructor MkCon : (tag : Int) -> (arity : Nat) -> CDef + -- Foreign definition + MkForeign : (ccs : List String) -> + (fargs : List CFType) -> + CFType -> + CDef -- A function which will fail at runtime (usually due to being a hole) so needs -- to run, discarding arguments, no matter how many arguments are passed MkError : CExp [] -> CDef @@ -99,10 +117,25 @@ mutual show (MkConstAlt x exp) = "(%constcase " ++ show x ++ " " ++ show exp ++ ")" +export +Show CFType where + show CFUnit = "Unit" + show CFInt = "Int" + show CFString = "String" + show CFDouble = "Double" + show CFChar = "Char" + show CFPtr = "Ptr" + show CFWorld = "%World" + show (CFIORes t) = "IORes " ++ show t + show (CFUser n args) = show n ++ " " ++ show args + export Show CDef where show (MkFun args exp) = show args ++ ": " ++ show exp show (MkCon tag arity) = "Constructor tag " ++ show tag ++ " arity " ++ show arity + show (MkForeign ccs args ret) + = "Foreign call " ++ show ccs ++ " " ++ + show args ++ " -> " ++ show ret show (MkError exp) = "Error: " ++ show exp mutual diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 5ab2578..92cf952 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -34,6 +34,10 @@ data Def : Type where -- find size changes in termination checking Def -- Ordinary function definition ExternDef : (arity : Nat) -> Def + ForeignDef : (arity : Nat) -> + List String -> -- supported calling conventions, + -- e.g "C:printf,libc,stdlib.h", "scheme:display", ... + Def Builtin : {arity : Nat} -> PrimFn arity -> Def DCon : (tag : Int) -> (arity : Nat) -> Def -- data constructor TCon : (tag : Int) -> (arity : Nat) -> @@ -65,7 +69,9 @@ Show Def where = "TyCon " ++ show t ++ " " ++ show a ++ " params: " ++ show ps ++ " constructors: " ++ show cons ++ " mutual with: " ++ show ms - show (ExternDef arity) = "" + show (ExternDef arity) = "" + show (ForeignDef a cs) = "" show (Builtin {arity} _) = "" show (Hole _ p) = "Hole" ++ if p then " [impl]" else "" show (BySearch c depth def) = "Search in " ++ show def diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index c0ee3a5..9e715d4 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -638,20 +638,48 @@ mutual pure (MkConstAlt c sc) export - TTC CDef where - toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr - toBuf b (MkCon t arity) = do tag 1; toBuf b t; toBuf b arity - toBuf b (MkError cexpr) = do tag 2; toBuf b cexpr +TTC CFType where + toBuf b CFUnit = tag 0 + toBuf b CFInt = tag 1 + toBuf b CFString = tag 2 + toBuf b CFDouble = tag 3 + toBuf b CFChar = tag 4 + toBuf b CFPtr = tag 5 + toBuf b CFWorld = tag 6 + toBuf b (CFIORes t) = do tag 7; toBuf b t + toBuf b (CFUser n a) = do tag 8; toBuf b n; toBuf b a - fromBuf b - = case !getTag of - 0 => do args <- fromBuf b; cexpr <- fromBuf b - pure (MkFun args cexpr) - 1 => do t <- fromBuf b; arity <- fromBuf b - pure (MkCon t arity) - 2 => do cexpr <- fromBuf b - pure (MkError cexpr) - _ => corrupt "CDef" + fromBuf b + = case !getTag of + 0 => pure CFUnit + 1 => pure CFInt + 2 => pure CFString + 3 => pure CFDouble + 4 => pure CFChar + 5 => pure CFPtr + 6 => pure CFWorld + 7 => do t <- fromBuf b; pure (CFIORes t) + 8 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a) + _ => corrupt "CFType" + +export +TTC CDef where + toBuf b (MkFun args cexpr) = do tag 0; toBuf b args; toBuf b cexpr + toBuf b (MkCon t arity) = do tag 1; toBuf b t; toBuf b arity + toBuf b (MkForeign cs args ret) = do tag 2; toBuf b cs; toBuf b args; toBuf b ret + toBuf b (MkError cexpr) = do tag 3; toBuf b cexpr + + fromBuf b + = case !getTag of + 0 => do args <- fromBuf b; cexpr <- fromBuf b + pure (MkFun args cexpr) + 1 => do t <- fromBuf b; arity <- fromBuf b + pure (MkCon t arity) + 2 => do cs <- fromBuf b; args <- fromBuf b; ret <- fromBuf b + pure (MkForeign cs args ret) + 3 => do cexpr <- fromBuf b + pure (MkError cexpr) + _ => corrupt "CDef" export TTC CG where @@ -708,19 +736,21 @@ TTC Def where = do tag 1; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats toBuf b (ExternDef a) = do tag 2; toBuf b a + toBuf b (ForeignDef a cs) + = do tag 3; toBuf b a; toBuf b cs toBuf b (Builtin a) = throw (InternalError "Trying to serialise a Builtin") - toBuf b (DCon t arity) = do tag 3; toBuf b t; toBuf b arity + toBuf b (DCon t arity) = do tag 4; toBuf b t; toBuf b arity toBuf b (TCon t arity parampos detpos ms datacons) - = do tag 4; toBuf b t; toBuf b arity; toBuf b parampos + = do tag 5; toBuf b t; toBuf b arity; toBuf b parampos toBuf b detpos; toBuf b ms; toBuf b datacons toBuf b (Hole locs p) - = do tag 5; toBuf b locs; toBuf b p + = do tag 6; toBuf b locs; toBuf b p toBuf b (BySearch c depth def) - = do tag 6; toBuf b c; toBuf b depth; toBuf b def - toBuf b (Guess guess constraints) = do tag 7; toBuf b guess; toBuf b constraints - toBuf b ImpBind = tag 8 - toBuf b Delayed = tag 9 + = do tag 7; toBuf b c; toBuf b depth; toBuf b def + toBuf b (Guess guess constraints) = do tag 8; toBuf b guess; toBuf b constraints + toBuf b ImpBind = tag 9 + toBuf b Delayed = tag 10 fromBuf b = case !getTag of @@ -732,22 +762,25 @@ TTC Def where pure (PMDef False args ct rt pats) 2 => do a <- fromBuf b pure (ExternDef a) - 3 => do t <- fromBuf b; a <- fromBuf b - pure (DCon t a) + 3 => do a <- fromBuf b + cs <- fromBuf b + pure (ForeignDef a cs) 4 => do t <- fromBuf b; a <- fromBuf b + pure (DCon t a) + 5 => do t <- fromBuf b; a <- fromBuf b ps <- fromBuf b; dets <- fromBuf b; ms <- fromBuf b; cs <- fromBuf b pure (TCon t a ps dets ms cs) - 5 => do l <- fromBuf b + 6 => do l <- fromBuf b p <- fromBuf b pure (Hole l p) - 6 => do c <- fromBuf b; depth <- fromBuf b + 7 => do c <- fromBuf b; depth <- fromBuf b def <- fromBuf b pure (BySearch c depth def) - 7 => do g <- fromBuf b; cs <- fromBuf b + 8 => do g <- fromBuf b; cs <- fromBuf b pure (Guess g cs) - 8 => pure ImpBind - 9 => pure Context.Delayed + 9 => pure ImpBind + 10 => pure Context.Delayed _ => corrupt "Def" TTC TotalReq where diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 6079e47..25cb3c1 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1024,6 +1024,9 @@ fnDirectOpt pure Inline <|> do exactIdent "extern" pure ExternFn + <|> do exactIdent "foreign" + cs <- many strLit + pure (ForeignFn cs) visOpt : Rule (Either Visibility FnOpt) visOpt diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 17f611c..d0376be 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -17,6 +17,8 @@ import TTImp.TTImp import Data.NameMap +%default covering + getRetTy : Defs -> NF [] -> Core Name getRetTy defs (NBind fc _ (Pi _ _ _) sc) = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc))) @@ -39,6 +41,8 @@ processFnOpt fc ndef (GlobalHint a) = addGlobalHint ndef a processFnOpt fc ndef ExternFn = setFlag fc ndef Inline -- if externally defined, inline when compiling +processFnOpt fc ndef (ForeignFn _) + = setFlag fc ndef Inline -- if externally defined, inline when compiling processFnOpt fc ndef Invertible = setFlag fc ndef Invertible processFnOpt fc ndef Total @@ -48,6 +52,25 @@ processFnOpt fc ndef Covering processFnOpt fc ndef PartialOK = setFlag fc ndef (SetTotal PartialOK) +-- If it's declared as externally defined, set the definition to +-- ExternFn , where the arity is assumed to be fixed (i.e. +-- not dependent on any of the arguments) +-- Similarly set foreign definitions. Possibly combine these? +initDef : {auto c : Ref Ctxt Defs} -> + Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def +initDef n env ty [] + = do addUserHole n + pure None +initDef n env ty (ExternFn :: opts) + = do defs <- get Ctxt + a <- getArity defs env ty + pure (ExternDef a) +initDef n env ty (ForeignFn cs :: opts) + = do defs <- get Ctxt + a <- getArity defs env ty + pure (ForeignDef a cs) +initDef n env ty (_ :: opts) = initDef n env ty opts + export processType : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -76,16 +99,8 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw) (gType fc) logTermNF 5 ("Type of " ++ show n) [] (abstractEnvType tfc env ty) -- TODO: Check name visibility - -- If it's declared as externally defined, set the definition to - -- ExternFn , where the arity is assumed to be fixed (i.e. - -- not dependent on any of the arguments) - def <- if ExternFn `elem` opts - then do defs <- get Ctxt - a <- getArity defs env ty - pure (ExternDef a) - else do addUserHole n - pure None + def <- initDef n env ty opts addDef (Resolved idx) (newDef fc n rig vars (abstractEnvType tfc env ty) vis def) -- Flag it as checked, because we're going to check the clauses -- from the top level. diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 821dfed..e80e2b0 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -163,6 +163,8 @@ mutual -- Flag means to use as a default if all else fails GlobalHint : Bool -> FnOpt ExternFn : FnOpt + -- Defined externally, list calling conventions + ForeignFn : List String -> FnOpt -- assume safe to cancel arguments in unification Invertible : FnOpt Total : FnOpt @@ -175,6 +177,7 @@ mutual show (Hint t) = "%hint " ++ show t show (GlobalHint t) = "%globalhint " ++ show t show ExternFn = "%extern" + show (ForeignFn cs) = "%foreign " ++ showSep " " (map show cs) show Invertible = "%invertible" show Total = "total" show Covering = "covering" @@ -186,6 +189,7 @@ mutual (Hint x) == (Hint y) = x == y (GlobalHint x) == (GlobalHint y) = x == y ExternFn == ExternFn = True + (ForeignFn xs) == (ForeignFn ys) = xs == ys Invertible == Invertible = True Total == Total = True Covering == Covering = True @@ -789,10 +793,11 @@ mutual toBuf b (Hint t) = do tag 1; toBuf b t toBuf b (GlobalHint t) = do tag 2; toBuf b t toBuf b ExternFn = tag 3 - toBuf b Invertible = tag 4 - toBuf b Total = tag 5 - toBuf b Covering = tag 6 - toBuf b PartialOK = tag 7 + toBuf b (ForeignFn cs) = do tag 4; toBuf b cs + toBuf b Invertible = tag 5 + toBuf b Total = tag 6 + toBuf b Covering = tag 7 + toBuf b PartialOK = tag 8 fromBuf b = case !getTag of @@ -800,10 +805,11 @@ mutual 1 => do t <- fromBuf b; pure (Hint t) 2 => do t <- fromBuf b; pure (GlobalHint t) 3 => pure ExternFn - 4 => pure Invertible - 5 => pure Total - 6 => pure Covering - 7 => pure PartialOK + 4 => do cs <- fromBuf b; pure (ForeignFn cs) + 5 => pure Invertible + 6 => pure Total + 7 => pure Covering + 8 => pure PartialOK _ => corrupt "FnOpt" export diff --git a/support/chez/support.ss b/support/chez/support.ss index 3633696..d3f7cfa 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -45,6 +45,7 @@ (define blodwen-error-quit (lambda (msg) (display msg) + (newline) (exit 1))) ;; Buffers diff --git a/support/chicken/support.scm b/support/chicken/support.scm index b7599fa..e26e1e5 100644 --- a/support/chicken/support.scm +++ b/support/chicken/support.scm @@ -45,6 +45,7 @@ (define blodwen-error-quit (lambda (msg) (display msg) + (newline) (exit 1))) ;; Files: Much of the following adapted from idris-chez, thanks to Niklas diff --git a/support/racket/support.rkt b/support/racket/support.rkt index 50087af..5150006 100644 --- a/support/racket/support.rkt +++ b/support/racket/support.rkt @@ -45,6 +45,7 @@ (define blodwen-error-quit (lambda (msg) (display msg) + (newline) (exit 1))) ;; Files : Much of the following adapted from idris-chez, thanks to Niklas From 25bbaf7d741aee20ce79475254e3725ac4a06291 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 3 Sep 2019 14:37:16 +0100 Subject: [PATCH 16/20] Add dynamic library extension In the Chez back end, if the library spec is a name and a version number, build an appropriate guess for the library file name based on the system extension. --- src/Compiler/Common.idr | 9 +++ src/Compiler/Scheme/Chez.idr | 21 ++++++- src/Compiler/Scheme/Racket.idr | 112 ++++++++++++++++++++++++++++++++- src/Core/CompileExpr.idr | 2 +- 4 files changed, 138 insertions(+), 6 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index c68e9e6..69fd9fd 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -8,6 +8,8 @@ import Core.TT import Data.NameMap +import System.Info + %include C "sys/stat.h" ||| Generic interface to some code generator @@ -144,3 +146,10 @@ parseCC str = case span (/= ',') str of (opt, "") => [opt] (opt, rest) => opt :: getOpts (assert_total (strTail rest)) + +export +dylib_suffix : String +dylib_suffix + = cond [(os `elem` ["windows", "mingw32", "cygwin32"], "dll"), + (os == "darwin", "dylib")] + "so" diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index fe303e2..d2ade8f 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -30,11 +30,26 @@ findChez Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] maybe (pure "/usr/bin/env scheme") pure e - + locate : {auto c : Ref Ctxt Defs} -> String -> Core (String, String) -locate fname - = do fullname <- catch (findLibraryFile fname) +locate libspec + = do -- Attempt to turn libspec into an appropriate filename for the system + let fname + = case words libspec of + [] => "" + [fn] => if '.' `elem` unpack fn + then fn -- full filename given + else -- add system extension + fn ++ "." ++ dylib_suffix + (fn :: ver :: _) => + -- library and version givenm but don't add the version + -- on windows systems + if dylib_suffix == "dll" + then fn ++ ".dll" + else fn ++ "." ++ dylib_suffix ++ "." ++ ver + + fullname <- catch (findLibraryFile fname) (\err => -- assume a system library so not -- in our library path pure fname) diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 0fec850..30fbf37 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -43,16 +43,124 @@ mutual racketPrim i vs prim args = schExtCommon racketPrim i vs prim args +-- Reference label for keeping track of loaded external libraries +data Loaded : Type where + +cftySpec : FC -> CFType -> Core String +cftySpec fc CFUnit = pure "void" +cftySpec fc CFInt = pure "int" +cftySpec fc CFString = pure "string" +cftySpec fc CFDouble = pure "double" +cftySpec fc CFChar = pure "char" +cftySpec fc CFPtr = pure "void*" +cftySpec fc (CFIORes t) = cftySpec fc t +cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ + " to foreign function")) + +cCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> (cfn : String) -> (clib : Maybe String) -> + List (Name, CFType) -> CFType -> Core (String, String) +cCall fc cfn mclib args ret + = throw (GenericMsg fc "Racket back end can't talk to C yet") +-- do loaded <- get Loaded +-- lib <- maybe (pure "") +-- (\clib => +-- if clib `elem` loaded +-- then pure "" +-- else do (fname, fullname) <- locate clib +-- put Loaded (clib :: loaded) +-- pure $ "(load-shared-object \"" +-- ++ escapeQuotes fullname +-- ++ "\")\n") +-- mclib +-- argTypes <- traverse (\a => do s <- cftySpec fc (snd a) +-- pure (fst a, s)) args +-- retType <- cftySpec fc ret +-- let call = "((foreign-procedure #f " ++ show cfn ++ " (" +-- ++ showSep " " (map snd argTypes) ++ ") " ++ retType ++ ") " +-- ++ showSep " " (map (schName . fst) argTypes) ++ ")" +-- +-- pure (lib, case ret of +-- CFIORes _ => handleRet retType call +-- _ => call) + +schemeCall : FC -> (sfn : String) -> + List Name -> CFType -> Core String +schemeCall fc sfn argns ret + = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in + case ret of + CFIORes _ => pure $ mkWorld call + _ => pure call + +-- Use a calling convention to compile a foreign def. +-- Returns any preamble needed for loading libraries, and the body of the +-- function call. +useCC : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String) +useCC fc [] args ret + = throw (GenericMsg fc "No recognised foreign calling convention") +useCC fc (cc :: ccs) args ret + = case parseCC cc of + Nothing => useCC fc ccs args ret + Just ("scheme", [sfn]) => + do body <- schemeCall fc sfn (map fst args) ret + pure ("", body) + Just ("C", [cfn]) => cCall fc cfn Nothing args ret + Just ("C", [cfn, clib]) => cCall fc cfn (Just clib) args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn (Just clib) args ret + _ => useCC fc ccs args ret + +-- For every foreign arg type, return a name, and whether to pass it to the +-- foreign call (we don't pass '%World') +mkArgs : Int -> List CFType -> List (Name, Bool) +mkArgs i [] = [] +mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs +mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs + +schFgnDef : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + FC -> Name -> CDef -> Core (String, String) +schFgnDef fc n (MkForeign cs args ret) + = do let argns = mkArgs 0 args + let allargns = map fst argns + let useargns = map fst (filter snd argns) + (load, body) <- useCC fc cs (zip useargns args) ret + defs <- get Ctxt + pure (load, + "(define " ++ schName !(full (gamma defs) n) ++ + " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++ + body ++ "))\n") +schFgnDef _ _ _ = pure ("", "") + +getFgnCall : {auto c : Ref Ctxt Defs} -> + {auto l : Ref Loaded (List String)} -> + Name -> Core (String, String) +getFgnCall n + = do defs <- get Ctxt + case !(lookupCtxtExact n (gamma defs)) of + Nothing => throw (InternalError ("Compiling undefined name " ++ show n)) + Just def => case compexpr def of + Nothing => + throw (InternalError ("No compiled definition for " ++ show n)) + Just d => schFgnDef (location def) n d + compileToRKT : Ref Ctxt Defs -> ClosedTerm -> (outfile : String) -> Core () compileToRKT c tm outfile = do (ns, tags) <- findUsedNames tm defs <- get Ctxt + l <- newRef {t = List String} Loaded [] + fgndefs <- traverse getFgnCall ns compdefs <- traverse (getScheme racketPrim defs) ns - let code = concat compdefs + let code = concat (map snd fgndefs) ++ concat compdefs main <- schExp racketPrim 0 [] !(compileExp tags tm) support <- readDataFile "racket/support.rkt" - let scm = schHeader ++ support ++ code ++ "(void " ++ main ++ ")\n" ++ schFooter + let scm = schHeader ++ + support ++ code ++ + "(void " ++ main ++ ")\n" ++ + schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) coreLift $ chmod outfile 0o755 diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 1296837..98eb1c9 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -127,7 +127,7 @@ Show CFType where show CFPtr = "Ptr" show CFWorld = "%World" show (CFIORes t) = "IORes " ++ show t - show (CFUser n args) = show n ++ " " ++ show args + show (CFUser n args) = show n ++ " " ++ showSep " " (map show args) export Show CDef where From de0a097a40cbc99174968396ea5f201d2c521c30 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Tue, 3 Sep 2019 17:02:23 +0100 Subject: [PATCH 17/20] First attempt at a C FFI via Racket This aims to be consistent with the notation for the way the Chez->C FFI loads libraries. --- src/Compiler/Scheme/Chez.idr | 40 +++++++------ src/Compiler/Scheme/Racket.idr | 101 +++++++++++++++++++++------------ 2 files changed, 84 insertions(+), 57 deletions(-) diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index d2ade8f..a78a009 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -43,11 +43,13 @@ locate libspec else -- add system extension fn ++ "." ++ dylib_suffix (fn :: ver :: _) => - -- library and version givenm but don't add the version - -- on windows systems - if dylib_suffix == "dll" - then fn ++ ".dll" - else fn ++ "." ++ dylib_suffix ++ "." ++ ver + -- library and version given, build path name as + -- appropriate for the system + cond [(dylib_suffix == "dll", + fn ++ "-" ++ ver ++ ".dll"), + (dylib_suffix == "dylib", + fn ++ "." ++ ver ++ ".dylib")] + (fn ++ "." ++ dylib_suffix ++ "." ++ ver) fullname <- catch (findLibraryFile fname) (\err => -- assume a system library so not @@ -151,20 +153,17 @@ cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t + cCall : {auto c : Ref Ctxt Defs} -> {auto l : Ref Loaded (List String)} -> - FC -> (cfn : String) -> (clib : Maybe String) -> + FC -> (cfn : String) -> (clib : String) -> List (Name, CFType) -> CFType -> Core (String, String) -cCall fc cfn mclib args ret +cCall fc cfn clib args ret = do loaded <- get Loaded - lib <- maybe (pure "") - (\clib => - if clib `elem` loaded - then pure "" - else do (fname, fullname) <- locate clib - put Loaded (clib :: loaded) - pure $ "(load-shared-object \"" - ++ escapeQuotes fullname - ++ "\")\n") - mclib + lib <- if clib `elem` loaded + then pure "" + else do (fname, fullname) <- locate clib + put Loaded (clib :: loaded) + pure $ "(load-shared-object \"" + ++ escapeQuotes fullname + ++ "\")\n" argTypes <- traverse (\a => do s <- cftySpec fc (snd a) pure (fst a, s)) args retType <- cftySpec fc ret @@ -198,9 +197,8 @@ useCC fc (cc :: ccs) args ret Just ("scheme", [sfn]) => do body <- schemeCall fc sfn (map fst args) ret pure ("", body) - Just ("C", [cfn]) => cCall fc cfn Nothing args ret - Just ("C", [cfn, clib]) => cCall fc cfn (Just clib) args ret - Just ("C", [cfn, clib, chdr]) => cCall fc cfn (Just clib) args ret + Just ("C", [cfn, clib]) => cCall fc cfn clib args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn clib args ret _ => useCC fc ccs args ret -- For every foreign arg type, return a name, and whether to pass it to the @@ -245,7 +243,7 @@ compileToSS c tm outfile libs <- findLibs ds (ns, tags) <- findUsedNames tm defs <- get Ctxt - l <- newRef {t = List String} Loaded [] + l <- newRef {t = List String} Loaded ["libc", "libc 6"] fgndefs <- traverse getFgnCall ns compdefs <- traverse (getScheme chezExtPrim defs) ns let code = concat (map snd fgndefs) ++ concat compdefs diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 30fbf37..7ed7983 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -27,10 +27,12 @@ findRacket = pure "/usr/bin/env racket" findRacoExe : IO String findRacoExe = pure "raco exe" -schHeader : String -schHeader +schHeader : String -> String +schHeader libs = "#lang racket/base\n" ++ "(require racket/promise)\n" ++ -- for force/delay + "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C + libs ++ "(let ()\n" schFooter : String @@ -47,43 +49,71 @@ mutual data Loaded : Type where cftySpec : FC -> CFType -> Core String -cftySpec fc CFUnit = pure "void" -cftySpec fc CFInt = pure "int" -cftySpec fc CFString = pure "string" -cftySpec fc CFDouble = pure "double" -cftySpec fc CFChar = pure "char" -cftySpec fc CFPtr = pure "void*" +cftySpec fc CFUnit = pure "_void" +cftySpec fc CFInt = pure "_int" +cftySpec fc CFString = pure "_string/utf-8" +cftySpec fc CFDouble = pure "_double" +cftySpec fc CFChar = pure "_int8" +cftySpec fc CFPtr = pure "_pointer" cftySpec fc (CFIORes t) = cftySpec fc t cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++ " to foreign function")) +loadlib : String -> String -> String +loadlib libn ver + = "(define-ffi-definer define-" ++ libn ++ + " (ffi-lib \"" ++ libn ++ "\" " ++ ver ++ "))\n" + +getLibVers : String -> (String, String) +getLibVers libspec + = case words libspec of + [] => ("", "") + [fn] => case span (/='.') libspec of + (root, rest) => (root, "") + (fn :: vers) => + (fst (span (/='.') fn), + "'(" ++ showSep " " (map show vers) ++ " #f)" ) + +cToRkt : CFType -> String -> String +cToRkt CFChar op = "(integer->char " ++ op ++ ")" +cToRkt _ op = op + +rktToC : CFType -> String -> String +rktToC CFChar op = "(char->integer " ++ op ++ ")" +rktToC _ op = op + +handleRet : CFType -> String -> String +handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor 0 []) +handleRet ret op = mkWorld (cToRkt ret op) + +useArg : (Name, CFType) -> String +useArg (n, ty) + = rktToC ty (schName n) + cCall : {auto c : Ref Ctxt Defs} -> {auto l : Ref Loaded (List String)} -> - FC -> (cfn : String) -> (clib : Maybe String) -> + FC -> (cfn : String) -> (clib : String) -> List (Name, CFType) -> CFType -> Core (String, String) -cCall fc cfn mclib args ret - = throw (GenericMsg fc "Racket back end can't talk to C yet") --- do loaded <- get Loaded --- lib <- maybe (pure "") --- (\clib => --- if clib `elem` loaded --- then pure "" --- else do (fname, fullname) <- locate clib --- put Loaded (clib :: loaded) --- pure $ "(load-shared-object \"" --- ++ escapeQuotes fullname --- ++ "\")\n") --- mclib --- argTypes <- traverse (\a => do s <- cftySpec fc (snd a) --- pure (fst a, s)) args --- retType <- cftySpec fc ret --- let call = "((foreign-procedure #f " ++ show cfn ++ " (" --- ++ showSep " " (map snd argTypes) ++ ") " ++ retType ++ ") " --- ++ showSep " " (map (schName . fst) argTypes) ++ ")" --- --- pure (lib, case ret of --- CFIORes _ => handleRet retType call --- _ => call) +cCall fc cfn libspec args ret + = do loaded <- get Loaded + let (libn, vers) = getLibVers libspec + lib <- if libn `elem` loaded + then pure "" + else do put Loaded (libn :: loaded) + pure (loadlib libn vers) + + argTypes <- traverse (\a => do s <- cftySpec fc (snd a) + pure (a, s)) args + retType <- cftySpec fc ret + let cbind = "(define-" ++ libn ++ " " ++ cfn ++ + " (_fun " ++ showSep " " (map snd argTypes) ++ " -> " ++ + retType ++ "))\n" + let call = "(" ++ cfn ++ " " ++ + showSep " " (map (useArg . fst) argTypes) ++ ")" + + pure (lib ++ cbind, case ret of + CFIORes rt => handleRet rt call + _ => call) schemeCall : FC -> (sfn : String) -> List Name -> CFType -> Core String @@ -107,9 +137,8 @@ useCC fc (cc :: ccs) args ret Just ("scheme", [sfn]) => do body <- schemeCall fc sfn (map fst args) ret pure ("", body) - Just ("C", [cfn]) => cCall fc cfn Nothing args ret - Just ("C", [cfn, clib]) => cCall fc cfn (Just clib) args ret - Just ("C", [cfn, clib, chdr]) => cCall fc cfn (Just clib) args ret + Just ("C", [cfn, clib]) => cCall fc cfn clib args ret + Just ("C", [cfn, clib, chdr]) => cCall fc cfn clib args ret _ => useCC fc ccs args ret -- For every foreign arg type, return a name, and whether to pass it to the @@ -157,7 +186,7 @@ compileToRKT c tm outfile let code = concat (map snd fgndefs) ++ concat compdefs main <- schExp racketPrim 0 [] !(compileExp tags tm) support <- readDataFile "racket/support.rkt" - let scm = schHeader ++ + let scm = schHeader (concat (map fst fgndefs)) ++ support ++ code ++ "(void " ++ main ++ ")\n" ++ schFooter From 68b0d648797c67bde81dade0e1a21c9ee31c755f Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 4 Sep 2019 10:25:45 +0100 Subject: [PATCH 18/20] Add parameterised pointer type For at least a bit of safety in foreign APIs. AnyPtr has the old Ptr behaviour. --- libs/base/Data/Buffer.idr | 4 ++-- libs/network/Network/Socket.idr | 6 +++--- libs/network/Network/Socket/Data.idr | 2 +- libs/network/Network/Socket/Raw.idr | 16 ++++++++-------- libs/prelude/PrimIO.idr | 9 ++++++++- src/Compiler/CompileExpr.idr | 4 ++++ src/Compiler/Scheme/Chez.idr | 5 ++++- 7 files changed, 30 insertions(+), 16 deletions(-) diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr index 30bf3c6..be1df78 100644 --- a/libs/base/Data/Buffer.idr +++ b/libs/base/Data/Buffer.idr @@ -4,12 +4,12 @@ import System.File export data Buffer : Type where - MkBuffer : Ptr -> (size : Int) -> (loc : Int) -> Buffer + MkBuffer : AnyPtr -> (size : Int) -> (loc : Int) -> Buffer export newBuffer : Int -> IO Buffer newBuffer size - = do buf <- schemeCall Ptr "blodwen-new-buffer" [size] + = do buf <- schemeCall AnyPtr "blodwen-new-buffer" [size] pure (MkBuffer buf size 0) export diff --git a/libs/network/Network/Socket.idr b/libs/network/Network/Socket.idr index e255f58..f058c09 100644 --- a/libs/network/Network/Socket.idr +++ b/libs/network/Network/Socket.idr @@ -85,7 +85,7 @@ accept sock = do -- We need a pointer to a sockaddr structure. This is then passed into -- idrnet_accept and populated. We can then query it for the SocketAddr and free it. - sockaddr_ptr <- cCall Ptr "idrnet_create_sockaddr" [] + sockaddr_ptr <- cCall AnyPtr "idrnet_create_sockaddr" [] accept_res <- cCall Int "idrnet_accept" [ descriptor sock, sockaddr_ptr ] if accept_res == (-1) @@ -128,7 +128,7 @@ recv : (sock : Socket) recv sock len = do -- Firstly make the request, get some kind of recv structure which -- contains the result of the recv and possibly the retrieved payload - recv_struct_ptr <- cCall Ptr "idrnet_recv" [ descriptor sock, len] + recv_struct_ptr <- cCall AnyPtr "idrnet_recv" [ descriptor sock, len] recv_res <- cCall Int "idrnet_get_recv_res" [ recv_struct_ptr ] if recv_res == (-1) @@ -202,7 +202,7 @@ recvFrom : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (UDPAddrInfo, String, ResultCode)) recvFrom sock bl = do - recv_ptr <- cCall Ptr "idrnet_recvfrom" + recv_ptr <- cCall AnyPtr "idrnet_recvfrom" [ descriptor sock, bl ] let recv_ptr' = RFPtr recv_ptr diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 70c4f1f..12dc008 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -63,7 +63,7 @@ getErrno : IO SocketError getErrno = cCall Int "idrnet_errno" [] export -nullPtr : Ptr -> IO Bool +nullPtr : AnyPtr -> IO Bool nullPtr p = cCall Bool "isNull" [p] -- -------------------------------------------------------------- [ Interfaces ] diff --git a/libs/network/Network/Socket/Raw.idr b/libs/network/Network/Socket/Raw.idr index 41515f3..6dc59b7 100644 --- a/libs/network/Network/Socket/Raw.idr +++ b/libs/network/Network/Socket/Raw.idr @@ -10,16 +10,16 @@ import public Network.Socket.Data -- ---------------------------------------------------------------- [ Pointers ] public export -data RecvStructPtr = RSPtr Ptr +data RecvStructPtr = RSPtr AnyPtr public export -data RecvfromStructPtr = RFPtr Ptr +data RecvfromStructPtr = RFPtr AnyPtr public export -data BufPtr = BPtr Ptr +data BufPtr = BPtr AnyPtr public export -data SockaddrPtr = SAPtr Ptr +data SockaddrPtr = SAPtr AnyPtr -- ---------------------------------------------------------- [ Socket Utilies ] @@ -35,7 +35,7 @@ sockaddr_free (SAPtr ptr) = cCall () "idrnet_free" [ptr] ||| ||| Used to allocate a mutable pointer to be given to the Recv functions. sock_alloc : ByteLength -> IO BufPtr -sock_alloc bl = map BPtr $ cCall Ptr "idrnet_malloc" [bl] +sock_alloc bl = map BPtr $ cCall AnyPtr "idrnet_malloc" [bl] ||| Retrieves the port the given socket is bound to export @@ -141,14 +141,14 @@ foreignGetRecvfromPayload (RFPtr p) = cCall String "idrnet_get_recvfrom_payload" export foreignGetRecvfromAddr : RecvfromStructPtr -> IO SocketAddress foreignGetRecvfromAddr (RFPtr p) = do - sockaddr_ptr <- map SAPtr $ cCall Ptr "idrnet_get_recvfrom_sockaddr" [p] + sockaddr_ptr <- map SAPtr $ cCall AnyPtr "idrnet_get_recvfrom_sockaddr" [p] getSockAddr sockaddr_ptr ||| Utility function to return sender's IPV4 port. export foreignGetRecvfromPort : RecvfromStructPtr -> IO Port foreignGetRecvfromPort (RFPtr p) = do - sockaddr_ptr <- cCall Ptr "idrnet_get_recvfrom_sockaddr" [p] + sockaddr_ptr <- cCall AnyPtr "idrnet_get_recvfrom_sockaddr" [p] port <- cCall Int "idrnet_sockaddr_ipv4_port" [sockaddr_ptr] pure port @@ -169,7 +169,7 @@ recvFromBuf : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (UDPAddrInfo, ResultCode)) recvFromBuf sock (BPtr ptr) bl = do - recv_ptr <- cCall Ptr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl] + recv_ptr <- cCall AnyPtr "idrnet_recvfrom_buf" [ descriptor sock, ptr, bl] let recv_ptr' = RFPtr recv_ptr diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 6c00710..b8411d5 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -28,8 +28,15 @@ PrimIO a = (1 x : %World) -> IORes a %extern prim__putStr : String -> (1 x : %World) -> IORes () %extern prim__getStr : (1 x : %World) -> IORes String +-- A pointer representing a given parameter type +-- The parameter is a phantom type, to help differentiate between +-- different pointer types public export -data Ptr : Type where +data Ptr : Type -> Type where + +-- A pointer to any type (representing a void* in foreign calls) +public export +data AnyPtr : Type where public export data ThreadID : Type where diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 2edcea3..63aaf44 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -276,10 +276,13 @@ mkArgList i (S k) data NArgs : Type where User : Name -> List (Closure []) -> NArgs NUnit : NArgs + NPtr : NArgs NIORes : Closure [] -> NArgs getNArgs : Name -> List (Closure []) -> NArgs getNArgs (NS _ (UN "IORes")) [arg] = NIORes arg +getNArgs (NS _ (UN "Ptr")) [arg] = NPtr +getNArgs (NS _ (UN "AnyPtr")) [] = NPtr getNArgs (NS _ (UN "Unit")) [] = NUnit getNArgs n args = User n args @@ -298,6 +301,7 @@ nfToCFType (NTCon _ n _ _ args) cargs <- traverse nfToCFType nargs pure (CFUser n cargs) NUnit => pure CFUnit + NPtr => pure CFPtr NIORes uarg => do narg <- evalClosure defs uarg carg <- nfToCFType narg diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index a78a009..99488c0 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -105,9 +105,12 @@ mutual tySpec (CCon fc (UN "String") _ []) = pure "string" tySpec (CCon fc (UN "Double") _ []) = pure "double" tySpec (CCon fc (UN "Char") _ []) = pure "char" + tySpec (CCon fc (NS _ n) _ [_]) + = cond [(n == UN "Ptr", pure "void*")] + (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) tySpec (CCon fc (NS _ n) _ []) = cond [(n == UN "Unit", pure "void"), - (n == UN "Ptr", pure "void*")] + (n == UN "AnyPtr", pure "void*")] (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function"))) tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function")) From 65db4fbf961cbdd36f10a9a75e7c3311b91f5585 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 4 Sep 2019 12:41:16 +0100 Subject: [PATCH 19/20] Put built ttcs in build/ttc, rather than build This is so that we can put other build artefacts (e.g. executables) in properly organised subdirectories of build, e.g. build/bin/chez, build/bin/js, etc. --- Makefile | 2 +- libs/network/Makefile | 1 - src/Core/Directory.idr | 6 +++--- src/Idris/Package.idr | 6 +++--- tests/ttimp/basic001/run | 2 +- tests/ttimp/basic003/run | 2 +- tests/ttimp/lazy001/run | 2 +- tests/ttimp/record001/run | 2 +- tests/ttimp/search002/run | 2 +- tests/ttimp/search003/run | 2 +- tests/ttimp/search004/run | 2 +- 11 files changed, 14 insertions(+), 15 deletions(-) diff --git a/Makefile b/Makefile index 5f7e72b..49adf74 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ PREFIX ?= ${HOME}/.idris2 IDRIS_VERSION := $(shell idris --version) VALID_IDRIS_VERSION_REGEXP = "1.3.2.*" -export IDRIS2_PATH = ${CURDIR}/libs/prelude/build:${CURDIR}/libs/base/build +export IDRIS2_PATH = ${CURDIR}/libs/prelude/build/ttc:${CURDIR}/libs/base/build/ttc export IDRIS2_DATA = ${CURDIR}/support -include custom.mk diff --git a/libs/network/Makefile b/libs/network/Makefile index b63547e..4e44a6d 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -31,7 +31,6 @@ LIBTARGET = $(LIBNAME).a TARGET=${HOME}/.idris2 build: $(DYLIBTARGET) $(IDRIS_SRCS) - @if ! [ -d build ]; then echo "creating 'build' directory"; mkdir build ; else echo "directory 'build' exists"; fi @if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi ${IDRIS2} --build network.ipkg diff --git a/src/Core/Directory.idr b/src/Core/Directory.idr index d27f370..767cc5e 100644 --- a/src/Core/Directory.idr +++ b/src/Core/Directory.idr @@ -81,7 +81,7 @@ nsToPath loc ns = do d <- getDirs let fnameBase = showSep (cast sep) (reverse ns) let fs = map (\p => p ++ cast sep ++ fnameBase ++ ".ttc") - (build_dir d :: extra_dirs d) + ((build_dir d ++ cast sep ++ "ttc") :: extra_dirs d) Just f <- firstAvailable fs | Nothing => pure (Left (ModuleNotFound loc ns)) pure (Right f) @@ -151,7 +151,7 @@ makeBuildDirectory ns [] => [] (n :: ns) => ns -- first item is file name let fname = showSep (cast sep) (reverse ndirs) - Right _ <- coreLift $ mkdirs (build_dir d :: reverse ndirs) + Right _ <- coreLift $ mkdirs (build_dir d :: "ttc" :: reverse ndirs) | Left err => throw (FileErr (bdir ++ cast sep ++ fname) err) pure () @@ -167,7 +167,7 @@ getTTCFileName inp ext let ns = pathToNS (working_dir d) inp let fname = showSep (cast sep) (reverse ns) ++ ext let bdir = build_dir d - pure $ bdir ++ cast sep ++ fname + pure $ bdir ++ cast sep ++ "ttc" ++ cast sep ++ fname -- Given a root executable name, return the name in the build directory export diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index dd8e529..6eab6ef 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -234,9 +234,9 @@ installFrom : {auto c : Ref Ctxt Defs} -> String -> String -> String -> List String -> Core () installFrom _ _ _ [] = pure () installFrom pname builddir destdir ns@(m :: dns) - = do let ttcfile = showSep "/" (reverse ns) - let ttcPath = builddir ++ dirSep ++ ttcfile ++ ".ttc" - let destPath = destdir ++ dirSep ++ showSep "/" (reverse dns) + = do let ttcfile = showSep dirSep (reverse ns) + let ttcPath = builddir ++ dirSep ++ "ttc" ++ dirSep ++ ttcfile ++ ".ttc" + let destPath = destdir ++ dirSep ++ showSep dirSep (reverse dns) let destFile = destdir ++ dirSep ++ ttcfile ++ ".ttc" Right _ <- coreLift $ mkdirs (reverse dns) | Left err => throw (FileErr pname err) diff --git a/tests/ttimp/basic001/run b/tests/ttimp/basic001/run index 16c00f5..04cc9c3 100755 --- a/tests/ttimp/basic001/run +++ b/tests/ttimp/basic001/run @@ -1,4 +1,4 @@ $1 --yaffle Interp.yaff < input -$1 --yaffle build/Interp.ttc < input +$1 --yaffle build/ttc/Interp.ttc < input rm -rf build diff --git a/tests/ttimp/basic003/run b/tests/ttimp/basic003/run index 349a2e8..9b22c83 100755 --- a/tests/ttimp/basic003/run +++ b/tests/ttimp/basic003/run @@ -1,4 +1,4 @@ $1 --yaffle Hole.yaff < input -$1 --yaffle build/Hole.ttc < input +$1 --yaffle build/ttc/Hole.ttc < input rm -rf build diff --git a/tests/ttimp/lazy001/run b/tests/ttimp/lazy001/run index 0ef2cc8..036a669 100755 --- a/tests/ttimp/lazy001/run +++ b/tests/ttimp/lazy001/run @@ -1,5 +1,5 @@ $1 --yaffle Lazy.yaff < input $1 --yaffle LazyInf.yaff < input -$1 --yaffle build/LazyInf.ttc < input +$1 --yaffle build/ttc/LazyInf.ttc < input rm -rf build diff --git a/tests/ttimp/record001/run b/tests/ttimp/record001/run index ac0007b..2811e75 100755 --- a/tests/ttimp/record001/run +++ b/tests/ttimp/record001/run @@ -1,4 +1,4 @@ $1 --yaffle Record.yaff < input -$1 --yaffle build/Record.ttc < input +$1 --yaffle build/ttc/Record.ttc < input rm -rf build diff --git a/tests/ttimp/search002/run b/tests/ttimp/search002/run index f51c121..9814e21 100755 --- a/tests/ttimp/search002/run +++ b/tests/ttimp/search002/run @@ -1,4 +1,4 @@ $1 --yaffle Auto.yaff < input -$1 --yaffle build/Auto.ttc < input +$1 --yaffle build/ttc/Auto.ttc < input rm -rf build diff --git a/tests/ttimp/search003/run b/tests/ttimp/search003/run index b5a5978..36c2588 100755 --- a/tests/ttimp/search003/run +++ b/tests/ttimp/search003/run @@ -1,4 +1,4 @@ $1 --yaffle FakeTC.yaff < input -$1 --yaffle build/FakeTC.ttc < input +$1 --yaffle build/ttc/FakeTC.ttc < input rm -rf build diff --git a/tests/ttimp/search004/run b/tests/ttimp/search004/run index 5ac4524..045b45c 100755 --- a/tests/ttimp/search004/run +++ b/tests/ttimp/search004/run @@ -1,4 +1,4 @@ $1 --yaffle Functor.yaff < input -$1 --yaffle build/Functor.ttc < input +$1 --yaffle build/ttc/Functor.ttc < input rm -rf build From e669140f9ad8d83f9d79043c6a250df2b65b3d31 Mon Sep 17 00:00:00 2001 From: Alex Gryzlov Date: Thu, 5 Sep 2019 03:21:43 +0300 Subject: [PATCH 20/20] code golfing --- src/Compiler/CompileExpr.idr | 88 +++++++++++++++---------------- src/Compiler/Scheme/Chez.idr | 25 ++++----- src/Compiler/Scheme/Chicken.idr | 4 -- src/Compiler/Scheme/Common.idr | 5 ++ src/Compiler/Scheme/Racket.idr | 4 -- src/Core/AutoSearch.idr | 2 +- src/Core/CompileExpr.idr | 36 ++++++------- src/Core/Core.idr | 92 ++++++++++++++++----------------- src/Core/Env.idr | 12 ++--- src/Core/InitPrimitives.idr | 3 +- src/Core/Name.idr | 6 +-- src/Core/TT.idr | 20 +++---- src/Idris/Desugar.idr | 18 +++---- src/Idris/REPLCommon.idr | 2 +- src/Parser/Lexer.idr | 4 +- src/TTImp/BindImplicits.idr | 3 -- src/TTImp/Utils.idr | 1 + 17 files changed, 155 insertions(+), 170 deletions(-) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 63aaf44..c2fb900 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -50,7 +50,7 @@ etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args)) mkApp (CExtPrim fc p args) args' = CExtPrim fc p (args ++ args') mkApp tm args = CApp (getFC tm) tm args etaExpand i (S k) exp args - = CLam (getFC exp) (MN "x" i) + = CLam (getFC exp) (MN "x" i) (etaExpand (i + 1) k (weaken exp) (MkVar First :: map weakenVar args)) @@ -106,7 +106,7 @@ natBranch (MkConAlt n _ _ _) = isNatCon n trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars) trySBranch n (MkConAlt (NS ["Prelude"] (UN "S")) _ [arg] sc) = let fc = getFC n in - Just (CLet fc arg (CApp fc (CRef fc (UN "prim__sub_Integer")) + Just (CLet fc arg (CApp fc (CRef fc (UN "prim__sub_Integer")) [n, CPrimVal fc (BI 1)]) sc) trySBranch _ _ = Nothing @@ -136,9 +136,9 @@ natHackTree t = t mutual toCExpTm : {auto c : Ref Ctxt Defs} -> NameTags -> Name -> Term vars -> Core (CExp vars) - toCExpTm tags n (Local fc _ _ prf) + toCExpTm tags n (Local fc _ _ prf) = pure $ CLocal fc prf - toCExpTm tags n (Ref fc (DataCon tag arity) fn) + toCExpTm tags n (Ref fc (DataCon tag arity) fn) = let tag' = case lookup fn tags of Just t => t _ => tag in @@ -149,9 +149,9 @@ mutual Just t => t _ => tag in pure $ CCon fc fn tag' [] - toCExpTm tags n (Ref fc _ fn) - = do full <- getFullName fn - -- ^ For readability of output code, and the Nat hack, + toCExpTm tags n (Ref fc _ fn) + = do full <- getFullName fn + -- ^ For readability of output code, and the Nat hack, pure $ CApp fc (CRef fc full) [] toCExpTm tags n (Meta fc mn i args) = pure $ CApp fc (CRef fc mn) !(traverse (toCExp tags n) args) @@ -161,12 +161,12 @@ mutual = pure $ CLet fc x (CErased fc) !(toCExp tags n sc) toCExpTm tags n (Bind fc x (Let _ val _) sc) = pure $ CLet fc x !(toCExp tags n val) !(toCExp tags n sc) - toCExpTm tags n (Bind fc x (Pi c e ty) sc) + toCExpTm tags n (Bind fc x (Pi c e ty) sc) = pure $ CCon fc (UN "->") 1 [!(toCExp tags n ty), CLam fc x !(toCExp tags n sc)] toCExpTm tags n (Bind fc x b tm) = pure $ CErased fc -- We'd expect this to have been dealt with in toCExp, but for completeness... - toCExpTm tags n (App fc tm arg) + toCExpTm tags n (App fc tm arg) = pure $ CApp fc !(toCExp tags n tm) [!(toCExp tags n arg)] -- This shouldn't be in terms any more, but here for completeness toCExpTm tags n (As _ _ p) = toCExpTm tags n p @@ -176,7 +176,7 @@ mutual = pure (CDelay fc !(toCExp tags n arg)) toCExpTm tags n (TForce fc arg) = pure (CForce fc !(toCExp tags n arg)) - toCExpTm tags n (PrimVal fc c) + toCExpTm tags n (PrimVal fc c) = let t = constTag c in if t == 0 then pure $ CPrimVal fc c @@ -197,7 +197,7 @@ mutual mutual conCases : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> List (CaseAlt vars) -> + NameTags -> Name -> List (CaseAlt vars) -> Core (List (CConAlt vars)) conCases tags n [] = pure [] conCases tags n (ConCase x tag args sc :: ns) @@ -205,60 +205,60 @@ mutual Just t => t _ => tag xn <- getFullName x - pure $ MkConAlt xn tag' args !(toCExpTree tags n sc) + pure $ MkConAlt xn tag' args !(toCExpTree tags n sc) :: !(conCases tags n ns) conCases tags n (_ :: ns) = conCases tags n ns constCases : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> List (CaseAlt vars) -> + NameTags -> Name -> List (CaseAlt vars) -> Core (List (CConstAlt vars)) constCases tags n [] = pure [] constCases tags n (ConstCase x sc :: ns) - = pure $ MkConstAlt x !(toCExpTree tags n sc) :: + = pure $ MkConstAlt x !(toCExpTree tags n sc) :: !(constCases tags n ns) constCases tags n (_ :: ns) = constCases tags n ns getDef : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> List (CaseAlt vars) -> + NameTags -> Name -> List (CaseAlt vars) -> Core (Maybe (CExp vars)) getDef tags n [] = pure Nothing - getDef tags n (DefaultCase sc :: ns) + getDef tags n (DefaultCase sc :: ns) = pure $ Just !(toCExpTree tags n sc) getDef tags n (_ :: ns) = getDef tags n ns toCExpTree : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> CaseTree vars -> + NameTags -> Name -> CaseTree vars -> Core (CExp vars) toCExpTree tags n alts@(Case _ x scTy (DelayCase ty arg sc :: rest)) = let fc = getLoc scTy in - pure $ + pure $ CLet fc arg (CForce fc (CLocal (getLoc scTy) x)) $ CLet fc ty (CErased fc) !(toCExpTree tags n sc) toCExpTree tags n alts = toCExpTree' tags n alts toCExpTree' : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> CaseTree vars -> + NameTags -> Name -> CaseTree vars -> Core (CExp vars) - toCExpTree' tags n (Case _ x scTy alts@(ConCase _ _ _ _ :: _)) + toCExpTree' tags n (Case _ x scTy alts@(ConCase _ _ _ _ :: _)) = let fc = getLoc scTy in - pure $ natHackTree - (CConCase fc (CLocal fc x) !(conCases tags n alts) + pure $ natHackTree + (CConCase fc (CLocal fc x) !(conCases tags n alts) !(getDef tags n alts)) toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _)) = throw (InternalError "Unexpected DelayCase") - toCExpTree' tags n (Case _ x scTy alts@(ConstCase _ _ :: _)) + toCExpTree' tags n (Case _ x scTy alts@(ConstCase _ _ :: _)) = let fc = getLoc scTy in - pure $ CConstCase fc (CLocal fc x) + pure $ CConstCase fc (CLocal fc x) !(constCases tags n alts) !(getDef tags n alts) - toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _)) + toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _)) = toCExpTree tags n sc - toCExpTree' tags n (Case _ x scTy []) + toCExpTree' tags n (Case _ x scTy []) = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n toCExpTree' tags n (STerm tm) = toCExp tags n tm - toCExpTree' tags n (Unmatched msg) - = pure $ CCrash emptyFC msg - toCExpTree' tags n Impossible + toCExpTree' tags n (Unmatched msg) + = pure $ CCrash emptyFC msg + toCExpTree' tags n Impossible = pure $ CCrash emptyFC ("Impossible case encountered in " ++ show n) -- Need this for ensuring that argument list matches up to operator arity for @@ -288,11 +288,11 @@ getNArgs n args = User n args nfToCFType : {auto c : Ref Ctxt Defs} -> NF [] -> Core CFType -nfToCFType (NPrimVal _ IntType) = pure CFInt +nfToCFType (NPrimVal _ IntType) = pure CFInt nfToCFType (NPrimVal _ StringType) = pure CFString nfToCFType (NPrimVal _ DoubleType) = pure CFDouble nfToCFType (NPrimVal _ CharType) = pure CFChar -nfToCFType (NPrimVal _ WorldType) = pure CFWorld +nfToCFType (NPrimVal _ WorldType) = pure CFWorld nfToCFType (NTCon _ n _ _ args) = do defs <- get Ctxt case getNArgs !(toFullNames n) args of @@ -319,8 +319,8 @@ getCFTypes args (NBind fc _ (Pi _ _ ty) sc) getCFTypes args t = pure (reverse args, !(nfToCFType t)) -toCDef : {auto c : Ref Ctxt Defs} -> - NameTags -> Name -> ClosedTerm -> Def -> +toCDef : {auto c : Ref Ctxt Defs} -> + NameTags -> Name -> ClosedTerm -> Def -> Core CDef toCDef tags n ty None = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n)) @@ -350,31 +350,27 @@ toCDef tags n ty (Builtin {arity} op) getVars : ArgList k ns -> Vect k (Var ns) getVars NoArgs = [] getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest) -toCDef tags n ty (DCon tag arity) - = case lookup n tags of - Just t => pure $ MkCon t arity - _ => pure $ MkCon tag arity -toCDef tags n ty (TCon tag arity _ _ _ _) - = case lookup n tags of - Just t => pure $ MkCon t arity - _ => pure $ MkCon tag arity +toCDef tags n _ (DCon tag arity) + = pure $ MkCon (fromMaybe tag $ lookup n tags) arity +toCDef tags n _ (TCon tag arity _ _ _ _) + = pure $ MkCon (fromMaybe tag $ lookup n tags) arity -- We do want to be able to compile these, but also report an error at run time -- (and, TODO: warn at compile time) toCDef tags n ty (Hole _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ + = pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++ show !(getFullName n)) toCDef tags n ty (Guess _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ + = pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++ show !(getFullName n)) toCDef tags n ty (BySearch _ _ _) - = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ + = pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++ show !(getFullName n)) toCDef tags n ty def - = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ + = pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++ show (!(getFullName n), def)) export -compileExp : {auto c : Ref Ctxt Defs} -> +compileExp : {auto c : Ref Ctxt Defs} -> NameTags -> ClosedTerm -> Core (CExp []) compileExp tags tm = toCExp tags (UN "main") tm diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 99488c0..49083ae 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -18,10 +18,6 @@ import System.Info %default covering -firstExists : List String -> IO (Maybe String) -firstExists [] = pure Nothing -firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs - findChez : IO String findChez = do env <- getEnv "CHEZ" @@ -29,7 +25,7 @@ findChez Just n => pure n Nothing => do e <- firstExists [p ++ x | p <- ["/usr/bin/", "/usr/local/bin/"], x <- ["scheme", "chez", "chezscheme9.5"]] - maybe (pure "/usr/bin/env scheme") pure e + pure $ fromMaybe "/usr/bin/env scheme" e locate : {auto c : Ref Ctxt Defs} -> String -> Core (String, String) @@ -42,15 +38,15 @@ locate libspec then fn -- full filename given else -- add system extension fn ++ "." ++ dylib_suffix - (fn :: ver :: _) => + (fn :: ver :: _) => -- library and version given, build path name as -- appropriate for the system - cond [(dylib_suffix == "dll", - fn ++ "-" ++ ver ++ ".dll"), + cond [(dylib_suffix == "dll", + fn ++ "-" ++ ver ++ ".dll"), (dylib_suffix == "dylib", fn ++ "." ++ ver ++ ".dylib")] (fn ++ "." ++ dylib_suffix ++ "." ++ ver) - + fullname <- catch (findLibraryFile fname) (\err => -- assume a system library so not -- in our library path @@ -164,7 +160,7 @@ cCall fc cfn clib args ret then pure "" else do (fname, fullname) <- locate clib put Loaded (clib :: loaded) - pure $ "(load-shared-object \"" + pure $ "(load-shared-object \"" ++ escapeQuotes fullname ++ "\")\n" argTypes <- traverse (\a => do s <- cftySpec fc (snd a) @@ -197,7 +193,7 @@ useCC fc [] args ret useCC fc (cc :: ccs) args ret = case parseCC cc of Nothing => useCC fc ccs args ret - Just ("scheme", [sfn]) => + Just ("scheme", [sfn]) => do body <- schemeCall fc sfn (map fst args) ret pure ("", body) Just ("C", [cfn, clib]) => cCall fc cfn clib args ret @@ -214,7 +210,7 @@ mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs schFgnDef : {auto c : Ref Ctxt Defs} -> {auto l : Ref Loaded (List String)} -> FC -> Name -> CDef -> Core (String, String) -schFgnDef fc n (MkForeign cs args ret) +schFgnDef fc n (MkForeign cs args ret) = do let argns = mkArgs 0 args let allargns = map fst argns let useargns = map fst (filter snd argns) @@ -253,8 +249,8 @@ compileToSS c tm outfile main <- schExp chezExtPrim 0 [] !(compileExp tags tm) chez <- coreLift findChez support <- readDataFile "chez/support.ss" - let scm = schHeader chez (map snd libs) ++ - support ++ code ++ + let scm = schHeader chez (map snd libs) ++ + support ++ code ++ concat (map fst fgndefs) ++ main ++ schFooter Right () <- coreLift $ writeFile outfile scm @@ -300,4 +296,3 @@ executeExpr c tm export codegenChez : Codegen codegenChez = MkCG compileExpr executeExpr - diff --git a/src/Compiler/Scheme/Chicken.idr b/src/Compiler/Scheme/Chicken.idr index dbbcf04..2ae43d6 100644 --- a/src/Compiler/Scheme/Chicken.idr +++ b/src/Compiler/Scheme/Chicken.idr @@ -18,10 +18,6 @@ import System.Info %default covering -firstExists : List String -> IO (Maybe String) -firstExists [] = pure Nothing -firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs - findCSI : IO String findCSI = pure "/usr/bin/env csi" diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index 48a364b..a49ac26 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -13,6 +13,11 @@ import Data.Vect %default covering +export +firstExists : List String -> IO (Maybe String) +firstExists [] = pure Nothing +firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs + schString : String -> String schString s = concatMap okchar (unpack s) where diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 7ed7983..5616cf8 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -17,10 +17,6 @@ import System.Info %default covering -firstExists : List String -> IO (Maybe String) -firstExists [] = pure Nothing -firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs - findRacket : IO String findRacket = pure "/usr/bin/env racket" diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index 80f22f3..b81ab1b 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -498,7 +498,7 @@ searchType {vars} fc rigc defaults trying depth def checkdets top env target logNF 5 "For target" env nty searchNames fc rigc defaults (target :: trying) depth def top env ambigok g nty) (\err => if ambig err then throw err - else tryGroups (maybe (Just err) Just merr) nty gs) + else tryGroups (Just $ fromMaybe err merr) nty gs) -- Declared in Core.Unify as: -- search : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index 98eb1c9..e0e4950 100644 --- a/src/Core/CompileExpr.idr +++ b/src/Core/CompileExpr.idr @@ -144,7 +144,7 @@ mutual thin n (CLocal fc prf) = let MkVar var' = insertVar {n} _ prf in CLocal fc var' - thin n (CRef fc x) = CRef fc x + thin _ (CRef fc x) = CRef fc x thin {outer} {inner} n (CLam fc x sc) = let sc' = thin {outer = x :: outer} {inner} n sc in CLam fc x sc' @@ -167,9 +167,9 @@ mutual thin n (CConstCase fc sc xs def) = CConstCase fc (thin n sc) (assert_total (map (thinConstAlt n) xs)) (assert_total (map (thin n) def)) - thin n (CPrimVal fc x) = CPrimVal fc x - thin n (CErased fc) = CErased fc - thin n (CCrash fc x) = CCrash fc x + thin _ (CPrimVal fc x) = CPrimVal fc x + thin _ (CErased fc) = CErased fc + thin _ (CCrash fc x) = CCrash fc x thinConAlt : (n : Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ n :: inner) thinConAlt {outer} {inner} n (MkConAlt x tag args sc) @@ -219,18 +219,18 @@ mutual export getFC : CExp args -> FC -getFC (CLocal fc y) = fc -getFC (CRef fc x) = fc -getFC (CLam fc x y) = fc -getFC (CLet fc x y z) = fc -getFC (CApp fc x xs) = fc -getFC (CCon fc x tag xs) = fc -getFC (COp fc x xs) = fc -getFC (CExtPrim fc p xs) = fc -getFC (CForce fc x) = fc -getFC (CDelay fc x) = fc -getFC (CConCase fc sc xs x) = fc -getFC (CConstCase fc sc xs x) = fc -getFC (CPrimVal fc x) = fc +getFC (CLocal fc _) = fc +getFC (CRef fc _) = fc +getFC (CLam fc _ _) = fc +getFC (CLet fc _ _ _) = fc +getFC (CApp fc _ _) = fc +getFC (CCon fc _ _ _) = fc +getFC (COp fc _ _) = fc +getFC (CExtPrim fc _ _) = fc +getFC (CForce fc _) = fc +getFC (CDelay fc _) = fc +getFC (CConCase fc _ _ _) = fc +getFC (CConstCase fc _ _ _) = fc +getFC (CPrimVal fc _) = fc getFC (CErased fc) = fc -getFC (CCrash fc x) = fc +getFC (CCrash fc _) = fc diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 48d2bd7..f94cc42 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -248,65 +248,65 @@ Show Error where export getErrorLoc : Error -> Maybe FC getErrorLoc (Fatal err) = getErrorLoc err -getErrorLoc (CantConvert loc env tm y) = Just loc -getErrorLoc (CantSolveEq loc env tm y) = Just loc -getErrorLoc (PatternVariableUnifies loc env n x) = Just loc -getErrorLoc (CyclicMeta loc n) = Just loc -getErrorLoc (WhenUnifying loc env tm y z) = Just loc -getErrorLoc (ValidCase loc env y) = Just loc -getErrorLoc (UndefinedName loc y) = Just loc -getErrorLoc (InvisibleName loc y _) = Just loc -getErrorLoc (BadTypeConType loc y) = Just loc -getErrorLoc (BadDataConType loc y z) = Just loc +getErrorLoc (CantConvert loc _ _ _) = Just loc +getErrorLoc (CantSolveEq loc _ _ _) = Just loc +getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc +getErrorLoc (CyclicMeta loc _) = Just loc +getErrorLoc (WhenUnifying loc _ _ _ _) = Just loc +getErrorLoc (ValidCase loc _ _) = Just loc +getErrorLoc (UndefinedName loc _) = Just loc +getErrorLoc (InvisibleName loc _ _) = Just loc +getErrorLoc (BadTypeConType loc _) = Just loc +getErrorLoc (BadDataConType loc _ _) = Just loc getErrorLoc (NotCovering loc _ _) = Just loc getErrorLoc (NotTotal loc _ _) = Just loc -getErrorLoc (LinearUsed loc k y) = Just loc -getErrorLoc (LinearMisuse loc y z w) = Just loc +getErrorLoc (LinearUsed loc _ _) = Just loc +getErrorLoc (LinearMisuse loc _ _ _) = Just loc getErrorLoc (BorrowPartial loc _ _ _) = Just loc getErrorLoc (BorrowPartialType loc _ _) = Just loc -getErrorLoc (AmbiguousName loc xs) = Just loc -getErrorLoc (AmbiguousElab loc _ xs) = Just loc -getErrorLoc (AmbiguousSearch loc _ xs) = Just loc -getErrorLoc (AllFailed ((_, x) :: xs)) = getErrorLoc x +getErrorLoc (AmbiguousName loc _) = Just loc +getErrorLoc (AmbiguousElab loc _ _) = Just loc +getErrorLoc (AmbiguousSearch loc _ _) = Just loc +getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x getErrorLoc (AllFailed []) = Nothing getErrorLoc (RecordTypeNeeded loc _) = Just loc getErrorLoc (NotRecordField loc _ _) = Just loc getErrorLoc (NotRecordType loc _) = Just loc getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc -getErrorLoc (InvalidImplicits loc _ y tm) = Just loc +getErrorLoc (InvalidImplicits loc _ _ _) = Just loc getErrorLoc (TryWithImplicits loc _ _) = Just loc getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc -getErrorLoc (CantSolveGoal loc _ tm) = Just loc -getErrorLoc (DeterminingArg loc n y env tm) = Just loc -getErrorLoc (UnsolvedHoles ((loc, _) :: xs)) = Just loc +getErrorLoc (CantSolveGoal loc _ _) = Just loc +getErrorLoc (DeterminingArg loc _ _ _ _) = Just loc +getErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just loc getErrorLoc (UnsolvedHoles []) = Nothing -getErrorLoc (CantInferArgType loc _ y z tm) = Just loc -getErrorLoc (SolvedNamedHole loc _ _ y) = Just loc -getErrorLoc (VisibilityError loc y z w s) = Just loc -getErrorLoc (NonLinearPattern loc y) = Just loc -getErrorLoc (BadPattern loc y) = Just loc -getErrorLoc (NoDeclaration loc y) = Just loc -getErrorLoc (AlreadyDefined loc y) = Just loc -getErrorLoc (NotFunctionType loc _ tm) = Just loc -getErrorLoc (RewriteNoChange loc _ tm ty) = Just loc -getErrorLoc (NotRewriteRule loc _ ty) = Just loc -getErrorLoc (CaseCompile loc y z) = Just loc -getErrorLoc (MatchTooSpecific loc y tm) = Just loc -getErrorLoc (BadDotPattern loc _ y tm z) = Just loc -getErrorLoc (BadImplicit loc y) = Just loc -getErrorLoc (BadRunElab loc _ tm) = Just loc -getErrorLoc (GenericMsg loc y) = Just loc -getErrorLoc (TTCError x) = Nothing -getErrorLoc (FileErr x y) = Nothing -getErrorLoc (ParseFail loc x) = Just loc -getErrorLoc (ModuleNotFound loc xs) = Just loc -getErrorLoc (CyclicImports xs) = Nothing +getErrorLoc (CantInferArgType loc _ _ _ _) = Just loc +getErrorLoc (SolvedNamedHole loc _ _ _) = Just loc +getErrorLoc (VisibilityError loc _ _ _ _) = Just loc +getErrorLoc (NonLinearPattern loc _) = Just loc +getErrorLoc (BadPattern loc _) = Just loc +getErrorLoc (NoDeclaration loc _) = Just loc +getErrorLoc (AlreadyDefined loc _) = Just loc +getErrorLoc (NotFunctionType loc _ _) = Just loc +getErrorLoc (RewriteNoChange loc _ _ _) = Just loc +getErrorLoc (NotRewriteRule loc _ _) = Just loc +getErrorLoc (CaseCompile loc _ _) = Just loc +getErrorLoc (MatchTooSpecific loc _ _) = Just loc +getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc +getErrorLoc (BadImplicit loc _) = Just loc +getErrorLoc (BadRunElab loc _ _) = Just loc +getErrorLoc (GenericMsg loc _) = Just loc +getErrorLoc (TTCError _) = Nothing +getErrorLoc (FileErr _ _) = Nothing +getErrorLoc (ParseFail loc _) = Just loc +getErrorLoc (ModuleNotFound loc _) = Just loc +getErrorLoc (CyclicImports _) = Nothing getErrorLoc ForceNeeded = Nothing -getErrorLoc (InternalError x) = Nothing -getErrorLoc (InType x y err) = getErrorLoc err -getErrorLoc (InCon x y err) = getErrorLoc err -getErrorLoc (InLHS x y err) = getErrorLoc err -getErrorLoc (InRHS x y err) = getErrorLoc err +getErrorLoc (InternalError _) = Nothing +getErrorLoc (InType _ _ err) = getErrorLoc err +getErrorLoc (InCon _ _ err) = getErrorLoc err +getErrorLoc (InLHS _ _ err) = getErrorLoc err +getErrorLoc (InRHS _ _ err) = getErrorLoc err -- Core is a wrapper around IO that is specialised for efficiency. export diff --git a/src/Core/Env.idr b/src/Core/Env.idr index 824b4ca..762c3b4 100644 --- a/src/Core/Env.idr +++ b/src/Core/Env.idr @@ -15,7 +15,7 @@ extend x = (::) {x} export length : Env tm xs -> Nat length [] = 0 -length (x :: xs) = S (length xs) +length (_ :: xs) = S (length xs) public export data IsDefined : Name -> List Name -> Type where @@ -118,11 +118,6 @@ letToLam (Let c val ty :: env) = Lam c Explicit ty :: letToLam env letToLam (b :: env) = b :: letToLam env mutual - dropS : List Nat -> List Nat - dropS [] = [] - dropS (Z :: xs) = dropS xs - dropS (S p :: xs) = p :: dropS xs - -- Quicker, if less safe, to store variables as a Nat, for quick comparison findUsed : Env Term vars -> List Nat -> Term vars -> List Nat findUsed env used (Local fc r idx p) @@ -145,6 +140,11 @@ mutual dropS (findUsed (b :: env) (map S (findUsedInBinder env used b)) tm) + where + dropS : List Nat -> List Nat + dropS [] = [] + dropS (Z :: xs) = dropS xs + dropS (S p :: xs) = p :: dropS xs findUsed env used (App fc fn arg) = findUsed env (findUsed env used fn) arg findUsed env used (As fc a p) diff --git a/src/Core/InitPrimitives.idr b/src/Core/InitPrimitives.idr index cb49a07..cdcd1a4 100644 --- a/src/Core/InitPrimitives.idr +++ b/src/Core/InitPrimitives.idr @@ -17,5 +17,4 @@ addPrim p export addPrimitives : {auto c : Ref Ctxt Defs} -> Core () addPrimitives - = do traverse addPrim allPrimitives - pure () + = traverse_ addPrim allPrimitives diff --git a/src/Core/Name.idr b/src/Core/Name.idr index dd63433..50cdd91 100644 --- a/src/Core/Name.idr +++ b/src/Core/Name.idr @@ -36,9 +36,9 @@ nameRoot (UN n) = n nameRoot (MN n _) = n nameRoot (PV n _) = nameRoot n nameRoot (DN _ n) = nameRoot n -nameRoot (Nested n inner) = nameRoot inner -nameRoot (CaseBlock n inner) = "$" ++ show n -nameRoot (WithBlock n inner) = "$" ++ show n +nameRoot (Nested _ inner) = nameRoot inner +nameRoot (CaseBlock n _) = "$" ++ show n +nameRoot (WithBlock n _) = "$" ++ show n nameRoot (Resolved i) = "$" ++ show i --- Drop a namespace from a name diff --git a/src/Core/TT.idr b/src/Core/TT.idr index 584c924..b775b32 100644 --- a/src/Core/TT.idr +++ b/src/Core/TT.idr @@ -407,16 +407,16 @@ data Term : List Name -> Type where export getLoc : Term vars -> FC -getLoc (Local fc x idx y) = fc -getLoc (Ref fc x name) = fc -getLoc (Meta fc x y xs) = fc -getLoc (Bind fc x b scope) = fc -getLoc (App fc fn arg) = fc -getLoc (As fc x y) = fc -getLoc (TDelayed fc x y) = fc -getLoc (TDelay fc x t y) = fc -getLoc (TForce fc x) = fc -getLoc (PrimVal fc c) = fc +getLoc (Local fc _ _ _) = fc +getLoc (Ref fc _ _) = fc +getLoc (Meta fc _ _ _) = fc +getLoc (Bind fc _ _ _) = fc +getLoc (App fc _ _) = fc +getLoc (As fc _ _) = fc +getLoc (TDelayed fc _ _) = fc +getLoc (TDelay fc _ _ _) = fc +getLoc (TForce fc _) = fc +getLoc (PrimVal fc _) = fc getLoc (Erased fc) = fc getLoc (TType fc) = fc diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 448e17b..d83c928 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -464,18 +464,18 @@ mutual = Just (PNamespace fc ns (mapMaybe (getDecl p) ds)) getDecl AsType d@(PClaim _ _ _ _ _) = Just d - getDecl AsType (PData fc vis (MkPData dfc tyn tyc opts cons)) + getDecl AsType (PData fc vis (MkPData dfc tyn tyc _ _)) = Just (PData fc vis (MkPLater dfc tyn tyc)) - getDecl AsType d@(PInterface fc vis cons n ps det cname ds) = Just d - getDecl AsType d@(PRecord fc vis n ps con fs) = Just d + getDecl AsType d@(PInterface _ _ _ _ _ _ _ _) = Just d + getDecl AsType d@(PRecord _ _ _ _ _ _) = Just d getDecl AsType d@(PFixity _ _ _ _) = Just d getDecl AsType d@(PDirective _ _) = Just d getDecl AsType d = Nothing getDecl AsDef (PClaim _ _ _ _ _) = Nothing - getDecl AsDef d@(PData fc vis (MkPLater dfc tyn tyc)) = Just d - getDecl AsDef (PInterface fc vis cons n ps det cname ds) = Nothing - getDecl AsDef (PRecord fc vis n ps con fs) = Nothing + getDecl AsDef d@(PData _ _ (MkPLater _ _ _)) = Just d + getDecl AsDef (PInterface _ _ _ _ _ _ _ _) = Nothing + getDecl AsDef (PRecord _ _ _ _ _ _) = Nothing getDecl AsDef (PFixity _ _ _ _) = Nothing getDecl AsDef (PDirective _ _) = Nothing getDecl AsDef d = Just d @@ -504,8 +504,8 @@ mutual where getFn : RawImp -> Core Name getFn (IVar _ n) = pure n - getFn (IApp _ f a) = getFn f - getFn (IImplicitApp _ f _ a) = getFn f + getFn (IApp _ f _) = getFn f + getFn (IImplicitApp _ f _ _) = getFn f getFn tm = throw (InternalError (show tm ++ " is not a function application")) toIDef : ImpClause -> Core ImpDecl @@ -559,7 +559,7 @@ mutual -- is a bit of a hack, but it's necessary to build parent constraint -- chasing functions correctly pairToCons : PTerm -> List PTerm - pairToCons (PPair fc l r) = pairToCons l ++ pairToCons r + pairToCons (PPair _ l r) = pairToCons l ++ pairToCons r pairToCons t = [t] expandConstraint : (Maybe Name, PTerm) -> List (Maybe Name, PTerm) diff --git a/src/Idris/REPLCommon.idr b/src/Idris/REPLCommon.idr index a31ae57..1cd984d 100644 --- a/src/Idris/REPLCommon.idr +++ b/src/Idris/REPLCommon.idr @@ -87,7 +87,7 @@ updateErrorLine : {auto o : Ref ROpts REPLOpts} -> updateErrorLine [] = do opts <- get ROpts put ROpts (record { errorLine = Nothing } opts) -updateErrorLine (e :: es) +updateErrorLine (e :: _) = do opts <- get ROpts put ROpts (record { errorLine = map getFCLine (getErrorLoc e) } opts) diff --git a/src/Parser/Lexer.idr b/src/Parser/Lexer.idr index 328dbbc..7cf477b 100644 --- a/src/Parser/Lexer.idr +++ b/src/Parser/Lexer.idr @@ -30,8 +30,8 @@ Show Token where show (Symbol x) = "symbol " ++ x show (Keyword x) = x show (Unrecognised x) = "Unrecognised " ++ x - show (Comment x) = "comment" - show (DocComment x) = "doc comment" + show (Comment _) = "comment" + show (DocComment _) = "doc comment" show (CGDirective x) = "CGDirective " ++ x show EndInput = "end of input" diff --git a/src/TTImp/BindImplicits.idr b/src/TTImp/BindImplicits.idr index 4a22e60..cb2afef 100644 --- a/src/TTImp/BindImplicits.idr +++ b/src/TTImp/BindImplicits.idr @@ -10,9 +10,6 @@ import Control.Monad.State %default covering -getUnique : List String -> String -> String -getUnique xs x = if x `elem` xs then getUnique xs (x ++ "'") else x - -- Rename the IBindVars in a term. Anything which appears in the list 'renames' -- should be renamed, to something which is *not* in the list 'used' export diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 588fffb..69a34ad 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -10,6 +10,7 @@ lowerFirst : String -> Bool lowerFirst "" = False lowerFirst str = assert_total (isLower (strHead str)) +export getUnique : List String -> String -> String getUnique xs x = if x `elem` xs then getUnique xs (x ++ "'") else x