Constraint.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Collect.Constraint where

-- vim: ft=haskell
-- import Data.Bool
-- import Data.Defaults (Defaults(..))
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($), (.))
import Data.Functor ((<$>))
import qualified Data.List as List
import qualified Data.Foldable as Foldable
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..), (<>))
import Data.Text (Text)
import Data.Text.Buildable (Buildable(..))
import Data.Tuple (fst, snd)
import Text.Show (Show(..))
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq

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

-- * Type 'Collect_Context'

-- | A 'Polytyref' substitution.
type Collect_Context = [(Name, Polytyref)]

-- * Type 'Collect_Constraint'

type Collect_Constraint
 =   Constraint_Either
     Constraint_Monotype
     Constraint_Polytype
     Collect_Infos

-- | Build a 'Constraint_Monotype_Unification' lifted into 'Collect_Constraint'.
unifies_with
 :: (Monotypeable x, Monotypeable y)
 => x -> y
 -> Collect_Info_Grammar -> Collect_Constraint
unifies_with x y info =
	Constraint_Either $ Left $
	Constraint_Monotype_Unification (monotype x) (monotype y) $
	Collect_Infos [Collect_Info_Grammar info]

-- | Build a 'Constraint_Polytype_instantiates_to_Monotype' lifted into 'Collect_Constraint'.
instantiates_to
 :: (Polytyrefable polyty, Monotypeable monoty)
 => polyty -> monoty
 -> Collect_Info_Grammar -> Collect_Constraint
instantiates_to p m info =
	Constraint_Either $ Right $
	Constraint_Polytype_instantiates_to_Monotype (polytyref p) (monotype m) $
	Collect_Infos [Collect_Info_Grammar info]

-- | Build a 'Constraint_Polytype_generalizes_from_Monotype' lifted into 'Collect_Constraint'.
generalizes_from
 :: Monotypeable monoty
 => Polyvar -> monoty -> Collect_Context
 -> Collect_Info_Grammar -> Collect_Constraint
generalizes_from p m ctx info =
	Constraint_Either $ Right $
	Constraint_Polytype_generalizes_from_Monotype
	 p (context_rigtypes ctx, monotype m) $
	Collect_Infos [Collect_Info_Grammar info]

-- | Build a 'Constraint_Polytype_generalized_by_Monotype' lifted into 'Collect_Constraint'.
generalized_by
 :: (Polytyrefable polyty, Monotypeable monoty)
 => polyty -> monoty -> Collect_Context
 -> Collect_Info_Grammar -> Collect_Constraint
generalized_by p m ctx info =
	Constraint_Either $ Right $
	Constraint_Polytype_generalized_by_Monotype
	 (context_rigtypes ctx, polytyref p) (monotype m) $
	Collect_Infos [Collect_Info_Grammar info]

-- * Type 'Collect_Info'

data Collect_Info
 =   Collect_Info_Solver  (Solver_Info Collect_Infos)
 |   Collect_Info_Grammar Collect_Info_Grammar
 deriving (Eq, Show)
newtype Collect_Infos
 =      Collect_Infos [Collect_Info]
 deriving (Eq, Show)

instance Infoable Info_Monotype Collect_Infos where
	info_insert i (Collect_Infos is) =
		Collect_Infos $
		( Collect_Info_Solver $ Solver_Info_Monotype i
		) : is
instance Infoable Info_Polytype Collect_Infos where
	info_insert i (Collect_Infos is) =
		Collect_Infos $
		( Collect_Info_Solver $ Solver_Info_Polytype i
		) : is
instance Infoable (Info_Class Collect_Infos) Collect_Infos where
	info_insert i (Collect_Infos is) =
		Collect_Infos $
		( Collect_Info_Solver $ Solver_Info_Class i
		) : is

instance Buildable Collect_Infos where
	build (Collect_Infos is) = Build.list is
instance Buildable Collect_Info where
	build x =
		case x of
		 Collect_Info_Solver  i -> build i
		 Collect_Info_Grammar i -> build i

-- ** Type 'Collect_Info_Grammar'

data Collect_Info_Grammar
 =   Collect_Info_Grammar_Expr Text
 deriving (Eq, Show)
instance Buildable Collect_Info_Grammar where
	build x =
		case x of
		 Collect_Info_Grammar_Expr t -> build t

-- * Type 'Collect_Error'

data Collect_Error info err
 =   Collect_Error_Solver  [(info, err)]
 |   Collect_Error_Grammar [Collect_Error_Grammar]
 deriving (Eq, Show)

-- ** Type 'Collect_Error_Grammar'

data Collect_Error_Grammar
 =   Collect_Error_Grammar_Variable_not_in_scope Text
 deriving (Eq, Show)

context_insert :: Polytyrefable a => Name -> a -> Collect_Context -> Collect_Context
context_insert i p = ((i, polytyref p) :)

context_lookup :: Name -> Collect_Context -> Maybe Polytyref
context_lookup = List.lookup

context_rigtypes :: Collect_Context -> [Rigtype]
context_rigtypes ctx = Monotype_Var <$> subvars (snd <$> ctx)

hussel :: Seq Collect_Constraint -> Seq Collect_Constraint
hussel = (\(as, bs) -> (snd <$> bs) <> as) . go mempty
	where
	go :: Seq Polyvar -> Seq Collect_Constraint
	 -> (Seq Collect_Constraint, Seq (Polyvar, Collect_Constraint))
	go polyvars cs =
		case Seq.viewl cs of
		 Seq.EmptyL -> mempty
		 (c@(Constraint_Either e) Seq.:< rest) ->
			case e of
			 Right (Constraint_Polytype_instantiates_to_Monotype (Polytyref_Var var) _ _) ->
				let (new, gs)  = go (var Seq.<| polyvars) rest in
				let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in
				((snd <$> gs2)<>Seq.singleton c<>new, gs1)
			 Right (Constraint_Polytype_generalizes_from_Monotype var _ _)
				| var `Foldable.elem` polyvars ->
				let (new, gs) = go polyvars rest in
				(new, (var,c) Seq.<| gs)
			 _ ->
				let (new, gs)  = go polyvars rest in
				let (gs1, gs2) = Seq.partition ((`Foldable.elem` polyvars) . fst) gs in
				((snd <$> gs2)<>Seq.singleton c<>new, gs1)