[ new ] inlining let-bound expressions used at most one

Author: gallais

src/Generic/Semantics/Elaboration/LetCounter.agda

@@ -0,0 +1,72 @@
+module Generic.Semantics.Elaboration.LetCounter where
+
+import Level as L
+open import Size
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Bool
+open import Data.Product
+import Data.Product.Categorical.Right as PC
+open import Data.List.Base
+open import Data.List.Relation.Unary.All as All
+open import Data.List.Relation.Unary.All.Properties
+open import Function
+
+open import var
+open import varlike
+open import indexed
+open import environment using (Kripke; th^Var; ε; _∙_; extend)
+open import Generic.Syntax
+import Generic.Syntax.LetCounter as LetCounter
+open LetCounter hiding (Let)
+import Generic.Syntax.LetBinder as LetBinder
+open import Generic.Semantics
+open import Generic.Semantics.Syntactic
+
+module _ {I : Set} {d : Desc I} where
+
+  module PCR {Γ : List I} = PC L.zero (rawMonoid Γ)
+
+  Counted : I ─Scoped → I ─Scoped
+  Counted T i Γ = T i Γ × Count Γ
+
+  count : ∀ {σ Γ} e → ⟦ e ⟧ (Kripke Var (Counted (Tm (d `+ LetCounter.Let) ∞))) σ Γ →
+                      Counted (⟦ e ⟧ (Scope (Tm (d `+ LetCounter.Let) ∞))) σ Γ
+  count (`σ A e)   (a , t)  = map₁ (a ,_) (count (e a) t)
+  count (`X Δ j e) (kr , t) =
+    let (r , cr) = reify vl^Var Δ j kr
+        (u , cu) = count e t
+    in (r , u) , merge (++⁻ʳ Δ cr) cu
+  count (`∎ eq)    t        = t , zeros
+
+  LetCount : Sem (d `+ LetBinder.Let) Var (Counted (Tm (d `+ LetCounter.Let) ∞))
+  Sem.th^𝓥  LetCount = th^Var
+  Sem.var    LetCount = λ v → `var v , fromVar v
+  Sem.alg    LetCount = λ where
+    (true , t) → map₁ (`con ∘′ (true ,_)) (count d t)
+    (false , στ , (e , ce) , tct , refl) →
+      let (t , ct) = tct extend (ε ∙ z)
+          e-usage  = All.head ct
+      in `con (false , e-usage , στ , e , t , refl)
+       , -- if e (the let-bound expression) is not used in t (the body of the let)
+         -- we can ignore its contribution to the count:
+         (case e-usage of λ where
+           zero → All.tail ct
+           _    → merge ce (All.tail ct))
+
+  annotate : ∀ {σ Γ} → Tm (d `+ LetBinder.Let) ∞ σ Γ → Tm (d `+ LetCounter.Let) ∞ σ Γ
+  annotate = proj₁ ∘′ Sem.sem LetCount (base vl^Var)
+
+  Inline : Sem (d `+ LetCounter.Let) (Tm (d `+ LetBinder.Let) ∞)
+                                     (Tm (d `+ LetBinder.Let) ∞)
+  Sem.th^𝓥 Inline = th^Tm
+  Sem.var   Inline = id
+  Sem.alg   Inline = λ where
+    (true , t)                       → `con (true , fmap d (reify vl^Tm) t)
+    (false , many , στ , e , b , eq) → `con (false , στ , e , b extend (ε ∙ `var z) , eq)
+    (false , _ , στ , e , b , refl)  → b (base vl^Var) (ε ∙ e)
+
+  inline : ∀ {σ Γ} → Tm (d `+ LetCounter.Let) ∞ σ Γ → Tm (d `+ LetBinder.Let) ∞ σ Γ
+  inline = Sem.sem Inline (base vl^Tm)
+
+  inline-affine : ∀ {σ Γ} → Tm (d `+ LetBinder.Let) ∞ σ Γ → Tm (d `+ LetBinder.Let) ∞ σ Γ
+  inline-affine = inline ∘′ annotate

src/Generic/Syntax/LetBinder.agda

@@ -18,3 +18,8 @@ module _ {I : Set} where
 
 pattern `IN' e t = (_ , e , t , refl)
 pattern `IN  e t = `con (`IN' e t)
+
+module _ {I : Set} {d : Desc I} where
+
+  embed : ∀ {i σ} → [ Tm d i σ ⟶ Tm (d `+ Let) i σ ]
+  embed = map^Tm (MkDescMorphism (true ,_))

src/Generic/Syntax/LetBinders.agda

@@ -1,14 +1,21 @@
 module Generic.Syntax.LetBinders where
 
+open import Data.Bool
 open import Data.Product
 open import Agda.Builtin.List
 open import Agda.Builtin.Equality
 open import Function
 
+open import indexed
 open import Generic.Syntax
 
 module _ {I : Set} where
 
   Lets : Desc I
   Lets = `σ (List I × I) $ uncurry $ λ Δ σ →
          `Xs Δ (`X Δ σ (`∎ σ))
+
+module _ {I : Set} {d : Desc I} where
+
+  embed : ∀ {i σ} → [ Tm d i σ ⟶ Tm (d `+ Lets) i σ ]
+  embed = map^Tm (MkDescMorphism (true ,_))

src/Generic/Syntax/LetCounter.agda

@@ -0,0 +1,61 @@
+module Generic.Syntax.LetCounter where
+
+open import Algebra
+open import Data.Bool
+open import Data.Product
+open import Data.List.Relation.Unary.All
+open import Agda.Builtin.List
+open import Agda.Builtin.Equality
+open import Function
+
+open import indexed
+open import var
+open import Generic.Syntax
+
+import Generic.Syntax.LetBinder as LetBinder
+
+data Counter : Set where
+  zero : Counter
+  one  : Counter
+  many : Counter
+
+_+_ : Counter → Counter → Counter
+zero + n = n
+m + zero = m
+_ + _    = many
+
+module _ {I : Set} where
+
+  Count : List I → Set
+  Count = All (λ _ → Counter)
+
+  zeros : [ Count ]
+  zeros = tabulate (λ _ → zero)
+
+  fromVar : ∀ {i} → [ Var i ⟶ Count ]
+  fromVar z     = one ∷ zeros
+  fromVar (s v) = zero ∷ fromVar v
+
+  merge : [ Count ⟶ Count ⟶ Count ]
+  merge = curry (zipWith (uncurry _+_))
+
+  rawMonoid : List I → RawMonoid _ _
+  rawMonoid Γ = record
+    { Carrier = Count Γ
+    ; _≈_     = _≡_
+    ; _∙_     = merge
+    ; ε       = tabulate (λ _ → zero)
+    }
+
+module _ {I : Set} where
+
+  Let : Desc I
+  Let = `σ Counter $ λ _ → LetBinder.Let
+
+pattern `IN' e t = (_ , e , t , refl)
+pattern `IN  e t = `con (`IN' e t)
+
+module _ {I : Set} {d : Desc I} where
+
+  embed : ∀ {i σ} → [ Tm d i σ ⟶ Tm (d `+ Let) i σ ]
+  embed = map^Tm (MkDescMorphism (true ,_))