hets/HasCASL/MixAna.hs

	MixAna.hs revision 3f69b6948966979163bdfe8331c38833d5d90ecd
0N/A{- |
196N/AModule      :  $Header$
0N/ADescription :  mixfix analysis for terms
0N/ACopyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
0N/ALicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0N/A
0N/AMaintainer  :  Christian.Maeder@dfki.de
0N/AStability   :  experimental
0N/APortability :  portable
0N/A
0N/AMixfix analysis of terms and patterns, type annotations are also analysed
0N/A-}
0N/A
0N/Amodule HasCASL.MixAna where
0N/A
0N/Aimport Common.GlobalAnnotations
0N/Aimport Common.Result
0N/Aimport Common.Id
0N/Aimport Common.DocUtils
0N/Aimport Common.Earley
0N/Aimport Common.Lexer
0N/Aimport Common.Prec
0N/Aimport Common.ConvertMixfixToken
0N/Aimport Common.Lib.State
0N/Aimport Common.AnnoState
0N/Aimport qualified Data.Map as Map
0N/Aimport qualified Data.Set as Set
0N/A
91N/Aimport HasCASL.As
0N/Aimport HasCASL.AsUtils
0N/Aimport HasCASL.PrintAs
0N/Aimport HasCASL.Unify
0N/Aimport HasCASL.VarDecl
0N/Aimport HasCASL.Le
0N/Aimport HasCASL.HToken
0N/Aimport HasCASL.ParseTerm
0N/Aimport HasCASL.TypeAna
0N/A
0N/Aimport qualified Text.ParserCombinators.Parsec as P
0N/A
0N/Aimport Data.Maybe
0N/Aimport Data.List (partition)
0N/Aimport Control.Exception (assert)
0N/A
0N/AaddType :: Term -> Term -> Term
0N/AaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
0N/AaddType _ _ = error "addType"
0N/A
0N/AisCompoundList :: Set.Set [Id] -> [Term] -> Bool
0N/AisCompoundList compIds l =
0N/A    maybe False (flip Set.member compIds) $ sequence $ map termToId l
0N/A
0N/AisTypeList :: Env -> [Term] -> Bool
0N/AisTypeList e l = case sequence $ map termToType l of
0N/A                 Nothing -> False
0N/A                 Just ts ->
0N/A                     let Result ds ml =
0N/A                             mapM ( \ t -> anaTypeM (Nothing, t) e) ts
0N/A                     in isJust ml && not (hasErrors ds)
0N/A
0N/AtermToType :: Term -> Maybe Type
0N/AtermToType t =
0N/A    case P.runParser (parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of
0N/A      Right x -> Just x
0N/A      _ -> Nothing
0N/A
0N/AtermToId :: Term -> Maybe Id
0N/AtermToId t = case P.parse (uninstOpId << P.eof) "" $ showDoc t "" of
0N/A               Right x -> Just x
0N/A               _ -> Nothing
0N/A
0N/AiterateCharts :: GlobalAnnos ->  Set.Set [Id] -> [Term] -> Chart Term
0N/A              -> State Env (Chart Term)
0N/AiterateCharts ga compIds terms chart =
0N/A    do e <- get
0N/A       let self = iterateCharts ga compIds
0N/A           oneStep = nextChart addType toMixTerm ga chart
0N/A           vs = localVars e
0N/A           tm = typeMap e
0N/A       case terms of
0N/A         [] -> return chart
0N/A         t:tt -> do
0N/A             let recurse trm = self tt $
0N/A                          oneStep (trm, exprTok {tokPos = getRange trm})
0N/A             case t of
0N/A                    MixfixTerm ts -> self (ts ++ tt) chart
0N/A                    MixTypeTerm q typ ps -> do
0N/A                       mTyp <- anaStarType typ
0N/A                       case mTyp of
0N/A                           Nothing -> recurse t
0N/A                           Just nTyp -> self tt $ oneStep
0N/A                                        (MixTypeTerm q (monoType nTyp) ps,
0N/A                                         typeTok {tokPos = ps})
0N/A                    BracketTerm b ts ps ->
0N/A                      let bres = self (expandPos TermToken
0N/A                                       (getBrackets b) ts ps ++ tt) chart
0N/A                      in case (b, ts) of
0N/A                        (Squares, _ : _) ->
0N/A                            if isCompoundList compIds ts then bres
0N/A                            else if isTypeList e ts then self tt $ oneStep
0N/A                                 (t, typeInstTok {tokPos = ps})
0N/A                                 else bres
0N/A                        _ -> bres
0N/A                    QualVar (VarDecl v typ ok ps) -> do
0N/A                       mTyp <- anaStarType typ
0N/A                       case mTyp of
0N/A                           Nothing -> recurse t
0N/A                           Just nType -> recurse $ QualVar $
0N/A                                         VarDecl v (monoType nType) ok ps
0N/A                    QualOp b (InstOpId v ts qs) sc ps -> do
0N/A                       mSc <- anaTypeScheme sc
0N/A                       newTs <- anaInstTypes ts
0N/A                       case mSc of
0N/A                           Nothing -> recurse t
0N/A                           Just nSc -> do
0N/A                               case findOpId e v nSc of
0N/A                                    Nothing -> addDiags [mkDiag Error
0N/A                                                   "operation not found" v]
0N/A                                    _ -> return ()
0N/A                               recurse $ QualOp b (InstOpId v newTs qs) nSc ps
0N/A                    QuantifiedTerm quant decls hd ps -> do
0N/A                       newDs <- mapM (anaddGenVarDecl False) decls
0N/A                       mt <- resolve ga hd
0N/A                       putLocalVars vs
0N/A                       putTypeMap tm
0N/A                       let newT = case mt of Just trm -> trm
0N/A                                             _ -> hd
0N/A                       recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
0N/A                    LambdaTerm decls part hd ps -> do
0N/A                       mDecls <- mapM (resolvePattern ga) decls
0N/A                       let anaDecls = catMaybes mDecls
0N/A                           bs = concatMap extractVars anaDecls
0N/A                       checkUniqueVars bs
0N/A                       mapM_ (addLocalVar False) bs
0N/A                       mt <- resolve ga hd
0N/A                       putLocalVars vs
0N/A                       recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
0N/A                    CaseTerm hd eqs ps -> do
0N/A                       mt <- resolve ga hd
0N/A                       newEs <- resolveCaseEqs ga eqs
0N/A                       recurse $ CaseTerm (maybe hd id mt) newEs ps
0N/A                    LetTerm b eqs hd ps -> do
0N/A                       newEs <- resolveLetEqs ga eqs
0N/A                       mt <- resolve ga hd
0N/A                       putLocalVars vs
0N/A                       recurse $ LetTerm b newEs (maybe hd id mt) ps
0N/A                    TermToken tok -> do
0N/A                        let (ds1, trm) = convertMixfixToken
0N/A                                         (literal_annos ga)
0N/A                                         ResolvedMixTerm TermToken tok
0N/A                        addDiags ds1
0N/A                        self tt $ oneStep $
0N/A                                       case trm of
0N/A                                                TermToken _ -> (trm, tok)
0N/A                                                _ -> (trm, exprTok
0N/A                                                      {tokPos = tokPos tok})
91N/A                    AsPattern vd p ps -> do
0N/A                        mp <- resolvePattern ga p
0N/A                        let newP = case mp of Just pat -> pat
0N/A                                              Nothing -> p
0N/A                        recurse $ AsPattern vd newP ps
0N/A                    TypedTerm trm k ty ps -> do
0N/A                        -- assume that type is analysed
0N/A                        mt <- resolve ga trm
0N/A                        recurse $ TypedTerm (maybe trm id mt) k ty ps
0N/A                    _ -> error ("iterCharts: " ++ show t)
0N/A
0N/A-- * equation stuff
0N/AresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
0N/AresolveCaseEq ga (ProgEq p t ps) =
0N/A    do mp <- resolvePattern ga p
0N/A       case mp of
0N/A           Nothing -> return Nothing
0N/A           Just newP -> do
0N/A                let bs = extractVars newP
0N/A                checkUniqueVars bs
0N/A                vs <- gets localVars
0N/A                mapM_ (addLocalVar False) bs
0N/A                mtt <- resolve ga t
0N/A                putLocalVars vs
0N/A                return $ case mtt of
0N/A                    Nothing -> Nothing
0N/A                    Just newT -> Just $ ProgEq newP newT ps
0N/A
0N/AresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
0N/AresolveCaseEqs _ [] = return []
0N/AresolveCaseEqs ga (eq : rt) =
0N/A    do mEq <- resolveCaseEq ga eq
0N/A       eqs <- resolveCaseEqs ga rt
0N/A       return $ case mEq of
0N/A               Nothing -> eqs
0N/A               Just newEq -> newEq : eqs
0N/A
0N/AresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
0N/AresolveLetEqs _ [] = return []
0N/AresolveLetEqs ga (ProgEq pat trm ps : rt) =
0N/A    do mPat <- resolvePattern ga pat
0N/A       case mPat of
0N/A           Nothing -> do resolve ga trm
0N/A                         resolveLetEqs ga rt
0N/A           Just newPat -> do
0N/A               let bs = extractVars newPat
0N/A               checkUniqueVars bs
0N/A               mapM_ (addLocalVar False) bs
0N/A               mTrm <- resolve ga trm
0N/A               case mTrm of
0N/A                   Nothing -> resolveLetEqs ga rt
0N/A                   Just newTrm -> do
0N/A                       eqs <- resolveLetEqs ga rt
0N/A                       return (ProgEq newPat newTrm ps : eqs)
0N/A
0N/AmkPatAppl :: Term -> Term -> Range -> Term
0N/AmkPatAppl op arg qs =
0N/A    case op of
0N/A            QualVar (VarDecl i (MixfixType []) _ _) ->
0N/A                ResolvedMixTerm i [arg] qs
0N/A            _ -> ApplTerm op arg qs

toMixTerm :: Id -> [Term] -> Range -> Term
toMixTerm i ar qs =
    if i == applId then assert (length ar == 2) $
           let [op, arg] = ar in mkPatAppl op arg qs
    else if i == tupleId || i == unitId then
         mkTupleTerm ar qs
    else case unPolyId i of
           Just j@(Id ts [] ps) ->
              if isMixfix j && isSingle ar then
                   ResolvedMixTerm j [] qs
              else assert (length ar == 1 + placeCount j) $
              let (toks, _) = splitMixToken ts
                  (far, _tar : sar) = splitAt (placeCount $ Id toks [] ps) ar
              in ResolvedMixTerm j (far ++ sar) qs
           _ -> ResolvedMixTerm i ar qs

getKnowns :: Id -> Set.Set Token
getKnowns (Id ts cs _) = Set.union (Set.fromList ts) $
                         Set.unions (map getKnowns cs)

resolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
resolvePattern = resolver True

resolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
resolve = resolver False

resolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
resolver isPat ga trm =
    do ass <- gets assumps
       vs <- gets localVars
       ps <- gets preIds
       compIds <- gets getCompoundLists
       let (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
                 $ Set.union (Map.keysSet ass) $ Map.keysSet vs
       chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
       let Result ds mr = getResolved
              (showDoc . parenTerm) (getRange trm)
                          toMixTerm chart
       addDiags ds
       if isPat then case mr of
           Nothing -> return mr
           Just pat -> fmap Just $ anaPattern sIds pat
           else return mr

getPolyIds :: Assumps -> Set.Set Id
getPolyIds = Set.unions . map ( \ (i, OpInfos l) ->
            foldr ( \ oi s -> case opType oi of
               TypeScheme (_ : _) _ _ -> Set.insert i s
               _ -> s) Set.empty l) . Map.toList .
            Map.filterWithKey ( \ (Id _ cs _) _ -> null cs)

getCompound :: Id -> [Id]
getCompound (Id _ cs _) = cs

getCompoundLists :: Env -> Set.Set [Id]
getCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union
    (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e

uTok :: Token
uTok = mkSimpleId "_"

builtinIds :: [Id]
builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]

makeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
          -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)
makeRules ga ps@(p, _) polyIds aIds =
    let (sIds, ids) = Set.partition isSimpleId aIds
        ks = Set.fold (Set.union . getKnowns) Set.empty ids
        rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks
        m2 = maxWeight p + 2
    in ( \ tok -> if isSimpleToken tok
                     && not (Set.member tok ks)
                         || tok == uTok then
                     [(simpleIdToId tok, m2, [tok])] else []
       , partitionRules $ listRules m2 ga ++
             initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)
       , sIds)

initRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
initRules (p, ps) polyIds bs is =
    map ( \ i -> mixRule (getIdPrec p ps i) i)
            (bs ++ is) ++
    map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))
            (filter isMixfix is) ++
-- identifiers with a positive number of type arguments
    map ( \ i -> let j = polyId i in
        (j, getIdPrec p ps i, getTokenPlaceList j)) polyIds ++
    map ( \ i -> let j = polyId i in
        (protect j, maxWeight p + 3, getPlainTokenList j))
            (filter isMixfix polyIds)

polyId :: Id -> Id
polyId (Id ts _ ps) = let (toks, pls) = splitMixToken ts in
    Id (toks ++ [typeInstTok] ++ pls) [] ps

unPolyId :: Id -> Maybe Id
unPolyId (Id ts cs ps) = let (ft, rt) = partition (== typeInstTok) ts in
    case ft of
      [_] -> Just $ Id rt cs ps
      _ -> Nothing

-- create fresh type vars for unknown ids tagged with type MixfixType [].
anaPattern :: Set.Set Id -> Pattern -> State Env Pattern
anaPattern s pat = case pat of
    QualVar vd -> do newVd <- checkVarDecl vd
                     return $ QualVar newVd
    ResolvedMixTerm i pats ps | null pats &&
        (isSimpleId i || i == simpleIdToId uTok) &&
        not (Set.member i s) -> do
            (tvar, c) <- toEnvState $ freshVar $ posOfId i
            return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
        | otherwise -> do
            l <- mapM (anaPattern s) pats
            return $ ResolvedMixTerm i l ps
    ApplTerm p1 p2 ps -> do
         p3 <- anaPattern s p1
         p4 <- anaPattern s p2
         return $ ApplTerm p3 p4 ps
    TupleTerm pats ps -> do
         l <- mapM (anaPattern s) pats
         return $ TupleTerm l ps
    TypedTerm p q ty ps -> do
         case p of
             QualVar (VarDecl v (MixfixType []) ok qs) ->
                 let newVd = VarDecl v ty ok (qs `appRange` ps) in
                 return $ QualVar newVd
             _ -> do newP <- anaPattern s p
                     return $ TypedTerm newP q ty ps
    AsPattern vd p2 ps -> do
         newVd <- checkVarDecl vd
         p4 <- anaPattern s p2
         return $ AsPattern newVd p4 ps
    _ -> return pat
    where checkVarDecl vd@(VarDecl v t ok ps) = case t of
            MixfixType [] -> do
                (tvar, c) <- toEnvState $ freshVar $ posOfId v
                return $ VarDecl v (TypeName tvar rStar c) ok ps
            _ -> return vd