{- |
Module      :  ./CASL/StaticAna.hs
Description :  CASL static analysis for basic specifications
Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

CASL static analysis for basic specifications

Follows Chaps. III:2 and III:3 of the CASL Reference Manual.

The static analysis takes an abstract syntax tree of a basic specification
and outputs a signature and a set of formulas, while checking that
- all sorts used in operation and predicate declarations have been declared
- all sorts, operation and predicate symbols used in formulas have
  been declared
- formulas type-check
The formulas are returned with fully-qualified variables, operation
and predicate symbols.

The static analysis functions are parameterized with functions for
treating CASL extensions, that is, additional basic items, signature
items and formulas.
-}

module CASL.StaticAna where

import CASL.AS_Basic_CASL
import CASL.MixfixParser
import CASL.Overload
import CASL.Quantification
import CASL.Sign
import CASL.ToDoc

import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.GlobalAnnotations
import Common.Id
import Common.Keywords
import Common.Lib.State
import Common.Result
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import Control.Monad

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
import Data.List

checkPlaces :: [SORT] -> Id -> [Diagnosis]
checkPlaces args i = let n = placeCount i in
    [mkDiag Error "wrong number of places" i | n > 0 && n /= length args ]

checkWithVars :: String -> Map.Map SIMPLE_ID a -> Id -> [Diagnosis]
checkWithVars s m i@(Id ts _ _) = if isSimpleId i then
    case Map.lookup (head ts) m of
    Nothing -> []
    Just _ -> alsoWarning s varS i
    else []

addOp :: Annoted a -> OpType -> Id -> State (Sign f e) ()
addOp a ty i =
    do checkSorts (opRes ty : opArgs ty)
       e <- get
       let m = opMap e
           l = MapSet.lookup i m
           ds = checkWithOtherMap opS predS (predMap e) i
                ++ checkWithVars opS (varMap e) i
           check = addDiags $
                   (if Set.member ty l then [mkDiag Hint "redeclared op" i]
                    else checkPlaces (opArgs ty) i ++ checkNamePrefix i)
                   ++ ds
           store = put e { opMap = addOpTo i ty m }
           pTy = mkPartial ty
       case opKind ty of
          Partial -> if Set.member (mkTotal ty) l then
                     addDiags $ mkDiag Warning "partially redeclared" i : ds
                     else store >> check
          Total -> if Set.member pTy l then do
                         put e { opMap = MapSet.insert i ty
                                   $ MapSet.delete i pTy m }
                         addDiags $ mkDiag Hint "redeclared as total" i : ds
                   else store >> check
       addAnnoSet a $ Symbol i $ OpAsItemType ty

addAssocOp :: OpType -> Id -> State (Sign f e) ()
addAssocOp ty i = do
       e <- get
       put e { assocOps = addOpTo i ty $ assocOps e
             , globAnnos = updAssocMap (addAssocId i) $ globAnnos e
             }

updateExtInfo :: (e -> Result e) -> State (Sign f e) ()
updateExtInfo upd = do
    s <- get
    let re = upd $ extendedInfo s
    case maybeResult re of
         Nothing -> return ()
         Just e -> put s { extendedInfo = e }
    addDiags $ diags re

addPred :: Annoted a -> PredType -> Id -> State (Sign f e) ()
addPred a ty i =
    do checkSorts $ predArgs ty
       e <- get
       let m = predMap e
           l = MapSet.lookup i m
           ds = checkWithOtherMap predS opS (opMap e) i
                ++ checkWithVars predS (varMap e) i
       if Set.member ty l then
          addDiags $ mkDiag Hint "redeclared pred" i : ds
          else do
            put e { predMap = MapSet.insert i ty m }
            addDiags $ checkPlaces (predArgs ty) i ++ checkNamePrefix i ++ ds
       addAnnoSet a $ Symbol i $ PredAsItemType ty

nonConsts :: OpMap -> Set.Set Id
nonConsts = MapSet.keysSet . MapSet.filter (not . null . opArgs)

opMapConsts :: OpMap -> Set.Set Id
opMapConsts = MapSet.keysSet . MapSet.filter (null . opArgs)

allOpIds :: Sign f e -> Set.Set Id
allOpIds = nonConsts . opMap

allConstIds :: Sign f e -> Set.Set Id
allConstIds = opMapConsts . opMap

addAssocs :: Sign f e -> GlobalAnnos -> GlobalAnnos
addAssocs e =
  updAssocMap (\ m -> Set.fold addAssocId m $ MapSet.keysSet $ assocOps e)

updAssocMap :: (AssocMap -> AssocMap) -> GlobalAnnos -> GlobalAnnos
updAssocMap f ga = ga { assoc_annos = f $ assoc_annos ga }

addAssocId :: Id -> AssocMap -> AssocMap
addAssocId i m = case Map.lookup i m of
                   Nothing -> Map.insert i ALeft m
                   _ -> m

formulaIds :: Sign f e -> Set.Set Id
formulaIds e = let ops = allOpIds e in
    Set.fromDistinctAscList (map simpleIdToId $ Map.keys $ varMap e)
               `Set.union` ops

allPredIds :: Sign f e -> Set.Set Id
allPredIds = MapSet.keysSet . predMap

addSentences :: [Named (FORMULA f)] -> State (Sign f e) ()
addSentences ds =
    do e <- get
       put e { sentences = reverse ds ++ sentences e }

-- * traversing all data types of the abstract syntax

ana_BASIC_SPEC :: (FormExtension f, TermExtension f) => Min f e
               -> Ana b b s f e -> Ana s b s f e -> Mix b s f e
               -> BASIC_SPEC b s f -> State (Sign f e) (BASIC_SPEC b s f)
ana_BASIC_SPEC mef ab anas mix (Basic_spec al) = fmap Basic_spec $
      mapAnM (ana_BASIC_ITEMS mef ab anas mix) al

-- looseness of a datatype
data GenKind = Free | Generated | Loose deriving (Show, Eq, Ord)

unionGenAx :: [GenAx] -> GenAx
unionGenAx = foldr (\ (s1, r1, f1) (s2, r2, f2) ->
                        (Set.union s1 s2,
                         Rel.union r1 r2,
                         Set.union f1 f2)) emptyGenAx

anaVarForms :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
  -> State (Sign f e) [Annoted (FORMULA f)]
anaVarForms mef mix vs fs r = do
   (resFs, fufs) <- anaLocalVarForms (anaForm mef mix) vs fs r
   addSentences $ map makeNamedSen fufs
   return resFs

anaLocalVarForms :: TermExtension f
  => (Sign f e -> FORMULA f -> Result (FORMULA f, FORMULA f))
  -> [VAR_DECL] -> [Annoted (FORMULA f)] -> Range
  -> State (Sign f e) ([Annoted (FORMULA f)], [Annoted (FORMULA f)])
anaLocalVarForms anaFrm il afs ps = do
           e <- get -- save
           mapM_ addVars il
           vds <- gets envDiags
           sign <- get
           unless (null il) $ put e { envDiags = vds }
           -- restore with shadowing warnings
           let (es, resFs, anaFs) = foldr (\ f (dss, ress, ranas) ->
                      let Result ds m = anaFrm sign $ item f
                      in case m of
                         Nothing -> (ds ++ dss, ress, ranas)
                         Just (resF, anaF) ->
                             (ds ++ dss, f {item = resF} : ress,
                                 f {item = anaF} : ranas))
                     ([], [], []) afs
               fufs = map (mapAn (\ f -> quantFreeVars sign
                            (mkForallRange il f ps) ps))
                      anaFs
           addDiags es
           return (resFs, fufs)

anaDatatypeDecls :: GenKind -> SortsKind -> [Annoted DATATYPE_DECL]
  -> State (Sign f e) ()
anaDatatypeDecls gk sk al = do
           let ts = map (\ i -> case item i of
                        Datatype_decl s _ _ -> (i, s)) al
           addDiags . map (\ l -> case l of
              _ : t : _ -> mkDiag (if gk == Loose then Warning else Error)
               "duplicate type name in mutually recursive type definition" t
              _ -> error "anaDatatypeDecls")
               . filter ((> 1) . length) . group . sort $ map snd ts
           mapM_ (uncurry $ addSort sk) ts
           mapAnM (ana_DATATYPE_DECL gk) al
           closeSubsortRel

ana_BASIC_ITEMS :: (FormExtension f, TermExtension f)
  => Min f e -> Ana b b s f e -> Ana s b s f e -> Mix b s f e
    -> BASIC_ITEMS b s f -> State (Sign f e) (BASIC_ITEMS b s f)
ana_BASIC_ITEMS mef ab anas mix bi =
    case bi of
    Sig_items sis -> fmap Sig_items $
                     ana_SIG_ITEMS mef anas mix Loose sis
    Free_datatype sk al ps -> do
           anaDatatypeDecls Free sk al
           toSortGenAx ps True $ getDataGenSig al
           return bi
    Sort_gen al ps -> do
           (gs, ul) <- ana_Generated mef anas mix al
           toSortGenAx ps False $ unionGenAx gs
           return $ Sort_gen ul ps
    Var_items il _ -> do
           mapM_ addVars il
           return bi
    Local_var_axioms il afs ps -> do
        resFs <- anaVarForms mef mix il afs ps
        return $ Local_var_axioms il resFs ps
    Axiom_items afs ps -> do
        resFs <- anaVarForms mef mix [] afs ps
        return $ Axiom_items resFs ps
    Ext_BASIC_ITEMS b -> fmap Ext_BASIC_ITEMS $ ab mix b

mapAn :: (a -> b) -> Annoted a -> Annoted b
mapAn f an = replaceAnnoted (f $ item an) an

type GenAx = (Set.Set SORT, Rel.Rel SORT, Set.Set Component)

emptyGenAx :: GenAx
emptyGenAx = (Set.empty, Rel.empty, Set.empty)

toSortGenAx :: Range -> Bool -> GenAx -> State (Sign f e) ()
toSortGenAx ps isFree (sorts, rel, ops) = do
    let sortList = Set.toList sorts
        opSyms = map (\ c -> let ide = compId c in Qual_op_name ide
                      (toOP_TYPE $ compType c) $ posOfId ide) $ Set.toList ops
        injSyms = map (\ (s, t) -> let p = posOfId s in
                        Qual_op_name (mkUniqueInjName s t)
                        (Op_type Total [s] t p) p) $ Rel.toList
                  $ Rel.irreflex rel
        allSyms = opSyms ++ injSyms
        resType (Op_name _) = error "CASL.StaticAna.resType"
        resType (Qual_op_name _ t _) = res_OP_TYPE t
        argTypes (Op_name _) = error "CASL.StaticAna.argTypes"
        argTypes (Qual_op_name _ t _) = args_OP_TYPE t
        getIndex l s = fromMaybe (-1) $ elemIndex s l
        addIndices l os =
            (os, map (getIndex l) $ argTypes os)
        collectOps s = (s, filter ((== s) . resType) allSyms)
        constrs0 = map collectOps sortList
        dRel = Rel.depSort . Rel.transClosure $ foldr (\ (s, os) r ->
               Set.fold (`Rel.insertDiffPair` s) (Rel.insertKey s r)
               $ Set.unions
               $ map (Set.intersection sorts . Set.fromList . argTypes) os)
               Rel.empty constrs0
        m2 = Map.fromList constrs0
        mkConstr ss =
            let sl = Set.toList ss in
            toSortGenNamed
            (mkSort_gen_ax
            (map (\ s -> Constraint s
                   (map (addIndices sl)
                    $ Map.findWithDefault (error "CASL.StaticAna.mkConstr")
                    s m2) s) sl) isFree) sl
        resList = Set.fromList $ map resType allSyms
        noConsList = Set.difference sorts resList
        voidOps = Set.difference resList sorts
        sens = map mkConstr dRel
    when (null sortList)
      $ addDiags [Diag Error "missing generated sort" ps]
    unless (Set.null noConsList)
      $ addDiags [mkDiag Warning "generated sorts without constructor"
          noConsList]
    unless (Set.null voidOps)
      $ addDiags [mkDiag Warning "non-generated sorts as constructor result"
                  voidOps]
    when (length dRel > 1)
      $ addDiags [mkDiag Warning "splittable groups of generated sorts" dRel]
    addSentences sens

ana_SIG_ITEMS :: (FormExtension f, TermExtension f)
  => Min f e -> Ana s b s f e -> Mix b s f e -> GenKind -> SIG_ITEMS s f
    -> State (Sign f e) (SIG_ITEMS s f)
ana_SIG_ITEMS mef anas mix gk si =
    case si of
    Sort_items sk al ps ->
        do ul <- mapM (ana_SORT_ITEM mef mix sk) al
           closeSubsortRel
           return $ Sort_items sk ul ps
    Op_items al ps ->
        do ul <- mapM (ana_OP_ITEM mef mix) al
           return $ Op_items ul ps
    Pred_items al ps ->
        do ul <- mapM (ana_PRED_ITEM mef mix) al
           return $ Pred_items ul ps
    Datatype_items sk al _ ->
        do anaDatatypeDecls gk sk al
           return si
    Ext_SIG_ITEMS s -> fmap Ext_SIG_ITEMS $ anas mix s

-- helper
ana_Generated :: (FormExtension f, TermExtension f)
  => Min f e -> Ana s b s f e -> Mix b s f e -> [Annoted (SIG_ITEMS s f)]
    -> State (Sign f e) ([GenAx], [Annoted (SIG_ITEMS s f)])
ana_Generated mef anas mix al = do
   ul <- mapAnM (ana_SIG_ITEMS mef anas mix Generated) al
   return (map (getGenSig . item) ul, ul)

getGenSig :: SIG_ITEMS s f -> GenAx
getGenSig si = case si of
      Sort_items _ al _ -> unionGenAx $ map (getGenSorts . item) al
      Op_items al _ -> (Set.empty, Rel.empty,
                           Set.unions (map (getOps . item) al))
      Datatype_items _ dl _ -> getDataGenSig dl
      _ -> emptyGenAx

isConsAlt :: ALTERNATIVE -> Bool
isConsAlt a = case a of
  Subsorts _ _ -> False
  _ -> True

getDataGenSig :: [Annoted DATATYPE_DECL] -> GenAx
getDataGenSig dl =
    let alts = concatMap ((\ (Datatype_decl s al _) ->
                          map (\ a -> (s, item a)) al) . item) dl
        sorts = map fst alts
        (realAlts, subs) = partition (isConsAlt . snd) alts
        cs = map (\ (s, a) ->
               let (i, ty, _) = getConsType s a
               in Component i ty) realAlts
        rel = foldr (\ (t, a) r ->
                  foldr (`Rel.insertDiffPair` t)
                  r $ getAltSubsorts a)
               Rel.empty subs
        in (Set.fromList sorts, rel, Set.fromList cs)

getGenSorts :: SORT_ITEM f -> GenAx
getGenSorts si = let
  (sorts, rel) = case si of
    Sort_decl il _ -> (Set.fromList il, Rel.empty)
    Subsort_decl il i _ ->
      (Set.fromList (i : il), foldr (`Rel.insertDiffPair` i) Rel.empty il)
    Subsort_defn sub _ super _ _ ->
      (Set.singleton sub, Rel.insertDiffPair sub super Rel.empty)
    Iso_decl il _ -> (Set.fromList il,
      foldr (\ s r -> foldr (Rel.insertDiffPair s) r il) Rel.empty il)
    in (sorts, rel, Set.empty)

getOps :: OP_ITEM f -> Set.Set Component
getOps oi = case oi of
    Op_decl is ty _ _ ->
        Set.fromList $ map (flip Component $ toOpType ty) is
    Op_defn i par _ _ -> maybe Set.empty
        (Set.singleton . Component i . toOpType) $ headToType par

ana_SORT_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> SortsKind -> Annoted (SORT_ITEM f)
    -> State (Sign f e) (Annoted (SORT_ITEM f))
ana_SORT_ITEM mef mix sk asi =
    case item asi of
    Sort_decl il _ ->
        do mapM_ (addSort sk asi) il
           return asi
    Subsort_decl il i _ ->
        do mapM_ (addSort sk asi) (i : il)
           mapM_ (addSubsort i) il
           return asi
    Subsort_defn sub v super af ps ->
        do e <- get -- save
           put e { varMap = Map.empty }
           addVars (Var_decl [v] super ps)
           sign <- get
           put e -- restore
           let Result ds mf = anaForm mef mix sign $ item af
               lb = getRLabel af
               lab = if null lb then getRLabel asi else lb
           addDiags ds
           addSort sk asi sub
           addSubsort super sub
           case mf of
             Nothing -> return asi { item = Subsort_decl [sub] super ps}
             Just (resF, anaF) -> do
               let p = posOfId sub
                   pv = tokPos v
               addSentences [(makeNamed lab $
                              mkForallRange [Var_decl [v] super pv]
                              (Relation
                               (Membership (Qual_var v super pv) sub p)
                               Equivalence anaF p) p) {
                              isAxiom = notImplied af }]
               return asi { item = Subsort_defn sub v super
                                   af { item = resF } ps}
    Iso_decl il _ ->
        do mapM_ (addSort sk asi) il
           case il of
               [] -> return ()
               _ : tl -> mapM_ (uncurry $ addSubsortOrIso False)
                         $ zip tl il
           return asi

putVarsInEmptyMap :: [VAR_DECL] -> State (Sign f e) (Sign f e)
putVarsInEmptyMap vs = do
           e <- get -- save
           put e { varMap = Map.empty }
           mapM_ addVars vs
           sign <- get
           put e -- restore
           return sign

ana_OP_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Annoted (OP_ITEM f)
    -> State (Sign f e) (Annoted (OP_ITEM f))
ana_OP_ITEM mef mix aoi =
    case item aoi of
    Op_decl ops ty il ps ->
        do let oty = toOpType ty
               ni = notImplied aoi
           mapM_ (addOp aoi oty) ops
           ul <- mapM (ana_OP_ATTR mef mix oty ni ops) il
           when (any (\ a -> case a of
                  Assoc_op_attr -> True
                  _ -> False) il) $ do
              mapM_ (addAssocOp oty) ops
              when (any (\ a -> case a of
                  Comm_op_attr -> True
                  _ -> False) il)
                   $ addSentences $ map (addLeftComm oty ni) ops
           return aoi {item = Op_decl ops ty (catMaybes ul) ps}
    Op_defn i ohd@(Op_head k vs _ _) at ps ->
        do let mty = headToType ohd
               lb = getRLabel at
               lab = if null lb then getRLabel aoi else lb
               arg = concatMap (\ (Var_decl v s qs) ->
                                 map (\ j -> Qual_var j s qs) v) vs
           maybe (return ()) (\ ty -> addOp aoi (toOpType ty) i) mty
           sign <- putVarsInEmptyMap vs
           let Result ds mt = anaTerm mef mix sign
                 (fmap res_OP_TYPE mty) ps $ item at
           addDiags ds
           case mt of
             Nothing -> return $ maybe aoi
               (\ ty -> aoi { item = Op_decl [i] ty [] ps }) mty
             Just (resT, anaT) -> do
                 let p = posOfId i
                     tvs = freeTermVars sign anaT
                     ty = headToTypeM (Op_type k (sortsOfArgs vs)
                                       (sortOfTerm anaT) ps) id ohd
                 maybe (addOp aoi (toOpType ty) i) (const $ return ()) mty
                 addDiags $ warnUnusedVars " local " sign tvs
                 addSentences [(makeNamed lab $ mkForallRange vs
                     (Equation
                      (Application (Qual_op_name i ty p) arg ps)
                      Strong anaT p) ps) {
                       isAxiom = notImplied at, isDef = True }]
                 return aoi {item = Op_defn i ohd at { item = resT } ps }

headToTypeM :: a -> (OP_TYPE -> a) -> OP_HEAD -> a
headToTypeM def f (Op_head k args mr ps) = maybe def
  (\ r -> f $ Op_type k (sortsOfArgs args) r ps) mr

headToType :: OP_HEAD -> Maybe OP_TYPE
headToType = headToTypeM Nothing Just

sortsOfArgs :: [VAR_DECL] -> [SORT]
sortsOfArgs = concatMap (\ (Var_decl l s _) -> map (const s) l)

threeVars :: SORT -> ([VAR_DECL], [TERM f])
threeVars rty =
      let q = posOfId rty
          ns = map mkSimpleId ["x", "y", "z"]
          vs = map (\ v -> Var_decl [v] rty q) ns
      in (vs, map toQualVar vs)

-- see Isabelle/doc/ref.pdf 10.6 Permutative rewrite rules (p. 137)
addLeftComm :: OpType -> Bool -> Id -> Named (FORMULA f)
addLeftComm ty ni i =
  let sty = toOP_TYPE ty
      rty = opRes ty
      (vs, [v1, v2, v3]) = threeVars rty
      p = posOfId i
      qi = Qual_op_name i sty p
  in (makeNamed ("ga_left_comm_" ++ showId i "") $
             mkForallRange vs
             (Equation
              (Application qi [v1, Application qi [v2, v3] p] p) Strong
              (Application qi [v2, Application qi [v1, v3] p] p) p) p)
            { isAxiom = ni }

ana_OP_ATTR :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> OpType -> Bool -> [Id] -> OP_ATTR f
    -> State (Sign f e) (Maybe (OP_ATTR f))
ana_OP_ATTR mef mix ty ni ois oa = do
  let sty = toOP_TYPE ty
      rty = opRes ty
      atys = opArgs ty
      q = posOfId rty
      tds = case atys of
         [t1, t2] | t1 == t2 -> case oa of
              Comm_op_attr -> []
              _ -> [ Diag Error "result sort must be equal to argument sorts" q
                   | t1 /= rty ]
         _ -> [Diag Error "expecting two arguments of equal sort" q]
  addDiags tds
  case oa of
    Unit_op_attr t -> do
           sign <- get
           let Result ds mt = anaTerm mef mix
                              sign { varMap = Map.empty } (Just rty) q t
           addDiags ds
           case mt of
             Nothing -> return Nothing
             Just (resT, anaT) -> do
               when (null tds) $ do
                 addSentences $ map (makeUnit True anaT ty ni) ois
                 addSentences $ map (makeUnit False anaT ty ni) ois
               return $ Just $ Unit_op_attr resT
    Assoc_op_attr -> do
      let (vs, [v1, v2, v3]) = threeVars rty
          makeAssoc i = let p = posOfId i
                            qi = Qual_op_name i sty p in
            (makeNamed ("ga_assoc_" ++ showId i "") $
             mkForallRange vs
             (Equation
              (Application qi [Application qi [v1, v2] p, v3] p) Strong
              (Application qi [v1, Application qi [v2, v3] p] p) p) p)
            { isAxiom = ni }
      when (null tds) . addSentences $ map makeAssoc ois
      return $ Just oa
    Comm_op_attr -> do
      let ns = map mkSimpleId ["x", "y"]
          vs = zipWith (\ v t -> Var_decl [v] t
                         $ concatMapRange posOfId atys) ns atys
          args = map toQualVar vs
          makeComm i = let p = posOfId i
                           qi = Qual_op_name i sty p in
            (makeNamed ("ga_comm_" ++ showId i "") $
             mkForallRange vs
             (Equation (Application qi args p) Strong
              (Application qi (reverse args) p) p) p) {
             isAxiom = ni }
      when (null tds) . addSentences $ map makeComm ois
      return $ Just oa
    Idem_op_attr -> do
      let v = mkSimpleId "x"
          vd = Var_decl [v] rty q
          qv = toQualVar vd
          makeIdem i = let p = posOfId i in
           (makeNamed ("ga_idem_" ++ showId i "") $
            mkForallRange [vd]
            (Equation
             (Application (Qual_op_name i sty p) [qv, qv] p)
             Strong qv p) p) { isAxiom = ni }
      when (null tds) . addSentences $ map makeIdem ois
      return $ Just oa

-- first bool for left and right, second one for no implied annotation
makeUnit :: Bool -> TERM f -> OpType -> Bool -> Id -> Named (FORMULA f)
makeUnit b t ty ni i =
    let lab = "ga_" ++ (if b then "right" else "left") ++ "_unit_"
              ++ showId i ""
        v = mkSimpleId "x"
        vty = opRes ty
        q = posOfId vty
        p = posOfId i
        qv = Qual_var v vty q
        args = [qv, t]
        rargs = if b then args else reverse args
    in (makeNamed lab $ mkForallRange [Var_decl [v] vty q]
                     (Equation
                      (Application (Qual_op_name i (toOP_TYPE ty) p) rargs p)
                      Strong qv p) p) {isAxiom = ni }

ana_PRED_ITEM :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Annoted (PRED_ITEM f)
    -> State (Sign f e) (Annoted (PRED_ITEM f))
ana_PRED_ITEM mef mix apr = case item apr of
    Pred_decl preds ty _ -> do
      mapM_ (addPred apr $ toPredType ty) preds
      return apr
    Pred_defn i phd@(Pred_head vs rs) at ps -> do
           let lb = getRLabel at
               lab = if null lb then getRLabel apr else lb
               ty = Pred_type (sortsOfArgs vs) rs
               arg = concatMap (\ (Var_decl v s qs) ->
                                 map (\ j -> Qual_var j s qs) v) vs
           addPred apr (toPredType ty) i
           sign <- putVarsInEmptyMap vs
           let Result ds mt = anaForm mef mix sign $ item at
           addDiags ds
           case mt of
             Nothing -> return apr {item = Pred_decl [i] ty ps}
             Just (resF, anaF) -> do
               let p = posOfId i
               addSentences [(makeNamed lab $
                              mkForallRange vs
                              (Relation (Predication (Qual_pred_name i ty p)
                                            arg p) Equivalence anaF p) p) {
                              isDef = True }]
               return apr {item = Pred_defn i phd at { item = resF } ps}

-- full function type of a selector (result sort is component sort)
data Component = Component { compId :: Id, compType :: OpType } deriving Show

instance Eq Component where
    Component i1 t1 == Component i2 t2 =
        (i1, opArgs t1, opRes t1) == (i2, opArgs t2, opRes t2)

instance Ord Component where
    Component i1 t1 <= Component i2 t2 =
        (i1, opArgs t1, opRes t1) <= (i2, opArgs t2, opRes t2)

instance Pretty Component where
    pretty (Component i ty) =
        pretty i <+> colon <> pretty ty

instance GetRange Component where
    getRange = getRange . compId

-- | return list of constructors
ana_DATATYPE_DECL :: GenKind -> DATATYPE_DECL -> State (Sign f e) [Component]
ana_DATATYPE_DECL gk (Datatype_decl s al _) =
    do ul <- mapM (ana_ALTERNATIVE s) al
       let constr = catMaybes ul
           cs = map fst constr
       unless (null constr) $ do
                  addDiags $ checkUniqueness cs
                  let totalSels = Set.unions $ map snd constr
                      wrongConstr = filter ((totalSels /=) . snd) constr
                  addDiags $ map (\ (c, _) -> mkDiag Warning
                      ("total selectors '" ++ showSepList (showString ", ")
                       showDoc (Set.toList totalSels)
                       "'\n  should be in alternative") c) wrongConstr
       case gk of
         Free -> do
           let allts = map item al
               (alts, subs) = partition isConsAlt allts
               sbs = concatMap getAltSubsorts subs
               comps = map (getConsType s) alts
               ttrips = map ((\ (a, vs, t, ses) -> (a, vs, t, catSels ses))
                               . selForms1 "X" ) comps
               sels = concatMap (\ (_, _, _, ses) -> ses) ttrips
           addDiags $ foldr (\ a ds -> case a of
             Alt_construct p i _ _ | p == Partial ->
               mkDiag Error
               "illegal free partial constructor" i : ds
             _ -> ds) [] allts
           addSentences $ map makeInjective
                            $ filter (\ (_, _, ces) -> not $ null ces)
                              comps
           addSentences $ makeDisjSubsorts s sbs
           addSentences $ concatMap (\ c -> map (makeDisjToSort c) sbs)
                        comps
           addSentences $ makeDisjoint comps
           addSentences $ catMaybes $ concatMap
                             (\ ses ->
                               map (makeUndefForm ses) ttrips) sels
         _ -> return ()
       return cs

makeDisjSubsorts :: SORT -> [SORT] -> [Named (FORMULA f)]
makeDisjSubsorts d subs = case subs of
    [] -> []
    s : rs -> map (makeDisjSubsort s) rs ++ makeDisjSubsorts d rs
  where
  makeDisjSubsort :: SORT -> SORT -> Named (FORMULA f)
  makeDisjSubsort s1 s2 = let
     n = mkSimpleId "x"
     pd = posOfId d
     p1 = posOfId s1
     p2 = posOfId s2
     p = pd `appRange` p1 `appRange` p2
     v = Var_decl [n] d pd
     qv = toQualVar v
     in makeNamed ("ga_disjoint_sorts_" ++ showId s1 "_" ++ showId s2 "")
         $ mkForallRange [v] (Negation (Junction Con [
              Membership qv s1 p1, Membership qv s2 p2] p) p) p

makeDisjToSort :: (Id, OpType, [COMPONENTS]) -> SORT -> Named (FORMULA f)
makeDisjToSort a s =
    let (c, v, t, _) = selForms1 "X" a
        p = posOfId s
    in makeNamed ("ga_disjoint_" ++ showId c "_sort_" ++ showId s "")
         $ mkForallRange v (Negation (Membership t s p) p) p

makeInjective :: (Id, OpType, [COMPONENTS]) -> Named (FORMULA f)
makeInjective a =
    let (c, v1, t1, _) = selForms1 "X" a
        (_, v2, t2, _) = selForms1 "Y" a
        p = posOfId c
    in makeNamed ("ga_injective_" ++ showId c "")
        $ mkForallRange (v1 ++ v2)
        (Relation (Equation t1 Strong t2 p) Equivalence
         (let ces = zipWith (\ w1 w2 -> Equation
                              (toQualVar w1) Strong (toQualVar w2) p) v1 v2
          in conjunctRange ces p)
         p) p

makeDisjoint :: [(Id, OpType, [COMPONENTS])] -> [Named (FORMULA f)]
makeDisjoint l = case l of
    [] -> []
    c : cs -> map (makeDisj c) cs ++ makeDisjoint cs
  where
  makeDisj :: (Id, OpType, [COMPONENTS]) -> (Id, OpType, [COMPONENTS])
           -> Named (FORMULA f)
  makeDisj a1 a2 =
    let (c1, v1, t1, _) = selForms1 "X" a1
        (c2, v2, t2, _) = selForms1 "Y" a2
        p = posOfId c1 `appRange` posOfId c2
    in makeNamed ("ga_disjoint_" ++ showId c1 "_" ++ showId c2 "")
        $ mkForallRange (v1 ++ v2) (Negation (Equation t1 Strong t2 p) p) p

catSels :: [(Maybe Id, OpType)] -> [(Id, OpType)]
catSels = map (\ (m, t) -> (fromJust m, t)) .
                 filter (\ (m, _) -> isJust m)

makeUndefForm :: (Id, OpType) -> (Id, [VAR_DECL], TERM f, [(Id, OpType)])
              -> Maybe (Named (FORMULA f))
makeUndefForm (s, ty) (i, vs, t, sels) =
    let p = posOfId s in
    if any (\ (se, ts) -> s == se && opRes ts == opRes ty ) sels
    then Nothing else
       Just $ makeNamed ("ga_selector_undef_" ++ showId s "_" ++ showId i "")
              $ mkForallRange vs
               (Negation
                (Definedness
                 (Application (Qual_op_name s (toOP_TYPE ty) p) [t] p)
                 p) p) p

getAltSubsorts :: ALTERNATIVE -> [SORT]
getAltSubsorts c = case c of
    Subsorts cs _ -> cs
    _ -> []

getConsType :: SORT -> ALTERNATIVE -> (Id, OpType, [COMPONENTS])
getConsType s c =
    let getConsTypeAux (part, i, il) =
          (i, OpType part (concatMap
                            (map (opRes . snd) . getCompType s) il) s, il)
     in case c of
        Subsorts _ _ -> error "getConsType"
        Alt_construct k a l _ -> getConsTypeAux (k, a, l)

getCompType :: SORT -> COMPONENTS -> [(Maybe Id, OpType)]
getCompType s c = case c of
  Cons_select k l cs _ -> map (\ i -> (Just i, OpType k [s] cs)) l
  Sort cs -> [(Nothing, OpType Partial [s] cs)]

genSelVars :: String -> Int -> [OpType] -> [VAR_DECL]
genSelVars str n tys = case tys of
  [] -> []
  ty : rs -> mkVarDecl (mkNumVar str n) (opRes ty)
    : genSelVars str (n + 1) rs

makeSelForms :: Int -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
             -> [Named (FORMULA f)]
makeSelForms n (i, vs, t, tys) = case tys of
  [] -> []
  (mi, ty) : rs ->
    (case mi of
            Nothing -> []
            Just j -> let p = posOfId j
                          rty = opRes ty
                          q = posOfId rty in
              [makeNamed ("ga_selector_" ++ showId j "")
                     $ mkForallRange vs
                      (Equation
                       (Application (Qual_op_name j (toOP_TYPE ty) p) [t] p)
                       Strong (Qual_var (mkNumVar "X" n) rty q) p) p]
    ) ++ makeSelForms (n + 1) (i, vs, t, rs)

selForms1 :: String -> (Id, OpType, [COMPONENTS])
          -> (Id, [VAR_DECL], TERM f, [(Maybe Id, OpType)])
selForms1 str (i, ty, il) =
    let cs = concatMap (getCompType (opRes ty)) il
        vs = genSelVars str 1 $ map snd cs
    in (i, vs, mkAppl (mkQualOp i $ toOP_TYPE ty)
            (map toQualVar vs), cs)

selForms :: (Id, OpType, [COMPONENTS]) -> [Named (FORMULA f)]
selForms = makeSelForms 1 . selForms1 "X"

-- | return the constructor and the set of total selectors
ana_ALTERNATIVE :: SORT -> Annoted ALTERNATIVE
                -> State (Sign f e) (Maybe (Component, Set.Set Component))
ana_ALTERNATIVE s c = case item c of
    Subsorts ss _ -> do
        mapM_ (addSubsort s) ss
        return Nothing
    ic -> do
        let cons@(i, ty, il) = getConsType s ic
        addOp c ty i
        ul <- mapM (ana_COMPONENTS s) il
        let ts = concatMap fst ul
        addDiags $ checkUniqueness (ts ++ concatMap snd ul)
        addSentences $ selForms cons
        return $ Just (Component i ty, Set.fromList ts)

-- | return total and partial selectors
ana_COMPONENTS :: SORT -> COMPONENTS
               -> State (Sign f e) ([Component], [Component])
ana_COMPONENTS s c = do
    let cs = getCompType s c
    sels <- mapM (\ (mi, ty) ->
            case mi of
            Nothing -> return Nothing
            Just i -> do
              addOp (emptyAnno ()) ty i
              return $ Just $ Component i ty) cs
    return $ partition (isTotal . compType) $ catMaybes sels

-- | utility
resultToState :: (a -> Result a) -> a -> State (Sign f e) a
resultToState f a = do
    let r = f a
    addDiags $ diags r
    case maybeResult r of
        Nothing -> return a
        Just b -> return b

-- wrap it all up for a logic

type Ana a b s f e = Mix b s f e -> a -> State (Sign f e) a

anaForm :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Sign f e -> FORMULA f
    -> Result (FORMULA f, FORMULA f)
anaForm mef mixIn sign f = do
    let mix = extendMix (Map.keysSet $ varMap sign) mixIn
    resF <- resolveFormula (putParen mix) (mixResolve mix)
            (globAnnos sign) (mixRules mix) f
    anaF <- minExpFORMULA mef sign resF
    return (resF, anaF)

anaTerm :: (FormExtension f, TermExtension f)
  => Min f e -> Mix b s f e -> Sign f e -> Maybe SORT -> Range -> TERM f
    -> Result (TERM f, TERM f)
anaTerm mef mixIn sign msrt pos t = do
    let mix = extendMix (Map.keysSet $ varMap sign) mixIn
    resT <- resolveMixfix (putParen mix) (mixResolve mix)
            (globAnnos sign) (mixRules mix) t
    anaT <- oneExpTerm mef sign $ maybe resT
      (\ srt -> Sorted_term resT srt pos) msrt
    return (resT, anaT)

basicAnalysis :: (FormExtension f, TermExtension f)
              => Min f e -- ^ type analysis of f
              -> Ana b b s f e  -- ^ static analysis of basic item b
              -> Ana s b s f e  -- ^ static analysis of signature item s
              -> Mix b s f e -- ^ for mixfix analysis
              -> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
  -> Result (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
            {- ^ (BS with analysed mixfix formulas for pretty printing,
            differences to input Sig,accumulated Sig,analysed Sentences) -}
basicAnalysis mef anab anas mix (bs, inSig, ga) =
    let allIds = unite $ ids_BASIC_SPEC (getBaseIds mix) (getSigIds mix) bs
                 : getExtIds mix (extendedInfo inSig) :
                  [mkIdSets (allConstIds inSig) (allOpIds inSig)
                  $ allPredIds inSig]
        (newBs, accSig) = runState (ana_BASIC_SPEC mef anab anas
               mix { mixRules = makeRules ga allIds }
               bs) inSig { globAnnos = addAssocs inSig ga }
        ds = reverse $ envDiags accSig
        sents = reverse $ sentences accSig
        cleanSig = (emptySign $ extendedInfo accSig)
                   { emptySortSet = emptySortSet accSig
                   , sortRel = sortRel accSig
                   , opMap = opMap accSig
                   , assocOps = assocOps accSig
                   , predMap = predMap accSig
                   , annoMap = annoMap accSig
                   , globAnnos = ga }
    in Result (ds ++ warnUnused accSig sents) $
       Just (newBs, ExtSign cleanSig $ declaredSymbols accSig, sents)

basicCASLAnalysis :: (BASIC_SPEC () () (), Sign () (), GlobalAnnos)
  -> Result (BASIC_SPEC () () (),
             ExtSign (Sign () ()) Symbol,
             [Named (FORMULA ())])
basicCASLAnalysis = basicAnalysis (const return) (const return)
                                  (const return) emptyMix

-- | extra
cASLsen_analysis ::
        (BASIC_SPEC () () (), Sign () (), FORMULA ()) -> Result (FORMULA ())
cASLsen_analysis (bs, s, f) = let
                         mix = emptyMix
                         allIds = unite $
                                ids_BASIC_SPEC (getBaseIds mix)
                                               (getSigIds mix) bs
                                : getExtIds mix (extendedInfo s) :
                                [mkIdSets (allConstIds s) (allOpIds s)
                                $ allPredIds s]
                         mix' = mix { mixRules = makeRules emptyGlobalAnnos
                                                           allIds }
                         in liftM fst $ anaForm (const return) mix' s f
