{-# 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 Int -> HasCASL2PCoClTyConsHOL -> ShowS
[HasCASL2PCoClTyConsHOL] -> ShowS
HasCASL2PCoClTyConsHOL -> String
(Int -> HasCASL2PCoClTyConsHOL -> ShowS)
-> (HasCASL2PCoClTyConsHOL -> String)
-> ([HasCASL2PCoClTyConsHOL] -> ShowS)
-> Show HasCASL2PCoClTyConsHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasCASL2PCoClTyConsHOL] -> ShowS
$cshowList :: [HasCASL2PCoClTyConsHOL] -> ShowS
show :: HasCASL2PCoClTyConsHOL -> String
$cshow :: HasCASL2PCoClTyConsHOL -> String
showsPrec :: Int -> HasCASL2PCoClTyConsHOL -> ShowS
$cshowsPrec :: Int -> HasCASL2PCoClTyConsHOL -> ShowS
Show

instance Language HasCASL2PCoClTyConsHOL where
  language_name :: HasCASL2PCoClTyConsHOL -> String
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
sourceLogic HasCASL2PCoClTyConsHOL = HasCASL
HasCASL
    sourceSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic
sourceSublogic HasCASL2PCoClTyConsHOL = Sublogic
forall l. SemiLatticeWithTop l => l
top
    targetLogic :: HasCASL2PCoClTyConsHOL -> HasCASL
targetLogic HasCASL2PCoClTyConsHOL = HasCASL
HasCASL
    mapSublogic :: HasCASL2PCoClTyConsHOL -> Sublogic -> Maybe Sublogic
mapSublogic HasCASL2PCoClTyConsHOL sl :: Sublogic
sl = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just (Sublogic -> Maybe Sublogic) -> Sublogic -> Maybe Sublogic
forall a b. (a -> b) -> a -> b
$ if Sublogic -> Bool
has_sub Sublogic
sl then Sublogic
sl
        { has_sub :: Bool
has_sub = Bool
False
        , has_part :: Bool
has_part = Bool
True
        , has_polymorphism :: Bool
has_polymorphism = Bool
True
        , which_logic :: Formulas
which_logic = Formulas -> Formulas -> Formulas
forall a. Ord a => a -> a -> a
max Formulas
Horn (Formulas -> Formulas) -> Formulas -> Formulas
forall a b. (a -> b) -> a -> b
$ Sublogic -> Formulas
which_logic Sublogic
sl
        , has_eq :: Bool
has_eq = Bool
True } else Sublogic
sl
    map_theory :: HasCASL2PCoClTyConsHOL
-> (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
map_theory HasCASL2PCoClTyConsHOL = (Env -> Result (Env, [Named Sentence]))
-> (Env -> Sentence -> Result Sentence)
-> (Env, [Named Sentence])
-> Result (Env, [Named Sentence])
forall (m :: * -> *) sign1 sign2 sentence2 sentence1.
Monad m =>
(sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping
      (\ sig :: Env
sig -> (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Env
encodeSig Env
sig, Env -> [Named Sentence]
monos Env
sig [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ TypeMap -> [Named Sentence]
subtAxioms (Env -> TypeMap
typeMap Env
sig)))
      (HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> sentence1 -> Result sentence2
map_sentence HasCASL2PCoClTyConsHOL
HasCASL2PCoClTyConsHOL)
    map_morphism :: HasCASL2PCoClTyConsHOL -> Morphism -> Result Morphism
map_morphism HasCASL2PCoClTyConsHOL mor :: Morphism
mor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
mor
        { msource :: Env
msource = Env -> Env
encodeSig (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
msource Morphism
mor
        , mtarget :: Env
mtarget = Env -> Env
encodeSig (Env -> Env) -> Env -> Env
forall a b. (a -> b) -> a -> b
$ Morphism -> Env
mtarget Morphism
mor }
      -- other components need not to be adapted!
    map_sentence :: HasCASL2PCoClTyConsHOL -> Env -> Sentence -> Result Sentence
map_sentence HasCASL2PCoClTyConsHOL _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (Sentence -> Sentence) -> Sentence -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Sentence
f2Formula
    map_symbol :: HasCASL2PCoClTyConsHOL -> Env -> Symbol -> Set Symbol
map_symbol HasCASL2PCoClTyConsHOL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: HasCASL2PCoClTyConsHOL -> Bool
has_model_expansion HasCASL2PCoClTyConsHOL = Bool
True
    is_weakly_amalgamable :: HasCASL2PCoClTyConsHOL -> Bool
is_weakly_amalgamable HasCASL2PCoClTyConsHOL = Bool
True

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

f2Formula :: Sentence -> Sentence
f2Formula :: Sentence -> Sentence
f2Formula s :: Sentence
s = case Sentence
s of
    Formula trm :: Term
trm -> Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Term
t2term Term
trm
    _ -> Sentence
s

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