From 60f678f221d05c288dab67b56cff9e06a36086ae Mon Sep 17 00:00:00 2001 From: aarne Date: Mon, 18 Dec 2006 15:25:00 +0000 Subject: [PATCH] Koji's bug fixed --- src/GF/Grammar/AbsCompute.hs | 78 +++++++++++++++++++++++++++++------- 1 file changed, 64 insertions(+), 14 deletions(-) diff --git a/src/GF/Grammar/AbsCompute.hs b/src/GF/Grammar/AbsCompute.hs index 593c6d96f..57e21f1dd 100644 --- a/src/GF/Grammar/AbsCompute.hs +++ b/src/GF/Grammar/AbsCompute.hs @@ -26,13 +26,16 @@ import GF.Data.Operations import GF.Grammar.Abstract import GF.Grammar.PrGrammar import GF.Grammar.LookAbs -import GF.Grammar.PatternMatch import GF.Grammar.Compute import Debug.Trace - +import Data.List(intersperse) import Control.Monad (liftM, liftM2) +-- for debugging +tracd m t = t +-- tracd = trace + compute :: GFCGrammar -> Exp -> Err Exp compute = computeAbsTerm @@ -53,23 +56,24 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where let vv' = yy ++ vv aa' <- mapM (compt vv') aa case look f of - Just (Eqs eqs) -> ----trace ("matching" +++ prt f) $ + Just (Eqs eqs) -> tracd ("\nmatching" +++ prt f) $ case findMatch eqs aa' of Ok (d,g) -> do - let (xs,ts) = unzip g - ts' <- alphaFreshAll vv' ts --- - let g' = zip xs ts' + --- let (xs,ts) = unzip g + --- ts' <- alphaFreshAll vv' ts + let g' = g --- zip xs ts' d' <- compt vv' $ substTerm vv' g' d - return $ mkAbs yy $ d' - _ -> ---- trace ("no match" +++ prt t') $ + tracd ("by Egs:" +++ prt d') $ return $ mkAbs yy $ d' + _ -> tracd ("no match" +++ prt t') $ do let v = mkApp f aa' return $ mkAbs yy $ v - Just d -> do + Just d -> tracd ("define" +++ prt t') $ do da <- compt vv' $ mkApp d aa' return $ mkAbs yy $ da _ -> do - return $ mkAbs yy $ mkApp f aa' + let t2 = mkAbs yy $ mkApp f aa' + tracd ("not defined" +++ prt_ t2) $ return t2 look t = case t of (Q m f) -> case lookd m f of @@ -81,15 +85,61 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where beta :: [Ident] -> Exp -> Exp beta vv c = case c of - Let (x,(_,a)) b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) - where xvv = (x,beta vv a) + Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b) App f a -> let (a',f') = (beta vv a, beta vv f) in case f' of - Abs x b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) - where xvv = (x,beta vv a) + Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) _ -> (if a'==a && f'==f then id else beta vv) $ App f' a' Prod x a b -> Prod x (beta vv a) (beta (x:vv) b) Abs x b -> Abs x (beta (x:vv) b) _ -> c +-- special version of pattern matching, to deal with comp under lambda + +findMatch :: [([Patt],Term)] -> [Term] -> Err (Term, Substitution) +findMatch cases terms = case cases of + [] -> Bad $"no applicable case for" +++ unwords (intersperse "," (map prt terms)) + (patts,_):_ | length patts /= length terms -> + Bad ("wrong number of args for patterns :" +++ + unwords (map prt patts) +++ "cannot take" +++ unwords (map prt terms)) + (patts,val):cc -> case mapM tryMatch (zip patts terms) of + Ok substs -> return (tracd ("value" +++ prt_ val) val, concat substs) + _ -> findMatch cc terms + +tryMatch :: (Patt, Term) -> Err [(Ident, Term)] +tryMatch (p,t) = do + t' <- termForm t + trym p t' + where + + trym p t' = err (\s -> tracd s (Bad s)) (\t -> tracd (prtm p t) (return t)) $ ---- + case (p,t') of + (PV IW, _) | notMeta t -> return [] -- optimization with wildcard + (PV x, _) | notMeta t -> return [(x,t)] + (PString s, ([],K i,[])) | s==i -> return [] + (PInt s, ([],EInt i,[])) | s==i -> return [] + (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding? + (PP q p pp, ([], QC r f, tt)) | + p `eqStrIdent` f && length pp == length tt -> do + matches <- mapM tryMatch (zip pp tt) + return (concat matches) + (PP q p pp, ([], Q r f, tt)) | + p `eqStrIdent` f && length pp == length tt -> do + matches <- mapM tryMatch (zip pp tt) + return (concat matches) + (PT _ p',_) -> trym p' t' + (_, ([],Alias _ _ d,[])) -> tryMatch (p,d) + (PAs x p',_) -> do + subst <- trym p' t' + return $ (x,t) : subst + _ -> Bad ("no match in pattern" +++ prt p +++ "for" +++ prt t) + + notMeta e = case e of + Meta _ -> False + App f a -> notMeta f && notMeta a + Abs _ b -> notMeta b + _ -> True + + prtm p g = + prt p +++ ":" ++++ unwords [" " ++ prt_ x +++ "=" +++ prt_ y +++ ";" | (x,y) <- g]