-----------------------------------------------------------------------------
-- |The Helium Compiler : Static Analysis
-- 
-- Maintainer  :  bastiaan@cs.uu.nl
-- Stability   :  experimental
-- Portability :  unknown
--
-- Extra information for overloading (for code generation)
--
-----------------------------------------------------------------------------

ATTR Declarations Declaration Expressions Expression Statements Statement
     Qualifiers Qualifier GuardedExpressions GuardedExpression 
     Alternatives Alternative FunctionBindings FunctionBinding
     RightHandSide MaybeDeclarations MaybeExpression RecordExpressionBinding
     RecordExpressionBindings Body
        [ availablePredicates   : Predicates
          classEnvironment      : ClassEnvironment
        | dictionaryEnvironment : DictionaryEnvironment          
        | 
        ]
	
SEM Module
  | Module
       -- return an empty dictionary environment for the non-overloading setting
       lhs  . dictionaryEnvironment = if Overloading `elem` @lhs.options 
                                        then @body.dictionaryEnvironment
                                        else emptyDictionaryEnvironment
       body . dictionaryEnvironment = emptyDictionaryEnvironment
            . classEnvironment      = @classEnv
            . availablePredicates   = []
	    
SEM Declaration   
 
  | FunctionBindings
       loc      . declPredicates        = let scheme     = M.findWithDefault err (NameWithRange @bindings.name) @lhs.allTypeSchemes
                                              predicates = matchTypeWithScheme @lhs.orderedTypeSynonyms 
                                                              (@lhs.substitution |-> @beta) 
                                                              (@lhs.substitution |-> scheme)
                                              err = internalError "TypeInferenceOverloading.ag" "n/a" "could not find type for function binding"
                                          in expandPredicates @lhs.orderedTypeSynonyms predicates      
       bindings . availablePredicates   = @declPredicates ++ @lhs.availablePredicates
       lhs      . dictionaryEnvironment = addForDeclaration @bindings.name @declPredicates @bindings.dictionaryEnvironment
       
  | PatternBinding 
       loc           . declPredicates = case @pattern.self of
                                          Pattern_Variable _ name -> 
                                             let scheme     = M.findWithDefault err (NameWithRange name) @lhs.allTypeSchemes
                                                 predicates = matchTypeWithScheme @lhs.orderedTypeSynonyms 
                                                                 (@lhs.substitution |-> @betaRight)  
                                                                 (@lhs.substitution |-> scheme)                                                                                                            
                                                 err = internalError "TypeInferenceOverloading.ag" "n/a" ("could not find type for pattern binding "++show name)
                                             in Just (name, expandPredicates @lhs.orderedTypeSynonyms predicates)
                                          _ -> Nothing
       righthandside . availablePredicates = case @declPredicates of
                                                Just (_, ps) -> ps ++ @lhs.availablePredicates
                                                Nothing      -> @lhs.availablePredicates
       lhs           . dictionaryEnvironment = case @declPredicates of
                                                  Just (n, ps) -> addForDeclaration n ps @righthandside.dictionaryEnvironment
                                                  Nothing      -> @righthandside.dictionaryEnvironment
       
SEM Expression 

  | Variable   lhs . dictionaryEnvironment = @newDEnv              
               loc . nameInScope           = case filter (@name.self==) @lhs.namesInScope of 
                                                [name] -> NameWithRange name
                                                _      -> internalError "TypeInferenceOverloading.ag" "n/a" "name not in scope"
                   . maybeInferredType     = M.lookup @nameInScope @lhs.allTypeSchemes
                   . requiredDictionaries  = -- if not in finitemap then this is bound by a monomorphic pattern variable
                                             case @maybeInferredType of
                                                Nothing     -> [] 
                                                Just scheme -> getRequiredDictionaries 
                                                                  (getOrderedTypeSynonyms @lhs.importEnvironment) 
                                                                  (@lhs.substitution |-> @usedAsType)
                                                                  (@lhs.substitution |-> scheme)
                   . newDEnv               = resolveOverloading (@lhs.classEnvironment)
                                                                @name.self 
                                                                (@lhs.substitution |-> @lhs.availablePredicates)
                                                                (@lhs.substitution |-> @requiredDictionaries)
                                                                @lhs.dictionaryEnvironment 
                   . usedAsType            = @lhs.substitution |-> @beta

  | Enum     lhs . dictionaryEnvironment = @newDEnv
             loc . localName             = flip setNameRange @range.self $ 
                                           case (@then.section, @to.section) of
                                              (False, False) -> enumFromThenToName 
                                              (False, True ) -> enumFromThenName 
                                              (True , False) -> enumFromToName 
                                              (True , True ) -> enumFromName 
                 . requiredDictionaries  = if @overloaded then @lhs.substitution |-> [Predicate "Enum" @elementType] else []
                 . newDEnv               = resolveOverloading (@lhs.classEnvironment)  @localName 
                                                              (@lhs.substitution |-> @lhs.availablePredicates) 
                                                              (@lhs.substitution |-> @requiredDictionaries) 
                                                              @to.dictionaryEnvironment 

  
  | Negate   lhs . dictionaryEnvironment = @newDEnv
             loc . localName             = setNameRange intUnaryMinusName @range.self
                 . negateTypeScheme      = case M.lookup @localName (typeEnvironment @lhs.importEnvironment) of 
                                              Just scheme -> scheme
                                              Nothing     -> internalError "TypeInferenceOverloading.ag" "n/a" "type of negate unknown"
                 . requiredDictionaries  = getRequiredDictionaries 
                                              (getOrderedTypeSynonyms @lhs.importEnvironment) 
                                              (@lhs.substitution |-> @usedAsType)
                                              (@lhs.substitution |-> @negateTypeScheme)
                 . usedAsType            = @lhs.substitution |-> (@expression.beta .->. @beta)
                 . newDEnv               = resolveOverloading (@lhs.classEnvironment)  @localName 
                                                              (@lhs.substitution |-> @lhs.availablePredicates) 
                                                              (@lhs.substitution |-> @requiredDictionaries)
                                                              @expression.dictionaryEnvironment                                              
             
{         
getRequiredDictionaries :: OrderedTypeSynonyms -> Tp -> TpScheme -> Predicates
getRequiredDictionaries synonyms useType defType =
   expandPredicates synonyms (matchTypeWithScheme synonyms useType defType)

matchTypeWithScheme :: OrderedTypeSynonyms -> Tp -> TpScheme -> Predicates
matchTypeWithScheme synonyms tp scheme =
   let (ips, itp) = split . snd . instantiate 0 . freezeFTV $ scheme
   in case mguWithTypeSynonyms synonyms itp (freezeVariablesInType tp) of
         Left _ -> internalError "TypeInferenceOverloading.ag" "matchTypeWithScheme" "no unification"
         Right (_, sub) -> 
            let f (Predicate s typ) = Predicate s (unfreezeVariablesInType $ sub |-> typ)
            in map f ips
            
resolveOverloading :: ClassEnvironment -> Name -> Predicates -> Predicates ->
                         DictionaryEnvironment -> DictionaryEnvironment
resolveOverloading classEnv name availablePredicates predicates dEnv = 
   let maybeTrees = map (makeDictionaryTree classEnv availablePredicates) predicates
   in if all isJust maybeTrees
        then addForVariable name (map fromJust maybeTrees) dEnv
        else internalError "TypeInferenceOverloading.ag" "resolveOverloading" ("cannot resolve overloading (" ++ show name ++ ")")
   
expandPredicates :: OrderedTypeSynonyms -> Predicates -> Predicates
expandPredicates synonyms = map (expandPredicate synonyms)

expandPredicate :: OrderedTypeSynonyms -> Predicate -> Predicate
expandPredicate (_, synonyms) (Predicate className tp) = Predicate className (expandType synonyms tp)
}