Skip to content
Browse files

fix a bunch, but not enough

  • Loading branch information...
1 parent 00891d7 commit 8f87763bf82fa68f382ae8037091077061df369c @bblum committed Nov 27, 2012
Showing with 44 additions and 14 deletions.
  1. +36 −8 Check.hs
  2. +6 −6 Constraints.hs
  3. +2 −0 todo.txt
View
44 Check.hs
@@ -76,7 +76,7 @@ instance Show Type where
argstr = case args of [] -> "unit"
_ -> intercalate ", " argstrs
in "(" ++ argstr ++ " -> " ++ show ret
- ++ " {" ++ maybe "???" show a' ++ "})"
+ ++ " {" ++ either show show a' ++ "})"
show (Pointer t) = show t ++ "*"
show (Struct (Just name) contence) =
"struct " ++ show name ++ " {" ++ show contence ++ "}"
@@ -312,6 +312,7 @@ restoreState oldstate =
modify (\s -> s { context = context oldstate, types = types oldstate })
-- TODO: deprecate
+-- TODO: merge effect constraints
mergeState :: NodeInfo -> Checker -> Checker -> State Checker ()
mergeState nobe state1 state2 =
let (g1,g2) = (context state1, context state2)
@@ -328,17 +329,40 @@ setTypes :: Map.Map TypeName Type -> State Checker ()
setTypes ts = modify (\s -> s { types = ts })
--
+-- Constraints
+--
+
+newRV :: String -> State Checker RV
+newRV desc = do rv <- nextRV <$> get
+ modify (\s -> s { nextRV = rv + 1 })
+ return $ RV rv desc
+newEV :: String -> State Checker EV
+newEV desc = do ev <- nextEV <$> get
+ modify (\s -> s { nextEV = ev + 1 })
+ return $ EV ev desc
+newUnknown :: String -> State Checker (RV,EV)
+newUnknown desc = do rv <- newRV desc; ev <- newEV desc; return (rv,ev)
+
+-- TODO: solve constraints progressively each time one is added?
+addConstraint :: Constraint -> State Checker ()
+addConstraint c = modify (\s -> s { constraints = c:(constraints s) })
+
+--
-- Messaging
--
emptyMsg = [] :: [String]
-msg :: (Show a) => String -> NodeInfo -> String -> [a] -> State Checker ()
-msg prefix nobe str noobs =
+filerowcol :: NodeInfo -> String
+filerowcol nobe =
let -- (row,col) = (posRow $ posOfNode nobe, posColumn $ posOfNode nobe)
row = posRow $ posOfNode nobe
file = case fileOfNode nobe of Just f -> f; Nothing -> "((unknown))"
- mess0 = prefix ++ ": at " ++ file ++ ":" ++ (show row) ++ ": " ++ str
+ in file ++ ":" ++ (show row)
+
+msg :: (Show a) => String -> NodeInfo -> String -> [a] -> State Checker ()
+msg prefix nobe str noobs =
+ let mess0 = prefix ++ ": at " ++ filerowcol nobe ++ ": " ++ str
mess = foldl (\output noob -> output ++ "\n\t" ++ show noob) mess0 noobs
in modify (\s -> s { msgs = mess:(msgs s) })
@@ -385,6 +409,7 @@ mergeType doDisjoin nobe t1@(Arrow args1 ret1 iv1 a1) t2@(Arrow args2 ret2 iv2 a
when (iv1 /= iv2) $ warn nobe "variadicity mismatch in fn merge" emptyMsg
let iv = iv1 || iv2
case (a1,a2) of
+ -- TODO constraint
(Just a1', Just a2') -> -- good case
case (if doDisjoin then disjoin else intersect) a1' a2' of
a@(Just _) -> return $ Arrow args ret iv a
@@ -411,6 +436,7 @@ mergeType doDisjoin nobe t1 t2 =
verifyAssign :: NodeInfo -> Bool -> Type -> Type -> State Checker ()
verifyAssign nobe subtyping t1@(Arrow args1 ret1 iv1 a1) t2@(Arrow args2 ret2 iv2 a2) =
let verifyAnnotation True =
+ -- TODO constraint
case (liftM2 subtype a1 a2) of
Just False ->
err nobe "illegal subtyped function pointer assignment"
@@ -470,6 +496,7 @@ verifyCall nobe a =
[M "target function" $ show a, M "while in context" $ show g]
-- Mashes an annotation into an arrow type that might already have one.
+-- TODO constraint
injectAnnotation :: NodeInfo -> Type -> Maybe Annotation -> State Checker Type
injectAnnotation nobe (Arrow args ret iv (Just a0)) (Just a) =
do warn nobe "multiply-differently-annotated function" [a0,a]
@@ -666,14 +693,14 @@ checkAttr (attr@(CAttr name es nobe)) =
return a'
else return Nothing
-checkAttrs :: NodeInfo -> [CAttr] -> State Checker (Maybe Annotation)
+checkAttrs :: NodeInfo -> [CAttr] -> State Checker (Either Annotation Unknown)
checkAttrs nobe attrs =
do annos <- catMaybes <$> mapM checkAttr attrs
case annos of
- [] -> return Nothing
- [a] -> return $ Just a
+ [] -> Right <$> (newUnknown $ filerowcol nobe)
+ [a] -> return $ Left a
a:rest -> do warn nobe "ignoring extra annotations" rest
- return $ Just a
+ return $ Left a
-- Declarators
-- When called from fundef, need to add the args to the context. otherwise not.
@@ -956,6 +983,7 @@ checkExpr (CCall e args nobe) =
when (length args /= length argtypes) $
warn nobe "argument number mismatch"
[M "expected" argtypes]
+ -- TODO constraints
case a' of
Just a ->
do verifyCall nobe a
View
12 Constraints.hs
@@ -27,15 +27,15 @@ instance Show EV where
show (EV _ name) = "E{" ++ name ++ "}"
-- The elements of constraint expressions. Can be variables or fixed constants.
-newtype R = R (Either RV R.Rule) deriving Eq
-newtype E = E (Either EV R.Effect) deriving Eq
+data R = RuleVar RV | RuleConst R.Rule deriving Eq
+data E = EffectVar EV | EffectConst R.Effect deriving Eq
instance Show R where
- show (R (Left rv)) = show rv
- show (R (Right rule)) = show rule
+ show (RuleVar rv) = show rv
+ show (RuleConst rule) = show rule
instance Show E where
- show (E (Left ev)) = show ev
- show (E (Right effect)) = show effect
+ show (EffectVar ev) = show ev
+ show (EffectConst effect) = show effect
-- Note: the "<=" in the rule constraint is the subtyping comparison, not
-- the numeric comparison, so it's reversed (e.g., infinity <= 0).
View
2 todo.txt
@@ -1,5 +1,7 @@
milestones:
get constraint solving working w/o flow control
+ add constraints where TODO constraints are
+ make current-context possibly symbolic
features:
when exiting ifs, effect1 == effect2. what about for?

0 comments on commit 8f87763

Please sign in to comment.
Something went wrong with that request. Please try again.