blob: b61b5ffc3c893f3c5870858bac92e2b0744ec494 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
module CHAD.Accum where
import AST
import CHAD.Types
import Data
makeAccumulators :: SList STy envPro -> Ex (Append (D2AcE envPro) env) t -> Ex env (InvTup t (D2E envPro))
makeAccumulators SNil e = e
makeAccumulators (t `SCons` envpro) e =
makeAccumulators envpro $
EWith ext t (EZero ext t) e
uninvertTup :: SList STy list -> STy core -> Ex env (InvTup core list) -> Ex env (TPair core (Tup list))
uninvertTup SNil _ e = EPair ext e (ENil ext)
uninvertTup (t `SCons` list) tcore e =
ELet ext (uninvertTup list (STPair tcore t) e) $
let recT = STPair (STPair tcore t) (tTup list) -- type of the RHS of that let binding
in EPair ext
(EFst ext (EFst ext (EVar ext recT IZ)))
(EPair ext
(ESnd ext (EVar ext recT IZ))
(ESnd ext (EFst ext (EVar ext recT IZ))))
|
