Add a primitive Let that is compiled to let in Haskell

lib/Haskell/Prim.agda

@@ -61,6 +61,9 @@ if_then_else_ : {@0 a : Set ℓ} → (flg : Bool) → (@0 {{ flg ≡ True }} →
 if False then x else y = y
 if True  then x else y = x
 
+Let : a → (a → b) → b
+Let x f = f x
+
 --------------------------------------------------
 -- Agda strings
 

src/Agda2Hs/Compile/Term.hs

@@ -44,6 +44,7 @@ isSpecialTerm q = case prettyShow q of
   "Haskell.Prim.Enum.Enum.enumFromThen"         -> Just mkEnumFromThen
   "Haskell.Prim.Enum.Enum.enumFromThenTo"       -> Just mkEnumFromThenTo
   "Haskell.Prim.case_of_"                       -> Just caseOf
+  "Haskell.Prim.Let"                            -> Just hsLet
   "Haskell.Prim.Monad.Do.Monad._>>=_"           -> Just bind
   "Haskell.Prim.Monad.Do.Monad._>>_"            -> Just sequ
   "Agda.Builtin.FromNat.Number.fromNat"         -> Just fromNat
@@ -172,6 +173,12 @@ caseOf _ es = compileElims es >>= \case
   -- applied to non-lambda / partially applied
   _ -> genericError $ "case_of_ must be fully applied to a lambda"
 
+hsLet :: QName -> Elims -> C (Hs.Exp ())
+hsLet _ es = compileElims es >>= \case
+  v : (Hs.Lambda _ [Hs.PVar () p] body) : [] -> do
+    return $ Hs.Let () (Hs.BDecls () [Hs.FunBind () [Hs.Match () p [] (Hs.UnGuardedRhs () v) Nothing]]) body
+  _ -> genericError $ "Let must be fully applied to a lambda"
+
 lambdaCase :: QName -> Elims -> C (Hs.Exp ())
 lambdaCase q es = setCurrentRangeQ q $ do
   Function{funClauses = cls, funExtLam = Just ExtLamInfo {extLamModule = mname}}