GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-08-19 10:46:22 -06:00
Code Issues Packages Projects Releases Wiki Activity

switch to using the new type checker by default

Browse Source
This commit is contained in:
Krasimir Angelov
2025-05-18 07:20:12 +02:00
parent e54f748efa
commit 3a1990fd1d
7 changed files with 56 additions and 48 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/compiler/api/GF/Command/SourceCommands.hs
+3 -3
View File
@@ -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]
src/compiler/api/GF/Compile/CheckGrammar.hs
+20 -18
View File
@@ -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)
src/compiler/api/GF/Compile/Compute/Concrete2.hs
+4 -4
View File
@@ -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)
src/compiler/api/GF/Compile/Repl.hs
+6 -8
View File
@@ -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 _) ->
src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+20 -12
View File
@@ -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
src/compiler/api/GF/Grammar/Grammar.hs
+1 -1
View File
@@ -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 ; ...}@
src/compiler/api/GF/Grammar/Parser.y
+2 -2
View File
@@ -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] }