re-add unsorted equality to type of unpackCString

ucsd-progsys · Jul 13, 2015 · 5cb3d80 · 5cb3d80
1 parent 18d264f
commit 5cb3d80
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/include/GHC/CString.spec b/include/GHC/CString.spec
@@ -4,4 +4,4 @@ import GHC.Prim
 
 GHC.CString.unpackCString#
   :: x:GHC.Prim.Addr#
-  -> {v:String | len v == strLen x}
+  -> {v:[Char] | v ~~ x && len v == strLen x}
diff --git a/src/Language/Haskell/Liquid/ANFTransform.hs b/src/Language/Haskell/Liquid/ANFTransform.hs
@@ -125,11 +125,11 @@ normalizeName :: VarEnv Id -> CoreExpr -> DsMW CoreExpr
 -- normalizeNameDebug γ e 
 --   = liftM (tracePpr ("normalizeName" ++ showPpr e)) $ normalizeName γ e
 
-normalizeName _ e@(Lit _)
-  = normalizeLiteral e
-
-normalizeName _ e@(Tick _ (Lit _))
+normalizeName _ e@(Lit l)
+  | shouldNormalize l
   = normalizeLiteral e
+  | otherwise
+  = return e
 
 normalizeName γ (Var x)
   = return $ Var (lookupWithDefaultVarEnv γ x x)
@@ -152,6 +152,10 @@ normalizeName γ e
        add [NonRec x e']
        return $ Var x
 
+shouldNormalize l = case l of
+  LitInteger _ _ -> True
+  MachStr _ -> True
+  _ -> False
 
 add :: [CoreBind] -> DsMW ()
 add w = modify $ \s -> s{st_binds = st_binds s++w}

diff --git a/src/Language/Haskell/Liquid/CoreToLogic.hs b/src/Language/Haskell/Liquid/CoreToLogic.hs
@@ -388,6 +388,7 @@ isUndefined (_, _, e) = isUndefinedExpr e
   where 
    -- auto generated undefined case: (\_ -> (patError @type "error message")) void
    isUndefinedExpr (C.App (C.Var x) _) | (show x) `elem` perrors = True
+   isUndefinedExpr (C.Let _ e) = isUndefinedExpr e
    -- otherwise 
    isUndefinedExpr _ = False