From 3698d4d3a309d34dc154a90f9f09b9893bf22013 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Thu, 23 Oct 2025 23:50:17 +0200 Subject: Helper functions bpush and weakenBindingsE --- src/AST/Bindings.hs | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/AST/Bindings.hs') diff --git a/src/AST/Bindings.hs b/src/AST/Bindings.hs index 2310f4b..463586a 100644 --- a/src/AST/Bindings.hs +++ b/src/AST/Bindings.hs @@ -28,6 +28,10 @@ data Bindings f env binds where deriving instance (forall e t. Show (f e t)) => Show (Bindings f env env') infixl `BPush` +bpush :: Bindings (Expr x) env binds -> Expr x (Append binds env) t -> Bindings (Expr x) env (t : binds) +bpush b e = b `BPush` (typeOf e, e) +infixl `bpush` + mapBindings :: (forall env' t'. f env' t' -> g env' t') -> Bindings f env binds -> Bindings g env binds mapBindings _ BTop = BTop @@ -42,6 +46,11 @@ weakenBindings wf w (BPush b (t, x)) = let (b', w') = weakenBindings wf w b in (BPush b' (t, wf w' x), WCopy w') +weakenBindingsE :: env1 :> env2 + -> Bindings (Expr x) env1 binds + -> (Bindings (Expr x) env2 binds, Append binds env1 :> Append binds env2) +weakenBindingsE = weakenBindings weakenExpr + weakenOver :: SList STy ts -> env :> env' -> Append ts env :> Append ts env' weakenOver SNil w = w weakenOver (SCons _ ts) w = WCopy (weakenOver ts w) -- cgit v1.2.3-70-g09d2