Rename Refund to Close.

input-output-hk · Oct 14, 2019 · 3894d7d · 3894d7d
1 parent f99c477
commit 3894d7d
Show file tree

Hide file tree

Showing 18 changed files with 223 additions and 223 deletions.
diff --git a/isabelle/PositiveAccounts.thy b/isabelle/PositiveAccounts.thy
@@ -38,7 +38,7 @@ lemma addMoneyToAccountPositive :
 
 lemma giveMoney_geZero :
     "\<forall>x. 0 \<le> moneyInAccount x accs \<Longrightarrow>
-       (eff, newAccs) = giveMoney payee money accs \<Longrightarrow> 
+       (eff, newAccs) = giveMoney payee money accs \<Longrightarrow>
        0 \<le> moneyInAccount y newAccs"
   by (metis addMoneyToAccount.simps addMoneyToAccountPositive giveMoney.elims linear snd_conv)
 
@@ -86,7 +86,7 @@ lemma reduceOne_geZero :
   apply (meson MList.sublist_valid not_le reduceOne_geZero_aux)
   by auto
 
-lemma reduceContractStep_geZero_Refund_aux : 
+lemma reduceContractStep_geZero_Refund_aux :
   "valid_state state \<Longrightarrow>
    \<forall>x. 0 \<le> moneyInAccount x (accounts state) \<Longrightarrow>
    refundOne (accounts state) = Some ((party, money), newAccount) \<Longrightarrow>
@@ -95,11 +95,11 @@ lemma reduceContractStep_geZero_Refund_aux :
    0 \<le> moneyInAccount y newAccount"
   using reduceOne_geZero valid_state.elims(2) by blast
 
-lemma reduceContractStep_geZero_Refund : 
+lemma reduceContractStep_geZero_Refund :
   "valid_state state \<Longrightarrow>
    \<forall>x. 0 \<le> moneyInAccount x (accounts state) \<Longrightarrow>
-   refundOne (accounts state) = Some ((party, money), newAccount) \<Longrightarrow> 
-   Reduced ReduceNoWarning (ReduceWithPayment (Payment party money)) (state\<lparr>accounts := newAccount\<rparr>) Refund =
+   refundOne (accounts state) = Some ((party, money), newAccount) \<Longrightarrow>
+   Reduced ReduceNoWarning (ReduceWithPayment (Payment party money)) (state\<lparr>accounts := newAccount\<rparr>) Close =
       Reduced wa eff newState newCont \<Longrightarrow>
    0 \<le> moneyInAccount y (accounts newState)"
   using reduceContractStep_geZero_Refund_aux by auto

diff --git a/isabelle/Semantics.thy b/isabelle/Semantics.thy
@@ -263,7 +263,7 @@ datatype Payee = Account AccountId
                | Party Party
 
 datatype Case = Case Action Contract
-and Contract = Refund
+and Contract = Close
              | Pay AccountId Payee Value Contract
              | If Observation Contract Contract
              | When "Case list" Timeout Contract
@@ -425,11 +425,11 @@ datatype ReduceStepResult = Reduced ReduceWarning ReduceEffect State Contract
                           | AmbiguousSlotIntervalReductionError
 
 fun reduceContractStep :: "Environment \<Rightarrow> State \<Rightarrow> Contract \<Rightarrow> ReduceStepResult" where
-"reduceContractStep _ state Refund =
+"reduceContractStep _ state Close =
   (case refundOne (accounts state) of
      Some ((party, money), newAccount) \<Rightarrow>
        let newState = state \<lparr> accounts := newAccount \<rparr> in
-       Reduced ReduceNoWarning (ReduceWithPayment (Payment party money)) newState Refund
+       Reduced ReduceNoWarning (ReduceWithPayment (Payment party money)) newState Close
    | None \<Rightarrow> NotReduced)" |
 "reduceContractStep env state (Pay accId payee val cont) =
   (let moneyToPay = evalValue env state val in
@@ -479,9 +479,9 @@ lemma reduceContractStepReducesSize_Refund_aux :
 
 lemma reduceContractStepReducesSize_Refund_aux2 :
   "Reduced ReduceNoWarning (ReduceWithPayment (Payment party money))
-          (sta\<lparr>accounts := newAccount\<rparr>) Refund =
+          (sta\<lparr>accounts := newAccount\<rparr>) Close =
    Reduced twa tef nsta nc \<Longrightarrow>
-   c = Refund \<Longrightarrow>
+   c = Close \<Longrightarrow>
    refundOne (accounts sta) = Some ((party, money), newAccount) \<Longrightarrow>
    length (accounts nsta) + 2 * size nc < length (accounts sta)"
   apply simp
@@ -491,9 +491,9 @@ lemma reduceContractStepReducesSize_Refund :
   "(case a of
           ((party, money), newAccount) \<Rightarrow>
             Reduced ReduceNoWarning (ReduceWithPayment (Payment party money))
-             (sta\<lparr>accounts := newAccount\<rparr>) Refund) =
+             (sta\<lparr>accounts := newAccount\<rparr>) Close) =
          Reduced twa tef nsta nc \<Longrightarrow>
-         c = Refund \<Longrightarrow>
+         c = Close \<Longrightarrow>
          refundOne (accounts sta) = Some a \<Longrightarrow>
          length (accounts nsta) + 2 * size nc < length (accounts sta)"
   apply (cases a)
@@ -801,7 +801,7 @@ fun getSignatures :: "Input list \<Rightarrow> TransactionSignatures" where
 "getSignatures l = foldl addSig SList.empty l"
 
 fun isQuiescent :: "Contract \<Rightarrow> bool" where
-"isQuiescent Refund = True" |
+"isQuiescent Close = True" |
 "isQuiescent (When _ _ _) = True" |
 "isQuiescent _ = False"
 

diff --git a/isabelle/ValidState.thy b/isabelle/ValidState.thy
@@ -12,7 +12,7 @@ lemma refundOne_preserves_valid_map_accounts :
 
 lemma reductionStep_preserves_valid_state_Refund :
   "valid_state state \<Longrightarrow>
-   reduceContractStep env state Refund = Reduced wa ef newState newCont \<Longrightarrow>
+   reduceContractStep env state Close = Reduced wa ef newState newCont \<Longrightarrow>
    state = \<lparr>accounts = oldAccounts, choices = oldChoices, boundValues = oldBoundValues, minSlot = oldMinSlot\<rparr> \<Longrightarrow>
    newState = \<lparr>accounts = newAccounts, choices = newChoices, boundValues = newBoundValues, minSlot = newMinSlot\<rparr> \<Longrightarrow>
    valid_state newState"

diff --git a/src/Language/Marlowe/ACTUS/ActusContracts.hs b/src/Language/Marlowe/ACTUS/ActusContracts.hs
@@ -39,7 +39,7 @@ cb ied md notional rate = (emptyContractConfig ied)
 genPrincialAtMaturnityContract :: Party -> Party -> ContractConfig -> Contract
 genPrincialAtMaturnityContract investor issuer config@ContractConfig{..} = let
     (f, _) = foldl generator (id, state) schedule
-    in f Refund
+    in f Close
   where
     acc = AccountId 1 investor
     maturityDay = fromJust maturityDate
@@ -61,13 +61,13 @@ genPrincialAtMaturnityContract investor issuer config@ContractConfig{..} = let
             amount = abs daysum
             cont = if amount == 0 then id
                    else \contract -> f $ When [Case (Deposit acc from $ Constant amount)
-                        (Pay acc (Party to) (Constant amount) contract)] (dayToSlot day) Refund
+                        (Pay acc (Party to) (Constant amount) contract)] (dayToSlot day) Close
             in (cont, newState)
 
 genPrincialAtMaturnityGuaranteedContract :: Party -> Party -> Party ->  ContractConfig -> Contract
 genPrincialAtMaturnityGuaranteedContract investor issuer guarantor config@ContractConfig{..} = guaranteed
   where
-    cont = let (f, _) = foldl generator (id, state) schedule in f Refund
+    cont = let (f, _) = foldl generator (id, state) schedule in f Close
     acc = AccountId 1 investor
     gacc = AccountId 2 guarantor
     maturityDay = fromJust maturityDate
@@ -85,7 +85,7 @@ genPrincialAtMaturnityGuaranteedContract investor issuer guarantor config@Contra
         in amount
 
     guaranteed = When [Case (Deposit acc guarantor $ Constant totalPayoff) cont]
-                startDate Refund
+                startDate Close
 
     generator (f, state) (day, events) =
         let (daysum, newState) = foldl
@@ -101,5 +101,5 @@ genPrincialAtMaturnityGuaranteedContract investor issuer guarantor config@Contra
                         (Pay acc (Party to) (Constant amount)
                             (if from == investor then contract
                             else (Pay acc (Party guarantor) (Constant amount) contract)))]
-                        (dayToSlot day) Refund
+                        (dayToSlot day) Close
             in (cont, newState)