hets/HasCASL/OpDecl.hs

	OpDecl.hs revision 715ffaf874309df081d1e1cd8e05073fc1227729
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinModule      :  $Header$
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinCopyright   :  (c) Christian Maeder and Uni Bremen 2003
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinMaintainer  :  maeder@tzi.de
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinStability   :  experimental
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinPortability :  portable
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin   analyse operation declarations
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-}
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinmodule HasCASL.OpDecl where
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport Data.Maybe
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel Calinimport Common.Id
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport Common.AS_Annotation
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport Common.Lib.State
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport Common.Result
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.GlobalAnnotations
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.As
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport HasCASL.VarDecl
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Le
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Builtin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport HasCASL.AsUtils
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport HasCASL.Unify
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport HasCASL.TypeCheck
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport HasCASL.ProgEq
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaAttr :: GlobalAnnos -> TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederanaAttr ga (TypeScheme tvs (_ :=> ty) _) (UnitOpAttr trm ps) =
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    do let mTy = case ty of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin              FunType (ProductType [t1, t2] _) _ t3 _ ->
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin              Just (t1,t2,t3)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin              FunType t1 _ (FunType t2 _ t3 _) _ ->
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin              Just (t1,t2,t3)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin              _ -> Nothing
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       tm <- gets typeMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder       mapM_ (addTypeVarDecl False) tvs
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       case mTy of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin         Nothing -> do addDiags [mkDiag Error
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                     "unexpected type of operation" ty]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder               mt <- resolveTerm ga Nothing trm
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin               putTypeMap tm
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin               case mt of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                   Nothing -> return Nothing
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                   Just t  -> return $ Just $ UnitOpAttr t ps
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin         Just (t1, t2, t3) ->
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin         do if t1 == t2 && t2 == t3 then
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin               return ()
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               else addDiags [mkDiag Error
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                     "unexpected type of operation" ty]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                    mt <- resolveTerm ga (Just t3) trm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder            putTypeMap tm
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            case mt of Nothing -> return Nothing
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                           Just t -> return $ Just $ UnitOpAttr t ps
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinanaAttr _ _ b = return $ Just b
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinfilterVars :: Assumps -> Assumps
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinfilterVars = filterAssumps (not . isVarDefn)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinpatternsToType :: [[VarDecl]] -> Type -> Type
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinpatternsToType [] t = t
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederpatternsToType (p: ps) t = FunType (tuplePatternToType p) PFunArr
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder              (patternsToType ps t) []
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertuplePatternToType :: [VarDecl] -> Type
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalintuplePatternToType vds = mkProductType (map ( \ (VarDecl _ t _ _) -> t) vds) []
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaOpItem :: GlobalAnnos -> OpBrand -> OpItem -> State Env OpItem
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaOpItem ga br ods@(OpDecl is sc attr ps) =
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin    do mSc <- anaTypeScheme sc
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       case mSc of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           Nothing -> return ods
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       Just s -> do
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin           let nSc = generalize s
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin           mAttrs <- mapM (anaAttr ga nSc) attr
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin           us <- mapM (anaOpId br nSc attr) is
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           return $ OpDecl (catMaybes us) nSc (catMaybes mAttrs) ps
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaederanaOpItem ga br (OpDefn o oldPats sc partial trm ps) =
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin    do let (op@(OpId i _ _), extSc) = getUninstOpId sc o
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder       mSc <- anaTypeScheme extSc
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin       as <- gets assumps
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin       checkUniqueVars $ concat oldPats
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin       putAssumps $ filterVars as
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin       mPats <- mapM (mapM anaVarDecl) oldPats
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin       let newPats = map catMaybes mPats
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       monoPats = map (map makeMonomorph) newPats
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       pats = map (\ l -> mkTupleTerm (map toQualVar l) []) monoPats
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       case mSc of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin        Just newSc@(TypeScheme tArgs (qu :=> scTy) qs) -> do
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            ty <- toEnvState $ freshInst newSc
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            mapM (mapM addVarDecl) monoPats
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder            mt <- resolveTerm ga (Just ty) trm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder            putAssumps as
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            case mt of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                  Nothing -> return $ OpDefn op newPats
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                         newSc partial trm ps
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                  Just lastTrm -> do
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      let lastSc = TypeScheme tArgs
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                    (qu :=> patternsToType newPats scTy) qs
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      lamTrm = case (pats, partial) of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                           ([], Total) -> lastTrm
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                           _ -> LambdaTerm pats partial
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                            lastTrm ps
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      ot = QualOp br (InstOpId i [] [])
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      lastSc []
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      lhs = mkApplTerm ot pats
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin                      ef = mkEqTerm eqId ps lhs lastTrm
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                      f = mkForall (map GenTypeVarDecl tArgs
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                      ++ (map GenVarDecl $
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                          concatMap extractVars pats)) ef
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                  addOpId i lastSc [] $ Definition br lamTrm
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                  appendSentences [NamedSen
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                           ("def_" ++ showId i "")
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                           $ Formula f]
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                  return $ OpDefn op [] lastSc
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin                       Total lamTrm ps
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin        Nothing -> do
122a14383b01d8ed63cf28dad7aaebb5c97dbf0dGeorgel Calin            mt <- resolveTerm ga Nothing trm
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            putAssumps as
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin            return $ OpDefn op newPats extSc partial
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                  (case mt of Nothing -> trm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                              Just x -> x) ps
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalingetUninstOpId :: TypeScheme -> OpId -> (OpId, TypeScheme)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalingetUninstOpId (TypeScheme tvs q ps) (OpId i args qs) =
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin      (OpId i [] qs, TypeScheme (args ++ tvs) q ps)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> OpId -> State Env (Maybe OpId)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinanaOpId br sc attrs o =
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin    do let (OpId i _ _, newSc) = getUninstOpId sc o
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin       mo <- addOpId i newSc attrs $ NoOpDefn br
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       return $ fmap (const o) mo
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder-- ----------------------------------------------------------------------------
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- ProgEq
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- ----------------------------------------------------------------------------
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederanaProgEq :: GlobalAnnos -> ProgEq -> State Env ProgEq
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalinanaProgEq ga pe@(ProgEq pat trm qs) =
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    do as <- gets assumps
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       putAssumps $ filterVars as
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       mp <- checkPattern ga pat
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder       case mp of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       Nothing -> return pe
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin       Just newPat -> do
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           let exbs = extractVars newPat
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           checkUniqueVars exbs
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           mapM_ addVarDecl exbs
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           mt <- resolveTerm ga Nothing trm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           putAssumps as
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder           case mt of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           Just newTerm  -> let newPrg = ProgEq newPat newTerm qs in
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin             case getAppl newPat of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder               Just (i, sc, args) -> let
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               defTrm = if null args then newTerm
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                    else LambdaTerm args
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         Partial newTerm [] in do
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               addOpId i sc [] $ Definition Op defTrm
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               appendSentences [NamedSen ("pe_" ++ showId i "")
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                        $ ProgEqSen i sc newPrg]
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               e <- get
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               if isLHS e newPat then return ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                  else addDiags [mkDiag Warning
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                     "illegal lhs pattern"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder                     newPat]
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               return newPrg
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin               _ -> do addDiags [mkDiag Error
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                     "illegal toplevel pattern"
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                     newPat]
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                   return newPrg
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin           _ -> return $ ProgEq newPat trm qs
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalingetApplConstr :: Pattern -> (Pattern, [Pattern])
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalingetApplConstr pat =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder    case pat of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    ApplTerm p1 p2 _ ->
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    let (tp, args) = getApplConstr p1 in (tp, p2:args)
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    TypedTerm tp _ _ _ -> getApplConstr tp
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin    _ -> (pat, [])
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin