mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-09 04:59:31 -06:00
make it possible to control whether to expand variants or not
This commit is contained in:
@@ -19,7 +19,7 @@ import GF.Grammar.Analyse
|
||||
import GF.Grammar.ShowTerm
|
||||
import GF.Grammar.Lookup (allOpers,allOpersTo)
|
||||
import GF.Compile.Rename(renameSourceTerm)
|
||||
import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef)
|
||||
import GF.Compile.Compute.Concrete(normalForm,normalFlatForm,Globals(..),stdPredef)
|
||||
import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType)
|
||||
|
||||
import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts)
|
||||
@@ -50,7 +50,7 @@ sourceCommands = Map.fromList [
|
||||
("one","pick the first strings, if there is any, from records and tables"),
|
||||
("table","show all strings labelled by parameters"),
|
||||
("unqual","hide qualifying module names"),
|
||||
("trace","trace computations")
|
||||
("flat","expand all variants and show a flat list of terms")
|
||||
],
|
||||
needsTypeCheck = False, -- why not True?
|
||||
exec = withTerm compute_concrete
|
||||
@@ -167,8 +167,8 @@ sourceCommands = Map.fromList [
|
||||
liftSIO (exec opts (toTerm ts) sgr)
|
||||
|
||||
compute_concrete opts t sgr = fmap fst $ runCheck $ do
|
||||
t <- checkComputeTerm opts sgr t
|
||||
return (fromString (showTerm sgr style q t))
|
||||
ts <- checkComputeTerm opts sgr t
|
||||
return (fromStrings (map (showTerm sgr style q) ts))
|
||||
where
|
||||
(style,q) = pOpts TermPrintDefault Qualified opts
|
||||
|
||||
@@ -198,9 +198,8 @@ sourceCommands = Map.fromList [
|
||||
|
||||
show_operations os t sgr = fmap fst $ runCheck $ do
|
||||
let greps = map valueString (listFlags "grep" os)
|
||||
ops <- do ty <- checkComputeTerm os sgr t
|
||||
return $ allOpersTo sgr ty
|
||||
-- _ -> return $ allOpers sgr
|
||||
ops <- do tys <- checkComputeTerm os sgr t
|
||||
return $ concatMap (allOpersTo sgr) tys
|
||||
let sigs = [(op,ty) | ((mo,op),ty,pos) <- ops]
|
||||
printer = showTerm sgr TermPrintDefault
|
||||
(if isOpt "raw" os then Qualified else Unqualified)
|
||||
@@ -247,9 +246,13 @@ checkComputeTerm os sgr t =
|
||||
Just mo -> return mo
|
||||
t <- renameSourceTerm sgr mo t
|
||||
(t,_) <- inferLType sgr [] t
|
||||
fmap evalStr (normalForm (Gl sgr stdPredef) t)
|
||||
if isOpt "flat" os
|
||||
then fmap (map evalStr) (normalFlatForm (Gl sgr stdPredef) t)
|
||||
else fmap (singleton . evalStr) (normalForm (Gl sgr stdPredef) t)
|
||||
where
|
||||
-- ** Try to compute pre{...} tokens in token sequences
|
||||
singleton x = [x]
|
||||
|
||||
evalStr t =
|
||||
case t of
|
||||
C t1 t2 -> foldr1 C (evalC [t])
|
||||
|
||||
@@ -3,7 +3,7 @@
|
||||
-- | Functions for computing the values of terms in the concrete syntax, in
|
||||
-- | preparation for PMCFG generation.
|
||||
module GF.Compile.Compute.Concrete
|
||||
( normalForm, normalStringForm
|
||||
( normalForm, normalFlatForm, normalStringForm
|
||||
, Value(..), Thunk, ThunkState(..), Env, Scope, showValue
|
||||
, MetaThunks, Constraint, Globals(..), ConstValue(..)
|
||||
, EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn
|
||||
@@ -43,13 +43,19 @@ import PGF2.Transactions(LIndex)
|
||||
|
||||
-- * Main entry points
|
||||
|
||||
-- | The term is fully evaluated. Variants are only expanded if necessary for the evaluation.
|
||||
normalForm :: Globals -> Term -> Check Term
|
||||
normalForm globals t =
|
||||
fmap mkFV (runEvalM globals (eval [] t [] >>= value2term []))
|
||||
fmap mkFV (runEvalM globals (eval [] t [] >>= value2term False []))
|
||||
where
|
||||
mkFV [t] = t
|
||||
mkFV ts = FV ts
|
||||
|
||||
-- | The result is a list of terms and contains all variants. Each term by itself does not contain any variants.
|
||||
normalFlatForm :: Globals -> Term -> Check [Term]
|
||||
normalFlatForm globals t =
|
||||
runEvalM globals (eval [] t [] >>= value2term True [])
|
||||
|
||||
normalStringForm :: Globals -> Term -> Check [String]
|
||||
normalStringForm globals t =
|
||||
fmap toStrs (runEvalM globals (fmap value2string (eval [] t [])))
|
||||
@@ -194,7 +200,7 @@ eval env (S t1 t2) vs = do v1 <- eval env t1 []
|
||||
let v0 = VS v1 tnk2 vs
|
||||
case v1 of
|
||||
VT _ env cs -> patternMatch v0 (map (\(p,t) -> (env,[p],tnk2:vs,t)) cs)
|
||||
VV vty tnks -> do ty <- value2term (map fst env) vty
|
||||
VV vty tnks -> do ty <- value2term True (map fst env) vty
|
||||
vtableSelect v0 ty tnks tnk2 vs
|
||||
v1 -> return v0
|
||||
eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
|
||||
@@ -449,7 +455,7 @@ vtableSelect v0 ty tnks tnk2 vs = do
|
||||
value2index (VSusp i k vs) ty = do
|
||||
v <- susp i (\v -> k v >>= \v -> apply v vs)
|
||||
value2index v ty
|
||||
value2index v ty = do t <- value2term [] v
|
||||
value2index v ty = do t <- value2term True [] v
|
||||
evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
@@ -501,109 +507,112 @@ susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
|
||||
| otherwise = return (Success r msgs)
|
||||
|
||||
|
||||
value2term xs (VApp q tnks) =
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks
|
||||
value2term xs (VMeta m vs) = do
|
||||
value2term flat xs (VApp q tnks) =
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (if fst q == cPredef then Q q else QC q) tnks
|
||||
value2term flat xs (VMeta m vs) = do
|
||||
s <- getRef m
|
||||
case s of
|
||||
Evaluated _ v -> do v <- apply v vs
|
||||
value2term xs v
|
||||
value2term flat xs v
|
||||
Unevaluated env t -> do v <- eval env t vs
|
||||
value2term xs v
|
||||
Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
|
||||
value2term flat xs v
|
||||
Hole i -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs
|
||||
Residuation i _ ctr -> case ctr of
|
||||
Just ctr -> value2term xs ctr
|
||||
Nothing -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
|
||||
Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
|
||||
value2term xs (VSusp j k vs) = do
|
||||
Just ctr -> value2term flat xs ctr
|
||||
Nothing -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs
|
||||
Narrowing i _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Meta i) vs
|
||||
value2term flat xs (VSusp j k vs) = do
|
||||
v <- k (VGen maxBound vs)
|
||||
value2term xs v
|
||||
value2term xs (VGen j tnks) =
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Vr (reverse xs !! j)) tnks
|
||||
value2term xs (VClosure env (Abs b x t)) = do
|
||||
value2term flat xs v
|
||||
value2term flat xs (VGen j tnks) =
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (Vr (reverse xs !! j)) tnks
|
||||
value2term flat xs (VClosure env (Abs b x t)) = do
|
||||
tnk <- newEvaluatedThunk (VGen (length xs) [])
|
||||
v <- eval ((x,tnk):env) t []
|
||||
let x' = mkFreshVar xs x
|
||||
t <- value2term (x':xs) v
|
||||
t <- value2term flat (x':xs) v
|
||||
return (Abs b x' t)
|
||||
value2term xs (VProd b x v1 v2)
|
||||
| x == identW = do t1 <- value2term xs v1
|
||||
value2term flat xs (VProd b x v1 v2)
|
||||
| x == identW = do t1 <- value2term flat xs v1
|
||||
v2 <- case v2 of
|
||||
VClosure env t2 -> eval env t2 []
|
||||
v2 -> return v2
|
||||
t2 <- value2term xs v2
|
||||
t2 <- value2term flat xs v2
|
||||
return (Prod b x t1 t2)
|
||||
| otherwise = do t1 <- value2term xs v1
|
||||
| otherwise = do t1 <- value2term flat xs v1
|
||||
tnk <- newEvaluatedThunk (VGen (length xs) [])
|
||||
v2 <- case v2 of
|
||||
VClosure env t2 -> eval ((x,tnk):env) t2 []
|
||||
v2 -> return v2
|
||||
t2 <- value2term (x:xs) v2
|
||||
t2 <- value2term flat (x:xs) v2
|
||||
return (Prod b (mkFreshVar xs x) t1 t2)
|
||||
value2term xs (VRecType lbls) = do
|
||||
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term xs v)) lbls
|
||||
value2term flat xs (VRecType lbls) = do
|
||||
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2term flat xs v)) lbls
|
||||
return (RecType lbls)
|
||||
value2term xs (VR as) = do
|
||||
as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (tnk2term xs tnk)) as
|
||||
value2term flat xs (VR as) = do
|
||||
as <- mapM (\(lbl,tnk) -> fmap (\t -> (lbl,(Nothing,t))) (tnk2term flat xs tnk)) as
|
||||
return (R as)
|
||||
value2term xs (VP v lbl tnks) = do
|
||||
t <- value2term xs v
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (P t lbl) tnks
|
||||
value2term xs (VExtR v1 v2) = do
|
||||
t1 <- value2term xs v1
|
||||
t2 <- value2term xs v2
|
||||
value2term flat xs (VP v lbl tnks) = do
|
||||
t <- value2term flat xs v
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (P t lbl) tnks
|
||||
value2term flat xs (VExtR v1 v2) = do
|
||||
t1 <- value2term flat xs v1
|
||||
t2 <- value2term flat xs v2
|
||||
return (ExtR t1 t2)
|
||||
value2term xs (VTable v1 v2) = do
|
||||
t1 <- value2term xs v1
|
||||
t2 <- value2term xs v2
|
||||
value2term flat xs (VTable v1 v2) = do
|
||||
t1 <- value2term flat xs v1
|
||||
t2 <- value2term flat xs v2
|
||||
return (Table t1 t2)
|
||||
value2term xs (VT vty env cs)= do
|
||||
ty <- value2term xs vty
|
||||
value2term flat xs (VT vty env cs)= do
|
||||
ty <- value2term flat xs vty
|
||||
cs <- forM cs $ \(p,t) -> do
|
||||
(_,xs',env') <- pattVars (length xs,xs,env) p
|
||||
v <- eval env' t []
|
||||
t <- value2term xs' v
|
||||
t <- value2term flat xs' v
|
||||
return (p,t)
|
||||
return (T (TTyped ty) cs)
|
||||
value2term xs (VV vty tnks)= do ty <- value2term xs vty
|
||||
ts <- mapM (tnk2term xs) tnks
|
||||
return (V ty ts)
|
||||
value2term xs (VS v1 tnk2 tnks) = do t1 <- value2term xs v1
|
||||
t2 <- tnk2term xs tnk2
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (S t1 t2) tnks
|
||||
value2term xs (VSort s) = return (Sort s)
|
||||
value2term xs (VStr tok) = return (K tok)
|
||||
value2term xs (VInt n) = return (EInt n)
|
||||
value2term xs (VFlt n) = return (EFloat n)
|
||||
value2term xs VEmpty = return Empty
|
||||
value2term xs (VC v1 v2) = do
|
||||
t1 <- value2term xs v1
|
||||
t2 <- value2term xs v2
|
||||
value2term flat xs (VV vty tnks)= do
|
||||
ty <- value2term flat xs vty
|
||||
ts <- mapM (tnk2term flat xs) tnks
|
||||
return (V ty ts)
|
||||
value2term flat xs (VS v1 tnk2 tnks) = do
|
||||
t1 <- value2term flat xs v1
|
||||
t2 <- tnk2term flat xs tnk2
|
||||
foldM (\e1 tnk -> fmap (App e1) (tnk2term flat xs tnk)) (S t1 t2) tnks
|
||||
value2term flat xs (VSort s) = return (Sort s)
|
||||
value2term flat xs (VStr tok) = return (K tok)
|
||||
value2term flat xs (VInt n) = return (EInt n)
|
||||
value2term flat xs (VFlt n) = return (EFloat n)
|
||||
value2term flat xs VEmpty = return Empty
|
||||
value2term flat xs (VC v1 v2) = do
|
||||
t1 <- value2term flat xs v1
|
||||
t2 <- value2term flat xs v2
|
||||
return (C t1 t2)
|
||||
value2term xs (VGlue v1 v2) = do
|
||||
t1 <- value2term xs v1
|
||||
t2 <- value2term xs v2
|
||||
value2term flat xs (VGlue v1 v2) = do
|
||||
t1 <- value2term flat xs v1
|
||||
t2 <- value2term flat xs v2
|
||||
return (Glue t1 t2)
|
||||
value2term xs (VPatt min max p) = return (EPatt min max p)
|
||||
value2term xs (VPattType v) = do t <- value2term xs v
|
||||
return (EPattType t)
|
||||
value2term xs (VAlts vd vas) = do
|
||||
d <- value2term xs vd
|
||||
value2term flat xs (VPatt min max p) = return (EPatt min max p)
|
||||
value2term flat xs (VPattType v) = do
|
||||
t <- value2term flat xs v
|
||||
return (EPattType t)
|
||||
value2term flat xs (VAlts vd vas) = do
|
||||
d <- value2term flat xs vd
|
||||
as <- forM vas $ \(vt,vs) -> do
|
||||
t <- value2term xs vt
|
||||
s <- value2term xs vs
|
||||
t <- value2term flat xs vt
|
||||
s <- value2term flat xs vs
|
||||
return (t,s)
|
||||
return (Alts d as)
|
||||
value2term xs (VStrs vs) = do
|
||||
ts <- mapM (value2term xs) vs
|
||||
value2term flat xs (VStrs vs) = do
|
||||
ts <- mapM (value2term flat xs) vs
|
||||
return (Strs ts)
|
||||
value2term xs (VCInts (Just i) Nothing) = return (App (Q (cPredef,cInts)) (EInt i))
|
||||
value2term xs (VCInts Nothing (Just j)) = return (App (Q (cPredef,cInts)) (EInt j))
|
||||
value2term xs (VCRecType lctrs) = do
|
||||
ltys <- mapM (\(l,o,ctr) -> value2term xs ctr >>= \ty -> return (l,ty)) lctrs
|
||||
value2term flat xs (VCInts (Just i) Nothing) = return (App (Q (cPredef,cInts)) (EInt i))
|
||||
value2term flat xs (VCInts Nothing (Just j)) = return (App (Q (cPredef,cInts)) (EInt j))
|
||||
value2term flat xs (VCRecType lctrs) = do
|
||||
ltys <- mapM (\(l,o,ctr) -> value2term flat xs ctr >>= \ty -> return (l,ty)) lctrs
|
||||
return (RecType ltys)
|
||||
value2term xs (VSymCat d r rs) = return (TSymCat d r [(i,(identW,ty)) | (i,(_,ty)) <- rs])
|
||||
value2term xs v = error (showValue v)
|
||||
value2term flat xs (VSymCat d r rs) = return (TSymCat d r [(i,(identW,ty)) | (i,(_,ty)) <- rs])
|
||||
value2term flat xs v = error (showValue v)
|
||||
|
||||
pattVars st (PP _ ps) = foldM pattVars st ps
|
||||
pattVars st (PV x) = case st of
|
||||
@@ -885,7 +894,8 @@ force tnk = EvalM $ \gr k mt d r msgs -> do
|
||||
Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs
|
||||
Narrowing _ _ -> k (VMeta tnk []) mt d r msgs
|
||||
|
||||
tnk2term xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
tnk2term True xs tnk = force tnk >>= value2term True xs
|
||||
tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
let join f g = do res <- f
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
@@ -904,7 +914,7 @@ tnk2term xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
Unevaluated env t -> do let d0 = length env
|
||||
res <- case eval env t [] of
|
||||
EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v)
|
||||
r <- case value2term xs v of
|
||||
r <- case value2term False xs v of
|
||||
EvalM f -> f gr (acc d0) mt d msgs r
|
||||
writeSTRef tnk s
|
||||
return r) mt maxBound (r,0,[]) msgs
|
||||
@@ -912,7 +922,7 @@ tnk2term xs tnk = EvalM $ \gr k mt d r msgs ->
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
Success (r,0,xs) msgs -> k (FV []) mt d r msgs
|
||||
Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs
|
||||
Evaluated d0 v -> do res <- case value2term xs v of
|
||||
Evaluated d0 v -> do res <- case value2term False xs v of
|
||||
EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs
|
||||
case res of
|
||||
Fail msg msgs -> return (Fail msg msgs)
|
||||
|
||||
@@ -219,7 +219,7 @@ str2lin (VAlts def alts) = do def <- str2lin def
|
||||
lin <- str2lin v
|
||||
return (lin,[s | VStr s <- vs])
|
||||
return [SymKP def alts]
|
||||
str2lin v = do t <- value2term [] v
|
||||
str2lin v = do t <- value2term False [] v
|
||||
evalError ("the string:" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
@@ -259,7 +259,7 @@ param2int (VMeta tnk _) ty = do
|
||||
Evaluated _ v -> param2int v ty
|
||||
Narrowing j ty -> do ts <- getAllParamValues ty
|
||||
return (0,[(1,j-1)],length ts)
|
||||
param2int v ty = do t <- value2term [] v
|
||||
param2int v ty = do t <- value2term True [] v
|
||||
evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be evaluated at compile time.")
|
||||
|
||||
|
||||
@@ -34,7 +34,7 @@ inferLType :: Globals -> Term -> Check (Term, Type)
|
||||
inferLType globals t = runEvalOneM globals $ do
|
||||
(t,ty) <- inferSigma [] t
|
||||
t <- zonkTerm [] t
|
||||
ty <- value2term [] ty
|
||||
ty <- value2term False [] ty
|
||||
return (t,ty)
|
||||
|
||||
inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s)
|
||||
@@ -178,7 +178,7 @@ tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET
|
||||
(rhs,_) <- tcRho scope rhs (Just v_ann_ty)
|
||||
return (rhs, v_ann_ty)
|
||||
(body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty
|
||||
var_ty <- value2term (scopeVars scope) var_ty
|
||||
var_ty <- value2term True (scopeVars scope) var_ty
|
||||
return (Let (var, (Just var_ty, rhs)) body, body_ty)
|
||||
tcRho scope (Typed body ann_ty) mb_ty = do -- ANNOT
|
||||
(ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
|
||||
@@ -214,7 +214,7 @@ tcRho scope t@(RecType rs) (Just ty) = do
|
||||
VMeta i vs -> case rs of
|
||||
[] -> unifyVar scope i vs vtypePType
|
||||
_ -> return ()
|
||||
ty -> do ty <- value2term (scopeVars scope) ty
|
||||
ty -> do ty <- value2term False (scopeVars scope) ty
|
||||
evalError ("The record type" <+> ppTerm Unqualified 0 t $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 ty)
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs (Just ty')
|
||||
@@ -248,7 +248,7 @@ tcRho scope (T tt ps) Nothing = do -- ABS1/AABS1 for t
|
||||
eval env ty []
|
||||
res_ty <- fmap mk_val $ newResiduation scope
|
||||
ps <- tcCases scope ps p_ty res_ty
|
||||
p_ty_t <- value2term [] p_ty
|
||||
p_ty_t <- value2term True [] p_ty
|
||||
return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
|
||||
tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
@@ -260,7 +260,7 @@ tcRho scope (T tt ps) (Just ty) = do -- ABS2/AABS2 for t
|
||||
ty <- eval env ty []
|
||||
unify scope ty p_ty
|
||||
ps <- tcCases scope ps p_ty res_ty
|
||||
p_ty_t <- value2term (scopeVars scope) p_ty
|
||||
p_ty_t <- value2term True (scopeVars scope) p_ty
|
||||
return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
|
||||
tcRho scope (V p_ty ts) Nothing = do
|
||||
(p_ty, _) <- tcRho scope p_ty (Just vtypeType)
|
||||
@@ -285,7 +285,7 @@ tcRho scope (V p_ty0 ts) (Just ty) = do
|
||||
return (V p_ty0 ts, VTable p_ty res_ty)
|
||||
tcRho scope (R rs) Nothing = do
|
||||
lttys <- inferRecFields scope rs
|
||||
rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
rs <- mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
return (R rs,
|
||||
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
)
|
||||
@@ -293,12 +293,12 @@ tcRho scope (R rs) (Just ty) = do
|
||||
(scope,f,ty') <- skolemise scope ty
|
||||
case ty' of
|
||||
(VRecType ltys) -> do lttys <- checkRecFields scope rs ltys
|
||||
rs <- mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
rs <- mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
|
||||
return ((f . R) rs,
|
||||
VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
)
|
||||
ty -> do lttys <- inferRecFields scope rs
|
||||
t <- liftM (f . R) (mapM (\(l,t,ty) -> value2term (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
t <- liftM (f . R) (mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
|
||||
let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
|
||||
t <- subsCheckRho scope t ty' ty
|
||||
return (t, ty')
|
||||
@@ -502,7 +502,7 @@ tcRecTypeFields scope ((l,ty):rs) mb_ty = do
|
||||
| s == cType -> return (Just sort)
|
||||
| s == cPType -> return mb_ty
|
||||
VMeta _ _ -> return mb_ty
|
||||
_ -> do sort <- value2term (scopeVars scope) sort
|
||||
_ -> do sort <- value2term False (scopeVars scope) sort
|
||||
evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
|
||||
"cannot be of type" <+> ppTerm Unqualified 0 sort)
|
||||
(rs,mb_ty) <- tcRecTypeFields scope rs mb_ty
|
||||
@@ -662,7 +662,7 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
|
||||
let x = newVar scope
|
||||
xt <- subsCheckRho scope (Vr x) p2 p1
|
||||
t <- subsCheckRho ((x,vtypePType):scope) (S t xt) r1 r2
|
||||
p2 <- value2term (scopeVars scope) p2
|
||||
p2 <- value2term True (scopeVars scope) p2
|
||||
return (T (TTyped p2) [(PV x,t)])
|
||||
|
||||
subtype scope Nothing (VApp p [tnk])
|
||||
@@ -782,8 +782,8 @@ unify scope (VStr s1) (VStr s2)
|
||||
| s1 == s2 = return ()
|
||||
unify scope VEmpty VEmpty = return ()
|
||||
unify scope v1 v2 = do
|
||||
t1 <- value2term (scopeVars scope) v1
|
||||
t2 <- value2term (scopeVars scope) v2
|
||||
t1 <- value2term False (scopeVars scope) v1
|
||||
t2 <- value2term False (scopeVars scope) v2
|
||||
evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
|
||||
ppTerm Unqualified 0 t2))
|
||||
|
||||
@@ -810,8 +810,8 @@ occursCheck scope' tnk scope v =
|
||||
where
|
||||
check m n (VApp f vs) = mapM_ (follow m n) vs
|
||||
check m n (VMeta i vs)
|
||||
| tnk == i = do ty1 <- value2term (scopeVars scope) (VMeta i vs)
|
||||
ty2 <- value2term (scopeVars scope) v
|
||||
| tnk == i = do ty1 <- value2term False (scopeVars scope) (VMeta i vs)
|
||||
ty2 <- value2term False (scopeVars scope) v
|
||||
evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$
|
||||
nest 2 (ppTerm Unqualified 0 ty2))
|
||||
| otherwise = do
|
||||
@@ -1087,8 +1087,8 @@ zonkTerm xs (Meta i) = do
|
||||
case st of
|
||||
Hole _ -> return (Meta i)
|
||||
Residuation _ scope v -> case v of
|
||||
Just v -> zonkTerm xs =<< value2term (map fst scope) v
|
||||
Just v -> zonkTerm xs =<< value2term False (map fst scope) v
|
||||
Nothing -> return (Meta i)
|
||||
Narrowing _ _ -> return (Meta i)
|
||||
Evaluated _ v -> zonkTerm xs =<< value2term xs v
|
||||
Evaluated _ v -> zonkTerm xs =<< value2term False xs v
|
||||
zonkTerm xs t = composOp (zonkTerm xs) t
|
||||
|
||||
@@ -3,7 +3,7 @@ module GF.Term (renameSourceTerm,
|
||||
Value(..), showValue, Thunk, newThunk, newEvaluatedThunk,
|
||||
evalError, evalWarn,
|
||||
inferLType, checkLType,
|
||||
normalForm, normalStringForm,
|
||||
normalForm, normalFlatForm, normalStringForm,
|
||||
unsafeIOToEvalM, force
|
||||
) where
|
||||
|
||||
|
||||
Reference in New Issue
Block a user