helium-1.8: src/Helium/StaticAnalysis/Directives/TS_Apply.ag
-----------------------------------------------------------------------------
-- |The Helium Compiler : Static Analysis
--
-- Maintainer : bastiaan@cs.uu.nl
-- Stability : experimental
-- Portability : unknown
--
-- Apply specialized type rules during the type inference process.
--
-- (directives based on "Scripting the Type Inference Process", ICFP 2003)
-----------------------------------------------------------------------------
INCLUDE "TS_CoreSyntax.ag"
imports {
import Helium.Syntax.UHA_Syntax
import Helium.StaticAnalysis.Miscellaneous.TypeConstraints
import Helium.StaticAnalysis.Miscellaneous.ConstraintInfo
import Data.List
import Helium.Utils.Utils (internalError)
import Helium.StaticAnalysis.Messages.Messages
import Helium.StaticAnalysis.Messages.TypeErrors
import Helium.ModuleSystem.ImportEnvironment
import Helium.StaticAnalysis.Inferencers.BindingGroupAnalysis (Assumptions, combine, noAssumptions)
import Helium.Parser.OperatorTable (OperatorTable)
import Helium.Parser.Parser (exp_)
import Helium.Parser.Lexer (strategiesLexer)
import Helium.Parser.ParseLibrary (runHParser)
import qualified Helium.Parser.ResolveOperators as ResolveOperators
import qualified Data.Map as M
import Helium.StaticAnalysis.Directives.TS_Attributes
import Helium.StaticAnalysis.Directives.TS_CoreSyntax
import Top.Ordering.Tree
}
{
applyTypingStrategy :: Core_TypingStrategy -> MetaVariableInfo -> MetaVariableTable -> Int
-> (Assumptions, ConstraintSet, IO (), Int)
applyTypingStrategy strategy infoTuple metaVar unique =
let res = wrap_Core_TypingStrategy (sem_Core_TypingStrategy strategy)
Inh_Core_TypingStrategy {
infoTuple_Inh_Core_TypingStrategy = infoTuple,
metaVariableTable_Inh_Core_TypingStrategy = metaVar,
unique_Inh_Core_TypingStrategy = unique }
in (assumptions_Syn_Core_TypingStrategy res, constraintSet_Syn_Core_TypingStrategy res, debugIO_Syn_Core_TypingStrategy res, unique_Syn_Core_TypingStrategy res)
matchInformation :: ImportEnvironment -> Core_TypingStrategy -> [(Expression, [String])]
matchInformation importEnvironment typingStrategy =
case typingStrategy of
TypingStrategy _ (TypeRule premises conclusion) _ ->
let Judgement exprstring _ = conclusion
expression = expressionParser (operatorTable importEnvironment) exprstring
metas = [ s | Judgement s _ <- premises ]
in [(expression, metas)]
_ -> []
expressionParser :: OperatorTable -> String -> Expression
expressionParser theOperatorTable string =
case strategiesLexer [] "TS_Apply" string of
Left _ -> intErr
Right (tokens, _) ->
case runHParser exp_ "TS_Apply" tokens True {- wait for EOF -} of
Left _ -> intErr
Right expression ->
ResolveOperators.expression theOperatorTable expression
where
intErr = internalError "TS_Apply.ag" "n/a" ("unparsable expression: "++show string)
}
ATTR Core_TypingStrategy
[ infoTuple : MetaVariableInfo
metaVariableTable : MetaVariableTable
| unique : Int
| assumptions : Assumptions
constraintSet : ConstraintSet
debugIO : {IO ()}
]
SEM Core_TypingStrategy
| Siblings
lhs . assumptions = noAssumptions
. constraintSet = emptyTree
. debugIO = return ()
| TypingStrategy
lhs . assumptions = foldr combine noAssumptions (map (getAssumptions . snd) @lhs.metaVariableTable)
. constraintSet = Node @allConstraintTrees
. unique = length @normalTV + @lhs.unique
. debugIO = putStrLn "applying typing strategy"
loc . substitution = listToSubstitution (@standardSubst ++ @specialSubst)
. allTV = @typerule.ftv `union` @statements.ftv `union` ftv (map snd @typeEnv)
{- judgement with only a type variable should not introduce a new constraint -}
. specialTV = concat . exactlyOnce . map ftv . filter isTVar . map snd $ @typerule.judgements
. normalTV = @allTV \\ @specialTV
. standardSubst = zip @normalTV (map TVar [@lhs.unique..])
. specialSubst = let conclusionVar = case snd (last @typerule.judgements) of
TVar i -> Just i
_ -> Nothing
find' i | Just i == conclusionVar = [ (i, getType @lhs.infoTuple) ]
| otherwise = [ (i, getType infoTuple)
| (s1, TVar j) <- @typerule.judgements
, i == j
, (s2,infoTuple) <- @lhs.metaVariableTable
, s1 == s2
]
in concatMap find' @specialTV
ATTR Core_TypeRule Core_Judgements Core_Judgement Core_UserStatements Core_UserStatement
[ substitution : MapSubstitution
infoTuple : MetaVariableInfo
metaVariableTable : MetaVariableTable
|
| ftv USE {`union`} {[]} : {[Int]}
]
SEM Core_UserStatement
| Equal lhs . ftv = ftv [@leftType, @rightType]
SEM Core_Judgement
| Judgement lhs . ftv = ftv @type
ATTR Core_UserStatements Core_UserStatement
[ fromAttribute : {Attribute -> MessageBlock}
| collectConstraints : {Trees (TypeConstraint ConstraintInfo)}
currentPhase : {Maybe Int}
currentPosition : {(Int, Int)}
metavarConstraints : {[(String,Tree (TypeConstraint ConstraintInfo))]}
|
]
SEM Core_TypingStrategy
| TypingStrategy
loc.allConstraintTrees =
listTree (reverse @typerule.constraints) :
Phase 999 @patchConstraints :
(map snd @statements.metavarConstraints) ++
(reverse @statements.collectConstraints)
loc.patchConstraints =
let parent = concat (M.elems (getAssumptions @lhs.infoTuple))
children = concat (concatMap (M.elems . getAssumptions . snd) @lhs.metaVariableTable)
(ns, tps1) = unzip (parent \\ children)
(ss, tps2) = unzip @typeEnv
zipF t1 t2 = (t1 .==. @substitution |-> t2) infoF
infoF = emptyConstraintInfo
{ location = "Typing Strategy (patch)" }
err = internalError "TS_Apply.ag" "n/a" "the type environments do not match"
in if (map show ns /= ss) then err else
zipWith zipF tps1 tps2
statements . collectConstraints = []
. currentPhase = Nothing
. currentPosition = (@lhs.unique, 0)
. metavarConstraints = [ (s, getConstraintSet info) | (s, info) <- @lhs.metaVariableTable ]
. fromAttribute = let locals = map f (dom @substitution)
f i = (show i, MessageType (toTpScheme (lookupInt i @substitution)))
in toMessageBlock locals @lhs.infoTuple @lhs.metaVariableTable
SEM Core_UserStatement
| Equal
lhs . currentPosition = (\(x, y) -> (x, y+1)) @lhs.currentPosition
. collectConstraints = case @lhs.currentPhase of
Just phase | phase /= 5
-> Phase phase [ @newConstraint ] : @lhs.collectConstraints
_ -> unitTree @newConstraint : @lhs.collectConstraints
| Pred
lhs . collectConstraints = unitTree @newConstraint : @lhs.collectConstraints
loc . newConstraint =
let cinfo = setTypeError (TypeError [] message [] [])
$ addProperty (ReductionErrorInfo thePred)
$ emptyConstraintInfo
thePred = Predicate @predClass (@lhs.substitution |-> @predType)
message = let f = MessageOneLiner . substituteAttributes @lhs.fromAttribute
in map f (lines @message)
in predicate thePred cinfo
| MetaVariableConstraints
lhs . metavarConstraints = filter ((@name /=) . fst) @lhs.metavarConstraints
. collectConstraints = case lookup @name @lhs.metavarConstraints of
Just tree -> tree : @lhs.collectConstraints
Nothing -> internalError "TS_Apply.ag" "n/a" "unknown constraint set"
| CorePhase
lhs . currentPhase = Just @phase
SEM Core_UserStatement
| Equal
loc . newConstraint =
let cinfo = setTypeError (TypeError [] message [] [])
$ addProperty (uncurry IsUserConstraint @lhs.currentPosition)
$ inPhase emptyConstraintInfo
inPhase = case @lhs.currentPhase of
Just phase | phase /= 5
-> addProperty (ConstraintPhaseNumber phase)
_ -> id
message = let f = MessageOneLiner . substituteAttributes @lhs.fromAttribute
in map f (lines @message)
in (@lhs.substitution |-> @leftType .==. @lhs.substitution |-> @rightType) cinfo
ATTR Core_TypeRule [ | | constraints : {TypeConstraints ConstraintInfo} ]
SEM Core_TypeRule
| TypeRule
lhs.constraints =
let conclusionSource = self (getLocalInfo @lhs.infoTuple)
conclusionType = getType @lhs.infoTuple
in [ (stp1 .==. conclusionType)
(addProperty FolkloreConstraint $ defaultConstraintInfo (conclusionSource, Nothing))
| (_, tp1) <- @conclusion.judgements
, let stp1 = @lhs.substitution |-> tp1
, stp1 /= conclusionType -- don't generate trivial constraints
] ++
[ (getType mvinfo .==. stp1)
(defaultConstraintInfo (conclusionSource, Just (self (getLocalInfo mvinfo))))
| (s1, tp1) <- @premises.judgements
, (s2, mvinfo) <- @lhs.metaVariableTable
, s1 == s2
, let stp1 = @lhs.substitution |-> tp1
, getType mvinfo /= stp1 -- don't generate trivial constraints
]
{
exactlyOnce :: Eq a => [a] -> [a]
exactlyOnce [] = []
exactlyOnce (x:xs) | x `elem` xs = exactlyOnce . filter (/= x) $ xs
| otherwise = x : exactlyOnce xs
}
ATTR Core_Judgements Core_Judgement Core_TypeRule [ | | judgements USE {++} {[]} : {[(String, Tp)]} ]
SEM Core_Judgement
| Judgement
lhs . judgements = [(@expression, @type)]