dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

Remove original Idris version of newt.

Browse Source
This commit is contained in:
Steve Dunham
2025-09-29 11:59:13 -07:00
parent a53c5b4fba
commit f3a5e9012c
21 changed files with 7 additions and 5460 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
README.md
View File

@@ -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. 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 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 has a dropdown with some sample code, including `newt` itself.
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.
## Sample code ## Sample code
@@ -23,11 +20,11 @@ The directory `orig` contains the original version of newt written in Idris. It
## Building ## 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 ## Playground

4
newt-vscode/package.json
View File

@@ -61,8 +61,8 @@
"properties": { "properties": {
"newt.path": { "newt.path": {
"type": "string", "type": "string",
"default": "build/exec/newt", "default": "node bootstrap/newt.js",
"description": "Path to the newt executable" "description": "Command to run newt"
} }
} }
} }

4
newt-vscode/src/extension.ts
View File

@@ -32,7 +32,6 @@ export function activate(context: vscode.ExtensionContext) {
const lastChange = changes[changes.length - 1]; const lastChange = changes[changes.length - 1];
const text = lastChange.text; const text = lastChange.text;
console.log("lastChange", lastChange)
// Check if the last change is a potential shortcut trigger // Check if the last change is a potential shortcut trigger
if (!text || !( " ')\\".includes(text) || text.startsWith('\n'))) return; if (!text || !( " ')\\".includes(text) || text.startsWith('\n'))) return;
@@ -70,8 +69,7 @@ export function activate(context: vscode.ExtensionContext) {
? workspaceFolder.uri.fsPath ? workspaceFolder.uri.fsPath
: path.dirname(fileName); : path.dirname(fileName);
const config = vscode.workspace.getConfiguration("newt"); const config = vscode.workspace.getConfiguration("newt");
// FIXME wrong newt now. const cmd = config.get<string>("path", "node bootstrap/newt.js");
const cmd = config.get<string>("path", "build/exec/newt");
const command = `${cmd} --top ${fileName}`; const command = `${cmd} --top ${fileName}`;
let st = +new Date(); let st = +new Date();
exec( exec(

59
newt.ipkg
View File

@@ -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 =

154
orig/Lib/Common.idr
View File

@@ -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

349
orig/Lib/Compile.idr
View File

@@ -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

159
orig/Lib/CompileExp.idr
View File

@@ -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)

1398
orig/Lib/Elab.idr
View File

File diff suppressed because it is too large Load Diff

102
orig/Lib/Erasure.idr
View File

@@ -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

312
orig/Lib/Eval.idr
View File

@@ -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

616
orig/Lib/Parser.idr
View File

@@ -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

219
orig/Lib/Parser/Impl.idr
View File

@@ -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

149
orig/Lib/Prettier.idr
View File

@@ -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

426
orig/Lib/ProcessDecl.idr
View File

@@ -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

316
orig/Lib/Syntax.idr
View File

@@ -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

103
orig/Lib/Token.idr
View File

@@ -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)

161
orig/Lib/Tokenizer.idr
View File

@@ -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

54
orig/Lib/TopContext.idr
View File

@@ -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 ::)

599
orig/Lib/Types.idr
View File

@@ -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

28
orig/Lib/Util.idr
View File

@@ -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)

244
orig/Main.idr
View File

@@ -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"