From d0eb9a1edfb4233d557d954f46685f25382234d8 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Tue, 29 Apr 2025 20:37:06 +0200
Subject: Reorder TLEither to after TEither

---
 src/AST.hs | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'src/AST.hs')

diff --git a/src/AST.hs b/src/AST.hs
index b2f5ce7..ca66e87 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -55,10 +55,6 @@ data Expr x env t where
   ENothing :: x (TMaybe t) -> STy t -> Expr x env (TMaybe t)
   EJust :: x (TMaybe t) -> Expr x env t -> Expr x env (TMaybe t)
   EMaybe :: x b -> Expr x env b -> Expr x (t : env) b -> Expr x env (TMaybe t) -> Expr x env b
-  ELNil :: x (TLEither a b) -> STy a -> STy b -> Expr x env (TLEither a b)
-  ELInl :: x (TLEither a b) -> STy b -> Expr x env a -> Expr x env (TLEither a b)
-  ELInr :: x (TLEither a b) -> STy a -> Expr x env b -> Expr x env (TLEither a b)
-  ELCase :: x c -> Expr x env (TLEither a b) -> Expr x env c -> Expr x (a : env) c -> Expr x (b : env) c -> Expr x env c
 
   -- array operations
   EConstArr :: Show (ScalRep t) => x (TArr n (TScal t)) -> SNat n -> SScalTy t -> Array n (ScalRep t) -> Expr x env (TArr n (TScal t))
@@ -99,6 +95,12 @@ data Expr x env t where
   EPlus :: x t -> SMTy t -> Expr x env t -> Expr x env t -> Expr x env t
   EOneHot :: x t -> SMTy t -> SAcPrj p t a -> Expr x env (AcIdx p t) -> Expr x env a -> Expr x env t
 
+  -- interface of abstract monoidal types
+  ELNil :: x (TLEither a b) -> STy a -> STy b -> Expr x env (TLEither a b)
+  ELInl :: x (TLEither a b) -> STy b -> Expr x env a -> Expr x env (TLEither a b)
+  ELInr :: x (TLEither a b) -> STy a -> Expr x env b -> Expr x env (TLEither a b)
+  ELCase :: x c -> Expr x env (TLEither a b) -> Expr x env c -> Expr x (a : env) c -> Expr x (b : env) c -> Expr x env c
+
   -- partiality
   EError :: x a -> STy a -> String -> Expr x env a
 deriving instance (forall ty. Show (x ty)) => Show (Expr x env t)
@@ -376,11 +378,11 @@ class KnownTy t where knownTy :: STy t
 instance KnownTy TNil where knownTy = STNil
 instance (KnownTy s, KnownTy t) => KnownTy (TPair s t) where knownTy = STPair knownTy knownTy
 instance (KnownTy s, KnownTy t) => KnownTy (TEither s t) where knownTy = STEither knownTy knownTy
+instance (KnownTy s, KnownTy t) => KnownTy (TLEither s t) where knownTy = STLEither knownTy knownTy
 instance KnownTy t => KnownTy (TMaybe t) where knownTy = STMaybe knownTy
 instance (KnownNat n, KnownTy t) => KnownTy (TArr n t) where knownTy = STArr knownNat knownTy
 instance KnownScalTy t => KnownTy (TScal t) where knownTy = STScal knownScalTy
 instance KnownMTy t => KnownTy (TAccum t) where knownTy = STAccum knownMTy
-instance (KnownTy s, KnownTy t) => KnownTy (TLEither s t) where knownTy = STLEither knownTy knownTy
 
 class KnownMTy t where knownMTy :: SMTy t
 instance KnownMTy TNil where knownMTy = SMTNil
@@ -398,11 +400,11 @@ styKnown :: STy t -> Dict (KnownTy t)
 styKnown STNil = Dict
 styKnown (STPair a b) | Dict <- styKnown a, Dict <- styKnown b = Dict
 styKnown (STEither a b) | Dict <- styKnown a, Dict <- styKnown b = Dict
+styKnown (STLEither a b) | Dict <- styKnown a, Dict <- styKnown b = Dict
 styKnown (STMaybe t) | Dict <- styKnown t = Dict
 styKnown (STArr n t) | Dict <- snatKnown n, Dict <- styKnown t = Dict
 styKnown (STScal t) | Dict <- sscaltyKnown t = Dict
 styKnown (STAccum t) | Dict <- smtyKnown t = Dict
-styKnown (STLEither a b) | Dict <- styKnown a, Dict <- styKnown b = Dict
 
 smtyKnown :: SMTy t -> Dict (KnownMTy t)
 smtyKnown SMTNil = Dict
-- 
cgit v1.2.3-70-g09d2