Autoweak!

1 files changed, 30 insertions, 21 deletions

diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index 6c66b07..42cdbd5 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
@@ -97,24 +98,6 @@ wCopies :: SList f bs -> env1 :> env2 -> Append bs env1 :> Append bs env2
 wCopies SNil w = w
 wCopies (SCons _ spine) w = WCopy (wCopies spine w)
 
-wStack :: forall env b1 b2. b1 :> b2 -> Append b1 env :> Append b2 env
-wStack WId = WId
-wStack WSink = WSink
-wStack (WCopy w) = WCopy (wStack @env w)
-wStack (WPop w) = WPop (wStack @env w)
-wStack (WThen w1 w2) = WThen (wStack @env w1) (wStack @env w2)
-wStack (WClosed s) = wSinks s
-wStack (WIdx i) = WIdx (goIdx i)
-  where
-    goIdx :: Idx b t -> Idx (Append b env) t
-    goIdx IZ = IZ
-    goIdx (IS i') = IS (goIdx i')
-wStack (WPick @t @_ @env1 @env2 (pre :: SList (Const ()) pre) w)
-  | Refl <- lemAppendAssoc @pre @env2 @env
-  , Refl <- lemAppendAssoc @pre @(t : env1) @env
-  = WPick @t @_ pre (wStack @env w)
-wStack WSwap{} = error "OOPS"
-
 wRaiseAbove :: SList f env1 -> SList g env -> env1 :> Append env1 env
 wRaiseAbove SNil env = WClosed (slistMap (\_ -> Const ()) env)
 wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env)
@@ -127,6 +110,7 @@ type family Lookup name list where
 data Layout (segments :: [(Symbol, [t])]) (env :: [t]) where
   LSeg :: forall name segments. KnownSymbol name => Layout segments (Lookup name segments)
   (:++:) :: Layout segments env1 -> Layout segments env2 -> Layout segments (Append env1 env2)
+infixr :++:
 
 data SSegments (segments :: [(Symbol, [t])]) where
   SSegNil :: SSegments '[]
@@ -142,6 +126,31 @@ instance (KnownSymbol name, KnownListSpine ts, KnownSegments list)
       => KnownSegments ('(name, ts) : list) where
   knownSegments = SSegCons symbolSing knownListSpine knownSegments
 
+class ToSegments k a | a -> k where
+  type SegmentsOf k a :: [(Symbol, [k])]
+  toSegments :: a -> SSegments (SegmentsOf k a)
+
+instance ToSegments k (SSegments (segments :: [(Symbol, [k])])) where
+  type SegmentsOf k (SSegments segments) = segments
+  toSegments = id
+
+data GivenSegment name ts = forall f. KnownSymbol name => Seg (SList f ts)
+                          | (KnownSymbol name, KnownListSpine ts) => Seg'
+
+instance ToSegments k (GivenSegment name (ts :: [k])) where
+  type SegmentsOf k (GivenSegment name (ts :: [k])) = '[ '(name, ts)]
+  toSegments (Seg list) = SSegCons symbolSing (slistMap (\_ -> Const ()) list) SSegNil
+  toSegments Seg' = SSegCons symbolSing knownListSpine SSegNil
+
+infixr $..
+($..) :: (ToSegments k a, ToSegments k b) => a -> b -> SSegments (Append (SegmentsOf k a) (SegmentsOf k b))
+x $.. y = ssegmentsAppend (toSegments x) (toSegments y)
+  where
+    ssegmentsAppend :: SSegments a -> SSegments b -> SSegments (Append a b)
+    ssegmentsAppend SSegNil l2 = l2
+    ssegmentsAppend (SSegCons name list l1) l2 = SSegCons name list (ssegmentsAppend l1 l2)
+
+-- | If the found segment is a TopSeg, returns Nothing.
 segmentLookup :: forall segments name. SSegments segments -> SSymbol name -> SList (Const ()) (Lookup name segments)
 segmentLookup = \segs name -> case go segs name of
                            Just ts -> ts
@@ -179,9 +188,9 @@ linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ())
 linLayoutEnv _ LinEnd = SNil
 linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin)
 
-autoWeak :: forall segments env1 env2. KnownSegments segments
-         => Layout segments env1 -> Layout segments env2 -> env1 :> env2
-autoWeak ly1 ly2 = sortLinLayouts knownSegments (lineariseLayout ly1) (lineariseLayout ly2)
+autoWeak :: forall segments env1 env2.
+            SSegments segments -> Layout segments env1 -> Layout segments env2 -> env1 :> env2
+autoWeak segs ly1 ly2 = sortLinLayouts segs (lineariseLayout ly1) (lineariseLayout ly2)
 
 pullDown :: SSegments segments -> SSymbol name -> LinLayout segments env
          -> r  -- Name was not found in source