{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}

{-# OPTIONS_GHC -Wall      #-}

-- TODO: Function calls
module Language.Fortran.Model.Op.Core.Core where

import           Data.Singletons.TypeLits

import           Data.Vinyl

import           Language.Fortran.Model.Singletons
import           Language.Fortran.Model.Types

--------------------------------------------------------------------------------
--  Closed Typeclasses on BasicTypes
--------------------------------------------------------------------------------

data NumericBasicType k where
  NBTInt :: NumericBasicType 'BTInt
  NBTReal :: NumericBasicType 'BTReal

data ComparableBasicTypes k1 k2 where
  CBTNum :: NumericBasicType k1 -> NumericBasicType k2 -> ComparableBasicTypes k1 k2
  CBTBool :: ComparableBasicTypes 'BTLogical 'BTLogical
  CBTChar :: ComparableBasicTypes 'BTChar 'BTChar

--------------------------------------------------------------------------------
--  Operator Result Types
--------------------------------------------------------------------------------

data OpSpec ok args result where
  -- TODO: non-primitive literals (initialization)
  OSLit
    :: Prim p k a
    -> a
    -> OpSpec 'OKLit '[] (PrimS a)

  OSNum1
    :: NumericBasicType k1
    -> Prim p1 k1 a
    -> Prim p2 k2 b
    -> OpSpec 'OKNum '[PrimS a] (PrimS b)

  OSNum2
    :: NumericBasicType k1 -> NumericBasicType k2
    -> Prim p1 k1 a -> Prim p2 k2 b
    -> Prim (PrecMax p1 p2) (BasicTypeMax k1 k2) c
    -> OpSpec 'OKNum '[PrimS a, PrimS b] (PrimS c)

  OSLogical1
    :: Prim p1 'BTLogical a
    -> Prim 'P8 'BTLogical b
    -> OpSpec 'OKLogical '[PrimS a] (PrimS b)

  OSLogical2
    :: Prim p1 'BTLogical a
    -> Prim p2 'BTLogical b
    -> Prim 'P8 'BTLogical c
    -> OpSpec 'OKLogical '[PrimS a, PrimS b] (PrimS c)

  OSEq
    :: ComparableBasicTypes k1 k2
    -> Prim p1 k1 a -> Prim p2 k2 b
    -> Prim 'P8 'BTLogical c
    -> OpSpec 'OKEq '[PrimS a, PrimS b] (PrimS c)

  OSRel
    :: ComparableBasicTypes k1 k2
    -> Prim p1 k1 a -> Prim p2 k2 b
    -> Prim 'P8 'BTLogical c
    -> OpSpec 'OKRel '[PrimS a, PrimS b] (PrimS c)

  OSLookup
    :: D (Array i v)
    -> OpSpec 'OKLookup '[Array i v, i] v

  OSDeref
    :: RElem '(fname, a) fields i
    => D (Record rname fields)
    -> SSymbol fname
    -> OpSpec 'OKDeref '[Record rname fields] a

--------------------------------------------------------------------------------
--  Specific Operators
--------------------------------------------------------------------------------

data Op n ok where
  OpLit       :: Op 0 'OKLit

  OpNeg       :: Op 1 'OKNum
  OpPos       :: Op 1 'OKNum

  OpAdd       :: Op 2 'OKNum
  OpSub       :: Op 2 'OKNum
  OpMul       :: Op 2 'OKNum
  OpDiv       :: Op 2 'OKNum

  OpEq        :: Op 2 'OKEq
  OpNE        :: Op 2 'OKEq

  OpLT        :: Op 2 'OKRel
  OpLE        :: Op 2 'OKRel
  OpGT        :: Op 2 'OKRel
  OpGE        :: Op 2 'OKRel

  OpNot       :: Op 1 'OKLogical
  OpAnd       :: Op 2 'OKLogical
  OpOr        :: Op 2 'OKLogical
  OpEquiv     :: Op 2 'OKLogical
  OpNotEquiv  :: Op 2 'OKLogical

  OpLookup    :: Op 2 'OKLookup

  OpDeref     :: Op 1 'OKDeref