{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Constraint.Extra where

import Data.Function (($))
import Data.Functor (Functor(..))
import Data.Monoid ((<>))
import Data.Text.Buildable (Buildable(..))
import Text.Show (Show(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver

-- * Type 'Constraint_Extra'

data Constraint_Extra info
 =   Constraint_Extra_ToProve Class_Qualifier info
 |   Constraint_Extra_Assume  Class_Qualifier info
 deriving (Show)

instance Functor Constraint_Extra where
	fmap f c =
		case c of
		 Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve p (f info)
		 Constraint_Extra_Assume  p info -> Constraint_Extra_Assume  p (f info)
instance Buildable info => Buildable (Constraint_Extra info) where
	build c =
		case c of
		 Constraint_Extra_ToProve p info ->
			build $ Infoed info $ "Prove (" <> build p <> ")"
		 Constraint_Extra_Assume p info ->
			build $ Infoed info $ "Assume (" <> build p <> ")"
instance Substitutable (Constraint_Extra info) where
	subvars c =
		case c of
		 Constraint_Extra_ToProve p _ -> subvars p
		 Constraint_Extra_Assume  p _ -> subvars p
	sub `substitute` c =
		case c of
		 Constraint_Extra_ToProve p info -> Constraint_Extra_ToProve (sub `substitute` p) info
		 Constraint_Extra_Assume  p info -> Constraint_Extra_Assume  (sub `substitute` p) info
instance
 ( info ~ Info m
 , Show info
 , Buildable info
 , Solver_Class m
 ) => Solvable (Constraint_Extra info) m where
	constraint_solver c =
		case c of
		 Constraint_Extra_ToProve p info -> class_qualifier_toprove info p
		 Constraint_Extra_Assume  p info -> class_qualifier_assume  info p