{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
-- | Constraints for /parametric polymorphism/ and /type class polymorphism/.
module Language.LOL.Typing.Constraint.Polytype where

import Control.Applicative (Applicative(..))
import Control.Monad (forM_, join)
import Data.Function (($), (.))
import Data.Functor (Functor(..), (<$>))
import qualified Data.List as List
import Data.Monoid ((<>))
import qualified Data.Sequence as Seq
import Data.Text.Buildable (Buildable(..))
import qualified Data.Text.Lazy.Builder as Builder
import Text.Show (Show(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver
import Language.LOL.Typing.Constraint.Monotype
import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build

-- * Type 'Constraint_Polytype'

-- | The /polymorphism 'Constraint's/.
data Constraint_Polytype info
 =   Constraint_Polytype_generalizes_from_Monotype Polyvar ([Rigtype], Monotype) info
  -- ^ A /polytype generalization constraint/:
  -- assign a 'Polyvar' to the 'Polytype'
  -- obtained by generalizing a 'Monotype' to a 'Forall' 'Quantification'
  -- over all its 'subvars' except those of the given 'Rigtype's.
  -- These excluded 'Rigtype's are used to avoid generalizing
  -- 'Monovar's appearing in the /typing context/,
  -- since they appear in 'Constraint's that /need/ to be satisfied.
  --
  -- NOTE: a 'Constraint_Polytype_generalizes_from_Monotype' requires
  -- that the 'Polytype'’s 'quantifiers' have at least the 'qualifiers'
  -- of the 'Monotype'’s 'subvars' they generalize. See 'class_polytype_forall'.
 |   Constraint_Polytype_instantiates_to_Monotype Polytyref Monotype info
  -- ^ A /polytype explicit instantiation constraint/
  -- (/explicit/ meaning known when collecting the 'Constraint's):
  -- restricts a 'Monotype' to be /less general/
  -- than a 'Polytype' (from given 'Polytyref')
  -- i.e. to be an /instance/ of it.
  --
  -- NOTE: instantiating a 'Polytyref'
  -- implies that the instantiated 'qualifiers'
  -- are entailed by the 'qualifiers' in the solving 'Substitution'.
 |   Constraint_Polytype_implicit_instantiates_to_Monotype ([Rigtype], Monotype) Monotype info
  -- ^ A /polytype implicit instantiation constraint/:
  -- restrict a 'Monotype' to be an /instance/ of the 'Polytype'
  -- obtained by 'generalize'-ing another 'Monotype'
  -- over all its 'subvars' except those of the given 'Rigtype's.
  --
  -- NOTE: the idea is that such a 'Constraint'
  -- can be solved only if no more deductions
  -- can be found in the remaining 'Constraint's ('state_constraint_constraints')
  -- about the 'quantifiers' of the 'Polytype' returned by 'class_polytype_forall'.
 |   Constraint_Polytype_generalized_by_Monotype ([Rigtype], Polytyref) Monotype info
  -- ^ A /polytype rigidification constraint/:
  -- restricts a 'Monotype' to be /more general/
  -- than a 'Polytype' (from given 'Polytyref').
  --
  -- NOTE: determining this requires to know which 'Monovar's in the 'Monotype'
  -- are 'Polyvar's, and which are 'Monovar's, hence
  -- a set of 'Rigtype's is attached.
  --
  -- NOTE: this 'Constraint' becomes important
  -- to handle /expression/ with /type signature/,
  -- because then the inferred 'Monotype' of the /expression/
  -- should be /more general/ than the /type signature/.
 deriving (Show)

-- | Infix alias for 'Constraint_Polytype_generalized_by_Monotype'.
(.::.) :: Monotype -> Polytyref -> [Rigtype] -> info -> Constraint_Polytype info
(.::.) monoty polyty rigtys = Constraint_Polytype_generalized_by_Monotype (rigtys, polyty) monoty

instance Functor Constraint_Polytype where
	fmap f c =
		case c of
		 Constraint_Polytype_generalizes_from_Monotype polyty monos info ->
			Constraint_Polytype_generalizes_from_Monotype polyty monos (f info)
		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->
			Constraint_Polytype_instantiates_to_Monotype polyref monoty (f info)
		 Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 info ->
			Constraint_Polytype_implicit_instantiates_to_Monotype (monotys, t2) t1 (f info)
		 Constraint_Polytype_generalized_by_Monotype ty pair info ->
			Constraint_Polytype_generalized_by_Monotype ty pair (f info)
instance Buildable info => Buildable (Constraint_Polytype info) where
	build c =
		case c of
		 Constraint_Polytype_generalizes_from_Monotype polyty (rigtys, monoty) info ->
			"p" <> build polyty
			 <> " := Generalize"
			 <> Build.tuple [build_rigvars rigtys, build monoty]
			 <> build_info info
		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->
			build monoty
			 <> " := Instantiate"
			 <> Build.tuple [build polyref]
			 <> build_info info
		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, polyty) monoty info ->
			build monoty
			 <> " := Implicit"
			 <> Build.tuple [build_rigvars rigtys, build polyty]
			 <> build_info info
		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info ->
			build monoty
			 <> " := Rigidify"
			 <> Build.tuple [build_rigvars rigtys, build polyref]
			 <> build_info info
		where
		build_info info = " {- " <> build info <> " -}"
		build_rigvars :: [Monotype] -> Builder.Builder
		build_rigvars = Build.list . (Monotype_Var <$>) . subvars

instance Substitutable (Constraint_Polytype info) where
	subvars c =
		case c of
		 Constraint_Polytype_generalizes_from_Monotype _ (rigtys, monoty) _ ->
			subvars rigtys `List.union` subvars monoty
		 Constraint_Polytype_instantiates_to_Monotype polyref monoty _ ->
			subvars monoty `List.union` subvars polyref
		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 _ ->
			subvars t1 `List.union` subvars rigtys `List.union` subvars t2
		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty _ ->
			subvars monoty `List.union` subvars rigtys `List.union` subvars polyref
	sub `substitute` c =
		case c of
		 Constraint_Polytype_generalizes_from_Monotype sv (rigtys, monoty) info ->
			Constraint_Polytype_generalizes_from_Monotype sv
			 ( sub `substitute` rigtys
			 , sub `substitute` monoty )
			 info
		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info ->
			Constraint_Polytype_instantiates_to_Monotype
			 (sub `substitute` polyref)
			 (sub `substitute` monoty)
			 info
		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info ->
			Constraint_Polytype_implicit_instantiates_to_Monotype
			 ( sub `substitute` rigtys
			 , sub `substitute` t2 )
			 (sub `substitute` t1)
			 info
		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info ->
			Constraint_Polytype_generalized_by_Monotype
			 ( sub `substitute` rigtys
			 , sub `substitute` polyref )
			 (sub `substitute` monoty)
			 info
instance
 ( info ~ Info m
 , Show info
 , Buildable info
 , Solver_Constraint m
 , Solver_Monotype m
 , Solver_Polytype m
 , Solver_Class m
 ) => Solvable (Constraint_Polytype info) m where
	constraint_solver con =
		case con of
		 Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, monoty) _ -> do
			-- NOTE: Here 'monotype_substitution'
			-- can be in an inconsistent state,
			-- however 'class_reduction' makes it consistent
			-- (by calling: 'monotype_substitution_consistentify'),
			-- it then applies it to the 'class_qualifiers'
			-- (by calling: 'class_qualifiers_map' 'monotype_substitute').
			class_reduction
			-- NOTE: Apply 'monotype_substitution'
			-- to the 'Monotype's which must remain so,
			-- and to the 'Monotype' before generalizing it.
			polyty <- join $ class_polytype_forall
			 <$> monotype_substitute rigtys
			 <*> monotype_substitute monoty
			-- NOTE: The 'Polyvar' given by the 'Constraint'
			-- is then associated to the just computed 'Polytype',
			-- within 'state_polytype_substitution'.
			polytype_insert polyvar polyty
		
		 Constraint_Polytype_instantiates_to_Monotype polyref monoty info -> do
			polyty <- polytype_lookup polyref
			 -- NOTE: get a (known) 'Polytype' from the given 'Polytyref'.
			Qualification
			 { qualifiers
			 , qualified=inst_monoty
			 } <- polytype_instantiate monoty polyty
			 -- NOTE: instantiate the 'Polytype' into a 'Monotype'
			 -- using the 'polytype_freshvar'.
			let info' = info_insert (Info_Polytype_Instantiated polyty) info
			forM_ qualifiers $
			 -- NOTE: all instantiated 'qualifiers' have to be proven
				class_qualifier_toprove $
				info_insert (Info_Monotype_Unification monoty inst_monoty) info'
			constraint_push $
				constraint (monoty .==. inst_monoty $ info')
			 -- NOTE: add a 'Constraint_Monotype_Unification'
			 -- between the given 'Monotype' and the instantiated 'Polytype',
			 -- using the 'info' to store the original 'Polytype'.
		
		 Constraint_Polytype_implicit_instantiates_to_Monotype (rigtys, t2) t1 info -> do
			polyvar <- polytype_freshvar
			constraint_push_many $ constraints $ Seq.fromList
			 [ Constraint_Polytype_generalizes_from_Monotype polyvar (rigtys, t2) info
			 , Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var polyvar) t1 info
			 ]
		
		 Constraint_Polytype_generalized_by_Monotype (rigtys, polyref) monoty info -> do
			polyty <- polytype_lookup polyref
			let info' = info_insert (Info_Polytype_Rigidified rigtys polyty) info
			Qualification
			 { qualifiers
			 , qualified=rigid_polyty
			 } <- polytype_rigvarify info rigtys polyty
			forM_ qualifiers $
			 -- NOTE: all rigidified 'qualifiers' are assumed.
				class_qualifier_assume $
				info_insert (Info_Monotype_Unification rigid_polyty monoty) info'
			 -- FIXME: Top has (monoty, monoty), but (rigid_polyty, monoty)
			 -- seems to be the correct thing to do.
			constraint_push $
				constraint (monoty .==. rigid_polyty $ info')