From e059fddb6d802edad61252bf4d05daa85a1768fc Mon Sep 17 00:00:00 2001 From: peb Date: Tue, 4 Apr 2006 09:33:22 +0000 Subject: [PATCH] adding support for 2nd order functions in SimpleGFC format --- src/GF/Conversion/GFCtoSimple.hs | 20 ++++++++------ src/GF/Conversion/Prolog.hs | 15 ++++++---- src/GF/Conversion/SimpleToFinite.hs | 38 +++++++++++++------------ src/GF/Conversion/TypeGraph.hs | 2 +- src/GF/Formalism/GCFG.hs | 2 +- src/GF/Formalism/SimpleGFC.hs | 43 ++++++++++++++++++----------- 6 files changed, 71 insertions(+), 49 deletions(-) diff --git a/src/GF/Conversion/GFCtoSimple.hs b/src/GF/Conversion/GFCtoSimple.hs index 72b774e16..a01deb08a 100644 --- a/src/GF/Conversion/GFCtoSimple.hs +++ b/src/GF/Conversion/GFCtoSimple.hs @@ -1,4 +1,4 @@ ----------------------------------------------------------------------- +--------------------------------------------------------------------- -- | -- Maintainer : PL -- Stability : (stable) @@ -63,17 +63,21 @@ convertAbsFun gram fun typing = -- trace2 "GFCtoSimple - converting function" (p convertAbstract :: [SDecl] -> Fun -> A.Exp -> Abstract SDecl Name convertAbstract env fun (A.EProd x a b) - = convertAbstract (convertType x' [] a : env) fun b + = convertAbstract (convertAbsType x' [] a : env) fun b where x' = if x==I.identC "h_" then anyVar else x convertAbstract env fun a - = Abs (convertType anyVar [] a) (reverse env) name + = Abs (convertAbsType anyVar [] a) (reverse env) name where name = Name fun [ Unify [n] | n <- [0 .. length env-1] ] -convertType :: Var -> [TTerm] -> A.Exp -> SDecl -convertType x args (A.EApp a b) = convertType x (convertExp [] b : args) a -convertType x args (A.EAtom at) = Decl x (convertCat at) args -convertType x args (A.EProd _ _ b) = convertType x args b ---- AR 7/10 workaround -convertType x args exp = error $ "GFCtoSimple.convertType: " ++ prt exp +convertAbsType :: Var -> [FOType SCat] -> A.Exp -> SDecl +convertAbsType x args (A.EProd _ a b) = convertAbsType x (convertType [] a : args) b +convertAbsType x args a = Decl x (reverse args ::--> convertType [] a) + +convertType :: [TTerm] -> A.Exp -> FOType SCat +convertType args (A.EApp a b) = convertType (convertExp [] b : args) a +convertType args (A.EAtom at) = convertCat at ::@ reverse args +convertType args (A.EProd _ _ b) = convertType args b ---- AR 7/10 workaround +convertType args exp = error $ "GFCtoSimple.convertType: " ++ prt exp {- Exp from GF/Canon/GFC.cf: EApp. Exp1 ::= Exp1 Exp2 ; diff --git a/src/GF/Conversion/Prolog.hs b/src/GF/Conversion/Prolog.hs index ebad8e587..b930cb476 100644 --- a/src/GF/Conversion/Prolog.hs +++ b/src/GF/Conversion/Prolog.hs @@ -81,8 +81,8 @@ prtSRule lang (Rule (Abs cat cats (Name fun _prof)) (Cnc _ _ mterm)) = (if null lang then "" else prtQ lang ++ " : ") ++ prtFunctor "rule" [plfun, plcat, plcats, plcnc] ++ "." where plfun = prtQ fun - plcat = prtSCat cat - plcats = prtFunctor "c" (map prtSCat cats) + plcat = prtSDecl cat + plcats = prtFunctor "c" (map prtSDecl cats) plcnc = "\n\t" ++ prtSTerm (maybe Empty id mterm) prtSTerm (Arg n c p) = prtFunctor "arg" [prtQ c, prt (n+1), prtSPath p] @@ -101,9 +101,14 @@ prtSTerm (term :! sel) = prtOper "/" (prtSTerm term) (prtSTerm sel) prtSPath (Path path) = prtPList (map (either prtQ prtSTerm) path) -prtSCat (Decl var cat args) = prVar ++ prtFunctor (prtQ cat) (map prtSTTerm args) - where prVar | var == anyVar = "" - | otherwise = "_" ++ prtVar var ++ ":" +prtSDecl (Decl var typ) | var == anyVar = prtSAbsType typ + | otherwise = "_" ++ prtVar var ++ ":" ++ prtSAbsType typ + + +prtSAbsType ([] ::--> typ) = prtSFOType typ +prtSAbsType (args ::--> typ) = prtOper ":->" (prtPList (map prtSFOType args)) (prtSFOType typ) + +prtSFOType (cat ::@ args) = prtFunctor (prtQ cat) (map prtSTTerm args) prtSTTerm (con :@ args) = prtFunctor (prtQ con) (map prtSTTerm args) prtSTTerm (TVar var) = "_" ++ prtVar var diff --git a/src/GF/Conversion/SimpleToFinite.hs b/src/GF/Conversion/SimpleToFinite.hs index 9dbbf5da2..bbd3ae355 100644 --- a/src/GF/Conversion/SimpleToFinite.hs +++ b/src/GF/Conversion/SimpleToFinite.hs @@ -74,7 +74,7 @@ convertAbstract :: Splitable -> Abstract SDecl Name -> CnvMonad (Abstract SDecl Name) convertAbstract split (Abs decl decls name) = case splitableFun split fun of - Just cat' -> return $ Abs (Decl anyVar (mergeFun fun cat') []) decls name + Just cat' -> return $ Abs (Decl anyVar ([] ::--> (mergeFun fun cat' ::@ []))) decls name Nothing -> expandTyping split [] fun profiles [] decl decls [] where Name fun profiles = name @@ -82,29 +82,30 @@ expandTyping :: Splitable -> [(Var, SCat)] -> Fun -> [Profile (SyntaxForest Fun)] -> [Profile (SyntaxForest Fun)] -> SDecl -> [SDecl] -> [SDecl] -> CnvMonad (Abstract SDecl Name) -expandTyping split env fun [] profiles (Decl x cat args) [] decls +expandTyping split env fun [] profiles (Decl x (typargs ::--> (cat ::@ args))) [] decls = return $ Abs decl (reverse decls) (Name fun (reverse profiles)) - where decl = substArgs split x env cat args [] -expandTyping split env fun (prof:profiles) profsDone typ (Decl x xcat xargs : declsToDo) declsDone + where decl = substArgs split x env typargs cat args [] +expandTyping split env fun (prof:profiles) profsDone typ + (Decl x (xtypargs ::--> (xcat ::@ xargs)) : declsToDo) declsDone = do (x', xcat', env', prof') <- calcNewEnv - let decl = substArgs split x' env xcat' xargs [] - expandTyping split env' fun profiles (prof':profsDone) typ declsToDo (decl : declsDone) + let decl = substArgs split x' env xtypargs xcat' xargs [] + expandTyping split env' fun profiles (prof' : profsDone) typ declsToDo (decl : declsDone) where calcNewEnv = case splitableCat split xcat of + Nothing -> return (x, xcat, env, prof) Just newFuns -> do newFun <- member newFuns let newCat = mergeFun newFun xcat newProf = Constant (FNode newFun [[]]) -- should really be using some kind of -- "profile unification" return (anyVar, newCat, (x,newCat) : env, newProf) - Nothing -> return (x, xcat, env, prof) - -substArgs :: Splitable -> Var -> [(Var, SCat)] -> SCat -> [TTerm] -> [TTerm] -> SDecl -substArgs split x env cat [] args = Decl x cat (reverse args) -substArgs split x env cat (arg:argsToDo) argsDone +substArgs :: Splitable -> Var -> [(Var, SCat)] -> [FOType SCat] + -> SCat -> [TTerm] -> [TTerm] -> SDecl +substArgs split x env typargs cat [] args = Decl x (typargs ::--> (cat ::@ reverse args)) +substArgs split x env typargs cat (arg:argsToDo) argsDone = case argLookup split env arg of - Just newCat -> substArgs split x env (mergeArg cat newCat) argsToDo argsDone - Nothing -> substArgs split x env cat argsToDo (arg : argsDone) + Just newCat -> substArgs split x env typargs (mergeArg cat newCat) argsToDo argsDone + Nothing -> substArgs split x env typargs cat argsToDo (arg : argsDone) argLookup split env (TVar x) = lookup x env argLookup split env (con :@ _) = fmap (mergeFun fun) (splitableFun split fun) @@ -133,7 +134,7 @@ calcSplitable rules = (listAssoc splitableCat2Funs, listAssoc splitableFun2Cat) -- cat-fun pairs that are splitable splitableCatFuns = tracePrt "SimpleToFinite - splitable functions" prt $ [ (cat, name2fun name) | - Rule (Abs (Decl _ cat []) [] name) _ <- rules, + Rule (Abs (Decl _ ([] ::--> (cat ::@ []))) [] name) _ <- rules, splitableCats ?= cat ] -- all cats that are splitable @@ -143,12 +144,12 @@ calcSplitable rules = (listAssoc splitableCat2Funs, listAssoc splitableFun2Cat) -- all result cats for some pure function resultCats = tracePrt "SimpleToFinite - result cats" prt $ - nubsort [ cat | Rule (Abs (Decl _ cat _) decls _) _ <- rules, + nubsort [ cat | Rule (Abs (Decl _ (_ ::--> (cat ::@ _))) decls _) _ <- rules, not (null decls) ] -- all cats in constants without dependencies nondepCats = tracePrt "SimpleToFinite - nondep cats" prt $ - nubsort [ cat | Rule (Abs (Decl _ cat []) [] _) _ <- rules ] + nubsort [ cat | Rule (Abs (Decl _ ([] ::--> (cat ::@ []))) [] _) _ <- rules ] -- all cats occurring as some dependency of another cat depCats = tracePrt "SimpleToFinite - dep cats" prt $ @@ -156,9 +157,10 @@ calcSplitable rules = (listAssoc splitableCat2Funs, listAssoc splitableFun2Cat) cat <- varCats [] (decls ++ [decl]) ] varCats _ [] = [] - varCats env (Decl x xcat args : decls) + varCats env (Decl x (xargs ::--> xtyp@(xcat ::@ _)) : decls) = varCats ((x,xcat) : env) decls ++ - [ cat | arg <- args, y <- varsInTTerm arg, cat <- lookupList y env ] + [ cat | (_::@args) <- (xtyp:xargs), arg <- args, + y <- varsInTTerm arg, cat <- lookupList y env ] ---------------------------------------------------------------------- diff --git a/src/GF/Conversion/TypeGraph.hs b/src/GF/Conversion/TypeGraph.hs index d527c6598..62ee9726e 100644 --- a/src/GF/Conversion/TypeGraph.hs +++ b/src/GF/Conversion/TypeGraph.hs @@ -53,6 +53,6 @@ prtFunctionGraphRule (Rule abs@(Abs cat cats (Name fun _prof)) _) unlines [ prtSCat c ++ " -> " ++ pfun ++ ";" | c <- cats ] where pfun = "GF_FUNCTION_" ++ prt fun -prtSCat (Decl var cat args) = prt cat +prtSCat decl = prt (decl2cat decl) diff --git a/src/GF/Formalism/GCFG.hs b/src/GF/Formalism/GCFG.hs index 1248208c0..9cf47637a 100644 --- a/src/GF/Formalism/GCFG.hs +++ b/src/GF/Formalism/GCFG.hs @@ -42,7 +42,7 @@ instance (Print c, Print n, Print l, Print t) => Print (Rule n c l t) where instance (Print c, Print n) => Print (Abstract c n) where prt (Abs cat args name) = prt name ++ ". " ++ prt cat ++ ( if null args then "" - else " -> " ++ prtSep " " args ) + else " --> " ++ prtSep " " args ) instance (Print l, Print t) => Print (Concrete l t) where prt (Cnc lcat args term) = prt term diff --git a/src/GF/Formalism/SimpleGFC.hs b/src/GF/Formalism/SimpleGFC.hs index 24e8e3f73..63a9ed43f 100644 --- a/src/GF/Formalism/SimpleGFC.hs +++ b/src/GF/Formalism/SimpleGFC.hs @@ -37,22 +37,29 @@ type SimpleRule c n t = Rule (Decl c) n (LinType c t) (Maybe (Term c t)) -- ** dependent type declarations --- | 'Decl x c ts' == x is of type (c applied to ts) -data Decl c = Decl Var c [TTerm] - deriving (Eq, Ord, Show) +-- 'Decl x c ts' == x is of type (c applied to ts) +-- data Decl c = Decl Var c [TTerm] +-- deriving (Eq, Ord, Show) + +-- | 'Decl x t' == 'x' is of type 't' +data Decl c = Decl Var (AbsType c) deriving (Eq, Ord, Show) +-- | '[t1..tn] ::--> t' == 't1 -> ... -> tn -> t' +data AbsType c = [FOType c] ::--> FOType c deriving (Eq, Ord, Show) +-- | 'c ::@ [t1..tn]' == '(c t1 ... tn)' +data FOType c = c ::@ [TTerm] deriving (Eq, Ord, Show) + +-- including second order functions: +-- (A -> B) ==> Decl _ ([A ::@ []] ::--> (B ::@ [])) +-- (x : A -> B -> C) ==> Decl x ([A ::@ [], B ::@ []] ::--> (C ::@ [])) +-- (y : A t x -> B (t x)) ==> Decl y ([A ::@ [t:@[],TVar x]] ::--> (B ::@ [t:@[TVar x]])) + + data TTerm = Constr :@ [TTerm] | TVar Var deriving (Eq, Ord, Show) -{-- andra ordningens funktioner: -data Decl c = Decl Var [(c,[TTerm])] (c,[TTerm]) --- (A -> B) ==> Decl _ [(A,[])] (B,[]) --- (A -> B -> C) ==> Decl _ [(A,[]), (B,[])] (C,[]) --- (y : A t x -> B (t x)) ==> Decl y [(A,[t:@[],TVar x])] (B,[t:@[TVar x]]) --} - decl2cat :: Decl c -> c -decl2cat (Decl _ cat _) = cat +decl2cat (Decl _ (_ ::--> (cat ::@ _))) = cat varsInTTerm :: TTerm -> [Var] varsInTTerm tterm = vars tterm [] @@ -218,11 +225,15 @@ lintype2paths path (TblT pt vt) = concat [ lintype2paths (path ++! pat) vt | -- * pretty-printing instance Print c => Print (Decl c) where - prt (Decl var cat args) - | null args = prVar ++ prt cat - | otherwise = "(" ++ prVar ++ prt cat ++ prtBefore " " args ++ ")" - where prVar | var == anyVar = "" - | otherwise = "?" ++ prt var ++ ":" + prt (Decl var typ) | var == anyVar = prt typ + | otherwise = "(?" ++ prt var ++ ":" ++ prt typ ++ ")" + +instance Print c => Print (AbsType c) where + prt ([] ::--> typ) = prt typ + prt (args ::--> typ) = "(" ++ prtAfter "->" args ++ prt typ ++ ")" + +instance Print c => Print (FOType c) where + prt (cat ::@ args) = prt cat ++ prtBefore " " args instance Print TTerm where prt (con :@ args)