----------------------------------------------------------------------------- -- |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)]