1690N/A{- |

1690N/AModule : ./Omega/Terms.hs

1690N/ADescription : Hets-to-Omega conversion

1690N/ACopyright : (c) Ewaryst Schulz, DFKI Bremen 2009

1690N/ALicense : GPLv2 or higher, see LICENSE.txt

1690N/A

1690N/AMaintainer : ewaryst.schulz@dfki.de

1690N/AStability : provisional

1690N/APortability : non-portable(Logic)

1690N/A

1690N/AHasCASL terms will be exported to omega terms.

1690N/A-}

1690N/A

1690N/Amodule Omega.Terms

1690N/A ( toTerm

1690N/A ) where

1690N/A

1690N/Aimport Omega.DataTypes as DT

1690N/A

1690N/Aimport HasCASL.FoldTerm

1690N/Aimport HasCASL.As as As

1690N/A

1690N/Aimport Data.Maybe

1690N/A

3231N/AtoTerm :: As.Term -> DT.Term

1690N/AtoTerm = foldTerm toTermRec

1690N/A

1690N/AfailInTermRec :: String -> a

1690N/AfailInTermRec x = error $ "Occurence of " ++ x ++ " in toTermRec!"

2601N/A

2601N/A{- Structs: VarDecl PolyId GenVarDecl

2601N/AEnums: OpBrand Quantifier Partiality LetBrand -}

2601N/A

2601N/AquantifierName :: Quantifier -> String

2601N/AquantifierName Universal = "!"

2601N/AquantifierName Existential = "?"

2601N/AquantifierName Unique = "?!"

2601N/A

2601N/AlambdaName :: String

2601N/AlambdaName = "\\"

2601N/A

2601N/AtupleName :: String

2601N/AtupleName = "TUPLE"

2601N/A

2601N/AtoTermRec :: FoldRec DT.Term DT.Term

2601N/AtoTermRec = FoldRec

2601N/A { -- Term VarDecl

1690N/A foldQualVar = \ _ (VarDecl v _ _ _) -> DT.Var $ show v

1690N/A -- Term OpBrand PolyId TypeScheme [Type] InstKind Range

2601N/A , foldQualOp = \ _ _ (PolyId i _ _) _ _ _ _ -> Symbol $ show i

2601N/A -- Term a a Range

2601N/A , foldApplTerm = \ (ApplTerm _ o2 _) y z _ ->

2601N/A App y

2601N/A -- flatten the tuple to an argument list

2601N/A $ case (o2, z) of (TupleTerm _ _, App _ l) -> l

2601N/A _ -> [z]

2601N/A -- Term [a] Range

2601N/A , foldTupleTerm = \ _ l _ -> App (Symbol tupleName) l

2601N/A -- Term a TypeQual Type Range

1690N/A , foldTypedTerm = \ _ z _ _ _ -> z

2601N/A -- Term Quantifier [GenVarDecl] a Range

2601N/A , foldQuantifiedTerm =

2601N/A \ _ q vars z _ ->

2601N/A let bvars =

2601N/A -- we skip the type variables

2601N/A mapMaybe (\ x -> case x of

2601N/A GenVarDecl (VarDecl v _ _ _) -> Just $ DT.Var $ show v

1690N/A _ -> Nothing) vars

1690N/A in if null bvars then z else Bind (quantifierName q) bvars z

1690N/A -- Term [a] Partiality a Range

2439N/A , foldLambdaTerm = \ _ y _ z _ -> Bind lambdaName y z

1690N/A -- Term VarDecl a Range

2601N/A , foldAsPattern = \ _ _ _ _ -> failInTermRec "AsPattern"

2601N/A -- Term a [b] Range

2601N/A , foldCaseTerm = \ _ _ _ _ -> failInTermRec "CaseTerm"

2601N/A -- Term LetBrand [b] a Range

2601N/A , foldLetTerm = \ _ _ _ _ _ -> failInTermRec "LetTerm"

2601N/A -- ProgEq a a Range

2601N/A , foldProgEq = \ _ _ _ _ -> failInTermRec "ProgEq"

2601N/A -- Term Id [Type] [a] Range

1690N/A , foldResolvedMixTerm = \ _ _ _ _ _ -> failInTermRec "ResolvedMixTerm"

1690N/A -- Term Token

1690N/A , foldTermToken = \ _ _ -> failInTermRec "TermToken"

1690N/A -- TermTypeQual Type Range

2601N/A , foldMixTypeTerm = \ _ _ _ _ -> failInTermRec "MixTypeTerm"

2601N/A -- Term [a]

2601N/A , foldMixfixTerm = \ _ _ -> failInTermRec "MixfixTerm"

2601N/A -- Term BracketKind [a] Range

2601N/A , foldBracketTerm = \ _ _ _ _ -> failInTermRec "BracketTerm"

1690N/A }

2601N/A