From ad2a18592bc23bdadb2c068bc7af211576c67d0b Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 6 Mar 2017 14:09:16 +0000 Subject: [PATCH] added overload resolution in the experimental type checker --- .../GF/Compile/TypeCheck/ConcreteNew.hs | 101 +++++++++++++----- src/compiler/GF/Grammar/Lookup.hs | 23 ++++ 2 files changed, 98 insertions(+), 26 deletions(-) diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs index 69ba41708..25f4e9c19 100644 --- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs +++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs @@ -59,32 +59,18 @@ tcRho ge scope t@(Vr v) mb_ty = do -- VAR case lookup v scope of Just v_sigma -> instSigma ge scope t v_sigma mb_ty Nothing -> tcError ("Unknown variable" <+> v) -tcRho ge scope t@(Q id) mb_ty = -- VAR (global) - case lookupResType (geGrammar ge) id of - Ok ty -> do vty <- liftErr (eval ge [] ty) - instSigma ge scope t vty mb_ty - Bad err -> tcError (pp err) -tcRho ge scope t@(QC id) mb_ty = -- VAR (global) - case lookupResType (geGrammar ge) id of - Ok ty -> do vty <- liftErr (eval ge [] ty) - instSigma ge scope t vty mb_ty - Bad err -> tcError (pp err) -tcRho ge scope t@(App fun (ImplArg arg)) mb_ty = do -- APP1 - (fun,fun_ty) <- tcRho ge scope fun Nothing - (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty - if (bt == Implicit) - then return () - else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - instSigma ge scope (App fun (ImplArg arg)) (res_ty varg) mb_ty -tcRho ge scope (App fun arg) mb_ty = do -- APP2 - (fun,fun_ty) <- tcRho ge scope fun Nothing - (fun,fun_ty) <- instantiate scope fun fun_ty - (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty - (arg,_) <- tcRho ge scope arg (Just arg_ty) - varg <- liftErr (eval ge (scopeEnv scope) arg) - instSigma ge scope (App fun arg) (res_ty varg) mb_ty +tcRho ge scope t@(Q id) mb_ty = + runTcA (tcOverloadFailed t) $ + tcApp ge scope t `bindTcA` \(t,ty) -> + instSigma ge scope t ty mb_ty +tcRho ge scope t@(QC id) mb_ty = + runTcA (tcOverloadFailed t) $ + tcApp ge scope t `bindTcA` \(t,ty) -> + instSigma ge scope t ty mb_ty +tcRho ge scope t@(App fun arg) mb_ty = do + runTcA (tcOverloadFailed t) $ + tcApp ge scope t `bindTcA` \(t,ty) -> + instSigma ge scope t ty mb_ty tcRho ge scope (Abs bt var body) Nothing = do -- ABS1 i <- newMeta scope vtypeType let arg_ty = VMeta i (scopeEnv scope) [] @@ -258,6 +244,39 @@ tcCases ge scope ((p,t):cs) p_ty mb_res_ty = do (cs,mb_res_ty) <- tcCases ge scope cs p_ty (Just res_ty) return ((p,t):cs,mb_res_ty) + +tcApp ge scope t@(App fun (ImplArg arg)) = do -- APP1 + tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> + do (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty + if (bt == Implicit) + then return () + else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected") + (arg,_) <- tcRho ge scope arg (Just arg_ty) + varg <- liftErr (eval ge (scopeEnv scope) arg) + return (App fun (ImplArg arg), res_ty varg) +tcApp ge scope (App fun arg) = -- APP2 + tcApp ge scope fun `bindTcA` \(fun,fun_ty) -> + do (fun,fun_ty) <- instantiate scope fun fun_ty + (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty + (arg,_) <- tcRho ge scope arg (Just arg_ty) + varg <- liftErr (eval ge (scopeEnv scope) arg) + return (App fun arg, res_ty varg) +tcApp ge scope (Q id) = -- VAR (global) + mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> + do ty <- liftErr (eval ge [] ty) + return (t,ty) +tcApp ge scope (QC id) = -- VAR (global) + mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> + do ty <- liftErr (eval ge [] ty) + return (t,ty) + + +tcOverloadFailed t ttys = + tcError ("Overload resolution failed" $$ + "term " <+> pp t $$ + "types" <+> vcat [pp ty | (_,ty) <- ttys]) + + tcPatt ge scope PW ty0 = return scope tcPatt ge scope (PV x) ty0 = @@ -623,6 +642,7 @@ tcWarn msg = TcM (\ms msgs -> TcOk () ms (msg : msgs)) unimplemented str = fail ("Unimplemented: "++str) + runTcM :: TcM a -> Check a runTcM f = case unTcM f IntMap.empty [] of TcOk x _ msgs -> do checkWarnings msgs; return x @@ -709,3 +729,32 @@ tc_value2term loc xs v = case value2term loc xs v of Left i -> tcError ("Variable #" <+> pp i <+> "has escaped") Right t -> return t + + + +data TcA x a + = TcSingle (MetaStore -> [Message] -> TcResult a) + | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])]) + +mkTcA :: Err [a] -> TcA a a +mkTcA f = case f of + Bad msg -> TcSingle (\ms msgs -> TcFail (pp msg : msgs)) + Ok [x] -> TcSingle (\ms msgs -> TcOk x ms msgs) + Ok xs -> TcMany xs (\ms msgs -> [(x,ms,msgs) | x <- xs]) + +bindTcA :: TcA x a -> (a -> TcM b) -> TcA x b +bindTcA f g = case f of + TcSingle f -> TcSingle (unTcM (TcM f >>= g)) + TcMany xs f -> TcMany xs (\ms msgs -> foldr add [] (f ms msgs)) + where + add (y,ms,msgs) rs = + case unTcM (g y) ms msgs of + TcFail _ -> rs + TcOk y ms msgs -> (y,ms,msgs):rs + +runTcA :: ([x] -> TcM a) -> TcA x a -> TcM a +runTcA g f = TcM (\ms msgs -> case f of + TcMany xs f -> case f ms msgs of + [(x,ms,msgs)] -> TcOk x ms msgs + rs -> unTcM (g xs) ms msgs + TcSingle f -> f ms msgs) diff --git a/src/compiler/GF/Grammar/Lookup.hs b/src/compiler/GF/Grammar/Lookup.hs index fbab56499..9435d1ec4 100644 --- a/src/compiler/GF/Grammar/Lookup.hs +++ b/src/compiler/GF/Grammar/Lookup.hs @@ -22,6 +22,7 @@ module GF.Grammar.Lookup ( lookupResDef, lookupResDefLoc, lookupResType, lookupOverload, + lookupOverloadTypes, lookupParamValues, allParamValues, lookupAbsDef, @@ -101,6 +102,28 @@ lookupResType gr (m,c) = do ResValue (L _ t) -> return t _ -> raise $ render (c <+> "has no type defined in resource" <+> m) +lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)] +lookupOverloadTypes gr id@(m,c) = do + info <- lookupQIdentInfo gr (m,c) + case info of + ResOper (Just (L _ ty)) _ -> ret ty + + -- used in reused concrete + CncCat _ _ _ _ _ -> ret typeType + CncFun (Just (cat,cont,val)) _ _ _ -> do + val' <- lock cat val + ret $ mkProd cont val' [] + ResParam _ _ -> ret typePType + ResValue (L _ t) -> ret t + ResOverload os tysts -> do + tss <- mapM (\x -> lookupOverloadTypes gr (x,c)) os + return $ [(tr,ty) | (L _ ty,L _ tr) <- tysts] ++ + concat tss + AnyInd _ n -> lookupOverloadTypes gr (n,c) + _ -> raise $ render (c <+> "has no types defined in resource" <+> m) + where + ret ty = return [(Q id,ty)] + lookupOverload :: ErrorMonad m => Grammar -> QIdent -> m [([Type],(Type,Term))] lookupOverload gr (m,c) = do info <- lookupQIdentInfo gr (m,c)