From f959dc28fed352d2974a234f659f97bbfed2481f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 20 Feb 2023 21:38:47 +0100
Subject: [PATCH] add Functor etc for IfConsistent

---
 lib/Quox/Syntax/DimEq.idr | 28 +++++++++++++++++++++++++++-
 lib/Quox/Typechecker.idr  | 10 ++--------
 2 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 1ee5d39..f1ca157 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -29,10 +29,36 @@ data DimEq : Nat -> Type where
 
 
 public export
-data IfConsistent : DimEq d -> a -> Type where
+consistent : DimEq d -> Bool
+consistent ZeroIsOne = False
+consistent (C eqs)   = True
+
+
+public export
+data IfConsistent : DimEq d -> Type -> Type where
   Nothing :      IfConsistent ZeroIsOne a
   Just    : a -> IfConsistent (C eqs)   a
 
+export
+Functor (IfConsistent eqs) where
+  map f Nothing  = Nothing
+  map f (Just x) = Just (f x)
+
+export
+Foldable (IfConsistent eqs) where
+  foldr f z Nothing  = z
+  foldr f z (Just x) = f x z
+
+export
+Traversable (IfConsistent eqs) where
+  traverse f Nothing  = pure Nothing
+  traverse f (Just x) = Just <$> f x
+
+public export
+ifConsistent : Applicative f => (eqs : DimEq d) -> f a -> f (IfConsistent eqs a)
+ifConsistent ZeroIsOne act = pure Nothing
+ifConsistent (C _)     act = Just <$> act
+
 
 export %inline
 zeroEq : DimEq 0
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 81c37e9..7c804ae 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -62,10 +62,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   export covering %inline
   check : (ctx : TyContext q d n) -> SQty q -> Term q d n -> Term q d n ->
           m (CheckResult ctx.dctx q n)
-  check ctx@(MkTyContext {dctx, _}) sg subj ty =
-    case dctx of
-      ZeroIsOne => pure Nothing
-      C _       => Just <$> checkC ctx sg subj ty
+  check ctx sg subj ty = ifConsistent ctx.dctx $ checkC ctx sg subj ty
 
   ||| "Ψ | Γ ⊢₀ s ⇐ A"
   |||
@@ -95,10 +92,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   export covering %inline
   infer : (ctx : TyContext q d n) -> SQty q -> Elim q d n ->
           m (InferResult ctx.dctx q d n)
-  infer ctx@(MkTyContext {dctx, _}) sg subj =
-    case dctx of
-      ZeroIsOne => pure Nothing
-      C _       => Just <$> inferC ctx sg subj
+  infer ctx sg subj = ifConsistent ctx.dctx $ inferC ctx sg subj
 
   ||| `infer`, assuming the dimension context is consistent
   export covering %inline