diff --git a/HFusion/CHANGELOG.hs b/HFusion/CHANGELOG.hs --- a/HFusion/CHANGELOG.hs +++ b/HFusion/CHANGELOG.hs @@ -1,4 +1,9 @@ -- | +-- Version 0.0.6 +-- +-- This version contains several tweaks and fixes as a result of fusing the +-- example of game trees in John Hughes's paper Why Functional Programming Matters. +-- -- Version 0.0.5.1 -- -- * Lists missing file in hfusion.cabal. diff --git a/HFusion/Internal/FsDeriv.lhs b/HFusion/Internal/FsDeriv.lhs --- a/HFusion/Internal/FsDeriv.lhs +++ b/HFusion/Internal/FsDeriv.lhs @@ -38,7 +38,7 @@ vsis is expected to contain the constant parameters of the function f. Values returned in the following triplet -> type DReturnType = ([(Variable,Variable)], [(Variable, Int,[[Int]], [Term])], Term) +> type DReturnType = ([(Variable,Variable)], [(Variable, Int,[Term])], Term) are: * A set of free variables in t1 appearing in c1. These variables go paired with fresh variables. @@ -49,10 +49,10 @@ the corresponding fresh variables. This algorithm expects to be invoked as - aD (vars pi) fs t -where vars pi are the variables bound by pattern pi. And pattern pi + aD [... (j,vars arg_j ++ vars pi_j) ...] fs t +where vars pi_j are the variables bound by pattern pi for the argument j. And pattern pi is the pattern of the case in the body of the function over which the -derivation algorithm is applied. +derivation algorithm is applied. arg_j is the jth input argument of the function. Errors: @@ -66,10 +66,10 @@ t is the unexpected term. -> aD :: [(Int,[Variable])] -> [Variable] -> [(Variable,Int)] -> Term -> FusionState DReturnType +> aD :: [Variable] -> [(Variable,Int)] -> Term -> FusionState DReturnType -> aD pvss c1 fs t = -> let d = aD pvss c1 fs +> aD c1 fs t = +> let d = aD c1 fs > except ex t = > -- I want to eliminate variables of vsis when examining > -- expressions in a let or lambda scope. @@ -77,7 +77,7 @@ > -- vsis is non-empty, then if recursive calls appear in the > -- the term they are not saturated and so I must throw NotSaturated. > let vs = vars ex in -> aD pvss (c1 \\ vs) fs t +> aD (c1 \\ vs) fs t > in > case t of > Tvar v -> if elem v c1 then do u<-lift$ getFreshVar (varPrefix v); return ([(v,u)],[],Tvar u) @@ -114,7 +114,7 @@ > if length ts==nargs then > do let tvs=vars ts > u<-lift$ getFreshVar (if null tvs then "v" else varPrefix (head tvs)) -> return ([],[(u,idx,map (findArgumentIndexes pvss) ts,ts)],Tvar u) +> return ([],[(u,idx,ts)],Tvar u) > else throwError (NotSaturated t) > _ -> return retres > @@ -127,7 +127,6 @@ > (vs2,ps2,t2') <- d t2 > return (vs1++vs2, ps1++ps2, Tapp t1' t2') > _ -> throwError (NotExpected t) -> where findArgumentIndexes pvss t = map fst . filter (not . null . intersect (vars t) . snd)$ pvss @@ -215,8 +214,7 @@ > -- pi is the pattern in a case alternative and ti the corresponding term. > appD recs pi ti = > let ps = patternToList pi -> in do r<-aD [(i,vars r++vars p) | (i,Bvar r,p)<-zip3 [0..] recs ps] -> (union (vars recs) (vars ps)) fs ti +> in do r<-aD (union (vars recs) (vars ps)) fs ti > return (ps,r) > adaptPattern recs [] p = ptuple$ map (toPat (vars p))$ concat$ recs > adaptPattern recs _ p = diff --git a/HFusion/Internal/FunctorRep.lhs b/HFusion/Internal/FunctorRep.lhs --- a/HFusion/Internal/FunctorRep.lhs +++ b/HFusion/Internal/FunctorRep.lhs @@ -16,11 +16,10 @@ > import Control.Monad.Trans(lift) > import Control.Monad(zipWithM) > import qualified Data.Map as M(lookup,adjust,insert) +> import Data.Function(on) > import HFusion.Internal.Messages - import Debug.Trace - > import HFusion.Internal.Inline sss t = trace (show t) @@ -235,12 +234,13 @@ > => [hylo a OutF] -> Int -> [hylo InF ca] -> Int -> FusionState (Int,[(Int,Int)],[hylo a ca]) > fusionarSimple hs1 i1 hs2 i2 = fusionarSimpleAcc [((i1,i2),0)] [(i1,i2)] > where -> fusionarSimpleAcc accfi@((_,acci):_) is = +> fusionarSimpleAcc accfi is = > do res<-mapM (\(i1,i2)->do (h1,h2)<-lift$ renameVariables (hs1!!i1) (hs2!!i2) [];fusionarSimple' h1 i1 h2 i2) is > let (ws,hs,hused) = unzip3 res > nused = nub [ p | ll<-hused, l<-ll, (_,p)<-l, all ((/=p).fst) accfi] -> lnused = length nused+acci -> accfi'= zip nused [acci+1..lnused]++accfi +> laccfi = length accfi +> lnused = length nused+laccfi +> accfi'= zip nused [laccfi..lnused]++accfi > recmaps = map (map (map (\(v,p)->maybe (error "fusionarSimple: recmaps") (\i->(v,i))$ lookup p accfi'))) hused > hs'=zipWith remap recmaps hs > in if null nused then return ( sum ws @@ -248,7 +248,6 @@ > , hs') > else do (w,res,hss)<-fusionarSimpleAcc accfi' nused > return (w+sum ws,res, hs'++hss) -> fusionarSimpleAcc [] _ = error$ "fusionarSimpleAcc: unexpected empty request list" > fusionarSimple' :: (CHylo hylo,HasComponents ca,TermWrappable a) => hylo a OutF -> Int -> hylo InF ca -> Int > -> FusionState (Int,hylo a ca,[[(Position,(Int,Int))]]) > fusionarSimple' h1 i1 h2 i2 = @@ -307,19 +306,19 @@ > [h a OutF] -> Int -> [h Phii cb] -> Int -> VarGenState (Int,[(Int,Int)],[h Tau cb]) > fusionarTau hs1 i1 hs2 i2 = fusionarTauAcc [((i1,i2),0)] [(i1,i2)] > where -> fusionarTauAcc accfi@((_,acci):_) is = +> fusionarTauAcc accfi is = > do res<-mapM fusionarTau' is > let (ws,hs,hused) = unzip3 res > nused = nub$ map snd$ concat$ map (concat . map (filter (\(_,pair)->all ((/=pair).fst) accfi))) hused -> lnused = length nused+acci -> accfi'= zip nused [acci+1..lnused]++accfi +> laccfi = length accfi +> lnused = length nused+laccfi +> accfi'= zip nused [laccfi..lnused]++accfi > recmaps = map (map (map (\(v,p)->maybe (error "fusionarTau: recmaps") (\i->(v,i))$ lookup p accfi'))) hused > hs'=zipWith remap recmaps hs > if null nused then return ( sum ws > , map fst$ sortBy (\a b -> compare (snd a) (snd b)) accfi' > , hs') > else fusionarTauAcc accfi' nused >>= (\(w,res,hss)->return (w+sum ws,res,hs'++hss)) -> fusionarTauAcc [] _ = error$ "fusionarTauAcc: unexpected empty request list" > fusionarTau' (i1,i2) = > do (_,h2')<-renameVariables (hs1!!i1) (hs2!!i2) [] > h2<-toPara hs2 h2' i2 @@ -464,8 +463,8 @@ > -- * the patterns of the resulting coalgebra > -- * the pairs of hylomorphism that need to be fused. Each pair specifies the position in the output of the > -- coalgebra on which the result of fusion should be called, the index identifying the mutual component -> -- of the left hylomorphism, the index identfying the argument on which the composition occurs and -> -- the index identfying the mutual component of the unfold to fuse. There is one list of pairs for each +> -- of the left hylomorphism, the index identifying the argument on which the composition occurs and +> -- the index identifying the mutual component of the unfold to fuse. There is one list of pairs for each > -- alternative of the sigma coalgebra (after taking into account duplicated constructor occurences in inF). > deriveSigmaPatterns :: Int -> Int -> [(PatternS,[TupleTerm],HFunctor)] > -> [[(Acomponent InF,HFunctor)]] -> VarGenState (Int,[PatternS],[[((Position,Int),(Int,Int))]]) @@ -477,8 +476,8 @@ > return (matches,ps,concat hused) > where getFreshVar pr = do k<-get > case M.lookup pr (ivar k) of -> Just i -> put (k {ivar=M.adjust (+1) "v" (ivar k)}) >> return (Vgen pr i) -> _ -> put (k {ivar=M.insert "v" 1 (ivar k)}) >> return (Vgen pr 0) +> Just i -> put (k {ivar=M.adjust (+1) pr (ivar k)}) >> return (Vgen pr i) +> _ -> put (k {ivar=M.insert pr 1 (ivar k)}) >> return (Vgen pr 0) > derivePattern' inF (Ppattern v p@(Pvar _),tts,fnc1) = derivePattern ih2 v inF p tts fnc1 Pdone > derivePattern' inF (Ppattern v p,tts,fnc1) = derivePattern ih2 v inF p tts fnc1 Pdone >>= \(ps,hused0) -> > derivePattern ih2 v inF (Pvar v) tts fnc1 Pdone >>= \(_,hused1) -> @@ -549,34 +548,70 @@ > PcaseR _ _ _ _ ps -> sum$ map (countCases . fst) ps > _ -> error$ "FunctorRep: countCases: " ++ (unexpected_Pattern p) + +Collects the indexes identifying the components of the mutual unfold +which are used by a given PatternS + +> collectHyloIndexes :: PatternS -> [Int] +> collectHyloIndexes p = +> case p of +> PcaseS _ _ t -> collectHyloIndexes t +> PcaseSana _ _ _ t -> collectHyloIndexes t +> PcaseR ih _ _ _ ps -> ih : concatMap (collectHyloIndexes . fst) ps +> _ -> [] + +Collects recursive variables for each alternative of a sigma pattern. + +> collectRecVars :: PatternS -> [[Variable]] +> collectRecVars p = +> case p of +> PcaseS _ _ t -> collectRecVars t +> PcaseSana _ _ _ t -> collectRecVars t +> PcaseR ih _ _ args ps -> concatMap (\(p,nrs) -> map ((args \\ nrs) ++) (collectRecVars p)) ps +> _ -> [[]] + + + Constructs sigma. Returns the branches of the corresponding hylomorphism. -> getSigma :: (CHylo h, HasComponents b, TermWrappable a ) => [[(Acomponent InF,HFunctor)]] -> -> h a Sigma -> Int -> Int -> [h InF b] -> h InF b -> Int -> [(Acomponent a,Etai,HFunctor)] -> -> FusionState (Int,Coalgebra Sigma,[(Acomponent a,Etai,HFunctor)],[[((Position,Int),(Int,Int))]]) +> getSigma :: (CHylo h, HasComponents b, TermWrappable a, Vars b, Vars a, VarsB b, VarsB a, AlphaConvertible a, AlphaConvertible b ) => +> [[(Acomponent InF,HFunctor)]] -> +> h a Sigma -> Int -> Int -> [h InF b] -> h InF b -> Int -> [(Acomponent a,Etai,HFunctor)] -> +> FusionState (Int,Coalgebra Sigma,[(Acomponent a,Etai,HFunctor)],[[((Position,Int),(Int,Int))]]) > getSigma inF h1 ih1 ia hs2 h2 ih2 as = > do -> let etas2 h2=zipWith3 applypara (getEta h2) (getFunctor h2).getComponentTerms.(\(_,_,ca)->ca).getCoalgebra$ h2 -> applypara etai2 fnc2 tts = -> let para2 p = mapStructure (Tvar p) (Tvar p)$ expanded fnc2 p -> pos=map getPosition tts -> in etai2 `rightCompose` EOgeneral (map Bvar pos) (map para2 pos) -> v0s'' <-lift$ mapM regenVars v0s' +> v0s'' <- lift$ mapM regenVars v0s' > (pss,tts',fcn1s',as',casemap)<-addInFNoConstructorCase (pss'!!ia) pss' tts (getFunctor h1) as casemap' h2 > (matches,sps,hused)<-lift$ deriveSigmaPatterns ih2 ia (zip3 (pss!!ia) tts' fcn1s') inF > let t0t = bv2term (recbvtuple v0s'') -> caseCounts = map countCases$ sps +> caseCounts = map countCases sps > joined = replicateList (replicateList casemap caseCounts) (zip as' (replicateList casemap (zip (transpose pss) tts'))) > (psb',psa') = splitAt ia pss > (hsb',hsa') = splitAt ia hss -> return$ (matches,(v0b++recbvtuple v0s'':tail v0a,t0b++t0t:tail t0a,Sigma (zipWith (*) casemap caseCounts,tts', -> transpose (psb'++sps:(tail psa')), -> hsb'++ -> Just (ih2,getAlgebra h2,etas2 h2,wrapSigma (getCoalgebra h2), applyHyloWithCtxCntArgs (getContext h2).(hs2!!)) -> : tail hsa' +> pps = transpose (psb'++sps:(tail psa')) +> unfoldComps <- mapM extractUnfoldComponents (nub (concatMap (concatMap collectHyloIndexes) pps)) +> return (matches,(v0b++recbvtuple v0s'':tail v0a,t0b++t0t:tail t0a, +> Sigma (zipWith (*) casemap caseCounts,tts', +> pps, +> hsb'++ Just unfoldComps : tail hsa' > )), > map fst joined, hused) -> where (v0,t0s,Sigma (casemap',tts,pss'',hss))=getCoalgebra h1 +> where +> extractUnfoldComponents ih = +> if (ih==ih2) then return (extractComp ih2 h2) +> else do +> let h2'' = hs2!!ih +> (_,h2')<-lift$ renameVariables h1 (setContext emptyContext h2'') (getConstantArgs (getContext h2'')) +> return$ extractComp ih$ setContext (getContext h2'') h2' +> +> extractComp ih h = (ih,getAlgebra h,etas2 h,wrapSigma (getCoalgebra h), applyHyloWithCtxCntArgs (getContext h).(hs2!!)) +> etas2 h=zipWith3 applypara (getEta h) (getFunctor h).getComponentTerms.(\(_,_,ca)->ca).getCoalgebra$ h +> applypara etai2 fnc2 tts = +> let para2 p = mapStructure (Tvar p) (Tvar p)$ expanded fnc2 p +> pos=map getPosition tts +> in etai2 `rightCompose` EOgeneral (map Bvar pos) (map para2 pos) +> +> (v0,t0s,Sigma (casemap',tts,pss'',hss))=getCoalgebra h1 > (v0b,v0a) = break ((head t0a==) . bv2term) v0 > (t0b,t0a) = splitAt ia t0s > (v0s',_,_) = getCoalgebra h2 @@ -590,7 +625,7 @@ > do us<-lift$ zipWithM getPpatternVar t0s pss > u1<-lift$ getFreshVar (varPrefix u0) > let acomp = wrapA [Bvar u1] (TWsimple (wrapTerm (Tvar u1))) -> fnc = HF [(u1,ih1,map (:[]) [0..length us-1],PFid u1)] +> fnc = HF [(u1,ih1,PFid u1)] > eqPRow (Ppattern _ (Pcons _ _),_,prow,_,_,_) (Ppattern _ (Pcons _ _),_,prow',_,_,_) = > and$ zipWith matchPattern (take ia prow) (take ia prow') > eqPRow _ _ = False @@ -650,17 +685,17 @@ > -> (Int -> Term -> Term) -- ^ function which applies the given component of the unfold to the given term > -> HFunctor -- ^ original functor of sigma > -> HFunctor -- ^ functor of sigma after transforming the sigma hylo into a paramorphism +> -> [Variable] -- ^ recursive variables bound by the sigma pattern on the fusion argument > -> [TupleTerm] -- ^ terms returned by sigma > -> VarGenState EtaOp -> etaParaSigma ps v0s ia defaultIndex vis h fncOld fnc tts = +> etaParaSigma ps v0s ia defaultIndex vis h fncOld fnc rvars tts = > do vts' <- if nr>1 then mapM (expandHyloMutipleArgs fncOld fnc . getPosition) tts > else return$ map (Bvar . getPosition) tts > -- variables which are recursive with respect to the ia argument -> let rs = topmostVar ps ++ (vars (v0s!!ia) \\ (vars ps)) ++ (concat$ map (recvars ia) tts) +> let rs = topmostVar (drop ia ps) ++ (vars (v0s!!ia) \\ (vars ps)) ++ (concatMap (recvars rvars) tts) > return$ EOgeneral vts' (zipWith (applyh rs) vts' tts) > where nr = length v0s -> recvars ia tt = vars$ map (\(i,_)->filter isVar [termToList (getTerm tt)!!i])$ filter (elem ia.snd)$ zip [0..]$ -> getArgIndexes fnc (getPosition tt) +> recvars rvars tt = intersect rvars$ vars (getTerm tt) > topmostVar (PcaseR _ v _ _ _ : _) = [v] > topmostVar _ = [] > applyh :: [Variable] -> Boundvar -> TupleTerm -> Term @@ -709,21 +744,21 @@ > where > (v0s',_,_)=getCoalgebra (hs1!!i1) > ia = max 0 (min (length v0s'-1) ia') -> fusionarSigmaAcc accfi@((_,acci):_) is = +> fusionarSigmaAcc accfi is = > do res<-mapM fusionarSigma' is > let (ws,hs,hused) = unzip3 res > hused' :: [[[(Position,(Int,[(Int,Int)]))]]] > hused' = map (map joinHylos) hused > nused = nub$ map snd$ concat$ map (concat . map (filter (\(_,pair)->all ((/=pair).fst) accfi))) hused' -> lnused = length nused+acci -> accfi'= zip nused [acci+1..lnused]++accfi +> laccfi = length accfi +> lnused = length nused+laccfi +> accfi'= zip nused [laccfi..lnused]++accfi > recmaps = map (map (map (\(v,p)->maybe (error "fusionarSigma: recmaps") (\i->(v,i))$ lookup p accfi'))) hused' > hs'=zipWith remap recmaps hs > if null nused then return ( sum ws -> , map fst$ sortBy (\a b -> compare (snd a) (snd b)) accfi' +> , map fst$ sortBy (compare `on` snd) accfi' > , hs') > else fusionarSigmaAcc accfi' nused >>= (\(w,res,hss)->return (w+sum ws,res,hs'++hss)) -> fusionarSigmaAcc [] _ = error$ "fusionarSigmaAcc: unexpected empty request list" > -- join requests for fusion of the same hylo with different arguments > joinHylos us@(((v,ih1),_):_) = (v,(ih1,sort$ map snd us')) : joinHylos uss > where (us',uss) = partition ((==v).fst.fst) us @@ -739,15 +774,16 @@ > (getFunctor h) reptts > updPara :: [HFunctor] -> (Int,Int) -> [[EtaOp]] -> VarGenState [[EtaOp]] > updPara fncs (ia,ih2) etas = -> do etas'<-mapM (upd ia ih2 v0)$ zip5 (getFunctor h) fncs +> do etas'<-mapM (upd ia ih2 v0)$ zip6 (getFunctor h) fncs > (map (nub . map (\((a,_),(_,d))->(a,d))) hused) > (replicateList casemap pss) +> (concatMap (collectRecVars . (!!ia)) pss) > reptts > return$ zipWith (:) etas' etas > in do etas2<-foldrM (updPara fncs) (replicate (length fncs) []) is > return$ setEta (zipWith3 composeEtas (getEta h) etas1 etas2)$ setFunctor fncs h -> upd ia ih2 v0 (fnc1,fnc1',indexes,ps,tts) = -> etaParaSigma ps v0 ia ih2 indexes (applyHyloList hs2 (hs2!!ih2) ih2) fnc1 fnc1' tts +> upd ia ih2 v0 (fnc1,fnc1',indexes,ps,rvars,tts) = +> etaParaSigma ps v0 ia ih2 indexes (applyHyloList hs2 (hs2!!ih2) ih2) fnc1 fnc1' rvars tts > composeEtas eta e1 es2 = foldl rightCompose (eta `rightCompose` e1) es2 > paraMKNRSigma :: CHylo h => [h a ca] -> h a ca -> Context -> Int -> [Position] -> HFunctor -> [TupleTerm] -> (EtaOp,HFunctor) > paraMKNRSigma hs1 h1 ctx ih1 recs fnc1 tts = diff --git a/HFusion/Internal/FuseFace.lhs b/HFusion/Internal/FuseFace.lhs --- a/HFusion/Internal/FuseFace.lhs +++ b/HFusion/Internal/FuseFace.lhs @@ -43,7 +43,7 @@ > import HFusion.Internal.Utils > import HFusion.Internal.Messages -> import Debug.Trace + import Debug.Trace sss s v = trace (s++": "++show v) v diff --git a/HFusion/Internal/HsSyn.hs b/HFusion/Internal/HsSyn.hs --- a/HFusion/Internal/HsSyn.hs +++ b/HFusion/Internal/HsSyn.hs @@ -216,6 +216,9 @@ instance AlphaConvertible Variable where alphaConvert sc lvars v = if elem v sc then maybe v id $ lookup v lvars else v +instance AlphaConvertible Def where + alphaConvert sc ss (Defvalue v t) = (maybe (Defvalue v) Defvalue$ lookup v ss)$ alphaConvert (v:sc) ss t + instance AlphaConvertible Term where alphaConvert sc ss t@(Tvar v) = if elem v sc then maybe t Tvar $ lookup v ss else t alphaConvert sc ss (Tlamb bv t) = Tlamb (alphaConvert sc ss bv) (alphaConvert (sc++vars bv) ss t) diff --git a/HFusion/Internal/HyloFace.lhs b/HFusion/Internal/HyloFace.lhs --- a/HFusion/Internal/HyloFace.lhs +++ b/HFusion/Internal/HyloFace.lhs @@ -15,7 +15,7 @@ > , getTerm, setTerm, getPosition, getPositions, rightCompose, leftCompose, compose > , composeEta, idEta, expanded, mapTau, mapTW, mapTWacc, wrapA, isRec > , runFusionState, FusionState, FusionError(..) -> , mapTWaccM, expandPositions, remapPositions, getArgIndexes, isIdEta, tupleterm +> , mapTWaccM, expandPositions, remapPositions, isIdEta, tupleterm > , getTupletermsWithArgIndexes, makePosNR, OutFi(..) > , CoalgebraTerm(..), HasComponents(..), Coalgebra, TermWrappable(..) > , module HFusion.Internal.HsSyn @@ -287,7 +287,9 @@ > -- Each list element contains a tuple of patterns and > -- a tuple of terms to be returned when the pattern matches. > newtype Psi = Psi [Psii] +> deriving Show > newtype Psii = Psii PsiiRep +> deriving Show > type PsiiRep = ([Pattern],[TupleTerm]) > -- | Representation for alternatives of coalgebras in OutF form. @@ -309,20 +311,24 @@ > -- where beta_1,...,beta_n are coalgebras of mutual hylomorphism. Each coalgebra > -- component i is applied only to the i^th argument of the transfomer result. -> newtype Sigma = Sigma ([Int],[[TupleTerm]],[[PatternS]],[Maybe (Int,[Acomponent InF],[Etai],WrappedCA,Int->Term->Term)]) +> newtype Sigma = Sigma ([Int],[[TupleTerm]],[[PatternS]],[Maybe [(Int,[Acomponent InF],[Etai],WrappedCA,Int->Term->Term)]]) > -- ^ In Sigma (casemap,ts,[ps_1,...,ps_n],[psi_1,...,psi_n]), > -- * ts are the terms returned by sigma. > -- * ps_i are the patterns corresponding to each alternative of the hylomorphism, -> -- it contains one pattern for each recursive argument. +> -- the inner lists contain one pattern for each recursive argument. > -- * psi_i is the coalgebra given as argument to sigma in position i. > -- Each coalgebra psi_i is really a mutual hylomorphism, that's why > -- it is a list. When inlining, the coalgebra and the natural transformations of this > -- mutual hylo are extracted. Each component of the mutual hylo has an algebra, a > -- natural transformation, a coalgebra and a function fapp returning an application -> -- of the hylo to its input term. The algebra is stored, because it may contain part +> -- of the hylo to its input term. The algebra is stored because it may contain part > -- of the natural transformation, but it is also used during inlining to match cases > -- of its hylo with patterns of sigma. +> -- +> -- If no fusion happend on the ith parameter, psi_i is Nothing, otherwise it contains +> -- a list with the components of the mutual unfold. +> -- > -- * casemap tells how the alternatives of sigma connects with the alternatives of the > -- hylomorphism. Each sigma tuple must be replicated the amount specified in the > -- corresponding position of casemap. @@ -511,19 +517,16 @@ > -- which they appear in the product. For getting the order, use the tuples returned > -- by the coalgebra and retrieve the descriptions using the positions of the tuple elements. > -- In: -> -- @HF [(p,mri,mais,copies)]@ +> -- @HF [(p,mri,copies)]@ > -- * @p@ is a unique identifier for the position in the product. > -- * @mri@ is the index of the mutual hylo component that is applied to this position. > -- If the position is not recursive, most likely there is not an entry in the list. > -- However there will be non-recursive positions if originally they were recursive > -- and then were made non-recursive as the result of a restructure. -> -- * @mais@ are the indices of the hylomorphism arguments involved in the construction of -> -- the recursive argument. They are used for fusion of hylomorphims of multiple -> -- arguments. > -- * @copies@ is a tree-like structures that tells how the recursive values are copied. > -- It is used for fusion of paramorphisms. -> newtype HFunctor = HF [(Position,Int,[[Int]],ParaFunctor)] +> newtype HFunctor = HF [(Position,Int,ParaFunctor)] > deriving Show > -- | Representation of sum terms of functors. @@ -562,30 +565,24 @@ > isRec :: HFunctor -> Position -> Bool > isRec (HF vrs) p = any isR vrs -> where isR (p',_,_,bv) = p==p' && foldPF (const True) (const False) or bv || foldPF (==p) (const False) or bv +> where isR (p',_,bv) = p==p' && foldPF (const True) (const False) or bv || foldPF (==p) (const False) or bv > -- | Returns the identifier of the projection in a recursive position. > getRecIndex :: HFunctor -> Position -> Maybe Int -> getRecIndex (HF vrs) p = fmap (\(_,i,_,_)->i)$ find (findPos p)$ vrs -> where findPos p (p',_,_,bv) = p==p' && foldPF (const True) (const False) or bv || foldPF (p==) (const False) or bv - -> -- | Returns indexes of the arguments involved in constructing the term for a given position. - -> getArgIndexes :: HFunctor -> Position -> [[Int]] -> getArgIndexes (HF vrs) p = maybe [] (\(_,_,iss,_)->iss)$ find (findPos p)$ vrs -> where findPos p (p',_,_,bv) = p==p' && foldPF (const True) (const False) or bv || foldPF (p==) (const False) or bv +> getRecIndex (HF vrs) p = fmap (\(_,i,_)->i)$ find (findPos p)$ vrs +> where findPos p (p',_,bv) = p==p' && foldPF (const True) (const False) or bv || foldPF (p==) (const False) or bv > -- | Transforms the given positions from recursive to non-recursive. > makePosNR :: [Position] -> HFunctor -> HFunctor > makePosNR ps (HF vrs) = HF (mknr' ps vrs) -> where mknr' ps vrs = if any (\(v,_,_,_)->elem v ps) vrs -> then map (\t@(v,i,iss,bv)-> if elem v ps then (v,i,iss,foldPF PFcnt PFcnt PFprod bv) else t) vrs +> where mknr' ps vrs = if any (\(v,_,_)->elem v ps) vrs +> then map (\t@(v,i,bv)-> if elem v ps then (v,i,foldPF PFcnt PFcnt PFprod bv) else t) vrs > else mknr ps vrs -> mknr ps (h@(p,i,iss,bv):vs) | any (flip elem ps) (vars bv) = (p,i,iss,foldPF (mknrbv ps) PFcnt PFprod bv):vs -> | otherwise = h:mknr ps vs +> mknr ps (h@(p,i,bv):vs) | any (flip elem ps) (vars bv) = (p,i,foldPF (mknrbv ps) PFcnt PFprod bv):vs +> | otherwise = h:mknr ps vs > mknr _ [] = [] > mknrbv ps p | elem p ps = PFcnt p > | otherwise = PFid p @@ -596,7 +593,7 @@ > expandPositions :: [(ParaFunctor,Position)] -> HFunctor -> HFunctor > expandPositions ps (HF vrs) = HF (map (exp ps) vrs) -> where exp ps (p,i,iss,bv) = (p,i,iss,foldPF (expbv ps) PFcnt PFprod bv) +> where exp ps (p,i,bv) = (p,i,foldPF (expbv ps) PFcnt PFprod bv) > where expbv ps v = case find ((v==).snd) ps of > Just (PFprod [],_) -> PFid v > Just (pf,_) -> pf @@ -606,9 +603,9 @@ > -- | Returns the functor term corresponding to a given position of a functor. > expanded :: HFunctor -> Position -> ParaFunctor -> expanded fnc@(HF vrs) p = case find (\(p',_,_,_)->p'==p) vrs of -> Just (_,_,_,PFprod []) -> PFcnt p -> Just (_,_,_,bv) -> bv +> expanded fnc@(HF vrs) p = case find (\(p',_,_)->p'==p) vrs of +> Just (_,_,PFprod []) -> PFcnt p +> Just (_,_,bv) -> bv > _ | isRec fnc p -> PFid p > | otherwise -> PFcnt p @@ -616,9 +613,9 @@ > remapPositions :: [(Position,Int)] -> HFunctor -> HFunctor > remapPositions idxs (HF vrs) = -> HF$ map (\o@(a,_,iss,b)->maybe o (\i'->(a,i',iss,b))$ -> maybe (foldPF (flip lookup idxs) (const Nothing) findJust b) Just$ -> lookup a idxs) +> HF$ map (\o@(a,_,b)->maybe o (\i'->(a,i',b))$ +> maybe (foldPF (flip lookup idxs) (const Nothing) findJust b) Just$ +> lookup a idxs) > vrs > where findJust (Just a:_) = Just a > findJust (_:as) = findJust as diff --git a/HFusion/Internal/HyloRep.lhs b/HFusion/Internal/HyloRep.lhs --- a/HFusion/Internal/HyloRep.lhs +++ b/HFusion/Internal/HyloRep.lhs @@ -63,7 +63,7 @@ > instance CHylo Hylo where > buildHylo names ts = aA names ts >>= (return . zipWith buildHylo' names) -> where buildHylo' :: Variable -> ([Boundvar],[Term],[([Pattern],([(Variable,Variable)], [(Variable, Int,[[Int]], [Term])], Term))]) +> where buildHylo' :: Variable -> ([Boundvar],[Term],[([Pattern],([(Variable,Variable)], [(Variable, Int, [Term])], Term))]) > -> Hylo Phii Psi > buildHylo' name (vsm,t0,lns) = Hylo { hylo_algebra = a, > hylo_nattrans = etas, @@ -73,13 +73,13 @@ > hylo_name = name } > where > (a,etas,fncs,ca)=unzip4$ map buildLine lns -> buildLine :: ([Pattern],([(Variable,Variable)], [(Variable, Int,[[Int]], [Term])], Term)) +> buildLine :: ([Pattern],([(Variable,Variable)], [(Variable, Int, [Term])], Term)) > -> (Acomponent Phii,Etai,HFunctor,Psii) > buildLine (pattern,(vs,vts,t)) = -> (wrapA (map Bvar$ phiNoRecVars++phiRecVars) (TWsimple t),idEta,HF .zip4 phiRecVars idxs ias.map PFid$ phiRecVars, +> (wrapA (map Bvar$ phiNoRecVars++phiRecVars) (TWsimple t),idEta,HF .zip3 phiRecVars idxs . map PFid$ phiRecVars, > Psii (pattern,zipWith (flip tupleterm.Tvar) psiNoRecVars phiNoRecVars > ++zipWith (\v ts -> tupleterm v (recArgsToTerm ts)) phiRecVars psiRecTerms)) -> where (phiRecVars,idxs,ias,psiRecTerms) = unzip4 vts +> where (phiRecVars,idxs,psiRecTerms) = unzip3 vts > (psiNoRecVars,phiNoRecVars) = unzip vs > recArgsToTerm [t] = t > recArgsToTerm ts = Ttuple True ts diff --git a/HFusion/Internal/Inline.lhs b/HFusion/Internal/Inline.lhs --- a/HFusion/Internal/Inline.lhs +++ b/HFusion/Internal/Inline.lhs @@ -98,18 +98,19 @@ > inlineSigma :: [Term] -> Sigma -> [Term] -> VarGenState Term > inlineSigma t0s (Sigma (casemap,ts,pss,hss)) ts' = -> do t<-inlineTHS (reorganizeSigma$ weaveTermS (splitList initialTerms casemap)$ pss) +> do t<-inlineTHS (reorganizeSigma$ weaveTermS (splitList initialTerms casemap) pss) > return$ insertRecvarCases t0s pss t -> where inlineTHS t = inlineTermS inlWCA (\ia ih -> lookupfapp ih (hss!!ia)) (matchSigmaTerms t0s pss) t +> where inlineTHS = inlineTermS inlWCA (\ia ih -> lookupfapp ih (hss!!ia)) (matchSigmaTerms t0s pss) > getCaTerm = Ttuple False . map getTerm > initialTerms | null ts' = map getCaTerm ts > | otherwise = ts' > inlWCA :: Int -> Int -> [(Variable,Term)] -> Variable -> > (Acomponent InF->(Term->Term,[Term])->State InlST Term)->State InlST Term -> inlWCA ia _ sust t0 f = -> do let Just (_,inFs,etas,wca,_) = hss!!ia +> inlWCA ia ih sust t0 f = +> do let Just hss' = hss!!ia +> Just (_,inFs,etas,wca,_) = find (\(i,_,_,_,_)->ih==i) hss' > k<-get -> let (wca',i')=runState (renamePatternVars wca) (gi k) -- renombrar variables de patrones +> let (wca',i')=runState (renamePatternVars wca) (gi k) -- rename pattern variables > put (k {gi=i'}) > ts<-sequence$ zipWith f inFs (inlEtas wca' sust etas) > k<-get @@ -120,8 +121,9 @@ > inlCA (WCApsi c) t0 ts = caGetInline ts t0 c > inlCA (WCAoutF c) t0 ts = caGetInline ts t0 c > inlCA (WCAsigma c) t0 ts = caGetInline ts t0 c -> lookupfapp i (Just (_,_,_,_,fapp)) = fapp i -> lookupfapp _ _ = error "lookupfapp: unexpected case" +> lookupfapp i (Just hss') = maybe (error "lookupfapp: unexpected case") (\(_,_,_,_,fapp) -> fapp i) +> $ find (\(i',_,_,_,fapp)->i==i') hss' +> lookupfapp _ _ = error "lookupfapp: unexpected case in recursive argument data" > inlineTermS inlWCA fapp sust t = > case t of > TtermS t -> return t @@ -715,31 +717,31 @@ > showDocSigma i ia bvs t0s (Sigma (casemap,tts,pss,hss)) = -> (prefix i ia <+>text ("Sigma_"++show i) <> -> cat (text "(" : map (nest 2) (uncurry (++)$ (id *** map (text ","<+>))$ splitAt 1 sigmaargs)++[text ")"]) +> (text ("Sigma_"++show i) <> catArgs (map catArgs sigmaargs) > $$) . nest 2 . (text "where" <+>) $ > (((text ("Sigma_"++show i++" =") <+>) . showDoc . -> Tlamb (Bvtuple False [ Bvar (beta ia) | (ia,Just _)<-zip [0..] hss]) . +> Tlamb (Bvtuple False [ Bvtuple False [ Bvar (beta ia ih) | (ih,_,_,_,_) <- hss' ] | (ia,Just hss')<-zip [0..] hss ]) . > Tlamb (bvtuple bvs) . nullPatternVariables . delCases . insertRecvarCases t0s pss . -> termS2Term (\ia _ ->Tfapp (beta ia)) . +> termS2Term (\ia ih ->Tfapp (beta ia ih)) . > reorganizeSigma . weaveTermS (zipWith (zipWith mksum) > (splitList [1..] casemap) > (zipWith replicate casemap tts))$ pss ) -> $$ vcat [ showCA ia h | (ia,Just h)<-zip [0..] hss]) -> where sigmaargs = [ text (eta' ia++"."++eta'' ia++"."++psi ia) | (ia,Just _)<-zip [0..] hss] -> prefix 0 _ = empty -> prefix _ ia = text (psi ia++" =") -> showCA ia (_,acomps,etas,ca,_) = -> text (eta' ia) <+> char '=' <+> vcat (map showDoc (evalState (mapM buildeta' acomps) [])) -> $$ text (eta'' ia) <+> char '=' <+> vcat (map showDoc etas) -> $$ innerPrefix ca ia <+> showDocWCA (i+1) ia ca -> psi ia = "psi_"++show ia++"'" -> eta' ia = "eta_"++show ia++"'" -> eta'' ia = "eta_"++show ia++"''" -> innerPrefix (WCAsigma _) _ = empty -> innerPrefix _ ia = text (psi ia++" =") +> $$ vcat [ showCA ia h | (ia,Just hss')<-zip [0..] hss , h<-hss' ]) +> where catArgs = cat . (text "(" :) . (++[text ")"]) . map (nest 2) . uncurry (++) . (id *** map (text ","<+>)) . splitAt 1 +> sigmaargs = [ [ text (eta' ia ih++"."++eta'' ia ih++"."++psi ia ih) | (ih,_,_,_,_)<-hss' ] +> | (ia,Just hss')<-zip [0..] hss +> ] +> showCA ia (ih,acomps,etas,ca,_) = +> text (eta' ia ih) <+> char '=' <+> vcat (map showDoc (evalState (mapM buildeta' acomps) [])) +> $$ text (eta'' ia ih) <+> char '=' <+> vcat (map showDoc etas) +> $$ innerPrefix ca ia ih <+> showDocWCA (i+1) ia ca +> psi ia ih = "psi_"++show ia++"_"++show ih++"'" +> eta' ia ih = "eta_"++show ia++"_"++show ih++"'" +> eta'' ia ih = "eta_"++show ia++"_"++show ih++"''" +> innerPrefix (WCAsigma _) _ _ = empty +> innerPrefix _ ia ih = text (psi ia ih++" =") > mksum i tts = Ttuple False [Tlit (Lint (show i)),Ttuple False$ map getTerm tts] -> beta ia = Vuserdef ("@beta_"++show ia) +> beta ia ih = Vuserdef ("@beta_"++show ia++"_"++show ih) > buildeta' acomp = do let bvs=getVars acomp > t<-inlA inF2Term acomp (id,map bv2term bvs) > return$ Tlamb (Bvtuple False bvs) t diff --git a/HFusion/Internal/Messages.lhs b/HFusion/Internal/Messages.lhs --- a/HFusion/Internal/Messages.lhs +++ b/HFusion/Internal/Messages.lhs @@ -99,12 +99,13 @@ > cmd_command = "!cmd executes de cmd command" > save_command = "save f1..fn saves all files f1..fn" > hylo_command = "hn: dispplays the definition of hn as hylomorphism" +> hylor_command = "hylor dispplays the definition of hn as hylomorphism" > envi_command = "env displays the list of definitions in the environment" > def_command = "hn displays the recursive definition of hn" > fuse_command = "nh = h1 . h2 fuse h1.h2 & binds the result to the identifier nh" > help_command = "help shows the available commands" > check_command = "checkfile fn matches the definitions of previous fusions calculations in a repository" -> assertEq_command= "assertEq f g prints an error messages if the definitions are different (modulus alpha conversion)" +> assertEq_command= "assertEq [(v0,q0),...,(vn,qn)] f g prints an error messages if the definitions are different (modulus alpha conversion and the specified free variables which will be taken as equal)" > cata_command = "cata h displays h as catamorphism" > ana_command = "ana h displays h as anamorphism" > quit_command = "quit ends the program" diff --git a/HFusion/Internal/Parsing/HyloParser.lhs b/HFusion/Internal/Parsing/HyloParser.lhs --- a/HFusion/Internal/Parsing/HyloParser.lhs +++ b/HFusion/Internal/Parsing/HyloParser.lhs @@ -18,13 +18,15 @@ > import Control.Monad.Trans(lift) > import Control.Monad.State(StateT(..),State,MonadState(..)) > import List(partition,intersect,union,find,nubBy,(\\),deleteFirstsBy,sort) +> import Data.Maybe(isJust,catMaybes) + import Debug.Trace + -- Posición de un token. Es utilizada por el parser y el -- lexer para resolver los problemas del layout. data SrcLoc = SrcLoc Int Int -- (Line, Indentation) deriving (Eq,Ord,Show) - > parse :: String -> FusionState [HyloT] > parse inp = parseResult2FusionState (parseModule inp) >>= hsModule2HsSyn >>= > lift . deriveHylos >>= \(errors,hs) -> if null errors then return (map snd hs) @@ -38,7 +40,7 @@ > -- output together with the error obtained when attempting derivation. > deriveHylos :: [Def] -> VarGenState ([([Def],FusionError)],[([Def],HyloT)]) > deriveHylos dfs = removeInputVar dfs >>= -> handleRegularFunctions . getCycles >>= \ cdfs -> +> handleRegularFunctions . getCycles >>= \ cdfs -> > mapM (\cdf -> runErrorT$ fmap ((,) cdf)$ deriveHylo cdf) cdfs >>= \ehs -> > return (concat (zipWith (\df -> either ((:[]) . ((,) df)) (const [])) cdfs ehs) > ,concat (map (either (const []) (:[])) ehs)) @@ -69,7 +71,7 @@ > catchParseState _ h (ParseFailed loc err) = h loc err -getCycles agrupa las definiciones de funciones mutuamente recursivas. +getCycles groups mutually recursive function definitions. > getCycles :: [Def] -> [[Def]] > getCycles defs = let idxs=findCycles (getDependencyGraph defs) @@ -128,8 +130,9 @@ > pat2term (Pas v _) = Tvar v -> type CallDescription = (Variable,Def,Int,[Variable],Term) +> type CallDescription = (Variable,Def,Int,[Maybe Term],Term) + handleRegularFunctions creates new definition where recursion of regular functors can be expressed with mutually recursive functions. @@ -152,8 +155,8 @@ > eqDefs d d' = getDefName d == getDefName d' > buildDef :: CallDescription -> VarGenState Def -> buildDef (u,d,i,vs,t) = buildDef' u i vs t d -> buildDef' u i vs t (Defvalue nd t0) = +> buildDef (u,d,i,tsargs,t) = buildDef' u i tsargs t d +> buildDef' u i tsargs t (Defvalue nd t0) = > do (us,t')<-regenVars t > t0'<-regenConstantArgs t t0 > let (bvs,t0'') = getInputVars t0' @@ -166,11 +169,21 @@ > getInputVars t = ([],t) > bv2pat (Bvar v) = Pvar v > bv2pat (Bvtuple _ bvs) = Ptuple (map bv2pat bvs) -> regenConstantArgs t t0 = do let freeVars = vars t \\ vs -> us<-mapM (getFreshVar . varPrefix) freeVars -> return$ alphaConvert [] (zip freeVars us) t0 -> regenVars t = do us<-mapM (getFreshVar . varPrefix) vs -> return (us,substitution (zip vs (map Tvar us)) t) +> regenConstantArgs t t0 = +> do let freeVars = case t of +> Tfapp v args -> v : concat (zipWith (\a -> maybe (vars a) (const [])) args tsargs) +> _ -> vars t +> us<-mapM (getFreshVar . varPrefix) freeVars +> return$ alphaConvert [] (zip freeVars us) t0 +> regenVars t = do us<-mapM (maybe (return Nothing) (\t -> fmap Just$ +> case vars t of +> [] -> getFreshVar "u" +> v:_ -> getFreshVar (varPrefix v))) tsargs +> return (catMaybes us, +> case t of +> Tfapp v args -> Tfapp v (zipWith (\a -> maybe a Tvar) args us) +> _ -> t +> ) > adaptr bs us (Ttuple b ts) = Ttuple b (map (adaptr bs us) ts) > adaptr bs us (Tcapp c ts) = Tcapp c (map (adaptr bs us) ts) > adaptr bs us (Tcase t0 ps ts) = Tcase (adaptr bs us t0) ps @@ -183,17 +196,19 @@ > in Tfapp u (map Tvar us++ant++tail pos) > | otherwise = Tfapp fv (map (adaptr bs us) ts) > adaptr _ _ t = t +> isVar (Tvar _) = True +> isVar _ = False getCalls collects the information about each recursive call that can be rewritten as -a call to a recursive function which fixates one of the arguments. +a call to a recursive function which fixes one of the arguments. The returned pair (def,l) contains the rewritten definition (with fresh vars for some recursive calls), and l is a list containing data for each of the new definitions to be introduced. Each item in the list is a tuple (u,def,i,vrs,t) where u is the name for the new definition, -def is the definition to be rewritten with a fixated argument, -i is the index of the fixated argument, +def is the definition to be rewritten with a fixed argument, +i is the index of the fixed argument, vrs are the bounded variables appearing in the term in the ith argument, and t is that term. @@ -215,47 +230,45 @@ > return (Tlet v t0' t1',n0++n1) > getCalls' bs (Tcapp c ts) = do (ts',ns)<-mapGetCalls' bs ts > return (Tcapp c ts',ns) -> getCalls' bs (Tfapp v ts) = +> getCalls' bs tt@(Tfapp v ts) = > do (ts',ns)<-mapGetCalls' bs ts > let rr = return (Tfapp v ts',ns) -> mi = [ p | p@(_,t)<-zip [0..] ts', any (flip elem (vars t)) ds ] > checkNoPattern (idxs,d@(Defvalue _ t)) = -> if not (null mi) -- there is a recursive call -> && all (flip elem idxs.fst) mi -- all recursive calls appear in constant positions -> && all callIsOkToSpecialize mi -> then mr (fst (head mi)) d -> else rr +> case [ i | (i,t)<-zip [0..] ts', any (flip elem (vars t)) ds, callIsOkToSpecialize i t ] of +> i:_ | elem i idxs -> mr i d -- recursive calls appear in constant positions +> _ -> rr > where (vargs,t') = extractVars t -> callIsOkToSpecialize (i,Tfapp v' ts) = -> elem v' ds && all isVar ts +> callIsOkToSpecialize i (Tfapp v' ts) = +> elem v' ds > && (length ts < lengthvargs' > || length ts==lengthvargs' > -- variable is used at most once > && countLinear (getVar (vargs!!i)) t'<2) > where lengthvargs' = maybe (error "lengthvars'") > (length.fst.extractVars.getDefTerm) $ find ((v'==).getDefName)$ concat ps -> callIsOkToSpecialize (_,Tvar _) = True -> callIsOkToSpecialize _ = False -> isVar (Tvar _) = True -> isVar _ = False +> callIsOkToSpecialize _ (Tvar _) = True +> callIsOkToSpecialize _ _ = False > getVar (Bvar v) = v > getVar _ = error "getCalls': getVar" > mr i d = do let (ant,pos)=splitAt i ts' -> vs = filter (\x-> elem x bs) (vars (head pos)) +> tsargs = map (\t -> if (not$ isVar t) || (not$ null$ intersect (vars t) bs) then Just t else Nothing)$ +> case (head pos) of { Tfapp _ ts -> ts; _ -> [] } > calls<-get -> case find (\(_,d',i',vs',t')-> i'==i +> case find (\(_,d',i',tsargs',t')-> i'==i > && getDefName d'==getDefName d -> && vs==vs' +> && and (zipWith (\t t' -> isJust t == isJust t') tsargs tsargs') > && t'==head pos) > calls of > Nothing -> do u<-lift$ getFreshVar (varPrefix v) -> let c = (u,d,i,vs,head pos) +> let c = (u,d,i,tsargs,head pos) > put (c:calls) -> return (Tfapp u (map Tvar vs++ant++tail pos),c:ns) -> Just (u,_,_,_,_) -> return (Tfapp u (map Tvar vs++ant++tail pos),ns) +> return (Tfapp u (catMaybes tsargs++ant++tail pos),c:ns) +> Just (u,_,_,_,_) -> return (Tfapp u (catMaybes tsargs++ant++tail pos),ns) > if elem v bs then rr > else maybe rr checkNoPattern (lookupDef v (map constantArgs ps) ps) > getCalls' _ t = return (t,[]) +> isVar (Tvar _) = True +> isVar _ = False > constantArgs :: [Def] -> [Int] > constantArgs dfs = findConstantArguments dfs > mapGetCalls' bs ts = do res<-mapM (getCalls' bs) ts diff --git a/HFusion/Internal/Parsing/Translator.lhs b/HFusion/Internal/Parsing/Translator.lhs --- a/HFusion/Internal/Parsing/Translator.lhs +++ b/HFusion/Internal/Parsing/Translator.lhs @@ -13,6 +13,8 @@ > import Control.Monad.State(get,put) > import Language.Haskell.Syntax > import qualified Data.Map as M(insertWith) +> import Data.Data(gmapQ,Data) +> import Data.Generics(extQ) > import HFusion.Internal.HyloFace import Debug.Trace @@ -22,16 +24,35 @@ sss t = trace (show t) t sss' t = trace (show t) +> -- | collects variable names in haskell module. +> collectVarNames :: Data a => a -> [String] +> collectVarNames t = concat$ gmapQ gvars t +> where +> gvars :: Data a => a -> [String] +> gvars = collectVarNames `extQ` hsname +> hsname :: HsName -> [String] +> hsname (HsIdent n) = [n] +> hsname (HsSymbol _) = [] + + + > -- | Converts an 'HsModule' into the abstract syntax tree used by HFusion. > -- The HsModule can be obtained by parsing a Haskell program with > -- 'Language.Haskell.Parser.parseModule' > hsModule2HsSyn :: HsModule -> FusionState [Def] -> hsModule2HsSyn m = do p <- lift (hsModule2HsSyn_ m) +> hsModule2HsSyn m = do lift$ updateVariableGeneratorState$ collectVarNames m +> p <- lift$ hsModule2HsSyn_ m > case p of > ([],dfs) -> return dfs > (e:_,_) -> throwError e +> where +> updateVariableGeneratorState vs = do gi<-get; put (foldr updateSt gi vs) +> updateSt s gi = case str2var s of +> (Vgen p i) -> M.insertWith max p (i+1) gi +> _ -> gi + > hsModule2HsSyn_ :: HsModule -> VarGenState ([FusionError],[Def]) > hsModule2HsSyn_ (HsModule _ _ _ _ decls) = > do m<-mapM (runErrorT . convertDecl2Def) ((filter selectd) decls) @@ -60,13 +81,7 @@ > do r <- mapM convertHsMatch hsMatches > let (ns,args,ts)= unzip3 r > if null ns then fail "convertDecl2Term: we got an empty declaration" -> else lift (updateVariableGeneratorState (nub (vars (head ns)++vars args++varsB ts)) -> >> joinEquations args ts >>= return . Defvalue (head ns)) -> updateVariableGeneratorState vs = do gi<-get; put (foldr updateSt gi vs) -> updateSt (Vgen p i) gi = M.insertWith max p (i+1) gi -> updateSt (Vuserdef s) gi = case str2var s of -> v@(Vgen _ _) -> updateSt v gi -> _ -> gi +> else lift (joinEquations args ts >>= return . Defvalue (head ns)) @@ -260,6 +275,7 @@ > Special HsCons -> Tcapp ":" args > where cons s | isUpper (head s) = Tcapp s > | not (null args) = Tfapp (str2var s) +> | s=="undef" = const Tbottom > | otherwise = const (Tvar (str2var s)) > convertLit2Lit :: HsLiteral -> Literal @@ -301,4 +317,5 @@ > fixInfixAssoc (Tfapp v ts) = Tfapp v $ map fixInfixAssoc ts > fixInfixAssoc t@(Tvar _) = t > fixInfixAssoc t@(Tlit _) = t +> fixInfixAssoc t@Tbottom = t > fixInfixAssoc _ = error "fixInfixAssoc Term: not defined." diff --git a/HFusion/Internal/RenVars.lhs b/HFusion/Internal/RenVars.lhs --- a/HFusion/Internal/RenVars.lhs +++ b/HFusion/Internal/RenVars.lhs @@ -102,9 +102,8 @@ > vars (Acomp (bvs, termwrapper)) = vars termwrapper \\ vars bvs > instance Vars Sigma where -> vars (Sigma (_,listatps,_,hss)) = vars listatps ++ concat (map varshs hss) -> where varshs (Just (_,apcomsInf,_,wca,_)) = vars apcomsInf ++ vars wca -> varshs _ = [] +> vars (Sigma (_,listatps,_,hss)) = vars listatps ++ concat (map (maybe [] (concatMap varshs)) hss) +> where varshs (_,apcomsInf,_,wca,_) = vars apcomsInf ++ vars wca > instance Vars WrappedCA where > vars (WCApsi (bv, t0, psi)) = (vars t0 ++ vars psi) \\ vars bv @@ -174,9 +173,16 @@ > alphaConvert sc lvars (Etai (etaOp1,etaOp2)) = Etai (alphaConvert sc lvars etaOp1, alphaConvert sc lvars etaOp2) > instance (AlphaConvertible a) => AlphaConvertible (TermWrapper a) where -> alphaConvert sc lvars tw = foldTW (\t0 ps ts sc -> TWcase (alphaConvert sc lvars t0) ps (zipWith ($) ts (map ((sc++).vars) ps))) -> (\t e sc ->TWeta (t sc) (alphaConvert sc lvars e)) (\t sc -> TWsimple (alphaConvert sc lvars t) ) -> (\t sc -> TWacomp (alphaConvert sc lvars t)) (const TWbottom) tw sc +> alphaConvert sc lvars tw = +> foldTW (\t0 ps ts sc -> TWcase (alphaConvert sc lvars t0) +> (alphaConvert sc lvars ps) +> (zipWith ($) ts (map ((sc++).vars) ps)) +> ) +> (\t e sc ->TWeta (t sc) (alphaConvert sc lvars e)) (\t sc -> TWsimple (alphaConvert sc lvars t) ) +> (\t sc -> TWacomp (alphaConvert sc lvars t)) +> (const TWbottom) +> tw +> sc ====================================================================== @@ -198,10 +204,9 @@ > instance AlphaConvertible Sigma where > alphaConvert sc lvars (Sigma (casemap,listatupleterms, pss, hss)) = > Sigma (casemap,alphaConvert (sc++varsB pss) lvars listatupleterms, -> map (alphaConvert sc lvars) pss, map ss hss) -> where ss (Just (i,compsInf, etais, wrappedCa, funcTermTerm)) = -> Just (i,alphaConvert sc lvars compsInf, alphaConvert sc lvars etais, alphaConvert sc lvars wrappedCa, funcTermTerm) -> ss _ = Nothing +> map (alphaConvert sc lvars) pss, map (fmap (map ss)) hss) +> where ss (i,compsInf, etais, wrappedCa, funcTermTerm) = +> (i,alphaConvert sc lvars compsInf, alphaConvert sc lvars etais, alphaConvert sc lvars wrappedCa, funcTermTerm) > instance AlphaConvertible WrappedCA where > alphaConvert sc lvars (WCApsi (bound,term,psi)) = WCApsi (alphaConvert sc lvars bound,alphaConvert sc' lvars term,alphaConvert sc' lvars psi) diff --git a/HFusion/Internal/Utils.lhs b/HFusion/Internal/Utils.lhs --- a/HFusion/Internal/Utils.lhs +++ b/HFusion/Internal/Utils.lhs @@ -134,13 +134,15 @@ > Ttuple b ts -> Ttuple b $ map (substitution ss) ts > Tfapp v ts -> -> let -> mts = map (substitution ss) ts -> in -> case lookup v ss of -> Just valor -> case valor of Tfapp v' ts' -> Tfapp v' (ts'++mts) -> _ -> foldl tapp valor mts -> Nothing -> Tfapp v mts +> let mts = map (substitution ss) ts +> in +> case lookup v ss of +> Just newt -> +> case newt of +> Tfapp v' ts' -> Tfapp v' (ts'++mts) +> Tvar v' -> Tfapp v' mts +> _ -> foldl tapp newt mts +> Nothing -> Tfapp v mts > Tcapp cons ts -> > let > nts = map (substitution ss) ts @@ -378,6 +380,7 @@ > equalTerms tbl (Tpar t0) (Tpar t1) = equalTerms tbl t0 t1 > equalTerms tbl (Tapp (Tvar v0) t0) t1 = equalTerms tbl (Tfapp v0 [t0]) t1 > equalTerms tbl t0 (Tapp (Tvar v1) t1) = equalTerms tbl t0 (Tfapp v1 [t1]) +> equalTerms tbl Tbottom Tbottom = Nothing > equalTerms _ t0 t1 = Just (t0,t1) > zipPatterns :: Pattern -> Pattern -> [(Variable, Variable)] -> [(Variable, Variable)] diff --git a/hfusion.cabal b/hfusion.cabal --- a/hfusion.cabal +++ b/hfusion.cabal @@ -1,5 +1,5 @@ name: hfusion -version: 0.0.5.1 +version: 0.0.6 build-type: Simple cabal-version: >= 1.6 license: BSD3 @@ -17,7 +17,7 @@ library - build-depends: base<5, mtl, haskell-src, haskell98, containers, pretty + build-depends: base<5, mtl, haskell-src, haskell98, containers, pretty, syb exposed-modules: HFusion.HFusion, HFusion.CHANGELOG other-modules: @@ -42,10 +42,10 @@ source-repository head type: darcs - location: http://www.fing.edu.uy/inco/proyectos/fusion/darcs/hfusion/ + location: http://patch-tag.com/r/facundo/hfusion source-repository this type: darcs - location: http://www.fing.edu.uy/inco/proyectos/fusion/darcs/hfusion/ - tag: 0.0.5.1 + location: http://patch-tag.com/r/facundo/hfusion + tag: 0.0.6