LoadFile does the parsing

lib/Quox/Parser/FromParser.idr

@@ -19,6 +19,7 @@ import System.File
 import System.Path
 import Data.IORef
 
+
 %hide Typing.Error
 %hide Lexer.Error
 %hide Parser.Error
@@ -63,9 +64,9 @@ fromParserIO : (MonadRec io, HasIO io) =>
                IncludePath -> IORef SeenSet ->
                IORef NameSuf -> IORef Definitions ->
                Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act = liftIO $ fromIOErr $ do
+fromParserIO inc seen suf defs act =
-  runEff act $ with Union.(::)
+  liftIO $ fromIOErr $ runEff act $ with Union.(::)
-    [handleLoadFileIOE LoadError seen inc,
+    [handleLoadFileIOE LoadError WrapParseError seen inc,
      handleExcept (\e => ioLeft e),
      handleStateIORef defs,
      handleStateIORef !(newIORef [<]),
@@ -392,9 +393,7 @@ mutual
   loadProcessFile : Loc -> String -> Eff FromParserIO (List NDefinition)
   loadProcessFile loc file =
     case !(loadFile loc file) of
-      Just inp => do
+      Just tl => concat <$> traverse fromPTopLevel tl
-        tl <- either (throw . WrapParseError file) pure $ lexParseInput file inp
-        concat <$> traverse fromPTopLevel tl
       Nothing => pure []
 
   ||| populates the `defs` field of the state

lib/Quox/Parser/LoadFile.idr

@@ -1,5 +1,7 @@
 module Quox.Parser.LoadFile
 
+import public Quox.Parser.Syntax
+import Quox.Parser.Parser
 import Quox.Loc
 import Quox.EffExtra
 import Data.IORef
@@ -20,7 +22,7 @@ data LoadFileL : (lbl : k) -> Type -> Type where
   [search lbl]
   Seen    : FilePath -> LoadFileL lbl Bool
   SetSeen : FilePath -> LoadFileL lbl ()
-  DoLoad  : Loc -> FilePath -> LoadFileL lbl String
+  DoLoad  : Loc -> FilePath -> LoadFileL lbl PFile
 
 public export
 LoadFile : Type -> Type
@@ -47,11 +49,11 @@ setSeen = setSeenAt ()
 
 export
 doLoadAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
-           Loc -> FilePath -> Eff fs String
+           Loc -> FilePath -> Eff fs PFile
 doLoadAt lbl loc file = send $ DoLoad {lbl} loc file
 
 export %inline
-doLoad : Has LoadFile fs => Loc -> FilePath -> Eff fs String
+doLoad : Has LoadFile fs => Loc -> FilePath -> Eff fs PFile
 doLoad = doLoadAt ()
 
 
@@ -63,10 +65,6 @@ public export
 IncludePath : Type
 IncludePath = List String
 
-public export
-ErrorWrapper : Type -> Type
-ErrorWrapper e = Loc -> FilePath -> FileError -> e
-
 export covering
 readFileFrom : HasIO io => IncludePath -> FilePath ->
                io (Either FileError String)
@@ -76,23 +74,27 @@ readFileFrom inc f =
     Nothing   => pure $ Left $ FileNotFound
 
 export covering
-handleLoadFileIOE : ErrorWrapper e ->
+handleLoadFileIOE : (Loc -> FilePath -> FileError -> e) ->
+                    (FilePath -> Parser.Error -> e) ->
                     IORef SeenSet -> IncludePath ->
                     LoadFileL lbl a -> IOErr e a
-handleLoadFileIOE inj seen inc = \case
+handleLoadFileIOE injf injp seen inc = \case
   Seen    f   => contains f <$> readIORef seen
   SetSeen f   => modifyIORef seen $ insert f
-  DoLoad  l f => readFileFrom inc f >>= either (ioLeft . inj l f) pure
+  DoLoad  l f =>
+    case !(readFileFrom inc f) of
+      Left  err => ioLeft $ injf l f err
+      Right str => either (ioLeft . injp f) pure $ lexParseInput f str
 
 
 export
 loadFileAt : (0 lbl : k) -> Has (LoadFileL lbl) fs =>
-             Loc -> FilePath -> Eff fs (Maybe String)
+             Loc -> FilePath -> Eff fs (Maybe PFile)
 loadFileAt lbl loc file =
   if !(seenAt lbl file)
      then pure Nothing
      else Just <$> doLoadAt lbl loc file <* setSeenAt lbl file
 
 export
-loadFile : Has LoadFile fs => Loc -> FilePath -> Eff fs (Maybe String)
+loadFile : Has LoadFile fs => Loc -> FilePath -> Eff fs (Maybe PFile)
 loadFile = loadFileAt ()

lib/Quox/Parser/Parser.idr

@@ -641,7 +641,7 @@ topLevel : FileName -> Grammar True PTopLevel
 topLevel fname = load fname <|> [|PD $ decl fname|]
 
 export
-input : FileName -> Grammar False (List PTopLevel)
+input : FileName -> Grammar False PFile
 input fname = [] <$ eof
           <|> [|(topLevel fname <* commit) :: assert_total input fname|]
 
@@ -650,5 +650,5 @@ lexParseTerm : FileName -> String -> Either Error PTerm
 lexParseTerm = lexParseWith . term
 
 export
-lexParseInput : FileName -> String -> Either Error (List PTopLevel)
+lexParseInput : FileName -> String -> Either Error PFile
 lexParseInput = lexParseWith . input

lib/Quox/Parser/Syntax.idr

@@ -208,3 +208,8 @@ public export
 fromNat : Nat -> Loc -> PTerm
 fromNat 0     loc = Zero loc
 fromNat (S k) loc = Succ (fromNat k loc) loc
+
+
+public export
+PFile : Type
+PFile = List PTopLevel