msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

The typechecker is still unfinished but at least it can typecheck the English resource grammar

Browse Source
This commit is contained in:
kr.angelov
2011-12-02 12:33:26 +00:00
parent 9baa13476a
commit c52f05ed46
3 changed files with 114 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
src/compiler/GF/Compile/CheckGrammar.hs
View File

@@ -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)) ->

21
src/compiler/GF/Compile/Compute/ConcreteNew.hs
View File

@@ -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

97
src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -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 ()