never inline let bindings from the original source

lib/Quox/Untyped/Erase.idr

@@ -250,7 +250,7 @@ eraseTerm' defs ctx ty (Let pi e s loc) = do
     Kept => do
       EraRes ety e' <- eraseElim defs ctx e
       s' <- eraseTerm defs (extendTyLet pi x ety (E e) ctx) (weakT 1 ty) s.term
-      pure $ Let x e' s' loc
+      pure $ Let True x e' s' loc
 
 --  e ⤋ e' ⇒ B
 -- ------------
@@ -321,9 +321,9 @@ eraseElim defs ctx (CasePair qty pair ret body loc) = do
       body' <- eraseTerm defs ctx' ty body.term
       p <- mnb "p" loc
       pure $ EraRes (sub1 ret pair) $
-        Let p eterm
+        Let False p eterm
-          (Let x (Fst (B VZ loc) loc)
+          (Let False x (Fst (B VZ loc) loc)
-            (Let y (Snd (B (VS VZ) loc) loc)
+            (Let False y (Snd (B (VS VZ) loc) loc)
               (body' // (B VZ loc ::: B (VS VZ) loc ::: shift 3))
               loc) loc) loc
     Erased => do
@@ -425,7 +425,7 @@ eraseElim defs ctx (CaseBox qty box ret body loc) = do
     Kept => do
       ebox  <- eraseElim defs ctx box
       ebody <- eraseTerm defs ctx' bty body.term
-      pure $ EraRes (sub1 ret box) $ Let body.name ebox.term ebody loc
+      pure $ EraRes (sub1 ret box) $ Let False body.name ebox.term ebody loc
     Erased => do
       body' <- eraseTerm defs ctx' bty body.term
       pure $ EraRes (sub1 ret box) $ body' // one (Erased loc)
@@ -487,7 +487,7 @@ uses i (CaseNat nat zer suc _) = uses i nat + max (uses i zer) (uses' suc)
         uses' (NSRec  _ _ s) = uses (VS (VS i)) s
         uses' (NSNonrec _ s) = uses (VS i) s
 uses i (Str {}) = 0
-uses i (Let x rhs body _) = uses i rhs + uses (VS i) body
+uses i (Let _ x rhs body _) = uses i rhs + uses (VS i) body
 uses i (Erased {}) = 0
 
 export
@@ -539,13 +539,15 @@ trimLets (CaseNat nat zer suc loc) =
         trimLets' (NSRec x ih s) = NSRec    x ih $ trimLets s
         trimLets' (NSNonrec x s) = NSNonrec x    $ trimLets s
 trimLets (Str s loc) = Str s loc
-trimLets (Let x rhs body loc) =
+trimLets (Let True x rhs body loc) =
+  Let True x (trimLets rhs) (trimLets body) loc
+trimLets (Let False x rhs body loc) =
   let rhs'  = trimLets rhs
       body' = trimLets body
       uses  = uses VZ body in
   if inlineable rhs' || uses == 1 || (droppable rhs' && uses == 0)
      then sub1 rhs' body'
-     else Let x rhs' body' loc
+     else Let False x rhs' body' loc
 trimLets (Erased loc) = Erased loc
 
 

lib/Quox/Untyped/Scheme.idr

@@ -225,7 +225,7 @@ toScheme xs (CaseNat nat zer (NSNonrec p suc) _) =
        Lambda [p] !(toScheme (xs :< p) suc),
        !(toScheme xs nat)]
 
-toScheme xs (Let x rhs body _) =
+toScheme xs (Let _ x rhs body _) =
   freshInB x $ \x =>
   pure $ Let x !(toScheme xs rhs) !(toScheme (xs :< x) body)
 

lib/Quox/Untyped/Syntax.idr

@@ -41,16 +41,14 @@ data Term where
 
   Nat : (val : Nat) -> Loc -> Term n
   Succ : (nat : Term n) -> Loc -> Term n
-  CaseNat : (nat : Term n) ->
+  CaseNat : (nat : Term n) -> (zer : Term n) -> (suc : CaseNatSuc n) ->
-            (zer : Term n) ->
+            Loc -> Term n
-            (suc : CaseNatSuc n) ->
-            Loc ->
-            Term n
 
   Str : (str : String) -> Loc -> Term n
 
-  Let : (x : BindName) -> (rhs : Term n) -> (body : Term (S n)) -> Loc ->
+  ||| bool is true if the let comes from the original source code
-        Term n
+  Let : (real : Bool) -> (x : BindName) -> (rhs : Term n) ->
+        (body : Term (S n)) -> Loc -> Term n
 
   Erased : Loc -> Term n
 %name Term s, t, u
@@ -80,7 +78,7 @@ Located (Term n) where
   (Succ _ loc).loc        = loc
   (CaseNat _ _ _ loc).loc = loc
   (Str _ loc).loc         = loc
-  (Let _ _ _ loc).loc     = loc
+  (Let _ _ _ _ loc).loc   = loc
   (Erased loc).loc        = loc
 
 
@@ -165,8 +163,8 @@ splitLam ys t              = Evidence _ (ys, t)
 export
 splitLet : Telescope (\i => (BindName, Term i)) a b -> Term b ->
            Exists $ \c => (Telescope (\i => (BindName, Term i)) a c, Term c)
-splitLet ys (Let x rhs body _) = splitLet (ys :< (x, rhs)) body
+splitLet ys (Let _ x rhs body _) = splitLet (ys :< (x, rhs)) body
-splitLet ys t                  = Evidence _ (ys, t)
+splitLet ys t                    = Evidence _ (ys, t)
 
 private covering
 prettyLets : {opts : LayoutOpts} ->
@@ -219,7 +217,7 @@ prettyTerm xs (CaseNat nat zer suc _) =
   prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
 prettyTerm xs (Str s _) =
   prettyStrLit s
-prettyTerm xs (Let x rhs body _) =
+prettyTerm xs (Let _ x rhs body _) =
   parensIfM Outer =<< do
     let Evidence n' (lets, body) = splitLet [< (x, rhs)] body
     heads <- prettyLets xs lets
@@ -288,8 +286,8 @@ CanSubstSelf Term where
               (assert_total substSuc suc th) loc
     Str s loc =>
       Str s loc
-    Let x rhs body loc =>
+    Let u x rhs body loc =>
-      Let x (rhs // th) (assert_total $ body // push th) loc
+      Let u x (rhs // th) (assert_total $ body // push th) loc
     Erased loc =>
       Erased loc
   where