packages feed

helium-1.8: src/Helium/StaticAnalysis/Inferencers/TypeInferenceRules.ag

-----------------------------------------------------------------------------
-- |The Helium Compiler : Static Analysis
-- 
-- Maintainer  :  bastiaan@cs.uu.nl
-- Stability   :  experimental
-- Portability :  unknown
--
-- Contains all the typing rules for the an UHA abstract syntax tree.
--
-----------------------------------------------------------------------------

----------------------------------------------------------------------------------------
-- Type Inferencing : Module

SEM Module
  | Module
      loc  -- Solve the type constraints.
           . (SolveResult betaUniqueAtTheEnd substitution typeschemeMap _ solveErrors) = @solveResult
           . (solveResult, logEntries) =
                (selectConstraintSolver @lhs.options @lhs.importEnvironment) 
                   @classEnv
                   @orderedTypeSynonyms 
                   @body.betaUnique 
                   @body.constraints
                   
           . orderedTypeSynonyms = getOrderedTypeSynonyms @lhs.importEnvironment   
           . classEnv            = -- extend the set of imported instance declarations with the 
                                   -- derived instances
                                   foldr (\(n, i) -> insertInstance (show n) i) 
                                         (createClassEnvironment @lhs.importEnvironment) 
                                         @body.collectInstances
           . typeErrors          = case makeTypeErrors @lhs.options @classEnv @orderedTypeSynonyms @substitution @solveErrors of
                                      []   -> if NoOverloadingTypeCheck `elem` @lhs.options
                                                 then filter (\(TypeError _ ms _ _) -> not $ isInfixOf "Illegal overloaded type" $ show ms) @body.collectErrors
                                                 else @body.collectErrors
                                      errs -> reverse errs
           . warnings            = @body.collectWarnings -- ++ @tooSpecificWarnings
           . assumptions         = let f xs = [ (n, @substitution |-> tp) | (n, tp) <- xs ] 
                                   in M.map f @body.assumptions
           . initialScope        = M.keys (typeEnvironment @lhs.importEnvironment)           
           . monos               = map TVar @monomorphics
           . monomorphics        = ftv (  (M.elems $ valueConstructors @lhs.importEnvironment) 
                                       ++ (M.elems $ typeEnvironment   @lhs.importEnvironment)
                                       )
                                  
      body . typeschemeMap = M.fromList (M.assocs @typeschemeMap) -- was a copy rule.
           . betaUnique          = if null @monomorphics 
                                     then 0 
                                     else maximum @monomorphics + 1 
                                 
---------------------------------------------------------------------------------------
-- Type Inferencing : Body

ATTR Body
    [ 
      monos                 : Monos
    | betaUnique            : Int
    | assumptions           : Assumptions
      constraints           : ConstraintSet
    ]

SEM Body
  | Hole
      lhs . assumptions = noAssumptions
          . constraints = emptyTree
  | Body  
      declarations . bindingGroups    = []       
      (loc.csetBinds,lhs.assumptions) = (typeEnvironment @lhs.importEnvironment .:::. @aset) @cinfo      
      loc . constraints               = @csetBinds .>>. @cset
                                           
      (loc.aset, loc.cset, loc.inheritedBDG, loc.chunkNr, lhs.betaUnique, loc.implicitsFM) = 
         let inputBDG = (True, @lhs.currentChunk, @declarations.uniqueChunk, @lhs.monos, @declarations.typeSignatures, Nothing, @declarations.betaUnique)
         in performBindingGroup inputBDG @declarations.bindingGroups  
                        
      
---------------------------------------------------------------------------------------
-- Type Inferencing : Declaration, Declarations, MaybeDeclarations

ATTR Declaration Declarations MaybeDeclarations [ monos:Monos | betaUnique:Int | ]
ATTR Declaration Declarations                   [ inheritedBDG:InheritedBDG | bindingGroups:BindingGroups | ]
ATTR                          MaybeDeclarations [ | assumptions:Assumptions constraints:ConstraintSet | ]

SEM Declaration

  | FunctionBindings
      lhs      . bindingGroups = @mybdggrp : @lhs.bindingGroups
      bindings . betaUnique    = @lhs.betaUnique + 2 + @bindings.numberOfPatterns
               . monos         = findMono @bindings.name @lhs.inheritedBDG ++ @lhs.monos               
      loc      . beta          = TVar @lhs.betaUnique
               . betaRight     = TVar (@lhs.betaUnique + 1)
               . betasLeft     = take @bindings.numberOfPatterns (map TVar [@lhs.betaUnique + 2..])
               . newcon        = (@beta .==. foldr (.->.) @betaRight @betasLeft) @cinfo
               . mybdggrp      = ( M.singleton @bindings.name @beta
                                 , @bindings.assumptions
                                 , [ Node [ Phase (-1) [@newcon] 
                                          , Receive @lhs.betaUnique
                                          , Node @bindings.constraintslist
                                          ]
                                   ]
                                 )

  | PatternBinding
      lhs           . bindingGroups = @mybdggrp : @lhs.bindingGroups
      pattern       . betaUnique    = @lhs.betaUnique + 1
      righthandside . monos         = findMono (head (M.keys @pattern.environment)) @lhs.inheritedBDG ++ @lhs.monos    
      loc           . betaRight     = TVar @lhs.betaUnique
                    . newcon        = [ (@betaRight .==. @pattern.beta) @cinfo ]
                    . mybdggrp      = ( @pattern.environment
                                      , @righthandside.assumptions
                                      , [ @newcon .>.
                                          Node [ @pattern.constraints
                                               , @righthandside.constraints
                                               ]
                                        ]
                                      )

SEM MaybeDeclarations
  | Just
      declarations . bindingGroups  = []
      (lhs.assumptions, lhs.constraints, loc.inheritedBDG, loc.chunkNr, lhs.betaUnique, loc.implicitsFM) = 
         let inputBDG   = (False, @lhs.currentChunk, @declarations.uniqueChunk, @lhs.monos, @declarations.typeSignatures, mybdggroup, @declarations.betaUnique)
             mybdggroup = Just (@lhs.assumptions, [@lhs.constraints])
         in performBindingGroup inputBDG @declarations.bindingGroups
                                                                   
---------------------------------------------------------------------------------------
-- Type Inferencing : FunctionBinding, FunctionBindings

ATTR FunctionBinding FunctionBindings [ betasLeft:Tps betaRight:Tp monos:Monos | betaUnique:Int | assumptions:Assumptions numberOfPatterns:Int name:Name ]
ATTR FunctionBinding                  [ | | constraints:ConstraintSet]
ATTR                 FunctionBindings [ | | constraintslist:ConstraintSets]

SEM FunctionBinding

  | Hole
      loc . assumptions      = noAssumptions
          . constraints      = emptyTree
          . numberOfPatterns = 0
          . name             = internalError "TypeInferencing.ag" "n/a" "FunctionBindings(2)"
  | FunctionBinding
      righthandside . monos       = M.elems @lefthandside.environment ++ getMonos @csetBinds ++ @lhs.monos
      loc           . constraints = @csetBinds .>>.
                                    Node [ @conLeft  .<. @lefthandside.constraints
                                         , @righthandside.constraints
                                         ]
                    . conLeft     = zipWith3 (\t1 t2 nr -> (t1 .==. t2) (@cinfoLeft nr)) @lefthandside.betas @lhs.betasLeft [0..]                                         
      (loc.csetBinds,lhs.assumptions) = (@lefthandside.environment .===. @righthandside.assumptions) @cinfoBind                    

SEM FunctionBindings

  | Cons
      lhs . assumptions      = @hd.assumptions `combine` @tl.assumptions
          . numberOfPatterns = @hd.numberOfPatterns
          . name             = @hd.name
          . constraintslist  = @hd.constraints : @tl.constraintslist
  | Nil
      lhs . assumptions      = noAssumptions
          . numberOfPatterns = internalError "TypeInferencing.ag" "n/a" "FunctionBindings(1)"
          . name             = internalError "TypeInferencing.ag" "n/a" "FunctionBindings(2)"
          . constraintslist  = []

---------------------------------------------------------------------------------------
-- Type Inferencing : LeftHandSide, RightHandSide

ATTR LeftHandSide RightHandSide [ monos:Monos | betaUnique:Int | constraints:ConstraintSet ]
ATTR LeftHandSide               [ | | betas:Tps environment:PatternAssumptions numberOfPatterns:Int name:Name ]
ATTR              RightHandSide [ betaRight:Tp | | assumptions:Assumptions ]

SEM LeftHandSide
  | Function
      lhs . name             = @name.self
      loc . constraints      = Node @patterns.constraintslist
          

  | Infix
      lhs . numberOfPatterns = 2
          . environment      = @leftPattern.environment `M.union` @rightPattern.environment
          . betas            = [@leftPattern.beta,@rightPattern.beta]
          . name             = @operator.self
      loc . constraints      = Node [ @leftPattern.constraints
                                    , @rightPattern.constraints
                                    ]
          

  | Parenthesized
      lhs . numberOfPatterns = @lefthandside.numberOfPatterns + @patterns.numberOfPatterns
          . environment      = @lefthandside.environment `M.union` @patterns.environment
          . betas            = @lefthandside.betas ++ @patterns.betas
      loc . constraints      = Node ( @lefthandside.constraints : @patterns.constraintslist )

SEM RightHandSide

  | Expression
     lhs   . assumptions = @where.assumptions   
           . constraints = @where.constraints        
     where . assumptions = @expression.assumptions
           . constraints = @newcon .>. @expression.constraints
     loc   . newcon      = [ (@expression.beta .==. @lhs.betaRight) @cinfo ]
          

  | Guarded
     lhs                . assumptions    = @where.assumptions
                        . constraints    = @where.constraints
     guardedexpressions . numberOfGuards = length @guardedexpressions.constraintslist
     where              . assumptions    = @guardedexpressions.assumptions
                        . constraints    = Node @guardedexpressions.constraintslist

---------------------------------------------------------------------------------------
-- Type Inferencing : Expression, Expressions, MaybeExpression

ATTR Expression Expressions MaybeExpression [ monos:Monos | betaUnique:Int | assumptions:Assumptions ]
ATTR Expression                             [ | | beta:Tp constraints:ConstraintSet ]
ATTR            Expressions                 [ | | betas:Tps constraintslist:ConstraintSets ]
ATTR                        MaybeExpression [ | | beta:Tp constraints:ConstraintSet section:Bool ]

SEM Expression

  | Literal
      lhs . betaUnique  = @lhs.betaUnique + 1
      loc . assumptions = noAssumptions
          . constraints = unitTree ((@literal.literalType .==. @beta) @cinfo)
          . beta        = TVar @lhs.betaUnique

  | Constructor
      lhs . betaUnique   = @lhs.betaUnique + 1
      loc . assumptions  = noAssumptions
          . constraints  = listTree @newcon
          . beta         = TVar @lhs.betaUnique
          . newcon       = case M.lookup @name.self (valueConstructors @lhs.importEnvironment) of
                              Nothing  -> []
                              Just ctp -> [ (@beta .::. ctp) @cinfo ]

  | Variable
      lhs . betaUnique  = @lhs.betaUnique + 1
      loc . assumptions = @name.self `single` @beta
          . constraints = Node [ Receive @lhs.betaUnique ]
          . beta        = TVar @lhs.betaUnique

  | Hole
      lhs . betaUnique  = @lhs.betaUnique + 1
      loc . assumptions = noAssumptions
          . constraints = emptyTree
          . beta        = TVar @lhs.betaUnique

  | NormalApplication   
      function . betaUnique  = @lhs.betaUnique + 1
      loc      . assumptions = @function.assumptions `combine` @arguments.assumptions
               . constraints = @newcon .>.
                               Node [ @function.constraints
                                    , Node @arguments.constraintslist
                                    ]      
               . beta        = TVar @lhs.betaUnique
               . newcon      = [ (@function.beta .==. foldr (.->.) @beta @arguments.betas) @cinfo ]

  | InfixApplication
      leftExpression . betaUnique  = @lhs.betaUnique + 2
      loc            . assumptions = @leftExpression.assumptions `combine` @operator.assumptions `combine` @rightExpression.assumptions
                     . constraints = @conTotal .>.
                                     Node [ @operator.constraints
                                          , @leftExpression.constraints
                                          , @rightExpression.constraints
                                          ]
                     . beta        = TVar @lhs.betaUnique
                     . betaResOp   = TVar (@lhs.betaUnique + 1)
                     . conOperator = (@operator.beta .==. @leftExpression.beta .->. @rightExpression.beta .->. @betaResOp) @cinfoOperator
                     . conTotal    = case (@leftExpression.section,@rightExpression.section) of
                                            (False,False) -> [ @conOperator, (@betaResOp     .==. @beta)                        @cinfoComplete     ]
                                            (True ,True ) -> [               (@operator.beta .==. @beta)                        @cinfoEmpty        ]
                                            (False,True ) -> [ @conOperator, (@rightExpression.beta .->. @betaResOp .==. @beta) @cinfoRightSection ]
                                            (True ,False) -> [ @conOperator, (@leftExpression.beta  .->. @betaResOp .==. @beta) @cinfoLeftSection  ]

  | If
      guardExpression . betaUnique  = @lhs.betaUnique + 1
      loc             . assumptions = @guardExpression.assumptions `combine` @thenExpression.assumptions `combine` @elseExpression.assumptions
                      . constraints = Node [ @conGuard .<. @guardExpression.constraints
                                           , @conThen  .<. @thenExpression.constraints
                                           , @conElse  .<. @elseExpression.constraints
                                           ]
                      . beta        = TVar @lhs.betaUnique
                      . conGuard    = [ (@guardExpression.beta .==. boolType) @cinfoGuard ]
                      . conThen     = [ (@thenExpression.beta  .==. @beta   ) @cinfoThen  ]
                      . conElse     = [ (@elseExpression.beta  .==. @beta   ) @cinfoElse  ]

  | Lambda
      patterns   . betaUnique  = @lhs.betaUnique + 1
      expression . monos       = M.elems @patterns.environment ++ getMonos @csetBinds ++ @lhs.monos
      loc        . constraints = @newcon .>. @csetBinds .>>.
                                 Node [ Node @patterns.constraintslist
                                      , @expression.constraints
                                      ]
                 . beta        = TVar @lhs.betaUnique                 
                 . newcon      = [ (foldr (.->.) @expression.beta @patterns.betas .==. @beta) @cinfoType ]
      (loc.csetBinds, loc.assumptions) = (@patterns.environment .===. @expression.assumptions) @cinfoBind                 

  | Case         
      expression   . betaUnique  = @lhs.betaUnique + 2
      alternatives . betaLeft    = @beta'
                   . betaRight   = @beta
      loc          . assumptions = @expression.assumptions `combine` @alternatives.assumptions
                   . constraints = Node [ @newcon .<. @expression.constraints
                                        , Node @alternatives.constraintslist
                                        ]                   
                   . beta        = TVar @lhs.betaUnique
                   . beta'       = TVar (@lhs.betaUnique + 1)
                   . newcon      = [ (@expression.beta .==. @beta') @cinfo ]

  | Let
      declarations . betaUnique     = @lhs.betaUnique + 1
                   . bindingGroups  = []
      loc          . constraints    = [ (@expression.beta .==. @beta) @cinfoType ] .>. @cset                   
                   . beta           = TVar @lhs.betaUnique                   
                   
      (loc.assumptions, loc.cset, loc.inheritedBDG, loc.chunkNr, lhs.betaUnique, loc.implicitsFM) =
         let inputBDG   = (False, @lhs.currentChunk, @expression.uniqueChunk, @lhs.monos, @declarations.typeSignatures, mybdggroup, @expression.betaUnique)
             mybdggroup = Just (@expression.assumptions, [@expression.constraints])
         in performBindingGroup inputBDG @declarations.bindingGroups

  | Do
      lhs        . constraints   = Node [ @newcon .<. @statements.constraints ]
      statements . betaUnique    = @lhs.betaUnique + 1
                 . generatorBeta = Nothing
                 . assumptions   = noAssumptions
      loc        . assumptions   = @statements.assumptions
                 . constraints   = emptyTree
                 . beta          = TVar @lhs.betaUnique
                 . newcon        = case @statements.generatorBeta of
                                      Nothing -> []
                                      Just b  -> [ (ioType b .==. @beta) @cinfo ]

  | List
      expressions . betaUnique   = @lhs.betaUnique + 2
      loc         . constraints  = @newcon .>.
                                    Node (zipWith3 @zipf @expressions.betas [0..] @expressions.constraintslist)
                  . beta         = TVar @lhs.betaUnique
                  . beta'        = TVar (@lhs.betaUnique + 1)
                  . newcon       = [ (listType @beta' .==. @beta) @cinfoResult ]
                  . zipf         = \tp childNr ctree -> [ (tp .==. @beta') (@cinfoElem childNr) ] .<. ctree

  | Tuple
      expressions . betaUnique  = @lhs.betaUnique + 1
      loc         . constraints = @newcon .>. Node @expressions.constraintslist
                  . beta        = TVar @lhs.betaUnique
                  . newcon      = [ (tupleType @expressions.betas .==. @beta) @cinfo ]

  | Typed     
      expression . betaUnique  = @lhs.betaUnique + 1
      loc        . assumptions = @expression.assumptions
                 . constraints = @conResult .>.
                                 Node [ @conExpr .<. @expression.constraints ]
                 . beta        = TVar @lhs.betaUnique
                 . typeScheme  = makeTpSchemeFromType @type.self 
                 . conResult   = [ (@beta            .::. @typeScheme) @cinfoResult          ]
                 . conExpr     = [ (@expression.beta !::! @typeScheme) @lhs.monos @cinfoExpr ]

  | Comprehension                      
      expression . betaUnique  = @lhs.betaUnique + 1
                 . monos       = @qualifiers.monos
      qualifiers . assumptions = @expression.assumptions
                 . constraints = @expression.constraints
                 . monos       = @lhs.monos
      loc        . assumptions = @qualifiers.assumptions  
                 . constraints = @newcon .>. Node [ @qualifiers.constraints ]
                 . beta        = TVar @lhs.betaUnique
                 . newcon      = [ (listType @expression.beta .==. @beta) @cinfo ]

  | Enum
       from . betaUnique   = @lhs.betaUnique + (if @overloaded then 2 else 1)
       loc  . assumptions  = @from.assumptions `combine` @then.assumptions `combine` @to.assumptions
            . constraints  = (@conList ++ @conPredicate) .>.
                             Node [ @conFrom .<. @from.constraints
                                  , @conThen .<. @then.constraints
                                  , @conTo   .<. @to.constraints
                                  ]
            . beta         = TVar @lhs.betaUnique
            . overloaded   = case M.lookup enumFromName (typeEnvironment @lhs.importEnvironment) of
                                Just scheme -> isOverloaded scheme
                                Nothing     -> False
            . elementType  = if @overloaded then TVar (@lhs.betaUnique + 1) else intType
            . conPredicate = if @overloaded then [predicate (Predicate "Enum" @elementType) @cinfoPred] else []
            . conList      = [ (listType @elementType .==. @beta) @cinfoResult ]
            . conFrom      = [ (@from.beta .==. @elementType) @cinfoFrom ]
            . conThen      = [ (@then.beta .==. @elementType) @cinfoThen ]
            . conTo        = [ (@to.beta   .==. @elementType) @cinfoTo   ]

  | Negate
       expression . betaUnique  = @lhs.betaUnique + 1
       loc        . constraints = @newcon .>. Node [ @expression.constraints ]
                  . beta        = TVar @lhs.betaUnique
                  . newcon      = -- search for the type of 'negate' in the import envionment: otherwise use the default type.
                                  let standard = makeScheme [] [Predicate "Num" (TVar 0)] (TVar 0 .->. TVar 0)
                                      tpscheme = M.findWithDefault standard (nameFromString "negate") (typeEnvironment @lhs.importEnvironment)
                                  in [ (@expression.beta .->. @beta .::. tpscheme) @cinfo]

{- only for type inference without overloading -}
  | NegateFloat
       expression . betaUnique  = @lhs.betaUnique + 1
       loc        . constraints = @newcon .>. Node [ @expression.constraints ]
                  . beta        = TVar @lhs.betaUnique
                  . newcon      = [ (floatType .->. floatType .==. @expression.beta .->. @beta) @cinfo]

SEM Expressions

  | Cons
      lhs . betas           = @hd.beta : @tl.betas
          . assumptions     = @hd.assumptions `combine` @tl.assumptions
          . constraintslist = @hd.constraints : @tl.constraintslist

  | Nil
      lhs . betas           = []
          . assumptions     = noAssumptions
          . constraintslist = []

SEM MaybeExpression

  | Just
      lhs . section = False

  | Nothing
      lhs . section     = True
          . betaUnique  = @lhs.betaUnique + 1
          . assumptions = noAssumptions
          . constraints = emptyTree
      loc . beta        = TVar @lhs.betaUnique

---------------------------------------------------------------------------------------
-- Type Inferencing : GuardedExpression, GuardedExpressions

ATTR GuardedExpressions GuardedExpression [ numberOfGuards:Int monos:Monos betaRight:Tp | betaUnique:Int | assumptions:Assumptions ]
ATTR GuardedExpressions                   [ | | constraintslist:ConstraintSets ]
ATTR                    GuardedExpression [ | | constraints:ConstraintSet      ]

SEM GuardedExpression

  | GuardedExpression
      lhs . constraints = Node [ @newconGuard .<. @guard.constraints
                               , @newconExpr  .<. @expression.constraints
                               ]
          . assumptions = @guard.assumptions `combine` @expression.assumptions
      loc . newconGuard = [ (@guard.beta .==. boolType) @cinfoGuard ]
          . newconExpr  = [ (@expression.beta .==. @lhs.betaRight) @cinfoExpr ]

SEM GuardedExpressions

  | Cons
      lhs . assumptions     = @hd.assumptions `combine` @tl.assumptions
          . constraintslist = @hd.constraints : @tl.constraintslist

  | Nil
      lhs . assumptions     = noAssumptions
          . constraintslist = []


---------------------------------------------------------------------------------------
-- Type Inferencing : Pattern

ATTR Pattern Patterns [ monos:Monos | betaUnique:Int | environment:PatternAssumptions ]
ATTR Pattern          [ | | beta:Tp constraints:ConstraintSet ]
ATTR         Patterns [ | | betas:Tps constraintslist:ConstraintSets numberOfPatterns:Int ]

SEM Pattern
  | Hole 
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = noAssumptions
      loc . constraints = emptyTree
          . beta        = TVar @lhs.betaUnique

  | Literal
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = noAssumptions
      loc . constraints = unitTree ((@literal.literalType .==. @beta) @cinfo)
          . beta        = TVar @lhs.betaUnique

  | Variable
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = M.singleton @name.self @beta
      loc . constraints = Receive @lhs.betaUnique
          . beta        = TVar @lhs.betaUnique

  | InfixConstructor
      lhs         . environment    = @leftPattern.environment `M.union` @rightPattern.environment
      leftPattern . betaUnique     = @lhs.betaUnique + 2
      loc         . constraints    = @conApply .>.
                                     Node [ listTree @conConstructor
                                          , @leftPattern.constraints
                                          , @rightPattern.constraints
                                          ]
                  . beta           = TVar @lhs.betaUnique
                  . betaCon        = TVar (@lhs.betaUnique + 1)
                  . conApply       = [ (@betaCon .==. @leftPattern.beta .->. @rightPattern.beta .->. @beta) @cinfoApply ]
                  . conConstructor = case M.lookup @constructorOperator.self (valueConstructors @lhs.importEnvironment) of
                                        Nothing  -> []
                                        Just ctp -> [ (@betaCon .::. ctp) @cinfoConstructor ]

  | Constructor
      patterns . betaUnique     = @lhs.betaUnique + 2
      loc      . constraints    = @conApply .>.
                                  Node [ listTree @conConstructor
                                       , Node @patterns.constraintslist
                                       ]
               . beta           = TVar (@lhs.betaUnique)
               . betaCon        = TVar (@lhs.betaUnique + 1)
               . conApply       = [ (@betaCon .==. foldr (.->.) @beta @patterns.betas) 
                                    (if @patterns.numberOfPatterns == 0  then @cinfoEmpty else @cinfoApply) ]             
               . conConstructor = case M.lookup @name.self (valueConstructors @lhs.importEnvironment) of
                                     Nothing  -> []
                                     Just ctp -> [ (@betaCon .::. ctp) @cinfoConstructor ]

  | As
      lhs     . environment = M.insert @name.self @beta @pattern.environment          
      pattern . betaUnique  = @lhs.betaUnique + 1
      loc     . constraints = @newcon .>.
                              Node [ Receive @lhs.betaUnique
                                   , @pattern.constraints
                                   ]
              . beta        = TVar @lhs.betaUnique
              . newcon      = [ (@beta .==. @pattern.beta) @cinfo ]

  | Wildcard
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = noAssumptions
      loc . constraints = emptyTree
          . beta        = TVar @lhs.betaUnique

  | List
      patterns . betaUnique   = @lhs.betaUnique + 2
      loc      . constraints  = @newcon .>.
                                Node (zipWith3 @zipf @patterns.betas [0..] @patterns.constraintslist)
               . beta         = TVar @lhs.betaUnique
               . beta'        = TVar (@lhs.betaUnique + 1)
               . newcon       = [ (listType @beta' .==. @beta) @cinfoResult ]
               . zipf         = \tp elemNr ctree -> [ (tp .==. @beta') (@cinfoElem elemNr) ] .<. ctree

  | Tuple    
      patterns . betaUnique  = @lhs.betaUnique + 1
      loc      . constraints = @newcon .>. Node @patterns.constraintslist
               . beta        = TVar @lhs.betaUnique
               . newcon      = [ (tupleType @patterns.betas .==. @beta) @cinfo ]

  | Negate
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = noAssumptions
      loc . constraints = listTree @newcon
          . beta        = TVar @lhs.betaUnique
          . newcon      = -- The parser only accepts a literal after '-' in a Pattern
                          -- search for the type of 'negate' in the import envionment: otherwise use the default type.
                          let standard = makeScheme [] [Predicate "Num" (TVar 0)] (TVar 0 .->. TVar 0)
                              tpscheme = M.findWithDefault standard (nameFromString "negate") (typeEnvironment @lhs.importEnvironment)
                          in [ (@literal.literalType .->. @beta .::. tpscheme) @cinfo]
          
{- only if type inferencing without overloading -}
  | NegateFloat
      lhs . betaUnique  = @lhs.betaUnique + 1
          . environment = noAssumptions
      loc . constraints = listTree @newcon
          . beta        = TVar @lhs.betaUnique
          . newcon      = -- The parser only accepts a literal after '-.' in a Pattern
                          [ (floatType .==. @beta) @cinfo ]

SEM Patterns

  | Cons
      lhs . betas            = @hd.beta : @tl.betas
          . environment      = @hd.environment `M.union` @tl.environment
          . numberOfPatterns = 1 + @tl.numberOfPatterns
          . constraintslist  = @hd.constraints : @tl.constraintslist

  | Nil
      lhs . betas            = []
          . environment      = noAssumptions
          . numberOfPatterns = 0
          . constraintslist  = []

---------------------------------------------------------------------------------------
-- Type Inferencing : Alternative, Alternatives

ATTR Alternative Alternatives [ betaLeft:Tp betaRight:Tp monos:Monos | betaUnique:Int | assumptions:Assumptions ]
ATTR Alternative              [ | | constraints:ConstraintSet ]
ATTR             Alternatives [ | | constraintslist:ConstraintSets ]

SEM Alternative

  | Hole
      lhs . assumptions = noAssumptions
      loc . constraints = emptyTree

  | Alternative
      righthandside . monos       = M.elems @pattern.environment ++ getMonos @csetBinds ++ @lhs.monos
      loc           . constraints = @csetBinds .>>.
                                    Node [ @conLeft  .<. @pattern.constraints
                                         , @righthandside.constraints
                                         ]                     
                    . conLeft     = [ (@pattern.beta .==. @lhs.betaLeft) @cinfoLeft ]
      (loc.csetBinds,lhs.assumptions) = (@pattern.environment .===. @righthandside.assumptions) @cinfoBind                    

  | Empty
      lhs . assumptions = noAssumptions
      loc . constraints = emptyTree

SEM Alternatives

  | Cons
      lhs . assumptions     = @hd.assumptions `combine` @tl.assumptions
          . constraintslist = @hd.constraints : @tl.constraintslist

  | Nil
      lhs . assumptions     = noAssumptions
          . constraintslist = []

---------------------------------------------------------------------------------------
-- Type Inferencing : Statement, Statements, Qualifier, Qualifiers

ATTR Statement Statements Qualifier Qualifiers [ | assumptions:Assumptions betaUnique:Int constraints:ConstraintSet | ]
ATTR Statement Statements                      [ | generatorBeta:{Maybe Tp} | ]
ATTR Statement            Qualifier Qualifiers [ | monos:Monos | ]
ATTR           Statements                      [ monos:Monos | | ]

SEM Statement

  | Expression
      lhs        . generatorBeta  = Just @beta
                 . assumptions    = @lhs.assumptions `combine` @expression.assumptions
                 . constraints    = @locConstraints
      expression . betaUnique     = @lhs.betaUnique + 1
      loc        . locConstraints = Node [ @newcon .<. @expression.constraints
                                         , @lhs.constraints
                                         ]
                 . beta           = TVar @lhs.betaUnique
                 . newcon         = [ (@expression.beta .==. ioType @beta) @cinfo ]

  | Let
      lhs          . generatorBeta  = Nothing
      declarations . bindingGroups  = []      
      (lhs.assumptions, lhs.constraints, loc.inheritedBDG, loc.chunkNr, lhs.betaUnique, loc.implicitsFM) = 
         let inputBDG    = (False, @lhs.currentChunk, @declarations.uniqueChunk, @lhs.monos, @declarations.typeSignatures, mybdggroup, @declarations.betaUnique)
             mybdggroup = Just (@lhs.assumptions, [@lhs.constraints])
         in performBindingGroup inputBDG @declarations.bindingGroups
                        
                   

  | Generator
      lhs . generatorBeta = Nothing
          . constraints   = @locConstraints
          . assumptions   = @assumptions' `combine` @expression.assumptions
          . monos         = M.elems @pattern.environment ++ getMonos @csetBinds ++ @lhs.monos
      loc . locConstraints = @newcon .>. @csetBinds .>>.
                                Node [ @pattern.constraints
                                     , @expression.constraints
                                     , @lhs.constraints
                                     ]
          . newcon        = [ (@expression.beta .==. ioType @pattern.beta) @cinfoResult ]
          . (csetBinds,assumptions') = (@pattern.environment .===. @lhs.assumptions) @cinfoBind

SEM Statements

  | Cons
      lhs . assumptions = @hd.assumptions
          . constraints = @hd.constraints
      hd  . assumptions = @tl.assumptions
          . constraints = @tl.constraints
      tl  . assumptions = @lhs.assumptions
          . constraints = @lhs.constraints

SEM Qualifier

  | Guard
      lhs . assumptions = @lhs.assumptions `combine` @guard.assumptions
          . constraints = @locConstraints
      loc . locConstraints = Node [ @newcon .<. @guard.constraints
                                  , @lhs.constraints
                                  ]
          . newcon      = [ (@guard.beta .==. boolType) @cinfo ]

  | Let   declarations . bindingGroups  = []
          (lhs.assumptions, lhs.constraints, loc.inheritedBDG, loc.chunkNr, lhs.betaUnique, loc.implicitsFM) = 
             let inputBDG   = (False, @lhs.currentChunk, @declarations.uniqueChunk, @lhs.monos, @declarations.typeSignatures, mybdggroup, @declarations.betaUnique)
                 mybdggroup = Just (@lhs.assumptions, [@lhs.constraints])
             in performBindingGroup inputBDG @declarations.bindingGroups


  | Generator
      lhs . assumptions = @assumptions' `combine` @expression.assumptions
          . constraints = @locConstraints
          . monos       = M.elems @pattern.environment ++ getMonos @csetBinds ++ @lhs.monos
      loc . locConstraints = @newcon .>. @csetBinds .>>.
                                Node [ @pattern.constraints
                                     , @expression.constraints
                                     , @lhs.constraints
                                     ]
          . (csetBinds,assumptions') = (@pattern.environment .===. @lhs.assumptions) @cinfoBind
          . newcon      = [ (@expression.beta .==. listType @pattern.beta) @cinfoResult ]

SEM Qualifiers

  | Cons
      lhs . assumptions = @hd.assumptions
          . constraints = @hd.constraints
      hd  . assumptions = @tl.assumptions
          . constraints = @tl.constraints
      tl  . assumptions = @lhs.assumptions
          . constraints = @lhs.constraints

---------------------------------------------------------------------------------------
-- Type Inferencing : Literal

ATTR Literal [ | | literalType:Tp ]

SEM Literal
  | Int     lhs . literalType = intType
  | Char    lhs . literalType = charType
  | String  lhs . literalType = stringType
  | Float   lhs . literalType = floatType