{- |

Module : $Header$

Description : Hets-to-Omega conversion

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : provisional

Portability : non-portable(Logic)

HasCASL terms will be exported to omega terms.

-}

module Omega.Terms

( toTerm

) where

import Omega.DataTypes as DT

import HasCASL.FoldTerm

import HasCASL.As as As

import Data.Maybe

toTerm :: As.Term -> DT.Term

toTerm = foldTerm toTermRec

failInTermRec :: String -> a

failInTermRec x = error $ "Occurence of " ++ x ++ " in toTermRec!"

-- Structs: VarDecl PolyId GenVarDecl

-- Enums: OpBrand Quantifier Partiality LetBrand

quantifierName :: Quantifier -> String

quantifierName Universal = "!"

quantifierName Existential = "?"

quantifierName Unique = "?!"

lambdaName :: String

lambdaName = "\\"

tupleName :: String

tupleName = "TUPLE"

toTermRec :: FoldRec DT.Term DT.Term

toTermRec = FoldRec

{ -- Term VarDecl

foldQualVar = \_ (VarDecl v _ _ _) -> DT.Var $ show v

-- Term OpBrand PolyId TypeScheme [Type] InstKind Range

, foldQualOp = \_ _ (PolyId i _ _) _ _ _ _ -> Symbol $ show i

-- Term a a Range

, foldApplTerm = \ (ApplTerm _ o2 _) y z _ ->

App y

-- flatten the tuple to an argument list

$ case (o2, z) of (TupleTerm _ _, App _ l) -> l

_ -> [z]

-- Term [a] Range

, foldTupleTerm = \_ l _ -> App (Symbol tupleName) l

-- Term a TypeQual Type Range

, foldTypedTerm = \_ z _ _ _ -> z

-- Term Quantifier [GenVarDecl] a Range

, foldQuantifiedTerm =

\_ q vars z _ ->

let bvars =

-- we skip the type variables

(catMaybes

$ map (\x -> case x of GenVarDecl (VarDecl v _ _ _)

-> Just $ DT.Var $ show v

_ -> Nothing) vars)

in if null bvars then z else Bind (quantifierName q) bvars z

-- Term [a] Partiality a Range

, foldLambdaTerm = \_ y _ z _ -> Bind lambdaName y z

-- Term VarDecl a Range

, foldAsPattern = \_ _ _ _ -> failInTermRec "AsPattern"

-- Term a [b] Range

, foldCaseTerm = \_ _ _ _ -> failInTermRec "CaseTerm"

-- Term LetBrand [b] a Range

, foldLetTerm = \_ _ _ _ _ -> failInTermRec "LetTerm"

-- ProgEq a a Range

, foldProgEq = \_ _ _ _ -> failInTermRec "ProgEq"

-- Term Id [Type] [a] Range

, foldResolvedMixTerm = \_ _ _ _ _ -> failInTermRec "ResolvedMixTerm"

-- Term Token

, foldTermToken = \_ _ -> failInTermRec "TermToken"

-- TermTypeQual Type Range

, foldMixTypeTerm = \_ _ _ _ -> failInTermRec "MixTypeTerm"

-- Term [a]

, foldMixfixTerm = \_ _ -> failInTermRec "MixfixTerm"

-- Term BracketKind [a] Range

, foldBracketTerm = \_ _ _ _ -> failInTermRec "BracketTerm"

}