{-# LANGUAGE CPP
           , ScopedTypeVariables
           , GADTs
           , DataKinds
           , KindSignatures
           , GeneralizedNewtypeDeriving
           , TypeOperators
           , FlexibleContexts
           , FlexibleInstances
           , OverloadedStrings
           , PatternGuards
           , Rank2Types
           , LiberalTypeSynonyms
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
-- |
-- Module      :  Language.Hakaru.Syntax.TypeCheck
-- Copyright   :  Copyright (c) 2017 the Hakaru team
-- License     :  BSD3
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Ad-hoc implementation of unification (ad-hoc because polytypes are
-- inexpressible, and this module makes no attempt to express them).
----------------------------------------------------------------
module Language.Hakaru.Syntax.TypeCheck.Unification where

import Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad
import Language.Hakaru.Types.DataKind (Hakaru(..), HPair)
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.IClasses
import qualified Language.Hakaru.Parser.AST as U
import Data.Text (Text)

type Metadata = Maybe U.SourceSpan

type Unify1 (t :: Hakaru -> Hakaru) r x
  =  Sing x
  -> Metadata
  -> (forall a . x ~ t a => Sing a -> TypeCheckMonad r)
  -> TypeCheckMonad r

type Unify2 (t :: Hakaru -> Hakaru -> Hakaru) r x
  =  Sing x
  -> Metadata
  -> (forall a b . x ~ t a b => Sing a -> Sing b -> TypeCheckMonad r)
  -> TypeCheckMonad r

class TCMTypeRepr x where
  toTypeRepr :: x -> Maybe (Either Text (Some1 (Sing :: Hakaru -> *)))

instance TCMTypeRepr (Sing (x :: Hakaru)) where
  toTypeRepr :: Sing x -> Maybe (Either Text (Some1 Sing))
toTypeRepr = Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing))
forall a. a -> Maybe a
Just (Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing)))
-> (Sing x -> Either Text (Some1 Sing))
-> Sing x
-> Maybe (Either Text (Some1 Sing))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some1 Sing -> Either Text (Some1 Sing)
forall a b. b -> Either a b
Right (Some1 Sing -> Either Text (Some1 Sing))
-> (Sing x -> Some1 Sing) -> Sing x -> Either Text (Some1 Sing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing x -> Some1 Sing
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1

instance TCMTypeRepr Text where
  toTypeRepr :: Text -> Maybe (Either Text (Some1 Sing))
toTypeRepr = Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing))
forall a. a -> Maybe a
Just (Either Text (Some1 Sing) -> Maybe (Either Text (Some1 Sing)))
-> (Text -> Either Text (Some1 Sing))
-> Text
-> Maybe (Either Text (Some1 Sing))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text (Some1 Sing)
forall a b. a -> Either a b
Left

instance TCMTypeRepr () where
  toTypeRepr :: () -> Maybe (Either Text (Some1 Sing))
toTypeRepr () = Maybe (Either Text (Some1 Sing))
forall a. Maybe a
Nothing

unifyMeasure :: Unify1 'HMeasure r x
unifyMeasure :: Unify1 'HMeasure r x
unifyMeasure Sing x
ty Metadata
m forall (a :: Hakaru).
(x ~ 'HMeasure a) =>
Sing a -> TypeCheckMonad r
k =
  case Sing x
ty of
    SMeasure a -> Sing a -> TypeCheckMonad r
forall (a :: Hakaru).
(x ~ 'HMeasure a) =>
Sing a -> TypeCheckMonad r
k Sing a
a
    Sing x
_          -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HMeasure") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)

unifyArray :: Unify1 'HArray r x
unifyArray :: Unify1 'HArray r x
unifyArray Sing x
ty Metadata
m forall (a :: Hakaru). (x ~ 'HArray a) => Sing a -> TypeCheckMonad r
k =
  case Sing x
ty of
    SArray a -> Sing a -> TypeCheckMonad r
forall (a :: Hakaru). (x ~ 'HArray a) => Sing a -> TypeCheckMonad r
k Sing a
a
    Sing x
_        -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HArray") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)

unifyFun :: Unify2 '(:->) r x
unifyFun :: Unify2 (':->) r x
unifyFun Sing x
ty Metadata
m forall (a :: Hakaru) (b :: Hakaru).
(x ~ (a ':-> b)) =>
Sing a -> Sing b -> TypeCheckMonad r
k =
  case Sing x
ty of
    SFun a b -> Sing a -> Sing b -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru).
(x ~ (a ':-> b)) =>
Sing a -> Sing b -> TypeCheckMonad r
k Sing a
a Sing b
b
    Sing x
_        -> Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
":->") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)

unifyPair :: Unify2 HPair r x
unifyPair :: Unify2 HPair r x
unifyPair Sing x
ty Metadata
m forall (a :: Hakaru) (b :: Hakaru).
(x ~ HPair a b) =>
Sing a -> Sing b -> TypeCheckMonad r
k =
  TypeCheckMonad r
-> (TypeCheckMonad r -> TypeCheckMonad r)
-> Maybe (TypeCheckMonad r)
-> TypeCheckMonad r
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Metadata
-> Either Text (Sing Any)
-> Either Text (Sing x)
-> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
"HPair") (Sing x -> Either Text (Sing x)
forall a b. b -> Either a b
Right Sing x
ty)) TypeCheckMonad r -> TypeCheckMonad r
forall a. a -> a
id (Maybe (TypeCheckMonad r) -> TypeCheckMonad r)
-> Maybe (TypeCheckMonad r) -> TypeCheckMonad r
forall a b. (a -> b) -> a -> b
$ do
    SData (STyCon sym `STyApp` a `STyApp` b) _ <- Sing x -> Maybe (Sing x)
forall a. a -> Maybe a
Just Sing x
ty
    TypeEq s "Pair"
Refl <- Sing s -> Sing "Pair" -> Maybe (TypeEq s "Pair")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Pair"
sSymbol_Pair
    TypeCheckMonad r -> Maybe (TypeCheckMonad r)
forall a. a -> Maybe a
Just (TypeCheckMonad r -> Maybe (TypeCheckMonad r))
-> TypeCheckMonad r -> Maybe (TypeCheckMonad r)
forall a b. (a -> b) -> a -> b
$ Sing b -> Sing b -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru).
(x ~ HPair a b) =>
Sing a -> Sing b -> TypeCheckMonad r
k Sing b
a Sing b
b

matchTypes
  :: (TCMTypeRepr t0, TCMTypeRepr t1)
  => Sing (x :: Hakaru)
  -> Sing y
  -> Metadata
  -> t0 -> t1
  -> (x ~ y => TypeCheckMonad r)
  -> TypeCheckMonad r
matchTypes :: Sing x
-> Sing y
-> Metadata
-> t0
-> t1
-> ((x ~ y) => TypeCheckMonad r)
-> TypeCheckMonad r
matchTypes Sing x
t0 Sing y
t1 Metadata
m t0
e0 t1
e1 (x ~ y) => TypeCheckMonad r
k
  | Just TypeEq x y
Refl <- Sing x -> Sing y -> Maybe (TypeEq x y)
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing x
t0 Sing y
t1 = TypeCheckMonad r
(x ~ y) => TypeCheckMonad r
k
  | Bool
otherwise                =
    let tyRepr
          :: TCMTypeRepr t
          => Sing (x :: Hakaru)
          -> t
          -> Either Text (Some1 (Sing :: Hakaru -> *))
        tyRepr :: Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing x
d = Either Text (Some1 Sing)
-> (Either Text (Some1 Sing) -> Either Text (Some1 Sing))
-> Maybe (Either Text (Some1 Sing))
-> Either Text (Some1 Sing)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Some1 Sing -> Either Text (Some1 Sing)
forall a b. b -> Either a b
Right (Some1 Sing -> Either Text (Some1 Sing))
-> Some1 Sing -> Either Text (Some1 Sing)
forall a b. (a -> b) -> a -> b
$ Sing x -> Some1 Sing
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 Sing x
d) Either Text (Some1 Sing) -> Either Text (Some1 Sing)
forall a. a -> a
id (Maybe (Either Text (Some1 Sing)) -> Either Text (Some1 Sing))
-> (t -> Maybe (Either Text (Some1 Sing)))
-> t
-> Either Text (Some1 Sing)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Maybe (Either Text (Some1 Sing))
forall x. TCMTypeRepr x => x -> Maybe (Either Text (Some1 Sing))
toTypeRepr
        err :: Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err = Metadata
-> Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
forall (a :: Hakaru) (b :: Hakaru) r.
Metadata
-> Either Text (Sing a) -> Either Text (Sing b) -> TypeCheckMonad r
typeMismatch Metadata
m
        err :: Either Text (Sing (x :: Hakaru))
            -> Either Text (Sing (y :: Hakaru))
            -> TypeCheckMonad r
    in case (Sing x -> t0 -> Either Text (Some1 Sing)
forall t (x :: Hakaru).
TCMTypeRepr t =>
Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing x
t0 t0
e0, Sing y -> t1 -> Either Text (Some1 Sing)
forall t (x :: Hakaru).
TCMTypeRepr t =>
Sing x -> t -> Either Text (Some1 Sing)
tyRepr Sing y
t1 t1
e1) of
         (Left Text
a, Left Text
b) -> Either Text (Sing Any)
-> Either Text (Sing Any) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
a) (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
b)
         (Left Text
a, Right (Some1 Sing i
b)) -> Either Text (Sing Any) -> Either Text (Sing i) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
a) (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
b)
         (Right (Some1 Sing i
a), Left Text
b) -> Either Text (Sing i) -> Either Text (Sing Any) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
a) (Text -> Either Text (Sing Any)
forall a b. a -> Either a b
Left Text
b)
         (Right (Some1 Sing i
a), Right (Some1 Sing i
b)) -> Either Text (Sing i) -> Either Text (Sing i) -> TypeCheckMonad r
forall (x :: Hakaru) (y :: Hakaru) r.
Either Text (Sing x) -> Either Text (Sing y) -> TypeCheckMonad r
err (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
a) (Sing i -> Either Text (Sing i)
forall a b. b -> Either a b
Right Sing i
b)