From f9c877eec6e72827b860be3f95b6c33d5835facb Mon Sep 17 00:00:00 2001 From: krasimir Date: Fri, 22 May 2009 18:54:51 +0000 Subject: [PATCH] some work on evaluation with abstract expressions in PGF --- src/GF/Command/Commands.hs | 2 +- src/GF/Compile/AbsCompute.hs | 4 +- src/GF/Compile/CheckGrammar.hs | 50 +++++------ src/GF/Compile/GFCCtoHaskell.hs | 2 +- src/GF/Compile/GFCCtoJS.hs | 4 +- src/GF/Compile/GFCCtoProlog.hs | 10 +-- src/GF/Compile/GenerateFCFG.hs | 14 ++-- src/GF/Compile/GeneratePMCFG.hs | 8 +- src/GF/Compile/GrammarToGFCC.hs | 9 +- src/GF/Compile/PGFPretty.hs | 4 +- src/GF/Compile/Rename.hs | 4 +- src/GF/Compile/TC.hs | 1 - src/GF/Compile/Update.hs | 14 +++- src/GF/Grammar/Binary.hs | 4 +- src/GF/Grammar/Grammar.hs | 8 +- src/GF/Grammar/Lookup.hs | 18 ++-- src/GF/Grammar/Macros.hs | 3 +- src/GF/Grammar/Parser.y | 20 ++--- src/GF/Grammar/Printer.hs | 2 +- src/GF/Source/CF.hs | 2 +- src/GF/Source/GrammarToSource.hs | 6 +- src/GF/Source/SourceToGrammar.hs | 2 +- src/PGF/Binary.hs | 2 +- src/PGF/Data.hs | 2 +- src/PGF/Expr.hs | 116 +++++++++++++++----------- src/PGF/Macros.hs | 12 +-- src/PGF/Paraphrase.hs | 2 +- src/PGF/ShowLinearize.hs | 2 +- src/PGF/TypeCheck.hs | 20 +++-- testsuite/update/ArrityCheck.gf | 5 ++ testsuite/update/ArrityCheck.gfs | 1 + testsuite/update/ArrityCheck.gfs.gold | 8 ++ 32 files changed, 207 insertions(+), 154 deletions(-) create mode 100644 testsuite/update/ArrityCheck.gf create mode 100644 testsuite/update/ArrityCheck.gfs create mode 100644 testsuite/update/ArrityCheck.gfs.gold diff --git a/src/GF/Command/Commands.hs b/src/GF/Command/Commands.hs index f29fd3d41..1c0a3c2f9 100644 --- a/src/GF/Command/Commands.hs +++ b/src/GF/Command/Commands.hs @@ -600,7 +600,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [ exec = \opts arg -> do case arg of [Fun id []] -> case Map.lookup id (funs (abstract pgf)) of - Just (ty,eqs) -> return $ fromString $ + Just (ty,_,eqs) -> return $ fromString $ render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$ if null eqs then empty diff --git a/src/GF/Compile/AbsCompute.hs b/src/GF/Compile/AbsCompute.hs index a4a8d803e..918682ecc 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 [Equation]) +type LookDef = Ident -> Ident -> Err (Maybe Int,Maybe [Equation]) computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where @@ -73,7 +73,7 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where look t = case t of (Q m f) -> case lookd m f of - Ok md -> md + Ok (_,md) -> md _ -> Nothing _ -> Nothing diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs index bad6bcbcf..8fa5d25b6 100644 --- a/src/GF/Compile/CheckGrammar.hs +++ b/src/GF/Compile/CheckGrammar.hs @@ -123,7 +123,7 @@ checkAbsInfo st m mo (c,info) = do case info of AbsCat (Just cont) _ -> mkCheck "category" $ checkContext st cont ---- also cstrs - AbsFun (Just typ0) md -> do + AbsFun (Just typ0) ma md -> do typ <- compAbsTyp [] typ0 -- to calculate let definitions mkCheck "type of function" $ checkTyp st typ @@ -131,7 +131,7 @@ checkAbsInfo st m mo (c,info) = do Just eqs -> mkCheck "definition of function" $ checkDef st (m,c) typ eqs Nothing -> return (c,info) - return $ (c,AbsFun (Just typ) md) + return $ (c,AbsFun (Just typ) ma md) _ -> return (c,info) where mkCheck cat ss = case ss of @@ -181,28 +181,28 @@ checkCompleteGrammar gr abs cnc = do CncCat _ _ _ -> True _ -> False checkOne js i@(c,info) = case info of - AbsFun (Just ty) _ -> do let mb_def = do - (cxt,(_,i),_) <- typeForm ty - info <- lookupIdent i js - info <- case info of - (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i - return info - _ -> return info - case info of - CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt) - _ -> Bad "no def lin" - case lookupIdent c js of - Ok (CncFun _ (Just _) _ ) -> return js - Ok (CncFun cty Nothing pn) -> - case mb_def of - Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js - Bad _ -> do checkWarn $ "no linearization of" +++ prt c - return js - _ -> do - case mb_def of - Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js - Bad _ -> do checkWarn $ "no linearization of" +++ prt c - return js + AbsFun (Just ty) _ _ -> do let mb_def = do + (cxt,(_,i),_) <- typeForm ty + info <- lookupIdent i js + info <- case info of + (AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i + return info + _ -> return info + case info of + CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt) + _ -> Bad "no def lin" + case lookupIdent c js of + Ok (CncFun _ (Just _) _ ) -> return js + Ok (CncFun cty Nothing pn) -> + case mb_def of + Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js + Bad _ -> do checkWarn $ "no linearization of" +++ prt c + return js + _ -> do + case mb_def of + Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js + Bad _ -> do checkWarn $ "no linearization of" +++ prt c + return js AbsCat (Just _) _ -> case lookupIdent c js of Ok (AnyInd _ _) -> return js Ok (CncCat (Just _) _ _) -> return js @@ -1115,7 +1115,7 @@ allDependencies ism b = ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont] CncCat pty _ _ -> [pty] CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type)) - AbsFun pty ptr -> [pty] --- ptr is def, which can be mutual + AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual AbsCat (Just co) _ -> [Just ty | (_,ty) <- co] _ -> [] diff --git a/src/GF/Compile/GFCCtoHaskell.hs b/src/GF/Compile/GFCCtoHaskell.hs index a8fd321b0..675cecad5 100644 --- a/src/GF/Compile/GFCCtoHaskell.hs +++ b/src/GF/Compile/GFCCtoHaskell.hs @@ -201,7 +201,7 @@ hSkeleton gr = fns = groupBy valtypg (sortBy valtyps (map jty (Map.assocs (funs (abstract gr))))) valtyps (_, (_,x)) (_, (_,y)) = compare x y valtypg (_, (_,x)) (_, (_,y)) = x == y - jty (f,(ty,_)) = (f,catSkeleton ty) + jty (f,(ty,_,_)) = (f,catSkeleton ty) updateSkeleton :: OIdent -> HSkeleton -> (OIdent, [OIdent]) -> HSkeleton updateSkeleton cat skel rule = diff --git a/src/GF/Compile/GFCCtoJS.hs b/src/GF/Compile/GFCCtoJS.hs index 7fbe06c98..8ca321eaa 100644 --- a/src/GF/Compile/GFCCtoJS.hs +++ b/src/GF/Compile/GFCCtoJS.hs @@ -34,8 +34,8 @@ 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,[Equation])) -> JS.Property -absdef2js (f,(typ,_)) = +absdef2js :: (CId,(Type,Int,[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 dec6b5412..48c3e620d 100644 --- a/src/GF/Compile/GFCCtoProlog.hs +++ b/src/GF/Compile/GFCCtoProlog.hs @@ -71,16 +71,16 @@ plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) args = reverse [EVar x | (_,x) <- subst] typ = wildcardUnusedVars $ DTyp hypos' cat args -plFun :: (CId, (Type, [Equation])) -> String -plFun (fun, (typ, _)) = plFact "fun" (plp fun : plTypeWithHypos typ') +plFun :: (CId, (Type, Int, [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, [Equation])) -> [String] -plFundef (fun, (_, [])) = [] -plFundef (fun, (_, eqs)) = [plFact "def" [plp fun, plp fundef']] +plFundef :: (CId, (Type,Int,[Equation])) -> [String] +plFundef (fun, (_,_,[])) = [] +plFundef (fun, (_,_,eqs)) = [plFact "def" [plp fun, plp fundef']] where fundef' = snd $ alphaConvert emptyEnv eqs diff --git a/src/GF/Compile/GenerateFCFG.hs b/src/GF/Compile/GenerateFCFG.hs index 254720e04..7597e71dd 100644 --- a/src/GF/Compile/GenerateFCFG.hs +++ b/src/GF/Compile/GenerateFCFG.hs @@ -43,30 +43,30 @@ convertConcrete abs cnc = fixHoasFuns $ convert abs_defs' conc' cats' cats = lincats cnc (abs_defs',conc',cats') = expandHOAS abs_defs conc cats -expandHOAS :: [(CId,(Type,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,[Equation]))],TermMap,TermMap) +expandHOAS :: [(CId,(Type,Int,[Equation]))] -> TermMap -> TermMap -> ([(CId,(Type,Int,[Equation]))],TermMap,TermMap) expandHOAS funs lins lincats = (funs' ++ hoFuns ++ varFuns, Map.unions [lins, hoLins, varLins], Map.unions [lincats, hoLincats, varLincat]) where -- replace higher-order fun argument types with new categories - funs' = [(f,(fixType ty,e)) | (f,(ty,e)) <- funs] + funs' = [(f,(fixType ty,a,e)) | (f,(ty,a,e)) <- funs] where fixType :: Type -> Type fixType ty = let (ats,rt) = typeSkeleton ty in cftype (map catName ats) rt hoTypes :: [(Int,CId)] - hoTypes = sortNub [(n,c) | (_,(ty,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0] + hoTypes = sortNub [(n,c) | (_,(ty,_,_)) <- funs, (n,c) <- fst (typeSkeleton ty), n > 0] 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),[])) | ty@(n,c) <- hoTypes] + hoFuns = [(funName ty,(cftype (c : replicate n varCat) (catName ty),0,[])) | 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,[])) | cat <- hoCats] + varFuns = [(varFunName cat, (cftype [varCat] cat,0,[])) | 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,12 +98,12 @@ 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,[Equation]))] -> TermMap -> TermMap -> ParserInfo +convert :: [(CId,(Type,Int,[Equation]))] -> TermMap -> TermMap -> ParserInfo convert abs_defs cnc_defs cat_defs = getParserInfo (loop grammarEnv) where srules = [ (XRule id args res (map findLinType args) (findLinType res) term) | - (id, (ty,_)) <- abs_defs, let (args,res) = catSkeleton ty, + (id, (ty,_,_)) <- abs_defs, let (args,res) = catSkeleton ty, term <- maybeToList (Map.lookup id cnc_defs)] findLinType id = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs) diff --git a/src/GF/Compile/GeneratePMCFG.hs b/src/GF/Compile/GeneratePMCFG.hs index 772adf81a..667b403b5 100644 --- a/src/GF/Compile/GeneratePMCFG.hs +++ b/src/GF/Compile/GeneratePMCFG.hs @@ -38,14 +38,14 @@ 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,[Equation]))] -> TermMap -> TermMap -> ParserInfo +convert :: [(CId,(Type,Int,[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) where pfrules = [ (PFRule id args (0,res) (map findLinType args) (findLinType (0,res)) term) | - (id, (ty,_)) <- abs_defs, let (args,res) = typeSkeleton ty, + (id, (ty,_,_)) <- abs_defs, let (args,res) = typeSkeleton ty, term <- maybeToList (Map.lookup id cnc_defs)] findLinType (_,id) = fromMaybe (error $ "No lincat for " ++ show id) (Map.lookup id cat_defs) @@ -320,11 +320,11 @@ expandHOAS abs_defs cnc_defs lincats env = foldl add_varFun (foldl (\env ncat -> add_hoFun (add_hoCat env ncat) ncat) env hoTypes) hoCats where hoTypes :: [(Int,CId)] - hoTypes = sortNub [(n,c) | (_,(ty,_)) <- abs_defs + hoTypes = sortNub [(n,c) | (_,(ty,_,_)) <- abs_defs , (n,c) <- fst (typeSkeleton ty), n > 0] hoCats :: [CId] - hoCats = sortNub [c | (_,(ty,_)) <- abs_defs + hoCats = sortNub [c | (_,(ty,_,_)) <- abs_defs , Hyp _ ty <- case ty of {DTyp hyps val _ -> hyps} , c <- fst (catSkeleton ty)] diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index e1c5b8fb7..14187f04a 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/src/GF/Compile/GrammarToGFCC.hs @@ -71,16 +71,19 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) = mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs] mkDef Nothing = [] + + mkArrity (Just a) = a + mkArrity Nothing = 0 -- concretes - lfuns = [(f', (mkType ty, mkDef pty)) | - (f,AbsFun (Just ty) pty) <- tree2list (M.jments abm), let f' = i2i f] + lfuns = [(f', (mkType ty, mkArrity ma, mkDef pty)) | + (f,AbsFun (Just ty) ma pty) <- tree2list (M.jments abm), let f' = i2i f] funs = Map.fromAscList lfuns lcats = [(i2i c, mkContext cont) | (c,AbsCat (Just cont) _) <- tree2list (M.jments abm)] cats = Map.fromAscList lcats catfuns = Map.fromList - [(cat,[f | (f, (C.DTyp _ c _,_)) <- lfuns, c==cat]) | (cat,_) <- lcats] + [(cat,[f | (f, (C.DTyp _ c _,_,_)) <- lfuns, c==cat]) | (cat,_) <- lcats] cncs = Map.fromList [mkConcr lang (i2i lang) mo | (lang,mo) <- cms] mkConcr lang0 lang mo = diff --git a/src/GF/Compile/PGFPretty.hs b/src/GF/Compile/PGFPretty.hs index 178f8866b..309ce5c31 100644 --- a/src/GF/Compile/PGFPretty.hs +++ b/src/GF/Compile/PGFPretty.hs @@ -31,8 +31,8 @@ prCat :: CId -> [Hypo] -> Doc prCat c h | isLiteralCat c = empty | otherwise = text "cat" <+> text (prCId c) -prFun :: CId -> (Type,[Equation]) -> Doc -prFun f (t,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t +prFun :: CId -> (Type,Int,[Equation]) -> Doc +prFun f (t,_,_) = text "fun" <+> text (prCId f) <+> text ":" <+> prType t prType :: Type -> Doc prType t = parens (hsep (punctuate (text ",") (map (text . prCId) cs))) <+> text "->" <+> text (prCId c) diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs index 87593c0eb..0c9a5c9fe 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 _ Nothing -> 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,7 +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) (renPerh (mapM (renameEquation status [])) ptr) + AbsFun pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr) ResOper pty ptr -> liftM2 ResOper (ren pty) (ren ptr) ResOverload os tysts -> liftM (ResOverload os) (mapM (pairM rent) tysts) diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs index a56c3b86d..fabe7e2a1 100644 --- a/src/GF/Compile/TC.hs +++ b/src/GF/Compile/TC.hs @@ -236,7 +236,6 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ ps2ts k = foldr p2t ([],0,[],k) p2t p (ps,i,g,k) = case p of PW -> (Meta (MetaSymb i) : ps, i+1,g,k) - PV IW -> (Meta (MetaSymb i) : ps, i+1,g,k) PV x -> (Vr x : ps, i, upd x k g,k+1) PString s -> (K s : ps, i, g, k) PInt n -> (EInt n : ps, i, g, k) diff --git a/src/GF/Compile/Update.hs b/src/GF/Compile/Update.hs index 0893db561..ec5161403 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 _ Nothing -> (True,n) + AbsFun _ _ Nothing -> (True,n) AnyInd b k -> (b,k) _ -> (False,n) ---- canonical in Abs @@ -171,8 +171,8 @@ unifyAnyInfo :: Ident -> Info -> Info -> Err Info unifyAnyInfo m i j = case (i,j) of (AbsCat mc1 mf1, AbsCat mc2 mf2) -> liftM2 AbsCat (unifMaybe mc1 mc2) (unifConstrs mf1 mf2) -- adding constrs - (AbsFun mt1 md1, AbsFun mt2 md2) -> - liftM2 AbsFun (unifMaybe mt1 mt2) (unifAbsDefs md1 md2) -- adding defs + (AbsFun mt1 ma1 md1, AbsFun mt2 ma2 md2) -> + liftM3 AbsFun (unifMaybe mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) -- adding defs (ResParam mt1, ResParam mt2) -> liftM ResParam $ unifMaybe mt1 mt2 (ResValue mt1, ResValue mt2) -> @@ -203,6 +203,14 @@ unifMaybe (Just p1) (Just p2) | p1==p2 = return (Just p1) | otherwise = fail "" +unifAbsArrity :: Maybe Int -> Maybe Int -> Err (Maybe Int) +unifAbsArrity Nothing Nothing = return Nothing +unifAbsArrity (Just a ) Nothing = return (Just a ) +unifAbsArrity Nothing (Just a ) = return (Just a ) +unifAbsArrity (Just a1) (Just a2) + | a1==a2 = return (Just a1) + | otherwise = fail "" + unifAbsDefs :: Maybe [Equation] -> Maybe [Equation] -> Err (Maybe [Equation]) unifAbsDefs Nothing Nothing = return Nothing unifAbsDefs (Just _ ) Nothing = fail "" diff --git a/src/GF/Grammar/Binary.hs b/src/GF/Grammar/Binary.hs index 0521ff9c3..18594d4eb 100644 --- a/src/GF/Grammar/Binary.hs +++ b/src/GF/Grammar/Binary.hs @@ -90,7 +90,7 @@ instance Binary Options where instance Binary Info where put (AbsCat x y) = putWord8 0 >> put (x,y) - put (AbsFun x y) = putWord8 1 >> put (x,y) + put (AbsFun x y z) = putWord8 1 >> put (x,y,z) put (ResParam x) = putWord8 2 >> put x put (ResValue x) = putWord8 3 >> put x put (ResOper x y) = putWord8 4 >> put (x,y) @@ -101,7 +101,7 @@ instance Binary Info where get = do tag <- getWord8 case tag of 0 -> get >>= \(x,y) -> return (AbsCat x y) - 1 -> get >>= \(x,y) -> return (AbsFun x y) + 1 -> get >>= \(x,y,z) -> return (AbsFun x y z) 2 -> get >>= \x -> return (ResParam x) 3 -> get >>= \x -> return (ResValue x) 4 -> get >>= \(x,y) -> return (ResOper x y) diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs index 37692ec39..13ddbdb8c 100644 --- a/src/GF/Grammar/Grammar.hs +++ b/src/GF/Grammar/Grammar.hs @@ -41,7 +41,6 @@ module GF.Grammar.Grammar (SourceGrammar, Param, Altern, Substitution, - wildPatt, varLabel, tupleLabel, linLabel, theLinLabel, ident2label, label2ident ) where @@ -80,8 +79,8 @@ type PValues = [Term] -- and indirection to module (/INDIR/) data Info = -- judgements in abstract syntax - AbsCat (Maybe Context) (Maybe [Term]) -- ^ (/ABS/) constructors; must be 'Id' or 'QId' - | AbsFun (Maybe Type) (Maybe [Equation]) -- ^ (/ABS/) + AbsCat (Maybe Context) (Maybe [Term]) -- ^ (/ABS/) the second parameter is list of constructors - must be 'Id' or 'QId' + | AbsFun (Maybe Type) (Maybe Int) (Maybe [Equation]) -- ^ (/ABS/) type, arrity and definition of function -- judgements in resource | ResParam (Maybe ([Param],Maybe PValues)) -- ^ (/RES/) @@ -229,6 +228,3 @@ ident2label c = LIdent (ident2bs c) label2ident :: Label -> Ident label2ident (LIdent s) = identC s label2ident (LVar i) = identC (BS.pack ('$':show i)) - -wildPatt :: Patt -wildPatt = PV identW diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs index 3df2db7da..b136eee83 100644 --- a/src/GF/Grammar/Lookup.hs +++ b/src/GF/Grammar/Lookup.hs @@ -121,7 +121,7 @@ lookupResType gr m c = do mu <- lookupModule gr a info <- lookupIdentInfo mu c case info of - AbsFun (Just ty) _ -> return $ redirectTerm e ty + AbsFun (Just ty) _ _ -> return $ redirectTerm e ty AbsCat _ _ -> return typeType AnyInd _ n -> lookFun e m c n _ -> prtBad "cannot find type of reused function" c @@ -227,14 +227,14 @@ qualifAnnotPar m t = case t of Con c -> QC m c _ -> composSafeOp (qualifAnnotPar m) t -lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe [Equation]) +lookupAbsDef :: SourceGrammar -> Ident -> Ident -> Err (Maybe Int,Maybe [Equation]) lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do mo <- lookupModule gr m info <- lookupIdentInfo mo c case info of - AbsFun _ (Just t) -> return (Just t) - AnyInd _ n -> lookupAbsDef gr n c - _ -> return Nothing + AbsFun _ a d -> return (a,d) + AnyInd _ n -> lookupAbsDef gr n c + _ -> return (Nothing,Nothing) lookupLincat :: SourceGrammar -> Ident -> Ident -> Err Type lookupLincat gr m c | isPredefCat c = return defLinType --- ad hoc; not needed? @@ -252,9 +252,9 @@ lookupFunType gr m c = do mo <- lookupModule gr m info <- lookupIdentInfo mo c case info of - AbsFun (Just t) _ -> return t - AnyInd _ n -> lookupFunType gr n c - _ -> prtBad "cannot find type of" c + AbsFun (Just t) _ _ -> return t + AnyInd _ n -> lookupFunType gr n c + _ -> prtBad "cannot find type of" c -- | this is needed at compile time lookupCatContext :: SourceGrammar -> Ident -> Ident -> Err Context @@ -281,7 +281,7 @@ opersForType gr orig val = let cat = err error snd (valCat orig) in --- ignore module [(f,ty) | Ok a <- [abstractOfConcrete gr i >>= lookupModule gr], - (f, AbsFun (Just ty0) _) <- tree2list $ jments a, + (f, AbsFun (Just ty0) _ _) <- tree2list $ jments a, let ty = redirectTerm i ty0, Ok valt <- [valCat ty], cat == snd valt --- diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs index fa1b75dda..2c0761f00 100644 --- a/src/GF/Grammar/Macros.hs +++ b/src/GF/Grammar/Macros.hs @@ -414,7 +414,8 @@ linAsStr s = mkRecord linLabel [K s] -- default linearization {s = s} term2patt :: Term -> Err Patt term2patt trm = case termForm trm of - Ok ([], Vr x, []) -> return (PV x) + Ok ([], Vr x, []) | x == identW -> return PW + | otherwise -> return (PV x) Ok ([], Val te ty x, []) -> do te' <- term2patt te return (PVal te' ty x) diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y index 981589ac0..1a9723c28 100644 --- a/src/GF/Grammar/Parser.y +++ b/src/GF/Grammar/Parser.y @@ -240,19 +240,19 @@ CatDef FunDef :: { [(Ident,SrcSpan,Info)] } FunDef - : Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) (Just [])) | fun <- $2] } + : Posn ListIdent ':' Exp Posn { [(fun, ($1,$5), AbsFun (Just $4) Nothing (Just [])) | fun <- $2] } DefDef :: { [(Ident,SrcSpan,Info)] } DefDef - : Posn ListName '=' Exp Posn { [(f, ($1,$5),AbsFun Nothing (Just [([],$4)])) | f <- $2] } - | Posn Name ListPatt '=' Exp Posn { [($2,($1,$6),AbsFun Nothing (Just [($3,$5)]))] } + : Posn ListName '=' Exp Posn { [(f, ($1,$5),AbsFun Nothing (Just 0) (Just [([],$4)])) | f <- $2] } + | Posn Name ListPatt '=' Exp Posn { [($2,($1,$6),AbsFun Nothing (Just (length $3)) (Just [($3,$5)]))] } DataDef :: { [(Ident,SrcSpan,Info)] } DataDef : Posn Ident '=' ListDataConstr Posn { ($2, ($1,$5), AbsCat Nothing (Just (map Cn $4))) : - [(fun, ($1,$5), AbsFun Nothing Nothing) | fun <- $4] } + [(fun, ($1,$5), AbsFun Nothing Nothing Nothing) | fun <- $4] } | Posn ListIdent ':' Exp Posn { [(cat, ($1,$5), AbsCat Nothing (Just (map Cn $2))) | Ok (_,cat) <- [valCat $4]] ++ - [(fun, ($1,$5), AbsFun (Just $4) Nothing) | fun <- $2] } + [(fun, ($1,$5), AbsFun (Just $4) Nothing Nothing) | fun <- $2] } ParamDef :: { [(Ident,SrcSpan,Info)] } ParamDef @@ -481,7 +481,7 @@ Patt2 | '[' String ']' { PChars $2 } | '#' Ident { PMacro $2 } | '#' Ident '.' Ident { PM $2 $4 } - | '_' { wildPatt } + | '_' { PW } | Ident { PV $1 } | Ident '.' Ident { PP $1 $3 [] } | Integer { PInt $1 } @@ -609,8 +609,8 @@ listCatDef id pos cont size = [catd,nilfund,consfund] consId = mkConsId id catd = (listId, pos, AbsCat (Just cont') (Just [Cn baseId,Cn consId])) - nilfund = (baseId, pos, AbsFun (Just niltyp) Nothing) - consfund = (consId, pos, AbsFun (Just constyp) Nothing) + nilfund = (baseId, pos, AbsFun (Just niltyp) Nothing Nothing) + consfund = (consId, pos, AbsFun (Just constyp) Nothing Nothing) cont' = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont] xs = map (Vr . fst) cont' @@ -667,7 +667,7 @@ type SrcSpan = (Posn,Posn) checkInfoType MTAbstract (id,pos,info) = case info of AbsCat _ _ -> return () - AbsFun _ _ -> return () + AbsFun _ _ _ -> return () _ -> failLoc (fst pos) "illegal definition in abstract module" checkInfoType MTResource (id,pos,info) = case info of @@ -701,7 +701,7 @@ checkInfoType (MTInstance _) (id,pos,info) = checkInfoType (MTTransfer _ _) (id,pos,info) = case info of AbsCat _ _ -> return () - AbsFun _ _ -> return () + AbsFun _ _ _ -> return () _ -> failLoc (fst pos) "illegal definition in transfer module" diff --git a/src/GF/Grammar/Printer.hs b/src/GF/Grammar/Printer.hs index 383d36d4f..12b7ba782 100644 --- a/src/GF/Grammar/Printer.hs +++ b/src/GF/Grammar/Printer.hs @@ -79,7 +79,7 @@ ppJudgement q (id, AbsCat pcont pconstrs) = case pconstrs of Just costrs -> text "data" <+> ppIdent id <+> equals <+> fsep (intersperse (char '|') (map (ppTerm q 0) costrs)) <+> semi Nothing -> empty -ppJudgement q (id, AbsFun ptype pexp) = +ppJudgement q (id, AbsFun ptype _ pexp) = (case ptype of Just typ -> text "fun" <+> ppIdent id <+> colon <+> ppTerm q 0 typ <+> semi Nothing -> empty) $$ diff --git a/src/GF/Source/CF.hs b/src/GF/Source/CF.hs index b142fd670..a25baddc1 100644 --- a/src/GF/Source/CF.hs +++ b/src/GF/Source/CF.hs @@ -105,7 +105,7 @@ cf2cat (_,(cat, items)) = map identS $ cat : [c | Left c <- items] cf2rule :: CFRule -> ((Ident,Info),(Ident,Info)) cf2rule (fun, (cat, items)) = (def,ldef) where f = identS fun - def = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing) + def = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing Nothing) args0 = zip (map (identS . ("x" ++) . show) [0..]) items args = [(v, Cn (identS c)) | (v, Left c) <- args0] args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0] diff --git a/src/GF/Source/GrammarToSource.hs b/src/GF/Source/GrammarToSource.hs index cff23f426..a3754336e 100644 --- a/src/GF/Source/GrammarToSource.hs +++ b/src/GF/Source/GrammarToSource.hs @@ -75,9 +75,9 @@ mkTopDefs ds = ds trAnyDef :: (Ident,Info) -> [P.TopDef] trAnyDef (i,info) = let i' = tri i in case info of AbsCat (Just co) pd -> [P.DefCat [P.SimpleCatDef i' (map trDecl co)]] - AbsFun (Just ty) Nothing -> [P.DefFunData [P.FunDef [i'] (trt ty)]] - AbsFun (Just ty) (Just eqs) -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++ - [P.DefDef [P.DPatt (mkName i') (map trp patts) (trt res)] | (patts,res) <- eqs] + AbsFun (Just ty) _ Nothing -> [P.DefFunData [P.FunDef [i'] (trt ty)]] + AbsFun (Just ty) _ (Just eqs) -> [P.DefFun [P.FunDef [i'] (trt ty)]] ++ + [P.DefDef [P.DPatt (mkName i') (map trp patts) (trt res)] | (patts,res) <- eqs] ResOper pty ptr -> [P.DefOper [trDef i' pty ptr]] ResParam pp -> [P.DefPar [case pp of diff --git a/src/GF/Source/SourceToGrammar.hs b/src/GF/Source/SourceToGrammar.hs index 67de8fd46..fc7c2b285 100644 --- a/src/GF/Source/SourceToGrammar.hs +++ b/src/GF/Source/SourceToGrammar.hs @@ -585,7 +585,7 @@ transPatts p = case p of transPatt :: Patt -> Err G.Patt transPatt x = case x of - PW -> return G.wildPatt + PW -> return G.PW PV id -> liftM G.PV $ transIdent id PC id patts -> liftM2 G.PC (transIdent id) (mapM transPatt patts) PCon id -> liftM2 G.PC (transIdent id) (return []) diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs index 2a96f0c91..ea99a3ed4 100644 --- a/src/PGF/Binary.hs +++ b/src/PGF/Binary.hs @@ -42,7 +42,7 @@ instance Binary Abstr where get = do aflags <- get funs <- get cats <- get - let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_)) <- Map.toList funs, c==cat]) cats + let catfuns = Map.mapWithKey (\cat _ -> [f | (f, (DTyp _ c _,_,_)) <- Map.toList funs, c==cat]) cats return (Abstr{ aflags=aflags , funs=funs, cats=cats , catfuns=catfuns diff --git a/src/PGF/Data.hs b/src/PGF/Data.hs index 58952dc7d..142968d8c 100644 --- a/src/PGF/Data.hs +++ b/src/PGF/Data.hs @@ -24,7 +24,7 @@ data PGF = PGF { data Abstr = Abstr { aflags :: Map.Map CId String, -- value of a flag - funs :: Map.Map CId (Type,[Equation]), -- type and def of a fun + funs :: Map.Map CId (Type,Int,[Equation]), -- type, arrity and definition of function cats :: Map.Map CId [Hypo], -- context of a cat catfuns :: Map.Map CId [CId] -- funs to a cat (redundant, for fast lookup) } diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs index 79c88303d..174da092e 100644 --- a/src/PGF/Expr.hs +++ b/src/PGF/Expr.hs @@ -11,9 +11,6 @@ module PGF.Expr(Tree(..), Literal(..), -- helpers pStr,pFactor, - - -- refresh metavariables - newMetas ) where import PGF.CId @@ -41,7 +38,7 @@ data Tree = | Var CId -- ^ variable | Fun CId [Tree] -- ^ function application | Lit Literal -- ^ literal - | Meta Int -- ^ meta variable + | Meta {-# UNPACK #-} !Int -- ^ meta variable deriving (Eq, Ord) -- | An expression represents a potentially unevaluated expression @@ -52,7 +49,7 @@ data Expr = EAbs CId Expr -- ^ lambda abstraction | EApp Expr Expr -- ^ application | ELit Literal -- ^ literal - | EMeta Int -- ^ meta variable + | EMeta {-# UNPACK #-} !Int -- ^ meta variable | EVar CId -- ^ variable or function reference | EPi CId Expr Expr -- ^ dependent function type deriving (Eq,Ord) @@ -219,7 +216,7 @@ expr2tree :: Funs -> Expr -> Tree expr2tree funs e = value2tree [] (eval funs Map.empty e) where value2tree xs (VApp f vs) = case Map.lookup f funs of - Just (DTyp hyps _ _,_) -> -- eta conversion + Just (DTyp hyps _ _,_,_) -> -- eta conversion let a1 = length hyps a2 = length vs a = a1 - a2 @@ -228,11 +225,13 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e) in ret (reverse xs'++xs) (Fun f (map (value2tree []) vs++map Var xs')) Nothing -> error ("unknown variable "++prCId f) - value2tree xs (VGen i) = ret xs (Var (var i)) - value2tree xs (VMeta n) = ret xs (Meta n) + value2tree xs (VGen i vs) | null vs = ret xs (Var (var i)) + | otherwise = error "variable of function type" + value2tree xs (VMeta n vs) | null vs = ret xs (Meta n) + | otherwise = error "meta variable of function type" value2tree xs (VLit l) = ret xs (Lit l) value2tree xs (VClosure env (EAbs x e)) = let i = length xs - in value2tree (var i:xs) (eval funs (Map.insert x (VGen i) env) e) + in value2tree (var i:xs) (eval funs (Map.insert x (VGen i []) env) e) var i = mkCId ('v':show i) @@ -242,73 +241,96 @@ expr2tree funs e = value2tree [] (eval funs Map.empty e) data Value = VApp CId [Value] | VLit Literal - | VMeta Int - | VGen Int + | VMeta {-# UNPACK #-} !Int [Value] + | VGen {-# UNPACK #-} !Int [Value] | VClosure Env Expr deriving (Eq,Ord) -type Funs = Map.Map CId (Type,[Equation]) -- type and def of a fun +type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun type Env = Map.Map CId Value eval :: Funs -> Env -> Expr -> Value eval funs env (EVar x) = case Map.lookup x env of Just v -> v Nothing -> case Map.lookup x funs of - Just (_,eqs) -> case eqs of - Equ [] e : _ -> eval funs env e - [] -> VApp x [] - Nothing -> error ("unknown variable "++prCId x) + Just (_,a,eqs) -> if a == 0 + then case eqs of + Equ [] e : _ -> eval funs env e + _ -> VApp x [] + else VApp x [] + Nothing -> error ("unknown variable "++prCId x) eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2] eval funs env (EAbs x e) = VClosure env (EAbs x e) -eval funs env (EMeta k) = VMeta k +eval funs env (EMeta k) = VMeta k [] eval funs env (ELit l) = VLit l apply :: Funs -> Env -> Expr -> [Value] -> Value apply funs env e [] = eval funs env e apply funs env (EVar x) vs = case Map.lookup x env of Just v -> case (v,vs) of + (VApp f vs0 , vs) -> apply funs env (EVar f) (vs0++vs) + (VLit _ , vs) -> error "literal of function type" + (VMeta i vs0 , vs) -> VMeta i (vs0++vs) + (VGen i vs0 , vs) -> VGen i (vs0++vs) (VClosure env (EAbs x e),v:vs) -> apply funs (Map.insert x v env) e vs Nothing -> case Map.lookup x funs of - Just (_,eqs) -> case match eqs vs of - Just (e,vs,env) -> apply funs env e vs - Nothing -> VApp x vs - Nothing -> error ("unknown variable "++prCId x) -apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs + Just (_,a,eqs) -> if a <= length vs + then let (as,vs') = splitAt a vs + in case match eqs as of + Match e env -> apply funs env e vs' + Fail -> VApp x vs + Susp -> VApp x vs + else VApp x vs + Nothing -> error ("unknown variable "++prCId x) apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs) +apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs +apply funs env (EMeta k) vs = VMeta k vs +apply funs env (ELit l) vs = error "literal of function type" -match :: [Equation] -> [Value] -> Maybe (Expr, [Value], Env) -match eqs vs = + +----------------------------------------------------- +-- Pattern matching +----------------------------------------------------- + +data MatchRes + = Match Expr Env + | Susp + | Fail + +match :: [Equation] -> [Value] -> MatchRes +match eqs as = case eqs of - [] -> Nothing - (Equ ps res):eqs -> let (as,vs') = splitAt (length ps) vs - in case zipWithM tryMatch ps as of - Just envs -> Just (res, vs', Map.unions envs) - Nothing -> match eqs vs + [] -> Fail + (Equ ps res):eqs -> case tryMatches ps as res Map.empty of + Fail -> match eqs as + res -> res where - tryMatch p v = case (p, v) of - (PVar x, _ ) -> Just (Map.singleton x v) - (PApp f ps, VApp fe vs) | f == fe -> do envs <- zipWithM tryMatch ps vs - return (Map.unions envs) - (PLit l, VLit le ) | l == le -> Just Map.empty - _ -> Nothing + tryMatches [] [] res env = Match res env + tryMatches (p:ps) (a:as) res env = tryMatch p a env + where + tryMatch (PApp f1 ps1) (VApp f2 vs2) env | f1 == f2 = tryMatches (ps1++ps) (vs2++as) res env + tryMatch (PApp f1 ps1) (VMeta _ _ ) env = Susp + tryMatch (PApp f1 ps1) (VGen _ _ ) env = Susp + tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches ps as res env + tryMatch (PLit l1 ) (VMeta _ _ ) env = Susp + tryMatch (PLit l1 ) (VGen _ _ ) env = Susp + tryMatch (PVar x ) (v ) env = tryMatches ps as res (Map.insert x v env) + tryMatch (PWild ) (_ ) env = tryMatches ps as res env + tryMatch _ _ env = Fail + + +----------------------------------------------------- +-- Equality checking +----------------------------------------------------- eqValue :: Int -> Value -> Value -> [(Value,Value)] eqValue k v1 v2 = case (v1,v2) of (VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue k) vs1 vs2) (VLit l1, VLit l2 ) | l1 == l2 -> [] - (VMeta i, VMeta j ) | i == j -> [] - (VGen i, VGen j ) | i == j -> [] + (VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) + (VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue k) vs1 vs2) (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) -> - let v = VGen k + let v = VGen k [] in eqValue (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2) _ -> [(v1,v2)] - ---- use composOp and state monad... -newMetas :: Expr -> Expr -newMetas = fst . metas 0 where - metas i exp = case exp of - EAbs x e -> let (f,j) = metas i e in (EAbs x f, j) - EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k) - EMeta _ -> (EMeta i, i+1) - _ -> (exp,i) diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs index 462fa9cba..fe00f4ff7 100644 --- a/src/PGF/Macros.hs +++ b/src/PGF/Macros.hs @@ -35,17 +35,19 @@ lookPrintName pgf lang fun = lookType :: PGF -> CId -> Type lookType pgf f = - fst $ lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) + case lookMap (error $ "lookType " ++ show f) f (funs (abstract pgf)) of + (ty,_,_) -> ty lookDef :: PGF -> CId -> [Equation] lookDef pgf f = - snd $ lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) + case lookMap (error $ "lookDef " ++ show f) f (funs (abstract pgf)) of + (_,a,eqs) -> eqs isData :: PGF -> CId -> Bool isData pgf f = case Map.lookup f (funs (abstract pgf)) of - Just (_,[]) -> True -- the encoding of data constrs - _ -> False + Just (_,_,[]) -> True -- the encoding of data constrs + _ -> False lookValCat :: PGF -> CId -> CId lookValCat pgf = valCat . lookType pgf @@ -74,7 +76,7 @@ lookConcrFlag pgf lang f = Map.lookup f $ cflags $ lookConcr pgf lang functionsToCat :: PGF -> CId -> [(CId,Type)] functionsToCat pgf cat = - [(f,ty) | f <- fs, Just (ty,_) <- [Map.lookup f $ funs $ abstract pgf]] + [(f,ty) | f <- fs, Just (ty,_,_) <- [Map.lookup f $ funs $ abstract pgf]] where fs = lookMap [] cat $ catfuns $ abstract pgf diff --git a/src/PGF/Paraphrase.hs b/src/PGF/Paraphrase.hs index ff718a785..64f9375d0 100644 --- a/src/PGF/Paraphrase.hs +++ b/src/PGF/Paraphrase.hs @@ -50,7 +50,7 @@ fromDef pgf t@(Fun f ts) = defDown t ++ defUp t where isClosed d || (length equs == 1 && isLinear d)] equss = [(f,[(Fun f (map patt2tree ps), expr2tree (funs (abstract pgf)) d) | (Equ ps d) <- eqs]) | - (f,(_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] + (f,(_,_,eqs)) <- Map.assocs (funs (abstract pgf)), not (null eqs)] trequ s f e = True ----trace (s ++ ": " ++ show f ++ " " ++ show e) True diff --git a/src/PGF/ShowLinearize.hs b/src/PGF/ShowLinearize.hs index b5fab007a..62329eb88 100644 --- a/src/PGF/ShowLinearize.hs +++ b/src/PGF/ShowLinearize.hs @@ -99,7 +99,7 @@ markLinearize pgf lang t = concat $ take 1 $ linearizesMark pgf lang t collectWords :: PGF -> CId -> [(String, [(String,String)])] collectWords pgf lang = concatMap collOne - [(f,c,0) | (f,(DTyp [] c _,_)) <- Map.toList $ funs $ abstract pgf] + [(f,c,0) | (f,(DTyp [] c _,_,_)) <- Map.toList $ funs $ abstract pgf] where collOne (f,c,i) = fromRec f [prCId c] (recLinearize pgf lang (Fun f (replicate i (Meta 888)))) diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs index 7a7a5ccc0..b2a28212a 100644 --- a/src/PGF/TypeCheck.hs +++ b/src/PGF/TypeCheck.hs @@ -61,7 +61,7 @@ infer pgf tenv@(k,rho,gamma) e = case e of checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)]) checkExp pgf tenv@(k,rho,gamma) e typ = do - let v = VGen k + let v = VGen k [] case e of EMeta m -> return $ (e,[]) EAbs x t -> case typ of @@ -82,7 +82,7 @@ checkInferExp pgf tenv@(k,_,_) e typ = do lookupEVar :: PGF -> TCEnv -> CId -> Err Value lookupEVar pgf (_,g,_) x = case Map.lookup x g of Just v -> return v - _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . fst) $ + _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $ Map.lookup x (funs (abstract pgf)) type2expr :: Type -> Expr @@ -103,7 +103,7 @@ prValue = showExpr . value2expr value2expr v = case v of VApp f vs -> foldl EApp (EVar f) (map value2expr vs) - VMeta i -> EMeta i + VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs) VClosure g e -> e ---- VLit l -> ELit l @@ -116,15 +116,15 @@ prConstraints cs = unwords splitConstraints :: [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)]) splitConstraints = mkSplit . partition isSubst . regroup . map reorder where reorder (v,w) = case w of - VMeta _ -> (w,v) + VMeta _ _ -> (w,v) _ -> (v,w) regroup = groupBy (\x y -> fst x == fst y) . sort isSubst cs@((v,u):_) = case v of - VMeta _ -> all ((==u) . snd) cs + VMeta _ _ -> all ((==u) . snd) cs _ -> False - mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i,v):_ <- ms], concat cs) + mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs) metaSubst :: [(Int,Expr)] -> Expr -> Expr metaSubst vs exp = case exp of @@ -136,3 +136,11 @@ metaSubst vs exp = case exp of where subst = metaSubst vs +--- use composOp and state monad... +newMetas :: Expr -> Expr +newMetas = fst . metas 0 where + metas i exp = case exp of + EAbs x e -> let (f,j) = metas i e in (EAbs x f, j) + EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k) + EMeta _ -> (EMeta i, i+1) + _ -> (exp,i) diff --git a/testsuite/update/ArrityCheck.gf b/testsuite/update/ArrityCheck.gf new file mode 100644 index 000000000..9ee03ba6e --- /dev/null +++ b/testsuite/update/ArrityCheck.gf @@ -0,0 +1,5 @@ +abstract ArrityCheck = { + fun f : Int -> Int -> Int ; + def f 0 = \x -> x ; + f 1 1 = 0 ; +} diff --git a/testsuite/update/ArrityCheck.gfs b/testsuite/update/ArrityCheck.gfs new file mode 100644 index 000000000..b63c0ca51 --- /dev/null +++ b/testsuite/update/ArrityCheck.gfs @@ -0,0 +1 @@ +i testsuite\update\ArrityCheck.gf diff --git a/testsuite/update/ArrityCheck.gfs.gold b/testsuite/update/ArrityCheck.gfs.gold new file mode 100644 index 000000000..924dddf1e --- /dev/null +++ b/testsuite/update/ArrityCheck.gfs.gold @@ -0,0 +1,8 @@ + + +C:\gf_2\testsuite\update\ArrityCheck.gf:6:1: cannot unify the informations + fun f : Int -> Int -> Int ; + def f 0 = \x -> x ; +and + def f 1 1 = 0 ; +in module ArrityCheck