content: {-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
  {- |
  Module      :  ./Comorphisms/HasCASL2Haskell.hs
  Description :  translating program equations to Haskell
  Copyright   :  (c) Christian Maeder, Uni Bremen 2004-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable
  
  The embedding comorphism from HasCASL to Haskell.
  -}
  
  module Comorphisms.HasCASL2Haskell where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import Data.List ((\\))
  
  import Common.Id
  import Common.Result
  import Common.AS_Annotation
  import Common.GlobalAnnotations
  import Common.ExtSign
  import qualified Control.Monad.Fail as Fail
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.Builtin
  import HasCASL.DataAna
  import HasCASL.Le as HC
  import HasCASL.Logic_HasCASL
  import HasCASL.Sublogic
  
  import Haskell.Logic_Haskell as HS
  import Haskell.HatParser hiding (TypeInfo, Kind)
  import Haskell.HatAna
  import Haskell.TranslateId
  
  -- | The identity of the comorphism
  data HasCASL2Haskell = HasCASL2Haskell deriving Show
  
  instance Language HasCASL2Haskell -- default definition is okay
  
  instance Comorphism HasCASL2Haskell
                 HasCASL Sublogic
                 BasicSpec Sentence SymbItems SymbMapItems
                 Env
                 Morphism
                 HC.Symbol HC.RawSymbol ()
                 Haskell ()
                 HsDecls (TiDecl PNT) () ()
                 Sign
                 HaskellMorphism
                 HS.Symbol HS.RawSymbol () where
      sourceLogic HasCASL2Haskell = HasCASL
      sourceSublogic HasCASL2Haskell = noSubtypes
      targetLogic HasCASL2Haskell = Haskell
      mapSublogic HasCASL2Haskell _ = Just ()
      map_sentence HasCASL2Haskell = mapSingleSentence
      map_theory HasCASL2Haskell = mapTheory
      isInclusionComorphism HasCASL2Haskell = True
  
  mapSingleSentence :: Env -> Sentence -> Result (TiDecl PNT)
  mapSingleSentence sign sen = do
      (_, l) <- mapTheory (sign, [makeNamed "" sen])
      case l of
        [] -> Fail.fail "sentence was not translated"
        [s] -> return $ sentence s
        _ -> do (_, o) <- mapTheory (sign, [])
                case l \\ o of
                  [] -> Fail.fail "not a new sentence"
                  [s] -> return $ sentence s
                  _ -> Fail.fail "several sentences resulted"
  
  mapTheory :: (Env, [Named Sentence]) -> Result (Sign, [Named (TiDecl PNT)])
  mapTheory (sig, csens) = do
      let hs = translateSig sig
          ps = concatMap (translateSentence sig) csens
          cs = cleanSig hs ps
      (_, ExtSign hsig _, sens) <-
              hatAna (HsDecls (cs ++ map sentence ps),
                              emptySign, emptyGlobalAnnos)
      return (diffSign hsig preludeSign,
              filter (not . preludeEntity . getHsDecl . sentence) sens)
  
  -- former file UniqueId
  
  -- | Generates distinct names for overloaded function identifiers.
  distinctOpIds :: Int -> [(Id, [OpInfo])] -> [(Id, OpInfo)]
  distinctOpIds n l = case l of
    [] -> []
    (i, info) : idInfoList ->
      case info of
      [] -> distinctOpIds 2 idInfoList
      [hd] -> (i, hd) : distinctOpIds 2 idInfoList
      hd : tl -> (newName i n, hd) :
               distinctOpIds (n + 1) ((i, tl) : idInfoList)
  
  -- | Adds a number to the name of an identifier.
  newName :: Id -> Int -> Id
  newName (Id tlist idlist poslist) n =
    Id (tlist ++ [mkSimpleId $ '0' : show n]) idlist poslist
  
  -- | Searches for the real name of an overloaded identifier.
  findUniqueId :: Env -> Id -> TypeScheme -> Maybe (Id, OpInfo)
  findUniqueId env uid ts =
      let l = Set.toList $ Map.findWithDefault Set.empty uid $ assumps env
          fit :: Int -> [OpInfo] -> Maybe (Id, OpInfo)
          fit n tl =
              case tl of
                     [] -> Nothing
                     oi : rt -> if ts == opType oi then
                              Just (if null rt then uid else newName uid n, oi)
                              else fit (n + 1) rt
      in fit 2 l
  
  -- former TranslateAna file
  
  {- -----------------------------------------------------------------------
  Translation of an HasCASL-Environement
  ----------------------------------------------------------------------- -}
  
  {- | Converts an abstract syntax of HasCASL (after the static analysis)
  to the top datatype of the abstract syntax of haskell. -}
  translateSig :: Env -> [HsDecl]
  translateSig env =
      concatMap (translateTypeInfo env) (Map.toList $ typeMap env)
      ++ concatMap translateAssump (distinctOpIds 2 $ Map.toList
                        $ Map.map Set.toList $ assumps env)
  
  {- -----------------------------------------------------------------------
  Translation of types
  ----------------------------------------------------------------------- -}
  
  -- | Converts one type to a data or type declaration in Haskell.
  translateTypeInfo :: Env -> (Id, TypeInfo) -> [HsDecl]
  translateTypeInfo env (tid, info) =
    let hsname = mkHsIdent UpperId tid
        hsTyName = hsTyCon hsname
        mkTp = foldl hsTyApp hsTyName
        k = typeKind info
        loc = toProgPos $ posOfId tid
        ddecl = hsDataDecl loc
                         [] -- empty HsContext
                         (mkTp $ kindToTypeArgs 1 k)
                         [HsConDecl loc [] [] hsname []]
                         derives
    in case typeDefn info of
         NoTypeDefn -> case Set.toList $ superTypes info of
           [] -> [ddecl]
           j : _ -> [typeSynonym loc hsTyName $ TypeName j k 0]
         AliasTypeDefn ts ->
             [hsTypeDecl loc (mkTp $ getAliasArgs ts) $ getAliasType ts]
         DatatypeDefn de -> [sentence $ translateDt env de]
         _ -> []  -- ignore others
  
  isSameId :: Id -> Type -> Bool
  isSameId tid (TypeName tid2 _ _) = tid == tid2
  isSameId _tid _ty = False
  
  typeSynonym :: SrcLoc -> HsType -> Type -> HsDecl
  typeSynonym loc hsname = hsTypeDecl loc hsname . translateType
  
  kindToTypeArgs :: Int -> RawKind -> [HsType]
  kindToTypeArgs i k = case k of
      ClassKind _ -> []
      FunKind _ _ kr ps -> hsTyVar (mkSName ('a' : show i)
                                  $ toProgPos ps)
                        : kindToTypeArgs (i + 1) kr
  
  getAliasArgs :: Type -> [HsType]
  getAliasArgs ty = case ty of
      TypeAbs v t _ -> getArg v : getAliasArgs t
      ExpandedType _ t -> getAliasArgs t
      KindedType t _ _ -> getAliasArgs t
      _ -> []
  
  getArg :: TypeArg -> HsType
  getArg = hsTyVar . mkHsIdent LowerId . getTypeVar
  
  getAliasType :: Type -> HsType
  getAliasType ty = case ty of
      TypeAbs _ t _ -> getAliasType t
      ExpandedType _ t -> getAliasType t
      KindedType t _ _ -> getAliasType t
      _ -> translateType ty
  
  -- | Translation of an alternative constructor for a datatype definition.
  translateAltDefn :: Env -> DataPat -> AltDefn
                   -> [HsConDecl HsType [HsType]]
  translateAltDefn env dp (Construct muid ts p _) = case muid of
      Just uid -> let loc = toProgPos $ posOfId uid
                      sc = getConstrScheme dp p ts
                      -- resolve overloading
                      (c, ui) = translateId env uid sc
                  in case c of
                     UpperId -> -- no existentials, no context
                         [HsConDecl loc [] [] ui $
                                    map (HsBangedType . translateType) ts]
                     _ -> error "HasCASL2Haskell.translateAltDefn"
      Nothing -> []
  
  translateDt :: Env -> DataEntry -> Named HsDecl
  translateDt env de@(DataEntry _ i _ args _ alts) =
           let dp@(DataPat _ j _ _ _) = toDataPat de
               loc = toProgPos $ posOfId i
               hsname = mkHsIdent UpperId j
               hsTyName = hsTyCon hsname
               tp = foldl hsTyApp hsTyName $ map getArg args
           in
           (makeNamed ("ga_" ++ showId j "") $ hsDataDecl loc
                         [] -- empty HsContext
                         tp (concatMap (translateAltDefn env dp)
                             $ Set.toList alts)
                         derives) { isDef = True }
  
  {- -----------------------------------------------------------------------
  Translation of functions
  ----------------------------------------------------------------------- -}
  
  {- | Converts one distinct named function in HasCASL to the corresponding
  haskell declaration.
  Generates a definition (Prelude.undefined) for functions that are not
  defined in HasCASL. -}
  translateAssump :: (Id, OpInfo) -> [HsDecl]
  translateAssump (i, opinf) =
    let fname = mkHsIdent LowerId i
        loc = toProgPos $ posOfId i
        res = hsTypeSig loc
                         [fname] []
                         $ translateTypeScheme $ opType opinf
    in case opDefn opinf of
      ConstructData _ -> [] -- wrong case!
      _ -> [res, functionUndef loc fname]
  
  {- | Translation of the result type of a typescheme to a haskell type.
  Uses 'translateType'. -}
  translateTypeScheme :: TypeScheme -> HsType
  translateTypeScheme (TypeScheme _ t _) =
    translateType t
  
  
  -- | Translation of types (e.g. product type, type application ...).
  translateType :: Type -> HsType
  translateType t = case getTypeAppl t of
     (TypeName tid _ n, tyArgs) -> let num = length tyArgs in
        if n == 0 then
            if tid == unitTypeId && null tyArgs then
               hsTyCon $ mkSName "Bool" $ toProgPos $ getRange t
            else if tid == lazyTypeId && num == 1 then
               translateType $ head tyArgs
            else if isArrow tid && num == 2 then
               let [t1, t2] = tyArgs in
               hsTyFun (translateType t1) (translateType t2)
            else if isProductId tid && num > 1 then
               hsTyTuple loc0 $ map translateType tyArgs
            else foldl hsTyApp (hsTyCon $ mkHsIdent UpperId tid)
                 $ map translateType tyArgs
         else foldl hsTyApp (hsTyVar $ mkHsIdent LowerId tid)
              $ map translateType tyArgs
     _ -> error "translateType"
  
  toProgPos :: Range -> SrcLoc
  toProgPos p = if isNullRange p then loc0
                 else let Range (SourcePos n l c : _) = p
                       in SrcLoc n (1000 + (l - 1) * 80 + c) l c
  
  mkSName :: String -> SrcLoc -> SN HsName
  mkSName = SN . UnQual
  
  mkHsIdent :: IdCase -> Id -> SN HsName
  mkHsIdent c i = mkSName (translateIdWithType c i) $ toProgPos $ posOfId i
  
  translateId :: Env -> Id -> TypeScheme -> (IdCase, SN HsName)
  translateId env uid sc =
        let oid = findUniqueId env uid sc
            mkUnQual :: IdCase -> Id -> (IdCase, SN HsName)
            mkUnQual c j = (c, mkHsIdent c j)
        in case oid of
          Just (i, oi) -> if isConstructor oi then mkUnQual UpperId i
                          else mkUnQual LowerId i
          _ -> mkUnQual LowerId uid -- variable
  
  
  -- | Converts a term in HasCASL to an expression in haskell
  translateTerm :: Env -> Term -> HsExp
  translateTerm env t =
    let loc = toProgPos $ getRange t
    in case t of
      QualVar (VarDecl v ty _ _) ->
          let (c, i) = translateId env v $ simpleTypeScheme ty in
              case c of
              LowerId -> rec $ HsId $ HsVar i
              _ -> error "translateTerm: variable with UpperId"
      QualOp _ (PolyId uid _ _) sc _ _ _ -> let
      {- The identifier 'uid' may have been renamed. To find its new name,
      the typescheme 'ts' is tested for unifiability with the
      typeschemes of the assumps. If an identifier is found, it is used
      as HsVar or HsCon. -}
        mkPHsVar s = rec $ HsPId $ HsVar $ mkSName s loc
        mkHsVar s = rec $ HsId $ HsVar $ mkSName s loc
        mkHsCon s = rec $ HsId $ HsCon $ mkSName s loc
        mkUncurry s = rec $ HsApp (mkHsVar "uncurry") (mkHsVar s)
        mkErr s = expUndef loc $ s ++ pp loc
        hTrue = mkHsCon "True"
        a = mkHsVar "a"
        b = mkHsVar "b"
        c = mkHsVar "c"
        vs2 = [mkPHsVar "a", mkPHsVar "b"]
        vs3 = vs2 ++ [mkPHsVar "c"]
        pat2 = [rec $ HsPTuple loc vs2]
        pat3 = [rec $ HsPTuple loc vs3]
        mkLam2 x y = rec $ HsParen $ rec $ HsLambda pat2 $ rec $ HsIf x y hTrue
        mkLam3 x y = rec $ HsParen $ rec $ HsLambda pat3 $ rec $ HsIf x y c
        in if uid == botId then mkErr "bottom at "
        else if uid == trueId then hTrue
        else if uid == falseId then mkHsCon "False"
        else if uid == notId || uid == negId then mkHsVar "not"
        else if uid == defId then rec $ HsRightSection
                 (HsVar $ mkSName "seq" loc) hTrue
        else if uid == orId then mkUncurry "||"
        else if uid == andId then mkUncurry "&&"
        else if elem uid [eqId, eqvId, exEq] then
             mkErr "equality at "
        else if uid == implId then mkLam2 a b
        else if uid == infixIf then mkLam2 b a
        else if uid == whenElse then mkLam3 b a
        else if uid == ifThenElse then mkLam3 a b
        else let (cs, ui) = translateId env uid sc
        in rec $ HsId $ case cs of
          UpperId -> HsCon ui
          LowerId -> HsVar ui
      ApplTerm t1 t2 _ ->
         rec $ HsApp (translateTerm env t1) $ translateTerm env t2
      TupleTerm ts _ -> rec $ HsTuple (map (translateTerm env) ts)
      TypedTerm t1 tqual _ty _ -> -- check for global types later
        case tqual of
          InType -> expUndef loc $ show tqual
          _ -> translateTerm env t1
      QuantifiedTerm qu _vars _t1 _ -> expUndef loc $ show qu
      LambdaTerm pats _part t1 _ ->
          rec $ HsLambda
                   (map (translatePattern env) pats)
                   (translateTerm env t1)
      CaseTerm t1 progeqs _ ->
          rec $ HsCase (translateTerm env t1)
                 (map (translateCaseProgEq env) progeqs)
  
      LetTerm _ progeqs t1 _ ->
          rec $ HsLet (map (translateLetProgEq env) progeqs)
                (translateTerm env t1)
      _ -> error ("translateTerm: unexpected term: " ++ show t)
  
  -- | Conversion of patterns form HasCASL to haskell.
  translatePattern :: Env -> Term -> HsPat
  translatePattern env pat = case pat of
        QualVar (VarDecl v ty _ _) ->
            if show v == "_" then rec HsPWildCard else
            let (c, i) = translateId env v $ simpleTypeScheme ty
                in case c of
                   LowerId -> rec $ HsPId $ HsVar i
                   _ -> error ("unexpected constructor as variable: " ++ show v)
        QualOp _ (PolyId uid _ _) sc _ _ _ ->
          let (_, ui) = translateId env uid sc
          in rec $ HsPApp ui []
        ApplTerm p1 p2 _ ->
            let tp = translatePattern env p1
                a = translatePattern env p2
                in case struct tp of
                   HsPApp u os -> rec $ HsPParen $ rec $ HsPApp u (os ++ [a])
                   HsPParen (Pat (HsPApp u os)) ->
                       rec $ HsPParen $ rec $ HsPApp u (os ++ [a])
                   _ -> error ("problematic application pattern " ++ show pat)
        TupleTerm pats _ ->
            rec $ HsPTuple (toProgPos $ getRange pat)
                    $ map (translatePattern env) pats
        TypedTerm _ InType _ _ -> error "translatePattern InType"
        TypedTerm p _ _ty _ -> translatePattern env p
                                   -- the type is implicit
        AsPattern (VarDecl v ty _ _) p _ ->
              let (c, i) = translateId env v $ simpleTypeScheme ty
                  hp = translatePattern env p
              in case c of
                 LowerId -> rec $ HsPAsPat i hp
                 _ -> error ("unexpected constructor as @-variable: " ++ show v)
        _ -> error ("translatePattern: unexpected pattern: " ++ show pat)
  
  -- | Translation of a program equation of a case term in HasCASL
  translateCaseProgEq :: Env -> ProgEq -> HsAlt HsExp HsPat [HsDecl]
  translateCaseProgEq env (ProgEq pat t ps) =
    HsAlt (toProgPos ps)
          (translatePattern env pat)
          (HsBody (translateTerm env t))
          []
  
  -- | Translation of a program equation of a let term in HasCASL
  translateLetProgEq :: Env -> ProgEq -> HsDecl
  translateLetProgEq env (ProgEq pat t ps) =
    hsPatBind (toProgPos ps)
              (translatePattern env pat)
              (HsBody (translateTerm env t))
              []
  
  -- | Translation of a toplevel program equation
  translateProgEq :: Env -> ProgEq -> HsDecl
  translateProgEq env (ProgEq pat t _) =
      let loc = toProgPos $ getRange pat in case getAppl pat of
      Just (uid, sc, args) ->
          let (_, ui) = translateId env uid sc
          in hsFunBind loc [HsMatch loc ui
                       (map (translatePattern env) args) -- [HsPat]
                       (HsBody $ translateTerm env t) -- HsRhs
                       []]
      Nothing -> error ("translateLetProgEq: no toplevel id: " ++ show pat)
  
  -- | remove dummy decls given by sentences
  cleanSig :: [HsDecl] -> [Named HsDecl] -> [HsDecl]
  cleanSig ds sens =
      let dds = foldr ( \ nd l -> case basestruct $ sentence nd of
                        Just (HsDataDecl _ _ n _ _) -> n : l
                        _ -> l) [] sens
          funs = foldr ( \ nd l -> case basestruct $ sentence nd of
                        Just (HsFunBind _ (HsMatch _ n _ _ _ : _)) -> n : l
                        _ -> l) [] sens
      in filter ( \ hs -> case basestruct hs of
          Just (HsDataDecl _ _ n _ _) -> n `notElem` dds
          Just (HsTypeDecl _ n _) -> n `notElem` dds
          Just (HsFunBind _ (HsMatch _ n _ _ _ : _)) -> n `notElem` funs
          _ -> True)
         ds
  
  expUndef :: SrcLoc -> String -> HsExp
  expUndef loc = rec . HsApp (rec $ HsId $ HsVar $ mkSName "error" loc)
                     . rec . HsLit loc . HsString
  
  {- For the definition of an undefined function.
  Takes the name of the function as argument. -}
  functionUndef :: SrcLoc -> SN HsName -> HsDecl
  functionUndef loc s =
      hsFunBind loc [HsMatch loc s []  -- hsPatBind loc (rec $ HsPId $ HsVar s)
                (HsBody $ expUndef loc $ pp s)
                []]
  
  translateSentence :: Env -> Named Sentence -> [Named HsDecl]
  translateSentence env sen = case sentence sen of
      DatatypeSen dt -> map (translateDt env) dt
      ProgEqSen _ _ pe -> [sen { sentence = translateProgEq env pe }]
      _ -> []
  
  derives :: [SN HsName]
  derives = [] -- map (fakeSN . UnQual) ["Show", "Eq", "Ord"]
  