content: {- |
  Module      :  ./CASL/MixfixParser.hs
  Description :  Mixfix analysis of terms
  Copyright   :  Christian Maeder and Uni Bremen 2002-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  Mixfix analysis of terms
  -}
  
  module CASL.MixfixParser
      ( resolveFormula, resolveMixfix, MixResolve
      , resolveMixTrm, resolveMixFrm
      , extendRules, varDeclTokens
      , extendMixResolve
      , IdSets, mkIdSets, emptyIdSets, unite, unite2
      , makeRules, Mix (..), emptyMix, extendMix
      , ids_BASIC_SPEC, ids_SIG_ITEMS, ids_OP_ITEM, ids_PRED_ITEM
      , ids_DATATYPE_DECL
      , addIdToRules
      ) where
  
  import CASL.AS_Basic_CASL
  import CASL.ShowMixfix
  import CASL.ToDoc
  
  import Common.AS_Annotation
  import Common.ConvertMixfixToken
  import Common.DocUtils
  import Common.Earley
  import Common.GlobalAnnotations
  import Common.Id
  import Common.Result
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import Data.Maybe
  
  data Mix b s f e = MixRecord
      { getBaseIds :: b -> IdSets -- ^ ids of extra basic items
      , getSigIds :: s -> IdSets  -- ^ ids of extra sig items
      , getExtIds :: e -> IdSets  -- ^ ids of signature extensions
      , mixRules :: (TokRules, Rules) -- ^ rules for Earley
      , putParen :: f -> f -- ^ parenthesize extended formula
      , mixResolve :: MixResolve f -- ^ resolve extended formula
      }
  
  -- | an initially empty record
  emptyMix :: Mix b s f e
  emptyMix = MixRecord
      { getBaseIds = const emptyIdSets
      , getSigIds = const emptyIdSets
      , getExtIds = const emptyIdSets
      , mixRules = (const Set.empty, emptyRules)
      , putParen = id
      , mixResolve = const $ const return
      }
  
  extendMix :: Set.Set Token -> Mix b s f e -> Mix b s f e
  extendMix ts r = r
    { mixRules = extendRules ts $ mixRules r
    , mixResolve = extendMixResolve ts $ mixResolve r }
  
  -- precompute non-simple op and pred identifier for mixfix rules
  
  -- | the precomputed sets of constant, op, and pred identifiers
  type IdSets = ((Set.Set Id, Set.Set Id), Set.Set Id) -- ops are first component
  
  -- | the empty 'IdSets'
  emptyIdSets :: IdSets
  emptyIdSets = let e = Set.empty in ((e, e), e)
  
  unite2 :: [(Set.Set Id, Set.Set Id)] -> (Set.Set Id, Set.Set Id)
  unite2 l = (Set.unions $ map fst l, Set.unions $ map snd l)
  
  -- | union 'IdSets'
  unite :: [IdSets] -> IdSets
  unite l = (unite2 $ map fst l, Set.unions $ map snd l)
  
  -- | get all ids of a basic spec
  ids_BASIC_SPEC :: (b -> IdSets) -> (s -> IdSets) -> BASIC_SPEC b s f -> IdSets
  ids_BASIC_SPEC f g (Basic_spec al) =
      unite $ map (ids_BASIC_ITEMS f g . item) al
  
  ids_BASIC_ITEMS :: (b -> IdSets) -> (s -> IdSets)
                  -> BASIC_ITEMS b s f -> IdSets
  ids_BASIC_ITEMS f g bi = case bi of
      Sig_items sis -> ids_SIG_ITEMS g sis
      Free_datatype _ al _ -> ids_anDATATYPE_DECLs al
      Sort_gen al _ -> unite $ map (ids_SIG_ITEMS g . item) al
      Ext_BASIC_ITEMS b -> f b
      _ -> emptyIdSets
  
  ids_anDATATYPE_DECLs :: [Annoted DATATYPE_DECL] -> IdSets
  ids_anDATATYPE_DECLs al =
      (unite2 $ map (ids_DATATYPE_DECL . item) al, Set.empty)
  
  -- | get all ids of a sig items
  ids_SIG_ITEMS :: (s -> IdSets) -> SIG_ITEMS s f -> IdSets
  ids_SIG_ITEMS f si = let e = Set.empty in case si of
      Sort_items {} -> emptyIdSets
      Op_items al _ -> (unite2 $ map (ids_OP_ITEM . item) al, e)
      Pred_items al _ -> ((e, e), Set.unions $ map (ids_PRED_ITEM . item) al)
      Datatype_items _ al _ -> ids_anDATATYPE_DECLs al
      Ext_SIG_ITEMS s -> f s
  
  -- | get all op ids of an op item
  ids_OP_ITEM :: OP_ITEM f -> (Set.Set Id, Set.Set Id)
  ids_OP_ITEM o = let e = Set.empty in case o of
      Op_decl ops (Op_type _ args _ _) _ _ ->
        let s = Set.fromList ops in
        if null args then (s, e) else (e, s)
      Op_defn i (Op_head _ args _ _) _ _ ->
        let s = Set.singleton i in
        if null args then (s, e) else (e, s)
  
  -- | get all pred ids of a pred item
  ids_PRED_ITEM :: PRED_ITEM f -> Set.Set Id
  ids_PRED_ITEM p = case p of
      Pred_decl preds _ _ -> Set.unions $ map Set.singleton preds
      Pred_defn i _ _ _ -> Set.singleton i
  
  ids_DATATYPE_DECL :: DATATYPE_DECL -> (Set.Set Id, Set.Set Id)
  ids_DATATYPE_DECL (Datatype_decl _ al _) =
      unite2 $ map (ids_ALTERNATIVE . item) al
  
  ids_ALTERNATIVE :: ALTERNATIVE -> (Set.Set Id, Set.Set Id)
  ids_ALTERNATIVE a = let e = Set.empty in case a of
      Alt_construct _ i cs _ -> let s = Set.singleton i in
        if null cs then (s, e) else (e, Set.unions $ s : map ids_COMPONENTS cs)
      Subsorts _ _ -> (e, e)
  
  ids_COMPONENTS :: COMPONENTS -> Set.Set Id
  ids_COMPONENTS c = case c of
      Cons_select _ l _ _ -> Set.unions $ map Set.singleton l
      Sort _ -> Set.empty
  
  -- predicates get lower precedence
  mkRule :: Id -> Rule
  mkRule = mixRule 1
  
  mkSingleArgRule :: Int -> Id -> Rule
  mkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
  
  mkArgsRule :: Int -> Id -> Rule
  mkArgsRule b ide =
    (protect ide, b, getPlainTokenList ide ++ getTokenPlaceList tupleId)
  
  singleArgId :: Id
  singleArgId = mkId [exprTok, varTok]
  
  multiArgsId :: Id
  multiArgsId = mkId (exprTok : getPlainTokenList tupleId)
  
  addIdToRules :: Id -> (TokRules, Rules) -> (TokRules, Rules)
  addIdToRules i (tr, rs) =
     (tr, let newSc = Set.union
                (Set.fromList [mkSingleArgRule 1 i, mkArgsRule 1 i])
                $ scanRules rs
          in if begPlace i then
              rs { postRules = Set.insert (mixRule 1 i) $ postRules rs
                 , scanRules = newSc }
          else rs { scanRules = Set.insert (mixRule 1 i) newSc })
  
  -- | additional scan rules
  addRule :: GlobalAnnos -> [Rule] -> Bool -> IdSets -> TokRules
  addRule ga uRules hasInvisible ((consts, ops), preds) tok =
      let addP = Set.fold (\ i -> case i of
                   Id (t : _) _ _ -> Map.insertWith (++) t
                     [ mixRule (if Set.member i consts then 1 else 0) i
                     , mkSingleArgRule 0 i, mkArgsRule 0 i]
                   _ -> error "addRule.addP")
          addO = Set.fold (\ i -> case i of
                   Id (t : _) _ _ -> Map.insertWith (++) t
                     $ [mkRule i | not (isSimpleId i)
                        || Set.member i (Set.union consts preds) ]
                     ++ [mkSingleArgRule 1 i, mkArgsRule 1 i]
                   _ -> error "addRule.addO")
          addC = Set.fold (\ i -> case i of
                   Id (t : _) _ _ -> Map.insertWith (++) t [mkRule i]
                   _ -> error "addRule.addC")
          lm = foldr (\ r -> case r of
                 (_, _, t : _) -> Map.insertWith (++) t [r]
                 _ -> error "addRule.lm") Map.empty $ listRules 1 ga
          (spreds, rpreds) = Set.partition isSimpleId preds
          {- do not add simple ids as preds as these may be variables
          with higher precedence -}
          ops2 = Set.union ops spreds
          sops = Set.union consts ops2
          rConsts = Set.difference consts $ Set.union ops preds
          varR = mkRule varId
          m = Map.insert placeTok uRules
              $ Map.insert varTok [varR]
              $ Map.insert exprTok
                    [varR, mkRule singleArgId, mkRule multiArgsId]
              $ addP (addC (addO lm ops2) rConsts) $ Set.difference rpreds ops
          tId = mkId [tok]
          tPId = mkId [tok, placeTok] -- prefix identifier
      in (if isSimpleToken tok && not (Set.member tId sops)
          then if hasInvisible then Set.empty else
               Set.insert (mkRule tId)
               -- add rule for unknown constant or variable
               $ if Set.member tPId ops || Set.member tPId rpreds
                 then Set.empty else
                   Set.fromList [mkSingleArgRule 1 tId, mkArgsRule 1 tId]
                -- add also rules for undeclared op
          else Set.empty) `Set.union` Set.fromList (Map.findWithDefault [] tok m)
  
  -- insert only identifiers starting with a place
  initRules :: (Set.Set Id, Set.Set Id) -> Rules
  initRules (opS, predS) =
    let addR p = Set.fold (Set.insert . mixRule p)
    in emptyRules
    { postRules = addR 1 (addR 0 (Set.singleton $ mkRule typeId) predS) opS }
  
  -- | construct rules from 'IdSets' to be put into a 'Mix' record
  makeRules :: GlobalAnnos -> IdSets -> (TokRules, Rules)
  makeRules ga ((constS, opS), predS) = let
      (cOps, sOps) = Set.partition begPlace opS
      (cPreds, sPreds) = Set.partition begPlace $ Set.difference predS opS
      addR p = Set.fold ( \ i l ->
             mkSingleArgRule p i : mkArgsRule p i : l)
      uRules = addR 0 (addR 1 [] cOps) cPreds
      in (addRule ga uRules (Set.member applId $ Set.union cOps cPreds)
          ((constS, sOps), sPreds), initRules (cOps, cPreds))
  
  -- | construct application
  asAppl :: Id -> [TERM f] -> Range -> TERM f
  asAppl f args ps = Application (Op_name f) args
                   $ if isNullRange ps then posOfId f else ps
  
  -- | constructing the parse tree from (the final) parser state(s)
  toAppl :: GetRange f => Id -> [TERM f] -> Range -> TERM f
  toAppl ide ar ps =
         if elem ide [singleArgId, multiArgsId]
              then case ar of
                har : tar -> case har of
                   Application q [] p ->
                       Application q tar $ appRange ps p
                   Mixfix_qual_pred _ ->
                       Mixfix_term [har, Mixfix_parenthesized tar ps]
                   _ -> error "stateToAppl"
                _ -> error "stateToAppl2"
              else asAppl ide ar ps
  
  addType :: TERM f -> TERM f -> TERM f
  addType tt t =
      case tt of
      Mixfix_sorted_term s ps -> Sorted_term t s ps
      Mixfix_cast s ps -> Cast t s ps
      _ -> error "addType"
  
  -- | the type for mixfix resolution
  type MixResolve f = GlobalAnnos -> (TokRules, Rules) -> f -> Result f
  
  iterateCharts :: FormExtension f => (f -> f)
                -> MixResolve f -> GlobalAnnos -> [TERM f]
                -> Chart (TERM f) -> Chart (TERM f)
  iterateCharts par extR g terms c =
      let self = iterateCharts par extR g
          expand = expandPos Mixfix_token
          oneStep = nextChart addType toAppl g c
          ids = (addRules c, rules c)
          resolveTerm = resolveMixTrm par extR g ids
      in case terms of
      [] -> c
      hd : tl -> case hd of
              Mixfix_term ts -> self (ts ++ tl) c
              Mixfix_bracketed ts ps ->
                  self (expand ("[", "]") ts ps ++ tl) c
              Mixfix_braced ts ps ->
                  self (expand ("{", "}") ts ps ++ tl) c
              Mixfix_parenthesized ts ps -> case ts of
                [h] -> let
                  Result mds v = resolveTerm h
                  c2 = self tl (oneStep (fromMaybe h v, varTok {tokPos = ps}))
                  in mixDiags mds c2
                _ -> self (expand ("(", ")") ts ps ++ tl) c
              h@(Conditional t1 f2 t3 ps) -> let
                Result mds v = do
                  t4 <- resolveTerm t1
                  f5 <- resolveMixFrm par extR g ids f2
                  t6 <- resolveTerm t3
                  return (Conditional t4 f5 t6 ps)
                c2 = self tl
                     (oneStep (fromMaybe h v, varTok {tokPos = ps}))
                in mixDiags mds c2
              Mixfix_token t -> let
                (ds1, trm) = convertMixfixToken (literal_annos g) asAppl
                  Mixfix_token t
                c2 = self tl $ oneStep $ case trm of
                  Mixfix_token tok -> (trm, tok)
                  _ -> (trm, varTok {tokPos = tokPos t})
                in mixDiags ds1 c2
              t@(Mixfix_sorted_term _ ps) ->
                self tl (oneStep (t, typeTok {tokPos = ps}))
              t@(Mixfix_cast _ ps) ->
                self tl (oneStep (t, typeTok {tokPos = ps}))
              t@(Qual_var _ _ ps) ->
                self tl (oneStep (t, varTok {tokPos = ps}))
              Application opNam ts ps -> let
                Result mds v = mapM resolveTerm ts
                c2 = self tl $ oneStep (Application opNam (fromMaybe ts v) ps
                                       , case opNam of
                       Qual_op_name _ _ qs -> exprTok {tokPos = qs}
                       Op_name o -> varTok {tokPos = posOfId o})
                in mixDiags mds c2
              t@(Mixfix_qual_pred (Qual_pred_name _ _ ps)) ->
                  self tl (oneStep (t, exprTok {tokPos = ps} ))
              Sorted_term t s ps -> let
                Result mds v = resolveTerm t
                tNew = Sorted_term (fromMaybe t v) s ps
                c2 = self tl (oneStep (tNew, varTok {tokPos = ps}))
                in mixDiags mds c2
              ExtTERM t -> let
                Result mds v = extR g ids t
                tNew = ExtTERM $ fromMaybe t v
                c2 = self tl $ oneStep (tNew, varTok {tokPos = getRange t})
                in mixDiags mds c2
              _ -> error "iterateCharts"
  
  -- | construct 'IdSets' from op and pred identifiers
  mkIdSets :: Set.Set Id -> Set.Set Id -> Set.Set Id -> IdSets
  mkIdSets consts ops preds = ((consts, ops), preds)
  
  -- | top-level resolution like 'resolveMixTrm' that fails in case of diags
  resolveMixfix :: FormExtension f => (f -> f)
                -> MixResolve f -> MixResolve (TERM f)
  resolveMixfix par extR g ruleS t =
      let r@(Result ds _) = resolveMixTrm par extR g ruleS t
          in if null ds then r else Result ds Nothing
  
  -- | basic term resolution that supports recursion without failure
  resolveMixTrm :: FormExtension f => (f -> f)
                -> MixResolve f -> MixResolve (TERM f)
  resolveMixTrm par extR ga (adder, ruleS) trm =
      getResolved (showTerm par ga) (getRangeSpan trm) toAppl
             $ iterateCharts par extR ga [trm] $ initChart adder ruleS
  
  showTerm :: FormExtension f => (f -> f) -> GlobalAnnos -> TERM f -> ShowS
  showTerm par ga = showGlobalDoc ga . mapTerm par
  
  -- | top-level resolution like 'resolveMixFrm' that fails in case of diags
  resolveFormula :: FormExtension f => (f -> f)
                 -> MixResolve f -> MixResolve (FORMULA f)
  resolveFormula par extR g ruleS f =
      let r@(Result ds _) = resolveMixFrm par extR g ruleS f
          in if null ds then r else Result ds Nothing
  
  varDeclTokens :: [VAR_DECL] -> Set.Set Token
  varDeclTokens = Set.unions . map (\ (Var_decl vs _ _) -> Set.fromList vs)
  
  extendRules :: Set.Set Token -> (TokRules, Rules)
    -> (TokRules, Rules)
  extendRules ts (f, rs) =
    (\ t -> let
       l = f t
       r = mkRule $ mkId [t]
       in if Set.member t ts then Set.insert r l else l, rs)
  
  extendMixResolve :: Set.Set Token -> MixResolve f -> MixResolve f
  extendMixResolve ts f ga = f ga . extendRules ts
  
  -- | basic formula resolution that supports recursion without failure
  resolveMixFrm :: FormExtension f => (f -> f)
                -> MixResolve f -> MixResolve (FORMULA f)
  resolveMixFrm par extR g ids frm =
      let self = resolveMixFrm par extR g ids
          resolveTerm = resolveMixTrm par extR g ids in
      case frm of
         Quantification q vs fOld ps ->
             do let ts = varDeclTokens vs
                fNew <- resolveMixFrm par (extendMixResolve ts extR)
                  g (extendRules ts ids) fOld
                return $ Quantification q vs fNew ps
         Junction j fsOld ps ->
             do fsNew <- mapM self fsOld
                return $ Junction j fsNew ps
         Relation f1 c f2 ps ->
             do f3 <- self f1
                f4 <- self f2
                return $ Relation f3 c f4 ps
         Negation fOld ps ->
             do fNew <- self fOld
                return $ Negation fNew ps
         Predication sym tsOld ps ->
             do tsNew <- mapM resolveTerm tsOld
                return $ Predication sym tsNew ps
         Definedness tOld ps ->
             do tNew <- resolveTerm tOld
                return $ Definedness tNew ps
         Equation t1 e t2 ps ->
             do t3 <- resolveTerm t1
                t4 <- resolveTerm t2
                return $ Equation t3 e t4 ps
         Membership tOld s ps ->
             do tNew <- resolveTerm tOld
                return $ Membership tNew s ps
         Mixfix_formula tOld ->
             do tNew <- resolveTerm tOld
                case tNew of
                   Application (Op_name ide) args ps ->
                       return $ Predication (Pred_name ide) args ps
                   Mixfix_qual_pred qide ->
                       return $ Predication qide [] nullRange
                   Mixfix_term [Mixfix_qual_pred qide,
                                Mixfix_parenthesized ts ps] ->
                       return $ Predication qide ts ps
                   _ -> return $ Mixfix_formula tNew
         QuantOp o t fOld -> let
           ts = if isSimpleId o then Set.singleton $ idToSimpleId o
                else Set.empty
           in fmap (QuantOp o t)
              $ resolveMixFrm par (extendMixResolve ts extR)
                g (extendRules ts ids) fOld
         QuantPred p t fOld -> let
           ts = if isSimpleId p then Set.singleton $ idToSimpleId p
                else Set.empty
           in fmap (QuantPred p t)
              $ resolveMixFrm par (extendMixResolve ts extR)
                g (extendRules ts ids) fOld
         ExtFORMULA f ->
             do newF <- extR g ids f
                return $ ExtFORMULA newF
         f -> return f
  