{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  $Header$
Description :  coding out subtyping
Copyright   :  (c) C.Maeder Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Coding out subtyping in analogy to (SubPCFOL= -> PCFOL=),
   following Chap. III:3.1 of the CASL Reference Manual

The higher kinded builtin function arrow subtypes must be ignored.
-}

module Comorphisms.HasCASL2PCoClTyConsHOL (HasCASL2PCoClTyConsHOL (..)) where

import Logic.Logic
import Logic.Comorphism
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel
import Common.Id

import HasCASL.Logic_HasCASL
import HasCASL.Sublogic
import HasCASL.TypeRel
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le
import HasCASL.FoldTerm
import HasCASL.Builtin
import HasCASL.Unify (getTypeOf)

-- | The identity of the comorphism
data HasCASL2PCoClTyConsHOL = HasCASL2PCoClTyConsHOL deriving Show

instance Language HasCASL2PCoClTyConsHOL where
  language_name HasCASL2PCoClTyConsHOL = "HasCASL2HasCASLNoSubtypes"

instance Comorphism HasCASL2PCoClTyConsHOL
               HasCASL Sublogic
               BasicSpec Sentence SymbItems SymbMapItems
               Env Morphism Symbol RawSymbol ()
               HasCASL Sublogic
               BasicSpec Sentence SymbItems SymbMapItems
               Env Morphism Symbol RawSymbol () where
    sourceLogic HasCASL2PCoClTyConsHOL = HasCASL
    sourceSublogic HasCASL2PCoClTyConsHOL = top
    targetLogic HasCASL2PCoClTyConsHOL = HasCASL
    mapSublogic HasCASL2PCoClTyConsHOL sl = Just $ if has_sub sl then sl
        { has_sub = False
        , has_part = True
        , has_polymorphism = True
        , which_logic = max Horn $ which_logic sl
        , has_eq = True } else sl
    map_theory HasCASL2PCoClTyConsHOL = mkTheoryMapping
      (\ sig -> return (encodeSig sig, monos sig ++ subtAxioms (typeMap sig)))
      (map_sentence HasCASL2PCoClTyConsHOL)
    map_morphism HasCASL2PCoClTyConsHOL mor = return mor
        { msource = encodeSig $ msource mor
        , mtarget = encodeSig $ mtarget mor }
      -- other components need not to be adapted!
    map_sentence HasCASL2PCoClTyConsHOL _ = return . f2Formula
    map_symbol HasCASL2PCoClTyConsHOL _ = Set.singleton . id
    has_model_expansion HasCASL2PCoClTyConsHOL = True
    is_weakly_amalgamable HasCASL2PCoClTyConsHOL = True

-- | Add injection and projection symbols to a signature, remove supersorts
encodeSig :: Env -> Env
encodeSig sig = let
    tm1 = typeMap sig
    injMap = Map.insert injName (mkInjOrProj FunArr) $ assumps sig
    projMap = Map.insert projName (mkInjOrProj PFunArr) injMap
    subtRelMap = Map.insert subtRelName subtRel projMap
    in if Rel.nullKeys $ typeRel tm1 then sig else sig
           { assumps = subtRelMap
           , typeMap = Map.map ( \ ti -> ti { superTypes = Set.empty } ) tm1 }

f2Formula :: Sentence -> Sentence
f2Formula s = case s of
    Formula trm -> Formula $ t2term trm
    _ -> s

t2term :: Term -> Term
t2term = foldTerm mapRec
    { foldTypedTerm = \ o ntrm q ty ps ->
      let origTerm = TypedTerm ntrm q ty ps
          TypedTerm trm _ _ _ = o
      in case getTypeOf trm of
        Nothing -> origTerm -- assume this to be the exact type
        Just sty -> if eqStrippedType ty sty
          then if q == InType then unitTerm trueId ps else
                   if q == OfType then origTerm else ntrm
          else let
            prTrm = mkTermInst
              (if q == InType then UserGiven else Infer)
              projName (mkInjOrProjType PFunArr) [sty, ty] ps ntrm
          in case q of
            InType -> mkTerm defId defType [ty] ps prTrm
            AsType -> TypedTerm prTrm Inferred ty ps
            _ -> let
              rty = case getTypeAppl ty of
                      (TypeName l _ _, [lt]) | l == lazyTypeId -> lt
                      _ -> ty
              {- do not create injections into lazy types
              (via strippedType all function arrows became partial) -}
              rtrm = mkTerm injName (mkInjOrProjType FunArr) [sty, rty] ps ntrm
              in TypedTerm rtrm q ty ps }
