From 02e8dcbb56c2ba094e79a782ee265c731e9c7f90 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Sat, 27 Apr 2024 14:55:01 +0200 Subject: [PATCH] make it possible to control whether to expand variants or not --- src/compiler/api/GF/Command/SourceCommands.hs | 19 ++- .../api/GF/Compile/Compute/Concrete.hs | 160 ++++++++++-------- src/compiler/api/GF/Compile/GeneratePMCFG.hs | 4 +- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 32 ++-- src/compiler/api/GF/Term.hs | 2 +- 5 files changed, 115 insertions(+), 102 deletions(-) diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index dbf9b604b..3b0689cbf 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -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]) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs index 9235fb81f..bcc930d68 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs @@ -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) diff --git a/src/compiler/api/GF/Compile/GeneratePMCFG.hs b/src/compiler/api/GF/Compile/GeneratePMCFG.hs index c11c52bdf..d8e83084d 100644 --- a/src/compiler/api/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/api/GF/Compile/GeneratePMCFG.hs @@ -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.") diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index ce80af716..cc9601dc8 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -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 diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs index fe9baadec..d9ffc9538 100644 --- a/src/compiler/api/GF/Term.hs +++ b/src/compiler/api/GF/Term.hs @@ -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