{- |
Module      :  ./HasCASL/TypeRel.hs
Description :  compute subtype dependencies
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

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

compute subtype dependencies
-}

module HasCASL.TypeRel where

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.ClassAna
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.DataAna
import HasCASL.MinType
import HasCASL.Merge

import Common.Id
import Common.AS_Annotation
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe

typeRel :: TypeMap -> Rel.Rel Id
typeRel = Rel.transReduce . Rel.irreflex . Rel.transClosure
  . Map.foldrWithKey ( \ i ti r ->
    Set.fold (Rel.insertPair i) r $ superTypes ti) Rel.empty

getRawKind :: TypeMap -> Id -> RawKind
getRawKind tm i = typeKind $
    Map.findWithDefault (error $ showId i " not found in type map") i tm

-- | make a polymorphic function from a to b
mkInjOrProjType :: Arrow -> TypeScheme
mkInjOrProjType arr =
    TypeScheme [aTypeArg, bTypeArg] (mkFunArrType aType arr bType) nullRange

injType :: TypeScheme
injType = mkInjOrProjType FunArr

projType :: TypeScheme
projType = mkInjOrProjType PFunArr

mkInjOrProj :: Arrow -> Set.Set OpInfo
mkInjOrProj arr = Set.singleton OpInfo
    { opType = mkInjOrProjType arr
    , opAttrs = Set.empty
    , opDefn = NoOpDefn Fun }

subtRelName :: Id
subtRelName = mkId [genToken "subt"]

subtRelType :: TypeScheme
subtRelType = TypeScheme [aTypeArg, bTypeArg]
  (mkFunArrType (mkProductType [aType, bType]) PFunArr unitType) nullRange

subtRel :: Set.Set OpInfo
subtRel = Set.singleton OpInfo
    { opType = subtRelType
    , opAttrs = Set.empty
    , opDefn = NoOpDefn Fun }

varRel :: Rel.Rel Id -> TypeMap -> Rel.Rel Id
varRel r =
  foldr (\ i -> Rel.insertPair i i) r . Map.keys
  . Map.filter (any (`elem` [CoVar, ContraVar]) . getKindAppl . typeKind)

subtAxioms :: TypeMap -> [Named Sentence]
subtAxioms tm0 =
  let tm = addUnit cpoMap tm0
      tr = varRel (typeRel tm) tm in
  if Rel.nullKeys $ typeRel tm0 then [] else
  subtReflex : subtTrans : subtInjProj : injTrans : idInj
  : map (subtAx tm) (Rel.toList tr)

nr :: Range
nr = nullRange

getKindAppl :: RawKind -> [Variance]
getKindAppl rk = case rk of
  ClassKind () -> []
  FunKind v _ r _ -> v : getKindAppl r

mkTypeArg :: Id -> Int -> TypeArg
mkTypeArg i c = TypeArg i NonVar (VarKind universe) rStar c Other nr

subtAx :: TypeMap -> (Id, Id) -> Named Sentence
subtAx tm (i1, i2) = let
    findType i = Map.findWithDefault
      (Map.findWithDefault (error "TypeRel.subtAx") i bTypes) i tm
    e1 = findType i1
    e2 = findType i2
    txt = shows i1 "_<_" ++ show i2
    l1 = getKindAppl $ typeKind e1
    l2 = getKindAppl $ typeKind e2
    l3 = zipWith minVariance l1 l2
    l4 = foldr (\ v (((tl, vl), pl), fl) ->
            let c = length pl + 1
                a = simpleIdToId $ genNumVar "a" c
                ta = mkTypeArg a (- (length tl + 1))
                b = simpleIdToId $ genNumVar "b" c
                tb = mkTypeArg b (- (length tl + 2))
                x = stringToId $ 'x' : show c
                y = stringToId $ 'y' : show c
                tx = typeArgToType ta
                ty = typeArgToType tb
                vx = mkVarDecl x tx
                vy = mkVarDecl y ty
            in (case v of
                  NonVar -> ((ta : tl, vx : vl), (tx, tx) : pl)
                  _ -> (([ta, tb] ++ tl, [vx, vy] ++ vl), (tx, ty) : pl)
               , case v of
                   CoVar -> mkSubtTerm tx ty vx vy : fl
                   ContraVar -> mkSubtTerm ty tx vy vx : fl
                   _ -> fl)) ((([], []), []), []) l3
    (args, fs) = l4
    (gens, acts) = args
    (act1, act2) = unzip acts
    (tyargs, vargs) = gens
    t1 = mkTypeAppl (toType i1) act1
    t2 = mkTypeAppl (toType i2) act2
    x1 = stringToId "x"
    x2 = stringToId "y"
    v1 = mkVarDecl x1 t1
    v2 = mkVarDecl x2 t2
    in makeNamed ("ga_subt_" ++ txt) $ Formula
         $ mkForall (map GenTypeVarDecl tyargs
                     ++ map GenVarDecl (vargs ++ [v1, v2]))
           $ (if null fs then id else
             mkLogTerm implId nr (foldr1 (mkLogTerm andId nr) fs))
               $ mkSubtTerm t1 t2 v1 v2

mkSubtTerm :: Type -> Type -> VarDecl -> VarDecl -> Term
mkSubtTerm t1 t2 v1 v2 = mkTerm subtRelName subtRelType [t1, t2] nr
  $ TupleTerm [QualVar v1, QualVar v2] nr

subtReflex :: Named Sentence
subtReflex = let
  v1 = mkVarDecl (stringToId "x") aType
  v2 = mkVarDecl (stringToId "y") aType
  in makeNamed "ga_subt_reflexive" $ Formula
       $ mkForall (GenTypeVarDecl aTypeArg : map GenVarDecl [v1, v2])
         $ mkSubtTerm aType aType v1 v2

xa :: VarDecl
xa = mkVarDecl (stringToId "x") aType

yb :: VarDecl
yb = mkVarDecl (stringToId "y") bType

zc :: VarDecl
zc = mkVarDecl (stringToId "z") cType

xaToZc :: [GenVarDecl]
xaToZc = map GenTypeVarDecl [aTypeArg, bTypeArg, cTypeArg]
  ++ map GenVarDecl [xa, yb, zc]

subtTrans :: Named Sentence
subtTrans = makeNamed "ga_subt_transitive" $ Formula
     $ mkForall xaToZc
     $ mkLogTerm implId nr
        (mkLogTerm andId nr
         (mkSubtTerm aType bType xa yb)
         $ mkSubtTerm bType cType yb zc)
        $ mkSubtTerm aType cType xa zc

mkInjTerm :: Type -> Type -> Term -> Term
mkInjTerm t1 t2 = mkTerm injName injType [t1, t2] nr

mkInjEq :: Type -> Type -> VarDecl -> VarDecl -> Term
mkInjEq t1 t2 v1 v2 =
   mkEqTerm eqId t2 nr (QualVar v2)
          $ mkInjTerm t1 t2 $ QualVar v1

subtInjProj :: Named Sentence
subtInjProj = makeNamed "ga_subt_inj_proj" $ Formula
     $ mkForall (map GenTypeVarDecl [aTypeArg, bTypeArg]
                 ++ map GenVarDecl [xa, yb])
     $ mkLogTerm implId nr
        (mkSubtTerm aType bType xa yb)
       $ mkLogTerm eqvId nr (mkInjEq aType bType xa yb)
        $ mkEqTerm eqId aType nr (QualVar xa)
          $ mkTerm projName projType [bType, aType] nr
            $ QualVar yb

injTrans :: Named Sentence
injTrans = makeNamed "ga_inj_transitive" $ Formula
     $ mkForall xaToZc
     $ mkLogTerm implId nr
        (mkLogTerm andId nr (mkSubtTerm aType bType xa yb)
          $ mkLogTerm andId nr (mkSubtTerm bType cType yb zc)
            $ mkInjEq aType bType xa yb)
       $ mkLogTerm eqvId nr (mkInjEq aType cType xa zc)
           $ mkInjEq bType cType yb zc

idInj :: Named Sentence
idInj = makeNamed "ga_inj_identity"
  $ Formula $ mkForall [GenTypeVarDecl aTypeArg, GenVarDecl xa]
  $ mkInjEq aType aType xa xa

monos :: Env -> [Named Sentence]
monos e = concatMap (makeMonos e) . Map.toList $ assumps e

makeMonos :: Env -> (Id, Set.Set OpInfo) -> [Named Sentence]
makeMonos e (i, s) = makeEquivMonos e i . map opType $ Set.toList s

makeEquivMonos :: Env -> Id -> [TypeScheme] -> [Named Sentence]
makeEquivMonos e i l = case l of
  [] -> []
  t : r -> mapMaybe (makeEquivMono e i t) r ++ makeEquivMonos e i r

mkTypedTerm :: Term -> Type -> Range -> Term
mkTypedTerm t = TypedTerm t OfType

mkTypedEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkTypedEqTerm i s r t1 t2 =
  mkEqTerm i s r (mkTypedTerm t1 s r) $ mkTypedTerm t2 s r

makeEquivMono :: Env -> Id -> TypeScheme -> TypeScheme -> Maybe (Named Sentence)
makeEquivMono e i s1 s2 = case getCommonSupertype e s1 s2 of
  Just (ty1, l1, ty2, l2, args, nTy) ->
    Just $ makeNamed "ga_monotonicity"
         $ Formula $ mkForall (map GenTypeVarDecl args)
           $ mkTypedEqTerm eqId nTy nr
           (mkInjTerm ty1 nTy
             $ QualOp Op (PolyId i [] nr) s1 l1 UserGiven nr)
           $ mkInjTerm ty2 nTy
             $ QualOp Op (PolyId i [] nr) s2 l2 UserGiven nr
  Nothing -> Nothing