diff --git a/TODO.md b/TODO.md index bed799f..34fcc70 100644 --- a/TODO.md +++ b/TODO.md @@ -17,7 +17,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [ ] There are issues with matching inside do blocks, I think we need to guess scrutinee? I could imagine constraining metas too (e.g. if Just ... at ?m123 then ?m123 =?= Maybe ?m456) - Also, the root cause is tough to track down if there is a type error (this happens with `do` in Idris, too). - Part of it is the auto solutions are getting discarded because of an unrelated unification failure. Either auto shouldn't go as deep or should run earlier. Forgetting that lookupMap returns a (k,v) pair is a good example. -- [ ] error for non-linear pattern +- [ ] add error for non-linear pattern - [ ] typeclass dependencies - need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this. - for something like an `isEq` field in `Ord`, auto-search is picking up the function being defined. diff --git a/aoc2023/Lib.newt b/aoc2023/Lib.newt index eaddf0b..d2b61d9 100644 --- a/aoc2023/Lib.newt +++ b/aoc2023/Lib.newt @@ -62,10 +62,10 @@ data IO : U -> U where MkIO : {a : U} -> (World -> Pair World a) -> IO a -- TODO unified Number for now -ptype Int -ptype String -ptype Char + + + ptype Array : U -> U diff --git a/aoc2023/Node.newt b/aoc2023/Node.newt index 6077b96..934740f 100644 --- a/aoc2023/Node.newt +++ b/aoc2023/Node.newt @@ -4,4 +4,4 @@ import Prelude pfunc fs : JSObject := `require('fs')` pfunc getArgs : List String := `arrayToList(String, process.argv)` -pfunc readFile uses (fs) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` +pfunc readFile uses (fs MkIORes Unit) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)` diff --git a/newt/JSLib.newt b/newt/JSLib.newt index a9a1b1a..fda49c6 100644 --- a/newt/JSLib.newt +++ b/newt/JSLib.newt @@ -1,7 +1,7 @@ module JSLib -ptype Int -ptype String + + infixl 4 _+_ infixl 5 _*_ diff --git a/newt/Prelude.newt b/newt/Prelude.newt index a974172..79c11a8 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -235,10 +235,6 @@ infixr 7 _++_ class Concat a where _++_ : a → a → a -ptype String -ptype Int -ptype Char - pfunc sconcat : String → String → String := `(x,y) => x + y` instance Concat String where _++_ = sconcat diff --git a/newt/TypeClass.newt b/newt/TypeClass.newt index c3463f1..cdfeda2 100644 --- a/newt/TypeClass.newt +++ b/newt/TypeClass.newt @@ -63,7 +63,7 @@ infixr 1 _,_ data Pair : U -> U -> U where _,_ : {A B : U} -> A -> B -> Pair A B -ptype Int + test : Maybe Int test = pure 10 diff --git a/newt/tutorial.newt b/newt/tutorial.newt index 593afe5..944d76d 100644 --- a/newt/tutorial.newt +++ b/newt/tutorial.newt @@ -5,7 +5,7 @@ module Tutorial -- import Prelude not implemented yet -- declare a primitive type -ptype Int + -- declare a more complex primitive type ptype Array : U -> U diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt index 15bf366..53b4317 100644 --- a/playground/samples/Tour.newt +++ b/playground/samples/Tour.newt @@ -101,9 +101,7 @@ foo a b = ? -- We can define native types, if the type is left off, it defaults to U -ptype Int : U -ptype String : U -ptype Char : U +ptype SomePrimType : U -- The names of these three types are special, primitive numbers, strings, -- and characters inhabit them, respectively. We can match on primitives, but diff --git a/playground/samples/TypeClass.newt b/playground/samples/TypeClass.newt index 6662230..442149e 100644 --- a/playground/samples/TypeClass.newt +++ b/playground/samples/TypeClass.newt @@ -51,7 +51,7 @@ infixr 1 _,_ data Pair : U -> U -> U where _,_ : ∀ A B. A -> B -> Pair A B -ptype Int + test : Maybe Int test = pure 10 diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 1056001..5414329 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -202,6 +202,8 @@ jsIdent id = if elem id keywords then text ("$" ++ id) else text $ pack $ fix (u fix (x :: xs) = if isAlphaNum x || x == '_' then x :: fix xs + -- make qualified names more readable + else if x == '.' then '_' :: fix xs else if x == '$' then '$' :: '$' :: fix xs else @@ -256,12 +258,12 @@ mkArgs : Nat -> List String -> List String mkArgs Z acc = acc mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc) -dcon : String -> Nat -> Doc -dcon nm Z = stmtToDoc $ JConst nm $ LitObject [("tag", LitString nm)] -dcon nm arity = +dcon : QName -> Nat -> Doc +dcon qn@(QN ns nm) Z = stmtToDoc $ JConst (show qn) $ LitObject [("tag", LitString nm)] +dcon qn@(QN ns nm) arity = let args := mkArgs arity [] obj := ("tag", LitString nm) :: map (\x => (x, Var x)) args - in stmtToDoc $ JConst nm (JLam args (JReturn (LitObject obj))) + in stmtToDoc $ JConst (show qn) (JLam args (JReturn (LitObject obj))) -- use iife to turn stmts into expr maybeWrap : JSStmt Return -> JSExp @@ -273,38 +275,47 @@ entryToDoc (MkEntry _ name ty (Fn tm)) = do debug "compileFun \{pprint [] tm}" ct <- compileFun tm let exp = maybeWrap $ termToJS empty ct JReturn - pure $ text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";" + pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ ";" entryToDoc (MkEntry _ name type Axiom) = pure "" entryToDoc (MkEntry _ name type (TCon strs)) = pure $ dcon name (piArity type) entryToDoc (MkEntry _ name type (DCon arity str)) = pure $ dcon name arity entryToDoc (MkEntry _ name type PrimTCon) = pure $ dcon name (piArity type) -entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent name <+> "=" <+> text src +entryToDoc (MkEntry _ name _ (PrimFn src _)) = pure $ text "const" <+> jsIdent (show name) <+> "=" <+> text src ||| This version (call `reverse . snd <$> process "main" ([],[])`) will do dead ||| code elimination, but the Prelude js primitives are reaching for ||| stuff like True, False, MkUnit, fs which get eliminated -process : (List String, List Doc) -> String -> M (List String, List Doc) +process : (List QName, List Doc) -> QName -> M (List QName, List Doc) process (done,docs) nm = do let False = nm `elem` done | _ => pure (done,docs) top <- get case TopContext.lookup nm top of Nothing => error emptyFC "\{nm} not in scope" Just entry@(MkEntry _ name ty (PrimFn src uses)) => do - (done,docs) <- foldlM process (nm :: done, docs) uses + (done,docs) <- foldlM assign (nm :: done, docs) uses pure (done, !(entryToDoc entry) :: docs) Just (MkEntry _ name ty (Fn tm)) => do debug "compileFun \{pprint [] tm}" ct <- compileFun tm -- If ct has zero arity and is a compount expression, this fails.. let exp = maybeWrap $ termToJS empty ct JReturn - let doc = text "const" <+> jsIdent name <+> text "=" <+/> expToDoc exp ++ ";" + let doc = text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ ";" (done,docs) <- walkTm tm (nm :: done, docs) pure (done, doc :: docs) - Just entry => pure (nm :: done, !(entryToDoc entry) :: docs) where - walkTm : Tm -> (List String, List Doc) -> M (List String, List Doc) - walkAlt : (List String, List Doc) -> CaseAlt -> M (List String, List Doc) + assign : (List QName, List Doc) -> String -> M (List QName, List Doc) + assign (done, docs) nm = case lookupRaw nm !get of + Nothing => pure (done, docs) + (Just (MkEntry fc name type def)) => do + let tag = QN [] nm + let False = tag `elem` done | _ => pure (done,docs) + (done,docs) <- process (done, docs) name + let doc = text "const" <+> jsIdent nm <+> text "=" <+> jsIdent (show name) ++ ";" + pure (tag :: done, doc :: docs) + + walkTm : Tm -> (List QName, List Doc) -> M (List QName, List Doc) + walkAlt : (List QName, List Doc) -> CaseAlt -> M (List QName, List Doc) walkAlt acc (CaseDefault t) = walkTm t acc walkAlt acc (CaseCons name args t) = walkTm t acc walkAlt acc (CaseLit lit t) = walkTm t acc @@ -322,10 +333,13 @@ export compile : M (List Doc) compile = do top <- get - case lookup "main" top of - Just _ => reverse . snd <$> process ([],[]) "main" + case lookupRaw "main" top of + Just (MkEntry fc name type def) => do + tmp <- snd <$> process ([],[]) name + let exec = stmtToDoc $ JPlain $ Apply (Var $ show name) [] + pure $ reverse (exec :: tmp) -- If there is no main, compile everything for the benefit of the playground Nothing => do top <- get - traverse entryToDoc top.defs + traverse entryToDoc $ map snd $ SortedMap.toList top.defs diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index a0eb0ec..4f91e7b 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -58,7 +58,7 @@ piArity _ = Z ||| This is how much we want to curry at top level ||| leading lambda Arity is used for function defs and metas ||| TODO - figure out how this will work with erasure -arityForName : FC -> Name -> M Nat +arityForName : FC -> QName -> M Nat arityForName fc nm = case lookup nm !get of -- let the magic hole through for now (will generate bad JS) Nothing => error fc "Name \{show nm} not in scope" @@ -111,7 +111,7 @@ compileTerm t@(Ref fc nm _) = do top <- get let Just (MkEntry _ _ type _) = lookup nm top | Nothing => error fc "Undefined name \{nm}" - apply (CRef nm) [] [<] !(arityForName fc nm) type + apply (CRef (show nm)) [] [<] !(arityForName fc nm) type compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME compileTerm (Lam _ nm _ _ t) = pure $ CLam nm !(compileTerm t) @@ -125,7 +125,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm) top <- get let Just (MkEntry _ _ type _) = lookup nm top | Nothing => error fc "Undefined name \{nm}" - apply (CRef nm) args' [<] arity type + apply (CRef (show nm)) args' [<] arity type _ | (t, args) = do debug "apply other \{pprint [] t}" t' <- compileTerm t @@ -138,7 +138,8 @@ compileTerm (Case _ t alts) = do t' <- compileTerm t alts' <- traverse (\case CaseDefault tm => pure $ CDefAlt !(compileTerm tm) - CaseCons nm args tm => pure $ CConAlt nm args !(compileTerm tm) + -- we use the base name for the tag, some primitives assume this + CaseCons (QN ns nm) args tm => pure $ CConAlt nm args !(compileTerm tm) CaseLit lit tm => pure $ CLitAlt lit !(compileTerm tm)) alts pure $ CCase t' alts' compileTerm (Lit _ lit) = pure $ CLit lit diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 35007fc..0976246 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -397,7 +397,7 @@ insert ctx tm ty = do insert ctx (App (getFC tm) tm m) !(b $$ mv) va => pure (tm, va) -primType : FC -> String -> M Val +primType : FC -> QName -> M Val primType fc nm = case lookup nm !(get) of Just (MkEntry _ name ty PrimTCon) => pure $ VRef fc name PrimTCon [<] _ => error fc "Primitive type \{show nm} not in scope" @@ -465,16 +465,16 @@ findSplit (x :: xs) = findSplit xs -- TODO, we may need to filter these against the type to rule out -- impossible cases -getConstructors : Context -> FC -> Val -> M (List (String, Nat, Tm)) +getConstructors : Context -> FC -> Val -> M (List (QName, Nat, Tm)) getConstructors ctx scfc (VRef fc nm _ _) = do names <- lookupTCon nm traverse lookupDCon names where - lookupTCon : String -> M (List String) + lookupTCon : QName -> M (List QName) lookupTCon str = case lookup nm !get of (Just (MkEntry _ name type (TCon names))) => pure names _ => error scfc "Not a type constructor \{nm}" - lookupDCon : String -> M (String, Nat, Tm) + lookupDCon : QName -> M (QName, Nat, Tm) lookupDCon nm = do case lookup nm !get of (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type) @@ -552,7 +552,7 @@ updateContext ctx ((k, val) :: cs) = -- ok, so this is a single constructor, CaseAlt -- return Nothing if dcon doesn't unify with scrut -buildCase : Context -> Problem -> String -> Val -> (String, Nat, Tm) -> M (Maybe CaseAlt) +buildCase : Context -> Problem -> String -> Val -> (QName, Nat, Tm) -> M (Maybe CaseAlt) buildCase ctx prob scnm scty (dcName, arity, ty) = do debug "CASE \{scnm} match \{dcName} ty \{pprint (names ctx) ty}" vty <- eval [] CBN ty @@ -684,7 +684,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do else pure $ (nm, pat) :: !(makeConstr xs pats) -- replace constraint with constraints on parameters, or nothing if non-matching clause - rewriteConstraint : String -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint)) + rewriteConstraint : QName -> List Bind -> List Constraint -> List Constraint -> M (Maybe (List Constraint)) rewriteConstraint sctynm vars [] acc = pure $ Just acc rewriteConstraint sctynm vars (c@(nm, y) :: xs) acc = if nm == scnm @@ -709,7 +709,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do Nothing => error fc "Internal Error: DCon \{nm} not found" else rewriteConstraint sctynm vars xs (c :: acc) - rewriteClause : String -> List Bind -> Clause -> M (Maybe Clause) + rewriteClause : QName -> List Bind -> Clause -> M (Maybe Clause) rewriteClause sctynm vars (MkClause fc cons pats expr) = do Just cons <- rewriteConstraint sctynm vars cons [] | _ => pure Nothing pure $ Just $ MkClause fc cons pats expr @@ -728,10 +728,10 @@ mkPat top (RAs fc as tm, icit) = t => error fc "Can't put as on non-constructor \{show tm}" mkPat top (tm, icit) = do case splitArgs tm [] of - ((RVar fc nm), b) => case lookup nm top of + ((RVar fc nm), b) => case lookupRaw nm top of (Just (MkEntry _ name type (DCon k str))) => -- TODO check arity, also figure out why we need reverse - pure $ PatCon fc icit nm !(traverse (mkPat top) b) Nothing + pure $ PatCon fc icit name !(traverse (mkPat top) b) Nothing -- This fires when a global is shadowed by a pattern var -- Just _ => error (getFC tm) "\{show nm} is not a data constructor" _ => case b of @@ -897,10 +897,18 @@ buildLitCases ctx prob fc scnm scty = do Nothing => True _ => False -litTyName : Literal -> String -litTyName (LString str) = "String" -litTyName (LInt i) = "Int" -litTyName (LChar c) = "Char" +-- TODO - figure out if these need to be in Prelude or have a special namespace +-- If we lookupRaw "String", we could get different answers in different contexts. +-- maybe Hardwire this one +stringType : QName +stringType = QN ["Prim"] "String" +intType = QN ["Prim"] "Int" +charType = QN ["Prim"] "Char" + +litTyName : Literal -> QName +litTyName (LString str) = stringType +litTyName (LInt i) = intType +litTyName (LChar c) = charType renameContext : String -> String -> Context -> Context renameContext from to ctx = { types $= go } ctx @@ -976,7 +984,7 @@ undo prev ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm -- undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) !(undo xs) Explicit undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs undo prev ((DoArrow fc left@(RVar fc' nm) right []) :: xs) = - case lookup nm !get of + case lookupRaw nm !get of Just _ => do let nm = "$sc" rest <- pure $ RCase fc (RVar fc nm) [MkAlt left !(undo fc xs)] @@ -1074,10 +1082,10 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of infer ctx (RVar fc nm) = go 0 ctx.types where go : Nat -> Vect n (String, Val) -> M (Tm, Val) - go i [] = case lookup nm !(get) of + go i [] = case lookupRaw nm !(get) of Just (MkEntry _ name ty def) => do debug "lookup \{name} as \{show def}" - pure (Ref fc nm def, !(eval [] CBN ty)) + pure (Ref fc name def, !(eval [] CBN ty)) Nothing => error fc "\{show nm} not in scope" go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd fc i, ty) else go (i + 1) xs @@ -1148,8 +1156,8 @@ infer ctx (RImplicit fc) = do tm <- freshMeta ctx fc vty Normal pure (tm, vty) -infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc "String")) -infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc "Int")) -infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), !(primType fc "Char")) +infer ctx (RLit fc (LString str)) = pure (Lit fc (LString str), !(primType fc stringType)) +infer ctx (RLit fc (LInt i)) = pure (Lit fc (LInt i), !(primType fc intType)) +infer ctx (RLit fc (LChar c)) = pure (Lit fc (LChar c), !(primType fc charType)) infer ctx (RAs fc _ _) = error fc "@ can only be used in patterns" infer ctx tm = error (getFC tm) "Implement infer \{show tm}" diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index a1b8a57..f613724 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -42,7 +42,9 @@ findMatches ctx ty ((MkEntry _ name type def) :: xs) = do debug "TRY \{name} : \{pprint [] type} for \{show ty}" -- This check is solving metas, so we save mc below in case we want this solution -- tm <- check (mkCtx fc) (RVar fc name) ty - tm <- check ctx (RVar fc name) ty + -- FIXME RVar should optionally have qualified names + let (QN ns nm) = name + tm <- check ctx (RVar fc nm) ty debug "Found \{pprint [] tm} for \{show ty}" mc' <- readIORef top.metas writeIORef top.metas mc @@ -103,7 +105,7 @@ solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do -- we want the context here too. top <- get [(tm, mc)] <- case !(contextMatches ctx ty) of - [] => findMatches ctx ty top.defs + [] => findMatches ctx ty $ toList top.defs xs => pure xs | res => do debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}" @@ -169,7 +171,7 @@ logMetas mstart = do -- we want the context here too. top <- get matches <- case !(contextMatches ctx ty) of - [] => findMatches ctx ty top.defs + [] => findMatches ctx ty $ toList top.defs xs => pure xs -- TODO try putting mc into TopContext for to see if it gives better terms pure $ " \{show $ length matches} Solutions:" :: map ((" " ++) . interpolate . pprint (names ctx) . fst) matches @@ -194,51 +196,51 @@ impTele tele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tel export -processDecl : Decl -> M () +processDecl : List String -> Decl -> M () -- REVIEW I supposed I could have updated top here instead of the dance with the parser... -processDecl (PMixFix{}) = pure () +processDecl ns (PMixFix{}) = pure () -processDecl (TypeSig fc names tm) = do +processDecl ns (TypeSig fc names tm) = do putStrLn "-----" top <- get mc <- readIORef top.metas let mstart = length mc.metas for_ names $ \nm => do - let Nothing := lookup nm top + let Nothing := lookupRaw nm top | Just entry => error fc "\{show nm} is already defined at \{show entry.fc}" pure () ty <- check (mkCtx fc) tm (VU fc) ty <- zonk top 0 [] ty putStrLn "TypeSig \{unwords names} : \{pprint [] ty}" - for_ names $ \nm => setDef nm fc ty Axiom + for_ names $ \nm => setDef (QN ns nm) fc ty Axiom -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here -- logMetas mstart -processDecl (PType fc nm ty) = do +processDecl ns (PType fc nm ty) = do top <- get ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) - setDef nm fc ty' PrimTCon + setDef (QN ns nm) fc ty' PrimTCon -processDecl (PFunc fc nm uses ty src) = do +processDecl ns (PFunc fc nm uses ty src) = do top <- get ty <- check (mkCtx fc) ty (VU fc) ty' <- nf [] ty putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}" -- TODO wire through fc? - for_ uses $ \ name => case lookup name top of + for_ uses $ \ name => case lookupRaw name top of Nothing => error fc "\{name} not in scope" _ => pure () - setDef nm fc ty' (PrimFn src uses) + setDef (QN ns nm) fc ty' (PrimFn src uses) -processDecl (Def fc nm clauses) = do +processDecl ns (Def fc nm clauses) = do putStrLn "-----" putStrLn "Def \{show nm}" top <- get mc <- readIORef top.metas let mstart = length mc.metas - let Just entry = lookup nm top + let Just entry = lookupRaw nm top | Nothing => throwError $ E fc "No declaration for \{nm}" let (MkEntry fc name ty Axiom) := entry | _ => throwError $ E fc "\{nm} already defined at \{show entry.fc}" @@ -269,10 +271,10 @@ processDecl (Def fc nm clauses) = do tm'' <- erase [] tm' [] when top.verbose $ putStrLn "ERASED\n\{render 80 $ pprint[] tm'}" debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" - updateDef nm fc ty (Fn tm') + updateDef (QN ns nm) fc ty (Fn tm') -- logMetas mstart -processDecl (DCheck fc tm ty) = do +processDecl ns (DCheck fc tm ty) = do putStrLn "----- DCheck" top <- get @@ -287,7 +289,7 @@ processDecl (DCheck fc tm ty) = do norm <- nfv [] res putStrLn " NFV \{pprint [] norm}" -processDecl (Class classFC nm tele decls) = do +processDecl ns (Class classFC nm tele decls) = do -- REVIEW maybe we can leverage Record for this -- a couple of catches, we don't want the dotted accessors and -- the self argument should be an auto-implicit @@ -306,7 +308,7 @@ processDecl (Class classFC nm tele decls) = do let decl = Data classFC nm tcType [TypeSig classFC [dcName] dcType] putStrLn "Decl:" putStrLn $ render 90 $ pretty decl - processDecl decl + processDecl ns decl for_ fields $ \ (fc,name,ty) => do let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Auto Many) tail ty let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields @@ -316,11 +318,11 @@ processDecl (Class classFC nm tele decls) = do putStrLn "\{name} : \{pretty funType}" putStrLn "\{pretty decl}" - processDecl $ TypeSig fc [name] funType - processDecl decl + processDecl ns $ TypeSig fc [name] funType + processDecl ns decl -processDecl (Instance instfc ty decls) = do +processDecl ns (Instance instfc ty decls) = do let decls = collectDecl decls putStrLn "-----" putStrLn "Instance \{pretty ty}" @@ -369,7 +371,7 @@ processDecl (Instance instfc ty decls) = do let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls | _ => error instfc "no definition for \{nm}" - setDef nm' fc ty' Axiom + setDef (QN ns nm') fc ty' Axiom let decl = (Def fc nm' xs) putStrLn "***" putStrLn "«\{nm'}» : \{pprint [] ty'}" @@ -379,17 +381,17 @@ processDecl (Instance instfc ty decls) = do -- This needs to be declared before processing the defs, but the defs need to be -- declared before this - side effect is that a duplicate def is noted at the first -- member - processDecl sigDecl + processDecl ns sigDecl for_ (mapMaybe id defs) $ \decl => do -- debug because already printed above, but nice to have it near processing debug $ render 80 $ pretty decl - processDecl decl - - let decl = Def instfc instname [(RVar instfc instname, mkRHS instname conTele (RVar instfc con))] + processDecl ns decl + let (QN _ con') = con + let decl = Def instfc instname [(RVar instfc instname, mkRHS instname conTele (RVar instfc con'))] putStrLn "SIGDECL" putStrLn "\{pretty sigDecl}" putStrLn $ render 80 $ pretty decl - processDecl decl + processDecl ns decl where -- try to extract types of individual fields from the typeclass dcon -- We're assuming they don't depend on each other. @@ -414,17 +416,17 @@ processDecl (Instance instfc ty decls) = do apply (VPi fc nm icit rig a b) (x :: xs) = apply !(b $$ x) xs apply x (y :: xs) = error instfc "expected pi type \{show x}" -processDecl (Data fc nm ty cons) = do +processDecl ns (Data fc nm ty cons) = do putStrLn "-----" putStrLn "Data \{nm}" top <- get mc <- readIORef top.metas tyty <- check (mkCtx fc) ty (VU fc) - case lookup nm top of + case lookupRaw nm top of Just (MkEntry _ name type Axiom) => do unifyCatch fc (mkCtx fc) !(eval [] CBN tyty) !(eval [] CBN type) Just (MkEntry _ name type _) => error fc "\{show nm} already declared" - Nothing => setDef nm fc tyty Axiom + Nothing => setDef (QN ns nm) fc tyty Axiom cnames <- for cons $ \x => case x of (TypeSig fc names tm) => do debug "check dcon \{show names} \{show tm}" @@ -438,15 +440,15 @@ processDecl (Data fc nm ty cons) = do let tnames = reverse $ map (\(MkBind _ nm _ _ _) => nm) tele let (Ref _ hn _, args) := funArgs codomain | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}" - when (hn /= nm) $ + when (hn /= QN ns nm) $ error (getFC codomain) "Constructor codomain is \{pprint tnames codomain} rather than \{nm}" for_ names $ \ nm' => do - setDef nm' fc dty (DCon (getArity dty) nm) - pure names + setDef (QN ns nm') fc dty (DCon (getArity dty) hn) + pure $ map (QN ns) names decl => throwError $ E (getFC decl) "expected constructor declaration" putStrLn "setDef \{nm} TCon \{show $ join cnames}" - updateDef nm fc tyty (TCon (join cnames)) + updateDef (QN ns nm) fc tyty (TCon (join cnames)) -- logMetas mstart where checkDeclType : Tm -> M () @@ -454,7 +456,7 @@ processDecl (Data fc nm ty cons) = do checkDeclType (Pi _ str icit rig t u) = checkDeclType u checkDeclType _ = error fc "data type doesn't return U" -processDecl (Record recordFC nm tele cname decls) = do +processDecl ns (Record recordFC nm tele cname decls) = do putStrLn "-----" putStrLn "Record" let fields = getSigs decls @@ -470,7 +472,7 @@ processDecl (Record recordFC nm tele cname decls) = do let decl = Data recordFC nm tcType [TypeSig recordFC [dcName] dcType] putStrLn "Decl:" putStrLn $ render 90 $ pretty decl - processDecl decl + processDecl ns decl for_ fields $ \ (fc,name,ty) => do -- TODO dependency isn't handled yet -- we'll need to replace stuff like `len` with `len self`. @@ -482,5 +484,5 @@ processDecl (Record recordFC nm tele cname decls) = do putStrLn "\{name} : \{pretty funType}" putStrLn "\{pretty decl}" - processDecl $ TypeSig fc [name] funType - processDecl decl + processDecl ns $ TypeSig fc [name] funType + processDecl ns decl diff --git a/src/Lib/Syntax.idr b/src/Lib/Syntax.idr index 44f7dd6..358cf37 100644 --- a/src/Lib/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -12,7 +12,7 @@ data Raw : Type where public export data Pattern = PatVar FC Icit Name - | PatCon FC Icit Name (List Pattern) (Maybe Name) + | PatCon FC Icit QName (List Pattern) (Maybe Name) | PatWild FC Icit -- Not handling this yet, but we need to be able to work with numbers and strings... | PatLit FC Literal @@ -231,8 +231,8 @@ export Pretty Pattern where -- FIXME - wrap Implicit with {} pretty (PatVar _ icit nm) = text nm - pretty (PatCon _ icit nm args Nothing) = text nm <+> spread (map pretty args) - pretty (PatCon _ icit nm args (Just as)) = text as ++ "@(" ++ text nm <+> spread (map pretty args) ++ ")" + pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args) + pretty (PatCon _ icit nm args (Just as)) = text as ++ "@(" ++ text (show nm) <+> spread (map pretty args) ++ ")" pretty (PatWild _icit) = "_" pretty (PatLit _ lit) = pretty lit diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index ecf1a97..df3aa5d 100644 --- a/src/Lib/TopContext.idr +++ b/src/Lib/TopContext.idr @@ -1,68 +1,51 @@ module Lib.TopContext +import Data.IORef +import Data.SortedMap import Data.String import Lib.Types -import Data.IORef -- I want unique ids, to be able to lookup, update, and a Ref so -- I don't need good Context discipline. (I seem to have made mistakes already.) export -lookup : String -> TopContext -> Maybe TopEntry -lookup nm top = go top.defs +lookup : QName -> TopContext -> Maybe TopEntry +lookup nm top = lookup nm top.defs + +-- TODO - look at imported namespaces, and either have a map of imported names or search imported namespaces.. +export +lookupRaw : String -> TopContext -> Maybe TopEntry +lookupRaw raw top = go $ toList top.defs where - go : List TopEntry -> Maybe TopEntry - go [] = Nothing - go (entry :: xs) = if entry.name == nm then Just entry else go xs + go : List (QName, TopEntry) -> Maybe TopEntry + go Nil = Nothing + go (((QN ns nm), entry) :: rest) = if nm == raw then Just entry else go rest -- Maybe pretty print? export covering Show TopContext where - show (MkTop defs metas _ _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" + show (MkTop defs metas _ _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map (show . snd) $ toList defs}]" public export empty : HasIO m => m TopContext -empty = pure $ MkTop [] !(newIORef (MC [] 0)) False !(newIORef []) [] empty - -||| set or replace def. probably need to check types and Axiom on replace --- public export --- setDef : String -> Tm -> Def -> TopContext -> TopContext --- setDef name ty def = { defs $= go } --- where --- go : List TopEntry -> List TopEntry --- go [] = [MkEntry name ty def] --- go (x@(MkEntry nm ty' def') :: defs) = if nm == name --- then MkEntry name ty def :: defs --- else x :: go defs +empty = pure $ MkTop empty !(newIORef (MC [] 0)) False !(newIORef []) [] empty public export -setDef : String -> FC -> Tm -> Def -> M () +setDef : QName -> FC -> Tm -> Def -> M () setDef name fc ty def = do top <- get - defs <- go top.defs - put $ { defs := defs } top - where - go : List TopEntry -> M (List TopEntry) - go [] = pure $ [MkEntry fc name ty def] - go (x@(MkEntry fc' nm ty' def') :: defs) = if nm == name - then error fc "\{name} is already defined at \{show fc'}" - else (x ::) <$> go defs + let Nothing = lookup name top.defs + | Just (MkEntry fc' nm' ty' def') => error fc "\{name} is already defined at \{show fc'}" + put $ { defs $= (insert name (MkEntry fc name ty def)) } top public export -updateDef : String -> FC -> Tm -> Def -> M () +updateDef : QName -> FC -> Tm -> Def -> M () updateDef name fc ty def = do top <- get - defs <- go top.defs - put $ { defs := defs } top - where - go : List TopEntry -> M (List TopEntry) - go [] = error fc "\{name} not declared" - go (x@(MkEntry fc' nm ty' def') :: defs) = if nm == name - -- keep original fc, so it points to the TypeSig - then pure $ MkEntry fc' name ty def :: defs - else (x ::) <$> go defs - + let Just (MkEntry fc' nm' ty' def') = lookup name top.defs + | Nothing => error fc "\{name} not declared" + put $ { defs $= (insert name (MkEntry fc' name ty def)) } top public export addError : Error -> M () diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index b64a718..a91e57d 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -16,6 +16,29 @@ import Data.SortedMap import Data.String import Data.Vect + +public export +data QName : Type where + QN : List String -> String -> QName + +public export +Eq QName where + QN ns n == QN ns' n' = n == n' && ns == ns' + +public export +Show QName where + show (QN [] n) = n + show (QN ns n) = joinBy "." ns ++ "." ++ n + +public export +Interpolation QName where + interpolate = show + +export +Ord QName where + compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' + + public export Name : Type Name = String @@ -97,7 +120,7 @@ Show Literal where public export data CaseAlt : Type where CaseDefault : Tm -> CaseAlt - CaseCons : (name : String) -> (args : List String) -> Tm -> CaseAlt + CaseCons : (name : QName) -> (args : List String) -> Tm -> CaseAlt CaseLit : Literal -> Tm -> CaseAlt data Def : Type @@ -113,7 +136,7 @@ Eq Literal where data Tm : Type where Bnd : FC -> Nat -> Tm -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. - Ref : FC -> String -> Def -> Tm + Ref : FC -> QName -> Def -> Tm Meta : FC -> Nat -> Tm -- kovacs optimization, I think we can App out meta instead -- InsMeta : Nat -> List BD -> Tm @@ -219,7 +242,7 @@ pprint names tm = go 0 names tm goAlt : Nat -> List String -> CaseAlt -> Doc goAlt p names (CaseDefault t) = "_" <+> "=>" <+> go p ("_" :: names) t - goAlt p names (CaseCons name args t) = text name <+> spread (map text args) <+> (nest 2 $ "=>" <+/> go p (reverse args ++ names) t) + goAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ "=>" <+/> go p (reverse args ++ names) t) -- `;` is not in surface syntax, but sometimes we print on one line goAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ "=>" <+/> go p names t ++ ";") @@ -227,7 +250,7 @@ pprint names tm = go 0 names tm -- Either a bug or we're printing without names Nothing => text "BND:\{show k}" Just nm => text "\{nm}:\{show k}" - go p names (Ref _ str mt) = text str + go p names (Ref _ str mt) = text (show str) go p names (Meta _ k) = text "?m:\{show k}" go p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> go 0 (nm :: names) t go p names (App _ t u) = parens 0 p $ go 0 names t <+> go 1 names u @@ -246,8 +269,8 @@ pprint names tm = go 0 names tm go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t <+> "in" (nest 2 $ go 0 (nm :: names) u) go p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> ":" <+> go 0 names ty <+> ":=" <+> go 0 names t <+> "in" (nest 2 $ go 0 (nm :: names) u) go p names (Erased _) = "ERASED" -data Val : Type +data Val : Type -- IS/TypeTheory.idr is calling this a Kripke function space -- Yaffle, IS/TypeTheory use a function here. @@ -259,7 +282,6 @@ data Val : Type -- Yaffle is vars -> vars here - public export data Closure : Type @@ -267,9 +289,7 @@ public export data Val : Type where -- This will be local / flex with spine. VVar : FC -> (k : Nat) -> (sp : SnocList Val) -> Val - -- I wanted the Maybe Tm in here, but for now we're always expanding. - -- Maybe this is where I glue - VRef : FC -> (nm : String) -> Def -> (sp : SnocList Val) -> Val + VRef : FC -> (nm : QName) -> Def -> (sp : SnocList Val) -> Val -- neutral case VCase : FC -> (sc : Val) -> List CaseAlt -> Val -- we'll need to look this up in ctx with IO @@ -306,8 +326,8 @@ covering export Show Val where show (VVar _ k [<]) = "%var\{show k}" show (VVar _ k sp) = "(%var\{show k} \{unwords $ map show (sp <>> [])})" - show (VRef _ nm _ [<]) = nm - show (VRef _ nm _ sp) = "(\{nm} \{unwords $ map show (sp <>> [])})" + show (VRef _ nm _ [<]) = show nm + show (VRef _ nm _ sp) = "(\{show nm} \{unwords $ map show (sp <>> [])})" show (VMeta _ ix sp) = "(%meta \{show ix} [\{show $ length sp} sp])" show (VLam _ str icit quant x) = "(%lam \{show quant}\{str} \{show x})" show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show x}}. \{show y})" @@ -387,7 +407,7 @@ record MetaContext where public export -data Def = Axiom | TCon (List String) | DCon Nat String | Fn Tm | PrimTCon +data Def = Axiom | TCon (List QName) | DCon Nat QName | Fn Tm | PrimTCon | PrimFn String (List String) public export @@ -405,7 +425,7 @@ public export record TopEntry where constructor MkEntry fc : FC - name : String + name : QName type : Tm def : Def @@ -426,9 +446,9 @@ public export record TopContext where constructor MkTop -- We'll add a map later? - defs : List TopEntry + defs : SortedMap QName TopEntry metas : IORef MetaContext - verbose : Bool + verbose : Bool -- command line flag errors : IORef (List Error) ||| loaded modules loaded : List String diff --git a/src/Main.idr b/src/Main.idr index fe2969d..0712eab 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -5,6 +5,7 @@ import Control.Monad.Error.Either import Control.Monad.Error.Interface import Control.Monad.State import Data.List +import Data.List1 import Data.String import Data.Vect import Data.IORef @@ -34,11 +35,11 @@ fail msg = putStrLn msg >> exitFailure jsonTopContext : M Json jsonTopContext = do top <- get - pure $ JsonObj [("context", JsonArray (map jsonDef top.defs))] + pure $ JsonObj [("context", JsonArray (map jsonDef $ toList top.defs))] where jsonDef : TopEntry -> Json -- There is no FC here... - jsonDef (MkEntry fc name type def) = JsonObj + jsonDef (MkEntry fc (QN ns name) type def) = JsonObj [ ("fc", toJson fc) , ("name", toJson name) , ("type", toJson (render 80 $ pprint [] type) ) @@ -47,7 +48,7 @@ jsonTopContext = do dumpContext : TopContext -> M () dumpContext top = do putStrLn "Context:" - go top.defs + go $ toList top.defs putStrLn "---" where go : List TopEntry -> M () @@ -61,7 +62,6 @@ writeSource fn = do [ "\"use strict\";" , "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" ] ++ map (render 90) docs - ++ [ "main();" ] Right _ <- writeFile fn src | Left err => fail (show err) Right _ <- chmodRaw fn 493 | Left err => fail (show err) @@ -111,7 +111,7 @@ processModule base stk name = do 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 Right (imports, ops, toks) := partialParse fn parseImports ops toks | Left (err, toks) => fail (showError src err) @@ -133,7 +133,7 @@ processModule base stk name = do putStrLn "process Decls" - traverse_ tryProcessDecl (collectDecl decls) + traverse_ (tryProcessDecl ns) (collectDecl decls) -- we don't want implict errors from half-processed functions -- but suppress them all on error for simplicity. @@ -144,9 +144,9 @@ processModule base stk name = do -- parseDecls : -- tryParseDecl : - tryProcessDecl : Decl -> M () - tryProcessDecl decl = do - Left err <- tryError {e=Error} $ processDecl decl | _ => pure () + tryProcessDecl : List String -> Decl -> M () + tryProcessDecl ns decl = do + Left err <- tryError {e=Error} $ processDecl ns decl | _ => pure () addError err processFile : String -> M () @@ -158,6 +158,11 @@ processFile fn = do let (name,ext) = splitFileName (fromMaybe "" $ last' parts) putStrLn "\{show dir} \{show name} \{show ext}" + -- declare internal primitives + processDecl ["Prim"] (PType emptyFC "Int" Nothing) + processDecl ["Prim"] (PType emptyFC "String" Nothing) + processDecl ["Prim"] (PType emptyFC "Char" Nothing) + src <- processModule dir [] name top <- get -- dumpContext top diff --git a/tests/black/Auto.newt b/tests/black/Auto.newt index d070a74..0dc13f1 100644 --- a/tests/black/Auto.newt +++ b/tests/black/Auto.newt @@ -1,8 +1,5 @@ module Auto -ptype String -ptype Int - pfunc i2s : Int -> String := `(i) => ''+i` pfunc _++_ : String -> String -> String := `(a,b) => a + b` diff --git a/tests/black/Auto2.newt b/tests/black/Auto2.newt index c04a400..33b7392 100644 --- a/tests/black/Auto2.newt +++ b/tests/black/Auto2.newt @@ -3,7 +3,7 @@ module Auto2 ptype World pfunc log : {A : U} -> A -> World := `(_, a) => console.log(a)` -ptype Int + pfunc i_plus : Int -> Int -> Int := `(x,y) => x + y` data Nat : U where diff --git a/tests/black/Let.newt b/tests/black/Let.newt index f29206c..ac13584 100644 --- a/tests/black/Let.newt +++ b/tests/black/Let.newt @@ -1,6 +1,6 @@ module Let -ptype Int + foo : Int -> Int foo n = let x = 42 in x diff --git a/tests/black/Oper.newt b/tests/black/Oper.newt index 8d5282c..cab95b3 100644 --- a/tests/black/Oper.newt +++ b/tests/black/Oper.newt @@ -14,8 +14,8 @@ module Oper infixl 8 _+_ _-_ infixl 9 _*_ _/_ -ptype Int -ptype String + + ptype JVoid -- If we had a different quote here, we could tell vscode it's javascript. diff --git a/tests/black/TestCase.newt b/tests/black/TestCase.newt index ec04867..0506799 100644 --- a/tests/black/TestCase.newt +++ b/tests/black/TestCase.newt @@ -5,7 +5,7 @@ module TestCase -- There are indexes below, but we're got pulling constraints out of them yet. -ptype Int + data Nat : U where Z : Nat diff --git a/tests/black/TestCase4.newt b/tests/black/TestCase4.newt index 38054d3..c956b0b 100644 --- a/tests/black/TestCase4.newt +++ b/tests/black/TestCase4.newt @@ -51,7 +51,7 @@ transpose : {a : U} {m n : Nat} -> Vect m (Vect n a) -> Vect n (Vect m a) transpose {a} {Z} {n} Nil = vec n Nil transpose {a} {S z} {n} (_::_ {a'} {j} x xs) = zipWith (_::_) x (transpose xs) -ptype Int + myArr : Vect (S (S (S Z))) (Vect (S (S Z)) Int) myArr = (1 :: 2 :: Nil) :: (3 :: 4 :: Nil) :: (5 :: 6 :: Nil) :: Nil diff --git a/tests/black/TestCase5.newt b/tests/black/TestCase5.newt index a26eebb..82436ca 100644 --- a/tests/black/TestCase5.newt +++ b/tests/black/TestCase5.newt @@ -9,7 +9,7 @@ infixl 7 _+_ _+_ : {A : U} {{_ : Plus A}} -> A -> A -> A _+_ {{MkPlus plus}} x y = plus x y -ptype Int + pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y` PlusInt : Plus Int diff --git a/tests/black/TestPrim.newt b/tests/black/TestPrim.newt index 7de5eca..7283af4 100644 --- a/tests/black/TestPrim.newt +++ b/tests/black/TestPrim.newt @@ -4,8 +4,8 @@ module TestPrim -- we need to be able to declare a primitive type -- distinct from inductive type. there are no constructors per-se but it is inhabited -ptype String -ptype Int + + pfunc strlen : String -> Int := `(x) => x.length()` diff --git a/tests/black/TypeClass.newt b/tests/black/TypeClass.newt index ec5335a..e7bf1ad 100644 --- a/tests/black/TypeClass.newt +++ b/tests/black/TypeClass.newt @@ -63,7 +63,7 @@ infixr 1 _,_ data Pair : U -> U -> U where _,_ : ∀ A B. A -> B -> Pair A B -ptype Int + test : Maybe Int test = pure 10 diff --git a/tests/black/Zoo1.newt b/tests/black/Zoo1.newt index 1380d2d..f03826a 100644 --- a/tests/black/Zoo1.newt +++ b/tests/black/Zoo1.newt @@ -2,8 +2,8 @@ module Zoo1 -- I'm starting to translate ezoo 01-eval-closures-debruijn as a test cases. -ptype Int -ptype String + + ------- Prelude stuff