mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-20 08:32:50 -06:00
Koji's bug fixed
This commit is contained in:
@@ -26,13 +26,16 @@ import GF.Data.Operations
|
|||||||
import GF.Grammar.Abstract
|
import GF.Grammar.Abstract
|
||||||
import GF.Grammar.PrGrammar
|
import GF.Grammar.PrGrammar
|
||||||
import GF.Grammar.LookAbs
|
import GF.Grammar.LookAbs
|
||||||
import GF.Grammar.PatternMatch
|
|
||||||
import GF.Grammar.Compute
|
import GF.Grammar.Compute
|
||||||
|
|
||||||
import Debug.Trace
|
import Debug.Trace
|
||||||
|
import Data.List(intersperse)
|
||||||
import Control.Monad (liftM, liftM2)
|
import Control.Monad (liftM, liftM2)
|
||||||
|
|
||||||
|
-- for debugging
|
||||||
|
tracd m t = t
|
||||||
|
-- tracd = trace
|
||||||
|
|
||||||
compute :: GFCGrammar -> Exp -> Err Exp
|
compute :: GFCGrammar -> Exp -> Err Exp
|
||||||
compute = computeAbsTerm
|
compute = computeAbsTerm
|
||||||
|
|
||||||
@@ -53,23 +56,24 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
|
|||||||
let vv' = yy ++ vv
|
let vv' = yy ++ vv
|
||||||
aa' <- mapM (compt vv') aa
|
aa' <- mapM (compt vv') aa
|
||||||
case look f of
|
case look f of
|
||||||
Just (Eqs eqs) -> ----trace ("matching" +++ prt f) $
|
Just (Eqs eqs) -> tracd ("\nmatching" +++ prt f) $
|
||||||
case findMatch eqs aa' of
|
case findMatch eqs aa' of
|
||||||
Ok (d,g) -> do
|
Ok (d,g) -> do
|
||||||
let (xs,ts) = unzip g
|
--- let (xs,ts) = unzip g
|
||||||
ts' <- alphaFreshAll vv' ts ---
|
--- ts' <- alphaFreshAll vv' ts
|
||||||
let g' = zip xs ts'
|
let g' = g --- zip xs ts'
|
||||||
d' <- compt vv' $ substTerm vv' g' d
|
d' <- compt vv' $ substTerm vv' g' d
|
||||||
return $ mkAbs yy $ d'
|
tracd ("by Egs:" +++ prt d') $ return $ mkAbs yy $ d'
|
||||||
_ -> ---- trace ("no match" +++ prt t') $
|
_ -> tracd ("no match" +++ prt t') $
|
||||||
do
|
do
|
||||||
let v = mkApp f aa'
|
let v = mkApp f aa'
|
||||||
return $ mkAbs yy $ v
|
return $ mkAbs yy $ v
|
||||||
Just d -> do
|
Just d -> tracd ("define" +++ prt t') $ do
|
||||||
da <- compt vv' $ mkApp d aa'
|
da <- compt vv' $ mkApp d aa'
|
||||||
return $ mkAbs yy $ da
|
return $ mkAbs yy $ da
|
||||||
_ -> do
|
_ -> 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
|
look t = case t of
|
||||||
(Q m f) -> case lookd m f 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 :: [Ident] -> Exp -> Exp
|
||||||
beta vv c = case c of
|
beta vv c = case c of
|
||||||
Let (x,(_,a)) b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b)
|
Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b)
|
||||||
where xvv = (x,beta vv a)
|
|
||||||
App f a ->
|
App f a ->
|
||||||
let (a',f') = (beta vv a, beta vv f) in
|
let (a',f') = (beta vv a, beta vv f) in
|
||||||
case f' of
|
case f' of
|
||||||
Abs x b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b)
|
Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
|
||||||
where xvv = (x,beta vv a)
|
|
||||||
_ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
|
_ -> (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)
|
Prod x a b -> Prod x (beta vv a) (beta (x:vv) b)
|
||||||
Abs x b -> Abs x (beta (x:vv) b)
|
Abs x b -> Abs x (beta (x:vv) b)
|
||||||
_ -> c
|
_ -> 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]
|
||||||
|
|||||||
Reference in New Issue
Block a user