content: {-
      This module adds Json encoding and decoding capabilities
      to the SemanticTypes generated by Isabelle.
  
      It is written with Literal Haskell to be both the actual code
      and part of the specification.
  -}
  
  -- To use lhs2TeX we need to include the "template" of tex generation
  %include polycode.fmt
  
  -- We configure ghci to include the relevant files so that \eval can print
  -- them
  %options cabal exec ghci -- -iisabelle/generated:isabelle/haskell
  
  -- The tex that this file generates includes all the necesary directives
  -- to be called by pdflatex directly, but we are actually including this
  -- inside of the specification that Isabelle generates, so we need to
  -- provide a...
  -- ===PATTERN FOR SED===
  
  %if False
  -- Everything inside the `if False` block is not seen by lhs2TeX but is
  -- seen by Haskell.
  \begin{code}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  
  module MarloweCoreJson where
  
  import Arith (Int(..))
  import qualified Arith
  import Control.Applicative ((<|>), (<*>))
  import CoreOrphanEq
  import ArithNumInstance
  import Data.Aeson (object, withArray, withObject, withText, withScientific, (.=), (.:), (.:?), encode)
  import Data.Aeson.Types (Parser, ToJSON(..), FromJSON(..))
  import qualified Data.Aeson.Types as JSON
  import Data.Aeson.Encode.Pretty (encodePretty)
  import qualified Data.ByteString.Lazy as L
  import qualified Data.ByteString.Lazy.Char8 as C
  import qualified Data.Foldable as F
  import qualified Data.Text as T
  import Data.Scientific (Scientific, floatingOrInteger)
  import qualified Examples.Swap
  import SemanticsTypes (Action(..), Case(..), Contract(..), Input(..), Party(..), Token(..), Payee(..), ChoiceId(..), ValueId(..), Value(..), Observation(..), Bound(..), State_ext(..), IntervalError(..), Environment_ext(..), Transaction_ext(..), Payment(..), TransactionWarning(..), TransactionError(..), TransactionOutput(..), TransactionOutputRecord_ext(..), txOutWarnings, txOutPayments, txOutState, txOutContract, )
  import Semantics (playTrace)
  
  
  
  -- These are some helper functions to print and pretty print a ToJSON example
  encodeExample :: ToJSON a => a -> IO ()
  encodeExample a = putStrLn $ C.unpack $ encode a
  
  prettyEncodeExample :: ToJSON a => a -> IO ()
  prettyEncodeExample a = putStrLn $ wrapInVerbatim $ C.unpack $ encodePretty a
      where
      wrapInVerbatim :: String -> String
      wrapInVerbatim str = "\\begin{verbatim}" ++ str ++ "\\end{verbatim}"
  
  \end{code}
  %endif
  
  The Json specification for Marlowe Core is defined in Literate Haskell using the Aeson library. In order
  to fully understand the specification, some knowledge of Haskell and the library is recommended but not necessary.
  \par
  
  For each Marlowe datatype we define a way to parse the JSON into a value (FromJSON instances) and a way to serialize a
  value to JSON (ToJSON instances).
  
  \isamarkupsection{Party}
  
  Parties are serialized as a simple object with an \emph{address} or \emph{role\_token} key, depending on the
  \emph{Party} type.
  \par
  
  \begin{code}
  instance ToJSON Party where
      toJSON (Address address) =
          object ["address" .= address]
      toJSON (Role name) =
          object ["role_token" .= name]
  
  instance FromJSON Party where
      parseJSON = withObject "Party" $
          \v -> asAddress v <|> asRole v
        where
        asAddress v = Address <$> v .: "address"
        asRole v = Role <$> v .: "role_token"
  
  \end{code}
  \par
  
  for example, the following \emph{Party}
  
  \begin{code}
  addressExample :: Party
  addressExample = Address "example address"
  \end{code}
  
  is serialized as \eval{encodeExample addressExample}, and
  
  \begin{code}
  roleExample :: Party
  roleExample = Role "example role"
  \end{code}
  \par
  
  is serialized as \eval{encodeExample roleExample}
  
  \isamarkupsection{Token}
  
  The \emph{Token} type is serialized as an object with two properties, \emph{currency\_symbol} and
  \emph{token\_name}
  
  
  \begin{code}
  
  instance ToJSON Token where
    toJSON (Token currSym tokName) = object
        [ "currency_symbol" .= currSym
        , "token_name" .= tokName
        ]
  
  
  instance FromJSON Token where
    parseJSON = withObject "Token"
      (\v ->
         Token <$> (v .: "currency_symbol")
               <*> (v .: "token_name")
      )
  
  \end{code}
  
  for example, the following \emph{Token}
  
  \begin{code}
  
  dolarToken :: Token
  dolarToken = Token "85bb65" "dolar"
  \end{code}
  
  is serialized as \eval{encodeExample dolarToken}
  
  \isamarkupsection{Payee}
  
  Payees are serialized as a simple object with an \emph{account} or \emph{party} key, depending on the
  \emph{Payee} type.
  \par
  
  \begin{code}
  instance ToJSON Payee where
      toJSON (Account account) =
          object ["account" .= account]
      toJSON (Party party) =
          object ["party" .= party]
  
  instance FromJSON Payee where
      parseJSON = withObject "Payee" $
          \v -> asAccount v <|> asParty v
        where
        asAccount v = Account <$> v .: "account"
        asParty v = Party <$> v .: "party"
  
  \end{code}
  
  for example, the following \emph{Payee}
  
  \begin{code}
  internalPayeeExample :: Payee
  internalPayeeExample = Account addressExample
  \end{code}
  
  is serialized as \eval{encodeExample internalPayeeExample}, and
  
  \begin{code}
  externalPayeeExample :: Payee
  externalPayeeExample = Party roleExample
  \end{code}
  \par
  
  is serialized as \eval{encodeExample externalPayeeExample}
  
  \isamarkupsection{ChoicesId}
  
  The \emph{ChoiceId} type is serialized as an object with two properties, \emph{choice\_name} and
  \emph{choice\_owner}
  
  
  \begin{code}
  
  instance ToJSON ChoiceId where
    toJSON (ChoiceId name party) = object
        [ "choice_name" .= name
        , "choice_owner" .= party
        ]
  
  
  instance FromJSON ChoiceId where
    parseJSON = withObject "ChoiceId"
      (\v ->
         ChoiceId <$> (v .: "choice_name")
                  <*> (v .: "choice_owner")
      )
  
  \end{code}
  
  for example, the following \emph{ChoiceId}
  
  \begin{code}
  choiceIdExample :: ChoiceId
  choiceIdExample = ChoiceId "ada price" addressExample
  \end{code}
  
  
  is serialized as
  
  \perform{prettyEncodeExample choiceIdExample}
  
  
  \isamarkupsection{Bound}
  
  The \emph{Bound} type is serialized as an object with two properties, \emph{from} and
  \emph{to}
  
  \begin{code}
  instance ToJSON Bound where
    toJSON (Bound from to) = object
        [ "from" .= from
        , "to" .= to
        ]
  
  instance FromJSON Bound where
    parseJSON = withObject "Bound" (\v ->
         Bound <$> (getInteger "lower bound" =<< (v .: "from"))
               <*> (getInteger "higher bound" =<< (v .: "to"))
                                   )
  \end{code}
  
  for example, the following \emph{Bound}
  
  \begin{code}
  exampleBound :: Bound
  exampleBound = Bound 2 10
  \end{code}
  
  is serialized as \eval{encodeExample exampleBound}
  
  \isamarkupsection{Values}
  
  The \emph{ValueId} type is serialized as a literal string.
  
  \begin{code}
  instance ToJSON ValueId where
      toJSON (ValueId x) = toJSON x
  
  instance FromJSON ValueId where
      parseJSON = withText "ValueId" $ return . ValueId . T.unpack
  \end{code}
  
  The \emph{Value} serialization depends on the constructor. A \emph{Constant}
  is serialized as a \emph{number}, \emph{TimeIntervalStart} and \emph{TimeIntervalEnd} are serialized as literal
  strings, and the rest are serialized as a single object (with keys depending on the constructor).
  
  \begin{code}
  instance ToJSON Value where
    toJSON (AvailableMoney accountId token) = object
        [ "amount_of_token" .= token
        , "in_account" .= accountId
        ]
    toJSON (Constant (Int_of_integer x)) = toJSON x
    toJSON (NegValue x) = object
        [ "negate" .= x ]
    toJSON (AddValue lhs rhs) = object
        [ "add" .= lhs
        , "and" .= rhs
        ]
    toJSON (SubValue lhs rhs) = object
        [ "value" .= lhs
        , "minus" .= rhs
        ]
    toJSON (MulValue lhs rhs) = object
        [ "multiply" .= lhs
        , "times" .= rhs
        ]
    toJSON (DivValue lhs rhs) = object
        [ "divide" .= lhs
        , "by" .= rhs
        ]
    toJSON (ChoiceValue choiceId) = object
        [ "value_of_choice" .= choiceId ]
    toJSON TimeIntervalStart = JSON.String $ T.pack "time_interval_start"
    toJSON TimeIntervalEnd = JSON.String $ T.pack "time_interval_end"
    toJSON (UseValue valueId) = object
        [ "use_value" .= valueId ]
    toJSON (Cond obs tv ev) = object
        [ "if" .= obs
        , "then" .= tv
        , "else" .= ev
        ]
  
  instance FromJSON Value where
    parseJSON (JSON.Object v) =
          (AvailableMoney <$> (v .: "in_account")
                          <*> (v .: "amount_of_token"))
      <|> (NegValue <$> (v .: "negate"))
      <|> (AddValue <$> (v .: "add")
                    <*> (v .: "and"))
      <|> (SubValue <$> (v .: "value")
                    <*> (v .: "minus"))
      <|> (MulValue <$> (v .: "multiply")
                    <*> (v .: "times"))
      <|> (DivValue <$> (v .: "divide") <*> (v .: "by"))
      <|> (ChoiceValue <$> (v .: "value_of_choice"))
      <|> (UseValue <$> (v .: "use_value"))
      <|> (Cond <$> (v .: "if")
                <*> (v .: "then")
                <*> (v .: "else"))
    parseJSON (JSON.String "time_interval_start") = return TimeIntervalStart
    parseJSON (JSON.String "time_interval_end") = return TimeIntervalEnd
    parseJSON (JSON.Number n) = Constant <$> getInteger "constant value" n
    parseJSON _ = fail "Value must be either a string, object or an integer"
  
  \end{code}
  
  Here are some examples for each \emph{Value}s constructor:
  
  \isamarkupsubsubsection{Constant}
  
  \begin{code}
  constantExample :: Value
  constantExample = Constant 1
  \end{code}
  
  is serialized as \eval{encodeExample constantExample}
  
  \isamarkupsubsubsection{TimeIntervalStart}
  
  \begin{code}
  intervalStartExample :: Value
  intervalStartExample = TimeIntervalStart
  \end{code}
  
  is serialized as \eval{encodeExample intervalStartExample}
  
  \isamarkupsubsubsection{TimeIntervalEnd}
  
  \begin{code}
  intervalEndExample :: Value
  intervalEndExample = TimeIntervalEnd
  \end{code}
  
  is serialized as \eval{encodeExample intervalEndExample}
  
  \isamarkupsubsubsection{AddValue}
  
  \begin{code}
  addExample :: Value
  addExample = AddValue (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample addExample}
  
  
  \isamarkupsubsubsection{SubValue}
  
  \begin{code}
  subExample :: Value
  subExample = SubValue (Constant 4) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample subExample}
  
  
  \isamarkupsubsubsection{MulValue}
  
  \begin{code}
  mulExample :: Value
  mulExample = MulValue (Constant 3) (Constant 6)
  \end{code}
  
  is serialized as \eval{encodeExample mulExample}
  
  
  \isamarkupsubsubsection{DivValue}
  
  \begin{code}
  divExample :: Value
  divExample = DivValue (Constant 8) (Constant 4)
  \end{code}
  
  is serialized as \eval{encodeExample divExample}
  
  \isamarkupsubsubsection{NegValue}
  
  \begin{code}
  negateExample :: Value
  negateExample = NegValue (Constant 3)
  \end{code}
  
  is serialized as \eval{encodeExample negateExample}
  
  \isamarkupsubsubsection{ChoiceValue}
  
  \begin{code}
  choiceValueExample :: Value
  choiceValueExample = ChoiceValue choiceIdExample
  \end{code}
  
  is serialized as \perform{prettyEncodeExample choiceValueExample}
  
  \isamarkupsubsubsection{UseValue}
  
  \begin{code}
  useValueExample :: Value
  useValueExample = UseValue (ValueId "variable name")
  \end{code}
  
  is serialized as \eval{encodeExample useValueExample}
  
  \isamarkupsubsubsection{Cond}
  
  \begin{code}
  condExample :: Value
  condExample = Cond TrueObs addExample mulExample
  \end{code}
  
  is serialized as \perform{prettyEncodeExample condExample}
  
  \isamarkupsubsubsection{AvailableMoney}
  
  \begin{code}
  availableMoneyExample :: Value
  availableMoneyExample = AvailableMoney addressExample dolarToken
  \end{code}
  
  is serialized as \perform{prettyEncodeExample availableMoneyExample}
  
  \isamarkupsection{Observation}
  
  The \emph{Observation} type is serialized as native boolean (for \emph{TrueObs} and \emph{FalseObs}) or as an object with different properties, depending on the constructor.
  
  \begin{code}
  instance ToJSON Observation where
    toJSON (AndObs lhs rhs) = object
        [ "both" .= lhs
        , "and" .= rhs
        ]
    toJSON (OrObs lhs rhs) = object
        [ "either" .= lhs
        , "or" .= rhs
        ]
    toJSON (NotObs v) = object
        [ "not" .= v ]
    toJSON (ChoseSomething choiceId) = object
        [ "chose_something_for" .= choiceId ]
    toJSON (ValueGE lhs rhs) = object
        [ "value" .= lhs
        , "ge_than" .= rhs
        ]
    toJSON (ValueGT lhs rhs) = object
        [ "value" .= lhs
        , "gt" .= rhs
        ]
    toJSON (ValueLT lhs rhs) = object
        [ "value" .= lhs
        , "lt" .= rhs
        ]
    toJSON (ValueLE lhs rhs) = object
        [ "value" .= lhs
        , "le_than" .= rhs
        ]
    toJSON (ValueEQ lhs rhs) = object
        [ "value" .= lhs
        , "equal_to" .= rhs
        ]
    toJSON TrueObs = toJSON True
    toJSON FalseObs = toJSON False
  
  
  instance FromJSON Observation where
    parseJSON (JSON.Bool True) = return TrueObs
    parseJSON (JSON.Bool False) = return FalseObs
    parseJSON (JSON.Object v) =
          (AndObs <$> (v .: "both")
                  <*> (v .: "and"))
      <|> (OrObs <$> (v .: "either")
                 <*> (v .: "or"))
      <|> (NotObs <$> (v .: "not"))
      <|> (ChoseSomething <$> (v .: "chose_something_for"))
      <|> (ValueGE <$> (v .: "value")
                   <*> (v .: "ge_than"))
      <|> (ValueGT <$> (v .: "value")
                   <*> (v .: "gt"))
      <|> (ValueLT <$> (v .: "value")
                   <*> (v .: "lt"))
      <|> (ValueLE <$> (v .: "value")
                   <*> (v .: "le_than"))
      <|> (ValueEQ <$> (v .: "value")
                   <*> (v .: "equal_to"))
    parseJSON _ = fail "Observation must be either an object or a boolean"
  \end{code}
  
  Here are some examples for each \emph{Observation} constructor:
  
  \isamarkupsubsubsection{TrueObs}
  
  \begin{code}
  trueExample :: Observation
  trueExample = TrueObs
  \end{code}
  
  is serialized as \eval{encodeExample trueExample}
  
  \isamarkupsubsubsection{FalseObs}
  
  \begin{code}
  falseExample :: Observation
  falseExample = FalseObs
  \end{code}
  
  is serialized as \eval{encodeExample falseExample}
  
  \isamarkupsubsubsection{AndObs}
  
  \begin{code}
  andExample :: Observation
  andExample = AndObs TrueObs FalseObs
  \end{code}
  
  is serialized as \eval{encodeExample andExample}
  
  \isamarkupsubsubsection{OrObs}
  
  \begin{code}
  orExample :: Observation
  orExample = OrObs TrueObs FalseObs
  \end{code}
  
  is serialized as \eval{encodeExample orExample}
  
  \isamarkupsubsubsection{NotObs}
  
  \begin{code}
  notExample :: Observation
  notExample = NotObs TrueObs
  \end{code}
  
  is serialized as \eval{encodeExample notExample}
  
  
  \isamarkupsubsubsection{ChoseSomething}
  
  \begin{code}
  choseExample :: Observation
  choseExample = ChoseSomething choiceIdExample
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample choseExample}
  
  
  \isamarkupsubsubsection{ValueGE}
  
  \begin{code}
  valueGEExample :: Observation
  valueGEExample = ValueGE (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample valueGEExample}
  
  
  \isamarkupsubsubsection{ValueGT}
  
  \begin{code}
  valueGTExample :: Observation
  valueGTExample = ValueGT (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample valueGTExample}
  
  
  \isamarkupsubsubsection{ValueLT}
  
  \begin{code}
  valueLTExample :: Observation
  valueLTExample = ValueLT (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample valueLTExample}
  
  
  \isamarkupsubsubsection{ValueLE}
  
  \begin{code}
  valueLEExample :: Observation
  valueLEExample = ValueLE (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample valueLEExample}
  
  
  \isamarkupsubsubsection{ValueEQ}
  
  \begin{code}
  valueEQExample :: Observation
  valueEQExample = ValueEQ (Constant 1) (Constant 2)
  \end{code}
  
  is serialized as \eval{encodeExample valueEQExample}
  
  \isamarkupsection{Action}
  
  The \emph{Action} type is serialized as an object with different properties, depending on the constructor.
  
  \begin{code}
  instance ToJSON Action where
    toJSON (Deposit accountId party token val) = object
        [ "into_account" .= accountId
        , "party" .= party
        , "of_token" .= token
        , "deposits" .= val
        ]
    toJSON (Choice choiceId bounds) = object
        [ "for_choice" .= choiceId
        , "choose_between" .= toJSONList (map toJSON bounds)
        ]
    toJSON (Notify obs) = object
        [ "notify_if" .= obs ]
  
  
  instance FromJSON Action where
    parseJSON = withObject "Action" (\v ->
         (Deposit <$> (v .: "into_account")
                  <*> (v .: "party")
                  <*> (v .: "of_token")
                  <*> (v .: "deposits"))
     <|> (Choice <$> (v .: "for_choice")
                 <*> ((v .: "choose_between") >>=
                      withArray "Bound list" (\bl ->
                        mapM parseJSON (F.toList bl)
                                              )))
     <|> (Notify <$> (v .: "notify_if"))
                                    )
  \end{code}
  
  Here are some examples for each \emph{Action} constructor:
  
  \isamarkupsubsubsection{Deposit}
  
  \begin{code}
  depositExample :: Action
  depositExample = Deposit
                      addressExample
                      roleExample
                      dolarToken
                      constantExample
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample depositExample}
  
  \isamarkupsubsubsection{Choice}
  
  \begin{code}
  choiceExample :: Action
  choiceExample = Choice
                      choiceIdExample
                      [Bound 0 1, Bound 4 8]
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample choiceExample}
  
  
  \isamarkupsubsubsection{Notify}
  
  \begin{code}
  notifyExample :: Action
  notifyExample = Notify (ChoseSomething choiceIdExample)
  
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample notifyExample}
  
  \isamarkupsection{Case}
  The \emph{Case} type is serialized as an object with two properties (\emph{case} and \emph{then}).
  
  \begin{code}
  instance ToJSON Case where
      toJSON (Case act cont) = object
          [ "case" .= act
          , "then" .= cont
          ]
  
  instance FromJSON Case where
      parseJSON = withObject "Case"
        (\v ->
          Case <$> (v .: "case") <*> (v .: "then")
        )
  \end{code}
  
  For example, the following \emph{Case}
  
  \begin{code}
  caseExample :: Case
  caseExample = Case notifyExample Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample caseExample}
  
  \isamarkupsection{Contract}
  
  The \emph{Contract} type is serialized as the literal string "close" or as an object, depending on the constructor
  
  \begin{code}
  
  instance ToJSON Contract where
    toJSON Close = JSON.String $ T.pack "close"
    toJSON (Pay accountId payee token value contract) = object
        [ "from_account" .= accountId
        , "to" .= payee
        , "token" .= token
        , "pay" .= value
        , "then" .= contract
        ]
    toJSON (If obs cont1 cont2) = object
        [ "if" .= obs
        , "then" .= cont1
        , "else" .= cont2
        ]
    toJSON (When caseList timeout cont) = object
        [ "when" .= toJSONList (map toJSON caseList)
        , "timeout" .= timeout
        , "timeout_continuation" .= cont
        ]
    toJSON (Let valId value cont) = object
        [ "let" .= valId
        , "be" .= value
        , "then" .= cont
        ]
    toJSON (Assert obs cont) = object
        [ "assert" .= obs
        , "then" .= cont
        ]
  
  
  instance FromJSON Contract where
    parseJSON (JSON.String "close") = return Close
    parseJSON (JSON.Object v) =
          (Pay <$> (v .: "from_account")
               <*> (v .: "to")
               <*> (v .: "token")
               <*> (v .: "pay")
               <*> (v .: "then"))
      <|> (If <$> (v .: "if")
              <*> (v .: "then")
              <*> (v .: "else"))
      <|> (When <$> ((v .: "when") >>=
                     withArray "Case list" (\cl ->
                       mapM parseJSON (F.toList cl)
                                            ))
                <*> (withInteger "when timeout" =<< (v .: "timeout"))
                <*> (v .: "timeout_continuation"))
      <|> (Let <$> (v .: "let")
               <*> (v .: "be")
               <*> (v .: "then"))
      <|> (Assert <$> (v .: "assert")
                  <*> (v .: "then"))
    parseJSON _ =
      fail "Contract must be either an object or a the string \"close\""
  \end{code}
  
  Here are some examples for each \emph{Contract} constructor:
  
  \isamarkupsubsubsection{Close}
  
  \begin{code}
  closeExample :: Contract
  closeExample = Close
  \end{code}
  
  is serialized as \eval{encodeExample closeExample}
  
  
  \isamarkupsubsubsection{Pay}
  
  \begin{code}
  payExample :: Contract
  payExample = Pay
                  roleExample
                  internalPayeeExample
                  dolarToken
                  (Constant 10)
                  Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample payExample}
  
  
  \isamarkupsubsubsection{If}
  
  \begin{code}
  ifExample :: Contract
  ifExample = If
                  TrueObs
                  Close
                  Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample ifExample}
  
  \isamarkupsubsubsection{When}
  
  \begin{code}
  whenExample :: Contract
  whenExample = When
                  [ Case (Notify TrueObs) Close
                  , Case (Notify FalseObs) Close
                  ]
                  20
                  Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample whenExample}
  
  \isamarkupsubsubsection{Let}
  
  \begin{code}
  letExample :: Contract
  letExample = Let (ValueId "var") (Constant 10) Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample letExample}
  
  
  \isamarkupsubsubsection{Assert}
  
  \begin{code}
  assertExample :: Contract
  assertExample = Assert choseExample Close
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample assertExample}
  
  
  \isamarkupsection{Input}
  The \emph{Input} type is serialized as the literal string "input\_notify" or as an object, depending on the constructor.
  
  \begin{code}
  instance ToJSON Input where
    toJSON (IDeposit accId party tok amount) = object
        [ "input_from_party" .= party
        , "that_deposits" .= amount
        , "of_token" .= tok
        , "into_account" .= accId
        ]
    toJSON (IChoice choiceId chosenNum) = object
        [ "input_that_chooses_num" .= chosenNum
        , "for_choice_id" .= choiceId
        ]
    toJSON INotify = JSON.String $ T.pack "input_notify"
  
  
  instance FromJSON Input where
    parseJSON (JSON.String "input_notify") = return INotify
    parseJSON (JSON.Object v) =
          IChoice <$> v .: "for_choice_id"
                  <*> v .: "input_that_chooses_num"
      <|> IDeposit <$> v .: "into_account"
                   <*> v .: "input_from_party"
                   <*> v .: "of_token"
                   <*> v .: "that_deposits"
    parseJSON _ =
      fail "Input must be either an object or the string \"input_notify\""
  \end{code}
  
  Here are some examples for each \emph{Input} constructor:
  
  \isamarkupsubsubsection{INotify}
  
  \begin{code}
  iNotifyExample :: Input
  iNotifyExample = INotify
  \end{code}
  
  is serialized as \eval{encodeExample iNotifyExample}
  
  
  \isamarkupsubsubsection{IChoice}
  
  \begin{code}
  iChoiceExample :: Input
  iChoiceExample = IChoice choiceIdExample 3
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample iChoiceExample}
  
  
  \isamarkupsubsubsection{IDeposit}
  
  \begin{code}
  iDepositExample :: Input
  iDepositExample = IDeposit addressExample roleExample dolarToken 5
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample iDepositExample}
  
  \isamarkupsection{Transaction}
  
  The \emph{Transaction} type is serialized as an object with two properties, \emph{tx\_interval} and \emph{tx\_inputs}.
  
  
  \begin{code}
  instance ToJSON (Transaction_ext a) where
    toJSON (Transaction_ext (from, to) txInps _) = object
        [ "tx_interval" .= timeIntervalJSON
        , "tx_inputs" .= toJSONList (map toJSON txInps)
        ]
      where timeIntervalJSON = object [ "from" .= from
                                      , "to" .= to
                                      ]
  
  instance FromJSON (Transaction_ext ()) where
    parseJSON (JSON.Object v) =
          Transaction_ext <$> (parseTimeInterval =<< (v .: "tx_interval"))
                           <*> ((v .: "tx_inputs") >>=
                     withArray "Transaction input list" (\cl ->
                       mapM parseJSON (F.toList cl)
                                                        ))
                           <*> pure ()
      where parseTimeInterval = withObject "TimeInterval" (\v ->
              do from <- withInteger "TimeInterval from" =<< (v .: "from")
                 to <- withInteger "TimeInterval to" =<< (v .: "to")
                 return (from, to)
                                                        )
    parseJSON _ = fail "Transaction must be an object"
  
  \end{code}
  
  For example, the following \emph{Transaction}
  
  \begin{code}
  transactionExample :: Transaction_ext ()
  transactionExample = Transaction_ext
                          (10, 100)
                          [ iChoiceExample
                          , iNotifyExample
                          ]
                          ()
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionExample}
  
  \isamarkupsection{Payment}
  
  The \emph{Payment} type is serialized as a single object with three properties
  
  \begin{code}
  instance ToJSON Payment where
    toJSON (Payment from to token amount) = object
        [ "payment_from" .= from
        , "to" .= to
        , "token" .= token
        , "amount" .= amount
        ]
  
  instance FromJSON Payment where
      parseJSON = withObject "Payment"
        (\v ->
          Payment <$> (v .: "payment_from")
                  <*> (v .: "to")
                  <*> (v .: "token")
                  <*> (v .: "amount")
        )
  \end{code}
  
  for example, the following \emph{Payment}
  
  \begin{code}
  paymentExample :: Payment
  paymentExample = Payment
                      addressExample
                      externalPayeeExample
                      dolarToken
                      10
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample paymentExample}
  
  \isamarkupsection{State}
  The \emph{State} type is serialized as a single object with four properties. Each Map is represented by a list
  of key value tuples.
  
  \begin{code}
  instance ToJSON (State_ext ()) where
    toJSON (State_ext accounts choices boundValues minTime _) = object
          [ "accounts" .= toJSON accounts
          , "choices" .= toJSON choices
          , "boundValues" .= toJSON boundValues
          , "minTime" .= minTime
          ]
  
  instance FromJSON (State_ext ()) where
      parseJSON = withObject "State"
        (\v ->
          State_ext <$> (v .: "accounts")
                  <*> (v .: "choices")
                  <*> (v .: "boundValues")
                  <*> (v .: "minTime")
                  <*> pure ()
        )
  \end{code}
  
  for example, the following state
  
  \begin{code}
  stateExample :: State_ext ()
  stateExample = State_ext
                  [((roleExample, dolarToken), 20)]
                  [(choiceIdExample, 10)]
                  [(ValueId "example", 30)]
                  90
                  ()
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample stateExample}
  
  \isamarkupsection{TransactionWarning}
  
  The \emph{TransactionWarning} type is serialized as a literal string (in case of \emph{TransactionAssertionFailed}) or as an object with different properties, depending the constructor.
  
  \begin{code}
  instance ToJSON TransactionWarning where
    toJSON (TransactionNonPositiveDeposit party accId tok amount) = object
        [ "party" .= party
        , "asked_to_deposit" .= amount
        , "of_token" .= tok
        , "in_account" .= accId
        ]
    toJSON (TransactionNonPositivePay accId payee tok amount) = object
        [ "account" .= accId
        , "asked_to_pay" .= amount
        , "of_token" .= tok
        , "to_payee" .= payee
        ]
    toJSON (TransactionPartialPay accId payee tok paid expected) = object
        [ "account" .= accId
        , "asked_to_pay" .= expected
        , "of_token" .= tok
        , "to_payee" .= payee
        , "but_only_paid" .= paid
        ]
    toJSON (TransactionShadowing valId oldVal newVal) = object
        [ "value_id" .= valId
        , "had_value" .= oldVal
        , "is_now_assigned" .= newVal
        ]
    toJSON TransactionAssertionFailed = JSON.String $ T.pack "assertion_failed"
  
  
  instance FromJSON TransactionWarning where
    parseJSON (JSON.String "assertion_failed") =
      return TransactionAssertionFailed
    parseJSON (JSON.Object v) =
          (TransactionNonPositiveDeposit <$> (v .: "party")
                                         <*> (v .: "in_account")
                                         <*> (v .: "of_token")
                                         <*> (v .: "asked_to_deposit"))
      <|> (do maybeButOnlyPaid <- v .:? "but_only_paid"
              case maybeButOnlyPaid :: Maybe Scientific of
                Nothing -> TransactionNonPositivePay <$> (v .: "account")
                                                     <*> (v .: "to_payee")
                                                     <*> (v .: "of_token")
                                                     <*> (v .: "asked_to_pay")
                Just butOnlyPaid -> TransactionPartialPay <$> (v .: "account")
                                                          <*> (v .: "to_payee")
                                                          <*> (v .: "of_token")
                                                          <*> getInteger "but only paid" butOnlyPaid
                                                          <*> (v .: "asked_to_pay"))
      <|> (TransactionShadowing <$> (v .: "value_id")
                                <*> (v .: "had_value")
                                <*> (v .: "is_now_assigned"))
    parseJSON _ =
      fail "Contract must be either an object or a the string \"close\""
  \end{code}
  
  Here are some examples for each \emph{TransactionWarning} constructor:
  
  
  \isamarkupsubsubsection{TransactionNonPositiveDeposit}
  
  \begin{code}
  transactionNonPositiveDepositExample :: TransactionWarning
  transactionNonPositiveDepositExample = TransactionNonPositiveDeposit
                                              addressExample
                                              roleExample
                                              dolarToken
                                              20
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionNonPositiveDepositExample}
  
  
  \isamarkupsubsubsection{TransactionNonPositivePay}
  
  \begin{code}
  transactionNonPositivePayExample :: TransactionWarning
  transactionNonPositivePayExample = TransactionNonPositivePay
                                              addressExample
                                              internalPayeeExample
                                              dolarToken
                                              20
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionNonPositivePayExample}
  
  
  \isamarkupsubsubsection{TransactionPartialPay}
  
  \begin{code}
  transactionPartialPayExample :: TransactionWarning
  transactionPartialPayExample = TransactionPartialPay
                                              addressExample
                                              internalPayeeExample
                                              dolarToken
                                              20
                                              30
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionPartialPayExample}
  
  
  \isamarkupsubsubsection{TransactionShadowing}
  
  \begin{code}
  transactionShadowingExample :: TransactionWarning
  transactionShadowingExample = TransactionShadowing
                                              (ValueId "example")
                                              4
                                              5
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionShadowingExample}
  
  
  \isamarkupsubsubsection{TransactionAssertionFailed}
  
  \begin{code}
  transactionAssertionFailedExample :: TransactionWarning
  transactionAssertionFailedExample = TransactionAssertionFailed
  \end{code}
  
  is serialized as \eval{encodeExample transactionAssertionFailedExample}
  
  \isamarkupsection{TimeInterval}
  
  The \emph{TimeInterval} type is serialized as an object with two properties "to" and "from".
  
  In Haskell the type is defined as a type alias for a Tuple of times, so we don't provide a ToJSON/FromJSON
  instance, instead we provide the following functions:
  
  \begin{code}
  intervalToJSON :: (Arith.Int, Arith.Int) -> JSON.Value
  intervalToJSON (from, to) = object [ "from" .= from, "to" .= to]
  
  intervalFromJSON :: JSON.Value -> Parser (Arith.Int, Arith.Int)
  intervalFromJSON = withObject "Interval" (\o -> (,) <$> (o .: "from") <*> (o .: "to"))
  \end{code}
  
  \isamarkupsection{IntervalError}
  
  The \emph{IntervalError} type is serialized as an object with a single property that corresponds to the error type, and the context of
  the error as a sub-object.
  \begin{code}
  instance ToJSON IntervalError where
    toJSON (InvalidInterval iv) = object
      [ "invalidInterval" .= intervalToJSON iv
      ]
    toJSON (IntervalInPastError t (s, e)) = object
      [ "intervalInPastError" .=
         object
           [ "minTime" .= toJSON t
           , "from" .= toJSON s
           , "to"  .= toJSON e
           ]
      ]
  
  instance FromJSON IntervalError where
    parseJSON (JSON.Object v) =
      let
        parseInvalidInterval = do
          err <- v .: "invalidInterval"
          s <- err .: "from"
          e <- err .: "to"
          pure $ InvalidInterval (s , e)
        parseIntervalInPastError = do
          err <- v .: "intervalInPastError"
          t <- err .: "minTime"
          s <- err .: "from"
          e <- err .: "to"
          pure $ IntervalInPastError t (s, e)
      in
        parseIntervalInPastError <|> parseInvalidInterval
    parseJSON invalid =
        JSON.prependFailure "parsing IntervalError failed, " (JSON.typeMismatch "Object" invalid)
  \end{code}
  
  Here are some examples for each \emph{IntervalError} constructor:
  
  
  \isamarkupsubsubsection{InvalidInterval}
  
  \begin{code}
  invalidIntervalExample :: IntervalError
  invalidIntervalExample = InvalidInterval (10, 20)
  \end{code}
  
  is serialized as \eval{encodeExample invalidIntervalExample}
  
  
  \isamarkupsubsubsection{IntervalInPastError}
  
  \begin{code}
  intervalInPastErrorExample :: IntervalError
  intervalInPastErrorExample = IntervalInPastError 30 (10, 20)
  \end{code}
  
  is serialized as \eval{encodeExample intervalInPastErrorExample}
  
  \isamarkupsection{TransactionError}
  
  The \emph{TransactionError} type is serialized as a literal string for errors without context, or as an object
  with the error type.
  
  \begin{code}
  instance ToJSON TransactionError where
    toJSON TEAmbiguousTimeIntervalError = JSON.String "TEAmbiguousTimeIntervalError"
    toJSON TEApplyNoMatchError = JSON.String "TEApplyNoMatchError"
    toJSON TEUselessTransaction = JSON.String "TEUselessTransaction"
    toJSON (TEIntervalError e) = object
      [ "error" .= JSON.String "TEIntervalError"
      , "context" .= toJSON e
      ]
  
  instance FromJSON TransactionError where
      parseJSON (JSON.String "TEAmbiguousTimeIntervalError") = return TEAmbiguousTimeIntervalError
      parseJSON (JSON.String "TEApplyNoMatchError") = return TEApplyNoMatchError
      parseJSON (JSON.String "TEUselessTransaction") = return TEUselessTransaction
      parseJSON (JSON.Object v) =
        do
         errorType :: String <- v .: "error"
         case errorType of
             "TEIntervalError" ->
                 TEIntervalError <$> v .: "context"
             _ ->
               fail "Invalid error type"
      parseJSON _ =
        fail "TransactionError must be either a string or an object"
  
  \end{code}
  
  Here are some examples for each \emph{TransactionError} constructor:
  
  \isamarkupsubsubsection{TEAmbiguousTimeIntervalError}
  
  \begin{code}
  teAmbiguousTimeIntervalErrorExample :: TransactionError
  teAmbiguousTimeIntervalErrorExample = TEAmbiguousTimeIntervalError
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample teAmbiguousTimeIntervalErrorExample}
  
  
  \isamarkupsubsubsection{TEApplyNoMatchError}
  
  \begin{code}
  teApplyNoMatchErrorExample :: TransactionError
  teApplyNoMatchErrorExample = TEApplyNoMatchError
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample teApplyNoMatchErrorExample}
  
  
  \isamarkupsubsubsection{TEIntervalError}
  
  \begin{code}
  teIntervalErrorExample :: TransactionError
  teIntervalErrorExample = TEIntervalError intervalInPastErrorExample
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample teIntervalErrorExample}
  
  \isamarkupsubsubsection{TEUselessTransaction}
  
  \begin{code}
  teUselessTransactionExample :: TransactionError
  teUselessTransactionExample = TEUselessTransaction
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample teUselessTransactionExample}
  
  
  \isamarkupsection{TransactionOutput}
  
  The \emph{TransactionOutput} is serialized as a single object with one property (\emph{transaction\_error})
  in case of an error, or 4 properties in case of success.
  
  
  \begin{code}
  instance ToJSON TransactionOutput where
    toJSON (TransactionError err) = object
      [ "transaction_error" .= toJSON err ]
    toJSON (TransactionOutput out)
      = object
          [ "warnings" .= toJSON (txOutWarnings out)
          , "payments" .= toJSON (txOutPayments out)
          , "state" .= toJSON (txOutState out)
          , "contract" .= toJSON (txOutContract out)
          ]
  
  instance FromJSON TransactionOutput where
    parseJSON = withObject "TransactionOutput"
                  (\v ->
                       (TransactionError <$> ( v .: "transaction_error"))
                    <|> (TransactionOutput <$>
                           (TransactionOutputRecord_ext
                              <$> (v .: "warnings")
                              <*> (v .: "payments")
                              <*> (v .: "state")
                              <*> (v .: "contract")
                              <*> pure ()
                           )
                        )
                  )
  \end{code}
  
  Here are some examples for each \emph{TransactionOutput} constructor:
  
  \isamarkupsubsubsection{TransactionError}
  
  \begin{code}
  transactionOutputErrorExample :: TransactionOutput
  transactionOutputErrorExample = TransactionError teUselessTransactionExample
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionOutputErrorExample}
  
  
  \isamarkupsubsubsection{TransactionOutput}
  
  \begin{code}
  transactionOutputSuccessExample :: TransactionOutput
  transactionOutputSuccessExample = playTrace
                                      0
                                      Examples.Swap.swapExample
                                      Examples.Swap.successfulExecutionPathTransactions
  \end{code}
  
  is serialized as
  \perform{prettyEncodeExample transactionOutputSuccessExample}
  
  \isamarkupsection{Full Contract Example}
  
  The Swap Example, defined in section \secref{sec:swap-example-execution} is serialized as
  \perform{prettyEncodeExample Examples.Swap.swapExample}
  
  \isamarkupsection{Parse utils}
  
  These are some Aeson utils to help parse a number to the Isabelle exported \emph{Arith\.Int}
  
  \begin{code}
  getInteger :: String -> Scientific -> Parser Arith.Int
  getInteger ctx x = case (floatingOrInteger x :: Either Double Integer) of
                   Right a -> return $ Int_of_integer a
                   Left _  -> fail $ "parsing " ++ ctx ++ " failed, expected integer, but encountered floating point"
  
  withInteger :: String -> JSON.Value -> Parser Arith.Int
  withInteger ctx = withScientific ctx $ getInteger ctx
  
  instance ToJSON Arith.Int where
    toJSON (Int_of_integer x) = toJSON x
  
  instance FromJSON Arith.Int where
    parseJSON (JSON.Number x) = getInteger "Int" x
    parseJSON _ = fail "expecting integer"
  \end{code}
  
  \isamarkupsection{Environment}
  
  The \emph{Environment} type is serialized as a single object with one property.
  
  \begin{code}
  instance ToJSON (Environment_ext ()) where
    toJSON (Environment_ext iv _) = object
          [ "timeInterval" .= intervalToJSON iv
          ]
  
  
  instance FromJSON (Environment_ext ()) where
      parseJSON = withObject "Environment"
        (\v ->
          Environment_ext
            <$> (intervalFromJSON =<< v .: "timeInterval")
            <*> pure ()
        )
  \end{code}
  