From 9c038ceb7c5dda39e0e8ad935e22e624eedee6d7 Mon Sep 17 00:00:00 2001 From: Krasimir Angelov Date: Thu, 22 May 2025 11:48:21 +0200 Subject: [PATCH] more updates to get English compile --- .../api/GF/Compile/Compute/Concrete2.hs | 18 +-- .../api/GF/Compile/TypeCheck/Concrete.hs | 119 +++++++++++------- src/compiler/api/GF/Grammar/Printer.hs | 1 + 3 files changed, 84 insertions(+), 54 deletions(-) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs index 6c2639740..fdb9a2cf4 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs @@ -348,7 +348,8 @@ evalPredef g@(Gl gr pds) c n args = stdPredef :: Globals -> PredefTable stdPredef g = Map.fromList - [(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v)) + [(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts (Just i) (Just i); vs -> VApp c (cPredef,cInts) vs})) + ,(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v)) ,(cTake, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2))) ,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2))) ,(cTk, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2))) @@ -972,9 +973,9 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do listify mn cat (t1:ts) = do t2 <- listify mn cat ts return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2) value2termM flat xs (VError msg) = evalError msg -value2termM flat xs (VInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0)) -value2termM flat xs (VInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min)) -value2termM flat xs (VInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max)) +value2termM flat xs (VInts Nothing Nothing) = return (App (Q (cPredef,cInts)) (Meta 0)) +value2termM flat xs (VInts (Just min) Nothing) = return (App (Q (cPredef,cInts)) (EInt min)) +value2termM flat xs (VInts _ (Just max)) = return (App (Q (cPredef,cInts)) (EInt max)) value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v) @@ -995,7 +996,10 @@ ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs)) ppValue q d (VGen _ _) = pp "VGen" ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]" -ppValue q d (VProd _ _ _ _) = pp "VProd" +ppValue q d (VProd bt x a b) = + if x == identW && bt == Explicit + then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b) + else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b) ppValue q d (VRecType xs) | q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of [cat] -> pp cat @@ -1032,9 +1036,7 @@ ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg))) ppValue q d (VInts Nothing Nothing) = prec d 4 (pp "Ints ?") ppValue q d (VInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> "..")) ppValue q d (VInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max)) -ppValue q d (VInts (Just min) (Just max)) - | min == max = prec d 4 (pp "Ints" <+> min) - | otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max)) +ppValue q d (VInts (Just min) (Just max)) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max)) ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs index ce9ea1add..5b55826ff 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs @@ -13,7 +13,7 @@ import GF.Grammar.Lockfield import GF.Compile.Compute.Concrete2 import GF.Infra.CheckM import GF.Data.ErrM ( Err(Ok, Bad) ) -import Control.Applicative(Applicative(..)) +import Control.Applicative(Applicative(..),(<|>)) import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) import Control.Monad.ST import GF.Text.Pretty @@ -68,7 +68,6 @@ inferSigma scope s t = do -- GEN1 vtypeInt = VApp poison (cPredef,cInt) [] vtypeFloat = VApp poison (cPredef,cFloat) [] -vtypeInts i= VApp poison (cPredef,cInts) [VInt i] vtypeStr = VSort cStr vtypeStrs = VSort cStrs vtypeType = VSort cType @@ -76,7 +75,7 @@ vtypePType = VSort cPType vtypeMarkup= VApp poison (cPredef,cMarkup) [] tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho) -tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT +tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (VInts (Just i) Nothing) mb_ty -- INT tcRho scope s t@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty @@ -328,14 +327,38 @@ tcRho scope c t@(ExtR t1 t2) mb_ty = do let (c1,c2,c3,c4) = split4 c (t1,t1_ty) <- tcRho scope c1 t1 Nothing (t2,t2_ty) <- tcRho scope c2 t2 Nothing - case (t1_ty,t2_ty) of - (VSort s1,VSort s2) + ty <- join t1_ty t2_ty + instSigma scope c3 (ExtR t1 t2) ty mb_ty + where + join (VMeta i vs) ty2 = do + mv <- getMeta i + case mv of + Bound _ v -> do + g <- globals + join (apply g v vs) ty2 + Residuation _ (Just ctr) -> do + g <- globals + join (apply g ctr vs) ty2 + join ty1 (VMeta j vs) = do + mv <- getMeta j + case mv of + Bound _ v -> do + g <- globals + join ty1 (apply g v vs) + Residuation _ (Just ctr) -> do + g <- globals + join ty1 (apply g ctr vs) + join (VSort s1) (VSort s2) | (s1 == cType || s1 == cPType) && - (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType - | otherwise = cType - in instSigma scope c3 (ExtR t1 t2) (VSort sort) mb_ty - (VRecType rs1, VRecType rs2) -> instSigma scope c3 (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty - _ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t) + (s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType + | otherwise = cType + in return (VSort sort) + join ty1@(VRecType _) ty2@(VRecType _) = subtype scope (Just ty1) ty2 + join ty1 ty2 = do ty1 <- value2termM False (scopeVars scope) ty1 + ty2 <- value2termM False (scopeVars scope) ty2 + evalError ("Cannot type check" <+> ppTerm Unqualified 0 t $$ + " with types" <+> (ppTerm Unqualified 0 ty1 $$ + ppTerm Unqualified 0 ty2)) tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser @@ -590,7 +613,7 @@ tcPatt scope c (PP q ps) ty0 = do unify scope ty0 ty return scope tcPatt scope c (PInt i) ty0 = do - subsCheckRho scope (EInt i) (vtypeInts i) ty0 + subsCheckRho scope (EInt i) (VInts (Just i) Nothing) ty0 return scope tcPatt scope c (PString s) ty0 = do unify scope ty0 vtypeStr @@ -778,35 +801,31 @@ subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE | s1 == cPType && s2 == cType = return t subsCheckRho scope t (VApp _ p1 []) rho2 -- for backwards compatibility | p1 == (cPredef,cErrorType) = return t -subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- This is not correct but there is in the RGL nextPrec relies on it. - | p1 == (cPredef,cInt) && p2 == (cPredef,cInts) = return t -- Should be only a temporary hack. -subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t -subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do - if i <= j - then return t - else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) +subsCheckRho scope t (VApp _ p _) (VInts _ _) -- This is not correct but nextPrec in the RGL relies on it. + | p == (cPredef,cInt) = return t -- Should be only a temporary hack. +subsCheckRho scope t (VInts _ _) (VApp _ p _) -- Rule INT1 + | p == (cPredef,cInt) = return t +subsCheckRho scope t ty1@(VInts min1 max1) ty2@(VInts min2 max2) -- Rule INT2 + | i <= j = return t + | otherwise = evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) + where + i = fromMaybe 0 (max1 <|> min1) + j = fromMaybe 0 (min2 <|> max2) subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC let mkAccess scope t = case t of - ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 - (scope,mkProj2,mkWrap2) <- mkAccess scope t2 - return (scope - ,\l -> mkProj2 l `mplus` mkProj1 l - ,mkWrap1 . mkWrap2 - ) + ExtR t1 (R rs) -> + do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 + sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] + return (scope + ,\l -> lookup l rs `mplus` mkProj1 l + ,mkWrap1 + ) R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] return (scope ,\l -> lookup l rs ,id ) - Vr x -> do return (scope - ,\l -> do VRecType rs <- lookup x scope - ty <- lookup3 l rs - return (Nothing,P t l) - ,id - ) t -> let x = newVar scope in return (((x,ty1):scope) ,\l -> return (Nothing,P (Vr x) l) @@ -863,12 +882,16 @@ subsCheckTbl scope t p1 r1 p2 r2 = do p2 <- value2termM True (scopeVars scope) p2 return (T (TTyped p2) [(PV x,t)]) -subtype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VInts Nothing (Just i)) -subtype scope (Just (VInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VInts j (Just (maybe k (min k) i))) +subtype scope (Just (VInts i1 j1)) (VInts i2 j2) = + case VInts (lift max i1 i2) (lift min j1 j2) of + ty@(VInts (Just i) (Just j)) + | i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type") + ty -> return ty + where + lift f Nothing Nothing = Nothing + lift f (Just x) Nothing = Just x + lift f Nothing (Just y) = Just y + lift f (Just x) (Just y) = Just (f x y) subtype scope Nothing (VRecType ltys) = do lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys return (VRecType lctrs) @@ -897,12 +920,16 @@ subtype scope (Just ctr) ty = do unify scope ctr ty return ty -supertype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VInts (Just i) Nothing) -supertype scope (Just (VInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VInts (Just (maybe k (max k) i)) j) +supertype scope (Just (VInts i1 j1)) (VInts i2 j2) = + case VInts (lift min i1 i2) (lift max j1 j2) of + ty@(VInts (Just i) (Just j)) + | i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type") + ty -> return ty + where + lift f Nothing Nothing = Nothing + lift f (Just x) Nothing = Nothing + lift f Nothing (Just y) = Nothing + lift f (Just x) (Just y) = Just (f x y) supertype scope Nothing (VRecType ltys) = do lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys return (VRecType lctrs) @@ -1009,8 +1036,8 @@ unify scope VEmpty VEmpty = return () unify scope v1 v2 = do t1 <- value2termM False (scopeVars scope) v1 t2 <- value2termM False (scopeVars scope) v2 - evalError ("Cannot unify:" <+> ppTerm Terse 0 t1 $$ - " with:" <+> ppTerm Terse 0 t2) + evalError ("Cannot unify:" <+> ppValue Terse 0 v1 $$ + " with:" <+> ppValue Terse 0 v2) -- | Invariant: tv1 is a flexible type variable diff --git a/src/compiler/api/GF/Grammar/Printer.hs b/src/compiler/api/GF/Grammar/Printer.hs index 3f7364bbb..e9947b494 100644 --- a/src/compiler/api/GF/Grammar/Printer.hs +++ b/src/compiler/api/GF/Grammar/Printer.hs @@ -17,6 +17,7 @@ module GF.Grammar.Printer , ppTerm , ppPatt , ppValue + , ppBind , ppConstrs , ppQIdent , ppMeta