diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-08 12:37:51 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-08 12:37:51 +0100 |
| commit | 83692cf41f76272423445c9cbbad65561ee3b50c (patch) | |
| tree | 49f56f498a68722a7302b4ce0b41402a9b9da9ef /src/AST/Weaken/Auto.hs | |
| parent | 58d4d0b47f5e609e21132f48b727de37d06b6777 (diff) | |
WIP custom derivatives
Diffstat (limited to 'src/AST/Weaken/Auto.hs')
| -rw-r--r-- | src/AST/Weaken/Auto.hs | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/AST/Weaken/Auto.hs b/src/AST/Weaken/Auto.hs index 8555516..6752c24 100644 --- a/src/AST/Weaken/Auto.hs +++ b/src/AST/Weaken/Auto.hs @@ -118,11 +118,6 @@ linLayoutAppend (LinAppPreW (name1 :: SSymbol name1) name2 w (lin1 :: LinLayout | Refl <- lemAppendAssoc @(Lookup name1 segments) @env1' @env2 = LinAppPreW name1 name2 w (linLayoutAppend lin1 lin2) -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 withPre segments env -> LinLayout withPre segments env lineariseLayout (LSeg name :: Layout _ _ seg) | Refl <- lemAppendNil @seg @@ -171,7 +166,7 @@ sortLinLayouts segs lin1@(LinApp name1@SSymbol tail1) (LinApp name2@SSymbol tail -- 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 segs LinEnd lin2@LinApp{} = WClosed (linLayoutEnv segs lin2) +sortLinLayouts _ LinEnd LinApp{} = WClosed sortLinLayouts _ LinApp{} LinEnd = error "Segments in source that do not occur in target" autoWeak :: forall segments env1 env2. |