add let to the core

lib/Quox/Displace.idr

@@ -34,6 +34,8 @@ parameters (k : Universe)
     doDisplace (Str s loc) = Str s loc
     doDisplace (BOX qty ty loc) = BOX qty (doDisplace ty) loc
     doDisplace (Box val loc) = Box (doDisplace val) loc
+    doDisplace (Let qty rhs body loc) =
+      Let qty (doDisplace rhs) (doDisplaceS body) loc
     doDisplace (E e) = E (doDisplace e)
     doDisplace (CloT (Sub t th)) =
       CloT (Sub (doDisplace t) (assert_total $ map doDisplace th))

lib/Quox/FreeVars.idr

@@ -197,6 +197,7 @@ HasFreeVars (Term d) where
   fv (Str     {})             = none
   fv (BOX     {ty, _})        = fv ty
   fv (Box     {val, _})       = fv val
+  fv (Let     {rhs, body, _}) = fv rhs <+> fv body
   fv (E       e)              = fv e
   fv (CloT    s)              = fv s
   fv (DCloT   s)              = fv s.term
@@ -275,6 +276,7 @@ HasFreeDVars Term where
   fdv (Str     {})             = none
   fdv (BOX     {ty, _})        = fdv ty
   fdv (Box     {val, _})       = fdv val
+  fdv (Let     {rhs, body, _}) = fdv rhs <+> fdvT body
   fdv (E       e)              = fdv e
   fdv (CloT    s)              = fdv s @{WithSubst}
   fdv (DCloT   s)              = fdvSubst s

lib/Quox/Parser/FromParser.idr

@@ -265,7 +265,10 @@ mutual
         <*> pure loc
 
     Let (qty, x, rhs) body loc =>
-      ?fromPTerm_let
+      Let (fromPQty qty)
+        <$> fromPTermElim ds ns rhs
+        <*> fromPTermTScope ds ns [< x] body
+        <*> pure loc
 
   private
   fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->

lib/Quox/Pretty.idr

@@ -267,8 +267,8 @@ prettyDBind = hl DVar . prettyBind'
 
 export %inline
 typeD, ioStateD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
-stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD,
+stringD, eqD, colonD, commaD, semiD, atD, caseD, typecaseD, returnD, ofD, dotD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD :
+zeroD, succD, coeD, compD, undD, cstD, pipeD, fstD, sndD, letD, inD :
   {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 ioStateD  = hl Syntax $ text "IOState"
@@ -300,6 +300,8 @@ cstD      = hl Syntax   $ text "="
 pipeD     = hl Delim    $ text "|"
 fstD      = hl Syntax   $ text "fst"
 sndD      = hl Syntax   $ text "snd"
+letD      = hl Syntax   $ text "let"
+inD       = hl Syntax   $ text "in"
 
 
 export

lib/Quox/Syntax/Term/Base.idr

@@ -99,6 +99,9 @@ mutual
     BOX : (qty : Qty) -> (ty : Term d n) -> (loc : Loc) -> Term d n
     Box : (val : Term d n) -> (loc : Loc) -> Term d n
 
+    Let : (qty : Qty) -> (rhs : Elim d n) ->
+          (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+
     ||| elimination
     E : (e : Elim d n) -> Term d n
 
@@ -383,6 +386,7 @@ Located (Term d n) where
   (Succ _ loc).loc      = loc
   (BOX _ _ loc).loc     = loc
   (Box _ loc).loc       = loc
+  (Let _ _ _ loc).loc   = loc
   (E e).loc             = e.loc
   (CloT (Sub t _)).loc  = t.loc
   (DCloT (Sub t _)).loc = t.loc
@@ -446,6 +450,7 @@ Relocatable (Term d n) where
   setLoc loc (Str s _) = Str s loc
   setLoc loc (BOX qty ty _) = BOX qty ty loc
   setLoc loc (Box val _) = Box val loc
+  setLoc loc (Let qty rhs body _) = Let qty rhs body loc
   setLoc loc (E e) = E $ setLoc loc e
   setLoc loc (CloT (Sub term subst)) = CloT $ Sub (setLoc loc term) subst
   setLoc loc (DCloT (Sub term subst)) = DCloT $ Sub (setLoc loc term) subst

lib/Quox/Syntax/Term/Pretty.idr

@@ -317,6 +317,44 @@ prettyCase dnames tnames qty head ret body =
   prettyCase_ dnames tnames ![|caseD <+> prettyQty qty|] head ret body
 
 
+private
+LetBinder : Nat -> Nat -> Type
+LetBinder d n = (Qty, BindName, Elim d n)
+
+private
+LetExpr : Nat -> Nat -> Nat -> Type
+LetExpr d n n' = (Telescope (LetBinder d) n n', Term d n')
+
+private
+PrettyLetResult : LayoutOpts -> Nat -> Type
+PrettyLetResult opts d =
+  Exists $ \n => (BContext n, Term d n, SnocList (Doc opts))
+
+-- [todo] factor out this and the untyped version somehow
+export
+splitLet : Telescope (LetBinder d) n n' -> Term d n' -> Exists (LetExpr d n)
+splitLet ys t@(Let qty rhs body _) =
+  splitLet (ys :< (qty, body.name, rhs)) (assert_smaller t body.term)
+splitLet ys t =
+  Evidence _ (ys, t)
+
+private covering
+prettyLets : {opts : LayoutOpts} ->
+             BContext d -> BContext a -> Telescope (LetBinder d) a b ->
+             Eff Pretty (SnocList (Doc opts))
+prettyLets dnames xs lets = sequence $ snd $ go lets where
+  go : forall b. Telescope (LetBinder d) a b ->
+       (BContext b, SnocList (Eff Pretty (Doc opts)))
+  go [<] = (xs, [<])
+  go (lets :< (qty, x, rhs)) =
+    let (ys, docs) = go lets
+        doc = do
+          x   <- prettyTBind x
+          rhs <- withPrec Outer $ assert_total prettyElim dnames ys rhs
+          hangDSingle (hsep [!letD, x, !cstD]) (hsep [rhs, !inD]) in
+    (ys :< x, docs :< doc)
+
+
 private
 isDefaultDir : Dim d -> Dim d -> Bool
 isDefaultDir (K Zero _) (K One _) = True
@@ -457,6 +495,14 @@ prettyTerm dnames tnames (BOX qty ty _) =
 prettyTerm dnames tnames (Box val _) =
   bracks =<< withPrec Outer (prettyTerm dnames tnames val)
 
+prettyTerm dnames tnames (Let qty rhs body _) = do
+  let Evidence _ (lets, body) = splitLet [< (qty, body.name, rhs)] body.term
+  heads <- prettyLets dnames tnames lets
+  let tnames = tnames . map (\(_, x, _) => x) lets
+  body <- withPrec Outer $ assert_total prettyTerm dnames tnames body
+  let lines = toList $ heads :< body
+  pure $ ifMultiline (hsep lines) (vsep lines)
+
 prettyTerm dnames tnames (E e) = prettyElim dnames tnames e
 
 prettyTerm dnames tnames t0@(CloT (Sub t ph)) =

lib/Quox/Syntax/Term/Subst.idr

@@ -249,52 +249,8 @@ mutual
   isCloE (DCloE {}) = True
   isCloE _          = False
 
-mutual
+export
-  export
+PushSubsts Elim Subst.isCloE where
-  PushSubsts Term Subst.isCloT where
-    pushSubstsWith th ph (TYPE l loc) =
-      nclo $ TYPE l loc
-    pushSubstsWith th ph (IOState loc) =
-      nclo $ IOState loc
-    pushSubstsWith th ph (Pi qty a body loc) =
-      nclo $ Pi qty (a // th // ph) (body // th // ph) loc
-    pushSubstsWith th ph (Lam body loc) =
-      nclo $ Lam (body // th // ph) loc
-    pushSubstsWith th ph (Sig a b loc) =
-      nclo $ Sig (a // th // ph) (b // th // ph) loc
-    pushSubstsWith th ph (Pair s t loc) =
-      nclo $ Pair (s // th // ph) (t // th // ph) loc
-    pushSubstsWith th ph (Enum tags loc) =
-      nclo $ Enum tags loc
-    pushSubstsWith th ph (Tag tag loc) =
-      nclo $ Tag tag loc
-    pushSubstsWith th ph (Eq ty l r loc) =
-      nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
-    pushSubstsWith th ph (DLam body loc) =
-      nclo $ DLam (body // th // ph) loc
-    pushSubstsWith _ _ (NAT loc) =
-      nclo $ NAT loc
-    pushSubstsWith _ _ (Nat n loc) =
-      nclo $ Nat n loc
-    pushSubstsWith th ph (Succ n loc) =
-      nclo $ Succ (n // th // ph) loc
-    pushSubstsWith _ _ (STRING loc) =
-      nclo $ STRING loc
-    pushSubstsWith _ _ (Str s loc) =
-      nclo $ Str s loc
-    pushSubstsWith th ph (BOX pi ty loc) =
-      nclo $ BOX pi (ty // th // ph) loc
-    pushSubstsWith th ph (Box val loc) =
-      nclo $ Box (val // th // ph) loc
-    pushSubstsWith th ph (E e) =
-      let Element e nc = pushSubstsWith th ph e in nclo $ E e
-    pushSubstsWith th ph (CloT (Sub s ps)) =
-      pushSubstsWith th (comp th ps ph) s
-    pushSubstsWith th ph (DCloT (Sub s ps)) =
-      pushSubstsWith (ps . th) ph s
-
-  export
-  PushSubsts Elim Subst.isCloE where
   pushSubstsWith th ph (F x u loc) =
     nclo $ F x u loc
   pushSubstsWith th ph (B i loc) =
@@ -335,3 +291,48 @@ mutual
     pushSubstsWith th (comp th ps ph) e
   pushSubstsWith th ph (DCloE (Sub e ps)) =
     pushSubstsWith (ps . th) ph e
+
+export
+PushSubsts Term Subst.isCloT where
+  pushSubstsWith th ph (TYPE l loc) =
+    nclo $ TYPE l loc
+  pushSubstsWith th ph (IOState loc) =
+    nclo $ IOState loc
+  pushSubstsWith th ph (Pi qty a body loc) =
+    nclo $ Pi qty (a // th // ph) (body // th // ph) loc
+  pushSubstsWith th ph (Lam body loc) =
+    nclo $ Lam (body // th // ph) loc
+  pushSubstsWith th ph (Sig a b loc) =
+    nclo $ Sig (a // th // ph) (b // th // ph) loc
+  pushSubstsWith th ph (Pair s t loc) =
+    nclo $ Pair (s // th // ph) (t // th // ph) loc
+  pushSubstsWith th ph (Enum tags loc) =
+    nclo $ Enum tags loc
+  pushSubstsWith th ph (Tag tag loc) =
+    nclo $ Tag tag loc
+  pushSubstsWith th ph (Eq ty l r loc) =
+    nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph) loc
+  pushSubstsWith th ph (DLam body loc) =
+    nclo $ DLam (body // th // ph) loc
+  pushSubstsWith _ _ (NAT loc) =
+    nclo $ NAT loc
+  pushSubstsWith _ _ (Nat n loc) =
+    nclo $ Nat n loc
+  pushSubstsWith th ph (Succ n loc) =
+    nclo $ Succ (n // th // ph) loc
+  pushSubstsWith _ _ (STRING loc) =
+    nclo $ STRING loc
+  pushSubstsWith _ _ (Str s loc) =
+    nclo $ Str s loc
+  pushSubstsWith th ph (BOX pi ty loc) =
+    nclo $ BOX pi (ty // th // ph) loc
+  pushSubstsWith th ph (Box val loc) =
+    nclo $ Box (val // th // ph) loc
+  pushSubstsWith th ph (E e) =
+    let Element e nc = pushSubstsWith th ph e in nclo $ E e
+  pushSubstsWith th ph (Let qty rhs body loc) =
+    nclo $ Let qty (rhs // th // ph) (body // th // ph) loc
+  pushSubstsWith th ph (CloT (Sub s ps)) =
+    pushSubstsWith th (comp th ps ph) s
+  pushSubstsWith th ph (DCloT (Sub s ps)) =
+    pushSubstsWith (ps . th) ph s

lib/Quox/Syntax/Term/Tighten.idr

@@ -75,8 +75,10 @@ mutual
     BOX qty <$> tightenT p ty <*> pure loc
   tightenT' p (Box val loc) =
     Box <$> tightenT p val <*> pure loc
+  tightenT' p (Let qty rhs body loc) =
+    Let qty <$> assert_total tightenE p rhs <*> tightenS p body <*> pure loc
   tightenT' p (E e) =
-    assert_total $ E <$> tightenE p e
+    E <$> assert_total tightenE p e
 
   private
   tightenE' : OPE n1 n2 -> (e : Elim d n2) -> (0 ne : NotClo e) =>
@@ -200,8 +202,10 @@ mutual
     BOX qty <$> dtightenT p ty <*> pure loc
   dtightenT' p (Box val loc) =
     Box <$> dtightenT p val <*> pure loc
+  dtightenT' p (Let qty rhs body loc) =
+    Let qty <$> assert_total dtightenE p rhs <*> dtightenS p body <*> pure loc
   dtightenT' p (E e) =
-    assert_total $ E <$> dtightenE p e
+    E <$> assert_total dtightenE p e
 
   export
   dtightenE' : OPE d1 d2 -> (e : Elim d2 n) -> (0 ne : NotClo e) =>

lib/Quox/Typechecker.idr

@@ -213,6 +213,13 @@ mutual
     -- then Ψ | Γ ⊢ σ · [s] ⇐ [π.A] ⊳ πΣ
     pure $ q * valout
 
+  check' ctx sg (Let qty rhs body loc) ty = do
+    eres <- inferC ctx (subjMult sg qty) rhs
+    qout <- checkC (extendTy (qty * sg.qty) body.name eres.type ctx) sg
+              body.term (weakT 1 ty)
+        >>= popQ loc qty
+    pure $ qty * eres.qout + qout
+
   check' ctx sg (E e) ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx sg e
@@ -286,6 +293,11 @@ mutual
   checkType' ctx (BOX q ty _) u = checkType ctx ty u
   checkType' ctx t@(Box {}) u = throw $ NotType t.loc ctx t
 
+  checkType' ctx (Let qty rhs body loc) u = do
+    expectEqualQ loc qty Zero
+    ety <- inferC ctx SZero rhs
+    checkType (extendTy Zero body.name ety.type ctx) body.term u
+
   checkType' ctx (E e) u = do
     -- if Ψ | Γ ⊢₀ E ⇒ Type ℓ
     infres <- inferC ctx SZero e

lib/Quox/Untyped/Erase.idr

@@ -222,6 +222,25 @@ eraseTerm ctx ty (Box val loc) = do
     Erased => pure $ Erased loc
     Kept   => eraseTerm ctx a val
 
+--         s ⤋ s' ⇐ A
+-- ----------------------------
+--   let0 x = e in s ⤋ s' ⇐ A
+--
+--     e ⤋ e'  s ⤋ s' ⇐ A   π ≠ 0
+-- -------------------------------------
+--  letπ x = e in s ⤋ let x = e' in s'
+eraseTerm ctx ty (Let pi e s loc) = do
+  let x = s.name
+  case isErased pi of
+    Erased => do
+      ety <- computeElimType ctx SZero e
+      s'  <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
+      pure $ sub1 (Erased e.loc) s'
+    Kept => do
+      EraRes ety e' <- eraseElim ctx e
+      s' <- eraseTerm (extendTy pi x ety ctx) (weakT 1 ty) s.term
+      pure $ Let x e' s' loc
+
 --  e ⤋ e' ⇒ B
 -- ------------
 --  e ⤋ e' ⇐ A

lib/Quox/Untyped/Syntax.idr

@@ -96,11 +96,6 @@ public export
 Definitions = SortedMap Name Definition
 
 
-export
-letD, inD : {opts : LayoutOpts} -> Eff Pretty (Doc opts)
-letD = hl Syntax "let"
-inD  = hl Syntax "in"
-
 export covering
 prettyTerm : {opts : LayoutOpts} -> BContext n ->
              Term n -> Eff Pretty (Doc opts)

lib/Quox/Whnf/Interface.idr

@@ -135,6 +135,7 @@ isTyCon (STRING  {}) = True
 isTyCon (Str     {}) = False
 isTyCon (BOX     {}) = True
 isTyCon (Box     {}) = False
+isTyCon (Let     {}) = False
 isTyCon (E       {}) = False
 isTyCon (CloT    {}) = False
 isTyCon (DCloT   {}) = False
@@ -182,6 +183,7 @@ canPushCoe sg (STRING  {}) _         = True
 canPushCoe sg (Str     {}) _         = False
 canPushCoe sg (BOX     {}) _         = True
 canPushCoe sg (Box     {}) _         = False
+canPushCoe sg (Let     {}) _         = False
 canPushCoe sg (E       {}) _         = False
 canPushCoe sg (CloT    {}) _         = False
 canPushCoe sg (DCloT   {}) _         = False
@@ -243,10 +245,12 @@ mutual
   |||    (the annotation is redundant in a checkable context)
   ||| 3. a closure
   ||| 4. `succ` applied to a natural constant
+  ||| 5. a `let` expression
   public export
   isRedexT : RedexTest Term
   isRedexT _    _  (CloT  {})  = True
   isRedexT _    _  (DCloT {})  = True
+  isRedexT _    _  (Let   {})  = True
   isRedexT defs sg (E {e, _})  = isAnn e || isRedexE defs sg e
   isRedexT _    _  (Succ p {}) = isNatConst p
   isRedexT _    _  _           = False

lib/Quox/Whnf/Main.idr

@@ -252,7 +252,10 @@ CanWhnf Term Interface.isRedexT where
       Left _ => case p of
         Nat p _               => pure $ nred $ Nat (S p) loc
         E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
-      Right nc => pure $ Element (Succ p loc) $ ?cc
+      Right nc => pure $ Element (Succ p loc) nc
+
+  whnf defs ctx sg (Let _ rhs body _) =
+    whnf defs ctx sg $ sub1 body rhs
 
   -- s ∷ A ⇝ s   (in term context)
   whnf defs ctx sg (E e) = do