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

more work on well scoped

Browse Source
This commit is contained in:
Steve Dunham
2023-07-18 22:28:08 -07:00
parent 59f726ab96
commit f221f09423
3 changed files with 153 additions and 57 deletions
Download Patch File Download Diff File Expand all files Collapse all files

93
src/Lib/Check.idr
View File

@@ -1,10 +1,95 @@
module Lib.Check
import Control.Monad.Error.Interface
import Control.Monad.Identity
import Lib.Parser.Impl
import Data.Vect
import Data.String
import Lib.TT
import Syntax
record Cxt where
env : List Val
record Context (n : Nat) (f : Nat) where
-- review this
env : Env f n -- Vect n (Val f)
types : List (String, Val f)
pos : SourcePos
extend : Context n f -> Val f -> Context (S n) f
extend ctx ty = { env := ty :: ctx.env } ctx
-- cribbed this, it avoids MonadError String m => everywhere
parameters {0 m : Type -> Type} {auto _ : MonadError String m}
infer : {f : Nat} -> Context n f -> Raw -> m (Tm f n, Val f)
-- I think I'm hand-waving n here, probably need it in Context
check : {f : Nat} -> Context n f -> Raw -> Val f -> m (Tm f n)
check ctx (RLam _ _ _) ty = ?ch_rhs
check ctx tm ty = do
(tm', ty') <- infer ctx tm
if quote _ ty /= quote _ ty' then
throwError "type mismatch"
else pure tm'
infer ctx (RVar nm) = go 0 ctx.types
where
go : Nat -> List (String, Val f) -> m (Tm f n, Val f)
go i [] = throwError "\{show nm} not in scope"
-- REVIEW Local or Bnd (ezoo does not have both)
go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd ?i_not_fin, 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...
(t, tty) <- infer ctx t
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
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
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
infer ctx (RAnn tm rty) = do
ty <- check ctx rty VU
let vty = eval ctx.env ty
tm <- check ctx tm vty
pure (tm, vty)
infer ctx (RLam str icit tm) = throwError "can't infer lambda"
infer ctx _ = ?later
-- 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

98
src/Lib/TT.idr
View File

@@ -10,7 +10,7 @@ Name = String
-- Trying to do well-scoped here, so the indices are proven.
export
public export
data Icit = Implicit | Explicit
%name Icit icit
@@ -28,9 +28,24 @@ data Tm : Nat -> Nat -> Type where
%name Tm t, u, v
-- TODO derive
export
Eq (Tm k n) where
(Local x) == (Local y) = x == y
(Bnd x) == (Bnd y) = x == y
(Ref x) == (Ref y) = x == y
(Lam str icit t) == y = ?rhs_3
(App t u) == y = ?rhs_4
U == y = ?rhs_5
(Pi str icit t u) == y = ?rhs_6
(Let str icit t u v) == y = ?rhs_7
_ == _ = False
-- public export
-- data Closure : Nat -> Type
data Val : Nat -> Type
public export
0 Closure : Nat -> Type
-- IS/TypeTheory.idr is calling this a Kripke function space
@@ -58,49 +73,51 @@ Env k n = Vect n (Val k)
export
eval : Env k n -> Tm k n -> Val k
export
vapp : Val k -> Val k -> Val k
vapp (VLam _ icit t) u = t 0 u
vapp t u = VApp t u
-- weakenEnv : (l : Nat) -> Env k n -> Env (l + k) n
-- thinEnv : (l : Nat) -> Env k n -> Env (l + k) n
weakenVal : {e : Nat} -> Val k -> Val (e + k)
weakenVal (VVar x) = VVar (shift _ x)
weakenVal (VRef str) = VRef str
weakenVal (VApp x y) = VApp (weakenVal x) (weakenVal y)
weakenVal (VLam str icit f) = VLam str icit
thinVal : {e : Nat} -> Val k -> Val (e + k)
thinVal (VVar x) = VVar (shift _ x)
thinVal (VRef str) = VRef str
thinVal (VApp x y) = VApp (thinVal x) (thinVal y)
thinVal (VLam str icit f) = VLam str icit
(\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
weakenVal (VPi str icit x f) = VPi str icit (weakenVal {e} x)
thinVal (VPi str icit x f) = VPi str icit (thinVal {e} x)
(\g, v => rewrite plusAssociative g e k in f (g + e) (rewrite sym $ plusAssociative g e k in v))
weakenVal VU = VU
thinVal VU = VU
bind : (e : Nat) -> Val (plus e k) -> Env k n -> Env (e + k) (S n)
bind e v env = v :: map weakenVal env
bind e v env = v :: map thinVal env
-- is this weaken or thin?
weaken : {e : Nat} -> Tm k (S n) -> Tm (plus e k) (S n)
weaken (Local x) = Local (shift _ x)
weaken (Bnd x) = Bnd x
weaken (Ref str) = Ref str
weaken (Lam str x t) = Lam str x (weaken t)
weaken (App t u) = App (weaken t) (weaken u)
weaken U = U
weaken (Pi str x t u) = Pi str x (weaken t) (weaken u)
weaken (Let str x t u v) = Let str x (weaken t) (weaken u) (weaken v)
-- is this thin or thin?
thin : {e : Nat} -> Tm k (S n) -> Tm (plus e k) (S n)
thin (Local x) = Local (shift _ x)
thin (Bnd x) = Bnd x
thin (Ref str) = Ref str
thin (Lam str x t) = Lam str x (thin t)
thin (App t u) = App (thin t) (thin u)
thin U = U
thin (Pi str x t u) = Pi str x (thin t) (thin u)
thin (Let str x t u v) = Let str x (thin t) (thin u) (thin v)
eval env (Local x) = VVar x -- this is a hole in intrinsic, vfree x in the other
eval env (Ref x) = VRef x
eval env (Bnd n) = index n env
eval env (Lam x icit t) = VLam x icit (\e, u => eval (bind e u env) (weaken t))-- (MkClosure env t)
eval env (Lam x icit t) = VLam x icit (\e, u => eval (bind e u env) (thin t))-- (MkClosure env t)
eval env (App t u) = vapp (eval env t) (eval env u)
eval env U = VU
eval env (Pi x icit a b) = VPi x icit (eval env a) (\e, u => eval (bind e u env) (weaken b))
eval env (Pi x icit a b) = VPi x icit (eval env a) (\e, u => eval (bind e u env) (thin b))
-- This one we need to make
eval env (Let x icit ty t u) = eval (eval env t :: env) u
vfresh : (l : Nat) -> Val (S l)
vfresh l = VVar last
export
quote : (k : Nat) -> Val k -> Tm 0 k
quote l (VVar k) = Bnd (complement k) -- level to index
quote l (VApp t u) = App (quote l t) (quote l u)
@@ -110,6 +127,7 @@ quote l (VPi x icit a b) = Pi x icit (quote l a) (quote (S l) (b 1 $ vfresh l))
quote l VU = U
quote _ (VRef n) = Ref n
export
nf : {n : Nat} -> Env 0 n -> Tm 0 n -> Tm 0 0
nf env t = quote 0 (eval env t)
@@ -122,29 +140,29 @@ public export
Types : Nat -> Type
Types n = Vect n (Name, Lazy (Val n))
public export
record Ctx (n : Nat) where
constructor MkCtx
env : Env k n -- for eval
types : Types n -- name lookup, pp
bds : Vect n BD -- meta creation
lvl : Nat -- This is n, do we need it?
-- Kovacs and Weirich use a position node
pos : SourcePos
-- public export
-- record Ctx (n : Nat) where
-- constructor MkCtx
-- env : Env k n -- for eval
-- types : Types n -- name lookup, pp
-- bds : Vect n BD -- meta creation
-- lvl : Nat -- This is n, do we need it?
-- -- Kovacs and Weirich use a position node
-- pos : SourcePos
%name Ctx ctx
public export
emptyCtx : Ctx Z
emptyCtx = MkCtx {k=0} [] [] [] 0 (0,0)
-- %name Ctx ctx
-- public export
-- bind : Name -> Lazy (Val (k + n)) -> Ctx n -> Ctx (S n)
-- bind x a (MkCtx env types bds l pos) =
-- MkCtx (VVar l :: env) ((x,a) :: types) (Bound :: bds) (l+1) pos
-- emptyCtx : Ctx Z
-- emptyCtx = MkCtx {k=0} [] [] [] 0 (0,0)
-- 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 n -> Lazy (Val n) -> Ctx n -> Ctx (S n)
-- define x v ty (MkCtx env types bds l pos) =
-- MkCtx (v :: env) ((x,ty) :: types) (Defined :: bds) (l + 1) pos
-- MkCtx (v :: env) ((x,ty) :: map (map thinVal) types) (Defined :: bds) (l + 1) pos