-- ==========================================================--
-- === Find frontiers using Hunt's algorithm. ===--
-- === Only works for functions whose result lattice ===--
-- === does not contain any function spaces ===--
-- === ("data functions"). ===--
-- === ===--
-- === FrontierDATAFN.hs ===--
-- ==========================================================--
module FrontierDATAFN2 where
import BaseDefs
import Utils
import MyUtils
import AbstractVals2
import SuccsAndPreds2
import AbstractMisc
import AbstractEval2
import AbsConc3
import FrontierMisc2
-- ==========================================================--
--
fdImprove :: (Route -> Route) -> -- coercion function
MemoList -> -- possibly useful info
[Domain] -> -- argument domains
Bool -> -- True == naive startup
[FrontierElem] -> -- max-0 superset
[FrontierElem] -> -- min-1 superset
([FrontierElem], [FrontierElem])
fdImprove coerce memo dss naive max0_super min1_super
= let
(zero_result_pairs, one_result_pairs)
= splitList (fdIsZero.coerce.second) memo
zero_nodes_max
= avMaxfrel (map (MkFrel . first) zero_result_pairs)
one_nodes_min
= avMinfrel (map (MkFrel . first) one_result_pairs)
new_max0
= (if naive then [MkFrel (map avTopR dss)] else max0_super)
`avLUBmax0frontier`
(spMax0FromMin1 dss one_nodes_min)
new_min1
= (if naive then [MkFrel (map avBottomR dss)] else min1_super)
`avGLBmin1frontier`
(spMin1FromMax0 dss zero_nodes_max)
in
(new_max0, new_min1)
-- ==========================================================--
--
fdFind :: ACMode ->
HExpr Naam -> -- tree of abstract function
Domain -> -- domain of function to be found
[Domain] -> -- small arg domains
[Domain] -> -- big arg domains
Rep -> -- bounding rep
(Route -> Route) -> -- the coercion function
Bool -> -- True == naive startup
[FrontierElem] -> -- inherited low factor's min-1-frontier
MemoList -> -- possibly useful information
(Rep, MemoList)
fdFind s_or_l hexpr (Func dss Two) small_argds big_argds
(RepTwo (Min1Max0 ar_prev min1_prev max0_prev))
coerce naive min1_ilf memo
= let
(better_max0, better_min1)
= fdImprove coerce memo small_argds naive max0_prev min1_prev
(fr, new_memo_additions)
= fdFs2 s_or_l hexpr small_argds big_argds
( {-min1_ilf `avGLBmin1frontier`-} better_min1)
better_max0 coerce
in
(RepTwo fr,
new_memo_additions)
fdFind s_or_l hexpr (Func dss (Lift1 dts)) small_argds big_argds
(Rep1 (Min1Max0 ar_prev min1_prev_lf max0_prev_lf) prev_hfs)
coerce naive min1_ilf memo
= let
(better_lf_max0, better_lf_min1)
= fdImprove (fdLo1.coerce) memo small_argds naive
max0_prev_lf min1_prev_lf
(lofact, lofact_memo_additions)
= fdFs2 s_or_l hexpr small_argds big_argds
( {-min1_ilf `avGLBmin1frontier`-} better_lf_min1)
better_lf_max0 (fdLo1.coerce)
useful_lofact_memo
= filter (not.fdIsZero.fdLo1.coerce.second)
(lofact_memo_additions ++ memo)
min1_lofact
= case lofact of {Min1Max0 lf_ar lf_f1 lf_f0 -> lf_f1}
(hifacts, hifact_memo_additions)
= fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce
useful_lofact_memo False min1_lofact naive
in
(Rep1 lofact hifacts,
lofact_memo_additions ++ hifact_memo_additions)
fdFind s_or_l hexpr (Func dss (Lift2 dts)) small_argds big_argds
(Rep2 (Min1Max0 ar_prev_lf min1_prev_lf max0_prev_lf)
(Min1Max0 ar_prev_mf min1_prev_mf max0_prev_mf) prev_hfs)
coerce naive min1_ilf memo
= let
(better_lf_max0, better_lf_min1)
= fdImprove (fdLo2.coerce) memo small_argds naive
max0_prev_lf min1_prev_lf
(lofact, lofact_memo_additions)
= fdFs2 s_or_l hexpr small_argds big_argds
( {-min1_ilf `avGLBmin1frontier`-} better_lf_min1)
better_lf_max0 (fdLo2.coerce)
useful_lofact_memo
= filter (not.fdIsZero.fdLo2.coerce.second)
(lofact_memo_additions ++ memo)
min1_lofact
= case lofact of {Min1Max0 lf_ar lf_f1 lf_f0 -> lf_f1}
(better_mf_max0, better_mf_min1)
= fdImprove (fdMid2.coerce) useful_lofact_memo small_argds naive
max0_prev_mf min1_prev_mf
(midfact, midfact_memo_additions)
= fdFs2 s_or_l hexpr small_argds big_argds
( {-min1_lofact `avGLBmin1frontier`-} better_mf_min1)
better_mf_max0 (fdMid2.coerce)
useful_midfact_memo
= filter (not.fdIsZero.fdMid2.coerce.second)
(midfact_memo_additions ++ useful_lofact_memo)
min1_midfact
= case midfact of {Min1Max0 mf_ar mf_f1 mf_f0 -> mf_f1}
(hifacts, hifact_memo_additions)
= fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce
useful_midfact_memo True min1_midfact naive
in
(Rep2 lofact midfact hifacts,
lofact_memo_additions ++
midfact_memo_additions ++ hifact_memo_additions)
-- ==========================================================--
--
fdFind_aux :: ACMode ->
[Domain] -> -- small argument domains
[Domain] -> -- big argument domains
[Domain] -> -- result domains
HExpr Naam -> -- the tree
[Rep] -> -- previous high factors
(Route -> Route) -> -- unlifted coercion function
MemoList -> -- the memo
Bool -> -- True => Lift2, False => Lift1
[FrontierElem] -> -- inherited low factor
Bool -> -- True => naive startup
([Rep], MemoList)
fdFind_aux s_or_l small_argds big_argds dts hexpr prev_hfs coerce
initial_hf_memo double_lift min1_ilf naive
= let
high_coerce
= if double_lift then fdHi2 else fdHi1
small_hifact_domains
= map (avUncurry small_argds) dts
hifact_info_tuples
= myZipWith4 mkTuple (0 `myIntsFromTo` (length dts - 1))
prev_hfs (map avBottomR dts) small_hifact_domains
mkTuple n hf_prev bottom small_hf_domain
= (small_hf_domain, (high_coerce bottom n . coerce), hf_prev)
(hf_memo_additions, hifacts)
= mapAccuml doOne [] hifact_info_tuples
doOne memo_adds_so_far (hf_dom, hf_coerce, hf_preev)
= let (rep, more_memo_additions)
= fdFind s_or_l hexpr hf_dom small_argds big_argds
hf_preev hf_coerce naive min1_ilf
(memo_adds_so_far ++ initial_hf_memo)
in (more_memo_additions ++ memo_adds_so_far, rep)
in
(hifacts, hf_memo_additions)
-- ==========================================================--
--
fdIdent :: Route -> Route
fdIdent p = p
fdLo1 :: Route -> Route
fdLo1 Stop1 = Zero
fdLo1 (Up1 rs) = One
fdHi1 :: Route -> Int -> Route -> Route
fdHi1 bottom n Stop1 = bottom
fdHi1 bottom n (Up1 rs) = rs ## n
fdLo2 :: Route -> Route
fdLo2 Stop2 = Zero
fdLo2 Up2 = One
fdLo2 (UpUp2 rs) = One
fdMid2 :: Route -> Route
fdMid2 Stop2 = Zero
fdMid2 Up2 = Zero
fdMid2 (UpUp2 rs) = One
fdHi2 :: Route -> Int -> Route -> Route
fdHi2 bottom n Stop2 = bottom
fdHi2 bottom n Up2 = bottom
fdHi2 bottom n (UpUp2 rs) = rs ## n
fdIsZero :: Route -> Bool
fdIsZero x = case x of {Zero -> True; One -> False}
-- ==========================================================--
--
fdFs2 :: ACMode ->
HExpr Naam -> -- the tree
[Domain] -> -- small arg domains
[Domain] -> -- big arg domains
[FrontierElem] -> -- min-1 superset (inherited low factor)
[FrontierElem] -> -- max-0 superset (previous value)
(Route -> Route) -> -- the coercion function
(Frontier, MemoList)
fdFs2 s_or_l hexpr small_argds big_argds min1_prev max0_prev coerce
= let initial_yy
= max0_prev
initial_xx
= min1_prev
(final_yy, final_xx, finalMemo)
= fdFs_aux s_or_l hexpr small_argds big_argds coerce
initial_yy initial_xx True [] (utRandomInts 1 2)
result
= Min1Max0 (length small_argds) final_xx final_yy
in
--if not (sane result small_argds)
--then panic (show (min1_prev, max0_prev,
-- fmSelect 2 initial_xx initial_yy False)) else
(result, finalMemo)
--sane (Min1Max0 ar f1 f0) dss
-- = f1 == spMin1FromMax0 dss f0 &&
-- f0 == spMax0FromMin1 dss f1
-- ==========================================================--
--
fdFs_aux :: ACMode ->
HExpr Naam -> -- the tree
[Domain] -> -- small argument domains
[Domain] -> -- big argument domains
(Route -> Route) -> -- the coercion function
[FrontierElem] -> -- tentative max-0 frontier
[FrontierElem] -> -- tentative min-1 frontier
Bool -> -- True == take from top
MemoList -> -- memo list so far
[Int] ->
([FrontierElem], [FrontierElem], MemoList)
fdFs_aux s_or_l hexpr small_argds big_argds
coerce trial_max_yy trial_min_xx fromTop memo rands
= let edgez
= fmSelect (head rands) trial_min_xx trial_max_yy fromTop
Just (MkFrel args)
= edgez
args_at_proper_sizes
= myZipWith3 (acConc s_or_l) big_argds small_argds args
evald_app
= aeEvalExact hexpr (map HPoint args_at_proper_sizes)
coerced_evald_app
= coerce evald_app
revised_max_yy
= fmReviseMaxYY small_argds trial_max_yy (MkFrel args)
revised_min_xx
= fmReviseMinXX small_argds trial_min_xx (MkFrel args)
new_memo
= (args, evald_app) : memo
in
if fmIsNothing edgez
then (sort trial_max_yy, sort trial_min_xx, memo)
else
if coerced_evald_app == One
then fdFs_aux s_or_l
hexpr small_argds big_argds coerce
revised_max_yy trial_min_xx False new_memo (tail rands)
else
if coerced_evald_app == Zero
then fdFs_aux s_or_l
hexpr small_argds big_argds coerce
trial_max_yy revised_min_xx True new_memo (tail rands)
else panic "fdFs_aux"
-- ==========================================================--
-- === end FrontierDATAFN.hs ===--
-- ==========================================================--
|
