diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs index b5d288cc8..d66fdad71 100644 --- a/src/compiler/GF/Compile/CheckGrammar.hs +++ b/src/compiler/GF/Compile/CheckGrammar.hs @@ -174,10 +174,14 @@ checkInfo opts ms (m,mo) c info = do CncCat mty mdef mpr mpmcfg -> do mty <- case mty of - Just (L loc typ) -> chIn loc "linearization type of" $ do - (typ,_) <- checkLType gr [] typ typeType - typ <- computeLType gr [] typ - return (Just (L loc typ)) + Just (L loc typ) -> chIn loc "linearization type of" $ + (if flag optNewComp opts + then do (typ,_) <- CN.checkLType gr typ typeType + typ <- computeLType gr [] typ + return (Just (L loc typ)) + else do (typ,_) <- checkLType gr [] typ typeType + typ <- computeLType gr [] typ + return (Just (L loc typ))) Nothing -> return Nothing mdef <- case (mty,mdef) of (Just (L _ typ),Just (L loc def)) -> diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs index f6f76e5c2..e61a12a22 100644 --- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs +++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs @@ -7,6 +7,9 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType) import GF.Grammar.Lookup import GF.Grammar.Predef import GF.Data.Operations +import Data.List (intersect) +import Text.PrettyPrint +import qualified Data.ByteString.Char8 as BS normalForm :: SourceGrammar -> Term -> Term normalForm gr t = value2term gr [] (eval gr [] t) @@ -40,6 +43,9 @@ eval gr env (Vr x) = case lookup x env of Just v -> v Nothing -> error ("Unknown variable "++showIdent x) eval gr env (Q x) + | x == (cPredef,cErrorType) -- to be removed + = let varP = identC (BS.pack "P") + in eval gr [] (mkProd [(Implicit,varP,typeType)] (Vr varP) []) | fst x == cPredef = VApp x [] | otherwise = case lookupResDef gr x of Ok t -> eval gr [] t @@ -53,16 +59,29 @@ eval gr env (EInt n) = VInt n eval gr env (EFloat f) = VFloat f eval gr env (K s) = VString s eval gr env Empty = VString "" -eval gr env (Sort s) = VSort s +eval gr env (Sort s) + | s == cTok = VSort cStr -- to be removed + | otherwise = VSort s eval gr env (ImplArg t) = VImplArg (eval gr env t) eval gr env (Table p res) = VTblType (eval gr env p) (eval gr env res) eval gr env (RecType rs) = VRecType [(l,eval gr env ty) | (l,ty) <- rs] +eval gr env t@(ExtR t1 t2) = + let error = VError (show (text "The term" <+> ppTerm Unqualified 0 t <+> text "is not reducible")) + in case (eval gr env t1, eval gr env t2) of + (VRecType rs1, VRecType rs2) -> case intersect (map fst rs1) (map fst rs2) of + [] -> VRecType (rs1 ++ rs2) + _ -> error + (VRec rs1, VRec rs2) -> case intersect (map fst rs1) (map fst rs2) of + [] -> VRec (rs1 ++ rs2) + _ -> error + _ -> error eval gr env t = error ("eval "++show t) apply gr env t [] = eval gr env t apply gr env (Q x) vs = case lookupResDef gr x of Ok t -> apply gr [] t vs Bad err -> error err +apply gr env (App t1 t2) vs = apply gr env t1 (eval gr env t2 : vs) apply gr env (Abs b x t) (v:vs) = case (b,v) of (Implicit,VImplArg v) -> apply gr ((x,v):env) t vs (Explicit, v) -> apply gr ((x,v):env) t vs diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 8fd196f87..4ece28cda 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -3,6 +3,7 @@ module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where import GF.Grammar hiding (Env, VGen, VApp, VRecType) import GF.Grammar.Lookup import GF.Grammar.Predef +import GF.Grammar.Lockfield import GF.Compile.Compute.ConcreteNew import GF.Compile.Compute.AppPredefined import GF.Infra.CheckM @@ -86,7 +87,17 @@ tcRho gr scope (Abs bt var body) (Just ty) = do -- ABS2 (var_ty, body_ty) <- unifyFun gr scope (VGen (length scope) []) ty (body, body_ty) <- tcRho gr ((var,var_ty):scope) body (Just body_ty) return (Abs bt var body,ty) +tcRho gr scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do -- LET + (rhs,var_ty) <- case mb_ann_ty of + Nothing -> inferSigma gr scope rhs + Just ann_ty -> do (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) + let v_ann_ty = eval gr (scopeEnv scope) ann_ty + rhs <- checkSigma gr scope rhs v_ann_ty + return (rhs, v_ann_ty) + (body, body_ty) <- tcRho gr ((var,var_ty):scope) body mb_ty + return (Let (var, (Just (value2term gr (scopeVars scope) var_ty), rhs)) body, body_ty) tcRho gr scope (Typed body ann_ty) mb_ty = do -- ANNOT + (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) let v_ann_ty = eval gr (scopeEnv scope) ann_ty body <- checkSigma gr scope body v_ann_ty instSigma gr scope (Typed body ann_ty) v_ann_ty mb_ty @@ -127,7 +138,8 @@ tcRho gr scope (S t p) mb_ty = do tcRho gr scope (T tt ps) mb_ty = do p_ty <- case tt of TRaw -> fmap Meta $ newMeta (eval gr [] typePType) - TTyped ty -> return ty + TTyped ty -> do (ty, _) <- tcRho gr scope ty (Just (eval gr [] typeType)) + return ty res_ty <- fmap Meta $ newMeta (eval gr [] typeType) ps <- mapM (tcCase gr scope (eval gr (scopeEnv scope) p_ty) (eval gr (scopeEnv scope) res_ty)) ps instSigma gr scope (T (TTyped p_ty) ps) (eval gr (scopeEnv scope) (Table p_ty res_ty)) mb_ty @@ -136,6 +148,7 @@ tcRho gr scope t@(R rs) mb_ty = do Nothing -> inferRecFields gr scope rs Just ty -> case ty of VRecType ltys -> checkRecFields gr scope rs ltys + VMeta _ _ _ -> inferRecFields gr scope rs _ -> tcError (text "Record type is inferred but:" $$ nest 2 (ppTerm Unqualified 0 (value2term gr (scopeVars scope) ty)) $$ text "is expected in the expresion:" $$ @@ -154,6 +167,36 @@ tcRho gr scope (C t1 t2) mb_ty = do (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr)) instSigma gr scope (C t1 t2) (eval gr [] typeStr) mb_ty +tcRho gr scope (Glue t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) + (t2,t2_ty) <- tcRho gr scope t2 (Just (eval gr [] typeStr)) + instSigma gr scope (Glue t1 t2) (eval gr [] typeStr) mb_ty +tcRho gr scope t@(ExtR t1 t2) mb_ty = do + (t1,t1_ty) <- tcRho gr scope t1 Nothing + (t2,t2_ty) <- tcRho gr scope t2 Nothing + case (t1_ty,t2_ty) of + (VSort s1,VSort s2) + | s1 == cType && s2 == cType -> instSigma gr scope (ExtR t1 t2) (VSort cType) mb_ty + (VRecType rs1, VRecType rs2) + | otherwise -> do tcWarn (text "bbbb") + instSigma gr scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty + _ -> tcError (text "Cannot type check" <+> ppTerm Unqualified 0 t) +tcRho gr scope (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho gr scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho gr scope (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho gr scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho gr scope (Alts t ss) mb_ty = do + (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr)) + ss <- flip mapM ss $ \(t1,t2) -> do + (t1,_) <- tcRho gr scope t1 (Just (eval gr [] typeStr)) + (t2,_) <- tcRho gr scope t2 (Just (eval gr [] typeStrs)) + return (t1,t2) + instSigma gr scope (Alts t ss) (eval gr [] typeStr) mb_ty +tcRho gr scope (Strs ss) mb_ty = do + ss <- flip mapM ss $ \t -> do + (t,_) <- tcRho gr scope t (Just (eval gr [] typeStr)) + return t + instSigma gr scope (Strs ss) (eval gr [] typeStrs) mb_ty tcRho gr scope t _ = error ("tcRho "++show t) tcCase gr scope p_ty res_ty (p,t) = do @@ -167,9 +210,41 @@ tcPatt gr scope (PV x) ty0 = return ((x,ty0):scope) tcPatt gr scope (PP c ps) ty0 = case lookupResType gr c of - Ok ty -> do unify gr scope ty0 (eval gr [] ty) + Ok ty -> do let go scope ty [] = return (scope,ty) + go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun gr scope (VGen (length scope) []) ty + scope <- tcPatt gr scope p arg_ty + go scope res_ty ps + (scope,ty) <- go scope (eval gr [] ty) ps + unify gr scope ty0 ty return scope Bad err -> tcError (text err) +tcPatt gr scope (PString s) ty0 = do + unify gr scope ty0 (eval gr [] typeStr) + return scope +tcPatt gr scope PChar ty0 = do + unify gr scope ty0 (eval gr [] typeStr) + return scope +tcPatt gr scope (PSeq p1 p2) ty0 = do + unify gr scope ty0 (eval gr [] typeStr) + scope <- tcPatt gr scope p1 (eval gr [] typeStr) + scope <- tcPatt gr scope p2 (eval gr [] typeStr) + return scope +tcPatt gr scope (PAs x p) ty0 = do + tcPatt gr ((x,ty0):scope) p ty0 +tcPatt gr scope (PR rs) ty0 = do + let go scope [] = return (scope,[]) + go scope ((l,p):rs) = do i <- newMeta (eval gr [] typePType) + let ty = VMeta i (scopeEnv scope) [] + scope <- tcPatt gr scope p ty + (scope,rs) <- go scope rs + return (scope,(l,ty) : rs) + (scope',rs) <- go scope rs + unify gr scope ty0 (VRecType rs) + return scope' +tcPatt gr scope (PAlt p1 p2) ty0 = do + tcPatt gr scope p1 ty0 + tcPatt gr scope p2 ty0 + return scope tcPatt gr scope p ty = error ("tcPatt "++show p) @@ -178,13 +253,13 @@ inferRecFields gr scope rs = checkRecFields gr scope [] ltys | null ltys = return [] - | otherwise = tcError (hsep (map (ppLabel . fst) ltys)) + | otherwise = tcError (text "Missing fields:" <+> hsep (map (ppLabel . fst) ltys)) checkRecFields gr scope ((l,t):lts) ltys = case takeIt l ltys of (Just ty,ltys) -> do ltty <- tcRecField gr scope l t (Just ty) lttys <- checkRecFields gr scope lts ltys return (ltty : lttys) - (Nothing,ltys) -> do tcWarn (ppLabel l) + (Nothing,ltys) -> do tcWarn (text "Discarded field:" <+> ppLabel l) ltty <- tcRecField gr scope l t Nothing lttys <- checkRecFields gr scope lts ltys return lttys -- ignore the field @@ -197,7 +272,8 @@ checkRecFields gr scope ((l,t):lts) ltys = tcRecField gr scope l (mb_ann_ty,t) mb_ty = do (t,ty) <- case mb_ann_ty of - Just ann_ty -> do let v_ann_ty = eval gr (scopeEnv scope) ann_ty + Just ann_ty -> do (ann_ty, _) <- tcRho gr scope ann_ty (Just (eval gr [] typeType)) + let v_ann_ty = eval gr (scopeEnv scope) ann_ty t <- checkSigma gr scope t v_ann_ty instSigma gr scope t v_ann_ty mb_ty Nothing -> tcRho gr scope t mb_ty @@ -242,7 +318,6 @@ subsCheckRho gr scope t (VClosure env (Prod Explicit _ a1 r1)) rho2 = do subsCheckFun gr scope t (eval gr env a1) (eval gr env r1) a2 r2 subsCheckRho gr scope t (VSort s1) (VSort s2) | s1 == cPType && s2 == cType = return t - | s1 == cTok && s2 == cStr = return t subsCheckRho gr scope t tau1 tau2 = do -- Rule MONO unify gr scope tau1 tau2 -- Revert to ordinary unification return t @@ -287,12 +362,12 @@ unify gr scope (VTblType p1 res1) (VTblType p2 res2) = do unify gr scope p1 p2 unify gr scope res1 res2 unify gr scope (VRecType rs1) (VRecType rs2) = do - tcWarn (text "aaaa") + sequence_ [unify gr scope ty1 ty2 | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]] unify gr scope v1 v2 = do - v1 <- zonkTerm (value2term gr (scopeVars scope) v1) - v2 <- zonkTerm (value2term gr (scopeVars scope) v2) - tcError (text "Cannot unify types:" <+> (ppTerm Unqualified 0 v1 $$ - ppTerm Unqualified 0 v2)) + t1 <- zonkTerm (value2term gr (scopeVars scope) v1) + t2 <- zonkTerm (value2term gr (scopeVars scope) v2) + tcError (text "Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$ + ppTerm Unqualified 0 t2)) -- | Invariant: tv1 is a flexible type variable unifyVar :: SourceGrammar -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()