From 3a1990fd1d399960babfbcb055b262d979a21d60 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Sun, 18 May 2025 07:20:12 +0200 Subject: [PATCH] switch to using the new type checker by default --- src/compiler/api/GF/Command/SourceCommands.hs | 6 +-- src/compiler/api/GF/Compile/CheckGrammar.hs | 38 ++++++++++--------- .../api/GF/Compile/Compute/Concrete2.hs | 8 ++-- src/compiler/api/GF/Compile/Repl.hs | 14 +++---- .../api/GF/Compile/TypeCheck/ConcreteNew.hs | 32 ++++++++++------ src/compiler/api/GF/Grammar/Grammar.hs | 2 +- src/compiler/api/GF/Grammar/Parser.y | 4 +- 7 files changed, 56 insertions(+), 48 deletions(-) diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index f7f98308d..2ef833a5c 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -245,10 +245,10 @@ checkComputeTerm os sgr t = Nothing -> checkError (pp "No source grammar in scope") Just mo -> return mo t <- renameSourceTerm sgr mo t - ttys <- inferLType g t + (t,_) <- inferLType g t if isOpt "flat" os - then fmap concat (mapM (\(t,_) -> fmap (map evalStr) (normalFlatForm g t)) ttys) - else fmap concat (mapM (\(t,_) -> fmap (singleton . evalStr) (normalForm g t)) ttys) + then fmap (map evalStr) (normalFlatForm g t) + else fmap (singleton . evalStr) (normalForm g t) where -- ** Try to compute pre{...} tokens in token sequences singleton x = [x] diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index 14fa23f47..9003a3485 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -27,9 +27,9 @@ import GF.Infra.Ident import GF.Infra.Option import GF.Compile.TypeCheck.Abstract -import GF.Compile.TypeCheck.Concrete(checkLType,inferLType,ppType) -import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType) -import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) +import GF.Compile.TypeCheck.Concrete(ppType) +import GF.Compile.TypeCheck.ConcreteNew(checkLType,inferLType) +import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef) import GF.Grammar import GF.Grammar.Lexer @@ -173,26 +173,26 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do CncCat mty mdef mref mpr mpmcfg -> do mty <- case mty of Just (L loc typ) -> chIn loc "linearization type of" $ do - (typ,_) <- checkLType gr [] typ typeType - typ <- normalForm (Gl gr stdPredef) typ + (typ,_) <- checkLType g typ typeType + typ <- normalForm g typ return (Just (L loc typ)) Nothing -> return Nothing mdef <- case (mty,mdef) of (Just (L _ typ),Just (L loc def)) -> chIn loc "default linearization of" $ do - (def,_) <- checkLType gr [] def (mkFunType [typeStr] typ) + (def,_) <- checkLType g def (mkFunType [typeStr] typ) return (Just (L loc def)) _ -> return Nothing mref <- case (mty,mref) of (Just (L _ typ),Just (L loc ref)) -> chIn loc "reference linearization of" $ do - (ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr) + (ref,_) <- checkLType g ref (mkFunType [typ] typeStr) return (Just (L loc ref)) _ -> return Nothing mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType gr [] t typeStr + (t,_) <- checkLType g t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncCat mty mdef mref mpr mpmcfg) @@ -201,13 +201,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do mt <- case (mty,mt) of (Just (_,cat,cont,val),Just (L loc trm)) -> chIn loc "linearization of" $ do - (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars + (trm,_) <- checkLType g trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars return (Just (L loc (etaExpand [] trm cont))) _ -> return mt mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType gr [] t typeStr + (t,_) <- checkLType g t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncFun mty mt mpr mpmcfg) @@ -216,14 +216,14 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do (pty', pde') <- case (pty,pde) of (Just (L loct ty), Just (L locd de)) -> do ty' <- chIn loct "operation" $ do - (ty,_) <- checkLType gr [] ty typeType - normalForm (Gl gr stdPredef) ty + (ty,_) <- checkLType g ty typeType + normalForm g ty (de',_) <- chIn locd "operation" $ - checkLType gr [] de ty' + checkLType g de ty' return (Just (L loct ty'), Just (L locd de')) (Nothing , Just (L locd de)) -> do (de',ty') <- chIn locd "operation" $ - inferLType gr [] de + inferLType g de return (Just (L locd ty'), Just (L locd de')) (Just (L loct ty), Nothing) -> do chIn loct "operation" $ @@ -231,9 +231,9 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do update sm c (ResOper pty' pde') ResOverload os tysts -> chIn NoLoc "overloading" $ do - tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones + tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too - tysts1 <- mapM (uncurry $ flip (checkLType gr [])) + tysts1 <- mapM (uncurry $ flip (checkLType g)) [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0] --- this can only be a partial guarantee, since matching --- with value type is only possible if expected type is given @@ -249,11 +249,12 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do _ -> return sm where gr = prependModule sgr sm + g = Gl gr (stdPredef g) chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c) mkParamValues sm c cnt ts [] = return (sm,cnt,[],[]) mkParamValues sm@(mn,mi) c cnt ts ((p,co):pcs) = do - co <- mapM (\(b,v,ty) -> normalForm (Gl gr stdPredef) ty >>= \ty -> return (b,v,ty)) co + co <- mapM (\(b,v,ty) -> normalForm g ty >>= \ty -> return (b,v,ty)) co sm <- case lookupIdent p (jments mi) of Ok (ResValue (L loc _) _) -> update sm p (ResValue (L loc (mkProdSimple co (QC (mn,c)))) cnt) Bad msg -> checkError (pp msg) @@ -327,6 +328,7 @@ linTypeOfType cnc m (L loc typ) = do plusRecType vars val return ((Explicit,varX i,rec),cat) lookLin (_,c) = checks [ --- rather: update with defLinType ? - lookupLincat cnc m c >>= normalForm (Gl cnc stdPredef) + lookupLincat cnc m c >>= normalForm g ,return defLinType ] + g = Gl cnc (stdPredef g) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs index ee7e4b024..d8e24a363 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs @@ -86,7 +86,7 @@ data Value | VAlts Value [(Value, Value)] | VStrs [Value] | VMarkup Ident [(Ident,Value)] [Value] - | VReset Ident (Maybe Value) Value QIdent + | VReset Ident (Maybe Value) Value (Maybe QIdent) | VSymCat Int LIndex [(LIndex, (Value, Type))] | VError Doc -- These two constructors are only used internally @@ -932,7 +932,7 @@ value2termM flat xs (VMarkup tag as vs) = do as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as ts <- mapM (value2termM flat xs) vs return (Markup tag as ts) -value2termM flat xs (VReset ctl mb_cv v qid) = do +value2termM flat xs (VReset ctl mb_cv v mb_qid) = do ts <- reset (value2termM True xs v) reduce ctl mb_cv ts where @@ -960,8 +960,8 @@ value2termM flat xs (VReset ctl mb_cv v qid) = do ([], _) -> mzero ([t], _) -> return t (ts,Just cv) -> - do let cat = showIdent (snd qid) - mn = fst qid + do let Just (mn,id) = mb_qid + cat = showIdent id ct <- value2termM flat xs cv t <- listify mn cat ts return (App (App (QC (mn,identS ("Conj"++cat))) ct) t) diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs index 8cb7d92a0..fd06bb8cd 100644 --- a/src/compiler/api/GF/Compile/Repl.hs +++ b/src/compiler/api/GF/Compile/Repl.hs @@ -167,12 +167,11 @@ runRepl' opts@ReplOpts { lang, evalToFlat } gl@(Gl g _) = do -- Show the inferred type of an expression command st "t" arg = do parseThen lang g arg $ \main -> - execCheck (inferLType gl main) $ \res -> - forM_ res $ \(t, ty) -> - let t' = case t of - Typed _ _ -> t - t -> Typed t ty - in outputStrLn $ render (ppTerm Unqualified 0 t') + execCheck (inferLType gl main) $ \(t, ty) -> + let t' = case t of + Typed _ _ -> t + t -> Typed t ty + in outputStrLn $ render (ppTerm Unqualified 0 t') nlrepl st -- Show the results of the last evaluated expression @@ -274,8 +273,7 @@ runRepl' opts@ReplOpts { lang, evalToFlat } gl@(Gl g _) = do Nothing -> nlrepl st doEval st t opts = inferLType gl t >>= \case - [] -> fail $ "No result while checking type: " ++ render (ppTerm Unqualified 0 t) - ((t', _):_) -> runEvalMWithOpts gl opts (value2termM evalToFlat [] (eval gl [] unit t' [])) + (t', _) -> runEvalMWithOpts gl opts (value2termM evalToFlat [] (eval gl [] unit t' [])) outputResults rs = forM_ (zip [1..] rs) $ \(i, ResultState r _ opts _) -> diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs index 90ddfa3bd..9fa151701 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs @@ -25,12 +25,16 @@ import Data.Bifunctor(second) import Data.Functor((<&>)) import qualified Control.Monad.Fail as Fail -checkLType :: Globals -> Term -> Type -> Check [(Term, Type)] -checkLType globals t ty = runEvalM globals $ - do let (c1,c2) = split unit - (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) - ty <- value2termM True [] vty - return (t,ty) +checkLType :: Globals -> Term -> Type -> Check (Term, Type) +checkLType globals t ty = do + res <- runEvalM globals $ do + let (c1,c2) = split unit + (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") checkLType' :: Choice -> Term -> Constraint -> EvalM (Term, Constraint) checkLType' c t vty = do @@ -38,11 +42,15 @@ checkLType' c t vty = do t <- zonkTerm [] t return (t,vty) -inferLType :: Globals -> Term -> Check [(Term, Type)] -inferLType globals t = runEvalM globals $ do - (t,vty) <- inferLType' t - ty <- value2termM True [] vty - return (t,ty) +inferLType :: Globals -> Term -> Check (Term, Type) +inferLType globals t = do + res <- runEvalM globals $ do + (t,vty) <- inferLType' t + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") inferLType' :: Term -> EvalM (Term, Constraint) inferLType' t = do @@ -404,7 +412,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty Nothing -> evalError (pp "[list: .. | ..] requires an argument") (t,ty) <- tcRho scope c2 t mb_ty case ty of - VApp c qid [] -> return (Reset ctl mb_ct t qid, ty) + VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") tcRho scope s (Opts n cs) mb_ty = do diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs index 0300b19a8..c2ad8660a 100644 --- a/src/compiler/api/GF/Grammar/Grammar.hs +++ b/src/compiler/api/GF/Grammar/Grammar.hs @@ -399,7 +399,7 @@ data Term = | FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@ | Markup Ident [(Ident,Term)] [Term] - | Reset Ident (Maybe Term) Term QIdent + | Reset Ident (Maybe Term) Term (Maybe QIdent) | Alts Term [(Term, Term)] -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@ | Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@ diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y index c81724d24..9167e5c1c 100644 --- a/src/compiler/api/GF/Grammar/Parser.y +++ b/src/compiler/api/GF/Grammar/Parser.y @@ -487,8 +487,8 @@ Exp6 | '{' ListLocDef '}' {% mkR $2 } | '<' ListTupleComp '>' { R (tuple2record $2) } | '<' Exp ':' Exp '>' { Typed $2 $4 } - | '[' Control '|' Tag ']' { Reset (fst $2) (snd $2) $4 undefined } - | '[' Control '|' Exp ']' { Reset (fst $2) (snd $2) $4 undefined } + | '[' Control '|' Tag ']' { Reset (fst $2) (snd $2) $4 Nothing } + | '[' Control '|' Exp ']' { Reset (fst $2) (snd $2) $4 Nothing } | '(' Exp ')' { $2 } ListExp :: { [Term] }