From effb35bda97bd963bd546f263dfc5fafed73032c Mon Sep 17 00:00:00 2001 From: David Smith Date: Fri, 17 Jan 2020 11:18:02 +0000 Subject: [PATCH] nothing changes --- .../worker/Marlowe/Symbolic.purs | 11 +++++++---- marlowe-playground-client/worker/Worker.purs | 17 +++++++---------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/marlowe-playground-client/worker/Marlowe/Symbolic.purs b/marlowe-playground-client/worker/Marlowe/Symbolic.purs index 7d6ac474dd7..05a431018a6 100644 --- a/marlowe-playground-client/worker/Marlowe/Symbolic.purs +++ b/marlowe-playground-client/worker/Marlowe/Symbolic.purs @@ -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 @@ -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 @@ -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 @@ -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 @@ -841,4 +844,4 @@ getTransactionOutput contract = do hasWarnings :: TransactionOutput -> Boolean hasWarnings (Error _) = false -hasWarnings (TransactionOutput vs) = not $ Array.null vs.txOutWarnings \ No newline at end of file +hasWarnings (TransactionOutput {txOutWarnings}) = not $ Array.null txOutWarnings \ No newline at end of file diff --git a/marlowe-playground-client/worker/Worker.purs b/marlowe-playground-client/worker/Worker.purs index 1e299105f4c..1d1b60c67cf 100644 --- a/marlowe-playground-client/worker/Worker.purs +++ b/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(..)) @@ -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 @@ -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 @@ -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