{-# OPTIONS --safe #-}

module Test.Examples.DEx.Test.Trace where

import Data.Rational.Base as Q
open import Data.Nat.Divisibility.Core
open import Data.Nat.Properties

open import Ledger.Prelude
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

open import Test.Examples.DEx.Datum
open import Test.Examples.DEx.Validator
open import Test.Prelude DExData
open import Test.SymbolicData DExData
open import Test.LedgerImplementation SData SData
open import Test.AbstractImplementation valContext
open import Test.Lib valContext
open import Ledger.Conway.Specification.Script.Validation SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Specification.Utxo SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Specification.Utxo.Properties.Computational SVTransactionStructure SVAbstractFunctions
open import Ledger.Conway.Specification.Utxow.Properties.Computational SVTransactionStructure SVAbstractFunctions


open import Test.Examples.DEx.OffChain.OffChain

open TransactionStructure SVTransactionStructure
open Implementation


par : Params
par = record { sellC =  ; buyC =  }

multiSigScript : PlutusScript
multiSigScript =  , applyScriptWithContext (dexValidator par)

initEnv : UTxOEnv
initEnv = createEnv 


initState' : UTxO
initState' = fromList' (createInitUtxoState  startValue)


data Tx' : Set where
    start      : ℕ → Value → Q.ℚ → Tx'
    close      : ℕ → Tx'
    updatetx   : ℕ → Value → Q.ℚ → Tx'
    exchange   : ℕ → Value → Tx'


makeTx : UTxOState → PlutusScript → Tx' → (id : ℕ) → Maybe Tx
makeTx s script (start w v r) id = just (startTx id w  v r script)
makeTx s script (close w) id = makeCloseTx id s script w
makeTx s script (updatetx w v r) id = makeUpdateTx id s script w v r
makeTx s script (exchange w v) id = makeExchangeTx id s script w v

evalTransanctions : UTxOEnv → ComputationResult String UTxOState → List Tx' → ℕ → ComputationResult String UTxOState
evalTransanctions env s [] id = s
evalTransanctions env state@(failure s) (x ∷ xs) id = state
evalTransanctions env (success s) (tx' ∷ txs') id =
  maybe
    (λ tx → evalTransanctions
              initEnv
              (UTXO-step initEnv s tx)
              txs'
              (suc id))
    (failure "failed to generate tx")
    (makeTx s multiSigScript tx' id)

evalTransanctionsW : UTxOEnv → ComputationResult String UTxOState → List Tx' → ℕ → ComputationResult String UTxOState
evalTransanctionsW env s [] id = s
evalTransanctionsW env state@(failure s) (x ∷ xs) id = state
evalTransanctionsW env (success s) (tx' ∷ txs') id =
  maybe
    (λ tx → evalTransanctions
              initEnv
              (UTXO-step initEnv s tx)
              txs'
              (suc id))
    (failure "failed to generate tx")
    (makeTx s multiSigScript tx' id)

pf : ∀ {d} -> (d Data.Nat.Divisibility.Core.∣ ) -> d ≡ 
pf {zero} (divides quotient equality) rewrite *-comm quotient zero = sym equality
pf {suc d} (divides (suc zero) eq) rewrite +-comm d  = sym eq
pf {suc zero} (divides (2+ q) ())
pf {2+ d} (divides (2+ q) ())

rate : Q.ℚ
rate = (Q.mkℚ (ℤ.pos (suc zero)) zero (λ { (fst , snd) → pf fst }) )

rate2 : Q.ℚ
rate2 = (Q.mkℚ (ℤ.pos (suc zero)) (suc zero) (λ { (fst , snd) → pf fst }) )

rate3 : Q.ℚ
rate3 = (Q.mkℚ (ℤ.pos (suc (suc (suc zero)))) (zero) (λ { (fst , snd) → pf snd }) )

validTrace : List Tx'
validTrace = start  (adaValueOf ) rate
             ∷ updatetx  (adaValueOf ) rate
             ∷ close 
             ∷ []


validTrace2 : List Tx'
validTrace2 = start  (adaValueOf ) rate
              ∷ exchange  (adaValueOf )
              ∷ []



failingTrace : List Tx'
failingTrace = start  (adaValueOf ) rate
               ∷ updatetx  (adaValueOf ) rate3
              ∷ []

opaque
  unfolding collectP2ScriptsWithContext
  unfolding setToList
  unfolding Computational-UTXO
  unfolding outs

  evalValidTrace : ComputationResult String UTxOState
  evalValidTrace = evalTransanctionsW initEnv (success $\begin{pmatrix} \,\href{Test.Examples.DEx.Test.Trace.html#1288}{\htmlId{4044}{\htmlClass{Function}{\text{initState'}}}}\, \\ \,\htmlId{4057}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{4061}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{4065}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$) validTrace 

  evalValidTrace2 : ComputationResult String UTxOState
  evalValidTrace2 = evalTransanctionsW initEnv (success $\begin{pmatrix} \,\href{Test.Examples.DEx.Test.Trace.html#1288}{\htmlId{4198}{\htmlClass{Function}{\text{initState'}}}}\, \\ \,\htmlId{4211}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{4215}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{4219}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$) validTrace2 

  evalFailingTrace : ComputationResult String UTxOState
  evalFailingTrace = evalTransanctionsW initEnv (success $\begin{pmatrix} \,\href{Test.Examples.DEx.Test.Trace.html#1288}{\htmlId{4355}{\htmlClass{Function}{\text{initState'}}}}\, \\ \,\htmlId{4368}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Class.HasEmptySet.html#287}{\htmlId{4372}{\htmlClass{Field}{\text{∅}}}}\, \\ \,\htmlId{4376}{\htmlClass{Number}{\text{0}}}\, \end{pmatrix}$) failingTrace 

  _ : isSuccess evalValidTrace ≡ true
  _ = refl

  _ : isSuccess evalValidTrace2 ≡ true
  _ = refl

  _ : isSuccess evalFailingTrace ≡ false
  _ = refl