{-# LANGUAGE MultiParamTypeClasses #-}

{- |

Module : ./Comorphisms/HasCASL2PCoClTyConsHOL.hs

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 }