{-# LANGUAGE BangPatterns, RankNTypes, FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
----------------------------------------------------------------------
-- |
-- Maintainer  : Krasimir Angelov
-- Stability   : (stable)
-- Portability : (portable)
--
-- Convert PGF grammar to PMCFG grammar.
--
-----------------------------------------------------------------------------

module GF.Compile.GeneratePMCFG
    (generatePMCFG, pgfCncCat, addPMCFG, resourceValues
    ) where

--import PGF.CId
import PGF.Internal as PGF(CncCat(..),Symbol(..),fidVar)

import GF.Infra.Option
import GF.Grammar hiding (Env, mkRecord, mkTable)
import GF.Grammar.Lookup
import GF.Grammar.Predef
import GF.Grammar.Lockfield (isLockLabel)
import GF.Data.BacktrackM
import GF.Data.Operations
import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
import GF.Data.Utilities (updateNthM) --updateNth
import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.List as List
--import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import GF.Text.Pretty
import Data.Array.IArray
import Data.Array.Unboxed
--import Data.Maybe
--import Data.Char (isDigit)
import Control.Applicative(Applicative(..))
import Control.Monad
import Control.Monad.Identity
--import Control.Exception
--import Debug.Trace(trace)

----------------------------------------------------------------------
-- main conversion function

--generatePMCFG :: Options -> SourceGrammar -> Maybe FilePath -> SourceModule -> IOE SourceModule
generatePMCFG opts sgr opath cmo@(cm,cmi) = do
  (seqs,js) <- mapAccumWithKeyM (addPMCFG opts gr cenv opath am cm) Map.empty (jments cmi)
  when (verbAtLeast opts Verbose) $ ePutStrLn ""
  return (cm,cmi{mseqs = Just (mkSetArray seqs), jments = js})
  where
    cenv = resourceValues opts gr
    gr = prependModule sgr cmo
    MTConcrete am = mtype cmi

mapAccumWithKeyM :: (Monad m, Ord k) => (a -> k -> b -> m (a,c)) -> a
                                     -> Map.Map k b -> m (a,Map.Map k c)
mapAccumWithKeyM f a m = do let xs = Map.toAscList m
                            (a,ys) <- mapAccumM f a xs
                            return (a,Map.fromAscList ys)
  where
    mapAccumM f a []          = return (a,[])
    mapAccumM f a ((k,x):kxs) = do (a,y ) <- f a k x
                                   (a,kys) <- mapAccumM f a kxs
                                   return (a,(k,y):kys)


--addPMCFG :: Options -> SourceGrammar -> GlobalEnv -> Maybe FilePath -> Ident -> Ident -> SeqSet -> Ident -> Info -> IOE (SeqSet, Info)
addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont,val)) mlin@(Just (L loc term)) mprn Nothing) = do
--when (verbAtLeast opts Verbose) $ ePutStr ("\n+ "++showIdent id++" ...")
  let pres  = protoFCat gr res val
      pargs = [protoFCat gr (snd $ catSkeleton ty) lincat | ((_,_,ty),(_,_,lincat)) <- zip ctxt cont]

      pmcfgEnv0   = emptyPMCFGEnv
  b             <- convert opts gr cenv (floc opath loc id) term (cont,val) pargs
  let (seqs1,b1) = addSequencesB seqs b
      pmcfgEnv1  = foldBM addRule
                          pmcfgEnv0
                          (goB b1 CNil [])
                          (pres,pargs)
      pmcfg      = getPMCFG pmcfgEnv1
      
      stats      = let PMCFG prods funs = pmcfg
                       (s,e)            = bounds funs
                       !prods_cnt       = length prods
                       !funs_cnt        = e-s+1
                   in (prods_cnt,funs_cnt)

  when (verbAtLeast opts Verbose) $
    ePutStr ("\n+ "++showIdent id++" "++show (product (map catFactor pargs)))
  seqs1 `seq` stats `seq` return ()
  when (verbAtLeast opts Verbose) $ ePutStr (" "++show stats)
  return (seqs1,GF.Grammar.CncFun mty mlin mprn (Just pmcfg))
  where
    (ctxt,res,_) = err bug typeForm (lookupFunType gr am id)

    addRule lins (newCat', newArgs') env0 =
      let [newCat] = getFIds newCat'
          !fun     = mkArray lins
          newArgs  = map getFIds newArgs'
      in addFunction env0 newCat fun newArgs

addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat)) 
                                                             mdef@(Just (L loc1 def))
                                                             mref@(Just (L loc2 ref))
                                                             mprn
                                                             Nothing) = do
  let pcat = protoFCat gr (am,id) lincat
      pvar = protoFCat gr (MN identW,cVar) typeStr

      pmcfgEnv0  = emptyPMCFGEnv

  let lincont    = [(Explicit, varStr, typeStr)]
  b             <- convert opts gr cenv (floc opath loc1 id) def (lincont,lincat) [pvar]
  let (seqs1,b1) = addSequencesB seqs b
      pmcfgEnv1  = foldBM addLindef
                          pmcfgEnv0
                          (goB b1 CNil [])
                          (pcat,[pvar])

  let lincont    = [(Explicit, varStr, lincat)]
  b             <- convert opts gr cenv (floc opath loc2 id) ref (lincont,typeStr) [pcat]
  let (seqs2,b2) = addSequencesB seqs1 b
      pmcfgEnv2  = foldBM addLinref
                          pmcfgEnv1
                          (goB b2 CNil [])
                          (pvar,[pcat])

  let pmcfg     = getPMCFG pmcfgEnv2

  when (verbAtLeast opts Verbose) $ ePutStr ("\n+ "++showIdent id++" "++show (catFactor pcat))
  seqs2 `seq` pmcfg `seq` return (seqs2,GF.Grammar.CncCat mty mdef mref mprn (Just pmcfg))
  where
    addLindef lins (newCat', newArgs') env0 =
      let [newCat] = getFIds newCat'
          !fun     = mkArray lins
      in addFunction env0 newCat fun [[fidVar]]

    addLinref lins (newCat', [newArg']) env0 =
      let newArg   = getFIds newArg'
          !fun     = mkArray lins
      in addFunction env0 fidVar fun [newArg]

addPMCFG opts gr cenv opath am cm seqs id info = return (seqs, info)

floc opath loc id = maybe (L loc id) (\path->L (External path loc) id) opath

convert opts gr cenv loc term ty@(_,val) pargs =
  case normalForm cenv loc (etaExpand ty term) of
    Error s -> fail $ render $ ppL loc ("Predef.error: "++s)
    term    -> return $ runCnvMonad gr (convertTerm opts CNil val term) (pargs,[])
  where
    etaExpand (context,val) = mkAbs pars . flip mkApp args
      where pars = [(Explicit,v) | v <- vars]
            args = map Vr vars
            vars = map (\(bt,x,t) -> x) context

pgfCncCat :: SourceGrammar -> Type -> Int -> CncCat
pgfCncCat gr lincat index =
  let ((_,size),schema) = computeCatRange gr lincat
  in PGF.CncCat index (index+size-1)
                      (mkArray (map (renderStyle style{mode=OneLineMode} . ppPath) 
                                    (getStrPaths schema)))
  where
    getStrPaths :: Schema Identity s c -> [Path]
    getStrPaths = collect CNil []
      where
        collect path paths (CRec rs)   = foldr (\(lbl,Identity t) paths -> collect (CProj lbl path) paths t) paths rs
        collect path paths (CTbl _ cs) = foldr (\(trm,Identity t) paths -> collect (CSel  trm path) paths t) paths cs
        collect path paths (CStr _)    = reversePath path : paths
        collect path paths (CPar _)    = paths

----------------------------------------------------------------------
-- CnvMonad monad
--
-- The branching monad provides backtracking together with
-- recording of the choices made. We have two cases
-- when we have alternative choices:
--
--      * when we have parameter type, then
--        we have to try all possible values
--      * when we have variants we have to try all alternatives
--
-- The conversion monad keeps track of the choices and they are
-- returned as 'Branch' data type.

data Branch a
  = Case Int Path [(Term,Branch a)]
  | Variant [Branch a]
  | Return  a

newtype CnvMonad a = CM {unCM :: SourceGrammar
                              -> forall b . (a -> ([ProtoFCat],[Symbol]) -> Branch b)
                              -> ([ProtoFCat],[Symbol])
                              -> Branch b}

instance Applicative CnvMonad where
  pure = return
  (<*>) = ap

instance Monad CnvMonad where
    return a   = CM (\gr c s -> c a s)
    CM m >>= k = CM (\gr c s -> m gr (\a s -> unCM (k a) gr c s) s)

instance MonadState ([ProtoFCat],[Symbol]) CnvMonad where
    get = CM (\gr c s -> c s s)
    put s = CM (\gr c _ -> c () s)

instance Functor CnvMonad where
    fmap f (CM m) = CM (\gr c s -> m gr (c . f) s)

runCnvMonad :: SourceGrammar -> CnvMonad a -> ([ProtoFCat],[Symbol]) -> Branch a
runCnvMonad gr (CM m) s = m gr (\v s -> Return v) s

-- | backtracking for all variants
variants :: [a] -> CnvMonad a
variants xs = CM (\gr c s -> Variant [c x s | x <- xs])

-- | backtracking for all parameter values that a variable could take
choices :: Int -> Path -> CnvMonad Term
choices nr path = do (args,_) <- get
                     let PFCat _ _ schema = args !! nr
                     descend schema path CNil
  where
    descend (CRec rs)     (CProj lbl path) rpath = case lookup lbl rs of
                                                     Just (Identity t) -> descend t path (CProj lbl rpath)
    descend (CRec rs)     CNil             rpath = do rs <- mapM (\(lbl,Identity t) -> fmap (assign lbl) (descend t CNil (CProj lbl rpath))) rs
                                                      return (R rs)
    descend (CTbl pt cs)  (CSel  trm path) rpath = case lookup trm cs of
                                                     Just (Identity t) -> descend t path (CSel trm rpath)
    descend (CTbl pt cs)  CNil             rpath = do cs <- mapM (\(trm,Identity t) -> descend t CNil (CSel trm rpath)) cs
                                                      return (V pt cs)
    descend (CPar (m,vs)) CNil             rpath = case vs of
                                                     [(value,index)] -> return value
                                                     values          -> let path = reversePath rpath
                                                                        in CM (\gr c s -> Case nr path [(value, updateEnv path value gr c s)
                                                                                                                    | (value,index) <- values])
    descend schema       path              rpath = bug $ "descend "++show (schema,path,rpath)

    updateEnv path value gr c (args,seq) = 
      case updateNthM (restrictProtoFCat path value) nr args of
        Just args -> c value (args,seq)
        Nothing   -> bug "conflict in updateEnv"

-- | the argument should be a parameter type and then
-- the function returns all possible values.
getAllParamValues :: Type -> CnvMonad [Term]
getAllParamValues ty = CM (\gr c -> c (err bug id (allParamValues gr ty)))

mkRecord :: [(Label,CnvMonad (Schema Branch s c))] -> CnvMonad (Schema Branch s c)
mkRecord xs = CM (\gr c -> foldl (\c (lbl,CM m) bs s -> c ((lbl,m gr (\v s -> Return v) s) : bs) s) (c . CRec) xs [])

mkTable  :: Type -> [(Term ,CnvMonad (Schema Branch s c))] -> CnvMonad (Schema Branch s c)
mkTable pt xs = CM (\gr c -> foldl (\c (trm,CM m) bs s -> c ((trm,m gr (\v s -> Return v) s) : bs) s) (c . CTbl pt) xs [])

----------------------------------------------------------------------
-- Term Schema
--
-- The term schema is a term-like structure, with records, tables,
-- strings and parameters values, but in addition we could add
-- annotations of arbitrary types

-- | Term schema
data Schema b s c
  = CRec      [(Label,b (Schema b s c))]
  | CTbl Type [(Term, b (Schema b s c))]
  | CStr s
  | CPar c
--deriving Show -- doesn't work

instance Show s => Show (Schema b s c) where
  showsPrec _ sch =
      case sch of
        CRec r   -> showString "CRec " . shows (map fst r)
        CTbl t _ -> showString "CTbl " . showsPrec 10 t . showString " _"
        CStr s   -> showString "CStr " . showsPrec 10 s
        CPar c   -> showString "CPar{}"

-- | Path into a term or term schema
data Path
  = CProj Label Path
  | CSel  Term  Path
  | CNil
  deriving (Eq,Show)

-- | The ProtoFCat represents a linearization type as term schema.
-- The annotations are as follows: the strings are annotated with
-- their index in the PMCFG tuple, the parameters are annotated
-- with their value both as term and as index.
data ProtoFCat  = PFCat Ident Int (Schema Identity Int (Int,[(Term,Int)]))
type Env        = (ProtoFCat, [ProtoFCat])

protoFCat :: SourceGrammar -> Cat -> Type -> ProtoFCat
protoFCat gr cat lincat =
  case computeCatRange gr lincat of
    ((_,f),schema) -> PFCat (snd cat) f schema

getFIds :: ProtoFCat -> [FId]
getFIds (PFCat _ _ schema) =
  reverse (solutions (variants schema) ())
  where
    variants (CRec rs)         = fmap sum $ mapM (\(lbl,Identity t) -> variants t) rs
    variants (CTbl _ cs)       = fmap sum $ mapM (\(trm,Identity t) -> variants t) cs
    variants (CStr _)          = return 0
    variants (CPar (m,values)) = do (value,index) <- member values
                                    return (m*index)

catFactor :: ProtoFCat -> Int
catFactor (PFCat _ f _) = f

computeCatRange gr lincat = compute (0,1) lincat
  where
    compute st (RecType  rs) = let (st',rs') = List.mapAccumL (\st (lbl,t) -> case lbl of
                                                                                LVar _ -> let (st',t') = compute st t
                                                                                          in (st ,(lbl,Identity t'))
                                                                                _      -> let (st',t') = compute st t
                                                                                          in (st',(lbl,Identity t'))) st rs
                               in (st',CRec rs')
    compute st (Table pt vt) = let vs        = err bug id (allParamValues gr pt)
                                   (st',cs') = List.mapAccumL (\st v       -> let (st',vt') = compute st vt
                                                                              in (st',(v,Identity vt'))) st vs
                               in (st',CTbl pt cs')
    compute st (Sort s)
                   | s == cStr = let (index,m) = st
                                 in ((index+1,m),CStr index)
    compute st t               = let vs = err bug id (allParamValues gr t)
                                     (index,m) = st
                                 in ((index,m*length vs),CPar (m,zip vs [0..]))

ppPath (CProj lbl path) = lbl <+> ppPath path
ppPath (CSel  trm path) = ppU 5 trm   <+> ppPath path
ppPath CNil             = empty

reversePath path = rev CNil path
  where
    rev path0 CNil             = path0
    rev path0 (CProj lbl path) = rev (CProj lbl path0) path
    rev path0 (CSel  trm path) = rev (CSel  trm path0) path


----------------------------------------------------------------------
-- term conversion

type Value a = Schema Branch a Term

convertTerm :: Options -> Path -> Type -> Term -> CnvMonad (Value [Symbol])
convertTerm opts sel ctype (Vr x)       = convertArg opts ctype (getVarIndex x) (reversePath sel)
convertTerm opts sel ctype (Abs _ _ t)  = convertTerm opts sel ctype t                -- there are only top-level abstractions and we ignore them !!!
convertTerm opts sel ctype (R record)   = convertRec opts sel ctype record
convertTerm opts sel ctype (P term l)   = convertTerm opts (CProj l sel) ctype term
convertTerm opts sel ctype (V pt ts)    = convertTbl opts sel ctype pt ts
convertTerm opts sel ctype (S term p)   = do v <- evalTerm CNil p
                                             convertTerm opts (CSel v sel) ctype term
convertTerm opts sel ctype (FV vars)    = do term <- variants vars
                                             convertTerm opts sel ctype term
convertTerm opts sel ctype (C t1 t2)    = do v1 <- convertTerm opts sel ctype t1
                                             v2 <- convertTerm opts sel ctype t2
                                             return (CStr (concat [s | CStr s <- [v1,v2]]))
convertTerm opts sel ctype (K t)        = return (CStr [SymKS t])
convertTerm opts sel ctype Empty        = return (CStr [])
convertTerm opts sel ctype (Alts s alts)= do CStr s <- convertTerm opts CNil ctype s
                                             alts <- forM alts $ \(u,alt) -> do
                                                            CStr u <- convertTerm opts CNil ctype u
                                                            Strs ps <- unPatt alt
                                                            ps     <- mapM (convertTerm opts CNil ctype) ps
                                                            return (u,map unSym ps)
                                             return (CStr [SymKP s alts])
  where
    unSym (CStr [])        = ""
    unSym (CStr [SymKS t]) = t
    unSym _                = ppbug $ hang ("invalid prefix in pre expression:") 4 (Alts s alts)

    unPatt (EPatt p) = fmap Strs (getPatts p)
    unPatt u         = return u

    getPatts p = case p of
      PAlt a b  -> liftM2 (++) (getPatts a) (getPatts b)
      PString s -> return [K s]
      PSeq a b  -> do
        as <- getPatts a
        bs <- getPatts b
        return [K (s ++ t) | K s <- as, K t <- bs]
      _ -> fail (render ("not valid pattern in pre expression" <+> ppPatt Unqualified 0 p))

convertTerm opts sel ctype (Q (m,f))
  | m == cPredef &&
    f == cBIND                          = return (CStr [SymBIND])
  | m == cPredef &&
    f == cSOFT_BIND                     = return (CStr [SymSOFT_BIND])
  | m == cPredef &&
    f == cSOFT_SPACE                    = return (CStr [SymSOFT_SPACE])
  | m == cPredef &&
    f == cCAPIT                         = return (CStr [SymCAPIT])
  | m == cPredef &&
    f == cALL_CAPIT                     = return (CStr [SymALL_CAPIT])
  | m == cPredef &&
    f == cNonExist                      = return (CStr [SymNE])
{-
convertTerm opts sel@(CProj l _) ctype (ExtR t1 t2@(R rs2))
                    | l `elem` map fst rs2 = convertTerm opts sel ctype t2
                    | otherwise            = convertTerm opts sel ctype t1

convertTerm opts sel@(CProj l _) ctype (ExtR t1@(R rs1) t2)
                    | l `elem` map fst rs1 = convertTerm opts sel ctype t1
                    | otherwise            = convertTerm opts sel ctype t2
-}
convertTerm opts CNil ctype t           = do v <- evalTerm CNil t
                                             return (CPar v)
convertTerm _    sel  _     t           = ppbug ("convertTerm" <+> sep [parens (show sel),ppU 10 t])

convertArg :: Options -> Term -> Int -> Path -> CnvMonad (Value [Symbol])
convertArg opts (RecType rs)  nr path =
  mkRecord (map (\(lbl,ctype) -> (lbl,convertArg opts ctype nr (CProj lbl path))) rs)
convertArg opts (Table pt vt) nr path = do
  vs <- getAllParamValues pt
  mkTable pt (map (\v -> (v,convertArg opts vt nr (CSel v path))) vs)
convertArg opts (Sort _)      nr path = do
  (args,_) <- get
  let PFCat cat _ schema = args !! nr
      l = index (reversePath path) schema
      sym | CProj (LVar i) CNil <- path = SymVar nr i
          | isLiteralCat opts cat       = SymLit nr l
          | otherwise                   = SymCat nr l
  return (CStr [sym])
  where
    index (CProj lbl path) (CRec   rs) = case lookup lbl rs of
                                           Just (Identity t) -> index path t
    index (CSel  trm path) (CTbl _ rs) = case lookup trm rs of
                                           Just (Identity t) -> index path t
    index CNil             (CStr idx)  = idx
convertArg opts ty nr path              = do
  value <- choices nr (reversePath path)
  return (CPar value)

convertRec opts CNil (RecType rs) record =
    mkRecord [(lbl,convertTerm opts CNil ctype (proj lbl))|(lbl,ctype)<-rs]
  where proj lbl = if isLockLabel lbl then R [] else projectRec lbl record
convertRec opts (CProj lbl path) ctype record =
  convertTerm opts path ctype (projectRec lbl record)
convertRec opts _ ctype _ = bug ("convertRec: "++show ctype)

convertTbl opts CNil (Table _ vt) pt ts = do
  vs <- getAllParamValues pt
  mkTable pt (zipWith (\v t -> (v,convertTerm opts CNil vt t)) vs ts)
convertTbl opts (CSel v sub_sel) ctype pt ts = do
  vs <- getAllParamValues pt
  case lookup v (zip vs ts) of
    Just t  -> convertTerm opts sub_sel ctype t
    Nothing -> ppbug ( "convertTbl:" <+> ("missing value" <+> v $$
                                          "among" <+> vcat vs))
convertTbl opts _ ctype _ _ = bug ("convertTbl: "++show ctype)


goB :: Branch (Value SeqId) -> Path -> [SeqId] -> BacktrackM Env [SeqId]
goB (Case nr path bs) rpath ss = do (value,b) <- member bs
                                    restrictArg nr path value
                                    goB b rpath ss
goB (Variant bs)      rpath ss = do b <- member bs
                                    goB b rpath ss
goB (Return  v)       rpath ss = goV v rpath ss

goV :: Value SeqId -> Path -> [SeqId] -> BacktrackM Env [SeqId]
goV (CRec xs)    rpath ss = foldM (\ss (lbl,b) -> goB b (CProj lbl rpath) ss) ss (reverse xs)
goV (CTbl _ xs)  rpath ss = foldM (\ss (trm,b) -> goB b (CSel  trm rpath) ss) ss (reverse xs)
goV (CStr seqid) rpath ss = return (seqid : ss)
goV (CPar t)     rpath ss = restrictHead (reversePath rpath) t >> return ss


----------------------------------------------------------------------
-- SeqSet

type SeqSet   = Map.Map Sequence SeqId

addSequencesB :: SeqSet -> Branch (Value [Symbol]) -> (SeqSet, Branch (Value SeqId))
addSequencesB seqs (Case nr path bs) = let !(seqs1,bs1) = mapAccumL' (\seqs (trm,b) -> let !(seqs',b') = addSequencesB seqs b
                                                                                       in (seqs',(trm,b'))) seqs bs
                                       in (seqs1,Case nr path bs1)
addSequencesB seqs (Variant bs)      = let !(seqs1,bs1) = mapAccumL' addSequencesB seqs bs
                                       in (seqs1,Variant bs1)
addSequencesB seqs (Return  v)       = let !(seqs1,v1) = addSequencesV seqs v
                                       in (seqs1,Return v1)

addSequencesV :: SeqSet -> Value [Symbol] -> (SeqSet, Value SeqId)
addSequencesV seqs (CRec vs)  = let !(seqs1,vs1) = mapAccumL' (\seqs (lbl,b) -> let !(seqs',b') = addSequencesB seqs b
                                                                                in (seqs',(lbl,b'))) seqs vs
                                in (seqs1,CRec vs1)
addSequencesV seqs (CTbl pt vs)=let !(seqs1,vs1) = mapAccumL' (\seqs (trm,b) -> let !(seqs',b') = addSequencesB seqs b
                                                                                in (seqs',(trm,b'))) seqs vs
                                in (seqs1,CTbl pt vs1)
addSequencesV seqs (CStr lin) = let !(seqs1,seqid) = addSequence seqs lin
                                in (seqs1,CStr seqid)
addSequencesV seqs (CPar i)   = (seqs,CPar i)

-- a strict version of Data.List.mapAccumL
mapAccumL' f s []     = (s,[])
mapAccumL' f s (x:xs) = (s'',y:ys)
                        where !(s', y ) = f s x
                              !(s'',ys) = mapAccumL' f s' xs

addSequence :: SeqSet -> [Symbol] -> (SeqSet,SeqId)
addSequence seqs lst =
  case Map.lookup seq seqs of
    Just id -> (seqs,id)
    Nothing -> let !last_seq = Map.size seqs
               in (Map.insert seq last_seq seqs, last_seq)
  where
    seq = mkArray lst


------------------------------------------------------------
-- eval a term to ground terms

evalTerm :: Path -> Term -> CnvMonad Term
evalTerm CNil (QC f)       = return (QC f)
evalTerm CNil (App x y)    = do x <- evalTerm CNil x
                                y <- evalTerm CNil y
                                return (App x y)
evalTerm path (Vr x)       = choices (getVarIndex x) path
evalTerm path (R rs)       =
    case path of
      CProj lbl path -> evalTerm path (projectRec lbl rs)
      CNil           -> R `fmap` mapM (\(lbl,(_,t)) -> assign lbl `fmap` evalTerm path t) rs
evalTerm path (P term lbl) = evalTerm (CProj lbl path) term
evalTerm path (V pt ts)    =
   case path of
     CNil          -> V pt `fmap` mapM (evalTerm path) ts
     CSel trm path ->
         do vs <- getAllParamValues pt
            case lookup trm (zip vs ts) of
              Just t  -> evalTerm path t
              Nothing -> ppbug $ "evalTerm: missing value:"<+>trm
                                 $$ "among:" <+>fsep (map (ppU 10) vs)
evalTerm path (S term sel) = do v <- evalTerm CNil sel
                                evalTerm (CSel v path) term
evalTerm path (FV terms)   = variants terms >>= evalTerm path
evalTerm path (EInt n)     = return (EInt n)
evalTerm path t            = ppbug ("evalTerm" <+> parens t)
--evalTerm path t            = ppbug (text "evalTerm" <+> sep [parens (text (show path)),parens (text (show t))])

getVarIndex x = maybe err id $ getArgIndex x
  where err = bug ("getVarIndex "++show x)

----------------------------------------------------------------------
-- GrammarEnv

data PMCFGEnv = PMCFGEnv !ProdSet !FunSet
type ProdSet  = Set.Set Production
type FunSet   = Map.Map (UArray LIndex SeqId) FunId

emptyPMCFGEnv =
  PMCFGEnv Set.empty Map.empty

addFunction :: PMCFGEnv -> FId -> UArray LIndex SeqId -> [[FId]] -> PMCFGEnv
addFunction (PMCFGEnv prodSet funSet) !fid fun args =
  case Map.lookup fun funSet of
    Just !funid -> PMCFGEnv (Set.insert (Production fid funid args) prodSet)
                            funSet
    Nothing     -> let !funid = Map.size funSet
                   in PMCFGEnv (Set.insert (Production fid funid args) prodSet)
                               (Map.insert fun funid funSet)

getPMCFG :: PMCFGEnv -> PMCFG
getPMCFG (PMCFGEnv prodSet funSet) =
  PMCFG (optimize prodSet) (mkSetArray funSet)
  where
    optimize ps = Map.foldrWithKey ff [] (Map.fromListWith (++) [((fid,funid),[args]) | (Production fid funid args) <- Set.toList ps])
      where
        ff :: (FId,FunId) -> [[[FId]]] -> [Production] -> [Production]
        ff (fid,funid) xs prods
          | product (map IntSet.size ys) == count
                      = (Production fid funid (map IntSet.toList ys)) : prods
          | otherwise = map (Production fid funid) xs ++ prods
          where
            count = sum (map (product . map length) xs)
            ys    = foldl (zipWith (foldr IntSet.insert)) (repeat IntSet.empty) xs

------------------------------------------------------------
-- updating the MCF rule

restrictArg :: LIndex -> Path -> Term -> BacktrackM Env ()
restrictArg nr path index = do
  (head, args) <- get
  args <- updateNthM (restrictProtoFCat path index) nr args
  put (head, args)

restrictHead :: Path -> Term -> BacktrackM Env ()
restrictHead path term = do
  (head, args) <- get
  head <- restrictProtoFCat path term head
  put (head, args)

restrictProtoFCat :: (Functor m, MonadPlus m) => Path -> Term -> ProtoFCat -> m ProtoFCat
restrictProtoFCat path v (PFCat cat f schema) = do
  schema <- addConstraint path v schema
  return (PFCat cat f schema)
  where
    addConstraint (CProj lbl path) v (CRec rs)     = fmap CRec      $ update lbl (addConstraint path v) rs
    addConstraint (CSel  trm path) v (CTbl pt cs)  = fmap (CTbl pt) $ update trm (addConstraint path v) cs
    addConstraint CNil             v (CPar (m,vs)) = case lookup v vs of
                                                       Just index -> return (CPar (m,[(v,index)]))
                                                       Nothing    -> mzero
    addConstraint CNil             v (CStr _)      = bug "restrictProtoFCat: string path"
    
    update k0 f [] = return []
    update k0 f (x@(k,Identity v):xs)
      | k0 == k    = do v <- f v
                        return ((k,Identity v):xs)
      | otherwise  = do xs <- update k0 f xs
                        return (x:xs)

mkArray    lst = listArray (0,length lst-1) lst
mkSetArray map = array (0,Map.size map-1) [(v,k) | (k,v) <- Map.toList map]

bug msg = ppbug msg
ppbug msg = error . render $ hang "Internal error in GeneratePMCFG:" 4 msg

ppU = ppTerm Unqualified