{-# LANGUAGE UndecidableInstances #-}

{-| Module      :  SelectConstraintSolver
    License     :  GPL

    Maintainer  :  helium@cs.uu.nl
    Stability   :  experimental
    Portability :  portable
    
    Select the type constraint solver of your own liking
-}

module Helium.StaticAnalysis.Inferencers.SelectConstraintSolver (selectConstraintSolver) where

import Helium.Main.Args (Option(..))
import Helium.StaticAnalysis.Miscellaneous.ConstraintInfo
import Helium.StaticAnalysis.Miscellaneous.TypeConstraints
import Helium.ModuleSystem.ImportEnvironment (ImportEnvironment, getSiblings, 
  getNeverDirectives, getCloseDirectives, getDisjointDirectives, getDefaultDirectives)
import Helium.StaticAnalysis.Heuristics.ListOfHeuristics (listOfHeuristics)
import Top.Types
import Top.Solver
import Top.Ordering.TreeWalk
import Top.Ordering.Tree
import Top.Solver.Greedy
import Top.Solver.TypeGraph
import Top.Solver.PartitionCombinator
import Top.Solver.SwitchCombinator
import Top.Constraint.Information()
import Top.Implementation.TypeClassDirectives
import Top.Interface.Substitution (makeSubstConsistent)

type TreeSolver = ClassEnvironment -> OrderedTypeSynonyms -> Int 
                       -> Tree (TypeConstraint ConstraintInfo) -> (SolveResult ConstraintInfo, LogEntries)

selectConstraintSolver :: [Option] -> ImportEnvironment -> TreeSolver
selectConstraintSolver options importenv classEnv synonyms unique constraintTree = 
   solve selectedOptions constraints selectedSolver

 where   
      
       -- spread type constraints or not (i.e., map some type constraints to a 
       -- corresponding node in the constraint tree)
       -- spreading is enabled by default 
       spreadingOrNot 
          | NoSpreading `elem` options = id
          | otherwise                  = spreadTree spreadFunction
         
       -- choose your treewalk to flatten the constraint tree
       -- the default treewalk is TreeWalkInorderTopLastPost (similar to 'W')
       simpleTreeWalk
          | TreeWalkTopDown             `elem` options = topDownTreeWalk
          | TreeWalkBottomUp            `elem` options = bottomUpTreeWalk
          | TreeWalkInorderTopFirstPre  `elem` options = inorderTopFirstPreTreeWalk
          | TreeWalkInorderTopLastPre   `elem` options = inorderTopLastPreTreeWalk
          | TreeWalkInorderTopFirstPost `elem` options = inorderTopFirstPostTreeWalk
          | otherwise                                  = inorderTopLastPostTreeWalk   
       
       selectedTreeWalk 
          | RightToLeft `elem` options = reverseTreeWalk simpleTreeWalk
          | otherwise                  = simpleTreeWalk
       
       phases       = phaseTree (TCOper "MakeConsistent" makeSubstConsistent)        
       flattening   = flattenTree selectedTreeWalk . phases . spreadingOrNot
       
       constraints      = flattening constraintTree
       chunkConstraints = chunkTree . phases . spreadTree spreadFunction $ constraintTree
       siblings         = getSiblings importenv

       neverDirectives      = map (uncurry NeverDirective)    $ getNeverDirectives importenv
       closeDirectives      = map (uncurry CloseDirective)    $ getCloseDirectives importenv
       disjointDirectives   = map (uncurry DisjointDirective) $ getDisjointDirectives importenv
       defaultDirectives    = map (uncurry (uncurry DefaultDirective))  $ getDefaultDirectives importenv

       selectedOptions :: SolveOptions ConstraintInfo
       selectedOptions = 
          solveOptions { uniqueCounter    = unique 
                       , typeSynonyms     = synonyms
                       , classEnvironment = classEnv
                       , typeClassDirectives = neverDirectives ++ closeDirectives ++ disjointDirectives ++ defaultDirectives
                       }
          
       selectedSolver :: ConstraintSolver (TypeConstraint ConstraintInfo) ConstraintInfo
       selectedSolver
          | SolverSimple      `elem` options = greedySimpleConstraintSolver 
          | SolverGreedy      `elem` options = greedyConstraintSolver                                                        
          | SolverTypeGraph   `elem` options = typegraphConstraintSolver heuristics
          | SolverCombination `elem` options = combinedSolver             
          | otherwise = 
               solveChunkConstraints polySubst combinedSolver (flattenTree selectedTreeWalk) chunkConstraints
            
       combinedSolver =
          -- (if SignatureWarnings `elem` options then warnForTooSpecificSignatures runGreedy else runGreedy)   
          greedyConstraintSolver |>>| typegraphConstraintSolver heuristics

          
       heuristics = listOfHeuristics options siblings


{-
warnForTooSpecificSignatures :: SolverX (TypeConstraint ConstraintInfo) ConstraintInfo Predicates Warnings -> SolverX (TypeConstraint ConstraintInfo) ConstraintInfo Predicates Warnings
warnForTooSpecificSignatures solver classEnv synonyms unique constraints =
   let -- split the constraints that come from an explicit type signature from the others.
       -- (only for the definition, not for the uses)
       (explicits, normalConstraints) = partition (isJust . maybeExplicitlyTyped) constraints
       -- make new (equality) constraints for the explicits
       newConstraints = concatMap makeNewConstraint
                      . groupBy (\x y -> fst x    ==     fst y)
                      . sortBy  (\x y -> fst x `compare` fst y)
                      $ map (fromJust . maybeExplicitlyTyped) explicits
       
       -- first solve the new constraint set and the "normal" constraints. Try to determine an "inferred" and more general
       -- type from this result. Then, solve the explicit constraints that were skipped to make the final substitution as
       -- it would be originally.
       result1 = solver classEnv synonyms unique (newConstraints ++ normalConstraints)
       result2 = solver classEnv synonyms (uniqueFromResult result1) (substitutionFromResult result1 |-> explicits)
       
       -- make the warnings
       warnings =
          let f (monos, name, tp, signature) =
                 let ms  = substitutionFromResult result1 |-> monos
                     ps  = qualifiersFromResult result1 
                     ts  = makeScheme (ftv ms) ps (substitutionFromResult result1 |-> tp)
                     b1  = genericInstanceOf synonyms classEnv signature ts
                     b2  = genericInstanceOf synonyms classEnv ts signature
                 in [ SignatureTooSpecific name signature ts | b1 && not b2 ] 

          in [ warning | Just x <- map splitExplicit explicits, warning <- f x ]    
       
   in (result1 { extensionFromResult = warnings ++ extensionFromResult result1 }) `plus` result2

 where 
   makeNewConstraint :: [(NameWithRange, Tp)] -> [TypeConstraint ConstraintInfo]
   makeNewConstraint [] = []
   makeNewConstraint ((name, t1):rest) = 
      let info = cinfoSameBindingGroup (nameWithRangeToName name)
      in [ (t1 .==. t2) info | (_, t2) <- rest ]

   maybeExplicitlyTyped :: TypeConstraint ConstraintInfo -> Maybe (NameWithRange, Tp)
   maybeExplicitlyTyped (TC3 (Skolemize tp _ info)) = 
      do (monos, name) <- maybeExplicitTypedDefinition info
         return (NameWithRange name, tp)
   maybeExplicitlyTyped _ = Nothing
         
   splitExplicit :: TypeConstraint ConstraintInfo -> Maybe (Tps, Name, Tp, TpScheme)
   splitExplicit (TC3 (Skolemize tp (_, SigmaScheme tpscheme) info))
      | isExplicitTypedBinding info =
           do (monos, name) <- maybeExplicitTypedDefinition info
              return (monos, name, tp, tpscheme)
   splitExplicit _ = Nothing
   
instance Show Warning where show _ = "<warning>"
instance IsState Warnings -}