55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maedermodule LocalEnv where

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- $Header$

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Id

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuimport AS_Annotation

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport FiniteMap

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Graph

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport List(intersperse)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Maybe(mapMaybe)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedertype SortId = Id -- non-mixfix, but possibly compound

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata FunKind = Total | Partial deriving (Show, Eq, Ord)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- constants have empty argument lists

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata OpType = OpType {opKind :: FunKind, opArgs :: [SortId], opRes :: SortId}

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder deriving (Show, Eq, Ord)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maedertype PredType = [SortId]

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata SymbType = OpAsItemType OpType

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder | PredType PredType

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder | Sort

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder deriving (Show, Eq, Ord)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata Symbol = Symbol {symbId :: Id, symbType :: SymbType}

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder deriving (Show, Eq, Ord)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- the list of items which are part of a "sort-gen" (or free type)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedertype GenItems = [Symbol]

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- full function type of a selector (result sort is component sort)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata Component = Component (Maybe Id) OpType [Pos] deriving (Show, Eq)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- full function type of constructor (result sort is the data type)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata Alternative = Construct Id OpType [Component] [Pos]

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder | Subsort SortId [Pos]

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder deriving (Show, Eq)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- looseness of a datatype

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- a datatype may (only) be (sub-)part of a "sort-gen"

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata GenKind = Free | Generated | Loose deriving (Show, Eq)

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederdata VarDecl = VarDecl {varId :: Id, varSort :: SortId} deriving (Show, Eq)

23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder-- sort defined as predicate subtype or as more or less loose datatype

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederdata SortDefn = SubsortDefn VarDecl Formula [Pos]

23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder | Datatype [Annoted Alternative] GenKind GenItems [Pos]

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder deriving (Show, Eq)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- the sub- and supertypes of a sort

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata SortRels = SortRels { subsorts :: [SortId] -- explicitly given

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , supersorts :: [SortId]

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , allsubsrts :: [SortId] -- transitively closed

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder , allsupersrts :: [SortId]

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder } deriving (Show, Eq)

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder

400321fd7a25a1c34eb95855ee86daf722734bd4Mihai Codescudata ItemStart = Key | Comma | Semi | Less deriving (Show, Eq)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata ItemPos = ItemPos String ItemStart [Pos] deriving (Show, Eq)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- "filename" plus positions of op, :, * ... *, ->, ",", assoc ...

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

-- sort or type

data SortItem = SortItem { sortId :: SortId

, sortRels :: SortRels

, sortDef :: Maybe SortDefn

, sortPos :: ItemPos

, altSorts :: [ItemPos] -- alternative positions

} -- of repeated decls

deriving (Show, Eq)

data BinOpAttr = Assoc | Comm | Idem deriving (Show, Eq)

data OpAttr = BinOpAttr BinOpAttr | UnitOpAttr Term deriving (Show, Eq)

type ConsId = Symbol

type SelId = Symbol

data OpDefn = OpDef [VarDecl] (Annoted Term) [[Pos]] -- ,,,;,,,;,,,

| Constr ConsId -- inferred

| Select [ConsId] SelId -- inferred

deriving (Show, Eq)

data OpItem = OpItem { opId :: Id

, opType :: OpType

, opAttrs :: [OpAttr]

, opDefn :: Maybe OpDefn

, opPos :: ItemPos -- positions of merged attributes

, altOps :: [ItemPos] -- may get lost

} deriving (Show, Eq)

data PredDefn = PredDef [VarDecl] Formula [[Pos]] deriving (Show, Eq)

data PredItem = PredItem { predId :: Id

, predType :: PredType

, predDefn :: Maybe PredDefn

, predPos :: ItemPos

, altPreds :: [ItemPos]

} deriving (Show, Eq)

data TypeQualifier = OfType | AsType deriving (Show, Eq)

data Qualified = Explicit | Inferred deriving (Show, Eq)

-- a constant op has an empty list of Arguments

data Term = VarId Id SortId Qualified [Pos]

| OpAppl Id OpType [Term] Qualified [Pos]

| Typed Term TypeQualifier SortId [Pos]

| Cond Term Formula Term [Pos] deriving (Show, Eq)

data Quantifier = Forall | Exists | ExistsUnique deriving (Show, Eq)

data LogOp = NotOp | AndOp | OrOp | ImplOp | EquivOp | IfOp deriving (Show, Eq)

data PolyOp = DefOp | EqualOp | ExEqualOp deriving (Show, Eq)

data Formula = Quantified Quantifier [VarDecl] Formula [[Pos]]

| Connect LogOp [Formula] [Pos]

| TermTest PolyOp [Term] [Pos]

| PredAppl Id PredType [Term] Qualified [Pos]

| ElemTest Term SortId [Pos]

| FalseAtom [Pos]

| TrueAtom [Pos]

| AnnFormula (Annoted Formula)

deriving (Show, Eq)

data SigItem = ASortItem (Annoted SortItem)

| AnOpItem (Annoted OpItem)

| APredItem (Annoted PredItem)

deriving (Show, Eq)

-- lost are unused global vars

-- and annotations for several ITEMS

data Sign = SignAsList [SigItem] deriving (Show, Eq)

data LocalEnv = SignAsMap (FiniteMap Id [SigItem]) (Graph SortId ())

instance Show LocalEnv where

show = error "show for type LocalEnv not defined"

data RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

deriving (Show, Eq)

data Kind = SortKind | FunKind | PredKind deriving (Show, Eq)

data Axiom = AxiomDecl [VarDecl] Formula [[Pos]] -- ,,,;,,,;

deriving (Show, Eq)

data Sentence = Axiom (Annoted Axiom)

| GenItems GenItems [Pos] -- generate/free, { , }

deriving (Show, Eq)

getLabel :: Sentence -> String

getLabel (Axiom ax) = let annos = r_annos(ax)

isLabel a = case a of Label _ _ -> True; _ -> False

labels = filter isLabel annos

getLabels(Label l _) = concat l

in if null labels then "" else getLabels(head(labels))

getLabel (GenItems l _) = let srts = filter (\x ->

case x of Symbol _ Sort -> True;

_ -> False) l

in "ga_generated_" ++ concat

(intersperse "__"

(map (show . symbId) srts))

type Sort_map = FiniteMap Id Id

type Fun_map = FiniteMap Id [(OpType, Id, Bool)]

{- The third field is true iff the target symbol is

total -}

type Pred_map = FiniteMap Id [(PredType,Id)]

--instance (Show a,Show b,Ord a) => Show (FiniteMap a b) where

-- showsPrec _ = shows . fmToList

data Morphism = Morphism {msource,mtarget :: Sign,

sort_map :: Sort_map,

fun_map :: Fun_map,

pred_map :: Pred_map}

deriving Eq -- (Eq,Show)

embedMorphism :: Sign -> Sign -> Morphism

embedMorphism a b =

let

l = case a of (SignAsList x) -> x

slist = map (\x -> (x,x)) $ map sortId $ map item $

mapMaybe (\x -> case x of (ASortItem s) -> Just s;

_ -> Nothing) l

flist = map (\x -> (opId x,[(opType x,opId x,(opKind.opType) x == Total)]))

$ map item $ mapMaybe (\x -> case x of (AnOpItem o) -> Just o;

_ -> Nothing) l

plist = map (\x -> (predId x,[(predType x,predId x)])) $

map item $ mapMaybe (\x -> case x of (APredItem p) -> Just p;

_ -> Nothing) l

in

Morphism a b (listToFM slist) (listToFM flist) (listToFM plist)