[ elab ] Implement resugaring primitive for elaborator scripts

Author: buzden

CHANGELOG_NEXT.md

@@ -85,6 +85,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
   `parameters {0 t : Type} (v : t)` to indicate if arguments are implicit or
   erased.
 
+* Elaborator scripts were made to be able to get pretty-printed resugared expressions.
+
 ### Compiler changes
 
 * The compiler now differentiates between "package search path" and "package

libs/base/Language/Reflection.idr

@@ -60,6 +60,8 @@ data Elab : Type -> Type where
      ||| * term
      LogSugaredTerm : String -> Nat -> String -> TTImp -> Elab ()
 
+     ResugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> Elab String
+
      -- Elaborate a TTImp term to a concrete value
      Check : TTImp -> Elab expected
      -- Quote a concrete expression back to a TTImp
@@ -149,6 +151,9 @@ interface Monad m => Elaboration m where
   ||| Write a log message and a resugared & rendered term, if the log level is >= the given level
   logSugaredTerm : String -> Nat -> String -> TTImp -> m ()
 
+  ||| Resugar given term to a pretty string
+  resugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> m String
+
   ||| Check that some TTImp syntax has the expected type
   ||| Returns the type checked value
   check : TTImp -> m expected
@@ -233,6 +238,7 @@ Elaboration Elab where
   logMsg         = LogMsg
   logTerm        = LogTerm
   logSugaredTerm = LogSugaredTerm
+  resugarTerm    = ResugarTerm
   check          = Check
   quote          = Quote
   lambda         = Lambda
@@ -260,6 +266,7 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
   logMsg s            = lift .: logMsg s
   logTerm s n         = lift .: logTerm s n
   logSugaredTerm s n  = lift .: logSugaredTerm s n
+  resugarTerm         = lift .: resugarTerm
   check               = lift . check
   quote v             = lift $ quote v
   lambda x            = lift . lambda x

src/Idris/Pretty/Render.idr

@@ -23,19 +23,22 @@ getPageWidth = do
     Just 0 => pure $ Unbounded
     Just cw => pure $ AvailablePerLine (cast cw) 1
 
+export
+render' : PageWidth ->
+          Maybe (ann -> AnsiStyle) ->
+          Doc ann -> String
+render' pageWidth stylerAnn doc = do
+  let opts = MkLayoutOptions pageWidth
+  let layout = layoutPretty opts doc
+  renderString $ case stylerAnn of
+    Just stylerAnn => reAnnotateS stylerAnn layout
+    Nothing => unAnnotateS layout
+
 export
 render : {auto o : Ref ROpts REPLOpts} ->
          (ann -> AnsiStyle) ->
          Doc ann -> Core String
-render stylerAnn doc = do
-  color <- getColor
-  pageWidth <- getPageWidth
-  let opts = MkLayoutOptions pageWidth
-  let layout = layoutPretty opts doc
-  pure $ renderString $
-    if color
-      then reAnnotateS stylerAnn layout
-      else unAnnotateS layout
+render stylerAnn doc = pure $ render' !getPageWidth (toMaybe !getColor stylerAnn) doc
 
 export
 renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc ann -> Core String

src/TTImp/Elab/RunElab.idr

@@ -15,10 +15,12 @@ import Core.Value
 
 import Idris.Resugar
 import Idris.REPL.Opts
+import Idris.Pretty
 import Idris.Syntax
 
 import Libraries.Data.NameMap
 import Libraries.Data.WithDefault
+import Libraries.Text.PrettyPrint.Prettyprinter.Doc -- for PageWidth
 import Libraries.Utils.Path
 
 import TTImp.Elab.Check
@@ -228,6 +230,12 @@ elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp
                      ptm <- pterm (map defaultKindedName tm')
                      pure $ !(reify defs str') ++ ": " ++ show ptm
              scriptRet ()
+    elabCon defs "ResugarTerm" [maxLineWidth, tm]
+        = do ptm <- pterm . map defaultKindedName =<< reify defs !(evalClosure defs tm)
+             mlw <- reify defs !(evalClosure defs maxLineWidth)
+             let _ : Maybe Nat = mlw
+             let pw = maybe Unbounded (\w => AvailablePerLine (cast w) 1) mlw
+             scriptRet $ render' pw Nothing $ pretty {ann=IdrisSyntax} ptm
     elabCon defs "Check" [exp, ttimp]
         = do exp' <- evalClosure defs exp
              ttimp' <- evalClosure defs ttimp

tests/idris2/reflection/reflection034/ResugarTerm.idr

@@ -0,0 +1,37 @@
+import Language.Reflection
+
+%language ElabReflection
+
+e1 : TTImp
+e1 = `(let x = 5 in x + 2)
+
+p1 : String
+p1 = %runElab resugarTerm (Just 20) e1
+
+p2 : String
+p2 = %runElab resugarTerm Nothing e1
+
+e2 : TTImp
+e2 = `(
+  do x <- case y of
+            Nice => pure $ nicest
+            Just x => x <*> foo "ha"
+     let f : Nat -> Nat; f = S . S . S . S . S . S . S . S . S . S
+     Z <- f 16
+       | S n => 18
+     f 2
+  )
+
+p3 : String
+p3 = %runElab resugarTerm (Just 20) e2
+
+p4 : String
+p4 = %runElab resugarTerm Nothing e2
+
+main : IO ()
+main = traverse_ (\(n, e) => do putStrLn "\n--------\n\{n}:"; putStrLn e)
+  [ ("p1", p1)
+  , ("p2", p2)
+  , ("p3", p3)
+  , ("p4", p4)
+  ]

tests/idris2/reflection/reflection034/expected

@@ -0,0 +1,28 @@
+1/1: Building ResugarTerm (ResugarTerm.idr)
+
+--------
+p1:
+let x =
+      fromInteger 5
+in x + fromInteger 2
+
+--------
+p2:
+let x = fromInteger 5 in x + fromInteger 2
+
+--------
+p3:
+(case y of
+  { Nice => pure nicest
+  ; Just x => x <*> foo (fromString "ha")
+  }) >>= (\x =>
+let {<<definitions>>}
+in f (fromInteger 16) >>= (\_ =>
+case _ of
+  { Z => f (fromInteger 2)
+  ; S n => fromInteger 18
+  }))
+
+--------
+p4:
+(case y of { Nice => pure nicest ; Just x => x <*> foo (fromString "ha") }) >>= (\x => let {<<definitions>>} in f (fromInteger 16) >>= (\_ => case _ of { Z => f (fromInteger 2) ; S n => fromInteger 18 }))

tests/idris2/reflection/reflection034/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check ResugarTerm.idr
+run ResugarTerm.idr