From 468c3a4c6aa8172a3697426801e8a237116b56f1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 27 Apr 2022 21:58:09 +0200
Subject: [PATCH] grtt -> qtt

---
 README.md                       |   4 +-
 src/Quox/Equal.idr              |   6 +-
 src/Quox/Syntax/Term/Base.idr   |   4 +-
 src/Quox/Syntax/Term/Pretty.idr |   4 +-
 src/Quox/Syntax/Term/Reduce.idr |  11 ++--
 src/Quox/Typechecker.idr        | 110 +++++++++++++++-----------------
 src/Quox/Typing.idr             |  15 ++---
 7 files changed, 70 insertions(+), 84 deletions(-)

diff --git a/README.md b/README.md
index db91c2f..149d3ca 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,4 @@
 # ![](qtuwu.png) quantitative observational extensional(ish) type theory
 
-hey what would happen if some idiot tried to weld qtt[^1] and xtt together?
+hey what would happen if some idiot tried to weld qtt and xtt together?
 let's find out together
-
-[^1]: actually grtt but wtf is a grox
diff --git a/src/Quox/Equal.idr b/src/Quox/Equal.idr
index c96d872..e017a3b 100644
--- a/src/Quox/Equal.idr
+++ b/src/Quox/Equal.idr
@@ -43,10 +43,8 @@ parameters {auto _ : MonadThrow Error m}
            Sub   => unless (k <= l) $ throw $ ClashU Sub   k l
     compareTN' mode s@(TYPE _) t _ _ = clashT mode s t
 
-    compareTN' mode (Pi qtm1 qty1 _ arg1 res1)
-                    (Pi qtm2 qty2 _ arg2 res2) _ _ = do
-      -- [todo] these should probably always be ==, right..?
-      unless (qtm1 == qtm2) $ throw $ ClashQ qtm1 qtm2
+    compareTN' mode (Pi qty1 _ arg1 res1) (Pi qty2 _ arg2 res2) _ _ = do
+      -- [todo] this should probably always be ==, right..?
       unless (qty1 == qty2) $ throw $ ClashQ qty1 qty2
       compareT0  mode arg2 arg1 -- reversed for contravariant Sub
       compareTS0 mode res1 res2
diff --git a/src/Quox/Syntax/Term/Base.idr b/src/Quox/Syntax/Term/Base.idr
index a377339..6017846 100644
--- a/src/Quox/Syntax/Term/Base.idr
+++ b/src/Quox/Syntax/Term/Base.idr
@@ -36,7 +36,7 @@ mutual
     TYPE : (l : Universe) -> Term d n
 
     ||| function type
-    Pi  : (qtm, qty : Qty) -> (x : Name) ->
+    Pi  : (qty : Qty) -> (x : Name) ->
           (arg : Term d n) -> (res : ScopeTerm d n) -> Term d n
     ||| function term
     Lam : (x : Name) -> (body : ScopeTerm d n) -> Term d n
@@ -91,7 +91,7 @@ mutual
 
 public export %inline
 Arr : Qty -> Term d n -> Term d n -> Term d n
-Arr pi a b = Pi {qtm = pi, qty = zero, x = "_", arg = a, res = TUnused b}
+Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
 
 ||| same as `F` but as a term
 public export %inline
diff --git a/src/Quox/Syntax/Term/Pretty.idr b/src/Quox/Syntax/Term/Pretty.idr
index ae78f7e..59d0578 100644
--- a/src/Quox/Syntax/Term/Pretty.idr
+++ b/src/Quox/Syntax/Term/Pretty.idr
@@ -30,9 +30,9 @@ mutual
   PrettyHL (Term d n) where
     prettyM (TYPE l) =
       parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
-    prettyM (Pi qtm qty x s t) =
+    prettyM (Pi qty x s t) =
       parensIfM Outer $ hang 2 $
-        !(prettyBinder [qtm, qty] x s) <++> !arrowD
+        !(prettyBinder [qty] x s) <++> !arrowD
           <//> !(under T x $ prettyM t)
     prettyM (Lam x t) =
       parensIfM Outer $
diff --git a/src/Quox/Syntax/Term/Reduce.idr b/src/Quox/Syntax/Term/Reduce.idr
index 611fba0..267304a 100644
--- a/src/Quox/Syntax/Term/Reduce.idr
+++ b/src/Quox/Syntax/Term/Reduce.idr
@@ -64,8 +64,8 @@ mutual
                     Term dfrom from -> NotCloTerm dto to
   pushSubstsTWith th ph (TYPE l) =
     ncloT $ TYPE l
-  pushSubstsTWith th ph (Pi qtm qty x a body) =
-    ncloT $ Pi qtm qty x (subs a th ph) (subs body th ph)
+  pushSubstsTWith th ph (Pi qty x a body) =
+    ncloT $ Pi qty x (subs a th ph) (subs body th ph)
   pushSubstsTWith th ph (Lam x body) =
     ncloT $ Lam x $ subs body th ph
   pushSubstsTWith th ph (E e) =
@@ -120,9 +120,9 @@ mutual
   Tighten (Term d) where
     tighten p (TYPE l) =
       pure $ TYPE l
-    tighten p (Pi qtm qty x arg res) =
-      Pi qtm qty x <$> tighten p arg
-                   <*> tighten p res
+    tighten p (Pi qty x arg res) =
+      Pi qty x <$> tighten p arg
+               <*> tighten p res
     tighten p (Lam x body) =
       Lam x <$> tighten p body
     tighten p (E e) =
@@ -160,4 +160,3 @@ weakT t = t //. shift 1
 public export %inline
 weakE : Elim d n -> Elim d (S n)
 weakE t = t //. shift 1
-
diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr
index 973ed89..144127a 100644
--- a/src/Quox/Typechecker.idr
+++ b/src/Quox/Typechecker.idr
@@ -16,11 +16,11 @@ expectTYPE s =
 
 private covering %inline
 expectPi : MonadThrow Typing.Error m => Term d n ->
-           m (Qty, Qty, Term d n, ScopeTerm d n)
+           m (Qty, Term d n, ScopeTerm d n)
 expectPi ty =
   case (whnfT ty).fst of
-       Pi qtm qty _ arg res => pure (qtm, qty, arg, res)
-       _                    => throw $ ExpectedPi ty
+       Pi qty _ arg res => pure (qty, arg, res)
+       _                => throw $ ExpectedPi ty
 
 private %inline
 expectEqualQ : MonadThrow Equal.Error m =>
@@ -40,14 +40,14 @@ tail = {tctx $= tail, qctx $= tail}
 
 private %inline
 weakI : InferResult d n -> InferResult d (S n)
-weakI = {type $= weakT, tmout $= (:< zero), tyout $= (:< zero)}
+weakI = {type $= weakT, qout $= (:< zero)}
 
 private
-lookupBound : {n : Nat} -> Var n -> TyContext d n -> InferResult d n
-lookupBound VZ (MkTyContext {tctx = _ :< ty, qctx = _ :< tyout, _}) =
-  InfRes {type = weakT ty, tmout = zero :< one, tyout = tyout :< zero}
-lookupBound (VS i) ctx =
-  weakI $ lookupBound i (tail ctx)
+lookupBound : {n : Nat} -> Qty -> Var n -> TyContext d n -> InferResult d n
+lookupBound pi VZ (MkTyContext {tctx = _ :< ty, _}) =
+  InfRes {type = weakT ty, qout = zero :< pi}
+lookupBound pi (VS i) ctx =
+  weakI $ lookupBound pi i (tail ctx)
 
 
 mutual
@@ -55,88 +55,80 @@ mutual
   -- to either push them or parametrise the whole typechecker over ambient
   -- substitutions. both of them seem like the same amount of work for the
   -- computer but pushing is less work for the me
+  --
+  -- [todo] probably need to check that pi is 1 or 0 like atkey said
 
   export covering %inline
   check : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (subj : Term d n) -> (ty : Term d n) ->
+          (ctx : TyContext d n) -> (pi : Qty) ->
+          (subj : Term d n) -> (ty : Term d n) ->
           m (CheckResult n)
-  check ctx subj ty = check' ctx (pushSubstsT subj) ty
+  check ctx pi subj ty = check' ctx pi (pushSubstsT subj) ty
 
   export covering %inline
   infer : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-          (ctx : TyContext d n) -> (subj : Elim d n) ->
+          (ctx : TyContext d n) -> (pi : Qty) -> (subj : Elim d n) ->
           m (InferResult d n)
-  infer ctx subj = infer' ctx (pushSubstsE subj)
+  infer ctx pi subj = infer' ctx pi (pushSubstsE subj)
 
 
   export covering
   check' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-           (ctx : TyContext d n) ->
+           (ctx : TyContext d n) -> (pi : Qty) ->
            (subj : NotCloTerm d n) -> (ty : Term d n) ->
            m (CheckResult n)
 
-  check' ctx (Element (TYPE l) _) ty = do
+  check' ctx pi (Element (TYPE l) _) ty = do
     l' <- expectTYPE ty
+    expectEqualQ zero pi
     unless (l < l') $ throw $ BadUniverse l l'
-    pure $ ChkRes {tmout = zero, tyout = zero}
+    pure zero
 
   -- [todo] factor this stuff out
-  check' ctx (Element (Pi qtm qty x arg (TUsed res)) _) ty = do
+  check' ctx pi (Element (Pi qty x arg res) _) ty = do
     l <- expectTYPE ty
-    argty <- check ctx arg (TYPE l)
-    resty <- check (extendTy arg argty.tmout ctx) res (TYPE l)
-    res'tmout <- popQ qty resty.tmout
-    pure $ ChkRes {tmout = argty.tmout + res'tmout, tyout = zero}
-  check' ctx (Element (Pi qtm qty x arg (TUnused res)) _) ty = do
-    ignore $ expectTYPE ty
-    argty <- check ctx arg ty
-    resty <- check ctx res ty
-    expectEqualQ qty zero
-    pure $ ChkRes {tmout = argty.tmout + resty.tmout, tyout = zero}
+    expectEqualQ zero pi
+    ignore $ check ctx zero arg (TYPE l)
+    case res of
+         TUsed   res => ignore $ check (extendTy arg zero ctx) zero res (TYPE l)
+         TUnused res => ignore $ check ctx                     zero res (TYPE l)
+    pure zero
 
-  check' ctx (Element (Lam x body) _) ty = do
-    (qtm, qty, arg, res) <- expectPi ty
+  check' ctx pi (Element (Lam x body) _) ty = do
+    (qty, arg, res) <- expectPi ty
     -- [todo] do this properly?
     let body = fromScopeTerm body; res = fromScopeTerm res
-    argres <- check ctx arg (TYPE UAny)
-    let ctx' = extendTy arg argres.tmout ctx
-    bodyres <- check ctx' body res
-    tmout <- popQ qtm bodyres.tmout
-    tyout <- popQ qty bodyres.tyout
-    pure $ ChkRes {tmout, tyout = argres.tmout + tyout}
+    qout <- check (extendTy arg (pi * qty) ctx) pi body res
+    popQ qty qout
 
-  check' ctx (Element (E e) _) ty = do
-    infres <- infer ctx e
-    tyres  <- check ctx ty (TYPE UAny)
+  check' ctx pi (Element (E e) _) ty = do
+    infres <- infer ctx pi e
+    ignore $ check ctx zero ty (TYPE UAny)
     infres.type `subT` ty
-    pure $ ChkRes {tmout = infres.tmout, tyout = tyres.tmout}
+    pure infres.qout
 
   export covering
   infer' : MonadThrows [Typing.Error, Equal.Error] m => {d, n : Nat} ->
-           (ctx : TyContext d n) -> (subj : NotCloElim d n) ->
+           (ctx : TyContext d n) -> (pi : Qty) -> (subj : NotCloElim d n) ->
            m (InferResult d n)
 
-  infer' ctx (Element (F x) _) =
+  infer' ctx pi (Element (F x) _) =
+    -- [todo] check that global is erased ==> pi = zero
     case lookup x ctx.globals of
-         Just g  => pure $ InfRes {type = g.type, tmout = zero, tyout = zero}
+         Just g  => pure $ InfRes {type = g.type, qout = zero}
          Nothing => throw $ NotInScope x
 
-  infer' ctx (Element (B i) _) = pure $ lookupBound i ctx
+  infer' ctx pi (Element (B i) _) =
+    pure $ lookupBound pi i ctx
 
-  infer' ctx (Element (fun :@ arg) _) = do
-    funres <- infer ctx fun
-    (qtm, qty, argty, resty) <- expectPi funres.type
-    let resty = fromScopeTerm resty
-    argres <- check ctx arg argty
-    let ctx' = extendTy argty argres.tyout ctx
-    resres <- check ctx' resty (TYPE UAny)
-    res'tyout <- popQ qty resres.tmout
-    let type = resty //. (arg :# argty ::: id)
-    pure $ InfRes {type,
-                   tmout = funres.tmout + qtm * argres.tmout,
-                   tyout = res'tyout    + qty * argres.tmout}
+  infer' ctx pi (Element (fun :@ arg) _) = do
+    funres <- infer ctx pi fun
+    (qty, argty, res) <- expectPi funres.type
+    argout <- check ctx (pi * qty) arg argty
+    pure $ InfRes {type = fromScopeTerm res //. ((arg :# argty) ::: id),
+                   qout = funres.qout + argout}
 
-  infer' ctx (Element (tm :# ty) _) = do
-    ignore $ check ctx ty (TYPE UAny)
-    res <- check ctx tm ty
-    pure $ InfRes {type = ty, tmout = res.tmout, tyout = res.tyout}
+  infer' ctx pi (Element (tm :# ty) _) = do
+    ignore $ check ctx zero ty (TYPE UAny)
+    qout <- check ctx pi tm ty
+    pure $ InfRes {type = ty, qout}
diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr
index a3174f9..0974914 100644
--- a/src/Quox/Typing.idr
+++ b/src/Quox/Typing.idr
@@ -24,11 +24,11 @@ TContext d = Context (Term d)
 
 public export
 QContext : Nat -> Type
-QContext = Triangle' Qty
+QContext = Context' Qty
 
 public export
 QOutput : Nat -> Type
-QOutput = Context' Qty
+QOutput = QContext
 
 
 public export
@@ -60,8 +60,8 @@ namespace TContext
 
 namespace TyContext
   export
-  extendTy : Term d n -> QOutput n -> TyContext d n -> TyContext d (S n)
-  extendTy s rhos = {tctx $= (:< s), qctx $= (:< rhos)}
+  extendTy : Term d n -> Qty -> TyContext d n -> TyContext d (S n)
+  extendTy s rho = {tctx $= (:< s), qctx $= (:< rho)}
 
   export
   extendDim : TyContext d n -> TyContext (S d) n
@@ -87,15 +87,14 @@ namespace QOutput
 
 
 public export
-record CheckResult n where
-  constructor ChkRes
-  tmout, tyout : QOutput n
+CheckResult : Nat -> Type
+CheckResult = QOutput
 
 public export
 record InferResult d n where
   constructor InfRes
   type : Term d n
-  tmout, tyout : QOutput n
+  qout : QOutput n
 
 
 public export