{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Ord'.
module Language.Symantic.Compiling.Ord where

import Control.Monad
import Data.Ord (Ord)
import qualified Data.Ord as Ord
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (Ord(..))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Eq
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Ord'
-- | Symantic.
class Sym_Eq term => Sym_Ord term where
	compare :: Ord a => term a -> term a -> term Ordering
	(<)     :: Ord a => term a -> term a -> term Bool
	(<=)    :: Ord a => term a -> term a -> term Bool
	(>)     :: Ord a => term a -> term a -> term Bool
	(>=)    :: Ord a => term a -> term a -> term Bool
	max     :: Ord a => term a -> term a -> term a
	min     :: Ord a => term a -> term a -> term a
	
	default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
	default (<)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (<=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (>)     :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default (>=)    :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
	default max     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
	default min     :: (Trans t term, Ord a) => t term a -> t term a -> t term a
	
	compare  = trans_map2 compare
	(<)      = trans_map2 (<)
	(<=)     = trans_map2 (<=)
	(>)      = trans_map2 (>)
	(>=)     = trans_map2 (>=)
	min      = trans_map2 min
	max      = trans_map2 max

infix 4 <
infix 4 <=
infix 4 >
infix 4 >=

type instance Sym_of_Iface (Proxy Ord) = Sym_Ord

instance Sym_Ord HostI where
	compare = liftM2 Ord.compare
	(<)     = liftM2 (Ord.<)
	(<=)    = liftM2 (Ord.<=)
	(>)     = liftM2 (Ord.>)
	(>=)    = liftM2 (Ord.>=)
	min     = liftM2 Ord.min
	max     = liftM2 Ord.max
instance Sym_Ord TextI where
	compare = textI_app2  "compare"
	(<)     = textI_infix "<"  (Precedence 4)
	(<=)    = textI_infix "<=" (Precedence 4)
	(>)     = textI_infix ">"  (Precedence 4)
	(>=)    = textI_infix ">=" (Precedence 4)
	min     = textI_app2  "min"
	max     = textI_app2  "max"
instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
	compare = dupI2 sym_Ord compare
	(<)     = dupI2 sym_Ord (<)
	(<=)    = dupI2 sym_Ord (<=)
	(>)     = dupI2 sym_Ord (>)
	(>=)    = dupI2 sym_Ord (>=)
	min     = dupI2 sym_Ord min
	max     = dupI2 sym_Ord max

sym_Ord :: Proxy Sym_Ord
sym_Ord = Proxy

instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Ord
 , Inj_Const (Consts_of_Ifaces is) Ordering
 , Proj_Con (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Ord) ast where
	term_fromI ast =
		case ast_lexem ast of
		 "compare" -> test2_from compare tyOrdering
		 "<="      -> test2_from (<=)    tyBool
		 "<"       -> test2_from (<)     tyBool
		 ">="      -> test2_from (>=)    tyBool
		 ">"       -> test2_from (>)     tyBool
		 "min"     -> op2_from min
		 "max"     -> op2_from max
		 _ -> \_ctx _k -> Left $ Error_Term_unsupported
		where
		test2_from
		 :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term (UnProxy res))
		 -> Type (Consts_of_Ifaces is) 'KiTerm res
		 -> LamCtx_Type is (Lexem ast) ctx
		 -> ( forall h. Type (Consts_of_Ifaces is) 'KiTerm h
		             -> Term_of_LamCtx ctx h is ls (Proxy Ord ': rs)
		             -> Either (Error_Term is ast) ret )
		 -> Either (Error_Term is ast) ret
		test2_from op ty_res ctx k =
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_x] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
				k (ty_x ~> ty_res) $ Term_of_LamCtx $
				 \c -> lam $ op (x c)
			 [ast_x, ast_y] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
				check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
				check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
				k ty_res $ Term_of_LamCtx $
				 \c -> x c `op` y c
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2
		op2_from
		 :: (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term a)
		 -> LamCtx_Type is (Lexem ast) ctx
		 -> ( forall h. Type (Consts_of_Ifaces is) 'KiTerm h
		             -> Term_of_LamCtx ctx h is ls (Proxy Ord ': rs)
		             -> Either (Error_Term is ast) ret )
		 -> Either (Error_Term is ast) ret
		op2_from op ctx k =
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_x] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
				k (ty_x ~> ty_x) $ Term_of_LamCtx $
				 \c -> lam $ op (x c)
			 [ast_x, ast_y] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
				check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
				check_constraint (At (Just ast_x) (tyOrd :$ ty_x)) $ \Con ->
				k ty_x $ Term_of_LamCtx $
				 \c -> x c `op` y c
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2