From 054a0675f415ef5d1345ce37ce1216446955ab03 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 29 Dec 2024 12:55:09 -0800 Subject: [PATCH] fix importing with dots, prep work for porting --- scripts/translate.sh | 32 +++++++++++++++++++++++++++ src/Lib/CompileExp.idr | 1 - src/Lib/Parser.idr | 20 +++++++++++++++-- src/Lib/Token.idr | 3 +++ src/Lib/Tokenizer2.idr | 8 ++++++- src/Main.idr | 49 ++++++++++++++++++++++++++++++++---------- 6 files changed, 98 insertions(+), 15 deletions(-) create mode 100755 scripts/translate.sh diff --git a/scripts/translate.sh b/scripts/translate.sh new file mode 100755 index 0000000..312df64 --- /dev/null +++ b/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 diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 4f91e7b..44fbd72 100644 --- a/src/Lib/CompileExp.idr +++ b/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 diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index f19a881..4b413d2 100644 --- a/src/Lib/Parser.idr +++ b/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 diff --git a/src/Lib/Token.idr b/src/Lib/Token.idr index 4af2cc3..0f763fa 100644 --- a/src/Lib/Token.idr +++ b/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 diff --git a/src/Lib/Tokenizer2.idr b/src/Lib/Tokenizer2.idr index 935d6a7..b2e378e 100644 --- a/src/Lib/Tokenizer2.idr +++ b/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 = diff --git a/src/Main.idr b/src/Main.idr index 455907b..1a7e651 100644 --- a/src/Main.idr +++ b/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 importFC base stk name = do +processModule : FC -> String -> List String -> QName -> M String +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 = init parts + let (dirs,file) = unsnoc 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