judgements lindef are now respected by both the parser and the linearizer

This commit is contained in:
krasimir
2009-12-11 17:39:18 +00:00
parent fc1d03f2f1
commit 7c2bce5779
4 changed files with 50 additions and 30 deletions

View File

@@ -40,14 +40,15 @@ convertConcrete opts abs lang cnc = do
let env0 = emptyGrammarEnv cnc_defs cat_defs
when (flag optProf opts) $ do
profileGrammar lang cnc_defs env0 pfrules
let env1 = expandHOAS abs_defs cnc_defs cat_defs env0
let env1 = expandHOAS abs_defs cnc_defs cat_defs lin_defs env0
env2 = List.foldl' (convertRule cnc_defs) env1 pfrules
return $ getParserInfo env2
where
abs_defs = Map.assocs (funs abs)
cnc_defs = Map.union (opers cnc) (lins cnc) -- "union big+small most efficient"
cat_defs = lincats cnc
cat_defs = Map.insert cidVar (S []) (lincats cnc)
lin_defs = lindefs cnc
pfrules = [
(PFRule id args (0,res) (map findLinType args) (findLinType (0,res)) term) |
(id, (ty,_,_)) <- abs_defs, let (args,res) = typeSkeleton ty,
@@ -352,6 +353,7 @@ emptyGrammarEnv cnc_defs lincats =
| cat == cidString = (index, (fcatString,fcatString,[]))
| cat == cidInt = (index, (fcatInt, fcatInt, []))
| cat == cidFloat = (index, (fcatFloat, fcatFloat, []))
| cat == cidVar = (index, (fcatVar, fcatVar, []))
| otherwise = (index+size,(index,index+size-1,poly))
where
(size,poly) = getMultipliers 1 [] ctype
@@ -363,7 +365,7 @@ emptyGrammarEnv cnc_defs lincats =
Just term -> getMultipliers m ms term
Nothing -> error ("unknown identifier: "++showCId id)
expandHOAS abs_defs cnc_defs lincats env =
expandHOAS abs_defs cnc_defs lincats lindefs env =
foldl add_varFun (foldl (\env ncat -> add_hoFun (add_hoCat env ncat) ncat) env hoTypes) hoCats
where
hoTypes :: [(Int,CId)]
@@ -405,17 +407,22 @@ expandHOAS abs_defs cnc_defs lincats env =
-- add one PMCFG function for each high-order category: _V : Var -> Cat
add_varFun env cat =
let (env1,seqid) = addFSeq env [FSymLit 0 0]
lins = replicate (case res of {PFCat _ _ rcs _ -> length rcs}) seqid
(env2,funid) = addFFun env1 (FFun _V [[0]] (mkArray lins))
env3 = foldl (\env res -> addProduction env2 res (FApply funid [fcatVar]))
env2
(getFCats env2 res)
in env3
convertRule cnc_defs env (PFRule _V [(0,cidVar)] (0,cat) [arg] res lindef)
where
res = case Map.lookup cat lincats of
Nothing -> error $ "No lincat for " ++ showCId cat
Just ctype -> protoFCat cnc_defs (0,cat) ctype
lindef =
case Map.lookup cat lindefs of
Nothing -> error $ "No lindef for " ++ showCId cat
Just def -> def
arg =
case Map.lookup cidVar lincats of
Nothing -> error $ "No lincat for " ++ showCId cat
Just ctype -> ctype
res =
case Map.lookup cat lincats of
Nothing -> error $ "No lincat for " ++ showCId cat
Just ctype -> ctype
_B = mkCId "_B"
_V = mkCId "_V"

View File

@@ -1,3 +1,4 @@
{-# LANGUAGE ParallelListComp #-}
module PGF.Linearize
(linearizes,realize,realizes,linTree, linTreeMark,linearizesMark) where
@@ -56,20 +57,26 @@ liftVariants = f
f t = return t
linTree :: PGF -> CId -> Expr -> Term
linTree pgf lang = lin . expr2tree
linTree pgf lang e = lin (expr2tree e) Nothing
where
lin (Abs xs e ) = case lin e of
R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs)
TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
lin (Fun fun es) = let argVariants = mapM (liftVariants . lin) es
in variants [compute pgf lang args $ look fun | args <- argVariants]
lin (Lit (LStr s)) = R [kks (show s)] -- quoted
lin (Lit (LInt i)) = R [kks (show i)]
lin (Lit (LFlt d)) = R [kks (show d)]
lin (Var x) = TM (showCId x)
lin (Meta i) = TM (show i)
look = lookLin pgf lang
cnc = lookMap (error "no lang") lang (concretes pgf)
lin (Abs xs e ) mty = case lin e Nothing of
R ts -> R $ ts ++ (Data.List.map (kks . showCId . snd) xs)
TM s -> R $ (TM s) : (Data.List.map (kks . showCId . snd) xs)
lin (Fun fun es) mty = case Map.lookup fun (funs (abstract pgf)) of
Just (DTyp hyps _ _,_,_) -> let argVariants = sequence [liftVariants (lin e (Just ty)) | e <- es | (_,_,ty) <- hyps]
in variants [compute pgf lang args $ lookMap tm0 fun (lins cnc) | args <- argVariants]
Nothing -> tm0
lin (Lit (LStr s)) mty = R [kks (show s)] -- quoted
lin (Lit (LInt i)) mty = R [kks (show i)]
lin (Lit (LFlt d)) mty = R [kks (show d)]
lin (Var x) mty = case mty of
Just (DTyp _ cat _) -> compute pgf lang [K (KS (showCId x))] (lookMap tm0 cat (lindefs cnc))
Nothing -> TM (showCId x)
lin (Meta i) mty = case mty of
Just (DTyp _ cat _) -> compute pgf lang [K (KS (show i))] (lookMap tm0 cat (lindefs cnc))
Nothing -> TM (show i)
variants :: [Term] -> Term
variants ts = case ts of

View File

@@ -146,8 +146,9 @@ combinations t = case t of
aa:uu -> [a:u | a <- aa, u <- combinations uu]
isLiteralCat :: CId -> Bool
isLiteralCat = (`elem` [cidString, cidFloat, cidInt])
isLiteralCat = (`elem` [cidString, cidFloat, cidInt, cidVar])
cidString = mkCId "String"
cidInt = mkCId "Int"
cidFloat = mkCId "Float"
cidVar = mkCId "#Var"

View File

@@ -1,7 +1,12 @@
concrete TestCnc of Test = {
lincat E,P = {s:Str} ;
param Number = Pl | Sg;
lincat E = {s:Str; n : Number} ;
lindef E = \s -> {s=s; n=Sg} ;
lincat P = {s:Str} ;
lin Exist f = {s = "exists" ++ f.$0 ++ "such that" ++ f.s};
lin Even x = {s = x.s ++ "is even"};
lin Even x = {s = x.s ++ case x.n of {Sg => "is"; Pl => "are"} ++ "even"};
}