summaryrefslogtreecommitdiff
path: root/src/GF
diff options
context:
space:
mode:
Diffstat (limited to 'src/GF')
-rw-r--r--src/GF/Conversion/GFCtoSimple.hs20
-rw-r--r--src/GF/Conversion/Prolog.hs15
-rw-r--r--src/GF/Conversion/SimpleToFinite.hs38
-rw-r--r--src/GF/Conversion/TypeGraph.hs2
-rw-r--r--src/GF/Formalism/GCFG.hs2
-rw-r--r--src/GF/Formalism/SimpleGFC.hs43
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)
generated by cgit v1.2.3 (git 2.39.1) at 2026-05-20 20:16:35 +0000