From c3eb6973f4023766f61830f8fb8aba8c24d1869e Mon Sep 17 00:00:00 2001
From: krangelov <kr.angelov@gmail.com>
Date: Wed, 13 Oct 2021 19:14:56 +0200
Subject: [PATCH] working PMCFG generation

---
 src/compiler/GF/Compile/CheckGrammar.hs       |  89 ++++++-----
 src/compiler/GF/Compile/Compute/Concrete.hs   |  22 ++-
 src/compiler/GF/Compile/GeneratePMCFG.hs      | 146 ++++++++++++------
 src/compiler/GF/Compile/GrammarToCanonical.hs |   2 +-
 src/compiler/GF/Compile/Rename.hs             |   8 +-
 src/compiler/GF/Compile/Tags.hs               |   2 +-
 .../GF/Compile/TypeCheck/Primitives.hs        |   8 +-
 src/compiler/GF/Compile/Update.hs             |  10 +-
 src/compiler/GF/Grammar/Analyse.hs            |   4 +-
 src/compiler/GF/Grammar/Binary.hs             |  14 +-
 src/compiler/GF/Grammar/Grammar.hs            |  26 ++--
 src/compiler/GF/Grammar/Lookup.hs             |  26 ++--
 src/compiler/GF/Grammar/Parser.y              |   4 +-
 src/compiler/GF/Grammar/Printer.hs            |  68 ++++----
 src/compiler/GF/Infra/CheckM.hs               |  28 +---
 src/runtime/haskell/PGF2/Transactions.hsc     |   6 +-
 16 files changed, 253 insertions(+), 210 deletions(-)

diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs
index 29a400002..db5dcf65d 100644
--- a/src/compiler/GF/Compile/CheckGrammar.hs
+++ b/src/compiler/GF/Compile/CheckGrammar.hs
@@ -29,7 +29,7 @@ import GF.Infra.Option
 import GF.Compile.TypeCheck.Abstract
 import GF.Compile.TypeCheck.Concrete(checkLType,inferLType,ppType)
 import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
-import qualified GF.Compile.Compute.Concrete as CN(normalForm)
+import GF.Compile.Compute.Concrete(normalForm)
 
 import GF.Grammar
 import GF.Grammar.Lexer
@@ -54,11 +54,7 @@ checkModule opts cwd sgr mo@(m,mi) = do
                              checkCompleteGrammar opts cwd gr (a,abs) mo
           _            -> return mo
   infoss <- checkInModule cwd mi NoLoc empty $ topoSortJments2 mo
-  foldM updateCheckInfos mo infoss
-  where
-    updateCheckInfos mo = fmap (foldl update mo) . parallelCheck . map check
-      where check (i,info) = fmap ((,) i) (checkInfo opts cwd sgr mo i info)
-    update mo@(m,mi) (i,info) = (m,mi{jments=Map.insert i info (jments mi)})
+  foldM (foldM (checkInfo opts cwd sgr)) mo infoss
 
 -- check if restricted inheritance modules are still coherent
 -- i.e. that the defs of remaining names don't depend on omitted names
@@ -120,8 +116,7 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
                                     return js
                    _ -> do
                      case mb_def of
-                       Ok def -> do (cont,val) <- linTypeOfType gr cm (L loc ty)
-                                    let linty = (snd (valCat ty),cont,val)
+                       Ok def -> do linty <- linTypeOfType gr cm (L loc ty)
                                     return $ Map.insert c (CncFun (Just linty) (Just (L NoLoc def)) Nothing Nothing) js
                        Bad _  -> do noLinOf c
                                     return js
@@ -141,8 +136,7 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
      case info of
        CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
                              Ok (_,AbsFun (Just (L loc ty)) _ _ _) ->
-                                        do (cont,val) <- linTypeOfType gr cm (L loc ty)
-                                           let linty = (snd (valCat ty),cont,val)
+                                        do linty <- linTypeOfType gr cm (L loc ty)
                                            return $ Map.insert c (CncFun (Just linty) d mn mf) js
                              _       -> do checkWarn ("function" <+> c <+> "is not in abstract")
                                            return js
@@ -158,32 +152,29 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
 
        _ -> return $ Map.insert c info js
 
-
--- | General Principle: only Just-values are checked.
--- A May-value has always been checked in its origin module.
-checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
-checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
+checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> (Ident,Info) -> Check SourceModule
+checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
   checkReservedId c
   case info of
     AbsCat (Just (L loc cont)) ->
       mkCheck loc "the category" $
         checkContext gr cont
 
-    AbsFun (Just (L loc typ0)) ma md moper -> do
-      typ <- compAbsTyp [] typ0   -- to calculate let definitions
+    AbsFun (Just (L loc typ)) ma md moper -> do
       mkCheck loc "the type of function" $
         checkTyp gr typ
+      typ <- compAbsTyp [] typ   -- to calculate let definitions
       case md of
         Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $
-                                          checkDef gr (m,c) typ eq) eqs
+                                          checkDef gr (fst sm,c) typ eq) eqs
         Nothing  -> return ()
-      return (AbsFun (Just (L loc typ)) ma md moper)
+      update sm c (AbsFun (Just (L loc typ)) ma md moper)
 
     CncCat mty mdef mref mpr mpmcfg -> do
       mty  <- case mty of
                 Just (L loc typ) -> chIn loc "linearization type of" $ do
                                       (typ,_) <- checkLType gr [] typ typeType
-                                      typ  <- CN.normalForm gr typ
+                                      typ  <- normalForm gr typ
                                       return (Just (L loc typ))
                 Nothing          -> return Nothing
       mdef <- case (mty,mdef) of
@@ -204,11 +195,11 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
                 _ -> return Nothing
-      return (CncCat mty mdef mref mpr mpmcfg)
+      update sm c (CncCat mty mdef mref mpr mpmcfg)
 
     CncFun mty mt mpr mpmcfg -> do
       mt <- case (mty,mt) of
-              (Just (cat,cont,val),Just (L loc trm)) ->
+              (Just (_,cat,cont,val),Just (L loc trm)) ->
                   chIn loc "linearization of" $ do
                      (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
                      return (Just (L loc trm))
@@ -219,14 +210,14 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
                 _ -> return Nothing
-      return (CncFun mty mt mpr mpmcfg)
+      update sm c (CncFun mty mt mpr mpmcfg)
 
     ResOper pty pde -> do
       (pty', pde') <- case (pty,pde) of
          (Just (L loct ty), Just (L locd de)) -> do
            ty'     <- chIn loct "operation" $ do
                          (ty,_) <- checkLType gr [] ty typeType
-                         CN.normalForm gr ty
+                         normalForm gr ty
            (de',_) <- chIn locd "operation" $
                          checkLType gr [] de ty'
            return (Just (L loct ty'), Just (L locd de'))
@@ -237,32 +228,37 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
          (Just (L loct ty), Nothing) -> do
            chIn loct "operation" $
              checkError (pp "No definition given to the operation")
-      return (ResOper pty' pde')
+      update sm c (ResOper pty' pde')
 
     ResOverload os tysts -> chIn NoLoc "overloading" $ do
       tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
-      tysts0 <- lookupOverload gr (m,c)  -- check against inherited ones too
+      tysts0 <- lookupOverload gr (fst sm,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
       --- with value type is only possible if expected type is given
       checkUniq $
         sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
-      return (ResOverload os [(y,x) | (x,y) <- tysts'])
+      update sm c (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (L loc pcs)) _ -> do
-      ts <- chIn loc "parameter type" $
-              liftM concat $ mapM mkPar pcs
-      return (ResParam (Just (L loc pcs)) (Just ts))
+      (sm,cnt,ts) <- chIn loc "parameter type" $
+                        mkParamValues sm 0 [] pcs
+      update sm c (ResParam (Just (L loc pcs)) (Just (ts,cnt)))
 
-    _ ->  return info
+    _ ->  return sm
  where
-   gr = prependModule sgr (m,mo)
-   chIn loc cat = checkInModule cwd mo loc ("Happened in" <+> cat <+> c)
+   gr = prependModule sgr sm
+   chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c)
 
-   mkPar (f,co) = do
-       vs <- liftM sequence $ mapM (\(_,_,ty) -> allParamValues gr ty) co
-       return $ map (mkApp (QC (m,f))) vs
+   mkParamValues sm         cnt ts []          = return (sm,cnt,[])
+   mkParamValues sm@(mn,mi) cnt ts ((f,co):fs) = do
+     sm <- case lookupIdent f (jments mi) of
+             Ok (ResValue ty _) -> update sm f (ResValue ty cnt)
+             Bad msg            -> checkError (pp msg)
+     vs <- liftM sequence $ mapM (\(_,_,ty) -> allParamValues gr ty) co
+     (sm,cnt,ts) <- mkParamValues sm (cnt+length vs) ts fs
+     return (sm,cnt,map (mkApp (QC (mn,f))) vs ++ ts)
 
    checkUniq xss = case xss of
      x:y:xs
@@ -272,7 +268,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
      _ -> return ()
 
    mkCheck loc cat ss = case ss of
-     [] -> return info
+     [] -> return sm
      _ -> chIn loc cat $ checkError (vcat ss)
 
    compAbsTyp g t = case t of
@@ -285,7 +281,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
        t' <- compAbsTyp ((x,Vr x):g) t
        return $ Prod b x a' t'
      Abs _ _ _ -> return t
-     _ -> composOp (compAbsTyp g) t
+     _ -> composOp (compAbsTyp g) t  
+
+   update (mn,mi) c info = return (mn,mi{jments=Map.insert c info (jments mi)})
 
 
 -- | for grammars obtained otherwise than by parsing ---- update!!
@@ -297,12 +295,13 @@ checkReservedId x =
 -- auxiliaries
 
 -- | linearization types and defaults
-linTypeOfType :: Grammar -> ModuleName -> L Type -> Check (Context,Type)
+linTypeOfType :: Grammar -> ModuleName -> L Type -> Check ([Ident],Ident,Context,Type)
 linTypeOfType cnc m (L loc typ) = do
-  let (cont,cat) = typeSkeleton typ
-  val  <- lookLin cat
-  args <- mapM mkLinArg (zip [0..] cont)
-  return (args, val)
+  let (ctxt,res_cat) = typeSkeleton typ
+  val <- lookLin res_cat
+  lin_args <- mapM mkLinArg (zip [0..] ctxt)
+  let (args,arg_cats) = unzip lin_args
+  return (arg_cats, snd res_cat, args, val)
  where
    mkLinArg (i,(n,mc@(m,cat))) = do
      val  <- lookLin mc
@@ -314,8 +313,8 @@ linTypeOfType cnc m (L loc typ) = do
                                       "with" $$
                                       nest 2 val)) $
                              plusRecType vars val
-     return (Explicit,symb,rec)
+     return ((Explicit,symb,rec),cat)
    lookLin (_,c) = checks [ --- rather: update with defLinType ?
-      lookupLincat cnc m c >>= CN.normalForm cnc
+      lookupLincat cnc m c >>= normalForm cnc
      ,return defLinType
      ]
diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs
index d2ccf8931..5dc1e6a15 100644
--- a/src/compiler/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/GF/Compile/Compute/Concrete.hs
@@ -6,10 +6,10 @@ module GF.Compile.Compute.Concrete
            ( normalForm
            , Value(..), Thunk, ThunkState(..), Env
            , EvalM, runEvalM, evalError
-           , eval, apply, force, value2term
+           , eval, apply, force, value2term, patternMatch
            , newMeta,getMeta,setMeta
-           , newThunk,newEvaluatedThunk,getAllParamValues
-           , lookupParams
+           , newThunk,newEvaluatedThunk
+           , getResDef, getInfo, getAllParamValues
            ) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
@@ -144,7 +144,7 @@ eval env (Q q@(m,id))   vs
                                  case mb_res of
                                    Just res -> return res
                                    Nothing  -> return (VApp q vs)
-  | otherwise               = do t <- lookupGlobal q
+  | otherwise               = do t <- getResDef q
                                  eval env t vs
 eval env (QC q)         vs  = return (VApp q vs)
 eval env (C t1 t2)      []  = do v1 <- eval env t1 []
@@ -263,7 +263,7 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
     match env []              eqs      args  = eval env t args
     match env (PT ty p   :ps) eqs      args  = match env (p:ps) eqs args
     match env (PAlt p1 p2:ps) eqs      args  = match env (p1:ps) ((env,p2:ps,args,t):eqs) args
-    match env (PM q      :ps) eqs      args  = do t <- lookupGlobal q
+    match env (PM q      :ps) eqs      args  = do t <- getResDef q
                                                   case t of
                                                     EPatt _ _ p -> match env (p:ps) eqs args
                                                     _ -> evalError $ hang "Expected pattern macro:" 4
@@ -466,18 +466,16 @@ runEvalM gr f =
 evalError :: Doc -> EvalM s a
 evalError msg = EvalM (\gr k _ r -> return (Fail msg))
   
-lookupGlobal :: QIdent -> EvalM s Term
-lookupGlobal q = EvalM $ \gr k mt r -> do
+getResDef :: QIdent -> EvalM s Term
+getResDef q = EvalM $ \gr k mt r -> do
   case lookupResDef gr q of
     Ok t    -> k t mt r
     Bad msg -> return (Fail (pp msg))
 
-lookupParams :: QIdent -> EvalM s (ModuleName,[Param])
-lookupParams q = EvalM $ \gr k mt r -> do
+getInfo :: QIdent -> EvalM s (ModuleName,Info)
+getInfo q = EvalM $ \gr k mt r -> do
   case lookupOrigInfo gr q of
-    Ok (m,info) -> case info of
-                     ResParam (Just (L _ ps)) _ -> k (m,ps) mt r
-                     _                          -> return (Fail (ppQIdent Qualified q <+> "is not a parameter type"))
+    Ok res  -> k res mt r
     Bad msg -> return (Fail (pp msg))
 
 getAllParamValues :: Type -> EvalM s [Term]
diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs
index dec233a5a..8e5acb0cd 100644
--- a/src/compiler/GF/Compile/GeneratePMCFG.hs
+++ b/src/compiler/GF/Compile/GeneratePMCFG.hs
@@ -25,7 +25,6 @@ import PGF2.Transactions
 import qualified Data.Map.Strict as Map
 import Control.Monad
 import Data.List(mapAccumL)
-import Debug.Trace
 
 generatePMCFG :: Options -> FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
 generatePMCFG opts cwd gr cmo@(cm,cmi) = do
@@ -33,24 +32,39 @@ generatePMCFG opts cwd gr cmo@(cm,cmi) = do
   js <- mapM (addPMCFG opts cwd gr' cmi) (Map.toList (jments cmi))
   return (cm,cmi{jments = (Map.fromAscList js)})
 
-addPMCFG opts cwd gr cmi (id,CncFun mty@(Just (cat,ctxt,val)) mlin@(Just (L loc term)) mprn Nothing) =
+addPMCFG opts cwd gr cmi (id,CncFun mty@(Just (_,cat,ctxt,val)) mlin@(Just (L loc term)) mprn Nothing) =
   checkInModule cwd cmi loc ("Happened in the PMCFG generation for" <+> id) $ do
-    lins <- pmcfgForm gr (L loc id) term ctxt
-    return (id,CncFun mty mlin mprn (Just (PMCFG lins)))
+    rules <- pmcfgForm gr term ctxt val
+    return (id,CncFun mty mlin mprn (Just rules))
 addPMCFG opts cwd gr cmi id_info = return id_info
 
-pmcfgForm :: Grammar -> L Ident -> Term -> Context -> Check [[[Symbol]]]
-pmcfgForm gr _ t ctxt =
+pmcfgForm :: Grammar -> Term -> Context -> Type -> Check [PMCFGRule]
+pmcfgForm gr t ctxt ty =
   runEvalM gr $ do
     ((_,ms),args) <- mapAccumM (\(d,ms) (_,_,ty) -> do
                                    let (ms',_,t) = type2metaTerm gr d ms 0 [] ty
-                                   tnk <- trace (show (ppTerm Unqualified 0 t)) $ newThunk [] t
+                                   tnk <- newThunk [] t
                                    return ((d+1,ms'),tnk))
                                (0,Map.empty) ctxt
     sequence_ [newMeta (Just ty) i | (i,ty) <- Map.toList ms]
     v <- eval [] t args
-    (lins,_) <- value2pmcfg v []
-    return (reverse lins)
+    (lins,params) <- flatten v ty ([],[])
+    lins <- mapM str2lin lins
+    (r,rs,_) <- compute params
+    args <- zipWithM tnk2pmcfgcat args ctxt
+    return (PMCFGRule (PMCFGCat r rs) args (reverse lins))
+    where
+      tnk2pmcfgcat tnk (_,_,ty) = do
+        v <- force tnk []
+        (_,params) <- flatten v ty ([],[])
+        (r,rs,_) <- compute params
+        return (PMCFGCat r rs)
+
+      compute []     = return (0,[],1)
+      compute (v:vs) = do
+        (r, rs ,cnt ) <- param2int v
+        (r',rs',cnt') <- compute vs
+        return (r*cnt'+r',combine cnt' rs rs',cnt*cnt')
 
 type2metaTerm :: SourceGrammar -> Int -> Map.Map MetaId Type -> LIndex -> [(LIndex,Ident)] -> Type -> (Map.Map MetaId Type,Int,Term)
 type2metaTerm gr d ms r rs (Sort s) | s == cStr =
@@ -71,52 +85,94 @@ type2metaTerm gr d ms r rs ty@(QC q) =
   let i = Map.size ms + 1
   in (Map.insert i ty ms,r,Meta i)
 
-value2pmcfg (VSusp tnk env vs k) lins = do
-  st <- getMeta tnk
-  case st of
-    Unevaluated _ t         -> do v <- eval env t vs
-                                  value2pmcfg v lins
+
+flatten (VSusp tnk env vs k) ty st = do
+  tnk_st <- getMeta tnk
+  case tnk_st of
     Evaluated v             -> do v <- apply v vs
-                                  value2pmcfg v lins
-    Unbound (Just (QC q)) _ -> do (m,ps) <- lookupParams q
+                                  flatten v ty st
+    Unbound (Just (QC q)) _ -> do (m,ResParam (Just (L _ ps)) _) <- getInfo q
                                   msum [bind tnk m p | p <- ps]
                                   v <- k tnk
-                                  value2pmcfg v lins
+                                  flatten v ty st
   where
     bind tnk m (p, ctxt) = do
       tnks <- mapM (\(_,_,ty) -> newMeta (Just ty) 0) ctxt
       setMeta tnk (Evaluated (VApp (m,p) tnks))
-value2pmcfg (VR as) lins = do
-  (lins,as) <- collectFields lins as
-  return (lins,VR as)
+flatten (VR as) (RecType lbls) st = do
+  foldM collect st lbls
   where
-    collectFields lins []             = do
-      return (lins,[])
-    collectFields lins ((lbl,tnk):as) = do
+    collect st (lbl,ty) =
+      case lookup lbl as of
+        Just tnk -> do v <- force tnk []
+                       flatten v ty st
+        Nothing  -> evalError ("Missing value for label" <+> pp lbl $$
+                               "among" <+> hsep (punctuate (pp ',') (map fst as)))
+flatten v@(VT _ cs) (Table p q) st = do
+  ts <- getAllParamValues p
+  foldM collect st ts
+  where
+    collect st t = do
+      tnk <- newThunk [] t
+      let v0 = VS v tnk []
+      v <- patternMatch v0 (map (\(p,t) -> ([],[p],[tnk],t)) cs)
+      flatten v q st
+flatten (VV _ tnks) (Table _ q) st = do
+  foldM collect st tnks
+  where
+    collect st tnk = do
       v <- force tnk []
-      (lins,v) <- value2pmcfg v lins
-      case v of
-        VR [] -> collectFields lins as
-        _     -> do (lins,as) <- collectFields lins as
-                    tnk <- newEvaluatedThunk v
-                    return (lins,(lbl,tnk):as)
-value2pmcfg v lins = do
-  lin <- value2lin v
-  return (lin:lins,VR [])
+      flatten v q st
+flatten v (Sort s) (lins,params) | s == cStr = do
+  return (v:lins,params)
+flatten v (QC q) (lins,params) = do
+  return (lins,v:params)
 
-value2lin (VStr s)         = return [SymKS s]
-value2lin (VSymCat d r rs) = do rs <- forM rs $ \(i,tnk) -> do
-                                        v <- force tnk []
-                                        j <- case v of
-                                               VMeta tnk _ _ -> do st <- getMeta tnk
-                                                                   case st of
-                                                                     Unbound _ j -> return j
-                                        return (i,j)
-                                return [SymCat d r rs]
-value2lin (VC vs)          = fmap concat (mapM value2lin vs)
-value2lin v                = do t <- value2term 0 v
-                                evalError ("the term" <+> ppTerm Unqualified 0 t $$
-                                           "cannot be evaluated at compile time.")
+str2lin (VStr s)         = return [SymKS s]
+str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs
+                              return [SymCat d r rs]
+  where
+    compute r' []                = return (r',[])
+    compute r' ((cnt',tnk):tnks) = do
+      (r, rs,_) <- force tnk [] >>= param2int
+      (r',rs' ) <- compute r' tnks
+      return (r*cnt'+r',combine cnt' rs rs')
+str2lin (VC vs)          = fmap concat (mapM str2lin vs)
+str2lin v                = do t <- value2term 0 v
+                              evalError ("the term" <+> ppTerm Unqualified 0 t $$
+                                         "cannot be evaluated at compile time.")
+
+param2int (VApp q tnks) = do
+  (r ,    cnt ) <- getIdxCnt q
+  (r',rs',cnt') <- compute tnks
+  return (r*cnt' + r',rs',cnt*cnt')
+  where
+    getIdxCnt q = do
+      (_,ResValue (L _ ty) idx) <- getInfo q
+      let QC p = valTypeCnc ty
+      (_,ResParam _ (Just (_,cnt))) <- getInfo p
+      return (idx,cnt)
+
+    compute []         = return (0,[],1)
+    compute (tnk:tnks) = do
+      (r, rs ,cnt ) <- force tnk [] >>= param2int
+      (r',rs',cnt') <- compute tnks
+      return (r*cnt'+r',combine cnt' rs rs',cnt*cnt')
+param2int (VMeta tnk _ _) = do
+  tnk_st <- getMeta tnk
+  case tnk_st of
+    Evaluated v         -> param2int v
+    Unbound (Just ty) j -> do let QC q = valTypeCnc ty
+                              (_,ResParam _ (Just (_,cnt))) <- getInfo q
+                              return (0,[(1,j)],cnt)
+
+combine cnt'          []            rs' = rs'
+combine cnt'         rs              [] = [(r*cnt',pv) | (r,pv) <- rs]
+combine cnt' ((r,pv):rs) ((r',pv'):rs') =
+  case compare pv pv' of
+    LT -> (r*cnt',   pv ) : combine cnt' rs ((r',pv'):rs')
+    EQ -> (r*cnt'+r',pv ) : combine cnt' rs ((r',pv'):rs')
+    GT -> (       r',pv') : combine cnt' ((r,pv):rs) rs'
 
 mapAccumM f a []     = return (a,[])
 mapAccumM f a (x:xs) = do (a, y) <- f a x
diff --git a/src/compiler/GF/Compile/GrammarToCanonical.hs b/src/compiler/GF/Compile/GrammarToCanonical.hs
index 34aa01df7..b19a0ba44 100644
--- a/src/compiler/GF/Compile/GrammarToCanonical.hs
+++ b/src/compiler/GF/Compile/GrammarToCanonical.hs
@@ -97,7 +97,7 @@ toCanonical gr absname (name,jment) =
       ntyp <- normalForm gr typ
       let pts = paramTypes gr ntyp
       return [(pts,Left (LincatDef (gId name) (convType ntyp)))]
-    CncFun (Just r@(cat,ctx,lincat)) (Just (L loc def)) pprn _ -> do
+    CncFun (Just r@(_,cat,ctx,lincat)) (Just (L loc def)) pprn _ -> do
       let params = [(b,x)|(b,x,_)<-ctx]
           args   = map snd params
       e0 <- normalForm gr (mkAbs params (mkApp def (map Vr args)))
diff --git a/src/compiler/GF/Compile/Rename.hs b/src/compiler/GF/Compile/Rename.hs
index 6889a11bf..46d2e8b9e 100644
--- a/src/compiler/GF/Compile/Rename.hs
+++ b/src/compiler/GF/Compile/Rename.hs
@@ -130,8 +130,8 @@ renameIdentTerm' env@(act,imps) t0 =
 info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
 info2status mq c i = case i of
   AbsFun _ _ Nothing _ -> maybe Con (curry QC) mq
-  ResValue _  -> maybe Con (curry QC) mq
-  ResParam _ _  -> maybe Con (curry QC) mq
+  ResValue _ _ -> maybe Con (curry QC) mq
+  ResParam _ _ -> maybe Con (curry QC) mq
   AnyInd True m -> maybe Con (const (curry QC m)) mq
   AnyInd False m -> maybe Cn (const (curry Q m)) mq
   _           -> maybe Cn (curry Q) mq
@@ -168,9 +168,9 @@ renameInfo cwd status (m,mi) i info =
     ResParam (Just pp) m -> do
       pp' <- renLoc (mapM (renParam status)) pp
       return (ResParam (Just pp') m)
-    ResValue t -> do
+    ResValue t i -> do
       t <- renLoc (renameTerm status []) t
-      return (ResValue t)
+      return (ResValue t i)
     CncCat mcat mdef mref mpr mpmcfg -> liftM5 CncCat (renTerm mcat) (renTerm mdef) (renTerm mref) (renTerm mpr) (return mpmcfg)
     CncFun mty mtr mpr mpmcfg -> liftM3 (CncFun mty)         (renTerm mtr) (renTerm mpr) (return mpmcfg)
     _ -> return info
diff --git a/src/compiler/GF/Compile/Tags.hs b/src/compiler/GF/Compile/Tags.hs
index 6452e066f..8b2e2c312 100644
--- a/src/compiler/GF/Compile/Tags.hs
+++ b/src/compiler/GF/Compile/Tags.hs
@@ -31,7 +31,7 @@ getLocalTags x (m,mi) =
     getLocations (AbsFun mb_type _ mb_eqs _)    = maybe (ltype "fun")        mb_type ++
                                                   maybe (list (loc "def"))   mb_eqs  
     getLocations (ResParam mb_params _)         = maybe (loc "param")        mb_params
-    getLocations (ResValue mb_type)             = ltype "param-value"          mb_type
+    getLocations (ResValue mb_type _)           = ltype "param-value"          mb_type
     getLocations (ResOper  mb_type mb_def)      = maybe (ltype "oper-type")  mb_type ++
                                                   maybe (loc "oper-def")     mb_def
     getLocations (ResOverload _ defs)           = list (\(x,y) -> ltype "overload-type" x ++ 
diff --git a/src/compiler/GF/Compile/TypeCheck/Primitives.hs b/src/compiler/GF/Compile/TypeCheck/Primitives.hs
index d82cd1568..8f9d977b4 100644
--- a/src/compiler/GF/Compile/TypeCheck/Primitives.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Primitives.hs
@@ -8,7 +8,7 @@ typPredefined :: Ident -> Maybe Type
 typPredefined f = case Map.lookup f primitives of
                     Just (ResOper (Just (L _ ty)) _) -> Just ty
                     Just (ResParam _ _)              -> Just typePType
-                    Just (ResValue (L _ ty))         -> Just ty
+                    Just (ResValue (L _ ty) _)       -> Just ty
                     _                                -> Nothing
 
 primitives = Map.fromList
@@ -16,9 +16,9 @@ primitives = Map.fromList
   , (cInt      , ResOper (Just (noLoc typePType)) Nothing)
   , (cFloat    , ResOper (Just (noLoc typePType)) Nothing)
   , (cInts     , fun [typeInt] typePType)
-  , (cPBool    , ResParam (Just (noLoc [(cPTrue,[]),(cPFalse,[])])) (Just [QC (cPredef,cPTrue), QC (cPredef,cPFalse)]))
-  , (cPTrue    , ResValue (noLoc typePBool))
-  , (cPFalse   , ResValue (noLoc typePBool))
+  , (cPBool    , ResParam (Just (noLoc [(cPTrue,[]),(cPFalse,[])])) (Just ([QC (cPredef,cPTrue), QC (cPredef,cPFalse)],2)))
+  , (cPTrue    , ResValue (noLoc typePBool) 0)
+  , (cPFalse   , ResValue (noLoc typePBool) 1)
   , (cError    , fun [typeStr] typeError)  -- non-can. of empty set
   , (cLength   , fun [typeTok] typeInt)
   , (cDrop     , fun [typeInt,typeTok] typeTok)
diff --git a/src/compiler/GF/Compile/Update.hs b/src/compiler/GF/Compile/Update.hs
index a437b0ea8..cbbad5f9b 100644
--- a/src/compiler/GF/Compile/Update.hs
+++ b/src/compiler/GF/Compile/Update.hs
@@ -168,7 +168,7 @@ extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jme
     indirInfo :: ModuleName -> Info -> Info
     indirInfo n info = AnyInd b n' where
       (b,n') = case info of
-        ResValue _ -> (True,n)
+        ResValue _ _ -> (True,n)
         ResParam _ _ -> (True,n)
         AbsFun _ _ Nothing _ -> (True,n)
         AnyInd b k -> (b,k)
@@ -179,7 +179,7 @@ globalizeLoc fpath i =
     AbsCat mc             -> AbsCat (fmap gl mc)
     AbsFun mt ma md moper -> AbsFun (fmap gl mt) ma (fmap (fmap gl) md) moper
     ResParam mt mv        -> ResParam (fmap gl mt) mv
-    ResValue t            -> ResValue (gl t)
+    ResValue t i          -> ResValue (gl t) i
     ResOper mt m          -> ResOper (fmap gl mt) (fmap gl m)
     ResOverload ms os     -> ResOverload ms (map (\(x,y) -> (gl x,gl y)) os)
     CncCat mc md mr mp mpmcfg-> CncCat (fmap gl mc) (fmap gl md) (fmap gl mr) (fmap gl mp) mpmcfg
@@ -201,9 +201,9 @@ unifyAnyInfo m i j = case (i,j) of
 
   (ResParam mt1 mv1, ResParam mt2 mv2) ->
     liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
-  (ResValue (L l1 t1), ResValue (L l2 t2))
-      | t1==t2    -> return (ResValue (L l1 t1))
-      | otherwise -> fail ""
+  (ResValue (L l1 t1) i1, ResValue (L l2 t2) i2)
+      | t1==t2 && i1 == i2 -> return (ResValue (L l1 t1) i1)
+      | otherwise          -> fail ""
   (_, ResOverload ms t) | elem m ms ->
     return $ ResOverload ms t
   (ResOper mt1 m1, ResOper mt2 m2) ->
diff --git a/src/compiler/GF/Grammar/Analyse.hs b/src/compiler/GF/Grammar/Analyse.hs
index 4c8f2020f..64a7fa4d4 100644
--- a/src/compiler/GF/Grammar/Analyse.hs
+++ b/src/compiler/GF/Grammar/Analyse.hs
@@ -29,7 +29,7 @@ stripInfo i = case i of
   AbsCat _ -> i
   AbsFun mt mi me mb -> AbsFun mt mi Nothing mb
   ResParam mp mt -> ResParam mp Nothing
-  ResValue lt -> i ----
+  ResValue lt _ -> i ----
   ResOper mt md -> ResOper mt Nothing
   ResOverload is fs -> ResOverload is [(lty, L loc (EInt 0)) | (lty,L loc _) <- fs]
   CncCat mty mte _ mtf mpmcfg -> CncCat mty Nothing Nothing Nothing Nothing
@@ -108,7 +108,7 @@ sizeInfo i = case i of
     sum [sum (map (sizeTerm . patt2term) ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
   ResParam mp mt -> 
     1 + sum [1 + sum [1 + sizeTerm ty | (_,_,ty) <- co] | Just (L _ ps) <- [mp], (_,co) <- ps]
-  ResValue lt -> 0
+  ResValue _ _ -> 0
   ResOper mt md -> 1 + msize mt + msize md
   ResOverload is fs -> 1 + sum [sizeTerm ty + sizeTerm tr | (L _ ty, L _ tr) <- fs]
   CncCat mty _ _ _ _ -> 1 + msize mty   -- ignoring lindef, linref and printname
diff --git a/src/compiler/GF/Grammar/Binary.hs b/src/compiler/GF/Grammar/Binary.hs
index b893a5215..c1594adab 100644
--- a/src/compiler/GF/Grammar/Binary.hs
+++ b/src/compiler/GF/Grammar/Binary.hs
@@ -103,15 +103,19 @@ instance Binary Options where
              toString (LInt n) = show n
              toString (LFlt d) = show d
 
-instance Binary PMCFG where
-  put (PMCFG lins) = put lins
-  get = fmap PMCFG get
+instance Binary PMCFGCat where
+  put (PMCFGCat r rs) = put (r,rs)
+  get = get >>= \(r,rs) -> return (PMCFGCat r rs)
+
+instance Binary PMCFGRule where
+  put (PMCFGRule res args rules) = put (res,args,rules)
+  get = get >>= \(res,args,rules) -> return (PMCFGRule res args rules)
 
 instance Binary Info where
   put (AbsCat x)       = putWord8 0 >> put x
   put (AbsFun w x y z) = putWord8 1 >> put (w,x,y,z)
   put (ResParam x y)   = putWord8 2 >> put (x,y)
-  put (ResValue x)     = putWord8 3 >> put x
+  put (ResValue x y)   = putWord8 3 >> put (x,y)
   put (ResOper x y)    = putWord8 4 >> put (x,y)
   put (ResOverload x y)= putWord8 5 >> put (x,y)
   put (CncCat v w x y z)=putWord8 6 >> put (v,w,x,y,z)
@@ -122,7 +126,7 @@ instance Binary Info where
              0 -> get >>= \x         -> return (AbsCat x)
              1 -> get >>= \(w,x,y,z) -> return (AbsFun w x y z)
              2 -> get >>= \(x,y)     -> return (ResParam x y)
-             3 -> get >>= \x         -> return (ResValue x)
+             3 -> get >>= \(x,y)     -> return (ResValue x y)
              4 -> get >>= \(x,y)     -> return (ResOper x y)
              5 -> get >>= \(x,y)     -> return (ResOverload x y)
              6 -> get >>= \(v,w,x,y,z)->return (CncCat v w x y z)
diff --git a/src/compiler/GF/Grammar/Grammar.hs b/src/compiler/GF/Grammar/Grammar.hs
index a6c7d2cb5..77fcda184 100644
--- a/src/compiler/GF/Grammar/Grammar.hs
+++ b/src/compiler/GF/Grammar/Grammar.hs
@@ -64,7 +64,7 @@ module GF.Grammar.Grammar (
         Location(..), L(..), unLoc, noLoc, ppLocation, ppL,
 
         -- ** PMCFG        
-        PMCFG(..)
+        PMCFGCat(..), PMCFGRule(..)
         ) where
 
 import GF.Infra.Ident
@@ -74,7 +74,7 @@ import GF.Infra.Location
 import GF.Data.Operations
 
 import PGF2(BindType(..))
-import PGF2.Transactions(Symbol,LIndex)
+import PGF2.Transactions(Symbol,LIndex,LParam)
 
 import Data.Array.IArray(Array)
 import Data.Array.Unboxed(UArray)
@@ -304,8 +304,11 @@ allConcreteModules gr =
   [i | (i, m) <- modules gr, MTConcrete _ <- [mtype m], isCompleteModule m]
 
 
-data PMCFG = PMCFG [[[Symbol]]]
-             deriving (Eq,Show)
+data PMCFGCat  = PMCFGCat LIndex [(LIndex,LParam)]
+                 deriving (Eq,Show)
+
+data PMCFGRule = PMCFGRule PMCFGCat [PMCFGCat] [[Symbol]]
+                 deriving (Eq,Show)
 
 -- | the constructors are judgements in 
 --
@@ -322,15 +325,18 @@ data Info =
  | AbsFun   (Maybe (L Type)) (Maybe Int) (Maybe [L Equation]) (Maybe Bool) -- ^ (/ABS/) type, arrity and definition of a function
 
 -- judgements in resource
- | ResParam (Maybe (L [Param])) (Maybe [Term])   -- ^ (/RES/) the second parameter is list of all possible values
- | ResValue (L Type)                             -- ^ (/RES/) to mark parameter constructors for lookup
- | ResOper  (Maybe (L Type)) (Maybe (L Term))    -- ^ (/RES/)
+ | ResParam (Maybe (L [Param])) (Maybe ([Term],Int)) -- ^ (/RES/) The second argument is list of all possible values
+                                                     -- and its precomputed length.
+ | ResValue (L Type) Int                             -- ^ (/RES/) to mark parameter constructors for lookup.
+                                                     -- The second argument is the offset into the list of all values
+                                                     -- where that constructor appears first.
+ | ResOper  (Maybe (L Type)) (Maybe (L Term))        -- ^ (/RES/)
 
- | ResOverload [ModuleName] [(L Type,L Term)]         -- ^ (/RES/) idents: modules inherited
+ | ResOverload [ModuleName] [(L Type,L Term)]        -- ^ (/RES/) idents: modules inherited
 
 -- judgements in concrete syntax
- | CncCat  (Maybe (L Type))             (Maybe (L Term)) (Maybe (L Term)) (Maybe (L Term)) (Maybe PMCFG) -- ^ (/CNC/) lindef ini'zed, 
- | CncFun  (Maybe (Ident,Context,Type)) (Maybe (L Term))                  (Maybe (L Term)) (Maybe PMCFG) -- ^ (/CNC/) type info added at 'TC'
+ | CncCat  (Maybe (L Type))                     (Maybe (L Term)) (Maybe (L Term)) (Maybe (L Term)) (Maybe [PMCFGRule]) -- ^ (/CNC/) lindef ini'zed, 
+ | CncFun  (Maybe ([Ident],Ident,Context,Type)) (Maybe (L Term))                  (Maybe (L Term)) (Maybe [PMCFGRule]) -- ^ (/CNC/) type info added at 'TC'
 
 -- indirection to module Ident
  | AnyInd Bool ModuleName                        -- ^ (/INDIR/) the 'Bool' says if canonical
diff --git a/src/compiler/GF/Grammar/Lookup.hs b/src/compiler/GF/Grammar/Lookup.hs
index 97aa5639e..558da5b63 100644
--- a/src/compiler/GF/Grammar/Lookup.hs
+++ b/src/compiler/GF/Grammar/Lookup.hs
@@ -78,12 +78,12 @@ lookupResDefLoc gr (m,c)
         CncCat (Just (L l ty)) _ _ _ _ -> fmap (L l) (lock c ty)
         CncCat _ _ _ _ _         -> fmap noLoc (lock c defLinType)
 
-        CncFun (Just (cat,_,_)) (Just (L l tr)) _ _ -> fmap (L l) (unlock cat tr)
-        CncFun _                (Just ltr) _ _ -> return ltr
+        CncFun (Just (_,cat,_,_)) (Just (L l tr)) _ _ -> fmap (L l) (unlock cat tr)
+        CncFun _                  (Just ltr) _ _ -> return ltr
 
         AnyInd _ n        -> look n c
         ResParam _ _      -> return (noLoc (QC (m,c)))
-        ResValue _        -> return (noLoc (QC (m,c)))
+        ResValue _ _      -> return (noLoc (QC (m,c)))
         _   -> raise $ render (c <+> "is not defined in resource" <+> m)
 
 lookupResType :: ErrorMonad m => Grammar -> QIdent -> m Type
@@ -94,12 +94,12 @@ 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' []
     AnyInd _ n        -> lookupResType gr (n,c)
-    ResParam _ _      -> return typePType
-    ResValue (L _ t)  -> return t
+    ResParam _ _    -> return typePType
+    ResValue (L _ t) _ -> return t
     _   -> raise $ render (c <+> "has no type defined in resource" <+> m)
 
 lookupOverloadTypes :: ErrorMonad m => Grammar -> QIdent -> m [(Term,Type)]
@@ -110,11 +110,11 @@ lookupOverloadTypes gr id@(m,c) = do
 
     -- used in reused concrete
     CncCat _ _ _ _ _ -> ret typeType
-    CncFun (Just (cat,cont,val)) _ _ _ -> do
+    CncFun (Just (_,cat,cont,val)) _ _ _ -> do
           val' <- lock cat val
           ret $ mkProd cont val' []
-    ResParam _ _      -> ret typePType
-    ResValue (L _ t)  -> ret t
+    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] ++
@@ -154,8 +154,8 @@ lookupParamValues :: ErrorMonad m => Grammar -> QIdent -> m [Term]
 lookupParamValues gr c = do
   (_,info) <- lookupOrigInfo gr c
   case info of
-    ResParam _ (Just pvs) -> return pvs
-    _                     -> raise $ render (ppQIdent Qualified c <+> "has no parameter values defined")
+    ResParam _ (Just (pvs,_)) -> return pvs
+    _                         -> raise $ render (ppQIdent Qualified c <+> "has no parameter values defined")
 
 allParamValues :: ErrorMonad m => Grammar -> Type -> m [Term]
 allParamValues cnc ptyp =
@@ -226,9 +226,9 @@ allOpers gr =
     typesIn info = case info of
       AbsFun  (Just ltyp) _ _ _ -> [ltyp]
       ResOper (Just ltyp) _     -> [ltyp]
-      ResValue ltyp             -> [ltyp]
+      ResValue ltyp _           -> [ltyp]
       ResOverload _ tytrs       -> [ltyp | (ltyp,_) <- tytrs]
-      CncFun  (Just (i,ctx,typ)) _ _ _ ->
+      CncFun  (Just (_,i,ctx,typ)) _ _ _ ->
                                    [L NoLoc (mkProdSimple ctx (lock' i typ))]
       _                         -> []
 
diff --git a/src/compiler/GF/Grammar/Parser.y b/src/compiler/GF/Grammar/Parser.y
index 7216c7594..678920c36 100644
--- a/src/compiler/GF/Grammar/Parser.y
+++ b/src/compiler/GF/Grammar/Parser.y
@@ -267,7 +267,7 @@ DataDef
 ParamDef :: { [(Ident,Info)] }
 ParamDef
   : Posn LhsIdent '=' ListParConstr Posn { ($2, ResParam (Just (mkL $1 $5 [param | L loc param <- $4])) Nothing) :
-                                        [(f, ResValue (L loc (mkProdSimple co (Cn $2)))) | L loc (f,co) <- $4] }
+                                           [(f, ResValue (L loc (mkProdSimple co (Cn $2))) 0) | L loc (f,co) <- $4] }
   | Posn LhsIdent                   Posn { [($2, ResParam Nothing Nothing)] }
 
 OperDef :: { [(Ident,Info)] }
@@ -774,7 +774,7 @@ checkInfoType mt jment@(id,info) =
     CncCat pty pd pr ppn _->ifConcrete mt (locPerh pty ++ locPerh pd ++ locPerh pr ++ locPerh ppn)
     CncFun _   pd ppn _  -> ifConcrete mt (locPerh pd ++ locPerh ppn)
     ResParam pparam _    -> ifResource mt (locPerh pparam)
-    ResValue ty          -> ifResource mt (locL ty)
+    ResValue ty _        -> ifResource mt (locL ty)
     ResOper  pty pt      -> ifOper mt pty pt
     ResOverload _ xs     -> ifResource mt (concat [[loc1,loc2] | (L loc1 _,L loc2 _) <- xs])
   where
diff --git a/src/compiler/GF/Grammar/Printer.hs b/src/compiler/GF/Grammar/Printer.hs
index cfd2ce416..13a06b826 100644
--- a/src/compiler/GF/Grammar/Printer.hs
+++ b/src/compiler/GF/Grammar/Printer.hs
@@ -24,8 +24,8 @@ module GF.Grammar.Printer
            ) where
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
 
-import PGF2 as PGF2
-import PGF2.Transactions as PGF2
+import PGF2(Literal(..))
+import PGF2.Transactions(LIndex,LParam,Symbol(..))
 import GF.Infra.Ident
 import GF.Infra.Option
 import GF.Grammar.Values
@@ -108,10 +108,10 @@ ppJudgement q (id, ResParam pparams _) =
   (case pparams of
      Just (L _ ps) -> '=' <+> ppParams q ps
      _             -> empty) <+> ';'
-ppJudgement q (id, ResValue pvalue) =
+ppJudgement q (id, ResValue pvalue idx) =
   "-- param constructor" <+> id <+> ':' <+>
   (case pvalue of
-     (L _ ty) -> ppTerm q 0 ty) <+> ';'
+     (L _ ty) -> ppTerm q 0 ty) <+> ';' <+> parens (pp "index = " <> pp idx)
 ppJudgement q (id, ResOper  ptype pexp) =
   "oper" <+> id <+>
   (case ptype of {Just (L _ t) -> ':'  <+> ppTerm q 0 t; Nothing -> empty} $$
@@ -121,8 +121,8 @@ ppJudgement q (id, ResOverload ids defs) =
   ("overload" <+> '{' $$
    nest 2 (vcat [id <+> (':' <+> ppTerm q 0 ty $$ '=' <+> ppTerm q 0 e <+> ';') | (L _ ty,L _ e) <- defs]) $$
    '}') <+> ';'
-ppJudgement q (id, CncCat pcat pdef pref pprn mpmcfg) =
-  (case pcat of
+ppJudgement q (id, CncCat mtyp pdef pref pprn mpmcfg) =
+  (case mtyp of
      Just (L _ typ) -> "lincat" <+> id <+> '=' <+> ppTerm q 0 typ <+> ';'
      Nothing        -> empty) $$
   (case pdef of
@@ -134,13 +134,13 @@ ppJudgement q (id, CncCat pcat pdef pref pprn mpmcfg) =
   (case pprn of
      Just (L _ prn) -> "printname" <+> id <+> '=' <+> ppTerm q 0 prn <+> ';'
      Nothing        -> empty) $$
-  (case (mpmcfg,q) of
-     (Just (PMCFG lins),Internal)
-                    -> "pmcfg" <+> id <+> '=' <+> '{' $$
-                       nest 2 (vcat (map ppPmcfgLin lins)) $$
+  (case (mtyp,mpmcfg,q) of
+     (Just (L _ typ),Just rules,Internal)
+                    -> "pmcfg" <+> '{' $$
+                       nest 2 (vcat (map (ppPmcfgRule id [] id) rules)) $$
                        '}'
      _              -> empty)
-ppJudgement q (id, CncFun  ptype pdef pprn mpmcfg) =
+ppJudgement q (id, CncFun mtyp pdef pprn mpmcfg) =
   (case pdef of
      Just (L _ e) -> let (xs,e') = getAbs e
                      in "lin" <+> id <+> hsep (map ppBind xs) <+> '=' <+> ppTerm q 0 e' <+> ';'
@@ -148,10 +148,10 @@ ppJudgement q (id, CncFun  ptype pdef pprn mpmcfg) =
   (case pprn of
      Just (L _ prn) -> "printname" <+> id <+> '=' <+> ppTerm q 0 prn <+> ';'
      Nothing        -> empty) $$
-  (case (mpmcfg,q) of
-     (Just (PMCFG lins),Internal)
-                    -> "pmcfg" <+> id <+> '=' <+> '{' $$
-                       nest 2 (vcat (map ppPmcfgLin lins)) $$
+  (case (mtyp,mpmcfg,q) of
+     (Just (args,res,_,_),Just rules,Internal)
+                    -> "pmcfg" <+> '{' $$
+                       nest 2 (vcat (map (ppPmcfgRule id args res) rules)) $$
                        '}'
      _              -> empty)
 ppJudgement q (id, AnyInd cann mid) =
@@ -159,8 +159,12 @@ ppJudgement q (id, AnyInd cann mid) =
     Internal -> "ind" <+> id <+> '=' <+> (if cann then pp "canonical" else empty) <+> mid <+> ';'
     _        -> empty
 
-ppPmcfgLin lin =
-  brackets (vcat (map (hsep . map ppSymbol) lin))
+ppPmcfgRule id arg_cats res_cat (PMCFGRule res args lins) =
+  pp id <+> (':' <+> hsep (intersperse (pp '*') (zipWith ppPmcfgCat arg_cats args)) <+> "->" <+> ppPmcfgCat res_cat res $$
+             '=' <+> brackets (vcat (map (hsep . map ppSymbol) lins)))
+
+ppPmcfgCat :: Ident -> PMCFGCat -> Doc
+ppPmcfgCat cat (PMCFGCat r rs) = pp cat <> parens (ppLinFun ppLParam r rs)
 
 instance Pretty Term where pp = ppTerm Unqualified 0
 
@@ -353,21 +357,21 @@ ppMeta n
   | n == 0    = pp '?'
   | otherwise = pp '?' <> pp n
 
-ppLit (PGF2.LStr s) = pp (show s)
-ppLit (PGF2.LInt n) = pp n
-ppLit (PGF2.LFlt d) = pp d
+ppLit (LStr s) = pp (show s)
+ppLit (LInt n) = pp n
+ppLit (LFlt d) = pp d
 
-ppSymbol (PGF2.SymCat d r rs)= pp '<' <> pp d <> pp ',' <> ppLinFun ppIntVar r rs <> pp '>'
-ppSymbol (PGF2.SymLit d r)   = pp '{' <> pp d <> pp ',' <> pp r <> pp '}'
-ppSymbol (PGF2.SymVar d r)   = pp '<' <> pp d <> pp ',' <> pp '$' <> pp r <> pp '>'
-ppSymbol (PGF2.SymKS t)      = doubleQuotes (pp t)
-ppSymbol PGF2.SymNE          = pp "nonExist"
-ppSymbol PGF2.SymBIND        = pp "BIND"
-ppSymbol PGF2.SymSOFT_BIND   = pp "SOFT_BIND"
-ppSymbol PGF2.SymSOFT_SPACE  = pp "SOFT_SPACE"
-ppSymbol PGF2.SymCAPIT       = pp "CAPIT"
-ppSymbol PGF2.SymALL_CAPIT   = pp "ALL_CAPIT"
-ppSymbol (PGF2.SymKP syms alts) = pp "pre" <+> braces (hsep (punctuate (pp ';') (hsep (map ppSymbol syms) : map ppAlt alts)))
+ppSymbol (SymCat d r rs)= pp '<' <> pp d <> pp ',' <> ppLinFun ppLParam r rs <> pp '>'
+ppSymbol (SymLit d r)   = pp '{' <> pp d <> pp ',' <> pp r <> pp '}'
+ppSymbol (SymVar d r)   = pp '<' <> pp d <> pp ',' <> pp '$' <> pp r <> pp '>'
+ppSymbol (SymKS t)      = doubleQuotes (pp t)
+ppSymbol SymNE          = pp "nonExist"
+ppSymbol SymBIND        = pp "BIND"
+ppSymbol SymSOFT_BIND   = pp "SOFT_BIND"
+ppSymbol SymSOFT_SPACE  = pp "SOFT_SPACE"
+ppSymbol SymCAPIT       = pp "CAPIT"
+ppSymbol SymALL_CAPIT   = pp "ALL_CAPIT"
+ppSymbol (SymKP syms alts) = pp "pre" <+> braces (hsep (punctuate (pp ';') (hsep (map ppSymbol syms) : map ppAlt alts)))
 
 ppLinFun ppParam r rs
   | r == 0 && not (null rs) = hcat (intersperse (pp '+') (       map ppTerm rs))
@@ -377,7 +381,7 @@ ppLinFun ppParam r rs
       | i == 1    = ppParam p
       | otherwise = pp i <> pp '*' <> ppParam p
 
-ppIntVar p
+ppLParam p
   | i == 0    = pp (chars !! j)
   | otherwise = pp (chars !! j : show i)
   where
diff --git a/src/compiler/GF/Infra/CheckM.hs b/src/compiler/GF/Infra/CheckM.hs
index 5fa8365af..6ad8d72e0 100644
--- a/src/compiler/GF/Infra/CheckM.hs
+++ b/src/compiler/GF/Infra/CheckM.hs
@@ -16,7 +16,7 @@ module GF.Infra.CheckM
           (Check, CheckResult(..), Message, runCheck, runCheck',
            checkError, checkCond, checkWarn, checkWarnings, checkAccumError,
            checkIn, checkInModule, checkMap, checkMapRecover,
-           parallelCheck, accumulateError, commitCheck,
+           accumulateError, commitCheck,
           ) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
@@ -118,39 +118,15 @@ runCheck' opts c =
     list = vcat . reverse
     wlist ws = if verbAtLeast opts Normal then list ws else empty
 
-parallelCheck :: [Check a] -> Check [a]
-parallelCheck cs =
-  Check $ \ {-ctxt-} (es0,ws0) ->
-  let os = [unCheck c {-[]-} ([],[])|c<-cs] `using` parList rseq
-      (msgs1,crs) = unzip os
-      (ess,wss) = unzip msgs1
-      rs = [r | Success r<-crs]
-      fs = [f | Fail f<-crs]
-      msgs = (concat ess++es0,concat wss++ws0)
-  in if null fs
-     then (msgs,Success rs)
-     else (msgs,Fail (vcat $ reverse fs))
-
 checkMap :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b)
 checkMap f map = do xs <- mapM (\(k,v) -> do v <- f k v
                                              return (k,v)) (Map.toList map)
                     return (Map.fromAscList xs)
 
 checkMapRecover :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b)
-checkMapRecover f = fmap Map.fromList . parallelCheck . map f' . Map.toList
+checkMapRecover f = fmap Map.fromList . mapM f' . Map.toList
   where f' (k,v) = fmap ((,)k) (f k v)
 
-{-
-checkMapRecover f mp = do
-  let xs = map (\ (k,v) -> (k,runCheck (f k v))) (Map.toList mp)
-  case [s | (_,Bad s) <- xs] of
-    ss@(_:_) -> checkError (text (unlines ss))
-    _   -> do
-      let (kx,ss) = unzip [((k,x),s) | (k, Ok (x,s)) <- xs]
-      if not (all null ss) then checkWarn (text (unlines ss)) else return ()
-      return (Map.fromAscList kx)
--}
-
 checkIn :: Doc -> Check a -> Check a
 checkIn msg c = Check $ \{-ctxt-} msgs0 ->
     case unCheck c {-ctxt-} ([],[]) of
diff --git a/src/runtime/haskell/PGF2/Transactions.hsc b/src/runtime/haskell/PGF2/Transactions.hsc
index cda9883ad..41c5625e4 100644
--- a/src/runtime/haskell/PGF2/Transactions.hsc
+++ b/src/runtime/haskell/PGF2/Transactions.hsc
@@ -13,7 +13,7 @@ module PGF2.Transactions
           , setAbstractFlag
 
             -- concrete syntax
-          , Token, LIndex, Symbol(..)
+          , Token, LIndex, LParam, Symbol(..)
           ) where
 
 import PGF2.FFI
@@ -153,9 +153,9 @@ setAbstractFlag name value = Transaction $ \c_db c_revision c_exn ->
 
 type Token  = String
 type LIndex = Int
-type Param  = Int
+type LParam = Int
 data Symbol
-  = SymCat {-# UNPACK #-} !Int {-# UNPACK #-} !LIndex [(LIndex,Param)]
+  = SymCat {-# UNPACK #-} !Int {-# UNPACK #-} !LIndex [(LIndex,LParam)]
   | SymLit {-# UNPACK #-} !Int {-# UNPACK #-} !LIndex
   | SymVar {-# UNPACK #-} !Int {-# UNPACK #-} !Int
   | SymKS Token