use unsorted equality for string literals

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

Hide file tree

Showing 2 changed files with 16 additions and 16 deletions.
diff --git a/src/Language/Haskell/Liquid/Constraint/Generate.hs b/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -1453,8 +1453,8 @@ consE γ (Var x)
        addLocA (Just x) (loc γ) (varAnn γ x t)
        return t
 
-consE γ (Lit c)
-  = refreshVV $ uRType $ literalFRefType (emb γ) c
+consE _ (Lit c)
+  = refreshVV $ uRType $ literalFRefType c
 
 consE γ e'@(App e (Type τ))
   = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e
@@ -1686,7 +1686,7 @@ caseEnv γ x acs a _
        cγ     <- addBinders γ x' [(x', xt')]
        return cγ
 
-altReft γ _ (LitAlt l)   = literalFReft (emb γ) l
+altReft _ _ (LitAlt l)   = literalFReft l
 altReft γ acs DEFAULT    = mconcat [notLiteralReft l | LitAlt l <- acs]
   where notLiteralReft   = maybe mempty F.notExprReft . snd . literalConst (emb γ)
 altReft _ _ _            = error "Constraint : altReft"

diff --git a/src/Language/Haskell/Liquid/Literals.hs b/src/Language/Haskell/Liquid/Literals.hs
@@ -29,19 +29,19 @@ makeRTypeBase (TyConApp c ts) x
 makeRTypeBase _              _
   = error "RefType : makeRTypeBase"
 
-literalFRefType tce l
-  = makeRTypeBase (literalType l) (addStrLen l $ literalFReft tce l)
-
-literalFReft tce = maybe mempty F.exprReft . snd . literalConst tce
-
-addStrLen l = F.meet r
-  where
-    r = case l of
-          MachStr str ->
-            F.reft "v" (F.PAtom F.Eq
-                        (F.EApp (name strLen) [F.EVar "v"])
-                        (F.ECon (F.I (fromIntegral (T.length $ T.decodeUtf8 str)))))
-          _ -> mempty
+literalFRefType l
+  = makeRTypeBase (literalType l) (literalFReft l)
+
+literalFReft l = maybe mempty mkReft $ mkLit l
+
+mkReft e = case e of
+            F.ESym (F.SL str) ->
+              -- FIXME: unsorted equality is shady, better to not embed Add# as int..
+              F.meet (F.uexprReft e)
+                     (F.reft "v" (F.PAtom F.Eq
+                                  (F.EApp (name strLen) [F.EVar "v"])
+                                  (F.ECon (F.I (fromIntegral (T.length str))))))
+            _ -> F.exprReft e
 
 -- | `literalConst` returns `Nothing` for unhandled lits because
 --    otherwise string-literals show up as global int-constants