updating ap-pal synatx to mixfix to match the text, alias for splice,…

… some unicode trickery
hazelgrove · Oct 19, 2020 · a9708e3 · a9708e3
1 parent d733529
commit a9708e3
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 32 deletions.
diff --git a/core.agda b/core.agda
@@ -85,34 +85,41 @@ module core where
       model-type : typ
       expansion-type : typ
 
+
   -- unexpanded expressions, the outermost layer of expressions: a langauge
   -- exactly like eexp, but also with livelits
-  data uexp : Set where
-    c       : uexp
-    _·:_    : uexp → typ → uexp
-    X       : varname → uexp
-    ·λ      : varname → uexp → uexp
-    ·λ_[_]_ : varname → typ → uexp → uexp
-    ⦇⦈[_]   : holename → uexp
-    ⦇⌜_⌟⦈[_]  : uexp → holename → uexp
-    _∘_     : uexp → uexp → uexp
-    ⟨_,_⟩   : uexp → uexp → uexp
-    fst     : uexp → uexp
-    snd     : uexp → uexp
-    -- new forms below
-    -- macro-like livelits --todo pal
-    ap-pal : livelitname → iexp → (typ × uexp) → uexp  -- paper: $a<d_model; {phi_i} i<n >^u
-
-    -- ap-pal : ($a : Nat) → (d : iexp) → (splice : typ × uexp) → uexp --
-    -- give livelit name = nat and then this first nat is that
-
-    -- phi is a splice, which is a pair of typ and uexp. in the paper it's
-    -- n-ary but here we have one becauase we could tuple it up. look into
-    -- making it List (type × uexp). also define a type for splice that's this pair.
-
-    -- u doesn't appear here, it's a hole name which is nat but we can make
-    -- a separate alias. add it but just carry it around. todo: generally
-    -- give aliases for names instead of Nat everywhere.
+  mutual
+    data uexp : Set where
+      c       : uexp
+      _·:_    : uexp → typ → uexp
+      X       : varname → uexp
+      ·λ      : varname → uexp → uexp
+      ·λ_[_]_ : varname → typ → uexp → uexp
+      ⦇⦈[_]   : holename → uexp
+      ⦇⌜_⌟⦈[_]  : uexp → holename → uexp
+      _∘_     : uexp → uexp → uexp
+      ⟨_,_⟩   : uexp → uexp → uexp
+      fst     : uexp → uexp
+      snd     : uexp → uexp
+      -- new forms below
+      -- macro-like livelits --todo pal
+      --ap-pal : livelitname → iexp → splice → uexp  -- paper: $a<d_model; {phi_i} i<n >^u
+      ＄_⟨_⁏_⟩[_] : livelitname → iexp → splice → holename → uexp
+
+      -- ap-pal : ($a : Nat) → (d : iexp) → (splice : typ × uexp) → uexp --
+      -- give livelit name = nat and then this first nat is that
+
+      -- phi is a splice, which is a pair of typ and uexp. in the paper it's
+      -- n-ary but here we have one becauase we could tuple it up. look into
+      -- making it List (type × uexp). also define a type for splice that's this pair.
+
+      -- u doesn't appear here, it's a hole name which is nat but we can make
+      -- a separate alias. add it but just carry it around. todo: generally
+      -- give aliases for names instead of Nat everywhere.
+
+    splice : Set
+    splice = typ × uexp
+
 
   -- type consistency
   data _~_ : (t1 t2 : typ) → Set where
@@ -964,16 +971,16 @@ module core where
                            Φ , Γ ⊢ ê2 ~~> e2 ⇒ τ2 →
                            holes-disjoint e1 e2 →
                            Φ , Γ ⊢ ⟨ ê1 , ê2 ⟩ ~~> ⟨ e1 , e2 ⟩ ⇒ τ1 ⊗ τ2
-        SPEApPal  : ∀{Φ Γ ρ dm π denc eexpanded τsplice psplice esplice} →
+        SPEApPal  : ∀{Φ Γ a dm π denc eexpanded τsplice psplice esplice u} →
                          holes-disjoint eexpanded esplice →
                          freshΓ Γ eexpanded →
-                         (ρ , π) ∈ (Φ)₁ →
+                         (a , π) ∈ (Φ)₁ →
                          ∅ , ∅ ⊢ dm :: (livelitdef.model-type π) →
                          ((livelitdef.expand π) ∘ dm) ⇓ denc →
                          denc ↑ eexpanded →
                          Φ , Γ ⊢ psplice ~~> esplice ⇐ τsplice →
                          ∅ ⊢ eexpanded <= τsplice ==> (livelitdef.expansion-type π) →
-                         Φ , Γ ⊢ ap-pal ρ dm (τsplice , psplice) ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π
+                         Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) ⟩[ u ] ~~> ((eexpanded ·: τsplice ==> livelitdef.expansion-type π) ∘ esplice) ⇒ livelitdef.expansion-type π
 
     data _,_⊢_~~>_⇐_ : (Φ : palctx) →
                        (Γ : tctx) →

diff --git a/livelit-reasoning-principles.agda b/livelit-reasoning-principles.agda
@@ -27,9 +27,9 @@ module livelit-reasoning-principles where
       splice-typing             : Φ , Γ ⊢ êsplice ~~> esplice ⇐ τsplice × Γ ⊢ esplice <= τsplice
       context-independence      : free-vars (eexpanded ·: τsplice ==> τresult) == []
 
-  livelit-reasoning-principles : ∀{Φ Γ ρ dm τsplice psplice eresult τresult} →
-        Φ , Γ ⊢ ap-pal ρ dm (τsplice , psplice) ~~> eresult ⇒ τresult →
-        reasoning-principles Φ Γ ρ dm τsplice psplice eresult τresult
+  livelit-reasoning-principles : ∀{Φ Γ a dm τsplice psplice eresult τresult u} →
+        Φ , Γ ⊢ ＄ a ⟨ dm ⁏ (τsplice , psplice) ⟩[ u ] ~~> eresult ⇒ τresult →
+        reasoning-principles Φ Γ a dm τsplice psplice eresult τresult
   livelit-reasoning-principles h@(SPEApPal {dm = dm} {π} {denc} {eexpanded} {esplice = esplice} x x₁ x₂ x₃ x₄ x₅ x₆ x₇) =
        record
          { π                         = π