remove arity from Scoped syntax files as there is not scoped semantic…

…s anymore

plutus-metatheory/src/Algorithmic.lagda

@@ -93,28 +93,28 @@ application.
 \begin{code}
 ISIG : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢Nf⋆ *
 ISIG ifThenElse = _ ,, ∅ ,⋆ * , con bool , ne (` Z) , ne (` Z) ,, ne (` Z)
-ISIG addInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG subtractInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG multiplyInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG divideInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG quotientInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG remainderInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG modInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG lessThanInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG lessThanEqualsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG equalsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG appendByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bytestring
-ISIG lessThanByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG lessThanEqualsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG sha2-256 = ∅ ,, ∅ , con bytestring ,, con bytestring
-ISIG sha3-256 = ∅ ,, ∅ , con bytestring ,, con bytestring
-ISIG verifySignature = ∅ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool
-ISIG equalsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG appendString = ∅ ,, ∅ , con string , con string ,, con string
+ISIG addInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG subtractInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG multiplyInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG divideInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG quotientInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG remainderInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG modInteger = _ ,, ∅ , con integer , con integer ,, con integer
+ISIG lessThanInteger = _ ,, ∅ , con integer , con integer ,, con bool
+ISIG lessThanEqualsInteger = _ ,, ∅ , con integer , con integer ,, con bool
+ISIG equalsInteger = _ ,, ∅ , con integer , con integer ,, con bool
+ISIG appendByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bytestring
+ISIG lessThanByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+ISIG lessThanEqualsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+ISIG sha2-256 = _ ,, ∅ , con bytestring ,, con bytestring
+ISIG sha3-256 = _ ,, ∅ , con bytestring ,, con bytestring
+ISIG verifySignature = _ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool
+ISIG equalsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+ISIG appendString = _ ,, ∅ , con string , con string ,, con string
 ISIG trace = _ ,, ∅ ,⋆ * , con string , ne (` Z) ,, ne (` Z)
-ISIG equalsString = ∅ ,, ∅ , con string , con string ,, con bool
-ISIG encodeUtf8 = ∅ ,, ∅ , con string ,, con bytestring
-ISIG decodeUtf8 = ∅ ,, ∅ , con bytestring ,, con string
+ISIG equalsString = _ ,, ∅ , con string , con string ,, con bool
+ISIG encodeUtf8 = _ ,, ∅ , con string ,, con bytestring
+ISIG decodeUtf8 = _ ,, ∅ , con bytestring ,, con string
 ISIG fstPair =
   _ ,, ∅ ,⋆ * ,⋆ * , con (pair (ne (` (S Z))) (ne (` Z))) ,, ne (` (S Z))
 ISIG sndPair = 

plutus-metatheory/src/Scoped.lagda

@@ -25,72 +25,6 @@ open import Utils
 \end{code}
 
 \begin{code}
-arity : Builtin → ℕ
-arity addInteger = 2
-arity subtractInteger = 2
-arity multiplyInteger = 2
-arity divideInteger = 2
-arity quotientInteger = 2
-arity remainderInteger = 2
-arity modInteger = 2
-arity lessThanInteger = 2
-arity lessThanEqualsInteger = 2
-arity equalsInteger = 2
-arity appendByteString = 2
-arity lessThanByteString = 2
-arity lessThanEqualsByteString = 2
-arity sha2-256 = 1
-arity sha3-256 = 1
-arity verifySignature = 3
-arity equalsByteString = 2
-arity ifThenElse = 3
-arity appendString = 2
-arity trace = 2
-arity equalsString = 2
-arity encodeUtf8 = 1
-arity decodeUtf8 = 1
-arity fstPair = 1
-arity sndPair = 1
-arity nullList = 1
-arity headList = 1
-arity tailList = 1
-arity chooseList = 3
-arity constrData = 2
-arity mapData = 1
-arity listData = 1
-arity iData = 1
-arity bData = 1
-arity unConstrData = 1
-arity unMapData = 1
-arity unListData = 1
-arity unIData = 1
-arity unBData = 1
-arity equalsData = 2
-arity chooseData = 6
-arity chooseUnit = 2
-arity mkPairData = 2
-arity mkNilData = 1
-arity mkNilPairData = 1
-arity mkCons = 2
-arity consByteString = 2
-arity sliceByteString = 3
-arity lengthOfByteString = 1
-arity indexByteString = 2
-arity blake2b-256 = 1
-
-
-arity⋆ : Builtin → ℕ
-arity⋆ ifThenElse = 1
-arity⋆ fstPair = 2
-arity⋆ sndPair = 2
-arity⋆ nullList = 1
-arity⋆ headList = 1
-arity⋆ tailList = 1
-arity⋆ chooseList = 2
-arity⋆ chooseData = 1
-arity⋆ chooseUnit = 1
-arity⋆ trace = 1
-arity⋆ _ = 0
 open import Type
 
 data ScopedTy (n : ℕ) : Set

plutus-metatheory/src/Scoped/Extrication.lagda

@@ -86,9 +86,6 @@ extricateC (bool b)       = bool b
 extricateC unit           = unit
 extricateC (Data d)       = Data d
 
-open import Data.Product as P
-open import Function hiding (_∋_)
-
 extricateSub : ∀ {Γ Δ} → (∀ {J} → Δ ∋⋆ J → Γ ⊢Nf⋆ J)
   → Scoped.Tel⋆ (len⋆ Γ) (len⋆ Δ)
 extricateSub {Δ = ∅}     σ = []
@@ -97,117 +94,6 @@ extricateSub {Γ}{Δ ,⋆ K} σ =
            (+-comm (len⋆ Δ) 1)
            (extricateSub {Δ = Δ} (σ ∘ S) ++ Data.Vec.[ extricateNf⋆ (σ Z) ])
 
-open import Data.List
-
-lemma⋆ : ∀ b → len⋆ (proj₁ (ISIG b)) ≡ arity⋆ b
-lemma⋆ addInteger = refl
-lemma⋆ subtractInteger = refl
-lemma⋆ multiplyInteger = refl
-lemma⋆ divideInteger = refl
-lemma⋆ quotientInteger = refl
-lemma⋆ remainderInteger = refl
-lemma⋆ modInteger = refl
-lemma⋆ lessThanInteger = refl
-lemma⋆ lessThanEqualsInteger = refl
-lemma⋆ equalsInteger = refl
-lemma⋆ appendByteString = refl
-lemma⋆ lessThanByteString = refl
-lemma⋆ lessThanEqualsByteString = refl
-lemma⋆ sha2-256 = refl
-lemma⋆ sha3-256 = refl
-lemma⋆ verifySignature = refl
-lemma⋆ equalsByteString = refl
-lemma⋆ ifThenElse = refl
-lemma⋆ appendString = refl
-lemma⋆ trace = refl
-lemma⋆ equalsString = refl
-lemma⋆ encodeUtf8 = refl
-lemma⋆ decodeUtf8 = refl
-lemma⋆ fstPair = refl
-lemma⋆ sndPair = refl
-lemma⋆ nullList = refl
-lemma⋆ headList = refl
-lemma⋆ tailList = refl
-lemma⋆ chooseList = refl
-lemma⋆ constrData = refl
-lemma⋆ mapData = refl
-lemma⋆ listData = refl
-lemma⋆ iData = refl
-lemma⋆ bData = refl
-lemma⋆ unConstrData = refl
-lemma⋆ unMapData = refl
-lemma⋆ unListData = refl
-lemma⋆ unIData = refl
-lemma⋆ unBData = refl
-lemma⋆ equalsData = refl
-lemma⋆ chooseData = refl
-lemma⋆ chooseUnit = refl
-lemma⋆ mkPairData = refl
-lemma⋆ mkNilData = refl
-lemma⋆ mkNilPairData = refl
-lemma⋆ mkCons = refl
-lemma⋆ consByteString = refl
-lemma⋆ sliceByteString = refl
-lemma⋆ lengthOfByteString = refl
-lemma⋆ indexByteString = refl
-lemma⋆ blake2b-256 = refl
-
-lemma : ∀ b → wtoℕTm (len (proj₁ (proj₂ (ISIG b)))) ≡ Scoped.arity b
-lemma addInteger = refl
-lemma subtractInteger = refl
-lemma multiplyInteger = refl
-lemma divideInteger = refl
-lemma quotientInteger = refl
-lemma remainderInteger = refl
-lemma modInteger = refl
-lemma lessThanInteger = refl
-lemma lessThanEqualsInteger = refl
-lemma equalsInteger = refl
-lemma appendByteString = refl
-lemma lessThanByteString = refl
-lemma lessThanEqualsByteString = refl
-lemma sha2-256 = refl
-lemma sha3-256 = refl
-lemma verifySignature = refl
-lemma equalsByteString = refl
-lemma ifThenElse = refl
-lemma appendString = refl
-lemma trace = refl
-lemma equalsString = refl
-lemma encodeUtf8 = refl
-lemma decodeUtf8 = refl
-lemma fstPair = refl
-lemma sndPair = refl
-lemma nullList = refl
-lemma headList = refl
-lemma tailList = refl
-lemma chooseList = refl
-lemma constrData = refl
-lemma mapData = refl
-lemma listData = refl
-lemma iData = refl
-lemma bData = refl
-lemma unConstrData = refl
-lemma unMapData = refl
-lemma unListData = refl
-lemma unIData = refl
-lemma unBData = refl
-lemma equalsData = refl
-lemma chooseData = refl
-lemma chooseUnit = refl
-lemma mkPairData = refl
-lemma mkNilData = refl
-lemma mkNilPairData = refl
-lemma mkCons = refl
-lemma consByteString = refl
-lemma sliceByteString = refl
-lemma lengthOfByteString = refl
-lemma indexByteString = refl
-lemma blake2b-256 = refl
-
-≡2≤‴ : ∀{m n} → m ≡ n → m ≤‴ n
-≡2≤‴ refl = ≤‴-refl
-
 extricate : ∀{Φ Γ}{A : Φ ⊢Nf⋆ *} → Γ ⊢ A → ScopedTm (len Γ)
 extricate (` x) = ` (extricateVar x)
 extricate {Φ}{Γ} (ƛ {A = A} t) = ƛ (extricateNf⋆ A) (extricate t)