make context explicit, drop explicit module arg

agda-core.cabal

@@ -28,6 +28,8 @@ library
                     , Agda.Core.Reduce
                     , Agda.Core.Syntax
                     , Agda.Core.Substitute
+                    , Agda.Core.Utils
+                    , Utils.Either
                     -- , Agda.Core.Typechecker
                     -- , Agda.Core.Typing
     build-depends:    base   >= 4.17    && < 4.20
@@ -37,6 +39,7 @@ library
     ghc-options:
       -- agda2hs generates many (safe) incomplete patterns
       -fno-warn-incomplete-patterns
+      -fno-warn-name-shadowing
 
 executable agda-core
     import:           warnings
@@ -46,7 +49,6 @@ executable agda-core
     other-modules:    Agda.Core.ToCore
                     , Paths_agda_core
     autogen-modules:  Paths_agda_core
-    documentation: True
     default-extensions:
       LambdaCase
       RecordWildCards

src/Agda/Core/Typechecker.agda

@@ -6,12 +6,12 @@ open import Haskell.Prelude
 open import Scope
 
 open import Agda.Core.GlobalScope using (Globals)
-import Agda.Core.Signature
+import Agda.Core.Signature as Signature
 
 module Agda.Core.Typechecker
     {@0 name    : Set}
     (@0 globals : Globals name)
-    (open Agda.Core.Signature globals)
+    (open Signature globals)
     (@0 sig     : Signature)
   where
 
@@ -31,81 +31,80 @@ open import Haskell.Extra.Erase
 
 private variable
   @0 α : Scope name
-  Γ    : Context α
-
+
 postulate
-  inferSort : (t : Type α) → TCM (Σ[ s ∈ Sort α ] Γ ⊢ t ∶ TSort s)
-  convert : (@0 ty : Type α) (@0 a b : Term α) → Γ ⊢ a ≅ b ∶ ty
+  inferSort : (Γ : Context α) (t : Type α) → TCM (Σ[ s ∈ Sort α ] Γ ⊢ t ∶ TSort s)
+  convert   : (Γ : Context α) (@0 ty : Type α) (@0 a b : Term α) → Γ ⊢ a ≅ b ∶ ty
 
-inferType : ∀ u   → TCM (Σ[ t ∈ Type α ] Γ ⊢ u ∶ t)
-{-# COMPILE AGDA2HS inferType #-}
+inferType : ∀ (Γ : Context α) u → TCM (Σ[ t ∈ Type α ] Γ ⊢ u ∶ t)
+checkType : ∀ (Γ : Context α) u t → TCM (Γ ⊢ u ∶ t)
 
-checkType : ∀ u t → TCM (Γ ⊢ u ∶ t)
-{-# COMPILE AGDA2HS checkType #-}
 
-inferVar : ∀ (@0 x) (p : x ∈ α) → TCM (Σ[ t ∈ Type α ] Γ ⊢ TVar x p ∶ t)
-inferVar {Γ = g} x p = return (lookupVar g x p , TyTVar p)
+inferVar : ∀ Γ (@0 x) (p : x ∈ α) → TCM (Σ[ t ∈ Type α ] Γ ⊢ TVar x p ∶ t)
+inferVar g x p = return (lookupVar g x p , TyTVar p)
 
-inferApp : ∀ u e → TCM (Σ[ t ∈ Type α ] Γ ⊢ TApp u e ∶ t)
-inferApp {Γ = Γ} u (Syntax.EArg v) = do
-  let r = rezzScope Γ
+inferApp : ∀ Γ u e → TCM (Σ[ t ∈ Type α ] Γ ⊢ TApp u e ∶ t)
+inferApp ctx u (Syntax.EArg v) = do
+  let r = rezzScope ctx
 
   fuel      ← tcmFuel
   rezz sig  ← tcmSignature
 
-  tu  , gtu ← inferType {Γ = Γ} u
-  stu , _   ← inferSort {Γ = Γ} tu
+  tu  , gtu ← inferType ctx u
+  stu , _   ← inferSort ctx tu
 
   case reduce r sig tu fuel of λ where
     Nothing → tcError "not enough fuel to reduce term"
     (Just (TPi x sa sr at rt)) ⦃ p ⦄ → do
-      gtv ← checkType {Γ = Γ} v at
+      gtv ← checkType ctx v at
       let gc = CRedL (⟨ r ⟩ fuel ⟨ p ⟩) CRefl
       pure $ substTop r v rt , TyAppE gtu (TyArg {k = funSort sa sr} gc gtv)
     (Just _) → tcError "couldn't reduce term to pi type"
 
-inferApp {Γ = Γ} u (Syntax.EProj x x₁) = tcError "not implemented"
-inferApp {Γ = Γ} u (Syntax.ECase bs) = tcError "not implemented"
-
-inferPi : (@0 x : name)
-          (su sv : Sort α)
-          (u : Term α)
-          (v : Term (x ◃ α))
-          → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TPi x su sv u v ∶ ty)
-inferPi {Γ = Γ} x su sv u v = do
-  tu <- checkType {Γ = Γ} u (TSort su)
-  tv <- checkType {Γ = Γ , x ∶ u} v (TSort (weakenSort (subWeaken subRefl) sv))
+inferApp ctx u (Syntax.EProj _ _) = tcError "not implemented"
+inferApp ctx u (Syntax.ECase bs)  = tcError "not implemented"
+
+inferPi
+  : ∀ Γ (@0 x : name)
+  (su sv : Sort α)
+  (u : Term α)
+  (v : Term (x ◃ α))
+  → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TPi x su sv u v ∶ ty)
+inferPi ctx x su sv u v = do
+  tu <- checkType ctx u (TSort su)
+  tv <- checkType (ctx , x ∶ u) v (TSort (weakenSort (subWeaken subRefl) sv))
   pure $ TSort (funSort su sv) , TyPi tu tv
 
-inferTySort : (s : Sort α) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TSort s ∶ ty)
-inferTySort (STyp x) = pure $ TSort (STyp (suc x)) , TyType
+inferTySort : ∀ Γ (s : Sort α) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TSort s ∶ ty)
+inferTySort ctx (STyp x) = pure $ TSort (STyp (suc x)) , TyType
 
-inferDef : (@0 f : name) (p : f ∈ defScope ) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TDef f p ∶ ty)
-inferDef f p = do
+inferDef : ∀ Γ (@0 f : name) (p : f ∈ defScope) → TCM (Σ[ ty ∈ Type α ] Γ ⊢ TDef f p ∶ ty)
+inferDef ctx f p = do
   rezz sig ← tcmSignature
   pure $ weaken subEmpty (getType sig f p) , TyDef p
 
-checkLambda : (@0 x : name)
+checkLambda : ∀ Γ (@0 x : name)
               (u : Term (x ◃ α))
               (ty : Type α)
               → TCM (Γ ⊢ TLam x u ∶ ty)
-checkLambda {Γ = Γ} x u (TPi y su sv tu tv) = do
-  d ← checkType {Γ = Γ , x ∶ tu} u (renameTop (rezzScope Γ) tv)
+checkLambda ctx x u (TPi y su sv tu tv) = do
+  d ← checkType (ctx , x ∶ tu) u (renameTop (rezzScope ctx) 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"
+checkLambda ctx x u _ = tcError "can't check lambda against a type that isn't a Pi"
 
-checkLet : (@0 x : name)
+checkLet : ∀ Γ (@0 x : name)
            (u : Term α)
            (v : Term (x ◃ α))
            (ty : Type α)
            → TCM (Γ ⊢ TLet x u v ∶ ty)
-checkLet {Γ = Γ} x u v ty = do
-  tu , dtu  ← inferType {Γ = Γ} u
-  dtv ← checkType {Γ = Γ , x ∶ tu} v (weaken (subWeaken subRefl) ty)
-  return (TyLet {r = rezzScope Γ} dtu dtv)
+checkLet ctx x u v ty = do
+  tu , dtu  ← inferType ctx u
+  dtv       ← checkType (ctx , x ∶ tu) v (weaken (subWeaken subRefl) ty)
+
+  return (TyLet {r = rezzScope ctx} dtu dtv)
 
-checkCoerce : (t : Term α)
+checkCoerce : ∀ Γ (t : Term α)
             → Σ[ ty ∈ Type α ] Γ ⊢ t ∶ ty
             → (cty : Type α) -- the type we want to have
             → (tty : Type α) -- the type of types
@@ -120,42 +119,45 @@ checkCoerce : (t : Term α)
 --for pi
 --for sort
 --the rest should be reduced away
-checkCoerce t (s , d) cty tty = return (TyConv d (convert tty s cty))
-
-
-
-checkType {Γ = Γ} t@(TVar x p) ty = do
-  tvar     ← inferVar {Γ = Γ} x p
-  tsor , _ ← inferSort {Γ = Γ} ty
-  checkCoerce {Γ = Γ} t tvar ty (TSort tsor)
-checkType {Γ = Γ} (TDef d p) ty =  do
-  tdef     ← inferDef d p
-  tsor , _ ← inferSort {Γ = Γ} ty
-  checkCoerce {Γ = Γ} (TDef d p) tdef ty (TSort tsor)
-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
-  tapp     ← inferApp {Γ = Γ} u e
-  tsor , _ ← inferSort {Γ = Γ} ty
-  checkCoerce {Γ = Γ} t tapp ty (TSort tsor)
-checkType {Γ = Γ} t@(TPi x su sv u v) ty = do
-  tpi      ← inferPi {Γ = Γ} x su sv u v
-  tsor , _ ← inferSort {Γ = Γ} ty
-  checkCoerce {Γ = Γ} t tpi ty (TSort tsor)
-checkType {Γ = Γ} t@(TSort s) ty = do
-  tts      ← inferTySort {Γ = Γ} s
-  tsor , _ ← inferSort {Γ = Γ} ty
-  checkCoerce {Γ = Γ} t tts ty (TSort tsor)
-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 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
-inferType (TPi x su sv u v) = inferPi x su sv u v
-inferType (TSort s) = inferTySort s
-inferType (TLet x te te₁) = tcError "can't infer the type of a let"
-inferType (TAnn u t) = tcError "not implemented yet"
+checkCoerce ctx t (s , d) cty tty = return (TyConv d (convert ctx tty s cty))
+
+
+
+checkType ctx (TVar x p) ty = do
+  tvar     ← inferVar ctx x p
+  tsor , _ ← inferSort ctx ty
+  checkCoerce ctx (TVar x p) tvar ty (TSort tsor)
+checkType ctx (TDef d p) ty =  do
+  tdef     ← inferDef ctx d p
+  tsor , _ ← inferSort ctx ty
+  checkCoerce ctx (TDef d p) tdef ty (TSort tsor)
+checkType ctx (TCon c p x) ty = tcError "not implemented yet"
+checkType ctx (TLam x te) ty =  checkLambda ctx x te ty
+checkType ctx (TApp u e) ty = do
+  tapp     ← inferApp ctx u e
+  tsor , _ ← inferSort ctx ty
+  checkCoerce ctx (TApp u e) tapp ty (TSort tsor)
+checkType ctx (TPi x su sv u v) ty = do
+  tpi      ← inferPi ctx x su sv u v
+  tsor , _ ← inferSort ctx ty
+  checkCoerce ctx (TPi x su sv u v) tpi ty (TSort tsor)
+checkType ctx (TSort s) ty = do
+  tts      ← inferTySort ctx s
+  tsor , _ ← inferSort ctx ty
+  checkCoerce ctx (TSort s) tts ty (TSort tsor)
+checkType ctx (TLet x u v) ty = checkLet ctx x u v ty
+checkType ctx (TAnn u t) ty = tcError "not implemented yet"
 
+{-# COMPILE AGDA2HS checkType #-}
+
+inferType ctx (TVar x p) = inferVar ctx x p
+inferType ctx (TDef d p) = inferDef ctx d p
+inferType ctx (TCon c p x) = tcError "not implemented yet"
+inferType ctx (TLam x te) = tcError "can't infer the type of a lambda"
+inferType ctx (TApp u e) = inferApp ctx u e
+inferType ctx (TPi x su sv u v) = inferPi ctx x su sv u v
+inferType ctx (TSort s) = inferTySort ctx s
+inferType ctx (TLet x te te₁) = tcError "can't infer the type of a let"
+inferType ctx (TAnn u t) = tcError "not implemented yet"
+
+{-# COMPILE AGDA2HS inferType #-}