content: {-# LANGUAGE FlexibleContexts, NamedFieldPuns, OverlappingInstances,
               QuasiQuotes, RankNTypes, RecordWildCards, TemplateHaskell,
               ViewPatterns, DeriveGeneric #-}
  
  module Forml.Types.Type where
  
  import Control.Applicative
  
  import Text.InterpolatedString.Perl6
  import Text.Parsec        hiding (State, label, many, parse, spaces, (<|>))
  import Text.Parsec.Indent hiding (same)
  
  import qualified Data.Map as M
  import qualified Data.Set as S
  
  import Forml.Parser.Utils
  import Forml.Types.Symbol
  
  import Data.Serialize
  
  import GHC.Generics
  
  data UnionType = UnionType (S.Set ComplexType)
                 deriving (Ord, Eq, Generic)
  
  data ComplexType = RecordType (M.Map Symbol UnionType)
                   | InheritType SimpleType (M.Map Symbol UnionType)
                   | FunctionType UnionType UnionType
                   | SimpleType SimpleType
                   deriving (Eq, Ord, Generic)
  
  data SimpleType = PolymorphicType SimpleType [UnionType]
                  | SymbolType Symbol
                  | VariableType String
                  deriving (Ord, Eq, Generic)
  
  instance Serialize SimpleType
  instance Serialize UnionType
  instance Serialize ComplexType
  
  instance Show UnionType where
      show (UnionType xs)         = [qq|{sep_with " | " $ S.toList xs}|]
  
  instance Show ComplexType where
      show (SimpleType y)         = [qq|$y|]
      show (InheritType n m)      = [qq|\{ $n with {unsep_with ": " m} \}|]
      show (RecordType m)         = [qq|\{ {unsep_with ": " m} \}|]
  
      show (FunctionType g @ (UnionType (S.toList -> ((FunctionType _ _):[]))) h) =
          [qq|($g -> $h)|]
  
      show (FunctionType g h)     = [qq|$g -> $h|]
  
  instance Show SimpleType where
      show (PolymorphicType x y)  = [qq|($x {sep_with " " y})|]
      show (SymbolType x)   = show x
      show (VariableType x) = x
  
  
  
  -- Type Signatures
  -- -----------------------------------------------------------------------------
  -- TODO ! (IO type)
  -- TODO type axioms need nominative types?
  -- ? TODO List, Map, Set shorthand?
  
  -- The type algebra of Sonnet is broken into 3 types to preserve the
  -- associativity of UnionTypes: (x | y) | z == x | y | z
  
  
  
  -- Where a type signature may be used in Sonnet had two slightly different parsers
  -- in order to allow for somewhat overloaded surrounding characters (eg "|" - when
  -- declaring the type of an axiom, one must be careful to disambiguate UnionTypes
  -- and sets of EqualityAxioms).  However, these types are otherwise equivalent,
  -- and any type that may be declared in a TypeDefinition may also be the explicit
  -- type of a Definition (Note, however, that in the case of NamedTypes, the
  -- names introduced into scope will be inaccessible in the case of a Definition).
  
  
  type_axiom_signature      :: Parser UnionType
  type_definition_signature :: Parser UnionType
  
  type_axiom_signature = do option "" (string "|" <* whitespace)
                            t <- (u $ try function_type) <|> try nested_union_type <|> u inner_type
                            whitespace
                            return t
  
      where u = (<$>) $ UnionType . S.fromList . (:[])
  
  type_definition_signature = UnionType . S.fromList <$> types <* whitespace
      where types = (try function_type <|> inner_type) `sepBy1` type_sep
  
  
  -- Through various complexities of the recursive structure of these types, we will
  -- need a few mutually recursive parsers to express these slightly different
  -- signature parsers.
  
  inner_type        :: Parser ComplexType
  nested_function   :: Parser ComplexType
  nested_union_type :: Parser UnionType
  
  inner_type  = nested_function
                <|> try record_type
                <|> try named_type
                <|> try poly_type
                <|> var_type
                <|> symbol_type
  
  nested_function   = indentPairs "(" (try function_type <|> inner_type) ")"
  nested_union_type = indentPairs "(" type_definition_signature ")"
  
  
  -- Now that we've expressed the possible parses of a UnionType, we can move on to
  -- parsing the ComplexType and SimpleType layers.  While these are also mutually
  -- recursive, the recursion is uniform, as the various allowable combinations
  -- have already been defined above.
  
  function_type :: Parser ComplexType
  poly_type     :: Parser ComplexType
  record_type   :: Parser ComplexType
  named_type    :: Parser ComplexType
  symbol_type   :: Parser ComplexType
  var_type      :: Parser ComplexType
  
  function_type = do x <- try nested_union_type <|> unionize inner_type
                     spaces
                     string "->" <|> string "→"
                     spaces
                     y <- (unionize $ try function_type) <|> try nested_union_type <|> unionize inner_type
                     return $ FunctionType x y
  
  poly_type = do name <- (SymbolType <$> type_name) <|> (VariableType <$> try type_var)
                 whitespace
                 SimpleType . PolymorphicType name <$> (j_style <|> h_style)
  
       where rvs = record_type <|> var_type <|> symbol_type
             h_style = (try nested_union_type <|> unionize (try rvs)) `sepEndBy1` whitespace
             j_style = indentPairs "<" ((try nested_union_type <|> unionize (try rvs)) `sepBy1` optional_sep) ">"
  
  record_type   = let key_value = (,) <$> syntax <* div' <*> type_definition_signature
                      div'      = spaces <* string ":" <* spaces
                      pairs     = key_value `sepEndBy` optional_sep
                      inner     = RecordType . M.fromList <$> pairs
                      inherit   = do SimpleType n <- try poly_type <|> try symbol_type <|> var_type
                                     spaces
                                     indented
                                     string "with"
                                     spaces *> indented
                                     InheritType n . M.fromList <$> pairs
  
                  in indentPairs "{" (try inherit <|> inner) "}"
  
  named_type = do x <- indentPairs "{" name "}"
  
  -- named_type = do x <- name
  --                 y <- option bool (try nested_union_type <|> unionize inner_type)
  
                  return $ RecordType (M.fromList [(Symbol x, bool)])
  
      where name = type_var
            bool = UnionType (S.fromList [(SimpleType (SymbolType (Symbol "Bool")))])
  
  symbol_type   = SimpleType . SymbolType <$> type_name
  var_type      = SimpleType . VariableType <$> type_var
  
  unionize :: Parser ComplexType -> Parser UnionType
  unionize = fmap $ UnionType . S.fromList . (:[])
  
  
  type_name   :: Parser Symbol
  type_var    :: Parser String
  
  type_name   = Symbol <$> not_reserved (upper <:> many (alphaNum <|> oneOf "_'"))
  
  type_var    = 
      not_reserved (oneOf "_abscdefghijklmnopqrstuvwxyz" <:> many (alphaNum <|> oneOf "_'")) >>= f
      
      where f "_" = do x <- getPosition
                       return $ "_" ++ show (sourceLine x * sourceColumn x)
            f x   = return x
  
  
  