mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-23 09:52:55 -06:00
small progress on PMCFG
This commit is contained in:
@@ -258,7 +258,7 @@ checkComputeTerm os sgr t =
|
|||||||
t <- renameSourceTerm sgr mo t
|
t <- renameSourceTerm sgr mo t
|
||||||
(t,_) <- inferLType sgr [] t
|
(t,_) <- inferLType sgr [] t
|
||||||
let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
|
let opts = modifyFlags (\fs->fs{optTrace=isOpt "trace" os})
|
||||||
fmap evalStr (normalForm sgr (L NoLoc identW) t)
|
fmap evalStr (normalForm sgr t)
|
||||||
where
|
where
|
||||||
-- ** Try to compute pre{...} tokens in token sequences
|
-- ** Try to compute pre{...} tokens in token sequences
|
||||||
evalStr t =
|
evalStr t =
|
||||||
|
|||||||
@@ -183,7 +183,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
mty <- case mty of
|
mty <- case mty of
|
||||||
Just (L loc typ) -> chIn loc "linearization type of" $ do
|
Just (L loc typ) -> chIn loc "linearization type of" $ do
|
||||||
(typ,_) <- checkLType gr [] typ typeType
|
(typ,_) <- checkLType gr [] typ typeType
|
||||||
typ <- CN.normalForm gr (L loc c) typ
|
typ <- CN.normalForm gr typ
|
||||||
return (Just (L loc typ))
|
return (Just (L loc typ))
|
||||||
Nothing -> return Nothing
|
Nothing -> return Nothing
|
||||||
mdef <- case (mty,mdef) of
|
mdef <- case (mty,mdef) of
|
||||||
@@ -226,7 +226,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
|
|||||||
(Just (L loct ty), Just (L locd de)) -> do
|
(Just (L loct ty), Just (L locd de)) -> do
|
||||||
ty' <- chIn loct "operation" $ do
|
ty' <- chIn loct "operation" $ do
|
||||||
(ty,_) <- checkLType gr [] ty typeType
|
(ty,_) <- checkLType gr [] ty typeType
|
||||||
CN.normalForm gr (L loct c) ty
|
CN.normalForm gr ty
|
||||||
(de',_) <- chIn locd "operation" $
|
(de',_) <- chIn locd "operation" $
|
||||||
checkLType gr [] de ty'
|
checkLType gr [] de ty'
|
||||||
return (Just (L loct ty'), Just (L locd de'))
|
return (Just (L loct ty'), Just (L locd de'))
|
||||||
@@ -316,6 +316,6 @@ linTypeOfType cnc m (L loc typ) = do
|
|||||||
plusRecType vars val
|
plusRecType vars val
|
||||||
return (Explicit,symb,rec)
|
return (Explicit,symb,rec)
|
||||||
lookLin (_,c) = checks [ --- rather: update with defLinType ?
|
lookLin (_,c) = checks [ --- rather: update with defLinType ?
|
||||||
lookupLincat cnc m c >>= CN.normalForm cnc (L loc c)
|
lookupLincat cnc m c >>= CN.normalForm cnc
|
||||||
,return defLinType
|
,return defLinType
|
||||||
]
|
]
|
||||||
|
|||||||
@@ -4,15 +4,18 @@
|
|||||||
-- | preparation for PMCFG generation.
|
-- | preparation for PMCFG generation.
|
||||||
module GF.Compile.Compute.Concrete
|
module GF.Compile.Compute.Concrete
|
||||||
( normalForm
|
( normalForm
|
||||||
, Value(..), Thunk, ThunkState(..), Env, EvalM, runEvalM
|
, Value(..), Thunk, ThunkState(..), Env
|
||||||
|
, EvalM, runEvalM, evalError
|
||||||
, eval, apply, force, value2term
|
, eval, apply, force, value2term
|
||||||
, newMeta,newEvaluatedThunk,getAllParamValues
|
, newMeta,getMeta,setMeta
|
||||||
|
, newEvaluatedThunk,getAllParamValues
|
||||||
|
, lookupParams
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||||
|
|
||||||
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
||||||
import GF.Grammar.Lookup(lookupResDef,allParamValues)
|
import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo,allParamValues)
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Grammar.Lockfield(lockLabel)
|
import GF.Grammar.Lockfield(lockLabel)
|
||||||
import GF.Grammar.Printer
|
import GF.Grammar.Printer
|
||||||
@@ -34,8 +37,8 @@ import GF.Text.Pretty
|
|||||||
|
|
||||||
-- * Main entry points
|
-- * Main entry points
|
||||||
|
|
||||||
normalForm :: Grammar -> L Ident -> Term -> Check Term
|
normalForm :: Grammar -> Term -> Check Term
|
||||||
normalForm gr loc t =
|
normalForm gr t =
|
||||||
fmap mkFV (runEvalM gr (eval [] t [] >>= value2term 0))
|
fmap mkFV (runEvalM gr (eval [] t [] >>= value2term 0))
|
||||||
where
|
where
|
||||||
mkFV [t] = t
|
mkFV [t] = t
|
||||||
@@ -45,7 +48,7 @@ normalForm gr loc t =
|
|||||||
data ThunkState s
|
data ThunkState s
|
||||||
= Unevaluated (Env s) Term
|
= Unevaluated (Env s) Term
|
||||||
| Evaluated (Value s)
|
| Evaluated (Value s)
|
||||||
| Unbound {-# UNPACK #-} !MetaId
|
| Unbound (Maybe Type) {-# UNPACK #-} !MetaId
|
||||||
|
|
||||||
type Thunk s = STRef s (ThunkState s)
|
type Thunk s = STRef s (ThunkState s)
|
||||||
type Env s = [(Ident,Thunk s)]
|
type Env s = [(Ident,Thunk s)]
|
||||||
@@ -91,7 +94,7 @@ eval env (App t1 t2) vs = do tnk <- newThunk env t2
|
|||||||
eval env t1 (tnk : vs)
|
eval env t1 (tnk : vs)
|
||||||
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
|
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
|
||||||
eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
|
eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
|
||||||
eval env (Meta i) vs = do tnk <- newMeta i
|
eval env (Meta i) vs = do tnk <- newMeta Nothing i
|
||||||
return (VMeta tnk env vs)
|
return (VMeta tnk env vs)
|
||||||
eval env (ImplArg t) [] = eval env t []
|
eval env (ImplArg t) [] = eval env t []
|
||||||
eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 []
|
eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 []
|
||||||
@@ -180,11 +183,14 @@ eval env (Strs ts) [] = do vs <- mapM (\t -> eval env t []) ts
|
|||||||
return (VStrs vs)
|
return (VStrs vs)
|
||||||
eval env t vs = evalError ("Cannot reduce term" <+> pp t)
|
eval env t vs = evalError ("Cannot reduce term" <+> pp t)
|
||||||
|
|
||||||
apply v [] = return v
|
apply (VMeta m env vs0) vs = do st <- getMeta m
|
||||||
|
case st of
|
||||||
|
Evaluated v -> apply v vs
|
||||||
|
Unbound _ _ -> return (VMeta m env (vs0++vs))
|
||||||
apply (VApp f vs0) vs = return (VApp f (vs0++vs))
|
apply (VApp f vs0) vs = return (VApp f (vs0++vs))
|
||||||
apply (VMeta m env vs0) vs = return (VMeta m env (vs0++vs))
|
|
||||||
apply (VGen i vs0) vs = return (VGen i (vs0++vs))
|
apply (VGen i vs0) vs = return (VGen i (vs0++vs))
|
||||||
apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
|
apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
|
||||||
|
apply v [] = return v
|
||||||
|
|
||||||
evalPredef id [v]
|
evalPredef id [v]
|
||||||
| id == cLength = return (fmap VInt (liftM genericLength (value2string v)))
|
| id == cLength = return (fmap VInt (liftM genericLength (value2string v)))
|
||||||
@@ -243,6 +249,7 @@ update lbl v (a@(lbl',_):as)
|
|||||||
| lbl==lbl' = (lbl,v) : as
|
| lbl==lbl' = (lbl,v) : as
|
||||||
| otherwise = a : update lbl v as
|
| otherwise = a : update lbl v as
|
||||||
|
|
||||||
|
|
||||||
patternMatch v0 [] = fail "No matching pattern found"
|
patternMatch v0 [] = fail "No matching pattern found"
|
||||||
patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
|
patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
|
||||||
where
|
where
|
||||||
@@ -393,6 +400,7 @@ value2term i (VAlts vd vas) = do
|
|||||||
value2term i (VStrs vs) = do
|
value2term i (VStrs vs) = do
|
||||||
ts <- mapM (value2term i) vs
|
ts <- mapM (value2term i) vs
|
||||||
return (Strs ts)
|
return (Strs ts)
|
||||||
|
|
||||||
value2string (VStr s) = Just s
|
value2string (VStr s) = Just s
|
||||||
value2string (VC vs) = fmap unwords (mapM value2string vs)
|
value2string (VC vs) = fmap unwords (mapM value2string vs)
|
||||||
value2string _ = Nothing
|
value2string _ = Nothing
|
||||||
@@ -457,6 +465,14 @@ lookupGlobal q = EvalM $ \gr k mt r -> do
|
|||||||
Ok t -> k t mt r
|
Ok t -> k t mt r
|
||||||
Bad msg -> return (Fail (pp msg))
|
Bad msg -> return (Fail (pp msg))
|
||||||
|
|
||||||
|
lookupParams :: QIdent -> EvalM s (ModuleName,[Param])
|
||||||
|
lookupParams q = EvalM $ \gr k mt r -> do
|
||||||
|
case lookupOrigInfo gr q of
|
||||||
|
Ok (m,info) -> case info of
|
||||||
|
ResParam (Just (L _ ps)) _ -> k (m,ps) mt r
|
||||||
|
_ -> return (Fail (ppQIdent Qualified q <+> "is not a parameter type"))
|
||||||
|
Bad msg -> return (Fail (pp msg))
|
||||||
|
|
||||||
getAllParamValues :: Type -> EvalM s [Term]
|
getAllParamValues :: Type -> EvalM s [Term]
|
||||||
getAllParamValues ty = EvalM $ \gr k mt r ->
|
getAllParamValues ty = EvalM $ \gr k mt r ->
|
||||||
case allParamValues gr ty of
|
case allParamValues gr ty of
|
||||||
@@ -471,15 +487,24 @@ newEvaluatedThunk v = EvalM $ \gr k mt r -> do
|
|||||||
tnk <- newSTRef (Evaluated v)
|
tnk <- newSTRef (Evaluated v)
|
||||||
k tnk mt r
|
k tnk mt r
|
||||||
|
|
||||||
newMeta i = EvalM $ \gr k mt r ->
|
newMeta mb_ty i = EvalM $ \gr k mt r ->
|
||||||
if i == 0
|
if i == 0
|
||||||
then do tnk <- newSTRef (Unbound i)
|
then do tnk <- newSTRef (Unbound mb_ty i)
|
||||||
k tnk mt r
|
k tnk mt r
|
||||||
else case Map.lookup i mt of
|
else case Map.lookup i mt of
|
||||||
Just tnk -> k tnk mt r
|
Just tnk -> k tnk mt r
|
||||||
Nothing -> do tnk <- newSTRef (Unbound i)
|
Nothing -> do tnk <- newSTRef (Unbound mb_ty i)
|
||||||
k tnk (Map.insert i tnk mt) r
|
k tnk (Map.insert i tnk mt) r
|
||||||
|
|
||||||
|
getMeta tnk = EvalM $ \gr k mt r -> readSTRef tnk >>= \st -> k st mt r
|
||||||
|
|
||||||
|
setMeta tnk st = EvalM $ \gr k mt r -> do
|
||||||
|
old <- readSTRef tnk
|
||||||
|
writeSTRef tnk st
|
||||||
|
r <- k () mt r
|
||||||
|
writeSTRef tnk old
|
||||||
|
return r
|
||||||
|
|
||||||
newGen i = EvalM $ \gr k mt r -> do
|
newGen i = EvalM $ \gr k mt r -> do
|
||||||
tnk <- newSTRef (Evaluated (VGen i []))
|
tnk <- newSTRef (Evaluated (VGen i []))
|
||||||
k tnk mt r
|
k tnk mt r
|
||||||
@@ -494,10 +519,11 @@ force tnk vs = EvalM $ \gr k mt r -> do
|
|||||||
return r) mt r
|
return r) mt r
|
||||||
Evaluated v -> case apply v vs of
|
Evaluated v -> case apply v vs of
|
||||||
EvalM f -> f gr k mt r
|
EvalM f -> f gr k mt r
|
||||||
|
Unbound _ _ -> k (VMeta tnk [] vs) mt r
|
||||||
|
|
||||||
zonk tnk vs = EvalM $ \gr k mt r -> do
|
zonk tnk vs = EvalM $ \gr k mt r -> do
|
||||||
s <- readSTRef tnk
|
s <- readSTRef tnk
|
||||||
case s of
|
case s of
|
||||||
Evaluated v -> case apply v vs of
|
Evaluated v -> case apply v vs of
|
||||||
EvalM f -> f gr (k . Left) mt r
|
EvalM f -> f gr (k . Left) mt r
|
||||||
Unbound i -> k (Right i) mt r
|
Unbound _ i -> k (Right i) mt r
|
||||||
|
|||||||
@@ -13,24 +13,27 @@ module GF.Compile.GeneratePMCFG
|
|||||||
(generatePMCFG, pgfCncCat, addPMCFG
|
(generatePMCFG, pgfCncCat, addPMCFG
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Grammar
|
import GF.Grammar hiding (VApp)
|
||||||
import GF.Grammar.Predef
|
import GF.Grammar.Predef
|
||||||
import GF.Infra.CheckM
|
import GF.Infra.CheckM
|
||||||
import GF.Infra.Option
|
import GF.Infra.Option
|
||||||
|
import GF.Text.Pretty
|
||||||
import GF.Compile.Compute.Concrete
|
import GF.Compile.Compute.Concrete
|
||||||
import PGF2.Transactions
|
import PGF2.Transactions
|
||||||
import qualified Data.Map.Strict as Map
|
import qualified Data.Map.Strict as Map
|
||||||
|
import Control.Monad
|
||||||
|
|
||||||
generatePMCFG :: Options -> SourceGrammar -> SourceModule -> Check SourceModule
|
generatePMCFG :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
|
||||||
generatePMCFG opts gr cmo@(cm,cmi) = do
|
generatePMCFG opts cwd gr cmo@(cm,cmi) = do
|
||||||
let gr' = prependModule gr cmo
|
let gr' = prependModule gr cmo
|
||||||
js <- mapM (addPMCFG opts gr') (Map.toList (jments cmi))
|
js <- mapM (addPMCFG opts cwd gr' cmi) (Map.toList (jments cmi))
|
||||||
return (cm,cmi{jments = (Map.fromAscList js)})
|
return (cm,cmi{jments = (Map.fromAscList js)})
|
||||||
|
|
||||||
addPMCFG opts gr (id,CncFun mty@(Just (cat,ctxt,val)) mlin@(Just (L loc term)) mprn Nothing) = do
|
addPMCFG opts cwd gr cmi (id,CncFun mty@(Just (cat,ctxt,val)) mlin@(Just (L loc term)) mprn Nothing) =
|
||||||
|
checkInModule cwd cmi loc ("Happened in the PMCFG generation for" <+> id) $ do
|
||||||
lins <- pmcfgForm gr (L loc id) term ctxt
|
lins <- pmcfgForm gr (L loc id) term ctxt
|
||||||
return (id,CncFun mty mlin mprn (Just (PMCFG lins)))
|
return (id,CncFun mty mlin mprn (Just (PMCFG lins)))
|
||||||
addPMCFG opts gr id_info = return id_info
|
addPMCFG opts cwd gr cmi id_info = return id_info
|
||||||
|
|
||||||
pmcfgForm :: Grammar -> L Ident -> Term -> Context -> Check [[[Symbol]]]
|
pmcfgForm :: Grammar -> L Ident -> Term -> Context -> Check [[[Symbol]]]
|
||||||
pmcfgForm gr _ t ctxt =
|
pmcfgForm gr _ t ctxt =
|
||||||
@@ -57,10 +60,23 @@ type2metaValue d r (Table p q) = do
|
|||||||
(r,vs) <- mapAccumM (\r _ -> type2metaValue d r q) r ts
|
(r,vs) <- mapAccumM (\r _ -> type2metaValue d r q) r ts
|
||||||
tnk <- newEvaluatedThunk (VV p vs)
|
tnk <- newEvaluatedThunk (VV p vs)
|
||||||
return (r, tnk)
|
return (r, tnk)
|
||||||
type2metaValue d r (QC q) = do
|
type2metaValue d r ty@(QC q) = do
|
||||||
tnk <- newMeta 0
|
tnk <- newMeta (Just ty) 0
|
||||||
return (r, tnk)
|
return (r, tnk)
|
||||||
|
|
||||||
|
value2pmcfg (VSusp tnk env vs k) lins = do
|
||||||
|
st <- getMeta tnk
|
||||||
|
case st of
|
||||||
|
Evaluated v -> do v <- apply v vs
|
||||||
|
value2pmcfg v lins
|
||||||
|
Unbound (Just (QC q)) _ -> do (m,ps) <- lookupParams q
|
||||||
|
msum [bind tnk m p | p <- ps]
|
||||||
|
v <- k tnk
|
||||||
|
value2pmcfg v lins
|
||||||
|
where
|
||||||
|
bind tnk m (p, ctxt) = do
|
||||||
|
tnks <- mapM (\(_,_,ty) -> newMeta (Just ty) 0) ctxt
|
||||||
|
setMeta tnk (Evaluated (VApp (m,p) tnks))
|
||||||
value2pmcfg (VR as) lins = do
|
value2pmcfg (VR as) lins = do
|
||||||
(lins,as) <- collectFields lins as
|
(lins,as) <- collectFields lins as
|
||||||
return (lins,VR as)
|
return (lins,VR as)
|
||||||
@@ -76,16 +92,16 @@ value2pmcfg (VR as) lins = do
|
|||||||
tnk <- newEvaluatedThunk v
|
tnk <- newEvaluatedThunk v
|
||||||
return (lins,(lbl,tnk):as)
|
return (lins,(lbl,tnk):as)
|
||||||
value2pmcfg v lins = do
|
value2pmcfg v lins = do
|
||||||
lin <- value2lin v
|
case value2lin v of
|
||||||
return (lin:lins,VR [])
|
Just lin -> return (lin:lins,VR [])
|
||||||
|
Nothing -> do t <- value2term 0 v
|
||||||
value2lin (VStr s) =
|
evalError ("the term" <+> ppTerm Unqualified 0 t $$
|
||||||
return [SymKS s]
|
"cannot be evaluated at compile time.")
|
||||||
value2lin (VC vs) =
|
|
||||||
fmap concat (mapM value2lin vs)
|
|
||||||
value2lin (VSymCat d r) =
|
|
||||||
return [SymCat d r]
|
|
||||||
|
|
||||||
|
value2lin (VStr s) = Just [SymKS s]
|
||||||
|
value2lin (VSymCat d r) = Just [SymCat d r]
|
||||||
|
value2lin (VC vs) = fmap concat (mapM value2lin vs)
|
||||||
|
value2lin _ = Nothing
|
||||||
|
|
||||||
mapAccumM f a [] = return (a,[])
|
mapAccumM f a [] = return (a,[])
|
||||||
mapAccumM f a (x:xs) = do (a, y) <- f a x
|
mapAccumM f a (x:xs) = do (a, y) <- f a x
|
||||||
|
|||||||
@@ -94,13 +94,13 @@ concrete2canonical gr absname cnc modinfo = do
|
|||||||
toCanonical gr absname (name,jment) =
|
toCanonical gr absname (name,jment) =
|
||||||
case jment of
|
case jment of
|
||||||
CncCat (Just (L loc typ)) _ _ pprn _ -> do
|
CncCat (Just (L loc typ)) _ _ pprn _ -> do
|
||||||
ntyp <- normalForm gr (L loc name) typ
|
ntyp <- normalForm gr typ
|
||||||
let pts = paramTypes gr ntyp
|
let pts = paramTypes gr ntyp
|
||||||
return [(pts,Left (LincatDef (gId name) (convType ntyp)))]
|
return [(pts,Left (LincatDef (gId name) (convType ntyp)))]
|
||||||
CncFun (Just r@(cat,ctx,lincat)) (Just (L loc def)) pprn _ -> do
|
CncFun (Just r@(cat,ctx,lincat)) (Just (L loc def)) pprn _ -> do
|
||||||
let params = [(b,x)|(b,x,_)<-ctx]
|
let params = [(b,x)|(b,x,_)<-ctx]
|
||||||
args = map snd params
|
args = map snd params
|
||||||
e0 <- normalForm gr (L loc name) (mkAbs params (mkApp def (map Vr args)))
|
e0 <- normalForm gr (mkAbs params (mkApp def (map Vr args)))
|
||||||
let e = cleanupRecordFields lincat (unAbs (length params) e0)
|
let e = cleanupRecordFields lincat (unAbs (length params) e0)
|
||||||
tts = tableTypes gr [e]
|
tts = tableTypes gr [e]
|
||||||
return [(tts,Right (LinDef (gId name) (map gId args) (convert gr e)))]
|
return [(tts,Right (LinDef (gId name) (map gId args) (convert gr e)))]
|
||||||
|
|||||||
@@ -107,7 +107,7 @@ compileSourceModule opts cwd mb_gfFile gr =
|
|||||||
-- Apply to complete modules when not generating tags
|
-- Apply to complete modules when not generating tags
|
||||||
backend mo3 =
|
backend mo3 =
|
||||||
do if isModCnc (snd mo3) && flag optPMCFG opts
|
do if isModCnc (snd mo3) && flag optPMCFG opts
|
||||||
then runPassI "generating PMCFG" $ fmap fst $ runCheck' opts (generatePMCFG opts gr mo3)
|
then runPassI "generating PMCFG" $ fmap fst $ runCheck' opts (generatePMCFG opts cwd gr mo3)
|
||||||
else runPassI "" $ return mo3
|
else runPassI "" $ return mo3
|
||||||
|
|
||||||
ifComplete yes mo@(_,mi) =
|
ifComplete yes mo@(_,mi) =
|
||||||
|
|||||||
@@ -446,7 +446,7 @@ data Label =
|
|||||||
|
|
||||||
type MetaId = Int
|
type MetaId = Int
|
||||||
|
|
||||||
type Hypo = (BindType,Ident,Term) -- (x:A) (_:A) A ({x}:A)
|
type Hypo = (BindType,Ident,Type) -- (x:A) (_:A) A ({x}:A)
|
||||||
type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
|
type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
|
||||||
type Equation = ([Patt],Term)
|
type Equation = ([Patt],Term)
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user