hets/Omega/Terms.hs

{- |
Module      :  ./Omega/Terms.hs
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
                    mapMaybe (\ 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"
    }