small refactoring in GF.Compile.CheckGrammar

4 files changed, 80 insertions, 109 deletions

diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index 520a7adbf..d315ba098 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -45,28 +45,17 @@ import Text.PrettyPrint
 
 -- | checking is performed in the dependency order of modules
 checkModule :: [SourceModule] -> SourceModule -> Check SourceModule
-checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
-    let js = jments mo
-    checkRestrictedInheritance ms (name, mo)
-    js' <- case mtype mo of
-      MTAbstract -> checkMap (checkAbsInfo gr name mo) js
-
-      MTResource -> checkMap (checkResInfo gr name mo) js
-
-      MTConcrete a -> do
-        checkErr $ topoSortOpers $ allOperDependencies name js
-        abs <- checkErr $ lookupModule gr a
-        js1 <- checkCompleteGrammar gr abs mo
-        checkMap (checkCncInfo gr name mo (a,abs)) js1
-
-      MTInterface -> checkMap (checkResInfo gr name mo) js
-
-      MTInstance a -> do
-        checkMap (checkResInfo gr name mo) js
-
-    return (name, replaceJudgements mo js')
- where
-   gr  = MGrammar $ (name,mo):ms
+checkModule ms m@(name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
+  checkRestrictedInheritance ms m
+  js <- case mtype mo of
+          MTConcrete a -> do checkErr $ topoSortOpers $ allOperDependencies name (jments mo)
+                             abs <- checkErr $ lookupModule gr a
+                             checkCompleteGrammar gr (a,abs) m
+          _            -> return (jments mo)
+  js <- checkMap (checkInfo gr m) js
+  return (name, replaceJudgements mo js)
+  where
+    gr  = MGrammar $ (name,mo):ms
 
 -- check if restricted inheritance modules are still coherent
 -- i.e. that the defs of remaining names don't depend on omitted names
@@ -89,42 +78,8 @@ checkRestrictedInheritance mos (name,mo) = do
                          nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs]))
    allDeps = concatMap (allDependencies (const True) . jments . snd) mos
 
-checkAbsInfo :: 
-  SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
-checkAbsInfo st m mo c info = do
- checkReservedId c
- case info of
-   AbsCat (Just cont) _ -> mkCheck "category" $ 
-     checkContext st cont ---- also cstrs
-   AbsFun (Just typ0) ma md -> do
-     typ <- compAbsTyp [] typ0   -- to calculate let definitions
-     mkCheck "type of function" $
-       checkTyp st typ
-     case md of
-       Just eqs -> mkCheck "definition of function" $
-	             checkDef st (m,c) typ eqs
-       Nothing  -> return info
-     return $ (AbsFun (Just typ) ma md)
-   _ -> return info
- where
-   mkCheck cat ss = case ss of
-     [] -> return info
-     _  -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
-
-   compAbsTyp g t = case t of
-     Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
-     Let (x,(_,a)) b -> do
-       a' <- compAbsTyp g a
-       compAbsTyp ((x, a'):g) b
-     Prod b x a t -> do
-       a' <- compAbsTyp g a
-       t' <- compAbsTyp ((x,Vr x):g) t
-       return $ Prod b x a' t'
-     Abs _ _ _ -> return t
-     _ -> composOp (compAbsTyp g) t
-
-checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info)
-checkCompleteGrammar gr abs cnc = do
+checkCompleteGrammar :: SourceGrammar -> SourceModule -> SourceModule -> Check (BinTree Ident Info)
+checkCompleteGrammar gr (am,abs) (cm,cnc) = do
   let jsa = jments abs
   let fsa = tree2list jsa
   let jsc = jments cnc
@@ -154,16 +109,21 @@ checkCompleteGrammar gr abs cnc = do
                                       case info of
                                         CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
                                         _                              -> Bad "no def lin"
+                                             
+                                (cont,val) <- linTypeOfType gr cm ty
+                                let linty = (snd (valCat ty),cont,val)
+
                                 case lookupIdent c js of
-                                  Ok (CncFun _   (Just _) _ ) -> return js
-                                  Ok (CncFun cty Nothing  pn) ->
+                                  Ok (CncFun _ (Just def) pn) -> 
+                                                return $ updateTree (c,CncFun (Just linty) (Just def) pn) js
+                                  Ok (CncFun _ Nothing    pn) ->
                                     case mb_def of
-                                      Ok def -> return $ updateTree (c,CncFun cty (Just def) pn) js
+                                      Ok def -> return $ updateTree (c,CncFun (Just linty) (Just def) pn) js
                                       Bad _  -> do checkWarn $ text "no linearization of" <+> ppIdent c
                                                    return js
                                   _ -> do
                                     case mb_def of
-                                      Ok def -> return $ updateTree (c,CncFun Nothing (Just def) Nothing) js
+                                      Ok def -> return $ updateTree (c,CncFun (Just linty) (Just def) Nothing) js
                                       Bad _  -> do checkWarn $ text "no linearization of" <+> ppIdent c
                                                    return js
      AbsCat (Just _) _ -> case lookupIdent c js of
@@ -181,10 +141,38 @@ checkCompleteGrammar gr abs cnc = do
 
 -- | General Principle: only Just-values are checked. 
 -- A May-value has always been checked in its origin module.
-checkResInfo :: SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
-checkResInfo gr mo mm c info = do
+checkInfo :: SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
+checkInfo gr (m,mo) c info = do
   checkReservedId c
   case info of
+    AbsCat (Just cont) _ -> mkCheck "category" $ 
+      checkContext gr cont
+
+    AbsFun (Just typ0) ma md -> do
+      typ <- compAbsTyp [] typ0   -- to calculate let definitions
+      mkCheck "type of function" $
+        checkTyp gr typ
+      case md of
+        Just eqs -> mkCheck "definition of function" $
+	                  checkDef gr (m,c) typ eqs
+        Nothing  -> return info
+      return (AbsFun (Just typ) ma md)
+
+    CncFun linty@(Just (cat,cont,val)) (Just trm) mpr -> chIn "linearization of" $ do
+      (trm',_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
+      mpr <- checkPrintname gr mpr
+      return (CncFun linty (Just trm') mpr)
+
+    CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
+      typ'  <- computeLType gr [] typ
+      mdef' <- case mdef of
+        Just def -> do
+          (def',_) <- checkLType gr [] def (mkFunType [typeStr] typ)
+          return $ Just def'
+        _ -> return mdef
+      mpr <- checkPrintname gr mpr
+      return (CncCat (Just typ') mdef' mpr)
+
     ResOper pty pde -> chIn "operation" $ do
       (pty', pde') <- case (pty,pde) of
          (Just ty, Just de) -> do
@@ -200,7 +188,7 @@ checkResInfo gr mo mm c info = do
 
     ResOverload os tysts -> chIn "overloading" $ do
       tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts  -- return explicit ones
-      tysts0 <- checkErr $ lookupOverload gr mo c  -- check against inherited ones too
+      tysts0 <- checkErr $ lookupOverload gr m c  -- check against inherited ones too
       tysts1 <- mapM (uncurry $ flip (checkLType gr [])) 
                   [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
       --- this can only be a partial guarantee, since matching
@@ -210,12 +198,12 @@ checkResInfo gr mo mm c info = do
       return (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
-      ts <- checkErr $ lookupParamValues gr mo c
+      ts <- checkErr $ lookupParamValues gr m c
       return (ResParam (Just (pcs, Just ts)))
 
     _ ->  return info
  where
-   chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon)
+   chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
 
    checkUniq xss = case xss of
      x:y:xs 
@@ -224,44 +212,27 @@ checkResInfo gr mo mm c info = do
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
+   mkCheck cat ss = case ss of
+     [] -> return info
+     _  -> checkError (vcat ss $$ text "in" <+> text cat <+> ppIdent c <+> ppPosition mo c)
 
-checkCncInfo :: SourceGrammar -> Ident -> SourceModInfo -> 
-                (Ident,SourceModInfo) -> 
-                Ident -> Info -> Check Info
-checkCncInfo gr m mo (a,abs) c info = do
-  checkReservedId c
-  case info of
-
-    CncFun _ (Just trm) mpr -> chIn "linearization of" $ do
-      typ        <- checkErr $ lookupFunType gr a c
-      let cat0   =  valCat typ
-      (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
-      (trm',_)   <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
-      checkPrintname gr mpr
-      cat        <- return $ snd cat0
-      return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
-                                                   -- cat for cf, typ for pe
-
-    CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
-      checkErr $ lookupCatContext gr a c
-      typ'  <- computeLType gr [] typ
-      mdef' <- case mdef of
-        Just def -> do
-          (def',_) <- checkLType gr [] def (mkFunType [typeStr] typ)
-          return $ Just def'
-        _ -> return mdef
-      checkPrintname gr mpr
-      return (CncCat (Just typ') mdef' mpr)
-
-    _ -> checkResInfo gr m mo c info
-
- where
-   chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
+   compAbsTyp g t = case t of
+     Vr x -> maybe (checkError (text "no value given to variable" <+> ppIdent x)) return $ lookup x g
+     Let (x,(_,a)) b -> do
+       a' <- compAbsTyp g a
+       compAbsTyp ((x, a'):g) b
+     Prod b x a t -> do
+       a' <- compAbsTyp g a
+       t' <- compAbsTyp ((x,Vr x):g) t
+       return $ Prod b x a' t'
+     Abs _ _ _ -> return t
+     _ -> composOp (compAbsTyp g) t  
 
 
-checkPrintname :: SourceGrammar -> Maybe Term -> Check ()
-checkPrintname st (Just t) = checkLType st [] t typeStr >> return ()
-checkPrintname _  _        = return ()
+checkPrintname :: SourceGrammar -> Maybe Term -> Check (Maybe Term)
+checkPrintname gr (Just t) = do (t,_) <- checkLType gr [] t typeStr
+                                return (Just t)
+checkPrintname gr Nothing  = return Nothing
 
 -- | for grammars obtained otherwise than by parsing ---- update!!
 checkReservedId :: Ident -> Check ()
diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs
index c5b244903..c4ea4ae34 100644
--- a/src/GF/Compile/Optimize.hs
+++ b/src/GF/Compile/Optimize.hs
@@ -104,10 +104,10 @@ evalCncInfo opts gr cnc abs (c,info) = do
 
     return (CncCat ptyp pde' ppr')
 
-  CncFun (mt@(Just (_,ty@(cont,val)))) pde ppr -> --trace (prt c) $
+  CncFun (mt@(Just (_,cont,val))) pde ppr -> --trace (prt c) $
        eIn (text "linearization in type" <+> ppTerm Unqualified 0 (mkProd cont val []) $$ text "of function") $ do
     pde' <- case pde of
-      Just de -> liftM Just $ pEval ty de
+      Just de -> liftM Just $ pEval (cont,val) de
       Nothing -> return pde
     ppr' <-  liftM Just $ evalPrintname gr c ppr pde'
     return $ CncFun mt pde' ppr' -- only cat in type actually needed
diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs
index e3b4ddbae..a4223585a 100644
--- a/src/GF/Grammar/Grammar.hs
+++ b/src/GF/Grammar/Grammar.hs
@@ -91,8 +91,8 @@ data Info =
  | ResOverload [Ident] [(Type,Term)]         -- ^ (/RES/) idents: modules inherited
 
 -- judgements in concrete syntax
- | CncCat  (Maybe Type)                   (Maybe Term) (Maybe Term)  -- ^ (/CNC/) lindef ini'zed, 
- | CncFun  (Maybe (Ident,(Context,Type))) (Maybe Term) (Maybe Term)  -- ^ (/CNC/) type info added at 'TC'
+ | CncCat  (Maybe Type)                 (Maybe Term) (Maybe Term)  -- ^ (/CNC/) lindef ini'zed, 
+ | CncFun  (Maybe (Ident,Context,Type)) (Maybe Term) (Maybe Term)  -- ^ (/CNC/) type info added at 'TC'
 
 -- indirection to module Ident
  | AnyInd Bool Ident                         -- ^ (/INDIR/) the 'Bool' says if canonical
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
index 0d31b0a9e..62796aeed 100644
--- a/src/GF/Grammar/Lookup.hs
+++ b/src/GF/Grammar/Lookup.hs
@@ -90,8 +90,8 @@ lookupResDefKind gr m c
       CncCat (Just ty) _ _ -> liftM (flip (,) 1) $ lock c ty
       CncCat _ _ _         -> liftM (flip (,) 1) $ lock c defLinType
       
-      CncFun (Just (cat,_)) (Just tr) _ -> liftM (flip (,) 1) $ unlock cat tr
-      CncFun _              (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
+      CncFun (Just (cat,_,_)) (Just tr) _ -> liftM (flip (,) 1) $ unlock cat tr
+      CncFun _                (Just tr) _ -> liftM (flip (,) 1) (return tr) ---- $ unlock c tr
 
       AnyInd _ n        -> look False n c
       ResParam _        -> return (QC m c,2)
@@ -109,7 +109,7 @@ lookupResType gr m c = do
 
     -- used in reused concrete
     CncCat _ _ _ -> return typeType
-    CncFun (Just (cat,(cont@(_:_),val))) _ _ -> do
+    CncFun (Just (cat,cont@(_:_),val)) _ _ -> do
           val' <- lock cat val 
           return $ mkProd cont val' []
     CncFun _ _ _      -> lookFunType m m c