Quantification.hs

{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Type.Quantification where

import Data.Bool
import Data.Eq (Eq)
import qualified Data.Foldable as Foldable
import Data.Function (($), (.))
import Data.Functor (Functor(..), (<$>))
import Data.Int (Int)
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Data.Maybe (Maybe(..), fromMaybe, maybeToList, isNothing)
import Data.Monoid (Monoid(..), (<>))
import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
import Data.Tuple (fst)
import Prelude (Num(..))
import Text.Read (read)
import Text.Show (Show(..))

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Substitution
import Language.LOL.Typing.Lib.Data.Default (Default(..))

-- * Type 'Quantification'

-- | 'Universal' and 'Existential' /quantification of 'Monotype's/.
--
-- A 'Quantification' is an abstract interpretation
-- of an expression that can be inlined in many places.
data Quantification quantification_type a
 =   Quantification
 { quantifiers :: [Quantifier]
   -- ^ /quantifying type variables/
 , quantifier_hintnames :: [Quantifier_Hinted]
   -- ^ original names used for some 'quantifiers'
   -- (likely to carry some meaning for a human)
 , quantified :: a
   -- ^ value upon which the 'Quantification' applies
 } deriving (Eq, Show)

-- | A type synonym indicating a /quantifying type variable/:
-- a /type variable/ bound by a 'Quantification'.
type Quantifier = Monovar

quantification :: a -> Quantification quantification_type a
quantification = Quantification mempty mempty

quantify
 :: Substitutable a
 => [Monovar] -> a
 -> Quantification qt a
quantify quantifiers quantified =
	Quantification
	 { quantifiers
	 , quantifier_hintnames = []
	 , quantified
	 }

quantify_rigvars
 :: Rigvarifiable a
 => [Rigvar] -> a
 -> Quantification qt a
quantify_rigvars quantifiers a =
	Quantification
	 { quantifiers
	 , quantifier_hintnames = []
	 , quantified = [ (v, Monotype_Var v) | v <- quantifiers ] `rigidvars_substitute` a
	 }

instance Functor (Quantification quantification_type) where
	fmap f q = q{quantified = f (quantified q)}
instance Substitutable a => Substitutable (Quantification quantification_type a) where
	-- | NOTE: the 'subvars' of a 'Quantification'
	-- do not include the 'quantifiers'.
	subvars q = subvars (quantified q) List.\\ quantifiers q
	sub `substitute` q = q{ quantified =
		substitution_domain_remove (quantifiers q) sub
		 `substitute` quantified q }
instance Has_Monotypes a => Has_Monotypes (Quantification quantification_type a) where
	monotypes = monotypes . quantified
	monotypes_map f q = q{ quantified = monotypes_map f $ quantified q }
{-
instance
 ( Buildable (Quantification_Build_Options, a)
 , Substitutable a
 ) => Buildable (Quantification q a) where
	build q = build ((def::Quantification_Build_Options), q)
-}

-- ** Type 'Quantifier_Freshname'

-- | A 'Quantifier_Name' for a 'Quantifier',
-- which is unique with respect to some 'Monoconst's.
type Quantifier_Freshname = (Quantifier, Quantifier_Name)
type Quantifier_Name = Monoconst
-- | A 'Quantifier_Name' for a 'Quantifier',
-- to be used as a hint to determine a 'Quantifier_Freshname'.
type Quantifier_Hinted = (Quantifier, Quantifier_Name)
-- | A 'Quantifier' without any hint
-- to determine a 'Quantifier_Freshname'.
type Quantifier_Hintless = Quantifier

-- | Return 'Quantifier_Freshname's
-- for given 'Quantifier's,
-- without using any of given 'Monoconst's.
quantifiers_freshify
 :: Monoconsts -- ^ 'Monoconst's already used.
 -> [Quantifier_Hinted] -- ^ Hints to use.
 -> [Quantifier] -- ^ 'Quantifier's to freshify.
 -> (Monoconsts, [Quantifier_Freshname]) -- ^ Fresh 'Quantifier_Name's, and 'Monoconst's now used.
quantifiers_freshify consts_used hints quants =
	quantifiers_hint_freshify consts_used $
	quantifiers_hint_partition hints quants

-- | Partition between 'Quantifier_Hinted' and 'Quantifier_Hintless'.
quantifiers_hint_partition
 :: [Quantifier_Hinted] -- ^ Hints to use.
 -> [Quantifier] -- ^ 'Quantifier's to partition.
 -> ([Quantifier_Hinted], [Quantifier_Hintless])
quantifiers_hint_partition hints =
	List.foldr (\q (yes, no) ->
		case List.lookup q hints of
		 Nothing -> (yes, q:no)
		 Just n -> ((q, n):yes, no))
	 mempty

-- | Return 'Quantifier_Freshname's
-- for given hinted and hintless 'Quantifier's,
-- without using any of given 'Monoconst's.
quantifiers_hint_freshify
 :: Monoconsts -- ^ 'Monoconst's already used.
 -> ([Quantifier_Hinted], [Quantifier_Hintless]) -- ^ 'Quantifier's to freshify.
 -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.
quantifiers_hint_freshify consts_used (quants_hinted, quants_hintless) =
	let (consts_used', quants_hinted_fresh) =
		quantifiers_freshify_hinted consts_used quants_hinted in
	let (consts_used'', quants_hintless_fresh) =
		quantifiers_freshify_hintless consts_used' quants_hintless in
	let quants_fresh = quants_hinted_fresh <> quants_hintless_fresh in
	(consts_used'', quants_fresh)

-- | Rename a bit any hinted 'Quantifier_Name'
-- in order to avoid capturing given 'Monoconst's:
-- by appending an increasing integer suffix
-- to any given 'Quantifier_Hinted' colliding.
quantifiers_freshify_hinted
 :: Monoconsts -- ^ 'Monoconst's already used.
 -> [Quantifier_Hinted] -- ^ 'Quantifier's to freshify.
 -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.
quantifiers_freshify_hinted monoconsts_used =
	List.foldr freshify (monoconsts_used, [])
	where
	freshify
	 :: (Quantifier, Quantifier_Name)
	 -> (Monoconsts, [Quantifier_Hinted])
	 -> (Monoconsts, [Quantifier_Freshname])
	freshify (q, name) (consts_used, qnames) =
		let ints = [1..] :: [Int] in
		let fresh_name =
			List.head
			 [ x
			 | extra <- "" : (show <$> ints)
			 , x <- [name <> Text.pack extra]
			 , isNothing (Map.lookup x consts_used)
			 ] in
		( Map.insert fresh_name () consts_used
		, (q, fresh_name):qnames )

quantifiers_freshify_hintless
 :: Monoconsts -- ^ 'Monoconst's already used.
 -> [Quantifier_Hintless] -- ^ 'Quantifier's to freshify.
 -> (Monoconsts, [Quantifier_Freshname]) -- ^ 'Monoconst's now used, and Fresh 'Quantifier_Name's.
quantifiers_freshify_hintless consts_used quants =
	let fresh_qnames = List.zip quants (const_pool List.\\ Map.keys consts_used) in
	let fresh_consts = Map.fromList $ (\(_, x) -> (x, ())) <$> fresh_qnames in
	( Map.union fresh_consts consts_used
	, fresh_qnames )

-- ** Type 'Quantification_Build_Options'

data Quantification_Build_Options
 =   Quantification_Build_Options
	 { quantification_build_option_consts_used :: Monoconsts
	   -- ^ The context of 'Monoconst's not to be captured
	   -- by the 'quantifiers' to output.
	 , quantification_build_option_force_var_names :: Bool
	   -- ^ Output 'quantifiers' like other 'subvars'
	   -- instead of using 'quantifier_hintnames' and 'const_pool'.
	 , quantification_build_option_show_toplevel_quantifiers :: Bool
	   -- ^ Output a declaration for the 'quantifiers',
	   --
	   -- Example: @forall a b.@
	   --
	   -- Example: @exists a b.@
	 , quantification_build_option_use_hints :: Bool
	   -- ^ Whether to use 'quantifier_hintnames'
	   -- to output the 'quantifiers'.
	 , quantification_build_option_var_prefix :: Text
	   -- ^ A prefix for 'subvars' which are not 'quantifiers'.
	 }

instance Default Quantification_Build_Options where
	def =
		Quantification_Build_Options
		 { quantification_build_option_consts_used               = mempty
		 , quantification_build_option_force_var_names           = False
		 , quantification_build_option_show_toplevel_quantifiers = True
		 , quantification_build_option_use_hints                 = True
		 , quantification_build_option_var_prefix                = "m"
		 }
instance Buildable (Quantification_Build_Options, Monotype) where
	build (_opts, ty) = build ty
instance
 ( Buildable (Quantification_Build_Options, a)
 , Buildable (Proxy qt)
 , Substitutable a
 ) => Buildable (Quantification_Build_Options, Quantification qt a) where
	build
	 ( opts@Quantification_Build_Options
		 { quantification_build_option_consts_used
		 , quantification_build_option_force_var_names
		 , quantification_build_option_show_toplevel_quantifiers
		 , quantification_build_option_use_hints
		 , quantification_build_option_var_prefix
		 }
	 , Quantification
		 { quantifiers
		 , quantifier_hintnames
		 , quantified
		 } ) =
		let subvas = subvars quantified in
		let quants = quantifiers `List.intersect` subvas in
		 -- NOTE: hide unused 'quantifiers'.
		let (consts_used, freshnames_quanted) =
			if quantification_build_option_force_var_names
			then (quantification_build_option_consts_used, [])
			else
				quantifiers_hint_freshify
				 quantification_build_option_consts_used $
					if quantification_build_option_use_hints
					then quantifiers_hint_partition quantifier_hintnames quants
					else ([], quants) in
		let freshnames_quantless =
			(\v -> -- NOTE: find a name for the non-quantifying substitutable 'Monovar's.
				(v, quantification_build_option_var_prefix <> Text.pack (show v))
			 ) <$> (subvas List.\\ (fst <$> freshnames_quanted)) in
		let freshsub = substitution_finite $
			(Monotype_Const <$>) <$> (freshnames_quanted <> freshnames_quantless) in
		(if quantification_build_option_show_toplevel_quantifiers
		&& not (Foldable.null quants)
		then build_declaration $ (freshsub `substitute`) . Monotype_Var <$> quants
		else "") <>
		build
		 ( opts
			 { quantification_build_option_consts_used = consts_used
			 , quantification_build_option_show_toplevel_quantifiers = True
			 }
		 , freshsub `substitute` quantified
		 )
		where
		build_declaration quants =
			build (Proxy::Proxy qt) <> " " <>
			mconcat (List.intersperse " " $ build <$> quants) <> ". "

-- ** Type 'Unquantification'

data Unquantification a
 =   Unquantification
 {   unquantification_freshvar :: Freshvar
     -- ^ The given 'Freshvar'
     -- usable for the next fresh 'Monovar' (or 'Rigvar'),
     -- incremented by one for each fresh 'Monovar' (or 'Rigvar's)
     -- as needed by 'unquantify'.
 ,   unquantified :: a
     -- ^ The given 'quantified' value with the 'quantifiers'
     -- replaced by fresh 'Monovar's (or 'Rigvar's).
 }

-- | Type synonym to signify that a 'Monovar' is used as a counter.
type Freshvar = Monovar

-- | Perform a /type variable unabstraction/ (aka. /type variable instantiation/).
--
-- Return the 'quantified' value of the given 'Quantification'
-- with its 'quantifiers' 'substitute'd
-- by 'Monovar's counting from given 'Monovar'
-- and applied to given 'Monotype' injection,
-- along with the 'Freshvar' incremented as needed.
unquantify
 :: Substitutable a
 => (Freshvar -> Monotype)
 -> Freshvar
 -> Quantification qt a
 -> Unquantification a
unquantify monoty freshvar
 Quantification{quantifiers, quantified} =
	Unquantification
	 { unquantification_freshvar = freshvar + List.length quantifiers
	 , unquantified              = sub `substitute` quantified
	 }
	where
	sub = substitution_finite $
		List.zip quantifiers (monoty <$> [freshvar..])

-- ** Type 'Universal'

data Universal
type Forall = Quantification Universal

instance Show (Proxy Universal) where
	show _ = "Universal"
instance Buildable (Proxy Universal) where
	build _ = "forall"

-- | /Generalize/ a 'Monotype' to a 'Polytype',
-- 'quantify'ing all its 'subvars'.
for_all :: Substitutable a => a -> Forall a
for_all a = quantify (subvars a) a

-- | /Generalize/ a 'Monotype' to a 'Polytype',
-- 'quantify'ing its 'subvars' which are within given 'Monovar's.
forall_in :: Substitutable a => [Monovar] -> a -> Forall a
forall_in quants a = quantify (quants `List.intersect` subvars a) a

-- | /Generalize/ a 'Monotype' to a 'Polytype'
-- 'quantify'ing all its 'subvars'
-- except those within given 'Monovar's.
forall_but
 :: Substitutable a
 => [Monovar] -> a -> Forall a
forall_but vars_mono a = forall_in (subvars a List.\\ vars_mono) a

-- | 'unquantify' a 'Forall' with fresh 'Monovar's.
unquantify_forall
 :: Substitutable a
 => Freshvar -> Forall a
 -> Unquantification a
unquantify_forall = unquantify Monotype_Var

-- ** Type 'Existential'

data Existential
type Exists = Quantification Existential

instance Show (Proxy Existential) where
	show _ = "Existential"
instance Buildable (Proxy Existential) where
	build _ = "exists"

exists :: Rigvarifiable a => a -> Exists a
exists a = quantify_rigvars (rigidvars a) a

unquantify_exists
 :: Substitutable a
 => Rigvar -> Exists a
 -> Unquantification a
unquantify_exists = unquantify (Monotype_Const . monoconst_from_rigvar)

reveal
 :: Substitutable a
 => Freshvar -> Exists a
 -> Unquantification a
reveal = unquantify Monotype_Var

unreveal :: Substitutable a => [Monovar] -> a -> Exists a
unreveal vars a = quantify (vars `List.intersect` subvars a) a

-- * Type 'Rigvar'

-- | A /rigid type variable/ (aka. /skolem constant/, named after Thoralf Skolem)
-- is a 'Monovar' bound by a 'Quantification'
-- outside the current /typing context/
-- (therefore a 'Rigvar' cannot be unified with an other 'Monovar').
--
-- Intuitionally, a 'Rigvar' represents a /fixed unknown 'Monotype'/.
type Rigvar = Monovar

-- | 'Monotype' which must remain monomorphic,
-- used to form the current /typing context/.
type Rigtype = Monotype

-- | A /rigvarification/ is a special form of 'unquantify'cation
-- in which the 'quantifiers' are replaced by fresh 'Rigvar's:
-- these are 'Monoconst's that do not appear elsewhere.
--
-- NOTE: 'rigconstify'ing a 'Forall' 'Quantification'
-- is an implementation technique
-- used to ensure that no assumption can be made
-- about certain 'Monovar's.
rigconstify
 :: Substitutable a
 => Freshvar -> Forall a
 -> Unquantification a
rigconstify  = unquantify (Monotype_Const . monoconst_from_rigvar)

unrigconstify :: Rigvarifiable a => a -> Forall a
unrigconstify a = quantify_rigvars (rigidvars a) a

-- | A prefix to single out 'Rigvar's from other 'Monoconst's.
rigvar_prefix :: Text
rigvar_prefix = "_"

monoconst_from_rigvar :: Rigvar -> Monoconst
monoconst_from_rigvar = (rigvar_prefix <>) . Text.pack . show

rigvar_from_monoconst :: Monoconst -> Maybe Rigvar
rigvar_from_monoconst c
 | rigvar_prefix `Text.isPrefixOf` c =
	Just $ read $ Text.unpack $
	Text.drop (Text.length rigvar_prefix) c
 | otherwise = Nothing

-- | Return the given 'Substitutable' value
-- with its 'subvars' mapped to 'Monotype_Const'.
constify_subvars :: Substitutable a => a -> a
constify_subvars a = sub `substitute` a
	where
	sub =
		substitution_finite
		 [ (v, Monotype_Const $ monoconst_from_rigvar v)
		 | v <- subvars a
		 ]

-- ** Type 'Rigvar_Substitution'

type Rigvar_Substitution = [(Rigvar, Monotype)]

-- ** Class 'Rigvarifiable'

-- | Like 'Substitutable', but acting on 'Rigvar's.
class Rigvarifiable a where
	rigidvars :: a -> [Rigvar]
	rigidvars_substitute :: Rigvar_Substitution -> a -> a

instance Rigvarifiable Monotype where
	rigidvars monoty =
		case monoty of
		 Monotype_Var _   -> []
		 Monotype_Const c -> maybeToList $ rigvar_from_monoconst c
		 Monotype_App l r -> rigidvars l `List.union` rigidvars r
	
	rigidvars_substitute rsub monoty =
		case monoty of
		 Monotype_Var _ -> monoty
		 Monotype_Const c ->
			fromMaybe monoty $ do
				rig <- rigvar_from_monoconst c
				rig `List.lookup` rsub
		 Monotype_App l r ->
			Monotype_App
			 (rsub `rigidvars_substitute` l)
			 (rsub `rigidvars_substitute` r)
instance Rigvarifiable a => Rigvarifiable [a] where
	rigidvars = List.foldr (List.union . rigidvars) []
	rigidvars_substitute rsub = ((rsub `rigidvars_substitute`) <$>)