0 | module Yaffle.Main
 1 |
 2 | import Compiler.Common
 3 | import Core.Binary
 4 | import Core.Directory
 5 | import Core.InitPrimitives
 6 | import Core.Metadata
 7 | import Core.UnifyState
 8 | import Libraries.Utils.Path
 9 |
10 | import Idris.REPL.Opts
11 | import Idris.Syntax
12 |
13 | import TTImp.ProcessDecls
14 |
15 | import Yaffle.REPL
16 |
17 | import System
18 |
19 | %default covering
20 |
21 | usage : String
22 | usage = "Usage: yaffle <input file> [--timing]"
23 |
24 | processArgs : List String -> Core (Maybe Nat)
25 | processArgs [] = pure Nothing
26 | processArgs ["--timing"] = pure (Just 10)
27 | processArgs _
28 |     = coreLift $ do ignore $ putStrLn usage
29 |                     exitWith (ExitFailure 1)
30 |
31 | HasNames () where
32 |   full _ _ = pure ()
33 |   resolved _ _ = pure ()
34 |
35 | export
36 | yaffleMain : String -> List String -> Core ()
37 | yaffleMain sourceFileName args
38 |     = do defs <- initDefs
39 |          c <- newRef Ctxt defs
40 |          t <- processArgs args
41 |          modIdent <- ctxtPathToNS sourceFileName
42 |          m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))
43 |          u <- newRef UST initUState
44 |          s <- newRef Syn initSyntax
45 |          o <- newRef ROpts (defaultOpts (Just sourceFileName) (REPL ErrorLvl) [])
46 |          whenJust t $ setLogTimings
47 |          addPrimitives
48 |          case extension sourceFileName of
49 |               Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC"
50 |                                ignore $ readFromTTC {extra = ()} True emptyFC True sourceFileName (nsAsModuleIdent emptyNS) emptyNS
51 |                                coreLift_ $ putStrLn "Read TTC"
52 |               _ => do coreLift_ $ putStrLn "Processing as TTImp"
53 |                       ok <- processTTImpFile sourceFileName
54 |                       when ok $
55 |                          do makeBuildDirectory modIdent
56 |                             ttcFileName <- getTTCFileName sourceFileName "ttc"
57 |                             writeToTTC () sourceFileName ttcFileName
58 |                             coreLift_ $ putStrLn "Written TTC"
59 |          repl {c} {u} {s} {o}
60 |
61 | ymain : IO ()
62 | ymain
63 |     = do (_ :: fname :: rest) <- getArgs
64 |              | _ => do putStrLn usage
65 |                        exitWith (ExitFailure 1)
66 |          coreRun (yaffleMain fname rest)
67 |                (\err : Error => putStrLn ("Uncaught error: " ++ show err))
68 |                (\res => pure ())
69 |