-----------------------------------------------------------------------------
-- |The Helium Compiler : Static Analysis
--
-- Maintainer  :  bastiaan@cs.uu.nl
-- Stability   :  experimental
-- Portability :  unknown
--
-- Translate the type inference directives into a core datatype. In this core
-- datatype, type variable identifiers are (for instance) replaced by standard
-- type variables (ints).
--
-- (directives based on "Scripting the Type Inference Process", ICFP 2003)
-----------------------------------------------------------------------------

{
typingStrategyToCore :: ImportEnvironment -> TypingStrategy -> Core_TypingStrategy
typingStrategyToCore importEnv strategy = 
   core_Syn_TypingStrategy (wrap_TypingStrategy (sem_TypingStrategy strategy) Inh_TypingStrategy { importEnvironment_Inh_TypingStrategy = importEnv })
}

INCLUDE "TS_Syntax.ag"
INCLUDE "TS_Collect.ag"
INCLUDE "UHA_Syntax.ag"

imports {
import Helium.StaticAnalysis.Directives.TS_Syntax
import Helium.StaticAnalysis.Directives.TS_CoreSyntax
import Helium.ModuleSystem.ImportEnvironment
import Helium.StaticAnalysis.Messages.Messages
import Top.Types

import Helium.StaticAnalysis.Miscellaneous.ConstraintInfo
import Helium.Syntax.UHA_Utils (getNameName, nameFromString)
import qualified Helium.Syntax.UHA_OneLine as UHA_OneLine
import Helium.StaticAnalysis.Miscellaneous.TypeConversion
import Helium.Utils.Utils (internalError)
import Data.List
import Helium.Utils.OneLiner
import Helium.StaticAnalysis.Directives.TS_Attributes
import Helium.StaticAnalysis.Miscellaneous.TypeConstraints

}
ATTR TypingStrategies TypingStrategy [ importEnvironment : ImportEnvironment | | ]

SEM TypingStrategy [ | | core : Core_TypingStrategy ]
  | Siblings
      lhs . core = Siblings (map getNameName @names.self)
  | TypingStrategy
      lhs . core = TypingStrategy @typeEnv @typerule.core @statements.core    
      loc . nameMap = zip @uniqueTypevariables (map TVar [0..])

SEM TypeRule [ | | core : Core_TypeRule ]
  | TypeRule 
      lhs . core = TypeRule @premises.core @conclusion.core

SEM Judgement [ | | core : Core_Judgement ]
  | Judgement
       lhs . core = Judgement (showOneLine 10000 $ UHA_OneLine.oneLineTree_Syn_Expression $ UHA_OneLine.wrap_Expression (UHA_OneLine.sem_Expression @expression.self) UHA_OneLine.Inh_Expression) (makeTpFromType @lhs.nameMap @type.self)   

SEM SimpleJudgements [ | | core : Core_Judgements ]
  | Cons  lhs . core = @hd.core : @tl.core
  | Nil   lhs . core = []

SEM SimpleJudgement [ | | core : Core_Judgement ] 
  | SimpleJudgement 
       lhs . core = Judgement (show @name.self) (makeTpFromType @lhs.nameMap @type.self)              
       
SEM UserStatements [ | | core : Core_UserStatements ]
  | Cons  lhs . core = @hd.core : @tl.core
  | Nil   lhs . core = []

SEM UserStatement [ | | core : Core_UserStatement ]
  | Equal                     lhs . core = Equal 
                                             (makeTpFromType @lhs.nameMap @leftType.self) 
                                             (makeTpFromType @lhs.nameMap @rightType.self) 
                                             (changeAttributes (useNameMap @lhs.nameMap) @message)
  | Pred                      lhs . core = Pred
                                             (show @predClass.self)
                                             (makeTpFromType @lhs.nameMap @predType.self)
                                             (changeAttributes (useNameMap @lhs.nameMap) @message)
  | MetaVariableConstraints   lhs . core = MetaVariableConstraints (show @name.self)
  | Phase                     lhs . core = CorePhase @phase
  
-- collecting the fixed constant types
--
-- This approach to determine the types of the fixed constants does not work in general!
-- For the moment, the type variables assigned to the premises and the conclusion are skolemized 
-- (in particular, when building the newEnvironment). In some cases however, this results in
-- a type inconsistency:
-- For instance: 
--    f : t1   =>   f id ::t2     (f is a meta-variable, id has the type forall a . a -> a)
--   in this case, the type for id cannot be expressed in t1 and t2    (since t1 is in fact a function type)
--
-- Todo: fix this problem.

SEM TypingStrategy
  | TypingStrategy
       loc . typeEnv = 
          let newEnvironment = 
                 let list = [ (nameFromString s, toTpScheme $ freezeVariablesInType tp) 
                            | (s, tp) <- ("$$conclusion", @typerule.conclusionType) : @typerule.simpleJudgements 
                            ]
                 in @lhs.importEnvironment { typeEnvironment = M.fromList list }
              (inferredType, freeVariables, _) = expressionTypeInferencer newEnvironment @typerule.conclusionExpression
              monoType = unqualify (unquantify inferredType)
              synonyms = getOrderedTypeSynonyms @lhs.importEnvironment
              sub = case mguWithTypeSynonyms synonyms monoType (freezeVariablesInType @typerule.conclusionType) of
                       Left _       -> internalError "TS_ToCore.ag" "n/a" "no unification possible" 
                       Right (_, s) -> s
          in [ (show name, unfreezeVariablesInType (sub |-> tp))
             | (name, tp) <- concat (M.elems freeVariables) 
             ]
             
{
useNameMap :: [(Name, Tp)] -> Attribute -> Attribute
useNameMap nameMap attribute = 
   case attribute of
      LocalAttribute s ->
         case lookup s [ (show n, i) | (n, TVar i) <- nameMap ] of
            Just i  -> LocalAttribute (show i)
            Nothing -> attribute
      _             -> attribute
   
}