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

Add vscode extension, command line argument, and positioned error handling.

Browse Source
This commit is contained in:
Steve Dunham
2024-07-04 23:40:38 -04:00
parent 0cad438f4d
commit b9f921ab3b
24 changed files with 5701 additions and 98 deletions
Download Patch File Download Diff File Expand all files Collapse all files

31
src/Lib/Check.idr
View File

@@ -10,13 +10,13 @@ import Lib.TopContext
import Syntax
-- cribbed this, it avoids MonadError String m => everywhere
parameters {0 m : Type -> Type} {auto _ : MonadError String m} (top : TopContext)
parameters {0 m : Type -> Type} {auto _ : MonadError Error m} (top : TopContext)
export
infer : Context -> Raw -> m (Tm, Val)
export
check : Context -> Raw -> Val -> m Tm
check ctx (RSrcPos x tm) ty = check ({pos := x} ctx) tm ty
check ctx (RLam nm icit tm) ty = case ty of
(VPi pinm icit a b) => do
-- TODO icit
@@ -24,18 +24,25 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m} (top : TopContext
let ctx' = extend ctx nm a
tm' <- check ctx' tm (b $$ var)
pure $ Lam nm icit tm'
other => throwError "Expected pi type \{show $ quote 0 ty}"
-- So it gets stuck for `List a`, not a pi type, and we want the
-- (This is not a data constructor, but a church encoding)
-- List reduces now and we're stuck for `Nat`.
other => error [(DS "Expected pi type, got \{show $ quote 0 ty}")]
check ctx tm ty = do
(tm', ty') <- infer ctx tm
if quote 0 ty /= quote 0 ty' then
throwError "type mismatch"
error [DS "type mismatch"]
else pure tm'
infer ctx (RVar nm) = go 0 ctx.types
where
go : Nat -> Vect n (String, Val) -> m (Tm, Val)
go i [] = throwError "\{show nm} not in scope \{show $ map fst ctx.types}"
go i [] = case lookup nm top of
Just (MkEntry name ty (Fn t)) => pure (Ref nm (Just t), eval [] CBN ty)
Just (MkEntry name ty _) => pure (Ref nm Nothing, eval [] CBN ty)
Nothing => error [DS "\{show nm} not in scope"]
go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty)
else go (i + 1) xs
-- need environment of name -> type..
@@ -45,12 +52,12 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m} (top : TopContext
case tty of
(VPi str icit' a b) => do
u <- check ctx u a
pure (App t u, b $$ eval ctx.env t)
_ => throwError "Expected Pi type"
pure (App t u, b $$ eval ctx.env CBN t)
_ => error [DS "Expected Pi type"]
infer ctx RU = pure (U, VU) -- YOLO
infer ctx (RPi nm icit ty ty2) = do
ty' <- check ctx ty VU
let vty' := eval ctx.env ty'
let vty' := eval ctx.env CBN ty'
let nm := fromMaybe "_" nm
ty2' <- check (extend ctx nm vty') ty2 VU
pure (Pi nm icit ty' ty2', VU)
@@ -58,13 +65,13 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m} (top : TopContext
infer ctx (RSrcPos x tm) = infer ({pos := x} ctx) tm
infer ctx (RAnn tm rty) = do
ty <- check ctx rty VU
let vty = eval ctx.env ty
let vty = eval ctx.env CBN ty
tm <- check ctx tm vty
pure (tm, vty)
infer ctx (RLam str icit tm) = throwError "can't infer lambda"
infer ctx (RLam str icit tm) = error [DS "can't infer lambda"]
infer ctx _ = throwError "TODO"
infer ctx _ = error [DS "TODO"]
-- I don't have types for these yet...
-- infer ctx (RLit (LString str)) = ?rhs_10

14
src/Lib/Parser.idr
View File

@@ -1,13 +1,11 @@
module Lib.Parser
import Lib.TT
-- NEXT - need to sort out parsing implicits
--
-- app: foo {a} a b
-- lam: λ {A} {b : A} (c : Blah) d e f. something
-- app: foo {a} a b
-- lam: λ {A} {b : A} (c : Blah) d e f => something
-- lam: \ {A} {b : A} (c : Blah) d e f => something
-- pi: (A : Set) -> {b : A} -> (c : Foo b) -> c -> bar d
-- pi: (A B : Set) {b : A} -> (c : Foo b) -> c -> bar d
import Lib.Token
import Lib.Parser.Impl
@@ -139,7 +137,7 @@ pLetArg = (Implicit,,) <$> braces ident <*> optional (sym ":" >> typeExpr)
export
lamExpr : Parser Raw
lamExpr = do
keyword "\\"
keyword "\\" <|> keyword "λ"
commit
args <- some pLetArg
keyword "=>"
@@ -170,7 +168,7 @@ caseExpr = do
alts <- startBlock $ someSame $ caseAlt
pure $ RCase sc alts
term = caseExpr
term = withPos $ caseExpr
<|> letExpr
<|> lamExpr
<|> parseOp

6
src/Lib/Parser/Impl.idr
View File

@@ -23,14 +23,14 @@ data Error = E SourcePos String
public export
showError : String -> Error -> String
showError src (E (line, col) msg) = "Err at \{show (line,col)} \{msg}\n" ++ go 0 (lines src)
showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ go 0 (lines src)
where
go : Int -> List String -> String
go l [] = ""
go l (x :: xs) =
if l == line then
"\{x}\n\{replicate (cast col) ' '}^\n"
else if line - 3 < l then x ++ "\n" ++ go (l + 1) xs
" \{x}\n \{replicate (cast col) ' '}^\n"
else if line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs
else go (l + 1) xs
-- Result of a parse

11
src/Lib/Prettier.idr
View File

@@ -57,10 +57,13 @@ best : Nat -> Nat -> Doc -> DOC
best w k x = be w k [(0,x)]
-- Public interface
public export
interface Pretty a where
pretty : a -> Doc
export
pretty : Nat -> Doc -> String
pretty w x = layout (best w 0 x)
render : Nat -> Doc -> String
render w x = layout (best w 0 x)
public export
Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y)
@@ -124,3 +127,7 @@ fill : List Doc -> Doc
fill [] = Empty
fill [x] = x
fill (x :: y :: xs) = (flatten x <+> fill (flatten y :: xs)) `Alt` (x </> fill (y :: xs))
public export
FromString Doc where
fromString = text

80
src/Lib/TT.idr
View File

@@ -3,11 +3,10 @@
-- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q
-- or drop the indices for now.
-- The Control.App requires a patched idris. :(
module Lib.TT
-- For SourcePos
import Lib.Parser.Impl
import Lib.Prettier
import Control.Monad.Error.Interface
import Data.Fin
@@ -27,7 +26,8 @@ data Icit = Implicit | Explicit
public export
data Tm : Type where
Bnd : Nat -> Tm
Ref : String -> Tm
-- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc.
Ref : String -> Maybe Tm -> Tm
Lam : Name -> Icit -> Tm -> Tm
App : Tm -> Tm -> Tm
U : Tm
@@ -38,8 +38,8 @@ data Tm : Type where
public export
Show Tm where
show (Bnd k) = "Bnd \{show k}"
show (Ref str) = "Ref \{show str}"
show (Bnd k) = "(Bnd \{show k})"
show (Ref str _) = "(Ref \{show str})"
show (Lam nm Implicit t) = "(λ {\{nm}} => \{show t})"
show (Lam nm Explicit t) = "(λ \{nm} => \{show t})"
show (App t u) = "(\{show t} \{show u})"
@@ -61,7 +61,7 @@ export
Eq (Tm) where
-- (Local x) == (Local y) = x == y
(Bnd x) == (Bnd y) = x == y
(Ref x) == (Ref y) = x == y
(Ref x _) == (Ref y _) = x == y
(Lam n icit t) == (Lam n' icit' t') = icit == icit' && t == t'
(App t u) == App t' u' = t == t' && u == u'
U == U = True
@@ -92,7 +92,7 @@ public export
data Val : Type where
-- This will be local / flex with spine.
VVar : Nat -> Val
VRef : String -> Val
VRef : String -> Maybe Tm -> Val
VApp : Val -> Lazy (Val) -> Val
VLam : Name -> Icit -> Closure -> Val
VPi : Name -> Icit -> Lazy Val -> Closure -> Val
@@ -102,14 +102,17 @@ public export
Env : Type
Env = List Val
public export
data Mode = CBN | CBV
export
eval : Env -> Tm -> Val
eval : Env -> Mode -> Tm -> Val
data Closure = MkClosure Env Tm
public export
($$) : Closure -> Val -> Val
($$) (MkClosure env tm) u = eval (u :: env) tm
($$) : {auto mode : Mode} -> Closure -> Val -> Val
($$) (MkClosure env tm) u = eval (u :: env) mode tm
public export
infixl 8 $$
@@ -122,40 +125,38 @@ vapp t u = VApp t u
bind : Val -> Env -> Env
bind v env = v :: env
eval env (Ref x) = VRef x
eval env (App t u) = vapp (eval env t) (eval env u)
eval env U = VU
eval env (Lam x icit t) = VLam x icit (MkClosure env t)
eval env (Pi x icit a b) = VPi x icit (eval env a) (MkClosure env b)
eval env (Let x icit ty t u) = eval (eval env t :: env) u
eval env (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index
-- Do we want a def in here instead? We'll need DCon/TCon eventually
-- I need to be aggressive about reduction, I guess. I'll figure it out
-- later, maybe need lazy glued values.
eval env mode (Ref x (Just tm)) = eval env mode tm
eval env mode (Ref x Nothing) = VRef x Nothing
eval env mode (App (Ref x (Just tm)) u) = vapp (eval env mode tm) (eval env mode u)
eval env mode (App t u) = vapp (eval env mode t) (eval env mode u)
eval env mode U = VU
eval env mode (Lam x icit t) = VLam x icit (MkClosure env t)
eval env mode (Pi x icit a b) = VPi x icit (eval env mode a) (MkClosure env b)
eval env mode (Let x icit ty t u) = eval (eval env mode t :: env) mode u
eval env mode (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index
in rval
export
quote : (lvl : Nat) -> Val -> Tm
quote l (VVar k) = Bnd ((l `minus` k) `minus` 1) -- level to index
quote l (VApp t u) = App (quote l t) (quote l u)
-- so this one is calling the kripke on [x] and a fresh var
quote l (VLam x icit t) = Lam x icit (quote (S l) (t $$ VVar l)) -- that one is too big
quote l (VLam x icit t) = Lam x icit (quote (S l) (t $$ VVar l))
quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b $$ VVar l))
quote l VU = U
quote _ (VRef n) = Ref n
quote l (VRef n tm) = Ref n tm
-- how are we using this? Can we assume completely closed?
-- ezoo only seems to use it at [], but essentially does this:
export
nf : Env -> Tm -> Tm
nf env t = quote (length env) (eval env t)
nf env t = quote (length env) (eval env CBN t)
public export
conv : (lvl : Nat) -> Val -> Val -> Bool
-- data BD = Bound | Defined
-- public export
-- Types : Type
-- Types = List (Name, Lazy Val)
{-
smalltt
@@ -208,6 +209,25 @@ export partial
Show Context where
show ctx = "Context \{show $ map fst $ ctx.types}"
-- TODO Pretty Context
-- idea cribbed from pi-forall
public export
data ErrorSeg : Type where
DD : Pretty a => a -> ErrorSeg
DS : String -> ErrorSeg
toDoc : ErrorSeg -> Doc
toDoc (DD x) = pretty x
toDoc (DS str) = text str
export
error : {0 m : Type -> Type} -> {auto _ : MonadError Error m} ->
{auto ctx : Context} -> List ErrorSeg -> m a
error xs = throwError $ E ctx.pos (render 80 $ spread $ map toDoc xs)
||| add a binding to environment
export
extend : Context -> String -> Val -> Context
@@ -220,10 +240,7 @@ define : Context -> String -> Val -> Val -> Context
define (MkCtx lvl env types bds pos) name val ty =
MkCtx (S lvl) (val :: env) ((name, ty) :: types) (Defined :: bds) pos
update : Context -> String -> Tm -> Context
-- oof
-- not used
lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} ->
Context -> String -> m Val
lookup ctx nm = go ctx.types
@@ -232,3 +249,4 @@ lookup ctx nm = go ctx.types
go [] = throwError "Name \{nm} not in scope"
go ((n, ty) :: xs) = if n == nm then pure ty else go xs

9
src/Lib/TopContext.idr
View File

@@ -25,7 +25,7 @@ record TopEntry where
export
Show TopEntry where
show (MkEntry name type def) = "\{show name} : \{show type} := \{show def}"
show (MkEntry name type def) = "\{name} : \{show type} := \{show def}"
||| Top level context.
||| Most of the reason this is separate is to have a different type
@@ -65,5 +65,10 @@ claim tc name ty = { defs $= (MkEntry name ty Axiom ::) } tc
public export
addDef : TopContext -> String -> Tm -> Tm -> TopContext
addDef tc name tm ty = { defs $= (MkEntry name ty (Fn tm) ::) } tc
addDef tc name tm ty = { defs $= go } tc
where
go : List TopEntry -> List TopEntry
-- FIXME throw if we hit [] or is not an axiom
go [] = []
go ((MkEntry nm _ _) :: xs) = MkEntry nm ty (Fn tm) :: xs