diff options
Diffstat (limited to 'src/AST/Weaken/Auto.hs')
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 82 |
1 files changed, 60 insertions, 22 deletions
diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs index 444c540..8555516 100644 --- a/src/AST/Weaken/Auto.hs +++ b/src/AST/Weaken/Auto.hs @@ -35,15 +35,29 @@ import Lemmas type family Lookup name list where Lookup name ('(name, x) : _) = x Lookup name (_ : list) = Lookup name list + Lookup name '[] = TypeError (Text "The name '" :<>: Text name :<>: Text "' does not appear in the list.") + + +-- | The @withPre@ type parameter indicates whether there can be 'LPreW' +-- occurrences within this layout. +data Layout (withPre :: Bool) (segments :: [(Symbol, [t])]) (env :: [t]) where + LSeg :: forall name segments withPre. SSymbol name -> Layout withPre segments (Lookup name segments) + -- | Pre-weaken with a weakening + LPreW :: forall name1 name2 segments. + SegmentName name1 -> SegmentName name2 + -> Lookup name1 segments :> Lookup name2 segments + -> Layout True segments (Lookup name1 segments) + (:++:) :: Layout withPre segments env1 -> Layout withPre segments env2 -> Layout withPre segments (Append env1 env2) +infixr :++: +instance (KnownSymbol name, seg ~ Lookup name segments) => IsLabel name (Layout withPre segments seg) where + fromLabel = LSeg (symbolSing @name) -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 :++: +newtype SegmentName name = SegmentName (SSymbol name) + deriving (Show) -instance (KnownSymbol name, seg ~ Lookup name segments) => IsLabel name (Layout segments seg) where - fromLabel = LSeg @name @segments +instance (KnownSymbol name, name ~ name') => IsLabel name (SegmentName name') where + fromLabel = SegmentName symbolSing data SSegments (segments :: [(Symbol, [t])]) where @@ -86,29 +100,51 @@ segmentLookup = \segs name -> case go segs name of 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) +data LinLayout (withPre :: Bool) (segments :: [(Symbol, [t])]) (env :: [t]) where + LinEnd :: LinLayout withPre segments '[] + LinApp :: SSymbol name -> LinLayout withPre segments env + -> LinLayout withPre segments (Append (Lookup name segments) env) + LinAppPreW :: SSymbol name1 -> SSymbol name2 + -> Lookup name1 segments :> Lookup name2 segments + -> LinLayout True segments env + -> LinLayout True segments (Append (Lookup name1 segments) env) -linLayoutAppend :: LinLayout segments env1 -> LinLayout segments env2 -> LinLayout segments (Append env1 env2) +linLayoutAppend :: LinLayout withPre segments env1 -> LinLayout withPre segments env2 -> LinLayout withPre segments (Append env1 env2) linLayoutAppend LinEnd lin = lin -linLayoutAppend (LinApp (name :: SSymbol name) (lin1 :: LinLayout segments env1')) (lin2 :: LinLayout _ env2) +linLayoutAppend (LinApp (name :: SSymbol name) (lin1 :: LinLayout _ segments env1')) (lin2 :: LinLayout _ _ env2) | Refl <- lemAppendAssoc @(Lookup name segments) @env1' @env2 = LinApp name (linLayoutAppend lin1 lin2) +linLayoutAppend (LinAppPreW (name1 :: SSymbol name1) name2 w (lin1 :: LinLayout _ segments env1')) (lin2 :: LinLayout _ _ env2) + | Refl <- lemAppendAssoc @(Lookup name1 segments) @env1' @env2 + = LinAppPreW name1 name2 w (linLayoutAppend lin1 lin2) -linLayoutEnv :: SSegments segments -> LinLayout segments env -> SList (Const ()) env +linLayoutEnv :: SSegments segments -> LinLayout withPre segments env -> SList (Const ()) env linLayoutEnv _ LinEnd = SNil linLayoutEnv segs (LinApp name lin) = sappend (segmentLookup segs name) (linLayoutEnv segs lin) +linLayoutEnv segs (LinAppPreW name1 _ _ lin) = sappend (segmentLookup segs name1) (linLayoutEnv segs lin) -lineariseLayout :: Layout segments env -> LinLayout segments env -lineariseLayout (LSeg @name :: Layout _ seg) +lineariseLayout :: Layout withPre segments env -> LinLayout withPre segments env +lineariseLayout (LSeg name :: Layout _ _ seg) | Refl <- lemAppendNil @seg - = LinApp (symbolSing @name) LinEnd + = LinApp name LinEnd lineariseLayout (ly1 :++: ly2) = lineariseLayout ly1 `linLayoutAppend` lineariseLayout ly2 - -pullDown :: SSegments segments -> SSymbol name -> LinLayout segments env +lineariseLayout (LPreW (SegmentName name1) (SegmentName name2) w :: Layout _ _ seg) + | Refl <- lemAppendNil @seg + = LinAppPreW name1 name2 w LinEnd + +preWeaken :: SSegments segments -> LinLayout True segments env + -> (forall env'. env :> env' -> LinLayout False segments env' -> r) -> r +preWeaken _ LinEnd k = k WId LinEnd +preWeaken segs (LinApp name lin) k = + preWeaken segs lin $ \w lin' -> + k (wCopies (segmentLookup segs name) w) (LinApp name lin') +preWeaken segs (LinAppPreW name1 name2 weak lin) k = + preWeaken segs lin $ \w lin' -> + k (WStack (segmentLookup segs name1) (segmentLookup segs name2) weak w) (LinApp name2 lin') + +pullDown :: SSegments segments -> SSymbol name -> LinLayout False segments env -> r -- Name was not found in source - -> (forall env'. LinLayout segments env' -> env :> Append (Lookup name segments) env' -> r) + -> (forall env'. LinLayout False segments env' -> env :> Append (Lookup name segments) env' -> r) -> r pullDown segs name@SSymbol linlayout kNotFound k = case linlayout of @@ -116,13 +152,13 @@ pullDown segs name@SSymbol linlayout kNotFound k = LinApp n'@SSymbol lin | Just Refl <- sameSymbol name n' -> k lin WId | otherwise -> - pullDown segs name lin kNotFound $ \(lin' :: LinLayout _ env') w -> + pullDown segs name lin kNotFound $ \(lin' :: LinLayout _ _ env') w -> k (LinApp n' lin') (WSwap @env' (segmentLookup segs n') (segmentLookup segs name) .> wCopies (segmentLookup segs n') w) sortLinLayouts :: forall segments env1 env2. SSegments segments - -> LinLayout segments env1 -> LinLayout segments env2 -> env1 :> env2 + -> LinLayout False segments env1 -> LinLayout False 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) @@ -139,5 +175,7 @@ sortLinLayouts segs LinEnd lin2@LinApp{} = WClosed (linLayoutEnv segs lin2) sortLinLayouts _ LinApp{} LinEnd = error "Segments in source that do not occur in target" 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) + SSegments segments -> Layout True segments env1 -> Layout False segments env2 -> env1 :> env2 +autoWeak segs ly1 ly2 = + preWeaken segs (lineariseLayout ly1) $ \wPreweak lin1 -> + sortLinLayouts segs lin1 (lineariseLayout ly2) .> wPreweak |