diff --git a/newt-vscode-lsp/src/lsp.ts b/newt-vscode-lsp/src/lsp.ts index c60b642..e2b3ecf 100644 --- a/newt-vscode-lsp/src/lsp.ts +++ b/newt-vscode-lsp/src/lsp.ts @@ -16,6 +16,7 @@ import { InitializeResult, TextDocumentSyncKind, Location, + TextDocumentIdentifier, } from "vscode-languageserver/node"; import { TextDocument } from "vscode-languageserver-textdocument"; @@ -24,10 +25,10 @@ const documents = new TextDocuments(TextDocument); // the last is the most important to the user, but we run FIFO // to ensure dependencies are seen in causal order -let changes: TextDocument[] = [] +let changes: (TextDocument|TextDocumentIdentifier)[] = [] let running = false let lastChange = 0 -function addChange(doc: TextDocument) { +function addChange(doc: TextDocument | TextDocumentIdentifier) { console.log('enqueue', doc.uri) // drop stale pending changes let before = changes.length @@ -94,15 +95,20 @@ connection.onHover((params): Hover | null => { console.log('HOVER', uri, pos) let res = LSP_hoverInfo(uri, pos.line, pos.character) if (!res) return null - console.log('HOVER is ', res) - return { contents: { kind: "plaintext", value: res.info } }; + if (res == true) { + addChange(params.textDocument) + return null + } else { + console.log('HOVER is ', res) + return { contents: { kind: "plaintext", value: res.info } }; + } }); connection.onDefinition((params): Location | null => { const uri = params.textDocument.uri; const pos = params.position; let value = LSP_hoverInfo(uri, pos.line, pos.character) - if (!value) return null; + if (!value || value == true) return null; return value.location }) diff --git a/newt-vscode-lsp/src/newt.d.ts b/newt-vscode-lsp/src/newt.d.ts index d22a4b5..7ae6b8b 100644 --- a/newt-vscode-lsp/src/newt.d.ts +++ b/newt-vscode-lsp/src/newt.d.ts @@ -6,5 +6,5 @@ interface HoverResult { info: string location: Location } -export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|null; +export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|boolean|null; export function LSP_codeActionInfo(name: string, row: number, col: number): CodeAction[]|null; diff --git a/newt-vscode-lsp/syntaxes/newt.tmLanguage.json b/newt-vscode-lsp/syntaxes/newt.tmLanguage.json index d494284..36ebd1d 100644 --- a/newt-vscode-lsp/syntaxes/newt.tmLanguage.json +++ b/newt-vscode-lsp/syntaxes/newt.tmLanguage.json @@ -20,7 +20,7 @@ }, { "name": "keyword.newt", - "match": "\\b(λ|=>|<-|->|→|:=|\\$|data|record|constructor|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + "match": "\\b(λ|=>|<-|->|→|:=|\\$|data|record|constructor|where|do|derive|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" }, { "name": "string.js", diff --git a/playground/src/cmeditor.ts b/playground/src/cmeditor.ts index c69c8c1..b38a50b 100644 --- a/playground/src/cmeditor.ts +++ b/playground/src/cmeditor.ts @@ -26,6 +26,7 @@ const keywords = [ "case", "of", "data", + "derive", "U", "do", "ptype", diff --git a/src/Commands.newt b/src/Commands.newt index 006edf2..40ff298 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -35,35 +35,38 @@ switchModule repo modns = do -- TODO processing on hover is expensive, but info is not always there -- I suspect this picks up the case where a file has been invalidated by a change to -- another file and we switch editors. Handle that (enqueue a check) and switch this back. + -- this is also broken, because diagnostics don't get updated.. top <- getTop - mod <- processModule emptyFC repo Nil modns - -- let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing + -- mod <- processModule emptyFC repo Nil modns + let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing modifyTop [ currentMod := mod; ops := mod.modOps ] pure $ Just mod +data HoverInfo = NoHoverInfo | NeedCheck | HasHover FC String + -- The cheap version of type at point, find the token, lookup in global context -- Later we will either get good FC for entries or scan them all and build a cache. -getHoverInfo : FileSource → String → Int → Int → M (Maybe (String × FC)) +getHoverInfo : FileSource → String → Int → Int → M HoverInfo getHoverInfo repo modns row col = do - Just mod <- switchModule repo modns | _ => pure Nothing + Just mod <- switchModule repo modns | _ => pure NeedCheck top <- getTop -- Find the token at the point let lines = split mod.modSource "\n" let line = fromMaybe "" (getAt' row lines) - let (Right toks) = tokenise "" line | Left _ => pure Nothing - let (Just name) = getTok toks | _ => pure Nothing + let (Right toks) = tokenise "" line | Left _ => pure NoHoverInfo + let (Just name) = getTok toks | _ => pure NoHoverInfo let (Left _) = partialParse "" parseImport emptyMap toks | Right ((MkImport _ (fc, nm)), _, _) => do let (baseDir, _) = splitFileName fc.file - let fc = MkFC (repo.baseDir ++ "/" ++ joinBy "/" (split nm ".")) (MkBounds 0 0 0 0) - pure $ Just ("module \{nm}", fc) - + let fc = MkFC ("\{repo.baseDir}/\{joinBy "/" (split nm ".")}.newt") (MkBounds 0 0 0 0) + pure $ HasHover fc "module \{nm}" + putStrLn "Hover name is \{show name}" -- Lookup the name - let (Just e) = lookupRaw name top | _ => pure Nothing + let (Just e) = lookupRaw name top | _ => pure NoHoverInfo ty <- nf Nil e.type - pure $ Just ("\{show e.name} : \{rpprint Nil ty}", e.fc) + pure $ HasHover e.fc ("\{show e.name} : \{rpprint Nil ty}") where getTok : List BTok → Maybe String @@ -140,7 +143,9 @@ makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do let phead = pack head let indent = getIndent 0 head let nextrow = scan indent lines (sr + 1) - + -- FIXME - doesn't handle `let`, but that's a little messy + -- need to remove let and add `|`, but also indent. + -- Existing `|` would have their own indent, indent of let matters. etc. -- No init or first :: rest for add missing case let (edits, rest) = doFirst inPlace cons @@ -193,8 +198,8 @@ getCaseSplit row col fc@(MkFC uri (MkBounds sr sc er ec)) ctx nm scty = do pure $ Just $ CaseSplitAction edits posInFC : Int → Int → FC → Bool --- FIXME ec + 1 again... -posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec + 1) +posInFC row col (MkFC _ (MkBounds 0 0 0 0)) = False +posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec) getHole : ModContext → Int → Int → Maybe MetaEntry getHole mod row col = @@ -243,7 +248,7 @@ introActions _ = pure Nil errorActions : Int → Int → Error → M (List CodeAction) errorActions row col err = do - let (ENotFound fc nm) = err | _ => pure Nil + let (ENotInScope fc nm) = err | _ => pure Nil let (True) = posInFC row col fc | _ => pure Nil top <- getTop let mods = map (\e => e.name.qns) $ lookupAll nm top diff --git a/src/LSP.newt b/src/LSP.newt index 9520db8..751c469 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -94,11 +94,15 @@ hoverInfo uri line col = unsafePerformIO $ do st <- readIORef state repo <- lspFileSource -- We're proactively running check if there is no module information, make sure we save it - Right (top, Just (msg, fc)) <- (getHoverInfo repo modns line col).runM st.topContext - | Right (top, _) => do + Right (top, HasHover fc msg) <- (getHoverInfo repo modns line col).runM st.topContext + | Right (top, NeedCheck) => do + modifyIORef state $ [ topContext := top ] + putStrLn $ "NeedsCheck" + pure $ js_castBool True + | Right (top, NoHoverInfo) => do modifyIORef state $ [ topContext := top ] putStrLn $ "Nothing to see here" - pure $ jsonToJObject JsonNull + pure $ js_castBool True | Left err => do putStrLn $ showError "" err pure $ jsonToJObject JsonNull diff --git a/src/Lib/Derive.newt b/src/Lib/Derive.newt new file mode 100644 index 0000000..72ae218 --- /dev/null +++ b/src/Lib/Derive.newt @@ -0,0 +1,151 @@ +module Lib.Derive + +import Prelude +import Lib.Common +import Lib.Types +import Lib.Syntax +import Lib.TopContext +import Lib.Error +import Lib.Elab -- (lookupDCon) +import Lib.Prettier + +-- describe type + +data Desc : U + +data DConst : U where + MkConst : (name : String) → List (String × Desc) → DConst + + +data Desc : U where + DInd : List DConst → Desc + +-- So I guess we do a few of these and then figure out how to make it easier + +deriveEq : FC → String → M (List Decl) +deriveEq fc name = do + top <- getTop + let (Just (MkEntry fc qname type (TCon _ names) eflags)) = lookupRaw name top + | Just _ => throwError $ E fc "\{name} is not a type constructor" + | _ => throwError $ ENotInScope fc name + dcons <- traverse lookupDCon names + clauses <- traverse makeClause dcons + let fallback = (buildApp "_==_" (rvar "_" :: rvar "_" :: Nil), Just (rvar "False")) + let eqDecl = FunDef fc "_==_" (snoc clauses fallback) + let inst = Instance fc (buildApp "Eq" (rvar name :: Nil)) (Just $ eqDecl :: Nil) + pure $ inst :: Nil + + where + arr : Raw → Raw → Raw + arr a b = RPi emptyFC (BI fc "_" Explicit Many) a b + + rvar : String → Raw + rvar nm = RVar emptyFC nm + + getExplictNames : SnocList String → Tm → List String + getExplictNames acc (Pi fc nm Explicit quant a b) = getExplictNames (acc :< nm) b + getExplictNames acc (Pi fc nm Implicit quant a b) = getExplictNames acc b + getExplictNames acc (Pi fc nm Auto quant a b) = getExplictNames acc b + getExplictNames acc _ = acc <>> Nil + + buildApp : String → List Raw → Raw + buildApp nm nms = foldl (\ t u => RApp emptyFC t u Explicit) (rvar nm) $ nms + + equate : (Raw × Raw) → Raw + equate (a,b) = buildApp "_==_" (a :: b :: Nil) + + makeClause : (QName × Int × Tm) → M (Raw × Maybe Raw) + makeClause ((QN ns nm), _, ty) = do + -- We're only looking at explicit args for now. + -- TODO check quantity + let names = getExplictNames Lin ty + anames <- map rvar <$> traverse freshName names + bnames <- map rvar <$> traverse freshName names + let a = buildApp nm anames + let b = buildApp nm bnames + + let left = equate (a,b) + let right = case map equate $ zip anames bnames of + Nil => rvar "True" + (hd :: tl) => foldr (\a b => buildApp "_&&_" (a :: b :: Nil)) hd tl + + pure (left, Just right) + + +-- This is a little more of a pain, we'll generate a number for each constructor +-- and use that as the fallback. Eventually we'll want something like quasi-quote +deriveShow : FC → String → M (List Decl) +deriveShow fc name = do + top <- getTop + let (Just (MkEntry fc qname type (TCon _ names) eflags)) = lookupRaw name top + | Just _ => throwError $ E fc "\{name} is not a type constructor" + | _ => throwError $ ENotInScope fc name + dcons <- traverse lookupDCon names + clauses <- traverse makeClause dcons + + let eqDecl = FunDef fc "show" clauses + let inst = Instance fc (buildApp "Show" (rvar name :: Nil)) (Just $ eqDecl :: Nil) + pure $ inst :: Nil + + where + arr : Raw → Raw → Raw + arr a b = RPi emptyFC (BI fc "_" Explicit Many) a b + + rvar : String → Raw + rvar nm = RVar emptyFC nm + + lstring : String → Raw + lstring s = RLit emptyFC (LString s) + + getExplictNames : SnocList String → Tm → List String + getExplictNames acc (Pi fc nm Explicit quant a b) = getExplictNames (acc :< nm) b + getExplictNames acc (Pi fc nm Implicit quant a b) = getExplictNames acc b + getExplictNames acc (Pi fc nm Auto quant a b) = getExplictNames acc b + getExplictNames acc _ = acc <>> Nil + + buildApp : String → List Raw → Raw + buildApp nm nms = foldl (\ t u => RApp emptyFC t u Explicit) (rvar nm) $ nms + + equate : (Raw × Raw) → Raw + equate (a,b) = buildApp "_==_" (a :: b :: Nil) + + makeList : List Raw → Raw + makeList Nil = rvar "Nil" + makeList (x :: xs) = buildApp "_::_" (x :: makeList xs :: Nil) + + makeClause : (QName × Int × Tm) → M (Raw × Maybe Raw) + makeClause ((QN ns nm), _, ty) = do + let names = getExplictNames Lin ty + anames <- map rvar <$> traverse freshName names + let left = buildApp "show" $ buildApp nm anames :: Nil + let shows = map (\ nm => RApp emptyFC (rvar "show") nm Explicit) anames + let right = case anames of + Nil => lstring nm + _ => + let parts = makeList $ lstring ("(" ++ nm) :: shows in + buildApp "_++_" $ buildApp "joinBy" (lstring " " :: parts :: Nil) :: lstring ")" :: Nil + + pure (left, Just right) + + + +-- -- A description would be nice. +-- deriveShow : FC → QName → M Raw +-- deriveShow fc qn = do +-- top <- getTop +-- case lookup qn top : Maybe TopEntry of +-- Nothing => error {Raw} fc "Can't find \{show qn} in derive Show" +-- -- I want case split too... I need to tie the editor into the repl. +-- (Just (MkEntry fc name type (TCon _ conNames) eflags) ) => ? +-- (Just (MkEntry fc name type (Axiom) eflags) ) => ? +-- (Just (MkEntry fc name type (DCon _ _ _ _) eflags) ) => ? +-- (Just (MkEntry fc name type (Fn _) eflags) ) => ? +-- (Just (MkEntry fc name type (PrimTCon _) eflags) ) => ? +-- (Just (MkEntry fc name type (PrimFn _ _ _) eflags) ) => ? +-- (Just (MkEntry fc name type (PrimOp _) eflags) ) => ? + +-- error fc "TODO" + + +-- HasFC as example of user-defined derivation (when we get to that) +-- SetFC would be nice, too. diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 1327991..bffc9f1 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1544,8 +1544,10 @@ infer ctx (RVar fc nm) = go 0 ctx.types debug $ \ _ => "lookup \{show name} as \{show def}" vty <- eval Nil ty pure (Ref fc name, vty) - -- Can we soften this without introducing a meta? - Nothing => throwError $ ENotFound fc nm + -- Can we soften this without introducing a meta for the type + -- it might be additional errors, but also could lead to narrowing of possible names... + -- especially when we hit this for .foo + Nothing => throwError $ ENotInScope fc nm go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty) else go (i + 1) xs diff --git a/src/Lib/Error.newt b/src/Lib/Error.newt index b8c91a2..2efe79f 100644 --- a/src/Lib/Error.newt +++ b/src/Lib/Error.newt @@ -7,18 +7,18 @@ import Lib.Common -- and a pretty printer in the monad data Error = E FC String - | ENotFound FC String + | ENotInScope FC String | Postpone FC QName String instance HasFC Error where getFC (E x str) = x - getFC (ENotFound x _) = x + getFC (ENotInScope x _) = x getFC (Postpone x k str) = x errorMsg : Error -> String errorMsg (E x str) = str -errorMsg (ENotFound x nm) = "\{nm} not in scope" +errorMsg (ENotInScope x nm) = "\{nm} not in scope" errorMsg (Postpone x k str) = str showError : (src : String) -> Error -> String diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index 2769192..59e8c59 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -538,8 +538,11 @@ parseImport = do -- TODO revisit when we have parser for qualified names in source (nameFC, ident) <- withFC uident (restFC,rest) <- withFC $ many $ token Projection + let nameFC = case rest of + Nil => nameFC + (_ :: _) => nameFC + restFC let name = joinBy "" (ident :: rest) - pure $ MkImport fc (nameFC + restFC, name) + pure $ MkImport fc (nameFC, name) -- Do we do pattern stuff now? or just name = lambda? -- TODO multiple names @@ -679,11 +682,19 @@ parseExport = do names <- many $ withFC ident pure $ Exports loc names +parseDerive : Parser Decl +parseDerive = do + loc <- getPos + keyword "derive" + className <- withFC uident + name <- withFC uident + pure $ DDerive loc className name + parseDecl : Parser Decl parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseData <|> parseShortData <|> parseClass <|> parseInstance <|> parseRecord - <|> parseExport + <|> parseExport <|> parseDerive -- We'll put the backtracing stuff last, but there is a commit issue in parseDef <|> parseSig <|> parseDef diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index 179efc6..af5350a 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -16,6 +16,7 @@ import Lib.Prettier import Lib.Types import Lib.Util import Lib.Erasure +import Lib.Derive dumpEnv : Context -> M String dumpEnv ctx = @@ -529,6 +530,17 @@ processRecord ns recordFC (nameFC, nm) tele cname decls = do let deps = ((name, RApp fc (RVar fc pname) (RVar fc "$self") Explicit) :: deps) processFields autoPat tail deps rest +processDerive : String → FC → FC × String → (FC × String) → M Unit +processDerive ns fc (clFC, clName) (fc, name) = do + case clName of + "Eq" => do + decls <- deriveEq fc name + for_ decls $ processDecl ns + "Show" => do + decls <- deriveShow fc name + for_ decls $ processDecl ns + _ => error fc "derive \{clName} is not supported" + processExports : String → FC → List (FC × String) → M Unit processExports ns fc names = do top <- getTop @@ -542,6 +554,7 @@ processExports ns fc names = do -- currently mixfix registration is handled in the parser -- since we now run a decl at a time we could do it here. processDecl ns (PMixFix _ _ _ _) = pure MkUnit +processDecl ns (DDerive fc tclass name) = processDerive ns fc tclass name processDecl ns (TypeSig fc names tm) = processTypeSig ns fc names tm processDecl ns (PType fc nm ty) = processPrimType ns fc nm ty processDecl ns (PFunc fc nm used ty src) = processPrimFn ns fc nm used ty src diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index 14d93c4..53aaf87 100644 --- a/src/Lib/Syntax.newt +++ b/src/Lib/Syntax.newt @@ -88,6 +88,7 @@ data Decl = TypeSig FC (List Name) Raw | FunDef FC Name (List (Raw × Maybe Raw)) | DCheck FC Raw Raw + | DDerive FC (FC × String) (FC × String) -- TODO maybe add Telescope (before `:`) and auto-add to constructors... | Data FC (FC × Name) Raw (Maybe $ List Decl) | ShortData FC Raw (List Raw) @@ -113,6 +114,7 @@ instance HasFC Decl where getFC (Class x str xs ys) = x getFC (Instance x tm xs) = x getFC (Record x str tm str1 xs) = x + getFC (DDerive x _ _) = x record Module where @@ -126,7 +128,6 @@ foo ts = "(" ++ unwords ts ++ ")" instance Show Raw - instance Show Clause where show (MkClause fc cons pats expr) = show (fc, cons, pats, expr) @@ -140,6 +141,7 @@ instance Show BindInfo where instance Show Decl where show (TypeSig _ str x) = foo ("TypeSig" :: show str :: show x :: Nil) + show (DDerive _ x y) = foo ("DDerive" :: show x :: show y :: Nil) show (FunDef _ str clauses) = foo ("FunDef" :: show str :: show clauses :: Nil) show (Data _ str xs ys) = foo ("Data" :: show str :: show xs :: show ys :: Nil) show (DCheck _ x y) = foo ("DCheck" :: show x :: show y :: Nil) @@ -248,6 +250,7 @@ pipeSep = folddoc (\a b => a <+/> text "|" <+> b) instance Pretty Decl where pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty) + pretty (DDerive _ x y) = text "derive" <+> text (snd x) <+> text (snd y) pretty (FunDef _ nm clauses) = stack $ map prettyPair clauses where prettyPair : Raw × Maybe Raw → Doc @@ -264,7 +267,8 @@ instance Pretty Decl where <+> (nest 2 $ text "where" stack (maybe empty (\ nm' => text "constructor" <+> text (snd nm')) cname :: map pretty decls)) pretty (Class _ (_,nm) tele decls) = text "class" <+> text nm <+> text ":" <+> spread (map prettyBind tele) <+> (nest 2 $ text "where" stack (map pretty decls)) - pretty (Instance _ _ _) = text "TODO pretty Instance" + pretty (Instance fc top Nothing) = text "instance" <+> pretty top + pretty (Instance fc top (Just decls)) = text "instance" <+> pretty top <+> nest 2 (text "where" stack (map pretty decls)) pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) pretty (Exports _ nms) = text "#export" <+> spread (map (text ∘ show ∘ snd) nms) diff --git a/src/Lib/Tokenizer.newt b/src/Lib/Tokenizer.newt index 7109be9..aee1014 100644 --- a/src/Lib/Tokenizer.newt +++ b/src/Lib/Tokenizer.newt @@ -20,7 +20,7 @@ standalone = unpack "()\\{}[],.@;" keywords : List String keywords = ("let" :: "in" :: "where" :: "case" :: "of" :: "data" :: "U" :: "do" :: "ptype" :: "pfunc" :: "module" :: "infixl" :: "infixr" :: "infix" :: - "∀" :: "forall" :: "import" :: "uses" :: + "∀" :: "forall" :: "import" :: "uses" :: "derive" :: "class" :: "instance" :: "record" :: "constructor" :: "if" :: "then" :: "else" :: -- it would be nice to find a way to unkeyword "." so it could be diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index d48201e..20e2964 100644 --- a/src/Lib/TopContext.newt +++ b/src/Lib/TopContext.newt @@ -46,7 +46,7 @@ instance Show TopContext where show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.currentMod.modDefs}]" emptyTop : TopContext -emptyTop = MkTop emptyMap emptyMap (emptyModCtx "" "") 0 emptyMap +emptyTop = MkTop emptyMap emptyMap (emptyModCtx "" "") 0 emptyMap 0 setFlag : QName → FC → EFlag → M Unit setFlag name fc flag = do @@ -94,3 +94,10 @@ addError err = modifyTop [ currentMod $= [ modErrors $= (err ::) ] ] addInfo : EditorInfo → M Unit addInfo info = modifyTop [ currentMod $= [modInfos $= (info ::) ] ] + +-- temporary? used in derive for now +freshName : String → M String +freshName nm = do + top <- getTop + modifyTop [ freshIx $= 1 + ] + pure $ "f$" ++ nm ++ show top.freshIx diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 0818801..24a22b0 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -81,7 +81,7 @@ data Tm : U where Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Tm UU : FC -> Tm - Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm + Pi : (fc : FC) -> (nm : Name) -> Icit -> Quant -> (a : Tm) -> (b : Tm) -> Tm Case : FC -> Tm -> List CaseAlt -> Tm -- need type? Let : FC -> Name -> Tm -> Tm -> Tm @@ -442,6 +442,7 @@ record TopContext where currentMod : ModContext verbose : Int -- command line flag increments this ops : Operators + freshIx : Int -- we'll use this for typechecking, but need to keep a TopContext around too. @@ -594,6 +595,8 @@ lookupMeta ix@(QN ns nm) = do mkCtx : FC -> Context mkCtx fc = MkCtx 0 Nil Nil Nil fc +-- Used by Syntax and Elab + data Pattern = PatVar FC Icit Name | PatCon FC Icit QName (List Pattern) (Maybe Name) @@ -627,8 +630,8 @@ instance Show Constraint where show (PC nm pat ty) = show (nm,pat,ty) -- Lazy because `let` would do work at the top of a `M a` -prof : ∀ a. String → Lazy (M a) → M a -prof desc work = do +profile : ∀ a. String → Lazy (M a) → M a +profile desc work = do start <- getTime res <- force work end <- getTime diff --git a/tests/Derive.newt b/tests/Derive.newt new file mode 100644 index 0000000..789297b --- /dev/null +++ b/tests/Derive.newt @@ -0,0 +1,14 @@ +module Derive + +import Prelude + +data Blah = Foo Int | Bar | Baz String + +derive Eq Blah +derive Show Blah + +main : IO Unit +main = do + printLn $ Foo 42 + printLn $ Bar + printLn $ Baz "woo" diff --git a/tests/Derive.newt.golden b/tests/Derive.newt.golden new file mode 100644 index 0000000..66b5863 --- /dev/null +++ b/tests/Derive.newt.golden @@ -0,0 +1,3 @@ +(Foo 42) +Bar +(Baz woo) diff --git a/tests/ImportError.newt b/tests/ImportError.newt new file mode 100644 index 0000000..0bf7c76 --- /dev/null +++ b/tests/ImportError.newt @@ -0,0 +1,7 @@ +module ImportError + +-- test the FC are right and don't include next line +-- TODO continue on and hit the next one. +import Blah +import Foo.Bar +import Prelude diff --git a/tests/ImportError.newt.fail b/tests/ImportError.newt.fail new file mode 100644 index 0000000..d626657 --- /dev/null +++ b/tests/ImportError.newt.fail @@ -0,0 +1,2 @@ +*** Process tests/ImportError.newt +ERROR at tests/ImportError.newt:5:8--5:12: error reading tests/Blah.newt: Error: ENOENT: no such file or directory, open 'tests/Blah.newt' diff --git a/tests/UnsafeIO.newt b/tests/UnsafeIO.newt new file mode 100644 index 0000000..b6ebd3b --- /dev/null +++ b/tests/UnsafeIO.newt @@ -0,0 +1,8 @@ +module UnsafeIO + +import Prelude + +main : IO Unit +main = do + let x = unsafePerformIO $ putStrLn "Hello, World!" + pure MkUnit diff --git a/tests/UnsafeIO.newt.golden b/tests/UnsafeIO.newt.golden new file mode 100644 index 0000000..8ab686e --- /dev/null +++ b/tests/UnsafeIO.newt.golden @@ -0,0 +1 @@ +Hello, World!