From 7db4b641ce6abe90dd404459cd5eccb6e67f618c Mon Sep 17 00:00:00 2001 From: krasimir Date: Wed, 20 May 2009 21:03:56 +0000 Subject: refactor the PGF.Expr type and the evaluation of abstract expressions --- src/GF/Compile/AbsCompute.hs | 9 ++------- src/GF/Compile/CheckGrammar.hs | 29 ++++++++--------------------- src/GF/Compile/GFCCtoJS.hs | 2 +- src/GF/Compile/GFCCtoProlog.hs | 29 +++++++++++++++-------------- src/GF/Compile/GenerateFCFG.hs | 8 ++++---- src/GF/Compile/GeneratePMCFG.hs | 2 +- src/GF/Compile/GrammarToGFCC.hs | 24 +++++++++++++----------- src/GF/Compile/PGFPretty.hs | 2 +- src/GF/Compile/Rename.hs | 6 ++---- src/GF/Compile/TC.hs | 7 +------ src/GF/Compile/TypeCheck.hs | 13 +++++++------ src/GF/Compile/Update.hs | 14 ++++++-------- 12 files changed, 61 insertions(+), 84 deletions(-) (limited to 'src/GF/Compile') diff --git a/src/GF/Compile/AbsCompute.hs b/src/GF/Compile/AbsCompute.hs index 8546dc3bc..ce3528b68 100644 --- a/src/GF/Compile/AbsCompute.hs +++ b/src/GF/Compile/AbsCompute.hs @@ -42,7 +42,7 @@ computeAbsTerm :: Grammar -> Exp -> Err Exp computeAbsTerm gr = computeAbsTermIn (lookupAbsDef gr) [] -- | a hack to make compute work on source grammar as well -type LookDef = Ident -> Ident -> Err (Maybe Term) +type LookDef = Ident -> Ident -> Err (Maybe [Equation]) computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where @@ -55,7 +55,7 @@ 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) -> tracd ("\nmatching" +++ prt f) $ + Just eqs -> tracd ("\nmatching" +++ prt f) $ case findMatch eqs aa' of Ok (d,g) -> do --- let (xs,ts) = unzip g @@ -67,19 +67,14 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where do let v = mkApp f aa' return $ mkAbs yy $ v - Just d -> tracd ("define" +++ prt t') $ do - da <- compt vv' $ mkApp d aa' - return $ mkAbs yy $ da _ -> do 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 - Ok (Just EData) -> Nothing -- canonical --- should always be QC Ok md -> md _ -> Nothing - Eqs _ -> return t ---- for nested fn _ -> Nothing beta :: [Ident] -> Exp -> Exp diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs index 9947de64f..59961e0cd 100644 --- a/src/GF/Compile/CheckGrammar.hs +++ b/src/GF/Compile/CheckGrammar.hs @@ -124,16 +124,14 @@ checkAbsInfo st m mo (c,info) = do AbsCat (Just cont) _ -> mkCheck "category" $ checkContext st cont ---- also cstrs AbsFun (Just typ0) md -> do - typ <- compAbsTyp [] typ0 -- to calculate let definitions - mkCheck "type of function" $ checkTyp st typ - md' <- case md of - Just d -> do - let d' = elimTables d ----- mkCheckWarn "definition of function" $ checkEquation st (m,c) d' - mkCheck "definition of function" $ checkEquation st (m,c) d' - return $ Just d' - _ -> return md - return $ (c,AbsFun (Just typ) md') + typ <- compAbsTyp [] typ0 -- to calculate let definitions + mkCheck "type of function" $ + checkTyp st typ + case md of + Just eqs -> mkCheck "definition of function" $ + checkDef st (m,c) typ eqs + Nothing -> return (c,info) + return $ (c,AbsFun (Just typ) md) _ -> return (c,info) where mkCheck cat ss = case ss of @@ -161,17 +159,6 @@ checkAbsInfo st m mo (c,info) = do Abs _ _ -> return t _ -> composOp (compAbsTyp g) t - elimTables e = case e of - S t a -> elimSel (elimTables t) (elimTables a) - T _ cs -> Eqs [(elimPatt p, elimTables t) | (p,t) <- cs] - _ -> composSafeOp elimTables e - elimPatt p = case p of - PR lps -> map snd lps - _ -> [p] - elimSel t a = case a of - R fs -> mkApp t (map (snd . snd) fs) - _ -> mkApp t [a] - checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info) checkCompleteGrammar gr abs cnc = do let jsa = jments abs diff --git a/src/GF/Compile/GFCCtoJS.hs b/src/GF/Compile/GFCCtoJS.hs index c8e4e0e4b..7fbe06c98 100644 --- a/src/GF/Compile/GFCCtoJS.hs +++ b/src/GF/Compile/GFCCtoJS.hs @@ -34,7 +34,7 @@ pgf2js pgf = abstract2js :: String -> Abstr -> JS.Expr abstract2js start ds = new "GFAbstract" [JS.EStr start, JS.EObj $ map absdef2js (Map.assocs (funs ds))] -absdef2js :: (CId,(Type,Expr)) -> JS.Property +absdef2js :: (CId,(Type,[Equation])) -> JS.Property absdef2js (f,(typ,_)) = let (args,cat) = M.catSkeleton typ in JS.Prop (JS.IdentPropName (JS.Ident (prCId f))) (new "Type" [JS.EArray [JS.EStr (prCId x) | x <- args], JS.EStr (prCId cat)]) diff --git a/src/GF/Compile/GFCCtoProlog.hs b/src/GF/Compile/GFCCtoProlog.hs index 4e1ccfba6..dec6b5412 100644 --- a/src/GF/Compile/GFCCtoProlog.hs +++ b/src/GF/Compile/GFCCtoProlog.hs @@ -71,17 +71,17 @@ plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) args = reverse [EVar x | (_,x) <- subst] typ = wildcardUnusedVars $ DTyp hypos' cat args -plFun :: (CId, (Type, Expr)) -> String +plFun :: (CId, (Type, [Equation])) -> String plFun (fun, (typ, _)) = plFact "fun" (plp fun : plTypeWithHypos typ') where typ' = wildcardUnusedVars $ snd $ alphaConvert emptyEnv typ plTypeWithHypos :: Type -> [String] plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos] -plFundef :: (CId, (Type, Expr)) -> [String] -plFundef (fun, (_, EEq [])) = [] -plFundef (fun, (_, fundef)) = [plFact "def" [plp fun, plp fundef']] - where fundef' = snd $ alphaConvert emptyEnv fundef +plFundef :: (CId, (Type, [Equation])) -> [String] +plFundef (fun, (_, [])) = [] +plFundef (fun, (_, eqs)) = [plFact "def" [plp fun, plp fundef']] + where fundef' = snd $ alphaConvert emptyEnv eqs ---------------------------------------------------------------------- @@ -122,8 +122,14 @@ instance PLPrint Expr where plp (EApp e e') = plOper " * " (plp e) (plp e') plp (ELit lit) = plp lit plp (EMeta n) = "Meta_" ++ show n - plp (EEq eqs) = plList [plOper ":" (plp patterns) (plp result) | - Equ patterns result <- eqs] + +instance PLPrint Patt where + plp (PVar x) = plp x + plp (PApp f ps) = plOper " * " (plp f) (plp ps) + plp (PLit lit) = plp lit + +instance PLPrint Equation where + plp (Equ patterns result) = plOper ":" (plp patterns) (plp result) instance PLPrint Term where plp (S terms) = plTerm "s" [plp terms] @@ -267,17 +273,14 @@ instance AlphaConvert Expr where where (env', e1') = alphaConvert env e1 (env'', e2') = alphaConvert env' e2 alphaConvert env expr@(EVar i) = (env, maybe expr EVar (lookup i (snd env))) - alphaConvert env (EEq eqs) = (env', EEq eqs') - where (env', eqs') = alphaConvert env eqs alphaConvert env expr = (env, expr) -- pattern variables are not alpha converted -- (but they probably should be...) instance AlphaConvert Equation where alphaConvert env@(_,subst) (Equ patterns result) - = ((ctr,subst), Equ patterns' result') - where (env', patterns') = alphaConvert env patterns - ((ctr,_), result') = alphaConvert env' result + = ((ctr,subst), Equ patterns result') + where ((ctr,_), result') = alphaConvert env result ---------------------------------------------------------------------- -- translate unused variables to wildcards @@ -295,6 +298,4 @@ wildcardUnusedVars typ@(DTyp hypos cat args) = DTyp hypos' cat args unusedInExpr x (EAbs y e) = unusedInExpr x e unusedInExpr x (EApp e e') = unusedInExpr x e && unusedInExpr x e' unusedInExpr x (EVar y) = x/=y - unusedInExpr x (EEq eqs) = and [all (unusedInExpr x) (result:patterns) | - Equ patterns result <- eqs] unusedInExpr x expr = True diff --git a/src/GF/Compile/GenerateFCFG.hs b/src/GF/Compile/GenerateFCFG.hs index bb8ba9452..254720e04 100644 --- a/src/GF/Compile/GenerateFCFG.hs +++ b/src/GF/Compile/GenerateFCFG.hs @@ -43,7 +43,7 @@ convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats' cats = lincats cnc (abs_defs',conc',cats') = expandHOAS abs_defs conc cats -expandHOAS :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ([(CId,(Type,Expr))],TermMap,TermMap) +expandHOAS :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,[Equation]))],TermMap,TermMap) expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, Map.unions [lins, hoLins, varLins], Map.unions [lincats, hoLincats, varLincat]) @@ -59,14 +59,14 @@ expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, hoCats = sortNub (map snd hoTypes) -- for each Cat with N bindings, we add a new category _NCat -- each new category contains a single function __NCat : Cat -> _Var -> ... -> _Var -> _NCat - hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),EEq [])) | ty@(n,c) <- hoTypes] + hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),[])) | ty@(n,c) <- hoTypes] -- lincats for the new categories hoLincats = Map.fromList [(catName ty, modifyRec (++ replicate n (S [])) (lincatOf c)) | ty@(n,c) <- hoTypes] -- linearizations of the new functions, lin __NCat v_0 ... v_n-1 x = { s1 = x.s1; ...; sk = x.sk; $0 = v_0.s ... hoLins = Map.fromList [ (funName ty, mkLin c n) | ty@(n,c) <- hoTypes] where mkLin c n = modifyRec (\fs -> [P (V 0) (C j) | j <- [0..length fs-1]] ++ [P (V i) (C 0) | i <- [1..n]]) (lincatOf c) -- for each Cat, we a add a fun _Var_Cat : _Var -> Cat - varFuns = [(varFunName cat, (cftype [varCat] cat,EEq [])) | cat <- hoCats] + varFuns = [(varFunName cat, (cftype [varCat] cat,[])) | cat <- hoCats] -- linearizations of the _Var_Cat functions varLins = Map.fromList [(varFunName cat, R [P (V 0) (C 0)]) | cat <- hoCats] -- lincat for the _Var category @@ -98,7 +98,7 @@ fixHoasFuns pinfo = pinfo{functions=mkArray [FFun (fixName n) prof lins | FFun n | BS.pack "_Var_" `BS.isPrefixOf` n = wildCId fixName n = n -convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ParserInfo +convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo convert abs_defs cnc_defs cat_defs = getParserInfo (loop grammarEnv) where srules = [ diff --git a/src/GF/Compile/GeneratePMCFG.hs b/src/GF/Compile/GeneratePMCFG.hs index 3da4d9763..772adf81a 100644 --- a/src/GF/Compile/GeneratePMCFG.hs +++ b/src/GF/Compile/GeneratePMCFG.hs @@ -38,7 +38,7 @@ convertConcrete abs cnc = convert abs_defs conc cats conc = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient" cats = lincats cnc -convert :: [(CId,(Type,Expr))] -> TermMap -> TermMap -> ParserInfo +convert :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ParserInfo convert abs_defs cnc_defs cat_defs = let env = expandHOAS abs_defs cnc_defs cat_defs (emptyGrammarEnv cnc_defs cat_defs) in getParserInfo (List.foldl' (convertRule cnc_defs) env pfrules) diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index 272692be7..e1c5b8fb7 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/src/GF/Compile/GrammarToGFCC.hs @@ -68,9 +68,9 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) = abs = D.Abstr aflags funs cats catfuns gflags = Map.empty aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)] - mkDef pty = case pty of - Just t -> mkExp t - _ -> CM.primNotion + + mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs] + mkDef Nothing = [] -- concretes lfuns = [(f', (mkType ty, mkDef pty)) | @@ -119,9 +119,7 @@ mkType t = case GM.typeForm t of Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args) mkExp :: A.Term -> C.Expr -mkExp t = case t of - A.Eqs eqs -> C.EEq [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs] - _ -> case GM.termForm t of +mkExp t = case GM.termForm t of Ok (xs,c,args) -> mkAbs xs (mkApp c (map mkExp args)) where mkAbs xs t = foldr (C.EAbs . i2i) t xs @@ -134,11 +132,15 @@ mkExp t = case t of K s -> C.ELit (C.LStr s) Meta (MetaSymb i) -> C.EMeta i _ -> C.EMeta 0 - mkPatt p = case p of - A.PP _ c ps -> foldl C.EApp (C.EVar (i2i c)) (map mkPatt ps) - A.PV x -> C.EVar (i2i x) - A.PW -> C.EVar wildCId - A.PInt i -> C.ELit (C.LInt i) + +mkPatt p = case p of + A.PP _ c ps -> C.PApp (i2i c) (map mkPatt ps) + A.PV x -> C.PVar (i2i x) + A.PW -> C.PWild + A.PInt i -> C.PLit (C.LInt i) + A.PFloat f -> C.PLit (C.LFlt f) + A.PString s -> C.PLit (C.LStr s) + mkContext :: A.Context -> [C.Hypo] mkContext hyps = [C.Hyp (i2i x) (mkType ty) | (x,ty) <- hyps] diff --git a/src/GF/Compile/PGFPretty.hs b/src/GF/Compile/PGFPretty.hs index b6d8f514b..178f8866b 100644 --- a/src/GF/Compile/PGFPretty.hs +++ b/src/GF/Compile/PGFPretty.hs @@ -31,7 +31,7 @@ prCat :: CId -> [Hypo] -> Doc prCat c h | isLiteralCat c = empty | otherwise = text "cat" <+> text (prCId c) -prFun :: CId -> (Type,Expr) -> Doc +prFun :: CId -> (Type,[Equation]) -> Doc prFun f (t,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t prType :: Type -> Doc diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs index c00e31d95..8011d2171 100644 --- a/src/GF/Compile/Rename.hs +++ b/src/GF/Compile/Rename.hs @@ -116,7 +116,7 @@ renameIdentPatt env p = do info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo info2status mq (c,i) = case i of - AbsFun _ (Just EData) -> maybe Con QC mq + AbsFun _ Nothing -> maybe Con QC mq ResValue _ -> maybe Con QC mq ResParam _ -> maybe Con QC mq AnyInd True m -> maybe Con (const (QC m)) mq @@ -156,8 +156,7 @@ renameInfo mo status (i,info) = errIn liftM ((,) i) $ case info of AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco) (renPerh (mapM rent) pfs) - AbsFun pty ptr -> liftM2 AbsFun (ren pty) (ren ptr) - + AbsFun pty ptr -> liftM2 AbsFun (ren pty) (renPerh (mapM (renameEquation status [])) ptr) ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr) ResOverload os tysts -> liftM (ResOverload os) (mapM (pairM rent) tysts) @@ -191,7 +190,6 @@ renameTerm env vars = ren vars where Con _ -> renid trm Q _ _ -> renid trm QC _ _ -> renid trm - Eqs eqs -> liftM Eqs $ mapM (renameEquation env vars) eqs T i cs -> do i' <- case i of TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs index 5ecbdf8e5..a56c3b86d 100644 --- a/src/GF/Compile/TC.hs +++ b/src/GF/Compile/TC.hs @@ -16,6 +16,7 @@ module GF.Compile.TC (AExp(..), Theory, checkExp, inferExp, + checkBranch, eqVal, whnf ) where @@ -122,7 +123,6 @@ checkExp th tenv@(k,rho,gamma) e ty = do let v = VGen k case e of Meta m -> return $ (AMeta m typ,[]) - EData -> return $ (AData typ,[]) Abs x t -> case typ of VClos env (Prod y a b) -> do @@ -132,11 +132,6 @@ checkExp th tenv@(k,rho,gamma) e ty = do return (AAbs x a' t', cs) _ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ - Eqs es -> do - bcs <- mapM (\b -> checkBranch th tenv b typ) es - let (bs,css) = unzip bcs - return (AEqs bs, concat css) - Prod x a b -> do testErr (typ == vType) "expected Type" (a',csa) <- checkType th tenv a diff --git a/src/GF/Compile/TypeCheck.hs b/src/GF/Compile/TypeCheck.hs index e824a0cfe..71fe5b067 100644 --- a/src/GF/Compile/TypeCheck.hs +++ b/src/GF/Compile/TypeCheck.hs @@ -15,7 +15,7 @@ module GF.Compile.TypeCheck (-- * top-level type checking functions; TC should not be called directly. checkContext, checkTyp, - checkEquation, + checkDef, checkConstrs, ) where @@ -71,11 +71,12 @@ checkContext st = checkTyp st . cont2exp checkTyp :: Grammar -> Type -> [String] checkTyp gr typ = err singleton prConstrs $ justTypeCheck gr typ vType -checkEquation :: Grammar -> Fun -> Term -> [String] -checkEquation gr (m,fun) def = err singleton prConstrs $ do - typ <- lookupFunType gr m fun - cs <- justTypeCheck gr def (vClos typ) - return $ filter notJustMeta cs +checkDef :: Grammar -> Fun -> Type -> [Equation] -> [String] +checkDef gr (m,fun) typ eqs = err singleton prConstrs $ do + bcs <- mapM (\b -> checkBranch (grammar2theory gr) (initTCEnv []) b (type2val typ)) eqs + let (bs,css) = unzip bcs + (constrs,_) <- unifyVal (concat css) + return $ filter notJustMeta constrs checkConstrs :: Grammar -> Cat -> [Ident] -> [String] checkConstrs gr cat _ = [] ---- check constructors! diff --git a/src/GF/Compile/Update.hs b/src/GF/Compile/Update.hs index ba4a91874..0893db561 100644 --- a/src/GF/Compile/Update.hs +++ b/src/GF/Compile/Update.hs @@ -163,7 +163,7 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old (b,n') = case info of ResValue _ -> (True,n) ResParam _ -> (True,n) - AbsFun _ (Just EData) -> (True,n) + AbsFun _ Nothing -> (True,n) AnyInd b k -> (b,k) _ -> (False,n) ---- canonical in Abs @@ -203,13 +203,11 @@ unifMaybe (Just p1) (Just p2) | p1==p2 = return (Just p1) | otherwise = fail "" -unifAbsDefs :: Maybe Term -> Maybe Term -> Err (Maybe Term) -unifAbsDefs p1 p2 = case (p1,p2) of - (Nothing, _) -> return p2 - (_, Nothing) -> return p1 - (Just (Eqs bs), Just (Eqs ds)) - -> return $ Just $ Eqs $ bs ++ ds --- order! - _ -> fail "definitions" +unifAbsDefs :: Maybe [Equation] -> Maybe [Equation] -> Err (Maybe [Equation]) +unifAbsDefs Nothing Nothing = return Nothing +unifAbsDefs (Just _ ) Nothing = fail "" +unifAbsDefs Nothing (Just _ ) = fail "" +unifAbsDefs (Just xs) (Just ys) = return (Just (xs ++ ys)) unifConstrs :: Maybe [Term] -> Maybe [Term] -> Err (Maybe [Term]) unifConstrs p1 p2 = case (p1,p2) of -- cgit v1.2.3