{- |
Module      :  ./ConstraintCASL/StaticAna.hs
Description :  static analysis for ConstraintCASL
Copyright   :  (c) Uni Bremen 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis for ConstraintCASL specifications
 Follows Chaps. III:2 and III:3 of the CASL Reference Manual.
-}

module ConstraintCASL.StaticAna where

import ConstraintCASL.AS_ConstraintCASL
import ConstraintCASL.Print_AS ()
import CASL.StaticAna
import CASL.Sign
import CASL.Morphism
import CASL.MixfixParser
import CASL.ToDoc

import Common.Result
import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.ExtSign

type ConstraintCASLSign = Sign ConstraintFORMULA ()
type ConstraintCASLMor = Morphism ConstraintFORMULA () ()

basicConstraintCASLAnalysis
    :: (ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
    -> Result (ConstraintCASLBasicSpec,
               ExtSign ConstraintCASLSign Symbol,
               [Named ConstraintCASLFORMULA])
basicConstraintCASLAnalysis :: (ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
-> Result
     (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
      [Named ConstraintCASLFORMULA])
basicConstraintCASLAnalysis =
    Min ConstraintFORMULA ()
-> Ana () () () ConstraintFORMULA ()
-> Ana () () () ConstraintFORMULA ()
-> Mix () () ConstraintFORMULA ()
-> (ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
-> Result
     (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
      [Named ConstraintCASLFORMULA])
forall f e b s.
(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, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis ((ConstraintFORMULA -> Result ConstraintFORMULA)
-> Min ConstraintFORMULA ()
forall a b. a -> b -> a
const ConstraintFORMULA -> Result ConstraintFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return) ((() -> State ConstraintCASLSign ())
-> Ana () () () ConstraintFORMULA ()
forall a b. a -> b -> a
const () -> State ConstraintCASLSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) ((() -> State ConstraintCASLSign ())
-> Ana () () () ConstraintFORMULA ()
forall a b. a -> b -> a
const () -> State ConstraintCASLSign ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix () () ConstraintFORMULA ()
forall b s f e. Mix b s f e
emptyMix

instance FormExtension ConstraintFORMULA

instance TermExtension ConstraintFORMULA