From 83692cf41f76272423445c9cbbad65561ee3b50c Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Fri, 8 Nov 2024 12:37:51 +0100 Subject: WIP custom derivatives --- src/AST/Weaken/Auto.hs | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'src/AST/Weaken/Auto.hs') 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. -- cgit v1.2.3-70-g09d2