write quantities before names in binders again

also fixup comments in typechecker
2023-02-13 22:05:27 +01:00 · 2023-02-13 22:05:27 +01:00 · fe8c224299
commit fe8c224299
parent a6f43a772e
4 changed files with 78 additions and 57 deletions
--- a/lib/Quox/Pretty.idr
+++ b/lib/Quox/Pretty.idr
@ -90,6 +90,14 @@ parensIf : Bool -> Doc HL -> Doc HL
 parensIf True  = parens
 parensIf False = id

+export %inline
+comma : Doc HL
+comma = hl Delim ","
+
+
+export %inline
+asep : List (Doc a) -> Doc a
+asep = align . sep

 export
 separate' : Doc a -> List (Doc a) -> List (Doc a)
@ -109,6 +117,10 @@ export %inline
 vseparate : Doc a -> List (Doc a) -> Doc a
 vseparate s = vsep . separate' s

+export %inline
+aseparate : Doc a -> List (Doc a) -> Doc a
+aseparate s = align . separate s
+

 public export
 record PrettyEnv where
@ -178,6 +190,10 @@ export PrettyHL BaseName where prettyM = pure . pretty . baseStr
 export PrettyHL Name     where prettyM = pure . pretty . toDots


+export
+nameSeq : HL -> List Name -> Doc HL
+nameSeq h = hl h . asep . map (pretty0 False)
+
 export %inline
 prettyStr : PrettyHL a => (unicode : Bool) -> a -> String
 prettyStr unicode =
@ -217,3 +233,13 @@ infixr 6 </>
 export %inline
 (</>) : Doc a -> Doc a -> Doc a
 a </> b = cat [a, b]
+
+
+
+||| wrapper for names that pretty-prints highlighted as a `TVar`.
+public export data TVarName = TV Name
+export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
+
+||| wrapper for names that pretty-prints highlighted as a `DVar`.
+public export data DVarName = DV Name
+export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@ -1,6 +1,7 @@
 module Quox.Syntax.Qty

 import Quox.Pretty
+import Quox.Name
 import public Quox.Decidable
 import Data.DPair

@ -18,10 +19,12 @@ blobD : Pretty.HasEnv m => m (Doc HL)
 blobD = hlF Delim $ ifUnicode "·" "@"

 export %inline
-prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => List q -> m (Doc HL)
-prettyQtyBinds [] = pure ""
-prettyQtyBinds qtys =
-  pure $ !blobD <++> align (sep $ commas !(traverse pretty0M qtys))
+prettyQtyBinds : Pretty.HasEnv m => PrettyHL q => PrettyHL a =>
+                 List q -> a -> m (Doc HL)
+prettyQtyBinds []   x = pretty0M x
+prettyQtyBinds qtys x = pure $
+  hang 2 $ sep [aseparate comma !(traverse pretty0M qtys) <++> !blobD,
+                !(pretty0M x)]


 public export
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@ -31,6 +31,7 @@ caseD   = hl Syntax "case"
 ofD     = hl Syntax "of"
 returnD = hl Syntax "return"

+
 mutual
  export covering
  PrettyHL q => PrettyHL (Term q d n) where
@ -110,18 +111,9 @@ mutual
                   ScopeTerm q d n -> m (Doc HL)
  prettyBindType qtys x s arr t =
      parensIfM Outer $ hang 2 $
-        !(prettyBinder qtys x s) <++> arr
+        parens !(prettyQtyBinds qtys $ TV x) <++> arr
          <//> !(under T x $ prettyM t)

-  export covering
-  prettyBinder : Pretty.HasEnv m => PrettyHL q =>
-                 List q -> Name -> Term q d n -> m (Doc HL)
-  prettyBinder pis x a =
-    pure $ parens $ hang 2 $
-      hsep [hl TVar !(prettyM x),
-            sep [!(prettyQtyBinds pis),
-                 hsep [colonD, !(withPrec Outer $ prettyM a)]]]
-
  export covering
  prettyLams : Pretty.HasEnv m => PrettyHL q =>
               BinderSort -> List Name -> Term q _ _ -> m (Doc HL)
@ -161,6 +153,6 @@ mutual
               q -> a -> Name -> b -> List (List Name, Doc HL, c) -> m (Doc HL)
  prettyCase pi elim r ret arms =
    pure $ align $ sep $
-      [hsep [caseD,   !(prettyM elim), !(prettyQtyBinds [pi])],
+      [hsep [caseD,   !(prettyQtyBinds [pi] elim)],
       hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
       hsep [ofD,     !(prettyArms arms)]]
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@ -100,86 +100,86 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
           (subj : Term q d n) -> (0 nc : NotClo subj) -> Term q d n ->
           m (CheckResult q n)

-  check' ctx sg (TYPE l) _ ty = do
-    -- if ℓ < ℓ' then Ψ | Γ ⊢ Type ℓ · 0 ⇐ Type ℓ' ⊳ 𝟎
-    l' <- expectTYPE !ask ty
+  check' ctx sg (TYPE k) _ ty = do
+    -- if 𝓀 < ℓ then Ψ | Γ ⊢₀ Type 𝓀 ⇐ Type ℓ
+    l <- expectTYPE !ask ty
    expectEqualQ zero sg.fst
-    unless (l < l') $ throwError $ BadUniverse l l'
+    unless (k < l) $ throwError $ BadUniverse k l
    pure $ zeroFor ctx

  check' ctx sg (Pi qty _ arg res) _ ty = do
    l <- expectTYPE !ask ty
    expectEqualQ zero sg.fst
-    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
    ignore $ check0 ctx arg (TYPE l)
-    -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
    case res of
      TUsed   res => ignore $ check0 (extendTy arg zero ctx) res (TYPE l)
      TUnused res => ignore $ check0 ctx res (TYPE l)
-    -- then Ψ | Γ ⊢ (x : A) → B · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
    pure $ zeroFor ctx

  check' ctx sg (Lam _ body) _ ty = do
    (qty, arg, res) <- expectPi !ask ty
-    -- if Ψ | Γ, x · πσ : A ⊢ t · σ ⇐ B ⊳ Σ, x · σπ
+    -- if Ψ | Γ, πσ·x : A ⊢ σ · t ⇐ B ⊳ Σ, σπ·x
    qout <- check (extendTy arg (sg.fst * qty) ctx) sg body.term res.term
-    -- then Ψ | Γ ⊢ λx. t · σ ⇐ (x · π : A) → B ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
    popQ (sg.fst * qty) qout

  check' ctx sg (Sig _ fst snd) _ ty = do
    l <- expectTYPE !ask ty
    expectEqualQ zero sg.fst
-    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
    ignore $ check0 ctx fst (TYPE l)
-    -- if Ψ | Γ, x · 0 : A ⊢ B · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
    case snd of
      TUsed   snd => ignore $ check0 (extendTy fst zero ctx) snd (TYPE l)
      TUnused snd => ignore $ check0 ctx snd (TYPE l)
-    -- then Ψ | Γ ⊢ (x : A) × B · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
    pure $ zeroFor ctx

  check' ctx sg (Pair fst snd) _ ty = do
    (tfst, tsnd) <- expectSig !ask ty
-    -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ₁
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
    qfst <- check ctx sg fst tfst
    let tsnd = sub1 tsnd (fst :# tfst)
-    -- if Ψ | Γ ⊢ t · σ ⇐ B[s] ⊳ Σ₂
+    -- if Ψ | Γ ⊢ σ · t ⇐ B[s] ⊳ Σ₂
    qsnd <- check ctx sg snd tsnd
-    -- then Ψ | Γ ⊢ (s, t) · σ ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
    pure $ qfst + qsnd

  check' ctx sg (Eq i t l r) _ ty = do
    u <- expectTYPE !ask ty
    expectEqualQ zero sg.fst
-    -- if Ψ, i | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
    case t of
      DUsed   t => ignore $ check0 (extendDim ctx) t (TYPE u)
      DUnused t => ignore $ check0 ctx t (TYPE u)
-    -- if Ψ | Γ ⊢ l · 0 ⇐ A‹0› ⊳ 𝟎
+    -- if Ψ | Γ ⊢₀ l ⇐ A‹0›
    ignore $ check0 ctx t.zero l
-    -- if Ψ | Γ ⊢ r · 0 ⇐ A‹1› ⊳ 𝟎
+    -- if Ψ | Γ ⊢₀ r ⇐ A‹1›
    ignore $ check0 ctx t.one  r
-    -- then Ψ | Γ ⊢ Eq [i ⇒ A] l r ⇐ Type ℓ ⊳ 𝟎
+    -- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
    pure $ zeroFor ctx

  check' ctx sg (DLam i body) _ ty = do
    (ty, l, r) <- expectEq !ask ty
-    -- if Ψ, i | Γ ⊢ t · σ ⇐ A ⊳ Σ
+    -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
    qout <- check (extendDim ctx) sg body.term ty.term
    let eqs = makeDimEq ctx.dctx
-    -- if Ψ ⊢ t‹0› = l
+    -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
    equal eqs ctx.tctx ty.zero body.zero l
-    -- if Ψ ⊢ t‹1› = r
+    -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
    equal eqs ctx.tctx ty.one body.one  r
-    -- then Ψ | Γ ⊢ (λᴰi ⇒ t) · σ ⇐ Eq [i ⇒ A] l r ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
    pure qout

  check' ctx sg (E e) _ ty = do
-    -- if Ψ | Γ ⊢ e · σ ⇒ A' ⊳ Σ
+    -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
    infres <- infer ctx sg e
-    -- if Ψ ⊢ A' <: A
+    -- if Ψ | Γ ⊢ A' <: A
    subtype (makeDimEq ctx.dctx) ctx.tctx infres.type ty
-    -- then Ψ | Γ ⊢ e · σ ⇐ A ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
    pure infres.qout

  export covering
@ -192,22 +192,22 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
    g <- lookupFree x
    -- if σ ≤ π
    expectCompatQ sg.fst g.qty
-    -- then Ψ | Γ ⊢ x ⇒ A ⊳ 𝟎
+    -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
    pure $ InfRes {type = g.type.get, qout = zeroFor ctx}

  infer' ctx sg (B i) _ =
    -- if x : A ∈ Γ
-    -- then Ψ | Γ ⊢ x · σ ⇒ A ⊳ (𝟎, σ · x, 𝟎)
+    -- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ · x, 𝟎)
    pure $ lookupBound sg.fst i ctx

  infer' ctx sg (fun :@ arg) _ = do
-    -- if Ψ | Γ ⊢ f · σ ⇒ (x · π : A) → B ⊳ Σ₁
+    -- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
    funres <- infer ctx sg fun
    (qty, argty, res) <- expectPi !ask funres.type
-    -- if Ψ | Γ ⊢ s · σ∧π ⇐ A ⊳ Σ₂
+    -- if Ψ | Γ ⊢ σ∧π · s ⇐ A ⊳ Σ₂
    --   (0∧π = σ∧0 = 0; σ∧π = σ otherwise)
    argout <- check ctx (subjMult sg qty) arg argty
-    -- then Ψ | Γ ⊢ f s · σ ⇒ B[s] ⊳ Σ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · f s ⇒ B[s] ⊳ Σ₁ + Σ₂
    pure $ InfRes {
      type = sub1 res $ arg :# argty,
      qout = funres.qout + argout
@ -216,33 +216,33 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  infer' ctx sg (CasePair pi pair _ ret _ _ body) _ = do
    -- if 1 ≤ π
    expectCompatQ one pi
-    -- if Ψ | Γ ⊢ pair · 1 ⇒ (x : A) × B ⊳ Σ₁
+    -- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁
    pairres <- infer ctx sone pair
    ignore $ check0 (extendTy pairres.type zero ctx) ret.term (TYPE UAny)
    (tfst, tsnd) <- expectSig !ask pairres.type
-    -- if Ψ | Γ, x · π : A, y · π : B ⊢ σ body ⇐ ret[(x, y)]
-    --      ⊳ Σ₂, x · π₁, y · π₂
-    -- if π₁, π₂ ≤ π
+    -- if Ψ | Γ, π·x : A, π·y : B ⊢ σ body ⇐ ret[(x, y)]
+    --      ⊳ Σ₂, π₁·x, π₂·y
+    -- with π₁, π₂ ≤ π
    let bodyctx = extendTyN [< (tfst, pi), (tsnd.term, pi)] ctx
        bodyty  = substCasePairRet pairres.type ret
    bodyout <- check bodyctx sg body.term bodyty >>= popQs [< pi, pi]
-    -- then Ψ | Γ ⊢ σ case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
+    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[pair] ⊳ πΣ₁ + Σ₂
    pure $ InfRes {
      type = sub1 ret pair,
      qout = pi * pairres.qout + bodyout
    }

  infer' ctx sg (fun :% dim) _ = do
-    -- if Ψ | Γ ⊢ f · σ ⇒ Eq [i ⇒ A] l r ⊳ Σ
+    -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
    InfRes {type, qout} <- infer ctx sg fun
    (ty, _, _) <- expectEq !ask type
-    -- then Ψ | Γ ⊢ f p · σ ⇒ A‹p› ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
    pure $ InfRes {type = dsub1 ty dim, qout}

  infer' ctx sg (term :# type) _ = do
-    -- if Ψ | Γ ⊢ A · 0 ⇐ Type ℓ ⊳ 𝟎
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
    ignore $ check0 ctx type (TYPE UAny)
-    -- if Ψ | Γ ⊢ s · σ ⇐ A ⊳ Σ
+    -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ
    qout <- check ctx sg term type
-    -- then Ψ | Γ ⊢ (s ∷ A) · σ ⇒ A ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · (s ∷ A) ⇒ A ⊳ Σ
    pure $ InfRes {type, qout}