{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# 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 #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.LOL.Calculus.Axiom where

import Data.Bool
import qualified Data.Char as Char
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($), (.), const)
import Data.Functor ((<$>))
import Data.List ((++))
import qualified Data.Map.Strict as Map
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid (Monoid(..), (<>))
import Data.Ord (Ord(..))
import Data.String (String)
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
import qualified Data.Text.Lazy as TL
import qualified Data.Text.Lazy.Builder as Builder
import Data.Typeable as Typeable
import Prelude (Int, Integer, Num(..), error)
import System.IO (IO)
import Text.Show (Show(..), showParen, showString)

import Language.LOL.Calculus.Abstraction
import Language.LOL.Calculus.Term
import Language.LOL.Calculus.Type
import Language.LOL.Calculus.Form


-- * Type 'Axiom'

-- data family Axiom r
-- deriving instance Typeable Axiom

axiom_cast :: (Typeable a, Typeable b) => Axiom a -> Maybe (Axiom b)
axiom_cast = cast

-- ** Type 'Axioms'
-- | 'Axioms' are made of 'Axiom's injected in regular 'Env_Item's,
-- see 'env_item_from_axiom'.
type Axioms = Env

env_item_from_axiom
 :: ( Axiomable (Axiom ax)
    , Typeable ax )
 => Context Var_Name -> Axiom ax -> Env_Item
env_item_from_axiom ctx ax =
	Env_Item
	 { env_item_term = form ctx $ TeTy_Axiom ax
	 , env_item_type = form ctx $ axiom_type_of ctx ax
	 }

-- ** Class 'Axiom_Type'

-- | A class to embed an Haskell-type within an 'Axiom'.
class Axiom_Type h where
	axiom_type :: Axiom h
	 -- ^ Construct (implicitely) an Haskell-term representing
	 -- the Haskell-type @h@.
	axiom_Type :: Axiom h -> Type Var_Name
	 -- ^ Return a 'Type' representing the Haskell-type @h@,
	 -- given through its representation as an Haskell-term
	 -- (which is an 'Axiom' and thus has itself a 'Type',
	 -- given by its 'axiom_type_of').

axiom_term
 :: (Axiom_Type h, Typeable h)
 => h -> Axiom (Axiom_Term h)
axiom_term (x::h) =
	Axiom_Term x $ \ctx ->
		context_lift ctx <$> axiom_Type (axiom_type::Axiom h)

-- ** Type 'Axiom_Type_Assume'
-- | An instance to use 'Type' as an 'Axiom'.
data Axiom_Type_Assume
newtype instance Axiom Axiom_Type_Assume
 =               Axiom_Type_Assume (Type Var_Name)
 deriving (Eq, Show)
instance Buildable (Axiom Axiom_Type_Assume) where
	build (Axiom_Type_Assume ty) = "(_:" <> build ty <> ")"
instance Axiomable (Axiom Axiom_Type_Assume) where
	axiom_type_of ctx (Axiom_Type_Assume ty) =
		context_lift ctx <$> ty

-- ** Type 'Axiom_MonoPoly'
-- | Non-'Sort' constants for /boxed parametric polymorphism/.
--
-- Used to embed /polymorphic types/ into first-class /monomorphic types/
-- via explicit injection ('Axiom_Term_MonoPoly_Box') and projection ('Axiom_Term_MonoPoly_UnBox') functions.
--
-- Special treatment of 'Axiom_MonoPoly' constructors is done in 'normalize' and 'whnf'
-- to remove adjacent pairs of 'Axiom_Term_MonoPoly_Box' / 'Axiom_Term_MonoPoly_UnBox'
-- or 'Axiom_Term_MonoPoly_UnBox' / 'Axiom_Term_MonoPoly_Box'.
--
-- __Ressources:__
--
-- * /Recasting MLF/, Didier Le Botlan, Didier Rémy, June 2009,
--   https://hal.inria.fr/inria-00156628
data Axiom_MonoPoly
data instance Axiom Axiom_MonoPoly
 =   Axiom_Type_MonoPoly
 |   Axiom_Term_MonoPoly_Box
 |   Axiom_Term_MonoPoly_UnBox
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Axiom_MonoPoly) where
	build ax = case ax of
	 Axiom_Type_MonoPoly       -> "Monotype"
	 Axiom_Term_MonoPoly_Box   -> "monotype"
	 Axiom_Term_MonoPoly_UnBox -> "polytype"
instance Axiomable (Axiom Axiom_MonoPoly) where
	axiom_type_of ctx ax =
		case ax of
		 Axiom_Type_MonoPoly ->
			 -- Monotype : *p -> *m
			Type_Abst "" (Type_Sort sort_star_poly) $
			(const Nothing `abstract`) $
			Type_Sort sort_star_mono
		 Axiom_Term_MonoPoly_Box ->
			 -- monotype : (Polytype : *p) -> Polytype -> Monotype Polytype
			(context_lift ctx <$>) $
			Type_Abst "Polytype" (Type_Sort sort_star_poly) $
			(("Polytype" =?) `abstract`) $
			Type_Abst "" (TeTy_Var "Polytype") $
			(("" =?) `abstract`) $
			TeTy_App
			 (TeTy_Axiom Axiom_Type_MonoPoly)
			 (TeTy_Var "Polytype")
		 Axiom_Term_MonoPoly_UnBox ->
			 -- polytype : (Polytype : *p) -> Monotype Polytype -> Polytype
			(context_lift ctx <$>) $
			Type_Abst "Polytype" (Type_Sort sort_star_poly) $
			(("Polytype" =?) `abstract`) $
			Type_Abst ""
			 (TeTy_App
				 (TeTy_Axiom Axiom_Type_MonoPoly)
				 (TeTy_Var "Polytype")) $
			 (("" =?) `abstract`) $
			TeTy_Var "Polytype"
	axiom_normalize _ctx
	 Axiom_Term_MonoPoly_UnBox
	 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_Box)) _ty') te:args)
	 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_UnBox / Axiom_Term_MonoPoly_Box
	 = Just (te, args)
	axiom_normalize _ctx
	 Axiom_Term_MonoPoly_Box
	 (_ty:TeTy_App (TeTy_App (TeTy_Axiom (axiom_cast -> Just Axiom_Term_MonoPoly_UnBox)) _ty') te:args)
	 -- NOTE: Remove adjacent Axiom_Term_MonoPoly_Box / Axiom_Term_MonoPoly_UnBox
	 = Just (te, args)
	axiom_normalize _ctx _ax _args = Nothing

-- | /PTS/ axioms for 'Axiom_MonoPoly':
--
-- * AXIOM: @⊦ Monotype : *p -> *m@
-- * AXIOM: @⊦ monotype : (Polytype : *p) -> Polytype -> Monotype Polytype@
-- * AXIOM: @⊦ polytype : (Polytype : *p) -> Monotype Polytype -> Polytype@
axioms_monopoly :: Axioms
axioms_monopoly =
	Map.fromList
	 [ ("Monotype", item Axiom_Type_MonoPoly)
	 , ("monotype", item Axiom_Term_MonoPoly_Box)
	 , ("polytype", item Axiom_Term_MonoPoly_UnBox)
	 ]
	where
	item = env_item_from_axiom ctx
	ctx = context_from_env mempty

-- ** Type 'Axiom_Term'

-- | Embed an Haskell-term of Haskell-type @h@ within an 'Axiom'
data Axiom_Term h
data instance Axiom (Axiom_Term h)
 = Typeable h
 => Axiom_Term h
               (forall var. Typeable var => Context var -> Type var)
 deriving (Typeable)

-- Instance 'Axiom' 'Integer'
data instance Axiom Integer
 = Axiom_Type_Integer
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Integer) where
	build Axiom_Type_Integer = "Int"
instance Axiomable (Axiom Integer) where
	axiom_type_of _ctx Axiom_Type_Integer =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type Integer where
	axiom_type = Axiom_Type_Integer
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term Integer)) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term Integer)) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term Integer)) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term Integer)) where
	build (Axiom_Term i _ty) = build i
instance Axiomable (Axiom (Axiom_Term Integer)) where
	axiom_type_of _ctx (Axiom_Term _ _ty) =
		TeTy_Axiom Axiom_Type_Integer

-- Instance 'Axiom' '()'
data instance Axiom ()
 = Axiom_Type_Unit
 deriving (Eq, Ord, Show)
instance Buildable (Axiom ()) where
	build Axiom_Type_Unit = "()"
instance Axiomable (Axiom ()) where
	axiom_type_of _ctx Axiom_Type_Unit =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type () where
	axiom_type = Axiom_Type_Unit
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term ())) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term ())) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term ())) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term ())) where
	build (Axiom_Term _te _ty) = "()"
instance Axiomable (Axiom (Axiom_Term ())) where
	axiom_type_of _ctx (Axiom_Term _te _ty) =
		TeTy_Axiom Axiom_Type_Unit

-- Instance 'Axiom' 'Text'
data instance Axiom Text
 = Axiom_Type_Text
 deriving (Eq, Ord, Show)
instance Buildable (Axiom Text) where
	build Axiom_Type_Text = "Text"
instance Axiomable (Axiom Text) where
	axiom_type_of _ctx Axiom_Type_Text =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance Axiom_Type Text where
	axiom_type = Axiom_Type_Text
	axiom_Type = TeTy_Axiom
instance Eq   (Axiom (Axiom_Term Text)) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord  (Axiom (Axiom_Term Text)) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term Text)) where
	showsPrec n (Axiom_Term te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showsPrec n te .
		showString " " .
		showsPrec n (ty context)
instance Buildable (Axiom (Axiom_Term Text)) where
	build (Axiom_Term t _) = build $ show t
instance Axiomable (Axiom (Axiom_Term Text)) where
	axiom_type_of _ctx (Axiom_Term _te _ty) =
		TeTy_Axiom Axiom_Type_Text

-- Instance 'Axiom' type variable

-- ** Type 'Axiom_Type_Var'

-- | Singleton type, whose constructors
-- are bijectively mapped to Haskell types
-- of kind 'Type_Var'.
data Axiom_Type_Var (v::Type_Var) where
 Axiom_Type_Var_Zero ::                     Axiom_Type_Var  'Type_Var_Zero
 Axiom_Type_Var_Succ :: Axiom_Type_Var v -> Axiom_Type_Var ('Type_Var_Succ v)
deriving instance Eq   (Axiom_Type_Var v)
deriving instance Ord  (Axiom_Type_Var v)
deriving instance Show (Axiom_Type_Var v)
deriving instance Typeable Axiom_Type_Var
instance Buildable (Axiom_Type_Var v) where
	build v = build $ type_var_string v

-- *** Type 'Type_Var'

-- | Natural numbers (aka. /Peano numbers/)
-- promoted by @DataKinds@ to Haskell type-level.
data Type_Var
 =   Type_Var_Zero
 |   Type_Var_Succ Type_Var
 deriving (Eq, Ord, Show, Typeable)

type A = Axiom_Type_Var 'Type_Var_Zero
type B = Axiom_Type_Var ('Type_Var_Succ 'Type_Var_Zero)
type C = Axiom_Type_Var ('Type_Var_Succ ('Type_Var_Succ 'Type_Var_Zero))
-- ^ …aliases only for the first few 'Axiom_Type_Var' used: extend on need.

-- | Return the Haskell term-level 'Int' encoded by the given Haskell type-level @(v :: 'Type_Var')@.
type_var_int :: Axiom_Type_Var v -> Int
type_var_int v =
	case v of
	 Axiom_Type_Var_Zero   -> 0
	 Axiom_Type_Var_Succ n -> 1 + type_var_int n

-- | Return a readable 'String' encoding the given Haskell type-level @(v :: 'Type_Var')@.
--
-- First 26 variables give: @\"A"@ to @\"Z"@,
-- and followings give: @(\"A" ++ show n)@, where @n@ is a positive 'Int' starting at @0@.
type_var_string :: Axiom_Type_Var v -> String
type_var_string v =
	case type_var_int v of
	 x | 0 <= x && x < 26 -> [Char.chr (Char.ord 'A' + x)]
	 x -> 'A' : show (x - 26)

-- *** Class 'Type_Var_Implicit'
class Type_Var_Implicit (v::Type_Var) where
	type_var :: Axiom_Type_Var v
instance Type_Var_Implicit 'Type_Var_Zero where
	type_var = Axiom_Type_Var_Zero
instance Type_Var_Implicit v => Type_Var_Implicit ('Type_Var_Succ v) where
	type_var = Axiom_Type_Var_Succ type_var

data instance Axiom (Axiom_Type_Var (v::Type_Var))
 =                   Axiom_Type_Var (Axiom_Type_Var v)
 deriving (Eq, Ord, Show)
instance Buildable (Axiom (Axiom_Type_Var (v::Type_Var))) where
	build (Axiom_Type_Var v) = build v
instance (Typeable v) => Axiomable (Axiom (Axiom_Type_Var (v::Type_Var))) where
	axiom_type_of _ctx (Axiom_Type_Var _v) =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)
instance Type_Var_Implicit v => Axiom_Type (Axiom_Type_Var (v::Type_Var)) where
	axiom_type = Axiom_Type_Var (type_var::Axiom_Type_Var v)
	axiom_Type (Axiom_Type_Var v) = TeTy_Var $ Text.pack $ type_var_string v

instance Eq (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	Axiom_Term x _ == Axiom_Term y _ = x == y
instance Ord (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	Axiom_Term x _ `compare` Axiom_Term y _ = x `compare` y
instance Show (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	showsPrec n (Axiom_Term v ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showParen (n > 10) (
			showString "Axiom_Type_Var " .
			showsPrec n v) .
		showString " " .
		showParen (n > 10) (
			showString " " .
			showsPrec n (ty context))
instance Buildable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	build (Axiom_Term v _ty) = build v
instance Typeable v => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var (v::Type_Var)))) where
	axiom_type_of ctx (Axiom_Term _ ty) = ty ctx

-- Instance 'Axiom' '->'
data instance Axiom (i -> o)
 =            Axiom_Term_Abst (Axiom i) (Axiom o)
deriving instance (Eq   (Axiom i), Eq   (Axiom o)) => Eq   (Axiom (i -> o))
deriving instance (Ord  (Axiom i), Ord  (Axiom o)) => Ord  (Axiom (i -> o))
deriving instance (Show (Axiom i), Show (Axiom o)) => Show (Axiom (i -> o))
instance (Buildable (Axiom i), Buildable (Axiom o)) => Buildable (Axiom (i -> o)) where
	build (Axiom_Term_Abst i o) =
		"(" <> build i <> " -> " <> build o <> ")"
instance
 ( Typeable i
 , Typeable o
 , Eq        (Axiom i)
 , Show      (Axiom i)
 , Buildable (Axiom i)
 , Eq        (Axiom o)
 , Show      (Axiom o)
 , Buildable (Axiom o)
 -- , Axiomable (Axiom i)
 -- , Axiomable (Axiom o)
 ) => Axiomable (Axiom (i -> o)) where
	axiom_type_of _ctx (Axiom_Term_Abst _i _o) =
		Type_Sort (Type_Level_0, Type_Morphism_Mono)

instance (Axiom_Type i, Axiom_Type o) => Axiom_Type (i -> o) where
	axiom_type =
		Axiom_Term_Abst
		 axiom_type
		 axiom_type
	axiom_Type (Axiom_Term_Abst i o) =
		Type_Abst ""
		(axiom_Type i) $
		(const Nothing `abstract`)
		(axiom_Type o)
instance Eq (Axiom (Axiom_Term (i -> o))) where
	(==) = error "Eq Axiom: (==) on functions"
instance Ord (Axiom (Axiom_Term (i -> o))) where
	compare = error "Eq Axiom: compare on functions"
instance
 {-( Buildable (Axiom (i -> o))
 ) =>-} Show (Axiom (Axiom_Term (i -> o))) where
	showsPrec n (Axiom_Term _ ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showString "(_:" .
		showString (
			Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ty context)
		 ) .
		showString ")"
instance
 {-( Buildable (Axiom i)
 , Buildable (Axiom o)
 ) =>-} Buildable (Axiom (Axiom_Term (i -> o))) where
	build (Axiom_Term _o ty) =
		"(_:" <> build (ty context) <> ")"

instance
 ( Typeable (Term var)
 , Typeable o
 , Axiomable (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (Term var))
 -- , Axiomable (Axiom o)
 -- , Buildable (Axiom (Term var))
 -- , Show (Axiom (Axiom_Term (Term var)))
 -- , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Term var -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize (ctx::Context var_)
	 {-ax@-}(Axiom_Term (cast -> Just (o::Term var_ -> o)) o_ty)
	 (arg:args) =
		{-
		trace ("axiom_normalize (i -> o): Term"
		 ++ "\n ax=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ax))
		 ++ "\n ax=" ++ show ax
		 ++ "\n ty(ax)=" ++ show (typeOf ax)
		 ++ "\n arg=" ++ show (context_unlift ctx <$> arg)
		 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
		 ++ "\n o=" ++ show (Axiom_Term (o arg) o_ty)
		 ) $
		-}
		case type_of ctx arg of
		 Right i_ty ->
			case o_ty ctx of
			 Type_Abst _ _o_in o_out ->
				let oi = o arg in
				let oi_ty = const i_ty `unabstract` o_out in
				Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
			 _ -> Nothing
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Term var -> io)
 , Typeable o
 , Typeable io
 , Axiomable (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (Term var -> io))
 -- , Axiomable (Axiom o)
 -- , Show (Axiom (Axiom_Term (Term var -> io)))
 -- , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term ((Term var -> io) -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize
	 (ctx::Context var_)
	 {-ax@-}(Axiom_Term (cast -> Just (o::(Term var_ -> io) -> o)) o_ty)
	 (arg@(Term_Abst _arg_v _arg_f_in arg_f):args) =
		case type_of ctx arg of
		 Right i_ty ->
			case o_ty ctx of
			 Type_Abst _ _o_in o_out ->
				{-
				trace ("axiom_normalize (i -> o): Term ->"
				 ++ "\n ax=" ++
					(Text.unpack $
					TL.toStrict $
					Builder.toLazyText $
					build (ax))
				 ++ "\n ax=" ++ show ax
				 ++ "\n args=" ++ show ((context_unlift ctx <$>) <$> args)
				 ++ "\n ty(args)=" ++ show (typeOf <$> args)
				 ++ "\n ty(ax)=" ++ show (typeOf ax)
				 ++ "\n i~" ++ show (typeOf (undefined::Term var -> io))
				 ++ "\n o~" ++ show (typeOf (undefined::o))
				 ++ "\n i=" ++ show (typeOf i)
				 ) $
				-}
				let i te =
					case normalize ctx (const te `unabstract` arg_f) of
					 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
					 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
				 in
				let oi = o i in
				let oi_ty = const i_ty `unabstract` o_out in
				Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
			 _ -> Nothing
		 _ -> Nothing
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): Term var -> io"
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Axiom_Type_Var v -> io)
 , Typeable o
 , Axiomable (Axiom (Axiom_Type_Var v -> io))
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (Axiom_Type_Var v -> io)))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term ((Axiom_Type_Var v -> io) -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx

instance
 ( Typeable Integer
 , Typeable o
 , Axiomable (Axiom Integer)
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term Integer))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Integer -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable Text
 , Typeable o
 , Axiomable (Axiom Text)
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term Text))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Text -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (Axiom_Type_Var v)
 , Typeable o
 , Axiomable (Axiom (Axiom_Type_Var v))
 , Axiomable (Axiom o)
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (Axiom_Type_Var v)))
 , Show (Axiom (Axiom_Term o))
 ) => Axiomable (Axiom (Axiom_Term (Axiom_Type_Var v -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (i -> o): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

instance
 ( Typeable (IO a)
 , Typeable o
 , Typeable a
 , Axiomable (Axiom (Axiom_Term o))
 , Show (Axiom (Axiom_Term (IO a)))
 , Show (Axiom (Axiom_Term o))
 -- , Axiomable (Axiom (IO a))
 -- , Axiomable (Axiom o)
 ) => Axiomable (Axiom (Axiom_Term (IO a -> o))) where
	axiom_type_of ctx (Axiom_Term _o ty) = ty ctx
	axiom_normalize ctx
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term i i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			{-
			trace ("axiom_normalize (Axiom_Term ((IO a) -> o)): "
			 ++ (
				Text.unpack $
				TL.toStrict $
				Builder.toLazyText $
				build (context_unlift ctx <$> oi_ty))
			 ) $
			-}
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize (ctx::Context var)
	 (Axiom_Term o o_ty)
	 (TeTy_Axiom (axiom_cast -> Just (Axiom_Term (i::IO (Term var)) i_ty)):args)
	 =
		case o_ty ctx of
		 Type_Abst _ _o_in o_out ->
			let oi = o $
				(\te ->
						case normalize ctx te of
						 TeTy_Axiom (axiom_cast -> Just (Axiom_Term io _io_ty)) -> io
						 _ -> error "axiom_normalize: Axiom_Term ((Term var -> io) -> o): cannot extract io"
				) <$> i in
			let oi_ty = const (i_ty ctx) `unabstract` o_out in
			Just (TeTy_Axiom $ Axiom_Term oi (context_relift ctx oi_ty), args)
		 _ -> Nothing
	axiom_normalize _ctx _ax _args = Nothing

-- ** Type 'Axiom_Type_Abst'

-- | Encode a @forall a.@ within an 'Axiom'.
data Axiom_Type_Abst
data instance Axiom Axiom_Type_Abst
 = Axiom_Type_Abst
   { axiom_type_abst_Var :: Suggest Var_Name
      -- ^ A name for the variable inhabiting the abstracting 'Type'.
   , axiom_type_abst_Term :: Type Var_Name -> Term Var_Name
      -- ^ The abstracted 'Term', abstracted by a 'Type'.
   , axiom_type_abst_Type :: Abstraction (Suggest Var_Name) Type Var_Name
      -- ^ The 'Type' of the abstracted 'Term'
      -- (not exactly a 'Type', but just enough to build it with 'Type_Abst').
   }
 deriving (Typeable)
instance Eq (Axiom Axiom_Type_Abst) where
	Axiom_Type_Abst{} == Axiom_Type_Abst{} =
		error "Eq Axiom_Type_Abst" -- maybe False (x ==) (cast y)
instance Show (Axiom Axiom_Type_Abst) where
	show Axiom_Type_Abst{} = "Axiom_Type_Abst"
instance Buildable (Axiom Axiom_Type_Abst) where
	build ax = "(_:" <> build (axiom_type_of context ax) <> ")"
instance Axiomable (Axiom Axiom_Type_Abst) where
	axiom_type_of ctx (Axiom_Type_Abst v _o ty) =
		Type_Abst v
		 (Type_Sort (Type_Level_0, Type_Morphism_Mono))
		 (context_lift ctx <$> ty)
	axiom_normalize ctx
	 {-ax@-}(Axiom_Type_Abst _ o ty)
	 (arg:args)
	 =
		let a = context_unlift ctx <$> arg in
		let ty_a = const a `unabstract` ty in
		let r = o ty_a in
		{-
		trace ("axiom_normalize: Axiom_Type_Abst:"
		 ++ "\n a=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (a)
			)
		 ++ "\n ty=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (axiom_type_of context ax)
			)
		 ++ "\n ty_a=" ++
			(Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ty_a)
			)
		 ++ "\n r=" ++
			(show r
			)
		 ) $
		-}
		Just (context_lift ctx <$> r, args)
	axiom_normalize _ctx _ax _args = Nothing

-- Instance 'Axiom' 'IO'
data instance Axiom (IO a)
 = Axiom_Type_IO
 deriving (Eq, Ord, Show)
instance Buildable (Axiom (IO a)) where
	build _ = "IO"
instance (Typeable a) => Axiomable (Axiom (IO a)) where
	axiom_type_of _ctx ax =
		case ax of
		 Axiom_Type_IO ->
			 -- IO : * -> *
			Type_Abst "" (Type_Sort sort_star_mono) $
			(const Nothing `abstract`) $
			Type_Sort sort_star_mono
	axiom_eq x y =
		maybe (
			case
			 ( Typeable.splitTyConApp (typeOf x)
			 , Typeable.splitTyConApp (typeOf y)
			 ) of
			 (  (xc,[Typeable.typeRepTyCon -> xc'])
			  , (yc,[Typeable.typeRepTyCon -> yc'])
			  ) | xc == yc && xc' == yc' -> True
			 _ ->
				error $ "Eq: Axiomable (Axiom (IO a)): "
				 ++ "\n x : " ++ show (Typeable.splitTyConApp (typeOf x))
				 ++ "\n y : " ++ show (Typeable.splitTyConApp (typeOf y))
		 ) (x ==) (cast y)

instance
 ( Typeable a
 , Axiom_Type a
 ) => Axiom_Type (IO a) where
	axiom_type = Axiom_Type_IO
	axiom_Type Axiom_Type_IO =
		TeTy_App
		(TeTy_Axiom (Axiom_Type_IO::Axiom (IO a)))
		(axiom_Type (axiom_type::Axiom a))

instance Eq (Axiom (Axiom_Term (IO a))) where
	(==) = error "Eq Axiom: (==) on IO"
instance Ord (Axiom (Axiom_Term (IO a))) where
	compare = error "Eq Axiom: compare on IO"
instance
 {-( Buildable (Axiom a)
 ) =>-} Show (Axiom (Axiom_Term (IO a))) where
	showsPrec n (Axiom_Term _te ty) =
		showParen (n > 10) $
		showString "Axiom_Term " .
		showString "(_:" .
		showString (
			Text.unpack $
			TL.toStrict $
			Builder.toLazyText $
			build (ty context)
		 ) .
		showString ")"
instance
 {-( Buildable (Axiom a)
 ) =>-} Buildable (Axiom (Axiom_Term (IO a))) where
	build (Axiom_Term _a ty) =
		"(_:" <> build (ty context) <> ")"
instance
 ( Typeable a
 -- , Buildable (Axiom a)
 -- , Axiomable (Axiom a)
 -- , Axiomable (Axiom (Axiom_Term a))
 ) => Axiomable (Axiom (Axiom_Term (IO a))) where
	axiom_type_of ctx (Axiom_Term _a ty) = ty ctx