Add quotation to help metaprogramming.

1 files changed, 162 insertions, 115 deletions

diff --git a/src/Inky.idr b/src/Inky.idr
index ad3a503..3f6b755 100644
--- a/src/Inky.idr
+++ b/src/Inky.idr
@@ -6,6 +6,8 @@ import Control.App
 import Control.App.Console
 import Control.App.FileIO
 
+import Data.String
+
 import Flap.Decidable
 import Flap.Decidable.Maybe
 import Flap.Parser
@@ -35,45 +37,110 @@ record Erased (a : Type) where
   constructor Forget
   0 value : a
 
+record SynthFailed where
+  constructor UhOh
+  term : Term NoSugar Bounds [<] [<]
+  err : NotSynths {m = Bounds} [<] [<] term
+
+Err : Type
+Err = List1 (WithBounds String)
+
+Interpolation Bounds where
+  interpolate b =
+    "\{show (1 + b.startLine)}:\{show (1 + b.startCol)}--\{show (1 + b.endLine)}:\{show (1 + b.endCol)}"
+
+Interpolation a => Interpolation (WithBounds a) where
+  interpolate x =
+    if x.isIrrelevant
+    then "?:?--?:?: \{x.val}"
+    else "\{x.bounds}: \{x.val}"
+
 -- Actions ---------------------------------------------------------------------
 
-lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken))
+readFile : FileIO es => File -> App es String
+readFile f = do
+  content <- read [<] f
+  pure (fastConcat $ content <>> [])
+  where
+  read : SnocList String -> File -> App es (SnocList String)
+  read acc f = do
+    False <- fEOF f
+      | True => pure acc
+    str <- fGetStr f
+    read (acc :< str) f
+
+readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
+readFileOrStdin Nothing = readFile stdin
+readFileOrStdin (Just path) = withFile path Read throw readFile
+
+lexInkyString : HasErr (WithBounds String) es => String -> App es (List (WithBounds InkyToken))
 lexInkyString file = do
   let (tokens, _, _, "") = lex tokenMap file
-    | (_, line, col, rest) => throw "\{show (1 + line)}:\{show col}: unexpected character"
+    | (_, line, col, rest) => 
+      throw (MkBounded "unexpected character" False (MkBounds line col line col))
   pure (filter (\x => relevant x.val.kind) tokens)
 
-parseType : HasErr String es => List (WithBounds InkyToken) -> App es (Ty [<])
-parseType toks = do
-  let Ok res [] _ = parse @{EqI} OpenType toks
-    | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
-    | Err msg => throw msg
-  let Right a = res.try [<]
-    | Left msg => throw msg
+Interpolation (List InkyKind) where
+  interpolate [t] = interpolate t
+  interpolate ts = "one of " ++ joinBy ", " (map interpolate ts)
+
+doParse :
+  HasErr (WithBounds String) es =>
+  (p : InkyParser False [<] [<] a) ->
+  {auto 0 wf : collectTypeErrs @{ListSet} [<] [<] [<] [<] p = []} ->
+  List (WithBounds InkyToken) ->
+  App es a
+doParse p toks =
+  case parse @{ListSet} p toks of
+    Ok res [] _ => pure res
+    Ok res (x :: _) _ =>
+      throw ("expected end of input; got token \{x.val.kind}" <$ x)
+    Err err => throw (parseErrToString err)
+  where
+  parseErrToString : ParseErr InkyKind -> WithBounds String
+  parseErrToString (BadEOF ts) =
+    irrelevantBounds "expected \{ts}; got end of input"
+  parseErrToString (Unexpected ts got) =
+    "expected \{ts}; got token \{got.val.kind}" <$ got
+
+parseType :
+  Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
+  Maybe FilePath -> App es (Ty [<])
+parseType path = do
+  txt <- readFileOrStdin path
+  toks <- lexInkyString txt
+  res <- doParse OpenType toks
+  let Ok a = res.try [<]
+    | Errs errs => throw errs
   pure a
 
-parseTerm : HasErr String es => List (WithBounds InkyToken) -> App es (Term Sugar Bounds [<] [<])
-parseTerm toks = do
-  let Ok res [] _ = parse @{EqI} OpenTerm toks
-    | Ok res (x :: _) _ => throw "\{x.bounds}: unexpected token \{x.val.kind}, expected end of input"
-    | Err msg => throw msg
-  let Right t = res.try [<] [<]
-    | Left msg => throw msg
-  pure t
+parseTerm :
+  Has [HasErr (WithBounds String), HasErr Err, HasErr IOError, FileIO] es =>
+  (termPath, tyPath : Maybe FilePath) -> App es (Term (Sugar [<]) Bounds [<] [<])
+parseTerm termPath tyPath = do
+  txt <- readFileOrStdin termPath
+  toks <- lexInkyString txt
+  res <- doParse OpenTerm toks
+  let Ok t = res.try (Sugar [<]) [<] [<]
+    | Errs errs => throw errs
+  -- Annotate with type
+  let Just _ = tyPath
+    | Nothing => pure t
+  a <- parseType tyPath
+  pure (Annot (MkBounds 0 0 0 0) t a)
 
-checkType : HasErr String es => (a : Ty [<]) -> App es (Erased $ WellFormed a)
-checkType a = do
-  let True `Because` wf = wellFormed a
-    | False `Because` bad => throw "type ill-formed"
-  pure (Forget wf)
+checkType : HasErr String es => (a : Ty [<]) -> App es ()
+checkType a =
+  unless (wellFormed a).does $
+    throw "type ill-formed"
 
 synthTerm :
-  (t : Term mode m [<] [<]) ->
-  HasErr (NotSynths [<] [<] t) es =>
+  (t : Term NoSugar Bounds [<] [<]) ->
+  HasErr SynthFailed es =>
   App es (Subset (Ty [<]) (Synths [<] [<] t))
 synthTerm t = do
   let Just a `Because` prf = synths [<] [<] t
-    | Nothing `Because` contra => throw contra
+    | Nothing `Because` contra => throw (UhOh t contra)
   pure (Element a prf)
 
 printType :
@@ -84,23 +151,13 @@ printType a = do
 
 printTerm :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  Term mode m [<] [<] -> App es ()
+  {mode : Term.Mode} -> Term mode m [<] [<] -> App es ()
 printTerm a = do
   primIO $ renderIO $ layoutSmart opts $ prettyTerm a Open
 
-printSynthError :
-  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {t : Term mode Bounds [<] [<]} ->
-  NotSynths [<] [<] t -> App es ()
-printSynthError contra =
-  primIO $ renderIO $ layoutSmart opts $
-  concatWith (surround hardline) $
-  map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
-  prettyNotSynths contra
-
 compileTerm :
   PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
-  {t : Term mode m [<] [<]} ->
+  {t : Term NoSugar m [<] [<]} ->
   (0 prf : Synths [<] [<] t a) ->
   App es ()
 compileTerm prf =
@@ -108,22 +165,6 @@ compileTerm prf =
   pretty "(use-modules (ice-9 match))" <+> line <+>
   parens (hang 1 $ pretty "define main" <+> line <+> group (compileSynths [<] [<] prf))
 
-readFile : FileIO es => File -> App es String
-readFile f = do
-  content <- read [<] f
-  pure (fastConcat $ content <>> [])
-  where
-  read : SnocList String -> File -> App es (SnocList String)
-  read acc f = do
-    False <- fEOF f
-      | True => pure acc
-    str <- fGetStr f
-    read (acc :< str) f
-
-readFileOrStdin : FileIO es => HasErr IOError es => Maybe FilePath -> App es String
-readFileOrStdin Nothing = readFile stdin
-readFileOrStdin (Just path) = withFile path Read throw readFile
-
 
 -- Arguments -------------------------------------------------------------------
 
@@ -188,27 +229,25 @@ Inky = MkCommand
 
 -- Driver ----------------------------------------------------------------------
 
-parseArgs :
-  (cmd : Command nm) ->
-  App (String :: Init) (ParseTree cmd)
-parseArgs cmd = do
-  Right args <- primIO cmd.parseArgs
-    | Left msg => throw msg
-  let Pure args = ParsedTree.finalising args
-    | Fail errs => throw (show $ the (Error ()) $ Fail errs)
-  pure args
-
-abortErr : PrimIO es => String -> App es a
-abortErr msg = do
-  primIO $ () <$ fPutStrLn stderr msg
-  primIO exitFailure
-
 showHelp : Console es => App es ()
 showHelp = putStrLn "Usage: \{Inky .usage}"
 
-main : IO ()
-main = run {l = MayThrow} $ do
-  args <- handle {err = String} (parseArgs Inky) pure abortErr
+process :
+  Has
+    [ HasErr String
+    , HasErr (WithBounds String)
+    , HasErr (List1 $ WithBounds String)
+    , HasErr (List1 ErrorMsg)
+    , HasErr SynthFailed
+    , FileIO
+    , PrimIO
+    ] es =>
+  App es ()
+process = do
+  Right args <- primIO (Inky).parseArgs
+    | Left msg => throw msg
+  let Pure args = ParsedTree.finalising args
+    | Fail errs => throw errs
   Collie.handle {cmd = ("inky" ** Inky)} args
     [ const showHelp
     , "--help" ::= [ const showHelp ]
@@ -217,24 +256,16 @@ main = run {l = MayThrow} $ do
       , "type" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          a <- handle {err = String} (parseType toks) pure abortErr
+          a <- parseType path
           printType a
-          pure ()
         ]
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
+          t <- parseTerm path Nothing
           let [noSugar] = cmd.modifiers.content
           case noSugar of
-            True => do
-              let Just t = maybeDesugar t
-                | Nothing => abortErr "failed to desugar term"
-              printTerm t
+            True => printTerm (desugar t)
             False => printTerm t
         ]
       ]
@@ -243,29 +274,18 @@ main = run {l = MayThrow} $ do
       , "type" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          a <- handle {err = String} (parseType toks) pure abortErr
-          handle {err = String} (checkType a) (const $ pure ()) abortErr
+          a <- parseType path
+          _ <- checkType a
+          pure ()
         ]
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          t <-
-            maybe (pure t)
-              (\path => do
-                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
-                toks <- handle {err = String} (lexInkyString txt) pure abortErr
-                a <- handle {err = String} (parseType toks) pure abortErr
-                handle {err = String} (checkType a) (const $ pure ()) abortErr
-                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
-              type
-          handle {err = NotSynths [<] [<] t} (synthTerm t) (const $ pure ())
-            (\contra => do printSynthError contra; primIO exitFailure)
+          t <- parseTerm path type
+          let t = desugar t
+          _ <- synthTerm t
+          pure ()
         ]
       ]
     , "compile" ::=
@@ -273,23 +293,50 @@ main = run {l = MayThrow} $ do
       , "term" ::=
         [ \cmd => do
           let path = cmd.arguments
-          txt <- handle {err = IOError} (readFileOrStdin path) pure (abortErr . show)
-          toks <- handle {err = String} (lexInkyString txt) pure abortErr
-          t <- handle {err = String} (parseTerm toks) pure abortErr
           let [type] = cmd.modifiers.content
-          t <-
-            maybe (pure t)
-              (\path => do
-                txt <- handle {err = IOError} (readFileOrStdin $ Just path) pure (abortErr . show)
-                toks <- handle {err = String} (lexInkyString txt) pure abortErr
-                a <- handle {err = String} (parseType toks) pure abortErr
-                handle {err = String} (checkType a) (const $ pure ()) abortErr
-                pure (Annot (MkBounds (-1) (-1) (-1) (-1)) t a))
-              type
-          Element _ prf <-
-            handle {err = NotSynths [<] [<] t} (synthTerm t) pure
-              (\contra => do printSynthError contra; primIO exitFailure)
+          t <- parseTerm path type
+          let t = desugar t
+          Element _ prf <- synthTerm t
           compileTerm prf
         ]
       ]
     ]
+
+handleErr : (0 e : Type) -> (forall a. e -> App es a) -> App (e :: es) a -> App es a
+handleErr e handler app = handle app pure handler
+
+printSynthFailed :
+  PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} ->
+  SynthFailed -> App es ()
+printSynthFailed (UhOh t err) =
+  primIO $ renderIO $ layoutSmart opts $
+  concatWith (surround hardline) $
+  map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $
+  prettyNotSynths err
+
+main : IO ()
+main =
+  run {l = MayThrow} $
+  handleErr (List String)
+    (\msgs => do
+      foldlM (\_, msg => primIO $ () <$ fPutStrLn stderr msg) () msgs
+      primIO exitFailure) $
+  handleErr String
+    (throw . List.singleton) $
+  handleErr (List1 ErrorMsg)
+    (throw . map show . forget) $
+  handleErr (List1 $ WithBounds String)
+    (throw . map interpolate . forget) $
+  handleErr (WithBounds String)
+    (throw . (::: [])) $
+  handleErr IOError
+    (throw . show) $
+  handleErr SynthFailed
+    (\err => do
+      printSynthFailed err
+      primIO exitFailure) $
+  process
+
+-- main =
+--   run {l = MayThrow} $
+--   handle