Merge pull request #1729 from jmchapman/master

remove names from metatheory

default.nix

@@ -338,7 +338,7 @@ let
       }).overrideAttrs (oldAttrs: rec {
         # Need to override the source this way
         name = "agda-stdlib-${version}";
-        version = "1.0.1";
+        version = "1.2";
         src = sources.agda-stdlib;
       });
     };

language-plutus-core/src/Language/PlutusCore/Parser.y

@@ -1,6 +1,8 @@
 {
     {-# LANGUAGE OverloadedStrings  #-}
     module Language.PlutusCore.Parser ( parse
+				      , parseTm
+				      , parseTy 
                                       , parseST
                                       , parseTermST
                                       , parseTypeST
@@ -187,6 +189,12 @@ parseType str = mapParseRun (parseTypeST str)
 parse :: BSL.ByteString -> Either (ParseError AlexPosn) (Program TyName Name AlexPosn)
 parse str = fmap fst $ runExcept $ runStateT (parseST str) emptyIdentifierState
 
+parseTm :: BSL.ByteString -> Either (ParseError AlexPosn) (Term TyName Name AlexPosn)
+parseTm str = fmap fst $ runExcept $ runStateT (parseTermST str) emptyIdentifierState
+
+parseTy :: BSL.ByteString -> Either (ParseError AlexPosn) (Type TyName AlexPosn)
+parseTy str = fmap fst $ runExcept $ runStateT (parseTypeST str) emptyIdentifierState
+
 type Parse = ExceptT (ParseError AlexPosn) Alex
 
 parseError :: Token AlexPosn -> Parse b

metatheory/Algorithmic.lagda

@@ -68,21 +68,19 @@ A variable is indexed by its context and type.
 open import Type.BetaNormal.Equality
 data _∋_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
 
-  Z : ∀ {Φ Γ} {A B : Φ ⊢Nf⋆ *}
-    → A ≡Nf B
+  Z : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *}
       ----------
-    → Γ , A ∋ B
+    → Γ , A ∋ A
 
   S : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *} {B : Φ ⊢Nf⋆ *}
     → Γ ∋ A
       ----------
     → Γ , B ∋ A
 
-  T : ∀ {Φ Γ K}{A : Φ ⊢Nf⋆ *}{B : Φ ,⋆ K ⊢Nf⋆ *}
+  T : ∀ {Φ Γ K}{A : Φ ⊢Nf⋆ *}
     → Γ ∋ A
-    → weakenNf A ≡Nf B
       -------------------
-    → Γ ,⋆ K ∋ B
+    → Γ ,⋆ K ∋ weakenNf A
 \end{code}
 Let `x`, `y` range over variables.
 
@@ -104,7 +102,6 @@ data _⊢_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
     → Γ ⊢ A
 
   ƛ : ∀ {Φ Γ}{A B : Φ ⊢Nf⋆ *}
-    → String
     → Γ , A ⊢ B
       -----------
     → Γ ⊢ A ⇒ B
@@ -116,20 +113,17 @@ data _⊢_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
     → Γ ⊢ B
 
   Λ : ∀ {Φ Γ K}
-    → (x : String)
     → {B : Φ ,⋆ K ⊢Nf⋆ *}
     → Γ ,⋆ K ⊢ B
       ----------
-    → Γ ⊢ Π x B
+    → Γ ⊢ Π B
 
-  ·⋆ : ∀ {Φ Γ K x}
+  _·⋆_ : ∀ {Φ Γ K}
     → {B : Φ ,⋆ K ⊢Nf⋆ *}
-    → {C : Φ ⊢Nf⋆ *}
-    → Γ ⊢ Π x B
+    → Γ ⊢ Π B
     → (A : Φ ⊢Nf⋆ K)
-    → (B [ A ]) ≡Nf C
       ---------------
-    → Γ ⊢ C
+    → Γ ⊢ B [ A ]
 
   wrap1 : ∀{Φ Γ K}
    → (pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *)
@@ -141,9 +135,7 @@ data _⊢_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
     → {pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}
     → {arg : Φ ⊢Nf⋆ K}
     → (term : Γ ⊢ ne (μ1 · pat · arg))
-    → {B : Φ ⊢Nf⋆ *}
-    → nf (embNf pat · (μ1 · embNf pat) · embNf arg) ≡Nf B
-    → Γ ⊢ B 
+    → Γ ⊢ nf (embNf pat · (μ1 · embNf pat) · embNf arg)
 
   con : ∀{Φ}{Γ : Ctx Φ}{tcn}
     → TermCon {Φ} (con tcn)
@@ -155,10 +147,8 @@ data _⊢_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
     → let Δ ,, As ,, C = SIG bn in
       (σ : ∀ {J} → Δ ∋⋆ J → Φ ⊢Nf⋆ J)
     → Tel Γ Δ σ As
-    → {B : Φ ⊢Nf⋆ *}
-    → substNf σ C ≡Nf B
       -------------------------------
-    → Γ ⊢ B
+    → Γ ⊢ substNf σ C
 
   error : ∀{Φ Γ} → (A : Φ ⊢Nf⋆ *) → Γ ⊢ A
 
@@ -173,10 +163,10 @@ Tel Γ Δ σ (A ∷ As) = Γ ⊢ substNf σ A × Tel Γ Δ σ As
 --void = Λ (ƛ (` Z))
 
 true : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ booleanNf
-true = Λ "α" (ƛ "t" (ƛ "f" (` (S (Z reflNf)))))
+true = Λ (ƛ (ƛ (` (S Z))))
 
 false : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ booleanNf
-false = Λ "α" (ƛ "t" (ƛ "f" (` (Z reflNf))))
+false = Λ (ƛ (ƛ (` Z)))
 \end{code}
 
 Utility functions
@@ -185,64 +175,29 @@ Utility functions
 open import Type.BetaNormal.Equality
 
 
-data _≡Ctx_ : ∀{Φ} → Ctx Φ → Ctx Φ → Set where
-  ∅ : ∅ ≡Ctx ∅
-  _,⋆_ : ∀{Φ}{Γ Γ' : Ctx Φ} → Γ ≡Ctx Γ' → ∀ K → (Γ ,⋆ K) ≡Ctx (Γ' ,⋆ K)
-  _,_  : ∀{Φ}{Γ Γ' : Ctx Φ} → Γ ≡Ctx Γ' → {A A' : Φ ⊢Nf⋆ *} → A ≡Nf A'
-    → (Γ , A) ≡Ctx (Γ' , A')
-
-reflCtx : ∀{Φ}{Γ : Ctx Φ} → Γ ≡Ctx Γ
-reflCtx {Γ = ∅} = ∅
-reflCtx {Γ = Γ ,⋆ J} = reflCtx ,⋆ J
-reflCtx {Γ = Γ , A} = reflCtx , reflNf
-
 conv∋ : ∀ {Φ Γ Γ'}{A A' : Φ ⊢Nf⋆ *}
- → Γ ≡Ctx Γ'
- → A ≡Nf A'
- →  (Γ ∋ A)
+ → Γ ≡ Γ'
+ → A ≡ A'
+ → Γ ∋ A
  → Γ' ∋ A'
-conv∋ (p , q) r (Z s) = Z (transNf (symNf q) (transNf s r))
-conv∋ (p , q) r (S α) = S (conv∋ p r α)
-conv∋ (p  ,⋆ K) q (T α r) = T (conv∋ p reflNf α) (transNf r q)
+conv∋ refl refl x = x
 
 open import Type.BetaNBE.Completeness
 open import Type.Equality
 open import Type.BetaNBE.RenamingSubstitution
 
 conv⊢ : ∀ {Φ Γ Γ'}{A A' : Φ ⊢Nf⋆ *}
- → Γ ≡Ctx Γ'
- → A ≡Nf A'
+ → Γ ≡ Γ'
+ → A ≡ A'
  → Γ ⊢ A
  → Γ' ⊢ A'
+conv⊢ refl refl t = t
 
 convTel : ∀ {Φ Ψ}{Γ Γ' : Ctx Φ}
-  → Γ ≡Ctx Γ'
+  → Γ ≡ Γ'
   → (σ : ∀{J} → Ψ ∋⋆ J → Φ ⊢Nf⋆ J)
   → (As : List (Ψ ⊢Nf⋆ *))
   → Tel Γ Ψ σ As → Tel Γ' Ψ σ As
 convTel p σ []       tt        = tt
-convTel p σ (A ∷ As) (t ,, ts) = conv⊢ p reflNf t ,, convTel p σ As ts
-
-conv⊢ p q          (` x)             = ` (conv∋ p q x)
-conv⊢ p (⇒≡Nf q r) (ƛ x t)           = ƛ x (conv⊢ (p , q) r t)
-conv⊢ p q          (t · u)           =
-  conv⊢ p (⇒≡Nf reflNf q) t · conv⊢ p reflNf u
-conv⊢ p (Π≡Nf q)   (Λ x t)           = Λ _ (conv⊢ (p ,⋆ _) q t)
-conv⊢ p q          (·⋆ t A r)        = ·⋆ (conv⊢ p reflNf t) A (transNf r q) 
-conv⊢ p (ne≡Nf (·≡Ne {B' = arg'} (·≡Ne {B' = pat'} μ≡Ne q) r)) (wrap1 pat arg t)
-  =
-  wrap1
-    _
-    _
-    (conv⊢ p (completeness
-        {s = embNf pat · (μ1 · embNf pat) · embNf arg}
-        {t = embNf pat'  · (μ1 · embNf pat') · embNf arg'}
-        (α2β (·≡α (·≡α (embNf-cong q) (·≡α μ≡α (embNf-cong q)))
-                  (embNf-cong r)))) t)
-conv⊢ p q          (unwrap1 t r)       =
-  unwrap1 (conv⊢ p reflNf t) (transNf r q)
-conv⊢ p con≡Nf     (con c)             = con c
-conv⊢ p q          (builtin bn σ ts r) =
-  builtin bn σ (convTel p σ _ ts) (transNf r q)
-conv⊢ p q          (error A)           = error _
+convTel p σ (A ∷ As) (t ,, ts) = conv⊢ p refl t ,, convTel p σ As ts
 \end{code}

metatheory/Algorithmic/CK.lagda.md

@@ -26,16 +26,14 @@ data Frame : ∀{Φ Φ'} → Ctx Φ → (T : Φ ⊢Nf⋆ *) → Ctx Φ' → (H :
   where
   -·_     : ∀{Φ}{Γ}{A B : Φ ⊢Nf⋆ *} → Γ ⊢ A → Frame Γ B Γ (A ⇒ B)
   _·-     : ∀{Φ}{Γ}{A B : Φ ⊢Nf⋆ *}{t : Γ ⊢ A ⇒ B} → Value t → Frame Γ B Γ A
-  Λ-      : ∀{Φ}{Γ}{K}{x}{B : Φ ,⋆ K ⊢Nf⋆ *} → Frame Γ (Π x B) (Γ ,⋆ K) B
-  -·⋆    : ∀{Φ K Γ x}{B : Φ ,⋆ K ⊢Nf⋆ *}(A : Φ ⊢Nf⋆ K){C : Φ ⊢Nf⋆ *} → (B [ A ]Nf) ≡Nf C
-    → Frame Γ C Γ (Π x B)
+  Λ-      : ∀{Φ}{Γ}{K}{B : Φ ,⋆ K ⊢Nf⋆ *} → Frame Γ (Π B) (Γ ,⋆ K) B
+  -·⋆    : ∀{Φ K Γ}{B : Φ ,⋆ K ⊢Nf⋆ *}(A : Φ ⊢Nf⋆ K)
+    → Frame Γ (B [ A ]Nf) Γ (Π B)
   wrap-   : ∀{Φ Γ K}{pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}{arg : Φ ⊢Nf⋆ K}
     → Frame Γ (ne (μ1 · pat · arg))
             Γ (nf (embNf pat · (μ1 · embNf pat) · embNf arg))
   unwrap- : ∀{Φ Γ K}{pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}{arg : Φ ⊢Nf⋆ K}
-    → {B : Φ ⊢Nf⋆ *}
-    → nf (embNf pat · (μ1 · embNf pat) · embNf arg) ≡Nf B
-    → Frame Γ B
+    → Frame Γ (nf (embNf pat · (μ1 · embNf pat) · embNf arg))
             Γ (ne (μ1 · pat · arg))
 
 data Stack : ∀{Φ Φ'}(Γ : Ctx Φ)(T : Φ ⊢Nf⋆ *)(Γ' : Ctx Φ')(H : Φ' ⊢Nf⋆ *) → Set
@@ -61,10 +59,10 @@ closeFrame : ∀{Φ}{Γ : Ctx Φ}{T : Φ ⊢Nf⋆ *} → ∀{Φ'}{Γ' : Ctx Φ'}
   → Frame Γ T Γ' H → Γ' ⊢ H →  Γ ⊢ T
 closeFrame (-· u)          t = t · u
 closeFrame (_·- {t = t} v) u = t · u
-closeFrame (Λ- {x = x})    t = Λ x t
-closeFrame (-·⋆ A p)       t = ·⋆ t A p
+closeFrame Λ-              t = Λ t
+closeFrame (-·⋆ A)         t = _·⋆_ t A
 closeFrame wrap-           t = wrap1 _ _ t
-closeFrame (unwrap- p)     t = unwrap1 t p
+closeFrame unwrap-         t = unwrap1 t
 
 -- Plugging a term into a stack yields a term again
 
@@ -99,23 +97,23 @@ step : ∀{Φ Φ'}{Γ : Ctx Φ}{Γ' : Ctx Φ'}{A : Φ ⊢Nf⋆ *}{H : Φ' ⊢Nf
   → Σ (Ctx Φ'') λ Γ''
   → NoVar Γ'' × Σ (Φ'' ⊢Nf⋆ *) (State Γ A Γ'')
 step p (s ▻ ` x)                          = ⊥-elim (noVar p x)
-step p (s ▻ ƛ x L)                        = _ ,, _ ,, p ,, _ ,, s ◅ V-ƛ {x = x}{N = L}
+step p (s ▻ ƛ L)                          = _ ,, _ ,, p ,, _ ,, s ◅ V-ƛ {N = L}
 step p (s ▻ (L · M))                      = _ ,, _ ,, p ,, _ ,, (s , -· M) ▻ L
-step p (s ▻ Λ x L)                        = _ ,, _ ,, p ,, _ ,, (s , Λ-) ▻ L
-step p (s ▻ (·⋆ L A q))                   = _ ,, _ ,, p ,, _ ,, (s , -·⋆ A q) ▻ L
+step p (s ▻ Λ L)                          = _ ,, _ ,, p ,, _ ,, (s , Λ-) ▻ L
+step p (s ▻ (_·⋆_ L A))                   = _ ,, _ ,, p ,, _ ,, (s , -·⋆ A) ▻ L
 step p (s ▻ wrap1 pat arg L)              = _ ,, _ ,, p ,, _ ,, (s , wrap-) ▻ L
-step p (s ▻ unwrap1 L q)                  = _ ,, _ ,, p ,, _ ,, (s , unwrap- q) ▻ L
+step p (s ▻ unwrap1 L)                    = _ ,, _ ,, p ,, _ ,, (s , unwrap-) ▻ L
 step {Γ' = Γ'} p (s ▻ con cn)             = _ ,, Γ' ,, p ,, _ ,, s ◅ V-con cn
-step {Γ' = Γ'} p (s ▻ builtin bn σ tel q) =
+step {Γ' = Γ'} p (s ▻ builtin bn σ tel)   =
   _ ,, Γ' ,, p ,, _ ,, ◆ Γ' (substNf σ (proj₂ (proj₂ (SIG bn))))
 step {Γ' = Γ'} p (s ▻ error A)            =  _ ,, Γ' ,, p ,, _ ,, ◆ Γ' A
 step p (ε ◅ V)                            = _ ,, _ ,, p ,, _ ,, □ V
 step p ((s , (-· M)) ◅ V)                 = _ ,, _ ,, p ,, _ ,, ((s , V ·-) ▻ M)
 step p (_◅_ (s , (V-ƛ {N = t} ·-)) {u} V) = _ ,, _ ,, p ,, _ ,, s ▻ (t [ u ])
 step p ((s , Λ-) ◅ V)                     = _ ,, _ ,, p ,, _ ,, s ◅ V-Λ V
-step p ((s , (-·⋆ A q)) ◅ V-Λ {N = t} V)  = _ ,, _ ,, p ,, _ ,, s ▻ conv⊢ reflCtx q (t [ A ]⋆)
+step p ((s , (-·⋆ A)) ◅ V-Λ {N = t} V)  = _ ,, _ ,, p ,, _ ,, s ▻ (t [ A ]⋆)
 step p ((s , wrap-) ◅ V)                  = _ ,, _ ,, p ,, _ ,, s ◅ (V-wrap V)
-step p ((s , unwrap- q) ◅ V-wrap V)       = _ ,, _ ,, p ,, _ ,, s ◅ convVal reflCtx q V
+step p ((s , unwrap-) ◅ V-wrap V)         = _ ,, _ ,, p ,, _ ,, s ◅ V
 step p (□ V)                              = _ ,, _ ,, p ,, _ ,, □ V
 step {Γ = Γ} p (◆ Γ' A)                   = _ ,, _ ,, p ,, _ ,, ◆ Γ' A
 ```