{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} module CHAD.Accum where import AST import CHAD.Types import Data hasArrays :: STy t' -> Bool hasArrays STNil = False hasArrays (STPair a b) = hasArrays a || hasArrays b hasArrays (STEither a b) = hasArrays a || hasArrays b hasArrays (STMaybe t) = hasArrays t hasArrays STArr{} = True hasArrays STScal{} = False hasArrays STAccum{} = error "Accumulators not allowed in source program" 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 (EZero 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))))