diff options
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 61 |
1 files changed, 1 insertions, 60 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 12d28e2..bcc1485 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -34,6 +34,7 @@ import GHC.Stack (HasCallStack) import GHC.TypeLits (Symbol) import AST +import AST.Bindings import AST.Count import AST.Env import AST.Weaken.Auto @@ -42,66 +43,10 @@ import Data import Lemmas --- binding lists: a let stack without a body. The stack lives in 'env' and defines 'binds'. -data Bindings f env binds where - BTop :: Bindings f env '[] - BPush :: Bindings f env binds -> (STy t, f (Append binds env) t) -> Bindings f env (t : binds) -deriving instance (forall e t. Show (f e t)) => Show (Bindings f env env') -infixl `BPush` - -mapBindings :: (forall env' t'. f env' t' -> g env' t') - -> Bindings f env binds -> Bindings g env binds -mapBindings _ BTop = BTop -mapBindings f (BPush b (t, e)) = BPush (mapBindings f b) (t, f e) - -weakenBindings :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t) - -> env1 :> env2 - -> Bindings f env1 binds - -> (Bindings f env2 binds, Append binds env1 :> Append binds env2) -weakenBindings _ w BTop = (BTop, w) -weakenBindings wf w (BPush b (t, x)) = - let (b', w') = weakenBindings wf w b - in (BPush b' (t, wf w' x), WCopy w') - -weakenOver :: SList STy ts -> env :> env' -> Append ts env :> Append ts env' -weakenOver SNil w = w -weakenOver (SCons _ ts) w = WCopy (weakenOver ts w) - -sinkWithBindings :: Bindings f env binds -> env' :> Append binds env' -sinkWithBindings BTop = WId -sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b - -bconcat :: forall f env binds1 binds2. Bindings f env binds1 -> Bindings f (Append binds1 env) binds2 -> Bindings f env (Append binds2 binds1) -bconcat b1 BTop = b1 -bconcat b1 (BPush (b2 :: Bindings _ (Append binds1 env) binds2C) (t, x)) - | Refl <- lemAppendAssoc @binds2C @binds1 @env - = BPush (bconcat b1 b2) (t, x) - --- bconcat' :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t) --- -> Bindings f env env1 -> Bindings f env env2 --- -> (forall env12. Bindings f env env12 -> r) -> r --- bconcat' wf b1 b2 k = weakenBindings wf (sinkWithBindings b1) b2 $ \b2' _ -> k (bconcat b1 b2') - --- bsnoc :: (forall env1 env2 t'. env1 :> env2 -> f env1 t' -> f env2 t') --- -> STy t -> f env t -> Bindings f env binds -> (Bindings f env (Snoc binds t), Append binds env :> Append (Snoc binds t) env) --- bsnoc _ t x BTop = (BPush BTop (t, x), WSink) --- bsnoc wf t x (BPush b (t', y)) = --- let (b', w) = bsnoc wf t x b --- in (BPush b' (t', wf w y), WCopy w) - type family Tape binds where Tape '[] = TNil Tape (t : ts) = TPair t (Tape ts) --- data TupBinds f env binds = --- TupBinds (SList STy binds) --- (forall env2. Append binds env :> env2 -> Ex env2 (Tape binds)) --- (forall env2. Idx env2 (Tape binds) -> Bindings f env2 binds) - -bindingsBinds :: Bindings f env binds -> SList STy binds -bindingsBinds BTop = SNil -bindingsBinds (BPush binds (t, _)) = SCons t (bindingsBinds binds) - tapeTy :: SList STy binds -> STy (Tape binds) tapeTy SNil = STNil tapeTy (SCons t ts) = STPair t (tapeTy ts) @@ -240,10 +185,6 @@ reconstructBindings binds tape = (bconcat (mapBindings fromUnfExpr unf) build) ,sreverse (stapeUnfoldings binds)) -letBinds :: Bindings Ex env binds -> Ex (Append binds env) t -> Ex env t -letBinds BTop = id -letBinds (BPush b (_, rhs)) = letBinds b . ELet ext rhs - type family Vectorise n list where Vectorise _ '[] = '[] Vectorise n (t : ts) = TArr n t : Vectorise n ts |