Common.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
module Language.LOL.Typing.Expr.Common where

import qualified Data.Foldable as Foldable
import Data.Eq (Eq(..))
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Function (const)
import Data.Functor ((<$>))
import Data.Maybe (Maybe(..))
import Data.Text.Buildable (Buildable(..))

import qualified Language.LOL.Calculus as Calc
import Language.LOL.Typing.Type
import Text.Show

type Name = Text

data TeTy_Var
 =   TeTy_Var_Name Calc.Var_Name
 |   TeTy_Var_Monovar Monovar
 deriving (Eq, Show)
instance Buildable TeTy_Var where
	build x =
		case x of
		 TeTy_Var_Name n -> build n
		 TeTy_Var_Monovar v -> build (Monotype_Var v)

class Calc_Type a where
	calc_type :: a -> Calc.Type TeTy_Var
instance Calc_Type Monotype where
	calc_type ty =
		case app_spine_left ty of
		 Monotype_Var v `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Monovar v)
		 Monotype_Const c `App_Spine` [] -> Calc.TeTy_Var (TeTy_Var_Name c)
		 Monotype_Const "->" `App_Spine` [t1, t2] ->
			Calc.Type_Abst (Calc.Suggest "")
			 (calc_type t1)
			 (const Nothing `Calc.abstract` calc_type t2)
		 t `App_Spine` tys ->
			Calc.term_apps
			 (calc_type t)
			 (calc_type <$> tys)
calc_of_polytype
 :: Monoconsts
 -> Polytype
 -> (Monoconsts, Calc.Type TeTy_Var)
calc_of_polytype consts_used Quantification
	 { quantifiers
	 , quantifier_hintnames
	 , quantified } =
	Foldable.foldr
	 (\(quant, qname) ty ->
		let nam = Calc.Suggest qname in
		Calc.Type_Abst nam
		 (Calc.Type_Sort Calc.sort_star_mono)
		 ((\x -> case x of
			 TeTy_Var_Monovar v | v == quant-> Just nam
			 _ -> Nothing) `Calc.abstract` ty)
	 ) (calc_type quantified) <$>
	quantifiers_freshify consts_used quantifier_hintnames quantifiers
calc_abst_term_of_polytype
 :: Monoconsts
 -> Polytype
 -> Calc.Term TeTy_Var
 -> (Monoconsts, Calc.Type TeTy_Var)
calc_abst_term_of_polytype consts_used Quantification
	 { quantifiers
	 , quantifier_hintnames } term =
	Foldable.foldr
	 (\(quant, qname) ty ->
		let nam = Calc.Suggest qname in
		Calc.Term_Abst nam
		 (Calc.Type_Sort Calc.sort_star_mono)
		 ((\x -> case x of
			 TeTy_Var_Monovar v | v == quant -> Just nam
			 _ -> Nothing) `Calc.abstract` ty)
	 ) term <$>
	quantifiers_freshify consts_used quantifier_hintnames quantifiers
{-
instance (Show a, Substitutable a, Buildable (Quantification_Build_Options, a), Calc_Type a)
 => Calc_Type ([Monoconst], Forall a) where
	calc_type (consts_used, f@Quantification
	 { quantifiers
	 , quantifier_hintnames
	 , quantified }) =
		let (_consts_used, quants) = quantifiers_freshify consts_used quantifier_hintnames quantifiers in
		let qty = calc_type quantified in
		Foldable.foldr
		 (\(quant, qname) ty ->
			Calc.Type_Abst (Calc.Suggest qname)
			 (Calc.Type_Sort Calc.sort_star_mono)
			 ((\x ->
				case x of
				 TeTy_Var_Name _ -> Nothing
				 TeTy_Var_Monovar v ->
					if v == quant
					then Just (Calc.Suggest qname)
					else Nothing) `Calc.abstract` ty)
		 ) qty $
		trace ("quants: " <> Build.string (Build.list $ (\(x, y) -> Build.tuple [build x, build y]) <$> quants))
		trace ("forall: " <> Build.string (def::Quantification_Build_Options,f))
		trace ("forall: " <> show f)
		trace ("quantified: " <> show quantified)
		quants
-}
instance (Calc_Type a) => Calc_Type (Qualification [Class_Qualifier] a) where
	calc_type Qualification
	 { qualifiers
	 , qualified } =
		Foldable.foldr
		 (\(Class_Qualifier qname qty) ty ->
			Calc.Term_Abst (Calc.Suggest qname)
			 (calc_type qty)
			 ((\x -> case x of
				 TeTy_Var_Name n | Text.toLower n == qname -> Just (Calc.Suggest qname)
				 _ -> Nothing) `Calc.abstract` ty)
		 ) (calc_type qualified) qualifiers