diff options
Diffstat (limited to 'src/Inky.idr')
| -rw-r--r-- | src/Inky.idr | 277 |
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 |