diff options
Diffstat (limited to 'src/AST/Count.hs')
| -rw-r--r-- | src/AST/Count.hs | 68 |
1 files changed, 50 insertions, 18 deletions
diff --git a/src/AST/Count.hs b/src/AST/Count.hs index bec5a9d..cb363a3 100644 --- a/src/AST/Count.hs +++ b/src/AST/Count.hs @@ -356,7 +356,14 @@ pruneExpr env ex = occCountX SsFull ex $ \_ mkex -> mkex (fullOccEnv env) fullOccEnv SNil = OccEnd fullOccEnv (_ `SCons` e) = OccPush (fullOccEnv e) () SsFull --- * s: how much of the result is required +-- In one traversal, count occurrences of variables and determine what parts of +-- expressions are actually used. These two results are computed independently: +-- even if (almost) nothing of a particular term is actually used, variable +-- references in that term still count as usual. +-- +-- In @occCountX s t k@: +-- * s: how much of the result of this term is required +-- * t: the term to analyse -- * k: is passed the actual environment usage of this expression, including -- occurrence counts. The callback reconstructs a new expression in an -- updated "response" environment. The response must be at least as large as @@ -434,8 +441,7 @@ occCountX initialS topexpr k = case topexpr of occEnvPop' env1' $ \env1 s1 -> occEnvPop' env2' $ \env2 s2 -> occCountX (SsEither s1 s2) e $ \env0 mke -> - withSome (Some env1 <||> Some env2) $ \env12 -> - withSome (Some env12 <> Some env0) $ \env -> + withSome (Some env0 <> (Some env1 <||> Some env2)) $ \env -> k env $ \env' -> ECase ext (mke env') (mka (OccPush env' () s1)) (mkb (OccPush env' () s2)) ENothing _ t -> @@ -459,8 +465,7 @@ occCountX initialS topexpr k = case topexpr of occCountX s b $ \env2' mkb -> occEnvPop' env2' $ \env2 s2 -> occCountX (SsMaybe s2) e $ \env0 mke -> - withSome (Some env1 <||> Some env2) $ \env12 -> - withSome (Some env12 <> Some env0) $ \env -> + withSome (Some env0 <> (Some env1 <||> Some env2)) $ \env -> k env $ \env' -> EMaybe ext (mka env') (mkb (OccPush env' () s2)) (mke env') ELNil _ t1 t2 -> @@ -497,9 +502,7 @@ occCountX initialS topexpr k = case topexpr of occEnvPop' env2' $ \env2 s1 -> occEnvPop' env3' $ \env3 s2 -> occCountX (SsLEither s1 s2) e $ \env0 mke -> - withSome (Some env1 <||> Some env2) $ \env12 -> - withSome (Some env12 <||> Some env3) $ \env123 -> - withSome (Some env123 <> Some env0) $ \env -> + withSome (Some env0 <> (Some env1 <||> Some env2 <||> Some env3)) $ \env -> k env $ \env' -> ELCase ext (mke env') (mka env') (mkb (OccPush env' () s1)) (mkc (OccPush env' () s2)) @@ -550,16 +553,11 @@ occCountX initialS topexpr k = case topexpr of occCountX (SsArr sElt) c $ \env3 mkc -> withSome (Some env1 <> Some env2 <> Some env3) $ \env -> k env $ \env' -> - let expr = EFold1Inner ext commut - (projectSmallerSubstruc SsFull sElt $ - mka (OccPush (OccPush env' () sElt) () sElt)) - (mkb env') (mkc env') in - case s of - SsNone -> use expr $ ENil ext - SsArr s' -> projectSmallerSubstruc (SsArr sElt) (SsArr s') expr - SsFull -> case testEquality sElt SsFull of - Just Refl -> expr - Nothing -> error "unreachable" + projectSmallerSubstruc (SsArr sElt) s $ + EFold1Inner ext commut + (projectSmallerSubstruc SsFull sElt $ + mka (OccPush (OccPush env' () sElt) () sElt)) + (mkb env') (mkc env') ESum1Inner _ e -> handleReduction (ESum1Inner ext) e @@ -594,6 +592,40 @@ occCountX initialS topexpr k = case topexpr of EMaximum1Inner _ e -> handleReduction (EMaximum1Inner ext) e EMinimum1Inner _ e -> handleReduction (EMinimum1Inner ext) e + EFold1InnerD1 _ cm a b c -> + -- TODO: currently maximally pessimistic on usage here; in particular, + -- usage tracking of the 'tape' stores can be improved + occCountX SsFull a $ \env1_2' mka -> + withSome (scaleMany (Some env1_2')) $ \env1_2 -> + occEnvPop' env1_2 $ \env1_1 _ -> + occEnvPop' env1_1 $ \env1 _ -> + occCountX SsFull b $ \env2 mkb -> + occCountX SsFull c $ \env3 mkc -> + withSome (Some env1 <> Some env2 <> Some env3) $ \env -> + k env $ \env' -> + projectSmallerSubstruc SsFull s $ + EFold1InnerD1 ext cm (mka (OccPush (OccPush env' () SsFull) () SsFull)) + (mkb env') (mkc env') + + EFold1InnerD2 _ cm t2 ef ep ezi ebog ed -> + -- TODO: currently very pessimistic on usage here, can at the very least improve tape usage + occCountX SsFull ef $ \env1_4' mkef -> + withSome (scaleMany (Some env1_4')) $ \env1_4 -> + occEnvPop' env1_4 $ \env1_3 _ -> + occEnvPop' env1_3 $ \env1_2 _ -> + occEnvPop' env1_2 $ \env1_1 _ -> + occEnvPop' env1_1 $ \env1 sTape -> + occCountX SsFull ep $ \env2 mkep -> + occCountX SsFull ezi $ \env3 mkezi -> + occCountX (SsArr (SsPair SsFull sTape)) ebog $ \env4 mkebog -> + occCountX SsFull ed $ \env5 mked -> + withSome (Some env1 <> Some env2 <> Some env3 <> Some env4 <> Some env5) $ \env -> + k env $ \env' -> + projectSmallerSubstruc SsFull s $ + EFold1InnerD2 ext cm t2 + (mkef (OccPush (OccPush (OccPush (OccPush env' () sTape) () SsFull) () SsFull) () SsFull)) + (mkep env') (mkezi env') (mkebog env') (mked env') + EConst _ t x -> k OccEnd $ \_ -> case s of |