fix importing with dots, prep work for porting

scripts/translate.sh

@@ -0,0 +1,32 @@
+#!/bin/zsh
+
+# script to translate a file from idris to newt
+# this is just a first pass, hopefully
+mkdir -p port
+
+find src -type f -name '*.idr' | while read -r file; do
+  output_file="port/${file#src/}"
+  output_file="${output_file%.idr}.newt"
+  mkdir -p "$(dirname "$output_file")"
+  if [[ ! -f "$output_file" ]]; then
+    echo "$file -> $output_file"
+    perl -pe '
+      s/^%.*//;
+      s/\bType\b/U/g;
+      s/\binterface\b/class/g;
+      s/import public/import/g;
+      s/^export//g;
+      s/^public export//g;
+      s/\(([A-Z]\w+), ?([^)]+)\)/(\1 × \2)/g;
+      s/\|\|\|/--/;
+      # maybe break down an add the sugar?
+      # patterns would be another option, but
+      # we would need to handle overlapping ones
+      s/\[\]/Nil/g;
+      s/\[<\]/Lin/g;
+      s/\[<([^\],]+)\]/(Lin :< \1)/g;
+      s/\[([^\],]+)\]/(\1 :: Nil)/g;
+      s/^([A-Z].*where)/instance \1/g;
+    ' "$file" > "$output_file"
+  fi
+done

src/Lib/CompileExp.idr

@@ -12,7 +12,6 @@ import Data.List
 import Lib.Types -- Name / Tm
 import Lib.TopContext
 import Lib.Prettier
-import Lib.Eval -- lookupMeta
 import Lib.Util
 
 public export

src/Lib/Parser.idr

@@ -389,7 +389,13 @@ parseSig : Parser Decl
 parseSig = TypeSig <$> getPos <*> try (some (ident <|> uident) <* keyword ":") <*> typeExpr
 
 parseImport : Parser Import
-parseImport = MkImport <$> getPos <* keyword "import" <*> uident
+parseImport = do
+  fc <- getPos
+  keyword "import"
+  ident <- uident
+  rest <- many $ token Projection
+  let name = joinBy "" (ident :: rest)
+  pure $ MkImport fc name
 
 -- Do we do pattern stuff now? or just name = lambda?
 -- TODO multiple names
@@ -523,7 +529,14 @@ parseDecl = parseMixfix <|> parsePType <|> parsePFunc
 
 export
 parseModHeader : Parser (FC, String)
-parseModHeader = sameLevel (keyword "module") >> withPos uident
+parseModHeader = do
+  sameLevel (keyword "module")
+  fc <- getPos
+  name <- uident
+  rest <- many $ token Projection
+  -- FIXME use QName
+  let name = joinBy "" (name :: rest)
+  pure (fc, name)
 
 export
 parseImports : Parser (List Import)
@@ -535,6 +548,9 @@ parseMod = do
   startBlock $ do
     keyword "module"
     name <- uident
+    rest <- many $ token Projection
+    -- FIXME use QName
+    let name = joinBy "" (name :: rest)
     imports <- manySame $ parseImport
     decls <- manySame $ parseDecl
     pure $ MkModule name imports decls

src/Lib/Token.idr

@@ -18,6 +18,7 @@ data Kind
   | Space
   | Comment
   | Pragma
+  | Projection
   -- not doing Layout.idr
   | LBrace
   | Semi
@@ -42,6 +43,7 @@ Show Kind where
   show Pragma  = "Pragma"
   show StringKind = "String"
   show JSLit = "JSLit"
+  show Projection = "Projection"
 
 export
 Eq Kind where
@@ -58,6 +60,7 @@ Eq Kind where
   RBrace  == RBrace = True
   StringKind == StringKind = True
   JSLit == JSLit = True
+  Projection == Projection = True
   _ == _ = False
 
 export

src/Lib/Tokenizer2.idr

@@ -15,7 +15,9 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do",
             "∀", "forall", "import", "uses",
             "class", "instance", "record", "constructor",
             "if", "then", "else",
-            "$", "λ", "?", "@",
+            -- it would be nice to find a way to unkeyword "." so it could be
+            -- used as an operator too
+            "$", "λ", "?", "@", ".",
              "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"]
 
 -- This makes a big case tree...
@@ -38,6 +40,7 @@ tokenise' sl sc toks chars = case chars of
   '/' :: '-' :: cs => blockComment sl (sc + 2) toks cs
   '`' :: cs => doBacktick sl (sc + 1) toks cs [<]
   '"' :: cs => doQuote sl (sc + 1) toks cs [<]
+  '.' :: cs => doRest sl (sc + 1) toks cs Projection isIdent (Lin :< '.')
   '-' :: c :: cs => if isDigit c
     then doRest sl (sc + 2) toks cs Number isDigit (Lin :< '-' :< c)
     else doRest sl (sc + 1) toks (c :: cs) Ident isIdent (Lin :< '-')
@@ -48,6 +51,9 @@ tokenise' sl sc toks chars = case chars of
     isIdent : Char -> Bool
     isIdent c = not (isSpace c || elem c standalone)
 
+    isUIdent : Char -> Bool
+    isUIdent c = isIdent c || c == '.'
+
     doBacktick : Int -> Int -> SnocList BTok -> List Char -> SnocList Char -> Either Error (List BTok)
     doBacktick l c toks Nil acc = Left $ E (MkFC "" (l,c)) "EOF in backtick string"
     doBacktick el ec toks ('`' :: cs) acc =

src/Main.idr

@@ -93,12 +93,14 @@ fastReadFile fn = do
 
 
 ||| New style loader, one def at a time
-processModule : FC -> String -> List String -> String -> M String
+processModule : FC -> String -> List String -> QName -> M String
-processModule importFC base stk name = do
+processModule importFC base stk qn@(QN ns nm) = do
   top <- get
+  -- TODO make top.loaded a List QName
+  let name = joinBy "." (snoc ns nm)
   let False := elem name top.loaded | _ => pure ""
   modify { loaded $= (name::) }
-  let fn = if base == "" then name ++ ".newt" else base ++ "/" ++ name ++ ".newt"
+  let fn = (String.joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt"
   Right src <- fastReadFile $ fn
     | Left err => fail "ERROR at \{show importFC}: error reading \{fn}: \{show err}"
   let Right toks = tokenise fn src
@@ -107,19 +109,23 @@ processModule importFC base stk name = do
   let Right ((nameFC, modName), ops, toks) := partialParse fn parseModHeader top.ops toks
     | Left (err, toks) => fail (showError src err)
 
-
   putStrLn "module \{modName}"
-  let True = name == modName
-    | _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
   let ns = forget $ split (== '.') modName
+  let (path, modName') = unsnoc $ split (== '.') modName
+  let bparts = split (== '/') base
+  let True = qn == QN path modName'
+    | _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
+
   let Right (imports, ops, toks) := partialParse fn parseImports ops toks
     | Left (err, toks) => fail (showError src err)
 
   for_ imports $ \ (MkImport fc name') => do
+    let (a,b) = unsnoc $ split (== '.') name'
+    let qname = QN a b
     -- we could use `fc` if it had a filename in it
-
     when (name' `elem` stk) $ error emptyFC "import loop \{show name} -> \{show name'}"
-    processModule fc base (name :: stk) name'
+
+    processModule fc base (name :: stk) qname
 
   top <- get
   mc <- readIORef top.metas
@@ -153,18 +159,31 @@ processFile : String -> M ()
 processFile fn = do
   putStrLn "*** Process \{fn}"
   let parts = split (== '/') fn
-  let file = last parts
+  let (dirs,file) = unsnoc parts
-  let dirs = init parts
   let dir = if dirs == Nil then "." else joinBy "/" dirs
   let (name,ext) = splitFileName file
   putStrLn "\{show dir} \{show name} \{show ext}"
 
+  top <- get
+  Right src <- fastReadFile $ fn
+    | Left err => fail "ERROR at \{fn}:(0, 0): error reading \{fn}: \{show err}"
+  let Right toks = tokenise fn src
+    | Left err => fail (showError src err)
+  let Right ((nameFC, modName), ops, toks) := partialParse fn parseModHeader top.ops toks
+    | Left (err, toks) => fail (showError src err)
+  let ns = forget $ split (== '.') modName
+  let (path, modName') = unsnoc $ split (== '.') modName
+  let True = modName' == name
+    | False => fail "ERROR at \{fn}:(0, 0): module name \{modName'} doesn't match \{name}"
+  let Right base = baseDir (Lin <>< dirs) (Lin <>< path)
+    | Left err => fail "ERROR at \{show nameFC}: \{err}"
+  let base = if base == "" then "." else base
   -- declare internal primitives
   processDecl ["Prim"] (PType emptyFC "Int" Nothing)
   processDecl ["Prim"] (PType emptyFC "String" Nothing)
   processDecl ["Prim"] (PType emptyFC "Char" Nothing)
 
-  src <- processModule emptyFC dir [] name
+  src <- processModule emptyFC base [] (QN path modName')
   top <- get
   -- dumpContext top
 
@@ -175,6 +194,14 @@ processFile fn = do
       exitFailure
   pure ()
 
+  where
+    baseDir : SnocList String -> SnocList String -> Either String String
+    baseDir dirs Lin = Right $ joinBy "/" (dirs <>> [])
+    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"
+
 cmdLine : List String -> M (Maybe String, List String)
 cmdLine [] = pure (Nothing, [])
 cmdLine ("--top" :: args) = cmdLine args -- handled later