mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-05-03 16:22:52 -06:00
done with partial evaluation for records and variants
This commit is contained in:
@@ -3,21 +3,20 @@
|
||||
-- | Functions for computing the values of terms in the concrete syntax, in
|
||||
-- | preparation for PMCFG generation.
|
||||
module GF.Compile.Compute.Concrete
|
||||
(GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
|
||||
normalForm,
|
||||
(normalForm,
|
||||
Value(..), Env, value2term, eval
|
||||
) where
|
||||
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
|
||||
|
||||
import GF.Grammar hiding (Env, VGen, VApp, VRecType)
|
||||
import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
|
||||
import GF.Grammar.Lookup(lookupResDef,allParamValues)
|
||||
import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
|
||||
import GF.Grammar.PatternMatch(matchPattern,measurePatt)
|
||||
import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
|
||||
import GF.Compile.Compute.Value hiding (Error)
|
||||
import GF.Compile.Compute.Predef(predef,predefName,delta)
|
||||
import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
|
||||
import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
|
||||
import GF.Data.Operations(Err(..),err,errIn,maybeErr,mapPairsM)
|
||||
import GF.Data.Utilities(mapFst,mapSnd)
|
||||
import GF.Infra.Option
|
||||
import Data.STRef
|
||||
@@ -28,9 +27,9 @@ import qualified Data.Map as Map
|
||||
|
||||
-- * Main entry points
|
||||
|
||||
normalForm :: GlobalEnv -> L Ident -> Term -> Term
|
||||
normalForm ge loc t =
|
||||
case runEvalM (eval [] t [] >>= value2term 0) of
|
||||
normalForm :: Grammar -> L Ident -> Term -> Term
|
||||
normalForm gr loc t =
|
||||
case runEvalM gr (eval [] t [] >>= value2term 0) of
|
||||
[t] -> t
|
||||
ts -> FV ts
|
||||
|
||||
@@ -39,6 +38,7 @@ eval env (Vr x) vs = case lookup x env of
|
||||
Nothing -> error "Unknown variable"
|
||||
eval env (Con f) vs = return (VApp f vs)
|
||||
eval env (K t) vs = return (VStr t)
|
||||
eval env Empty vs = return (VC [])
|
||||
eval env (App t1 t2) vs = do tnk <- newThunk env t2
|
||||
eval env t1 (tnk : vs)
|
||||
eval env (Abs b x t) [] = return (VClosure env (Abs b x t))
|
||||
@@ -46,10 +46,27 @@ eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
|
||||
eval env (Meta i) vs = do tnk <- newMeta i
|
||||
return (VMeta tnk env vs)
|
||||
eval env (Typed t ty) vs = eval env t vs
|
||||
eval env (C t1 t2) vs = do tnk1 <- newThunk env t1
|
||||
tnk2 <- newThunk env t2
|
||||
return (VC tnk1 tnk2)
|
||||
eval env (R as) vs = do as <- mapM (\(lbl,(_,t)) -> fmap ((,) lbl) (newThunk env t)) as
|
||||
return (VR as)
|
||||
eval env (P t lbl) vs = do v <- eval env t []
|
||||
case v of
|
||||
VR as -> case lookup lbl as of
|
||||
Nothing -> error ("Missing value for label "++show lbl)
|
||||
Just tnk -> force tnk vs
|
||||
v -> return (VP v lbl)
|
||||
eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
|
||||
eval ((x,tnk):env) t2 vs
|
||||
eval env (Q q) vs = do t <- lookupGlobal q
|
||||
eval env t vs
|
||||
eval env (C t1 t2) vs = do v1 <- eval env t1 vs
|
||||
v2 <- eval env t2 vs
|
||||
case (v1,v2) of
|
||||
(VC vs1,VC vs2) -> return (VC (vs1++vs2))
|
||||
(VC vs1,v2 ) -> return (VC (vs1++[v2]))
|
||||
(v1, VC vs2) -> return (VC ([v1]++vs2))
|
||||
(v1, v2 ) -> return (VC [v1,v2])
|
||||
eval env (FV ts) vs = msum [eval env t vs | t <- ts]
|
||||
eval env t vs = error (show t)
|
||||
|
||||
apply v [] = return v
|
||||
apply (VApp f vs0) vs = return (VApp f (vs0++vs))
|
||||
@@ -72,62 +89,60 @@ value2term i (VClosure env (Abs b x t)) = do
|
||||
v <- eval ((x,tnk):env) t []
|
||||
t <- value2term (i+1) v
|
||||
return (Abs b (identS ('v':show i)) t)
|
||||
value2term i (VR as) = do
|
||||
as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (force tnk [] >>= value2term i)) as
|
||||
return (R as)
|
||||
value2term i (VP v lbl) = do
|
||||
t <- value2term i v
|
||||
return (P t lbl)
|
||||
value2term i (VStr tok) = return (K tok)
|
||||
value2term i (VC tnk1 tnk2) = do
|
||||
t1 <- force tnk1 [] >>= value2term i
|
||||
t2 <- force tnk2 [] >>= value2term i
|
||||
return (C t1 t2)
|
||||
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- * Environments
|
||||
|
||||
data GlobalEnv = GE Grammar Options GLocation
|
||||
type GLocation = L Ident
|
||||
|
||||
geLoc (GE _ _ loc) = loc
|
||||
geGrammar (GE gr _ _ ) = gr
|
||||
|
||||
-- | Convert operators once, not every time they are looked up
|
||||
resourceValues :: Options -> SourceGrammar -> GlobalEnv
|
||||
resourceValues opts gr = GE gr opts (L NoLoc identW)
|
||||
|
||||
value2term i (VC vs) = do
|
||||
ts <- mapM (value2term i) vs
|
||||
case ts of
|
||||
[] -> return Empty
|
||||
(t:ts) -> return (foldl C t ts)
|
||||
|
||||
-----------------------------------------------------------------------
|
||||
-- * Evaluation monad
|
||||
|
||||
type MetaThunks s = Map.Map MetaId (Thunk s)
|
||||
|
||||
newtype EvalM s a = EvalM (forall r . (a -> MetaThunks s -> r -> ST s r) -> MetaThunks s -> r -> ST s r)
|
||||
newtype EvalM s a = EvalM (forall r . Grammar -> (a -> MetaThunks s -> r -> ST s r) -> MetaThunks s -> r -> ST s r)
|
||||
|
||||
instance Functor (EvalM s) where
|
||||
fmap f (EvalM g) = EvalM (\k -> g (k . f))
|
||||
fmap f (EvalM g) = EvalM (\gr k -> g gr (k . f))
|
||||
|
||||
instance Applicative (EvalM s) where
|
||||
pure x = EvalM (\k -> k x)
|
||||
(EvalM f) <*> (EvalM x) = EvalM (\k -> f (\f -> x (\x -> k (f x))))
|
||||
pure x = EvalM (\gr k -> k x)
|
||||
(EvalM f) <*> (EvalM x) = EvalM (\gr k -> f gr (\f -> x gr (\x -> k (f x))))
|
||||
|
||||
instance Monad (EvalM s) where
|
||||
(EvalM f) >>= g = EvalM (\k -> f (\x -> case g x of
|
||||
EvalM g -> g k))
|
||||
(EvalM f) >>= g = EvalM (\gr k -> f gr (\x -> case g x of
|
||||
EvalM g -> g gr k))
|
||||
|
||||
instance Alternative (EvalM s) where
|
||||
empty = EvalM (\k _ -> return)
|
||||
(EvalM f) <|> (EvalM g) = EvalM (\k mt r -> f k mt r >>= \r -> g k mt r)
|
||||
empty = EvalM (\gr k _ -> return)
|
||||
(EvalM f) <|> (EvalM g) = EvalM (\gr k mt r -> f gr k mt r >>= \r -> g gr k mt r)
|
||||
|
||||
instance MonadPlus (EvalM s) where
|
||||
|
||||
|
||||
runEvalM :: (forall s . EvalM s a) -> [a]
|
||||
runEvalM f = reverse $
|
||||
runST (case f of
|
||||
EvalM f -> f (\x mt xs -> return (x:xs)) Map.empty [])
|
||||
runEvalM :: Grammar -> (forall s . EvalM s a) -> [a]
|
||||
runEvalM gr f = reverse $
|
||||
runST (case f of
|
||||
EvalM f -> f gr (\x mt xs -> return (x:xs)) Map.empty [])
|
||||
|
||||
newThunk env t = EvalM $ \k mt r -> do
|
||||
lookupGlobal :: QIdent -> EvalM s Term
|
||||
lookupGlobal q = EvalM $ \gr k mt r -> do
|
||||
case lookupResDef gr q of
|
||||
Ok t -> k t mt r
|
||||
Bad msg -> error msg
|
||||
|
||||
newThunk env t = EvalM $ \gr k mt r -> do
|
||||
tnk <- newSTRef (Unevaluated env t)
|
||||
k tnk mt r
|
||||
|
||||
newMeta i = EvalM $ \k mt r ->
|
||||
newMeta i = EvalM $ \gr k mt r ->
|
||||
if i == 0
|
||||
then do tnk <- newSTRef (Unbound i)
|
||||
k tnk mt r
|
||||
@@ -136,24 +151,24 @@ newMeta i = EvalM $ \k mt r ->
|
||||
Nothing -> do tnk <- newSTRef (Unbound i)
|
||||
k tnk (Map.insert i tnk mt) r
|
||||
|
||||
newGen i = EvalM $ \k mt r -> do
|
||||
newGen i = EvalM $ \gr k mt r -> do
|
||||
tnk <- newSTRef (Evaluated (VGen i []))
|
||||
k tnk mt r
|
||||
|
||||
force tnk vs = EvalM $ \k mt r -> do
|
||||
force tnk vs = EvalM $ \gr k mt r -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Unevaluated env t -> case eval env t vs of
|
||||
EvalM f -> f (\v mt r -> do writeSTRef tnk (Evaluated v)
|
||||
r <- k v mt r
|
||||
writeSTRef tnk s
|
||||
return r) mt r
|
||||
EvalM f -> f gr (\v mt r -> do writeSTRef tnk (Evaluated v)
|
||||
r <- k v mt r
|
||||
writeSTRef tnk s
|
||||
return r) mt r
|
||||
Evaluated v -> case apply v vs of
|
||||
EvalM f -> f k mt r
|
||||
EvalM f -> f gr k mt r
|
||||
|
||||
zonk tnk vs = EvalM $ \k mt r -> do
|
||||
zonk tnk vs = EvalM $ \gr k mt r -> do
|
||||
s <- readSTRef tnk
|
||||
case s of
|
||||
Evaluated v -> case apply v vs of
|
||||
EvalM f -> f (k . Left) mt r
|
||||
EvalM f -> f gr (k . Left) mt r
|
||||
Unbound i -> k (Right i) mt r
|
||||
|
||||
Reference in New Issue
Block a user