mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-14 15:29:31 -06:00
native representation for HOAS in PMCFG and incremental type checking of the parse forest
This commit is contained in:
krasimir
@@ -51,6 +51,7 @@ instance Binary Concr where
|
||||
put (printnames cnc)
|
||||
putArray2 (sequences cnc)
|
||||
putArray (cncfuns cnc)
|
||||
put (lindefs cnc)
|
||||
put (productions cnc)
|
||||
put (cnccats cnc)
|
||||
put (totalCats cnc)
|
||||
@@ -58,11 +59,13 @@ instance Binary Concr where
|
||||
printnames <- get
|
||||
sequences <- getArray2
|
||||
cncfuns <- getArray
|
||||
lindefs <- get
|
||||
productions <- get
|
||||
cnccats <- get
|
||||
totalCats <- get
|
||||
return (Concr{ cflags=cflags, printnames=printnames
|
||||
, sequences=sequences, cncfuns=cncfuns, productions=productions
|
||||
, sequences=sequences, cncfuns=cncfuns, lindefs=lindefs
|
||||
, productions=productions
|
||||
, pproductions = IntMap.empty
|
||||
, lproductions = Map.empty
|
||||
, cnccats=cnccats, totalCats=totalCats
|
||||
@@ -141,16 +144,22 @@ instance Binary CncCat where
|
||||
instance Binary Symbol where
|
||||
put (SymCat n l) = putWord8 0 >> put (n,l)
|
||||
put (SymLit n l) = putWord8 1 >> put (n,l)
|
||||
put (SymKS ts) = putWord8 2 >> put ts
|
||||
put (SymKP d vs) = putWord8 3 >> put (d,vs)
|
||||
put (SymVar n l) = putWord8 2 >> put (n,l)
|
||||
put (SymKS ts) = putWord8 3 >> put ts
|
||||
put (SymKP d vs) = putWord8 4 >> put (d,vs)
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 SymCat get get
|
||||
1 -> liftM2 SymLit get get
|
||||
2 -> liftM SymKS get
|
||||
3 -> liftM2 (\d vs -> SymKP d vs) get get
|
||||
2 -> liftM2 SymVar get get
|
||||
3 -> liftM SymKS get
|
||||
4 -> liftM2 (\d vs -> SymKP d vs) get get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary PArg where
|
||||
put (PArg hypos fid) = put (map snd hypos,fid)
|
||||
get = get >>= \(hypos,fid) -> return (PArg (zip (repeat fidVar) hypos) fid)
|
||||
|
||||
instance Binary Production where
|
||||
put (PApply ruleid args) = putWord8 0 >> put (ruleid,args)
|
||||
put (PCoerce fcat) = putWord8 1 >> put fcat
|
||||
|
||||
@@ -36,6 +36,7 @@ data Concr = Concr {
|
||||
cflags :: Map.Map CId Literal, -- value of a flag
|
||||
printnames :: Map.Map CId String, -- printname of a cat or a fun
|
||||
cncfuns :: Array FunId CncFun,
|
||||
lindefs :: IntMap.IntMap [FunId],
|
||||
sequences :: Array SeqId Sequence,
|
||||
productions :: IntMap.IntMap (Set.Set Production), -- the original productions loaded from the PGF file
|
||||
pproductions :: IntMap.IntMap (Set.Set Production), -- productions needed for parsing
|
||||
@@ -51,14 +52,16 @@ type DotPos = Int
|
||||
data Symbol
|
||||
= SymCat {-# UNPACK #-} !Int {-# UNPACK #-} !LIndex
|
||||
| SymLit {-# UNPACK #-} !Int {-# UNPACK #-} !LIndex
|
||||
| SymVar {-# UNPACK #-} !Int {-# UNPACK #-} !Int
|
||||
| SymKS [Token]
|
||||
| SymKP [Token] [Alternative]
|
||||
deriving (Eq,Ord,Show)
|
||||
data Production
|
||||
= PApply {-# UNPACK #-} !FunId [FId]
|
||||
= PApply {-# UNPACK #-} !FunId [PArg]
|
||||
| PCoerce {-# UNPACK #-} !FId
|
||||
| PConst CId Expr [Token]
|
||||
deriving (Eq,Ord,Show)
|
||||
data PArg = PArg [(FId,FId)] {-# UNPACK #-} !FId deriving (Eq,Ord,Show)
|
||||
data CncCat = CncCat {-# UNPACK #-} !FId {-# UNPACK #-} !FId {-# UNPACK #-} !(Array LIndex String)
|
||||
data CncFun = CncFun CId {-# UNPACK #-} !(UArray LIndex SeqId) deriving (Eq,Ord,Show)
|
||||
type Sequence = Array DotPos Symbol
|
||||
|
||||
@@ -14,12 +14,14 @@
|
||||
module PGF.Forest( Forest(..)
|
||||
, BracketedString, showBracketedString, lengthBracketedString
|
||||
, linearizeWithBrackets
|
||||
, getAbsTrees
|
||||
, foldForest
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
import PGF.Data
|
||||
import PGF.Macros
|
||||
import PGF.TypeCheck
|
||||
import Data.List
|
||||
import Data.Array.IArray
|
||||
import qualified Data.Set as Set
|
||||
@@ -34,7 +36,7 @@ data Forest
|
||||
{ abstr :: Abstr
|
||||
, concr :: Concr
|
||||
, forest :: IntMap.IntMap (Set.Set Production)
|
||||
, root :: [([Symbol],[FId])]
|
||||
, root :: [([Symbol],[PArg])]
|
||||
}
|
||||
|
||||
--------------------------------------------------------------------
|
||||
@@ -51,29 +53,39 @@ linearizeWithBrackets = head . snd . untokn "" . bracketedTokn
|
||||
|
||||
bracketedTokn :: Forest -> BracketedTokn
|
||||
bracketedTokn f@(Forest abs cnc forest root) =
|
||||
case [computeSeq seq (map (render forest) args) | (seq,args) <- root] of
|
||||
case [computeSeq isTrusted seq (map (render forest) args) | (seq,args) <- root] of
|
||||
([bs@(Bracket_ _ _ _ _ _)]:_) -> bs
|
||||
(bss:_) -> Bracket_ wildCId 0 0 [] bss
|
||||
[] -> Bracket_ wildCId 0 0 [] []
|
||||
where
|
||||
isTrusted (_,fid) = IntSet.member fid trusted
|
||||
|
||||
trusted = foldl1 IntSet.intersection [IntSet.unions (map (trustedSpots IntSet.empty) args) | (_,args) <- root]
|
||||
|
||||
render forest fid =
|
||||
render forest arg@(PArg hypos fid) =
|
||||
case IntMap.lookup fid forest >>= Set.maxView of
|
||||
Just (p,set) -> descend (if Set.null set then forest else IntMap.insert fid set forest) p
|
||||
Just (p,set) -> let (ct,es,(_,lin)) = descend (if Set.null set then forest else IntMap.insert fid set forest) p
|
||||
in (ct,es,(map getVar hypos,lin))
|
||||
Nothing -> error ("wrong forest id " ++ show fid)
|
||||
where
|
||||
descend forest (PApply funid args) = let (CncFun fun lins) = cncfuns cnc ! funid
|
||||
Just (DTyp _ cat _,_,_) = Map.lookup fun (funs abs)
|
||||
largs = map (render forest) args
|
||||
ltable = listArray (bounds lins)
|
||||
[computeSeq (elems (sequences cnc ! seqid)) largs |
|
||||
seqid <- elems lins]
|
||||
in (fid,cat,ltable)
|
||||
descend forest (PCoerce fid) = render forest fid
|
||||
descend forest (PConst cat _ ts) = (fid,cat,listArray (0,0) [[LeafKS ts]])
|
||||
cat = case isLindefCId fun of
|
||||
Just cat -> cat
|
||||
Nothing -> case Map.lookup fun (funs abs) of
|
||||
Just (DTyp _ cat _,_,_) -> cat
|
||||
largs = map (render forest) args
|
||||
ltable = mkLinTable cnc isTrusted [] funid largs
|
||||
in ((cat,fid),either (const []) id $ getAbsTrees f arg Nothing,ltable)
|
||||
descend forest (PCoerce fid) = render forest (PArg [] fid)
|
||||
descend forest (PConst cat e ts) = ((cat,fid),[e],([],listArray (0,0) [[LeafKS ts]]))
|
||||
|
||||
trustedSpots parents fid
|
||||
getVar (fid,_)
|
||||
| fid == fidVar = wildCId
|
||||
| otherwise = x
|
||||
where
|
||||
(x:_) = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)]
|
||||
|
||||
trustedSpots parents (PArg _ fid)
|
||||
| fid < totalCats cnc || -- forest ids from the grammar correspond to metavariables
|
||||
IntSet.member fid parents -- this avoids loops in the grammar
|
||||
= IntSet.empty
|
||||
@@ -85,65 +97,116 @@ bracketedTokn f@(Forest abs cnc forest root) =
|
||||
parents' = IntSet.insert fid parents
|
||||
|
||||
descend (PApply funid args) = IntSet.unions (map (trustedSpots parents') args)
|
||||
descend (PCoerce fid) = trustedSpots parents' fid
|
||||
descend (PCoerce fid) = trustedSpots parents' (PArg [] fid)
|
||||
descend (PConst c e _) = IntSet.empty
|
||||
|
||||
computeSeq :: [Symbol] -> [(FId,CId,LinTable)] -> [BracketedTokn]
|
||||
computeSeq seq args = concatMap compute seq
|
||||
where
|
||||
compute (SymCat d r) = getArg d r
|
||||
compute (SymLit d r) = getArg d r
|
||||
compute (SymKS ts) = [LeafKS ts]
|
||||
compute (SymKP ts alts) = [LeafKP ts alts]
|
||||
|
||||
getArg d r
|
||||
| not (null arg_lin) &&
|
||||
IntSet.member fid trusted
|
||||
= [Bracket_ cat fid r es arg_lin]
|
||||
| otherwise = arg_lin
|
||||
where
|
||||
arg_lin = lin ! r
|
||||
(fid,cat,lin) = args !! d
|
||||
es = getAbsTrees f fid
|
||||
isLindefCId id
|
||||
| take l s == lindef = Just (mkCId (drop l s))
|
||||
| otherwise = Nothing
|
||||
where
|
||||
s = showCId id
|
||||
lindef = "lindef "
|
||||
l = length lindef
|
||||
|
||||
-- | This function extracts the list of all completed parse trees
|
||||
-- that spans the whole input consumed so far. The trees are also
|
||||
-- limited by the category specified, which is usually
|
||||
-- the same as the startup category.
|
||||
getAbsTrees :: Forest -> FId -> [Expr]
|
||||
getAbsTrees (Forest abs cnc forest root) fid =
|
||||
nubsort $ do (fvs,e) <- go Set.empty 0 (0,fid)
|
||||
guard (Set.null fvs)
|
||||
return e
|
||||
getAbsTrees :: Forest -> PArg -> Maybe Type -> Either [(FId,TcError)] [Expr]
|
||||
getAbsTrees (Forest abs cnc forest root) arg@(PArg _ fid) ty =
|
||||
let (res,err) = unTcFM (do e <- go Set.empty emptyScope arg (fmap (TTyp []) ty)
|
||||
e <- runTcM abs fid (refineExpr e)
|
||||
runTcM abs fid (checkResolvedMetaStore emptyScope e)
|
||||
return e) IntMap.empty
|
||||
in if null res
|
||||
then Left (nub err)
|
||||
else Right (nubsort (map snd res))
|
||||
where
|
||||
go rec_ fcat' (d,fcat)
|
||||
| fcat < totalCats cnc = return (Set.empty,EMeta (fcat'*10+d)) -- FIXME: here we assume that every rule has at most 10 arguments
|
||||
| Set.member fcat rec_ = mzero
|
||||
| otherwise = foldForest (\funid args trees ->
|
||||
go rec_ scope_ (PArg hypos fid) mb_tty_
|
||||
| fid < totalCats cnc = case mb_tty of
|
||||
Just tty -> do i <- runTcM abs fid (newMeta scope tty)
|
||||
return (mkAbs (EMeta i))
|
||||
Nothing -> mzero
|
||||
| Set.member fid rec_ = mzero
|
||||
| otherwise = foldForest (\funid args trees ->
|
||||
do let CncFun fn lins = cncfuns cnc ! funid
|
||||
args <- mapM (go (Set.insert fcat rec_) fcat) (zip [0..] args)
|
||||
check_ho_fun fn args
|
||||
case isLindefCId fn of
|
||||
Just _ -> do arg <- go (Set.insert fid rec_) scope (head args) mb_tty
|
||||
return (mkAbs arg)
|
||||
Nothing -> do tty_fn <- runTcM abs fid (lookupFunType fn)
|
||||
(e,tty0) <- foldM (\(e1,tty) arg -> goArg (Set.insert fid rec_) scope fid e1 arg tty)
|
||||
(EFun fn,tty_fn) args
|
||||
case mb_tty of
|
||||
Just tty -> runTcM abs fid $ do
|
||||
i <- newGuardedMeta e
|
||||
eqType scope (scopeSize scope) i tty tty0
|
||||
Nothing -> return ()
|
||||
return (mkAbs e)
|
||||
`mplus`
|
||||
trees)
|
||||
(\const _ trees ->
|
||||
return (freeVar const,const)
|
||||
(\const _ trees -> do
|
||||
const <- runTcM abs fid $
|
||||
case mb_tty of
|
||||
Just tty -> tcExpr scope const tty
|
||||
Nothing -> fmap fst $ infExpr scope const
|
||||
return (mkAbs const)
|
||||
`mplus`
|
||||
trees)
|
||||
[] fcat forest
|
||||
mzero fid forest
|
||||
where
|
||||
(scope,mkAbs,mb_tty) = updateScope hypos scope_ id mb_tty_
|
||||
|
||||
check_ho_fun fun args
|
||||
| fun == _V = return (head args)
|
||||
| fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args))
|
||||
| otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args)
|
||||
|
||||
mkVar (EFun v) = v
|
||||
mkVar (EMeta _) = wildCId
|
||||
|
||||
freeVar (EFun v) = Set.singleton v
|
||||
freeVar _ = Set.empty
|
||||
goArg rec_ scope fid e1 arg (TTyp delta (DTyp ((bt,x,ty):hs) c es)) = do
|
||||
e2' <- go rec_ scope arg (Just (TTyp delta ty))
|
||||
let e2 = case bt of
|
||||
Explicit -> e2'
|
||||
Implicit -> EImplArg e2'
|
||||
if x == wildCId
|
||||
then return (EApp e1 e2,TTyp delta (DTyp hs c es))
|
||||
else do v2 <- runTcM abs fid (eval (scopeEnv scope) e2')
|
||||
return (EApp e1 e2,TTyp (v2:delta) (DTyp hs c es))
|
||||
|
||||
updateScope [] scope mkAbs mb_tty = (scope,mkAbs,mb_tty)
|
||||
updateScope ((fid,_):hypos) scope mkAbs mb_tty =
|
||||
case mb_tty of
|
||||
Just (TTyp delta (DTyp ((bt,y,ty):hs) c es)) ->
|
||||
if y == wildCId
|
||||
then updateScope hypos (addScopedVar x (TTyp delta ty) scope)
|
||||
(mkAbs . EAbs bt x)
|
||||
(Just (TTyp delta (DTyp hs c es)))
|
||||
else updateScope hypos (addScopedVar x (TTyp delta ty) scope)
|
||||
(mkAbs . EAbs bt x)
|
||||
(Just (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es)))
|
||||
Nothing -> (scope,mkAbs,Nothing)
|
||||
where
|
||||
(x:_) | fid == fidVar = [wildCId]
|
||||
| otherwise = [x | PConst _ (EFun x) _ <- maybe [] Set.toList (IntMap.lookup fid forest)]
|
||||
|
||||
|
||||
foldForest :: (FunId -> [FId] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b
|
||||
newtype TcFM a = TcFM {unTcFM :: MetaStore -> ([(MetaStore,a)],[(FId,TcError)])}
|
||||
|
||||
instance Functor TcFM where
|
||||
fmap f g = TcFM (\ms -> let (res_g,err_g) = unTcFM g ms
|
||||
in ([(ms,f x) | (ms,x) <- res_g],err_g))
|
||||
|
||||
instance Monad TcFM where
|
||||
return x = TcFM (\ms -> ([(ms,x)],[]))
|
||||
f >>= g = TcFM (\ms -> case unTcFM f ms of
|
||||
(res,err) -> let (res',err') = unzip [unTcFM (g x) ms | (ms,x) <- res]
|
||||
in (concat res',concat (err:err')))
|
||||
|
||||
instance MonadPlus TcFM where
|
||||
mzero = TcFM (\ms -> ([],[]))
|
||||
mplus f g = TcFM (\ms -> let (res_f,err_f) = unTcFM f ms
|
||||
(res_g,err_g) = unTcFM g ms
|
||||
in (res_f++res_g,err_f++err_g))
|
||||
|
||||
runTcM :: Abstr -> FId -> TcM a -> TcFM a
|
||||
runTcM abstr fid f = TcFM (\ms -> case unTcM f abstr ms of
|
||||
Ok ms x -> ([(ms,x)],[] )
|
||||
Fail err -> ([], [(fid,err)]))
|
||||
|
||||
foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b
|
||||
foldForest f g b fcat forest =
|
||||
case IntMap.lookup fcat forest of
|
||||
Nothing -> b
|
||||
|
||||
@@ -23,7 +23,7 @@ import qualified Data.Set as Set
|
||||
|
||||
-- | Linearizes given expression as string in the language
|
||||
linearize :: PGF -> Language -> Tree -> String
|
||||
linearize pgf lang = concat . take 1 . map (unwords . concatMap flattenBracketedString . snd . untokn "" . (!0)) . linTree pgf lang
|
||||
linearize pgf lang = concat . take 1 . map (unwords . concatMap flattenBracketedString . snd . untokn "" . firstLin) . linTree pgf lang
|
||||
|
||||
-- | The same as 'linearizeAllLang' but does not return
|
||||
-- the language.
|
||||
@@ -37,101 +37,86 @@ linearizeAllLang pgf t = [(lang,linearize pgf lang t) | lang <- Map.keys (concre
|
||||
|
||||
-- | Linearizes given expression as a bracketed string in the language
|
||||
bracketedLinearize :: PGF -> Language -> Tree -> BracketedString
|
||||
bracketedLinearize pgf lang = head . concat . map (snd . untokn "" . (!0)) . linTree pgf lang
|
||||
bracketedLinearize pgf lang = head . concat . map (snd . untokn "" . firstLin) . linTree pgf lang
|
||||
where
|
||||
head [] = error "cannot linearize"
|
||||
head (bs:bss) = bs
|
||||
|
||||
firstLin (_,arr)
|
||||
| inRange (bounds arr) 0 = arr ! 0
|
||||
| otherwise = LeafKS []
|
||||
|
||||
-- | Creates a table from feature name to linearization.
|
||||
-- The outher list encodes the variations
|
||||
tabularLinearizes :: PGF -> CId -> Expr -> [[(String,String)]]
|
||||
tabularLinearizes pgf lang e = map (zip lbls . map (unwords . concatMap flattenBracketedString . snd . untokn "") . elems)
|
||||
(linTree pgf lang e)
|
||||
tabularLinearizes pgf lang e = map cnv (linTree pgf lang e)
|
||||
where
|
||||
lbls = case unApp e of
|
||||
Just (f,_) -> let cat = valCat (lookType pgf f)
|
||||
in case Map.lookup cat (cnccats (lookConcr pgf lang)) of
|
||||
Just (CncCat _ _ lbls) -> elems lbls
|
||||
Nothing -> error "No labels"
|
||||
Nothing -> error "Not function application"
|
||||
cnv ((cat,_),lin) = zip (lbls cat) $ map (unwords . concatMap flattenBracketedString . snd . untokn "") (elems lin)
|
||||
|
||||
lbls cat = case Map.lookup cat (cnccats (lookConcr pgf lang)) of
|
||||
Just (CncCat _ _ lbls) -> elems lbls
|
||||
Nothing -> error "No labels"
|
||||
|
||||
--------------------------------------------------------------------
|
||||
-- Implementation
|
||||
--------------------------------------------------------------------
|
||||
|
||||
type CncType = (CId, FId) -- concrete type is the abstract type (the category) + the forest id
|
||||
|
||||
linTree :: PGF -> Language -> Expr -> [Array LIndex BracketedTokn]
|
||||
linTree :: PGF -> Language -> Expr -> [(CncType, Array LIndex BracketedTokn)]
|
||||
linTree pgf lang e =
|
||||
nub [amapWithIndex (\label -> Bracket_ cat fid label [e]) lin | (_,((cat,fid),e,lin)) <- lin0 [] [] Nothing 0 e e]
|
||||
nub [(ct,amapWithIndex (\label -> Bracket_ cat fid label es) lin) | (_,(ct@(cat,fid),es,(xs,lin))) <- lin Nothing 0 e [] [] e []]
|
||||
where
|
||||
cnc = lookMap (error "no lang") lang (concretes pgf)
|
||||
lp = lproductions cnc
|
||||
|
||||
lin0 xs ys mb_cty n_fid e0 (EAbs _ x e) = lin0 (showCId x:xs) ys mb_cty n_fid e0 e
|
||||
lin0 xs ys mb_cty n_fid e0 (ETyped e _) = lin0 xs ys mb_cty n_fid e0 e
|
||||
lin0 xs ys mb_cty n_fid e0 e | null xs = lin ys mb_cty n_fid e0 e []
|
||||
| otherwise = apply (xs ++ ys) mb_cty n_fid e0 _B (e:[ELit (LStr x) | x <- xs])
|
||||
|
||||
lin xs mb_cty n_fid e0 (EApp e1 e2) es = lin xs mb_cty n_fid e0 e1 (e2:es)
|
||||
lin xs mb_cty n_fid e0 (ELit l) [] = case l of
|
||||
LStr s -> return (n_fid+1,((cidString,n_fid),e0,ss s))
|
||||
LInt n -> return (n_fid+1,((cidInt, n_fid),e0,ss (show n)))
|
||||
LFlt f -> return (n_fid+1,((cidFloat, n_fid),e0,ss (show f)))
|
||||
lin xs mb_cty n_fid e0 (EMeta i) es = apply xs mb_cty n_fid e0 _V (ELit (LStr ('?':show i)):es)
|
||||
lin xs mb_cty n_fid e0 (EFun f) es = apply xs mb_cty n_fid e0 f es
|
||||
lin xs mb_cty n_fid e0 (EVar i) es = apply xs mb_cty n_fid e0 _V (ELit (LStr (xs !! i)) :es)
|
||||
lin xs mb_cty n_fid e0 (ETyped e _) es = lin xs mb_cty n_fid e0 e es
|
||||
lin xs mb_cty n_fid e0 (EImplArg e) es = lin xs mb_cty n_fid e0 e es
|
||||
lin mb_cty n_fid e0 ys xs (EAbs _ x e) es = lin mb_cty n_fid e0 ys (x:xs) e es
|
||||
lin mb_cty n_fid e0 ys xs (EApp e1 e2) es = lin mb_cty n_fid e0 ys xs e1 (e2:es)
|
||||
lin mb_cty n_fid e0 ys xs (EImplArg e) es = lin mb_cty n_fid e0 ys xs e es
|
||||
lin mb_cty n_fid e0 ys xs (ETyped e _) es = lin mb_cty n_fid e0 ys xs e es
|
||||
lin mb_cty n_fid e0 ys xs (EFun f) es = apply mb_cty n_fid e0 ys xs f es
|
||||
lin mb_cty n_fid e0 ys xs (EMeta i) es = def mb_cty n_fid e0 ys xs ('?':show i)
|
||||
lin mb_cty n_fid e0 ys xs (EVar i) [] = def mb_cty n_fid e0 ys xs (showCId ((xs++ys) !! i))
|
||||
lin mb_cty n_fid e0 ys xs (ELit l) [] = case l of
|
||||
LStr s -> return (n_fid+1,((cidString,n_fid),[e0],([],ss s)))
|
||||
LInt n -> return (n_fid+1,((cidInt, n_fid),[e0],([],ss (show n))))
|
||||
LFlt f -> return (n_fid+1,((cidFloat, n_fid),[e0],([],ss (show f))))
|
||||
|
||||
ss s = listArray (0,0) [[LeafKS [s]]]
|
||||
|
||||
apply :: [String] -> Maybe CncType -> FId -> Expr -> CId -> [Expr] -> [(FId,(CncType, Expr, LinTable))]
|
||||
apply xs mb_cty n_fid e0 f es =
|
||||
apply :: Maybe CncType -> FId -> Expr -> [CId] -> [CId] -> CId -> [Expr] -> [(FId,(CncType, [Expr], LinTable))]
|
||||
apply mb_cty n_fid e0 ys xs f es =
|
||||
case Map.lookup f lp of
|
||||
Just prods -> do (funid,(cat,fid),ctys) <- getApps prods
|
||||
guard (length ctys == length es)
|
||||
(n_fid,args) <- descend n_fid (zip ctys es)
|
||||
let (CncFun _ lins) = cncfuns cnc ! funid
|
||||
return (n_fid+1,((cat,n_fid),e0,listArray (bounds lins) [computeSeq seqid args | seqid <- elems lins]))
|
||||
Nothing -> apply xs mb_cty n_fid e0 _V [ELit (LStr ("[" ++ showCId f ++ "]"))] -- fun without lin
|
||||
return (n_fid+1,((cat,n_fid),[e0],mkLinTable cnc (const True) xs funid args))
|
||||
Nothing -> def mb_cty n_fid e0 ys xs ("[" ++ showCId f ++ "]") -- fun without lin
|
||||
where
|
||||
getApps prods =
|
||||
case mb_cty of
|
||||
Just cty@(cat,fid) -> maybe [] (concatMap (toApp cty) . Set.toList) (IntMap.lookup fid prods)
|
||||
Nothing | f == _B
|
||||
|| f == _V -> []
|
||||
| otherwise -> concat [toApp (wildCId,fid) prod | (fid,set) <- IntMap.toList prods, prod <- Set.toList set]
|
||||
Just (cat,fid) -> maybe [] (concatMap (toApp fid) . Set.toList) (IntMap.lookup fid prods)
|
||||
Nothing -> concat [toApp fid prod | (fid,set) <- IntMap.toList prods, prod <- Set.toList set]
|
||||
where
|
||||
toApp cty (PApply funid fids)
|
||||
| f == _V = [(funid,cty,zip ( repeat cidVar) fids)]
|
||||
| f == _B = [(funid,cty,zip (fst cty : repeat cidVar) fids)]
|
||||
| otherwise = let Just (ty,_,_) = Map.lookup f (funs (abstract pgf))
|
||||
(args,res) = catSkeleton ty
|
||||
in [(funid,(res,snd cty),zip args fids)]
|
||||
toApp cty (PCoerce fid) = concatMap (toApp cty) (maybe [] Set.toList (IntMap.lookup fid prods))
|
||||
toApp fid (PApply funid pargs) =
|
||||
let Just (ty,_,_) = Map.lookup f (funs (abstract pgf))
|
||||
(args,res) = catSkeleton ty
|
||||
in [(funid,(res,fid),zip args [fid | PArg _ fid <- pargs])]
|
||||
toApp _ (PCoerce fid) =
|
||||
maybe [] (concatMap (toApp fid) . Set.toList) (IntMap.lookup fid prods)
|
||||
|
||||
descend n_fid [] = return (n_fid,[])
|
||||
descend n_fid (((cat,fid),e):fes) = do (n_fid,arg) <- lin0 [] xs (Just (cat,fid)) n_fid e e
|
||||
(n_fid,args) <- descend n_fid fes
|
||||
return (n_fid,arg:args)
|
||||
descend n_fid [] = return (n_fid,[])
|
||||
descend n_fid ((cty,e):fes) = do (n_fid,arg) <- lin (Just cty) n_fid e (xs++ys) [] e []
|
||||
(n_fid,args) <- descend n_fid fes
|
||||
return (n_fid,arg:args)
|
||||
|
||||
computeSeq :: SeqId -> [(CncType,Expr,LinTable)] -> [BracketedTokn]
|
||||
computeSeq seqid args = concatMap compute (elems seq)
|
||||
where
|
||||
seq = sequences cnc ! seqid
|
||||
|
||||
compute (SymCat d r) = getArg d r
|
||||
compute (SymLit d r) = getArg d r
|
||||
compute (SymKS ts) = [LeafKS ts]
|
||||
compute (SymKP ts alts) = [LeafKP ts alts]
|
||||
|
||||
getArg d r
|
||||
| not (null arg_lin) = [Bracket_ cat fid r [e] arg_lin]
|
||||
| otherwise = arg_lin
|
||||
where
|
||||
arg_lin = lin ! r
|
||||
((cat,fid),e,lin) = args !! d
|
||||
def (Just (cat,fid)) n_fid e0 ys xs s =
|
||||
case IntMap.lookup fid (lindefs cnc) of
|
||||
Just funs -> do funid <- funs
|
||||
let args = [((wildCId, n_fid),[e0],([],ss s))]
|
||||
return (n_fid+2,((cat,n_fid+1),[e0],mkLinTable cnc (const True) xs funid args))
|
||||
Nothing
|
||||
| isPredefFId fid -> return (n_fid+2,((cat,n_fid+1),[e0],(xs,listArray (0,0) [[LeafKS [s]]])))
|
||||
| otherwise -> do PCoerce fid <- maybe [] Set.toList (IntMap.lookup fid (pproductions cnc))
|
||||
def (Just (cat,fid)) n_fid e0 ys xs s
|
||||
def Nothing n_fid e0 ys xs s = []
|
||||
|
||||
amapWithIndex :: (IArray a e1, IArray a e2, Ix i) => (i -> e1 -> e2) -> a i e1 -> a i e2
|
||||
amapWithIndex f arr = listArray (bounds arr) (map (uncurry f) (assocs arr))
|
||||
|
||||
@@ -10,6 +10,7 @@ import qualified Data.IntSet as IntSet
|
||||
import qualified Data.Array as Array
|
||||
import Data.Maybe
|
||||
import Data.List
|
||||
import Data.Array.IArray
|
||||
import Text.PrettyPrint
|
||||
|
||||
-- operations for manipulating PGF grammars and objects
|
||||
@@ -132,9 +133,6 @@ cidInt = mkCId "Int"
|
||||
cidFloat = mkCId "Float"
|
||||
cidVar = mkCId "__gfVar"
|
||||
|
||||
_B = mkCId "__gfB"
|
||||
_V = mkCId "__gfV"
|
||||
|
||||
|
||||
-- Utilities for doing linearization
|
||||
|
||||
@@ -162,7 +160,7 @@ data BracketedTokn
|
||||
| Bracket_ CId {-# UNPACK #-} !FId {-# UNPACK #-} !LIndex [Expr] [BracketedTokn] -- Invariant: the list is not empty
|
||||
deriving Eq
|
||||
|
||||
type LinTable = Array.Array LIndex [BracketedTokn]
|
||||
type LinTable = ([CId],Array.Array LIndex [BracketedTokn])
|
||||
|
||||
-- | Renders the bracketed string as string where
|
||||
-- the brackets are shown as @(S ...)@ where
|
||||
@@ -191,6 +189,34 @@ untokn nw (Bracket_ cat fid index es bss) =
|
||||
let (nw',bss') = mapAccumR untokn nw bss
|
||||
in (nw',[Bracket cat fid index es (concat bss')])
|
||||
|
||||
type CncType = (CId, FId) -- concrete type is the abstract type (the category) + the forest id
|
||||
|
||||
mkLinTable :: Concr -> (CncType -> Bool) -> [CId] -> FunId -> [(CncType,[Expr],LinTable)] -> LinTable
|
||||
mkLinTable cnc filter xs funid args = (xs,listArray (bounds lins) [computeSeq filter (elems (sequences cnc ! seqid)) args | seqid <- elems lins])
|
||||
where
|
||||
(CncFun _ lins) = cncfuns cnc ! funid
|
||||
|
||||
computeSeq :: (CncType -> Bool) -> [Symbol] -> [(CncType,[Expr],LinTable)] -> [BracketedTokn]
|
||||
computeSeq filter seq args = concatMap compute seq
|
||||
where
|
||||
compute (SymCat d r) = getArg d r
|
||||
compute (SymLit d r) = getArg d r
|
||||
compute (SymVar d r) = getVar d r
|
||||
compute (SymKS ts) = [LeafKS ts]
|
||||
compute (SymKP ts alts) = [LeafKP ts alts]
|
||||
|
||||
getArg d r
|
||||
| not (null arg_lin) &&
|
||||
filter ct = [Bracket_ cat fid r es arg_lin]
|
||||
| otherwise = arg_lin
|
||||
where
|
||||
arg_lin = lin ! r
|
||||
(ct@(cat,fid),es,(xs,lin)) = args !! d
|
||||
|
||||
getVar d r = [LeafKS [showCId (xs !! r)]]
|
||||
where
|
||||
(ct,es,(xs,lin)) = args !! d
|
||||
|
||||
flattenBracketedString :: BracketedString -> [String]
|
||||
flattenBracketedString (Leaf w) = [w]
|
||||
flattenBracketedString (Bracket _ _ _ _ bss) = concatMap flattenBracketedString bss
|
||||
|
||||
@@ -1,3 +1,4 @@
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
module PGF.Optimize
|
||||
( optimizePGF
|
||||
, updateProductionIndices
|
||||
@@ -16,6 +17,7 @@ import qualified Data.Map as Map
|
||||
import qualified Data.Set as Set
|
||||
import qualified Data.IntSet as IntSet
|
||||
import qualified Data.IntMap as IntMap
|
||||
import qualified Data.List as List
|
||||
import Control.Monad.ST
|
||||
import GF.Data.Utilities(sortNub)
|
||||
|
||||
@@ -29,14 +31,20 @@ updateProductionIndices pgf = pgf{concretes = fmap (updateConcrete (abstract pgf
|
||||
|
||||
topDownFilter :: CId -> Concr -> Concr
|
||||
topDownFilter startCat cnc =
|
||||
let ((seqs,funs),prods) = IntMap.mapAccumWithKey (\env res set -> mapAccumLSet (optimize res) env set)
|
||||
(Map.empty,Map.empty)
|
||||
(productions cnc)
|
||||
let env0 = (Map.empty,Map.empty)
|
||||
(env1,defs) = IntMap.mapAccumWithKey (\env fid funids -> mapAccumL (optimizeFun fid [PArg [] fidVar]) env funids)
|
||||
env0
|
||||
(lindefs cnc)
|
||||
(env2,prods) = IntMap.mapAccumWithKey (\env fid set -> mapAccumLSet (optimizeProd fid) env set)
|
||||
env1
|
||||
(productions cnc)
|
||||
cats = Map.mapWithKey filterCatLabels (cnccats cnc)
|
||||
(seqs,funs) = env2
|
||||
in cnc{ sequences = mkSetArray seqs
|
||||
, cncfuns = mkSetArray funs
|
||||
, productions = prods
|
||||
, cnccats = cats
|
||||
, lindefs = defs
|
||||
}
|
||||
where
|
||||
fid2cat fid =
|
||||
@@ -46,8 +54,8 @@ topDownFilter startCat cnc =
|
||||
(fid:_) -> fid2cat fid
|
||||
_ -> error "unknown forest id"
|
||||
where
|
||||
fid2catMap = IntMap.fromList [(fid,cat) | (cat,CncCat start end lbls) <- Map.toList (cnccats cnc),
|
||||
fid <- [start..end]]
|
||||
fid2catMap = IntMap.fromList ((fidVar,cidVar) : [(fid,cat) | (cat,CncCat start end lbls) <- Map.toList (cnccats cnc),
|
||||
fid <- [start..end]])
|
||||
|
||||
starts =
|
||||
case Map.lookup startCat (cnccats cnc) of
|
||||
@@ -64,11 +72,11 @@ topDownFilter startCat cnc =
|
||||
CncFun _ lin = cncfuns cnc ! funid
|
||||
rel fid _ = Map.empty
|
||||
|
||||
deps args seqid = Set.fromList [(fid2cat (args !! r),d) | SymCat r d <- elems seq]
|
||||
deps args seqid = Set.fromList [let PArg _ fid = args !! r in (fid2cat fid,d) | SymCat r d <- elems seq]
|
||||
where
|
||||
seq = sequences cnc ! seqid
|
||||
|
||||
-- here we create a mapping from category to an array of indices.
|
||||
-- here we create a mapping from a category to an array of indices.
|
||||
-- An element of the array is equal to -1 if the corresponding index
|
||||
-- is not going to be used in the optimized grammar, or the new index
|
||||
-- if it will be used
|
||||
@@ -122,11 +130,16 @@ topDownFilter startCat cnc =
|
||||
reindex indices (i+1) j (k+1)
|
||||
| otherwise = return ()
|
||||
|
||||
optimize res (seqs,funs) (PApply funid args) =
|
||||
optimizeProd res env (PApply funid args) =
|
||||
let (env',funid') = optimizeFun res args env funid
|
||||
in (env', PApply funid' args)
|
||||
optimizeProd res env prod = (env,prod)
|
||||
|
||||
optimizeFun res args (seqs,funs) funid =
|
||||
let (seqs',lin') = mapAccumL addUnique seqs [amap updateSymbol (sequences cnc ! seqid) |
|
||||
(lbl,seqid) <- assocs lin, indicesOf res ! lbl >= 0]
|
||||
(funs',funid') = addUnique funs (CncFun fun (mkArray lin'))
|
||||
in ((seqs',funs'), PApply funid' args)
|
||||
in ((seqs',funs'), funid')
|
||||
where
|
||||
CncFun fun lin = cncfuns cnc ! funid
|
||||
|
||||
@@ -140,11 +153,10 @@ topDownFilter startCat cnc =
|
||||
Just seqid -> (seqs,seqid)
|
||||
Nothing -> let seqid = Map.size seqs
|
||||
in (Map.insert seq seqid seqs, seqid)
|
||||
|
||||
updateSymbol (SymCat r d) = SymCat r (indicesOf (args !! r) ! d)
|
||||
|
||||
updateSymbol (SymCat r d) = let PArg _ fid = args !! r in SymCat r (indicesOf fid ! d)
|
||||
updateSymbol s = s
|
||||
optimize res env prod = (env,prod)
|
||||
|
||||
|
||||
filterCatLabels cat (CncCat start end lbls) =
|
||||
case Map.lookup cat closure of
|
||||
Just indices -> let lbls' = mkArray [lbl | (i,lbl) <- assocs lbls, indices ! i >= 0]
|
||||
@@ -159,50 +171,35 @@ topDownFilter startCat cnc =
|
||||
|
||||
|
||||
bottomUpFilter :: Concr -> Concr
|
||||
bottomUpFilter cnc = cnc{productions=filterProductions IntMap.empty (productions cnc)}
|
||||
bottomUpFilter cnc = cnc{productions=filterProductions IntMap.empty IntSet.empty (productions cnc)}
|
||||
|
||||
filterProductions prods0 prods
|
||||
filterProductions prods0 hoc0 prods
|
||||
| prods0 == prods1 = prods0
|
||||
| otherwise = filterProductions prods1 prods
|
||||
| otherwise = filterProductions prods1 hoc1 prods
|
||||
where
|
||||
prods1 = IntMap.unionWith Set.union prods0 (IntMap.mapMaybe (filterProdSet prods0) prods)
|
||||
(prods1,hoc1) = IntMap.foldWithKey foldProdSet (IntMap.empty,IntSet.empty) prods
|
||||
|
||||
filterProdSet prods0 set
|
||||
| Set.null set1 = Nothing
|
||||
| otherwise = Just set1
|
||||
foldProdSet fid set (!prods,!hoc)
|
||||
| Set.null set1 = (prods,hoc)
|
||||
| otherwise = (IntMap.insert fid set1 prods,hoc1)
|
||||
where
|
||||
set1 = Set.filter (filterRule prods0) set
|
||||
set1 = Set.filter filterRule set
|
||||
hoc1 = Set.fold accumHOC hoc set1
|
||||
|
||||
filterRule prods0 (PApply funid args) = all (\fid -> isPredefFId fid || IntMap.member fid prods0) args
|
||||
filterRule prods0 (PCoerce fid) = isPredefFId fid || IntMap.member fid prods0
|
||||
filterRule prods0 _ = True
|
||||
filterRule (PApply funid args) = all (\(PArg _ fid) -> isLive fid) args
|
||||
filterRule (PCoerce fid) = isLive fid
|
||||
filterRule _ = True
|
||||
|
||||
isLive fid = isPredefFId fid || IntMap.member fid prods0 || IntSet.member fid hoc0
|
||||
|
||||
accumHOC (PApply funid args) hoc = List.foldl' (\hoc (PArg hypos _) -> List.foldl' (\hoc (_,fid) -> IntSet.insert fid hoc) hoc hypos) hoc args
|
||||
accumHOC _ hoc = hoc
|
||||
|
||||
updateConcrete abs cnc =
|
||||
let p_prods = (filterProductions IntMap.empty . parseIndex cnc) (productions cnc)
|
||||
l_prods = (linIndex cnc . filterProductions IntMap.empty) (productions cnc)
|
||||
let p_prods = filterProductions IntMap.empty IntSet.empty (productions cnc)
|
||||
l_prods = linIndex cnc p_prods
|
||||
in cnc{pproductions = p_prods, lproductions = l_prods}
|
||||
where
|
||||
parseIndex cnc = IntMap.mapMaybeWithKey filterProdSet
|
||||
where
|
||||
filterProdSet fid prods
|
||||
| fid `IntSet.member` ho_fids = Just prods
|
||||
| otherwise = let prods' = Set.filter (not . is_ho_prod) prods
|
||||
in if Set.null prods'
|
||||
then Nothing
|
||||
else Just prods'
|
||||
|
||||
is_ho_prod (PApply _ [fid]) | fid == fidVar = True
|
||||
is_ho_prod _ = False
|
||||
|
||||
ho_fids :: IntSet.IntSet
|
||||
ho_fids = IntSet.fromList [fid | cat <- ho_cats
|
||||
, fid <- maybe [] (\(CncCat s e _) -> [s..e]) (Map.lookup cat (cnccats cnc))]
|
||||
|
||||
ho_cats :: [CId]
|
||||
ho_cats = sortNub [c | (ty,_,_) <- Map.elems (funs abs)
|
||||
, h <- case ty of {DTyp hyps val _ -> hyps}
|
||||
, c <- fst (catSkeleton (typeOfHypo h))]
|
||||
|
||||
linIndex cnc productions =
|
||||
Map.fromListWith (IntMap.unionWith Set.union)
|
||||
[(fun,IntMap.singleton res (Set.singleton prod)) | (res,prods) <- IntMap.toList productions
|
||||
|
||||
@@ -28,7 +28,7 @@ import PGF.Data
|
||||
import PGF.Expr(Tree)
|
||||
import PGF.Macros
|
||||
import PGF.TypeCheck
|
||||
import PGF.Forest(Forest(Forest), linearizeWithBrackets, foldForest)
|
||||
import PGF.Forest(Forest(Forest), linearizeWithBrackets, getAbsTrees, foldForest)
|
||||
|
||||
-- | The input to the parser is a pair of predicates. The first one
|
||||
-- 'piToken' checks that a given token, suggested by the grammar,
|
||||
@@ -50,6 +50,7 @@ data ParseOutput
|
||||
-- if there are many analizes for some phrase but they all are not type correct.
|
||||
| ParseOk [Tree] -- ^ If the parsing and the type checkeing are successful we get a list of abstract syntax trees.
|
||||
-- The list should be non-empty.
|
||||
| ParseIncomplete -- ^ The sentence is not complete. Only partial output is produced
|
||||
|
||||
parse :: PGF -> Language -> Type -> [Token] -> (ParseOutput,BracketedString)
|
||||
parse pgf lang typ toks = loop (initState pgf lang typ) toks
|
||||
@@ -108,7 +109,7 @@ simpleParseInput t = ParseInput (==t) (matchLit t)
|
||||
_ -> Nothing }
|
||||
| fid == fidFloat = case reads t of {[(d,"")] -> Just (cidFloat,ELit (LFlt d),[t]);
|
||||
_ -> Nothing }
|
||||
| fid == fidVar = Just (cidVar,EFun (mkCId t),[t])
|
||||
| fid == fidVar = Just (wildCId,EFun (mkCId t),[t])
|
||||
| otherwise = Nothing
|
||||
|
||||
mkParseInput :: PGF -> Language -> (a -> Token -> Bool) -> [(CId,a -> Maybe (Tree,[Token]))] -> a -> ParseInput
|
||||
@@ -140,7 +141,7 @@ nextState (PState pgf cnc chart items) input =
|
||||
let (mb_agenda,map_items) = TMap.decompose items
|
||||
agenda = maybe [] Set.toList mb_agenda
|
||||
acc = TMap.unions [tmap | (t,tmap) <- Map.toList map_items, piToken input t]
|
||||
(acc1,chart1) = process flit ftok (sequences cnc) (cncfuns cnc) agenda acc chart
|
||||
(acc1,chart1) = process flit ftok (sequences cnc) (cncfuns cnc) (lindefs cnc) agenda acc chart
|
||||
chart2 = chart1{ active =emptyAC
|
||||
, actives=active chart1 : actives chart1
|
||||
, passive=emptyPC
|
||||
@@ -166,7 +167,7 @@ getCompletions (PState pgf cnc chart items) w =
|
||||
let (mb_agenda,map_items) = TMap.decompose items
|
||||
agenda = maybe [] Set.toList mb_agenda
|
||||
acc = Map.filterWithKey (\tok _ -> isPrefixOf w tok) map_items
|
||||
(acc',chart1) = process flit ftok (sequences cnc) (cncfuns cnc) agenda acc chart
|
||||
(acc',chart1) = process flit ftok (sequences cnc) (cncfuns cnc) (lindefs cnc) agenda acc chart
|
||||
chart2 = chart1{ active =emptyAC
|
||||
, actives=active chart1 : actives chart1
|
||||
, passive=emptyPC
|
||||
@@ -184,7 +185,7 @@ recoveryStates :: [Type] -> ErrorState -> (ParseState, Map.Map Token ParseState)
|
||||
recoveryStates open_types (EState pgf cnc chart) =
|
||||
let open_fcats = concatMap type2fcats open_types
|
||||
agenda = foldl (complete open_fcats) [] (actives chart)
|
||||
(acc,chart1) = process flit ftok (sequences cnc) (cncfuns cnc) agenda Map.empty chart
|
||||
(acc,chart1) = process flit ftok (sequences cnc) (cncfuns cnc) (lindefs cnc) agenda Map.empty chart
|
||||
chart2 = chart1{ active =emptyAC
|
||||
, actives=active chart1 : actives chart1
|
||||
, passive=emptyPC
|
||||
@@ -200,7 +201,7 @@ recoveryStates open_types (EState pgf cnc chart) =
|
||||
foldl (Set.fold (\(Active j' ppos funid seqid args keyc) ->
|
||||
(:) (Active j' (ppos+1) funid seqid args keyc)))
|
||||
items
|
||||
[set | fcat <- open_fcats, set <- lookupACByFCat fcat ac]
|
||||
[set | fcat <- open_fcats, (set,_) <- lookupACByFCat fcat ac]
|
||||
|
||||
flit _ = Nothing
|
||||
ftok (tok:toks) item acc = Map.insertWith (TMap.unionWith Set.union) tok (TMap.singleton toks (Set.singleton item)) acc
|
||||
@@ -212,26 +213,24 @@ recoveryStates open_types (EState pgf cnc chart) =
|
||||
getParseOutput :: ParseState -> Type -> (ParseOutput,BracketedString)
|
||||
getParseOutput (PState pgf cnc chart items) ty@(DTyp _ start _) =
|
||||
let froots | null roots = getPartialSeq (sequences cnc) (reverse (active chart1 : actives chart1)) seq
|
||||
| otherwise = [([SymCat 0 lbl],[fid]) | AK fid lbl <- roots]
|
||||
| otherwise = [([SymCat 0 lbl],[PArg [] fid]) | AK fid lbl <- roots]
|
||||
|
||||
bs = linearizeWithBrackets (Forest (abstract pgf) cnc (forest chart1) froots)
|
||||
|
||||
exps = nubsort $ do
|
||||
(AK fid lbl) <- roots
|
||||
(fvs,e) <- go Set.empty 0 (0,fid)
|
||||
guard (Set.null fvs)
|
||||
Right e1 <- [checkExpr pgf e ty]
|
||||
return e1
|
||||
|
||||
res = if null exps
|
||||
then ParseFailed (offset chart)
|
||||
else ParseOk exps
|
||||
f = Forest (abstract pgf) cnc (forest chart1) froots
|
||||
|
||||
bs = linearizeWithBrackets f
|
||||
|
||||
res | not (null es) = ParseOk es
|
||||
| not (null errs) = TypeError errs
|
||||
| otherwise = ParseIncomplete
|
||||
where xs = [getAbsTrees f (PArg [] fid) (Just ty) | (AK fid lbl) <- roots]
|
||||
es = concat [es | Right es <- xs]
|
||||
errs = concat [errs | Left errs <- xs]
|
||||
|
||||
in (res,bs)
|
||||
where
|
||||
(mb_agenda,acc) = TMap.decompose items
|
||||
agenda = maybe [] Set.toList mb_agenda
|
||||
(acc',chart1) = process flit ftok (sequences cnc) (cncfuns cnc) agenda (TMap.compose Nothing acc) chart
|
||||
(acc',chart1) = process flit ftok (sequences cnc) (cncfuns cnc) (lindefs cnc) agenda (TMap.compose Nothing acc) chart
|
||||
seq = [(j,cutAt ppos toks seqid,args,key) | (toks,set) <- TMap.toList acc', Active j ppos funid seqid args key <- Set.toList set]
|
||||
|
||||
flit _ = Nothing
|
||||
@@ -255,32 +254,6 @@ getParseOutput (PState pgf cnc chart items) ty@(DTyp _ start _) =
|
||||
return (AK fid lbl)
|
||||
Nothing -> mzero
|
||||
|
||||
go rec_ fcat' (d,fcat)
|
||||
| fcat < totalCats cnc = return (Set.empty,EMeta (fcat'*10+d)) -- FIXME: here we assume that every rule has at most 10 arguments
|
||||
| Set.member fcat rec_ = mzero
|
||||
| otherwise = foldForest (\funid args trees ->
|
||||
do let CncFun fn lins = cncfuns cnc ! funid
|
||||
args <- mapM (go (Set.insert fcat rec_) fcat) (zip [0..] args)
|
||||
check_ho_fun fn args
|
||||
`mplus`
|
||||
trees)
|
||||
(\const _ trees ->
|
||||
return (freeVar const,const)
|
||||
`mplus`
|
||||
trees)
|
||||
[] fcat (forest chart1)
|
||||
|
||||
check_ho_fun fun args
|
||||
| fun == _V = return (head args)
|
||||
| fun == _B = return (foldl1 Set.difference (map fst args), foldr (\x e -> EAbs Explicit (mkVar (snd x)) e) (snd (head args)) (tail args))
|
||||
| otherwise = return (Set.unions (map fst args),foldl (\e x -> EApp e (snd x)) (EFun fun) args)
|
||||
|
||||
mkVar (EFun v) = v
|
||||
mkVar (EMeta _) = wildCId
|
||||
|
||||
freeVar (EFun v) = Set.singleton v
|
||||
freeVar _ = Set.empty
|
||||
|
||||
getPartialSeq seqs actives = expand Set.empty
|
||||
where
|
||||
expand acc [] =
|
||||
@@ -291,72 +264,99 @@ getPartialSeq seqs actives = expand Set.empty
|
||||
where
|
||||
acc' = Set.insert item acc
|
||||
items' = case lookupAC key (actives !! j) of
|
||||
Nothing -> items
|
||||
Just set -> [if j' < j
|
||||
then let lin' = take ppos (elems (unsafeAt seqs seqid))
|
||||
in (j',lin'++map (inc (length args')) lin,args'++args,key')
|
||||
else (j',lin,args,key') | Active j' ppos funid seqid args' key' <- Set.toList set] ++ items
|
||||
Nothing -> items
|
||||
Just (set,_) -> [if j' < j
|
||||
then let lin' = take ppos (elems (unsafeAt seqs seqid))
|
||||
in (j',lin'++map (inc (length args')) lin,args'++args,key')
|
||||
else (j',lin,args,key') | Active j' ppos funid seqid args' key' <- Set.toList set] ++ items
|
||||
|
||||
inc n (SymCat d r) = SymCat (n+d) r
|
||||
inc n (SymVar d r) = SymVar (n+d) r
|
||||
inc n (SymLit d r) = SymLit (n+d) r
|
||||
inc n s = s
|
||||
|
||||
process flit ftok !seqs !funs [] acc chart = (acc,chart)
|
||||
process flit ftok !seqs !funs (item@(Active j ppos funid seqid args key0):items) acc chart
|
||||
process flit ftok !seqs !funs defs [] acc chart = (acc,chart)
|
||||
process flit ftok !seqs !funs defs (item@(Active j ppos funid seqid args key0):items) acc chart
|
||||
| inRange (bounds lin) ppos =
|
||||
case unsafeAt lin ppos of
|
||||
SymCat d r -> let !fid = args !! d
|
||||
SymCat d r -> let PArg hypos !fid = args !! d
|
||||
key = AK fid r
|
||||
|
||||
|
||||
items2 = case lookupPC (mkPK key k) (passive chart) of
|
||||
Nothing -> items
|
||||
Just id -> (Active j (ppos+1) funid seqid (updateAt d id args) key0) : items
|
||||
Just id -> (Active j (ppos+1) funid seqid (updateAt d (PArg hypos id) args) key0) : items
|
||||
items3 = foldForest (\funid args items -> Active k 0 funid (rhs funid r) args key : items)
|
||||
(\_ _ items -> items)
|
||||
items2 fid (forest chart)
|
||||
items2 fid (IntMap.unionWith Set.union new_sc (forest chart))
|
||||
|
||||
new_sc = foldl uu parent_sc hypos
|
||||
parent_sc = case lookupAC key0 ((active chart : actives chart) !! (k-j)) of
|
||||
Nothing -> IntMap.empty
|
||||
Just (set,sc) -> sc
|
||||
|
||||
in case lookupAC key (active chart) of
|
||||
Nothing -> process flit ftok seqs funs items3 acc chart{active=insertAC key (Set.singleton item) (active chart)}
|
||||
Just set | Set.member item set -> process flit ftok seqs funs items acc chart
|
||||
| otherwise -> process flit ftok seqs funs items2 acc chart{active=insertAC key (Set.insert item set) (active chart)}
|
||||
Nothing -> process flit ftok seqs funs defs items3 acc chart{active=insertAC key (Set.singleton item,new_sc) (active chart)}
|
||||
Just (set,sc) | Set.member item set -> process flit ftok seqs funs defs items acc chart
|
||||
| otherwise -> process flit ftok seqs funs defs items2 acc chart{active=insertAC key (Set.insert item set,IntMap.unionWith Set.union new_sc sc) (active chart)}
|
||||
SymKS toks -> let !acc' = ftok toks (Active j (ppos+1) funid seqid args key0) acc
|
||||
in process flit ftok seqs funs items acc' chart
|
||||
in process flit ftok seqs funs defs items acc' chart
|
||||
SymKP strs vars
|
||||
-> let !acc' = foldl (\acc toks -> ftok toks (Active j (ppos+1) funid seqid args key0) acc) acc
|
||||
(strs:[strs' | Alt strs' _ <- vars])
|
||||
in process flit ftok seqs funs items acc' chart
|
||||
SymLit d r -> let fid = args !! d
|
||||
in process flit ftok seqs funs defs items acc' chart
|
||||
SymLit d r -> let PArg hypos fid = args !! d
|
||||
key = AK fid r
|
||||
!fid' = case lookupPC (mkPK key k) (passive chart) of
|
||||
Nothing -> fid
|
||||
Just fid -> fid
|
||||
|
||||
in case [ts | PConst _ _ ts <- maybe [] Set.toList (IntMap.lookup fid' (forest chart))] of
|
||||
(toks:_) -> let !acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d fid' args) key0) acc
|
||||
in process flit ftok seqs funs items acc' chart
|
||||
(toks:_) -> let !acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d (PArg hypos fid') args) key0) acc
|
||||
in process flit ftok seqs funs defs items acc' chart
|
||||
[] -> case flit fid of
|
||||
Just (cat,lit,toks)
|
||||
-> let fid' = nextId chart
|
||||
!acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d fid' args) key0) acc
|
||||
in process flit ftok seqs funs items acc' chart{passive=insertPC (mkPK key k) fid' (passive chart)
|
||||
,forest =IntMap.insert fid' (Set.singleton (PConst cat lit toks)) (forest chart)
|
||||
,nextId =nextId chart+1
|
||||
}
|
||||
Nothing -> process flit ftok seqs funs items acc chart{active=insertAC key (Set.singleton item) (active chart)}
|
||||
!acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d (PArg hypos fid') args) key0) acc
|
||||
in process flit ftok seqs funs defs items acc' chart{passive=insertPC (mkPK key k) fid' (passive chart)
|
||||
,forest =IntMap.insert fid' (Set.singleton (PConst cat lit toks)) (forest chart)
|
||||
,nextId =nextId chart+1
|
||||
}
|
||||
Nothing -> process flit ftok seqs funs defs items acc chart
|
||||
SymVar d r -> let PArg hypos fid0 = args !! d
|
||||
(fid1,fid2) = hypos !! r
|
||||
key = AK fid1 0
|
||||
!fid' = case lookupPC (mkPK key k) (passive chart) of
|
||||
Nothing -> fid1
|
||||
Just fid -> fid
|
||||
|
||||
in case [ts | PConst _ _ ts <- maybe [] Set.toList (IntMap.lookup fid' (forest chart))] of
|
||||
(toks:_) -> let !acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d (PArg (updateAt r (fid',fid2) hypos) fid0) args) key0) acc
|
||||
in process flit ftok seqs funs defs items acc' chart
|
||||
[] -> case flit fid1 of
|
||||
Just (cat,lit,toks)
|
||||
-> let fid' = nextId chart
|
||||
!acc' = ftok toks (Active j (ppos+1) funid seqid (updateAt d (PArg (updateAt r (fid',fid2) hypos) fid0) args) key0) acc
|
||||
in process flit ftok seqs funs defs items acc' chart{passive=insertPC (mkPK key k) fid' (passive chart)
|
||||
,forest =IntMap.insert fid' (Set.singleton (PConst cat lit toks)) (forest chart)
|
||||
,nextId =nextId chart+1
|
||||
}
|
||||
Nothing -> process flit ftok seqs funs defs items acc chart
|
||||
| otherwise =
|
||||
case lookupPC (mkPK key0 j) (passive chart) of
|
||||
Nothing -> let fid = nextId chart
|
||||
|
||||
items2 = case lookupAC key0 ((active chart:actives chart) !! (k-j)) of
|
||||
Nothing -> items
|
||||
Just set -> Set.fold (\(Active j' ppos funid seqid args keyc) ->
|
||||
let SymCat d _ = unsafeAt (unsafeAt seqs seqid) ppos
|
||||
in (:) (Active j' (ppos+1) funid seqid (updateAt d fid args) keyc)) items set
|
||||
in process flit ftok seqs funs items2 acc chart{passive=insertPC (mkPK key0 j) fid (passive chart)
|
||||
,forest =IntMap.insert fid (Set.singleton (PApply funid args)) (forest chart)
|
||||
,nextId =nextId chart+1
|
||||
}
|
||||
Nothing -> items
|
||||
Just (set,sc) -> Set.fold (\(Active j' ppos funid seqid args keyc) ->
|
||||
let SymCat d _ = unsafeAt (unsafeAt seqs seqid) ppos
|
||||
PArg hypos _ = args !! d
|
||||
in (:) (Active j' (ppos+1) funid seqid (updateAt d (PArg hypos fid) args) keyc)) items set
|
||||
in process flit ftok seqs funs defs items2 acc chart{passive=insertPC (mkPK key0 j) fid (passive chart)
|
||||
,forest =IntMap.insert fid (Set.singleton (PApply funid args)) (forest chart)
|
||||
,nextId =nextId chart+1
|
||||
}
|
||||
Just id -> let items2 = [Active k 0 funid (rhs funid r) args (AK id r) | r <- labelsAC id (active chart)] ++ items
|
||||
in process flit ftok seqs funs items2 acc chart{forest = IntMap.insertWith Set.union id (Set.singleton (PApply funid args)) (forest chart)}
|
||||
in process flit ftok seqs funs defs items2 acc chart{forest = IntMap.insertWith Set.union id (Set.singleton (PApply funid args)) (forest chart)}
|
||||
where
|
||||
!lin = unsafeAt seqs seqid
|
||||
!k = offset chart
|
||||
@@ -367,6 +367,10 @@ process flit ftok !seqs !funs (item@(Active j ppos funid seqid args key0):items)
|
||||
where
|
||||
CncFun _ lins = unsafeAt funs funid
|
||||
|
||||
uu forest (fid1,fid2) =
|
||||
case IntMap.lookup fid2 defs of
|
||||
Just funs -> foldl (\forest funid -> IntMap.insertWith Set.union fid2 (Set.singleton (PApply funid [PArg [] fid1])) forest) forest funs
|
||||
Nothing -> forest
|
||||
|
||||
updateAt :: Int -> a -> [a] -> [a]
|
||||
updateAt nr x xs = [if i == nr then x else y | (i,y) <- zip [0..] xs]
|
||||
@@ -381,22 +385,22 @@ data Active
|
||||
{-# UNPACK #-} !DotPos
|
||||
{-# UNPACK #-} !FunId
|
||||
{-# UNPACK #-} !SeqId
|
||||
[FId]
|
||||
[PArg]
|
||||
{-# UNPACK #-} !ActiveKey
|
||||
deriving (Eq,Show,Ord)
|
||||
data ActiveKey
|
||||
= AK {-# UNPACK #-} !FId
|
||||
{-# UNPACK #-} !LIndex
|
||||
deriving (Eq,Ord,Show)
|
||||
type ActiveChart = IntMap.IntMap (IntMap.IntMap (Set.Set Active))
|
||||
type ActiveChart = IntMap.IntMap (IntMap.IntMap (Set.Set Active, IntMap.IntMap (Set.Set Production)))
|
||||
|
||||
emptyAC :: ActiveChart
|
||||
emptyAC = IntMap.empty
|
||||
|
||||
lookupAC :: ActiveKey -> ActiveChart -> Maybe (Set.Set Active)
|
||||
lookupAC :: ActiveKey -> ActiveChart -> Maybe (Set.Set Active, IntMap.IntMap (Set.Set Production))
|
||||
lookupAC (AK fcat l) chart = IntMap.lookup fcat chart >>= IntMap.lookup l
|
||||
|
||||
lookupACByFCat :: FId -> ActiveChart -> [Set.Set Active]
|
||||
lookupACByFCat :: FId -> ActiveChart -> [(Set.Set Active, IntMap.IntMap (Set.Set Production))]
|
||||
lookupACByFCat fcat chart =
|
||||
case IntMap.lookup fcat chart of
|
||||
Nothing -> []
|
||||
@@ -408,7 +412,7 @@ labelsAC fcat chart =
|
||||
Nothing -> []
|
||||
Just map -> IntMap.keys map
|
||||
|
||||
insertAC :: ActiveKey -> Set.Set Active -> ActiveChart -> ActiveChart
|
||||
insertAC :: ActiveKey -> (Set.Set Active, IntMap.IntMap (Set.Set Production)) -> ActiveChart -> ActiveChart
|
||||
insertAC (AK fcat l) set chart = IntMap.insertWith IntMap.union fcat (IntMap.singleton l set) chart
|
||||
|
||||
|
||||
|
||||
@@ -46,7 +46,9 @@ ppCnc name cnc =
|
||||
nest 2 (ppAll ppFlag (cflags cnc) $$
|
||||
text "productions" $$
|
||||
nest 2 (vcat [ppProduction (fcat,prod) | (fcat,set) <- IntMap.toList (productions cnc), prod <- Set.toList set]) $$
|
||||
text "functions" $$
|
||||
text "lindefs" $$
|
||||
nest 2 (vcat (map ppLinDef (IntMap.toList (lindefs cnc)))) $$
|
||||
text "lin" $$
|
||||
nest 2 (vcat (map ppCncFun (assocs (cncfuns cnc)))) $$
|
||||
text "sequences" $$
|
||||
nest 2 (vcat (map ppSeq (assocs (sequences cnc)))) $$
|
||||
@@ -56,8 +58,13 @@ ppCnc name cnc =
|
||||
nest 2 (vcat (map ppPrintName (Map.toList (printnames cnc))))) $$
|
||||
char '}'
|
||||
|
||||
ppCncArg :: PArg -> Doc
|
||||
ppCncArg (PArg hyps fid)
|
||||
| null hyps = ppFId fid
|
||||
| otherwise = hsep (map (ppFId . snd) hyps) <+> text "->" <+> ppFId fid
|
||||
|
||||
ppProduction (fid,PApply funid args) =
|
||||
ppFId fid <+> text "->" <+> ppFunId funid <> brackets (hcat (punctuate comma (map ppFId args)))
|
||||
ppFId fid <+> text "->" <+> ppFunId funid <> brackets (hcat (punctuate comma (map ppCncArg args)))
|
||||
ppProduction (fid,PCoerce arg) =
|
||||
ppFId fid <+> text "->" <+> char '_' <> brackets (ppFId arg)
|
||||
ppProduction (fid,PConst _ _ ss) =
|
||||
@@ -66,6 +73,9 @@ ppProduction (fid,PConst _ _ ss) =
|
||||
ppCncFun (funid,CncFun fun arr) =
|
||||
ppFunId funid <+> text ":=" <+> parens (hcat (punctuate comma (map ppSeqId (elems arr)))) <+> brackets (ppCId fun)
|
||||
|
||||
ppLinDef (fid,funids) =
|
||||
ppFId fid <+> text "->" <+> hcat (punctuate comma (map ppFunId funids))
|
||||
|
||||
ppSeq (seqid,seq) =
|
||||
ppSeqId seqid <+> text ":=" <+> hsep (map ppSymbol (elems seq))
|
||||
|
||||
@@ -78,6 +88,7 @@ ppPrintName (id,name) =
|
||||
|
||||
ppSymbol (SymCat d r) = char '<' <> int d <> comma <> int r <> char '>'
|
||||
ppSymbol (SymLit d r) = char '{' <> int d <> comma <> int r <> char '}'
|
||||
ppSymbol (SymVar d r) = char '<' <> int d <> comma <> char '$' <> int r <> char '>'
|
||||
ppSymbol (SymKS ts) = ppStrs ts
|
||||
ppSymbol (SymKP ts alts) = text "pre" <+> braces (hsep (punctuate semi (ppStrs ts : map ppAlt alts)))
|
||||
|
||||
|
||||
@@ -11,9 +11,17 @@
|
||||
--
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PGF.TypeCheck (checkType, checkExpr, inferExpr,
|
||||
module PGF.TypeCheck ( checkType, checkExpr, inferExpr
|
||||
|
||||
ppTcError, TcError(..)
|
||||
, ppTcError, TcError(..)
|
||||
|
||||
-- internals needed for the typechecking of forests
|
||||
, MetaStore, newMeta, newGuardedMeta
|
||||
, Scope, emptyScope, scopeSize, scopeEnv, addScopedVar
|
||||
, TcM(..), TcResult(..), TType(..), tcError
|
||||
, tcExpr, infExpr, eqType
|
||||
, lookupFunType, eval
|
||||
, refineExpr, checkResolvedMetaStore
|
||||
) where
|
||||
|
||||
import PGF.Data
|
||||
@@ -65,7 +73,7 @@ scopeSize (Scope gamma) = length gamma
|
||||
|
||||
type MetaStore = IntMap MetaValue
|
||||
data MetaValue
|
||||
= MUnbound Scope [Expr -> TcM ()]
|
||||
= MUnbound Scope TType [Expr -> TcM ()]
|
||||
| MBound Expr
|
||||
| MGuarded Expr [Expr -> TcM ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
|
||||
-- to unlock this meta variable
|
||||
@@ -96,9 +104,9 @@ lookupFunType fun = TcM (\abstr ms -> case Map.lookup fun (funs abstr) of
|
||||
Just (ty,_,_) -> Ok ms (TTyp [] ty)
|
||||
Nothing -> Fail (UnknownFun fun))
|
||||
|
||||
newMeta :: Scope -> TcM MetaId
|
||||
newMeta scope = TcM (\abstr ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok (IntMap.insert metaid (MUnbound scope []) ms) metaid)
|
||||
newMeta :: Scope -> TType -> TcM MetaId
|
||||
newMeta scope tty = TcM (\abstr ms -> let metaid = IntMap.size ms + 1
|
||||
in Ok (IntMap.insert metaid (MUnbound scope tty []) ms) metaid)
|
||||
|
||||
newGuardedMeta :: Expr -> TcM MetaId
|
||||
newGuardedMeta e = TcM (\abstr ms -> let metaid = IntMap.size ms + 1
|
||||
@@ -115,7 +123,7 @@ lookupMeta ms i =
|
||||
Just (MBound t) -> Just t
|
||||
Just (MGuarded t _ x) | x == 0 -> Just t
|
||||
| otherwise -> Nothing
|
||||
Just (MUnbound _ _) -> Nothing
|
||||
Just (MUnbound _ _ _) -> Nothing
|
||||
Nothing -> Nothing
|
||||
|
||||
tcError :: TcError -> TcM a
|
||||
@@ -125,7 +133,7 @@ addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM
|
||||
addConstraint i j env vs c = do
|
||||
mv <- getMeta j
|
||||
case mv of
|
||||
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> apply env e vs >>= c) : cs))
|
||||
MUnbound scope tty cs -> addRef >> setMeta j (MUnbound scope tty ((\e -> release >> apply env e vs >>= c) : cs))
|
||||
MBound e -> apply env e vs >>= c
|
||||
MGuarded e cs x | x == 0 -> apply env e vs >>= c
|
||||
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> apply env e vs >>= c) : cs) x)
|
||||
@@ -162,6 +170,8 @@ data TcError
|
||||
| CannotInferType [CId] Expr -- ^ It is not possible to infer the type of an expression.
|
||||
| UnresolvedMetaVars [CId] Expr [MetaId] -- ^ Some metavariables have to be instantiated in order to complete the typechecking.
|
||||
| UnexpectedImplArg [CId] Expr -- ^ Implicit argument was passed where the type doesn't allow it
|
||||
| UnsolvableGoal [CId] MetaId Type -- ^ There is a goal that cannot be solved
|
||||
deriving Eq
|
||||
|
||||
-- | Renders the type checking error to a document. See 'Text.PrettyPrint'.
|
||||
ppTcError :: TcError -> Doc
|
||||
@@ -177,6 +187,8 @@ ppTcError (CannotInferType xs e) = text "Cannot infer the type of expressi
|
||||
ppTcError (UnresolvedMetaVars xs e ms) = text "Meta variable(s)" <+> fsep (List.map ppMeta ms) <+> text "should be resolved" $$
|
||||
text "in the expression:" <+> ppExpr 0 xs e
|
||||
ppTcError (UnexpectedImplArg xs e) = braces (ppExpr 0 xs e) <+> text "is implicit argument but not implicit argument is expected here"
|
||||
ppTcError (UnsolvableGoal xs metaid ty)= text "The goal:" <+> ppMeta metaid <+> colon <+> ppType 0 xs ty $$
|
||||
text "cannot be solved"
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkType
|
||||
@@ -223,7 +235,7 @@ tcCatArgs scope (EImplArg e:es) delta ((Implicit,x,ty):hs) ty0 n m = do
|
||||
tcCatArgs scope es (v:delta) hs ty0 n m
|
||||
return (delta,EImplArg e:es)
|
||||
tcCatArgs scope es delta ((Implicit,x,ty):hs) ty0 n m = do
|
||||
i <- newMeta scope
|
||||
i <- newMeta scope (TTyp delta ty)
|
||||
(delta,es) <- if x == wildCId
|
||||
then tcCatArgs scope es delta hs ty0 n m
|
||||
else tcCatArgs scope es (VMeta i (scopeEnv scope) [] : delta) hs ty0 n m
|
||||
@@ -281,7 +293,7 @@ tcExpr scope e0@(EAbs Explicit x e) tty =
|
||||
_ -> do ty <- evalType (scopeSize scope) tty
|
||||
tcError (NotFunType (scopeVars scope) e0 ty)
|
||||
tcExpr scope (EMeta _) tty = do
|
||||
i <- newMeta scope
|
||||
i <- newMeta scope tty
|
||||
return (EMeta i)
|
||||
tcExpr scope e0 tty = do
|
||||
(e0,tty0) <- infExpr scope e0
|
||||
@@ -352,7 +364,7 @@ tcArg scope e1 e2 delta ty0@(DTyp ((Explicit,x,ty):hs) c es) = do
|
||||
else do v2 <- eval (scopeEnv scope) e2
|
||||
return (EApp e1 e2,v2:delta,DTyp hs c es)
|
||||
tcArg scope e1 e2 delta ty0@(DTyp ((Implicit,x,ty):hs) c es) = do
|
||||
i <- newMeta scope
|
||||
i <- newMeta scope (TTyp delta ty)
|
||||
if x == wildCId
|
||||
then tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 delta (DTyp hs c es)
|
||||
else tcArg scope (EApp e1 (EImplArg (EMeta i))) e2 (VMeta i (scopeEnv scope) [] : delta) (DTyp hs c es)
|
||||
@@ -402,7 +414,7 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
MBound e -> apply env e vs
|
||||
MGuarded e _ x | x == 0 -> apply env e vs
|
||||
| otherwise -> return v
|
||||
MUnbound _ _ -> return v
|
||||
MUnbound _ _ _ -> return v
|
||||
deRef v = return v
|
||||
|
||||
eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
|
||||
@@ -410,15 +422,15 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VMeta i env1 vs1) v2 = do mv <- getMeta i
|
||||
case mv of
|
||||
MUnbound scopei cs -> do e2 <- mkLam i scopei env1 vs1 v2
|
||||
setMeta i (MBound e2)
|
||||
sequence_ [c e2 | c <- cs]
|
||||
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x)
|
||||
MUnbound scopei _ cs -> do e2 <- mkLam i scopei env1 vs1 v2
|
||||
setMeta i (MBound e2)
|
||||
sequence_ [c e2 | c <- cs]
|
||||
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env1 e vs1 >>= \v1 -> eqValue' k v1 v2) : cs) x)
|
||||
eqValue' k v1 (VMeta i env2 vs2) = do mv <- getMeta i
|
||||
case mv of
|
||||
MUnbound scopei cs -> do e1 <- mkLam i scopei env2 vs2 v1
|
||||
setMeta i (MBound e1)
|
||||
sequence_ [c e1 | c <- cs]
|
||||
MUnbound scopei _ cs -> do e1 <- mkLam i scopei env2 vs2 v1
|
||||
setMeta i (MBound e1)
|
||||
sequence_ [c e1 | c <- cs]
|
||||
MGuarded e cs x -> setMeta i (MGuarded e ((\e -> apply env2 e vs2 >>= \v2 -> eqValue' k v1 v2) : cs) x)
|
||||
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VConst f1 vs1) (VConst f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
|
||||
@@ -452,11 +464,11 @@ eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2
|
||||
else return ()
|
||||
mv <- getMeta i
|
||||
case mv of
|
||||
MBound e -> apply env e vs >>= occurCheck i0 k xs
|
||||
MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs
|
||||
MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
|
||||
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VMeta i env vs)
|
||||
MBound e -> apply env e vs >>= occurCheck i0 k xs
|
||||
MGuarded e _ _ -> apply env e vs >>= occurCheck i0 k xs
|
||||
MUnbound scopei _ _ | scopeSize scopei > k -> raiseTypeMatchError
|
||||
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VMeta i env vs)
|
||||
occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
|
||||
return (VSusp i env vs cnt)
|
||||
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
|
||||
@@ -480,7 +492,7 @@ checkResolvedMetaStore scope e = TcM (\abstr ms ->
|
||||
then Ok ms ()
|
||||
else Fail (UnresolvedMetaVars (scopeVars scope) e xs))
|
||||
where
|
||||
isResolved (MUnbound _ []) = True
|
||||
isResolved (MUnbound _ _ []) = True
|
||||
isResolved (MGuarded _ _ _) = True
|
||||
isResolved (MBound _) = True
|
||||
isResolved _ = False
|
||||
|
||||
@@ -28,7 +28,7 @@ import PGF.CId (CId,showCId,ppCId,pCId,mkCId)
|
||||
import PGF.Data
|
||||
import PGF.Expr (showExpr, Tree)
|
||||
import PGF.Linearize
|
||||
import PGF.Macros (lookValCat, lookMap, _B, _V,
|
||||
import PGF.Macros (lookValCat, lookMap,
|
||||
BracketedString(..), BracketedTokn(..), flattenBracketedString)
|
||||
|
||||
import qualified Data.Map as Map
|
||||
@@ -286,17 +286,14 @@ linTree pgf lang mark e = lin0 [] [] [] Nothing e
|
||||
|
||||
lin0 path xs ys mb_fid (EAbs _ x e) = lin0 path (showCId x:xs) ys mb_fid e
|
||||
lin0 path xs ys mb_fid (ETyped e _) = lin0 path xs ys mb_fid e
|
||||
lin0 path xs ys mb_fid e | null xs = lin path ys mb_fid e []
|
||||
| otherwise = apply path (xs ++ ys) mb_fid _B (e:[ELit (LStr x) | x <- xs])
|
||||
lin0 path xs ys mb_fid e = lin path ys mb_fid e []
|
||||
|
||||
lin path xs mb_fid (EApp e1 e2) es = lin path xs mb_fid e1 (e2:es)
|
||||
lin path xs mb_fid (ELit l) [] = case l of
|
||||
LStr s -> return (mark Nothing path (ss s))
|
||||
LInt n -> return (mark Nothing path (ss (show n)))
|
||||
LFlt f -> return (mark Nothing path (ss (show f)))
|
||||
lin path xs mb_fid (EMeta i) es = apply path xs mb_fid _V (ELit (LStr ('?':show i)):es)
|
||||
lin path xs mb_fid (EFun f) es = map (mark (Just f) path) (apply path xs mb_fid f es)
|
||||
lin path xs mb_fid (EVar i) es = apply path xs mb_fid _V (ELit (LStr (xs !! i)) :es)
|
||||
lin path xs mb_fid (ETyped e _) es = lin path xs mb_fid e es
|
||||
lin path xs mb_fid (EImplArg e) es = lin path xs mb_fid e es
|
||||
|
||||
@@ -308,21 +305,16 @@ linTree pgf lang mark e = lin0 [] [] [] Nothing e
|
||||
Just set -> do prod <- Set.toList set
|
||||
case prod of
|
||||
PApply funid fids -> do guard (length fids == length es)
|
||||
args <- sequence (zipWith3 (\i fid e -> lin0 (sub i path) [] xs (Just fid) e) [0..] fids es)
|
||||
args <- sequence (zipWith3 (\i (PArg _ fid) e -> lin0 (sub i path) [] xs (Just fid) e) [0..] fids es)
|
||||
let (CncFun _ lins) = cncfuns cnc ! funid
|
||||
return (listArray (bounds lins) [computeSeq seqid args | seqid <- elems lins])
|
||||
PCoerce fid -> apply path xs (Just fid) f es
|
||||
Nothing -> mzero
|
||||
Nothing -> apply path xs mb_fid _V [ELit (LStr ("[" ++ showCId f ++ "]"))] -- fun without lin
|
||||
where
|
||||
lookupProds (Just fid) prods = IntMap.lookup fid prods
|
||||
lookupProds Nothing prods
|
||||
| f == _B || f == _V = Nothing
|
||||
| otherwise = Just (Set.filter isApp (Set.unions (IntMap.elems prods)))
|
||||
lookupProds Nothing prods = Just (Set.filter isApp (Set.unions (IntMap.elems prods)))
|
||||
|
||||
sub i path
|
||||
| f == _B || f == _V = path
|
||||
| otherwise = i:path
|
||||
sub i path = i:path
|
||||
|
||||
isApp (PApply _ _) = True
|
||||
isApp _ = False
|
||||
|
||||
Reference in New Issue
Block a user