Skip to content

Commit

Permalink
nothing changes
Browse files Browse the repository at this point in the history
  • Loading branch information
shmish111 committed Jan 17, 2020
1 parent 19878f8 commit effb35b
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 14 deletions.
11 changes: 7 additions & 4 deletions marlowe-playground-client/worker/Marlowe/Symbolic.purs
Expand Up @@ -18,6 +18,7 @@ import Data.Newtype (class Newtype, unwrap, wrap)
import Data.Symbol (SProxy(..))
import Data.Symbolic (BooleanConstraint(..), IntConstraint(..), Sort(..), StringConstraint(..), Tree, Var(..), intVar, is, ite, smin, stringVar, (.<), (.<=), (.>), (.>=))
import Data.Tuple (Tuple(..), snd)
import Debug.Trace (trace)
import Marlowe.Semantics (AccountId, Action(..), Bound(..), Case(..), ChoiceId, Contract(..), Observation(..), Party, Payee, Token(..), Value(..), ValueId, maxDepth)
import Marlowe.Semantics as MS

Expand Down Expand Up @@ -711,7 +712,7 @@ computeTransaction tx currentWarnings state contract = do
IntervalError error -> pure $ Error (TEIntervalError error)

computeTransactions :: TransactionOutput -> Array STransactionInput -> Tree TransactionOutput
computeTransactions tout [] = pure tout
-- computeTransactions tout [] = pure tout

computeTransactions tout@(Error _) _ = pure tout

Expand Down Expand Up @@ -799,8 +800,8 @@ getTransactionOutput contract = do

mkSlotInterval suffix (SlotInterval (Slot a) (Slot b)) =
SlotInterval
(Slot $ (IntAdd a (intVar ("slot-start" <> suffix))))
(Slot $ (IntAdd a (intVar ("slot-end" <> suffix))))
(Slot $ (IntAdd b (intVar ("slot-start" <> suffix))))
(Slot $ (IntAdd b (intVar ("slot-end" <> suffix))))

state =
State
Expand All @@ -827,6 +828,8 @@ getTransactionOutput contract = do
i <- mkInput $ show idx
pure [ i ]
pure $ Tuple (idx + 1) $ TransactionInput { interval: slotInterval', inputs: inputs } : acc
-- FIXME: just trying to get rid of empty txs as an experiment
-- inputs <- filter notEmpty <$> mkTxs depth
inputs <- mkTxs depth
txs <- foldM mkTx (Tuple 1 []) inputs
let
Expand All @@ -841,4 +844,4 @@ getTransactionOutput contract = do

hasWarnings :: TransactionOutput -> Boolean
hasWarnings (Error _) = false
hasWarnings (TransactionOutput vs) = not $ Array.null vs.txOutWarnings
hasWarnings (TransactionOutput {txOutWarnings}) = not $ Array.null txOutWarnings
17 changes: 7 additions & 10 deletions marlowe-playground-client/worker/Worker.purs
@@ -1,7 +1,6 @@
module Worker where

import Prelude

import Control.Monad.Except (runExcept)
import Data.Array (filter, head)
import Data.Either (Either(..))
Expand Down Expand Up @@ -57,9 +56,10 @@ handleRequest ctx (AnalyseContractRequest contractString) = do
res <- checkContractForWarnings contractString
postMessage ctx (AnalyseContractResult (show res))

handleRequest ctx InitializeZ3 = onZ3Initialized do
Console.log "Z3 loaded"
postMessage ctx InitializedZ3
handleRequest ctx InitializeZ3 =
onZ3Initialized do
Console.log "Z3 loaded"
postMessage ctx InitializedZ3

checkContractForWarnings :: String -> Effect (Maybe (Map String String))
checkContractForWarnings contractString = do
Expand All @@ -72,16 +72,15 @@ checkContractForWarnings contractString = do
tree = getTransactionOutput contract

equations = filter (\a -> hasWarnings a.value) $ getEquations tree

liftEffect do
resA <-
runZ3 do
r1 <- declareVars equations
traverse f equations
case head (filter isJust resA) of
Nothing -> pure Nothing
(Just Nothing) -> pure Nothing
(Just (Just m)) -> pure $ Just m
Nothing -> pure Nothing
(Just Nothing) -> pure Nothing
(Just (Just m)) -> pure $ Just m
where
f :: forall a. Equation a -> Z3 (Maybe (Map String String))
f a = do
Expand All @@ -92,8 +91,6 @@ checkContractForWarnings contractString = do
void $ evalString "(pop)"
pure res

-- handler needs to recieve messages that are a map of type and body (string) and pattern match on the type
-- need to coerce to {messageType: "AnalyseContract|InitializeZ3", body: contractString|null }
main ::
Effect Unit
main = do
Expand Down

0 comments on commit effb35b

Please sign in to comment.