{- |
Module      :  ./HasCASL/Builtin.hs
Description :  builtin types and functions
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

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

HasCASL's builtin types and functions
-}

module HasCASL.Builtin
    ( cpoMap
    , bList
    , bTypes
    , bOps
    , preEnv
    , addBuiltins
    , aTypeArg
    , bTypeArg
    , cTypeArg
    , aType
    , bType
    , cType
    , botId
    , whenElse
    , ifThenElse
    , defId
    , eqId
    , exEq
    , falseId
    , trueId
    , notId
    , negId
    , andId
    , orId
    , logId
    , predTypeId
    , implId
    , infixIf
    , eqvId
    , resId
    , resType
    , botType
    , whenType
    , defType
    , eqType
    , notType
    , logType
    , mkQualOp
    , mkEqTerm
    , mkLogTerm
    , toBinJunctor
    , mkTerm
    , mkTermInst
    , unitTerm
    , unitTypeScheme
    ) where

import Common.Id
import Common.Keywords
import Common.GlobalAnnotations
import Common.AS_Annotation
import Common.AnnoParser
import Common.AnalyseAnnos
import Common.Result
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le

import Text.ParserCombinators.Parsec

-- * buitln identifiers

trueId :: Id
trueId = mkId [mkSimpleId trueS]

falseId :: Id
falseId = mkId [mkSimpleId falseS]

ifThenElse :: Id
ifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])

whenElse :: Id
whenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])

infixIf :: Id
infixIf = mkInfix ifS

andId :: Id
andId = mkInfix lAnd

orId :: Id
orId = mkInfix lOr

implId :: Id
implId = mkInfix implS

eqvId :: Id
eqvId = mkInfix equivS

resId :: Id
resId = mkInfix "res"

{-
    make these prefix identifier to allow "not def x" to be recognized
    as "not (def x)" by giving def__ higher precedence then not__.
    Simple identifiers usually have higher precedence then ____,
    otherwise "def x" would be rejected. But with simple identifiers
    "not def x" would be parsed as "(not def) x" because ____ is left
    associative.
-}

defId :: Id
defId = mkId [mkSimpleId defS, placeTok]

notId :: Id
notId = mkId [mkSimpleId notS, placeTok]

negId :: Id
negId = mkId [mkSimpleId negS, placeTok]

builtinRelIds :: Set.Set Id
builtinRelIds = Set.fromList [typeId, eqId, exEq, defId]

builtinLogIds :: Set.Set Id
builtinLogIds = Set.fromList [andId, eqvId, implId, orId, infixIf, notId]

-- | add builtin identifiers
addBuiltins :: GlobalAnnos -> GlobalAnnos
addBuiltins ga =
    let ass = assoc_annos ga
        newAss = Map.union ass $ Map.fromList
                 [(applId, ALeft), (andId, ALeft), (orId, ALeft),
                  (implId, ARight), (infixIf, ALeft),
                  (whenElse, ARight)]
        precs = prec_annos ga
        pMap = Rel.toMap precs
        opIds = Set.unions (Map.keysSet pMap : Map.elems pMap)
        opIs = Set.toList
               (((Set.filter (\ i -> begPlace i || endPlace i) opIds
                Set.\\ builtinRelIds) Set.\\ builtinLogIds)
                Set.\\ Set.fromList [applId, whenElse])
        logs = [(eqvId, implId), (implId, andId), (implId, orId),
                (eqvId, infixIf), (infixIf, andId), (infixIf, orId),
                 (andId, notId), (orId, notId),
                (andId, negId), (orId, negId)]
        rels1 = map ( \ i -> (notId, i)) $ Set.toList builtinRelIds
        rels1b = map ( \ i -> (negId, i)) $ Set.toList builtinRelIds
        rels2 = map ( \ i -> (i, whenElse)) $ Set.toList builtinRelIds
        ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
        ops2 = map ( \ i -> (i, applId)) opIs
        newPrecs = foldl (\ p (a, b) -> if Rel.path b a p then p else
                         Rel.insertDiffPair a b p) precs $
                   concat [logs, rels1, rels1b, rels2, ops1, ops2]
    in case addGlobalAnnos ga { assoc_annos = newAss
          , prec_annos = Rel.transClosure newPrecs } $
            map parseDAnno displayStrings of
         Result _ (Just newGa) -> newGa
         _ -> error "addBuiltins"

displayStrings :: [String]
displayStrings =
  [ "%display __\\/__ %LATEX __\\vee__"
  , "%display __/\\__ %LATEX __\\wedge__"
  , "%display __=>__ %LATEX __\\Rightarrow__"
  , "%display __<=>__ %LATEX __\\Leftrightarrow__"
  , "%display not__ %LATEX \\neg__"
  ]

parseDAnno :: String -> Annotation
parseDAnno str = case parse annotationL "" str of
    Left _ -> error "parseDAnno"
    Right a -> a

aVar :: Id
aVar = stringToId "a"

bVar :: Id
bVar = stringToId "b"

cVar :: Id
cVar = stringToId "c"

aType :: Type
aType = typeArgToType aTypeArg

bType :: Type
bType = typeArgToType bTypeArg

cType :: Type
cType = typeArgToType cTypeArg

lazyAType :: Type
lazyAType = mkLazyType aType

varToTypeArgK :: Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK i n v k = TypeArg i v (VarKind k) (toRaw k) n Other nullRange

varToTypeArg :: Id -> Int -> Variance -> TypeArg
varToTypeArg i n v = varToTypeArgK i n v universe

mkATypeArg :: Variance -> TypeArg
mkATypeArg = varToTypeArg aVar (-1)

aTypeArg :: TypeArg
aTypeArg = mkATypeArg NonVar

aTypeArgK :: Kind -> TypeArg
aTypeArgK = varToTypeArgK aVar (-1) NonVar

bTypeArg :: TypeArg
bTypeArg = varToTypeArg bVar (-2) NonVar

cTypeArg :: TypeArg
cTypeArg = varToTypeArg cVar (-3) NonVar

bindVarA :: TypeArg -> Type -> TypeScheme
bindVarA a t = TypeScheme [a] t nullRange

bindA :: Type -> TypeScheme
bindA = bindVarA aTypeArg

resType :: TypeScheme
resType = TypeScheme [aTypeArg, bTypeArg]
    (mkFunArrType (mkProductType [lazyAType, mkLazyType bType]) FunArr aType)
    nullRange

lazyLog :: Type
lazyLog = mkLazyType unitType

aPredType :: Type
aPredType = TypeAbs (mkATypeArg ContraVar)
    (mkFunArrType aType PFunArr unitType) nullRange

eqType :: TypeScheme
eqType = bindA $ mkFunArrType (mkProductType [lazyAType, lazyAType])
    PFunArr unitType

logType :: TypeScheme
logType = simpleTypeScheme $ mkFunArrType
    (mkProductType [lazyLog, lazyLog]) PFunArr unitType

notType :: TypeScheme
notType = simpleTypeScheme $ mkFunArrType lazyLog PFunArr unitType

whenType :: TypeScheme
whenType = bindA $ mkFunArrType
    (mkProductType [lazyAType, lazyLog, lazyAType]) PFunArr aType

unitTypeScheme :: TypeScheme
unitTypeScheme = simpleTypeScheme lazyLog

botId :: Id
botId = mkId [mkSimpleId "bottom"]

predTypeId :: Id
predTypeId = mkId [mkSimpleId "Pred"]

logId :: Id
logId = mkId [mkSimpleId "Logical"]

botType :: TypeScheme
botType = let a = aTypeArgK cppoCl in bindVarA a $ mkLazyType $ typeArgToType a

defType :: TypeScheme
defType = bindA $ mkFunArrType lazyAType PFunArr unitType

-- | builtin functions
bList :: [(Id, TypeScheme)]
bList = (botId, botType) : (defId, defType) : (notId, notType) :
        (negId, notType) : (whenElse, whenType) :
        (trueId, unitTypeScheme) : (falseId, unitTypeScheme) :
        (eqId, eqType) : (exEq, eqType) : (resId, resType) :
        map ( \ o -> (o, logType)) [andId, orId, eqvId, implId, infixIf]

mkTypesEntry :: Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry i k cs s d =
  (i, TypeInfo (toRaw k) (Set.fromList cs) (Set.fromList s) d)

funEntry :: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry a s cs =
  mkTypesEntry (arrowId a) funKind (funKind : cs) (map arrowId s) NoTypeDefn

mkEntry :: Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry i k cs = mkTypesEntry i k cs []

pEntry :: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry i k = mkEntry i k [k]

-- | builtin data type map
bTypes :: TypeMap
bTypes = Map.fromList $ funEntry PFunArr [] []
    : funEntry FunArr [PFunArr] []
    : funEntry PContFunArr [PFunArr] [funKind3 cpoCl cpoCl cppoCl]
    : funEntry ContFunArr [PContFunArr, FunArr]
        [funKind3 cpoCl cpoCl cpoCl, funKind3 cpoCl cppoCl cppoCl]
    : pEntry unitTypeId cppoCl NoTypeDefn
    : pEntry predTypeId (FunKind ContraVar universe universe nullRange)
        (AliasTypeDefn aPredType)
    : pEntry lazyTypeId coKind NoTypeDefn
    : pEntry logId universe (AliasTypeDefn $ mkLazyType unitType)
    : map (\ n -> let k = prodKind n nullRange in
            mkEntry (productId n nullRange) k
              (k : map (prodKind1 n nullRange) [cpoCl, cppoCl]) NoTypeDefn)
          [2 .. 5]

cpoId :: Id
cpoId = stringToId "Cpo"

cpoCl :: Kind
cpoCl = ClassKind cpoId

cppoId :: Id
cppoId = stringToId "Cppo"

cppoCl :: Kind
cppoCl = ClassKind cppoId

-- | builtin class map
cpoMap :: ClassMap
cpoMap = Map.fromList
  [ (cpoId, ClassInfo rStar $ Set.singleton universe)
  , (cppoId, ClassInfo rStar $ Set.singleton cpoCl)]

-- | builtin function map
bOps :: Assumps
bOps = Map.fromList $ map ( \ (i, sc) ->
    (i, Set.singleton $ OpInfo sc Set.empty $ NoOpDefn Fun)) bList

-- | environment with predefined names
preEnv :: Env
preEnv = initialEnv { classMap = cpoMap, typeMap = bTypes, assumps = bOps }

mkQualOpInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst k i sc tys ps = QualOp Fun (PolyId i [] ps) sc tys k ps

mkQualOp :: Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp = mkQualOpInst Infer

mkTermInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTermInst k i sc tys ps t = ApplTerm (mkQualOpInst k i sc tys ps) t ps

mkTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm = mkTermInst Infer

mkBinTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm i sc tys ps t1 t2 = mkTerm i sc tys ps $ TupleTerm [t1, t2] ps

mkLogTerm :: Id -> Range -> Term -> Term -> Term
mkLogTerm i = mkBinTerm i logType []

mkEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm i ty = mkBinTerm i eqType [ty]

unitTerm :: Id -> Range -> Term
unitTerm i = mkQualOp i unitTypeScheme []

toBinJunctor :: Id -> [Term] -> Range -> Term
toBinJunctor i ts ps = case ts of
    [] -> error "toBinJunctor"
    [t] -> t
    t : rs -> mkLogTerm i ps t (toBinJunctor i rs ps)