diff options
Diffstat (limited to 'src/Inky.idr')
| -rw-r--r-- | src/Inky.idr | 81 |
1 files changed, 71 insertions, 10 deletions
diff --git a/src/Inky.idr b/src/Inky.idr index 649c620..66124c6 100644 --- a/src/Inky.idr +++ b/src/Inky.idr @@ -6,11 +6,13 @@ import Control.App import Control.App.Console import Control.App.FileIO -import Inky.Decidable -import Inky.Decidable.Maybe -import Inky.Parser +import Flap.Decidable +import Flap.Decidable.Maybe +import Flap.Parser + import Inky.Term import Inky.Term.Checks +import Inky.Term.Compile import Inky.Term.Desugar import Inky.Term.Parser import Inky.Term.Pretty @@ -29,6 +31,10 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal %hide Collie.Modifiers.infix.(::=) +record Erased (a : Type) where + constructor Forget + 0 value : a + -- Actions --------------------------------------------------------------------- lexInkyString : HasErr String es => String -> App es (List (WithBounds InkyToken)) @@ -55,17 +61,20 @@ parseTerm toks = do | Left msg => throw msg pure t -checkType : HasErr String es => Ty [<] -> App es () +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 () + pure (Forget wf) -checkTerm : (a : Ty [<]) -> (t : Term mode m [<] [<]) -> HasErr (NotChecks [<] [<] a t) es => App es () +checkTerm : + (a : Ty [<]) -> (t : Term mode m [<] [<]) -> + HasErr (NotChecks [<] [<] a t) es => + App es (Erased $ Checks [<] [<] a t) checkTerm a t = do let True `Because` prf = checks [<] [<] a t | False `Because` contra => throw contra - pure () + pure (Forget prf) printType : PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> @@ -89,6 +98,18 @@ printCheckError contra = map (\(bounds, msg) => group $ align $ hang 2 $ pretty "\{bounds}:" <+> line <+> msg) $ prettyNotChecks contra +compileTerm : + PrimIO es => {default defaultLayoutOptions opts : LayoutOptions} -> + {a : Ty [<]} -> + {t : Term mode m [<] [<]} -> + (0 wf : WellFormed a) -> + (0 prf : Checks [<] [<] a t) -> + App es () +compileTerm wf prf = + primIO $ renderIO $ layoutSmart opts $ + pretty "(use-modules (ice-9 match))" <+> line <+> + parens (hang 1 $ pretty "define main" <+> line <+> group (compileChecks [<] [<] wf prf)) + readFile : FileIO es => File -> App es String readFile f = do content <- read [<] f @@ -147,6 +168,21 @@ Inky = MkCommand , modifiers = [] , arguments = none } + , "compile" ::= MkCommand + { description = """ + compile to scheme + """ + , subcommands = + [ "term" ::= MkCommand + { description = "compile a term" + , subcommands = [] + , modifiers = ["--type" ::= option "type to check against" filePath] + , arguments = filePath + } + ] + , modifiers = [] + , arguments = none + } ] , modifiers = [] , arguments = none @@ -212,7 +248,7 @@ main = run {l = MayThrow} $ do 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) pure abortErr + handle {err = String} (checkType a) (const $ pure ()) abortErr ] , "term" ::= [ \cmd => do @@ -227,11 +263,36 @@ main = run {l = MayThrow} $ 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) pure abortErr + handle {err = String} (checkType a) (const $ pure ()) abortErr pure a) type - handle {err = NotChecks [<] [<] a t} (checkTerm a t) pure + handle {err = NotChecks [<] [<] a t} (checkTerm a t) (const $ pure ()) (\contra => do printCheckError contra; primIO exitFailure) ] ] + , "compile" ::= + [ const showHelp + , "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 + Element a wf <- + the (App _ (Subset (Ty [<]) WellFormed)) $ + maybe (pure (Element (TArrow TNat TNat) %search)) + (\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 + Forget wf <- handle {err = String} (checkType a) pure abortErr + pure (Element a wf)) + type + Forget prf <- + handle {err = NotChecks [<] [<] a t} (checkTerm a t) pure + (\contra => do printCheckError contra; primIO exitFailure) + compileTerm wf prf + ] + ] ] |