we can finally compile the English RGL

This commit is contained in:
krangelov
2021-10-20 19:39:02 +02:00
parent ad3489f0f9
commit b6047463a9
5 changed files with 254 additions and 146 deletions

View File

@@ -202,7 +202,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
(Just (_,cat,cont,val),Just (L loc trm)) -> (Just (_,cat,cont,val),Just (L loc trm)) ->
chIn loc "linearization of" $ do chIn loc "linearization of" $ do
(trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
return (Just (L loc trm)) return (Just (L loc (etaExpand [] trm cont)))
_ -> return mt _ -> return mt
mpr <- case mpr of mpr <- case mpr of
(Just (L loc t)) -> (Just (L loc t)) ->
@@ -281,7 +281,19 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
t' <- compAbsTyp ((x,Vr x):g) t t' <- compAbsTyp ((x,Vr x):g) t
return $ Prod b x a' t' return $ Prod b x a' t'
Abs _ _ _ -> return t Abs _ _ _ -> return t
_ -> composOp (compAbsTyp g) t _ -> composOp (compAbsTyp g) t
etaExpand xs t [] = t
etaExpand xs (Abs bt x t) (_ :cont) = Abs bt x (etaExpand (x:xs) t cont)
etaExpand xs t ((bt,_,ty):cont) = Abs bt x (etaExpand (x:xs) (App t (Vr x)) cont)
where
x = freeVar 1 xs
freeVar i xs
| elem x xs = freeVar (i+1) xs
| otherwise = x
where
x = identS ("v"++show i)
update (mn,mi) c info = return (mn,mi{jments=Map.insert c info (jments mi)}) update (mn,mi) c info = return (mn,mi{jments=Map.insert c info (jments mi)})

View File

@@ -4,11 +4,12 @@
-- | preparation for PMCFG generation. -- | preparation for PMCFG generation.
module GF.Compile.Compute.Concrete module GF.Compile.Compute.Concrete
( normalForm ( normalForm
, Value(..), Thunk, ThunkState(..), Env , Value(..), Thunk, ThunkState(..), Env, showValue
, EvalM, runEvalM, evalError , EvalM, runEvalM, evalError
, eval, apply, force, value2term, patternMatch , eval, apply, force, value2term, patternMatch
, newMeta,getMeta,setMeta , newThunk, newEvaluatedThunk
, newThunk,newEvaluatedThunk , newResiduation, newNarrowing
, getRef
, getResDef, getInfo, getAllParamValues , getResDef, getInfo, getAllParamValues
) where ) where
@@ -30,7 +31,7 @@ import Data.List
import Data.Char import Data.Char
import Control.Monad import Control.Monad
import Control.Monad.ST import Control.Monad.ST
import Control.Applicative import Control.Applicative hiding (Const)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail
import qualified Data.Map as Map import qualified Data.Map as Map
import GF.Text.Pretty import GF.Text.Pretty
@@ -49,7 +50,8 @@ normalForm gr t =
data ThunkState s data ThunkState s
= Unevaluated (Env s) Term = Unevaluated (Env s) Term
| Evaluated (Value s) | Evaluated (Value s)
| Unbound (Maybe Type) {-# UNPACK #-} !MetaId | Residuation {-# UNPACK #-} !MetaId
| Narrowing {-# UNPACK #-} !MetaId Type
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)]
@@ -57,7 +59,7 @@ type Env s = [(Ident,Thunk s)]
data Value s data Value s
= VApp QIdent [Thunk s] = VApp QIdent [Thunk s]
| VMeta (Thunk s) (Env s) [Thunk s] | VMeta (Thunk s) (Env s) [Thunk s]
| VSusp (Thunk s) (Env s) [Thunk s] (Thunk s -> EvalM s (Value s)) | VSusp (Thunk s) (Env s) (Value s -> EvalM s (Value s)) [Thunk s]
| VGen {-# UNPACK #-} !Int [Thunk s] | VGen {-# UNPACK #-} !Int [Thunk s]
| VClosure (Env s) Term | VClosure (Env s) Term
| VProd BindType Ident (Value s) (Env s) Term | VProd BindType Ident (Value s) (Env s) Term
@@ -66,8 +68,8 @@ data Value s
| VP (Value s) Label [Thunk s] | VP (Value s) Label [Thunk s]
| VExtR (Value s) (Value s) | VExtR (Value s) (Value s)
| VTable (Value s) (Value s) | VTable (Value s) (Value s)
| VT TInfo (Env s) [Case] | VT (Value s) (Env s) [Case]
| VV Type [Thunk s] | VV (Value s) [Thunk s]
| VS (Value s) (Thunk s) [Thunk s] | VS (Value s) (Thunk s) [Thunk s]
| VSort Ident | VSort Ident
| VInt Integer | VInt Integer
@@ -84,8 +86,35 @@ data Value s
| VSymCat Int LIndex [(LIndex, Thunk s)] | VSymCat Int LIndex [(LIndex, Thunk s)]
showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
showValue (VMeta _ _ _) = "VMeta"
showValue (VSusp _ _ _ _) = "VSusp"
showValue (VGen _ _) = "VGen"
showValue (VClosure _ _) = "VClosure"
showValue (VProd _ _ _ _ _) = "VProd"
showValue (VRecType _) = "VRecType"
showValue (VR lbls) = "(VR {"++unwords (map (\(lbl,_) -> show lbl) lbls)++"})"
showValue (VP v l _) = "(VP "++showValue v++" "++show l++")"
showValue (VExtR _ _) = "VExtR"
showValue (VTable _ _) = "VTable"
showValue (VT _ _ cs) = "(VT "++show cs++")"
showValue (VV _ _) = "VV"
showValue (VS v _ _) = "(VS "++showValue v++")"
showValue (VSort _) = "VSort"
showValue (VInt _) = "VInt"
showValue (VFlt _) = "VFlt"
showValue (VStr _) = "VStr"
showValue (VC _) = "VC"
showValue (VGlue _ _) = "VGlue"
showValue (VPatt _ _ _) = "VPatt"
showValue (VPattType _) = "VPattType"
showValue (VAlts _ _) = "VAlts"
showValue (VStrs _) = "VStrs"
showValue (VSymCat _ _ _) = "VSymCat"
eval env (Vr x) vs = case lookup x env of eval env (Vr x) vs = case lookup x env of
Just tnk -> force tnk vs Just tnk -> do v <- force tnk
apply v vs
Nothing -> evalError ("Variable" <+> pp x <+> "is not in scope") Nothing -> evalError ("Variable" <+> pp x <+> "is not in scope")
eval env (Sort s) [] = return (VSort s) eval env (Sort s) [] = return (VSort s)
eval env (EInt n) [] = return (VInt n) eval env (EInt n) [] = return (VInt n)
@@ -96,7 +125,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 Nothing i eval env (Meta i) vs = do tnk <- newResiduation 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 []
@@ -110,8 +139,9 @@ eval env (P t lbl) vs = do v <- eval env t []
case v of case v of
VR as -> case lookup lbl as of VR as -> case lookup lbl as of
Nothing -> evalError ("Missing value for label" <+> pp lbl $$ Nothing -> evalError ("Missing value for label" <+> pp lbl $$
"in record" <+> pp t) "in" <+> pp (P t lbl))
Just tnk -> force tnk vs Just tnk -> do v <- force tnk
apply v vs
v -> return (VP v lbl vs) v -> return (VP v lbl vs)
eval env (ExtR t1 t2) [] = do v1 <- eval env t1 [] eval env (ExtR t1 t2) [] = do v1 <- eval env t1 []
v2 <- eval env t2 [] v2 <- eval env t2 []
@@ -122,28 +152,33 @@ eval env (ExtR t1 t2) [] = do v1 <- eval env t1 []
eval env (Table t1 t2) [] = do v1 <- eval env t1 [] eval env (Table t1 t2) [] = do v1 <- eval env t1 []
v2 <- eval env t2 [] v2 <- eval env t2 []
return (VTable v1 v2) return (VTable v1 v2)
eval env (T i cs) [] = return (VT i env cs) eval env (T (TTyped ty) cs)[]=do vty <- eval env ty []
eval env (V ty ts) [] = do tnks <- mapM (newThunk env) ts return (VT vty env cs)
return (VV ty tnks) eval env (V ty ts) [] = do vty <- eval env ty []
tnks <- mapM (newThunk env) ts
return (VV vty tnks)
eval env t@(S t1 t2) vs = do v1 <- eval env t1 [] eval env t@(S t1 t2) vs = do v1 <- eval env t1 []
tnk2 <- newThunk env t2 tnk2 <- newThunk env t2
let v0 = VS v1 tnk2 vs let v0 = VS v1 tnk2 vs
case v1 of case v1 of
VT _ env cs -> patternMatch v0 (map (\(p,t) -> (env,[p],tnk2:vs,t)) cs) VT _ env cs -> patternMatch v0 (map (\(p,t) -> (env,[p],tnk2:vs,t)) cs)
VV ty tnks -> do t2 <- force tnk2 [] >>= value2term (length env) VV vty tnks -> do t2 <- force tnk2 >>= value2term (length env)
ty <- value2term (length env) vty
ts <- getAllParamValues ty ts <- getAllParamValues ty
case lookup t2 (zip ts tnks) of case lookup t2 (zip ts tnks) of
Just tnk -> force tnk vs Just tnk -> do v <- force tnk
apply v vs
Nothing -> return v0 Nothing -> return v0
v1 -> return v0 v1 -> return v0
eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1 eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
eval ((x,tnk):env) t2 vs eval ((x,tnk):env) t2 vs
eval env (Q q@(m,id)) vs eval env (Q q@(m,id)) vs
| m == cPredef = do vs' <- mapM (flip force []) vs | m == cPredef = do vs' <- mapM force vs
mb_res <- evalPredef id vs' mb_res <- evalPredef id vs'
case mb_res of case mb_res of
Just res -> return res Const res -> return res
Nothing -> return (VApp q vs) RunTime -> return (VApp q vs)
NonExist -> return (VApp (cPredef,cNonExist) vs)
| otherwise = do t <- getResDef q | otherwise = do t <- getResDef q
eval env t vs eval env t vs
eval env (QC q) vs = return (VApp q vs) eval env (QC q) vs = return (VApp q vs)
@@ -156,9 +191,10 @@ eval env (C t1 t2) [] = do v1 <- eval env t1 []
(v1, v2 ) -> return (VC [v1,v2]) (v1, v2 ) -> return (VC [v1,v2])
eval env t@(Glue t1 t2) [] = do v1 <- eval env t1 [] eval env t@(Glue t1 t2) [] = do v1 <- eval env t1 []
v2 <- eval env t2 [] v2 <- eval env t2 []
case liftM2 (++) (value2string v1) (value2string v2) of case liftA2 (++) (value2string v1) (value2string v2) of
Just s -> return (string2value s) Const s -> return (string2value s)
Nothing -> return (VGlue v1 v2) RunTime -> return (VGlue v1 v2)
NonExist -> return (VApp (cPredef,cNonExist) [])
eval env (EPatt min max p) [] = return (VPatt min max p) eval env (EPatt min max p) [] = return (VPatt min max p)
eval env (EPattType t) [] = do v <- eval env t [] eval env (EPattType t) [] = do v <- eval env t []
return (VPattType v) return (VPattType v)
@@ -190,52 +226,52 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,pv) ->
return (VSymCat d r rs) return (VSymCat d r rs)
eval env t vs = evalError ("Cannot reduce term" <+> pp t) eval env t vs = evalError ("Cannot reduce term" <+> pp t)
apply (VMeta m env vs0) vs = do st <- getMeta m apply (VMeta m env vs0) vs = return (VMeta m env (vs0++vs))
case st of apply (VSusp m env k vs0) vs = return (VSusp m env k (vs0++vs))
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 (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 apply v [] = return v
evalPredef id [v] evalPredef id [v]
| id == cLength = return (fmap VInt (liftM genericLength (value2string v))) | id == cLength = case value2string v of
Const s -> return (Const (VInt (genericLength s)))
_ -> return RunTime
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cTake = return (fmap string2value (liftM2 genericTake (value2int v1) (value2string v2))) | id == cTake = return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cDrop = return (fmap string2value (liftM2 genericDrop (value2int v1) (value2string v2))) | id == cDrop = return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cTk = return (fmap string2value (liftM2 genericTk (value2int v1) (value2string v2))) | id == cTk = return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2)))
where where
genericTk n = reverse . genericTake n . reverse genericTk n = reverse . genericTake n . reverse
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cDp = return (fmap string2value (liftM2 genericDp (value2int v1) (value2string v2))) | id == cDp = return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2)))
where where
genericDp n = reverse . genericDrop n . reverse genericDp n = reverse . genericDrop n . reverse
evalPredef id [v] evalPredef id [v]
| id == cIsUpper= return (fmap toPBool (liftM (all isUpper) (value2string v))) | id == cIsUpper= return (fmap toPBool (liftA (all isUpper) (value2string v)))
evalPredef id [v] evalPredef id [v]
| id == cToUpper= return (fmap string2value (liftM (map toUpper) (value2string v))) | id == cToUpper= return (fmap string2value (liftA (map toUpper) (value2string v)))
evalPredef id [v] evalPredef id [v]
| id == cToLower= return (fmap string2value (liftM (map toLower) (value2string v))) | id == cToLower= return (fmap string2value (liftA (map toLower) (value2string v)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cEqStr = return (fmap toPBool (liftM2 (==) (value2string v1) (value2string v2))) | id == cEqStr = return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cOccur = return (fmap toPBool (liftM2 occur (value2string v1) (value2string v2))) | id == cOccur = return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cOccurs = return (fmap toPBool (liftM2 occurs (value2string v1) (value2string v2))) | id == cOccurs = return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cEqInt = return (fmap toPBool (liftM2 (==) (value2int v1) (value2int v2))) | id == cEqInt = return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cLessInt= return (fmap toPBool (liftM2 (<) (value2int v1) (value2int v2))) | id == cLessInt= return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2)))
evalPredef id [v1,v2] evalPredef id [v1,v2]
| id == cPlus = return (fmap VInt (liftM2 (+) (value2int v1) (value2int v2))) | id == cPlus = return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2)))
evalPredef id [v] evalPredef id [v]
| id == cError = case value2string v of | id == cError = case value2string v of
Just msg -> fail msg Const msg -> fail msg
Nothing -> return Nothing _ -> fail "Indescribable error appeared"
evalPredef id vs = return Nothing evalPredef id vs = return RunTime
toPBool True = VApp (cPredef,cPTrue) [] toPBool True = VApp (cPredef,cPTrue) []
toPBool False = VApp (cPredef,cPFalse) [] toPBool False = VApp (cPredef,cPFalse) []
@@ -273,11 +309,14 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
match env (PW :ps) eqs (arg:args) = match env ps eqs args match env (PW :ps) eqs (arg:args) = match env ps eqs args
match env (PTilde _ :ps) eqs (arg:args) = match env ps eqs args match env (PTilde _ :ps) eqs (arg:args) = match env ps eqs args
match env (p :ps) eqs (arg:args) = do match env (p :ps) eqs (arg:args) = do
v <- force arg [] v <- force arg
match' env p ps eqs arg v args
match' env p ps eqs arg v args = do
case (p,v) of case (p,v) of
(p, VMeta i envi vs ) -> return (VSusp i envi vs (\tnk -> match env (p:ps) eqs (tnk:args))) (p, VMeta i envi vs) -> susp i envi (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args) []
(p, VGen i vs ) -> return v0 (p, VGen i vs ) -> return v0
(p, VSusp i envi vs k) -> return (VSusp i envi vs (\tnk -> match env (p:ps) eqs (tnk:args))) (p, VSusp i envi k vs) -> susp i envi (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args) []
(PP q qs, VApp r tnks) (PP q qs, VApp r tnks)
| q == r -> match env (qs++ps) eqs (tnks++args) | q == r -> match env (qs++ps) eqs (tnks++args)
(PR pas, VR as) -> matchRec env pas as ps eqs args (PR pas, VR as) -> matchRec env pas as ps eqs args
@@ -287,19 +326,21 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
| null s1 -> match env ps eqs args | null s1 -> match env ps eqs args
(PSeq min1 max1 p1 min2 max2 p2,v) (PSeq min1 max1 p1 min2 max2 p2,v)
-> case value2string v of -> case value2string v of
Just s -> do let n = length s Const s -> do let n = length s
lo = min1 `max` (n-fromMaybe n max2) lo = min1 `max` (n-fromMaybe n max2)
hi = (n-min2) `min` fromMaybe n max1 hi = (n-min2) `min` fromMaybe n max1
(ds,cs) = splitAt lo s (ds,cs) = splitAt lo s
eqs <- matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args eqs <- matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args
patternMatch v0 eqs patternMatch v0 eqs
Nothing -> return v0 RunTime -> return v0
NonExist-> patternMatch v0 eqs
(PRep minp maxp p, v) (PRep minp maxp p, v)
-> case value2string v of -> case value2string v of
Just s -> do let n = length s `div` (max minp 1) Const s -> do let n = length s `div` (max minp 1)
eqs <- matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args) eqs <- matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args)
patternMatch v0 eqs patternMatch v0 eqs
Nothing -> return v0 RunTime -> return v0
NonExist-> patternMatch v0 eqs
(PChar, VStr [_]) -> match env ps eqs args (PChar, VStr [_]) -> match env ps eqs args
(PChars cs, VStr [c]) (PChars cs, VStr [c])
| elem c cs -> match env ps eqs args | elem c cs -> match env ps eqs args
@@ -334,21 +375,42 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
matchRep env n minp maxp p minq maxq q ps eqs args = do matchRep env n minp maxp p minq maxq q ps eqs args = do
matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args
susp i env ki vs = EvalM $ \gr k mt r -> do
s <- readSTRef i
case s of
Narrowing id (QC q) -> case lookupOrigInfo gr q of
Ok (m,ResParam (Just (L _ ps)) _) -> bind gr k mt r s m ps
Bad msg -> return (Fail (pp msg))
Evaluated v -> case ki v of
EvalM f -> f gr k mt r
_ -> k (VSusp i env ki vs) mt r
where
bind gr k mt r s m [] = return (Success r)
bind gr k mt r s m ((p, ctxt):ps) = do
tnks <- mapM (\(_,_,ty) -> newSTRef (Narrowing 0 ty)) ctxt
let v = VApp (m,p) tnks
writeSTRef i (Evaluated v)
res <- case ki v of
EvalM f -> f gr k mt r
writeSTRef i s
case res of
Fail msg -> return (Fail msg)
Success r -> bind gr k mt r s m ps
value2term i (VApp q tnks) = value2term i (VApp q tnks) =
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (QC q) tnks foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (QC q) tnks
value2term i (VMeta m env tnks) = do value2term i (VMeta m env tnks) = do
res <- zonk m tnks res <- zonk m tnks
case res of case res of
Right i -> foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Meta i) tnks Right i -> foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (Meta i) tnks
Left v -> value2term i v Left v -> value2term i v
value2term i (VSusp j env vs k) = do value2term i (VSusp j env k vs) = do
tnk <- newEvaluatedThunk (VGen maxBound vs) v <- k (VGen maxBound vs)
v <- k tnk
value2term i v value2term i v
value2term i (VGen j tnks) = value2term i (VGen j tnks) =
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (Vr (identS ('v':show j))) tnks foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (Vr (identS ('v':show j))) tnks
value2term i (VClosure env (Abs b x t)) = do value2term i (VClosure env (Abs b x t)) = do
tnk <- newGen i tnk <- newEvaluatedThunk (VGen i [])
v <- eval ((x,tnk):env) t [] v <- eval ((x,tnk):env) t []
t <- value2term (i+1) v t <- value2term (i+1) v
return (Abs b (identS ('v':show i)) t) return (Abs b (identS ('v':show i)) t)
@@ -358,7 +420,7 @@ value2term i (VProd b x v1 env t2)
t2 <- value2term i v2 t2 <- value2term i v2
return (Prod b x t1 t2) return (Prod b x t1 t2)
| otherwise = do t1 <- value2term i v1 | otherwise = do t1 <- value2term i v1
tnk <- newGen i tnk <- newEvaluatedThunk (VGen i [])
v2 <- eval ((x,tnk):env) t2 [] v2 <- eval ((x,tnk):env) t2 []
t2 <- value2term (i+1) v2 t2 <- value2term (i+1) v2
return (Prod b (identS ('v':show i)) t1 t2) return (Prod b (identS ('v':show i)) t1 t2)
@@ -366,11 +428,11 @@ value2term i (VRecType lbls) = do
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term i v)) lbls lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term i v)) lbls
return (RecType lbls) return (RecType lbls)
value2term i (VR as) = do value2term i (VR as) = do
as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (force tnk [] >>= value2term i)) as as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (force tnk >>= value2term i)) as
return (R as) return (R as)
value2term i (VP v lbl tnks) = do value2term i (VP v lbl tnks) = do
t <- value2term i v t <- value2term i v
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (P t lbl) tnks foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (P t lbl) tnks
value2term i (VExtR v1 v2) = do value2term i (VExtR v1 v2) = do
t1 <- value2term i v1 t1 <- value2term i v1
t2 <- value2term i v2 t2 <- value2term i v2
@@ -379,12 +441,14 @@ value2term i (VTable v1 v2) = do
t1 <- value2term i v1 t1 <- value2term i v1
t2 <- value2term i v2 t2 <- value2term i v2
return (Table t1 t2) return (Table t1 t2)
value2term i (VT ti _ cs) = return (T ti cs) value2term i (VT vty _ cs)= do ty <- value2term i vty
value2term i (VV ty tnks) = do ts <- mapM (\tnk -> force tnk [] >>= value2term i) tnks return (T (TTyped ty) cs)
value2term i (VV vty tnks)= do ty <- value2term i vty
ts <- mapM (\tnk -> force tnk >>= value2term i) tnks
return (V ty ts) return (V ty ts)
value2term i (VS v1 tnk2 tnks) = do t1 <- value2term i v1 value2term i (VS v1 tnk2 tnks) = do t1 <- value2term i v1
t2 <- force tnk2 [] >>= value2term i t2 <- force tnk2 >>= value2term i
foldM (\e1 tnk -> fmap (App e1) (force tnk [] >>= value2term i)) (S t1 t2) tnks foldM (\e1 tnk -> fmap (App e1) (force tnk >>= value2term i)) (S t1 t2) tnks
value2term i (VSort s) = return (Sort s) value2term i (VSort s) = return (Sort s)
value2term i (VStr tok) = return (K tok) value2term i (VStr tok) = return (K tok)
value2term i (VInt n) = return (EInt n) value2term i (VInt n) = return (EInt n)
@@ -412,9 +476,49 @@ 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 data ConstValue a
value2string (VC vs) = fmap unwords (mapM value2string vs) = Const a
value2string _ = Nothing | RunTime
| NonExist
instance Functor ConstValue where
fmap f (Const c) = Const (f c)
fmap f RunTime = RunTime
fmap f NonExist = NonExist
instance Applicative ConstValue where
pure = Const
liftA2 f (Const a) (Const b) = Const (f a b)
liftA2 f NonExist _ = NonExist
liftA2 f _ NonExist = NonExist
liftA2 f RunTime _ = RunTime
liftA2 f _ RunTime = RunTime
value2string =
fmap (\(_,_,ws) -> unwords (reverse ws)) .
value2string (Const (False,id,[]))
where
value2string (Const (True,f,(w0:ws))) (VStr w) = Const (False,id,(w0++f w):ws)
value2string (Const (_, f, ws )) (VStr w) = Const (False,id,( f w):ws)
value2string st (VC vs) = foldl value2string st vs
value2string st (VApp q [])
| q == (cPredef,cNonExist) = NonExist
value2string st (VApp q [])
| q == (cPredef,cSOFT_SPACE) = st
value2string (Const (b,f,ws)) (VApp q [])
| q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND) = Const (True,f,ws)
value2string (Const (b,f,ws)) (VApp q [])
| q == (cPredef,cCAPIT) = Const (b,f . capit,ws)
where
capit [] = []
capit (c:cs) = toUpper c : cs
value2string (Const (b,f,ws)) (VApp q [])
| q == (cPredef,cALL_CAPIT) = Const (b,f . all_capit,ws)
where
all_capit = map toUpper
-- value2string (b,f,ws) (VAlts vd vas) =
value2string st _ = st
string2value s = string2value s =
case words s of case words s of
@@ -422,8 +526,8 @@ string2value s =
[w] -> VStr w [w] -> VStr w
ws -> VC (map VStr ws) ws -> VC (map VStr ws)
value2int (VInt n) = Just n value2int (VInt n) = Const n
value2int _ = Nothing value2int _ = RunTime
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- * Evaluation monad -- * Evaluation monad
@@ -496,43 +600,42 @@ 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 mb_ty i = EvalM $ \gr k mt r -> newResiduation i = EvalM $ \gr k mt r ->
if i == 0 if i == 0
then do tnk <- newSTRef (Unbound mb_ty i) then do tnk <- newSTRef (Residuation 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 mb_ty i) Nothing -> do tnk <- newSTRef (Residuation 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 newNarrowing i ty = EvalM $ \gr k mt r ->
if i == 0
then do tnk <- newSTRef (Narrowing i ty)
k tnk mt r
else case Map.lookup i mt of
Just tnk -> k tnk mt r
Nothing -> do tnk <- newSTRef (Narrowing i ty)
k tnk (Map.insert i tnk mt) r
setMeta tnk st = EvalM $ \gr k mt r -> do getRef tnk = EvalM $ \gr k mt r -> readSTRef tnk >>= \st -> k st mt r
old <- readSTRef tnk
writeSTRef tnk st
r <- k () mt r
writeSTRef tnk old
return r
newGen i = EvalM $ \gr k mt r -> do force tnk = EvalM $ \gr k mt r -> do
tnk <- newSTRef (Evaluated (VGen i []))
k tnk mt r
force tnk vs = EvalM $ \gr k mt r -> do
s <- readSTRef tnk s <- readSTRef tnk
case s of case s of
Unevaluated env t -> case eval env t vs of Unevaluated env t -> case eval env t [] of
EvalM f -> f gr (\v mt r -> do writeSTRef tnk (Evaluated v) EvalM f -> f gr (\v mt r -> do writeSTRef tnk (Evaluated v)
r <- k v mt r r <- k v mt r
writeSTRef tnk s writeSTRef tnk s
return r) mt r return r) mt r
Evaluated v -> case apply v vs of Evaluated v -> k v mt r
EvalM f -> f gr k mt r Residuation _ -> k (VMeta tnk [] []) mt r
Unbound _ _ -> k (VMeta tnk [] vs) mt r Narrowing _ _ -> k (VMeta tnk [] []) 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 Residuation i -> k (Right i) mt r
Narrowing i _ -> k (Right i) mt r

View File

@@ -13,7 +13,7 @@ module GF.Compile.GeneratePMCFG
(generatePMCFG, pgfCncCat, addPMCFG (generatePMCFG, pgfCncCat, addPMCFG
) where ) where
import GF.Grammar hiding (VApp) import GF.Grammar hiding (VApp,VRecType)
import GF.Grammar.Predef import GF.Grammar.Predef
import GF.Grammar.Lookup import GF.Grammar.Lookup
import GF.Infra.CheckM import GF.Infra.CheckM
@@ -46,7 +46,7 @@ pmcfgForm gr t ctxt ty =
tnk <- newThunk [] t tnk <- newThunk [] t
return ((d+1,ms'),tnk)) return ((d+1,ms'),tnk))
(0,Map.empty) ctxt (0,Map.empty) ctxt
sequence_ [newMeta (Just ty) i | (i,ty) <- Map.toList ms] sequence_ [newNarrowing i ty | (i,ty) <- Map.toList ms]
v <- eval [] t args v <- eval [] t args
(lins,params) <- flatten v ty ([],[]) (lins,params) <- flatten v ty ([],[])
lins <- mapM str2lin lins lins <- mapM str2lin lins
@@ -55,7 +55,7 @@ pmcfgForm gr t ctxt ty =
return (PMCFGRule (PMCFGCat r rs) args (reverse lins)) return (PMCFGRule (PMCFGCat r rs) args (reverse lins))
where where
tnk2pmcfgcat tnk (_,_,ty) = do tnk2pmcfgcat tnk (_,_,ty) = do
v <- force tnk [] v <- force tnk
(_,params) <- flatten v ty ([],[]) (_,params) <- flatten v ty ([],[])
(r,rs,_) <- compute params (r,rs,_) <- compute params
return (PMCFGCat r rs) return (PMCFGCat r rs)
@@ -85,26 +85,12 @@ type2metaTerm gr d ms r rs ty@(QC q) =
let i = Map.size ms + 1 let i = Map.size ms + 1
in (Map.insert i ty ms,r,Meta i) in (Map.insert i ty ms,r,Meta i)
flatten (VSusp tnk env vs k) ty st = do
tnk_st <- getMeta tnk
case tnk_st of
Evaluated v -> do v <- apply v vs
flatten v ty st
Unbound (Just (QC q)) _ -> do (m,ResParam (Just (L _ ps)) _) <- getInfo q
msum [bind tnk m p | p <- ps]
v <- k tnk
flatten v ty st
where
bind tnk m (p, ctxt) = do
tnks <- mapM (\(_,_,ty) -> newMeta (Just ty) 0) ctxt
setMeta tnk (Evaluated (VApp (m,p) tnks))
flatten (VR as) (RecType lbls) st = do flatten (VR as) (RecType lbls) st = do
foldM collect st lbls foldM collect st lbls
where where
collect st (lbl,ty) = collect st (lbl,ty) =
case lookup lbl as of case lookup lbl as of
Just tnk -> do v <- force tnk [] Just tnk -> do v <- force tnk
flatten v ty st flatten v ty st
Nothing -> evalError ("Missing value for label" <+> pp lbl $$ Nothing -> evalError ("Missing value for label" <+> pp lbl $$
"among" <+> hsep (punctuate (pp ',') (map fst as))) "among" <+> hsep (punctuate (pp ',') (map fst as)))
@@ -121,25 +107,36 @@ flatten (VV _ tnks) (Table _ q) st = do
foldM collect st tnks foldM collect st tnks
where where
collect st tnk = do collect st tnk = do
v <- force tnk [] v <- force tnk
flatten v q st flatten v q st
flatten v (Sort s) (lins,params) | s == cStr = do flatten v (Sort s) (lins,params) | s == cStr = do
return (v:lins,params) return (v:lins,params)
flatten v (QC q) (lins,params) = do flatten v (QC q) (lins,params) = do
return (lins,v:params) return (lins,v:params)
flatten v _ _ = do
error (showValue v)
str2lin (VApp q [])
| q == (cPredef, cBIND) = return [SymBIND]
| q == (cPredef, cNonExist) = return [SymNE]
| q == (cPredef, cSOFT_BIND) = return [SymSOFT_BIND]
| q == (cPredef, cSOFT_SPACE) = return [SymSOFT_SPACE]
| q == (cPredef, cCAPIT) = return [SymCAPIT]
| q == (cPredef, cALL_CAPIT) = return [SymALL_CAPIT]
str2lin (VStr s) = return [SymKS s] str2lin (VStr s) = return [SymKS s]
str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs
return [SymCat d r rs] return [SymCat d r rs]
where where
compute r' [] = return (r',[]) compute r' [] = return (r',[])
compute r' ((cnt',tnk):tnks) = do compute r' ((cnt',tnk):tnks) = do
(r, rs,_) <- force tnk [] >>= param2int (r, rs,_) <- force tnk >>= param2int
(r',rs' ) <- compute r' tnks (r',rs' ) <- compute r' tnks
return (r*cnt'+r',combine cnt' rs rs') return (r*cnt'+r',combine cnt' rs rs')
str2lin (VC vs) = fmap concat (mapM str2lin vs) str2lin (VC vs) = fmap concat (mapM str2lin vs)
str2lin (VAlts def alts) = do def <- str2lin def
return [SymKP def []]
str2lin v = do t <- value2term 0 v str2lin v = do t <- value2term 0 v
evalError ("the term" <+> ppTerm Unqualified 0 t $$ evalError ("the string:" <+> ppTerm Unqualified 0 t $$
"cannot be evaluated at compile time.") "cannot be evaluated at compile time.")
param2int (VApp q tnks) = do param2int (VApp q tnks) = do
@@ -155,16 +152,19 @@ param2int (VApp q tnks) = do
compute [] = return (0,[],1) compute [] = return (0,[],1)
compute (tnk:tnks) = do compute (tnk:tnks) = do
(r, rs ,cnt ) <- force tnk [] >>= param2int (r, rs ,cnt ) <- force tnk >>= param2int
(r',rs',cnt') <- compute tnks (r',rs',cnt') <- compute tnks
return (r*cnt'+r',combine cnt' rs rs',cnt*cnt') return (r*cnt'+r',combine cnt' rs rs',cnt*cnt')
param2int (VMeta tnk _ _) = do param2int (VMeta tnk _ _) = do
tnk_st <- getMeta tnk tnk_st <- getRef tnk
case tnk_st of case tnk_st of
Evaluated v -> param2int v Evaluated v -> param2int v
Unbound (Just ty) j -> do let QC q = valTypeCnc ty Narrowing j ty -> do let QC q = valTypeCnc ty
(_,ResParam _ (Just (_,cnt))) <- getInfo q (_,ResParam _ (Just (_,cnt))) <- getInfo q
return (0,[(1,j)],cnt) return (0,[(1,j)],cnt)
param2int v = do t <- value2term 0 v
evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$
"cannot be evaluated at compile time.")
combine cnt' [] rs' = rs' combine cnt' [] rs' = rs'
combine cnt' rs [] = [(r*cnt',pv) | (r,pv) <- rs] combine cnt' rs [] = [(r*cnt',pv) | (r,pv) <- rs]

View File

@@ -13,7 +13,7 @@ import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.TypeCheck.Primitives import GF.Compile.TypeCheck.Primitives
import Data.List import Data.List
import Data.Maybe(fromMaybe) import Data.Maybe(fromMaybe,isJust,isNothing)
import Control.Monad import Control.Monad
import GF.Text.Pretty import GF.Text.Pretty
@@ -543,23 +543,18 @@ checkLType gr g trm typ0 = do
RecType rr -> do RecType rr -> do
ll2 <- case s of (fields1,fields2) <- case s of
R ss -> return $ map fst ss R ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr)
_ -> do _ -> do
(s',typ2) <- inferLType gr g s (s',typ2) <- inferLType gr g s
case typ2 of case typ2 of
RecType ss -> return $ map fst ss RecType ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr)
_ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2)) _ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
let ll1 = [l | (l,_) <- rr, notElem l ll2]
--- over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020 (r',_) <- checkLType gr g r (RecType fields1)
--- let r1 = maybe r fst over (s',_) <- checkLType gr g s (RecType fields2)
let r1 = r ---
(r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1]) let rec = R ([(l,(Nothing,P r' l)) | (l,_) <- fields1] ++ [(l,(Nothing,P s' l)) | (l,_) <- fields2])
(s',_) <- checkLType gr g s (RecType [field | field@(l,_) <- rr, elem l ll2])
let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
return (rec, typ) return (rec, typ)
ExtR ty ex -> do ExtR ty ex -> do

View File

@@ -19,7 +19,7 @@ module GF.Grammar.Lookup (
lookupIdent, lookupIdent,
lookupOrigInfo, lookupOrigInfo,
allOrigInfos, allOrigInfos,
lookupResDef, lookupResDefLoc, lookupResDef,
lookupResType, lookupResType,
lookupOverload, lookupOverload,
lookupOverloadTypes, lookupOverloadTypes,
@@ -64,26 +64,24 @@ lookupQIdentInfo :: ErrorMonad m => Grammar -> QIdent -> m Info
lookupQIdentInfo gr (m,c) = flip lookupIdentInfo c =<< lookupModule gr m lookupQIdentInfo gr (m,c) = flip lookupIdentInfo c =<< lookupModule gr m
lookupResDef :: ErrorMonad m => Grammar -> QIdent -> m Term lookupResDef :: ErrorMonad m => Grammar -> QIdent -> m Term
lookupResDef gr x = fmap unLoc (lookupResDefLoc gr x) lookupResDef gr (m,c)
| isPredefCat c = lock c defLinType
lookupResDefLoc gr (m,c)
| isPredefCat c = fmap noLoc (lock c defLinType)
| otherwise = look m c | otherwise = look m c
where where
look m c = do look m c = do
info <- lookupQIdentInfo gr (m,c) info <- lookupQIdentInfo gr (m,c)
case info of case info of
ResOper _ (Just lt) -> return lt ResOper _ (Just (L _ t)) -> return t
ResOper _ Nothing -> return (noLoc (Q (m,c))) ResOper _ Nothing -> return (Q (m,c))
CncCat (Just (L l ty)) _ _ _ _ -> fmap (L l) (lock c ty) CncCat (Just (L _ ty)) _ _ _ _ -> lock c ty
CncCat _ _ _ _ _ -> fmap noLoc (lock c defLinType) CncCat _ _ _ _ _ -> lock c defLinType
CncFun (Just (_,cat,_,_)) (Just (L l tr)) _ _ -> fmap (L l) (unlock cat tr) CncFun (Just (_,cat,_,_)) (Just (L _ tr)) _ _ -> unlock cat tr
CncFun _ (Just ltr) _ _ -> return ltr CncFun _ (Just (L _ tr)) _ _ -> return tr
AnyInd _ n -> look n c AnyInd _ n -> look n c
ResParam _ _ -> return (noLoc (QC (m,c))) ResParam _ _ -> return (QC (m,c))
ResValue _ _ -> return (noLoc (QC (m,c))) ResValue _ _ -> return (QC (m,c))
_ -> raise $ render (c <+> "is not defined in resource" <+> m) _ -> raise $ render (c <+> "is not defined in resource" <+> m)
lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type