{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Calculus.Term where

import Control.Applicative (Applicative(..), (<$>))
import Control.Monad
import Data.Bool
import Data.Eq (Eq(..))
import Data.Foldable (Foldable(..))
import Data.Function (($), (.))
import Data.Maybe (Maybe(..), maybe, catMaybes, fromJust)
import Data.Monoid (Monoid(..), (<>))
import Data.Ord (Ord(..))
import Data.Text.Buildable (Buildable(..))
import qualified Data.Text.Lazy.Builder as Builder
import Data.Traversable (Traversable(..))
import Data.Typeable as Typeable
import Text.Show (Show(..), showParen, showString)

-- import Debug.Trace

import Language.LOL.Calculus.Abstraction

-- * Type 'Term'
-- | 'Term' @var@ forms the main /Abstract Syntax Tree/
-- of the present /explicitely typed/ (aka. /à la Church/) /lambda-calculus/,
-- whose /term constructors/ are:
--
-- * 'TeTy_Var':      for /term variable/ or /type variable/, see 'Abstraction'.
-- * 'TeTy_App':      for /term application/ or /type application/, see 'normalize'.
-- * 'Term_Abst':     for /term abstraction/ (aka. /λ-term/), see 'Abstraction'.
-- * 'Type_Abst':     for /type abstraction/ (aka. /Π-type/, aka. /dependent product/), see 'sort_of_type_abst'.
-- * 'Type_Sort':     for /sort constant/ of a /Pure Type System/ (aka. /PTS/), see 'sort_of_sort'.
-- * 'TeTy_Axiom':    for /custom axiom/, see 'Axiomable'.
--
-- Note that 'Type' and 'Term' share this same data-type
-- (hence the varying prefixes of the Haskell /data constructors/),
-- which avoids duplication of code for their common operations.
--
-- Note that this Haskell type DOES NOT guarantee by itself
-- the /well-formedness/ of the 'Term' (or 'Type'),
-- for instance one can construct such @malformed_type@: @(* *)@:
--
-- @
-- > let star = 'Type_Sort' 'sort_star_mono'
-- > let malformed_type = 'TeTy_App' star star
-- > 'left' 'type_error_msg' '$' 'type_of' 'context' malformed_type
-- Left ('Type_Error_Msg_Not_a_function' … )
-- @
--
-- Though an Haskell type could be crafted to get a stronger guarantee
-- over the /well-formedness/, it is not done here
-- for the following reasons :
--
-- 1. The /well-formedness/ alone is not really useful,
-- it’s the /well-typedness/ which matters,
-- and this depends upon a specific 'Context'.
--
-- 2. Guaranteeing a good combinaison of 'TeTy_App' with respect to 'Term_Abst' (or 'Type_Abst')
-- while using the 'Abstraction' approach could be done:
-- for instance by using @GADTs@ on 'Term'
-- to add an Haskell /type parameter/ @ty@ (aka. /index/)
-- constrained to @(i -> o)@, @i@ or @o@ depending on the /term constructors/,
-- and then by defining Haskell /type classes/
-- replicating: 'Functor', 'Foldable', 'Traversable', 'Monad' and 'Monad_Module_Left',
-- but working on /natural transformations/ (giving /indexed functors/, /indexed monads/, …),
-- however this yields to a significant increase in code complexity,
-- which is not really worth the resulting guarantee
-- (to my mind, here, simplicity has priority
-- over comprehensive automated checking,
-- especially since it’s a research program
-- where I don't fully know all what will be needed
-- and thus appreciate some level of flexibility).
--
-- So, with this actual 'Term' data-type:
-- 'type_of' MUST be used to check the /well-formedness/ along the /well-typedness/
-- of a 'Term' (or equivalently of a 'Type') with respect to a 'Context'.
data Term var
 =   TeTy_Var  var
 |   TeTy_App  (Term var) (Term var)
 |   Term_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) Term var)
 |   Type_Abst (Suggest Var_Name) (Type var) (Abstraction (Suggest Var_Name) Type var)
 |   Type_Sort Sort
 |   forall ax .
     ( Axiomable (Axiom ax)
     , Typeable ax
     ) => TeTy_Axiom (Axiom ax)

-- * Type 'Type'

-- | 'Type' and 'Term' share the same data-type.
type Type = Term

-- | 'Eq' instance ignores /bound variables/' 'Var_Name',
-- effectively testing for /α-equivalence/.
instance (Eq var, Show var) => Eq (Term var) where
	TeTy_Var x         == TeTy_Var y         = x   == y
	TeTy_App xf xa     == TeTy_App yf ya     = xf  == yf  && xa == ya
	Term_Abst _ xty xf == Term_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
	Type_Abst _ xty xf == Type_Abst _ yty yf = xty == yty && xf == yf -- NOTE: ignore Var_Name
	Type_Sort x        == Type_Sort y        = x   == y
	TeTy_Axiom x       == TeTy_Axiom y       = x `axiom_eq` y
	_ == _ = False
deriving instance Show var => Show (Term var)
-- | A 'Functor' instance capturing the notion of /variable renaming/.
deriving instance Functor Term
deriving instance Foldable Term
deriving instance Traversable Term
deriving instance Typeable Term
instance Show1 Term where showsPrec1 = showsPrec
instance Eq1   Term where (==#) = (==)

instance Applicative Term where
	pure = TeTy_Var
	(<*>) = ap
-- | A 'Monad' instance capturing the notion of /variable substitution/ with /capture-avoiding/.
instance Monad Term where
	return = pure
	Type_Sort        s >>= _  = Type_Sort s
	TeTy_Axiom       a >>= _  = TeTy_Axiom a
	TeTy_Var         v >>= go = go v
	TeTy_App    f    x >>= go = TeTy_App    (f    >>= go) (x  >>= go)
	Term_Abst v f_in f >>= go = Term_Abst v (f_in >>= go) (f >>>= go)
	Type_Abst v f_in f >>= go = Type_Abst v (f_in >>= go) (f >>>= go)
instance Buildable var => Buildable (Term var) where
	build = go False False
		where
		go :: forall v. (Buildable v)
		 => Bool -> Bool
		 -> Term v
		 -> Builder.Builder
		go parenBind parenApp te =
			case te of
			 Type_Sort s -> build s
			 TeTy_Axiom ax -> build ax
			 TeTy_Var v -> build v
			 TeTy_App f x ->
				(if parenApp then "(" else "")
				<> go True False f <> " " <> go True True x
				<> (if parenApp then ")" else "")
			 Term_Abst{} ->
				(if parenBind then "(" else "")
				<> "λ"{- <> "\\"-} <> go_abst parenBind parenApp te
			 Type_Abst (Suggest x) f_in f_out ->
				(if parenBind then "(" else "")
				<> (if x == ""
					then go True  False f_in
					else "∀" <> "(" <> build x <> ":" <> go False False f_in <> ")" )
				<> " -> "
				<> go False False (abstract_normalize f_out)
				<> (if parenBind then ")" else "")
		go_abst :: forall v. (Buildable v)
		 => Bool -> Bool
		 -> Term v
		 -> Builder.Builder
		go_abst parenBind parenApp te =
			case te of
			 Term_Abst (Suggest x) f_in f ->
				let body = abstract_normalize f in
				case body of
				 Term_Abst{} ->
					"(" <> go_var_def x <> ":" <> go False False f_in <> ")"
					<> " " <> go_abst parenBind parenApp body
				 _ ->
					"(" <> go_var_def x <> ":" <> go False False f_in <> ")"
					<> " -> "
					<> go False False body
					<> (if parenBind then ")" else "")
			 _ -> go parenBind parenApp te
		go_var_def x = if x == "" then "_" else build x

-- ** Type 'Sort'
-- | Four /PTS/ /sort constants/
-- are formed by combining
-- 'Type_Level' and 'Type_Morphism':
--
-- * @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
-- * @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
-- * @□m@: the 'Sort' to form the 'Type' of a monomorphic 'Type'.
-- * @□p@: the 'Sort' to form the 'Type' of a polymorphic 'Type'.
type Sort = (Type_Level, Type_Morphism)
instance Buildable Sort where
	build x = case x of
	 (sort, morphism) -> build sort <> build morphism

-- *** Type 'Type_Level'
data Type_Level
 =   Type_Level_0 -- ^ aka. /@*@ (Star) sort constant/.
 |   Type_Level_1 -- ^ aka. /@□@ (Box)  sort constant/.
 deriving (Eq, Ord, Show)
instance Buildable Type_Level where
	build x = case x of
	 Type_Level_0 -> "*"
	 Type_Level_1 -> "□"

-- | @*m@: the 'Sort' to form the 'Type' of a monomorphic 'Term'.
sort_star_mono :: Sort
sort_star_mono = (Type_Level_0, Type_Morphism_Mono)

-- | @*p@: the 'Sort' to form the 'Type' of a polymorphic 'Term'.
sort_star_poly :: Sort
sort_star_poly = (Type_Level_0, Type_Morphism_Poly)

-- *** Type 'Type_Morphism'
data Type_Morphism
 =   Type_Morphism_Mono
 |   Type_Morphism_Poly
 deriving (Eq, Ord, Show)
instance Buildable Type_Morphism where
	build x = case x of
	 Type_Morphism_Mono -> "" -- "m"
	 Type_Morphism_Poly -> "p"

-- * Type 'Axiom'

data family Axiom r

-- ** Class 'Axiomable'

-- | Instances of this class are 'Axiom's injectable in 'TeTy_Axiom', that is:
--
-- * they have a 'Type', given by 'axiom_type_of',
-- * and they can perform an optional reduction
--   within 'normalize' or 'whnf', given by 'axiom_normalize'.
class
 ( Eq ax, Show ax, Buildable ax, Typeable ax
 ) => Axiomable ax where
	axiom_type_of
	 :: forall var. Typeable var
	 => Context var -> ax -> Type var
	 -- ^ Return the 'Type' of the given 'Axiomable' instance.
	axiom_normalize
	 :: forall var. (Typeable var, Ord var, Variable var)
	 => Context var -> ax -> [Term var] -> Maybe (Term var, [Term var])
	 -- ^ Custom-'normalize': given a typing 'Context',
	 -- an 'Axiomable' instance
	 -- and a list of arguments, return:
	 --
	 -- * 'Nothing': if the axiom performs no reduction,
	 -- * 'Just': with the reducted 'Term' and the arguments not used by the reduction.
	 --
	 -- Default: @\\_ctx _ax _args -> Nothing@
	axiom_normalize _ctx _ax _args = Nothing
	axiom_eq :: ax -> (forall ax'. Axiomable ax' => ax' -> Bool)
	 -- ^ Custom-bipolymorphic-@(==)@:
	 -- given an 'Axiomable' instance
	 -- return a function to test if any
	 -- other 'Axiomable' instance
	 -- is equal to the first instance given.
	 --
	 -- Default: @maybe False (x ==) (cast y)@
	axiom_eq x y = maybe False (x ==) (cast y)

-- * Type 'Form'

-- | A record to keep a same 'Term' (or 'Type')
-- in several forms (and avoid to 'normalize' it multiple times).
data Form var
 =   Form
 {   form_given  :: Term var
 ,   form_normal :: Term var -- ^ 'normalize'-d version of 'form_given'.
 } deriving (Functor, Show)

-- * Type 'Context'

-- | Map variables of type @var@
-- to their 'Type' and maybe also to their 'Term',
-- both in 'form_given' and 'form_normal'.
data Context var
 =   Context
 {   context_vars   :: [var]
  -- ^ used to dump the 'Context'
 ,   context_lookup :: var -> Maybe (Context_Item var)
  -- ^ used to query the 'Context'
 ,   context_lift   :: Typeable var => Var_Name -> var
  -- ^ used to promote a ('Term' 'Var_Name') to ('Term' @var@)
 ,   context_unlift :: Typeable var => var -> Var_Name
  -- ^ used to unpromote ('Term' @var@) to ('Term' 'Var_Name')
 }
data Context_Item var
 =   Context_Item
 {   context_item_term :: Maybe (Form var)
 ,   context_item_type :: Form var
 } deriving (Functor, Show)

instance Show var => Show (Context var) where
	showsPrec n ctx@Context{context_vars=vars} =
		showParen (n > 10) $
		showString "Context " .
		showsPrec n ((\k ->
			(k, fromJust $ context_item_type
			 <$> context_lookup ctx k))
		 <$> vars) .
		showString " " .
		showsPrec n (catMaybes $ (\k ->
			(k,) . form_given <$>
			(context_item_term =<< context_lookup ctx k))
		 <$> vars)
instance Buildable var => Buildable (Context var) where
	build ctx@Context{context_vars=vars} =
		foldMap (\var ->
			"  " <> build var
			 <> maybe mempty (\ty -> " : " <> build (form_given ty))
				 (context_item_type <$> context_lookup ctx var)
			 {-
			 <> maybe mempty (\te -> " = " <> build (form_given te))
				 (context_item_term =<< context_lookup ctx var)
			 -}
			 <> "\n"
		 ) vars