Skip to content
Permalink
Browse files

removing txhash and blocknum

  • Loading branch information...
jmchapman committed Mar 11, 2019
1 parent 432e816 commit 446f1931e500158e36690dabf88e74fe1c5b520d
Showing with 15 additions and 26 deletions.
  1. +1 −3 Builtin.lagda
  2. +0 −7 Builtin/Signature.lagda
  3. +0 −13 Declarative/Term/Reduction.lagda
  4. +14 −3 Scoped/Reduction.lagda
@@ -26,9 +26,7 @@ data Builtin : Set where
verifySignature : Builtin
resizeByteString : Builtin
equalsByteString : Builtin
txh : Builtin
blocknum : Builtin

{-# FOREIGN GHC import Language.PlutusCore.Lexer.Type #-}
{-# COMPILE GHC Builtin = data BuiltinName (AddInteger | SubtractInteger | MultiplyInteger | DivideInteger | QuotientInteger | RemainderInteger | ModInteger | LessThanInteger | LessThanEqInteger | GreaterThanInteger | GreaterThanEqInteger | EqInteger | ResizeInteger | SizeOfInteger | IntToByteString | Concatenate | TakeByteString | DropByteString | SHA2 | SHA3 | VerifySignature | ResizeByteString | EqByteString | TxHash | BlockNum) #-}
{-# COMPILE GHC Builtin = data BuiltinName (AddInteger | SubtractInteger | MultiplyInteger | DivideInteger | QuotientInteger | RemainderInteger | ModInteger | LessThanInteger | LessThanEqInteger | GreaterThanInteger | GreaterThanEqInteger | EqInteger | ResizeInteger | SizeOfInteger | IntToByteString | Concatenate | TakeByteString | DropByteString | SHA2 | SHA3 | VerifySignature | ResizeByteString | EqByteString) #-}
\end{code}
@@ -166,11 +166,4 @@ SIG equalsByteString =
con bytestring (` Z) ∷ con bytestring (` Z) ∷ []
,,
boolean
SIG txh = ∅ ,, [] ,, con bytestring (size⋆ 32)
SIG blocknum =
∅ ,⋆ #
,,
con size (` Z) ∷ []
,,
con integer (` Z)
\end{code}
@@ -296,19 +296,6 @@ BUILTIN
with equals b b'
... | Bool.true = just true
... | Bool.false = just false
BUILTIN txh σ tt with boundedB? 32 txhash
... | yes p = just (con (bytestring 32 txhash p))
... | no _ = nothing
-- ^ should this be impossible?
BUILTIN blocknum σ vtel with σ Z
BUILTIN
blocknum
σ
(_ ,, V-con (size s) ,, tt)
| size⋆ s
with boundedN? s bnum
... | yes p = just (con (integer s bnum (bN2I s bnum p)))
... | no _ = nothing
\end{code}

# recontructing the telescope after a reduction step
@@ -10,11 +10,19 @@ open import Data.Product
\end{code}

\begin{code}
data Value : ∀{n} → ScopedTm n → Set where
infix 2 _—→_
\end{code}

\begin{code}
data Value {n} : ScopedTm n → Set where
V-ƛ : (A : ScopedTy ∥ n ∥)(t : ScopedTm (S n)) → Value (ƛ A t)
-- V-con : (tcn : TermCon) → Value (con {n} tcn)
data Error : ∀{n} → ScopedTm n → Set where

data _—→_ {n} : ScopedTm n → ScopedTm n → Set where

ξ-· : {L L' M : ScopedTm n} → L —→ L' → L · M —→ L' · M
E-· : {L M : ScopedTm n} → Error L → L · M —→ error {!!}

\end{code}

\begin{code}
@@ -30,7 +38,10 @@ progress (` ())
progress (Λ K t) = {!!}
progress (t ·⋆ A) = {!!}
progress (ƛ A t) = {!!}
progress (t · u) = {!!}
progress (t · u) with progress t
progress (.(ƛ A t) · u) | inl (inl (V-ƛ A t)) = {!!}
progress (t · u) | inl (inr p) = inr ((error {!!}) , {!!})
progress (t · u) | inr y = {!!}
progress (con x) = {!!}
progress (error x) = {!!}
progress (builtin x) = {!!}

0 comments on commit 446f193

Please sign in to comment.
You can’t perform that action at this time.