Code cleanup, and OverloadedLabels for LSeg

1 files changed, 0 insertions, 129 deletions

diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
index 42cdbd5..aa88c8e 100644
--- a/src/AST/Weaken.hs
+++ b/src/AST/Weaken.hs
@@ -1,17 +1,12 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE TypeAbstractions #-}
 {-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
 {-# LANGUAGE PartialTypeSignatures #-}
@@ -25,8 +20,6 @@ module AST.Weaken (module AST.Weaken, Append) where
 import Data.Bifunctor (first)
 import Data.Functor.Const
 import Data.Kind (Type)
-import GHC.TypeLits
-import Unsafe.Coerce
 
 import Data
 import Lemmas
@@ -101,125 +94,3 @@ wCopies (SCons _ spine) w = WCopy (wCopies spine w)
 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)
-
-
-type family Lookup name list where
-  Lookup name ('(name, x) : _) = x
-  Lookup name (_ : list) = Lookup name list
-
-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 '[]
-  SSegCons :: SSymbol name -> SList (Const ()) ts -> SSegments list -> SSegments ('(name, ts) : list)
-
-class KnownSegments (segments :: [(Symbol, [t])]) where
-  knownSegments :: SSegments segments
-
-instance KnownSegments '[] where
-  knownSegments = SSegNil
-
-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
-                           Nothing -> error $ "Segment not found: " ++ fromSSymbol name
-  where
-    go :: forall segs'. SSegments segs' -> SSymbol name -> Maybe (SList (Const ()) (Lookup name segs'))
-    go SSegNil _ = Nothing
-    go (SSegCons n@(SSymbol @n) (ts :: SList _ ts) (sseg :: SSegments rest)) name@SSymbol =
-      case sameSymbol n name of
-        Just Refl ->
-          case go sseg name of
-            Nothing -> Just ts
-            Just _ -> error $ "Duplicate segment with name " ++ fromSSymbol name
-        Nothing ->
-          case unsafeCoerce Refl :: (Lookup name ('(n, ts) : rest) :~: Lookup name rest) of
-            Refl -> go sseg name
-
-data LinLayout (segments :: [(Symbol, [t])]) (env :: [t]) where
-  LinEnd :: LinLayout segments '[]
-  LinApp :: SSymbol name -> LinLayout segments env -> LinLayout segments (Append (Lookup name segments) env)
-
-linLayoutAppend :: LinLayout segments env1 -> LinLayout segments env2 -> LinLayout segments (Append env1 env2)
-linLayoutAppend LinEnd lin = lin
-linLayoutAppend (LinApp (name :: SSymbol name) (lin1 :: LinLayout segments env1')) (lin2 :: LinLayout _ env2)
-  | Refl <- lemAppendAssoc @(Lookup name segments) @env1' @env2
-  = LinApp name (linLayoutAppend lin1 lin2)
-
-lineariseLayout :: Layout segments env -> LinLayout segments env
-lineariseLayout (LSeg @name :: Layout _ seg)
-  | Refl <- lemAppendNil @seg
-  = LinApp (symbolSing @name) LinEnd
-lineariseLayout (ly1 :++: ly2) = lineariseLayout ly1 `linLayoutAppend` lineariseLayout ly2
-
-linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ()) env
-linLayoutEnv _ LinEnd = SNil
-linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin)
-
-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
-         -> (forall env'. LinLayout segments env' -> env :> Append (Lookup name segments) env' -> r)
-         -> r
-pullDown segs name@SSymbol linlayout kNotFound k =
-  case linlayout of
-    LinEnd -> kNotFound
-    LinApp n'@SSymbol lin
-      | Just Refl <- sameSymbol name n' -> k lin WId
-      | otherwise ->
-          pullDown segs name lin kNotFound $ \(lin' :: LinLayout _ env') w ->
-            k (LinApp n' lin') (WSwap (segmentLookup segs n') (segmentLookup segs name) (linLayoutEnv segs lin')
-                                  .> wCopies (segmentLookup segs n') w)
-
-sortLinLayouts :: forall segments env1 env2.
-                  SSegments segments
-               -> LinLayout segments env1 -> LinLayout segments env2 -> env1 :> env2
-sortLinLayouts _ LinEnd LinEnd = WId
-sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail2)
-  | Just Refl <- sameSymbol name1 name2 = wCopies (segmentLookup segs name1) (sortLinLayouts segs tail1 tail2)
-  | otherwise =
-      pullDown segs name2 lin1
-        (wSinks (segmentLookup segs name2) .> sortLinLayouts segs lin1 tail2)
-        (\tail1' w ->
-          -- We've pulled down name2 in lin1 so that it's at the head; the
-          -- resulting modified tail is tail1'. Thus now we have (name2 : tail1')
-          -- vs (name2 : tail2). Thus we continue sorting tail1' vs tail2, and
-          -- wCopies the name2 on top of that.
-          wCopies (segmentLookup segs name2) (sortLinLayouts segs tail1' tail2) .> w)
-sortLinLayouts _ LinEnd LinApp{} = error "Unequal number of segments: more in target than in source"
-sortLinLayouts _ LinApp{} LinEnd = error "Unequal number of segments: more in source than in target"