Calculus.ag

-- vim: syntax=haskell
optpragmas {
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -fno-warn-unused-matches #-}
}
module {Language.LOL.Typing.Expr.Calculus} {} {
import Data.Function (($))
import Data.Eq (Eq(..))
import Data.Maybe (Maybe(..), fromMaybe)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Prelude (Num(..), error)
import Data.Tuple (fst, snd)
import qualified Data.Foldable as Foldable


import Language.LOL.Typing.Type
import Language.LOL.Typing.Expr.Common
import Language.LOL.Typing.Expr.Grammar
-- import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build
import qualified Language.LOL.Calculus as Calc
import Data.Monoid ((<>))
import Text.Show (show)
-- import Debug.Trace
}

include "./Grammar.ag"

attr Expr Decl
	-- | top-down
	inh env :: {Calc.Env}
	inh monoconsts :: Monoconsts
	 -- ^ The 'Monoconst's
	 -- bound at the current node.
	inh monotys :: Substitution_Fixpoint
	 -- ^ The inferred 'Monotype's.
	inh polytys :: Polysub
	 -- ^ The inferred 'Polytype's.
	inh quantifiers :: {Map Monovar [Monotype]}
	 -- ^ The 'Monotype's (fully inferred)
	 -- which have been introduced when a 'Polytype'
	 -- has been instanciated to a 'Monovar',
	 -- and thus must be passed to the 'Expr_Var' derived from it.
	inh renames :: {Map Name Name}
	 -- ^ Used to accumulate 'Name's
	 -- bound at the current node
	 -- but conflicting with 'monoconsts_Inh_Expr',
	 -- and thus requiring a rename
	 -- at their corresponding 'Expr_Var' nodes;
	 -- this rename is important because 'quantifiers_Inh_Expr'
	 -- may introduce 'Monoconst's of 'monoconsts_Inh_Expr'.
	
	-- | bottom-up
	syn monovar :: Monovar
	syn term :: {Calc.Term TeTy_Var}
	
	-- | both
	chn freshvar :: Freshvar

sem Expr
 | Annot
 | Var
	lhs.monovar  = @loc.monovar
	loc.monovar  = @lhs.freshvar
	lhs.freshvar = @lhs.freshvar + 1
	loc.name     = Map.findWithDefault @name @name @lhs.renames
	lhs.term     = {-
	               let ty = @lhs.monotys `substitute` Monotype_Var @loc.monovar in
	               let fv = subvars ty in
	               trace ("trace: Var m"<>show @loc.monovar<>
	                " name="<>show @loc.name<>
	                " : "<>Build.string ty<>
	                " ~> "<>show (Build.list <$> Map.lookup @loc.monovar @lhs.quantifiers)) $
	               -}
	               Foldable.foldl
	                (\acc mty -> Calc.TeTy_App acc
	                 (calc_type mty))
	                (Calc.TeTy_Var (TeTy_Var_Name @loc.name))
	                (Map.findWithDefault [] @loc.monovar @lhs.quantifiers)
	               {-case Map.lookup @loc.monovar @lhs.quantifiers of
	                Nothing -> Calc.TeTy_Var (TeTy_Var_Name @name)
	                Just quants ->
	                  Foldable.foldl
	                   (\acc quant -> Calc.TeTy_App acc
	                    (calc_type $ @lhs.monotys `substitute` Monotype_Var quant))
	                   (Calc.TeTy_Var (TeTy_Var_Name @name))
	                   quants-}
 | Abst
	lhs.monovar     = @loc.monovar
	loc.monovar     = @lhs.freshvar
	loc.arg_monovar = @lhs.freshvar + 1
	body.freshvar   = @lhs.freshvar + 2
	loc.consts_name = const_freshify @lhs.monoconsts @name
	body.monoconsts = fst @loc.consts_name
	body.renames    = if @name == snd @loc.consts_name
	                  then @lhs.renames
	                  else Map.insert @name (snd @loc.consts_name) @lhs.renames
	loc.term        = Calc.Term_Abst (Calc.Suggest $ snd @loc.consts_name)
	                   (calc_type $ @lhs.monotys `substitute`
	                                Monotype_Var @loc.arg_monovar) $ -- TODO: cache calc_type
	                   (\v -> case v of
	                    TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n)
	                    _ -> Nothing) `Calc.abstract` @body.term
 | App
	lhs.monovar     = @loc.monovar
	loc.monovar     = @lhs.freshvar
	abst.freshvar   = @lhs.freshvar + 1
	lhs.term        = Calc.TeTy_App @abst.term @arg.term
 | Let
	lhs.monovar      = @loc.monovar
	loc.monovar      = @lhs.freshvar
	loc.decl_polyvar = @lhs.freshvar + 1
	decl.freshvar    = @lhs.freshvar + 2
	loc.consts_name  = const_freshify @lhs.monoconsts @name
	body.renames     = if @name == snd @loc.consts_name
	                   then @lhs.renames
	                   else Map.insert @name (snd @loc.consts_name) @lhs.renames
	loc.decl_polyty  = fromMaybe (error $ "Oops, Polytype missing " <> show @loc.decl_polyvar <> " in " <> show @lhs.polytys) $
	                   Map.lookup @loc.decl_polyvar @lhs.polytys
	loc.decl_quants  = quantifiers_freshify @lhs.monoconsts
	                                        (quantifier_hintnames @loc.decl_polyty)
	                                        (quantifiers          @loc.decl_polyty)
	decl.monoconsts  = fst @loc.decl_quants
	body.monoconsts  = fst @loc.consts_name
	lhs.term         = Calc.TeTy_App
	                    (Calc.Term_Abst
	                     (Calc.Suggest $ snd @loc.consts_name)
	                     (Foldable.foldr
	                       (\(quant, qname) ty ->
	                        let nam = Calc.Suggest qname in
	                        Calc.Type_Abst nam
	                         (Calc.Type_Sort Calc.sort_star_mono)
	                         ((\v -> case v of
	                           TeTy_Var_Monovar m | m == quant -> Just nam
	                           _ -> Nothing) `Calc.abstract` ty))
	                       (calc_type (quantified @loc.decl_polyty))
	                       (snd @loc.decl_quants))
	                     ((\v -> case v of
	                      TeTy_Var_Name n | n == snd @loc.consts_name -> Just (Calc.Suggest n)
	                      _ -> Nothing) `Calc.abstract` @body.term))
	                     (Foldable.foldr
	                       (\(quant, qname) te ->
	                        let nam = Calc.Suggest qname in
	                        Calc.Term_Abst nam
	                         (Calc.Type_Sort Calc.sort_star_mono)
	                         ((\v -> case v of
	                           TeTy_Var_Monovar m | m == quant -> Just nam
	                           _ -> Nothing) `Calc.abstract` te))
	                       @decl.term
	                       (snd @loc.decl_quants))
sem Decl
 | Let
	-- loc.monovar      = @lhs.freshvar
	-- loc.decl_polyvar = @lhs.freshvar + 1
	decl.freshvar    = @lhs.freshvar + 1