diff options
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 49 |
1 files changed, 27 insertions, 22 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 17ee12b..f01ab9e 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -37,14 +37,9 @@ bconcat b1 BTop = b1 bconcat b1 (BPush b2 x) = BPush (bconcat b1 b2) 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 env env12 -> r) -> r -bconcat' wf b1 b2 = weakenBindings --- bconcat :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t) --- -> Bindings f env env1 -> Bindings f env env2 -> env :> env' --- -> (forall env'12. Bindings f env' env'12 -> r) -> r --- bconcat wf BTop b w k = weakenBindings wf w b $ \b' _ -> k b' --- bconcat wf (BPush b x) b2 w k = --- bconcat wf + -> 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') type family D1 t where D1 TNil = TNil @@ -73,13 +68,6 @@ type family D2E env where D2E '[] = '[] D2E (t : env) = D2 t : D2E env -data Ret env t = - forall env'. - Ret (Bindings Ex (D1E env) env') - (Ex env' (D1 t)) - (Ex (D2 t : env') (TEVM (D2E env) TNil)) -deriving instance Show (Ret env t) - d1 :: STy t -> STy (D1 t) d1 STNil = STNil d1 (STPair a b) = STPair (d1 a) (d1 b) @@ -99,6 +87,10 @@ d2 (STScal t) = case t of STBool -> STNil d2 STEVM{} = error "EVM not allowed in input program" +d2list :: SList STy env -> SList STy (D2E env) +d2list SNil = SNil +d2list (SCons x l) = SCons (d2 x) (d2list l) + conv1Idx :: Idx env t -> Idx (D1E env) (D1 t) conv1Idx IZ = IZ conv1Idx (IS i) = IS (conv1Idx i) @@ -107,15 +99,28 @@ conv2Idx :: Idx env t -> Idx (D2E env) (D2 t) conv2Idx IZ = IZ conv2Idx (IS i) = IS (conv2Idx i) -drev :: Ex env t -> Ret env t -drev = \case +data Ret env t = + forall env'. + Ret (Bindings Ex (D1E env) env') + (Ex env' (D1 t)) + (Ex (D2 t : env') (TEVM (D2E env) TNil)) +deriving instance Show (Ret env t) + +drev :: SList STy env -> Ex env t -> Ret env t +drev senv = \case EVar _ t i -> Ret BTop (EVar ext (d1 t) (conv1Idx i)) - (EMOne (conv2Idx i) (EVar ext (d2 t) IZ)) - ELet _ rhs body -> - Ret _ - _ - _ + (EMOne (d2list senv) (conv2Idx i) (EVar ext (d2 t) IZ)) + ELet _ rhs body + | Ret rhs0 rhs1 rhs2 <- drev senv rhs + , Ret body0 body1 body2 <- drev (SCons (typeOf rhs) senv) body -> + weakenBindings weakenExpr (WCopy (sinkWithBindings rhs0)) body0 $ \body0' wbody0' -> + Ret (bconcat (BPush rhs0 rhs1) body0') + (weakenExpr wbody0' body1) + (EMBind (EMScope (weakenExpr (WCopy wbody0') body2)) + (ELet ext (ESnd ext STNil (EVar ext (STPair STNil (d2 (typeOf rhs))) IZ)) $ + weakenExpr (WCopy (WSink .> WSink .> WPop (sinkWithBindings body0'))) rhs2)) + _ -> undefined where ext = Const () |