-- vim: syntax=haskell
optpragmas {
{-# LANGUAGE OverloadedStrings #-}
}
module {Language.LOL.Typing.Collect.Grammar} {} {
import Data.Function (($))
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid (Monoid(..), (<>))
import Data.Sequence (Seq, (|>), (<|), (><))
import qualified Data.Sequence as Seq
import Prelude (Num(..))

import Language.LOL.Typing.Collect.Constraint
import Language.LOL.Typing.Type
import Language.LOL.Typing.Expr
import Language.LOL.Typing.Lib.Data.Default (Default(..))
import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build
}

include "../Expr/Grammar.ag"

attr Expr
	-- | top-down
	inh polytys :: Collect_Context
	-- | bottom-up
	syn monovar :: Monovar
	syn constraints :: {Seq Collect_Constraint}
	syn errors use {<>} {[]} :: {[Collect_Error_Grammar]}
	-- | both
	chn freshvar :: Freshvar
attr Decl
	-- | top-down
	inh polytys :: Collect_Context
	-- | bottom-up
	syn polyvar :: Polyvar
	syn constraints :: {Seq Collect_Constraint}
	syn errors use {<>} {[]} :: {[Collect_Error_Grammar]}
	-- | both
	chn freshvar :: Freshvar

sem Expr
 | Annot
	lhs.constraints = @body.constraints |>
	                  ((@sig `generalized_by` @body.monovar) @lhs.polytys $
	                   Collect_Info_Grammar_Expr $ "Annot " <> Build.text
	                    (def::Quantification_Build_Options, @sig))
 | Var
	lhs.monovar     = @loc.monovar
	loc.monovar     = @lhs.freshvar
	lhs.freshvar    = @lhs.freshvar + 1
	loc.polyty      = context_lookup @name @lhs.polytys
	-- loc.term        = TeTy_Var_Unknown @name @loc.monovar
	lhs.constraints = case @loc.polyty of
	                   Nothing -> mempty
	                   Just p -> Seq.singleton $
	                              p `instantiates_to` @loc.monovar $
	                               Collect_Info_Grammar_Expr $ "Var " <> @name
	lhs.errors = case @loc.polyty of
	              Nothing -> [Collect_Error_Grammar_Variable_not_in_scope @name]
	              Just _  -> []
 | Abst
	lhs.monovar     = @loc.monovar
	loc.monovar     = @lhs.freshvar
	loc.arg_monovar = @lhs.freshvar + 1
	body.freshvar   = @lhs.freshvar + 2
	body.polytys    = (@name `context_insert` Monotype_Var @loc.arg_monovar) @lhs.polytys
	lhs.constraints = (@loc.monovar `unifies_with`
	                    (Monotype_Var @loc.arg_monovar .->. Monotype_Var @body.monovar) $
	                    Collect_Info_Grammar_Expr $ "Abst(body) " <> @name) <|
	                  maybe mempty (\sig -> Seq.singleton ((sig `unifies_with` @loc.arg_monovar) $
	                   Collect_Info_Grammar_Expr $ "Abst(sig) " <> Build.text sig)) @sig ><
	                  @body.constraints
 | App
	lhs.monovar     = @loc.monovar
	loc.monovar     = @lhs.freshvar
	abst.freshvar   = @lhs.freshvar + 1
	abst.polytys    = @lhs.polytys
	arg.polytys     = @lhs.polytys
	lhs.constraints = @abst.constraints <>
	                  @arg.constraints |>
	                  (@abst.monovar `unifies_with`
	                    (Monotype_Var @arg.monovar .->. Monotype_Var @loc.monovar) $
	                    Collect_Info_Grammar_Expr $ "App")
 | Let
	lhs.monovar      = @loc.monovar
	loc.monovar      = @lhs.freshvar
	loc.decl_polyvar = @lhs.freshvar + 1
	decl.freshvar    = @lhs.freshvar + 2
	decl.polytys     = @lhs.polytys
	body.polytys     = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys
	lhs.constraints  = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in
	                   @decl.constraints ><
	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar)
	                    @lhs.polytys (info "decl") <|
	                   maybe mempty (\sig -> Seq.singleton
	                    ((sig `generalized_by` @decl.monovar) @lhs.polytys $
	                    Collect_Info_Grammar_Expr $ "Let(sig) " <>
	                    Build.text (def::Quantification_Build_Options, sig))) @sig ><
	                   (@loc.monovar `unifies_with` @body.monovar) (info "body") <|
	                   @body.constraints
 | Where
	lhs.monovar      = @loc.monovar
	loc.monovar      = @lhs.freshvar
	loc.decl_polyvar = @lhs.freshvar + 1
	body.freshvar    = @lhs.freshvar + 2
	decl.polytys     = @lhs.polytys
	body.polytys     = (@name `context_insert` @loc.decl_polyvar) @lhs.polytys
	lhs.constraints  = let info = Collect_Info_Grammar_Expr $ "Where " <> @name in
	                   @decl.constraints ><
	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys info <|
	                   maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $
	                    Collect_Info_Grammar_Expr $ "Where(sig) " <> Build.text
	                     (def::Quantification_Build_Options, sig))) @sig ><
	                   (@loc.monovar `unifies_with` @body.monovar) info <|
	                   @body.constraints

sem Decl
 | Let
	-- loc.monovar      = Monotype_Var @lhs.freshvar
	loc.decl_polyvar = @lhs.freshvar
	decl.freshvar    = @lhs.freshvar + 1
	decl.polytys     = @lhs.polytys
	lhs.polyvar      = @loc.decl_polyvar
	lhs.constraints  = let info x = Collect_Info_Grammar_Expr $ "Let" <> "(" <> x <> ") " <> @name in
	                   @decl.constraints ><
	                   (@loc.decl_polyvar `generalizes_from` @decl.monovar) @lhs.polytys (info "decl") <|
	                   maybe mempty (\sig -> Seq.singleton ((sig `generalized_by` @decl.monovar) @lhs.polytys $
	                    Collect_Info_Grammar_Expr $ "Let(sig) " <> Build.text
	                     (def::Quantification_Build_Options, sig))) @sig