-- ==========================================================--
-- === Concretisation of function points. ===--
-- === AbsConc3.hs ===--
-- ==========================================================--
module AbsConc3 where
import BaseDefs
import Utils
import MyUtils
import AbstractVals2
import SuccsAndPreds2
import AbstractMisc
import DomainExpr
-- ==========================================================--
--
acUncurryWRT :: Domain -> Domain -> Domain
-- small big
--
acUncurryWRT Two anyThing
= anyThing
acUncurryWRT (Lift1 ds1) (Lift1 ds2)
= Lift1 (myZipWith2 acUncurryWRT ds1 ds2)
acUncurryWRT (Lift2 ds1) (Lift2 ds2)
= Lift2 (myZipWith2 acUncurryWRT ds1 ds2)
acUncurryWRT (Func ds_s dt_s) (Func ds_b dt_b)
= let small_arity = length ds_s
big_arity = length ds_b
fixed_at_outer_level
= if small_arity == big_arity
then Func ds_b dt_b
else
if small_arity < big_arity
then Func (take small_arity ds_b)
(Func (drop small_arity ds_b) dt_b)
else panic "acUncurryWRT"
totally_fixed
= case fixed_at_outer_level of
Func ds_ol dt_ol
-> Func (myZipWith2 acUncurryWRT ds_s ds_ol)
(acUncurryWRT dt_s dt_ol)
in
totally_fixed
-- ==========================================================--
--
acNormAndCurried :: Domain -> Domain -> (Domain, Domain)
acNormAndCurried small_d big_d
= let big_d_u = amStrongNormalise big_d
in (big_d_u, acUncurryWRT small_d big_d_u)
-- ==========================================================--
-- big domain smaller domain
acCompatible :: Domain -> Domain -> Bool
--
-- In the (DFunc _ _) (DFunc _ _) case, note that
-- the big domain is
-- assumed to be curried, so its apparent arity is
-- the same as that of the small domain.
--
acCompatible _ Two
= True
acCompatible (Lift1 ds1) (Lift1 ds2)
= myAndWith2 acCompatible ds1 ds2
acCompatible (Lift2 ds1) (Lift2 ds2)
= myAndWith2 acCompatible ds1 ds2
acCompatible (Func big_ss big_t) (Func smaller_ss smaller_t)
= acCompatible big_t smaller_t &&
myAndWith2 acCompatible big_ss smaller_ss
acCompatible _ _
= False
-- ==========================================================--
--
acConc :: ACMode -> Domain -> Domain -> Route -> Route
acConc s_or_l big_d small_d small_r
= let isFn = case small_d of { Func _ _ -> True; _ -> False }
(big_d_u, big_d_c)
= if isFn then acNormAndCurried small_d big_d else (big_d, big_d)
isOk = acCompatible big_d_c small_d
small_rep = case small_r of Rep rep -> rep
in
if big_d == small_d
then small_r
else
if not isOk
then panic "acConc: incompatible domains\n\n"
else
if isFn
then Rep (acConcRep s_or_l big_d_c big_d_u small_d small_rep)
else acConcData s_or_l big_d_u small_d small_r
-- ==========================================================--
-- big small
--
acConcData :: ACMode -> Domain -> Domain -> Route -> Route
acConcData s_or_l db Two One
= avTopR db
acConcData s_or_l db Two Zero
= avBottomR db
acConcData s_or_l (Lift1 dbs) (Lift1 dss) Stop1
= Stop1
acConcData s_or_l (Lift1 dbs) (Lift1 dss) (Up1 rs)
= Up1 (myZipWith3 (acConc s_or_l) dbs dss rs)
acConcData s_or_l (Lift2 dbs) (Lift2 dss) Stop2
= Stop2
acConcData s_or_l (Lift2 dbs) (Lift2 dss) Up2
= Up2
acConcData s_or_l (Lift2 dbs) (Lift2 dss) (UpUp2 rs)
= UpUp2 (myZipWith3 (acConc s_or_l) dbs dss rs)
-- ==========================================================--
-- big_c big_u small
acConcRep :: ACMode -> Domain -> Domain -> Domain -> Rep -> Rep
acConcRep s_or_l big_d_c@(Func dss_b_c dt_b_c)
big_d_u@(Func dss_b_u dt_b_u)
small_d@(Func dss_s_c dt_s_c)
rep
= let concd_source
= acConcSource s_or_l big_d_u small_d rep
concd_source_d
= amStrongNormalise (acConcSourceD big_d_c small_d)
concd_all
= acConcTarget s_or_l dt_b_c concd_source_d concd_source
in
concd_all
-- ==========================================================--
-- Concretise target domain of a function.
-- target_big rep_current
acConcTarget :: ACMode -> Domain -> Domain -> Rep -> Rep
-- target_big may be a function space, derived from
-- *curried* final desired domain.
--
acConcTarget
s_or_l
Two
c@(Func dsc Two)
f@(RepTwo _)
= f
acConcTarget
s_or_l
(Lift1 dts)
c@(Func dsc Two)
f@(RepTwo fr)
= let doOne dt = acConcTarget s_or_l dt c f
in
Rep1 fr (map doOne dts)
acConcTarget
s_or_l
(Lift2 dts)
c@(Func dsc Two)
f@(RepTwo fr)
= let doOne dt = acConcTarget s_or_l dt c f
in
Rep2 fr fr (map doOne dts)
acConcTarget
s_or_l
(Func es g)
c@(Func dsc Two)
f@(RepTwo fr)
= let arity_increase = length es
new_c = Func (dsc++es) Two
increased_arity
= case s_or_l of
Safe -> ac_increase_arity_safe arity_increase dsc es fr
Live -> ac_increase_arity_live arity_increase dsc es fr
in
acConcTarget s_or_l g new_c increased_arity
acConcTarget
s_or_l
(Lift1 dts_b)
c@(Func dss (Lift1 dts_s))
f@(Rep1 lf hfs)
= let hfds_small = map (avUncurry dss) dts_s
hfds_big = map (avUncurry dss) dts_b
hfds_targ = myZipWith2 doOne hfds_small hfds_big
doOne (Func xxss_s xxt_s) (Func xxss_b xxt_b)
= let xxss_fin = drop (length xxss_s) xxss_b
in
if null xxss_fin
then xxt_b
else Func xxss_fin xxt_b
hfs_big = myZipWith3 (acConcTarget s_or_l) hfds_targ hfds_small hfs
in
Rep1 lf hfs_big
acConcTarget
s_or_l
(Lift2 dts_b)
c@(Func dss (Lift2 dts_s))
f@(Rep2 lf mf hfs)
= let hfds_small = map (avUncurry dss) dts_s
hfds_big = map (avUncurry dss) dts_b
hfds_targ = myZipWith2 doOne hfds_small hfds_big
doOne (Func xxss_s xxt_s) (Func xxss_b xxt_b)
= let xxss_fin = drop (length xxss_s) xxss_b
in
if null xxss_fin
then xxt_b
else Func xxss_fin xxt_b
hfs_big = myZipWith3 (acConcTarget s_or_l) hfds_targ hfds_small hfs
in
Rep2 lf mf hfs_big
-- ==========================================================--
--
ac_increase_arity_safe :: Int -> -- arity increase
[Domain] -> -- existing arg domains
[Domain] -> -- new arg domains
Frontier -> -- the function
Rep
ac_increase_arity_safe arity_increase argds new_argds fr
= let special_case = avIsBottomRep (RepTwo fr)
final_argds = argds ++ new_argds
new_bottoms = map avBottomR new_argds
special_fix = avBottomR_aux (Func final_argds Two)
in
if special_case
then special_fix
else ac_ia_aux Safe arity_increase new_bottoms final_argds fr
-- ==========================================================--
--
ac_increase_arity_live :: Int -> -- arity increase
[Domain] -> -- existing arg domains
[Domain] -> -- new arg domains
Frontier -> -- the function
Rep
ac_increase_arity_live arity_increase argds new_argds fr
= let special_case = avIsTopRep (RepTwo fr)
final_argds = argds ++ new_argds
new_tops = map avTopR new_argds
special_fix = avTopR_aux (Func final_argds Two)
in
if special_case
then special_fix
else ac_ia_aux Live arity_increase new_tops final_argds fr
-- ==========================================================--
--
ac_ia_aux :: ACMode -> -- mode
Int -> -- arity increase
[Route] -> -- top/bottom routes for new args
[Domain] -> -- arg domains **after** arity increase
Frontier -> -- the function
Rep
ac_ia_aux
s_or_l
ai
new_points
final_argds
(Min1Max0 ar f1 f0)
= let (new_f1, new_f0) = ac_extend_fr s_or_l final_argds f1 f0 new_points
in
RepTwo (Min1Max0 (ar+ai) new_f1 new_f0)
-- ==========================================================--
--
ac_extend_fr :: ACMode ->
[Domain] ->
[FrontierElem] ->
[FrontierElem] ->
[Route] ->
([FrontierElem], [FrontierElem])
ac_extend_fr s_or_l final_argds f1 f0 new_points
= let new_f0_safe = [MkFrel (frel++new_points) | MkFrel frel <- f0]
new_f1_safe = spMin1FromMax0 final_argds new_f0_safe
new_f1_live = [MkFrel (frel++new_points) | MkFrel frel <- f1]
new_f0_live = spMax0FromMin1 final_argds new_f1_live
in
case s_or_l of
Safe -> (new_f1_safe, new_f0_safe)
Live -> (new_f1_live, new_f0_live)
-- ==========================================================--
-- big_args small_args
acConcSource_aux :: ACMode -> [Domain] -> [Domain] -> Frontier -> Frontier
acConcSource_aux Safe dbs dss (Min1Max0 ar f1 f0)
= let dbs_used = take ar dbs
new_f0 = map ( \(MkFrel pts) ->
MkFrel (myZipWith3 (acConc Safe) dbs_used dss pts)) f0
new_f1 = spMin1FromMax0 dbs_used new_f0
in
Min1Max0 ar new_f1 new_f0
acConcSource_aux Live dbs dss (Min1Max0 ar f1 f0)
= let dbs_used = take ar dbs
new_f1 = map ( \(MkFrel pts) ->
MkFrel (myZipWith3 (acConc Live) dbs_used dss pts)) f1
new_f0 = spMax0FromMin1 dbs_used new_f1
in
Min1Max0 ar new_f1 new_f0
-- ==========================================================--
-- Concretise source domain of a function
-- big small
acConcSource :: ACMode -> Domain -> Domain -> Rep -> Rep
--
-- we pass in the *entire* desired final domain of the
-- function, in *curried* form. This is preserved by
-- subsequent calls. In general
-- there may be more "dss" than components of each frontier
-- point. This is OK: only as many "dss" as are relevant
-- are actually concretised. "acConcTarget"
-- sticks on those "dss" components ignored here.
--
acConcSource s_or_l (Func dss_b dt_b)
(Func dss_s Two)
(RepTwo fr)
= RepTwo (acConcSource_aux s_or_l dss_b dss_s fr)
acConcSource s_or_l (Func dss_b (Lift1 dts_b))
(Func dss_s (Lift1 dts_s))
(Rep1 lf hfs)
= let new_lf = acConcSource_aux s_or_l dss_b dss_s lf
hf_big_domains = map (avUncurry dss_b) dts_b
hf_small_domains = map (avUncurry dss_s) dts_s
new_hfs
= myZipWith3 (acConcSource s_or_l) hf_big_domains hf_small_domains hfs
in
Rep1 new_lf new_hfs
acConcSource s_or_l (Func dss_b (Lift2 dts_b))
(Func dss_s (Lift2 dts_s))
(Rep2 lf mf hfs)
= let new_lf = acConcSource_aux s_or_l dss_b dss_s lf
new_mf = acConcSource_aux s_or_l dss_b dss_s mf
hf_big_domains = map (avUncurry dss_b) dts_b
hf_small_domains = map (avUncurry dss_s) dts_s
new_hfs
= myZipWith3 (acConcSource s_or_l) hf_big_domains hf_small_domains hfs
in
Rep2 new_lf new_mf new_hfs
-- ==========================================================--
-- Figure out the domain of the thing created by acConcSource.
-- big small
acConcSourceD :: Domain -> Domain -> Domain
acConcSourceD (Func dss_b dt_b) (Func dss_s Two)
= Func dss_b Two
acConcSourceD (Func dss_b (Lift1 dts_b)) (Func dss_s (Lift1 dts_s))
= let low_fac_arity = length dss_s
hf_big_ds = map (avUncurry dss_b) dts_s {- XXXXXX -}
hf_small_ds = map (avUncurry dss_s) dts_s
hf_resultants = myZipWith2 acConcSourceD hf_big_ds hf_small_ds
hf_res2 = map drop_lf_ar hf_resultants
drop_lf_ar (Func ess et)
= let ess2 = drop low_fac_arity ess
in if null ess2
then et
else Func ess2 et
in
Func dss_b (Lift1 hf_res2)
acConcSourceD (Func dss_b (Lift2 dts_b)) (Func dss_s (Lift2 dts_s))
= case
acConcSourceD (Func dss_b (Lift1 dts_b)) (Func dss_s (Lift1 dts_s))
of
Func dss_res (Lift1 dts_res) -> Func dss_res (Lift2 dts_res)
-- ==========================================================--
--
acMakeInstance :: ACMode -> -- should be Safe for real applications
DExpr -> -- simplest instance domain of point (DXFunc _ _)
DSubst -> -- binds domain vars to required instances
Route -> -- simplest instance of function
Route -- function at desired instance
{- Constraints, assumptions, &c.
1. The domain variables in the DExpr correspond exactly with
those supplied in the DSubst.
2. The DExpr is of the form (DXFunc _ _) and correspondingly
the supplied Point is of the form (DFunc _ _, RFunc _),
and that the DFunc's args and DXFunc's args are
appropriately related.
-}
acMakeInstance s_or_l
simplest_dx
rho_d
f_simplest
= let
finalDomain = amStrongNormalise (dxApplyDSubst rho_d simplest_dx)
basicDomain = (dxApplyDSubst_2 simplest_dx)
in
acConc s_or_l finalDomain basicDomain f_simplest
-- ==========================================================--
-- === end AbsConc3.hs ===--
-- ==========================================================--
|
