{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./VSE/Ana.hs
Description :  static analysis of VSE parts
Copyright   :  (c) C. Maeder, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

analysis of VSE logic extension of CASL
-}

module VSE.Ana
  ( VSESign
  , uTrue
  , uFalse
  , aTrue
  , aFalse
  , uBoolean
  , constBoolType
  , boolSig
  , lookupProc
  , procsToOpMap
  , procsToPredMap
  , profileToOpType
  , profileToPredType
  , checkCases
  , basicAna
  , mapDlformula
  , minExpForm
  , simpDlformula
  , correctSign
  , correctTarget
  , inducedExt
  , VSEMorExt
  , VSEMor
  , VSEBasicSpec
  , extVSEColimit
  , vseMorExt
  ) where

import Control.Monad
import Data.Char (toLower)
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.ExtSign
import Common.Id
import Common.Result
import Common.Utils (hasMany)
import Common.Lib.State

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign
import CASL.MixfixParser
import CASL.MapSentence as MapSen
import CASL.Morphism
import CASL.Overload
import CASL.Quantification
import CASL.StaticAna
import CASL.ShowMixfix as Paren
import CASL.SimplifySen

import VSE.As
import VSE.Fold

import Data.Graph.Inductive.Graph
import Common.Lib.Graph

type VSESign = Sign Dlformula Procs

getVariables :: Sentence -> Set.Set Token
getVariables = foldFormula $ getVarsRec $ getVSEVars . unRanged

getVarsRec :: (f -> Set.Set Token) -> Record f (Set.Set Token) (Set.Set Token)
getVarsRec f =
  (constRecord f Set.unions Set.empty)
  { foldQuantification = \ _ _ vs r _ -> Set.union r
      $ Set.fromList $ map fst $ flatVAR_DECLs vs
  , foldQual_var = \ _ v _ _ -> Set.singleton v }

getVSEVars :: VSEforms -> Set.Set Token
getVSEVars vf = case vf of
  Dlformula _ p s -> Set.union (getProgVars p) $ getVariables s
  Defprocs l -> Set.unions $ map getDefprogVars l
  _ -> Set.empty -- no variables in a sort generation constraint

getProgVars :: Program -> Set.Set Token
getProgVars =
  let vrec = getVarsRec $ const Set.empty
      getTermVars = foldTerm vrec
      getCondVars = foldFormula vrec
  in foldProg (progToSetRec getTermVars getCondVars)
  { foldAssign = \ _ v t -> Set.insert v $ getTermVars t
  , foldBlock = \ _ vs p -> Set.union p
      $ Set.fromList $ map fst $ flatVAR_DECLs vs }

getDefprogVars :: Defproc -> Set.Set Token
getDefprogVars (Defproc _ _ vs p _) = Set.union (getProgVars p)
  $ Set.fromList vs

tokenToLower :: Token -> Token
tokenToLower (Token s r) = Token (map toLower s) r

idToLower :: Id -> Id
idToLower (Id ts cs r) = Id (map tokenToLower ts) (map idToLower cs) r

getCases :: String -> Set.Set Id -> [Diagnosis]
getCases msg =
  map (mkDiag Error ("overlapping " ++ msg ++ " identifiers") . Set.toList)
  . filter hasMany . Map.elems
  . Set.fold (\ i -> MapSet.setInsert (idToLower i) i) Map.empty

getCaseDiags :: Sign f e -> [Diagnosis]
getCaseDiags sig =
  getCases "sort" (sortSet sig)
  ++ getCases "op or function" (MapSet.keysSet $ opMap sig)
  ++ getCases "pred or proc" (MapSet.keysSet $ predMap sig)

uBoolean :: Id
uBoolean = stringToId "Boolean"

uTrue :: Id
uTrue = stringToId "True"

uFalse :: Id
uFalse = stringToId "False"

tBoolean :: OP_TYPE
tBoolean = Op_type Total [] uBoolean nullRange

constBoolType :: OpType
constBoolType = toOpType tBoolean

qBoolean :: Id -> OP_SYMB
qBoolean c = Qual_op_name c tBoolean nullRange

qTrue :: OP_SYMB
qTrue = qBoolean uTrue

qFalse :: OP_SYMB
qFalse = qBoolean uFalse

mkConstAppl :: OP_SYMB -> TERM f
mkConstAppl o = Application o [] nullRange

aTrue :: TERM f
aTrue = mkConstAppl qTrue

aFalse :: TERM f
aFalse = mkConstAppl qFalse

uOpMap :: OpMap
uOpMap = MapSet.fromList $ map (\ c -> (c, [constBoolType]))
  [uFalse, uTrue]

boolSig :: Sign f Procs
boolSig = (emptySign emptyProcs)
  { sortRel = Rel.insertKey uBoolean Rel.empty
  , opMap = uOpMap }

lookupProc :: Id -> Sign f Procs -> Maybe Profile
lookupProc i = Map.lookup i . procsMap . extendedInfo

procsSign :: Sign f Procs -> Sign f Procs
procsSign sig = (emptySign emptyProcs)
 { predMap = procsToPredMap $ extendedInfo sig }

-- | add procs as predicate
addProcs :: Sign f Procs -> Sign f Procs
addProcs sig = addSig const sig $ procsSign sig

-- | remove procs as predicate
subProcs :: Sign f Procs -> Sign f Procs
subProcs sig = diffSig const sig $ procsSign sig

checkCases :: Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases sig2 sens = getCaseDiags sig2 ++ concatMap
    (getCases "var" . Set.map simpleIdToId . getVariables . sentence) sens

type VSEBasicSpec = BASIC_SPEC () Procdecls Dlformula

basicAna :: (VSEBasicSpec, VSESign, GlobalAnnos)
         -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
basicAna (bs, sig, ga) = do
  let sigIn = subProcs $ addSig const sig boolSig
  (bs2, ExtSign sig2 syms, sens) <-
    basicAnalysis minExpForm (const return) anaProcdecls anaMix
        (bs, sigIn, ga)
  appendDiags $ checkCases sig2 sens
  appendDiags . map
    (mkDiag Error "illegal predicate declaration for procedure")
    . Set.toList . MapSet.keysSet . interMapSet
      (diffMapSet (predMap sig2) $ predMap sigIn)
    . procsToPredMap $ extendedInfo sig2
  let sig3 = diffSig const sig2 boolSig
      (rSens, fSens) = partition (foldFormula (checkRec True) . sentence) sens
  appendDiags $ map (mkDiag Error "unsupported VSE formula" . sentence) fSens
  appendDiags . map (mkDiag Error "illegal overloading of")
    . Set.toList . Set.intersection (MapSet.keysSet $ opMap sig3)
    $ MapSet.keysSet uOpMap
  return (bs2, ExtSign (addProcs sig3) syms, rSens)

anaMix :: Mix () Procdecls Dlformula Procs
anaMix = emptyMix
  { putParen = parenDlFormula
  , mixResolve = resolveDlformula }

-- | put parens around ambiguous mixfix formulas (for error messages)
parenDlFormula :: Dlformula -> Dlformula
parenDlFormula (Ranged f r) = case f of
  Dlformula b p s ->
    let n = mapFormula parenDlFormula s
    in Ranged (Dlformula b (parenProg p) n) r
  Defprocs ps -> Ranged (Defprocs $ map parenDefproc ps) r
  _ -> Ranged f r -- no mixfix formulas?

parenProg :: Program -> Program
parenProg = foldProg $ mapProg (Paren.mapTerm id) $ mapFormula id

parenDefproc :: Defproc -> Defproc
parenDefproc (Defproc k i vs p r) = Defproc k i vs (parenProg p) r

procsToPredMap :: Procs -> PredMap
procsToPredMap (Procs m) =
  foldr (\ (n, pr@(Profile _ mr)) pm -> case mr of
          Nothing -> MapSet.insert n (profileToPredType pr) pm
          Just _ -> pm) MapSet.empty $ Map.toList m

procsToOpMap :: Procs -> OpMap
procsToOpMap (Procs m) =
  foldr (\ (n, pr) om -> case profileToOpType pr of
          Just ot -> MapSet.insert n ot om
          Nothing -> om) MapSet.empty $ Map.toList m

-- | resolve mixfix applications of terms and formulas
resolveDlformula :: MixResolve Dlformula
resolveDlformula ga rules (Ranged f r) = case f of
  Dlformula b p s -> do
    np <- resolveProg ga rules p
    n <- resolveMixFrm id resolveDlformula ga rules s
    return $ Ranged (Dlformula b np n) r
  Defprocs ps -> do
    nps <- mapM (resolveDefproc ga rules) ps
    return $ Ranged (Defprocs nps) r
  _ -> return $ Ranged f r -- no mixfix?

resolveT :: MixResolve (TERM ())
resolveT = resolveMixTrm id (mixResolve emptyMix)

resolveF :: MixResolve (FORMULA ())
resolveF = resolveMixFrm id (mixResolve emptyMix)

resolveProg :: MixResolve Program
resolveProg ga rules p@(Ranged prg r) = case prg of
  Abort -> return p
  Skip -> return p
  Assign v t -> do
    nt <- resolveT ga rules t
    return $ Ranged (Assign v nt) r
  Call f -> do
    nf <- resolveF ga rules f
    return $ Ranged (Call nf) r
  Return t -> do
    nt <- resolveT ga rules t
    return $ Ranged (Return nt) r
  Block vs q -> do
    np <- resolveProg ga rules q
    return $ Ranged (Block vs np) r
  Seq p1 p2 -> do
    p3 <- resolveProg ga rules p1
    p4 <- resolveProg ga rules p2
    return $ Ranged (Seq p3 p4) r
  If f p1 p2 -> do
    c <- resolveF ga rules f
    p3 <- resolveProg ga rules p1
    p4 <- resolveProg ga rules p2
    return $ Ranged (If c p3 p4) r
  While f q -> do
    c <- resolveF ga rules f
    np <- resolveProg ga rules q
    return $ Ranged (While c np) r

resolveDefproc :: MixResolve Defproc
resolveDefproc ga rules (Defproc k i vs p r) = do
  np <- resolveProg ga rules p
  return $ Defproc k i vs np r

-- | resolve overloading and type check terms and formulas
minExpForm :: Min Dlformula Procs
minExpForm sign (Ranged f r) = let sig = castSign sign in case f of
  Dlformula b p s -> do
    np <- minExpProg Set.empty Nothing sig p
    n <- minExpFORMULA minExpForm sign s
    return $ Ranged (Dlformula b np n) r
  Defprocs ps -> do
    nps <- mapM (minProcdecl sig) ps
    return $ Ranged (Defprocs nps) r
  _ -> fail "nyi for restricted constraints"

oneExpT :: Sign () Procs -> TERM () -> Result (TERM ())
oneExpT = oneExpTerm (const return)

minExpF :: Sign () Procs -> FORMULA () -> Result (FORMULA ())
minExpF = minExpFORMULA (const return)

checkRec :: Bool -> Record f Bool Bool
checkRec b = (constRecord (const False) and True)
  { foldQuantification = \ _ _ _ _ _ -> b
  , foldDefinedness = \ _ _ _ -> False
  , foldEquation = \ _ _ e _ _ -> e == Strong
  , foldMembership = \ _ _ _ _ -> False
  , foldCast = \ _ _ _ _ -> False
  , foldConditional = \ _ _ _ _ _ -> False
  , foldExtFORMULA = \ _ _ -> b }

minExpProg :: Set.Set VAR -> Maybe SORT -> Sign () Procs
           -> Program -> Result Program
minExpProg invars res sig p@(Ranged prg r) = let
  checkCond f = if foldFormula (checkRec False) f then return f else
                    mkError "illegal formula" f
  checkTerm t = if foldTerm (checkRec False) t then return t else
                    mkError "illegal term" t
  in case prg of
  Abort -> return p
  Skip -> return p
  Assign v t -> case Map.lookup v $ varMap sig of
    Nothing -> Result [mkDiag Error "undeclared program variable" v] Nothing
    Just s -> do
      nt <- oneExpT sig $ Sorted_term t s r
      checkTerm nt
      when (Set.member v invars)
        $ appendDiags [mkDiag Warning "assignment to input variable" v]
      return $ Ranged (Assign v nt) r
  Call f -> case f of
    Predication ps ts _ -> let i = predSymbName ps in
      case lookupProc i sig of
        Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
        Just pr@(Profile l re) -> let
          nl = case re of
             Nothing -> l
             Just s -> l ++ [Procparam Out s]
          in if length nl /= length ts then
          Result [mkDiag Error "non-matching number of parameters for" i]
          Nothing
             else do
          sign <- if length l < length nl then
            Result [mkDiag Warning "function used as procedure" i] $ Just
              sig { predMap = MapSet.insert i (funProfileToPredType pr)
                    $ predMap sig }
            else return sig { predMap = MapSet.insert i (profileToPredType pr)
                    $ predMap sig }
          nf <- minExpF sign f
          checkCond nf
          return $ Ranged (Call nf) r
    _ -> Result [mkDiag Error "no procedure call" f] Nothing
  Return t -> case res of
    Nothing -> Result [mkDiag Error "unexpected return statement" t] Nothing
    Just s -> do
      nt <- oneExpT sig $ Sorted_term t s r
      checkTerm nt
      return $ Ranged (Return nt) r
  Block vs q -> do
    let sign' = execState (mapM_ addVSEVars vs) sig { envDiags = [] }
    appendDiags $ envDiags sign'
    np <- minExpProg invars res sign' q
    return $ Ranged (Block vs np) r
  Seq p1 p2 -> do
    p3 <- minExpProg invars res sig p1
    p4 <- minExpProg invars res sig p2
    return $ Ranged (Seq p3 p4) r
  If f p1 p2 -> do
    c <- minExpF sig f
    checkCond c
    p3 <- minExpProg invars res sig p1
    p4 <- minExpProg invars res sig p2
    return $ Ranged (If c p3 p4) r
  While f q -> do
    c <- minExpF sig f
    checkCond c
    np <- minExpProg invars res sig q
    return $ Ranged (While c np) r

addVSEVars :: VAR_DECL -> State (Sign f Procs) ()
addVSEVars vd@(Var_decl vs _ _) = do
    addVars vd
    p <- gets $ procsMap . extendedInfo
    mapM_ (addDiags . checkWithMap "var" "procedure" p . simpleIdToId) vs

minProcdecl :: Sign () Procs -> Defproc -> Result Defproc
minProcdecl sig (Defproc k i vs p r) = case lookupProc i sig of
    Nothing -> Result [mkDiag Error "unknown procedure" i] Nothing
    Just (Profile l re) -> if length vs /= length l then
      Result [mkDiag Error "unknown procedure" i] Nothing
      else do
        let invars = Set.fromList $ map fst $
              filter (\ (_, Procparam j _) -> j == In) $ zip vs l
        np <- minExpProg invars re sig { varMap = Map.fromList $ zipWith
                (\ v (Procparam _ s) -> (v, s)) vs l } p
        return $ Defproc k i vs np r

-- | analyse and add procedure declarations
anaProcdecls :: Ana Procdecls () Procdecls Dlformula Procs
anaProcdecls _ ds@(Procdecls ps _) = do
  mapM_ (anaProcdecl . item) ps
  return ds

anaProcdecl :: Sigentry -> State (Sign Dlformula Procs) ()
anaProcdecl (Procedure i p@(Profile ps mr) q) = do
     e <- get
     let prM = predMap e
         l = MapSet.lookup i prM
         ea = emptyAnno ()
         isPred = case mr of
           Nothing -> Set.member (profileToPredType p) l
           _ -> False
     updateExtInfo (\ pm@(Procs m) ->
       let n = Procs $ Map.insert i p m in case Map.lookup i m of
         Just o -> if p == o then
           hint n ("repeated procedure " ++ showId i "") q
           else plain_error pm
             ("cannot change profile of procedure " ++ showId i "") q
         Nothing -> if isPred then plain_error pm
           ("cannot change predicate to procedure " ++ showId i "") q
           else return n)
     case profileToOpType p of
       Just t -> do
         unless (all (\ (Procparam j _) -> j == In) ps)
           $ addDiags [mkDiag Warning "function must have IN params only" i]
         addOp ea t i
       _ -> unless isPred
         $ addAnnoSet ea $ Symbol i $ PredAsItemType $ profileToPredType p

paramsToArgs :: [Procparam] -> [SORT]
paramsToArgs = map (\ (Procparam _ s) -> s)

profileToPredType :: Profile -> PredType
profileToPredType (Profile a _) = PredType $ paramsToArgs a

funProfileToPredType :: Profile -> PredType
funProfileToPredType (Profile a r) = case r of
  Nothing -> error "funProfileToPredType"
  Just s -> PredType $ paramsToArgs a ++ [s]

profileToOpType :: Profile -> Maybe OpType
profileToOpType (Profile a r) = case r of
  Nothing -> Nothing
  Just s -> Just $ OpType Partial (paramsToArgs a) s

castSign :: Sign f e -> Sign a e
castSign s = s { sentences = [] }

castMor :: Morphism f e b -> Morphism a e b
castMor m = m
  { msource = castSign $ msource m
  , mtarget = castSign $ mtarget m }

type VSEMorExt = DefMorExt Procs
type VSEMor = Morphism Dlformula Procs VSEMorExt

-- | apply a morphism
mapMorProg :: Morphism f Procs VSEMorExt -> Program -> Program
mapMorProg mor = let m = castMor mor in
  foldProg (mapProg (MapSen.mapTerm (const id) m)
    $ mapSen (const id) m)
    { foldBlock = \ (Ranged _ r) vs p ->
        Ranged (Block (map (mapVars m) vs) p) r
    , foldCall = \ (Ranged _ r) f -> case f of
     Predication (Qual_pred_name i (Pred_type args r1) r2) ts r3 ->
      case lookupProc i $ msource mor of
        Nothing -> error "mapMorProg"
        Just pr -> let
          j = mapProcIdProfile mor i pr
          nargs = map (mapSrt mor) args
          nts = map (MapSen.mapTerm (const id) m) ts
          in Ranged (Call $ Predication
                (Qual_pred_name j (Pred_type nargs r1) r2) nts r3) r
     _ -> error $ "mapMorProg " ++ show f }

mapProcId :: Morphism f Procs VSEMorExt -> Id -> Id
mapProcId m i = case lookupProc i $ msource m of
  Just p -> mapProcIdProfile m i p
  Nothing -> error $ "VSE.mapProcId unknown " ++ show i

mapProcIdProfile :: Morphism f Procs VSEMorExt -> Id -> Profile -> Id
mapProcIdProfile m = mapProcIdProfileExt (sort_map m) (op_map m) (pred_map m)

mapProcIdProfileExt :: Sort_map -> Op_map -> Pred_map -> Id -> Profile -> Id
mapProcIdProfileExt sm om pm i p = case profileToOpType p of
  Just t -> fst $ mapOpSym sm om (i, t)
  Nothing -> fst $ mapPredSym sm pm (i, profileToPredType p)

mapMorDefproc :: Morphism f Procs VSEMorExt -> Defproc -> Defproc
mapMorDefproc m (Defproc k i vs p r) =
  Defproc k (mapProcId m i) vs (mapMorProg m p) r

mapDlformula :: MapSen Dlformula Procs VSEMorExt
mapDlformula m (Ranged f r) = case f of
  Dlformula b p s ->
    let n = mapSen mapDlformula m s
    in Ranged (Dlformula b (mapMorProg m p) n) r
  Defprocs ps -> Ranged (Defprocs $ map (mapMorDefproc m) ps) r
  RestrictedConstraint constr restr flag ->
   Ranged
    (RestrictedConstraint
       (map (MapSen.mapConstr m) constr)
       (Map.fromList
        $ map (\ (s, i) -> (mapSort (sort_map m) s, mapProcId m i))
        $ Map.toList restr)
    flag) r

-- | simplify fully qualified terms and formulas for pretty printing sentences
simpProg :: Sign () e -> Program -> Program
simpProg sig =
  foldProg (mapProg (simplifyCASLTerm sig)
  $ simplifyCASLSen sig)
    { foldBlock = \ (Ranged b r) _ _ -> case b of
                  Block vs p -> Ranged (Block vs $ simpProg
                           (execState (mapM_ addVars vs) sig) p) r
                  _ -> error "VSE.Ana.simpProg" }

simpDefproc :: Sign () Procs -> Defproc -> Defproc
simpDefproc sign (Defproc k i vs p r) =
  let sig = case lookupProc i sign of
              Nothing -> sign
              Just (Profile l _) -> if length vs /= length l then sign
                else sign { varMap = Map.fromList $ zipWith
                            (\ v (Procparam _ s) -> (v, s)) vs l }
  in Defproc k i vs (simpProg sig p) r

simpDlformula :: Sign Dlformula Procs -> Dlformula -> Dlformula
simpDlformula sign (Ranged f r) = let sig = castSign sign in case f of
  Dlformula b p s -> let
    q = simpProg sig p
    n = simplifySen minExpForm simpDlformula sign s
    in Ranged (Dlformula b q n) r
  Defprocs ps -> Ranged (Defprocs $ map (simpDefproc sig) ps) r
  RestrictedConstraint {} -> Ranged f r
    -- how should this be for restricted constraints?

-- | free variables to be universally bound on the top level
freeProgVars :: Sign () e -> Program -> VarSet
freeProgVars sig = let ft = freeTermVars sig in
  foldProg (progToSetRec ft (freeVars sig))
  { foldAssign = \ _ v t -> (case Map.lookup v $ varMap sig of
      Just s -> Set.insert (v, s)
      Nothing -> Set.insert (v, sortOfTerm t)) $ ft t
  , foldBlock = \ (Ranged b _) _ _ -> case b of
      Block vs p ->
        Set.difference (freeProgVars (execState (mapM_ addVars vs) sig) p)
          $ Set.fromList $ flatVAR_DECLs vs
      _ -> error "VSE.Ana.freeProgVars" }

freeDlVars :: Sign Dlformula e -> Dlformula -> VarSet
freeDlVars sig (Ranged f _) = case f of
  Dlformula _ p s -> Set.union (freeProgVars (castSign sig) p) $
          freeVars sig s
  Defprocs _ -> Set.empty
  RestrictedConstraint {} -> Set.empty

instance TermExtension Dlformula where
  freeVarsOfExt = freeDlVars

-- | adjust procs map in morphism target signature
correctTarget :: Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget m = m
  { mtarget = correctSign $ mtarget m
  , msource = correctSign $ msource m }

inducedExt :: InducedSign f Procs VSEMorExt Procs
inducedExt sm om pm _ = Procs . Map.fromList
    . map (\ (i, p) -> (mapProcIdProfileExt sm om pm i p, mapProfile sm p))
    . Map.toList . procsMap . extendedInfo

correctSign :: Sign f Procs -> Sign f Procs
correctSign sig = sig
  { extendedInfo = Procs $ Map.filterWithKey (\ i p -> case profileToOpType p of
         Just t -> let s = MapSet.lookup i $ opMap sig in
           Set.member t s || Set.member (mkTotal t) s
         Nothing ->
           Set.member (profileToPredType p) . MapSet.lookup i $ predMap sig
         ) $ procsMap $ extendedInfo sig }

mapProfile :: Sort_map -> Profile -> Profile
mapProfile m (Profile l r) = Profile
  (map (\ (Procparam k s) -> Procparam k $ mapSort m s) l)
  $ fmap (mapSort m) r

extVSEColimit :: Gr Procs (Int, VSEMorExt) ->
                  Map.Map Int VSEMor ->
                  (Procs, Map.Map Int VSEMorExt)
extVSEColimit graph morMap = let
  procs = Map.fromList $ nub $
          concatMap (\ (n, Procs p) -> let
            phi = Map.findWithDefault (error "extVSEColimit") n morMap
           in map (\ (idN, profile) ->
                    (mapProcId phi idN, mapProfile (sort_map phi) profile)) $
              Map.toList p) $
          labNodes graph
 in (Procs procs, Map.fromList $ map (\ n -> (n, emptyMorExt)) $
                  nodes graph)

vseMorExt :: CASLMor -> (Op_map, Pred_map)
vseMorExt m = let
  sm = Map.toList $ sort_map m
  om = op_map m
  pm = pred_map m
  eqOps = Map.fromList $ map (\ (s, t) ->
    ((gnEqName s, OpType Partial [s, s] uBoolean)
    , (gnEqName t, Partial))) sm
  restrPreds = Map.fromList $ map (\ (s, t) ->
    ((gnRestrName s, PredType [s]), gnRestrName t)) sm
  opsProcs = Map.fromList $ map (\ ((idN, OpType _ w s), (idN', _)) ->
    ((mkGenName idN, OpType Partial w s)
    , (mkGenName idN', Partial))) $ Map.toList om
  predProcs = Map.fromList $ map (\ ((idN, PredType w), idN') ->
    ((mkGenName idN, PredType w), mkGenName idN')) $ Map.toList pm
  in (Map.union eqOps opsProcs, Map.union restrPreds predProcs)
