diff --git a/.gitignore b/.gitignore index 7e73b8e..532a83a 100644 --- a/.gitignore +++ b/.gitignore @@ -25,3 +25,6 @@ cabal.project.local~ *.swp stack.yaml.lock result +exclude +result* +.vscode diff --git a/LICENSE b/LICENSE index f016c61..37de541 100644 --- a/LICENSE +++ b/LICENSE @@ -78,3 +78,38 @@ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +----------------------------------------------------------------------------- +The Buffer in the Networking module, is based on the Chan module by The University of Glasgow + +The Glasgow Haskell Compiler License + +Copyright 2004, The University Court of the University of Glasgow. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +- Redistributions of source code must retain the above copyright notice, +this list of conditions and the following disclaimer. + +- Redistributions in binary form must reproduce the above copyright notice, +this list of conditions and the following disclaimer in the documentation +and/or other materials provided with the distribution. + +- Neither name of the University nor the names of its contributors may be +used to endorse or promote products derived from this software without +specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY COURT OF THE UNIVERSITY OF +GLASGOW AND THE CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, +INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND +FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +UNIVERSITY COURT OF THE UNIVERSITY OF GLASGOW OR THE CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH +DAMAGE. \ No newline at end of file diff --git a/README-networking-communication-example.md b/README-networking-communication-example.md new file mode 100644 index 0000000..0beaab2 --- /dev/null +++ b/README-networking-communication-example.md @@ -0,0 +1,121 @@ +# A Communication Example of Networking in **LDGVNW** + +The following log shows an conversation of 4 conversation partners, running the "bidirhandoff" test. + +``` +Explanation: Client connects for the first time to the server +Client(4343)->Server(4242) +Message: NIntroduce (String:"qV8Xo421") (String:"4343") (TName (Bool:False) (String:"SendInt")) (TSend (String:"#!") (TInt) (TRecv (String:"#?") (TInt) (TSend (String:"#!") (TInt) (TRecv (String:"#?") (TInt) (TUnit))))) +Response: NOkayIntroduce (String:"Y1lPJ1sM") + +Explanation: Client sends the first value to the server +Client(4343)->Server(4242) +Message: NNewValue (String:"qV8Xo421") (Int:0) (VInt (Int:1)) +Response: NOkay + +Explanation: Server acknowledges the first value from the client +Server(4242)->Client(4343) +Message: NAcknowledgeValue (String:"Y1lPJ1sM") (Int:0) +Response: NOkay + +Explanation: Server sends the first value to the client +Server(4242)->Client(4343) +Message: NNewValue (String:"Y1lPJ1sM") (Int:0) (VInt (Int:1300)) +Response: NOkay + +Explanation: Client acknowledges the first value from the server +Client(4343)->Server(4242) +Message: NAcknowledgeValue (String:"qV8Xo421") (Int:0) +Response: NOkay + +Explanation: ServerHandoff connects to the Server +ServerHandoff(4240)->Server(4242) +Message: NIntroduce (String:"nCzR17XT") (String:"4240") (TName (Bool:True) (String:"SendSendIntServer")) (TSend (String:"#!") (TName (Bool:False) (String:"SendIntServer")) (TUnit) +Response: NOkayIntroduce(String:"unFbpEeg") + +Explanation: Client connects to the ClientHandoff +Client(4343)->ClientHandoff(4340) +Message: NIntroduce (String:"54AVQX89") (String:"4343") (TName (Bool:False) (String:"SendSendIntClient")) (TSend (String:"#!") (TName (Bool:False) (String:"SendIntClient")) (TUnit)) +Response: NOkayIntroduce (String:"dDF0Te3V") + +Explanation: Server sends the channel to the ServerHandoff, there are no values in the Handoff since all values are already acknowledged +Server(4242)->ServerHandoff(4240) +Message: NNewValue (String:"unFbpEeg") (Int:0) (VChanSerial (((SValuesArray []) (Int:1) (Int:1))) (((SValuesArray []) (Int:1) (Int:1))) (String:"qV8Xo421") (String:"Y1lPJ1sM") (((String:"127.0.0.1") (String:"4343") (String:"qV8Xo421")))) +Response: NOkay + +Explanation: Client sends the channel to the ClientHandoff +Client(4343)->ClientHandoff(4340) +Message: NNewValue (String:"54AVQX89") (Int:0) (VChanSerial (((SValuesArray []) (Int:1) (Int:1))) (((SValuesArray []) (Int:1) (Int:1))) (String:"Y1lPJ1sM") (String:"qV8Xo421") (((String:"127.0.0.1") (String:"4242") (String:"Y1lPJ1sM")))) +Response: NOkay + +Explanation: ClientHandoff wants to introduce itself to the Server, but fails since the channel is now owned by the ServerHandoff +ClientHandoff(4340)->Server(4242) +Message: NNewPartnerAddress (String:"qV8Xo421") (String:"4340") (String:"hh0kAZdY") +Response: NRedirect (String:"127.0.0.1") (String:"4240") + +Explanation: ServerHandoff wants to introduce itself to the Client, but fails since the channel is now owned by the ClientHandoff +ServerHandoff(4240)->Client(4343) +Message: NNewPartnerAddress (String:"Y1lPJ1sM") (String:"4240") (String:"OUN8jvH1") +Response: NRedirect (String:"127.0.0.1") (String:"4240") + +Explanation: ClientHandoff introduces itself to the ServerHandoff +ClientHandoff(4340)->ServerHandoff(4240) +Message: NNewPartnerAddress (String:"qV8Xo421") (String:"4340") (String:"hh0kAZdY") +Response: NOkay + +Explanation: ServerHandoff introduces itself to the ClientHandoff +ServerHandoff(4240)->ClientHandoff(4340) +Message: NNewPartnerAddress (String:"Y1lPJ1sM") (String:"4240") (String:"OUN8jvH1") +Response: NOkay + +Explanation: ClientHandoff acknowledges the new address of the ServerHandoff +ClientHandoff(4340)->ServerHandoff(4240) +Message: NAcknowledgePartnerAddress (String:"qV8Xo421") (String:"OUN8jvH1") +Response: NOkay + +Explanation: ServerHandoff acknowledges the new address of the ClientHandoff +ServerHandoff(4240)->ClientHandoff(4340) +Message: NAcknowledgePartnerAddress (String:"Y1lPJ1sM") (String:"hh0kAZdY") +Response: NOkay + +Explanation: Since the ServerHandoff has acknowledged the new address, the ClientHandoff can now acknowledge the successful receiving of the Channel to the Client +ClientHandoff(4340)->Client(4343) +Message: NAcknowledgeValue (String:"dDF0Te3V") (Int:0) +Response: NOkay + +Explanation: Since the ClientHandoff has acknowledged the new address, the ServerHandoff can now acknowledge the successful receiving of the Channel to the Server +ServerHandoff(4240)->Server(4242) +Message: NAcknowledgeValue (String:"nCzR17XT") (Int:0) +Response: NOkay + + +ClientHandoff(4340)->ServerHandoff(4240) +Message: NNewValue (String:"qV8Xo421") (Int:1) (VInt (Int:41)) +Response: NOkay + +Explanation: Since the client now has all of the values of its active connections acknowledged, it can disconnect +Client(4343)->ClientHandoff(4340) +Message: NDisconnect (String:"54AVQX89") +Response: NOkay + +Explanation: Since the server has now all of the values of its active connections acknowledged, it can disconnect +Server(4242)->ServerHandoff(4240) +Message: NDisconnect (String:"unFbpEeg") +Response: NOkay + +ServerHandoff(4240)->ClientHandoff(4340) +Message: NAcknowledgeValue (String:"Y1lPJ1sM") (Int:1) +Response: NOkay + +ServerHandoff(4240)->ClientHandoff(4340) +Message: NNewValue (String:"Y1lPJ1sM") (Int:1) (VInt (Int:37)) +Response: NOkay + +ClientHandoff(4340)->ServerHandoff(4240) +Message: NAcknowledgeValue (String:"qV8Xo421") (Int:1) +Response: NOkay + +ServerHandoff(4240)->ClientHandoff(4340) +Message: NDisconnect (String:"Y1lPJ1sM") +Response: NOkay +``` \ No newline at end of file diff --git a/README-networking.md b/README-networking.md new file mode 100644 index 0000000..9161056 --- /dev/null +++ b/README-networking.md @@ -0,0 +1,159 @@ +# How to run LDGVNW +Using LDGVNW is a little more difficult than simply starting a single program. In addition to the requirements of LDGV, you also need a network connected via IPv4. Should this network span more than one device, the IP-addresses within the LDGVNW programs need to be altered to reflect this architecture. The current version of LDGVNW was tested on Fedora 37 and macOS 13.2 and should work on every recent Linux or macOS machine, it is unknown whether LDGVNW works on Windows machines. + +To run a LDGVNW example, found in the networking-examples folder, each program in the example folder needs to be run. To start the "handoff" example, you would run the following commands in different terminals or on different machines: + +- `stack run ldgv -- interpret networking-examples/handoff/client.ldgvnw` +- `stack run ldgv -- interpret networking-examples/handoff/server.ldgvnw` +- `stack run ldgv -- interpret networking-examples/handoff/handoff.ldgvnw` + +The order in which these commands are executed is not relevant. + +To test all the different test-cases in an easier way, they can be automatically run, with the scrips provided in the networking-tests folder. Simply running one of these scripts will execute the whole test-case at once. +The testNW\* scripts contain all the tests, except for the recursion test. + + +# An Introduction to LDGVNW +LDGVNW adds two new commands to LDGV to allow for networking capabilities: + +- `accept ` +- `connect ` + +The accept command requires an integer, as a port for others to connect, and a type, that will be required of a connecting connection. +Once a communication partner connects with a desired type, the accept command will return a VChan, of this type. +The connect command also requires an integer port and a desired type, but also needs to specify a string, for the address of the connection partner, and an integer, for the port of the connection partner. +Just like with the accept command, the connect command will return a VChan, of the desired type, once a connection has been established. +Important to note is that, with the current implementation, only IPv4 addresses are supported. +IPv6 and Unix domain sockets could be supported in the future, with relatively low effort. + +# The Logical Communication Architecture +## Messages and Responses +In LDGVNW, there are 7 possible Messages and 5 possible Responses. +The messages are: + +- `Introduce ` +- `NewValue ` +- `RequestValue ` +- `AcknowledgeValue ` +- `NewPartnerAddress ` +- `AcknowledgePartnerAddress ` +- `Disconnect ` + +With possible responses: + +- `Redirect ` +- `Okay` +- `OkayIntroduce ` +- `Wait` +- `Error` + +Typing for the attributes: + +- **UserID** is a unique string, used to identify the logical communication partner +- **ConnectionID** is a unique string, used to identify the current physical connection, to a logical communication partner +- **Port** is a string, containing the port number +- **Address** is a string, containing the IPv4 address or URL of a communication partner +- **Value** is a type of data in LDGV. The VChans present in this Value are replaced with VChanSerials +- **Value Index** is an integer, containing the index of a Value +- **Type Name** is a TName Type, of the desired Type +- **Type Structure** is a Type, containing the resolved Type of the Type Name + +## Establishing a new Connection +As soon as B opens up their port with the accept command. A can connect, by sending an Introduce message to B. +This message contains the unique ID of A, As port, as well as the name and structure of the desired communication Type. +B then answers with a OkayIntroduce response, sharing their own unique ID with A. +Following that, A and B can send and recv values analog to Channels created with the new command. + +## Sending messages over a Connection +When communication partner A executes a send command to send Value V to B, A first analyses V. +Should V be or contain a Channel C, A will set a flag in C to redirect new messages to the address of B. +After that, C will be converted to a serializable form, CS. +With every Channel now being in a form, which can be sent over the network, A writes V to its write-buffer and sends B a NewValue message containing V. +Upon receiving V as B with the recv command, B undoes the conversion of every Channel in V. +B then contacts the communication partner of each Channel, to inform them, that their new communication partner is now B, instead of A. +After this, B sends an acknowledgment (AcknowledgeValue message) back to A, which finalizes the sending of V. +A can now remove V out of its write-buffer. + +## Responding to Messages +Except for the Introduce message, every message should be ideally answered with an Okay response. +But in some cases the messages don't arrive at the right communication partner or at the wrong time. In these cases, other responses are used. +- **Redirect** responses are sent, when a message is sent to an outdated address +- **Wait** responses are sent, when a message cannot be handled at the current moment + - This can be caused by currently being in a critical section while handling another message + - During the sending process of a Channel + - When the addressed Channel isn't yet known by the program +- **Error** responses are sent when an error occurs while handling a AcknowledgePartnerAddress message + +## Informing Communication Partners of a Communication Partner Change +If there is a Channel C between A and B and A sends their side of the Channel to D, B needs to be made aware of that. +To archive this, D sends a NewPartnerAddress message to B. This message contains the server port of D and a new ConnectionID DC for D. +B then replies with a AcknowledgePartnerAddress message, repeating DC. +As soon as the address is established, C is considered successfully received by D. + +## Shutting Down after Completing all Instructions +After A finishes the interpretation of their program, A waits until all messages they sent were acknowledged by their communication partners. After that, A sends a Disconnect message to all their peers. The Disconnect message is needed, since the recv command doesn't know the received Type during interpretation. Should the Disconnect message not exist, it would be theoretically possible to send a Unit-Type of an exhausted Channel to another communication partner. The recipient would now be unknowing whether their new communication partner is still online. + +## Making Channels serializable +One of the main focuses of LDGVNW is to send Channels over the network. +VChans are Channels that are directly useable by LDGV, but since VChans can't be serialized directly, they need to be converted into VChanSerials first. VChans have the following (simplified) architecture: +`VChan ` + +The contained NetworkConnection has this (simplified) architecture: + +`NetworkConnection ` + +The relevant part, for the conversion to VChanSerials, is found in the NetworkConnection. The ReadBuffer contains Values, that are not yet handled, while the WriteBuffer contains Values, that are not yet acknowledged by the communication partner. The implementation of these Buffers is based on the implementation of the Chan type of Haskell, this is also noted and acknowledged in the Buffer module. The PartnerID and OwnID are strings to identify the logical communication partner, these do not change when sent to another communication partner. Lastly, the ConnectionState contains information about whether the connection is an external connection, an internal connection, offline or should be redirected to another communication partner. + +The VChanSerial has the following architecture: + +`VChanSerial
` + +The ReadList contains the current elements of the ReadBuffer, the ReadOffset contains the logical index of the first element of the ReadBuffer, and the ReadLength is the number of all logical elements in the buffer. For example, let's say 5 Values were received, but the first 3 already were handled, so the ReadList would contain 2 elements, the ReadOffset would be 3 and the ReadLength would be 5. The WriteList, WriteOffset and WriteLength behave analogously. The PartnerID and OwnID are directly taken from the NetworkConnection and the Address, Port and ConnectionID (from the partner) are taken from the ConnectionState. + +To convert a VChanSerial to a VChan, an empty VChan is simply filled with the data provided by the VChanSerial. + +It is important to note that VChans only should be serialized after their ConnectionState has been set to Redirect. This freezes the VChan, as it can no longer receive new messages. This way it can be assured, that at the time of receipt, both the original VChan and the one generated from the VChanSerial contain identical data. + +## Why Values are Acknowledged +LDGVNW has separate messages for sending a Value (NewValue) and acknowledging a Value (AcknowledgeValue). Simply knowing that the other party has received a Value, isn't enough when Channels are involved. +Let's say there is a Channel C, between A and B. A sends their side of C to D and at the same time, B sends their side of C to E. Since the sending of the Channel sides, happened simultaneously, D still thinks they are talking to B and E thinks they are talking to A. Should A and B now go offline, before either D or E, can contact them, to find out where they redirected their connections to, D and E will not be able to connect. Since acknowledgments are only sent after a sent Channel has been reconnected, it can be assured that D and E are connected, before A and B can go offline. + +It would also be possible to use a Response to the NewValue message, to signal that the Value got acknowledged, but I decided to split this process into two messages, since the acknowledging can take long time, compared to other messages. + +## Requesting a Value +Sending of most messages is only attempted once, this includes NewValue messages. A Value can be requested, by the recv command, using a RequestValue message. + +## A communication example +The [communication example](README-networking-communication-example.md) gives a concrete demonstration of the communication protocol. + +# Serializing and Sending Messages +The logical messages are serialized first, then are sent either using a fast protocol, which reuses existing connections or a stateless protocol, which was primary used during development, as a fallback when the fast protocol wasn't working yet. The fast protocol is enabled by default, switching protocols requires a small change to the networking code. + +## Serialization +Messages and Responses in LDGVNW are serialized into ASCII-Strings and follow the form of the name of the Message, Value, etc. followed by their arguments in parentheses. For instance, the message `NewValue <2> ` would be translated to `NNewValue (String:"abcd1234") (Int:2) (VInt (Int:42))`. The N in front of NewValue, signals that it belongs to the networking messages, the V in front of Int makes differentiating between Value Ints and other Ints easier. + +To deserialize these messages, the alex and happy libraries are used. + +## Stateless Protocol +The stateless protocol allows sending serialized logical messages directly. A new connection is established, followed by, sending the serialized message, waiting for a response and disconnecting afterward. Always creating new connections assures that every message gets its correct response, but establishing a new TCP connection every time a message is sent, also causes a performance penalty. The stateless protocol has a thread permanently looking for new messages. This thread creates a new temporary thread to handle each incoming message. Messages are primarily sent from the main thread, in which also the interpretation occurs, except for some messages, like the acknowledging of a new partner address, which is sent from the temporary thread. + +## Fast Protocol +The fast protocol saves a once created TCP connection and reuses it as long as it stays open. Since LDGVNW uses multiple threads to send messages, this can lead to messages and responses being mismatched. To avoid this, each Message and Response is wrapped in a ConversationSession. + +- `ConversationMessage ` +- `ConversationResponse ` +- `ConversationCloseAll` + +The ConversationID is a random string, selected by the sender of the message and copied by the respondent. ConversationCloseAll is used when one party wants to close all connections to a peer, signaling to their peer that they would need to establish a new connection, if they would like to talk to this address and port again. +This is helpful if there are A and B. A has an address and port combination of AP. After A and B are done communicating, A goes offline and sends a ConversationCloseAll. Now, C can reuse AP to talk to B. +The fast protocol also has a permanent thread, looking for new incoming connections. Each new TCP connection gets its own permanent thread, where new incoming messages and responses are collected. Each Channel also gets its own thread, where incoming messages get handled. Responses can be picked up by the sending function, to determine its further behavior. +Similar to the stateless protocol, most messages are sent from the main thread, while some messages are sent from a connection specific thread. + +# Compatibility between Internal and External Channels +Internal Channels (Channels in the same program, typically created with new) and external Channels (Channels between two programs, typically created with connect and accept) are handled, for the most part, the same way in LDGVNW. Every Channel has a NetworkConnection. The NetworkConnection saves both incoming and outgoing messages and a ConnectionState. The ConnectionState dictates whether a NetworkConnection is internal or external. +In contrast to external Channels, which serialize and send messages, internal Channels write the data of these messages directly to their counterparts. +Should an internal Channel be sent to a peer, the internal Channel gets converted into an external Channel. Should both sides of an external Channel end up in the same program, the connection will be converted to an internal Channel. + + + + diff --git a/README.md b/README.md index d6baa47..dcd3add 100644 --- a/README.md +++ b/README.md @@ -80,6 +80,10 @@ properly curried, the top level symbol must have a type signature matching `LDST_fp0_t` and the name must match the name transformations pointed out above. (NB: this allows to subvert the type system, in all good and bad ways.) +## LDGVNW + +LDGVNW is a extension to LDGV, more can be read [here](README-networking.md). + ## Testing You can run the full test suite by: diff --git a/exe/Main.hs b/exe/Main.hs index c96b9c6..8e2fe27 100644 --- a/exe/Main.hs +++ b/exe/Main.hs @@ -2,7 +2,6 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} module Main (main) where @@ -25,7 +24,7 @@ import Parsing import qualified C.Compile as C import qualified C.Generate as C import qualified Interpreter as I -import qualified ProcessEnvironment as P +import qualified ProcessEnvironmentTypes as P import qualified Syntax import qualified Typechecker as T @@ -161,6 +160,7 @@ actionParserInfo :: Opts.ParserInfo (Action ()) actionParserInfo = Opts.info (actionParser <**> Opts.helper) $ mconcat [ Opts.progDesc "An implementation of Label Dependent Session Types (LDST)." , Opts.footer "Authors: \ + \Leon Läufer (LDGVNW implementation), \ \Thomas Leyh (CCLDLC implementation), \ \Nils Hagner (interpreter, web frontend), \ \Janek Spaderna (C backend, command line frontend), \ @@ -190,6 +190,7 @@ interpret Interpreter{ interpreterInputs = inputs, interpreterGradual = gradual Right a -> pure a Left err -> fail $ "Error: " ++ err liftIO $ I.interpret decls + -- For testing a small wait here, so all communications can come to a close liftIO $ putStrLn $ either (\v -> "Error: " ++ show v) (\v -> "Result: " ++ show v) @@ -252,6 +253,9 @@ parseFile mpath = do (name, src) <- liftIO $ case mpath of Nothing -> ("",) <$> getContents Just fp -> (fp,) <$> readFile fp + + -- Print declarations for debug + -- msgInfo . show $ parseDecls src case parseDecls src of Left err -> Nothing <$ formatMsg MsgError (Just name) err diff --git a/exe/Output.hs b/exe/Output.hs index 689ef8e..7f63318 100644 --- a/exe/Output.hs +++ b/exe/Output.hs @@ -46,6 +46,7 @@ stderrColumns = liftIO $ fmap Terminal.width <$!> size data MsgLevel = MsgError | MsgWarning + | MsgInfo msgWarning :: (MonadReader TerminalSize m, MonadIO m) => String -> m () msgWarning = formatMsg MsgWarning Nothing @@ -53,12 +54,16 @@ msgWarning = formatMsg MsgWarning Nothing msgFatal :: (MonadReader TerminalSize m, MonadIO m) => String -> m a msgFatal msg = formatMsg MsgError Nothing msg >> liftIO exitFailure +msgInfo :: (MonadReader TerminalSize m, MonadIO m) => String -> m () +msgInfo = formatMsg MsgInfo Nothing + formatMsg :: (MonadIO m, MonadReader TerminalSize m) => MsgLevel -> Maybe FilePath -> String -> m () formatMsg level mfile msg = do let levelDoc = let (levelString, color) = case level of MsgError -> ("error", Terminal.Red) MsgWarning -> ("warning", Terminal.Yellow) + MsgInfo -> ("info", Terminal.White) in annotate (Terminal.color color) $ levelString <> ": " let fileDoc = flip foldMap mfile \file -> diff --git a/ldgv.cabal b/ldgv.cabal index 2b5becf..88e3b2b 100644 --- a/ldgv.cabal +++ b/ldgv.cabal @@ -1,6 +1,6 @@ cabal-version: 1.18 --- This file has been generated from package.yaml by hpack version 0.35.0. +-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack @@ -9,12 +9,13 @@ version: 0.0.1 synopsis: Frontend, interpreter and C backend for LDGV/LDST homepage: https://github.com/proglang/ldgv#readme bug-reports: https://github.com/proglang/ldgv/issues -author: Thomas Leyh (CCLDLC implementation), +author: Leon Läufer (LDGVNW implementation), + Thomas Leyh (CCLDLC implementation), Nils Hagner (web frontend, interpreter), Janek Spaderna (command line fronted, C backend), Peter Thiemann (parser, typechecker) maintainer: thiemann@informatik.uni-freiburg.de -copyright: 2019-2021 Chair of Programming Languages, Uni Freiburg +copyright: 2019-2023 Chair of Programming Languages, Uni Freiburg license: BSD3 license-file: LICENSE build-type: Simple @@ -66,12 +67,29 @@ library Examples Interpreter Kinds + Networking.Assert + Networking.Buffer + Networking.Common + Networking.Incoming + Networking.Messages + Networking.NetworkBuffer + Networking.NetworkConnection + Networking.NetworkingMethod.Fast + Networking.NetworkingMethod.NetworkingMethodCommon + Networking.NetworkingMethod.Stateless + Networking.Outgoing + Networking.RandomID + Networking.Serialize + Networking.Tests Parsing Parsing.Grammar Parsing.Tokens ProcessEnvironment + ProcessEnvironmentTypes Syntax Typechecker + ValueParsing.ValueGrammar + ValueParsing.ValueTokens other-modules: PrettySyntax TCSubtyping @@ -87,15 +105,20 @@ library alex , happy build-depends: - array + SafeSemaphore >=0.10.1 + , array , base >=4.12 && <5 , bytestring , containers + , directory , file-embed , filepath , lens , mtl + , network + , network-run , prettyprinter + , random , text , transformers , typed-process diff --git a/networking-examples/add/client.ldgvnw b/networking-examples/add/client.ldgvnw new file mode 100644 index 0000000..e55430d --- /dev/null +++ b/networking-examples/add/client.ldgvnw @@ -0,0 +1,19 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + let con = (connect 4343 SendInt "127.0.0.1" 4242 ) in + send2 con diff --git a/networking-examples/add/server.ldgvnw b/networking-examples/add/server.ldgvnw new file mode 100644 index 0000000..fdb5e13 --- /dev/null +++ b/networking-examples/add/server.ldgvnw @@ -0,0 +1,23 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + -- let c4 = end c3 in + (m + n) + + +val main : Int +val main = + -- let sock = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + add2 con diff --git a/networking-examples/add2/add.ldgvnw b/networking-examples/add2/add.ldgvnw new file mode 100644 index 0000000..0df57b2 --- /dev/null +++ b/networking-examples/add2/add.ldgvnw @@ -0,0 +1,29 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val addClient : Unit +val addClient = + let con = connect 4242 SendInt "127.0.0.1" 4242 in + send2 con + +val addServer : Int +val addServer = + let con = accept 4242 (dualof SendInt) in + add2 con + +val main : Int +val main = + let c = fork addClient in + addServer diff --git a/networking-examples/bidirectional/client.ldgvnw b/networking-examples/bidirectional/client.ldgvnw new file mode 100644 index 0000000..a68a0a7 --- /dev/null +++ b/networking-examples/bidirectional/client.ldgvnw @@ -0,0 +1,26 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4343) in + let con = (connect 4343 SendInt "127.0.0.1" 4242 ) in -- This cannot be localhost, since this might break on containerized images + send2 con diff --git a/networking-examples/bidirectional/server.ldgvnw b/networking-examples/bidirectional/server.ldgvnw new file mode 100644 index 0000000..65dd284 --- /dev/null +++ b/networking-examples/bidirectional/server.ldgvnw @@ -0,0 +1,26 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + add2 con diff --git a/networking-examples/bidirhandoff/client.ldgvnw b/networking-examples/bidirhandoff/client.ldgvnw new file mode 100644 index 0000000..7e5607c --- /dev/null +++ b/networking-examples/bidirhandoff/client.ldgvnw @@ -0,0 +1,37 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers +-- Expected return 1300 + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit +type SendIntClient : ! ~ssn = !Int. ?Int. Unit +type SendSendIntClient : ! ~ssn = !SendIntClient. Unit +type SendIntServer : ! ~ssn = ?Int. !Int. Unit +type SendSendIntServer : ! ~ssn = !SendIntServer. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4343) in + let con = (connect 4343 SendInt "127.0.0.1" 4242 ) in -- This cannot be localhost, since this might break on containerized images + let x = ((send con) 1) in + let = recv x in + let con2 = (connect 4343 SendSendIntClient "127.0.0.1" 4340) in + let con22 = ((send con2) x2) in + -- let con23 = end con22 in + (n) + diff --git a/networking-examples/bidirhandoff/clienthandoff.ldgvnw b/networking-examples/bidirhandoff/clienthandoff.ldgvnw new file mode 100644 index 0000000..aac53d3 --- /dev/null +++ b/networking-examples/bidirhandoff/clienthandoff.ldgvnw @@ -0,0 +1,36 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers +-- Expected return 37 + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit +type SendIntClient : ! ~ssn = !Int. ?Int. Unit +type SendSendIntClient : ! ~ssn = !SendIntClient. Unit +type SendIntServer : ! ~ssn = ?Int. !Int. Unit +type SendSendIntServer : ! ~ssn = !SendIntServer. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4340) in + let con = (accept 4340 (dualof SendSendIntClient)) in -- This cannot be localhost, since this might break on containerized images + let = (recv con) in + let x = ((send talk) 41) in + let = recv x in + -- let con2 = end x2 in + (n) + diff --git a/networking-examples/bidirhandoff/server.ldgvnw b/networking-examples/bidirhandoff/server.ldgvnw new file mode 100644 index 0000000..77fe0cf --- /dev/null +++ b/networking-examples/bidirhandoff/server.ldgvnw @@ -0,0 +1,36 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers +-- Expected return 1 + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit +type SendIntClient : ! ~ssn = !Int. ?Int. Unit +type SendSendIntClient : ! ~ssn = !SendIntClient. Unit +type SendIntServer : ! ~ssn = ?Int. !Int. Unit +type SendSendIntServer : ! ~ssn = !SendIntServer. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + let = recv con in + let c22 = (send c2) 1300 in + let con2 = (accept 4242 (SendSendIntServer)) in + let con3 = ((send con2) c22) in + -- let con4 = end con3 in + (m) diff --git a/networking-examples/bidirhandoff/serverhandoff.ldgvnw b/networking-examples/bidirhandoff/serverhandoff.ldgvnw new file mode 100644 index 0000000..03fd2ad --- /dev/null +++ b/networking-examples/bidirhandoff/serverhandoff.ldgvnw @@ -0,0 +1,35 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers +-- Expected return 41 + +type SendInt : ! ~ssn = !Int. ?Int. !Int. ?Int. Unit +type SendIntClient : ! ~ssn = !Int. ?Int. Unit +type SendSendIntClient : ! ~ssn = !SendIntClient. Unit +type SendIntServer : ! ~ssn = ?Int. !Int. Unit +type SendSendIntServer : ! ~ssn = !SendIntServer. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let = recv x in + let y = ((send x2) 41) in + let = recv y in + -- let y3 = end y2 in + (m + n) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let c22 = (send c2) 1300 in + let = recv c22 in + let c32 = (send c3) 37 in + -- let c4 = end c32 in + (m + n) + +val main : Int +val main = + -- let sock = (create 4240) in + let con = (connect 4240 (dualof SendSendIntServer) "127.0.0.1" 4242) in + let = recv con in + let = recv talk in + let c22 = (send c2) 37 in + -- let con4 = end c22 in + (m) diff --git a/networking-examples/handoff/client.ldgvnw b/networking-examples/handoff/client.ldgvnw new file mode 100644 index 0000000..29d4175 --- /dev/null +++ b/networking-examples/handoff/client.ldgvnw @@ -0,0 +1,28 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit + +val send1 (c: SendInt) : SendOneInt = + let x = ((send c) 1) in + (x) + +val send2 (c2: SendOneInt) = + let y = ((send c2) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + -- let sock = (create 4141) in + let con = (connect 4141 SendInt "127.0.0.1" 4242) in -- This cannot be localhost, since this might break on containerized images + let oneint = (send1 con) in + let con2 = (connect 4141 SendSendOneInt "127.0.0.1" 4343) in + (send con2) oneint + diff --git a/networking-examples/handoff/handoff.ldgvnw b/networking-examples/handoff/handoff.ldgvnw new file mode 100644 index 0000000..096ba0b --- /dev/null +++ b/networking-examples/handoff/handoff.ldgvnw @@ -0,0 +1,27 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit + +val send1 (c: SendInt) : SendOneInt = + let x = ((send c) 1) in + (x) + +val send2 (c2: SendOneInt) = + let y = ((send c2) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + -- let con = (create 4343) in + let con = (accept 4343 (dualof SendSendOneInt)) in + let = recv con in + send2 oneint + diff --git a/networking-examples/handoff/server.ldgvnw b/networking-examples/handoff/server.ldgvnw new file mode 100644 index 0000000..0a9aa08 --- /dev/null +++ b/networking-examples/handoff/server.ldgvnw @@ -0,0 +1,20 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Int +val main = + -- let con = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + add2 con diff --git a/networking-examples/handoff2/client.ldgvnw b/networking-examples/handoff2/client.ldgvnw new file mode 100644 index 0000000..45c3aa7 --- /dev/null +++ b/networking-examples/handoff2/client.ldgvnw @@ -0,0 +1,22 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + -- let c4 = end c3 in + (m + n) + +val main : Unit +val main = + let sock = 4444 in + let con = (connect sock SendInt "127.0.0.1" 4242 ) in -- This cannot be localhost, since this might break on containerized images + send2 con diff --git a/networking-examples/handoff2/handoff.ldgvnw b/networking-examples/handoff2/handoff.ldgvnw new file mode 100644 index 0000000..4961512 --- /dev/null +++ b/networking-examples/handoff2/handoff.ldgvnw @@ -0,0 +1,18 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = ?Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit +-- type SendOneIntInv : ! ~ssn = ?Int. Unit + +val main : Int +val main = + let sock = 4343 in + let con = (connect sock (dualof SendSendOneInt) "127.0.0.1" 4242) in + let = recv con in + let = recv oneint in + -- let c4 = end c2 in + -- let c5 = end c3 in + result + diff --git a/networking-examples/handoff2/server.ldgvnw b/networking-examples/handoff2/server.ldgvnw new file mode 100644 index 0000000..9d9429e --- /dev/null +++ b/networking-examples/handoff2/server.ldgvnw @@ -0,0 +1,27 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = ?Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit +-- type SendOneIntInv : ! ~ssn = ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) (c3: SendSendOneInt)= + let = recv c1 in + let y = ((send c3) c2) in + -- let z = end y in + (m) + +-- Hier problematisch ldgv hat noch kein Konzept wie beim akzeptieren zwischen verschiedenen Types ungerschieden werden kann +val main : Int +val main = + let sock = 4242 in + let con1 = (accept sock (dualof SendInt)) in + let con2 = (accept sock (SendSendOneInt)) in + add2 con1 con2 diff --git a/networking-examples/handoff3/client.ldgvnw b/networking-examples/handoff3/client.ldgvnw new file mode 100644 index 0000000..874ca29 --- /dev/null +++ b/networking-examples/handoff3/client.ldgvnw @@ -0,0 +1,30 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. ?SendOneInt. Unit + +val send1 (c: SendInt) : SendOneInt = + let x = ((send c) 1) in + (x) + +val send2 (c2: SendOneInt) = + let y = ((send c2) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + -- let sock = (create 4141) in + let con = (connect 4141 SendInt "127.0.0.1" 4242) in -- This cannot be localhost, since this might break on containerized images + let oneint = (send1 con) in + let con2 = (connect 4141 SendSendOneInt "127.0.0.1" 4343) in + let con3 = (send con2) oneint in + let = recv con3 in + send2 oneint + diff --git a/networking-examples/handoff3/handoff.ldgvnw b/networking-examples/handoff3/handoff.ldgvnw new file mode 100644 index 0000000..70b7113 --- /dev/null +++ b/networking-examples/handoff3/handoff.ldgvnw @@ -0,0 +1,28 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. ?SendOneInt. Unit + +val send1 (c: SendInt) : SendOneInt = + let x = ((send c) 1) in + (x) + +val send2 (c2: SendOneInt) = + let y = ((send c2) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + -- let con = (create 4343) in + let con = (accept 4343 (dualof SendSendOneInt)) in + let = recv con in + let c2 = (send c2) oneint in + () + diff --git a/networking-examples/handoff3/server.ldgvnw b/networking-examples/handoff3/server.ldgvnw new file mode 100644 index 0000000..0a9aa08 --- /dev/null +++ b/networking-examples/handoff3/server.ldgvnw @@ -0,0 +1,20 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Int +val main = + -- let con = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + add2 con diff --git a/networking-examples/handoff4/client.ldgvnw b/networking-examples/handoff4/client.ldgvnw new file mode 100644 index 0000000..45c3aa7 --- /dev/null +++ b/networking-examples/handoff4/client.ldgvnw @@ -0,0 +1,22 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + -- let c4 = end c3 in + (m + n) + +val main : Unit +val main = + let sock = 4444 in + let con = (connect sock SendInt "127.0.0.1" 4242 ) in -- This cannot be localhost, since this might break on containerized images + send2 con diff --git a/networking-examples/handoff4/handoff.ldgvnw b/networking-examples/handoff4/handoff.ldgvnw new file mode 100644 index 0000000..53b4303 --- /dev/null +++ b/networking-examples/handoff4/handoff.ldgvnw @@ -0,0 +1,20 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = ?Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. ?SendOneInt. Unit +-- type SendOneIntInv : ! ~ssn = ?Int. Unit + +val main : Unit +val main = + let sock = 4343 in + let con = (connect sock (dualof SendSendOneInt) "127.0.0.1" 4242) in + let = recv con in + let c3 = (send c2) oneint in + -- let = recv oneint in + + -- let c4 = end c2 in + -- let c5 = end c3 in + () + diff --git a/networking-examples/handoff4/server.ldgvnw b/networking-examples/handoff4/server.ldgvnw new file mode 100644 index 0000000..feb3ecb --- /dev/null +++ b/networking-examples/handoff4/server.ldgvnw @@ -0,0 +1,29 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = ?Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. ?SendOneInt. Unit +-- type SendOneIntInv : ! ~ssn = ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) (c3: SendSendOneInt)= + let = recv c1 in + let y = ((send c3) c2) in + let = recv y in + let = recv oneint in + -- let z = end y in + (m+n) + +-- Hier problematisch ldgv hat noch kein Konzept wie beim akzeptieren zwischen verschiedenen Types ungerschieden werden kann +val main : Int +val main = + let sock = 4242 in + let con1 = (accept sock (dualof SendInt)) in + let con2 = (accept sock (SendSendOneInt)) in + add2 con1 con2 diff --git a/networking-examples/handoff5/add.ldgvnw b/networking-examples/handoff5/add.ldgvnw new file mode 100644 index 0000000..0f648b2 --- /dev/null +++ b/networking-examples/handoff5/add.ldgvnw @@ -0,0 +1,23 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let con = (connect 4242 SendSendOneInt "127.0.0.1" 4343 ) in + let con2 = (send con) x in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Int +val main = + let = (new SendInt) in + let a1 = fork (send2 a) in + add2 b diff --git a/networking-examples/handoff5/handoff.ldgvnw b/networking-examples/handoff5/handoff.ldgvnw new file mode 100644 index 0000000..096ba0b --- /dev/null +++ b/networking-examples/handoff5/handoff.ldgvnw @@ -0,0 +1,27 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendSendOneInt : ! ~ssn = !SendOneInt. Unit + +val send1 (c: SendInt) : SendOneInt = + let x = ((send c) 1) in + (x) + +val send2 (c2: SendOneInt) = + let y = ((send c2) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + -- let con = (create 4343) in + let con = (accept 4343 (dualof SendSendOneInt)) in + let = recv con in + send2 oneint + diff --git a/networking-examples/handoff6/client.ldgvnw b/networking-examples/handoff6/client.ldgvnw new file mode 100644 index 0000000..f13e3d3 --- /dev/null +++ b/networking-examples/handoff6/client.ldgvnw @@ -0,0 +1,25 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type EmptyConversation : ! ~ssn = Unit +type SendEmptyConversation : ! ~ssn = !EmptyConversation.Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + (y) + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + let con = (connect 4343 SendInt "127.0.0.1" 4242 ) in + let emptycon = send2 con in + let handoff = (accept 4343 SendEmptyConversation) in + let concon = (send handoff) emptycon in + () + diff --git a/networking-examples/handoff6/handoff.ldgvnw b/networking-examples/handoff6/handoff.ldgvnw new file mode 100644 index 0000000..0b6860c --- /dev/null +++ b/networking-examples/handoff6/handoff.ldgvnw @@ -0,0 +1,22 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type EmptyConversation : ! ~ssn = Unit +type SendEmptyConversation : ! ~ssn = !EmptyConversation.Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Unit +val main = + let con = (connect 4444 (dualof SendEmptyConversation) "127.0.0.1" 4343 ) in + let = recv con in + (empty) diff --git a/networking-examples/handoff6/server.ldgvnw b/networking-examples/handoff6/server.ldgvnw new file mode 100644 index 0000000..fdb5e13 --- /dev/null +++ b/networking-examples/handoff6/server.ldgvnw @@ -0,0 +1,23 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + -- let z = end y in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + -- let c4 = end c3 in + (m + n) + + +val main : Int +val main = + -- let sock = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + add2 con diff --git a/networking-examples/handoff7/add.ldgvnw b/networking-examples/handoff7/add.ldgvnw new file mode 100644 index 0000000..640dc75 --- /dev/null +++ b/networking-examples/handoff7/add.ldgvnw @@ -0,0 +1,23 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendRecvOneInt : ! ~ssn = !(dualof SendOneInt). Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let con = (connect 4100 SendRecvOneInt "127.0.0.1" 4000) in + let con2 = (send con) c2 in + (m) + +val main : Int +val main = + let = (new SendInt) in + let a1 = fork (send2 a) in + add2 b diff --git a/networking-examples/handoff7/handoff.ldgvnw b/networking-examples/handoff7/handoff.ldgvnw new file mode 100644 index 0000000..be92ae9 --- /dev/null +++ b/networking-examples/handoff7/handoff.ldgvnw @@ -0,0 +1,14 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendOneInt : ! ~ssn = !Int. Unit +type SendRecvOneInt : ! ~ssn = !(dualof SendOneInt). Unit + + +val main : Int +val main = + let con = (accept 4000 (dualof SendRecvOneInt)) in + let = recv con in + let = recv recvint in + (n) diff --git a/networking-examples/handoff8/add.ldgvnw b/networking-examples/handoff8/add.ldgvnw new file mode 100644 index 0000000..ba29c78 --- /dev/null +++ b/networking-examples/handoff8/add.ldgvnw @@ -0,0 +1,13 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendAdd : ! ~ssn = !SendInt. !(dualof SendInt). Unit + +val main : Unit +val main = + let = (new SendInt) in + let con = (connect 4100 SendAdd "127.0.0.1" 4000) in + let con2 = (send con) a in + let con3 = (send con2) b in + () diff --git a/networking-examples/handoff8/handoff.ldgvnw b/networking-examples/handoff8/handoff.ldgvnw new file mode 100644 index 0000000..bf009e3 --- /dev/null +++ b/networking-examples/handoff8/handoff.ldgvnw @@ -0,0 +1,24 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type SendAdd : ! ~ssn = !SendInt. !(dualof SendInt). Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val main : Int +val main = + let con = (accept 4000 (dualof SendAdd)) in + let = recv con in + let = recv con2 in + let a1 = fork (send2 a) in + add2 b + diff --git a/networking-examples/recursion/client.ldgvnw b/networking-examples/recursion/client.ldgvnw new file mode 100644 index 0000000..d6b21cc --- /dev/null +++ b/networking-examples/recursion/client.ldgvnw @@ -0,0 +1,45 @@ +type End : ~unit = Unit + +type SUMC : ~ssn = + ?(n : Nat) + natrec n + { !Int. End + , A. ?Int. A + } + +type SUM : ~ssn = + !(n : Nat) + natrec n + { ?Int. End + , A. !Int. A + } + +-- sum up incoming numbers +val sum (ch_in : SUMC) : End = + let = recv ch_in in + (natrec n + { fn (m : Int) fn (c : !Int.End) + send c m + , n1 . A . (y : (m : Int) -> (a:A) -> End) . + fn (m: Int) fn (c : ?Int. A) + let = recv c in + y (k + m) c + } + ) 0 ch + +-- sends the numbers n to 1 +val sendsum (ch_out : SUM) (n : Nat) : Int = + let ch = send ch_out n in + (natrec n + { fn (c : ?Int.End) + fst (recv c) + , n1 . A . (y : (a:A) -> Int) . + fn (c : !Int. A) + y (send c (n1 + 1)) + }) ch + +-- | the summation should be (n^2 + n) / 2 -> with 1000 it should return 500500 +val main : End +val main = + let a = (connect 4100 SUMC "127.0.0.1" 4000) in + sum a diff --git a/networking-examples/recursion/server.ldgvnw b/networking-examples/recursion/server.ldgvnw new file mode 100644 index 0000000..235f0ff --- /dev/null +++ b/networking-examples/recursion/server.ldgvnw @@ -0,0 +1,45 @@ +type End : ~unit = Unit + +type SUMC : ~ssn = + ?(n : Nat) + natrec n + { !Int. End + , A. ?Int. A + } + +type SUM : ~ssn = + !(n : Nat) + natrec n + { ?Int. End + , A. !Int. A + } + +-- sum up incoming numbers +val sum (ch_in : SUMC) : End = + let = recv ch_in in + (natrec n + { fn (m : Int) fn (c : !Int.End) + send c m + , n1 . A . (y : (m : Int) -> (a:A) -> End) . + fn (m: Int) fn (c : ?Int. A) + let = recv c in + y (k + m) c + } + ) 0 ch + +-- sends the numbers n to 1 +val sendsum (ch_out : SUM) (n : Nat) : Int = + let ch = send ch_out n in + (natrec n + { fn (c : ?Int.End) + fst (recv c) + , n1 . A . (y : (a:A) -> Int) . + fn (c : !Int. A) + y (send c (n1 + 1)) + }) ch + +-- | the summation should be (n^2 + n) / 2 -> with 1000 it should return 500500 +val main : Int +val main = + let b = (accept 4000 (dualof SUMC)) in + sendsum b 1000 diff --git a/networking-examples/sendString/client.ldgvnw b/networking-examples/sendString/client.ldgvnw new file mode 100644 index 0000000..95bae13 --- /dev/null +++ b/networking-examples/sendString/client.ldgvnw @@ -0,0 +1,8 @@ +type SendString : ! ~ssn = !String. ?String. Unit + +val main : String +val main = + let con = (connect 4343 SendString "127.0.0.1" 4242 ) in + let con2 = (send con) "Hello" in + let = recv con2 in + (world) diff --git a/networking-examples/sendString/server.ldgvnw b/networking-examples/sendString/server.ldgvnw new file mode 100644 index 0000000..10f7345 --- /dev/null +++ b/networking-examples/sendString/server.ldgvnw @@ -0,0 +1,9 @@ +type SendString : ! ~ssn = !String. ?String. Unit + +val main : String +val main = + let con = (accept 4242 (dualof SendString)) in + let = recv con in + let con3 = (send con2) "world" in + (hello) + diff --git a/networking-examples/simple/client.ldgvnw b/networking-examples/simple/client.ldgvnw new file mode 100644 index 0000000..67e9412 --- /dev/null +++ b/networking-examples/simple/client.ldgvnw @@ -0,0 +1,50 @@ +type End : ~unit = Unit + + +type EOS : ! ~un = {'EOS} +type End : ! ~unit = Unit + +type TClient : ! ~ssn = + !( l : {'neg, 'add}) + case l of + { 'neg : !Int. ?Int. ?EOS. End + , 'add : !Int. !Int. ?Int. ?EOS. End + } + +type LClient : ! ~ssn = + !{'neg}. !Int. ?Int. ?EOS. End + +val lClient (d : TClient) (x : Int) : Int = + let d1 = (send d) 'neg in + let d2 = (send d1) x in + let = recv d2 in + let = recv d3 in + -- let zzz = end zz in + r + +type TServer : ! ~ssn = + ? ( x : { 'neg, 'add }) + case x of + { 'neg : ?Int. !Int. !EOS. End + , 'add : ?Int. ?Int. !Int. !EOS. End + } + +val lServer (c : TServer) : End = + let < l , c1 > = recv c in + let < x , c2 > = recv c1 in + case l of + { 'neg : + let c3 = send c2 (-x) in + send c3 'EOS + + , 'add : + let < y , c3 > = recv c2 in + let c4 = send c3 (x + y) in + send c4 'EOS + } + +val main : Int +val main = + let sock = 4343 in + let con = (connect sock TClient "127.0.0.1" 4242 ) in + ((lClient con) 42) diff --git a/networking-examples/simple/server.ldgvnw b/networking-examples/simple/server.ldgvnw new file mode 100644 index 0000000..afc1ca4 --- /dev/null +++ b/networking-examples/simple/server.ldgvnw @@ -0,0 +1,51 @@ +type End : ~unit = Unit + + +type EOS : ! ~un = {'EOS} +type End : ! ~unit = Unit + +type TClient : ! ~ssn = + !( l : {'neg, 'add}) + case l of + { 'neg : !Int. ?Int. ?EOS. End + , 'add : !Int. !Int. ?Int. ?EOS. End + } + +type LClient : ! ~ssn = + !{'neg}. !Int. ?Int. ?EOS. End + +val lClient (d : TClient) (x : Int) : Int = + let d1 = (send d) 'neg in + let d2 = (send d1) x in + let = recv d2 in + let = recv d3 in + -- let zzz = end zz in + r + +type TServer : ! ~ssn = + ? ( x : { 'neg, 'add }) + case x of + { 'neg : ?Int. !Int. !EOS. End + , 'add : ?Int. ?Int. !Int. !EOS. End + } + +val lServer (c : TServer) : End = + let < l , c1 > = recv c in + let < x , c2 > = recv c1 in + case l of + { 'neg : + let c3 = send c2 (-x) in + send c3 'EOS + , 'add : + let < y , c3 > = recv c2 in + let c4 = send c3 (x + y) in + send c4 'EOS + } + +val main : Unit +val main = + let sock = 4242 in + let con = (accept sock (dualof TClient)) in + let e = lServer con in + -- let ee = end e in + () diff --git a/networking-examples/twoCons/client.ldgvnw b/networking-examples/twoCons/client.ldgvnw new file mode 100644 index 0000000..1db9891 --- /dev/null +++ b/networking-examples/twoCons/client.ldgvnw @@ -0,0 +1,29 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type ComInt : ! ~ssn = !Int. ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + (m + n) + +val com2C (c2: ComInt) = + let x = ((send c2) 1337) in + let = recv x in + (n) + +val main : Int +val main = + let con = (connect 4343 SendInt "127.0.0.1" 4242 ) in + let con2 = (connect 4343 ComInt "127.0.0.1" 4242 ) in + let s2 = fork (send2 con) in + com2C con2 + + diff --git a/networking-examples/twoCons/server.ldgvnw b/networking-examples/twoCons/server.ldgvnw new file mode 100644 index 0000000..96e37df --- /dev/null +++ b/networking-examples/twoCons/server.ldgvnw @@ -0,0 +1,29 @@ +-- Simple example of Label-Dependent Session Types +-- Interprets addition of two numbers + +type SendInt : ! ~ssn = !Int. !Int. Unit +type ComInt : ! ~ssn = !Int. ?Int. Unit + +val send2 (c: SendInt) = + let x = ((send c) 1) in + let y = ((send x) 42) in + () + +val add2 (c1: dualof SendInt) = + let = recv c1 in + let = recv c2 in + () + +val com2S (c2: dualof ComInt) = + let = recv c2 in + let y = (send x) 42 in + (n) + +val main : Int +val main = + -- let sock = (create 4242) in + let con = (accept 4242 (dualof SendInt)) in + let con2 = (accept 4242 (dualof ComInt)) in + let a2 = fork (add2 con) in + let cS = com2S con2 in + (cS) diff --git a/networking-tests/testAdd.sh b/networking-tests/testAdd.sh new file mode 100644 index 0000000..f692519 --- /dev/null +++ b/networking-tests/testAdd.sh @@ -0,0 +1,2 @@ +clear; echo "Add"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/add/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/add/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testBidirectional.sh b/networking-tests/testBidirectional.sh new file mode 100644 index 0000000..444e8ce --- /dev/null +++ b/networking-tests/testBidirectional.sh @@ -0,0 +1,2 @@ +clear; echo "Bidirectional"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirectional/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirectional/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testBidirhandoff.sh b/networking-tests/testBidirhandoff.sh new file mode 100644 index 0000000..07ec1fc --- /dev/null +++ b/networking-tests/testBidirhandoff.sh @@ -0,0 +1,2 @@ +clear; echo "Bidirhandoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirhandoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/serverhandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/clienthandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testHandoff.sh b/networking-tests/testHandoff.sh new file mode 100644 index 0000000..b68f9fc --- /dev/null +++ b/networking-tests/testHandoff.sh @@ -0,0 +1,2 @@ +clear; echo "Handoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testHandoff2.sh b/networking-tests/testHandoff2.sh new file mode 100644 index 0000000..667955e --- /dev/null +++ b/networking-tests/testHandoff2.sh @@ -0,0 +1,2 @@ +clear; echo "Handoff2"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff2/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testLDGVTests.sh b/networking-tests/testLDGVTests.sh new file mode 100644 index 0000000..ee81327 --- /dev/null +++ b/networking-tests/testLDGVTests.sh @@ -0,0 +1,21 @@ +clear; echo "add"; stack run ldgv -- interpret < ../examples/add.ldgv +clear; echo "case-singleton"; stack run ldgv -- interpret < ../examples/case-singleton.ldgv +clear; echo "casesub"; stack run ldgv -- interpret < ../examples/casesub.ldgv +clear; echo "casetest"; stack run ldgv -- interpret < ../examples/casetest.ldgv +clear; echo "casts"; stack run ldgv -- interpret < ../examples/casts.ccldgv +clear; echo "depcast"; stack run ldgv -- interpret < ../examples/depcast.ccldgv +clear; echo "depsum"; stack run ldgv -- interpret < ../examples/depsum.ldgv +clear; echo "just-f2"; stack run ldgv -- interpret < ../examples/just-f2.ccldgv +clear; echo "just-f3"; stack run ldgv -- interpret < ../examples/just-f3.ccldgv +clear; echo "mymap"; stack run ldgv -- interpret < ../examples/mymap.gldgv +clear; echo "natsum"; stack run ldgv -- interpret < ../examples/natsum.ldgv +clear; echo "natsum2-new"; stack run ldgv -- interpret < ../examples/natsum2-new.ldgv +clear; echo "natsum2-rec"; stack run ldgv -- interpret < ../examples/natsum2-rec.ldgv +clear; echo "natsum2"; stack run ldgv -- interpret < ../examples/natsum2.ldgv +clear; echo "node"; stack run ldgv -- interpret < ../examples/node.ldgv +clear; echo "noderec"; stack run ldgv -- interpret < ../examples/noderec.ldgv +clear; echo "person"; stack run ldgv -- interpret < ../examples/person.gldgv +clear; echo "simple_recursion"; stack run ldgv -- interpret < ../examples/simple_recursion.ldgv +clear; echo "simple"; stack run ldgv -- interpret < ../examples/simple.ldgv +# clear; echo "tclient"; stack run ldgv -- interpret < ../examples/tclient.ldgv +# clear; echo "tserver"; stack run ldgv -- interpret < ../examples/tserver.ldgv \ No newline at end of file diff --git a/networking-tests/testNWCount.sh b/networking-tests/testNWCount.sh new file mode 100644 index 0000000..8461e86 --- /dev/null +++ b/networking-tests/testNWCount.sh @@ -0,0 +1,17 @@ +for i in {1..10}; do + clear; echo "$i Add"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/add/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/add/client.ldgvnw & wait); + clear; echo "$i SendString"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/sendString/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/sendString/client.ldgvnw & wait); + clear; echo "$i TwoCons"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/twoCons/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/twoCons/client.ldgvnw & wait); + clear; echo "$i Add2"; stack run ldgv -- interpret ../networking-examples/add2/add.ldgvnw + clear; echo "$i Simple"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/simple/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/simple/client.ldgvnw & wait); + clear; echo "$i Bidirectional"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirectional/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirectional/client.ldgvnw & wait); + clear; echo "$i Handoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/client.ldgvnw & wait); + clear; echo "$i Handoff2"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff2/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/client.ldgvnw & wait); + clear; echo "$i Handoff3"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff3/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/client.ldgvnw & wait); + clear; echo "$i Handoff4"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff4/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/client.ldgvnw & wait); + clear; echo "$i Handoff5"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff5/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff5/handoff.ldgvnw & wait); + clear; echo "$i Handoff6"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff6/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/client.ldgvnw & wait); + clear; echo "$i Handoff7"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff7/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff7/handoff.ldgvnw & wait); + clear; echo "$i Handoff8"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff8/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff8/handoff.ldgvnw & wait); + clear; echo "$i Bidirhandoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirhandoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/serverhandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/clienthandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testNWCountHigh.sh b/networking-tests/testNWCountHigh.sh new file mode 100644 index 0000000..be538bd --- /dev/null +++ b/networking-tests/testNWCountHigh.sh @@ -0,0 +1,17 @@ +for i in {1..20000}; do + clear; echo "$i Add"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/add/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/add/client.ldgvnw & wait); + clear; echo "$i SendString"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/sendString/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/sendString/client.ldgvnw & wait); + clear; echo "$i TwoCons"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/twoCons/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/twoCons/client.ldgvnw & wait); + clear; echo "$i Add2"; stack run ldgv -- interpret ../networking-examples/add2/add.ldgvnw + clear; echo "$i Simple"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/simple/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/simple/client.ldgvnw & wait); + clear; echo "$i Bidirectional"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirectional/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirectional/client.ldgvnw & wait); + clear; echo "$i Handoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff/client.ldgvnw & wait); + clear; echo "$i Handoff2"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff2/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff2/client.ldgvnw & wait); + clear; echo "$i Handoff3"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff3/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/client.ldgvnw & wait); + clear; echo "$i Handoff4"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff4/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/client.ldgvnw & wait); + clear; echo "$i Handoff5"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff5/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff5/handoff.ldgvnw & wait); + clear; echo "$i Handoff6"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff6/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/client.ldgvnw & wait); + clear; echo "$i Handoff7"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff7/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff7/handoff.ldgvnw & wait); + clear; echo "$i Handoff8"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff8/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff8/handoff.ldgvnw & wait); + clear; echo "$i Bidirhandoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirhandoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/serverhandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/clienthandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenAdd2.sh b/networking-tests/testOftenAdd2.sh new file mode 100644 index 0000000..1fbfcd0 --- /dev/null +++ b/networking-tests/testOftenAdd2.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Add2"; stack run ldgv -- interpret ../networking-examples/add2/add.ldgvnw +done \ No newline at end of file diff --git a/networking-tests/testOftenBidirhandoff.sh b/networking-tests/testOftenBidirhandoff.sh new file mode 100644 index 0000000..4ed3faf --- /dev/null +++ b/networking-tests/testOftenBidirhandoff.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Bidirhandoff"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/bidirhandoff/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/serverhandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/clienthandoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/bidirhandoff/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff.sh b/networking-tests/testOftenHandoff.sh new file mode 100644 index 0000000..90397fb --- /dev/null +++ b/networking-tests/testOftenHandoff.sh @@ -0,0 +1,3 @@ +for i in {1..1000}; do + bash testHandoff.sh; +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff2.sh b/networking-tests/testOftenHandoff2.sh new file mode 100644 index 0000000..4496b1a --- /dev/null +++ b/networking-tests/testOftenHandoff2.sh @@ -0,0 +1,3 @@ +for i in {1..100}; do + bash testHandoff2.sh; +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff3.sh b/networking-tests/testOftenHandoff3.sh new file mode 100644 index 0000000..df35f25 --- /dev/null +++ b/networking-tests/testOftenHandoff3.sh @@ -0,0 +1,3 @@ +for i in {1..200000}; do + clear; echo "$i Handoff3"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff3/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff3/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff4.sh b/networking-tests/testOftenHandoff4.sh new file mode 100644 index 0000000..97c4da1 --- /dev/null +++ b/networking-tests/testOftenHandoff4.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Handoff4"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff4/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff4/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff5.sh b/networking-tests/testOftenHandoff5.sh new file mode 100644 index 0000000..763a153 --- /dev/null +++ b/networking-tests/testOftenHandoff5.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Handoff5"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff5/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff5/handoff.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff6.sh b/networking-tests/testOftenHandoff6.sh new file mode 100644 index 0000000..9881943 --- /dev/null +++ b/networking-tests/testOftenHandoff6.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Handoff6"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff6/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/handoff.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff6/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff7.sh b/networking-tests/testOftenHandoff7.sh new file mode 100644 index 0000000..fe3df5c --- /dev/null +++ b/networking-tests/testOftenHandoff7.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Handoff7"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff7/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff7/handoff.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenHandoff8.sh b/networking-tests/testOftenHandoff8.sh new file mode 100644 index 0000000..0197163 --- /dev/null +++ b/networking-tests/testOftenHandoff8.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i Handoff8"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/handoff8/add.ldgvnw & stack run ldgv -- interpret < ../networking-examples/handoff8/handoff.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testOftenRecursion.sh b/networking-tests/testOftenRecursion.sh new file mode 100644 index 0000000..8fc4f73 --- /dev/null +++ b/networking-tests/testOftenRecursion.sh @@ -0,0 +1,3 @@ +for i in {1..10}; do + bash testRecursion.sh; +done \ No newline at end of file diff --git a/networking-tests/testOftenTwoCons.sh b/networking-tests/testOftenTwoCons.sh new file mode 100644 index 0000000..c99e2b1 --- /dev/null +++ b/networking-tests/testOftenTwoCons.sh @@ -0,0 +1,3 @@ +for i in {1..2000}; do + clear; echo "$i TwoCons"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/twoCons/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/twoCons/client.ldgvnw & wait); +done \ No newline at end of file diff --git a/networking-tests/testRecursion.sh b/networking-tests/testRecursion.sh new file mode 100644 index 0000000..fcb64ea --- /dev/null +++ b/networking-tests/testRecursion.sh @@ -0,0 +1,2 @@ +clear; echo "Recursion"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/recursion/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/recursion/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/networking-tests/testSimple.sh b/networking-tests/testSimple.sh new file mode 100644 index 0000000..eaa4bc5 --- /dev/null +++ b/networking-tests/testSimple.sh @@ -0,0 +1,2 @@ +clear; echo "Simple"; (trap 'kill 0' SIGINT; stack run ldgv -- interpret < ../networking-examples/simple/server.ldgvnw & stack run ldgv -- interpret < ../networking-examples/simple/client.ldgvnw & wait); +exit; \ No newline at end of file diff --git a/package.yaml b/package.yaml index 32ba7d4..1a320c2 100644 --- a/package.yaml +++ b/package.yaml @@ -5,12 +5,13 @@ synopsis: Frontend, interpreter and C backend for LDGV/LDST license: BSD3 license-file: LICENSE author: -- Thomas Leyh (CCLDLC implementation) -- Nils Hagner (web frontend, interpreter) -- Janek Spaderna (command line fronted, C backend) -- Peter Thiemann (parser, typechecker) +- "Leon Läufer (LDGVNW implementation)" +- "Thomas Leyh (CCLDLC implementation)" +- "Nils Hagner (web frontend, interpreter)" +- "Janek Spaderna (command line fronted, C backend)" +- "Peter Thiemann (parser, typechecker)" maintainer: "thiemann@informatik.uni-freiburg.de" -copyright: "2019-2021 Chair of Programming Languages, Uni Freiburg" +copyright: "2019-2023 Chair of Programming Languages, Uni Freiburg" ghc-options: - -Wall @@ -60,6 +61,11 @@ library: - transformers - typed-process - validation-selective + - network + - network-run + - random + - SafeSemaphore >=0.10.1 + - directory tests: ldgv-test: diff --git a/src/C/CPS.hs b/src/C/CPS.hs index d796a36..b5f3a70 100644 --- a/src/C/CPS.hs +++ b/src/C/CPS.hs @@ -21,6 +21,7 @@ module C.CPS , Freevars(..) ) where +import Control.Exception import Control.Monad.Cont import Control.Monad.Reader import Data.Foldable @@ -31,6 +32,14 @@ import Syntax hiding (Exp(..)) import qualified Data.Set as Set import qualified Syntax as S +newtype CException = ExpNotImplementedException S.Exp + +instance Show CException where + show = \case + (ExpNotImplementedException e) -> "ExpNotImplementedException: Expression " ++ show e ++ " is not yet compilable to C" + +instance Exception CException + data Val = Lit Literal | Var Ident @@ -121,7 +130,7 @@ fromExp :: S.Exp -> (Val -> Reader Vars Exp) -> Reader Vars Exp fromExp e = runContT (fromExpC e) fromExpC :: S.Exp -> ContT Exp (Reader Vars) Val -fromExpC = \case +fromExpC expr = case expr of S.Lit l -> pure (Lit l) S.Var v -> do vBound <- isBound v @@ -167,6 +176,8 @@ fromExpC = \case S.Recv e -> do v <- fromExpC e captured $ pure . Recv v . Just + + _ -> throw $ ExpNotImplementedException expr getPair :: (forall a. (a, a) -> a) -> S.Exp -> ContT Exp (Reader Vars) Val getPair f e = do @@ -178,7 +189,7 @@ getPair f e = do LetPair xfst xsnd v <$> bound2 xfst xsnd (k x) fromExp' :: S.Exp -> Reader Vars Exp -fromExp' = \case +fromExp' expr = case expr of S.Var v -> do vBound <- isBound v if vBound @@ -208,6 +219,8 @@ fromExp' = \case e@S.Fork{} -> trivial e e@S.New{} -> trivial e e@S.Send{} -> trivial e + + _ -> throw $ ExpNotImplementedException expr where trivial e = fromExp e (pure . Return) diff --git a/src/Config.hs b/src/Config.hs index 84b948b..c684721 100644 --- a/src/Config.hs +++ b/src/Config.hs @@ -8,15 +8,16 @@ import Control.Monad.IO.Class selected :: String -> Bool selected ident = ident `elem` ["valueEquiv", "subtype"] -data DebugLevel = DebugNone | DebugAll +data DebugLevel = DebugNone | DebugNetwork | DebugAll deriving (Eq, Ord, Show) debugLevel :: DebugLevel ---debugLevel = DebugAll -debugLevel = DebugNone +-- debugLevel = DebugAll +debugLevel = DebugNetwork +-- debugLevel = DebugNone trace :: String -> a -> a -trace s a | debugLevel > DebugNone = D.trace s a +trace s a | debugLevel > DebugNetwork = D.trace s a | otherwise = a traceOnly :: String -> String -> a -> a @@ -30,17 +31,22 @@ traceOnlyM ident s | otherwise = pure () traceM :: Applicative f => String -> f () -traceM s | debugLevel > DebugNone = D.traceM s +traceM s | debugLevel > DebugNetwork = D.traceM s | otherwise = pure () traceShowM :: (Show a, Applicative f) => a -> f () traceShowM = traceM . show traceIO :: MonadIO m => String -> m () -traceIO s | debugLevel > DebugNone = liftIO $ D.traceIO s +traceIO s | debugLevel > DebugNetwork = liftIO $ D.traceIO s | otherwise = pure () +traceNetIO :: MonadIO m => String -> m () +traceNetIO s | debugLevel > DebugNone = liftIO $ D.traceIO s + | otherwise = pure () + + traceSuccess :: (Pretty a, Applicative f) => a -> f () traceSuccess a - | debugLevel > DebugNone = traceM $ "Success: " ++ pshow a + | debugLevel > DebugNetwork = traceM $ "Success: " ++ pshow a | otherwise = traceM "Success" diff --git a/src/Interpreter.hs b/src/Interpreter.hs index 575e9b8..436dff6 100644 --- a/src/Interpreter.hs +++ b/src/Interpreter.hs @@ -1,3 +1,5 @@ + +{-# OPTIONS_GHC -Wno-overlapping-patterns#-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} @@ -11,17 +13,28 @@ module Interpreter import qualified Config as C import Syntax import PrettySyntax -import qualified Control.Concurrent.Chan as Chan -import Control.Concurrent (forkIO) +import qualified Control.Concurrent.MVar as MVar import Data.Foldable (find) -import Data.Maybe (fromJust) +import qualified Data.Map as Map import ProcessEnvironment +import Networking.NetworkingMethod.NetworkingMethodCommon import qualified Control.Monad as M import Control.Monad.Reader as R import Control.Applicative ((<|>)) import Control.Exception import Kinds (Multiplicity(..)) +import qualified Networking.Common as NC +import qualified Networking.Outgoing as NO +import qualified Networking.Incoming as NI + + +import Control.Concurrent +import qualified Networking.NetworkConnection as NCon +import ProcessEnvironmentTypes +import qualified Data.Bifunctor +import Data.Maybe + data InterpreterException = MathException String | LookupException String @@ -31,6 +44,10 @@ data InterpreterException | RecursorNotNatException | NotImplementedException Exp | TypeNotImplementedException Type + | DeserializationException String + | NotAnExpectedValueException String Value + | CommunicationPartnerNotFoundException String + | VChanIsUsedException String deriving Eq instance Show InterpreterException where @@ -43,6 +60,10 @@ instance Show InterpreterException where RecursorNotNatException -> "Recursor only works on natural numbers" (NotImplementedException exp) -> "NotImplementedException: " ++ pshow exp (TypeNotImplementedException typ) -> "TypeNotImplementedException: " ++ pshow typ + (DeserializationException err) -> "DeserializationException: " ++ err + (NotAnExpectedValueException expected val) -> "NotAnExpectedValueException: This expresion: (" ++ pshow val ++ ") is not of type: " ++ expected + (CommunicationPartnerNotFoundException partner) -> "CommunicationPartnerNotFoundException: Partner:" ++ partner ++ " not found" + (VChanIsUsedException chan) -> "VChanIsUsedException: VChan " ++ chan ++ " is already used!" instance Exception InterpreterException @@ -51,15 +72,22 @@ blame exp = throw $ CastException exp -- | interpret the "main" value in an ldgv file given over stdin interpret :: [Decl] -> IO Value -interpret decls = R.runReaderT (interpretDecl decls) [] +interpret decls = do + sockets <- MVar.newMVar Map.empty + vchanconnections <- MVar.newMVar Map.empty + activeConnections <- NC.createActiveConnections + result <- R.runReaderT (interpretDecl decls) ([], (sockets, vchanconnections, activeConnections)) + NO.sendDisconnect activeConnections vchanconnections + NC.sayGoodbye activeConnections + return result interpretDecl :: [Decl] -> InterpretM Value interpretDecl (DFun "main" _ e _:_) = interpret' e -interpretDecl (DFun name [] e _:decls) = interpret' e >>= \v -> local (extendEnv name v) (interpretDecl decls) +interpretDecl (DFun name [] e _:decls) = interpret' e >>= \v -> local (Data.Bifunctor.first (extendEnv name v)) (interpretDecl decls) interpretDecl (DFun name binds e _:decls) = let lambda = foldr (\(mul, id, ty) -> Lam mul id ty) e binds - in interpret' lambda >>= \v -> local (extendEnv name v) (interpretDecl decls) -interpretDecl (DType name _ _ t:decls) = local (extendEnv name $ VType t) (interpretDecl decls) + in interpret' lambda >>= \v -> local (Data.Bifunctor.first (extendEnv name v)) (interpretDecl decls) +interpretDecl (DType name _ _ t:decls) = local (Data.Bifunctor.first (extendEnv name $ VType t)) (interpretDecl decls) interpretDecl (_:decls) = interpretDecl decls interpretDecl [] = throw $ LookupException "main" @@ -73,7 +101,7 @@ interpret' e = ask >>= \penv -> eval :: Exp -> InterpretM Value eval = \case Succ e -> interpretMath $ Add (Lit (LInt 1)) e - Rec f x e1 e0 -> ask >>= \env -> return $ VRec env f x e1 e0 + Rec f x e1 e0 -> ask >>= \(env, _) -> return $ VRec env f x e1 e0 NatRec e1 e2 i1 t1 i2 t e3 -> do -- returns a function indexed over e1 (should be a variable pointing to a Nat) -- e1 should be the recursive variable which gets decreased each time the @@ -85,16 +113,16 @@ eval = \case VInt 0 -> interpret' e2 VInt 1 -> do zero <- interpret' e2 - R.local (extendEnv i1 (VInt 0) . extendEnv i2 zero) (interpret' e3) + R.local (Data.Bifunctor.first (extendEnv i1 (VInt 0) . extendEnv i2 zero)) (interpret' e3) VInt n -> do -- interpret the n-1 case i2 and add it to the env -- together with n before interpreting the body e3 let lowerEnv = extendEnv i1 (VInt $ n-1) - lower <- R.local lowerEnv (interpret' $ NatRec (Var i1) e2 i1 t1 i2 t e3) - R.local (extendEnv i2 lower . lowerEnv) (interpret' e3) + lower <- R.local (Data.Bifunctor.first lowerEnv) (interpret' $ NatRec (Var i1) e2 i1 t1 i2 t e3) + R.local (Data.Bifunctor.first (extendEnv i2 lower . lowerEnv)) (interpret' e3) _ -> throw $ RecursorException "Evaluation of 'natrec x...' must yield Nat value" - NewNatRec f n tid ty ez x es -> ask >>= \env -> return $ VNewNatRec env f n tid ty ez x es - Lam _ i _ e -> ask >>= \env -> return $ VFunc env i e + NewNatRec f n tid ty ez x es -> ask >>= \(env, _) -> return $ VNewNatRec env f n tid ty ez x es + Lam _ i _ e -> ask >>= \(env, sock) -> return $ VFunc env i e cast@(Cast e t1 t2) -> do C.traceIO $ "Interpreting cast expression: " ++ pshow cast v <- interpret' e @@ -106,11 +134,12 @@ eval = \case case v of VPair {} -> do C.traceIO $ "Interpreting pair cast expression: Value(" ++ show v ++ ") NFType(" ++ show nft1 ++ ") NFType(" ++ show nft2 ++ ")" - v' <- lift $ reducePairCast v (toNFPair nft1) (toNFPair nft2) + (env, (sockets, vchanconnections, activeConnections)) <- ask + v' <- lift $ reducePairCast sockets vchanconnections activeConnections v (toNFPair nft1) (toNFPair nft2) maybe (blame cast) return v' _ -> let v' = reduceCast v nft1 nft2 in maybe (blame cast) return v' - Var s -> ask >>= \env -> maybe (throw $ LookupException s) (liftIO . pure) (lookup s env) - Let s e1 e2 -> interpret' e1 >>= \v -> R.local (extendEnv s v) (interpret' e2) + Var s -> ask >>= \(env, _) -> maybe (throw $ LookupException s) (liftIO . pure) (lookup s env) + Let s e1 e2 -> interpret' e1 >>= \v -> R.local (Data.Bifunctor.first (extendEnv s v)) (interpret' e2) Math m -> interpretMath m Lit l -> return (interpretLit l) e@(App e1 e2) -> do @@ -120,45 +149,95 @@ eval = \case interpretApp e val arg Pair mul s e1 e2 -> do v1 <- interpret' e1 - v2 <- R.local (extendEnv s v1) (interpret' e2) + v2 <- R.local (Data.Bifunctor.first (extendEnv s v1)) (interpret' e2) return $ VPair v1 v2 - LetPair s1 s2 e1 e2 -> interpret' e1 >>= \(VPair v1 v2) -> R.local (extendEnv s2 v2 . extendEnv s1 v1) (interpret' e2) + LetPair s1 s2 e1 e2 -> interpret' e1 >>= \(VPair v1 v2) -> R.local (Data.Bifunctor.first (extendEnv s2 v2 . extendEnv s1 v1)) (interpret' e2) fst@(Fst e) -> interpret' e >>= \(VPair s1 s2) -> return s1 snd@(Snd e) -> interpret' e >>= \(VPair s1 s2) -> return s2 Fork e -> do - penv <- ask + (penv, sock) <- ask liftIO $ forkIO (do - res <- R.runReaderT (interpret' e) penv + res <- R.runReaderT (interpret' e) (penv, sock) C.traceIO "Ran a forked operation") return VUnit New t -> do - r <- liftIO Chan.newChan - w <- liftIO Chan.newChan - return $ VPair (VChan r w) (VChan w r) - Send e -> VSend <$> interpret' e + (env, (sockets, vchanconnections, activeConnections)) <- ask + (nc1, nc2) <- liftIO $ NCon.newEmulatedConnection vchanconnections + used1 <- liftIO $ MVar.newMVar False + used2 <- liftIO $ MVar.newMVar False + return $ VPair (VChan nc1 used1) $ VChan nc2 used2 + Send e -> VSend <$> interpret' e -- Apply VSend to the output of interpret' e Recv e -> do - interpret' e >>= \v@(VChan c _) -> do - val <- liftIO $ Chan.readChan c - liftIO $ C.traceIO $ "Read " ++ show val ++ " from Chan " - return $ VPair val v + interpret' e >>= \v@(VChan ci usedmvar) -> do + used <- liftIO $ MVar.readMVar usedmvar + if used then throw $ VChanIsUsedException $ show v else do + (env, (sockets, vchanconnections, activeConnections)) <- ask + socketsraw <- liftIO $ MVar.readMVar sockets + let port = show $ head $ Map.keys socketsraw + val <- liftIO $ NI.receiveValue vchanconnections activeConnections ci port + liftIO $ C.traceIO $ "Read " ++ show val ++ " from Chan, over expression " ++ show e + + -- Disable the old channel and get a new one + newV <- liftIO $ disableOldVChan v + return $ VPair val newV Case e cases -> interpret' e >>= \(VLabel s) -> interpret' $ fromJust $ lookup s cases + Accept e tname -> do + val <- interpret' e + case val of + VInt port -> do + (env, (sockets, vchanconnections, activeConnections)) <- ask + (clientlist, ownport) <- liftIO $ NC.acceptConversations activeConnections NI.handleClient port sockets vchanconnections + t <- case tname of + TName _ s -> maybe (throw $ LookupException s) (\(VType t) -> return t) (lookup s env) + _ -> return tname + + newuser <- liftIO $ NI.findFittingClient clientlist (tname, t) + networkconnectionmap <- liftIO $ MVar.readMVar vchanconnections + case Map.lookup newuser networkconnectionmap of + Nothing -> throw $ CommunicationPartnerNotFoundException newuser + Just networkconnection -> do + used <- liftIO MVar.newEmptyMVar + liftIO $ MVar.putMVar used False + return $ VChan networkconnection used + _ -> throw $ NotAnExpectedValueException "VInt" val + + Connect e0 tname e1 e2-> do + val <- interpret' e0 + case val of + VInt port -> do + (env, (sockets, vchanconnections, activeConnections)) <- ask + (chan, ownport) <- liftIO $ NC.acceptConversations activeConnections NI.handleClient port sockets vchanconnections + addressVal <- interpret' e1 + case addressVal of + VString address -> do + portVal <- interpret' e2 + case portVal of + VInt port -> do + t <- case tname of + TName _ s -> maybe (throw $ LookupException s) (\(VType t) -> return t) (lookup s env) + _ -> return tname + + liftIO $ NO.initialConnect activeConnections vchanconnections address (show port) ownport (tname, t) + _ -> throw $ NotAnExpectedValueException "VInt" portVal + _ -> throw $ NotAnExpectedValueException "VString" addressVal + _ -> throw $ NotAnExpectedValueException "VInt" val e -> throw $ NotImplementedException e -- Exp is only used for blame interpretApp :: Exp -> Value -> Value -> InterpretM Value -interpretApp _ (VFunc env s exp) w = R.local (const $ extendEnv s w env) (interpret' exp) +interpretApp _ (VFunc env s exp) w = R.local (Data.Bifunctor.first (const $ extendEnv s w env)) (interpret' exp) interpretApp e (VFuncCast v (FuncType penv s t1 t2) (FuncType penv' s' t1' t2')) w' = do - env0 <- ask + (env0, socketMVar) <- ask let interpretAppCast :: IO Value interpretAppCast = do C.traceIO ("Attempting function cast in application (" ++ show v ++ ") with (" ++ show w' ++ ")") - nft1 <- R.runReaderT (evalType t1) penv - nft1' <- R.runReaderT (evalType t1') penv' + nft1 <- R.runReaderT (evalType t1) (penv, socketMVar) + nft1' <- R.runReaderT (evalType t1') (penv', socketMVar) w <- maybe (blame e) return (reduceCast w' nft1' nft1) - nft2' <- R.runReaderT (evalType t2') (extendEnv s' w' penv') - nft2 <- R.runReaderT (evalType t2) (extendEnv s w penv) - u <- R.runReaderT (interpretApp e v w) env0 + nft2' <- R.runReaderT (evalType t2') (extendEnv s' w' penv', socketMVar) + nft2 <- R.runReaderT (evalType t2) (extendEnv s w penv, socketMVar) + u <- R.runReaderT (interpretApp e v w) (env0, socketMVar) u' <- maybe (blame e) return (reduceCast u nft2 nft2') C.traceIO ("Function cast in application results in: " ++ show u') return u' @@ -168,14 +247,22 @@ interpretApp e rec@(VRec env f n1 e1 e0) (VInt n) | n == 0 = interpret' e0 | n > 0 = do let env' = extendEnv n1 (VInt (n-1)) (extendEnv f rec env) - R.local (const env') (interpret' e1) + R.local (Data.Bifunctor.first (const env')) (interpret' e1) interpretApp _ natrec@(VNewNatRec env f n1 tid ty ez y es) (VInt n) | n < 0 = throw RecursorNotNatException | n == 0 = interpret' ez | n > 0 = do let env' = extendEnv n1 (VInt (n-1)) (extendEnv f natrec env) - R.local (const env') (interpret' es) -interpretApp _ (VSend v@(VChan _ c)) w = liftIO (Chan.writeChan c w) >> return v + R.local (Data.Bifunctor.first (const env')) (interpret' es) +interpretApp _ (VSend v@(VChan cc usedmvar)) w = do + used <- liftIO $ MVar.readMVar usedmvar + if used then throw $ VChanIsUsedException $ show v else do + (env, (sockets, vchanconnections, activeConnections)) <- ask + socketsraw <- liftIO $ MVar.readMVar sockets + let port = show $ head $ Map.keys socketsraw + liftIO $ NO.sendValue vchanconnections activeConnections cc w port (-2) + -- Disable old VChan + liftIO $ disableOldVChan v interpretApp e _ _ = throw $ ApplicationException e interpretLit :: Literal -> Value @@ -225,14 +312,15 @@ evalType = \case then throw RecursorNotNatException else let lower = TNatRec (Lit $ LNat (n-1)) t1 tid t2 - in R.local (extendEnv tid (VType lower)) (evalType t2) + in do + R.local (Data.Bifunctor.first (extendEnv tid (VType lower))) (evalType t2) _ -> throw $ RecursorException "Evaluation of 'natrec x...' must yield Nat value" - TName _ s -> ask >>= \env -> maybe (throw $ LookupException s) (\(VType t) -> evalType t) (lookup s env) + TName _ s -> ask >>= \(env, _) -> maybe (throw $ LookupException s) (\(VType t) -> evalType t) (lookup s env) TLab ls -> return $ NFGType $ GLabel $ labelsFromList ls TFun m _ TDyn TDyn -> return $ NFGType $ GFunc m - TFun m s t1 t2 -> ask >>= \env -> return $ NFFunc $ FuncType env s t1 t2 + TFun m s t1 t2 -> ask >>= \(env, _) -> return $ NFFunc $ FuncType env s t1 t2 TPair _ TDyn TDyn -> return $ NFGType $ GPair - TPair s t1 t2 -> ask >>= \env -> return $ NFPair $ FuncType env s t1 t2 + TPair s t1 t2 -> ask >>= \(env, _) -> return $ NFPair $ FuncType env s t1 t2 TCase exp labels -> interpret' exp >>= \(VLabel l) -> let entry = find (\(l', _) -> l == l') labels in maybe (return NFBot) (evalType . snd) entry @@ -278,21 +366,21 @@ toNFPair :: NFType -> NFType toNFPair (NFGType (GPair)) = NFPair (FuncType [] "x" TDyn TDyn) toNFPair t = t -reducePairCast :: Value -> NFType -> NFType -> IO (Maybe Value) -reducePairCast (VPair v w) (NFPair (FuncType penv s t1 t2)) (NFPair (FuncType penv' s' t1' t2')) = do - mv' <- reduceComponent v (penv, t1) (penv', t1') +reducePairCast :: MVar.MVar (Map.Map Int ServerSocket) -> VChanConnections -> ActiveConnections -> Value -> NFType -> NFType -> IO (Maybe Value) +reducePairCast sockets vchanconnections activeConnections (VPair v w) (NFPair (FuncType penv s t1 t2)) (NFPair (FuncType penv' s' t1' t2')) = do + mv' <- reduceComponent sockets vchanconnections activeConnections v (penv, t1) (penv', t1') case mv' of Nothing -> return Nothing Just v' -> do - mw' <- reduceComponent w ((s, v) : penv, t2) ((s', v') : penv', t2') + mw' <- reduceComponent sockets vchanconnections activeConnections w ((s, v) : penv, t2) ((s', v') : penv', t2') return $ liftM2 VPair mv' mw' where - reduceComponent :: Value -> (PEnv, Type) -> (PEnv, Type) -> IO (Maybe Value) - reduceComponent v (penv, t) (penv', t') = do - nft <- R.runReaderT (evalType t) penv - nft' <- R.runReaderT (evalType t') penv' + reduceComponent :: MVar.MVar (Map.Map Int ServerSocket) -> VChanConnections -> ActiveConnections -> Value -> (PEnv, Type) -> (PEnv, Type) -> IO (Maybe Value) + reduceComponent sockets vchanconnections activeConnections v (penv, t) (penv', t') = do + nft <- R.runReaderT (evalType t) (penv, (sockets, vchanconnections, activeConnections)) + nft' <- R.runReaderT (evalType t') (penv', (sockets, vchanconnections, activeConnections)) return $ reduceCast v nft nft' -reducePairCast _ _ _ = return Nothing +reducePairCast _ _ _ _ _ _ = return Nothing equalsType :: NFType -> GType -> Bool equalsType (NFFunc (FuncType _ _ TDyn TDyn)) (GFunc _) = True diff --git a/src/Networking/Assert.hs b/src/Networking/Assert.hs new file mode 100644 index 0000000..7385142 --- /dev/null +++ b/src/Networking/Assert.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE LambdaCase #-} + +module Networking.Assert where + +import Control.Exception + + +newtype AssertException = TestErrorAssertEQ String + +instance Show AssertException where + show = \case + TestErrorAssertEQ err -> "AssertException (TestErrorAssertEQ): " ++ err + + +instance Exception AssertException + + +assertEQ :: Eq a => String -> a -> a -> IO () +assertEQ err v1 v2 = if v1==v2 then putStrLn $ "Assertion Success: "++ err else throw $ TestErrorAssertEQ err \ No newline at end of file diff --git a/src/Networking/Buffer.hs b/src/Networking/Buffer.hs new file mode 100644 index 0000000..c41898d --- /dev/null +++ b/src/Networking/Buffer.hs @@ -0,0 +1,229 @@ +{-# LANGUAGE CPP #-} + +module Networking.Buffer where + +{- +Buffer reuses and adapts vast amounts of code from the Control.Concurrent.Chan implementation licenced under: + +----------------------------------------------------------------------------- +-- | +-- Module : Control.Concurrent.Chan +-- Copyright : (c) The University of Glasgow 2001 +-- License : BSD-style (see the file libraries/base/LICENSE) +-- +-- Maintainer : libraries@haskell.org +-- Stability : stable +-- Portability : non-portable (concurrency) +-- +-- Unbounded channels. +-- +-- The channels are implemented with @MVar@s and therefore inherit all the +-- caveats that apply to @MVar@s (possibility of races, deadlocks etc). The +-- stm (software transactional memory) library has a more robust implementation +-- of channels called @TChan@s. +-- +----------------------------------------------------------------------------- + +This library (libraries/base) is derived from code from several +sources: + + * Code from the GHC project which is largely (c) The University of + Glasgow, and distributable under a BSD-style license (see below), + + * Code from the Haskell 98 Report which is (c) Simon Peyton Jones + and freely redistributable (but see the full license for + restrictions). + + * Code from the Haskell Foreign Function Interface specification, + which is (c) Manuel M. T. Chakravarty and freely redistributable + (but see the full license for restrictions). + +The full text of these licenses is reproduced below. All of the +licenses are BSD-style or compatible. + +----------------------------------------------------------------------------- + +The Glasgow Haskell Compiler License + +Copyright 2004, The University Court of the University of Glasgow. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +- Redistributions of source code must retain the above copyright notice, +this list of conditions and the following disclaimer. + +- Redistributions in binary form must reproduce the above copyright notice, +this list of conditions and the following disclaimer in the documentation +and/or other materials provided with the distribution. + +- Neither name of the University nor the names of its contributors may be +used to endorse or promote products derived from this software without +specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY COURT OF THE UNIVERSITY OF +GLASGOW AND THE CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, +INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND +FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE +UNIVERSITY COURT OF THE UNIVERSITY OF GLASGOW OR THE CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH +DAMAGE. + +----------------------------------------------------------------------------- + +Code derived from the document "Report on the Programming Language +Haskell 98", is distributed under the following license: + + Copyright (c) 2002 Simon Peyton Jones + + The authors intend this Report to belong to the entire Haskell + community, and so we grant permission to copy and distribute it for + any purpose, provided that it is reproduced in its entirety, + including this Notice. Modified versions of this Report may also be + copied and distributed for any purpose, provided that the modified + version is clearly presented as such, and that it does not claim to + be a definition of the Haskell 98 Language. + +----------------------------------------------------------------------------- + +Code derived from the document "The Haskell 98 Foreign Function +Interface, An Addendum to the Haskell 98 Report" is distributed under +the following license: + + Copyright (c) 2002 Manuel M. T. Chakravarty + + The authors intend this Report to belong to the entire Haskell + community, and so we grant permission to copy and distribute it for + any purpose, provided that it is reproduced in its entirety, + including this Notice. Modified versions of this Report may also be + copied and distributed for any purpose, provided that the modified + version is clearly presented as such, and that it does not claim to + be a definition of the Haskell 98 Foreign Function Interface. + +----------------------------------------------------------------------------- +-} + +import Control.Concurrent.MVar +import Control.Exception +import Control.Monad + + + +#define _UPK_(x) {-# UNPACK #-} !(x) + +data Buffer a = Buffer {bufferReadHead :: _UPK_(MVar (Chain a)), bufferSharedWriteHead :: _UPK_(MVar (Chain a))} + deriving Eq + +type Chain a = MVar (Element a) + +data Element a = Element {elementValue :: a, nextElement :: _UPK_(Chain a)} + deriving Eq + +newBuffer :: IO (Buffer a) +newBuffer = do + element <- newEmptyMVar + readHead <- newMVar element + sharedWriteHead <- newMVar element + return $ Buffer readHead sharedWriteHead + +writeBuffer :: Buffer a -> a -> IO () +writeBuffer buffer@(Buffer readVar sharedWriteVar) value = do + newElement <- newEmptyMVar + mask_ $ do + oldElement <- takeMVar sharedWriteVar + putMVar oldElement $ Element value newElement + putMVar sharedWriteVar newElement + +takeBuffer :: Buffer a -> IO a +takeBuffer buffer@(Buffer readVar sharedWriteVar) = do + readHead <- takeMVar readVar + (Element value bufferStart) <- readMVar readHead + putMVar readVar bufferStart + return value + +tryTakeBuffer :: Buffer a -> IO (Maybe a) +tryTakeBuffer buffer@(Buffer readVar sharedWriteVar) = do + mbyReadHead <- tryTakeMVar readVar + case mbyReadHead of + Just readHead -> do + mbyElement <- tryReadMVar readHead + case mbyElement of + Just (Element value bufferStart) -> do + putMVar readVar bufferStart + return $ Just value + Nothing -> do + putMVar readVar readHead + return Nothing + Nothing -> return Nothing + +readBuffer :: Buffer a -> IO a +readBuffer bufer@(Buffer readVar sharedWriteVar) = do + readHead <- readMVar readVar + (Element value bufferStart) <- readMVar readHead + return value + +tryReadBuffer :: Buffer a -> IO (Maybe a) +tryReadBuffer buffer@(Buffer readVar sharedWriteVar) = do + mbyReadHead <- tryReadMVar readVar + case mbyReadHead of + Just readHead -> do + mbyElement <- tryReadMVar readHead + case mbyElement of + Just (Element value bufferStart) -> do + return $ Just value + Nothing -> return Nothing + Nothing -> return Nothing + +-- Similar to dupChan in the Base package +duplicateBuffer :: Buffer a -> IO (Buffer a) +duplicateBuffer buffer@(Buffer readVar sharedWriteVar) = do + element <- readMVar sharedWriteVar + newReadVar <- newMVar element + return $ Buffer newReadVar sharedWriteVar + +-- Duplicate Buffer along with contents +cloneBuffer :: Buffer a -> IO (Buffer a) +cloneBuffer buffer@(Buffer readVar sharedWriteVar) = do + element <- readMVar readVar + newReadVar <- newMVar element + return $ Buffer newReadVar sharedWriteVar + +consumeBufferToList :: Buffer a -> IO [a] +consumeBufferToList buffer = do + mbyFirstElement <- tryTakeBuffer buffer + case mbyFirstElement of + Just firstElement -> do + listTail <- consumeBufferToList buffer + return $ firstElement:listTail + Nothing -> return [] + +writeBufferToList :: Buffer a -> IO [a] +writeBufferToList buffer = do + clone <- cloneBuffer buffer + consumeBufferToList clone + +getAt :: Buffer a -> Int -> IO a +getAt buffer count = do + clone <- cloneBuffer buffer + -- Take count-1 times + forM_ [1..count] $ \_ -> takeBuffer clone + takeBuffer clone + +tryGetAt :: Buffer a -> Int -> IO (Maybe a) +tryGetAt buffer count = do + clone <- cloneBuffer buffer + tryGetAtInternal clone count + where + tryGetAtInternal :: Buffer a -> Int -> IO (Maybe a) + tryGetAtInternal buffer count | count <= 0 = tryTakeBuffer buffer + | otherwise = do + mbyVal <- tryTakeBuffer buffer + case mbyVal of + Just val -> tryGetAtInternal buffer $ count-1 + Nothing -> return Nothing \ No newline at end of file diff --git a/src/Networking/Common.hs b/src/Networking/Common.hs new file mode 100644 index 0000000..ddab60b --- /dev/null +++ b/src/Networking/Common.hs @@ -0,0 +1,32 @@ +{-# OPTIONS_GHC -Wno-missing-signatures #-} + +module Networking.Common where + +-- import qualified Networking.NetworkingMethod.Stateless as NetMethod +import qualified Networking.NetworkingMethod.Fast as NetMethod + + +type ConversationOrHandle = NetMethod.Conversation + +-- type ConversationOrHandle = (Handle, (Socket, SockAddr)) + +-- The compiler sadly compains when these things get eta reduced :/ +sendMessage con ser = NetMethod.sendMessage con ser + +sendResponse con ser = NetMethod.sendResponse con ser + +startConversation activeCons host port waitTime tries = NetMethod.startConversation activeCons host port waitTime tries + +waitForConversation activeCons host port waitTime tries = NetMethod.waitForConversation activeCons host port waitTime tries + +createActiveConnections = NetMethod.createActiveConnections + +acceptConversations activeCons connectionhandler port socketsmvar = NetMethod.acceptConversations activeCons connectionhandler port socketsmvar + +receiveResponse con waitTime tries = NetMethod.receiveResponse con waitTime tries + +endConversation con waitTime tries = NetMethod.endConversation con waitTime tries + +sayGoodbye con = NetMethod.sayGoodbye con + +getPartnerHostaddress conv = NetMethod.getPartnerHostaddress conv diff --git a/src/Networking/Incoming.hs b/src/Networking/Incoming.hs new file mode 100644 index 0000000..4732bac --- /dev/null +++ b/src/Networking/Incoming.hs @@ -0,0 +1,299 @@ +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Redundant return" #-} +module Networking.Incoming where + +import Control.Concurrent +import Control.Monad +import Network.Socket +import Networking.Messages +import Networking.NetworkConnection +import ProcessEnvironmentTypes +import qualified Config +import qualified Control.Concurrent.MVar as MVar +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Bifunctor +import qualified Data.Map as Map +import qualified Data.Maybe +import qualified Networking.Common as NC +import qualified Networking.Messages as Messages +import qualified Networking.NetworkBuffer as NB +import qualified Networking.NetworkConnection as NCon +import qualified Networking.NetworkingMethod.NetworkingMethodCommon as NMC +import qualified Networking.Outgoing as NO +import qualified Networking.RandomID as RandomID +import qualified Networking.Serialize as NSerialize +import qualified Syntax + +handleClient :: NMC.ActiveConnections -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Socket, SockAddr) -> NC.ConversationOrHandle -> String -> String -> Message -> IO () +handleClient activeCons mvar clientlist clientsocket hdl ownport message deserialmessages = do + let userid = getUserID deserialmessages + clientHostaddress <- case snd clientsocket of + SockAddrInet _ hostname -> return $ hostaddressTypeToString hostname + _ -> do + receivedNetLog message "Error during receiving a networkmessage: only ipv4 is currently supported!" + return "" + + netcons <- MVar.readMVar mvar + case Map.lookup userid netcons of + Just ncToPartner -> do + receivedNetLog message $ "Received message as: " ++ ncOwnUserID ncToPartner ++ " (" ++ ownport ++ ") from: " ++ ncPartnerUserID ncToPartner + ncIsReady <- isReadyForUse ncToPartner + if ncIsReady then do + busy <- SSem.tryWait $ ncHandlingIncomingMessage ncToPartner + case busy of + Just num -> do + constate <- MVar.readMVar $ ncConnectionState ncToPartner + reply <- case constate of + RedirectRequest _ _ host port _ _ _ -> do + receivedNetLog message $ "Found redirect request for: " ++ userid + receivedNetLog message $ "Send redirect to:" ++ host ++ ":" ++ port + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl (Messages.Redirect host port) + Connected {} -> case deserialmessages of + NewValue userid count val -> do + -- DC.lockInterpreterReads (ncRead ncToPartner) + let fixedPartnerHostAddress = setPartnerHostAddress clientHostaddress val + success <- NB.writeIfNext (ncRead ncToPartner) count fixedPartnerHostAddress + if success then do + receivedNetLog message "Inserting VChans into VChanCons" + insertVChansIntoVChanCons mvar False fixedPartnerHostAddress + receivedNetLog message "Message written to Channel" + else receivedNetLog message "Message not correct" + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Okay + receivedNetLog message "Sent okay" + -- DC.unlockInterpreterReads (ncRead ncToPartner) + RequestValue userid count -> do + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Okay + mbyval <- NB.tryGetAtNB (NCon.ncWrite ncToPartner) count + Data.Maybe.maybe (return False) (\val -> NO.sendNetworkMessage activeCons ncToPartner (Messages.NewValue (ncOwnUserID ncToPartner) count val) 0) mbyval + return () + AcknowledgeValue userid count -> do + NC.sendResponse hdl Messages.Okay -- This okay is needed here to fix a race-condition with disconnects being faster than the okay + -- NB.serialize (ncWrite ncToPartner) >>= \x -> Config.traceNetIO $ "Online before acknowlegment: " ++ show x + NB.updateAcknowledgements (NCon.ncWrite ncToPartner) count + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NewPartnerAddress userid port connectionID -> do + receivedNetLog message $ "Trying to change the address to: " ++ clientHostaddress ++ ":" ++ port + NCon.changePartnerAddress ncToPartner clientHostaddress port connectionID + receivedNetLog message $ "Successfully changed address to: " ++ clientHostaddress ++ ":" ++ port + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Okay + + successSendingResponse <- NO.sendNetworkMessage activeCons ncToPartner (Messages.AcknowledgePartnerAddress (ncOwnUserID ncToPartner) connectionID) $ -2 + when successSendingResponse $ receivedNetLog message "Successfully acknowledged message" + return () + AcknowledgePartnerAddress userid connectionID -> do + conConfirmed <- NCon.confirmConnectionID ncToPartner connectionID + SSem.signal $ ncHandlingIncomingMessage ncToPartner + if conConfirmed then NC.sendResponse hdl Messages.Okay else NC.sendResponse hdl Messages.Error + Disconnect userid -> do + NC.sendResponse hdl Messages.Okay + NCon.disconnectFromPartner ncToPartner + SSem.signal $ ncHandlingIncomingMessage ncToPartner + return () + _ -> do + receivedNetLog message $ "Error unsupported networkmessage: "++ NSerialize.serialize deserialmessages + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Okay + _ -> do + receivedNetLog message "Network Connection is in a illegal state!" + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Okay + return reply + Nothing -> do + receivedNetLog message "Message cannot be handled at the moment! Sending wait response" + SSem.signal $ ncHandlingIncomingMessage ncToPartner + NC.sendResponse hdl Messages.Wait + else do + receivedNetLog message "Found a networkconnection, but it's not ready to be used yet" + NC.sendResponse hdl Messages.Wait + + Nothing -> do + receivedNetLog message "Received message from unknown connection" + case deserialmessages of + Introduce userid clientport synname syntype -> do + serverid <- RandomID.newRandomID + newpeer <- newNetworkConnection userid serverid clientHostaddress clientport userid serverid + NC.sendResponse hdl (Messages.OkayIntroduce serverid) + let repserial = NSerialize.serialize $ Messages.OkayIntroduce serverid + receivedNetLog message $ " Response to "++ userid ++ ": " ++ repserial + + receivedNetLog message "Patching MVar" + netcons <- MVar.takeMVar mvar + MVar.putMVar mvar $ Map.insert userid newpeer netcons + + + clientlistraw <- MVar.takeMVar clientlist + MVar.putMVar clientlist $ clientlistraw ++ [(userid, (synname, syntype))] + -- We must not write clients into the clientlist before adding them to the networkconnectionmap + + _ -> do + receivedNetLog message $ "Error unsupported networkmessage: " ++ NSerialize.serialize deserialmessages + receivedNetLog message "This is probably a timing issue! Lets resend later" + NC.sendResponse hdl Messages.Wait + + + receivedNetLog message "Message successfully handled" + +receivedNetLog :: String -> String -> IO () +receivedNetLog msg info = Config.traceNetIO $ "Received message: "++msg++" \n Status: "++info + +setPartnerHostAddress :: String -> Value -> Value +setPartnerHostAddress address = modifyVChansStatic (handleSerial address) + where + handleSerial :: String -> Value -> Value + handleSerial address input = case input of + VChanSerial r w p o c -> do + let (hostname, port, partnerID) = c + VChanSerial r w p o (if hostname == "" then address else hostname, port, partnerID) + _ -> input -- return input + +waitUntilContactedNewPeers :: VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> Value -> String -> IO () +waitUntilContactedNewPeers vchansmvar activeCons ownNC input ownport = do + contactedPeers <- contactNewPeers vchansmvar activeCons ownport ownNC input + unless contactedPeers $ do + threadDelay 50000 + waitUntilContactedNewPeers vchansmvar activeCons ownNC input ownport + +contactNewPeers :: VChanConnections -> NMC.ActiveConnections -> String -> NetworkConnection Value -> Value -> IO Bool +contactNewPeers vchansmvar activeCons ownport ownNC = searchVChans (handleVChan activeCons ownport ownNC) True (&&) + where + handleVChan :: NMC.ActiveConnections -> String -> NetworkConnection Value -> Value -> IO Bool + handleVChan activeCons ownport ownNC input = case input of + VChan nc bool -> do + connectionState <- MVar.readMVar $ ncConnectionState nc + case connectionState of + Emulated {} -> return True + _ -> do + if csConfirmedConnection connectionState then return True else do + -- Check whether their partner is also registered and connected on this instance, if so convert the connection into a emulated one + success <- NCon.tryConvertToEmulatedConnection vchansmvar nc + unless success $ do + sendSuccess <- NO.sendNetworkMessage activeCons nc (Messages.NewPartnerAddress (ncOwnUserID nc) ownport $ csOwnConnectionID connectionState) $ -2 + unless sendSuccess $ threadDelay 100000 + return success + + _ -> return True + +hostaddressTypeToString :: HostAddress -> String +hostaddressTypeToString hostaddress = do + let (a, b, c, d) = hostAddressToTuple hostaddress + show a ++ "." ++ show b ++ "."++ show c ++ "." ++ show d + +findFittingClientMaybe :: MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Syntax.Type, Syntax.Type) -> IO (Maybe String) +findFittingClientMaybe clientlist desiredType = do + clientlistraw <- MVar.takeMVar clientlist + let newclientlistrawAndReturn = fFCMRaw clientlistraw desiredType + -- We send the name of the type but not the type itself, this needs to change + MVar.putMVar clientlist $ fst newclientlistrawAndReturn + return $ snd newclientlistrawAndReturn + where + fFCMRaw :: [(String, (Syntax.Type, Syntax.Type))] -> (Syntax.Type, Syntax.Type) -> ([(String, (Syntax.Type, Syntax.Type))], Maybe String) + fFCMRaw [] _ = ([], Nothing) + fFCMRaw (x:xs) desiredtype = if compare (snd x) desiredtype then (xs, Just $ fst x) else do + let nextfFCMRaw = fFCMRaw xs desiredtype + Data.Bifunctor.first (x :) nextfFCMRaw + + compare :: (Syntax.Type, Syntax.Type) -> (Syntax.Type, Syntax.Type) -> Bool + compare a@(aName, aType) b@(bName, bType) = aName == Syntax.dualof bName && aType == bType + +-- This halts until a fitting client is found +findFittingClient :: MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Syntax.Type, Syntax.Type) -> IO String +findFittingClient clientlist desiredType = do + mbystring <- findFittingClientMaybe clientlist desiredType + case mbystring of + Just userid -> return userid + Nothing -> do + threadDelay 10000 -- Sleep for 10 ms to not hammer the CPU + findFittingClient clientlist desiredType + +insertVChansIntoVChanCons :: VChanConnections -> Bool -> Value -> IO () +insertVChansIntoVChanCons vchansmvar readyForUse = searchVChans (handleSerial vchansmvar readyForUse) () (\_ _ -> ()) + where + handleSerial :: VChanConnections -> Bool -> Value -> IO () + handleSerial vchansmvar readyForUse input = case input of + VChanSerial r w p o c -> do + networkconnection <- createNetworkConnection r w p o c + setReadyForUse networkconnection readyForUse + Config.traceNetIO $ "Set: " ++ ncOwnUserID networkconnection ++ " not ready for use" + ncmap <- MVar.takeMVar vchansmvar + MVar.putMVar vchansmvar $ Map.insert p networkconnection ncmap + used<- MVar.newEmptyMVar + MVar.putMVar used False + return () + _ -> return () + +replaceVChanSerial :: NMC.ActiveConnections -> VChanConnections -> Value -> IO Value +replaceVChanSerial activeCons mvar input = modifyVChans (handleSerial activeCons mvar) input + where + handleSerial :: NMC.ActiveConnections -> VChanConnections -> Value -> IO Value + handleSerial activeCons mvar input = case input of + VChanSerial r w p o c -> do + ncmap <- MVar.readMVar mvar + case Map.lookup p ncmap of + Nothing -> do + -- We simply need to wait for the other thread to finish + threadDelay 1000 + handleSerial activeCons mvar input + Just nc -> do + setReadyForUse nc True + Config.traceNetIO $ "Set: " ++ ncOwnUserID nc ++ " ready for use" + used <- MVar.newMVar False + return $ VChan nc used + _ -> return input + +receiveValue :: VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> String -> IO Value +receiveValue vchanconsvar activeCons networkconnection ownport = do + receiveValueInternal 0 vchanconsvar activeCons networkconnection ownport + where + receiveValueInternal :: Int -> VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> String -> IO Value + receiveValueInternal count vchanconsvar activeCons networkconnection ownport = do + let readDC = ncRead networkconnection + mbyUnclean <- NB.tryTake readDC + case mbyUnclean of + Just unclean -> do + val <- replaceVChanSerial activeCons vchanconsvar $ fst unclean + waitUntilContactedNewPeers vchanconsvar activeCons networkconnection val ownport + -- msgCount <- DC.unreadMessageStart $ ncRead networkconnection + connectionState <- MVar.readMVar $ ncConnectionState networkconnection + waitTillAcknowledged vchanconsvar activeCons networkconnection $ snd unclean + + return val + Nothing -> if count == 0 then do + msgCount <- NB.getNextOffset $ ncRead networkconnection + connectionState <- MVar.readMVar $ ncConnectionState networkconnection + case connectionState of + Connected {} -> NO.sendNetworkMessage activeCons networkconnection (Messages.RequestValue (ncOwnUserID networkconnection) msgCount) $ -2 + _ -> return True + receiveValueInternal 100 vchanconsvar activeCons networkconnection ownport + else do + threadDelay 5000 + receiveValueInternal (count-1) vchanconsvar activeCons networkconnection ownport + +waitTillAcknowledged :: VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> Int -> IO () +waitTillAcknowledged vcv ac nc vaToAck = do + success <- tryToAcknowledgeValue vcv ac nc vaToAck + unless success $ waitTillAcknowledged vcv ac nc vaToAck + +-- We need to seperate this in case the state of the connection changes to emulated +tryToAcknowledgeValue :: VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> Int -> IO Bool +tryToAcknowledgeValue vchanconsvar activeCons networkconnection valueToAcknowledge = do + connectionState <- MVar.readMVar $ ncConnectionState networkconnection + case connectionState of + Connected {} -> do + success <- NO.sendNetworkMessage activeCons networkconnection (Messages.AcknowledgeValue (ncOwnUserID networkconnection) valueToAcknowledge) $ -2 + unless success $ threadDelay 100000 -- If sending is not successful give the other party some time to recover + return success + Emulated {} -> do + vchancons <- MVar.readMVar vchanconsvar + let ownid = ncOwnUserID networkconnection + let mbypartner = Map.lookup ownid vchancons + case mbypartner of + Just partner -> do + -- NB.serialize (ncWrite partner) >>= \x -> Config.traceNetIO $ "Emulated "++ show unclean ++ " before acknowledgment: " ++ show x + NB.updateAcknowledgements (ncWrite partner) valueToAcknowledge + return True + _ -> Config.traceNetIO "Something went wrong when acknowledging value of emulated connection" >> return False + _ -> return True \ No newline at end of file diff --git a/src/Networking/Messages.hs b/src/Networking/Messages.hs new file mode 100644 index 0000000..2c9bdaf --- /dev/null +++ b/src/Networking/Messages.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE LambdaCase #-} + +module Networking.Messages where + +import ProcessEnvironmentTypes +import Syntax + +type UserID = String +type Hostname = String +type Port = String +type ConversationID = String +type ConnectionID = String + +data Message + = Introduce UserID Port Type Type + | NewValue UserID Int Value + | RequestValue UserID Int + | AcknowledgeValue UserID Int + | NewPartnerAddress UserID Port ConnectionID + | AcknowledgePartnerAddress UserID ConnectionID + | Disconnect UserID + | AcknowledgeDisconnect UserID -- Vielleicht brauchen wir das nicht mal sehen + deriving Eq + +data Response + = Redirect Hostname Port + | Okay + | OkayIntroduce UserID + | Wait + | Error + +data ConversationSession + = ConversationMessage ConversationID Message + | ConversationResponse ConversationID Response + | ConversationCloseAll + + +getUserID :: Message -> String +getUserID = \case + Introduce p _ _ _ -> p + NewValue p _ _ -> p + RequestValue p _ -> p + AcknowledgeValue p _ -> p + NewPartnerAddress p _ _ -> p + AcknowledgePartnerAddress p _ -> p + Disconnect p -> p + AcknowledgeDisconnect p -> p diff --git a/src/Networking/NetworkBuffer.hs b/src/Networking/NetworkBuffer.hs new file mode 100644 index 0000000..d80f1bc --- /dev/null +++ b/src/Networking/NetworkBuffer.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE LambdaCase #-} + +module Networking.NetworkBuffer where + +import Control.Concurrent.MVar +import Control.Exception +import Control.Monad +import Data.Functor +import Networking.Buffer +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Maybe + +data NetworkBuffer a = NetworkBuffer {buffer :: Buffer a, bufferOffset :: MVar Int, bufferAllMessagesLength :: MVar Int, working :: SSem.SSem} + deriving Eq + +data NetworkBufferSerial a = NetworkBufferSerial {serialList :: [a], serialBufferOffset :: Int, serialBufferAllMessagesLength :: Int} + deriving (Show, Eq) + +type MinimalNetworkBufferSerial a = ([a], Int, Int) + +data NetworkBufferException = InvalidAcknowledgementCount Int Int + | InvalidNetworkBufferState Int Int Int + +instance Show NetworkBufferException where + show = \case + InvalidAcknowledgementCount found requested -> "NetworkBufferException (InvalidAcknowledgement): Only " ++ show found ++ " values found, out of the requested " ++ show requested ++ " values to acknowledge!" + InvalidNetworkBufferState len offset allMsgs -> "NetworkBufferException (InvalidNetworkBufferState): List Length " ++ show len ++ " + " ++ show offset ++ " need to equal " ++ show allMsgs ++ "!" + +instance Exception NetworkBufferException + +newNetworkBuffer :: IO (NetworkBuffer a) +newNetworkBuffer = do + buf <- newBuffer + count <- newMVar 0 + allMessages <- newMVar 0 + work <- SSem.new 1 + return $ NetworkBuffer buf count allMessages work + +write :: NetworkBuffer a -> a -> IO Int +write nb value = SSem.withSem (working nb) $ modifyMVar (bufferAllMessagesLength nb) $ \len -> do + writeBuffer (buffer nb) value + return (len+1, len) + +writeIfNext :: NetworkBuffer a -> Int -> a -> IO Bool +writeIfNext nb index value = SSem.withSem (working nb) $ modifyMVar (bufferAllMessagesLength nb) $ \len -> if index == len then do + writeBuffer (buffer nb) value + return (len+1, True) else return (len, False) + +tryGetAtNB :: NetworkBuffer a -> Int -> IO (Maybe a) +tryGetAtNB nb count = SSem.withSem (working nb) $ do + offset <- readMVar $ bufferOffset nb + tryGetAt (buffer nb) (count-offset) + +tryGetAtRelativeNB :: NetworkBuffer a -> Int -> IO (Maybe a) +tryGetAtRelativeNB nb count = SSem.withSem (working nb) $ do + tryGetAt (buffer nb) count + +tryTake :: NetworkBuffer a -> IO (Maybe (a, Int)) +tryTake nb = SSem.withSem (working nb) $ modifyMVar (bufferOffset nb) (\offset -> do + mbyTakeValue <- tryTakeBuffer (buffer nb) + case mbyTakeValue of + Just value -> return (offset+1, Just (value, offset)) + Nothing -> return (offset, Nothing) + ) + +getNextOffset :: NetworkBuffer a -> IO Int +getNextOffset = readMVar . bufferOffset + +isAllAcknowledged :: NetworkBuffer a -> IO Bool +isAllAcknowledged nb = do + mbyBuffer <- tryReadBuffer $ buffer nb + return $ Data.Maybe.isNothing mbyBuffer + +updateAcknowledgements :: NetworkBuffer a -> Int -> IO () +updateAcknowledgements nb target = SSem.withSem (working nb) $ modifyMVar_ (bufferOffset nb) (\offset -> do + updateAcknowledgementsInternal (buffer nb) target offset + return $ target+1 + ) + where + updateAcknowledgementsInternal :: Buffer a -> Int -> Int -> IO () + updateAcknowledgementsInternal buf target current | target < current = return () + | otherwise = do + mbyTake <- tryTakeBuffer buf + case mbyTake of + Just _ -> updateAcknowledgementsInternal buf target $ current+1 + Nothing -> throw $ InvalidAcknowledgementCount current target + +serialize :: NetworkBuffer a -> IO (NetworkBufferSerial a) +serialize nb = SSem.withSem (working nb) $ do + list <- writeBufferToList $ buffer nb + offset <- readMVar $ bufferOffset nb + allMsgs <- readMVar $ bufferAllMessagesLength nb + return $ NetworkBufferSerial list offset allMsgs + + + +deserialize :: NetworkBufferSerial a -> IO (NetworkBuffer a) +deserialize nbs@(NetworkBufferSerial list offset allMsgs ) = do + when (length list + offset/=allMsgs) $ throw $ InvalidNetworkBufferState (length list) offset allMsgs + buffer <- newBuffer + -- Write all the values to buffer + foldM_ (\x y -> writeBuffer x y >> return x) buffer list + bOffset <- newMVar offset + bAllMsgs <- newMVar allMsgs + work <- SSem.new 1 + return $ NetworkBuffer buffer bOffset bAllMsgs work + +expandSerial :: MinimalNetworkBufferSerial a -> NetworkBufferSerial a +expandSerial (list, readC, ackC) = NetworkBufferSerial list readC ackC + +compressSerial :: NetworkBufferSerial a -> MinimalNetworkBufferSerial a +compressSerial (NetworkBufferSerial list readC ackC) = (list, readC, ackC) + +serializeMinimal :: NetworkBuffer a -> IO (MinimalNetworkBufferSerial a) +serializeMinimal nb = serialize nb <&> compressSerial + +deserializeMinimal :: MinimalNetworkBufferSerial a -> IO (NetworkBuffer a) +deserializeMinimal = deserialize . expandSerial \ No newline at end of file diff --git a/src/Networking/NetworkConnection.hs b/src/Networking/NetworkConnection.hs new file mode 100644 index 0000000..0c93c21 --- /dev/null +++ b/src/Networking/NetworkConnection.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE BlockArguments #-} +module Networking.NetworkConnection where + +import Networking.NetworkBuffer +import Networking.RandomID +import qualified Control.Concurrent.MVar as MVar +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Map as Map + +data NetworkConnection a = NetworkConnection {ncRead :: NetworkBuffer a, ncWrite :: NetworkBuffer a, ncPartnerUserID :: String, ncOwnUserID :: String, ncConnectionState :: MVar.MVar ConnectionState, ncHandlingIncomingMessage :: SSem.SSem, ncReadyToBeUsed :: MVar.MVar Bool} + deriving Eq + +data ConnectionState = Connected {csHostname :: String, csPort :: String, csPartnerConnectionID :: String, csOwnConnectionID :: String, csConfirmedConnection :: Bool} + | Disconnected {csHostname :: String, csPort :: String, csPartnerConnectionID :: String, csOwnConnectionID :: String, csConfirmedConnection :: Bool} + | Emulated {csPartnerConnectionID :: String, csOwnConnectionID :: String, csConfirmedConnection :: Bool} + | RedirectRequest {csHostname :: String, csPort :: String, csRedirectHostname :: String, csRedirectPort :: String, csPartnerConnectionID :: String, csOwnConnectionID :: String, csConfirmedConnection :: Bool} -- Asks to redirect to this connection + deriving (Eq, Show) + + +newNetworkConnection :: String -> String -> String -> String -> String -> String -> IO (NetworkConnection a) +newNetworkConnection partnerID ownID hostname port partnerConnectionID ownConnectionID = do + read <- newNetworkBuffer + write <- newNetworkBuffer + connectionstate <- MVar.newMVar $ Connected hostname port partnerConnectionID ownConnectionID True + incomingMsg <- SSem.new 1 + readyForUse <- MVar.newMVar True + return $ NetworkConnection read write partnerID ownID connectionstate incomingMsg readyForUse + + +createNetworkConnection :: ([a], Int, Int) -> ([a], Int, Int) -> String -> String -> (String, String, String) -> IO (NetworkConnection a) +createNetworkConnection (readList, readOffset, readLength) (writeList, writeOffset, writeLength) partnerID ownID (hostname, port, partnerConnectionID) = do + read <- deserializeMinimal (readList, readOffset, readLength) + write <- deserializeMinimal (writeList, writeOffset, writeLength) + ownConnectionID <- newRandomID + connectionstate <- if port=="" then + MVar.newMVar $ Disconnected "" "" partnerConnectionID ownConnectionID True + else + MVar.newMVar $ Connected hostname port partnerConnectionID ownConnectionID False + incomingMsg <- SSem.new 1 + readyForUse <- MVar.newMVar True + return $ NetworkConnection read write partnerID ownID connectionstate incomingMsg readyForUse + +setReadyForUse :: NetworkConnection a -> Bool -> IO () +setReadyForUse nc ready = do + old <- MVar.takeMVar (ncReadyToBeUsed nc) + MVar.putMVar (ncReadyToBeUsed nc) ready + -- putStrLn $ "setReadyForUse for: " ++ ncOwnUserID nc ++ " was: " ++ show old ++ " now is: " ++ show ready + + +isReadyForUse :: NetworkConnection a -> IO Bool +isReadyForUse nc = MVar.readMVar $ ncReadyToBeUsed nc + +newEmulatedConnection :: MVar.MVar (Map.Map String (NetworkConnection a)) -> IO (NetworkConnection a, NetworkConnection a) +newEmulatedConnection mvar = do + ncmap <- MVar.takeMVar mvar + read <- newNetworkBuffer + write <- newNetworkBuffer + read2 <- newNetworkBuffer + write2 <- newNetworkBuffer + connectionid1 <- newRandomID + connectionid2 <- newRandomID + connectionstate <- MVar.newMVar $ Emulated connectionid2 connectionid1 True + connectionstate2 <- MVar.newMVar $ Emulated connectionid1 connectionid2 True + userid <- newRandomID + userid2 <- newRandomID + incomingMsg <- SSem.new 1 + incomingMsg2 <- SSem.new 1 + readyForUse1 <- MVar.newMVar True + readyForUse2 <- MVar.newMVar True + let nc1 = NetworkConnection read write userid2 userid connectionstate incomingMsg readyForUse1 + let nc2 = NetworkConnection read2 write2 userid userid2 connectionstate2 incomingMsg2 readyForUse2 + let ncmap1 = Map.insert userid2 nc1 ncmap + let ncmap2 = Map.insert userid nc2 ncmap1 + MVar.putMVar mvar ncmap2 + return (nc1, nc2) + +serializeNetworkConnection :: NetworkConnection a -> IO ([a], Int, Int, [a], Int, Int, String, String, String, String, String) +serializeNetworkConnection nc = do + constate <- MVar.readMVar $ ncConnectionState nc + (readList, readOffset, readLength) <- serializeMinimal $ ncRead nc + (writeList, writeOffset, writeLength) <- serializeMinimal $ ncWrite nc + (address, port, partnerConnectionID) <- case constate of + Connected address port partnerConnectionID _ _ -> return (address, port, partnerConnectionID) + RedirectRequest address port _ _ partnerConnectionID _ _ -> return (address, port, partnerConnectionID) + _ -> return ("", "", csPartnerConnectionID constate) + return (readList, readOffset, readLength, writeList, writeOffset, writeLength, ncPartnerUserID nc, ncOwnUserID nc, address, port, partnerConnectionID) + +changePartnerAddress :: NetworkConnection a -> String -> String -> String -> IO () +changePartnerAddress con hostname port partnerConnectionID = do + oldConnectionState <- MVar.takeMVar $ ncConnectionState con + MVar.putMVar (ncConnectionState con) $ Connected hostname port partnerConnectionID (csOwnConnectionID oldConnectionState) $ csConfirmedConnection oldConnectionState + +disconnectFromPartner :: NetworkConnection a -> IO () +disconnectFromPartner con = do + oldConnectionState <- MVar.takeMVar $ ncConnectionState con + case oldConnectionState of + Emulated {} -> + MVar.putMVar (ncConnectionState con) $ Disconnected "" "" (csPartnerConnectionID oldConnectionState) (csOwnConnectionID oldConnectionState) True + _ -> MVar.putMVar (ncConnectionState con) $ Disconnected (csHostname oldConnectionState) (csPort oldConnectionState) (csPartnerConnectionID oldConnectionState) (csOwnConnectionID oldConnectionState) True + +isConnectionConfirmed :: NetworkConnection a -> IO Bool +isConnectionConfirmed con = do + conState <- MVar.readMVar $ ncConnectionState con + return $ csConfirmedConnection conState + +confirmConnectionID :: NetworkConnection a -> String -> IO Bool +confirmConnectionID con ownConnectionID = do + conState <- MVar.takeMVar $ ncConnectionState con + if ownConnectionID == csOwnConnectionID conState then do + newConState <- case conState of + Connected host port part own conf -> return $ Connected host port part own True + Disconnected host port part own conf -> return $ Disconnected host port part own True + Emulated part own conf -> return $ Emulated part own True + RedirectRequest host port rehost report part own conf -> return $ RedirectRequest host port rehost report part own True + MVar.putMVar (ncConnectionState con) newConState + return True + else do + MVar.putMVar (ncConnectionState con) conState + return False + +tryConvertToEmulatedConnection :: MVar.MVar (Map.Map String (NetworkConnection a)) -> NetworkConnection a -> IO Bool +tryConvertToEmulatedConnection vchans con = do + -- networkConnectionsMap <- MVar.takeMVar vchans + networkConnectionsMap <- MVar.readMVar vchans + case Map.lookup (ncOwnUserID con) networkConnectionsMap of + Just partner -> SSem.withSem (ncHandlingIncomingMessage partner) do + connectionState <- MVar.takeMVar $ ncConnectionState partner + case connectionState of + Connected {} -> do + partConID <- newRandomID + ownConID <- newRandomID + MVar.putMVar (ncConnectionState partner) $ Emulated ownConID partConID True + MVar.takeMVar $ ncConnectionState con + MVar.putMVar (ncConnectionState con) $ Emulated partConID ownConID True + -- MVar.putMVar vchans networkConnectionsMap + return True + _ -> do + -- MVar.putMVar vchans networkConnectionsMap + return False + _ -> do + -- MVar.putMVar vchans networkConnectionsMap + return False + diff --git a/src/Networking/NetworkingMethod/Fast.hs b/src/Networking/NetworkingMethod/Fast.hs new file mode 100644 index 0000000..19d8dbf --- /dev/null +++ b/src/Networking/NetworkingMethod/Fast.hs @@ -0,0 +1,226 @@ +module Networking.NetworkingMethod.Fast where + +import Control.Concurrent +import Control.Exception +import Control.Monad +import GHC.IO.Handle +import Network.Socket +import Networking.Messages +import Networking.NetworkConnection +import Networking.NetworkingMethod.NetworkingMethodCommon +import Networking.RandomID +import ProcessEnvironmentTypes +import qualified Config +import qualified Control.Concurrent.Chan as Chan +import qualified Control.Concurrent.MVar as MVar +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Map as Map +import qualified Networking.NetworkingMethod.Stateless as Stateless +import qualified Syntax +import qualified ValueParsing.ValueGrammar as VG + +type ResponseMapMVar = MVar.MVar (Map.Map String (String, Response)) + +data Conversation = Conversation {convID :: String, convHandle :: Stateless.Conversation, convRespMap :: ResponseMapMVar, convSending :: SSem.SSem} + +type ConnectionHandler = ActiveConnectionsFast -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Socket, SockAddr) -> Conversation -> String -> String -> Message -> IO () + +sendMessage :: Conversation -> Message -> IO () +sendMessage conv value = SSem.withSem (convSending conv) $ Stateless.sendMessage (convHandle conv) (ConversationMessage (convID conv) value) + +sendResponse :: Conversation -> Response -> IO () +sendResponse conv value = SSem.withSem (convSending conv) $ Stateless.sendResponse (convHandle conv) (ConversationResponse (convID conv) value) + +conversationHandler :: Stateless.Conversation -> IO Connection +conversationHandler handle = do + chan <- Chan.newChan + mvar <- MVar.newEmptyMVar + MVar.putMVar mvar Map.empty + sem <- SSem.new 1 + conversationHandlerChangeHandle handle chan mvar sem + +conversationHandlerChangeHandle :: Stateless.Conversation + -> Chan (ConversationID, (String, Message)) + -> MVar (Map.Map ConversationID (String, Response)) + -> e + -> IO + (Stateless.Conversation, MVar Bool, + Chan (ConversationID, (String, Message)), + MVar (Map.Map ConversationID (String, Response)), e) +conversationHandlerChangeHandle handle chan mvar sem = do + isClosed <- MVar.newEmptyMVar + MVar.putMVar isClosed False + forkIO $ whileNotMVar isClosed (do + Stateless.receiveMessageInternal handle VG.parseConversation (\_ -> return ()) (\mes des -> do + case des of + ConversationMessage cid message -> Chan.writeChan chan (cid, (mes, message)) + ConversationResponse cid response -> do + mymap <- MVar.takeMVar mvar + MVar.putMVar mvar $ Map.insert cid (mes, response) mymap + ConversationCloseAll -> do + Config.traceNetIO $ "Received Message: " ++ mes + MVar.takeMVar isClosed + MVar.putMVar isClosed True + forkIO $ catch (hClose $ fst handle) onException + return () + ) + ) + return (handle, isClosed, chan, mvar, sem) + where + whileNotMVar :: MVar.MVar Bool -> IO () -> IO () + whileNotMVar mvar func = do + shouldStop <- MVar.readMVar mvar + unless shouldStop (do + _ <- func + whileNotMVar mvar func + ) + onException :: IOException -> IO () + onException _ = return () + +receiveResponse :: Conversation -> Int -> Int -> IO (Maybe Response) +receiveResponse conv waitTime tries = do + responsesMap <- MVar.readMVar $ convRespMap conv + case Map.lookup (convID conv) responsesMap of + Just (messages, deserial) -> do + return $ Just deserial + Nothing -> do + if tries /= 0 then do + threadDelay waitTime + receiveResponse conv waitTime $ max (tries-1) (-1) else return Nothing + +receiveNewMessage :: Connection -> IO (Conversation, String, Message) +receiveNewMessage connection@(handle, isClosed, chan, mvar, sem) = do + (cid, (serial, deserial)) <- Chan.readChan chan + return (Conversation cid handle mvar sem, serial, deserial) + +startConversation :: ActiveConnectionsFast -> String -> String -> Int -> Int -> IO (Maybe Conversation) +startConversation = startConversationInternal True + +startConversationInternal :: Bool -> ActiveConnectionsFast -> String -> String -> Int -> Int -> IO (Maybe Conversation) +startConversationInternal shouldShowDebug acmvar hostname port waitTime tries = do + conversationid <- newRandomID + connectionMap <- MVar.takeMVar acmvar + case Map.lookup (hostname, port) connectionMap of + Just (handle, isClosed, chan, mvar, sem) -> do + handleClosed <- MVar.readMVar isClosed + if handleClosed then do + statelessActiveCons <- Stateless.createActiveConnections + mbyNewHandle <- Stateless.startConversationInternal shouldShowDebug statelessActiveCons hostname port waitTime tries + case mbyNewHandle of + Just handle -> do + newconnection@(handle, isClosed, chan, mvar, sem) <- conversationHandlerChangeHandle handle chan mvar sem + MVar.putMVar acmvar $ Map.insert (hostname, port) newconnection connectionMap + return $ Just (Conversation conversationid handle mvar sem) + Nothing -> do + MVar.putMVar acmvar connectionMap + return Nothing + else do + MVar.putMVar acmvar connectionMap + return $ Just (Conversation conversationid handle mvar sem) + Nothing -> do + statelessActiveCons <- Stateless.createActiveConnections + mbyNewHandle <- Stateless.startConversationInternal shouldShowDebug statelessActiveCons hostname port waitTime tries + case mbyNewHandle of + Just handle -> do + newconnection@(handle, isClosed, chan, mvar, sem) <- conversationHandler handle + MVar.putMVar acmvar $ Map.insert (hostname, port) newconnection connectionMap + return $ Just (Conversation conversationid handle mvar sem) + Nothing -> do + MVar.putMVar acmvar connectionMap + return Nothing + +waitForConversation :: ActiveConnectionsFast -> String -> String -> Int -> Int -> IO (Maybe Conversation) +waitForConversation ac hostname port waitTime tries = do + Config.traceNetIO $ "Trying to connect to: " ++ hostname ++":"++port + wFCInternal ac hostname port waitTime tries + where + wFCInternal :: ActiveConnectionsFast -> String -> String -> Int -> Int -> IO (Maybe Conversation) + wFCInternal ac hostname port waitTime tries = do + mbyConv <- startConversationInternal False ac hostname port waitTime tries + case mbyConv of + Just conv -> return mbyConv + Nothing -> wFCInternal ac hostname port waitTime tries + +createActiveConnections :: IO ActiveConnectionsFast +createActiveConnections = do + activeConnections <- MVar.newEmptyMVar + MVar.putMVar activeConnections Map.empty + return activeConnections + +acceptConversations :: ActiveConnectionsFast -> ConnectionHandler -> Int -> MVar.MVar (Map.Map Int ServerSocket) -> VChanConnections -> IO ServerSocket +acceptConversations ac connectionhandler port socketsmvar vchanconnections = do + sockets <- MVar.takeMVar socketsmvar + case Map.lookup port sockets of + Just socket -> do + MVar.putMVar socketsmvar sockets + return socket + Nothing -> do + clientlist <- createServer ac connectionhandler port vchanconnections + let newsocket = (clientlist, show port) + let updatedMap = Map.insert port newsocket sockets + MVar.putMVar socketsmvar updatedMap + return newsocket + where + createServer :: ActiveConnectionsFast -> ConnectionHandler -> Int -> VChanConnections -> IO (MVar.MVar [(String, (Syntax.Type, Syntax.Type))]) + createServer activeCons connectionhandler port vchanconnections = do + sock <- socket AF_INET Stream 0 + setSocketOption sock ReuseAddr 1 + let hints = defaultHints { + addrFamily = AF_INET + , addrFlags = [AI_PASSIVE] + , addrSocketType = Stream + } + addrInfo <- getAddrInfo (Just hints) Nothing $ Just $ show port + bind sock $ addrAddress $ head addrInfo + listen sock 1024 + clientlist <- MVar.newEmptyMVar + MVar.putMVar clientlist [] + forkIO $ acceptClients activeCons connectionhandler vchanconnections clientlist sock $ show port + return clientlist + + acceptClients :: ActiveConnectionsFast -> ConnectionHandler -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> Socket -> String -> IO () + acceptClients activeCons connectionhandler mvar clientlist socket ownport = do + clientsocket <- accept socket + + forkIO $ acceptClient activeCons connectionhandler mvar clientlist clientsocket ownport + acceptClients activeCons connectionhandler mvar clientlist socket ownport + + acceptClient :: ActiveConnectionsFast -> ConnectionHandler -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Socket, SockAddr) -> String -> IO () + acceptClient activeCons connectionhandler mvar clientlist clientsocket ownport = do + hdl <- Stateless.getHandleFromSocket $ fst clientsocket + let statelessConv = (hdl, clientsocket) + connection@(handle, isClosed, chan, responsesMvar, sem) <- conversationHandler statelessConv + forkIO $ forever (do + (conversationid, (serial, deserial)) <- Chan.readChan chan + connectionhandler activeCons mvar clientlist clientsocket (Conversation conversationid statelessConv responsesMvar sem) ownport serial deserial + ) + return () + +endConversation :: Conversation -> Int -> Int -> IO () +endConversation _ _ _ = return () + +sayGoodbye :: ActiveConnectionsFast -> IO () +sayGoodbye activeCons = do + activeConsMap <- MVar.readMVar activeCons + let connections = Map.elems activeConsMap + runAll sayGoodbyeConnection connections + where + sayGoodbyeConnection :: Connection -> IO () + sayGoodbyeConnection connection@(statelessconv@(handle, _), isClosed, messages, responses, sem) = do + forkIO $ catch (do + handleClosed <- MVar.readMVar isClosed + unless handleClosed $ SSem.withSem sem $ Stateless.sendMessage statelessconv ConversationCloseAll + unless handleClosed $ SSem.withSem sem $ hPutStr handle " " + hFlushAll handle + hClose handle + ) onException + return () + runAll _ [] = return () + runAll f (x:xs) = do + _ <- f x + runAll f xs + onException :: IOException -> IO () + onException _ = return () + +getPartnerHostaddress :: Conversation -> String +getPartnerHostaddress = Stateless.getPartnerHostaddress . convHandle diff --git a/src/Networking/NetworkingMethod/NetworkingMethodCommon.hs b/src/Networking/NetworkingMethod/NetworkingMethodCommon.hs new file mode 100644 index 0000000..4d151a4 --- /dev/null +++ b/src/Networking/NetworkingMethod/NetworkingMethodCommon.hs @@ -0,0 +1,23 @@ +module Networking.NetworkingMethod.NetworkingMethodCommon where + +import GHC.IO.Handle +import Network.Socket +import Networking.Messages +import qualified Control.Concurrent.Chan as Chan +import qualified Control.Concurrent.MVar as MVar +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Map as Map + +-- type ActiveConnections = ActiveConnectionsStateless + +type ActiveConnections = ActiveConnectionsFast + +data ActiveConnectionsStateless = ActiveConnectionsStateless + +type ConversationStateless = (Handle, (Socket, SockAddr)) + +type Connection = (ConversationStateless, MVar.MVar Bool, Chan.Chan (String, (String, Message)), MVar.MVar (Map.Map String (String, Response)), SSem.SSem) +-- isClosed Conversationid serial deserial +type ActiveConnectionsFast = MVar.MVar (Map.Map NetworkAddress Connection) + +type NetworkAddress = (String, String) diff --git a/src/Networking/NetworkingMethod/Stateless.hs b/src/Networking/NetworkingMethod/Stateless.hs new file mode 100644 index 0000000..d25b4f9 --- /dev/null +++ b/src/Networking/NetworkingMethod/Stateless.hs @@ -0,0 +1,196 @@ +module Networking.NetworkingMethod.Stateless where + +import Control.Concurrent +import Control.Exception +import Control.Monad +import GHC.IO.Handle +import Network.Socket +import Networking.Messages +import Networking.NetworkConnection +import Networking.NetworkingMethod.NetworkingMethodCommon +import ProcessEnvironmentTypes +import System.IO +import qualified Config +import qualified Control.Concurrent.MVar as MVar +import qualified Data.Map as Map +import qualified Networking.Serialize as NSerialize +import qualified Syntax +import qualified ValueParsing.ValueGrammar as VG +import qualified ValueParsing.ValueTokens as VT + +type ConnectionHandler = ActiveConnectionsStateless -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Socket, SockAddr) -> Conversation -> String -> String -> Message -> IO () + +type Conversation = ConversationStateless + +sendMessage :: NSerialize.Serializable a => Conversation -> a -> IO () +sendMessage conv@(handle, _) value = hPutStrLn handle (NSerialize.serialize value ++" ") + +sendResponse :: NSerialize.Serializable a => Conversation -> a -> IO () +sendResponse = sendMessage + +receiveMessageInternal :: Conversation -> VT.Alex t -> (String -> IO b) -> (String -> t -> IO b) -> IO b +receiveMessageInternal conv@(handle, _) grammar fallbackResponse messageHandler = do + waitWhileEOF conv + message <- hGetLine handle + case VT.runAlex message grammar of + Left err -> do + Config.traceNetIO $ "Error during receiving a networkmessage: "++err++" Malformed message: " ++ message + fallbackResponse message + Right deserialmessage -> do + messageHandler message deserialmessage + + +waitWhileEOF :: Conversation -> IO () +waitWhileEOF conv@(handle, _) = do + isEOF <- catch (hIsEOF handle) onException + when isEOF (do + threadDelay 10000 + waitWhileEOF conv + ) + where + onException :: IOException -> IO Bool + onException _ = return True + +startConversationInternal :: Bool -> ActiveConnectionsStateless -> String -> String -> Int -> Int -> IO (Maybe Conversation) +startConversationInternal shouldShowDebug _ hostname port waitTime tries = do + let hints = defaultHints { + addrFamily = AF_INET + , addrFlags = [] + , addrSocketType = Stream + } + convMVar <- MVar.newEmptyMVar + threadid <- forkIO $ catch (do + when shouldShowDebug $ Config.traceNetIO $ "Trying to connect to: " ++ hostname ++":"++port + addrInfo <- getAddrInfo (Just hints) (Just hostname) $ Just port + clientsocket <- openSocketNC $ head addrInfo + connect clientsocket $ addrAddress $ head addrInfo + handle <- getHandleFromSocket clientsocket + MVar.putMVar convMVar (handle, (clientsocket, addrAddress $ head addrInfo)) + Config.traceNetIO $ "Connected to: " ++ hostname ++ ":"++port + ) $ printConErr hostname port + getFromNetworkThread Nothing threadid convMVar waitTime tries + +startConversation :: ActiveConnectionsStateless -> String -> String -> Int -> Int -> IO (Maybe Conversation) +startConversation = startConversationInternal True + +printConErr :: String -> String -> IOException -> IO () +printConErr hostname port err = Config.traceIO $ "startConversation: Communication Partner " ++ hostname ++ ":" ++ port ++ "not found!" + +waitForConversation :: ActiveConnectionsStateless -> String -> String -> Int -> Int -> IO (Maybe Conversation) +waitForConversation ac hostname port waitTime tries = do + Config.traceNetIO $ "Trying to connect to: " ++ hostname ++":"++port + wFCInternal ac hostname port waitTime tries + where + wFCInternal :: ActiveConnectionsStateless -> String -> String -> Int -> Int -> IO (Maybe Conversation) + wFCInternal ac hostname port waitTime tries = do + mbyConv <- startConversationInternal False ac hostname port waitTime tries + case mbyConv of + Just conv -> return mbyConv + Nothing -> wFCInternal ac hostname port waitTime tries + + +acceptConversations :: ActiveConnectionsStateless -> ConnectionHandler -> Int -> MVar.MVar (Map.Map Int ServerSocket) -> VChanConnections -> IO ServerSocket +acceptConversations ac connectionhandler port socketsmvar vchanconnections = do + sockets <- MVar.takeMVar socketsmvar + case Map.lookup port sockets of + Just socket -> do + MVar.putMVar socketsmvar sockets + return socket + Nothing -> do + Config.traceIO "Creating socket!" + clientlist <- createServer ac connectionhandler port vchanconnections + Config.traceIO "Socket created" + let newsocket = (clientlist, show port) + let updatedMap = Map.insert port newsocket sockets + MVar.putMVar socketsmvar updatedMap + return newsocket + where + createServer :: ActiveConnectionsStateless -> ConnectionHandler -> Int -> VChanConnections -> IO (MVar.MVar [(String, (Syntax.Type, Syntax.Type))]) + createServer activeCons connectionhandler port vchanconnections = do + sock <- socket AF_INET Stream 0 + setSocketOption sock ReuseAddr 1 + let hints = defaultHints { + addrFamily = AF_INET + , addrFlags = [AI_PASSIVE] + , addrSocketType = Stream + } + addrInfo <- getAddrInfo (Just hints) Nothing $ Just $ show port + bind sock $ addrAddress $ head addrInfo + listen sock 1024 + clientlist <- MVar.newEmptyMVar + MVar.putMVar clientlist [] + forkIO $ acceptClients activeCons connectionhandler vchanconnections clientlist sock $ show port + return clientlist + acceptClients :: ActiveConnectionsStateless -> ConnectionHandler -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> Socket -> String -> IO () + acceptClients activeCons connectionhandler mvar clientlist socket ownport = do + clientsocket <- accept socket + + forkIO $ acceptClient activeCons connectionhandler mvar clientlist clientsocket ownport + acceptClients activeCons connectionhandler mvar clientlist socket ownport + + acceptClient :: ActiveConnectionsStateless -> ConnectionHandler -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> MVar.MVar [(String, (Syntax.Type, Syntax.Type))] -> (Socket, SockAddr) -> String -> IO () + acceptClient activeCons connectionhandler mvar clientlist clientsocket ownport = do + hdl <- getHandleFromSocket $ fst clientsocket + let conv = (hdl, clientsocket) + receiveMessageInternal conv VG.parseMessages (\_ -> return ()) $ connectionhandler activeCons mvar clientlist clientsocket conv ownport + hClose hdl + +getFromNetworkThread :: Maybe Conversation -> ThreadId -> MVar.MVar a -> Int -> Int -> IO (Maybe a) +getFromNetworkThread conv = getFromNetworkThreadWithModification conv Just + +getFromNetworkThreadWithModification :: Maybe Conversation -> (a -> Maybe b) -> ThreadId -> MVar a -> Int -> Int -> IO (Maybe b) +getFromNetworkThreadWithModification conv func threadid mvar waitTime currentTry = do + mbyResult <- MVar.tryReadMVar mvar + case mbyResult of + Just result -> return $ func result + Nothing -> do + if currentTry /= 0 then do + threadDelay waitTime + getFromNetworkThreadWithModification conv func threadid mvar waitTime $ max (currentTry-1) (-1) + else do + killThread threadid + return Nothing + +receiveResponse :: Conversation -> Int -> Int -> IO (Maybe Response) +receiveResponse conv waitTime tries = do + retVal <- MVar.newEmptyMVar + threadid <- forkIO $ receiveMessageInternal conv VG.parseResponses (\_ -> MVar.putMVar retVal Nothing) (\_ des -> MVar.putMVar retVal $ Just des) + getFromNetworkThreadWithModification (Just conv) id threadid retVal waitTime tries + +receiveNewMessage :: Conversation -> IO (Conversation, String, Message) +receiveNewMessage conv = do + receiveMessageInternal conv VG.parseMessages (\_ -> receiveNewMessage conv) $ \s des -> return (conv, s, des) + + +endConversation :: Conversation -> Int -> Int -> IO () +endConversation conv@(handle, _) waitTime tries = do + finished <- MVar.newEmptyMVar + threadid <- forkIO $ hClose handle >> MVar.putMVar finished True + _ <- getFromNetworkThread (Just conv) threadid finished waitTime tries + return () + +createActiveConnections :: IO ActiveConnectionsStateless +createActiveConnections = return ActiveConnectionsStateless + +openSocketNC :: AddrInfo -> IO Socket +openSocketNC addr = socket (addrFamily addr) (addrSocketType addr) (addrProtocol addr) + +getHandleFromSocket :: Socket -> IO Handle +getHandleFromSocket socket = do + hdl <- socketToHandle socket ReadWriteMode + -- hSetBuffering hdl NoBuffering + hSetBuffering hdl LineBuffering + return hdl + +sayGoodbye :: ActiveConnectionsStateless -> IO () +sayGoodbye _ = return () + +hostaddressTypeToString :: HostAddress -> String +hostaddressTypeToString hostaddress = do + let (a, b, c, d) = hostAddressToTuple hostaddress + show a ++ "." ++ show b ++ "."++ show c ++ "." ++ show d + +getPartnerHostaddress :: Conversation -> String +getPartnerHostaddress conv@(handle, (socket, sockAddress)) = case sockAddress of + SockAddrInet _ hostaddress -> hostaddressTypeToString hostaddress + _ -> "" \ No newline at end of file diff --git a/src/Networking/Outgoing.hs b/src/Networking/Outgoing.hs new file mode 100644 index 0000000..14047d4 --- /dev/null +++ b/src/Networking/Outgoing.hs @@ -0,0 +1,279 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE BlockArguments #-} + +module Networking.Outgoing where + +import Control.Concurrent +import Control.Exception +import Control.Monad +import Networking.Messages +import Networking.NetworkConnection +import ProcessEnvironmentTypes +import qualified Config +import qualified Control.Concurrent.MVar as MVar +import qualified Control.Concurrent.SSem as SSem +import qualified Data.Map as Map +import qualified Networking.Common as NC +import qualified Networking.Messages as Messages +import qualified Networking.NetworkBuffer as NB +import qualified Networking.NetworkConnection as NCon +import qualified Networking.NetworkingMethod.NetworkingMethodCommon as NMC +import qualified Networking.RandomID as RandomID +import qualified Networking.Serialize as NSerialize +import qualified Syntax + +newtype ClientException = NoIntroductionException String + deriving Eq + +instance Show ClientException where + show = \case + NoIntroductionException s -> "Partner didn't introduce itself, but sent: " ++ s + +instance Exception ClientException + +sendValue :: VChanConnections -> NMC.ActiveConnections -> NetworkConnection Value -> Value -> String -> Int -> IO Bool +sendValue vchanconsmvar activeCons networkconnection val ownport resendOnError = do + connectionstate <- MVar.readMVar $ ncConnectionState networkconnection + case connectionstate of + Emulated {} -> do + --waitTillReadyToSend val + vchancons <- MVar.readMVar vchanconsmvar + valCleaned <- serializeVChan val + NB.write(ncWrite networkconnection) valCleaned + let ownid = ncOwnUserID networkconnection + let mbypartner = Map.lookup ownid vchancons + case mbypartner of + Just partner -> do + Config.traceNetIO $ "Emulated Send for: " ++ NSerialize.serialize valCleaned + NB.write (ncRead partner) valCleaned + return True + _ -> do + Config.traceNetIO "Something went wrong when sending over a emulated connection" + return False + _ -> do + let hostname = csHostname connectionstate + let port = csPort connectionstate + --waitTillReadyToSend val + setRedirectRequests vchanconsmvar hostname port ownport val + Config.traceNetIO $ "Redirected: " ++ show val + valcleaned <- serializeVChan val + Config.traceNetIO $ "Serialized: " ++ show val + messagesCount <- NB.write (ncWrite networkconnection) valcleaned + Config.traceNetIO $ "Wrote to Buffer: " ++ show val + result <- tryToSendNetworkMessage activeCons networkconnection hostname port (Messages.NewValue (ncOwnUserID networkconnection) messagesCount valcleaned) resendOnError + Config.traceNetIO $ "Sent message: " ++ show val + return result + +waitTillReadyToSend :: Value -> IO () +waitTillReadyToSend input = do + ready <- channelReadyToSend input + unless ready $ threadDelay 5000 >> waitTillReadyToSend input + +channelReadyToSend :: Value -> IO Bool +channelReadyToSend = searchVChans handleChannel True (&&) + where + handleChannel :: Value -> IO Bool + handleChannel input = case input of + VChan nc used -> NB.isAllAcknowledged $ ncWrite nc + _ -> return True + +sendNetworkMessage :: NMC.ActiveConnections -> NetworkConnection Value -> Message -> Int -> IO Bool +sendNetworkMessage activeCons networkconnection message resendOnError = do + connectionstate <- MVar.readMVar $ ncConnectionState networkconnection + case connectionstate of + Emulated {} -> return True + _ -> do + let hostname = csHostname connectionstate + let port = csPort connectionstate + tryToSendNetworkMessage activeCons networkconnection hostname port message resendOnError + +-- ResendOnError gives the number of times a value might be resent when a error occures +-- There are three special cases +-- (-1) will send indefinitely until it succedes +-- (-2) will not wait and only act on redirect messages (wait messages and failed connections wont result in reattempting sending the message) +-- For numbers n smaller than -2 it will wait for abs(n)-2 times +tryToSendNetworkMessage :: NMC.ActiveConnections -> NetworkConnection Value -> String -> String -> Message -> Int -> IO Bool +tryToSendNetworkMessage activeCons networkconnection hostname port message resendOnError = do + let serializedMessage = NSerialize.serialize message + sendingNetLog serializedMessage $ "Sending message as: " ++ ncOwnUserID networkconnection ++ " to: " ++ ncPartnerUserID networkconnection ++ " Over: " ++ hostname ++ ":" ++ port + + mbycon <- NC.startConversation activeCons hostname port 10000 10 + mbyresponse <- case mbycon of + Just con -> do + sendingNetLog serializedMessage "Aquired connection" + NC.sendMessage con message + sendingNetLog serializedMessage "Sent message" + potentialResponse <- NC.receiveResponse con 10000 50 + sendingNetLog serializedMessage "Received response" + NC.endConversation con 10000 10 + sendingNetLog serializedMessage "Ended connection" + return potentialResponse + Nothing -> do + sendingNetLog serializedMessage "Connecting unsuccessful" + return Nothing + + success <- case mbyresponse of + Just response -> case response of + Okay -> do + sendingNetLog serializedMessage "Message okay" + return True + Redirect host port -> do + sendingNetLog serializedMessage "Communication partner changed address, resending" + tryToSendNetworkMessage activeCons networkconnection host port message if resendOnError < -2 then resendOnError +1 else resendOnError + Wait -> if resendOnError /= (-2) then do + sendingNetLog serializedMessage "Communication out of sync lets wait!" + threadDelay 1000000 + tryToSendNetworkMessage activeCons networkconnection hostname port message if resendOnError < -2 then resendOnError +1 else resendOnError + else do + sendingNetLog serializedMessage "Communication out of sync lets wait!, sending failed" + return False + _ -> do + sendingNetLog serializedMessage "Unknown communication error" + return False + + Nothing -> do + sendingNetLog serializedMessage "Error when receiving response" + if resendOnError /= 0 && resendOnError < (-2) then do + connectionState <- MVar.readMVar $ ncConnectionState networkconnection + case connectionState of + Connected updatedhost updatedport _ _ _ -> do + sendingNetLog serializedMessage $ "Trying to resend to: " ++ updatedhost ++ ":" ++ updatedport + tryToSendNetworkMessage activeCons networkconnection updatedhost updatedport message $ max (resendOnError-1) (-1) + _ -> return False + else return False + sendingNetLog serializedMessage "Message got send or finally failed!" + return success + + +sendingNetLog :: String -> String -> IO () +sendingNetLog msg info = Config.traceNetIO $ "Sending message: "++msg++" \n Status: "++info + +printConErr :: String -> String -> IOException -> IO Bool +printConErr hostname port err = do + Config.traceIO $ "Communication Partner " ++ hostname ++ ":" ++ port ++ "not found! \n " ++ show err + return False + + +initialConnect :: NMC.ActiveConnections -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> String -> String -> String -> (Syntax.Type, Syntax.Type) -> IO Value +initialConnect activeCons mvar hostname port ownport syntype= do + mbycon <- NC.waitForConversation activeCons hostname port 1000 100 -- This should be 10000 100 in the real world, expecting just a 100ms ping in the real world might be a little aggressive. + + case mbycon of + Just con -> do + ownuserid <- RandomID.newRandomID + NC.sendMessage con (Messages.Introduce ownuserid ownport (fst syntype) $ snd syntype) + mbyintroductionanswer <- NC.receiveResponse con 10000 (-1) + NC.endConversation con 10000 10 + case mbyintroductionanswer of + Just introduction -> case introduction of + OkayIntroduce introductionanswer -> do + let msgserial = NSerialize.serialize $ Messages.Introduce ownuserid ownport (fst syntype) $ snd syntype + Config.traceNetIO $ "Sending message as: " ++ ownuserid ++ " to: " ++ introductionanswer + Config.traceNetIO $ " Over: " ++ hostname ++ ":" ++ port + Config.traceNetIO $ " Message: " ++ msgserial + newConnection <- newNetworkConnection introductionanswer ownuserid hostname port introductionanswer ownuserid + + networkconnectionmap <- MVar.takeMVar mvar + let newNetworkconnectionmap = Map.insert introductionanswer newConnection networkconnectionmap + MVar.putMVar mvar newNetworkconnectionmap + + -- If it can be converted to local do that + NCon.tryConvertToEmulatedConnection mvar newConnection + + + used <- MVar.newEmptyMVar + MVar.putMVar used False + return $ VChan newConnection used + + _ -> do + let introductionserial = NSerialize.serialize introduction + Config.traceNetIO $ "Illegal answer from server: " ++ introductionserial + threadDelay 1000000 + initialConnect activeCons mvar hostname port ownport syntype + Nothing -> do + Config.traceNetIO "Something went wrong while connection to the server" + threadDelay 1000000 + initialConnect activeCons mvar hostname port ownport syntype + Nothing -> do + Config.traceNetIO "Couldn't connect to server. Retrying" + threadDelay 1000000 + initialConnect activeCons mvar hostname port ownport syntype + +setRedirectRequests :: VChanConnections -> String -> String -> String -> Value -> IO Bool +setRedirectRequests vchanconmvar newhost newport ownport = searchVChans (handleVChan vchanconmvar newhost newport ownport) True (&&) + where + handleVChan :: VChanConnections -> String -> String -> String -> Value -> IO Bool + handleVChan vchanconmvar newhost newport ownport input = case input of + VChan nc _ -> do + Config.traceNetIO $ "Trying to set RedirectRequest for " ++ ncPartnerUserID nc ++ " to " ++ newhost ++ ":" ++ newport + + SSem.withSem (ncHandlingIncomingMessage nc) (do + oldconnectionstate <- MVar.takeMVar $ ncConnectionState nc + case oldconnectionstate of + Connected hostname port partConID ownConID confirmed -> MVar.putMVar (ncConnectionState nc) $ RedirectRequest hostname port newhost newport partConID ownConID confirmed + RedirectRequest hostname port _ _ partConID ownConID confirmed -> MVar.putMVar (ncConnectionState nc) $ RedirectRequest hostname port newhost newport partConID ownConID confirmed + Emulated partConID ownConID confirmed -> do + Config.traceNetIO "TODO: Allow RedirectRequest for Emulated channel" + vchanconnections <- MVar.takeMVar vchanconmvar + + let userid = ncOwnUserID nc + let mbypartner = Map.lookup userid vchanconnections + case mbypartner of + Just partner -> do + MVar.putMVar (ncConnectionState nc) $ RedirectRequest "" ownport newhost newport partConID ownConID confirmed -- Setting this to 127.0.0.1 is a temporary hack + oldconnectionstatePartner <- MVar.takeMVar $ ncConnectionState partner + MVar.putMVar (ncConnectionState partner) $ Connected newhost newport partConID ownConID confirmed + Nothing -> do + MVar.putMVar (ncConnectionState nc) oldconnectionstate + Config.traceNetIO "Error occured why getting the linked emulated channel" + + + MVar.putMVar vchanconmvar vchanconnections + Disconnected hostname partner partConID ownConID confirmed -> do + MVar.putMVar (ncConnectionState nc) oldconnectionstate + Config.traceNetIO "Cannot set RedirectRequest for a disconnected channel" + ) + Config.traceNetIO $ "Set RedirectRequest for " ++ ncPartnerUserID nc ++ " to " ++ newhost ++ ":" ++ newport + return True + _ -> return True + +serializeVChan :: Value -> IO Value +serializeVChan = modifyVChans handleVChan + where + handleVChan :: Value -> IO Value + handleVChan input = case input of + VChan nc _-> do + (r, ro, rl, w, wo, wl, pid, oid, h, p, partConID) <- serializeNetworkConnection nc + return $ VChanSerial (r, ro, rl) (w, wo, wl) pid oid (h, p, partConID) + _ -> return input + +sendDisconnect :: NMC.ActiveConnections -> MVar.MVar (Map.Map String (NetworkConnection Value)) -> IO () +sendDisconnect ac mvar = do + networkConnectionMap <- MVar.readMVar mvar + let allNetworkConnections = Map.elems networkConnectionMap + goodbyes <- doForall ac allNetworkConnections + unless goodbyes $ do + threadDelay 100000 + sendDisconnect ac mvar + where + doForall ac (x:xs) = do + xres <- sendDisconnectNetworkConnection ac x + rest <- doForall ac xs + return $ xres && rest + doForall ac [] = return True + sendDisconnectNetworkConnection :: NMC.ActiveConnections -> NetworkConnection Value -> IO Bool + sendDisconnectNetworkConnection ac con = do + let writeVals = ncWrite con + connectionState <- MVar.readMVar $ ncConnectionState con + case connectionState of + Connected host port _ _ _ -> do + ret <- NB.isAllAcknowledged writeVals + if ret then do + sent <- catch (sendNetworkMessage ac con (Messages.Disconnect $ ncOwnUserID con) $ -1) (\x -> printConErr host port x >> return True) + when sent $ NCon.disconnectFromPartner con -- This should cause a small speedup + return sent + else + return False + -- return False + _ -> return True + \ No newline at end of file diff --git a/src/Networking/RandomID.hs b/src/Networking/RandomID.hs new file mode 100644 index 0000000..3578e2b --- /dev/null +++ b/src/Networking/RandomID.hs @@ -0,0 +1,15 @@ +module Networking.RandomID where + +import Data.Char +import System.Random + +mapToChar :: Int -> Char +mapToChar val + | 0 <= val && val <= 9 = chr (val + 48) + | 10 <= val && val <= 35 = chr (val + 55) + | 36 <= val && val <= 61 = chr (val + 61) + | otherwise = '-' + +newRandomID :: IO String +newRandomID = map mapToChar . take 8 . randomRs (0, 61) <$> newStdGen +-- newRandomID = map mapToChar . take 128 . randomRs (0, 61) <$> newStdGen diff --git a/src/Networking/Serialize.hs b/src/Networking/Serialize.hs new file mode 100644 index 0000000..687c5e1 --- /dev/null +++ b/src/Networking/Serialize.hs @@ -0,0 +1,220 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} + +module Networking.Serialize where + +import Control.Exception +import Data.Set +import Kinds +import Networking.Messages +import ProcessEnvironmentTypes +import Syntax + +newtype SerializationException = UnserializableException String + deriving Eq + +instance Show SerializationException where + show = \case + (UnserializableException s) -> "UnserializableException: " ++ s ++ " is not serializable" + +instance Exception SerializationException + + +class Serializable a where + serialize :: a -> String + +class SerializableList b where + toSer :: String -> b + +instance SerializableList String where + toSer = id + +instance (SerializableList b, Serializable a) => SerializableList (a -> b) where + toSer serList serElem = toSer $ serList ++ " (" ++ serialize serElem ++ ")" + +merge :: (SerializableList b) => b +merge = toSer "" + +serializeArgs :: (SerializableList b) => b +serializeArgs = toSer "" + +instance Serializable ConversationSession where + serialize = \case + ConversationMessage c m -> "NConversationMessage" ++ serializeArgs c m + ConversationResponse c r -> "NConversationResponse" ++ serializeArgs c r + ConversationCloseAll -> "NConversationCloseAll" + +instance Serializable Response where + serialize = \case + Redirect host port -> "NRedirect" ++ serializeArgs host port + Okay -> "NOkay" + OkayIntroduce u -> "NOkayIntroduce" ++ serializeArgs u + Wait -> "NWait" + Error -> "NError" + +instance Serializable Message where + serialize = \case + Introduce p port tn t -> "NIntroduce" ++ serializeArgs p port tn t + NewValue p c v -> "NNewValue" ++ serializeArgs p c v + RequestValue p c -> "NRequestValue" ++ serializeArgs p c + AcknowledgeValue p c -> "NAcknowledgeValue" ++ serializeArgs p c + NewPartnerAddress p port conID -> "NNewPartnerAddress" ++ serializeArgs p port conID + AcknowledgePartnerAddress p conID -> "NAcknowledgePartnerAddress" ++ serializeArgs p conID + Disconnect p -> "NDisconnect" ++ serializeArgs p + AcknowledgeDisconnect p -> "NAcknowledgeDisconnect" ++ serializeArgs p + +instance Serializable Value where + serialize = \case + VUnit -> "VUnit" + VLabel s -> "VLabel" ++ serializeArgs s + VInt i -> "VInt" ++ serializeArgs i + VDouble d -> "VDouble" ++ serializeArgs d + VString s -> "VString" ++ serializeArgs s + VSend v -> "VSend" ++ serializeArgs v + VPair a b -> "VPair" ++ serializeArgs a b + VType t -> "VType" ++ serializeArgs t + VFunc env s exp -> "VFunc" ++ serializeArgs env s exp + VDynCast v t -> "VDynCast" ++ serializeArgs v t + VFuncCast v ft1 ft2 -> "VFuncCast" ++ serializeArgs v ft1 ft2 + VRec env f x e0 e1 -> "VRec" ++ serializeArgs env f x e0 e1 + VNewNatRec env f n tid ty ez x es -> "VNewNatRec" ++ serializeArgs env f n tid ty ez x es + VChan {} -> throw $ UnserializableException "VChan" + VChanSerial r w p o c -> "VChanSerial" ++ serializeArgs r w p o c + +instance Serializable Multiplicity where + serialize = \case + MMany -> "MMany" + MOne -> "MOne" + +instance Serializable Type where + serialize = \case + TUnit -> "TUnit" + TInt -> "TInt" + TDouble -> "TDouble" + TBot -> "TBot" + TDyn -> "TDyn" + TNat -> "TNat" + TString -> "TString" + TNatLeq i -> "TNatLeq" ++ serializeArgs i + TNatRec e t1 ident t2 -> "TNatRec" ++ serializeArgs e t1 ident t2 + TVar b ident -> "TVar" ++ serializeArgs b ident + TAbs ident t1 t2 -> "TAbs" ++ serializeArgs ident t1 t2 + TName b ident -> "TName" ++ serializeArgs b ident + TLab arr -> "TLab" ++ serializeArgs arr + TFun mult ident t1 t2 -> "TFun" ++ serializeArgs mult ident t1 t2 + TPair ident t1 t2 -> "TPair" ++ serializeArgs ident t1 t2 + TSend ident t1 t2 -> "TSend" ++ serializeArgs ident t1 t2 + TRecv ident t1 t2 -> "TRecv" ++ serializeArgs ident t1 t2 + TCase e arr -> "TCase" ++ serializeArgs e arr + TEqn e1 e2 t -> "TEqn" ++ serializeArgs e1 e2 t + TSingle ident -> "TSingle" ++ serializeArgs ident + +instance Serializable Exp where + serialize = \case + Let ident e1 e2 -> "ELet" ++ serializeArgs ident e1 e2 + Math mathop -> "EMath" ++ serializeArgs mathop + Lit l -> "ELit" ++ serializeArgs l + Succ e -> "ESucc" ++ serializeArgs e + NatRec e1 e2 ident1 ident2 ident3 t e3 -> "NatRec" ++ serializeArgs e1 e2 ident1 ident2 ident3 t e3 + NewNatRec ident1 ident2 ident3 t e1 ident4 e2 -> "ENewNatRec" ++ serializeArgs ident1 ident2 ident3 t e1 ident4 e2 + Var ident -> "EVar" ++ serializeArgs ident + Lam mult ident t e -> "ELam" ++ serializeArgs mult ident t e + Rec ident1 ident2 e1 e2 -> "ERec" ++ serializeArgs ident1 ident2 e1 e2 + App e1 e2 -> "EApp" ++ serializeArgs e1 e2 + Pair mult ident e1 e2 -> "EPair" ++ serializeArgs mult ident e1 e2 + LetPair ident1 ident2 e1 e2 -> "ELetPair" ++ serializeArgs ident1 ident2 e1 e2 + Fst e -> "EFst" ++ serializeArgs e + Snd e -> "ESnd" ++ serializeArgs e + Fork e -> "EFork" ++ serializeArgs e + New t -> "ENew" ++ serializeArgs t + Send e -> "ESend" ++ serializeArgs e + Recv e -> "ERecv" ++ serializeArgs e + Case e arr -> "ECase" ++ serializeArgs e arr + Cast e t1 t2 -> "ECast" ++ serializeArgs e t1 t2 + + Connect e0 t e1 e2 -> "EConnect" ++ serializeArgs e0 t e1 e2 + Accept e t -> "EAccept" ++ serializeArgs e t + +instance Serializable (MathOp Exp) where + serialize = \case + Add e1 e2 -> "MAdd" ++ serializeArgs e1 e2 + Sub e1 e2 -> "MSub" ++ serializeArgs e1 e2 + Mul e1 e2 -> "MMul" ++ serializeArgs e1 e2 + Div e1 e2 -> "MDiv" ++ serializeArgs e1 e2 + Neg e -> "MNeg" ++ serializeArgs e +instance Serializable Literal where + serialize = \case + LInt i -> "LInt" ++ serializeArgs i + LNat i -> "LNat" ++ serializeArgs i + LDouble d -> "LDouble" ++ serializeArgs d + LLab s -> "LLab" ++ serializeArgs s + LUnit -> "LUnit" + LString s -> "LString" ++ serializeArgs s + +instance Serializable FuncType where + serialize (FuncType env s t1 t2) = "SFuncType" ++ serializeArgs env s t1 t2 + +instance Serializable GType where + serialize = \case + GUnit -> "GUnit" + GLabel lt -> "GLabel" ++ serializeArgs lt + GFunc mult -> "GFunc" ++ serializeArgs mult + GPair -> "GPair" + GNat -> "GNat" + GNatLeq i -> "GNatLeq" ++ serializeArgs i + GInt -> "GInt" + GDouble -> "GDouble" + GString -> "GString" + +instance {-# OVERLAPPING #-} Serializable String where + serialize s = "String:"++ show s + +instance Serializable Int where + serialize i = "Int:" ++ show i + +instance Serializable Integer where + serialize i = "Integer:" ++ show i + +instance Serializable Bool where + serialize b = "Bool:" ++ show b + +instance Serializable Double where + serialize d = "Double:" ++ show d + +instance (Serializable a, Serializable b) => Serializable (a, b) where + serialize (s, t) = "((" ++ serialize s++ ") (" ++ serialize t ++ "))" + +instance (Serializable a, Serializable b, Serializable c) => Serializable (a, b, c) where + serialize (s, t, u) = "((" ++ serialize s ++ ") (" ++ serialize t ++ ") (" ++ serialize u ++ "))" + +instance (Serializable a, Serializable b, Serializable c, Serializable d) => Serializable (a, b, c, d) where + serialize (s, t, u, v) = "((" ++ serialize s ++ ") (" ++ serialize t ++ ") (" ++ serialize u ++ ") (" ++ serialize v ++ "))" + +instance {-# OVERLAPPING #-} Serializable PEnv where + serialize arr = serializeLabeledArray "PEnv" arr + +instance {-# OVERLAPPING #-} Serializable PEnvEntry where + serialize (s, t) = "PEnvEntry (" ++ serialize s ++ ") (" ++ serialize t ++ ")" + +instance {-# OVERLAPPING #-} Serializable LabelType where + serialize as = serializeLabeledArray "SLabelType" (elems as) + +instance {-# OVERLAPPING #-} Serializable [(String, Exp)] where + serialize arr = serializeLabeledArray "SStringExpArray" arr + +instance {-# OVERLAPPING #-} Serializable [(String, Type)] where + serialize arr = serializeLabeledArray "SStringTypeArray" arr + +instance {-# OVERLAPPING #-} Serializable [String] where + serialize arr = serializeLabeledArray "SStringArray" arr + +instance {-# OVERLAPPING #-}Serializable [Value] where + serialize arr = serializeLabeledArray "SValuesArray" arr + +serializeLabeledArray :: Serializable a => String -> [a] -> String +serializeLabeledArray label arr = label ++ " [" ++ serializeElements arr ++ "]" + +serializeElements :: Serializable a => [a] -> String +serializeElements [] = "" +serializeElements [x] = serialize x +serializeElements (x:xs) = serialize x ++ ", " ++ serializeElements xs diff --git a/src/Networking/Tests.hs b/src/Networking/Tests.hs new file mode 100644 index 0000000..fcca97c --- /dev/null +++ b/src/Networking/Tests.hs @@ -0,0 +1,56 @@ +module Networking.Tests where + +import Networking.Assert +import Networking.Buffer +import Networking.NetworkBuffer + +test :: IO () +test = testBuffer >> testNetworkBuffer + +testBuffer :: IO () +testBuffer = do + newBuf <- newBuffer + writeBufferToList newBuf >>= assertEQ "1: Empty Buffer" ([] :: [Integer]) + tryTakeBuffer newBuf >>= assertEQ "2: Nothing" Nothing + tryReadBuffer newBuf >>= assertEQ "3: Read Nothing" Nothing + writeBuffer newBuf 42 + writeBufferToList newBuf >>= assertEQ "4: One Element Buffer" [42] + cloneBuffer <- cloneBuffer newBuf + writeBufferToList newBuf >>= assertEQ "5: One Element in Clone" [42] + writeBuffer cloneBuffer 1337 + writeBufferToList cloneBuffer >>= assertEQ "6: 2 Elements in Clone" [42, 1337] + writeBufferToList newBuf >>= assertEQ "7: 2 Elements in Buffer" [42, 1337] + tryReadBuffer cloneBuffer >>= assertEQ "8: Try Read from Clone" (Just 42) + readBuffer cloneBuffer >>= assertEQ "9: Read from Clone" 42 + takeBuffer cloneBuffer >>= assertEQ "10: Take from Clone " 42 + tryTakeBuffer cloneBuffer >>= assertEQ "11: Try Take from Clone" (Just 1337) + writeBufferToList newBuf >>= assertEQ "12: 2 Elements in Buffer" [42, 1337] + writeBufferToList cloneBuffer >>= assertEQ "13: Empty Clone" [] + writeBuffer newBuf 1 + writeBufferToList newBuf >>= assertEQ "14: 3 Elements in Buffer" [42, 1337, 1] + writeBufferToList cloneBuffer >>= assertEQ "15: 1 Element in Clone" [1] + + +testNetworkBuffer :: IO () +testNetworkBuffer = do + nb <- newNetworkBuffer + isAllAcknowledged nb >>= assertEQ "1: All acknowledged" True + write nb (42 :: Integer) + isAllAcknowledged nb >>= assertEQ "2: Not All acknowledged" False + serializeMinimal nb >>= assertEQ "3: Serial" ([42], 0, 1) + write nb 1337 + serializeMinimal nb >>= assertEQ "3: Serial" ([42, 1337], 0, 2) + tryGetAtNB nb 0 >>= assertEQ "4. 42" (Just 42) + tryGetAtNB nb 1 >>= assertEQ "5. 1337" (Just 1337) + tryTake nb >>= assertEQ "6. 42" (Just (42, 0)) + getNextOffset nb >>= assertEQ "7. 1" 1 + serializeMinimal nb >>= assertEQ "8: Serial" ([1337], 1, 2) + updateAcknowledgements nb 1 + isAllAcknowledged nb >>= assertEQ "9. All achnowledged" True + + + + + + + \ No newline at end of file diff --git a/src/Networking/ThingsToLookInto.txt b/src/Networking/ThingsToLookInto.txt new file mode 100644 index 0000000..ccf6c18 --- /dev/null +++ b/src/Networking/ThingsToLookInto.txt @@ -0,0 +1,3 @@ +https://hackage.haskell.org/package/port-utils-0.2.1.0 + +-- Get random free port for the connect command \ No newline at end of file diff --git a/src/Parsing/Grammar.y b/src/Parsing/Grammar.y index d339843..c4ab4d7 100644 --- a/src/Parsing/Grammar.y +++ b/src/Parsing/Grammar.y @@ -36,6 +36,8 @@ import qualified Parsing.Tokens as T new { T _ T.New } send { T _ T.Send } recv { T _ T.Recv } + connect { T _ T.Connect } + accept { T _ T.Accept } -- for Binary Session Types; obsolete for Label Dependent ones select { T _ T.Select } @@ -91,7 +93,7 @@ import qualified Parsing.Tokens as T %nonassoc '>' '<' %left '+' '-' NEG POS %left '*' '/' -%left send recv +%left send recv connect create accept end %nonassoc APP @@ -166,7 +168,9 @@ Exp : let var '=' Exp in Exp %prec LET { Let $2 $4 $6 } | fork Exp { Fork $2 } | send Exp %prec send { Send $2 } | recv Exp %prec recv { Recv $2 } - | Exp Exp %prec APP { App $1 $2 } + | connect Exp Typ Exp Exp %prec connect {Connect $2 $3 $4 $5} + | accept Exp Typ %prec accept { Accept $2 $3 } + | Exp Exp %prec APP { App $1 $2 } Labs : lab { [$1] } | lab ',' Labs { $1 : $3 } diff --git a/src/Parsing/Tokens.x b/src/Parsing/Tokens.x index c80c098..b29b052 100644 --- a/src/Parsing/Tokens.x +++ b/src/Parsing/Tokens.x @@ -42,6 +42,8 @@ tokens :- new { tok $ const New } send { tok $ const Send } recv { tok $ const Recv } + connect { tok $ const Connect } + accept { tok $ const Accept } -- for Binary Session Types; obsolete for Label Dependent ones select { tok $ const Select } @@ -96,6 +98,8 @@ data Token = New | Send | Recv | + Connect | + Accept | -- for Binary Session Types; obsolete for Label Dependent ones Select | diff --git a/src/PrettySyntax.hs b/src/PrettySyntax.hs index 5f2be89..fad7b54 100644 --- a/src/PrettySyntax.hs +++ b/src/PrettySyntax.hs @@ -6,7 +6,7 @@ module PrettySyntax (Pretty(), pretty, pshow) where import Kinds import Syntax -import ProcessEnvironment +import ProcessEnvironmentTypes import Data.Text.Prettyprint.Doc import qualified Data.Set as Set @@ -123,6 +123,8 @@ instance Pretty Exp where pretty (New t) = pretty "new" <+> pretty t pretty (Send e) = pretty "send" <+> pretty e pretty (Recv e) = pretty "recv" <+> pretty e + pretty (Connect s t a i) = pretty "connect" <+> pretty s <+> pretty t <+> pretty a <+> pretty i + pretty (Accept s t) = pretty "accept" <+> pretty s <+> pretty t pretty (Case e ses) = pcase e ses pretty (Cast e t1 t2) = @@ -164,7 +166,8 @@ instance Pretty Value where VInt i -> pretty $ show i VDouble d -> pretty $ show d VString s -> pretty $ show s - VChan _ _ -> pretty "VChan" + VChan {} -> pretty "VChan" + VChanSerial {} -> pretty "VChanSerial" VSend v -> pretty "VSend" VPair a b -> pretty "<" <+> pretty a <+> pretty ", " <+> pretty b <+> pretty ">" VType t -> pretty t diff --git a/src/ProcessEnvironment.hs b/src/ProcessEnvironment.hs index e831b3c..c07e3eb 100644 --- a/src/ProcessEnvironment.hs +++ b/src/ProcessEnvironment.hs @@ -1,114 +1,11 @@ {-# LANGUAGE LambdaCase #-} module ProcessEnvironment where -import Syntax as S -import Control.Concurrent.Chan as C +import ProcessEnvironmentTypes +import Control.Concurrent.MVar as MVar import Control.Monad.Reader as T -import Data.Set (Set) -import qualified Data.Set as Set -import Kinds (Multiplicity(..)) +import Data.Map as Map --- | the interpretation monad -type InterpretM a = T.ReaderT PEnv IO a +import qualified Networking.NetworkingMethod.NetworkingMethodCommon as NMC -extendEnv :: String -> Value -> PEnv -> PEnv -extendEnv = curry (:) - --- | a Process Envronment maps identifiers to Values of expressions and stores -type PEnv = [PEnvEntry] -type PEnvEntry = (String, Value) - -type Label = String -type LabelType = Set Label - -labelsFromList :: [Label] -> LabelType -labelsFromList = Set.fromList - -data FuncType = FuncType PEnv String S.Type S.Type - deriving Eq - -instance Show FuncType where - show (FuncType _ s t1 t2) = "FuncType " ++ show s ++ " " ++ show t1 ++ " " ++ show t2 - --- | (Unit, Label, Int, Values of self-declared Data Types), Channels -data Value - = VUnit - | VLabel String - | VInt Int - | VDouble Double - | VString String - -- we have two channels, one for reading and one for writing to the other - -- end, so we do not read our own written values - | VChan (C.Chan Value) (C.Chan Value) - | VSend Value - | VPair Value Value -- pair of ids that map to two values - | VType S.Type - | VFunc PEnv String Exp - | VDynCast Value GType -- (Value : G => *) - | VFuncCast Value FuncType FuncType -- (Value : (ρ,α,Π(x:A)A') => (ρ,α,Π(x:B)B')) - | VRec PEnv String String Exp Exp - | VNewNatRec PEnv String String String Type Exp String Exp - deriving Eq - -instance Show Value where - show = \case - VUnit -> "VUnit" - VLabel s -> "VLabel " ++ s - VInt i -> "VInt " ++ show i - VDouble d -> "VDouble " ++ show d - VString s -> "VString \"" ++ show s ++ "\"" - VChan _ _ -> "VChan" - VSend v -> "VSend (" ++ show v ++ ")" - VPair a b -> "VPair <" ++ show a ++ ", " ++ show b ++ ">" - VType t -> "VType " ++ show t - VFunc _ s exp -> "VFunc " ++ show s ++ " " ++ show exp - VDynCast v t -> "VDynCast (" ++ show v ++ ") (" ++ show t ++ ")" - VFuncCast v ft1 ft2 -> "VFuncCast (" ++ show v ++ ") (" ++ show ft1 ++ ") (" ++ show ft2 ++ ")" - VRec env f x e1 e0 -> "VRec " ++ " " ++ f ++ " " ++ x ++ " " ++ show e1 ++ " " ++ show e0 - VNewNatRec env f n tid ty ez x es -> "VNewNatRec " ++ f ++ n ++ tid ++ show ty ++ show ez ++ x ++ show es - -class Subtypeable t where - isSubtypeOf :: t -> t -> Bool - --- Types in Head Normal Form -data NFType - = NFBot - | NFDyn - | NFFunc FuncType -- (ρ, α, Π(x: A) B) - | NFPair FuncType -- (ρ, α, Σ(x: A) B) - | NFGType GType -- every ground type is also a type in normal form - deriving (Show, Eq) - -instance Subtypeable NFType where - -- NFFunc and NFPair default to false, which is not really correct. - -- Implementation would be quite complicated and its not necessary, - -- i.e. not used anywhere. - isSubtypeOf NFBot _ = True - isSubtypeOf NFDyn NFDyn = True - isSubtypeOf (NFGType gt1) (NFGType gt2) = gt1 `isSubtypeOf` gt2 - isSubtypeOf _ _ = False - -data GType - = GUnit - | GLabel LabelType - | GFunc Multiplicity -- Π(x: *) * - | GPair -- Σ(x: *) * - | GNat - | GNatLeq Integer - | GInt - | GDouble - | GString - deriving (Show, Eq) - -instance Subtypeable GType where - isSubtypeOf GUnit GUnit = True - isSubtypeOf (GLabel ls1) (GLabel ls2) = ls1 `Set.isSubsetOf` ls2 - isSubtypeOf (GFunc _) (GFunc _) = True - isSubtypeOf (GPair) (GPair) = True - isSubtypeOf GNat GNat = True - isSubtypeOf (GNatLeq _) GNat = True - isSubtypeOf (GNatLeq n1) (GNatLeq n2) = n1 <= n2 - isSubtypeOf GInt GInt = True - isSubtypeOf GDouble GDouble = True - isSubtypeOf GString GString = True - isSubtypeOf _ _ = False +type InterpretM a = T.ReaderT (PEnv, (MVar.MVar (Map.Map Int ServerSocket), VChanConnections, NMC.ActiveConnections)) IO a \ No newline at end of file diff --git a/src/ProcessEnvironmentTypes.hs b/src/ProcessEnvironmentTypes.hs new file mode 100644 index 0000000..06319d8 --- /dev/null +++ b/src/ProcessEnvironmentTypes.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE LambdaCase #-} +module ProcessEnvironmentTypes where +import Syntax as S +import Control.Concurrent.MVar as MVar +import Data.Set (Set) +import Data.Map as Map +import qualified Data.Set as Set +import Kinds (Multiplicity(..)) + +import qualified Networking.NetworkConnection as NCon + +extendEnv :: String -> Value -> PEnv -> PEnv +extendEnv = curry (:) + +-- | a Process Envronment maps identifiers to Values of expressions and stores +type PEnv = [PEnvEntry] +type PEnvEntry = (String, Value) + +type Label = String +type LabelType = Set Label + +labelsFromList :: [Label] -> LabelType +labelsFromList = Set.fromList + +data FuncType = FuncType PEnv String S.Type S.Type + deriving Eq + +instance Show FuncType where + show (FuncType _ s t1 t2) = "FuncType " ++ show s ++ " " ++ show t1 ++ " " ++ show t2 + +type ServerSocket = (MVar.MVar [(String, (Type, Type))], String) + +type VChanConnections = MVar.MVar (Map.Map String (NCon.NetworkConnection Value)) + +type ValueRepr = String + +-- | (Unit, Label, Int, Values of self-declared Data Types), Channels +data Value + = VUnit + | VLabel String + | VInt Int + | VDouble Double + | VString String + | VChan (NCon.NetworkConnection Value) (MVar.MVar Bool) + -- VChanSerials are only used to send VChans to other peers when networking + -- They are never used in normal program flow and should never be directly encountered in modules like the Interpreter + | VChanSerial ([Value], Int, Int) ([Value], Int, Int) String String (String, String, String) + | VSend Value + | VPair Value Value -- pair of ids that map to two values + | VType S.Type + | VFunc PEnv String Exp + | VDynCast Value GType -- (Value : G => *) + | VFuncCast Value FuncType FuncType -- (Value : (ρ,α,Π(x:A)A') => (ρ,α,Π(x:B)B')) + | VRec PEnv String String Exp Exp + | VNewNatRec PEnv String String String Type Exp String Exp + deriving Eq + + +modifyVChansStatic :: (Value -> Value) -> Value -> Value +modifyVChansStatic vchanhandler input = case input of + VSend v -> VSend $ modifyVChansStatic vchanhandler v + VPair v1 v2 -> do + let nv1 = modifyVChansStatic vchanhandler v1 + let nv2 = modifyVChansStatic vchanhandler v2 + VPair nv1 nv2 + VFunc penv a b -> do + let newpenv = modifyVChansPEnvStatic vchanhandler penv + VFunc newpenv a b + VDynCast v g -> do + let nv = modifyVChansStatic vchanhandler v + VDynCast nv g + VFuncCast v a b -> do + let nv = modifyVChansStatic vchanhandler v + VFuncCast nv a b + VRec penv a b c d -> do + let newpenv = modifyVChansPEnvStatic vchanhandler penv + VRec newpenv a b c d + VNewNatRec penv a b c d e f g -> do + let newpenv = modifyVChansPEnvStatic vchanhandler penv + VNewNatRec newpenv a b c d e f g + VChan nc used-> vchanhandler input + VChanSerial r w p o c -> vchanhandler input + _ -> input + where + modifyVChansPEnvStatic :: (Value -> Value) -> [(String, Value)] -> [(String, Value)] + modifyVChansPEnvStatic _ [] = [] + modifyVChansPEnvStatic vchanhandler penvs@(x:xs) = do + let newval = modifyVChansStatic vchanhandler $ snd x + (fst x, newval):modifyVChansPEnvStatic vchanhandler xs + +modifyVChans :: (Value -> IO Value) -> Value -> IO Value +modifyVChans vchanhandler input = case input of + VSend v -> do + nv <- modifyVChans vchanhandler v + return $ VSend nv + VPair v1 v2 -> do + nv1 <- modifyVChans vchanhandler v1 + nv2 <- modifyVChans vchanhandler v2 + return $ VPair nv1 nv2 + VFunc penv a b -> do + newpenv <- modifyVChansPEnv vchanhandler penv + return $ VFunc newpenv a b + VDynCast v g -> do + nv <- modifyVChans vchanhandler v + return $ VDynCast nv g + VFuncCast v a b -> do + nv <- modifyVChans vchanhandler v + return $ VFuncCast nv a b + VRec penv a b c d -> do + newpenv <- modifyVChansPEnv vchanhandler penv + return $ VRec newpenv a b c d + VNewNatRec penv a b c d e f g -> do + newpenv <- modifyVChansPEnv vchanhandler penv + return $ VNewNatRec newpenv a b c d e f g + VChan nc used-> vchanhandler input + VChanSerial r w p o c -> vchanhandler input + _ -> return input + where + modifyVChansPEnv :: (Value -> IO Value) -> [(String, Value)] -> IO [(String, Value)] + modifyVChansPEnv _ [] = return [] + modifyVChansPEnv vchanhandler penvs@(x:xs) = do + newval <- modifyVChans vchanhandler $ snd x + rest <- modifyVChansPEnv vchanhandler xs + return $ (fst x, newval):rest + +searchVChans :: (Value -> IO r) -> r -> (r -> r -> r) -> Value -> IO r +searchVChans vchanhandler defaultResult mergeResults input = case input of + VSend v -> searchVChans vchanhandler defaultResult mergeResults v + + VPair v1 v2 -> do + nv1 <- searchVChans vchanhandler defaultResult mergeResults v1 + nv2 <- searchVChans vchanhandler defaultResult mergeResults v2 + return $ mergeResults nv1 nv2 + VFunc penv a b -> searchVChansPEnv vchanhandler defaultResult mergeResults penv + VDynCast v g -> searchVChans vchanhandler defaultResult mergeResults v + VFuncCast v a b -> searchVChans vchanhandler defaultResult mergeResults v + VRec penv a b c d -> searchVChansPEnv vchanhandler defaultResult mergeResults penv + VNewNatRec penv a b c d e f g -> searchVChansPEnv vchanhandler defaultResult mergeResults penv + VChan nc used-> vchanhandler input + VChanSerial r w p o c -> vchanhandler input + _ -> return defaultResult + where + searchVChansPEnv :: (Value -> IO r) -> r -> (r -> r -> r) -> [(String, Value)] -> IO r + searchVChansPEnv _ defaultResult _ [] = return defaultResult + searchVChansPEnv vchanhandler defaultResult mergeResults penvs@(x:xs) = do + newval <- searchVChans vchanhandler defaultResult mergeResults $ snd x + rest <- searchVChansPEnv vchanhandler defaultResult mergeResults xs + return $ mergeResults newval rest + +disableOldVChan :: Value -> IO Value +disableOldVChan value = case value of + VChan nc used -> do + _ <- MVar.takeMVar used + MVar.putMVar used True + unused <- MVar.newEmptyMVar + MVar.putMVar unused False + return $ VChan nc unused + _ -> return value + +instance Show Value where + show = \case + VUnit -> "VUnit" + VLabel s -> "VLabel " ++ s + VInt i -> "VInt " ++ show i + VDouble d -> "VDouble " ++ show d + VString s -> "VString \"" ++ show s ++ "\"" + VChan {} -> "VChan" + VChanSerial {} -> "VChanSerial" + VSend v -> "VSend (" ++ show v ++ ")" + VPair a b -> "VPair <" ++ show a ++ ", " ++ show b ++ ">" + VType t -> "VType " ++ show t + VFunc _ s exp -> "VFunc " ++ show s ++ " " ++ show exp + VDynCast v t -> "VDynCast (" ++ show v ++ ") (" ++ show t ++ ")" + VFuncCast v ft1 ft2 -> "VFuncCast (" ++ show v ++ ") (" ++ show ft1 ++ ") (" ++ show ft2 ++ ")" + VRec env f x e1 e0 -> "VRec " ++ " " ++ f ++ " " ++ x ++ " " ++ show e1 ++ " " ++ show e0 + VNewNatRec env f n tid ty ez x es -> "VNewNatRec " ++ f ++ n ++ tid ++ show ty ++ show ez ++ x ++ show es + +class Subtypeable t where + isSubtypeOf :: t -> t -> Bool + +-- Types in Head Normal Form +data NFType + = NFBot + | NFDyn + | NFFunc FuncType -- (ρ, α, Π(x: A) B) + | NFPair FuncType -- (ρ, α, Σ(x: A) B) + | NFGType GType -- every ground type is also a type in normal form + deriving (Show, Eq) + +instance Subtypeable NFType where + -- NFFunc and NFPair default to false, which is not really correct. + -- Implementation would be quite complicated and its not necessary, + -- i.e. not used anywhere. + isSubtypeOf NFBot _ = True + isSubtypeOf NFDyn NFDyn = True + isSubtypeOf (NFGType gt1) (NFGType gt2) = gt1 `isSubtypeOf` gt2 + isSubtypeOf _ _ = False + +data GType + = GUnit + | GLabel LabelType + | GFunc Multiplicity -- Π(x: *) * + | GPair -- Σ(x: *) * + | GNat + | GNatLeq Integer + | GInt + | GDouble + | GString + deriving (Show, Eq) + +instance Subtypeable GType where + isSubtypeOf GUnit GUnit = True + isSubtypeOf (GLabel ls1) (GLabel ls2) = ls1 `Set.isSubsetOf` ls2 + isSubtypeOf (GFunc _) (GFunc _) = True + isSubtypeOf (GPair) (GPair) = True + isSubtypeOf GNat GNat = True + isSubtypeOf (GNatLeq _) GNat = True + isSubtypeOf (GNatLeq n1) (GNatLeq n2) = n1 <= n2 + isSubtypeOf GInt GInt = True + isSubtypeOf GDouble GDouble = True + isSubtypeOf GString GString = True + isSubtypeOf _ _ = False diff --git a/src/Syntax.hs b/src/Syntax.hs index e1ba9db..2a8d6ef 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -32,6 +32,9 @@ data Exp = Let Ident Exp Exp | Recv Exp | Case Exp [(String, Exp)] | Cast Exp Type Type + -- New types + | Connect Exp Type Exp Exp -- Connect URL Port Type + | Accept Exp Type -- Accept Socket Type deriving (Show,Eq) data MathOp e @@ -165,6 +168,8 @@ instance Freevars Exp where fv (New ty) = fv ty fv (Send e1) = fv e1 fv (Recv e1) = fv e1 + fv (Connect e0 ty e1 e2) = fv e0 <> fv ty <>fv e1 <> fv e2 + fv (Accept e1 ty) = fv e1 <> fv ty fv (Case e cases) = foldl' (<>) (fv e) $ map (fv . snd) cases fv (Cast e t1 t2) = fv e fv (Succ e) = fv e @@ -231,6 +236,8 @@ instance Substitution Exp where sb (New t) = New t sb (Send e1) = Send (sb e1) sb (Recv e1) = Recv (sb e1) + sb (Connect e0 t e1 e2) = Connect (sb e0) t (sb e1) (sb e2) + sb (Accept e1 t) = Accept (sb e1) t sb (Succ e1) = Succ (sb e1) sb (NatRec e ez y t z tyz es) = NatRec (sb e) (sb ez) y t z (subst x exp tyz) (if x /= y && x /= z then sb es else es) diff --git a/src/TCTyping.hs b/src/TCTyping.hs index 52d7b1f..eb5f610 100644 --- a/src/TCTyping.hs +++ b/src/TCTyping.hs @@ -241,6 +241,41 @@ tySynth te e = New ty -> do kiCheck (demoteTE te) ty Kssn return (TPair "" ty (dualof ty), te) + -- I've got no real clue of what I am doing here hope it kind of works + Connect e1 ty e2 e3 -> do + kiCheck (demoteTE te) ty Kssn + -- check whether e1 is Int + (top, te1) <- tySynth te e1 + topu <- unfold te1 top + case topu of + TInt -> return () + TNat -> return () + _ -> TC.mfail ("Int expected, but got " ++ pshow top ++ " (" ++ pshow topu ++ ")") + -- check whether e2 is String + (tps, te2) <- tySynth te e2 + tpsu <- unfold te2 tps + case tpsu of + TString -> return () + _ -> TC.mfail ("String expected, but got " ++ pshow tps ++ " (" ++ pshow tpsu ++ ")") + -- check whether e3 is Int + (tpp, te3) <- tySynth te e3 + tppu <- unfold te3 tpp + case tppu of + TInt -> return () + TNat -> return () + _ -> TC.mfail ("Int expected, but got " ++ pshow tpp ++ " (" ++ pshow tppu ++ ")") + + return (ty, te) + Accept e1 ty -> do + kiCheck (demoteTE te) ty Kssn + -- check whether e1 is Int + (top, te1) <- tySynth te e1 + topu <- unfold te1 top + case topu of + TInt -> return () + TNat -> return () + _ -> TC.mfail ("Int expected, but got " ++ pshow top ++ " (" ++ pshow topu ++ ")") + return (ty, te) Send e1 -> do (ts, te1) <- tySynth te e1 tsu <- unfold te1 ts diff --git a/src/ValueParsing/ValueGrammar.y b/src/ValueParsing/ValueGrammar.y new file mode 100644 index 0000000..f2a3895 --- /dev/null +++ b/src/ValueParsing/ValueGrammar.y @@ -0,0 +1,374 @@ +{ +module ValueParsing.ValueGrammar (parseValues, parseMessages, parseResponses, parseConversation) where + +import Control.Monad +import Kinds +import Networking.Messages +import ProcessEnvironmentTypes +import Syntax +import ValueParsing.ValueTokens (T(..)) +import qualified Data.List as List +import qualified Data.Set as Set +import qualified ValueParsing.ValueTokens as T + +} + +%monad { T.Alex } +%lexer { (\f -> T.alexMonadScan >>= f) } { T _ T.EOF } +%error { parseError } +%tokentype { T } + +--%name parseDecls Cmds +--%name parseType Typ + +%name parseValues Value +%name parseMessages Message +%name parseResponses Response +%name parseConversation ConversationSession +-- %name parseSStringTypeElement SStringTypeElement +-- %name parseSStringTypeElements SStringTypeElements +-- %name parseSStringTypeArray SStringTypeArray + +%token + vunit { T _ T.VUnit } + vlabel { T _ T.VLabel } + vint { T _ T.VInt } + vdouble { T _ T.VDouble } + vstring { T _ T.VString } + vchan { T _ T.VChan} + vchanserial { T _ T.VChanSerial} + vsend { T _ T.VSend } + vpair { T _ T.VPair } + vtype { T _ T.VType } + vfunc { T _ T.VFunc } + vdyncast { T _ T.VDynCast } + vfunccast { T _ T.VFuncCast } + vrec { T _ T.VRec } + vnewnatrec { T _ T.VNewNatRec } + + tunit { T _ T.TUnit } + tint { T _ T.TInt } + tdouble { T _ T.TDouble } + tbot { T _ T.TBot } + tdyn { T _ T.TDyn } + tnat { T _ T.TNat } + tstring { T _ T.TString } + tnatleq { T _ T.TNatLeq } + tnatrec { T _ T.TNatRec } + tvar { T _ T.TVar } + tabs { T _ T.TAbs } + tname { T _ T.TName } + tlab { T _ T.TLab } + tfun { T _ T.TFun } + tpair { T _ T.TPair } + tsend { T _ T.TSend } + trecv { T _ T.TRecv } + tcase { T _ T.TCase } + teqn { T _ T.TEqn } + tsingle { T _ T.TSingle } + + elet { T _ T.ELet } + emath { T _ T.EMath } + elit { T _ T.ELit } + esucc { T _ T.ESucc } + enatrec { T _ T.ENatRec } + enewnatrec { T _ T.ENewNatRec } + evar { T _ T.EVar } + elam { T _ T.ELam } + erec { T _ T.ERec } + eapp { T _ T.EApp } + epair { T _ T.EPair } + eletpair { T _ T.ELetPair } + efst { T _ T.EFst } + esnd { T _ T.ESnd } + efork { T _ T.EFork } + enew { T _ T.ENew } + esend { T _ T.ESend } + erecv { T _ T.ERecv } + ecase { T _ T.ECase } + ecast { T _ T.ECast } + + madd { T _ T.MAdd } + msub { T _ T.MSub } + mmul { T _ T.MMul } + mdiv { T _ T.MDiv } + mneg { T _ T.MNeg } + + mone { T _ T.MOne } + mmany { T _ T.MMany } + + lint { T _ T.LInt } + lnat { T _ T.LNat } + ldouble { T _ T.LDouble } + llab { T _ T.LLab } + lunit { T _ T.LUnit } + lstring { T _ T.LString } + + sfunctype { T _ T.SFuncType } + slabeltype { T _ T.SLabelType } + sstringexparray { T _ T.SStringExpArray } + sstringtypearray { T _ T.SStringTypeArray } + sstringarray { T _ T.SStringArray } + svaluesarray { T _ T.SValuesArray } + + snetworkconnection {T _ T.SNetworkConnection} + sdirectionalconnection {T _ T.SDirectionalConnection} + sconnected {T _ T.SConnected} + + nintroduce { T _ T.NIntroduce } + nnewvalue { T _ T.NNewValue } + nrequestvalue { T _ T.NRequestValue } + nacknowledgevalue {T _ T.NAcknowledgeValue } + nnewpartneraddress {T _ T.NNewPartnerAddress } + nacknowledgepartneraddress {T _ T.NAcknowledgePartnerAddress } + ndisconnect {T _ T.NDisconnect} + nacknowledgedisconnect {T _ T.NAcknowledgeDisconnect} + + nredirect { T _ T.NRedirect} + nokay { T _ T.NOkay} + nokayintroduce { T _ T.NOkayIntroduce } + nwait { T _ T.NWait } + nerror { T _ T.NError } + nconversationmessage { T _ T.NConversationMessage} + nconversationresponse { T _ T.NConversationResponse} + nconversationcloseall { T _ T.NConversationCloseAll } + + gunit { T _ T.GUnit } + glabel { T _ T.GLabel } + gfunc { T _ T.GFunc } + gpair { T _ T.GPair } + gnat { T _ T.GNat } + gnatleq { T _ T.GNatLeq } + gint { T _ T.GInt } + gdouble { T _ T.GDouble } + gstring { T _ T.GString } + + penv { T _ T.PEnv } + penventry { T _ T.PEnvEntry } + + + int { T _ (T.Int $$) } + integer { T _ (T.Integer $$) } + double { T _ (T.Double $$) } + string { T _ (T.String $$) } + bool { T _ (T.Bool $$) } + + '{' { T _ (T.Sym '{') } + '}' { T _ (T.Sym '}') } +-- '=' { T _ (T.Sym '=') } +-- '+' { T _ (T.Sym '+') } +-- '-' { T _ (T.Sym '-') } +-- '*' { T _ (T.Sym '*') } +-- '/' { T _ (T.Sym '/') } + '(' { T _ (T.Sym '(') } + ')' { T _ (T.Sym ')') } +-- '<' { T _ (T.Sym '<') } +-- '>' { T _ (T.Sym '>') } + '[' { T _ (T.Sym '[') } + ']' { T _ (T.Sym ']') } +-- '!' { T _ (T.Sym '!') } +-- '?' { T _ (T.Sym '?') } +-- '"' { T _ (T.Sym '"') } + ',' { T _ (T.Sym ',') } + +--%right LET +--%nonassoc int double '(' var lab case natrec '()' lam rec fst snd new fork +--%right in +--%nonassoc '>' '<' +--%left '+' '-' NEG POS +--%left '*' '/' +--%left send recv +--%nonassoc APP + + +%% + +-- Values : {[]} +-- | vunit { VUnit } +Value : vunit { VUnit } + | vlabel '(' String ')' {VLabel $3 } + | vint '(' int ')' {VInt $3} + | vdouble '(' double ')' {VDouble $3} + | vstring '(' String ')' {VString $3 } + -- | vchan '(' SValuesArray ')' '(' int ')' '(' SValuesArray ')' '(' int ')' '(' String ')' '(' String ')' '(' String ')' '(' String ')' {VChanSerial $3 $6 $9 $12 $15 $18 $21 $24 } + -- | vchan '(' NetworkConnection ')' {$3} + | vchanserial '(' SArrayIntElement ')' '(' SArrayIntElement ')' '(' String ')' '(' String ')' '(' SStringStringElement3 ')' {VChanSerial $3 $6 $9 $12 $15} + | vsend '(' Value ')' {VSend $3} + | vpair '(' Value ')' '(' Value ')' {VPair $3 $6} + | vtype '(' Type ')' {VType $3} + | vfunc '(' PEnv ')' '(' String ')' '(' Exp ')' {VFunc $3 $6 $9} + | vdyncast '(' Value ')' '(' GType ')' {VDynCast $3 $6} + | vfunccast '(' Value ')' '(' SFuncType ')' '(' SFuncType ')' {VFuncCast $3 $6 $9} + | vrec '(' PEnv ')' '(' String ')' '(' String ')' '(' Exp ')' '(' Exp ')' {VRec $3 $6 $9 $12 $15} + | vnewnatrec '(' PEnv ')' '(' String ')' '(' String ')' '(' String ')' '(' Type ')' '(' Exp ')' '(' String ')' '(' Exp ')' {VNewNatRec $3 $6 $9 $12 $15 $18 $21 $24} + +String : string {trimQuote $1} + +-- NetworkConnection : snetworkconnection '(' DirectionalConnection ')' '(' DirectionalConnection ')' '(' String ')' '(' String ')' '(' ConnectionState ')' {VChanSerial $3 $6 $9 $12 $15} + +-- DirectionalConnection : sdirectionalconnection '(' SValuesArray ')' '(' int ')' {($3, $6)} + +ConnectionState : sconnected '(' String ')' '(' String ')' '(' String ')' {($3, $6, $9)} + + +Mult : mone { MOne } + | mmany { MMany } + +Literal : lint '(' int ')' {LInt $3} + | lnat '(' int ')' {LNat $3} + | ldouble '(' double ')' {LDouble $3} + | llab '(' String ')' {LLab $3} + | lunit {LUnit} + | lstring '(' String ')' {LLab $3} + +SFuncType : sfunctype '(' PEnv ')' '(' String ')' '(' Type ')' '(' Type ')' {FuncType $3 $6 $9 $12} + +Type : tunit {TUnit} + | tint {TInt} + | tdouble {TDouble} + | tbot {TBot} + | tdyn {TDyn} + | tnat {TNat} + | tstring {TString} + | tnatleq '(' integer ')' {TNatLeq $3} + | tnatrec '(' Exp ')' '(' Type ')' '(' String ')' '(' Type ')' {TNatRec $3 $6 $9 $12} + | tvar '(' bool ')' '(' String ')' {TVar $3 $6} + | tabs '(' String ')' '(' Type ')' '(' Type ')' {TAbs $3 $6 $9} + | tname '(' bool ')' '(' String ')' {TName $3 $6} + | tlab '(' SStringArray ')' {TLab $3} + | tfun '(' Mult ')' '(' String ')' '(' Type ')' '(' Type ')' {TFun $3 $6 $9 $12} + | tpair '(' String ')' '(' Type ')' '(' Type ')' {TPair $3 $6 $9} + | tsend '(' String ')' '(' Type ')' '(' Type ')' {TSend $3 $6 $9} + | trecv '(' String ')' '(' Type ')' '(' Type ')' {TRecv $3 $6 $9} + | tcase '(' Exp ')' '(' SStringTypeArray ')' {TCase $3 $6} + | teqn '(' Exp ')' '(' Exp ')' '(' Type ')' {TEqn $3 $6 $9} + | tsingle '(' String ')' {TSingle $3} + +Exp : elet '(' String ')' '(' Exp ')' '(' Exp ')' {Let $3 $6 $9} + | emath '(' MathOp ')' {Math $3} + | elit '(' Literal ')' {Lit $3} + | esucc '(' Exp ')' {Succ $3} + | enatrec '(' Exp ')' '(' Exp ')' '(' String ')' '(' String ')' '(' String ')' '(' Type ')' '(' Exp ')' {NatRec $3 $6 $9 $12 $15 $18 $21} + | enewnatrec '(' String ')' '(' String ')' '(' String ')' '(' Type ')' '(' Exp ')' '(' String ')' '(' Exp ')' {NewNatRec $3 $6 $9 $12 $15 $18 $21} + | evar '(' String ')' {Var $3} + | elam '(' Mult ')' '(' String ')' '(' Type ')' '(' Exp ')' {Lam $3 $6 $9 $12} + | erec '(' String ')' '(' String ')' '(' Exp ')' '(' Exp ')' {Rec $3 $6 $9 $12} + | eapp '(' Exp ')' '(' Exp ')' {App $3 $6} + | epair '(' Mult ')' '(' String ')' '(' Exp ')' '(' Exp ')' {Pair $3 $6 $9 $12} + | eletpair '(' String ')' '(' String ')' '(' Exp ')' '(' Exp ')' {LetPair $3 $6 $9 $12} + | efst '(' Exp ')' {Fst $3} + | esnd '(' Exp ')' {Snd $3} + | efork '(' Exp ')' {Fork $3} + | enew '(' Type ')' {New $3} + | esend '(' Exp ')' {Send $3} + | erecv '(' Exp ')' {Recv $3} + | ecase '(' Exp ')' '(' SStringExpArray ')' {Case $3 $6} + | ecast '(' Exp ')' '(' Type ')' '(' Type ')' {Cast $3 $6 $9} + + +MathOp : madd '(' Exp ')' '(' Exp ')' {Add $3 $6} + | msub '(' Exp ')' '(' Exp ')' {Sub $3 $6} + | mmul '(' Exp ')' '(' Exp ')' {Mul $3 $6} + | mdiv '(' Exp ')' '(' Exp ')' {Div $3 $6} + | mneg '(' Exp ')' {Neg $3 } + +GType : gunit {GUnit} + | glabel '(' LabelType ')' {GLabel (Set.fromList $3) } + | gfunc '(' Mult ')' {GFunc $3} + | gpair {GPair} + | gnat {GNat} + | gnatleq '(' integer ')' {GNatLeq $3} + | gint {GInt} + | gdouble {GDouble} + | gstring {GString} + +Message : nintroduce '(' String ')' '(' String ')' '(' Type ')' '(' Type ')' {Introduce $3 $6 $9 $12} + | nnewvalue '(' String ')' '(' int ')' '(' Value ')' {NewValue $3 $6 $9} + | nrequestvalue '(' String ')' '(' int ')' {RequestValue $3 $6} + | nacknowledgevalue '(' String ')' '(' int ')' {AcknowledgeValue $3 $6} + | nnewpartneraddress '(' String ')' '(' String ')' '(' String ')' {NewPartnerAddress $3 $6 $9} + | nacknowledgepartneraddress '(' String ')' '(' String ')' {AcknowledgePartnerAddress $3 $6} + | ndisconnect '(' String ')' {Disconnect $3} + | nacknowledgedisconnect '(' String ')' {AcknowledgeDisconnect $3} + + + +Response : nredirect '(' String ')' '(' String ')' {Redirect $3 $6} + | nokay {Okay} + | nokayintroduce '(' String ')' {OkayIntroduce $3} + | nwait {Wait} + | nerror {Error} + +ConversationSession : nconversationmessage '(' String ')' '(' Message ')' {ConversationMessage $3 $6} + | nconversationresponse '(' String ')' '(' Response ')' {ConversationResponse $3 $6} + | nconversationcloseall {ConversationCloseAll} + + +PEnvEntry : penventry '(' String ')' '(' Value ')' {($3, $6)} + +PEnv : penv '[' PEnvElements ']' { $3 } + +PEnvElements : PEnvEntry ',' PEnvElements {$1 : $3} + | PEnvEntry {[$1]} + | {- empty -} {[]} + +SStringArray : sstringarray '[' SStringElements ']' {$3} + +SStringElements : String ',' SStringElements {$1 : $3} + | String {[$1]} + | {- empty -} {[]} + +SStringTypeArray : sstringtypearray '[' SStringTypeElements ']' {$3} + +SStringTypeElements : SStringTypeElement ',' SStringTypeElements {$1 : $3} + | SStringTypeElement {[$1]} + | {- empty -} {[]} + +SStringTypeElement : '(' '(' String ')' '(' Type ')' ')' {($3, $6)} + +SStringExpArray : sstringexparray '[' SStringExpElements ']' {$3} + +SStringExpElements : SStringExpElement ',' SStringExpElements {$1 : $3} + | SStringExpElement {[$1]} + | {- empty -} {[]} + +SStringExpElement : '(' '(' String ')' '(' Exp ')' ')' {($3, $6)} + +SValuesArray : svaluesarray '[' SValuesElements ']' {$3} + +SValuesElements : Value ',' SValuesElements {$1 : $3} + | Value {[$1]} + | {- empty -} {[]} + +LabelType : slabeltype '[' SStringElements ']' {$3} + +SArrayIntElement : '(' '(' SValuesArray ')' '(' int ')' '(' int ')' ')' {($3, $6, $9)} + +SStringStringElement : '(' '(' String ')' '(' String ')' ')' {($3, $6)} + +SStringStringElement3 : '(' '(' String ')' '(' String ')' '(' String ')' ')' {($3, $6, $9)} + + + +{ + + +parseError (T (T.AlexPn _ line column) t) = do + nextTokens <- filter (/= T.EOF) . (t:) <$> replicateM 9 (tokVal <$> T.alexMonadScan) + let err | null nextTokens = "parse error: unexpected end of file" + | otherwise = mconcat + [ "parse error at line " + , show line + , ", column " + , show column + , ": unexpected token" + , if null (tail nextTokens) then " " else "s " + , List.intercalate ", " $ showToken <$> nextTokens + ] + T.alexError err + +showToken t = "›" ++ show t ++ "‹" + +trimQuote :: String -> String +trimQuote (_:xs) = init xs +} \ No newline at end of file diff --git a/src/ValueParsing/ValueTokens.x b/src/ValueParsing/ValueTokens.x new file mode 100644 index 0000000..43d27c0 --- /dev/null +++ b/src/ValueParsing/ValueTokens.x @@ -0,0 +1,316 @@ +{ +{-# LANGUAGE BlockArguments #-} +module ValueParsing.ValueTokens + ( -- * Tokens + Token(..) + , AlexPosn(..) + , T(..) + + -- * Alex monad + , Alex + , runAlex + , alexMonadScan + , alexError + , scanner + ) where + +} + +%wrapper "monad" +-- %wrapper "monadUserState" +-- %wrapper "basic" + +$digit = 0-9 -- digits +$alpha = [a-zA-Z] -- alphabetic characters +$lower = [a-z] +$upper = [A-Z] + +tokens :- + + $white+ ; + "VUnit" { tok $ const VUnit } + "VLabel" { tok $ const VLabel } + "VInt" { tok $ const VInt } + "VDouble" { tok $ const VDouble } + "VString" { tok $ const VString } + "VChan" { tok $ const VChan } + "VChanSerial" { tok $ const VChanSerial } + "VSend" { tok $ const VSend } + "VPair" { tok $ const VPair } + "VType" { tok $ const VType } + "VFunc" { tok $ const VFunc } + "VDynCast" { tok $ const VDynCast } + "VFuncCast" { tok $ const VFuncCast } + "VRec" { tok $ const VRec} + "VNewNatRec" { tok $ const VNewNatRec } + + "TUnit" { tok $ const TUnit } + "TInt" { tok $ const TInt } + "TDouble" { tok $ const TDouble } + "TBot" { tok $ const TBot } + "TDyn" { tok $ const TDyn } + "TNat" { tok $ const TNat } + "TString" { tok $ const TString } + "TNatLeq" { tok $ const TNatLeq } + "TNatRec" { tok $ const TNatRec } + "TVar" { tok $ const TVar } + "TAbs" { tok $ const TAbs } + "TName" { tok $ const TName } + "TLab" { tok $ const TLab } + "TFun" { tok $ const TFun } + "TPair" { tok $ const TPair } + "TSend" { tok $ const TSend } + "TRecv" { tok $ const TRecv } + "TCase" { tok $ const TCase } + "TEqn" { tok $ const TEqn } + "TSingle" { tok $ const TSingle } + + "ELet" { tok $ const ELet } + "EMath" { tok $ const EMath } + "ELit" { tok $ const ELit } + "ESucc" { tok $ const ESucc } + "ENatRec" { tok $ const ENatRec } + "ENewNatRec" { tok $ const ENewNatRec } + "EVar" { tok $ const EVar } + "ELam" { tok $ const ELam } + "ERec" { tok $ const ERec } + "EApp" { tok $ const EApp } + "EPair" { tok $ const EPair } + "ELetPair" { tok $ const ELetPair } + "EFst" { tok $ const EFst } + "ESnd" { tok $ const ESnd } + "EFork" { tok $ const EFork } + "ENew" { tok $ const ENew } + "ESend" { tok $ const ESend } + "ERecv" { tok $ const ERecv } + "ECase" { tok $ const ECase } + "ECast" { tok $ const ECast } + + "MAdd" { tok $ const MAdd } + "MSub" { tok $ const MSub } + "MMul" { tok $ const MMul } + "MDiv" { tok $ const MDiv } + "MNeg" { tok $ const MNeg } + + "MOne" { tok $ const ValueParsing.ValueTokens.MOne } + "MMany" { tok $ const ValueParsing.ValueTokens.MMany } + + "LInt" { tok $ const LInt } + "LNat" { tok $ const LNat } + "LDouble" { tok $ const LDouble } + "LLab" { tok $ const LLab } + "LUnit" { tok $ const LUnit } + "LString" { tok $ const LString } + + "SFuncType" { tok $ const SFuncType } + + "GUnit" { tok $ const GUnit } + "GLabel" { tok $ const GLabel } + "GFunc" { tok $ const GFunc } + "GPair" { tok $ const GPair } + "GNat" { tok $ const GNat } + "GNatLeq" { tok $ const GNatLeq } + "GInt" { tok $ const GInt } + "GDouble" { tok $ const GDouble } + "GString" { tok $ const GString } + + "PEnv" { tok $ const PEnv } + "PEnvEntry" { tok $ const PEnvEntry } + "SLabelType" { tok $ const SLabelType } + "SStringExpArray" { tok $ const SStringExpArray } + "SStringTypeArray" { tok $ const SStringTypeArray } + "SStringArray" { tok $ const SStringArray } + "SValuesArray" { tok $ const SValuesArray } + "SNetworkConnection" { tok $ const SNetworkConnection} + "SDirectionalConnection" { tok $ const SDirectionalConnection} + "SConnected" { tok $ const SConnected} + + "NIntroduce" { tok $ const NIntroduce } + "NNewValue" { tok $ const NNewValue } + "NRequestValue" { tok $ const NRequestValue } + "NAcknowledgeValue" { tok $ const NAcknowledgeValue } + "NNewPartnerAddress" { tok $ const NNewPartnerAddress } + "NAcknowledgePartnerAddress" { tok $ const NAcknowledgePartnerAddress } + "NDisconnect" { tok $ const NDisconnect } + "NAcknowledgeDisconnect" { tok $ const NAcknowledgeDisconnect } + "NRedirect" { tok $ const NRedirect } + "NOkay" { tok $ const NOkay } + "NOkayIntroduce" { tok $ const NOkayIntroduce } + "NWait" { tok $ const NWait } + "NError" { tok $ const NError } + "NConversationMessage" { tok $ const NConversationMessage } + "NConversationResponse" { tok $ const NConversationResponse } + "NConversationCloseAll" { tok $ const NConversationCloseAll } + + Double\:[\-]?[0-9]+[\.][0-9]+ { tok $ Double . read . (drop 7) } + Int\:[\-]?[0-9]+ { tok $ Int . read . (drop 4)} + Integer\:[\-]?[0-9]+ { tok $ Integer . read . (drop 8)} + String\:\"[^\"]*\" { tok $ String . (drop 7)} + "Bool:False" { tok $ Bool . ignoreArgument False} + "Bool:True" { tok $ Bool . ignoreArgument True} + -- TODO: Add proper String parsing: https://www.jyotirmoy.net/posts/2015-08-17-alex-happy-startcodes.html + [\=\+\-\*\/\(\)\:\!\?\{\}\[\]\<\>\,] { tok $ Sym . head } +{ +-- The token type: +-- | (Unit, Label, Int, Values of self-declared Data Types), Channels +data Token + = VUnit + | VLabel + | VInt + | VDouble + | VString + | VChan + | VChanSerial + | VSend + | VPair + | VType + | VFunc + | VDynCast + | VFuncCast + | VRec + | VNewNatRec + + | TUnit + | TInt + | TDouble + | TBot + | TDyn + | TNat + | TString + | TNatLeq + | TNatRec + | TVar + | TAbs + | TName + | TLab + | TFun + | TPair + | TSend + | TRecv + | TCase + | TEqn + | TSingle + + | ELet + | EMath + | ELit + | ESucc + | ENatRec + | ENewNatRec + | EVar + | ELam + | ERec + | EApp + | EPair + | ELetPair + | EFst + | ESnd + | EFork + | ENew + | ESend + | ERecv + | ECase + | ECast + + | MAdd + | MSub + | MMul + | MDiv + | MNeg + + | MOne + | MMany + + | LInt + | LNat + | LDouble + | LLab + | LUnit + | LString + + | SFuncType + + | GUnit + | GLabel + | GFunc + | GPair + | GNat + | GNatLeq + | GInt + | GDouble + | GString + + | PEnv + | PEnvEntry + + | SLabelType + + | SStringExpArray + | SStringTypeArray + | SStringArray + | SValuesArray + + | SNetworkConnection + | SDirectionalConnection + | SConnected + + | NIntroduce + | NNewValue + | NRequestValue + | NAcknowledgeValue + | NNewPartnerAddress + | NAcknowledgePartnerAddress + | NDisconnect + | NAcknowledgeDisconnect + | NRedirect + | NOkay + | NOkayIntroduce + | NWait + | NError + | NConversationMessage + | NConversationResponse + | NConversationCloseAll + + | String String + | Int Int + | Integer Integer + | Double Double + | Bool Bool + + | Sym Char + | EOF + deriving (Eq, Show) + +data T = T { tokPos :: AlexPosn, tokVal :: !Token } + deriving (Eq, Show) + +alexEOF :: Alex T +alexEOF = do + (pos, _, _, _) <- alexGetInput + pure $ T pos EOF + +tok :: (String -> Token) -> AlexAction T +tok f = tok' (Right . f) + +tok' :: (String -> Either String Token) -> AlexAction T +tok' f (pos@(AlexPn _ line column), _, _, inp) len = do + let inp' = take len inp + case f inp' of + Left err -> alexError $ mconcat + [ "lexical error at line " + , show line + , ", column " + , show column + , if null err then "" else (": " ++ err) + ] + Right tok -> pure $ T pos tok + + +scanner str = runAlex str $ loop [] + where + loop i = do + tok <- alexMonadScan + if (tokVal tok) == EOF then return i else loop $! (i++[(tokVal tok)]) + +ignoreArgument a b = a +} diff --git a/stack.yaml b/stack.yaml index 46397eb..b2b0d7f 100644 --- a/stack.yaml +++ b/stack.yaml @@ -17,7 +17,7 @@ # # resolver: ./custom-snapshot.yaml # resolver: https://example.com/snapshots/2018-01-01.yaml -resolver: lts-18.8 +resolver: lts-20.21 # User packages to be built. # Various formats can be used as shown in the example below. @@ -39,7 +39,8 @@ packages: # - git: https://github.com/commercialhaskell/stack.git # commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a # -# extra-deps: [] +extra-deps: + - 'validation-selective-0.2.0.0' # Override default flag values for local packages and extra-deps # flags: {} diff --git a/syntax.txt b/syntax.txt index a445f28..e5205f1 100644 --- a/syntax.txt +++ b/syntax.txt @@ -40,6 +40,7 @@ lab ::= "'" id T ::= "Unit" | "Int" | "Bot" + | "String" | TID | "{" lab { "," lab } "}" | "case" M "of" "{" lab ":" T { "," lab ":" T } "}" @@ -72,6 +73,11 @@ M ::= "()" | "case" M "of" "{" lab ":" M { "," lab ":" M } "}" | "(" M ")" +## LDGVNW: + + | accept Int T + | connect Int T String Int + ## later: | "select" lab diff --git a/test/BufferSpec.hs b/test/BufferSpec.hs new file mode 100644 index 0000000..3028374 --- /dev/null +++ b/test/BufferSpec.hs @@ -0,0 +1,72 @@ +module BufferSpec (spec) where + +import Networking.Buffer +import Test.Hspec + +spec :: Spec +spec = do + describe "Buffer IO Test" $ do + it "Empty list" $ emptyBufferTest `shouldReturn` [] + it "Take from empty" $ tryTakeFromEmptyBufferTest `shouldReturn` Nothing + it "Read from empty" $ tryReadFromEmptyBufferTest `shouldReturn` Nothing + it "One Element in Buffer" $ (bufferWith42 >>= writeBufferToList) `shouldReturn` [42] + it "One Element in Clone" $ (bufferWith42AndClone >>= writeBufferToList . snd) `shouldReturn` [42] + it "Two Elements in Clone" $ (bufferWith42And1337AndClone >>= writeBufferToList . snd) `shouldReturn` [42, 1337] + it "Two Elements in Buffer" $ (bufferWith42And1337AndClone >>= writeBufferToList . fst) `shouldReturn` [42, 1337] + it "Try Read from Clone" $ (bufferWith42And1337AndClone >>= tryReadBuffer . snd) `shouldReturn` Just 42 + it "Read from Clone" $ (bufferWith42And1337AndClone >>= readBuffer . snd) `shouldReturn` 42 + it "Take from Clone" $ (bufferWith42And1337AndClone >>= takeBuffer . snd) `shouldReturn` 42 + it "Try Take from Clone" $ (bufferWith42And1337AndCloneTake42 >>= tryReadBuffer . snd) `shouldReturn` Just 1337 + it "Two Elements in Buffer #2" $ (bufferWith42And1337AndCloneTake42And1337 >>= writeBufferToList . fst) `shouldReturn` [42, 1337] + it "No Elements in Clone" $ (bufferWith42And1337AndCloneTake42And1337 >>= writeBufferToList . snd) `shouldReturn` [] + it "Three Elements in Buffer " $ (bufferWith42And1337And1AndCloneTake42And1337 >>= writeBufferToList . fst) `shouldReturn` [42, 1337, 1] + it "One Element in Clone #2" $ (bufferWith42And1337And1AndCloneTake42And1337 >>= writeBufferToList . snd) `shouldReturn` [1] + + + + +emptyBufferTest :: IO [Integer] +emptyBufferTest = newBuffer >>= writeBufferToList + +tryTakeFromEmptyBufferTest :: IO (Maybe Integer) +tryTakeFromEmptyBufferTest = newBuffer >>= tryTakeBuffer + +tryReadFromEmptyBufferTest :: IO (Maybe Integer) +tryReadFromEmptyBufferTest = newBuffer >>= tryReadBuffer + + +bufferWith42 :: IO (Buffer Integer) +bufferWith42 = do + newBuf <- newBuffer + writeBuffer newBuf 42 + return newBuf + +bufferWith42AndClone :: IO (Buffer Integer, Buffer Integer) +bufferWith42AndClone = do + buf <- bufferWith42 + clone <- cloneBuffer buf + return (buf, clone) + +bufferWith42And1337AndClone :: IO (Buffer Integer, Buffer Integer) +bufferWith42And1337AndClone = do + (buf, clone) <- bufferWith42AndClone + writeBuffer clone 1337 + return (buf, clone) + +bufferWith42And1337AndCloneTake42 :: IO (Buffer Integer, Buffer Integer) +bufferWith42And1337AndCloneTake42 = do + (buf, clone) <-bufferWith42And1337AndClone + takeBuffer clone + return (buf, clone) + +bufferWith42And1337AndCloneTake42And1337 :: IO (Buffer Integer, Buffer Integer) +bufferWith42And1337AndCloneTake42And1337 = do + (buf, clone) <-bufferWith42And1337AndCloneTake42 + tryTakeBuffer clone + return (buf, clone) + +bufferWith42And1337And1AndCloneTake42And1337 :: IO (Buffer Integer, Buffer Integer) +bufferWith42And1337And1AndCloneTake42And1337 = do + (buf, clone) <-bufferWith42And1337AndCloneTake42And1337 + writeBuffer buf 1 + return (buf, clone) \ No newline at end of file diff --git a/test/CSpec.hs b/test/CSpec.hs index 4d041ef..7077cc1 100644 --- a/test/CSpec.hs +++ b/test/CSpec.hs @@ -22,7 +22,7 @@ import C.Compile as C import C.Generate import Interpreter (interpret) import Parsing -import ProcessEnvironment (Value(..)) +import ProcessEnvironmentTypes import Typechecker (typecheck, Options(..)) import qualified Examples diff --git a/test/InterpreterSpec.hs b/test/InterpreterSpec.hs index eda367d..a0f1a57 100644 --- a/test/InterpreterSpec.hs +++ b/test/InterpreterSpec.hs @@ -6,7 +6,7 @@ import Utils import Kinds import Syntax import Interpreter -import ProcessEnvironment +import ProcessEnvironmentTypes import UtilsFuncCcldlc spec :: Spec diff --git a/test/NetworkBufferSpec.hs b/test/NetworkBufferSpec.hs new file mode 100644 index 0000000..a64adaf --- /dev/null +++ b/test/NetworkBufferSpec.hs @@ -0,0 +1,46 @@ +module NetworkBufferSpec (spec) where + +import Networking.NetworkBuffer +import Test.Hspec + +spec :: Spec +spec = do + describe "NetworkBuffer IO Test" $ do + it "All Acknowledged" $ (nb >>= isAllAcknowledged) `shouldReturn` True + it "Not All Acknowledged " $ (nb42 >>= isAllAcknowledged) `shouldReturn` False + it "Serialize" $ (nb42 >>= serializeMinimal) `shouldReturn` ([42], 0, 1) + it "Serialize #2" $ (nb42And1337 >>= serializeMinimal) `shouldReturn` ([42, 1337], 0, 2) + it "Try Read at 0" $ (nb42And1337 >>= \x -> tryGetAtNB x 0) `shouldReturn` Just 42 + it "Try Read at 1" $ (nb42And1337 >>= \x -> tryGetAtNB x 1) `shouldReturn` Just 1337 + it "Try Take" $ (nb42And1337 >>= tryTake) `shouldReturn` Just (42, 0) + it "Next Offset" $ (nb1337 >>= getNextOffset) `shouldReturn` 1 + it "Serialize #3" $ (nb1337 >>= serializeMinimal) `shouldReturn` ([1337], 1, 2) + it "All Acknowledged #2" $ (nb1337AllAck >>= isAllAcknowledged) `shouldReturn` True + it "Serialize #4" $ (nb1337AllAck >>= serializeMinimal) `shouldReturn` ([], 2, 2) + +nb :: IO (NetworkBuffer Integer) +nb = newNetworkBuffer + +nb42 :: IO (NetworkBuffer Integer) +nb42 = do + nb <- newNetworkBuffer + write nb 42 + return nb + +nb42And1337 :: IO (NetworkBuffer Integer) +nb42And1337 = do + nb <- nb42 + write nb 1337 + return nb + +nb1337 :: IO (NetworkBuffer Integer) +nb1337 = do + nb <- nb42And1337 + tryTake nb + return nb + +nb1337AllAck :: IO (NetworkBuffer Integer) +nb1337AllAck = do + nb <- nb1337 + updateAcknowledgements nb 1 + return nb diff --git a/test/SerializeSpec.hs b/test/SerializeSpec.hs new file mode 100644 index 0000000..88f34df --- /dev/null +++ b/test/SerializeSpec.hs @@ -0,0 +1,43 @@ +module SerializeSpec (spec) where + +import Networking.Messages +import Syntax +import Test.Hspec +import ProcessEnvironmentTypes +import qualified Data.Set as Set + +import Utils + +spec :: Spec +spec = do + describe "Serialize Values" $ do + it "VUnit" $ serializesConsistentlyValue VUnit + it "VLabel" $ serializesConsistentlyValue $ VLabel "MyLabel" + it "VInt" $ serializesConsistentlyValue $ VInt 42 + it "VDouble" $ serializesConsistentlyValue $ VDouble 42.1337 + it "VString" $ serializesConsistentlyValue $ VString "Hello World" + it "VSend" $ serializesConsistentlyValue $ VSend $ VString "Hello World" + it "VPair" $ serializesConsistentlyValue $ VPair (VInt 1337) (VLabel "var") + it "VType" $ serializesConsistentlyValue $ VType $ TNatLeq 42 + it "VFunc" $ serializesConsistentlyValue $ VFunc [("s1", VString "String1"), ("i1", VInt 32)] "VFuncString" (Math (Add (Var "v1") (Lit (LInt 42)))) + it "VDynCast" $ serializesConsistentlyValue $ VDynCast VUnit (GLabel (Set.fromList ["String1", "String2"])) + it "VFuncCast" $ serializesConsistentlyValue $ VFuncCast (VInt 42) (FuncType [("s1", VString "String1"), ("i1", VInt 32)] "FuncTypeString" TUnit TInt) (FuncType [("s2", VString "String2"), ("i2", VInt 42)] "FuncTypeString2" TInt (TVar False "Ident1")) + it "VChanSerial" $ serializesConsistentlyValue $ VChanSerial ([VInt 42], 2, 3) ([], 0, 0) "partnerID" "ownID" ("127.0.0.1", "4242", "conversationID") + describe "Serialize Messages" $ do + it "Introduce" $ serializesConsistentlyMessage $ Introduce "userID" "4242" (TName False "TestName") (TSend "#!" TInt (TRecv "#?" TString TUnit)) + it "NewValue" $ serializesConsistentlyMessage $ NewValue "userID" 2 $ VInt 42 + it "RequestValue" $ serializesConsistentlyMessage $ RequestValue "userID" 42 + it "AcknowledgeValue" $ serializesConsistentlyMessage $ AcknowledgeValue "userID" 42 + it "NewPartnerAddress" $ serializesConsistentlyMessage $ NewPartnerAddress "userID" "4200" "conID1337" + it "AcknowledgePartnerAddress" $ serializesConsistentlyMessage $ AcknowledgePartnerAddress "partnerID" "conID1337" + it "Disconnect" $ serializesConsistentlyMessage $ Disconnect "ownID" + describe "Serialize Responses" $ do + it "Redirect" $ serializesConsistentlyResponse $ Redirect "42.0.0.1" "1337" + it "Okay" $ serializesConsistentlyResponse Okay + it "OkayIntroduce" $ serializesConsistentlyResponse $ OkayIntroduce "ownID" + it "Wait" $ serializesConsistentlyResponse Wait + it "Error" $ serializesConsistentlyResponse Error + describe "Serialize ConversationSession" $ do + it "ConversationMessage" $ serializesConsistentlyConversation $ ConversationMessage "conv42" $ NewValue "userID" 2 $ VInt 42 + it "ConversationResponse" $ serializesConsistentlyConversation $ ConversationResponse "conv42" Okay + it "ConversationCloseAll" $ serializesConsistentlyConversation ConversationCloseAll \ No newline at end of file diff --git a/test/Utils.hs b/test/Utils.hs index 0da4917..9a97b57 100644 --- a/test/Utils.hs +++ b/test/Utils.hs @@ -3,9 +3,15 @@ module Utils where import Parsing import Syntax import Interpreter -import ProcessEnvironment +import ProcessEnvironmentTypes +import qualified Networking.Common as NC +import qualified Networking.Serialize as NSer +import qualified ValueParsing.ValueGrammar as VG +import qualified ValueParsing.ValueTokens as VT import Control.Monad.Reader (runReaderT) import Test.Hspec +import Control.Concurrent.MVar +import qualified Data.Map as Map shouldParseDecl :: HasCallStack => String -> Decl -> Expectation shouldParseDecl source expected = @@ -18,7 +24,10 @@ raiseFailure msg = do shouldInterpretTo :: [Decl] -> Value -> Expectation shouldInterpretTo givenDecls expectedValue = do - value <- runReaderT (interpretDecl givenDecls) [] + sockets <- newMVar Map.empty + vchanconnections <- newMVar Map.empty + handles <- NC.createActiveConnections + value <- runReaderT (interpretDecl givenDecls) ([], (sockets, vchanconnections, handles)) value `shouldBe` expectedValue shouldThrowCastException :: [Decl] -> Expectation @@ -26,12 +35,51 @@ shouldThrowCastException givenDecls = let isCastException :: InterpreterException -> Bool isCastException (CastException _) = True isCastException _ = False - in runReaderT (interpretDecl givenDecls) [] `shouldThrow` isCastException + in do + sockets <- newMVar Map.empty + vchanconnections <- newMVar Map.empty + handles <- NC.createActiveConnections + runReaderT (interpretDecl givenDecls) ([], (sockets, vchanconnections, handles)) `shouldThrow` isCastException shouldThrowInterpreterException :: Decl -> InterpreterException -> Expectation -shouldThrowInterpreterException given except = runReaderT (interpretDecl [given]) [] `shouldThrow` (== except) +shouldThrowInterpreterException given except = do + sockets <- newMVar Map.empty + vchanconnections <- newMVar Map.empty + handles <- NC.createActiveConnections + runReaderT (interpretDecl [given]) ([], (sockets, vchanconnections, handles)) `shouldThrow` (== except) shouldInterpretTypeTo :: Type -> NFType -> Expectation shouldInterpretTypeTo t expected = do - nft <- runReaderT (evalType t) [] + sockets <- newMVar Map.empty + vchanconnections <- newMVar Map.empty + handles <- NC.createActiveConnections + nft <- runReaderT (evalType t) ([], (sockets, vchanconnections, handles)) nft `shouldBe` expected + +serializesConsistentlyValue :: NSer.Serializable a => a -> Expectation +serializesConsistentlyValue serializable = + let serial = NSer.serialize serializable in + case VT.runAlex serial VG.parseValues of + Left err -> err `shouldBe` serial + Right deserial -> NSer.serialize deserial `shouldBe` serial + +serializesConsistentlyMessage :: NSer.Serializable a => a -> Expectation +serializesConsistentlyMessage serializable = + let serial = NSer.serialize serializable in + case VT.runAlex serial VG.parseMessages of + Left err -> err `shouldBe` serial + Right deserial -> NSer.serialize deserial `shouldBe` serial + +serializesConsistentlyResponse :: NSer.Serializable a => a -> Expectation +serializesConsistentlyResponse serializable = + let serial = NSer.serialize serializable in + case VT.runAlex serial VG.parseResponses of + Left err -> err `shouldBe` serial + Right deserial -> NSer.serialize deserial `shouldBe` serial + +serializesConsistentlyConversation :: NSer.Serializable a => a -> Expectation +serializesConsistentlyConversation serializable = + let serial = NSer.serialize serializable in + case VT.runAlex serial VG.parseConversation of + Left err -> err `shouldBe` serial + Right deserial -> NSer.serialize deserial `shouldBe` serial \ No newline at end of file