diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 9a8b3dd..15bf697 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -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 diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index af829a4..a875505 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -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 diff --git a/src/Syntax.idr b/src/Syntax.idr index 440474a..656b5d5 100644 --- a/src/Syntax.idr +++ b/src/Syntax.idr @@ -4,9 +4,7 @@ import Data.String import Data.Maybe import Lib.Parser.Impl import Lib.Prettier - - -Name = String +import Lib.TT data Raw : Type where @@ -14,11 +12,6 @@ public export data Literal = LString String | LInt Int | LBool Bool public export data RigCount = Rig0 | RigW --- I think I got Eq from pi-forall, it uses it for equality args (which are kinda like Prop/Rig0?) -public export -data Plicity = Implicit | Explicit -- | Eq - -%name Plicity icit public export data Pattern @@ -38,10 +31,10 @@ data CaseAlt = MkAlt Pattern Raw public export data Raw = RVar Name - | RLam String Plicity Raw - | RApp Raw Raw Plicity + | RLam String Icit Raw + | RApp Raw Raw Icit | RU - | RPi (Maybe Name) Plicity Raw Raw + | RPi (Maybe Name) Icit Raw Raw | RLet Name Raw Raw Raw | RSrcPos SourcePos Raw @@ -123,7 +116,7 @@ Show Pattern where Show CaseAlt where show (MkAlt x y)= foo ["MkAlt", show x, assert_total $ show y] -Show Plicity where +Show Icit where show Implicit = "Implicit" show Explicit = "Explicit" -- show Eq = "Eq" @@ -151,7 +144,7 @@ export Pretty Raw where pretty = asDoc 0 where - wrap : Plicity -> Doc -> Doc + wrap : Icit -> Doc -> Doc wrap Implicit x = x wrap Explicit x = text "{" ++ x ++ text "}"