From 8c3951bd05037ecb28c336146436b6e1f0936d0a Mon Sep 17 00:00:00 2001 From: Bohdan Date: Tue, 16 Jan 2024 16:59:16 +0100 Subject: [PATCH] fix typing rules and (parts of) the typechecker MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit fixes rules for TyElim, TyLam, TyLet move checkDef to inferDef add a sigma to getPi add rezz-scope to resurrect scopes from Γ --- src/Context.agda | 7 +++++ src/Conversion.agda | 11 +++++--- src/Typechecker.agda | 62 +++++++++++++++++++++++--------------------- src/Typing.agda | 22 ++++++++-------- 4 files changed, 57 insertions(+), 45 deletions(-) diff --git a/src/Context.agda b/src/Context.agda index f3000d5..c458ba0 100644 --- a/src/Context.agda +++ b/src/Context.agda @@ -53,3 +53,10 @@ lookupVar (CtxExtend Γ y s) x p = raise (rezz _) (inBindCase p (λ q → lookupVar Γ x q)) {-# COMPILE AGDA2HS lookupVar #-} + +rezz-scope : (Γ : Context α) → Rezz (Scope name) α +rezz-scope CtxEmpty = rezz _ +rezz-scope (CtxExtend Γ x _) = + rezzCong (λ t → (singleton x) <> t) (rezz-scope Γ) + +{-# COMPILE AGDA2HS rezz-scope #-} diff --git a/src/Conversion.agda b/src/Conversion.agda index 29ca3ef..8a59803 100644 --- a/src/Conversion.agda +++ b/src/Conversion.agda @@ -37,15 +37,18 @@ private variable data Conv (@0 Γ : Context α) : @0 Type α → @0 Term α → @0 Term α → Set data ConvElim (@0 Γ : Context α) : @0 Type α → @0 Term α → @0 Elim α → @0 Elim α → Set -@0 renameTop : Term (x ◃ α) → Term (y ◃ α) -renameTop {x = x} {y = y} = substTerm (liftBindSubst {x = x} {y = y} (idSubst (rezz _))) +renameTop : Rezz _ α → Term (x ◃ α) → Term (y ◃ α) +renameTop {x = x} {y = y} r = substTerm (liftBindSubst {x = x} {y = y} (idSubst r)) + +@0 renameTopE : Term (x ◃ α) → Term (y ◃ α) +renameTopE = renameTop (rezz _) data Conv {α} Γ where CRefl : Conv Γ t u u - CLam : Conv {α = x ◃ α} (Γ , x ∶ a) b (renameTop u) (renameTop v) + CLam : Conv {α = x ◃ α} (Γ , x ∶ a) b (renameTopE u) (renameTopE v) → Conv Γ (TPi x k l a b) (TLam y u) (TLam z v) CPi : Conv Γ (TSort k) a a' - → Conv (Γ , x ∶ a) (TSort (weakenSort (subWeaken subRefl) l)) b (renameTop b') + → Conv (Γ , x ∶ a) (TSort (weakenSort (subWeaken subRefl) l)) b (renameTopE b') → Conv Γ (TSort (funSort k l)) (TPi x k l a b) (TPi y k l a' b') CApp : Conv Γ a u u' → ConvElim Γ a u w w' diff --git a/src/Typechecker.agda b/src/Typechecker.agda index 557dbd4..325950a 100644 --- a/src/Typechecker.agda +++ b/src/Typechecker.agda @@ -74,7 +74,17 @@ postulate liftMaybe : Maybe a → TCError → TCM a liftEither : Either TCError a → TCM a - +-- this is Either and not TCM because otherwise some meta doesn't get solved 🤷 +getPi : (t : Term α) + → Either TCError + (Σ0 (name) + (λ x → ∃ ((Sort α × Sort α) × (Type α × Type (x ◃ α))) + (λ ( (sa , sb) , (ta , tb) ) → t ≡ TPi x sa sb ta tb) + )) +getPi term@(TPi x sa sr at rt) = Right ( ⟨ x ⟩ ((sa , sr) , (at , rt)) ⟨ refl ⟩) +getPi _ = Left "coudn't reduce the term to become a pi type" + +{-# TERMINATING #-} inferType : (te : Term α) → TCM (∃ (Type α) (λ ty → Γ ⊢ te ∷ ty)) @@ -90,25 +100,22 @@ inferApp : (u : Term α) (e : Elim α) → TCM (∃ (Type α) (λ ty → Γ ⊢ TApp u e ∷ ty)) inferApp {α = α} {Γ = Γ} u (Syntax.EArg v) = do + let r = (rezz-scope Γ) (tu ⟨ gtu ⟩ ) ← inferType {Γ = Γ} u fuel <- tcmFuel pifuel <- liftMaybe (tryFuel stepEither (Left (makeState tu)) fuel) "couldn't construct Fuel for Pi reduction" - -- FIXME: need to resurrect α, can be done from Γ potentially? - let rpi = reduce (rezz _) tu pifuel - (⟨ x ⟩ ( (sv , sr) , (tv , tr))) ← liftEither (getPi rpi) + let rpi = reduce r tu pifuel + --Would be nice to have an inlined case here instead of getPi + --https://agda.readthedocs.io/en/latest/language/syntactic-sugar.html#do-notation + --but it won't get compiled to haskell + (⟨ x ⟩ ((sv , sr) , (tv , tr)) ⟨ eq ⟩) ← liftEither (getPi rpi) + --FIXME: this should be CRedL, but that requires eq to be matched with refl + --atm agda can't unify it let gc = convert {Γ = Γ} (TSort (funSort sv sr)) tu (TPi x sv sr tv tr) gtv ← checkType {Γ = Γ} v tv - -- FIXME: need to resurrect α, can be done from Γ potentially? - return ((substTop (rezz _) v tr) ⟨ TyAppE gtu (TyArg gc gtv) ⟩ ) - where - getPi : Term α - → Either TCError - (Σ0 (name) - (λ x → (Sort α × Sort α) × (Type α × Type (x ◃ α)))) - getPi term@(TPi x sa sr at rt) = Right ( ⟨ x ⟩ ((sa , sr) , (at , rt))) - getPi _ = Left "coudn't reduce the term to become a pi type" + return ((substTop r v tr) ⟨ TyAppE gtu (TyArg gc gtv) ⟩ ) inferApp {Γ = Γ} u (Syntax.EProj x x₁) = tcError "not implemented" inferApp {Γ = Γ} u (Syntax.ECase bs) = tcError "not implemented" @@ -126,25 +133,19 @@ inferTySort : (s : Sort α) → TCM (∃ (Type α) (λ ty → Γ ⊢ TSort s ∷ ty)) inferTySort (STyp x) = return (TSort (STyp (suc x)) ⟨ TyType ⟩) -checkDef : (@0 f : name) +inferDef : (@0 f : name) (p : f ∈ defs) - (ty : Type α) - → TCM (Γ ⊢ TDef f p ∷ ty) -checkDef f p ty = do - -- FIXME: doesn't work with the error: weaken subEmpty (lookupAll defType p) != ty - --return (TyDef f) - tcError "can't typecheck because idk how" + → TCM (∃ (Type α) (λ ty → Γ ⊢ TDef f p ∷ ty)) +inferDef f p = return (((weaken subEmpty (defType ! f))) ⟨ (TyDef f) ⟩) checkLambda : (@0 x : name) (u : Term (x ◃ α)) (ty : Type α) → TCM (Γ ⊢ TLam x u ∷ ty) checkLambda {Γ = Γ} x u (TPi y su sv tu tv) = do - -- FIXME: the names x and y don't match - --d ← checkType {Γ = Γ , x ∶ tu} u tv - --return (TyLam d) - tcError "can't typecheck because idk how" ---FIXME + d ← checkType {Γ = Γ , y ∶ tu} (renameTop (rezz-scope Γ) u) tv + return (TyLam d) +--FIXME: reduce ty and see if it's a Pi checkLambda x u _ = tcError "can't check lambda against a type that isn't a Pi" checkLet : (@0 x : name) @@ -155,9 +156,7 @@ checkLet : (@0 x : name) checkLet {Γ = Γ} x u v ty = do tu ⟨ dtu ⟩ ← inferType {Γ = Γ} u dtv ← checkType {Γ = Γ , x ∶ tu} v (weaken (subWeaken subRefl) ty) - -- FIXME: doesn't work with the error: substTop (rezz α) u ty != ty - --return (TyLet dtu dtv) - tcError "can't typecheck because idk how" + return (TyLet {r = rezz-scope Γ} dtu dtv) checkConv : (t : Term α) (cty tty : Type α) @@ -169,7 +168,10 @@ checkType {Γ = Γ} t@(TVar x p) ty = do tvar ← inferVar {Γ = Γ} x p (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty checkConv {Γ = Γ} t ty (TSort tsor) tvar -checkType (TDef f p) ty = checkDef f p ty +checkType {Γ = Γ} (TDef d p) ty = do + tdef ← inferDef d p + (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty + checkConv {Γ = Γ} (TDef d p) ty (TSort tsor) tdef checkType (TCon c p x) ty = tcError "not implemented yet" checkType (TLam x te) ty = checkLambda x te ty checkType {Γ = Γ} t@(TApp u e) ty = do @@ -188,7 +190,7 @@ checkType (TLet x u v) ty = checkLet x u v ty checkType (TAnn u t) ty = tcError "not implemented yet" inferType (TVar x p) = inferVar x p -inferType (TDef d x) = tcError "can't infer the type of a definition" +inferType (TDef d p) = inferDef d p inferType (TCon c p x) = tcError "not implemented yet" inferType (TLam x te) = tcError "can't infer the type of a lambda" inferType (TApp u e) = inferApp u e diff --git a/src/Typing.agda b/src/Typing.agda index c5542e4..daf0df7 100644 --- a/src/Typing.agda +++ b/src/Typing.agda @@ -64,10 +64,10 @@ data TyTerm {α} Γ where -- TODO: constructor typing TyLam : - - (Γ , x ∶ s) ⊢ u ∷ t + {@0 r : Rezz _ α} + → (Γ , x ∶ s) ⊢ (renameTop r u) ∷ t ------------------------------------------------------------ - → Γ ⊢ TLam x u ∷ TPi x k l s t + → Γ ⊢ TLam y u ∷ TPi x k l s t TyAppE : Γ ⊢ u ∷ s @@ -87,12 +87,12 @@ data TyTerm {α} Γ where -------------------------------------------- Γ ⊢ TSort (STyp n) ∷ TSort (STyp (suc n)) - TyLet : + TyLet : {r : Rezz _ α} - Γ ⊢ u ∷ s - → (Γ , x ∶ s) ⊢ v ∷ t + → Γ ⊢ u ∷ s + → (Γ , x ∶ s) ⊢ v ∷ (weaken (subWeaken subRefl) t) ------------------------------------------ - → Γ ⊢ TLet x u v ∷ substTop (rezz α) u t + → Γ ⊢ TLet x u v ∷ t TyAnn : Γ ⊢ u ∷ t @@ -108,11 +108,11 @@ data TyTerm {α} Γ where {-# COMPILE AGDA2HS TyTerm #-} -data TyElim Γ where - TyArg : - Conv Γ (TSort k) v (TPi x l m s t) +data TyElim {α} Γ where + TyArg : {@0 r : Rezz _ α} + → Conv Γ (TSort k) v (TPi x l m s t) → TyTerm Γ u s - → TyElim Γ (EArg u) v (λ h → substTop (rezz _) u t) + → TyElim Γ (EArg u) v (λ h → substTop r u t) -- TODO: proj -- TODO: case