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

checkpoint

Browse Source
This commit is contained in:
Steve Dunham
2024-04-11 15:21:13 -07:00
parent 3b1bd4aad1
commit 46f9caccab
10 changed files with 138 additions and 217 deletions
Download Patch File Download Diff File Expand all files Collapse all files

47
src/Lib/Check.idr
View File

@@ -8,31 +8,27 @@ import Data.String
import Lib.TT
import Syntax
-- cribbed this, it avoids MonadError String m => everywhere
parameters {0 m : Type -> Type} {auto _ : MonadError String m}
export
infer : Context -> Raw -> m (Tm, Val)
infer : {f : Nat} -> Context -> Raw -> m (Tm, Val)
check : {f : Nat} -> Context -> Raw -> Val -> m Tm
export
check : Context -> Raw -> Val -> m Tm
check ctx (RLam _ _ _) ty = ?ch_rhs
check ctx tm ty = do
(tm', ty') <- infer ctx tm
if quote _ ty /= quote _ ty' then
if quote 0 ty /= quote 0 ty' then
throwError "type mismatch"
else pure tm'
infer ctx (RVar nm) = go 0 ctx.types
where
go : Nat -> List (String, Val) -> m (Tm, Val)
go i [] = throwError "\{show nm} not in scope"
-- REVIEW Local or Bnd (ezoo does not have both)
go i [] = throwError "\{show nm} not in scope \{show $ map fst ctx.types}"
go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty)
else go (i + 1) xs
-- need environment of name -> type..
infer ctx (RApp t u icit) = do
-- icit will be used for insertion, lets get this working first...
@@ -40,31 +36,14 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
case tty of
(VPi str icit' a b) => do
u <- check ctx u a
-- is zero right here?
-- I have ctx.env here and TypeTheory has []
-- maybe because I'm not substing?
pure (App t u, b 0 (eval ctx.env t))
_ => throwError "Expected Pi type"
-- FIXME ctx.env?
-- vtya <- nf ctx.env tma
pure (App t u, b (eval ctx.env t))
_ => throwError "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'
-- gallais and the source paper have subst here. They're using Tm rather
-- than raw. Lets look at the zoo.
-- maybe run through zoo2 well typed...
-- it just binds vty' into the environment and evaluates
-- Kovacs is sticking the type vty' and the value Var l into the context
-- and letting the Ix pick up the Var l from the context
-- gallais/paper are subst the Var l into the Tm.
-- yaffle just pushes to the environment, but it's a list of binders
-- so types, names, no values
ty2' <- check (extend ctx vty') ty2 VU
let nm := fromMaybe "_" nm
ty2' <- check (extend ctx nm vty') ty2 VU
pure (Pi nm icit ty' ty2', VU)
infer ctx (RLet str tm tm1 tm2) = ?rhs_5
infer ctx (RSrcPos x tm) = infer ({pos := x} ctx) tm
@@ -76,11 +55,13 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m}
infer ctx (RLam str icit tm) = throwError "can't infer lambda"
infer ctx _ = ?later
infer ctx _ = throwError "TODO"
-- I don't have types for these yet...
-- infer ctx (RLit (LString str)) = ?rhs_10
-- infer ctx (RLit (LInt i)) = ?rhs_11
-- infer ctx (RLit (LBool x)) = ?rhs_12
-- infer ctx RHole = ?todo_meta2
-- infer ctx (RParseError str) = ?todo_insert_meta
-- infer ctx (RCase tm xs) = ?rhs_9
-- infer ctx RHole = ?todo_meta2
-- The idea here is to insert a hole for a parse error
-- infer ctx (RParseError str) = ?todo_insert_meta

4
src/Lib/Parser.idr
View File

@@ -60,9 +60,9 @@ withPos p = RSrcPos <$> getPos <*> p
-- the inside of Raw
atom : Parser Raw
atom = withPos ( RVar <$> ident
atom = withPos (RU <$ keyword "U"
<|> RVar <$> ident
<|> lit
<|> RU <$ keyword "U"
<|> RHole <$ keyword "_")
<|> parens term

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

@@ -1,6 +1,8 @@
module Lib.Parser.Impl
import Lib.Token
import Data.String
import Data.Nat
public export
TokenList : Type
@@ -16,9 +18,21 @@ emptyPos = (0,0)
-- Error of a parse
public export
data Error = E String
data Error = E SourcePos String
%name Error err
public export
showError : String -> Error -> String
showError src (E (line, col) msg) = "Err 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
else ""
-- Result of a parse
public export
data Result : Type -> Type where
@@ -45,22 +59,26 @@ export
runP : Parser a -> TokenList -> Bool -> SourcePos -> Result a
runP (P f) = f
error : TokenList -> String -> Error
error [] msg = E emptyPos msg
error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line, col) msg
export
parse : Parser a -> TokenList -> Either String a
parse : Parser a -> TokenList -> Either Error a
parse pa toks = case runP pa toks False emptyPos of
Fail fatal (E msg) toks com => Left "error: \{msg} next at: \{show toks}"
Fail fatal err toks com => Left err
OK a [] _ => Right a
OK a ts _ => Left "Extra toks \{show ts}"
OK a ts _ => Left (error toks "Extra toks")
-- I think I want to drop the typeclasses for v1
export
fail : String -> Parser a
fail msg = P $ \toks,com,col => Fail False (E msg) toks com
fail msg = P $ \toks,com,col => Fail False (error toks msg) toks com
export
fatal : String -> Parser a
fatal msg = P $ \toks,com,col => Fail False (E msg) toks com
fatal msg = P $ \toks,com,col => Fail False (error toks msg) toks com
-- mustWork / commit copied from Idris, but I may switch to the parsec consumption thing.
export
@@ -106,8 +124,8 @@ Monad Parser where
pred : (BTok -> Bool) -> String -> Parser String
pred f msg = P $ \toks,com,col =>
case toks of
(t :: ts) => if f t then OK (value t) ts com else Fail False (E "\{msg} vt:\{value t}") toks com
[] => Fail False (E "eof") toks com
(t :: ts) => if f t then OK (value t) ts com else Fail False (error toks "\{msg} vt:\{value t}") toks com
[] => Fail False (error toks "eof") toks com
export
commit : Parser ()
@@ -133,7 +151,7 @@ mutual
export
getPos : Parser SourcePos
getPos = P $ \toks,com, (l,c) => case toks of
[] => Fail False (E "End of file") toks com -- OK emptyPos toks com
[] => Fail False (error toks "End of file") toks com -- OK emptyPos toks com
(t :: ts) => OK (start t) toks com
||| Start an indented block and run parser in it
@@ -154,8 +172,8 @@ sameLevel (P p) = P $ \toks,com,(l,c) => case toks of
(t :: _) =>
let (tl,tc) = start t
in if tc == c then p toks com (tl, c)
else if c < tc then Fail False (E "unexpected indent") toks com
else Fail False (E "unexpected indent") toks com
else if c < tc then Fail False (error toks "unexpected indent") toks com
else Fail False (error toks "unexpected indent") toks com
export
someSame : Parser a -> Parser (List a)
@@ -169,7 +187,7 @@ indented (P p) = P $ \toks,com,(l,c) => case toks of
(t::_) =>
let (tl,tc) = start t
in if tc > c || tl == l then p toks com (l,c)
else Fail False (E "unexpected outdent") toks com
else Fail False (error toks "unexpected outdent") toks com
export
token' : Kind -> Parser String

9
src/Lib/Prettier.idr
View File

@@ -1,11 +1,10 @@
||| 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
-- A prettier printer, Philip Wadler
-- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
||| `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
@@ -13,9 +12,9 @@ import Data.Nat
export
data Doc = Empty | Line | Text String | Nest Nat Doc | Seq Doc Doc | Alt Doc Doc
||| `DOC` is an intermediate form used during layout/rendering
data DOC = EMPTY | TEXT String DOC | LINE Nat DOC
flatten : Doc -> Doc
flatten Empty = Empty
flatten (Seq x y) = Seq (flatten x) (flatten y)
@@ -60,7 +59,7 @@ best w k x = be w k [(0,x)]
-- Public interface
export
pretty : Nat -> Doc-> String
pretty : Nat -> Doc -> String
pretty w x = layout (best w 0 x)
public export

96
src/Lib/TT.idr
View File

@@ -7,6 +7,7 @@
module Lib.TT
-- For SourcePos
import Lib.Parser.Impl
import Control.Monad.Error.Interface
import Data.Fin
import Data.List
@@ -81,17 +82,12 @@ data Val : Type where
VPi : Name -> Icit -> Lazy Val -> Closure -> Val
VU : Val
||| LocalEnv free vars
public export
LocalEnv : Type
LocalEnv = List Val
public export
Env : Type
Env = List Val
export
eval : LocalEnv -> Env -> Tm -> Val
eval : Env -> Tm -> Val
export
vapp : Val -> Val -> Val
@@ -103,15 +99,16 @@ bind v env = v :: env
-- so here we have LocalEnv free vars in Yaffle
eval locs env (Ref x) = VRef x
eval locs env (App t u) = vapp (eval locs env t) (eval locs env u)
eval locs env U = VU
eval env (Ref x) = VRef x
eval env (App t u) = vapp (eval env t) (eval env u)
eval env U = VU
-- yaffle breaks out binder
eval locs env (Lam x icit t) = VLam x icit (\u => eval (u :: locs) env t)
eval locs env (Pi x icit a b) = VPi x icit (eval locs env a) (\u => eval (u :: locs) env b)
eval env (Lam x icit t) = VLam x icit (\u => eval (u :: env) t)
eval env (Pi x icit a b) = VPi x icit (eval env a) (\u => eval (u :: env) b)
-- This one we need to make
eval locs env (Let x icit ty t u) = eval (eval locs env t :: locs) env u
eval locs env (Bnd i) = let Just rval = getAt i env | _ => ?out_of_index in rval
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
in rval
vfresh : Nat -> Val
vfresh l = VVar l
@@ -129,7 +126,7 @@ quote _ (VRef n) = Ref n
-- vars -> vars -> vars in yaffle
export
nf : {n : Nat} -> Env -> Tm -> Tm
nf env t = quote n (eval [] env t)
nf env t = quote n (eval env t)
public export
conv : (lvl : Nat) -> Val -> Val -> Bool
@@ -150,62 +147,29 @@ record Context where
-- lvl = length types
pos : SourcePos -- the last SourcePos that we saw
export
empty : Context
empty = MkCtx [] [] (0,0)
export partial
Show Context where
show ctx = "Context \{show $ map fst $ ctx.types}"
-- Kovacs Small-TT has locals and globals, lets do that.
||| add a binding to environment
extend : { n : Nat} -> Context -> String -> Val -> Context
export
extend : Context -> String -> Val -> Context
extend (MkCtx env types pos) name ty =
MkCtx (VVar (length env) :: env) ((name, ty) :: types) pos
-- weirich has 'hints' to store the claims before the def is seen/checked
-- saying it is unsafe. afterwards they are mixed into the context.
-- idris essentially leaves holes, filled in later, for undefined claims
-- Is it ok to leaving them in there (if they pass checkType) as long as
-- we don't register the def if it fails checking?
-- shoot, I have another context in Check.idr
-- -- public export
-- record Ctx (n : Nat) where
-- constructor MkCtx
-- env : Env k n -- for eval
-- types : Types n -- name lookup, prettyprint
-- bds : Vect n BD -- meta creation
-- lvl : Nat -- This is n, do we need it?
-- -- Kovacs and Weirich use a position node, Idris has FC
-- pos : SourcePos
-- %name Ctx ctx
-- public export
-- emptyCtx : Ctx Z
-- emptyCtx = MkCtx {k=0} [] [] [] 0 (0,0)
-- find out how pi-forall treats binders
-- Vars are unbound TName
-- ezoo
-- Tm has Ix
-- Val has Lvl
-- by the time we hit ezoo 5/6, there is a Map string -> (Lvl, Type) for name lookup.
-- smalltt
-- idris
-- public export
-- bindCtx : Name -> Lazy (Val (zz + n)) -> Ctx n -> Ctx (S n)
-- bindCtx x a (MkCtx env types bds l pos) =
-- MkCtx (VVar l :: env) ((x,a) :: map (map thinVal) types) (Bound :: bds) (l+1) pos
-- public export
-- define : Name -> Val -> Lazy (Val) -> Ctx n -> Ctx (S n)
-- define x v ty (MkCtx env types bds l pos) =
-- MkCtx (v :: env) ((x,ty) :: map (map thinVal) types) (Defined :: bds) (l + 1) pos
lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} ->
Context -> String -> m Val
lookup ctx nm = go ctx.types
where
go : List (String,Val) -> m Val
go [] = throwError "Name \{nm} not in scope"
go ((n, ty) :: xs) = if n == nm then pure ty else go xs

2
src/Lib/Token.idr
View File

@@ -1,5 +1,7 @@
module Lib.Token
-- TODO replace this with own lexer
import public Text.Lexer
public export