liquid-fixpoint 0.7.0.6 → 0.7.0.7

raw patch · 5 files changed

+38/−31 lines, 5 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• liquid-fixpoint.cabal +1/−1
• src/Language/Fixpoint/Solver/Instantiate.hs +11/−27
• src/Language/Fixpoint/SortCheck.hs +2/−2
• src/Language/Fixpoint/Types/Names.hs +1/−1
• src/Language/Fixpoint/Types/Visitor.hs +23/−0

@@ -1,5 +1,5 @@ name:                liquid-fixpoint-version:             0.7.0.6+version:             0.7.0.7 Copyright:           2010-17 Ranjit Jhala, University of California, San Diego. synopsis:            Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage:            https://github.com/ucsd-progsys/liquid-fixpoint

@@ -65,7 +65,7 @@   where     (is, ps)         = unzip ips     (ps', axs)       = defuncAxioms cfg env ps-    ps''             = elaborate "PLE1" env <$> ps'+    ps''             = zipWith (\i -> elaborate ("PLE1 " ++ show i) env) is ps' -- <$> ps'     axs'             = elaborate "PLE2" env <$> axs     fi'              = fi { asserts = axs' ++ asserts fi } @@ -416,40 +416,24 @@ substEqCoerce eq es bd = do   env      <- seSort <$> gets evEnv   let ts    = snd    <$> eqArgs eq-  let coSub = mkCoSub env es ts-  return    $ applyCoSub coSub bd---- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'---   to the ty-vars that they should be substituted with. Note the---   domain and range are both Symbol and not the Int used for real ty-vars.--type CoSub = M.HashMap Symbol Symbol+  let sp    = panicSpan "mkCoSub"+  let eTs   = sortExpr sp env <$> es+  let coSub = notracepp ("substEqCoerce" ++ showpp (eqName eq, es, eTs, ts)) $ mkCoSub eTs ts+  return    $ Vis.applyCoSub coSub bd -mkCoSub :: SEnv Sort -> [Expr] -> [Sort] -> CoSub-mkCoSub env es xTs = Misc.safeFromList "mkCoSub" xys+mkCoSub :: [Sort] -> [Sort] -> Vis.CoSub+mkCoSub eTs xTs = Misc.safeFromList "mkCoSub" xys   where-    eTs            = sortExpr sp env <$> es-    sp             = panicSpan "mkCoSub"-    xys            = concat (zipWith matchSorts xTs eTs)+    xys         = concat (zipWith matchSorts xTs eTs) -matchSorts :: Sort -> Sort -> [(Symbol, Symbol)]-matchSorts = go+matchSorts :: Sort -> Sort -> [(Symbol, Sort)]+matchSorts s1 s2 = notracepp ("matchSorts :" ++ show (s1, s2)) $ go s1 s2   where-    go (FObj x)      (FObj y)      = [(x, y)]+    go (FObj x)      {-FObj-} y    = [(x, y)]     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2     go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2     go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2     go _             _             = []--applyCoSub :: CoSub -> Expr -> Expr-applyCoSub coSub      = Vis.mapExpr fE-  where-    fE (ECoerc s t e) = ECoerc (txS s) (txS t) e-    fE e              = e-    txS               = Vis.mapSort fS-    fS (FObj a)       = FObj   (txV a)-    fS t              = t-    txV a             = M.lookupDefault a a coSub  -------------------------------------------------------------------------------- getEqBody :: Equation -> Maybe Expr

@@ -450,13 +450,13 @@   ps' <- mapM (elab f) ps   return (POr (fst <$> ps'), boolSort) -elab f@(_,g) e@(PAtom Eq e1 e2) = do+elab f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do   t1        <- checkExpr g e1   t2        <- checkExpr g e2   (t1',t2') <- unite g e  t1 t2 `withError` (errElabExpr e)   e1'       <- elabAs f t1' e1   e2'       <- elabAs f t2' e2-  return (PAtom Eq (ECst e1' t1') (ECst e2' t2') , boolSort)+  return (PAtom eq (ECst e1' t1') (ECst e2' t2') , boolSort)  elab f (PAtom r e1 e2)   | r == Ueq || r == Une = do

@@ -240,7 +240,7 @@ type LocText   = Located T.Text  isDummy :: (Symbolic a) => a -> Bool-isDummy a = symbol a == symbol dummyName+isDummy a = isPrefixOfSym (symbol dummyName) (symbol a)  instance Symbolic a => Symbolic (Located a) where   symbol = symbol . val

@@ -33,6 +33,10 @@   , mapKVars, mapKVars', mapGVars', mapKVarSubsts   , mapExpr, mapMExpr +  -- * Coercion Substitutions+  , CoSub+  , applyCoSub+   -- * Predicates on Constraints   , isConcC , isKvarC @@ -318,6 +322,25 @@ --  where --    go (ECst e _) = e --    go e          = e++--------------------------------------------------------------------------------+-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'+--   to the ty-vars that they should be substituted with. Note the+--   domain and range are both Symbol and not the Int used for real ty-vars.+--------------------------------------------------------------------------------++type CoSub = M.HashMap Symbol Sort -- Symbol++applyCoSub :: CoSub -> Expr -> Expr+applyCoSub coSub      = mapExpr fE+  where+    fE (ECoerc s t e) = ECoerc  (txS s) (txS t) e+    fE (ELam (x,t) e) = ELam (x, txS t)         e+    fE e              = e+    txS               = mapSort fS+    fS (FObj a)       = {- FObj -} (txV a)+    fS t              = t+    txV a             = M.lookupDefault (FObj a) a coSub  --------------------------------------------------------------------------------- -- | Visitors over @Sort@