diff --git a/README.md b/README.md index 663ed4e..1d5217f 100644 --- a/README.md +++ b/README.md @@ -9,10 +9,7 @@ It has inductive types, dependent pattern matching, a typeclass-like mechanism, to javascript, and is now written in itself. There is a browser playground and vscode extension. The web playground can be at https://dunhamsteve.github.io/newt. The top left corner -has a dropdown with some samples. Currently the web playground is using the Idris-built -version of newt because most browsers lack tail call optimization. - -The directory `orig` contains the original version of newt written in Idris. It is used by the playground until TCO is added to newt. +has a dropdown with some sample code, including `newt` itself. ## Sample code @@ -23,11 +20,11 @@ The directory `orig` contains the original version of newt written in Idris. It ## Building -The `Makefile` will build both the original Idris version of `newt`, which will end up in `build/exec` and the current version of newt, which will be `./newt.js`. There is a `pack.toml` file to allow building the original version of newt with `pack build`. +The `Makefile` will build builds `./newt.js`. There is a bootstrap version of newt in `bootstrap/newt.js`. -Newt can also be built by running `bun run bootstrap/newt.js src/Main.newt -o newt.js`. +Newt can also be built by running `node bootstrap/newt.js src/Main.newt -o newt.js`. -There is a vscode extension in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output format is in flux. +The source for the vscode extension is found in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output format is in flux. ## Playground diff --git a/newt-vscode/package.json b/newt-vscode/package.json index bc78194..5069f7b 100644 --- a/newt-vscode/package.json +++ b/newt-vscode/package.json @@ -61,8 +61,8 @@ "properties": { "newt.path": { "type": "string", - "default": "build/exec/newt", - "description": "Path to the newt executable" + "default": "node bootstrap/newt.js", + "description": "Command to run newt" } } } diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 41587af..ede0caa 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -32,7 +32,6 @@ export function activate(context: vscode.ExtensionContext) { const lastChange = changes[changes.length - 1]; const text = lastChange.text; - console.log("lastChange", lastChange) // Check if the last change is a potential shortcut trigger if (!text || !( " ')\\".includes(text) || text.startsWith('\n'))) return; @@ -70,8 +69,7 @@ export function activate(context: vscode.ExtensionContext) { ? workspaceFolder.uri.fsPath : path.dirname(fileName); const config = vscode.workspace.getConfiguration("newt"); - // FIXME wrong newt now. - const cmd = config.get("path", "build/exec/newt"); + const cmd = config.get("path", "node bootstrap/newt.js"); const command = `${cmd} --top ${fileName}`; let st = +new Date(); exec( diff --git a/newt.ipkg b/newt.ipkg deleted file mode 100644 index 5d0886b..0000000 --- a/newt.ipkg +++ /dev/null @@ -1,59 +0,0 @@ -package newt -version = 0.1.0 -authors = "Steve Dunham" --- maintainers = --- license = --- brief = --- readme = --- homepage = --- sourceloc = --- bugtracker = - --- the Idris2 version required (e.g. langversion >= 0.5.1) --- langversion - --- packages to add to search path -depends = contrib, base - --- modules to install -modules = - Lib.Elab, - Lib.Parser, - Lib.Parser.Impl, - Lib.Prettier, - Lib.ProcessDecl, - Lib.Syntax, - Lib.Common, - Lib.Eval, - Lib.Token, - Lib.TopContext, - Lib.Types, - Lib.Util - --- main file (i.e. file to load at REPL) -main = Main - --- name of executable -executable = "newt" --- opts = -sourcedir = "orig" --- builddir = --- outputdir = - --- script to run before building --- prebuild = - --- script to run after building --- postbuild = - --- script to run after building, before installing --- preinstall = - --- script to run after installing --- postinstall = - --- script to run before cleaning --- preclean = - --- script to run after cleaning --- postclean = diff --git a/orig/Lib/Common.idr b/orig/Lib/Common.idr deleted file mode 100644 index e58cc3a..0000000 --- a/orig/Lib/Common.idr +++ /dev/null @@ -1,154 +0,0 @@ -module Lib.Common - -import Data.String -import Data.Nat -import Data.Maybe -import public Data.SortedMap - --- l is environment size, this works for both lvl2ix and ix2lvl -public export -lvl2ix : Nat -> Nat -> Nat -lvl2ix l k = minus (minus l k) 1 - -hexChars : List Char -hexChars = unpack "0123456789ABCDEF" - --- export -hexDigit : Nat -> Char -hexDigit v = fromMaybe ' ' (getAt (mod v 16) hexChars) - -export -toHex : Nat -> List Char -toHex 0 = [] -toHex v = snoc (toHex (div v 16)) (hexDigit v) - -export -quoteString : String -> String -quoteString str = pack $ encode (unpack str) [< '"'] - where - encode : List Char -> SnocList Char -> List Char - encode [] acc = acc <>> ['"'] - encode ('"' :: cs) acc = encode cs (acc :< '\\' :< '"') - encode ('\n' :: cs) acc = encode cs (acc :< '\\' :< 'n') - encode ('\\' :: cs) acc = encode cs (acc :< '\\' :< '\\') - encode (c :: cs) acc = - let v : Nat = cast c in - if v < 32 then encode cs (acc :< '\\' :< 'u' :< hexDigit (div v 4096) :< hexDigit (div v 256) :< hexDigit (div v 16) :< hexDigit v ) - else encode cs (acc :< c) - -public export -data Json : Type where - JsonObj : List (String, Json) -> Json - JsonStr : String -> Json - JsonBool : Bool -> Json - JsonInt : Int -> Json - JsonArray : List Json -> Json - -export -renderJson : Json -> String -renderJson (JsonObj xs) = "{" ++ joinBy "," (map renderPair xs) ++ "}" - where - renderPair : (String,Json) -> String - renderPair (k,v) = quoteString k ++ ":" ++ renderJson v -renderJson (JsonStr str) = quoteString str -renderJson (JsonBool x) = ifThenElse x "true" "false" -renderJson (JsonInt i) = cast i -renderJson (JsonArray xs) = "[" ++ joinBy "," (map renderJson xs) ++ "]" - -public export -interface ToJSON a where - toJson : a -> Json - -export -ToJSON String where - toJson = JsonStr - -export -ToJSON Int where - toJson = JsonInt - -public export -record FC where - constructor MkFC - file : String - start : (Int,Int) - -export -ToJSON FC where - toJson (MkFC file (line,col)) = JsonObj (("file", toJson file) :: ("line", toJson line) :: ("col", toJson col) :: Nil) - -export -fcLine : FC -> Int -fcLine (MkFC file (l, c)) = l - -export -fcCol : FC -> Int -fcCol (MkFC file (l, c)) = c - -public export -interface HasFC a where - getFC : a -> FC - -%name FC fc - -export -emptyFC : FC -emptyFC = MkFC "" (0,0) - --- Error of a parse -public export -data Error - = E FC String - | Postpone FC Nat String -%name Error err - -export -Show FC where - show fc = "\{fc.file}:\{show fc.start}" - -public export -showError : String -> Error -> String -showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src) - where - go : Int -> List String -> String - go l [] = "" - go l (x :: xs) = - if l == fcLine fc then - " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" - else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs - else go (l + 1) xs -showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src) - where - go : Int -> List String -> String - go l [] = "" - go l (x :: xs) = - if l == fcLine fc then - " \{x}\n \{replicate (cast $ fcCol fc) ' '}^\n" - else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs - else go (l + 1) xs - -public export -data Fixity = InfixL | InfixR | Infix - -export -Show Fixity where - show InfixL = "infixl" - show InfixR = "infixr" - show Infix = "infix" - - -public export -record OpDef where - constructor MkOp - opname : String - prec : Int - fix : Fixity - isPrefix : Bool - ||| rule is everything after the first part of the operator, splitting on `_` - ||| a normal infix operator will have a trailing `""` which will match to - ||| prec / prec - 1 - rule : List String - -public export -Operators : Type -Operators = SortedMap String OpDef diff --git a/orig/Lib/Compile.idr b/orig/Lib/Compile.idr deleted file mode 100644 index 20ef115..0000000 --- a/orig/Lib/Compile.idr +++ /dev/null @@ -1,349 +0,0 @@ --- TODO Audit how much "outside" stuff could pile up in the continuation. -module Lib.Compile - -import Lib.Types -import Lib.Prettier -import Lib.CompileExp -import Lib.TopContext -import Data.String -import Data.Maybe -import Data.Nat - -data Kind = Plain | Return | Assign String - -data JSStmt : Kind -> Type -data JSExp : Type - -data JAlt : Type where - JConAlt : String -> JSStmt e -> JAlt - JDefAlt : JSStmt e -> JAlt - JLitAlt : JSExp -> JSStmt e -> JAlt - -data JSExp : Type where - LitArray : List JSExp -> JSExp - LitObject : List (String, JSExp) -> JSExp - LitString : String -> JSExp - LitInt : Int -> JSExp - Apply : JSExp -> List JSExp -> JSExp - Var : String -> JSExp - JLam : List String -> JSStmt Return -> JSExp - JUndefined : JSExp - Index : JSExp -> JSExp -> JSExp - Dot : JSExp -> String -> JSExp - -data JSStmt : Kind -> Type where - -- Maybe make this a snoc... - JSnoc : JSStmt Plain -> JSStmt a -> JSStmt a - JPlain : JSExp -> JSStmt Plain - JConst : (nm : String) -> JSExp -> JSStmt Plain - JReturn : JSExp -> JSStmt Return - JLet : (nm : String) -> JSStmt (Assign nm) -> JSStmt Plain -- need somebody to assign - JAssign : (nm : String) -> JSExp -> JSStmt (Assign nm) - -- TODO - switch to Nat tags - -- FIXME add e to JAlt (or just drop it?) - JCase : JSExp -> List JAlt -> JSStmt a - -- throw can't be used - JError : String -> JSStmt a - -Cont e = JSExp -> JSStmt e - -||| JSEnv contains `Var` for binders or `Dot` for destructured data. It -||| used to translate binders -record JSEnv where - constructor MkEnv - env : List JSExp - depth : Nat - -push : JSEnv -> JSExp -> JSEnv -push env exp = { env $= (exp ::) } env - -empty : JSEnv -empty = MkEnv [] Z - -litToJS : Literal -> JSExp -litToJS (LString str) = LitString str -litToJS (LChar c) = LitString $ cast c -litToJS (LInt i) = LitInt i - --- Stuff nm.h1, nm.h2, ... into environment --- TODO consider JSExp instead of nm, so we can have $foo.h1 instead of assigning a sc. -mkEnv : String -> Nat -> JSEnv -> List String -> JSEnv -mkEnv nm k env [] = env -mkEnv nm k env (x :: xs) = mkEnv nm (S k) (push env (Dot (Var nm) "h\{show k}")) xs - -envNames : Env -> List String - -||| given a name, find a similar one that doesn't shadow in Env -freshName : String -> JSEnv -> String -freshName nm env = if free env.env nm then nm else go nm 1 - where - free : List JSExp -> String -> Bool - free [] nm = True - free (Var n :: xs) nm = if n == nm then False else free xs nm - free (_ :: xs) nm = free xs nm - - go : String -> Nat -> String - go nm k = let nm' = "\{nm}\{show k}" in if free env.env nm' then nm' else go nm (S k) - -freshName' : String -> JSEnv -> (String, JSEnv) -freshName' nm env = - let nm' = freshName nm env -- "\{nm}$\{show $ length env}" - env' = push env (Var nm') - in (nm', env') - -freshNames : List String -> JSEnv -> (List String, JSEnv) -freshNames nms env = go nms env [<] - where - go : List Name -> JSEnv -> SnocList Name -> (List String, JSEnv) - go Nil env acc = (acc <>> Nil, env) - go (n :: ns) env acc = - let (n', env') = freshName' n env - in go ns env' (acc :< n') - --- This is inspired by A-normalization, look into the continuation monad --- There is an index on JSStmt, adopted from Stefan Hoeck's code. --- --- Here we turn a Term into a statement (which may be a sequence of statements), there --- is a continuation, which turns the final JSExpr into a JSStmt, and the function returns --- a JSStmt, wrapping recursive calls in JSnoc if necessary. -termToJS : JSEnv -> CExp -> Cont e -> JSStmt e -termToJS env (CBnd k) f = case getAt k env.env of - (Just e) => f e - Nothing => ?bad_bounds -termToJS env CErased f = f JUndefined -termToJS env (CLam nm t) f = - let (nm',env') = freshName' nm env -- "\{nm}$\{show $ length env}" - in f $ JLam [nm'] (termToJS env' t JReturn) -termToJS env (CFun nms t) f = - let (nms', env') = freshNames nms env - in f $ JLam nms' (termToJS env' t JReturn) -termToJS env (CRef nm) f = f $ Var nm -termToJS env (CMeta k) f = f $ LitString "META \{show k}" -termToJS env (CLit lit) f = f (litToJS lit) --- if it's a var, just use the original -termToJS env (CLet nm (CBnd k) u) f = case getAt k env.env of - Just e => termToJS (push env e) u f - Nothing => ?bad_bounds2 -termToJS env (CLet nm t u) f = - let nm' = freshName nm env - env' = push env (Var nm') - -- If it's a simple term, use const - in case termToJS env t (JAssign nm') of - (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) - t' => JSnoc (JLet nm' t') (termToJS env' u f) -termToJS env (CLetRec nm t u) f = - let nm' = freshName nm env - env' = push env (Var nm') - -- If it's a simple term, use const - in case termToJS env' t (JAssign nm') of - (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) - t' => JSnoc (JLet nm' t') (termToJS env' u f) - -termToJS env (CApp t args etas) f = termToJS env t (\ t' => (argsToJS t' args [<] f)) -- (f (Apply t' args')))) - where - etaExpand : JSEnv -> Nat -> SnocList JSExp -> JSExp -> JSExp - etaExpand env Z args tm = Apply tm (args <>> []) - etaExpand env (S etas) args tm = - let nm' = freshName "eta" env - env' = push env (Var nm') - in JLam [nm'] $ JReturn $ etaExpand (push env (Var nm')) etas (args :< Var nm') tm - - argsToJS : JSExp -> List CExp -> SnocList JSExp -> (JSExp -> JSStmt e) -> JSStmt e - argsToJS tm [] acc k = k (etaExpand env etas acc tm) - -- k (acc <>> []) - argsToJS tm (x :: xs) acc k = termToJS env x (\ x' => argsToJS tm xs (acc :< x') k) - - -termToJS env (CCase t alts) f = - -- need to assign the scrutinee to a variable (unless it is a var already?) - -- and add (Bnd -> JSExpr map) - -- TODO default case, let's drop the extra field. - - termToJS env t $ \case - (Var nm) => maybeCaseStmt env nm alts - t' => do - -- TODO refactor nm to be a JSExp with Var{} or Dot{} - -- FIXME sc$ seemed to shadow something else, lets get this straightened out - -- we need freshName names that are not in env (i.e. do not play in debruijn) - let nm = "_sc$\{show env.depth}" - let env' = { depth $= S } env - JSnoc (JConst nm t') (maybeCaseStmt env' nm alts) - - where - termToJSAlt : JSEnv -> String -> CAlt -> JAlt - termToJSAlt env nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) - -- intentionally reusing scrutinee name here - termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (env) u f) - termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f) - - maybeCaseStmt : JSEnv -> String -> List CAlt -> JSStmt e - -- If there is a single alt, assume it matched - maybeCaseStmt env nm [(CConAlt _ args u)] = (termToJS (mkEnv nm 0 env args) u f) - maybeCaseStmt env nm alts@(CLitAlt _ _ :: _) = - (JCase (Var nm) (map (termToJSAlt env nm) alts)) - maybeCaseStmt env nm alts = - (JCase (Dot (Var nm) "tag") (map (termToJSAlt env nm) alts)) - -jsKeywords : List String -jsKeywords = [ - "break", "case", "catch", "continue", "debugger", "default", "delete", "do", "else", - "finally", "for", "function", "if", "in", "instanceof", "new", "return", "switch", - "this", "throw", "try", "typeof", "var", "void", "while", "with", - "class", "const", "enum", "export", "extends", "import", "super", - "implements", "interface", "let", "package", "private", "protected", "public", - "static", "yield", - "null", "true", "false", - -- might not be a big issue with namespaces on names now. - "String", "Number", "Array", "BigInt" -] - -||| escape identifiers for js -jsIdent : String -> Doc -jsIdent id = if elem id jsKeywords then text ("$" ++ id) else text $ pack $ fix (unpack id) - where - fix : List Char -> List Char - fix [] = [] - 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 - '$' :: (toHex (cast x)) ++ fix xs - -stmtToDoc : JSStmt e -> Doc - - -expToDoc : JSExp -> Doc -expToDoc (LitArray xs) = ?expToDoc_rhs_0 -expToDoc (LitObject xs) = text "{" <+> folddoc (\ a, e => a ++ text ", " <+/> e) (map entry xs) <+> text "}" - where - entry : (String, JSExp) -> Doc - -- TODO quote if needed - entry (nm, exp) = jsIdent nm ++ text ":" <+> expToDoc exp - -expToDoc (LitString str) = text $ quoteString str -expToDoc (LitInt i) = text $ show i --- TODO add precedence -expToDoc (Apply x@(JLam{}) xs) = text "(" ++ expToDoc x ++ text ")" ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" -expToDoc (Apply x xs) = expToDoc x ++ text "(" ++ nest 2 (commaSep (map expToDoc xs)) ++ text ")" -expToDoc (Var nm) = jsIdent nm -expToDoc (JLam nms (JReturn exp)) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> text "(" ++ expToDoc exp ++ text ")" -expToDoc (JLam nms body) = text "(" <+> commaSep (map jsIdent nms) <+> text ") =>" <+> bracket "{" (stmtToDoc body) "}" -expToDoc JUndefined = text "null" -expToDoc (Index obj ix) = expToDoc obj ++ text "[" ++ expToDoc ix ++ text "]" -expToDoc (Dot obj nm) = expToDoc obj ++ text "." ++ jsIdent nm - -caseBody : JSStmt e -> Doc -caseBody stmt@(JReturn x) = nest 2 (line ++ stmtToDoc stmt) --- caseBody {e = Return} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt) -caseBody {e} stmt@(JCase{}) = nest 2 (line ++ stmtToDoc stmt text "break;") -caseBody stmt = line ++ text "{" ++ nest 2 (line ++ stmtToDoc stmt text "break;") text "}" - -altToDoc : JAlt -> Doc -altToDoc (JConAlt nm stmt) = text "case" <+> text (quoteString nm) ++ text ":" ++ caseBody stmt -altToDoc (JDefAlt stmt) = text "default" ++ text ":" ++ caseBody stmt -altToDoc (JLitAlt a stmt) = text "case" <+> expToDoc a ++ text ":" ++ caseBody stmt - -stmtToDoc (JSnoc x y) = stmtToDoc x stmtToDoc y -stmtToDoc (JPlain x) = expToDoc x ++ text ";" --- I might not need these split yet. -stmtToDoc (JLet nm body) = text "let" <+> jsIdent nm ++ text ";" stmtToDoc body -stmtToDoc (JAssign nm expr) = jsIdent nm <+> text "=" <+> expToDoc expr ++ text ";" -stmtToDoc (JConst nm x) = text "const" <+> jsIdent nm <+> nest 2 (text "=" <+/> expToDoc x ++ text ";") -stmtToDoc (JReturn x) = text "return" <+> expToDoc x ++ text ";" -stmtToDoc (JError str) = text "throw new Error(" ++ text (quoteString str) ++ text ");" -stmtToDoc (JCase sc alts) = - text "switch (" ++ expToDoc sc ++ text ")" <+> bracket "{" (stack $ map altToDoc alts) "}" - -mkArgs : Nat -> List String -> List String -mkArgs Z acc = acc -mkArgs (S k) acc = mkArgs k ("h\{show k}" :: acc) - -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 (show qn) (JLam args (JReturn (LitObject obj))) - --- use iife to turn stmts into expr -maybeWrap : JSStmt Return -> JSExp -maybeWrap (JReturn exp) = exp -maybeWrap stmt = Apply (JLam [] stmt) [] - -entryToDoc : TopEntry -> M Doc -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 (show name) <+> text "=" <+/> expToDoc exp ++ text ";" -entryToDoc (MkEntry _ name type Axiom) = pure $ text "" -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 (show name) <+> text "=" <+> 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 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 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 (show name) <+> text "=" <+/> expToDoc exp ++ text ";" - (done,docs) <- walkTm tm (nm :: done, docs) - pure (done, doc :: docs) - Just entry => pure (nm :: done, !(entryToDoc entry) :: docs) - where - 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) ++ text ";" - 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 - - walkTm (Ref x nm y) acc = process acc nm - walkTm (Lam x str _ _ t) acc = walkTm t acc - walkTm (App x t u) acc = walkTm t !(walkTm u acc) - walkTm (Pi x str icit y t u) acc = walkTm t !(walkTm u acc) - walkTm (Let x str t u) acc = walkTm t !(walkTm u acc) - walkTm (LetRec x str _ t u) acc = walkTm t !(walkTm u acc) - walkTm (Case x t alts) acc = foldlM walkAlt acc alts - walkTm _ acc = pure acc - -export -compile : M (List Doc) -compile = do - top <- get - 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 $ map snd $ SortedMap.toList top.defs - diff --git a/orig/Lib/CompileExp.idr b/orig/Lib/CompileExp.idr deleted file mode 100644 index 2af000e..0000000 --- a/orig/Lib/CompileExp.idr +++ /dev/null @@ -1,159 +0,0 @@ -||| First pass of compilation -||| - work out arities and fully apply functions / constructors (currying) -||| currying is problemmatic because we need to insert lambdas (η-expand) and -||| it breaks all of the de Bruijn indices -||| - expand metas (this is happening earlier) -||| - erase stuff (there is another copy that essentially does the same thing) -||| I could make names unique (e.q. on lambdas), but I might want that to vary per backend? -module Lib.CompileExp - -import Data.List - -import Lib.Types -- Name / Tm -import Lib.TopContext -import Lib.Prettier -import Lib.Util - -public export -data CExp : Type - -public export -data CAlt : Type where - CConAlt : String -> List String -> CExp -> CAlt - -- REVIEW keep var name? - CDefAlt : CExp -> CAlt - -- literal - CLitAlt : Literal -> CExp -> CAlt - -data CExp : Type where - CBnd : Nat -> CExp - CLam : Name -> CExp -> CExp - CFun : List Name -> CExp -> CExp - -- REVIEW This feels like a hack, but if we put CLam here, the - -- deBruijn gets messed up in code gen - CApp : CExp -> List CExp -> Nat -> CExp - -- TODO make DCon/TCon app separate so we can specialize - -- U / Pi are compiled to type constructors - CCase : CExp -> List CAlt -> CExp - CRef : Name -> CExp - CMeta : Nat -> CExp - CLit : Literal -> CExp - CLet : Name -> CExp -> CExp -> CExp - CLetRec : Name -> CExp -> CExp -> CExp - CErased : CExp - -||| I'm counting Lam in the term for arity. This matches what I need in -||| code gen. -export -lamArity : Tm -> Nat -lamArity (Lam _ _ _ _ t) = S (lamArity t) -lamArity _ = Z - -export -piArity : Tm -> Nat -piArity (Pi _ _ _ quant _ b) = S (piArity b) -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 -> 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" - (Just (MkEntry _ name type Axiom)) => pure 0 - (Just (MkEntry _ name type (TCon strs))) => pure $ piArity type - (Just (MkEntry _ name type (DCon k str))) => pure k - (Just (MkEntry _ name type (Fn t))) => pure $ lamArity t - (Just (MkEntry _ name type (PrimTCon))) => pure $ piArity type - -- Assuming a primitive can't return a function - (Just (MkEntry _ name type (PrimFn t uses))) => pure $ piArity type - -export -compileTerm : Tm -> M CExp - --- need to eta out extra args, fill in the rest of the apps -apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp --- out of args, make one up (fix that last arg) -apply t [] acc (S k) ty = pure $ CApp t (acc <>> []) (S k) - -- inserting Clam, index wrong? - -- CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k ty) -apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) = apply t xs (acc :< CErased) k b -apply t (x :: xs) acc (S k) (Pi y str icit Many a b) = apply t xs (acc :< x) k b --- see if there is anything we have to handle here -apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}. Overapplied function that escaped type checking?" --- once we hit zero, we fold the rest -apply t ts acc 0 ty = go (CApp t (acc <>> []) Z) ts - where - go : CExp -> List CExp -> M CExp - -- drop zero arg call - go (CApp t [] Z) args = go t args - go t [] = pure t - go t (arg :: args) = go (CApp t [arg] 0) args - --- apply : CExp -> List CExp -> SnocList CExp -> Nat -> M CExp --- -- out of args, make one up --- apply t [] acc (S k) = pure $ --- CLam "eta\{show k}" !(apply t [] (acc :< CBnd k) k) --- apply t (x :: xs) acc (S k) = apply t xs (acc :< x) k --- apply t ts acc 0 = go (CApp t (acc <>> [])) ts --- where --- go : CExp -> List CExp -> M CExp --- -- drop zero arg call --- go (CApp t []) args = go t args --- go t [] = pure t --- go t (arg :: args) = go (CApp t [arg]) args - -compileTerm (Bnd _ k) = pure $ CBnd k --- need to eta expand to arity -compileTerm t@(Ref fc nm _) = do - top <- get - let Just (MkEntry _ _ type _) = lookup nm top - | Nothing => error fc "Undefined name \{nm}" - 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) -compileTerm tm@(App _ _ _) with (funArgs tm) - _ | (Meta _ k, args) = do - error (getFC tm) "Compiling an unsolved meta \{showTm tm}" - info (getFC tm) "Compiling an unsolved meta \{showTm tm}" - pure $ CApp (CRef "Meta\{show k}") [] Z - _ | (t@(Ref fc nm _), args) = do - args' <- traverse compileTerm args - arity <- arityForName fc nm - top <- get - let Just (MkEntry _ _ type _) = lookup nm top - | Nothing => error fc "Undefined name \{nm}" - apply (CRef (show nm)) args' [<] arity type - _ | (t, args) = do - debug "apply other \{pprint [] t}" - t' <- compileTerm t - args' <- traverse compileTerm args - apply t' args' [<] 0 (UU emptyFC) - -- error (getFC t) "Don't know how to apply \{showTm t}" -compileTerm (UU _) = pure $ CRef "U" -compileTerm (Pi _ nm icit rig t u) = pure $ CApp (CRef "PiType") [ !(compileTerm t), CLam nm !(compileTerm u)] Z -compileTerm (Case _ t alts) = do - t' <- compileTerm t - alts' <- traverse (\case - CaseDefault tm => pure $ CDefAlt !(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 -compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u) -compileTerm (LetRec _ nm _ t u) = pure $ CLetRec nm !(compileTerm t) !(compileTerm u) -compileTerm (Erased _) = pure CErased - -export -compileFun : Tm -> M CExp -compileFun tm = go tm [<] - where - go : Tm -> SnocList String -> M CExp - go (Lam _ nm _ _ t) acc = go t (acc :< nm) - go tm [<] = compileTerm tm - go tm args = pure $ CFun (args <>> []) !(compileTerm tm) - - diff --git a/orig/Lib/Elab.idr b/orig/Lib/Elab.idr deleted file mode 100644 index b065d86..0000000 --- a/orig/Lib/Elab.idr +++ /dev/null @@ -1,1398 +0,0 @@ -module Lib.Elab - -import Lib.Parser.Impl -import Lib.Prettier -import Data.List -import Data.Vect -import Data.String -import Data.IORef -import Lib.Types -import Lib.Util -import Lib.Eval -import Lib.TopContext -import Lib.Syntax - - - - -||| collectDecl collects multiple Def for one function into one -export -collectDecl : List Decl -> List Decl -collectDecl [] = [] -collectDecl ((Def fc nm cl) :: rest@(Def _ nm' cl' :: xs)) = - if nm == nm' then collectDecl (Def fc nm (cl ++ cl') :: xs) - else (Def fc nm cl :: collectDecl rest) -collectDecl (x :: xs) = x :: collectDecl xs - --- renaming --- dom gamma ren -data Pden = PR Nat Nat (List Nat) - -showCtx : Context -> M String -showCtx ctx = - unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) [] - where - isVar : Nat -> Val -> Bool - isVar k (VVar _ k' [<]) = k == k' - isVar _ _ = False - - go : List String -> Nat -> List (Val, String, Val) -> List String -> M (List String) - go _ _ [] acc = pure acc - go names k ((v, n, ty) :: xs) acc = if isVar k v - -- TODO - use Doc and add <+/> as appropriate to printing - then go names (S k) xs (" \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc) - else go names (S k) xs (" \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc) - -dumpCtx : Context -> M String -dumpCtx ctx = do - let names = (toList $ map fst ctx.types) - -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too. - env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}" - let msg = unlines (toList $ reverse env) -- ++ " -----------\n" ++ " goal \{pprint names ty'}" - pure msg - - -pprint : Context -> Val -> M Doc -pprint ctx v = pure $ pprint (names ctx) !(quote (length ctx.env) v) - -||| return Bnd and type for name -export -lookupName : Context -> String -> Maybe (Tm, Val) -lookupName ctx name = go 0 ctx.types - where - go : Nat -> Vect n (String, Val) -> Maybe (Tm, Val) - go ix [] = Nothing - -- FIXME - we should stuff a Binder of some sort into "types" - go ix ((nm, ty) :: xs) = if nm == name then Just (Bnd emptyFC ix, ty) else go (S ix) xs - -export -lookupDef : Context -> String -> Maybe Val -lookupDef ctx name = go 0 ctx.types ctx.env - where - go : Nat -> Vect n (String, Val) -> List Val -> Maybe Val - go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (S ix) xs vs - go ix _ _ = Nothing - - --- IORef for metas needs IO -export -forceMeta : Val -> M Val -forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of - (Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp) - (Solved _ k t) => vappSpine t sp >>= forceMeta -forceMeta x = pure x - -public export -record UnifyResult where - constructor MkResult - -- wild guess here - lhs is a VVar - constraints : List (Nat, Val) - -Semigroup UnifyResult where - (MkResult cs) <+> (MkResult cs') = MkResult (cs ++ cs') - -Monoid UnifyResult where - neutral = MkResult [] - -data UnifyMode = Normal | Pattern - - -export -check : Context -> Raw -> Val -> M Tm - -export -unifyCatch : FC -> Context -> Val -> Val -> M () - --- Check that the arguments are not explicit and the type constructor in codomain matches --- Later we will build a table of codomain type, and maybe make the user tag the candidates --- like Idris does with %hint -isCandidate : Val -> Tm -> Bool -isCandidate ty (Pi fc nm Explicit rig t u) = False -isCandidate ty (Pi fc nm icit rig t u) = isCandidate ty u -isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm' -isCandidate ty (App fc t u) = isCandidate ty t -isCandidate _ _ = False - --- This is a crude first pass -export -findMatches : Context -> Val -> List TopEntry -> M (List String) -findMatches ctx ty [] = pure [] -findMatches ctx ty ((MkEntry _ name type def) :: xs) = do - let True = isCandidate ty type | False => findMatches ctx ty xs - top <- get - -- let ctx = mkCtx (getFC ty) - -- FIXME we're restoring state, but the INFO logs have already been emitted - -- Also redo this whole thing to run during elab, recheck constraints, etc. - mc <- readIORef top.metaCtx - catchError(do - -- TODO sort out the FC here - let fc = getFC ty - 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 - -- FIXME RVar should optionally have qualified names - let (QN ns nm) = name - let (cod, tele) = splitTele type - modifyIORef top.metaCtx { mcmode := CheckFirst } - tm <- check ctx (RVar fc nm) ty - debug "Found \{pprint [] tm} for \{show ty}" - writeIORef top.metaCtx mc - (nm ::) <$> findMatches ctx ty xs) - (\ err => do - debug "No match \{show ty} \{pprint [] type} \{showError "" err}" - writeIORef top.metaCtx mc - findMatches ctx ty xs) - -export -contextMatches : Context -> Val -> M (List (Tm, Val)) -contextMatches ctx ty = go (zip ctx.env (toList ctx.types)) - where - go : List (Val, String, Val) -> M (List (Tm, Val)) - go [] = pure [] - go ((tm, nm, vty) :: xs) = do - type <- quote ctx.lvl vty - let True = isCandidate ty type | False => go xs - top <- get - mc <- readIORef top.metaCtx - catchError(do - debug "TRY context \{nm} : \{pprint (names ctx) type} for \{show ty}" - unifyCatch (getFC ty) ctx ty vty - mc' <- readIORef top.metaCtx - writeIORef top.metaCtx mc - tm <- quote ctx.lvl tm - ((tm, vty) ::) <$> go xs) - (\ err => do - debug "No match \{show ty} \{pprint (names ctx) type} \{showError "" err}" - writeIORef top.metaCtx mc - go xs) - -export -getArity : Tm -> Nat -getArity (Pi x str icit rig t u) = S (getArity u) --- Ref or App (of type constructor) are valid -getArity _ = Z - --- Can metas live in context for now? --- We'll have to be able to add them, which might put gamma in a ref - - - --- Makes the arg for `solve` when we solve an auto -makeSpine : Nat -> Vect k BD -> SnocList Val -makeSpine k [] = [<] -makeSpine (S k) (Defined :: xs) = makeSpine k xs -makeSpine (S k) (Bound :: xs) = makeSpine k xs :< VVar emptyFC k [<] -makeSpine 0 xs = ?fixme - -export -solve : Env -> (k : Nat) -> SnocList Val -> Val -> M () - - -export -trySolveAuto : MetaEntry -> M Bool -trySolveAuto (Unsolved fc k ctx ty AutoSolve _) = do - debug "TRYAUTO solving \{show k} : \{show ty}" - -- fill in solved metas in type - x <- quote ctx.lvl ty - ty <- eval ctx.env CBN x - debug "AUTO ---> \{show ty}" - -- we want the context here too. - top <- get - [] <- contextMatches ctx ty - | [(tm, vty)] => do - unifyCatch (getFC ty) ctx ty vty - val <- eval ctx.env CBN tm - debug "SOLUTION \{pprint [] tm} evaled to \{show val}" - let sp = makeSpine ctx.lvl ctx.bds - solve ctx.env k sp val - pure True - | res => do - debug "FAILED to solve \{show ty}, matches: \{commaSep $ map (pprint [] . fst) res}" - pure False - [nm] <- findMatches ctx ty $ toList top.defs - | res => do - debug "FAILED to solve \{show ty}, matches: \{show res}" - pure False - tm <- check ctx (RVar fc nm) ty - val <- eval ctx.env CBN tm - debug "SOLUTION \{pprint [] tm} evaled to \{show val}" - let sp = makeSpine ctx.lvl ctx.bds - solve ctx.env k sp val - pure True -trySolveAuto _ = pure False - --- export --- solveAutos : Nat -> List MetaEntry -> M () --- solveAutos mstart [] = pure () --- solveAutos mstart (entry :: es) = do --- res <- trySolveAuto entry --- -- idris is inlining this and blowing stack? --- if res --- then do --- top <- get --- mc <- readIORef top.metaCtx --- let mlen = length mc.metas `minus` mstart --- solveAutos mstart (take mlen mc.metas) --- else --- solveAutos mstart es - - --- Called from ProcessDecl, this was popping the stack, the tail call optimization doesn't --- handle the traversal of the entire meta list. I've turned the restart into a trampoline --- and filtered it down to unsolved autos. -export -solveAutos : Nat -> M () -solveAutos mstart = do - top <- get - mc <- readIORef top.metaCtx - let mlen = length mc.metas `minus` mstart - res <- run $ filter isAuto (take mlen mc.metas) - if res then solveAutos mstart else pure () - where - isAuto : MetaEntry -> Bool - isAuto (Unsolved fc k ctx x AutoSolve xs) = True - isAuto _ = False - - run : List MetaEntry -> M Bool - run Nil = pure False - run (e :: es) = - if !(trySolveAuto e) then pure True else run es - --- We need to switch to SortedMap here -export -updateMeta : Nat -> (MetaEntry -> M MetaEntry) -> M () -updateMeta ix f = do - top <- get - mc <- readIORef top.metaCtx - metas <- go mc.metas - writeIORef top.metaCtx $ {metas := metas} mc - where - go : List MetaEntry -> M (List MetaEntry) - go [] = error' "Meta \{show ix} not found" - go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs - go (x@((Solved _ k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs - - -checkAutos : Nat -> List MetaEntry -> M () -checkAutos ix Nil = pure () -checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do - ty' <- quote ctx.lvl ty - when (usesMeta ty') $ ignore $ trySolveAuto entry - checkAutos ix rest - where - usesMeta : Tm -> Bool - usesMeta (App _ (Meta _ k) u) = if k == ix then True else usesMeta u - usesMeta (App _ _ u) = usesMeta u - usesMeta _ = False -checkAutos ix (_ :: rest) = checkAutos ix rest - - -export -addConstraint : Env -> Nat -> SnocList Val -> Val -> M () -addConstraint env ix sp tm = do - top <- get - mc <- readIORef top.metaCtx - let (CheckAll) = mc.mcmode | _ => pure () - updateMeta ix $ \case - (Unsolved pos k a b c cons) => do - debug "Add constraint m\{show ix} \{show sp} =?= \{show tm}" - pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons)) - (Solved _ k tm) => error' "Meta \{show k} already solved [addConstraint]" - mc <- readIORef top.metaCtx - checkAutos ix mc.metas - -- this loops too - -- solveAutos 0 mc.metas - pure () - - --- return renaming, the position is the new VVar -invert : Nat -> SnocList Val -> M (List Nat) -invert lvl sp = go sp [] - where - go : SnocList Val -> List Nat -> M (List Nat) - go [<] acc = pure $ reverse acc - go (xs :< VVar fc k [<]) acc = do - if elem k acc - then do - debug "\{show k} \{show acc}" - -- when does this happen? - error fc "non-linear pattern: \{show sp}" - else go xs (k :: acc) - go (xs :< v) _ = error emptyFC "non-variable in pattern \{show v}" - - --- REVIEW why am I converting to Tm? --- we have to "lift" the renaming when we go under a lambda --- I think that essentially means our domain ix are one bigger, since we're looking at lvl --- in the codomain, so maybe we can just keep that value - - -rename : Nat -> List Nat -> Nat -> Val -> M Tm - -renameSpine : Nat -> List Nat -> Nat -> Tm -> SnocList Val -> M Tm -renameSpine meta ren lvl tm [<] = pure tm -renameSpine meta ren lvl tm (xs :< x) = do - xtm <- rename meta ren lvl x - pure $ App emptyFC !(renameSpine meta ren lvl tm xs) xtm - - - - -rename meta ren lvl (VVar fc k sp) = case findIndex (== k) ren of - Nothing => error fc "scope/skolem thinger VVar \{show k} ren \{show ren}" - Just x => renameSpine meta ren lvl (Bnd fc $ cast x) sp -rename meta ren lvl (VRef fc nm def sp) = renameSpine meta ren lvl (Ref fc nm def) sp -rename meta ren lvl (VMeta fc ix sp) = do - -- So sometimes we have an unsolved meta in here which reference vars out of scope. - debug "rename Meta \{show ix} spine \{show sp}" - if ix == meta - -- REVIEW is this the right fc? - then error fc "meta occurs check" - else case !(lookupMeta ix) of - Solved fc _ val => do - debug "rename: \{show ix} is solved" - rename meta ren lvl !(vappSpine val sp) - _ => do - debug "rename: \{show ix} is unsolved" - catchError (renameSpine meta ren lvl (Meta fc ix) sp) (\err => throwError $ Postpone fc ix (errorMsg err)) -rename meta ren lvl (VLam fc n icit rig t) = pure (Lam fc n icit rig !(rename meta (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<]))) -rename meta ren lvl (VPi fc n icit rig ty tm) = pure (Pi fc n icit rig !(rename meta ren lvl ty) !(rename meta (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<]))) -rename meta ren lvl (VU fc) = pure (UU fc) -rename meta ren lvl (VErased fc) = pure (Erased fc) --- for now, we don't do solutions with case in them. -rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution" -rename meta ren lvl (VLit fc lit) = pure (Lit fc lit) -rename meta ren lvl (VLet fc name val body) = - pure $ Let fc name !(rename meta ren lvl val) !(rename meta (lvl :: ren) (S lvl) body) --- these probably shouldn't show up in solutions... -rename meta ren lvl (VLetRec fc name ty val body) = - pure $ LetRec fc name !(rename meta ren lvl ty) !(rename meta (lvl :: ren) (S lvl) val) !(rename meta (lvl :: ren) (S lvl) body) - -lams : Nat -> List String -> Tm -> Tm -lams 0 _ tm = tm --- REVIEW do we want a better FC, icity?, rig? -lams (S k) [] tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k [] tm) -lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm) - -export -unify : Env -> UnifyMode -> Val -> Val -> M UnifyResult - -(.boundNames) : Context -> List String -ctx.boundNames = map snd $ filter (\x => fst x == Bound) $ toList $ zip ctx.bds (map fst ctx.types) - - -maybeCheck : M () -> M () -maybeCheck action = do - top <- get - mc <- readIORef top.metaCtx - case mc.mcmode of - CheckAll => action - CheckFirst => do - modifyIORef top.metaCtx $ { mcmode := NoCheck } - action - modifyIORef top.metaCtx $ { mcmode := CheckFirst } - NoCheck => pure () - -solve env m sp t = do - meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m - | _ => error (getFC t) "Meta \{show m} already solved! [solve]" - debug "SOLVE \{show m} \{show kind} lvl \{show $ length env} sp \{show sp} is \{show t}" - let size = length $ filter (\x => x == Bound) $ toList ctx_.bds - debug "\{show m} size is \{show size} sps \{show $ length sp}" - let True = length sp == size - | _ => do - let l = length env - debug "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}" - debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}" - addConstraint env m sp t - let l = length env - debug "meta \{show meta}" - ren <- invert l sp - -- force unlet - hack <- quote l t - t <- eval env CBN hack - catchError (do - tm <- rename m ren l t - - let tm = lams (length sp) (reverse ctx_.boundNames) tm - top <- get - soln <- eval [] CBN tm - - updateMeta m $ \case - (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln - (Solved _ k x) => error' "Meta \{show ix} already solved! [solve2]" - - maybeCheck $ for_ cons $ \case - MkMc fc env sp rhs => do - val <- vappSpine soln sp - debug "discharge l=\{show $ length env} \{(show val)} =?= \{(show rhs)}" - unify env Normal val rhs - mc <- readIORef top.metaCtx - -- stack ... - -- checkAutos ix mc.metas - pure MkUnit - ) - - (\case - Postpone fc ix msg => do - -- let someone else solve this and then check again. - debug "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}" - addConstraint env m sp t - err => do - -- I get legit errors after stuffing in solution - -- report for now, tests aren't hitting this branch - throwError err - debug "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}" - debug "because \{showError "" err}" - addConstraint env m sp t) - -unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult -unifySpine env mode False _ _ = error emptyFC "unify failed at head" -- unreachable now -unifySpine env mode True [<] [<] = pure (MkResult []) -unifySpine env mode True (xs :< x) (ys :< y) = [| unify env mode x y <+> (unifySpine env mode True xs ys) |] -unifySpine env mode True _ _ = error emptyFC "meta spine length mismatch" - - -unify env mode t u = do - debug "Unify lvl \{show $ length env}" - debug " \{show t}" - debug " =?= \{show u}" - t' <- forceMeta t >>= unlet env - u' <- forceMeta u >>= unlet env - debug "forced \{show t'}" - debug " =?= \{show u'}" - debug "env \{show env}" - -- debug "types \{show $ ctx.types}" - let l = length env - -- On the LHS, variable matching is yields constraints/substitutions - -- We want this to happen before VRefs are expanded, and mixing mode - -- into the case tree explodes it further. - case mode of - Pattern => unifyPattern t' u' - Normal => unifyMeta t' u' - - -- The case tree is still big here. It's hard for idris to sort - -- What we really want is what I wrote - handle meta, handle lam, handle var, etc - - where - -- The case tree here was huge, so I split it into stages - -- newt will have similar issues because it doesn't emit a default case - - unifyRest : Val -> Val -> M UnifyResult - unifyRest (VPi fc _ _ _ a b) (VPi fc' _ _ _ a' b') = do - let fresh = VVar fc (length env) [<] - [| unify env mode a a' <+> unify (fresh :: env) mode !(b $$ fresh) !(b' $$ fresh) |] - - unifyRest (VU _) (VU _) = pure neutral - -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. - unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}" - - unifyRef : Val -> Val -> M UnifyResult - unifyRef t'@(VRef fc k def sp) u'@(VRef fc' k' def' sp') = - -- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y - do - -- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do - Nothing <- tryEval env t' - | Just v => do - debug "tryEval \{show t'} to \{show v}" - unify env mode v u' - Nothing <- tryEval env u' - | Just v => unify env mode t' v - if k == k' - then unifySpine env mode (k == k') sp sp' - else error fc "vref mismatch \{show t'} \{show u'}" - - -- Lennart.newt cursed type references itself - -- We _could_ look up the ref, eval against [] and vappSpine... - unifyRef t u@(VRef fc' k' def sp') = do - debug "expand \{show t} =?= %ref \{k'}" - case lookup k' !(get) of - Just (MkEntry _ name ty (Fn tm)) => unify env mode t !(vappSpine !(eval [] CBN tm) sp') - _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n env is \{show env}" - - unifyRef t@(VRef fc k def sp) u = do - debug "expand %ref \{k} \{show sp} =?= \{show u}" - case lookup k !(get) of - Just (MkEntry _ name ty (Fn tm)) => unify env mode !(vappSpine !(eval [] CBN tm) sp) u - _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n env is \{show env}" - unifyRef t u = unifyRest t u - - unifyVar : Val -> Val -> M UnifyResult - unifyVar t'@(VVar fc k sp) u'@(VVar fc' k' sp') = - if k == k' then unifySpine env mode (k == k') sp sp' - else error fc "Failed to unify \{show t'} and \{show u'}" - - unifyVar t'@(VVar fc k [<]) u = case !(tryEval env u) of - Just v => unify env mode t' v - Nothing => error fc "Failed to unify \{show t'} and \{show u}" - - unifyVar t u'@(VVar fc k [<]) = case !(tryEval env t) of - Just v => unify env mode v u' - Nothing => error fc "Failed to unify \{show t} and \{show u'}" - unifyVar t u = unifyRef t u - - unifyLam : Val -> Val -> M UnifyResult - unifyLam (VLam fc _ _ _ t) (VLam _ _ _ _ t') = do - let fresh = VVar fc (length env) [<] - unify (fresh :: env) mode !(t $$ fresh) !(t' $$ fresh) - unifyLam t (VLam fc' _ _ _ t') = do - debug "ETA \{show t}" - let fresh = VVar fc' (length env) [<] - unify (fresh :: env) mode !(t `vapp` fresh) !(t' $$ fresh) - unifyLam (VLam fc _ _ _ t) t' = do - debug "ETA' \{show t'}" - let fresh = VVar fc (length env) [<] - unify (fresh :: env) mode !(t $$ fresh) !(t' `vapp` fresh) - unifyLam t u = unifyVar t u - - unifyMeta : Val -> Val -> M UnifyResult - -- flex/flex - unifyMeta (VMeta fc k sp) (VMeta fc' k' sp') = - if k == k' then unifySpine env mode (k == k') sp sp' - -- TODO, might want to try the other way, too. - else if length sp < length sp' - then solve env k' sp' (VMeta fc k sp) >> pure neutral - else solve env k sp (VMeta fc' k' sp') >> pure neutral - unifyMeta t (VMeta fc' i' sp') = solve env i' sp' t >> pure neutral - unifyMeta (VMeta fc i sp) t' = solve env i sp t' >> pure neutral - unifyMeta t v = unifyLam t v - - unifyPattern : Val -> Val -> M UnifyResult - unifyPattern t'@(VVar fc k sp) u'@(VVar fc' k' sp') = - if k == k' then unifySpine env mode (k == k') sp sp' - else case (sp, sp') of - ([<],[<]) => if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')] - _ => error fc "Failed to unify \{show t'} and \{show u'}" - - unifyPattern (VVar fc k [<]) u = pure $ MkResult[(k, u)] - unifyPattern t (VVar fc k [<]) = pure $ MkResult [(k, t)] - unifyPattern t u = unifyMeta t u - - -unifyCatch fc ctx ty' ty = do - res <- catchError (unify ctx.env Normal ty' ty) $ \err => do - let names = toList $ map fst ctx.types - debug "fail \{show ty'} \{show ty}" - a <- quote ctx.lvl ty' - b <- quote ctx.lvl ty - let msg = "unification failure: \{errorMsg err}\n failed to unify \{pprint names a}\n with \{pprint names b}\n " - throwError (E fc msg) - case res of - MkResult [] => pure () - cs => do - -- probably want a unification mode that throws instead of returning constraints - -- TODO need a normalizeHoles, maybe on quote? - debug "fail with constraints \{show cs.constraints}" - a <- quote ctx.lvl ty' - b <- quote ctx.lvl ty - let names = toList $ map fst ctx.types - let msg = "xxunification failure\n failed to unify \{pprint names a}\n with \{pprint names b}" - let msg = msg ++ "\nconstraints \{show cs.constraints}" - throwError (E fc msg) - -- error fc "Unification yields constraints \{show cs.constraints}" - -export -freshMeta : Context -> FC -> Val -> MetaKind -> M Tm -freshMeta ctx fc ty kind = do - top <- get - mc <- readIORef top.metaCtx - debug "fresh meta \{show mc.next} : \{show ty} (\{show kind})" - let newmeta = Unsolved fc mc.next ctx ty kind [] - writeIORef top.metaCtx $ { next $= S, metas $= (newmeta ::) } mc - -- infinite loop - keeps trying Ord a => Ord (a \x a) - -- when (kind == AutoSolve) $ ignore $ trySolveAuto newmeta - pure $ applyBDs 0 (Meta fc mc.next) ctx.bds - where - -- hope I got the right order here :) - applyBDs : Nat -> Tm -> Vect k BD -> Tm - applyBDs k t [] = t - -- review the order here - applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k) - applyBDs k t (Defined :: xs) = applyBDs (S k) t xs - -insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) -insert ctx tm ty = do - case !(forceMeta ty) of - VPi fc x Auto rig a b => do - m <- freshMeta ctx (getFC tm) a AutoSolve - debug "INSERT Auto \{pprint (names ctx) m} : \{show a}" - debug "TM \{pprint (names ctx) tm}" - mv <- eval ctx.env CBN m - insert ctx (App (getFC tm) tm m) !(b $$ mv) - VPi fc x Implicit rig a b => do - m <- freshMeta ctx (getFC tm) a Normal - debug "INSERT \{pprint (names ctx) m} : \{show a}" - debug "TM \{pprint (names ctx) tm}" - mv <- eval ctx.env CBN m - insert ctx (App (getFC tm) tm m) !(b $$ mv) - va => pure (tm, va) - -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" - -export -infer : Context -> Raw -> M (Tm, Val) - - -data Bind = MkBind String Icit Val - -Show Bind where - show (MkBind str icit x) = "\{str} \{show icit}" - - ----------------- Case builder - -public export -record Problem where - constructor MkProb - clauses : List Clause - -- I think a pi-type representing the pattern args -> goal, so we're checking - -- We might pull out the pattern abstraction to a separate step and drop pats from clauses. - ty : Val - --- Might have to move this if Check reaches back in... --- this is kinda sketchy, we can't use it twice at the same depth with the same name. -fresh : {auto ctx : Context} -> String -> String -fresh base = base ++ "$" ++ show (length ctx.env) - --- The result is a casetree, but it's in Tm -export -buildTree : Context -> Problem -> M Tm - --- Updates a clause for INTRO -introClause : String -> Icit -> Clause -> M Clause -introClause nm icit (MkClause fc cons (pat :: pats) expr) = - if icit == getIcit pat then pure $ MkClause fc ((nm, pat) :: cons) pats expr - else if icit == Implicit then pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) (pat :: pats) expr - else if icit == Auto then pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) (pat :: pats) expr - else error fc "Explicit arg and \{show $ getIcit pat} pattern \{show nm} \{show pat}" --- handle implicts at end? -introClause nm Implicit (MkClause fc cons [] expr) = pure $ MkClause fc ((nm, PatWild fc Implicit) :: cons) [] expr -introClause nm Auto (MkClause fc cons [] expr) = pure $ MkClause fc ((nm, PatWild fc Auto) :: cons) [] expr -introClause nm icit (MkClause fc cons [] expr) = error fc "Clause size doesn't match" - --- A split candidate looks like x /? Con ... --- we need a type here. I pulled if off of the --- pi-type, but do we need metas solved or dependents split? --- this may dot into a dependent. -findSplit : List Constraint -> Maybe Constraint -findSplit [] = Nothing - -- FIXME look up type, ensure it's a constructor -findSplit (x@(nm, PatCon _ _ _ _ _) :: xs) = Just x -findSplit (x@(nm, PatLit _ val) :: xs) = Just x -findSplit (x :: xs) = findSplit xs - - --- *************** --- right, I think we rewrite the names in the context before running raw and we're good to go? --- We have stuff like S k /? x, but I think we can back up to whatever the scrutinee variable was? - --- we could pass into build case and use it for (x /? y) - --- TODO, we may need to filter these against the type to rule out --- impossible cases -getConstructors : Context -> FC -> Val -> M (List (QName, Nat, Tm)) -getConstructors ctx scfc (VRef fc nm _ _) = do - names <- lookupTCon nm - traverse lookupDCon names - where - 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 : QName -> M (QName, Nat, Tm) - lookupDCon nm = do - case lookup nm !get of - (Just (MkEntry _ name type (DCon k str))) => pure (name, k, type) - Just _ => error fc "Internal Error: \{nm} is not a DCon" - Nothing => error fc "Internal Error: DCon \{nm} not found" -getConstructors ctx scfc tm = error scfc "Can't split - not VRef: \{!(pprint ctx tm)}" - --- Extend environment with fresh variables from a pi-type --- the pi-type here is the telescope of a constructor --- return context, remaining type, and list of names -extendPi : Context -> Val -> SnocList Bind -> SnocList Val -> M (Context, Val, List Bind, SnocList Val) -extendPi ctx (VPi x str icit rig a b) nms sc = do - let nm = fresh str -- "pat" - let ctx' = extend ctx nm a - let v = VVar emptyFC (length ctx.env) [<] - tyb <- b $$ v - extendPi ctx' tyb (nms :< MkBind nm icit a) (sc :< VVar x (length ctx.env) [<]) -extendPi ctx ty nms sc = pure (ctx, ty, nms <>> [], sc) - --- turn vars into lets for forced values. --- substitute inside values --- FIXME we're not going under closures at the moment. -substVal : Nat -> Val -> Val -> Val -substVal k v tm = go tm - where - go : Val -> Val - go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp)) - go (VLet fc nm a b) = VLet fc nm (go a) b - go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b - go (VMeta fc ix sp) = VMeta fc ix (map go sp) - go (VRef fc nm y sp) = VRef fc nm y (map go sp) - go tm = tm - -- FIXME - do I need a Val closure like idris? - -- or env in unify... - -- or quote back - -- go (VLam fc nm sc) = VLam fc nm sc - -- go (VCase x sc xs) = ?rhs_2 - -- go (VU x) = ?rhs_7 - -- go (VLit x y) = ?rhs_8 - - --- need to turn k into a ground value - --- TODO rework this to do something better. We've got constraints, and --- and may need to do proper unification if it's already defined to a value --- below we're handling the case if it's defined to another var, but not --- checking for loops. -updateContext : Context -> List (Nat, Val) -> M Context -updateContext ctx [] = pure ctx -updateContext ctx ((k, val) :: cs) = - let ix = lvl2ix (length ctx.env) k in - case getAt ix ctx.env of - (Just (VVar _ k' [<])) => - if k' /= k - then updateContext ctx ((k',val) :: cs) - else updateContext ({env $= map (substVal k val), bds $= replaceV ix Defined } ctx) cs - (Just val') => do - -- This is fine for Z =?= Z but for other stuff, we probably have to match - info (getFC val) "need to unify \{show val} and \{show val'} or something" - updateContext ctx cs - Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext" - - -- - -- updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs - where - replace : Nat -> Val -> List Val -> List Val - replace k x [] = [] - replace 0 x (y :: xs) = x :: xs - replace (S k) x (y :: xs) = y :: replace k x xs - - replaceV : Nat -> a -> Vect n a -> Vect n a - replaceV k x [] = [] - replaceV 0 x (y :: xs) = x :: xs - replaceV (S k) x (y :: xs) = y :: replaceV k x xs - --- ok, so this is a single constructor, CaseAlt --- return Nothing if dcon doesn't unify with scrut -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 - (ctx', ty', vars, sc) <- extendPi ctx (vty) [<] [<] - - -- TODO I think we need to figure out what is dotted, maybe - -- the environment manipulation below is sufficient bookkeeping - -- or maybe it's a bad approach. - - -- At some point, I'll take a break and review more papers and code, - -- now that I know some of the questions I'm trying to answer. - - -- We get unification constraints from matching the data constructors - -- codomain with the scrutinee type - debug "unify dcon cod with scrut\n \{show ty'}\n \{show scty}" - Just res <- catchError(Just <$> unify ctx'.env Pattern ty' scty) - (\err => do - debug "SKIP \{dcName} because unify error \{errorMsg err}" - pure Nothing) - | _ => pure Nothing - - -- if the value is already constrained to a different constructor, return Nothing - debug "scrut \{scnm} constrained to \{show $ lookupDef ctx scnm}" - let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}" - - case lookupDef ctx scnm of - Just val@(VRef fc nm y sp) => - if nm /= dcName - then do - debug "SKIP \{dcName} because \{scnm} forced to \{show val}" - pure Nothing - else do - debug "case \{dcName} dotted \{show val}" - when (length vars /= length sp) $ error emptyFC "\{show $ length vars} vars /= \{show $ length sp}" - - -- TODO - I think we need to define the context vars to sp via updateContext - - let lvl = minus (length ctx'.env) (length vars) - let scons = constrainSpine lvl (sp <>> []) -- REVIEW is this the right order? - ctx' <- updateContext ctx' scons - - debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" - debug "(dcon \{show dcName}) (vars \{show vars}) clauses were" - for_ prob.clauses $ (\x => debug " \{show x}") - clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses - debug "and now:" - for_ clauses $ (\x => debug " \{show x}") - when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{dcName} splitting \{scnm}" - tm <- buildTree ctx' (MkProb clauses prob.ty) - pure $ Just $ CaseCons dcName (map getName vars) tm - - _ => do - Right res <- tryError (unify ctx'.env Pattern ty' scty) - | Left err => do - debug "SKIP \{dcName} because unify error \{errorMsg err}" - pure Nothing - - -- Constrain the scrutinee's variable to be dcon applied to args - let Just x = findIndex ((==scnm) . fst) ctx'.types - | Nothing => error ctx.ctxFC "\{scnm} not is scope?" - let lvl = lvl2ix (length ctx'.env) (cast x) - let scon : (Nat, Val) = (lvl, VRef ctx.ctxFC dcName (DCon arity dcName) sc) - - debug "scty \{show scty}" - debug "UNIFY results \{show res.constraints}" - debug "before types: \{show ctx'.types}" - debug "before env: \{show ctx'.env}" - debug "SC CONSTRAINT: \{show scon}" - - -- push the constraints into the environment by turning bind into define - -- Is this kosher? It might be a problem if we've already got metas over - -- this stuff, because it intends to ignore defines. - ctx' <- updateContext ctx' (scon :: res.constraints) - - debug "context types: \{show ctx'.types}" - debug "context env: \{show ctx'.env}" - - -- What if all of the pattern vars are defined to meta - - debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}" - debug "(dcon \{show dcName}) (vars \{show vars}) clauses were" - for_ prob.clauses $ (\x => debug " \{show x}") - clauses <- mapMaybe id <$> traverse (rewriteClause sctynm vars) prob.clauses - debug "and now:" - for_ clauses $ (\x => debug " \{show x}") - when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{dcName} splitting \{scnm}" - tm <- buildTree ctx' (MkProb clauses prob.ty) - pure $ Just $ CaseCons dcName (map getName vars) tm - where - constrainSpine : Nat -> List Val -> List (Nat, Val) - constrainSpine lvl [] = [] - constrainSpine lvl (v :: vs) = (lvl, v) :: constrainSpine (S lvl) vs - - getName : Bind -> String - getName (MkBind nm _ _) = nm - - -- for each clause in prob, find nm on LHS of some constraint, and - -- "replace" with the constructor and vars. - -- - -- This will be: - -- x /? y can probably just leave this - -- x /? D a b c split into three x /? a, y /? b, z /? c - -- x /? E a b drop this clause - -- We get a list of clauses back (a Problem) and then solve that - -- If they all fail, we have a coverage issue. (Assuming the constructor is valid) - - makeConstr : List Bind -> List Pattern -> M (List (String, Pattern)) - makeConstr [] [] = pure $ [] - makeConstr [] (pat :: pats) = error (getFC pat) "too many patterns" - makeConstr ((MkBind nm Implicit x) :: xs) [] = pure $ (nm, PatWild emptyFC Implicit) :: !(makeConstr xs []) - makeConstr ((MkBind nm Auto x) :: xs) [] = pure $ (nm, PatWild emptyFC Auto) :: !(makeConstr xs []) - makeConstr ((MkBind nm Explicit x) :: xs) [] = error ctx.ctxFC "not enough patterns" - makeConstr ((MkBind nm Explicit x) :: xs) (pat :: pats) = - if getIcit pat == Explicit - then pure $ (nm, pat) :: !(makeConstr xs pats) - else error ctx.ctxFC "mismatch between Explicit and \{show $ getIcit pat}" - makeConstr ((MkBind nm icit x) :: xs) (pat :: pats) = - if getIcit pat /= icit -- Implicit/Explicit Implicit/Auto, etc - then pure $ (nm, PatWild (getFC pat) icit) :: !(makeConstr xs (pat :: pats)) - else pure $ (nm, pat) :: !(makeConstr xs pats) - - -- replace constraint with constraints on parameters, or nothing if non-matching clause - 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 - then case y of - PatVar _ _ s => pure $ Just $ c :: (xs ++ acc) - PatWild _ _ => pure $ Just $ c :: (xs ++ acc) - -- FIXME why don't we hit this (when user puts 'x' for Just 'x') - PatLit fc lit => error fc "Literal \{show lit} in constructor split" - PatCon fc icit nm ys as => if nm == dcName - then case as of - Nothing => pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc - -- putting this in constraints causes it to be renamed scnm -> nm' when we check body. - Just nm' => pure $ Just $ (scnm, (PatVar fc icit nm')) :: !(makeConstr vars ys) ++ xs ++ acc - else do - -- TODO can we check this when we make the PatCon? - case lookup nm !get of - (Just (MkEntry _ name type (DCon k tcname))) => - if (tcname /= sctynm) - then error fc "Constructor is \{tcname} expected \{sctynm}" - else pure Nothing - Just _ => error fc "Internal Error: \{nm} is not a DCon" - Nothing => error fc "Internal Error: DCon \{nm} not found" - else rewriteConstraint sctynm vars xs (c :: acc) - - 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 - -export -splitArgs : Raw -> List (Raw, Icit) -> (Raw, List (Raw, Icit)) -splitArgs (RApp fc t u icit) args = splitArgs t ((u, icit) :: args) -splitArgs tm args = (tm, args) - - -mkPat : TopContext -> (Raw, Icit) -> M Pattern -mkPat top (RAs fc as tm, icit) = - case !(mkPat top (tm, icit)) of - (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as) - (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}" - 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 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 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 - [] => pure $ PatVar fc icit nm - _ => error (getFC tm) "patvar applied to args" - ((RImplicit fc), []) => pure $ PatWild fc icit - ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments" - ((RLit fc lit), []) => pure $ PatLit fc lit - ((RLit fc y), b) => error fc "lit cannot be applied to arguments" - (a,b) => error (getFC a) "expected pat var or constructor, got \{show a}" - - -export -makeClause : TopContext -> (Raw, Raw) -> M Clause -makeClause top (lhs, rhs) = do - let (nm, args) = splitArgs lhs [] - pats <- traverse (mkPat top) args - pure $ MkClause (getFC lhs) [] pats rhs - - - --- we'll want both check and infer, we're augmenting a context --- so probably a continuation: --- Context -> List Decl -> (Context -> M a) -> M a -checkWhere : Context -> List Decl -> Raw -> Val -> M Tm -checkWhere ctx decls body ty = do - -- we're going to be very proscriptive here - let (TypeSig sigFC [name] rawtype :: decls) = decls - | x :: _ => error (getFC x) "expected type signature" - | _ => check ctx body ty - funTy <- check ctx rawtype (VU sigFC) - debug "where clause \{name} : \{pprint (names ctx) funTy}" - let (Def defFC name' clauses :: decls') = decls - | x :: _ => error (getFC x) "expected function definition" - | _ => error sigFC "expected function definition after this signature" - unless (name == name') $ error defFC "Expected def for \{name}" - -- REVIEW is this right, cribbed from my top level code - top <- get - clauses' <- traverse (makeClause top) clauses - vty <- eval ctx.env CBN funTy - debug "\{name} vty is \{show vty}" - let ctx' = extend ctx name vty - - -- if I lift, I need to namespace it, add args, and add args when - -- calling locally - -- context could hold a Name -> Val (not Tm because levels) to help with that - -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...) - -- But I'll attempt letrec first - tm <- buildTree ({ ctxFC := defFC} ctx') (MkProb clauses' vty) - vtm <- eval ctx'.env CBN tm - -- Should we run the rest with the definition in place? - -- I'm wondering if switching from bind to define will mess with metas - -- let ctx' = define ctx name vtm vty - pure $ LetRec sigFC name funTy tm !(checkWhere ctx' decls' body ty) - - -checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm -checkDone ctx [] body ty = do - debug "DONE-> check body \{show body} at \{show ty}" - -- TODO better dump context function - debugM $ showCtx ctx - -- Hack to try to get Combinatory working - -- we're trying to subst in solutions here. - env' <- for ctx.env $ \ val => do - ty <- quote (length ctx.env) val - -- This is not getting vars under lambdas - eval ctx.env CBV ty - types' <- for ctx.types $ \case - (nm,ty) => do - nty <- quote (length env') ty - ty' <- eval env' CBV nty - pure (nm, ty') - let ctx = { env := env', types := types' } ctx - debug "AFTER" - debugM $ showCtx ctx - -- I'm running an eval here to run case statements that are - -- unblocked by lets in the env. (Tree.newt:cmp) - -- The case eval code only works in the Tm -> Val case at the moment. - -- we don't have anything like `vapp` for case - ty <- quote (length ctx.env) ty - ty <- eval ctx.env CBN ty - - debug "check at \{show ty}" - got <- check ctx body ty - debug "DONE<- got \{pprint (names ctx) got}" - pure got -checkDone ctx ((x, PatWild _ _) :: xs) body ty = checkDone ctx xs body ty -checkDone ctx ((nm, (PatVar _ _ nm')) :: xs) body ty = checkDone ({ types $= rename } ctx) xs body ty - where - rename : Vect n (String, Val) -> Vect n (String, Val) - rename [] = [] - rename ((name, ty) :: xs) = - if name == nm - then (nm', ty) :: xs - else (name, ty) :: rename xs - -checkDone ctx ((x, pat) :: xs) body ty = error (getFC pat) "stray constraint \{x} /? \{show pat}" - --- need to run constructors, then run default - --- wild/var can come before 'x' so we need a list first -getLits : String -> List Clause -> List Literal -getLits nm [] = [] -getLits nm ((MkClause fc cons pats expr) :: cs) = case find ((nm==) . fst) cons of - Just (_, (PatLit _ lit)) => lit :: getLits nm cs - _ => getLits nm cs - - --- then build a lit case for each of those - -buildLitCase : Context -> Problem -> FC -> String -> Val -> Literal -> M CaseAlt -buildLitCase ctx prob fc scnm scty lit = do - - -- Constrain the scrutinee's variable to be lit value - let Just ix = findIndex ((==scnm) . fst) ctx.types - | Nothing => error ctx.ctxFC "\{scnm} not is scope?" - let lvl = lvl2ix (length ctx.env) (cast ix) - let scon : (Nat, Val) = (lvl, VLit fc lit) - ctx' <- updateContext ctx [scon] - let clauses = mapMaybe rewriteClause prob.clauses - - when (length clauses == 0) $ error ctx.ctxFC "Missing case for \{show lit} splitting \{scnm}" - tm <- buildTree ctx' (MkProb clauses prob.ty) - pure $ CaseLit lit tm - - where - -- FIXME - thread in M for errors - -- replace constraint with constraints on parameters, or nothing if non-matching clause - rewriteConstraint : List Constraint -> List Constraint -> Maybe (List Constraint) - rewriteConstraint [] acc = Just acc - rewriteConstraint (c@(nm, y) :: xs) acc = - if nm == scnm - then case y of - PatVar _ _ s => Just $ c :: (xs ++ acc) - PatWild _ _ => Just $ c :: (xs ++ acc) - PatLit fc lit' => if lit' == lit then Just $ (xs ++ acc) else Nothing - PatCon _ _ str ys as => Nothing -- error matching lit against constructor - else rewriteConstraint xs (c :: acc) - - rewriteClause : Clause -> Maybe Clause - rewriteClause (MkClause fc cons pats expr) = pure $ MkClause fc !(rewriteConstraint cons []) pats expr - - - -buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt) -buildLitCases ctx prob fc scnm scty = do - let lits = nub $ getLits scnm prob.clauses - alts <- traverse (buildLitCase ctx prob fc scnm scty) lits - -- TODO build default case - -- run getLits - -- buildLitCase for each - - let defclauses = filter isDefault prob.clauses - when (length defclauses == 0) $ error fc "no default for literal slot on \{show scnm}" - tm <- buildTree ctx (MkProb defclauses prob.ty) - - pure $ alts ++ [ CaseDefault tm ] - where - isDefault : Clause -> Bool - isDefault cl = case find ((==scnm) . fst) cl.cons of - Just (_, (PatVar _ _ _)) => True - Just (_, (PatWild _ _)) => True - Nothing => True - _ => False - --- 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 - where - go : Vect n (String,Val) -> Vect n (String,Val) - go Nil = Nil - go ((a,b) :: types) = if a == from then (to,b) :: types else (a,b) :: go types - --- This process is similar to extendPi, but we need to stop --- if one clause is short on patterns. -buildTree ctx (MkProb [] ty) = error emptyFC "no clauses" -buildTree ctx prob@(MkProb ((MkClause fc cons (x :: xs) expr) :: cs) (VPi _ str icit rig a b)) = do - let l = length ctx.env - let nm = fresh str -- "pat" - let ctx' = extend ctx nm a - -- type of the rest - clauses <- traverse (introClause nm icit) prob.clauses - -- REVIEW fc from a pat? - vb <- b $$ VVar fc l [<] - Lam fc nm icit rig <$> buildTree ctx' ({ clauses := clauses, ty := vb } prob) -buildTree ctx prob@(MkProb ((MkClause fc cons pats@(x :: xs) expr) :: cs) ty) = - error fc "Extra pattern variables \{show pats}" --- need to find some name we can split in (x :: xs) --- so LHS of constraint is name (or VVar - if we do Val) --- then run the split --- some of this is copied into check -buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do - debug "buildTree \{show constraints} \{show expr}" - let Just (scnm, pat) = findSplit constraints - | _ => do - debug "checkDone \{show constraints}" - checkDone ctx constraints expr ty - - debug "SPLIT on \{scnm} because \{show pat} \{show $ getFC pat}" - let Just (sctm, scty) = lookupName ctx scnm - | _ => error fc "Internal Error: can't find \{scnm} in environment" - - -- REVIEW We probably need to know this is a VRef before we decide to split on this slot.. - scty' <- unlet ctx.env scty >>= forceType ctx.env - -- TODO attempting to pick up Autos that could have been solved immediately - -- If we try on creation, we're looping at the moment, because of the possibility - -- of Ord a -> Ord b -> Ord (a \x b). Need to cut earlier when solving or switch to - -- Idris method... - scty' <- case scty' of - (VMeta fc1 ix sp) => do - case !(lookupMeta ix) of - (Solved _ k t) => forceType ctx.env scty' - (Unsolved _ k xs _ _ _) => do - top <- get - mc <- readIORef top.metaCtx - ignore $ solveAutos 0 - forceType ctx.env scty' - - _ => pure scty' - - case pat of - PatCon fc _ _ _ as => do - -- expand vars that may be solved, eval top level functions - debug "EXP \{show scty} -> \{show scty'}" - -- this is per the paper, but it would be nice to coalesce - -- default cases - cons <- getConstructors ctx (getFC pat) scty' - debug "CONS \{show $ map fst cons}" - alts <- traverse (buildCase ctx prob scnm scty') cons - debug "GOTALTS \{show alts}" - when (length (catMaybes alts) == 0) $ error (fc) "no alts for \{show scty'}" - pure $ Case fc sctm (catMaybes alts) - PatLit fc v => do - let tyname = litTyName v - case scty' of - (VRef fc1 nm x sp) => when (nm /= tyname) $ error fc "expected \{show scty} and got \{tyname}" - _ => error fc "expected \{show scty} and got \{tyname}" - -- need to run through all of the PatLits in this slot and then find a fallback - -- walk the list of patterns, stop if we hit a PatVar / PatWild, fail if we don't - alts <- buildLitCases ctx prob fc scnm scty - pure $ Case fc sctm alts - pat => error (getFC pat) "Internal error - tried to split on \{show pat}" - -showDef : Context -> List String -> Nat -> Val -> M String -showDef ctx names n v@(VVar _ n' [<]) = if n == n' then pure "" else pure "= \{pprint names !(quote ctx.lvl v)}" -showDef ctx names n v = pure "= \{pprint names !(quote ctx.lvl v)}" - --- desugar do -undo : FC -> List DoStmt -> M Raw -undo prev [] = error prev "do block must end in expression" -undo prev ((DoExpr fc tm) :: Nil) = pure tm --- TODO decide if we want to use >> or just >>= -undo prev ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) !(undo fc xs)) Explicit --- 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 lookupRaw nm !get of - Just _ => do - let nm = "$sc" - rest <- pure $ RCase fc (RVar fc nm) [MkAlt left !(undo fc xs)] - pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) - (RLam fc (BI fc nm Explicit Many) rest) Explicit - Nothing => - pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) - (RLam fc (BI fc' nm Explicit Many) !(undo fc xs)) Explicit -undo prev ((DoArrow fc left right alts) :: xs) = do - let nm = "$sc" - rest <- pure $ RCase fc (RVar fc nm) (MkAlt left !(undo fc xs) :: alts) - pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit) - (RLam fc (BI fc nm Explicit Many) rest) Explicit - -check ctx tm ty = case (tm, !(forceType ctx.env ty)) of - (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty - (RIf fc a b c, ty) => - let tm' = RCase fc a [ MkAlt (RVar (getFC b) "True") b, MkAlt (RVar (getFC c) "False") c ] in - check ctx tm' ty - (RDo fc stmts, ty) => check ctx !(undo fc stmts) ty - (RCase fc rsc alts, ty) => do - (sc, scty) <- infer ctx rsc - scty <- forceMeta scty - debug "SCTM \{pprint (names ctx) sc}" - debug "SCTY \{show scty}" - - let scnm = fresh "sc" - top <- get - clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause (getFC pat) [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts - -- buildCase expects scrutinee to be a name in the context, so we need to let it. - -- if it's a Bnd and not shadowed we could skip the let, but that's messy. - let ctx' = withPos (extend ctx scnm scty) (getFC tm) - pure $ Let fc scnm sc !(buildTree ctx' $ MkProb clauses ty) - - -- rendered in ProcessDecl - (RHole fc, ty) => freshMeta ctx fc ty User - - (t@(RLam fc (BI _ nm icit _) tm), ty@(VPi fc' nm' icit' rig a b)) => do - debug "icits \{nm} \{show icit} \{nm'} \{show icit'}" - if icit == icit' then do - let var = VVar fc (length ctx.env) [<] - let ctx' = extend ctx nm a - tm' <- check ctx' tm !(b $$ var) - pure $ Lam fc nm icit rig tm' - else if icit' /= Explicit then do - let var = VVar fc (length ctx.env) [<] - ty' <- b $$ var - -- use nm' here if we want them automatically in scope - sc <- check (extend ctx nm' a) t ty' - pure $ Lam fc nm' icit rig sc - else - error fc "Icity issue checking \{show t} at \{show ty}" - (t@(RLam _ (BI fc nm icit quant) tm), ty) => - error fc "Expected pi type, got \{!(prvalCtx ty)}" - - - (RLet fc nm ty v sc, rty) => do - ty' <- check ctx ty (VU emptyFC) - vty <- eval ctx.env CBN ty' - v' <- check ctx v vty - vv <- eval ctx.env CBN v' - let ctx' = define ctx nm vv vty - sc' <- check ctx' sc rty - pure $ Let fc nm v' sc' - - (RImplicit fc, ty) => freshMeta ctx fc ty Normal - - (tm, ty@(VPi fc nm' Implicit rig a b)) => do - let names = toList $ map fst ctx.types - debug "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} " - let var = VVar fc (length ctx.env) [<] - ty' <- b $$ var - debugM $ pure "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" - sc <- check (extend ctx nm' a) tm ty' - pure $ Lam (getFC tm) nm' Implicit rig sc - - (tm, ty@(VPi fc nm' Auto rig a b)) => do - let names = toList $ map fst ctx.types - debug "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} " - let var = VVar fc (length ctx.env) [<] - ty' <- b $$ var - debugM $ pure "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" - sc <- check (extend ctx nm' a) tm ty' - pure $ Lam (getFC tm) nm' Auto rig sc - - (tm,ty) => do - (tm', ty') <- infer ctx tm - (tm', ty') <- insert ctx tm' ty' - - let names = toList $ map fst ctx.types - debug "INFER \{show tm} to (\{pprint names tm'} : \{show ty'}) expect \{show ty}" - unifyCatch (getFC tm) ctx ty' ty - pure tm' - -infer ctx (RVar fc nm) = go 0 ctx.types - where - go : Nat -> Vect n (String, Val) -> M (Tm, Val) - go i [] = case lookupRaw nm !(get) of - Just (MkEntry _ name ty def) => do - debug "lookup \{name} as \{show def}" - 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 --- FIXME tightens up output but hardcodes a name --- infer ctx (RApp fc (RVar _ "_$_") u icit) = infer ctx u -infer ctx (RApp fc t u icit) = do - -- If the app is explicit, add any necessary metas - (icit, t, tty) <- case the Icit icit of - Explicit => do - (t, tty) <- infer ctx t - (t, tty) <- insert ctx t tty - pure (Explicit, t, tty) - Implicit => do - (t, tty) <- infer ctx t - pure (Implicit, t, tty) - Auto => do - (t, tty) <- infer ctx t - pure (Auto, t, tty) - - (a,b) <- case !(forceMeta tty) of - (VPi fc' str icit' rig a b) => if icit' == icit then pure (a,b) - else error fc "IcitMismatch \{show icit} \{show icit'}" - - -- If it's not a VPi, try to unify it with a VPi - -- TODO test case to cover this. - tty => do - debug "unify PI for \{show tty}" - a <- eval ctx.env CBN !(freshMeta ctx fc (VU emptyFC) Normal) - b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal - -- FIXME - I had to guess Many here. What are the side effects? - unifyCatch fc ctx tty (VPi fc ":ins" icit Many a b) - pure (a,b) - - u <- check ctx u a - pure (App fc t u, !(b $$ !(eval ctx.env CBN u))) - -infer ctx (RU fc) = pure (UU fc, VU fc) -- YOLO -infer ctx (RPi _ (BI fc nm icit quant) ty ty2) = do - ty' <- check ctx ty (VU fc) - vty' <- eval ctx.env CBN ty' - ty2' <- check (extend ctx nm vty') ty2 (VU fc) - pure (Pi fc nm icit quant ty' ty2', (VU fc)) -infer ctx (RLet fc nm ty v sc) = do - ty' <- check ctx ty (VU emptyFC) - vty <- eval ctx.env CBN ty' - v' <- check ctx v vty - vv <- eval ctx.env CBN v' - let ctx' = define ctx nm vv vty - (sc',scty) <- infer ctx' sc - pure $ (Let fc nm v' sc', scty) - -infer ctx (RAnn fc tm rty) = do - ty <- check ctx rty (VU fc) - vty <- eval ctx.env CBN ty - tm <- check ctx tm vty - pure (tm, vty) - -infer ctx (RLam _ (BI fc nm icit quant) tm) = do - a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env CBN - let ctx' = extend ctx nm a - (tm', b) <- infer ctx' tm - debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}" - pure $ (Lam fc nm icit quant tm', VPi fc nm icit quant a $ MkClosure ctx.env !(quote (S ctx.lvl) b)) - -infer ctx (RImplicit fc) = do - ty <- freshMeta ctx fc (VU emptyFC) Normal - vty <- eval ctx.env CBN ty - tm <- freshMeta ctx fc vty Normal - pure (tm, vty) - -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/orig/Lib/Erasure.idr b/orig/Lib/Erasure.idr deleted file mode 100644 index a20123e..0000000 --- a/orig/Lib/Erasure.idr +++ /dev/null @@ -1,102 +0,0 @@ -module Lib.Erasure - -import Lib.Types -import Data.Maybe -import Data.SnocList -import Lib.TopContext - -public export -EEnv : Type -EEnv = List (String, Quant, Maybe Tm) - --- TODO look into removing Nothing below, can we recover all of the types? --- Idris does this in `chk` for linearity checking. - --- check App at type - -getType : Tm -> M (Maybe Tm) -getType (Ref fc nm x) = do - top <- get - case lookup nm top of - Nothing => error fc "\{show nm} not in scope" - (Just (MkEntry _ name type def)) => pure $ Just type -getType tm = pure Nothing - -export -erase : EEnv -> Tm -> List (FC, Tm) -> M Tm - --- App a spine using type -eraseSpine : EEnv -> Tm -> List (FC, Tm) -> (ty : Maybe Tm) -> M Tm -eraseSpine env tm [] _ = pure tm -eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Zero a b)) = do - let u = Erased (getFC arg) - eraseSpine env (App fc t u) args (Just b) -eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Many a b)) = do - u <- erase env arg [] - -- TODO this seems wrong, we need to subst u into b to get the type - eraseSpine env (App fc t u) args (Just b) --- eraseSpine env t ((fc, arg) :: args) (Just ty) = do --- error fc "ceci n'est pas une ∏ \{showTm ty}" -- e.g. Bnd 1 -eraseSpine env t ((fc, arg) :: args) _ = do - u <- erase env arg [] - eraseSpine env (App fc t u) args Nothing - -doAlt : EEnv -> CaseAlt -> M CaseAlt --- REVIEW do we extend env? -doAlt env (CaseDefault t) = CaseDefault <$> erase env t [] -doAlt env (CaseCons name args t) = do - top <- get - let (Just (MkEntry _ str type def)) = lookup name top - | _ => error emptyFC "\{show name} dcon missing from context" - let env' = piEnv env type args - CaseCons name args <$> erase env' t [] - where - piEnv : EEnv -> Tm -> List String -> EEnv - piEnv env (Pi fc nm icit rig t u) (arg :: args) = piEnv ((arg, rig, Just t) :: env) u args - piEnv env _ _ = env - -doAlt env (CaseLit lit t) = CaseLit lit <$> erase env t [] - --- Check erasure and insert "Erased" value --- We have a solution for Erased values, so important thing here is checking. --- build stack, see what to do when we hit a non-app --- This is a little fuzzy because we don't have all of the types. -erase env t sp = case t of - (App fc u v) => erase env u ((fc,v) :: sp) - (Ref fc nm x) => do - top <- get - case lookup nm top of - Nothing => error fc "\{nm} not in scope" - (Just (MkEntry _ name type def)) => eraseSpine env t sp (Just type) - (Lam fc nm icit rig u) => Lam fc nm icit rig <$> erase ((nm, rig, Nothing) :: env) u [] - -- If we get here, we're looking at a runtime pi type - (Pi fc nm icit rig u v) => do - u' <- erase env u [] - v' <- erase ((nm, Many, Just u) :: env) v [] - eraseSpine env (Pi fc nm icit rig u' v') sp (Just $ UU emptyFC) - -- leaving as-is for now, we don't know the quantity of the apps - (Meta fc k) => pure t - (Case fc u alts) => do - -- REVIEW check if this pushes to env, and write that down or get an index on there - u' <- erase env u [] - alts' <- traverse (doAlt env) alts - eraseSpine env (Case fc u' alts') sp Nothing - (Let fc nm u v) => do - u' <- erase env u [] - v' <- erase ((nm, Many, Nothing) :: env) v [] - eraseSpine env (Let fc nm u' v') sp Nothing - (LetRec fc nm ty u v) => do - u' <- erase ((nm, Many, Just ty) :: env) u [] - v' <- erase ((nm, Many, Just ty) :: env) v [] - eraseSpine env (LetRec fc nm ty u' v') sp Nothing - (Bnd fc k) => do - case getAt k env of - Nothing => error fc "bad index \{show k}" - -- This is working, but empty FC - Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" - Just (nm, Many, ty) => eraseSpine env t sp ty - (UU fc) => eraseSpine env t sp (Just $ UU fc) - (Lit fc lit) => eraseSpine env t sp Nothing - Erased fc => error fc "erased value in relevant context" -- eraseSpine env t sp Nothing - - diff --git a/orig/Lib/Eval.idr b/orig/Lib/Eval.idr deleted file mode 100644 index f45129d..0000000 --- a/orig/Lib/Eval.idr +++ /dev/null @@ -1,312 +0,0 @@ -module Lib.Eval - -import Lib.Types -import Lib.TopContext - -import Data.IORef -import Data.Fin -import Data.List -import Data.SnocList -import Data.Vect -import Data.SortedMap - -export -eval : Env -> Mode -> Tm -> M Val - --- REVIEW everything is evalutated whether it's needed or not --- It would be nice if the environment were lazy. --- e.g. case is getting evaluated when passed to a function because --- of dependencies in pi-types, even if the dependency isn't used - -public export -infixl 8 $$ - -public export -($$) : {auto mode : Mode} -> Closure -> Val -> M Val -($$) {mode} (MkClosure env tm) u = eval (u :: env) mode tm - -export -vapp : Val -> Val -> M Val -vapp (VLam _ _ _ _ t) u = t $$ u -vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u) -vapp (VRef fc nm def sp) u = pure $ VRef fc nm def (sp :< u) -vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u) -vapp t u = error' "impossible in vapp \{show t} to \{show u}\n" - -export -vappSpine : Val -> SnocList Val -> M Val -vappSpine t [<] = pure t -vappSpine t (xs :< x) = do - rest <- vappSpine t xs - vapp rest x - -lookupVar : Env -> Nat -> Maybe Val -lookupVar env k = let l = length env in - if k > l - then Nothing - else case getAt (lvl2ix l k) env of - Just v@(VVar fc k' sp) => if k == k' then Nothing else Just v - Just v => Just v - Nothing => Nothing - --- hoping to apply what we got via pattern matching -export -unlet : Env -> Val -> M Val -unlet env t@(VVar fc k sp) = case lookupVar env k of - Just tt@(VVar fc' k' sp') => do - debug "lookup \{show k} is \{show tt}" - if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet env) - Just t => vappSpine t sp >>= unlet env - Nothing => do - debug "lookup \{show k} is Nothing in env \{show env}" - pure t -unlet env x = pure x - -export -tryEval : Env -> Val -> M (Maybe Val) -tryEval env (VRef fc k _ sp) = do - top <- get - case lookup k top of - Just (MkEntry _ name ty (Fn tm)) => - catchError ( - do - debug "app \{show name} to \{show sp}" - vtm <- eval [] CBN tm - debug "tm is \{render 90 $ pprint [] tm}" - val <- vappSpine vtm sp - case val of - VCase _ _ _ => pure Nothing - VLetRec _ _ _ _ _ => pure Nothing - v => pure $ Just v) - (\ _ => pure Nothing) - _ => pure Nothing -tryEval _ _ = pure Nothing - --- Force far enough to compare types -export -forceType : Env -> Val -> M Val -forceType env (VMeta fc ix sp) = do - meta <- lookupMeta ix - case meta of - (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp) - (Solved _ k t) => vappSpine t sp >>= forceType env -forceType env x = do - Just x' <- tryEval env x - | _ => pure x - forceType env x' - -evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val) -evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) = do - top <- get - if nm == name - then do - debug "ECase \{show nm} \{show sp} \{show nms} \{showTm t}" - go env (sp <>> []) nms - else case lookup nm top of - (Just (MkEntry _ str type (DCon k str1))) => evalCase env mode sc xs - -- bail for a stuck function - _ => pure Nothing - where - go : Env -> List Val -> List String -> M (Maybe Val) - go env (arg :: args) (nm :: nms) = go (arg :: env) args nms - go env args [] = do - t' <- eval env mode t - Just <$> vappSpine t' ([<] <>< args) - go env [] rest = pure Nothing --- REVIEW - this is handled in the caller already -evalCase env mode sc@(VVar fc k sp) alts = case lookupVar env k of - Just tt@(VVar fc' k' sp') => do - debug "lookup \{show k} is \{show tt}" - if k' == k - then pure Nothing - else do - val <- vappSpine (VVar fc' k' sp') sp - evalCase env mode val alts - Just t => do - val <- vappSpine t sp - evalCase env mode val alts - Nothing => do - debug "lookup \{show k} is Nothing in env \{show env}" - pure Nothing -evalCase env mode sc (CaseDefault u :: xs) = Just <$> eval (sc :: env) mode u -evalCase env mode sc cc = do - debug "CASE BAIL sc \{show sc} vs \{show cc}" - debug "env is \{show env}" - pure Nothing - --- TODO maybe add glueing - -eval env mode (Ref fc x def) = pure $ VRef fc x def [<] -eval env mode (App _ t u) = do - t' <- eval env mode t - u' <- eval env mode u - vapp t' u' -eval env mode (UU fc) = pure (VU fc) -eval env mode (Erased fc) = pure (VErased fc) -eval env mode (Meta fc i) = do - meta <- lookupMeta i - case meta of - (Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<] - (Solved _ k t) => pure $ t -eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t) -eval env mode (Pi fc x icit rig a b) = do - a' <- eval env mode a - pure $ VPi fc x icit rig a' (MkClosure env b) -eval env mode (Let fc nm t u) = do - t' <- eval env mode t - u' <- eval (VVar fc (length env) [<] :: env) mode u - pure $ VLet fc nm t' u' -eval env mode (LetRec fc nm ty t u) = do - ty' <- eval env mode ty - t' <- eval (VVar fc (length env) [<] :: env) mode t - u' <- eval (VVar fc (length env) [<] :: env) mode u - pure $ VLetRec fc nm ty' t' u' --- Here, we assume env has everything. We push levels onto it during type checking. --- I think we could pass in an l and assume everything outside env is free and --- translate to a level -eval env mode (Bnd fc i) = case getAt i env of - Just rval => pure rval - Nothing => error fc "Bad deBruin index \{show i}" -eval env mode (Lit fc lit) = pure $ VLit fc lit - -eval env mode tm@(Case fc sc alts) = do - -- TODO we need to be able to tell eval to expand aggressively here. - sc' <- eval env mode sc - sc' <- unlet env sc' -- try to expand lets from pattern matching - sc' <- forceType env sc' - vsc <- eval env mode sc - vcase <- evalCase env mode sc' alts - pure $ fromMaybe (VCase fc vsc alts) vcase - -export -quote : (lvl : Nat) -> Val -> M Tm - -quoteSp : (lvl : Nat) -> Tm -> SnocList Val -> M Tm -quoteSp lvl t [<] = pure t -quoteSp lvl t (xs :< x) = do - t' <- quoteSp lvl t xs - x' <- quote lvl x - pure $ App emptyFC t' x' - -quote l (VVar fc k sp) = if k < l - then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index - else error fc "Bad index in quote \{show k} depth \{show l}" -quote l (VMeta fc i sp) = do - meta <- lookupMeta i - case meta of - (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp - (Solved _ k t) => vappSpine t sp >>= quote l -quote l (VLam fc x icit rig t) = do - val <- t $$ VVar emptyFC l [<] - tm <- quote (S l) val - pure $ Lam fc x icit rig tm -quote l (VPi fc x icit rig a b) = do - a' <- quote l a - val <- b $$ VVar emptyFC l [<] - tm <- quote (S l) val - pure $ Pi fc x icit rig a' tm -quote l (VLet fc nm t u) = do - t' <- quote l t - u' <- quote (S l) u - pure $ Let fc nm t' u' -quote l (VLetRec fc nm ty t u) = do - ty' <- quote l ty - t' <- quote (S l) t - u' <- quote (S l) u - pure $ LetRec fc nm ty' t' u' -quote l (VU fc) = pure (UU fc) -quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp -quote l (VCase fc sc alts) = do - sc' <- quote l sc - pure $ Case fc sc' alts -quote l (VLit fc lit) = pure $ Lit fc lit -quote l (VErased fc) = pure $ Erased fc - --- Can we assume closed terms? --- ezoo only seems to use it at [], but essentially does this: -export -nf : Env -> Tm -> M Tm -nf env t = eval env CBN t >>= quote (length env) - -export -nfv : Env -> Tm -> M Tm -nfv env t = eval env CBV t >>= quote (length env) - -export -prvalCtx : {auto ctx : Context} -> Val -> M String -prvalCtx v = do - tm <- quote ctx.lvl v - pure $ interpolate $ pprint (toList $ map fst ctx.types) tm - -export -zonk : TopContext -> Nat -> Env -> Tm -> M Tm - -zonkBind : TopContext -> Nat -> Env -> Tm -> M Tm -zonkBind top l env tm = zonk top (S l) (VVar (getFC tm) l [<] :: env) tm - --- I don't know if app needs an FC... - -appSpine : Tm -> List Tm -> Tm -appSpine t [] = t -appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs - --- REVIEW When metas are subst in, the fc point elsewhere --- We might want to update when it is solved and update recursively? --- For errors, I think we want to pretend the code has been typed in place -tweakFC : FC -> Tm -> Tm -tweakFC fc (Bnd fc1 k) = Bnd fc k -tweakFC fc (Ref fc1 nm x) = Ref fc nm x -tweakFC fc (UU fc1) = UU fc -tweakFC fc (Meta fc1 k) = Meta fc k -tweakFC fc (Lam fc1 nm icit rig t) = Lam fc nm icit rig t -tweakFC fc (App fc1 t u) = App fc t u -tweakFC fc (Pi fc1 nm icit x t u) = Pi fc nm icit x t u -tweakFC fc (Case fc1 t xs) = Case fc t xs -tweakFC fc (Let fc1 nm t u) = Let fc nm t u -tweakFC fc (LetRec fc1 nm ty t u) = LetRec fc nm ty t u -tweakFC fc (Lit fc1 lit) = Lit fc lit -tweakFC fc (Erased fc1) = Erased fc - --- TODO replace this with a variant on nf -zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm -zonkApp top l env (App fc t u) sp = do - u' <- zonk top l env u - zonkApp top l env t (u' :: sp) -zonkApp top l env t@(Meta fc k) sp = do - meta <- lookupMeta k - case meta of - (Solved _ j v) => do - sp' <- traverse (eval env CBN) sp - debug "zonk \{show k} -> \{show v} spine \{show sp'}" - foo <- vappSpine v ([<] <>< sp') - debug "-> result is \{show foo}" - tweakFC fc <$> quote l foo - (Unsolved x j xs _ _ _) => pure $ appSpine t sp -zonkApp top l env t sp = do - t' <- zonk top l env t - pure $ appSpine t' sp - -zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt -zonkAlt top l env (CaseDefault t) = CaseDefault <$> zonkBind top l env t -zonkAlt top l env (CaseLit lit t) = CaseLit lit <$> zonkBind top l env t -zonkAlt top l env (CaseCons name args t) = CaseCons name args <$> go l env args t - where - go : Nat -> Env -> List String -> Tm -> M Tm - go l env [] tm = zonk top l env t - go l env (x :: xs) tm = go (S l) (VVar (getFC tm) l [<] :: env) xs tm - -zonk top l env t = case t of - (Meta fc k) => zonkApp top l env t [] - (Lam fc nm icit rig u) => Lam fc nm icit rig <$> (zonk top (S l) (VVar fc l [<] :: env) u) - (App fc t u) => do - u' <- zonk top l env u - zonkApp top l env t [u'] - (Pi fc nm icit rig a b) => Pi fc nm icit rig <$> zonk top l env a <*> zonkBind top l env b - (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u - (LetRec fc nm ty t u) => LetRec fc nm <$> zonk top l env ty <*> zonkBind top l env t <*> zonkBind top l env u - (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts - UU fc => pure $ UU fc - Lit fc lit => pure $ Lit fc lit - Bnd fc ix => pure $ Bnd fc ix - Ref fc ix def => pure $ Ref fc ix def - Erased fc => pure $ Erased fc diff --git a/orig/Lib/Parser.idr b/orig/Lib/Parser.idr deleted file mode 100644 index 85e93ef..0000000 --- a/orig/Lib/Parser.idr +++ /dev/null @@ -1,616 +0,0 @@ -module Lib.Parser - -import Data.Maybe -import Data.String -import Lib.Parser.Impl -import Lib.Syntax -import Lib.Token -import Lib.Types - -ident : Parser String -ident = token Ident <|> token MixFix - -uident : Parser String -uident = token UIdent - -parenWrap : Parser a -> Parser a -parenWrap pa = do - sym "(" - t <- pa - sym ")" - pure t - -braces : Parser a -> Parser a -braces pa = do - sym "{" - t <- pa - sym "}" - pure t - -dbraces : Parser a -> Parser a -dbraces pa = do - sym "{{" - t <- pa - sym "}}" - pure t - - -optional : Parser a -> Parser (Maybe a) -optional pa = Just <$> pa <|> pure Nothing - -stringLit : Parser Raw -stringLit = do - fc <- getPos - t <- token StringKind - pure $ RLit fc (LString (cast t)) - - --- typeExpr is term with arrows. -export -typeExpr : Parser Raw -export -term : (Parser Raw) - -interp : Parser Raw -interp = token StartInterp *> term <* token EndInterp - - -interpString : Parser Raw -interpString = do - -- fc <- getPos - ignore $ token StartQuote - part <- term - parts <- many (stringLit <|> interp) - ignore $ token EndQuote - pure $ foldl append part parts - where - append : Raw -> Raw -> Raw - append t u = - let fc = getFC t in - (RApp (getFC t) (RApp fc (RVar fc "_++_") t Explicit) u Explicit) - -intLit : Parser Raw -intLit = do - fc <- getPos - t <- token Number - pure $ RLit fc (LInt (cast t)) - - -charLit : Parser Raw -charLit = do - fc <- getPos - v <- token Character - pure $ RLit fc (LChar $ assert_total $ strIndex v 0) - -lit : Parser Raw -lit = intLit <|> interpString <|> stringLit <|> charLit - - - --- helpful when we've got some / many and need FC for each -addPos : Parser a -> Parser (FC, a) -addPos pa = (,) <$> getPos <*> pa - -asAtom : Parser Raw -asAtom = do - fc <- getPos - nm <- ident - asPat <- optional $ keyword "@" *> parenWrap typeExpr - case asPat of - Just exp => pure $ RAs fc nm exp - Nothing => pure $ RVar fc nm - --- the inside of Raw -atom : Parser Raw -atom = RU <$> getPos <* keyword "U" - -- <|> RVar <$> getPos <*> ident - <|> asAtom - <|> RVar <$> getPos <*> uident - <|> RVar <$> getPos <*> token Projection - <|> lit - <|> RImplicit <$> getPos <* keyword "_" - <|> RHole <$> getPos <* keyword "?" - <|> parenWrap typeExpr - --- Argument to a Spine -pArg : Parser (Icit,FC,Raw) -pArg = do - fc <- getPos - (Explicit,fc,) <$> atom - <|> (Implicit,fc,) <$> braces typeExpr - <|> (Auto,fc,) <$> dbraces typeExpr - -AppSpine : Type -AppSpine = List (Icit,FC,Raw) - -pratt : Operators -> Int -> String -> Raw -> AppSpine -> Parser (Raw, AppSpine) -pratt ops prec stop left spine = do - (left, spine) <- runPrefix stop left spine - let (left, spine) = projectHead left spine - let spine = runProject spine - case spine of - [] => pure (left, []) - ((Explicit, fc, tm@(RVar x nm)) :: rest) => - if nm == stop then pure (left,spine) else - case lookup nm ops of - Just (MkOp name p fix False rule) => if p < prec - then pure (left, spine) - else - runRule p fix stop rule (RApp fc (RVar fc name) left Explicit) rest - Just _ => fail "expected operator" - Nothing => - if isPrefixOf "." nm - then pratt ops prec stop (RApp (getFC tm) tm left Explicit) rest - else pratt ops prec stop (RApp (getFC left) left tm Explicit) rest - ((icit, fc, tm) :: rest) => pratt ops prec stop (RApp (getFC left) left tm icit) rest - where - projectHead : Raw -> AppSpine -> (Raw, AppSpine) - projectHead t sp@((Explicit, fc', RVar fc nm) :: rest) = - if isPrefixOf "." nm - then projectHead (RApp fc (RVar fc nm) t Explicit) rest - else (t,sp) - projectHead t sp = (t, sp) - - -- we need to check left/AppSpine first - -- we have a case above for when the next token is a projection, but - -- we need this to make projection bind tighter than app - runProject : AppSpine -> AppSpine - runProject (t@(Explicit, fc', tm) :: u@(Explicit, _, RVar fc nm) :: rest) = - if isPrefixOf "." nm - then runProject ((Explicit, fc', RApp fc (RVar fc nm) tm Explicit) :: rest) - else (t :: u :: rest) - runProject tms = tms - - -- left has our partially applied operator and we're picking up args - -- for the rest of the `_` - runRule : Int -> Fixity -> String -> List String -> Raw -> AppSpine -> Parser (Raw,AppSpine) - runRule p fix stop [] left spine = pure (left,spine) - runRule p fix stop [""] left spine = do - let pr = case fix of - InfixR => p - _ => p + 1 - case spine of - ((_, fc, right) :: rest) => do - (right, rest) <- pratt ops pr stop right rest - pratt ops prec stop (RApp (getFC left) left right Explicit) rest - _ => fail "trailing operator" - - runRule p fix stop (nm :: rule) left spine = do - let ((_,_,right)::rest) = spine | _ => fail "short" - (right,rest) <- pratt ops 0 nm right rest -- stop!! - let ((_,fc',RVar fc name) :: rest) = rest - | _ => fail "expected \{nm}" - - if name == nm - then runRule p fix stop rule (RApp (getFC left) left right Explicit) rest - else fail "expected \{nm}" - - -- run any prefix operators - runPrefix : String -> Raw -> AppSpine -> Parser (Raw, AppSpine) - runPrefix stop (RVar fc nm) spine = - case lookup nm ops of - -- TODO False should be an error here - Just (MkOp name p fix True rule) => do - runRule p fix stop rule (RVar fc name) spine - _ => - pure (left, spine) - runPrefix stop left spine = pure (left, spine) - - - -parseOp : Parser Raw -parseOp = do - fc <- getPos - ops <- getOps - hd <- atom - rest <- many pArg - (res, []) <- pratt ops 0 "" hd rest - | _ => fail "extra stuff" - pure res - - --- TODO case let? We see to only have it for `do` --- try (keyword "let" >> sym "(") - -export -letExpr : Parser Raw -letExpr = do - keyword "let" - alts <- startBlock $ someSame $ letAssign - keyword' "in" - scope <- typeExpr - pure $ foldl (\ acc, (n,fc,ty,v) => RLet fc n (fromMaybe (RImplicit fc) ty) v acc) scope (reverse alts) - where - letAssign : Parser (Name,FC,Maybe Raw,Raw) - letAssign = do - fc <- getPos - name <- ident - -- TODO type assertion - ty <- optional (keyword ":" *> typeExpr) - keyword "=" - t <- typeExpr - pure (name,fc,ty,t) - -pLamArg : Parser (Icit, String, Maybe Raw) -pLamArg = (Implicit,,) <$> braces (ident <|> uident) <*> optional (sym ":" >> typeExpr) - <|> (Auto,,) <$> dbraces (ident <|> uident) <*> optional (sym ":" >> typeExpr) - <|> (Explicit,,) <$> parenWrap (ident <|> uident) <*> optional (sym ":" >> typeExpr) - <|> (Explicit,,Nothing) <$> (ident <|> uident) - <|> (Explicit,"_",Nothing) <$ keyword "_" - --- lam: λ {A} {b : A} (c : Blah) d e f. something -export -lamExpr : Parser Raw -lamExpr = do - pos <- getPos - keyword "\\" <|> keyword "λ" - args <- some $ addPos pLamArg - keyword "=>" - scope <- typeExpr - pure $ foldr (\(fc, icit, name, ty), sc => RLam pos (BI fc name icit Many) sc) scope args - -caseAlt : Parser RCaseAlt -caseAlt = do - pat <- typeExpr - keyword "=>" - t <- term - pure $ MkAlt pat t - -export -caseExpr : Parser Raw -caseExpr = do - fc <- getPos - keyword "case" - sc <- term - keyword "of" - alts <- startBlock $ someSame $ caseAlt - pure $ RCase fc sc alts - -caseLamExpr : Parser Raw -caseLamExpr = do - fc <- getPos - try ((keyword "\\" <|> keyword "λ") *> keyword "case") - alts <- startBlock $ someSame $ caseAlt - pure $ RLam fc (BI fc "$case" Explicit Many) $ RCase fc (RVar fc "$case") alts - -doExpr : Parser Raw -doStmt : Parser DoStmt - -caseLet : Parser Raw -caseLet = do - -- look ahead so we can fall back to normal let - fc <- getPos - try (keyword "let" >> sym "(") - pat <- typeExpr - sym ")" - keyword "=" - sc <- typeExpr - alts <- startBlock $ manySame $ sym "|" *> caseAlt - keyword "in" - body <- term - pure $ RCase fc sc (MkAlt pat body :: alts) - -doCaseLet : Parser DoStmt -doCaseLet = do - -- look ahead so we can fall back to normal let - -- Maybe make it work like arrow? - fc <- getPos - try (keyword "let" >> sym "(") - pat <- typeExpr - sym ")" - keyword "=" - sc <- typeExpr - alts <- startBlock $ manySame $ sym "|" *> caseAlt - bodyFC <- getPos - body <- RDo <$> getPos <*> someSame doStmt - pure $ DoExpr fc (RCase fc sc (MkAlt pat body :: alts)) - -doArrow : Parser DoStmt -doArrow = do - fc <- getPos - left <- typeExpr - (Just _) <- optional $ keyword "<-" - | _ => pure $ DoExpr fc left - right <- term - alts <- startBlock $ manySame $ sym "|" *> caseAlt - pure $ DoArrow fc left right alts - -doStmt - = doCaseLet - <|> DoLet <$> getPos <* keyword "let" <*> ident <* keyword "=" <*> term - <|> doArrow - -doExpr = RDo <$> getPos <* keyword "do" <*> (startBlock $ someSame doStmt) - -ifThenElse : Parser Raw -ifThenElse = do - fc <- getPos - keyword "if" - a <- term - keyword "then" - b <- term - keyword "else" - c <- term - pure $ RIf fc a b c - -term' : Parser Raw - -term' = caseExpr - <|> caseLet - <|> letExpr - <|> caseLamExpr - <|> lamExpr - <|> doExpr - <|> ifThenElse - -- Make this last for better error messages - <|> parseOp - -term = do - t <- term' - rest <- many ((,) <$> getPos <* keyword "$" <*> term') - pure $ apply t rest - where - apply : Raw -> List (FC,Raw) -> Raw - apply t [] = t - apply t ((fc,x) :: xs) = RApp fc t (apply x xs) Explicit - -varname : Parser String -varname = (ident <|> uident <|> keyword "_" *> pure "_") - -quantity : Parser Quant -quantity = fromMaybe Many <$> optional (Zero <$ keyword "0") - -ebind : Parser Telescope -ebind = do - -- don't commit until we see the ":" - sym "(" - quant <- quantity - names <- try (some (addPos varname) <* sym ":") - ty <- typeExpr - sym ")" - pure $ map (\(pos, name) => (BI pos name Explicit quant, ty)) names - -ibind : Parser Telescope -ibind = do - -- I've gone back and forth on this, but I think {m a b} is more useful than {Nat} - sym "{" - quant <- quantity - names <- (some (addPos varname)) - ty <- optional (sym ":" *> typeExpr) - sym "}" - pure $ map (\(pos,name) => (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)) names - -abind : Parser Telescope -abind = do - -- for this, however, it would be nice to allow {{Monad A}} - sym "{{" - name <- optional $ try (addPos varname <* sym ":") - ty <- typeExpr - sym "}}" - case name of - Just (pos,name) => pure [(BI pos name Auto Many, ty)] - Nothing => pure [(BI (getFC ty) "_" Auto Many, ty)] - -arrow : Parser Unit -arrow = sym "->" <|> sym "→" - --- Collect a bunch of binders (A : U) {y : A} -> ... - -forAll : Parser Raw -forAll = do - keyword "forall" <|> keyword "∀" - all <- some (addPos varname) - keyword "." - scope <- typeExpr - pure $ foldr (\ (fc, n), sc => RPi fc (BI fc n Implicit Zero) (RImplicit fc) sc) scope all - -binders : Parser Raw -binders = do - binds <- many (abind <|> ibind <|> ebind) - arrow - scope <- typeExpr - pure $ foldr mkBind scope (join binds) - where - mkBind : (BindInfo, Raw) -> Raw -> Raw - mkBind (info, ty) scope = RPi (getFC info) info ty scope - -typeExpr - = binders - <|> forAll - <|> do - fc <- getPos - exp <- term - scope <- optional (arrow *> typeExpr) - case scope of - Nothing => pure exp - -- consider Maybe String to represent missing - (Just scope) => pure $ RPi fc (BI fc "_" Explicit Many) exp scope - --- And top level stuff - -export -parseSig : Parser Decl -parseSig = TypeSig <$> getPos <*> try (some (ident <|> uident <|> token Projection) <* keyword ":") <*> typeExpr - -parseImport : Parser Import -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 -parseMixfix : Parser Decl -parseMixfix = do - fc <- getPos - fix <- InfixL <$ keyword "infixl" - <|> InfixR <$ keyword "infixr" - <|> Infix <$ keyword "infix" - prec <- token Number - ops <- some $ token MixFix - for_ ops $ \ op => addOp op (cast prec) fix - pure $ PMixFix fc ops (cast prec) fix - -getName : Raw -> Parser String -getName (RVar x nm) = pure nm -getName (RApp x t u icit) = getName t -getName tm = fail "bad LHS" - - -export -parseDef : Parser Decl -parseDef = do - fc <- getPos - t <- typeExpr - nm <- getName t - keyword "=" - body <- typeExpr - wfc <- getPos - w <- optional $ do - keyword "where" - startBlock $ manySame $ (parseSig <|> parseDef) - let body = maybe body (\ decls => RWhere wfc decls body) w - -- these get collected later - pure $ Def fc nm [(t, body)] -- [MkClause fc [] t body] - -export -parsePType : Parser Decl -parsePType = do - fc <- getPos - keyword "ptype" - id <- uident - ty <- optional $ do - keyword ":" - typeExpr - pure $ PType fc id ty - -parsePFunc : Parser Decl -parsePFunc = do - fc <- getPos - keyword "pfunc" - nm <- ident - uses <- optional (keyword "uses" >> parenWrap (many $ uident <|> ident <|> token MixFix)) - keyword ":" - ty <- typeExpr - keyword ":=" - src <- cast <$> token JSLit - pure $ PFunc fc nm (fromMaybe [] uses) ty src - - -parseShortData : Parser Decl -parseShortData = do - fc <- getPos - keyword "data" - lhs <- typeExpr - keyword "=" - sigs <- sepBy (keyword "|") typeExpr - pure $ ShortData fc lhs sigs - -export -parseData : Parser Decl -parseData = do - fc <- getPos - -- commit when we hit ":" - name <- try $ (keyword "data" *> (uident <|> ident <|> token MixFix) <* keyword ":") - ty <- typeExpr - keyword "where" - decls <- startBlock $ manySame $ parseSig - pure $ Data fc name ty decls - -nakedBind : Parser Telescope -nakedBind = do - names <- some (addPos varname) - pure $ map (\(pos,name) => (BI pos name Explicit Many, RImplicit pos)) names - -export -parseRecord : Parser Decl -parseRecord = do - fc <- getPos - keyword "record" - name <- uident - teles <- many $ ebind <|> nakedBind - keyword "where" - cname <- optional $ keyword "constructor" *> (uident <|> token MixFix) - decls <- startBlock $ manySame $ parseSig - pure $ Record fc name (join teles) cname decls - - -export -parseClass : Parser Decl -parseClass = do - fc <- getPos - keyword "class" - name <- uident - teles <- many $ ebind <|> nakedBind - keyword "where" - decls <- startBlock $ manySame $ parseSig - pure $ Class fc name (join teles) decls - -export -parseInstance : Parser Decl -parseInstance = do - fc <- getPos - keyword "instance" - ty <- typeExpr - -- is it a forward declaration - (Just _) <- optional $ keyword "where" - | _ => pure $ Instance fc ty Nothing - decls <- startBlock $ manySame $ parseDef - pure $ Instance fc ty (Just decls) - --- Not sure what I want here. --- I can't get a Tm without a type, and then we're covered by the other stuff -parseNorm : Parser Decl -parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr - -export -parseDecl : Parser Decl -parseDecl = parseMixfix <|> parsePType <|> parsePFunc - <|> parseNorm <|> parseData <|> parseShortData <|> parseSig <|> parseDef - <|> parseClass <|> parseInstance <|> parseRecord - - -export -parseModHeader : Parser (FC, String) -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) -parseImports = manySame $ parseImport - -export -parseMod : Parser Module -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 - -public export -data ReplCmd = - Def Decl - | Norm Raw -- or just name? - | Check Raw - - --- Eventually I'd like immediate actions in the file, like lean, but I --- also want to REPL to work and we can do that first. -export -parseRepl : Parser ReplCmd -parseRepl = Def <$> parseDecl <|> Norm <$ keyword "#nf" <*> typeExpr - <|> Check <$ keyword "#check" <*> typeExpr diff --git a/orig/Lib/Parser/Impl.idr b/orig/Lib/Parser/Impl.idr deleted file mode 100644 index cac7c58..0000000 --- a/orig/Lib/Parser/Impl.idr +++ /dev/null @@ -1,219 +0,0 @@ -module Lib.Parser.Impl - -import Prelude -import Lib.Token -import Lib.Common -import Data.String -import Data.Nat -import Data.List1 -import Data.SortedMap - -public export -TokenList : Type -TokenList = List BTok - --- Result of a parse -public export -data Result : Type -> Type where - OK : a -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a - Fail : Bool -> Error -> (toks : TokenList) -> (com : Bool) -> Operators -> Result a - -export -Functor Result where - map f (OK a toks com ops) = OK (f a) toks com ops - map _ (Fail fatal err toks com ops) = Fail fatal err toks com ops - --- So sixty just has a newtype function here now (probably for perf). --- A record might be more ergonomic, but would require a record impl before --- self hosting. - --- FC is a line and column for indents. The idea being that we check --- either the col < tokCol or line == tokLine, enabling sameLevel. - --- We need State for operators (or postpone that to elaboration) --- Since I've already built out the pratt stuff, I guess I'll --- leave it in the parser for now - --- This is a Reader in FC, a State in Operators, Commit flag, TokenList - -export -data Parser a = P (TokenList -> Bool -> Operators -> (lc : FC) -> Result a) - -export -runP : Parser a -> TokenList -> Bool -> Operators -> FC -> Result a -runP (P f) = f - --- FIXME no filename, also half the time it is pointing at the token after the error -error : String -> TokenList -> String -> Error -error fn [] msg = E (MkFC fn (0,0)) msg -error fn ((MkBounded val (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg - -export -parse : String -> Parser a -> TokenList -> Either Error a -parse fn pa toks = case runP pa toks False empty (MkFC fn (-1,-1)) of - Fail fatal err toks com ops => Left err - OK a [] _ _ => Right a - OK a ts _ _ => Left (error fn ts "Extra toks") - -||| Intended for parsing a top level declaration -export -partialParse : String -> Parser a -> Operators -> TokenList -> Either (Error, TokenList) (a, Operators, TokenList) -partialParse fn pa ops toks = case runP pa toks False ops (MkFC fn (0,0)) of - Fail fatal err toks com ops => Left (err, toks) - OK a ts _ ops => Right (a,ops,ts) - --- I think I want to drop the typeclasses for v1 - -export -try : Parser a -> Parser a -try (P pa) = P $ \toks,com,ops,col => case pa toks com ops col of - (Fail x err toks com ops) => Fail x err toks False ops - res => res - -export -fail : String -> Parser a -fail msg = P $ \toks,com,ops,col => Fail False (error col.file toks msg) toks com ops - -export -fatal : String -> Parser a -fatal msg = P $ \toks,com,ops,col => Fail True (error col.file toks msg) toks com ops - -export -getOps : Parser (Operators) -getOps = P $ \ toks, com, ops, col => OK ops toks com ops - -export -addOp : String -> Int -> Fixity -> Parser () -addOp nm prec fix = P $ \ toks, com, ops, col => - let parts = split (=='_') nm in - case parts of - "" ::: key :: rule => OK () toks com (insert key (MkOp nm prec fix False rule) ops) - key ::: rule => OK () toks com (insert key (MkOp nm prec fix True rule) ops) - - - -export -Functor Parser where - map f (P pa) = P $ \ toks, com, ops, col => map f (pa toks com ops col) - -export -Applicative Parser where - pure pa = P (\ toks, com, ops, col => OK pa toks com ops) - P pab <*> P pa = P $ \toks,com,ops,col => - case pab toks com ops col of - Fail fatal err toks com ops => Fail fatal err toks com ops - OK f toks com ops => - case pa toks com ops col of - (OK x toks com ops) => OK (f x) toks com ops - (Fail fatal err toks com ops) => Fail fatal err toks com ops - --- Second argument lazy so we don't have circular refs when defining parsers. -export -(<|>) : Parser a -> (Parser a) -> Parser a -(P pa) <|> (P pb) = P $ \toks,com,ops,col => - case pa toks False ops col of - OK a toks' _ ops => OK a toks' com ops - Fail True err toks' com ops => Fail True err toks' com ops - Fail fatal err toks' True ops => Fail fatal err toks' True ops - Fail fatal err toks' False ops => pb toks com ops col - -export -Monad Parser where - P pa >>= pab = P $ \toks,com,ops,col => - case pa toks com ops col of - (OK a toks com ops) => runP (pab a) toks com ops col - (Fail fatal err xs x ops) => Fail fatal err xs x ops - - -satisfy : (BTok -> Bool) -> String -> Parser String -satisfy f msg = P $ \toks,com,ops,col => - case toks of - (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error col.file toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops - [] => Fail False (error col.file toks "\{msg} at EOF") toks com ops - -export -commit : Parser () -commit = P $ \toks,com,ops,col => OK () toks True ops - - -export some : Parser a -> Parser (List a) -export many : Parser a -> Parser (List a) -some p = (::) <$> p <*> many p -many p = some p <|> pure [] - --- one or more `a` seperated by `s` -export -sepBy : Parser s -> Parser a -> Parser (List a) -sepBy s a = (::) <$> a <*> many (s *> a) - -export -getPos : Parser FC -getPos = P $ \toks, com, ops, indent => case toks of - [] => OK emptyFC toks com ops - (t :: ts) => OK (MkFC indent.file (getStart t)) toks com ops - -||| Start an indented block and run parser in it -export -startBlock : Parser a -> Parser a -startBlock (P p) = P $ \toks,com,ops,indent => case toks of - [] => p toks com ops indent - (t :: _) => - -- If next token is at or before the current level, we've got an empty block - let (tl,tc) = getStart t in - let (MkFC file (line,col)) = indent in - p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc)) - -||| Assert that parser starts at our current column by -||| checking column and then updating line to match the current -export -sameLevel : Parser a -> Parser a -sameLevel (P p) = P $ \toks, com, ops, indent => case toks of - [] => p toks com ops indent - (t :: _) => - let (tl,tc) = getStart t in - let (MkFC file (line,col)) = indent in - if tc == col then p toks com ops (MkFC file (tl, col)) - else if col < tc then Fail False (error file toks "unexpected indent") toks com ops - else Fail False (error file toks "unexpected indent") toks com ops - -export -someSame : Parser a -> Parser (List a) -someSame pa = some $ sameLevel pa - -export -manySame : Parser a -> Parser (List a) -manySame pa = many $ sameLevel pa - -||| check indent on next token and run parser -export -indented : Parser a -> Parser a -indented (P p) = P $ \toks,com,ops,indent => case toks of - [] => p toks com ops indent - (t::_) => - let (tl,tc) = getStart t - in if tc > fcCol indent || tl == fcLine indent then p toks com ops indent - else Fail False (error (file indent) toks "unexpected outdent") toks com ops - -||| expect token of given kind -export -token' : Kind -> Parser String -token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token" - -export -keyword' : String -> Parser () --- FIXME make this an appropriate whitelist -keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected \{kw}" - -||| expect indented token of given kind -export -token : Kind -> Parser String -token = indented . token' - -export -keyword : String -> Parser () -keyword kw = indented $ keyword' kw - -export -sym : String -> Parser () -sym = keyword - diff --git a/orig/Lib/Prettier.idr b/orig/Lib/Prettier.idr deleted file mode 100644 index ee1ef9a..0000000 --- a/orig/Lib/Prettier.idr +++ /dev/null @@ -1,149 +0,0 @@ -||| A prettier printer, Philip Wadler -||| https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf -module Lib.Prettier - -import Data.String -import Data.Nat -import Data.Maybe - -||| `Doc` is a pretty printing document. Constructors are private, use -||| methods below. `Alt` in particular has some invariants on it, see paper -||| for details. (Something along the lines of "the first line of left is not -||| bigger than the first line of the right".) -export -data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc - -||| The original paper had a List-like structure Doc (the above was DOC) which -||| had Empty and a tail on Text and Line. -data Item = TEXT String | LINE Nat - -export -empty : Doc -empty = Empty - -flatten : Doc -> Doc -flatten Empty = Empty -flatten (Seq x y) = Seq (flatten x) (flatten y) -flatten (Nest i x) = flatten x -flatten Line = Text " " -flatten (Text str) = Text str -flatten (Alt x y) = flatten x - -group : Doc -> Doc -group x = Alt (flatten x) x - --- TODO - we can accumulate snoc and cat all at once -layout : List Item -> SnocList String -> String -layout [] acc = fastConcat $ acc <>> [] -layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate k ' ') -layout (TEXT str :: x) acc = layout x (acc :< str) - -||| Whether a documents first line fits. -fits : Nat -> List Item -> Bool -fits w ((TEXT s) :: xs) = if length s < w then fits (w `minus` length s) xs else False -fits w _ = True - --- vs Wadler, we're collecting the left side as a SnocList to prevent --- blowing out the stack on the Text case. The original had DOC as --- a Linked-List like structure (now List Item) - --- I've now added a `fit` boolean to indicate if we should cut when we hit the line length --- Wadler was relying on laziness to stop the first branch before LINE if necessary -be : Bool -> SnocList Item -> Nat -> Nat -> List (Nat, Doc) -> Maybe (List Item) -be fit acc w k [] = Just (acc <>> []) -be fit acc w k ((i, Empty) :: xs) = be fit acc w k xs -be fit acc w k ((i, Line) :: xs) = (be False (acc :< LINE i) w i xs) -be fit acc w k ((i, (Text s)) :: xs) = - if not fit || (k + length s < w) - then (be fit (acc :< TEXT s) w (k + length s) xs) - else Nothing -be fit acc w k ((i, (Nest j x)) :: xs) = be fit acc w k ((i + j, x) :: xs) -be fit acc w k ((i, (Seq x y)) :: xs) = be fit acc w k ((i,x) :: (i,y) :: xs) -be fit acc w k ((i, (Alt x y)) :: xs) = - (acc <>>) <$> (be True [<] w k ((i,x) :: xs) <|> be fit [<] w k ((i,y) :: xs)) - -best : Nat -> Nat -> Doc -> List Item -best w k x = fromMaybe [] $ be False [<] w k [(0,x)] - --- Public interface -public export -interface Pretty a where - pretty : a -> Doc - -export -render : Nat -> Doc -> String -render w x = layout (best w 0 x) [<] - -public export -Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y) - --- Match System.File so we don't get warnings -public export -infixl 5 - -export -line : Doc -line = Line - -export -text : String -> Doc -text = Text - -export -nest : Nat -> Doc -> Doc -nest = Nest - -export -(++) : Doc -> Doc -> Doc -x ++ y = Seq x y - -export -() : Doc -> Doc -> Doc -x y = x ++ line ++ y - -||| fold, but doesn't emit extra nil -export -folddoc : (Doc -> Doc -> Doc) -> List Doc -> Doc -folddoc f [] = Empty -folddoc f [x] = x -folddoc f (x :: xs) = f x (folddoc f xs) - -||| separate with space -export -spread : List Doc -> Doc -spread = folddoc (<+>) - -||| separate with new lines -export -stack : List Doc -> Doc -stack = folddoc () - -||| bracket x with l and r, indenting contents on new line -export -bracket : String -> Doc -> String -> Doc -bracket l x r = group (text l ++ nest 2 (line ++ x) ++ line ++ text r) - -export -infixl 5 <+/> - -||| Either space or newline -export -(<+/>) : Doc -> Doc -> Doc -x <+/> y = x ++ Alt (text " ") line ++ y - -||| Reformat some docs to fill. Not sure if I want this precise behavior or not. -export -fill : List Doc -> Doc -fill [] = Empty -fill [x] = x -fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x fill (y :: xs)) - -||| separate with comma -export -commaSep : List Doc -> Doc -commaSep = folddoc (\a, b => a ++ text "," <+/> b) - -||| If we stick Doc into a String, try to avoid line-breaks via `flatten` -public export -Interpolation Doc where - interpolate = render 80 . flatten diff --git a/orig/Lib/ProcessDecl.idr b/orig/Lib/ProcessDecl.idr deleted file mode 100644 index 87e09d3..0000000 --- a/orig/Lib/ProcessDecl.idr +++ /dev/null @@ -1,426 +0,0 @@ -module Lib.ProcessDecl - -import Data.IORef -import Data.String -import Data.Vect -import Data.List -import Data.Maybe - -import Lib.Elab -import Lib.Parser -import Lib.Syntax -import Lib.TopContext -import Lib.Eval -import Lib.Types -import Lib.Util -import Lib.Erasure - -dumpEnv : Context -> M String -dumpEnv ctx = - unlines . reverse <$> go (names ctx) 0 (reverse $ zip ctx.env (toList ctx.types)) [] - where - isVar : Nat -> Val -> Bool - isVar k (VVar _ k' [<]) = k == k' - isVar _ _ = False - - go : List String -> Nat -> List (Val, String, Val) -> List String -> M (List String) - go _ _ [] acc = pure acc - go names k ((v, n, ty) :: xs) acc = if isVar k v - -- TODO - use Doc and add <+/> as appropriate to printing - then go names (S k) xs (" \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc) - else go names (S k) xs (" \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc) - -export -logMetas : Nat -> M () -logMetas mstart = do - -- FIXME, now this isn't logged for Sig / Data. - top <- get - mc <- readIORef top.metaCtx - let mlen = length mc.metas `minus` mstart - for_ (reverse $ take mlen mc.metas) $ \case - (Solved fc k soln) => do - -- TODO put a flag on this, vscode is getting overwhelmed and - -- dropping errors - --info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}" - pure () - (Unsolved fc k ctx ty User cons) => do - ty' <- quote ctx.lvl ty - let names = (toList $ map fst ctx.types) - env <- dumpEnv ctx - let msg = "\{env} -----------\n \{pprint names ty'}" - info fc "User Hole\n\{msg}" - - (Unsolved fc k ctx ty kind cons) => do - tm <- quote ctx.lvl !(forceMeta ty) - -- Now that we're collecting errors, maybe we simply check at the end - -- TODO - log constraints? - -- FIXME in Combinatory, the val doesn't match environment? - let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints" - msgs <- for cons $ \ (MkMc fc env sp val) => do - pure " * (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}" - sols <- case kind of - AutoSolve => do - x <- quote ctx.lvl ty - ty <- eval ctx.env CBN x - debug "AUTO ---> \{show ty}" - -- we want the context here too. - top <- get - -- matches <- case !(contextMatches ctx ty) of - -- [] => findMatches ctx ty $ toList top.defs - -- xs => pure xs - matches <- findMatches ctx ty $ toList top.defs - -- TODO try putting mc into TopContext for to see if it gives better terms - pure $ [" \{show $ length matches} Solutions: \{show matches}"] - -- pure $ " \{show $ length matches} Solutions:" :: map ((" " ++) . interpolate . pprint (names ctx) . fst) matches - - _ => pure [] - info fc $ unlines ([msg] ++ msgs ++ sols) - -- addError $ E fc $ unlines ([msg] ++ msgs ++ sols) - - --- Used for Class and Record -getSigs : List Decl -> List (FC, String, Raw) -getSigs [] = [] -getSigs ((TypeSig _ [] _) :: xs) = getSigs xs -getSigs ((TypeSig fc (nm :: nms) ty) :: xs) = (fc, nm, ty) :: getSigs xs -getSigs (_ :: xs) = getSigs xs - -teleToPi : Telescope -> Raw -> Raw -teleToPi [] end = end -teleToPi ((info, ty) :: tele) end = RPi (getFC info) info ty (teleToPi tele end) - -impTele : Telescope -> Telescope -impTele tele = map (\(BI fc nm _ quant, ty) => (BI fc nm Implicit Zero, ty)) tele - - -export -processDecl : List String -> Decl -> M () - --- REVIEW I supposed I could have updated top here instead of the dance with the parser... -processDecl ns (PMixFix{}) = pure () - -processDecl ns (TypeSig fc names tm) = do - putStrLn "-----" - - top <- get - mc <- readIORef top.metaCtx - let mstart = length mc.metas - for_ names $ \nm => do - 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 (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 ns (PType fc nm ty) = do - top <- get - ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) - setDef (QN ns nm) fc ty' PrimTCon - -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 lookupRaw name top of - Nothing => error fc "\{name} not in scope" - _ => pure () - setDef (QN ns nm) fc ty' (PrimFn src uses) - -processDecl ns (Def fc nm clauses) = do - putStrLn "-----" - putStrLn "Def \{show nm}" - top <- get - mc <- readIORef top.metaCtx - let mstart = length mc.metas - 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}" - - putStrLn "check \{nm} at \{pprint [] ty}" - vty <- eval empty CBN ty - - debug "\{nm} vty is \{show vty}" - - - -- I can take LHS apart syntactically or elaborate it with an infer - clauses' <- traverse (makeClause top) clauses - tm <- buildTree (mkCtx fc) (MkProb clauses' vty) - -- putStrLn "Ok \{pprint [] tm}" - - mc <- readIORef top.metaCtx - let mlen = length mc.metas `minus` mstart - solveAutos mstart - -- TODO - make nf that expands all metas and drop zonk - -- Day1.newt is a test case - -- tm' <- nf [] tm - tm' <- zonk top 0 [] tm - when top.verbose $ putStrLn "NF\n\{render 80 $ pprint[] tm'}" - -- TODO we want to keep both versions, but this is checking in addition to erasing - -- currently CompileExp is also doing erasure. - -- TODO we need erasure info on the lambdas or to fake up an appropriate environment - -- and erase inside. Currently the checking is imprecise - tm'' <- erase [] tm' [] - when top.verbose $ putStrLn "ERASED\n\{render 80 $ pprint[] tm'}" - debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" - updateDef (QN ns nm) fc ty (Fn tm') - -- logMetas mstart - -processDecl ns (DCheck fc tm ty) = do - putStrLn "----- DCheck" - top <- get - - putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}" - ty' <- check (mkCtx fc) ty (VU fc) - putStrLn " got type \{pprint [] ty'}" - vty <- eval [] CBN ty' - res <- check (mkCtx fc) tm vty - putStrLn " got \{pprint [] res}" - norm <- nf [] res - putStrLn " NF \{pprint [] norm}" - norm <- nfv [] res - putStrLn " NFV \{pprint [] norm}" - -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 - putStrLn "-----" - putStrLn "Class \{nm}" - let fields = getSigs decls - -- We'll need names for the telescope - let dcName = "Mk\{nm}" - let tcType = teleToPi tele (RU classFC) - let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar classFC nm) tele - let dcType = teleToPi (impTele tele) $ - foldr (\(fc, nm, ty), acc => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields - - putStrLn "tcon type \{pretty tcType}" - putStrLn "dcon type \{pretty dcType}" - let decl = Data classFC nm tcType [TypeSig classFC [dcName] dcType] - putStrLn "Decl:" - putStrLn $ render 90 $ pretty 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 - let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele - let lhs = RApp classFC lhs autoPat Auto - let decl = Def fc name [(lhs, (RVar fc name))] - - putStrLn "\{name} : \{pretty funType}" - putStrLn "\{pretty decl}" - processDecl ns $ TypeSig fc [name] funType - processDecl ns decl - - -processDecl ns (Instance instfc ty decls) = do - - putStrLn "-----" - putStrLn "Instance \{pretty ty}" - top <- get - let tyFC = getFC ty - - vty <- check (mkCtx instfc) ty (VU instfc) - -- Here `tele` holds arguments to the instance - let (codomain, tele) = splitTele vty - -- env represents the environment of those arguments - let env = tenv (length tele) - debug "codomain \{pprint [] codomain}" - debug "tele is \{show tele}" - - -- ok so we need a name, a hack for now. - -- Maybe we need to ask the user (e.g. `instance someName : Monad Foo where`) - -- or use "Monad\{show $ length defs}" - let instname = interpolate $ pprint [] codomain - let sigDecl = TypeSig instfc [instname] ty - -- 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 - case lookupRaw instname top of - Just _ => pure MkUnit -- TODO check that the types match - Nothing => processDecl ns sigDecl - - let (Just decls) = collectDecl <$> decls - | _ => do - debug "Forward declaration \{show sigDecl}" - - let (Ref _ tconName _, args) := funArgs codomain - | (tm, _) => error tyFC "\{pprint [] codomain} doesn't appear to be a TCon application" - let (Just (MkEntry _ name type (TCon cons))) = lookup tconName top - | _ => error tyFC "\{tconName} is not a type constructor" - let [con] = cons - | _ => error tyFC "\{tconName} has multiple constructors \{show cons}" - let (Just (MkEntry _ _ dcty (DCon _ _))) = lookup con top - | _ => error tyFC "can't find constructor \{show con}" - vdcty@(VPi _ nm icit rig a b) <- eval [] CBN dcty - | x => error (getFC x) "dcty not Pi" - debug "dcty \{pprint [] dcty}" - let (_,args) = funArgs codomain - - debug "traverse \{show $ map showTm args}" - -- This is a little painful because we're reverse engineering the - -- individual types back out from the composite type - args' <- traverse (eval env CBN) args - debug "args' is \{show args'}" - conTele <- getFields !(apply vdcty args') env [] - -- declare individual functions, collect their defs - defs <- for conTele $ \case - (MkBinder fc nm Explicit rig ty) => do - let ty' = foldr (\(MkBinder fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele - let nm' = "\{instname},\{nm}" - -- we're working with a Tm, so we define directly instead of processDecl - let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls - | _ => error instfc "no definition for \{nm}" - - setDef (QN ns nm') fc ty' Axiom - let decl = (Def fc nm' xs) - putStrLn "***" - putStrLn "«\{nm'}» : \{pprint [] ty'}" - putStrLn $ render 80 $ pretty decl - pure $ Just decl - _ => pure Nothing - - for_ (mapMaybe id defs) $ \decl => do - -- debug because already printed above, but nice to have it near processing - debug $ render 80 $ pretty decl - 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 ns decl - where - -- try to extract types of individual fields from the typeclass dcon - -- We're assuming they don't depend on each other. - getFields : Val -> Env -> List Binder -> M (List Binder) - getFields tm@(VPi fc nm Explicit rig ty sc) env bnds = do - bnd <- MkBinder fc nm Explicit rig <$> quote (length env) ty - getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds) - getFields tm@(VPi fc nm _ rig ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds - getFields tm xs bnds = pure $ reverse bnds - - tenv : Nat -> Env - tenv Z = [] - tenv (S k) = (VVar emptyFC k [<] :: tenv k) - - mkRHS : String -> List Binder -> Raw -> Raw - mkRHS instName (MkBinder fc nm Explicit rig ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit) - mkRHS instName (b :: bs) tm = mkRHS instName bs tm - mkRHS instName [] tm = tm - - apply : Val -> List Val -> M Val - apply x [] = pure x - 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 ns (ShortData fc lhs sigs) = do - (nm,args) <- getArgs lhs [] - let ty = foldr (\ (fc,n), a => (RPi fc (BI fc n Explicit Zero) (RU fc) a)) (RU fc) args - cons <- traverse (mkDecl args []) sigs - let dataDecl = Data fc nm ty cons - putStrLn "SHORTDATA" - putStrLn "\{pretty dataDecl}" - processDecl ns dataDecl - where - getArgs : Raw -> List (FC, String) -> M (String, List (FC, String)) - getArgs (RVar fc1 nm) acc = pure (nm, acc) - getArgs (RApp _ t (RVar fc' nm) _) acc = getArgs t ((fc', nm) :: acc) - getArgs tm _ = error (getFC tm) "Expected contructor application, got: \{show tm}" - - mkDecl : List (FC, Name) -> List Raw -> Raw -> M Decl - mkDecl args acc (RVar fc' name) = do - let base = foldr (\ ty, acc => RPi (getFC ty) (BI (getFC ty) "_" Explicit Many) ty acc) lhs acc - let ty = foldr (\ (fc,nm), acc => RPi fc (BI fc nm Implicit Zero) (RU fc) acc) base args - pure $ TypeSig fc' [name] ty - mkDecl args acc (RApp fc' t u icit) = mkDecl args (u :: acc) t - mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}" - -processDecl ns (Data fc nm ty cons) = do - putStrLn "-----" - putStrLn "Data \{nm}" - top <- get - mc <- readIORef top.metaCtx - tyty <- check (mkCtx fc) ty (VU fc) - 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 (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}" - dty <- check (mkCtx fc) tm (VU fc) - debug "dty \{show names} is \{pprint [] dty}" - - -- We only check that codomain uses the right type constructor - -- We know it's in U because it's part of a checked Pi type - let (codomain, tele) = splitTele dty - -- for printing - let tnames = reverse $ map (\(MkBinder _ nm _ _ _) => nm) tele - let (Ref _ hn _, args) := funArgs codomain - | (tm, _) => error (getFC tm) "expected \{nm} got \{pprint tnames tm}" - when (hn /= QN ns nm) $ - error (getFC codomain) "Constructor codomain is \{pprint tnames codomain} rather than \{nm}" - - for_ names $ \ nm' => do - 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 (QN ns nm) fc tyty (TCon (join cnames)) - -- logMetas mstart - where - checkDeclType : Tm -> M () - checkDeclType (UU _) = pure () - checkDeclType (Pi _ str icit rig t u) = checkDeclType u - checkDeclType _ = error fc "data type doesn't return U" - -processDecl ns (Record recordFC nm tele cname decls) = do - putStrLn "-----" - putStrLn "Record" - let fields = getSigs decls - let dcName = fromMaybe "Mk\{nm}" cname - let tcType = teleToPi tele (RU recordFC) - -- REVIEW - I probably want to stick the telescope in front of the fields - let tail = foldl (\ acc, (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele - let dcType = teleToPi (impTele tele) $ - foldr (\(fc, nm, ty), acc => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields - - putStrLn "tcon type \{pretty tcType}" - putStrLn "dcon type \{pretty dcType}" - let decl = Data recordFC nm tcType [TypeSig recordFC [dcName] dcType] - putStrLn "Decl:" - putStrLn $ render 90 $ pretty 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`. - let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Explicit Many) tail ty - let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields - - -- `fieldName` - consider dropping to keep namespace clean - -- let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele - -- let lhs = RApp recordFC lhs autoPat Explicit - -- let decl = Def fc name [(lhs, (RVar fc name))] - -- putStrLn "\{name} : \{pretty funType}" - -- putStrLn "\{pretty decl}" - -- processDecl ns $ TypeSig fc [name] funType - -- processDecl ns decl - - -- `.fieldName` - let pname = "." ++ name - let lhs = foldl (\acc, (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele - let lhs = RApp recordFC lhs autoPat Explicit - let pdecl = Def fc pname [(lhs, (RVar fc name))] - putStrLn "\{pname} : \{pretty funType}" - putStrLn "\{pretty pdecl}" - processDecl ns $ TypeSig fc [pname] funType - processDecl ns pdecl diff --git a/orig/Lib/Syntax.idr b/orig/Lib/Syntax.idr deleted file mode 100644 index bc2acbd..0000000 --- a/orig/Lib/Syntax.idr +++ /dev/null @@ -1,316 +0,0 @@ -module Lib.Syntax - -import Data.String -import Data.Maybe -import Lib.Prettier -import Lib.Types - -public export -data Raw : Type - -public export -data Pattern - = PatVar FC Icit 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 - -export -getIcit : Pattern -> Icit -getIcit (PatVar x icit str) = icit -getIcit (PatCon x icit str xs as) = icit -getIcit (PatWild x icit) = icit -getIcit (PatLit fc lit) = Explicit - - -export -HasFC Pattern where - getFC (PatVar fc _ _) = fc - getFC (PatCon fc _ _ _ _) = fc - getFC (PatWild fc _) = fc - getFC (PatLit fc lit) = fc - --- %runElab deriveShow `{Pattern} -public export -Constraint : Type -Constraint = (String, Pattern) - -public export -record Clause where - constructor MkClause - clauseFC : FC - -- I'm including the type of the left, so we can check pats and get the list of possibilities - -- But maybe rethink what happens on the left. - -- It's a VVar k or possibly a pattern. - -- a pattern either is zipped out, dropped (non-match) or is assigned to rhs - -- if we can do all three then we can have a VVar here. - cons : List Constraint - pats : List Pattern - -- We'll need some context to typecheck this - -- it has names from Pats, which will need types in the env - expr : Raw - --- could be a pair, but I suspect stuff will be added? -public export -data RCaseAlt = MkAlt Raw Raw - -public export -data DoStmt : Type where - DoExpr : (fc : FC) -> Raw -> DoStmt - DoLet : (fc : FC) -> String -> Raw -> DoStmt - DoArrow : (fc : FC) -> Raw -> Raw -> List RCaseAlt -> DoStmt - -data Decl : Type -data Raw : Type where - RVar : (fc : FC) -> (nm : Name) -> Raw - RLam : (fc : FC) -> BindInfo -> (ty : Raw) -> Raw - RApp : (fc : FC) -> (t : Raw) -> (u : Raw) -> (icit : Icit) -> Raw - RU : (fc : FC) -> Raw - RPi : (fc : FC) -> BindInfo -> (ty : Raw) -> (sc : Raw) -> Raw - RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw - RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw - RLit : (fc : FC) -> Literal -> Raw - RCase : (fc : FC) -> (scrut : Raw) -> (alts : List RCaseAlt) -> Raw - RImplicit : (fc : FC) -> Raw - RHole : (fc : FC) -> Raw - RDo : (fc : FC) -> List DoStmt -> Raw - RIf : (fc : FC) -> Raw -> Raw -> Raw -> Raw - RWhere : (fc : FC) -> (List Decl) -> Raw -> Raw - RAs : (fc : FC) -> Name -> Raw -> Raw - -%name Raw tm - - -export -HasFC Raw where - getFC (RVar fc nm) = fc - getFC (RLam fc _ ty) = fc - getFC (RApp fc t u icit) = fc - getFC (RU fc) = fc - getFC (RPi fc _ ty sc) = fc - getFC (RLet fc nm ty v sc) = fc - getFC (RAnn fc tm ty) = fc - getFC (RLit fc y) = fc - getFC (RCase fc scrut alts) = fc - getFC (RImplicit fc) = fc - getFC (RHole fc) = fc - getFC (RDo fc stmts) = fc - getFC (RIf fc _ _ _) = fc - getFC (RWhere fc _ _) = fc - getFC (RAs fc _ _) = fc - - --- derive some stuff - I'd like json, eq, show, ... - - - -public export -data Import = MkImport FC Name - - -public export -Telescope : Type -Telescope = List (BindInfo, Raw) - -public export -data Decl - = TypeSig FC (List Name) Raw - | Def FC Name (List (Raw, Raw)) -- (List Clause) - | DCheck FC Raw Raw - | Data FC Name Raw (List Decl) - | ShortData FC Raw (List Raw) - | PType FC Name (Maybe Raw) - | PFunc FC Name (List String) Raw String - | PMixFix FC (List Name) Nat Fixity - | Class FC Name Telescope (List Decl) - | Instance FC Raw (Maybe (List Decl)) - | Record FC Name Telescope (Maybe Name) (List Decl) - -public export -HasFC Decl where - getFC (TypeSig x strs tm) = x - getFC (Def x str xs) = x - getFC (DCheck x tm tm1) = x - getFC (Data x str tm xs) = x - getFC (ShortData x _ _) = x - getFC (PType x str mtm) = x - getFC (PFunc x str _ tm str1) = x - getFC (PMixFix x strs k y) = x - getFC (Class x str xs ys) = x - getFC (Instance x tm xs) = x - getFC (Record x str tm str1 xs) = x - -public export -record Module where - constructor MkModule - modname : Name - imports : List Import - decls : List Decl - -foo : List String -> String -foo ts = "(" ++ unwords ts ++ ")" - --- Show Literal where --- show (LString str) = foo [ "LString", show str] --- show (LInt i) = foo [ "LInt", show i] --- show (LChar c) = foo [ "LChar", show c] - -export -covering -implementation Show Raw - -export -implementation Show Decl - -export Show Pattern - -export -covering -Show Clause where - show (MkClause fc cons pats expr) = show (fc, cons, pats, expr) - -Show Import where - show (MkImport _ str) = foo ["MkImport", show str] - -Show BindInfo where - show (BI _ nm icit quant) = foo ["BI", show nm, show icit, show quant] - --- this is for debugging, use pretty when possible -covering -Show Decl where - show (TypeSig _ str x) = foo ["TypeSig", show str, show x] - show (Def _ str clauses) = foo ["Def", show str, show clauses] - show (Data _ str xs ys) = foo ["Data", show str, show xs, show ys] - show (DCheck _ x y) = foo ["DCheck", show x, show y] - show (PType _ name ty) = foo ["PType", name, show ty] - show (ShortData _ lhs sigs) = foo ["ShortData", show lhs, show sigs] - show (PFunc _ nm uses ty src) = foo ["PFunc", nm, show uses, show ty, show src] - show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix] - show (Class _ nm tele decls) = foo ["Class", nm, "...", (show $ map show decls)] - show (Instance _ nm decls) = foo ["Instance", show nm, (show $ map show decls)] - show (Record _ nm tele nm1 decls) = foo ["Record", show nm, show tele, show nm1, show decls] - -export covering -Show Module where - show (MkModule name imports decls) = foo ["MkModule", show name, show imports, show decls] - -export -covering -Show Pattern where - show (PatVar _ icit str) = foo ["PatVar", show icit, show str] - show (PatCon _ icit str xs as) = foo ["PatCon", show icit, show str, show xs, show as] - show (PatWild _ icit) = foo ["PatWild", show icit] - show (PatLit _ lit) = foo ["PatLit", show lit] - -covering -Show RCaseAlt where - show (MkAlt x y)= foo ["MkAlt", show x, show y] - -covering -Show Raw where - show (RImplicit _) = "_" - show (RHole _) = "?" - show (RVar _ name) = foo ["RVar", show name] - show (RAnn _ t ty) = foo [ "RAnn", show t, show ty] - show (RLit _ x) = foo [ "RLit", show x] - show (RLet _ x ty v scope) = foo [ "Let", show x, " : ", show ty, " = ", show v, " in ", show scope] - show (RPi _ bi y z) = foo [ "Pi", show bi, show y, show z] - show (RApp _ x y z) = foo [ "App", show x, show y, show z] - show (RLam _ bi y) = foo [ "Lam", show bi, show y] - show (RCase _ x xs) = foo [ "Case", show x, show xs] - show (RDo _ stmts) = foo [ "DO", "FIXME"] - show (RU _) = "U" - show (RIf _ x y z) = foo [ "If", show x, show y, show z] - show (RWhere _ _ _) = foo [ "Where", "FIXME"] - show (RAs _ nm x) = foo [ "RAs", nm, show x] - -export -Pretty Literal where - pretty (LString str) = text $ interpolate str - pretty (LInt i) = text $ show i - pretty (LChar c) = text $ show c - -export -Pretty Pattern where - -- FIXME - wrap Implicit with {} - pretty (PatVar _ icit nm) = text nm - pretty (PatCon _ icit nm args Nothing) = text (show nm) <+> spread (map pretty args) - pretty (PatCon _ icit nm args (Just as)) = text as ++ text "@(" ++ text (show nm) <+> spread (map pretty args) ++ text ")" - pretty (PatWild _ icit) = text "_" - pretty (PatLit _ lit) = pretty lit - -wrap : Icit -> Doc -> Doc -wrap Explicit x = text "(" ++ x ++ text ")" -wrap Implicit x = text "{" ++ x ++ text "}" -wrap Auto x = text "{{" ++ x ++ text "}}" - -export -Pretty Raw where - pretty = asDoc 0 - where - bindDoc : BindInfo -> Doc - bindDoc (BI _ nm icit quant) = ?rhs_0 - - par : Nat -> Nat -> Doc -> Doc - par p p' d = if p' < p then text "(" ++ d ++ text ")" else d - - asDoc : Nat -> Raw -> Doc - asDoc p (RVar _ str) = text str - asDoc p (RLam _ (BI _ nm icit q) x) = par p 0 $ text "\\" ++ wrap icit (text nm) <+> text "=>" <+> asDoc 0 x - -- This needs precedence and operators... - asDoc p (RApp _ x y Explicit) = par p 2 $ asDoc 2 x <+> asDoc 3 y - asDoc p (RApp _ x y Implicit) = par p 2 $ asDoc 2 x <+> text "{" ++ asDoc 0 y ++ text "}" - asDoc p (RApp _ x y Auto) = par p 2 $ asDoc 2 x <+> text "{{" ++ asDoc 0 y ++ text "}}" - asDoc p (RU _) = text "U" - asDoc p (RPi _ (BI _ "_" Explicit Many) ty scope) = par p 1 $ asDoc p ty <+> text "->" <+/> asDoc p scope - asDoc p (RPi _ (BI _ nm icit quant) ty scope) = - par p 1 $ wrap icit (text (show quant ++ nm) <+> text ":" <+> asDoc p ty ) <+> text "->" <+/> asDoc 1 scope - asDoc p (RLet _ x v ty scope) = - par p 0 $ text "let" <+> text x <+> text ":" <+> asDoc p ty - <+> text "=" <+> asDoc p v - <+/> text "in" <+> asDoc p scope - -- does this exist? - asDoc p (RAnn _ x y) = text "TODO - RAnn" - asDoc p (RLit _ lit) = pretty lit - asDoc p (RCase _ x xs) = text "TODO - RCase" - asDoc p (RImplicit _) = text "_" - asDoc p (RHole _) = text "?" - asDoc p (RDo _ stmts) = text "TODO - RDo" - asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z - asDoc p (RWhere _ dd b) = text "TODO pretty where" - asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")" - -prettyBind : (BindInfo, Raw) -> Doc -prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty) - -pipeSep : List Doc -> Doc -pipeSep = folddoc (\a, b => a <+/> text "|" <+> b) - -export -Pretty Decl where - pretty (TypeSig _ nm ty) = spread (map text nm) <+> text ":" <+> nest 2 (pretty ty) - pretty (Def _ nm clauses) = stack $ map (\(a,b) => pretty a <+> text "=" <+> pretty b) clauses - pretty (Data _ nm x xs) = text "data" <+> text nm <+> text ":" <+> pretty x <+> (nest 2 $ text "where" stack (map pretty xs)) - pretty (DCheck _ x y) = text "#check" <+> pretty x <+> text ":" <+> pretty y - pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => text ":" <+> pretty ty) ty) - pretty (PFunc _ nm [] ty src) = text "pfunc" <+> text nm <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) - pretty (PFunc _ nm uses ty src) = text "pfunc" <+> text nm <+> text "uses" <+> spread (map text uses) <+> text ":" <+> nest 2 (pretty ty <+> text ":=" <+/> text (show src)) - pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names) - pretty (Record _ nm tele cname decls) = text "record" <+> text nm <+> text ":" <+> spread (map prettyBind tele) - <+> (nest 2 $ text "where" stack (maybe empty (\ nm' => text "constructor" <+> text 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 (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs) - -export -Pretty Module where - pretty (MkModule name imports decls) = - text "module" <+> text name - stack (map doImport imports) - stack (map pretty decls) - where - doImport : Import -> Doc - doImport (MkImport _ nm) = text "import" <+> text nm ++ line - diff --git a/orig/Lib/Token.idr b/orig/Lib/Token.idr deleted file mode 100644 index 961c38f..0000000 --- a/orig/Lib/Token.idr +++ /dev/null @@ -1,103 +0,0 @@ -module Lib.Token - -public export -record Bounds where - constructor MkBounds - startLine : Int - startCol : Int - endLine : Int - endCol : Int - -export -Eq Bounds where - (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') = - sl == sl' - && sc == sc' - && el == el' - && ec == ec' - -public export -record WithBounds ty where - constructor MkBounded - val : ty - bounds : Bounds - -public export -data Kind - = Ident - | UIdent - | Keyword - | MixFix - | Number - | Character - | StringKind - | JSLit - | Symbol - | Space - | Comment - | Pragma - | Projection - -- not doing Layout.idr - | LBrace - | Semi - | RBrace - | EOI - | StartQuote - | EndQuote - | StartInterp - | EndInterp - -export -Show Kind where - show Ident = "Ident" - show UIdent = "UIdent" - show Keyword = "Keyword" - show MixFix = "MixFix" - show Number = "Number" - show Character = "Character" - show Symbol = "Symbol" - show Space = "Space" - show LBrace = "LBrace" - show Semi = "Semi" - show RBrace = "RBrace" - show Comment = "Comment" - show EOI = "EOI" - show Pragma = "Pragma" - show StringKind = "String" - show JSLit = "JSLit" - show Projection = "Projection" - show StartQuote = "StartQuote" - show EndQuote = "EndQuote" - show StartInterp = "StartInterp" - show EndInterp = "EndInterp" - -export -Eq Kind where - a == b = show a == show b - -public export -record Token where - constructor Tok - kind : Kind - text : String - - -export -Show Token where - show (Tok k v) = "<\{show k}:\{show v}>" - -public export -BTok : Type -BTok = WithBounds Token - -export -value : BTok -> String -value (MkBounded (Tok _ s) _) = s - -export -kind : BTok -> Kind -kind (MkBounded (Tok k s) _) = k - -export -getStart : BTok -> (Int, Int) -getStart (MkBounded _ (MkBounds l c _ _)) = (l,c) diff --git a/orig/Lib/Tokenizer.idr b/orig/Lib/Tokenizer.idr deleted file mode 100644 index 1e1f737..0000000 --- a/orig/Lib/Tokenizer.idr +++ /dev/null @@ -1,161 +0,0 @@ -module Lib.Tokenizer - --- Working alternate tokenizer, saves about 2k, can be translated to newt - --- Currently this processes a stream of characters, I may switch it to --- combinators for readability in the future. - -import Lib.Token -import Lib.Common -import Data.String - -standalone : List Char -standalone = unpack "()\\{}[,.@]" - -keywords : List String -keywords = ["let", "in", "where", "case", "of", "data", "U", "do", - "ptype", "pfunc", "module", "infixl", "infixr", "infix", - "∀", "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 - "$", "λ", "?", "@", ".", - "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"] - -record TState where - constructor TS - trow : Int - tcol : Int - acc : SnocList BTok - chars : List Char - --- This makes a big case tree... -rawTokenise : TState -> Either Error TState - -quoteTokenise : TState -> Int -> Int -> SnocList Char -> Either Error TState -quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of - '"' :: cs => Right (TS el ec (toks :< stok) chars) - '\\' :: '{' :: cs => do - let tok = MkBounded (Tok StartInterp "\\{") (MkBounds el ec el (ec + 2)) - (TS el ec toks chars) <- rawTokenise $ TS el (ec + 2) (toks :< stok :< tok) cs - case chars of - '}' :: cs => - let tok = MkBounded (Tok EndInterp "}") (MkBounds el ec el (ec + 1)) - in quoteTokenise (TS el (ec + 1) (toks :< tok) cs) el (ec + 1) [<] - cs => Left $ E (MkFC "" (el, ec)) "Expected '{'" - -- TODO newline in string should be an error - '\n' :: cs => Left $ E (MkFC "" (el, ec)) "Newline in string" - '\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n') - '\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c) - c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c) - Nil => Left $ E (MkFC "" (el, ec)) "Expected '\"' at EOF" - - where - stok : BTok - stok = MkBounded (Tok StringKind (pack $ acc <>> [])) (MkBounds startl startc el ec) - - - -rawTokenise ts@(TS sl sc toks chars) = case chars of - Nil => Right $ ts - ' ' :: cs => rawTokenise (TS sl (sc + 1) toks cs) - '\n' :: cs => rawTokenise (TS (sl + 1) 0 toks cs) - - '"' :: cs => do - let tok = mktok False sl (sc + 1) StartQuote "\"" - (TS sl sc toks chars) <- quoteTokenise (TS sl (sc + 1) (toks :< tok) cs) sl (sc + 1) [<] - case chars of - '"' :: cs => let tok = mktok False sl (sc + 1) EndQuote "\"" in - rawTokenise (TS sl (sc + 1) (toks :< tok) cs) - cs => Left $ E (MkFC "" (sl, sc)) "Expected '\"'" - - '{' :: '{' :: cs => do - let tok = mktok False sl (sc + 2) Keyword "{{" - (TS sl sc toks chars) <- rawTokenise (TS sl (sc + 2) (toks :< tok) cs) - case chars of - '}' :: '}' :: cs => let tok = mktok False sl (sc + 2) Keyword "}}" in - rawTokenise (TS sl (sc + 2) (toks :< tok) cs) - cs => Left $ E (MkFC "" (sl, sc)) "Expected '}}'" - - '}' :: cs => Right ts - '{' :: cs => do - let tok = mktok False sl (sc + 1) Symbol "{" - (TS sl sc toks chars) <- rawTokenise (TS sl (sc + 1) (toks :< tok) cs) - case chars of - '}' :: cs => let tok = mktok False sl (sc + 1) Symbol "}" in - rawTokenise (TS sl (sc + 1) (toks :< tok) cs) - cs => Left $ E (MkFC "" (sl, sc)) "Expected '}'" - - ',' :: cs => rawTokenise (TS sl (sc + 1) (toks :< mktok False sl (sc + 1) Ident ",") cs) - '_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs) - '_' :: '.' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_._") cs) - '\'' :: '\\' :: c :: '\'' :: cs => - let ch = ifThenElse (c == 'n') '\n' c - in rawTokenise (TS sl (sc + 4) (toks :< mktok False sl (sc + 4) Character (singleton ch)) cs) - '\'' :: c :: '\'' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) Character (singleton c)) cs) - '#' :: cs => doRest (TS sl (sc + 1) toks cs) Pragma isIdent (Lin :< '#') - '-' :: '-' :: cs => lineComment (TS sl (sc + 2) toks cs) - '/' :: '-' :: cs => blockComment (TS sl (sc + 2) toks cs) - '`' :: cs => doBacktick (TS sl (sc + 1) toks cs) [<] - '.' :: cs => doRest (TS sl (sc + 1) toks cs) Projection isIdent (Lin :< '.') - '-' :: c :: cs => if isDigit c - then doRest (TS sl (sc + 2) toks cs) Number isDigit (Lin :< '-' :< c) - else doRest (TS sl (sc + 1) toks (c :: cs)) Ident isIdent (Lin :< '-') - - c :: cs => doChar c cs - - where - isIdent : Char -> Bool - isIdent c = not (isSpace c || elem c standalone) - - isUIdent : Char -> Bool - isUIdent c = isIdent c || c == '.' - - doBacktick : TState -> SnocList Char -> Either Error TState - doBacktick (TS l c toks Nil) acc = Left $ E (MkFC "" (l,c)) "EOF in backtick string" - doBacktick (TS el ec toks ('`' :: cs)) acc = - let tok = MkBounded (Tok JSLit (pack $ acc <>> [])) (MkBounds sl sc el ec) in - rawTokenise (TS el (ec + 1) (toks :< tok) cs) - doBacktick (TS l c toks ('\n' :: cs)) acc = doBacktick (TS (l + 1) 0 toks cs) (acc :< '\n') - doBacktick (TS l c toks (ch :: cs)) acc = doBacktick (TS l (c + 1) toks cs) (acc :< ch) - - - -- temporary use same token as before - mktok : Bool -> Int -> Int -> Kind -> String -> BTok - mktok checkkw el ec kind text = let kind = if checkkw && elem text keywords then Keyword else kind in - MkBounded (Tok kind text) (MkBounds sl sc el ec) - - lineComment : TState -> Either Error TState - lineComment (TS line col toks Nil) = rawTokenise (TS line col toks Nil) - lineComment (TS line col toks ('\n' :: cs)) = rawTokenise (TS (line + 1) 0 toks cs) - lineComment (TS line col toks (c :: cs)) = lineComment (TS line (col + 1) toks cs) - - blockComment : TState -> Either Error TState - blockComment (TS line col toks Nil) = Left $ E (MkFC "" (line, col)) "EOF in block comment" - blockComment (TS line col toks ('-' :: '/' :: cs)) = rawTokenise (TS line (col + 2) toks cs) - blockComment (TS line col toks ('\n' :: cs)) = blockComment (TS (line + 1) 0 toks cs) - blockComment (TS line col toks (c :: cs)) = blockComment (TS line (col + 1) toks cs) - - doRest : TState -> Kind -> (Char -> Bool) -> SnocList Char -> Either Error TState - doRest (TS l c toks Nil) kind pred acc = rawTokenise (TS l c (toks :< mktok True l c kind (pack $ acc <>> [])) Nil) - doRest (TS l c toks (ch :: cs)) kind pred acc = if pred ch - then doRest (TS l (c + 1) toks cs) kind pred (acc :< ch) - else - let kind = if elem '_' acc then MixFix else kind in - rawTokenise (TS l c (toks :< mktok True l (c - 1) kind (pack $ acc <>> [])) (ch :: cs)) - - doChar : Char -> List Char -> Either Error TState - doChar c cs = if elem c standalone - then rawTokenise (TS sl (sc + 1) (toks :< mktok True sl (sc + 1) Symbol (singleton c)) cs) - else let kind = if isDigit c then Number else if isUpper c then UIdent else Ident in - doRest (TS sl sc toks (c :: cs)) kind isIdent [<] - -export -tokenise : String -> String -> Either Error (List BTok) -tokenise fn text = case rawTokenise (TS 0 0 Lin (unpack text)) of - Right (TS trow tcol acc []) => Right $ acc <>> [] - Right (TS trow tcol acc chars) => Left $ E (MkFC fn (trow, tcol)) "Extra toks" - Left (E (MkFC file start) str) => Left $ E (MkFC fn start) str - Left err => Left err - diff --git a/orig/Lib/TopContext.idr b/orig/Lib/TopContext.idr deleted file mode 100644 index 3bdb23a..0000000 --- a/orig/Lib/TopContext.idr +++ /dev/null @@ -1,54 +0,0 @@ -module Lib.TopContext - -import Data.IORef -import Data.SortedMap -import Data.String -import Lib.Types - --- 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 : 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 (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 . snd) $ toList defs}]" - -public export -empty : HasIO m => m TopContext -empty = pure $ MkTop empty !(newIORef (MC [] 0 CheckAll)) False !(newIORef []) [] empty - -public export -setDef : QName -> FC -> Tm -> Def -> M () -setDef name fc ty def = do - top <- get - 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 : QName -> FC -> Tm -> Def -> M () -updateDef name fc ty def = do - top <- get - 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 () -addError err = do - top <- get - modifyIORef top.errors (err ::) diff --git a/orig/Lib/Types.idr b/orig/Lib/Types.idr deleted file mode 100644 index ac877c7..0000000 --- a/orig/Lib/Types.idr +++ /dev/null @@ -1,599 +0,0 @@ -module Lib.Types - --- For FC, Error -import public Lib.Common -import public Lib.Prettier - -import Data.Fin -import Data.IORef -import Data.List -import Data.SnocList -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 - -public export -data Icit = Implicit | Explicit | Auto - -%name Icit icit - -export -Show Icit where - show Implicit = "Implicit" - show Explicit = "Explicit" - show Auto = "Auto" - -public export -data BD = Bound | Defined - -public export -Eq BD where - Bound == Bound = True - Defined == Defined = True - _ == _ = False - -public export -Show BD where - show Bound = "bnd" - show Defined = "def" - -public export -data Quant = Zero | Many - -public export -Show Quant where - show Zero = "0 " - show Many = "" - -Eq Quant where - Zero == Zero = True - Many == Many = True - _ == _ = False - --- We could make this polymorphic and use for environment... -public export -data BindInfo : Type where - BI : (fc : FC) -> (name : Name) -> (icit : Icit) -> (quant : Quant) -> BindInfo - -%name BindInfo bi - -public export -HasFC BindInfo where - getFC (BI fc _ _ _) = fc - -public export -data Tm : Type - -public export -data Literal = LString String | LInt Int | LChar Char - -%name Literal lit - -public export -Show Literal where - show (LString str) = show str - show (LInt i) = show i - show (LChar c) = show c - -public export -data CaseAlt : Type where - CaseDefault : Tm -> CaseAlt - CaseCons : (name : QName) -> (args : List String) -> Tm -> CaseAlt - CaseLit : Literal -> Tm -> CaseAlt - -data Def : Type - - -public export -Eq Literal where - LString x == LString y = x == y - LInt x == LInt y = x == y - LChar x == LChar y = x == y - _ == _ = False - -data Tm : Type where - Bnd : FC -> Nat -> Tm - -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. - Ref : FC -> QName -> Def -> Tm - Meta : FC -> Nat -> Tm - -- kovacs optimization, I think we can App out meta instead - -- InsMeta : Nat -> List BD -> Tm - Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm - App : FC -> Tm -> Tm -> Tm - UU : FC -> Tm - Pi : FC -> Name -> Icit -> Quant -> Tm -> Tm -> Tm - Case : FC -> Tm -> List CaseAlt -> Tm - -- need type? - Let : FC -> Name -> Tm -> Tm -> Tm - -- for desugaring where - LetRec : FC -> Name -> Tm -> Tm -> Tm -> Tm - Lit : FC -> Literal -> Tm - Erased : FC -> Tm - -%name Tm t, u, v - -export -HasFC Tm where - getFC (Bnd fc k) = fc - getFC (Ref fc str x) = fc - getFC (Meta fc k) = fc - getFC (Lam fc str _ _ t) = fc - getFC (App fc t u) = fc - getFC (UU fc) = fc - getFC (Pi fc str icit quant t u) = fc - getFC (Case fc t xs) = fc - getFC (Lit fc _) = fc - getFC (Let fc _ _ _) = fc - getFC (LetRec fc _ _ _ _) = fc - getFC (Erased fc) = fc - -covering -Show Tm - -public export -covering -Show CaseAlt where - show (CaseDefault tm) = "_ => \{show tm}" - show (CaseCons nm args tm) = "\{show nm} \{unwords args} => \{show tm}" - show (CaseLit lit tm) = "\{show lit} => \{show tm}" - -public export -covering -Show Tm where - show (Bnd _ k) = "(Bnd \{show k})" - show (Ref _ str _) = "(Ref \{show str})" - show (Lam _ nm icit rig t) = "(\\ \{show rig}\{nm} => \{show t})" - show (App _ t u) = "(\{show t} \{show u})" - show (Meta _ i) = "(Meta \{show i})" - show (Lit _ l) = "(Lit \{show l})" - show (UU _) = "U" - show (Pi _ str Explicit rig t u) = "(Pi (\{show rig}\{str} : \{show t}) => \{show u})" - show (Pi _ str Implicit rig t u) = "(Pi {\{show rig}\{str} : \{show t}} => \{show u})" - show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})" - show (Case _ sc alts) = "(Case \{show sc} \{show alts})" - show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})" - show (LetRec _ nm ty t u) = "(LetRec \{nm} : \{show ty} \{show t} \{show u})" - show (Erased _) = "ERASED" - -public export -showTm : Tm -> String -showTm = show - --- I can't really show val because it's HOAS... - --- TODO derive -export -Eq Icit where - Implicit == Implicit = True - Explicit == Explicit = True - Auto == Auto = True - _ == _ = False - -||| Eq on Tm. We've got deBruijn indices, so I'm not comparing names -export -Eq (Tm) where - -- (Local x) == (Local y) = x == y - (Bnd _ x) == (Bnd _ y) = x == y - (Ref _ x _) == Ref _ y _ = x == y - (Lam _ n _ _ t) == Lam _ n' _ _ t' = t == t' - (App _ t u) == App _ t' u' = t == t' && u == u' - (UU _) == (UU _) = True - (Pi _ n icit rig t u) == (Pi _ n' icit' rig' t' u') = icit == icit' && rig == rig' && t == t' && u == u' - _ == _ = False - - - --- TODO App and Lam should have <+/> but we need to fix --- INFO pprint to `nest 2 ...` --- maybe return Doc and have an Interpolation.. --- If we need to flatten, case is going to get in the way. - -pprint' : Nat -> List String -> Tm -> Doc -pprintAlt : Nat -> List String -> CaseAlt -> Doc -pprintAlt p names (CaseDefault t) = text "_" <+> text "=>" <+> pprint' p ("_" :: names) t -pprintAlt p names (CaseCons name args t) = text (show name) <+> spread (map text args) <+> (nest 2 $ text "=>" <+/> pprint' p (reverse args ++ names) t) --- `;` is not in surface syntax, but sometimes we print on one line -pprintAlt p names (CaseLit lit t) = text (show lit) <+> (nest 2 $ text "=>" <+/> pprint' p names t ++ text ";") - -parens : Nat -> Nat -> Doc -> Doc -parens a b doc = if a < b - then text "(" ++ doc ++ text ")" - else doc - -pprint' p names (Bnd _ k) = case getAt k names of - -- Either a bug or we're printing without names - Nothing => text "BND:\{show k}" - Just nm => text "\{nm}:\{show k}" -pprint' p names (Ref _ str mt) = text (show str) -pprint' p names (Meta _ k) = text "?m:\{show k}" -pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t -pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u -pprint' p names (UU _) = text "U" -pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $ - text "{{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}}" <+> text "->" <+> pprint' 0 (nm :: names) u -pprint' p names (Pi _ nm Implicit rig t u) = parens 0 p $ - text "{" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t <+> text "}" <+> text "->" <+> pprint' 0 (nm :: names) u -pprint' p names (Pi _ "_" Explicit Many t u) = - parens 0 p $ pprint' 1 names t <+> text "->" <+> pprint' 0 ("_" :: names) u -pprint' p names (Pi _ nm Explicit rig t u) = parens 0 p $ - text "(" ++ text (show rig) <+> text nm <+> text ":" <+> pprint' 0 names t ++ text ")" <+> text "->" <+> pprint' 0 (nm :: names) u --- FIXME - probably way wrong on the names here. There is implicit binding going on -pprint' p names (Case _ sc alts) = parens 0 p $ text "case" <+> pprint' 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (pprintAlt 0 names) alts))) -pprint' p names (Lit _ lit) = text (show lit) -pprint' p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) -pprint' p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> text ":" <+> pprint' 0 names ty <+> text ":=" <+> pprint' 0 names t <+> text "in" (nest 2 $ pprint' 0 (nm :: names) u) -pprint' p names (Erased _) = text "ERASED" - -||| Pretty printer for Tm. -export -pprint : List String -> Tm -> Doc -pprint names tm = pprint' 0 names tm - -data Val : Type - --- IS/TypeTheory.idr is calling this a Kripke function space --- Yaffle, IS/TypeTheory use a function here. --- Kovacs, Idris use Env and Tm - --- in cctt kovacs refers to this choice as defunctionalization vs HOAS --- https://github.com/AndrasKovacs/cctt/blob/main/README.md#defunctionalization --- the tradeoff is access to internals of the function - --- Yaffle is vars -> vars here - -public export -data Closure : Type - -public export -data Val : Type where - -- This will be local / flex with spine. - VVar : FC -> (k : Nat) -> (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 - VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val - VLam : FC -> Name -> Icit -> Quant -> Closure -> Val - VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val - VLet : FC -> Name -> Val -> Val -> Val - VLetRec : FC -> Name -> Val -> Val -> Val -> Val - VU : FC -> Val - VErased : FC -> Val - VLit : FC -> Literal -> Val - -public export -Env : Type -Env = List Val - -public export -data Mode = CBN | CBV - -public export -data Closure = MkClosure Env Tm - -public export -getValFC : Val -> FC -getValFC (VVar fc _ _) = fc -getValFC (VRef fc _ _ _) = fc -getValFC (VCase fc _ _) = fc -getValFC (VMeta fc _ _) = fc -getValFC (VLam fc _ _ _ _) = fc -getValFC (VPi fc _ _ _ a b) = fc -getValFC (VU fc) = fc -getValFC (VErased fc) = fc -getValFC (VLit fc _) = fc -getValFC (VLet fc _ _ _) = fc -getValFC (VLetRec fc _ _ _ _) = fc - - -public export -HasFC Val where getFC = getValFC - -Show Closure - -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 _ [<]) = 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})" - show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show x}). \{show y})" - show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show x}}}. \{show y})" - show (VCase fc sc alts) = "(%case \{show sc} ...)" - show (VU _) = "U" - show (VLit _ lit) = show lit - show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}" - show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}" - show (VErased _) = "ERASED" - -covering -Show Closure where - show (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})" - -record Context - -public export -data MetaKind = Normal | User | AutoSolve - -public export -Show MetaKind where - show Normal = "Normal" - show User = "User" - show AutoSolve = "Auto" - -public export -Eq MetaKind where - a == b = show a == show b - - --- constrain meta applied to val to be a val -public export -data MConstraint = MkMc FC Env (SnocList Val) Val - -public export -data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved FC Nat Val - -public export -data MetaMode = CheckAll | CheckFirst | NoCheck - -public export -record MetaContext where - constructor MC - metas : List MetaEntry - next : Nat - mcmode : MetaMode - -public export -data Def = Axiom | TCon (List QName) | DCon Nat QName | Fn Tm | PrimTCon - | PrimFn String (List String) - -public export -covering -Show Def where - show Axiom = "axiom" - show (TCon strs) = "TCon \{show strs}" - show (DCon k tyname) = "DCon \{show k} \{show tyname}" - show (Fn t) = "Fn \{show t}" - show (PrimTCon) = "PrimTCon" - show (PrimFn src used) = "PrimFn \{show src} \{show used}" - -||| entry in the top level context -public export -record TopEntry where - constructor MkEntry - fc : FC - name : QName - type : Tm - def : Def - --- FIXME snoc - -export -covering -Show TopEntry where - show (MkEntry fc name type def) = "\{name} : \{show type} := \{show def}" - -||| Top level context. -||| Most of the reason this is separate is to have a different type -||| `Def` for the entries. -||| -||| The price is that we have names in addition to levels. Do we want to -||| expand these during normalization? -public export -record TopContext where - constructor MkTop - -- We'll add a map later? - defs : SortedMap QName TopEntry - metaCtx : IORef MetaContext - verbose : Bool -- command line flag - errors : IORef (List Error) - ||| loaded modules - loaded : List String - ops : Operators - --- we'll use this for typechecking, but need to keep a TopContext around too. -public export -record Context where - [noHints] - constructor MkCtx - lvl : Nat - -- shall we use lvl as an index? - env : Env -- Values in scope - types : Vect lvl (String, Val) -- types and names in scope - -- so we'll try "bds" determines length of local context - bds : Vect lvl BD -- bound or defined - - -- FC to use if we don't have a better option - ctxFC : FC - -%name Context ctx - -||| add a binding to environment -export -extend : Context -> String -> Val -> Context -extend ctx name ty = - { lvl $= S, env $= (VVar emptyFC ctx.lvl [<] ::), types $= ((name, ty) ::), bds $= (Bound ::) } ctx - --- I guess we define things as values? -export -define : Context -> String -> Val -> Val -> Context -define ctx name val ty = - { lvl $= S, env $= (val ::), types $= ((name,ty) ::), bds $= (Defined ::) } ctx - - -export -covering -Show MetaEntry where - show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}" - show (Solved _ k x) = "Solved \{show k} \{show x}" - -export -withPos : Context -> FC -> Context -withPos ctx fc = { ctxFC := fc } ctx - -export -names : Context -> List String -names ctx = toList $ map fst ctx.types - --- public export --- M : Type -> Type --- M = (StateT TopContext (EitherT Error IO)) - -public export -record M a where - constructor MkM - runM : TopContext -> IO (Either Error (TopContext, a)) - -export -Functor M where - map f (MkM run) = MkM $ \tc => do - result <- run tc - case result of - Left err => pure $ Left err - Right (tc', a) => pure $ Right (tc', f a) - -export -Applicative M where - pure x = MkM $ \tc => pure $ Right (tc, x) - (MkM f) <*> (MkM x) = MkM $ \tc => do - resultF <- f tc - case resultF of - Left err => pure $ Left err - Right (tc', f') => do - resultX <- x tc' - case resultX of - Left err => pure $ Left err - Right (tc'', x') => pure $ Right (tc'', f' x') - -export -Monad M where - (MkM x) >>= f = MkM $ \tc => do - resultX <- x tc - case resultX of - Left err => pure $ Left err - Right (tc', a) => runM (f a) tc' - -export -HasIO M where - liftIO io = MkM $ \tc => do - result <- io - pure $ Right (tc, result) - -export -throwError : Error -> M a -throwError err = MkM $ \_ => pure $ Left err - -export -catchError : M a -> (Error -> M a) -> M a -catchError (MkM ma) handler = MkM $ \tc => do - result <- ma tc - case result of - Left err => runM (handler err) tc - Right (tc', a) => pure $ Right (tc', a) - -export -tryError : M a -> M (Either Error a) -tryError ma = catchError (map Right ma) (pure . Left) - -export -get : M TopContext -get = MkM $ \ tc => pure $ Right (tc, tc) - -export -put : TopContext -> M Unit -put tc = MkM $ \_ => pure $ Right (tc, MkUnit) - -export -modify : (TopContext -> TopContext) -> M Unit -modify f = do - tc <- get - put (f tc) - -||| Force argument and print if verbose is true -export -debug : Lazy String -> M Unit -debug x = do - top <- get - when top.verbose $ putStrLn $ Force x - -export -info : FC -> String -> M Unit -info fc msg = putStrLn "INFO at \{show fc}: \{msg}" - -||| Version of debug that makes monadic computation lazy -export -debugM : M String -> M Unit -debugM x = do - top <- get - when top.verbose $ do putStrLn !(x) - -export -Show Context where - show ctx = "Context \{show $ map fst $ ctx.types}" - -export -errorMsg : Error -> String -errorMsg (E x str) = str -errorMsg (Postpone x k str) = str - -export -HasFC Error where - getFC (E x str) = x - getFC (Postpone x k str) = x - -export -error : FC -> String -> M a -error fc msg = throwError $ E fc msg - -export -error' : String -> M a -error' msg = throwError $ E emptyFC msg - - -export -lookupMeta : Nat -> M MetaEntry -lookupMeta ix = do - top <- get - mc <- readIORef top.metaCtx - go mc.metas - where - go : List MetaEntry -> M MetaEntry - go [] = error' "Meta \{show ix} not found" - go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs - go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs - --- we need more of topcontext later - Maybe switch it up so we're not passing --- around top -export -mkCtx : FC -> Context -mkCtx fc = MkCtx 0 [] [] [] fc diff --git a/orig/Lib/Util.idr b/orig/Lib/Util.idr deleted file mode 100644 index e246b8b..0000000 --- a/orig/Lib/Util.idr +++ /dev/null @@ -1,28 +0,0 @@ -module Lib.Util - -import Lib.Types - -export -funArgs : Tm -> (Tm, List Tm) -funArgs tm = go tm [] - where - go : Tm -> List Tm -> (Tm, List Tm) - go (App _ t u) args = go t (u :: args) - go t args = (t, args) - -public export -data Binder : Type where - MkBinder : FC -> String -> Icit -> Quant -> Tm -> Binder - --- I don't have a show for terms without a name list -export -Show Binder where - show (MkBinder _ nm icit quant t) = "[\{show quant}\{nm} \{show icit} : ...]" - -export -splitTele : Tm -> (Tm, List Binder) -splitTele = go [] - where - 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) diff --git a/orig/Main.idr b/orig/Main.idr deleted file mode 100644 index 65a78eb..0000000 --- a/orig/Main.idr +++ /dev/null @@ -1,244 +0,0 @@ -module Main - -import Data.List -import Data.List1 -import Data.String -import Data.Vect -import Data.IORef -import Lib.Common -import Lib.Compile -import Lib.Parser -import Lib.Elab -import Lib.Parser.Impl -import Lib.Prettier -import Lib.ProcessDecl -import Lib.Token -import Lib.Tokenizer -import Lib.TopContext -import Lib.Types -import Lib.Syntax -import Lib.Syntax -import System -import System.Directory -import System.File -import System.Path -import Data.Buffer - -fail : String -> M a -fail msg = putStrLn msg >> exitFailure - -jsonTopContext : M Json -jsonTopContext = do - top <- get - pure $ JsonObj [("context", JsonArray (map jsonDef $ toList top.defs))] - where - jsonDef : TopEntry -> Json - -- There is no FC here... - jsonDef (MkEntry fc (QN ns name) type def) = JsonObj - [ ("fc", toJson fc) - , ("name", toJson name) - , ("type", toJson (render 80 $ pprint [] type) ) - ] - -dumpContext : TopContext -> M () -dumpContext top = do - putStrLn "Context:" - go $ toList top.defs - putStrLn "---" - where - go : List TopEntry -> M () - go [] = pure () - go (x :: xs) = putStrLn " \{show x}" >> go xs - -writeSource : String -> M () -writeSource fn = do - docs <- compile - let src = unlines $ - [ "\"use strict\";" - , "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 })" - , "const U = { tag: \"U\" };" - ] ++ map (render 90) docs - Right _ <- writeFile fn src - | Left err => fail (show err) - Right _ <- chmodRaw fn 493 | Left err => fail (show err) - pure () - - -parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl, Operators) -parseDecls fn ops [] acc = pure (acc <>> [], ops) -parseDecls fn ops toks@(first :: _) acc = - case partialParse fn (sameLevel parseDecl) ops toks of - Left (err, toks) => do - putStrLn $ showError "" err - addError err - parseDecls fn ops (recover toks) acc - Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl) - where - recover : TokenList -> TokenList - recover [] = [] - -- skip to top token, but make sure there is progress - recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds - then (tok :: toks) - else recover toks - -fastReadFile : HasIO io => String -> io (Either FileError String) -fastReadFile fn = do - Right buf <- createBufferFromFile fn | Left err => pure $ Left err - len <- rawSize buf - Right <$> getString buf 0 len - - -||| New style loader, one def at a time -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 = (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 - | 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) - - putStrLn "module \{modName}" - 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) qname - - top <- get - mc <- readIORef top.metaCtx - -- REVIEW suppressing unsolved and solved metas from previous files - -- I may want to know about (or fail early on) unsolved - let mstart = length mc.metas - -- let Right (decls, ops, toks) := partialParse fn (manySame parseDecl) top.ops toks - -- | Left (err, toks) => fail (showError src err) - (decls, ops) <- parseDecls fn top.ops toks [<] - modify { ops := ops } - - putStrLn "process Decls" - - traverse_ (tryProcessDecl ns) (collectDecl decls) - - -- we don't want implict errors from half-processed functions - -- but suppress them all on error for simplicity. - [] <- readIORef top.errors - | errors => do - for_ errors $ \err => - putStrLn (showError src err) - exitFailure - - if stk == [] then logMetas mstart else pure () - pure src - where - - -- parseDecls : - -- tryParseDecl : - tryProcessDecl : List String -> Decl -> M () - tryProcessDecl ns decl = do - Left err <- tryError $ processDecl ns decl | _ => pure () - addError err - -processFile : String -> M () -processFile fn = do - putStrLn "*** Process \{fn}" - let parts = split (== '/') fn - 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 base [] (QN path modName') - top <- get - -- dumpContext top - - [] <- readIORef top.errors - | errors => do - for_ errors $ \err => - putStrLn (showError src err) - 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 -cmdLine ("-v" :: args) = do - modify { verbose := True } - cmdLine args -cmdLine ("-o" :: fn :: args) = do - (out, files) <- cmdLine args - pure (out <|> Just fn, files) - -cmdLine (fn :: args) = do - let True := ".newt" `isSuffixOf` fn - | _ => error emptyFC "Bad argument \{show fn}" - (out, files) <- cmdLine args - pure $ (out, fn :: files) - -main' : M () -main' = do - (arg0 :: args) <- getArgs - | _ => error emptyFC "error reading args" - (out, files) <- cmdLine args - traverse_ processFile files - - when (elem "--top" args) $ putStrLn "TOP:\{renderJson !jsonTopContext}" - - case out of - Nothing => pure () - Just name => writeSource name - -%export "javascript:newtMain" -main : IO () -main = do - -- we'll need to reset for each file, etc. - ctx <- empty - Right _ <- runM main' ctx - | Left err => do - putStrLn "ERROR at \{show $ getFC err}: \{errorMsg err}" - exitFailure - putStrLn "done"