diff --git a/TODO.md b/TODO.md index fcaed6a..525d202 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,7 @@ ## TODO -- [ ] redo code to determine base path +- [x] redo code to determine base path - [ ] save/load results of processing a module - [ ] keep each module separate in context - search would include imported modules, collect ops into and from modules diff --git a/port/Lib/Util.newt b/port/Lib/Util.newt index 51ffc22..ef99172 100644 --- a/port/Lib/Util.newt +++ b/port/Lib/Util.newt @@ -1,6 +1,7 @@ module Lib.Util import Lib.Types +import Data.List1 funArgs : Tm -> (Tm × List Tm) @@ -24,3 +25,28 @@ splitTele = go Nil go : List Binder -> Tm -> (Tm × List Binder) go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u go ts tm = (tm, reverse ts) + + + +getBaseDir : String → String → M (String × QName) +getBaseDir fn modName = do + let (path, modName') = unsnoc $ split1 modName "." + let parts = split1 fn "/" + let (dirs,file) = unsnoc parts + let (name, ext) = splitFileName file + + let parts = split1 fn "/" + let (dirs,file) = unsnoc parts + let (path, modName') = unsnoc $ split1 modName "." + unless (modName' == name) $ \ _ => error (MkFC fn (0,0)) "module name \{modName'} doesn't match \{name}" + let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path) + | Left err => error (MkFC fn (0,0)) err + let base = if base == "" then "." else base + pure (base, QN path modName') + where + baseDir : SnocList String -> SnocList String -> Either String String + baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil) + baseDir (dirs :< d) (ns :< n) = if d == n + then baseDir dirs ns + else Left "module path doesn't match directory" + baseDir Lin _ = Left "module path doesn't match directory" diff --git a/port/Main.newt b/port/Main.newt index c8f4e4a..870add7 100644 --- a/port/Main.newt +++ b/port/Main.newt @@ -165,14 +165,15 @@ processFile fn = do let dir = if dirs == Nil then "." else joinBy "/" dirs let (name, ext) = splitFileName file putStrLn "\{show dir} \{show name} \{show ext}" + (Right src) <- liftIO {M} $ readFile fn | Left err => error (MkFC fn (0,0)) "error reading \{fn}: \{show err}" let (Right toks) = tokenise fn src | Left err => throwError err let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader EmptyMap toks | Left (err,toks) => throwError err - let ns = split modName "." - let (path, modName') = unsnoc $ split1 modName "." + + (base,qn) <- getBaseDir fn modName -- Any case splits after this point causes it to loop, no idea why @@ -186,9 +187,8 @@ processFile fn = do processDecl ("Prim" :: Nil) (PType emptyFC "Int" Nothing) processDecl ("Prim" :: Nil) (PType emptyFC "String" Nothing) processDecl ("Prim" :: Nil) (PType emptyFC "Char" Nothing) - -- let base = "aoc2024" -- FIXME - let base = "port" -- FIXME - src <- processModule emptyFC base Nil (QN path modName') + + src <- processModule emptyFC base Nil qn top <- get -- -- dumpContext top