added overload resolution in the experimental type checker

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)