msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

remove all files that aren't used in GF-3.0

Browse Source
This commit is contained in:
kr.angelov
2008-05-22 11:59:31 +00:00
parent d78e8d5469
commit fc42d8ec3b
286 changed files with 21 additions and 53176 deletions
Download Patch File Download Diff File Expand all files Collapse all files

145
src-3.0/GF/Grammar/AbsCompute.hs
View File

@@ -1,145 +0,0 @@
----------------------------------------------------------------------
-- |
-- Module : AbsCompute
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/02 20:50:19 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.8 $
--
-- computation in abstract syntax w.r.t. explicit definitions.
--
-- old GF computation; to be updated
-----------------------------------------------------------------------------
module GF.Grammar.AbsCompute (LookDef,
compute,
computeAbsTerm,
computeAbsTermIn,
beta
) where
import GF.Data.Operations
import GF.Grammar.Abstract
import GF.Grammar.PrGrammar
import GF.Grammar.LookAbs
import GF.Grammar.Compute
import Debug.Trace
import Data.List(intersperse)
import Control.Monad (liftM, liftM2)
-- for debugging
tracd m t = t
-- tracd = trace
compute :: GFCGrammar -> Exp -> Err Exp
compute = computeAbsTerm
computeAbsTerm :: GFCGrammar -> 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)
computeAbsTermIn :: LookDef -> [Ident] -> Exp -> Err Exp
computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
compt vv t = case t of
-- Prod x a b -> liftM2 (Prod x) (compt vv a) (compt (x:vv) b)
-- Abs x b -> liftM (Abs x) (compt (x:vv) b)
_ -> do
let t' = beta vv t
(yy,f,aa) <- termForm t'
let vv' = yy ++ vv
aa' <- mapM (compt vv') aa
case look f of
Just (Eqs eqs) -> tracd ("\nmatching" +++ prt f) $
case findMatch eqs aa' of
Ok (d,g) -> do
--- let (xs,ts) = unzip g
--- ts' <- alphaFreshAll vv' ts
let g' = g --- zip xs ts'
d' <- compt vv' $ substTerm vv' g' d
tracd ("by Egs:" +++ prt d') $ return $ mkAbs yy $ d'
_ -> tracd ("no match" +++ prt t') $
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
beta vv c = case c of
Let (x,(_,a)) b -> beta vv $ substTerm vv [(x,beta vv a)] (beta (x:vv) b)
App f a ->
let (a',f') = (beta vv a, beta vv f) in
case f' of
Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
_ -> (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)
Abs x b -> Abs x (beta (x:vv) b)
_ -> 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]

426
src-3.0/GF/Grammar/Compute.hs
View File

@@ -1,426 +0,0 @@
----------------------------------------------------------------------
-- |
-- Module : Compute
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/11/01 15:39:12 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.19 $
--
-- Computation of source terms. Used in compilation and in @cc@ command.
-----------------------------------------------------------------------------
module GF.Grammar.Compute (computeConcrete, computeTerm,computeConcreteRec) where
import GF.Data.Operations
import GF.Grammar.Grammar
import GF.Infra.Ident
import GF.Infra.Option
import GF.Data.Str
import GF.Grammar.PrGrammar
import GF.Infra.Modules
import GF.Grammar.Macros
import GF.Grammar.Lookup
import GF.Grammar.Refresh
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel) ----
import GF.Grammar.AppPredefined
import Data.List (nub,intersperse)
import Control.Monad (liftM2, liftM)
-- | computation of concrete syntax terms into normal form
-- used mainly for partial evaluation
computeConcrete :: SourceGrammar -> Term -> Err Term
computeConcrete g t = {- refreshTerm t >>= -} computeTerm g [] t
computeConcreteRec g t = {- refreshTerm t >>= -} computeTermOpt True g [] t
computeTerm :: SourceGrammar -> Substitution -> Term -> Err Term
computeTerm = computeTermOpt False
-- rec=True is used if it cannot be assumed that looked-up constants
-- have already been computed (mainly with -optimize=noexpand in .gfr)
computeTermOpt :: Bool -> SourceGrammar -> Substitution -> Term -> Err Term
computeTermOpt rec gr = comput True where
comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging
case t of
Q (IC "Predef") _ -> return t
Q p c -> look p c
-- if computed do nothing
Computed t' -> return $ unComputed t'
Vr x -> do
t' <- maybe (prtBad ("no value given to variable") x) return $ lookup x g
case t' of
_ | t == t' -> return t
_ -> comp g t'
-- Abs x@(IA _) b -> do
Abs x b | full -> do
let (xs,b1) = termFormCnc t
b' <- comp ([(x,Vr x) | x <- xs] ++ g) b1
return $ mkAbs xs b'
-- b' <- comp (ext x (Vr x) g) b
-- return $ Abs x b'
Abs _ _ -> return t -- hnf
Let (x,(_,a)) b -> do
a' <- comp g a
comp (ext x a' g) b
Prod x a b -> do
a' <- comp g a
b' <- comp (ext x (Vr x) g) b
return $ Prod x a' b'
-- beta-convert
App f a -> case appForm t of
(h,as) | length as > 1 -> do
h' <- hnf g h
as' <- mapM (comp g) as
case h' of
_ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
c@(QC _ _) -> do
return $ mkApp c as'
Q (IC "Predef") f -> do
(t',b) <- appPredefined (mkApp h' as')
if b then return t' else comp g t'
Abs _ _ -> do
let (xs,b) = termFormCnc h'
let g' = (zip xs as') ++ g
let as2 = drop (length xs) as'
let xs2 = drop (length as') xs
b' <- comp g' (mkAbs xs2 b)
if null as2 then return b' else comp g (mkApp b' as2)
_ -> compApp g (mkApp h' as')
_ -> compApp g t
P t l | isLockLabel l -> return $ R []
---- a workaround 18/2/2005: take this away and find the reason
---- why earlier compilation destroys the lock field
P t l -> do
t' <- comp g t
case t' of
FV rs -> mapM (\c -> comp g (P c l)) rs >>= returnC . variants
R r -> maybe (prtBad "no value for label" l) (comp g . snd) $
lookup l $ reverse r
ExtR a (R b) ->
case comp g (P (R b) l) of
Ok v -> return v
_ -> comp g (P a l)
--- { - --- this is incorrect, since b can contain the proper value
ExtR (R a) b -> -- NOT POSSIBLE both a and b records!
case comp g (P (R a) l) of
Ok v -> return v
_ -> comp g (P b l)
--- - } ---
Alias _ _ r -> comp g (P r l)
S (T i cs) e -> prawitz g i (flip P l) cs e
S (V i cs) e -> prawitzV g i (flip P l) cs e
_ -> returnC $ P t' l
PI t l i -> comp g $ P t l -----
S t@(T ti cc) v -> do
v' <- comp g v
case v' of
FV vs -> do
ts' <- mapM (comp g . S t) vs
return $ variants ts'
_ -> case ti of
{-
TComp _ -> do
case term2patt v' of
Ok p' -> case lookup p' cc of
Just u -> comp g u
_ -> do
t' <- comp g t
return $ S t' v' -- if v' is not canonical
_ -> do
t' <- comp g t
return $ S t' v'
-}
_ -> case matchPattern cc v' of
Ok (c,g') -> comp (g' ++ g) c
_ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t
_ -> do
t' <- comp g t
return $ S t' v' -- if v' is not canonical
S t v -> do
t' <- case t of
-- T _ _ -> return t
-- V _ _ -> return t
_ -> comp g t
v' <- comp g v
case v' of
FV vs -> mapM (\c -> comp g (S t' c)) vs >>= returnC . variants
_ -> case t' of
FV ccs -> mapM (\c -> comp g (S c v')) ccs >>= returnC . variants
T _ [(PV IW,c)] -> comp g c --- an optimization
T _ [(PT _ (PV IW),c)] -> comp g c
T _ [(PV z,c)] -> comp (ext z v' g) c --- another optimization
T _ [(PT _ (PV z),c)] -> comp (ext z v' g) c
-- course-of-values table: look up by index, no pattern matching needed
V ptyp ts -> do
vs <- allParamValues gr ptyp
case lookup v' (zip vs [0 .. length vs - 1]) of
Just i -> comp g $ ts !! i
----- _ -> prtBad "selection" $ S t' v' -- debug
_ -> return $ S t' v' -- if v' is not canonical
T (TComp _) cs -> do
case term2patt v' of
Ok p' -> case lookup p' cs of
Just u -> comp g u
_ -> return $ S t' v' -- if v' is not canonical
_ -> return $ S t' v'
T _ cc -> case matchPattern cc v' of
Ok (c,g') -> comp (g' ++ g) c
_ | isCan v' -> prtBad ("missing case" +++ prt v' +++ "in") t
_ -> return $ S t' v' -- if v' is not canonical
Alias _ _ d -> comp g (S d v')
S (T i cs) e -> prawitz g i (flip S v') cs e
S (V i cs) e -> prawitzV g i (flip S v') cs e
_ -> returnC $ S t' v'
-- normalize away empty tokens
K "" -> return Empty
-- glue if you can
Glue x0 y0 -> do
x <- comp g x0
y <- comp g y0
case (x,y) of
(FV ks,_) -> do
kys <- mapM (comp g . flip Glue y) ks
return $ variants kys
(_,FV ks) -> do
xks <- mapM (comp g . Glue x) ks
return $ variants xks
(Alias _ _ d, y) -> comp g $ Glue d y
(x, Alias _ _ d) -> comp g $ Glue x d
(S (T i cs) e, s) -> prawitz g i (flip Glue s) cs e
(s, S (T i cs) e) -> prawitz g i (Glue s) cs e
(S (V i cs) e, s) -> prawitzV g i (flip Glue s) cs e
(s, S (V i cs) e) -> prawitzV g i (Glue s) cs e
(_,Empty) -> return x
(Empty,_) -> return y
(K a, K b) -> return $ K (a ++ b)
(_, Alts (d,vs)) -> do
---- (K a, Alts (d,vs)) -> do
let glx = Glue x
comp g $ Alts (glx d, [(glx v,c) | (v,c) <- vs])
(Alts _, ka) -> checks [do
y' <- strsFromTerm ka
---- (Alts _, K a) -> checks [do
x' <- strsFromTerm x -- this may fail when compiling opers
return $ variants [
foldr1 C (map K (str2strings (glueStr v u))) | v <- x', u <- y']
---- foldr1 C (map K (str2strings (glueStr v (str a)))) | v <- x']
,return $ Glue x y
]
(C u v,_) -> comp g $ C u (Glue v y)
_ -> do
mapM_ checkNoArgVars [x,y]
r <- composOp (comp g) t
returnC r
Alts _ -> do
r <- composOp (comp g) t
returnC r
-- remove empty
C a b -> do
a' <- comp g a
b' <- comp g b
case (a',b') of
(Alts _, K a) -> checks [do
as <- strsFromTerm a' -- this may fail when compiling opers
return $ variants [
foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
,
return $ C a' b'
]
(Empty,_) -> returnC b'
(_,Empty) -> returnC a'
_ -> returnC $ C a' b'
-- reduce free variation as much as you can
FV ts -> mapM (comp g) ts >>= returnC . variants
-- merge record extensions if you can
ExtR r s -> do
r' <- comp g r
s' <- comp g s
case (r',s') of
(Alias _ _ d, _) -> comp g $ ExtR d s'
(_, Alias _ _ d) -> comp g $ Glue r' d
(R rs, R ss) -> plusRecord r' s'
(RecType rs, RecType ss) -> plusRecType r' s'
_ -> return $ ExtR r' s'
-- case-expand tables
-- if already expanded, don't expand again
T i@(TComp ty) cs -> do
-- if there are no variables, don't even go inside
cs' <- if (null g) then return cs else mapPairsM (comp g) cs
---- return $ V ty (map snd cs')
return $ T i cs'
--- this means some extra work; should implement TSh directly
TSh i cs -> comp g $ T i [(p,v) | (ps,v) <- cs, p <- ps]
T i cs -> do
pty0 <- getTableType i
ptyp <- comp g pty0
case allParamValues gr ptyp of
Ok vs -> do
cs' <- mapM (compBranchOpt g) cs
sts <- mapM (matchPattern cs') vs
ts <- mapM (\ (c,g') -> comp (g' ++ g) c) sts
ps <- mapM term2patt vs
let ps' = ps --- PT ptyp (head ps) : tail ps
---- return $ V ptyp ts -- to save space, just course of values
return $ T (TComp ptyp) (zip ps' ts)
_ -> do
cs' <- mapM (compBranch g) cs
return $ T i cs' -- happens with variable types
Alias c a d -> do
d' <- comp g d
return $ Alias c a d' -- alias only disappears in certain redexes
-- otherwise go ahead
_ -> composOp (comp g) t >>= returnC
where
compApp g (App f a) = do
f' <- hnf g f
a' <- comp g a
case (f',a') of
(Abs x b, FV as) ->
mapM (\c -> comp (ext x c g) b) as >>= return . variants
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
(Abs x b,_) -> comp (ext x a' g) b
(QC _ _,_) -> returnC $ App f' a'
(Alias _ _ d, _) -> comp g (App d a')
(S (T i cs) e,_) -> prawitz g i (flip App a') cs e
(S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
_ -> do
(t',b) <- appPredefined (App f' a')
if b then return t' else comp g t'
hnf = comput False
comp = comput True
look p c
| rec = lookupResDef gr p c >>= comp []
| otherwise = lookupResDef gr p c
{-
look p c = case lookupResDefKind gr p c of
Ok (t,_) | noExpand p || rec -> comp [] t
Ok (t,_) -> return t
Bad s -> raise s
noExpand p = errVal False $ do
mo <- lookupModMod gr p
return $ case getOptVal (iOpts (flags mo)) useOptimizer of
Just "noexpand" -> True
_ -> False
-}
ext x a g = (x,a):g
returnC = return --- . computed
variants ts = case nub ts of
[t] -> t
ts -> FV ts
isCan v = case v of
Con _ -> True
QC _ _ -> True
App f a -> isCan f && isCan a
R rs -> all (isCan . snd . snd) rs
_ -> False
compBranch g (p,v) = do
let g' = contP p ++ g
v' <- comp g' v
return (p,v')
compBranchOpt g c@(p,v) = case contP p of
[] -> return c
_ -> err (const (return c)) return $ compBranch g c
contP p = case p of
PV x -> [(x,Vr x)]
PC _ ps -> concatMap contP ps
PP _ _ ps -> concatMap contP ps
PT _ p -> contP p
PR rs -> concatMap (contP . snd) rs
PAs x p -> (x,Vr x) : contP p
PSeq p q -> concatMap contP [p,q]
PAlt p q -> concatMap contP [p,q]
PRep p -> contP p
PNeg p -> contP p
_ -> []
prawitz g i f cs e = do
cs' <- mapM (compBranch g) [(p, f v) | (p,v) <- cs]
return $ S (T i cs') e
prawitzV g i f cs e = do
cs' <- mapM (comp g) [(f v) | v <- cs]
return $ S (V i cs') e
-- | argument variables cannot be glued
checkNoArgVars :: Term -> Err Term
checkNoArgVars t = case t of
Vr (IA _) -> Bad $ glueErrorMsg $ prt t
Vr (IAV _) -> Bad $ glueErrorMsg $ prt t
_ -> composOp checkNoArgVars t
glueErrorMsg s =
"Cannot glue (+) term with run-time variable" +++ s ++ "." ++++
"Use Prelude.bind instead."

159
src-3.0/GF/Grammar/LookAbs.hs
View File

@@ -12,28 +12,12 @@
-- (Description of the module)
-----------------------------------------------------------------------------
module GF.Grammar.LookAbs (GFCGrammar,
lookupAbsDef,
module GF.Grammar.LookAbs (
lookupFunType,
lookupCatContext,
lookupTransfer,
isPrimitiveFun,
lookupRef,
refsForType,
funRulesOf,
hasHOAS,
allCatsOf,
allBindCatsOf,
funsForType,
funsOnType,
funsOnTypeFs,
allDefs,
lookupFunTypeSrc,
lookupCatContextSrc
lookupCatContext
) where
import GF.Data.Operations
import qualified GF.Canon.GFC as C
import GF.Grammar.Abstract
import GF.Infra.Ident
@@ -42,155 +26,28 @@ import GF.Infra.Modules
import Data.List (nub)
import Control.Monad
type GFCGrammar = C.CanonGrammar
lookupAbsDef :: GFCGrammar -> Ident -> Ident -> Err (Maybe Term)
lookupAbsDef gr m c = errIn ("looking up absdef of" +++ prt c) $ do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
C.AbsFun _ t -> return $ return t
C.AnyInd _ n -> lookupAbsDef gr n c
_ -> return Nothing
_ -> Bad $ prt m +++ "is not an abstract module"
lookupFunType :: GFCGrammar -> Ident -> Ident -> Err Type
lookupFunType gr m c = errIn ("looking up funtype of" +++ prt c +++ "in module" +++ prt m) $ do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
C.AbsFun t _ -> return t
C.AnyInd _ n -> lookupFunType gr n c
_ -> prtBad "cannot find type of" c
_ -> Bad $ prt m +++ "is not an abstract module"
lookupCatContext :: GFCGrammar -> Ident -> Ident -> Err Context
lookupCatContext gr m c = errIn ("looking up context of cat" +++ prt c) $ do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
C.AbsCat co _ -> return co
C.AnyInd _ n -> lookupCatContext gr n c
_ -> prtBad "unknown category" c
_ -> Bad $ prt m +++ "is not an abstract module"
-- | lookup for transfer function: transfer-module-name, category name
lookupTransfer :: GFCGrammar -> Ident -> Ident -> Err Term
lookupTransfer gr m c = errIn ("looking up transfer of cat" +++ prt c) $ do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
C.AbsTrans t -> return t
C.AnyInd _ n -> lookupTransfer gr n c
_ -> prtBad "cannot transfer function for" c
_ -> Bad $ prt m +++ "is not a transfer module"
-- | should be revised (20\/9\/2003)
isPrimitiveFun :: GFCGrammar -> Fun -> Bool
isPrimitiveFun gr (m,c) = case lookupAbsDef gr m c of
Ok (Just (Eqs [])) -> True -- is canonical
Ok (Just _) -> False -- has defining clauses
_ -> True -- has no definition
-- | looking up refinement terms
lookupRef :: GFCGrammar -> Binds -> Term -> Err Val
lookupRef gr binds at = case at of
Q m f -> lookupFunType gr m f >>= return . vClos
Vr i -> maybeErr ("unknown variable" +++ prt at) $ lookup i binds
EInt _ -> return valAbsInt
EFloat _ -> return valAbsFloat
K _ -> return valAbsString
_ -> prtBad "cannot refine with complex term" at ---
refsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Binds -> Val -> [(Term,(Val,Bool))]
refsForType compat gr binds val =
-- bound variables --- never recursive?
[(Vr i, (t,False)) | (i,t) <- binds, Ok ty <- [val2exp t], compat val ty] ++
-- integer and string literals
[(EInt i, (val,False)) | val == valAbsInt, i <- [0,1,2,5,11,1978]] ++
[(EFloat i, (val,False)) | val == valAbsFloat, i <- [3.1415926]] ++
[(K s, (val,False)) | val == valAbsString, s <- ["foo", "NN", "x"]] ++
-- functions defined in the current abstract syntax
[(qq f, (vClos t,isRecursiveType t)) | (f,t) <- funsForType compat gr val]
funRulesOf :: GFCGrammar -> [(Fun,Type)]
funRulesOf gr =
---- funRulesForLiterals ++
[((i,f),typ) | (i, ModMod m) <- modules gr,
mtype m == MTAbstract,
(f, C.AbsFun typ _) <- tree2list (jments m)]
-- testing for higher-order abstract syntax
hasHOAS :: GFCGrammar -> Bool
hasHOAS gr = any isHigherOrderType [t | (_,t) <- funRulesOf gr] where
allCatsOf :: GFCGrammar -> [(Cat,Context)]
allCatsOf gr =
[((i,c),cont) | (i, ModMod m) <- modules gr,
isModAbs m,
(c, C.AbsCat cont _) <- tree2list (jments m)]
allBindCatsOf :: GFCGrammar -> [Cat]
allBindCatsOf gr =
nub [c | (i, ModMod m) <- modules gr,
isModAbs m,
(c, C.AbsFun typ _) <- tree2list (jments m),
Ok (cont,_) <- [firstTypeForm typ],
c <- concatMap fst $ errVal [] $ mapM (catSkeleton . snd) cont
]
funsForType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [(Fun,Type)]
funsForType compat gr val = [(fun,typ) | (fun,typ) <- funRulesOf gr,
compat val typ]
funsOnType :: (Val -> Type -> Bool) -> GFCGrammar -> Val -> [((Fun,Int),Type)]
funsOnType compat gr = funsOnTypeFs compat (funRulesOf gr)
funsOnTypeFs :: (Val -> Type -> Bool) -> [(Fun,Type)] -> Val -> [((Fun,Int),Type)]
funsOnTypeFs compat fs val = [((fun,i),typ) |
(fun,typ) <- fs,
Ok (args,_,_) <- [typeForm typ],
(i,arg) <- zip [0..] (map snd args),
compat val arg]
allDefs :: GFCGrammar -> [(Fun,Term)]
allDefs gr = [((i,c),d) | (i, ModMod m) <- modules gr,
isModAbs m,
(c, C.AbsFun _ d) <- tree2list (jments m)]
-- | this is needed at compile time
lookupFunTypeSrc :: Grammar -> Ident -> Ident -> Err Type
lookupFunTypeSrc gr m c = do
lookupFunType :: Grammar -> Ident -> Ident -> Err Type
lookupFunType gr m c = do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
AbsFun (Yes t) _ -> return t
AnyInd _ n -> lookupFunTypeSrc gr n c
AnyInd _ n -> lookupFunType gr n c
_ -> prtBad "cannot find type of" c
_ -> Bad $ prt m +++ "is not an abstract module"
-- | this is needed at compile time
lookupCatContextSrc :: Grammar -> Ident -> Ident -> Err Context
lookupCatContextSrc gr m c = do
lookupCatContext :: Grammar -> Ident -> Ident -> Err Context
lookupCatContext gr m c = do
mi <- lookupModule gr m
case mi of
ModMod mo -> do
info <- lookupIdentInfo mo c
case info of
AbsCat (Yes co) _ -> return co
AnyInd _ n -> lookupCatContextSrc gr n c
AnyInd _ n -> lookupCatContext gr n c
_ -> prtBad "unknown category" c
_ -> Bad $ prt m +++ "is not an abstract module"

39
src-3.0/GF/Grammar/PrGrammar.hs
View File

@@ -29,7 +29,7 @@ module GF.Grammar.PrGrammar (Print(..),
tree2string, prprTree,
prConstrs, prConstraints,
prMetaSubst, prEnv, prMSubst,
prExp, prPatt, prOperSignature,
prExp, prOperSignature,
lookupIdent, lookupIdentInfo
) where
@@ -38,8 +38,6 @@ import GF.Data.Zipper
import GF.Grammar.Grammar
import GF.Infra.Modules
import qualified GF.Source.PrintGF as P
import qualified GF.Canon.PrintGFC as C
import qualified GF.Canon.AbsGFC as A
import GF.Grammar.Values
import GF.Source.GrammarToSource
--- import GFC (CanonGrammar) --- cycle of modules
@@ -106,32 +104,6 @@ prContext co = unwords $ map prParenth [prt x +++ ":" +++ prt t | (x,t) <- co]
-- some GFC notions
instance Print A.Exp where prt = C.printTree
instance Print A.Term where prt = C.printTree
instance Print A.Case where prt = C.printTree
instance Print A.CType where prt = C.printTree
instance Print A.Label where prt = C.printTree
instance Print A.Module where prt = C.printTree
instance Print A.Def where prt = C.printTree
instance Print A.Canon where prt = C.printTree
instance Print A.Sort where prt = C.printTree
instance Print A.Atom where
prt = C.printTree
prt_ (A.AC c) = prt_ c
prt_ (A.AD c) = prt_ c
prt_ a = prt a
instance Print A.Patt where
prt = C.printTree
prt_ = prPatt
instance Print A.CIdent where
prt = C.printTree
prt_ (A.CIQ _ c) = prt c
-- printing values and trees in editing
instance Print a => Print (Tr a) where
prt (Tr (n, trees)) = prt n +++ unwords (map prt2 trees)
prt2 t@(Tr (_,args)) = if null args then prt t else prParenth (prt t)
@@ -252,15 +224,6 @@ prExp e = case e of
App _ _ -> prParenth $ prExp e
_ -> pr1 e
prPatt :: A.Patt -> String
prPatt p = case p of
A.PC c ps -> prt_ c +++ unwords (map pr1 ps)
_ -> prt p --- PR
where
pr1 p = case p of
A.PC _ (_:_) -> prParenth $ prPatt p
_ -> prPatt p
-- | option @-strip@ strips qualifications
prTermOpt :: Options -> Term -> String
prTermOpt opts = if oElem nostripQualif opts then prt else prExp

169
src-3.0/GF/Grammar/SGrammar.hs
View File

@@ -1,169 +0,0 @@
----------------------------------------------------------------------
-- |
-- Module : SGrammar
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
--
-- A simple format for context-free abstract syntax used e.g. in
-- generation. AR 31\/3\/2006
--
-- (c) Aarne Ranta 2004 under GNU GPL
--
-- Purpose: to generate corpora. We use simple types and don't
-- guarantee the correctness of bindings\/dependences.
-----------------------------------------------------------------------------
module GF.Grammar.SGrammar where
import GF.Canon.GFC
import GF.Grammar.LookAbs
import GF.Grammar.PrGrammar
import GF.Grammar.Macros
import GF.Grammar.Values
import GF.Grammar.Grammar
import GF.Infra.Ident (Ident)
import GF.Data.Operations
import GF.Data.Zipper
import GF.Infra.Option
import Data.List
-- (c) Aarne Ranta 2006 under GNU GPL
type SGrammar = BinTree SCat [SRule]
type SIdent = String
type SRule = (SFun,SType)
type SType = ([SCat],SCat)
type SCat = SIdent
type SFun = (Double,SIdent)
allRules gr = concat [rs | (c,rs) <- tree2list gr]
data STree =
SApp (SFun,[STree])
| SMeta SCat
| SString String
| SInt Integer
| SFloat Double
deriving (Show,Eq)
depth :: STree -> Int
depth t = case t of
SApp (_,ts@(_:_)) -> maximum (map depth ts) + 1
_ -> 1
type Probs = BinTree Ident Double
emptyProbs :: Probs
emptyProbs = emptyBinTree
prProbs :: Probs -> String
prProbs = unlines . map pr . tree2list where
pr (f,p) = prt f ++ "\t" ++ show p
------------------------------------------
-- translate grammar to simpler form and generated trees back
gr2sgr :: Options -> Probs -> GFCGrammar -> SGrammar
gr2sgr opts probs gr = buildTree [(c,norm (noexp c rs)) | rs@((_,(_,c)):_) <- rules] where
noe = maybe [] (chunks ',') $ getOptVal opts (aOpt "noexpand")
only = maybe [] (chunks ',') $ getOptVal opts (aOpt "doexpand")
un = getOptInt opts (aOpt "atoms")
rules =
prune $
groupBy (\x y -> scat x == scat y) $
sortBy (\x y -> compare (scat x) (scat y)) $
[(trId f, ty') | (f,ty) <- funRulesOf gr, ty' <- trTy ty]
trId (_,f) = let f' = prt f in case lookupTree prt f probs of
Ok p -> (p,f')
_ -> (2.0, f')
trTy ty = case catSkeleton ty of
Ok (mcs,mc) -> [(map trCat mcs, trCat mc)]
_ -> []
trCat (m,c) = prt c ---
scat (_,(_,c)) = c
prune rs = maybe rs (\n -> map (onlyAtoms n) rs) $ un
norm = fillProb
onlyAtoms n rs =
let (rs1,rs2) = partition atom rs
in take n rs1 ++ rs2
atom = null . fst . snd
noexp c rs
| null only = if elem c noe then [((2.0,'?':c),([],c))] else rs
| otherwise = if elem c only then rs else [((2.0,'?':c),([],c))]
-- for cases where explicit probability is not given (encoded as
-- p > 1) divide the remaining mass by the number of such cases
fillProb :: [SRule] -> [SRule]
fillProb rs = [((defa p,f),ty) | ((p,f),ty) <- rs] where
defa p = if p > 1.0 then def else p
def = (1 - sum given) / genericLength nope
(nope,given) = partition (> 1.0) [p | ((p,_),_) <- rs]
-- str2tr :: STree -> Exp
str2tr t = case t of
SApp ((_,'?':c),[]) -> mkMeta 0 -- from noexpand=c
SApp ((_,f),ts) -> mkApp (trId f) (map str2tr ts)
SMeta _ -> mkMeta 0
SString s -> K s
SInt i -> EInt i
SFloat i -> EFloat i
where
trId = cn . zIdent
-- tr2str :: Tree -> STree
tr2str (Tr (N (_,at,val,_,_),ts)) = case (at,val) of
(AtC (_,f), _) -> SApp ((2.0,prt_ f),map tr2str ts)
(AtM _, v) -> SMeta (catOf v)
(AtL s, _) -> SString s
(AtI i, _) -> SInt i
(AtF i, _) -> SFloat i
_ -> SMeta "FAILED_TO_GENERATE" ---- err monad!
where
catOf v = case v of
VApp w _ -> catOf w
VCn (_,c) -> prt_ c
_ -> "FAILED_TO_GENERATE_FROM_META"
------------------------------------------
-- to test
prSTree t = case t of
SApp ((_,f),ts) -> f ++ concat (map pr1 ts)
SMeta c -> '?':c
SString s -> prQuotedString s
SInt i -> show i
SFloat i -> show i
where
pr1 t@(SApp (_,ts)) = ' ' : (if null ts then id else prParenth) (prSTree t)
pr1 t = prSTree t
pSRule :: String -> SRule
pSRule s = case words s of
f : _ : cs -> ((2.0,f),(init cs', last cs'))
where cs' = [cs !! i | i <- [0,2..length cs - 1]]
_ -> error $ "not a rule" +++ s
exSgr = map pSRule [
"Pred : NP -> VP -> S"
,"Compl : TV -> NP -> VP"
,"PredVV : VV -> VP -> VP"
,"DefCN : CN -> NP"
,"ModCN : AP -> CN -> CN"
,"john : NP"
,"walk : VP"
,"love : TV"
,"try : VV"
,"girl : CN"
,"big : AP"
]

299
src-3.0/GF/Grammar/TC.hs
View File

@@ -1,299 +0,0 @@
----------------------------------------------------------------------
-- |
-- Module : TC
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/10/02 20:50:19 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.11 $
--
-- Thierry Coquand's type checking algorithm that creates a trace
-----------------------------------------------------------------------------
module GF.Grammar.TC (AExp(..),
Theory,
checkExp,
inferExp,
checkEqs,
eqVal,
whnf
) where
import GF.Data.Operations
import GF.Grammar.Abstract
import GF.Grammar.AbsCompute
import Control.Monad
import Data.List (sortBy)
data AExp =
AVr Ident Val
| ACn QIdent Val
| AType
| AInt Integer
| AFloat Double
| AStr String
| AMeta MetaSymb Val
| AApp AExp AExp Val
| AAbs Ident Val AExp
| AProd Ident AExp AExp
| AEqs [([Exp],AExp)] --- not used
| AData Val
deriving (Eq,Show)
type Theory = QIdent -> Err Val
lookupConst :: Theory -> QIdent -> Err Val
lookupConst th f = th f
lookupVar :: Env -> Ident -> Err Val
lookupVar g x = maybe (prtBad "unknown variable" x) return $ lookup x ((IW,uVal):g)
-- wild card IW: no error produced, ?0 instead.
type TCEnv = (Int,Env,Env)
emptyTCEnv :: TCEnv
emptyTCEnv = (0,[],[])
whnf :: Val -> Err Val
whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
case v of
VApp u w -> do
u' <- whnf u
w' <- whnf w
app u' w'
VClos env e -> eval env e
_ -> return v
app :: Val -> Val -> Err Val
app u v = case u of
VClos env (Abs x e) -> eval ((x,v):env) e
_ -> return $ VApp u v
eval :: Env -> Exp -> Err Val
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
case e of
Vr x -> lookupVar env x
Q m c -> return $ VCn (m,c)
QC m c -> return $ VCn (m,c) ---- == Q ?
Sort c -> return $ VType --- the only sort is Type
App f a -> join $ liftM2 app (eval env f) (eval env a)
_ -> return $ VClos env e
eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
do
w1 <- whnf u1
w2 <- whnf u2
let v = VGen k
case (w1,w2) of
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
(VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
liftM2 (++)
(eqVal k (VClos env1 a1) (VClos env2 a2))
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
(VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
(VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
--- thus ignore qualifications; valid because inheritance cannot
--- be qualified. Simplifies annotation. AR 17/3/2005
_ -> return [(w1,w2) | w1 /= w2]
-- invariant: constraints are in whnf
checkType :: Theory -> TCEnv -> Exp -> Err (AExp,[(Val,Val)])
checkType th tenv e = checkExp th tenv e vType
checkExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
checkExp th tenv@(k,rho,gamma) e ty = do
typ <- whnf ty
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
a' <- whnf $ VClos env a ---
(t',cs) <- checkExp th
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
return (AAbs x a' t', cs)
_ -> prtBad ("function type expected for" +++ prt e +++ "instead of") typ
-- {- --- to get deprec when checkEqs works (15/9/2005)
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
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
return (AProd x a' b', csa ++ csb)
_ -> checkInferExp th tenv e typ
checkInferExp :: Theory -> TCEnv -> Exp -> Val -> Err (AExp, [(Val,Val)])
checkInferExp th tenv@(k,_,_) e typ = do
(e',w,cs1) <- inferExp th tenv e
cs2 <- eqVal k w typ
return (e',cs1 ++ cs2)
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
inferExp th tenv@(k,rho,gamma) e = case e of
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
Q m c
| m == cPredefAbs && (elem c (map identC ["Int","String","Float"])) ->
return (ACn (m,c) vType, vType, [])
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
EInt i -> return (AInt i, valAbsInt, [])
EFloat i -> return (AFloat i, valAbsFloat, [])
K i -> return (AStr i, valAbsString, [])
Sort _ -> return (AType, vType, [])
App f t -> do
(f',w,csf) <- inferExp th tenv f
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
(a',csa) <- checkExp th tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
_ -> prtBad "cannot infer type of expression" e
where
predefAbs c s = case c of
IC "Int" -> return $ const $ Q cPredefAbs cInt
IC "Float" -> return $ const $ Q cPredefAbs cFloat
IC "String" -> return $ const $ Q cPredefAbs cString
_ -> Bad s
checkEqs :: Theory -> TCEnv -> (Fun,Trm) -> Val -> Err [(Val,Val)]
checkEqs th tenv@(k,rho,gamma) (fun@(m,f),def) val = case def of
Eqs es -> liftM concat $ mapM checkBranch es
_ -> liftM snd $ checkExp th tenv def val
where
checkBranch (ps,df) =
let
(ps',_,vars) = foldr p2t ([],0,[]) ps
fps = mkApp (Q m f) ps'
in errIn ("branch" +++ prt fps) $ do
(aexp, typ, cs1) <- inferExp th tenv fps
let
bds = binds vars aexp
tenv' = (k, rho, bds ++ gamma)
(_,cs2) <- errIn (show bds) $ checkExp th tenv' df typ
return $ (cs1 ++ cs2)
p2t p (ps,i,g) = case p of
PW -> (meta (MetaSymb i) : ps, i+1, g)
PV IW -> (meta (MetaSymb i) : ps, i+1, g)
PV x -> (meta (MetaSymb i) : ps, i+1,upd x i g)
PString s -> ( K s : ps, i, g)
PInt n -> (EInt n : ps, i, g)
PFloat n -> (EFloat n : ps, i, g)
PP m c xs -> (mkApp (qq (m,c)) xss : ps, i', g')
where (xss,i',g') = foldr p2t ([],i,g) xs
_ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
upd x i g = (x,i) : g --- to annotate pattern variables: treat as metas
-- notice: in vars, the sequence 0.. is sorted. In subst aexp, all
-- this occurs and nothing else.
binds vars aexp = [(x,v) | ((x,_),v) <- zip vars metas] where
metas = map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ subst aexp
subst aexp = case aexp of
AMeta (MetaSymb i) v -> [(i,v)]
AApp c a _ -> subst c ++ subst a
_ -> [] -- never matter in patterns
checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Exp],AExp),[(Val,Val)])
checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
chB tenv' ps' ty
where
(ps',_,rho2,k') = ps2ts k ps
tenv' = (k, rho2++rho, gamma) ---- k' ?
(k,rho,gamma) = tenv
chB tenv@(k,rho,gamma) ps ty = case ps of
p:ps2 -> do
typ <- whnf ty
case typ of
VClos env (Prod y a b) -> do
a' <- whnf $ VClos env a
(p', sigma, binds, cs1) <- checkP tenv p y a'
let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
_ -> prtBad ("Product expected for definiens" +++prt t +++ "instead of") typ
[] -> do
(e,cs) <- checkExp th tenv t ty
return (([],e),cs)
checkP env@(k,rho,gamma) t x a = do
(delta,cs) <- checkPatt th env t a
let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
return (VClos sigma t, sigma, delta, cs)
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)
PFloat n -> (EFloat n : ps, i, g, k)
PP m c xs -> (mkApp (qq (m,c)) xss : ps, j, g',k')
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
_ -> error $ "undefined p2t case" +++ prt p +++ "in checkBranch"
upd x k g = (x, VGen k x) : g --- hack to recognize pattern variables
checkPatt :: Theory -> TCEnv -> Exp -> Val -> Err (Binds,[(Val,Val)])
checkPatt th tenv exp val = do
(aexp,_,cs) <- checkExpP tenv exp val
let binds = extrBinds aexp
return (binds,cs)
where
extrBinds aexp = case aexp of
AVr i v -> [(i,v)]
AApp f a _ -> extrBinds f ++ extrBinds a
_ -> [] -- no other cases are possible
--- ad hoc, to find types of variables
checkExpP tenv@(k,rho,gamma) exp val = case exp of
Meta m -> return $ (AMeta m val, val, [])
Vr x -> return $ (AVr x val, val, [])
EInt i -> return (AInt i, valAbsInt, [])
EFloat i -> return (AFloat i, valAbsFloat, [])
K s -> return (AStr s, valAbsString, [])
Q m c -> do
typ <- lookupConst th (m,c)
return $ (ACn (m,c) typ, typ, [])
QC m c -> do
typ <- lookupConst th (m,c)
return $ (ACn (m,c) typ, typ, []) ----
App f t -> do
(f',w,csf) <- checkExpP tenv f val
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
(a',_,csa) <- checkExpP tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
_ -> prtBad ("Prod expected for function" +++ prt f +++ "instead of") typ
_ -> prtBad "cannot typecheck pattern" exp
-- auxiliaries
noConstr :: Err Val -> Err (Val,[(Val,Val)])
noConstr er = er >>= (\v -> return (v,[]))
mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
mkAnnot a ti = do
(v,cs) <- ti
return (a v, v, cs)

311
src-3.0/GF/Grammar/TypeCheck.hs
View File

@@ -1,311 +0,0 @@
----------------------------------------------------------------------
-- |
-- Module : TypeCheck
-- Maintainer : AR
-- Stability : (stable)
-- Portability : (portable)
--
-- > CVS $Date: 2005/09/15 16:22:02 $
-- > CVS $Author: aarne $
-- > CVS $Revision: 1.16 $
--
-- (Description of the module)
-----------------------------------------------------------------------------
module GF.Grammar.TypeCheck (-- * top-level type checking functions; TC should not be called directly.
annotate, annotateIn,
justTypeCheck, checkIfValidExp,
reduceConstraints,
splitConstraints,
possibleConstraints,
reduceConstraintsNode,
performMetaSubstNode,
-- * some top-level batch-mode checkers for the compiler
justTypeCheckSrc,
grammar2theorySrc,
checkContext,
checkTyp,
checkEquation,
checkConstrs,
editAsTermCommand,
exp2termCommand,
exp2termlistCommand,
tree2termlistCommand
) where
import GF.Data.Operations
import GF.Data.Zipper
import GF.Grammar.Abstract
import GF.Grammar.AbsCompute
import GF.Grammar.Refresh
import GF.Grammar.LookAbs
import qualified GF.Grammar.Lookup as Lookup ---
import GF.Grammar.TC
import GF.Grammar.Unify ---
import Control.Monad (foldM, liftM, liftM2)
import Data.List (nub) ---
-- top-level type checking functions; TC should not be called directly.
annotate :: GFCGrammar -> Exp -> Err Tree
annotate gr exp = annotateIn gr [] exp Nothing
-- | type check in empty context, return a list of constraints
justTypeCheck :: GFCGrammar -> Exp -> Val -> Err Constraints
justTypeCheck gr e v = do
(_,constrs0) <- checkExp (grammar2theory gr) (initTCEnv []) e v
constrs1 <- reduceConstraints (lookupAbsDef gr) 0 constrs0
return $ fst $ splitConstraints gr constrs1
-- | type check in empty context, return the expression itself if valid
checkIfValidExp :: GFCGrammar -> Exp -> Err Exp
checkIfValidExp gr e = do
(_,_,constrs0) <- inferExp (grammar2theory gr) (initTCEnv []) e
constrs1 <- reduceConstraints (lookupAbsDef gr) 0 constrs0
ifNull (return e) (Bad . unwords . prConstrs) constrs1
annotateIn :: GFCGrammar -> Binds -> Exp -> Maybe Val -> Err Tree
annotateIn gr gamma exp = maybe (infer exp) (check exp) where
infer e = do
(a,_,cs) <- inferExp theory env e
aexp2treeC (a,cs)
check e v = do
(a,cs) <- checkExp theory env e v
aexp2treeC (a,cs)
env = initTCEnv gamma
theory = grammar2theory gr
aexp2treeC (a,c) = do
c' <- reduceConstraints (lookupAbsDef gr) (length gamma) c
aexp2tree (a,c')
-- | invariant way of creating TCEnv from context
initTCEnv gamma =
(length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
-- | process constraints after eqVal by computing by defs
reduceConstraints :: LookDef -> Int -> Constraints -> Err Constraints
reduceConstraints look i = liftM concat . mapM redOne where
redOne (u,v) = do
u' <- computeVal look u
v' <- computeVal look v
eqVal i u' v'
computeVal :: LookDef -> Val -> Err Val
computeVal look v = case v of
VClos g@(_:_) e -> do
e' <- compt (map fst g) e --- bindings of g in e?
whnf $ VClos g e'
{- ----
_ -> do ---- how to compute a Val, really??
e <- val2exp v
e' <- compt [] e
whnf $ vClos e'
-}
VApp f c -> liftM2 VApp (compv f) (compv c) >>= whnf
_ -> whnf v
where
compt = computeAbsTermIn look
compv = computeVal look
-- | take apart constraints that have the form (? <> t), usable as solutions
splitConstraints :: GFCGrammar -> Constraints -> (Constraints,MetaSubst)
splitConstraints gr = splitConstraintsGen (lookupAbsDef gr)
splitConstraintsSrc :: Grammar -> Constraints -> (Constraints,MetaSubst)
splitConstraintsSrc gr = splitConstraintsGen (Lookup.lookupAbsDef gr)
splitConstraintsGen :: LookDef -> Constraints -> (Constraints,MetaSubst)
splitConstraintsGen look cs = csmsu where
csmsu = (nub [(a,b) | (a,b) <- csf1,a /= b],msf1)
(csf1,msf1) = unif (csf,msf) -- alternative: filter first
(csf,msf) = foldr mkOne ([],[]) cs
csmsf = foldr mkOne ([],msu) csu
(csu,msu) = unif (cs1,[]) -- alternative: unify first
cs1 = errVal cs $ reduceConstraints look 0 cs
mkOne (u,v) = case (u,v) of
(VClos g (Meta m), v) | null g -> sub m v
(v, VClos g (Meta m)) | null g -> sub m v
-- do nothing if meta has nonempty closure; null g || isConstVal v WAS WRONG
c -> con c
con c (cs,ms) = (c:cs,ms)
sub m v (cs,ms) = (cs,(m,v):ms)
unifo = id -- alternative: don't use unification
unif cm@(cs,ms) = errVal cm $ do --- alternative: use unification
(cs',ms') <- unifyVal cs
return (cs', ms' ++ ms)
performMetaSubstNode :: MetaSubst -> TrNode -> TrNode
performMetaSubstNode subst n@(N (b,a,v,(c,m),s)) = let
v' = metaSubstVal v
b' = [(x,metaSubstVal v) | (x,v) <- b]
c' = [(u',v') | (u,v) <- c,
let (u',v') = (metaSubstVal u, metaSubstVal v), u' /= v']
in N (b',a,v',(c',m),s)
where
metaSubstVal u = errVal u $ whnf $ case u of
VApp f a -> VApp (metaSubstVal f) (metaSubstVal a)
VClos g e -> VClos [(x,metaSubstVal v) | (x,v) <- g] (metaSubstExp e)
_ -> u
metaSubstExp e = case e of
Meta m -> errVal e $ maybe (return e) val2expSafe $ lookup m subst
_ -> composSafeOp metaSubstExp e
reduceConstraintsNode :: GFCGrammar -> TrNode -> TrNode
reduceConstraintsNode gr = changeConstrs red where
red cs = errVal cs $ reduceConstraints (lookupAbsDef gr) 0 cs
-- | weak heuristic to narrow down menus; not used for TC. 15\/11\/2001.
-- the age-old method from GF 0.9
possibleConstraints :: GFCGrammar -> Constraints -> Bool
possibleConstraints gr = and . map (possibleConstraint gr)
possibleConstraint :: GFCGrammar -> (Val,Val) -> Bool
possibleConstraint gr (u,v) = errVal True $ do
u' <- val2exp u >>= compute gr
v' <- val2exp v >>= compute gr
return $ cts u' v'
where
cts t u = isUnknown t || isUnknown u || case (t,u) of
(Q m c, Q n d) -> c == d || notCan (m,c) || notCan (n,d)
(QC m c, QC n d) -> c == d
(App f a, App g b) -> cts f g && cts a b
(Abs x b, Abs y c) -> cts b c
(Prod x a f, Prod y b g) -> cts a b && cts f g
(_ , _) -> False
isUnknown t = case t of
Vr _ -> True
Meta _ -> True
_ -> False
notCan = not . isPrimitiveFun gr
-- interface to TC type checker
type2val :: Type -> Val
type2val = VClos []
aexp2tree :: (AExp,[(Val,Val)]) -> Err Tree
aexp2tree (aexp,cs) = do
(bi,at,vt,ts) <- treeForm aexp
ts' <- mapM aexp2tree [(t,[]) | t <- ts]
return $ Tr (N (bi,at,vt,(cs,[]),False),ts')
where
treeForm a = case a of
AAbs x v b -> do
(bi, at, vt, args) <- treeForm b
v' <- whnf v ---- should not be needed...
return ((x,v') : bi, at, vt, args)
AApp c a v -> do
(_,at,_,args) <- treeForm c
v' <- whnf v ----
return ([],at,v',args ++ [a])
AVr x v -> do
v' <- whnf v ----
return ([],AtV x,v',[])
ACn c v -> do
v' <- whnf v ----
return ([],AtC c,v',[])
AInt i -> do
return ([],AtI i,valAbsInt,[])
AFloat i -> do
return ([],AtF i,valAbsFloat,[])
AStr s -> do
return ([],AtL s,valAbsString,[])
AMeta m v -> do
v' <- whnf v ----
return ([],AtM m,v',[])
_ -> Bad "illegal tree" -- AProd
grammar2theory :: GFCGrammar -> Theory
grammar2theory gr (m,f) = case lookupFunType gr m f of
Ok t -> return $ type2val t
Bad s -> case lookupCatContext gr m f of
Ok cont -> return $ cont2val cont
_ -> Bad s
cont2exp :: Context -> Exp
cont2exp c = mkProd (c, eType, []) -- to check a context
cont2val :: Context -> Val
cont2val = type2val . cont2exp
-- some top-level batch-mode checkers for the compiler
justTypeCheckSrc :: Grammar -> Exp -> Val -> Err Constraints
justTypeCheckSrc gr e v = do
(_,constrs0) <- checkExp (grammar2theorySrc gr) (initTCEnv []) e v
return $ filter notJustMeta constrs0
---- return $ fst $ splitConstraintsSrc gr constrs0
---- this change was to force proper tc of abstract modules.
---- May not be quite right. AR 13/9/2005
notJustMeta (c,k) = case (c,k) of
(VClos g1 (Meta m1), VClos g2 (Meta m2)) -> False
_ -> True
grammar2theorySrc :: Grammar -> Theory
grammar2theorySrc gr (m,f) = case lookupFunTypeSrc gr m f of
Ok t -> return $ type2val t
Bad s -> case lookupCatContextSrc gr m f of
Ok cont -> return $ cont2val cont
_ -> Bad s
checkContext :: Grammar -> Context -> [String]
checkContext st = checkTyp st . cont2exp
checkTyp :: Grammar -> Type -> [String]
checkTyp gr typ = err singleton prConstrs $ justTypeCheckSrc gr typ vType
checkEquation :: Grammar -> Fun -> Trm -> [String]
checkEquation gr (m,fun) def = err singleton id $ do
typ <- lookupFunTypeSrc gr m fun
---- cs <- checkEqs (grammar2theorySrc gr) (initTCEnv []) ((m,fun),def) (vClos typ)
cs <- justTypeCheckSrc gr def (vClos typ)
let cs1 = filter notJustMeta cs ----- filter (not . possibleConstraint gr) cs ----
return $ ifNull [] (singleton . prConstraints) cs1
checkConstrs :: Grammar -> Cat -> [Ident] -> [String]
checkConstrs gr cat _ = [] ---- check constructors!
{- ----
err singleton concat . mapM checkOne where
checkOne con = do
typ <- lookupFunType gr con
typ' <- computeAbsTerm gr typ
vcat <- valCat typ'
return $ if (cat == vcat) then [] else ["wrong type in constructor" +++ prt con]
-}
editAsTermCommand :: GFCGrammar -> (Loc TrNode -> Err (Loc TrNode)) -> Exp -> [Exp]
editAsTermCommand gr c e = err (const []) singleton $ do
t <- annotate gr $ refreshMetas [] e
t' <- c $ tree2loc t
return $ tree2exp $ loc2tree t'
exp2termCommand :: GFCGrammar -> (Exp -> Err Exp) -> Tree -> Err Tree
exp2termCommand gr f t = errIn ("modifying term" +++ prt t) $ do
let exp = tree2exp t
exp2 <- f exp
annotate gr exp2
exp2termlistCommand :: GFCGrammar -> (Exp -> [Exp]) -> Tree -> [Tree]
exp2termlistCommand gr f = err (const []) fst . mapErr (annotate gr) . f . tree2exp
tree2termlistCommand :: GFCGrammar -> (Tree -> [Exp]) -> Tree -> [Tree]
tree2termlistCommand gr f = err (const []) fst . mapErr (annotate gr) . f