Lift specification on tuple elements outside of the tuple

src/G2/Liquid/Inference/GeneratedSpecs.hs

@@ -1,7 +1,7 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module G2.Liquid.Inference.GeneratedSpecs ( GeneratedSpecs
+module G2.Liquid.Inference.GeneratedSpecs ( GeneratedSpecs (..)
  , emptyGS
  , namesGS
 

src/G2/Liquid/Inference/Sygus/LiaSynth.hs

@@ -574,10 +574,72 @@ sySpecNamesForModel sys =
 modelToGS :: M.Map Name SpecInfo -> SMTModel -> GeneratedSpecs
 modelToGS m_si mdl =
  let
- lh_spec = M.map (\si -> buildLIA_LH si mdl) . M.filter (\si -> s_status si == Synth) $ m_si
+ lh_spec = M.map (\si -> liftTupleSpecs si $ buildLIA_LH si mdl) . M.filter (\si -> s_status si == Synth) $ m_si
  in
  M.foldrWithKey insertAssertGS emptyGS lh_spec
 
+-- | Only use measures for tuple specs
+liftTupleSpecs :: SpecInfo -> [PolyBound LHF.Expr] -> [PolyBound LHF.Expr]
+liftTupleSpecs si = map (uncurry3 liftTupleSpecs')
+ . zip3 (s_type_pre si ++ [s_type_post si]) (s_syn_pre si ++ [s_syn_post si])
+
+liftTupleSpecs' :: Type -> PolyBound SynthSpec -> PolyBound LHF.Expr -> PolyBound LHF.Expr
+liftTupleSpecs' t sy_spec pbe | Just i <- tupleCount (tyAppCenter t) =
+ liftTupleSpecs'' i
+ (map lh_rep . sy_rets $ headValue sy_spec)
+ (headValue pbe)
+ (removeHead sy_spec)
+ (removeHead pbe)
+ | otherwise = pbe
+
+tupleCount :: Type -> Maybe Int
+tupleCount (TyCon (Name n _ _ _) _)
+ | Just ('(', _) <- T.uncons n
+ , T.last n == ')'
+ , T.all (== ',') (T.init $ T.tail n) = Just (T.length n - 2)
+tupleCount _ = Nothing
+
+liftTupleSpecs'' :: Int
+ -> [LH.Expr] -- ^ Tuple extractors, i.e. x_Tuple##
+ -> LH.Expr
+ -> [PolyBound SynthSpec]
+ -> [PolyBound LHF.Expr]
+ -> PolyBound LH.Expr
+liftTupleSpecs'' tuple_size extractors e pb_syspec pb_e =
+ let
+ extract_ns = map (\j -> LHF.symbol $ "x_Tuple" ++ show tuple_size ++ show j) [1..tuple_size]
+ e' = map (uncurry3 liftTupleSpecs''') $ zip3 extractors (map headValue pb_syspec) (map headValue pb_e)
+ in
+ PolyBound (PAnd $ e:e') $ map (\(PolyBound _ ps) -> PolyBound LHF.PTrue ps) pb_e
+
+liftTupleSpecs''' :: LHF.Expr -> SynthSpec -> LHF.Expr -> LHF.Expr
+liftTupleSpecs''' _ (SynthSpec { sy_rets = [] }) = id
+liftTupleSpecs''' extracter (SynthSpec { sy_rets = (SpecArg { lh_rep = rep }):_}) = go
+ where
+ go e | e == rep = extracter
+ go e@(ESym _) = e
+ go e@(ECon _) = e
+ go e@(EVar _) = e
+ go (EApp e1 e2) = EApp (go e1) (go e2)
+ go (ENeg e) = ENeg (go e)
+ go (EBin bop e1 e2) = EBin bop (go e1) (go e2)
+ go (EIte e1 e2 e3) = EIte (go e1) (go e2) (go e3)
+ go (ECst e s) = ECst (go e) s
+ go (ELam sy e) = ELam sy (go e)
+ go (ETApp e s) = ETApp (go e) s
+ go (ETAbs e s) = ETAbs (go e) s
+ go (PAnd es) = PAnd (map go es)
+ go (POr es) = POr (map go es)
+ go (PNot e) = PNot (go e)
+ go (PImp e1 e2) = PImp (go e1) (go e2)
+ go (PIff e1 e2) = PIff (go e1) (go e2)
+ go (PAtom brel e1 e2) = PAtom brel (go e1) (go e2)
+ go e@(PKVar _ _) = e
+ go (PAll s e) = PAll s (go e)
+ go (PExist s e) = PExist s (go e)
+ go (PGrad k sub g e) = PGrad k sub g (go e)
+ go (ECoerc s1 s2 e) = ECoerc s1 s2 (go e)
+
 -- | Generates an Assert that, when added to a formula with the relevant variables,
 -- blocks it from returning the model
 blockModelDirectly :: SMTModel -> SMTHeader

tests/LiquidInf/Paper/Eval/compare.py

@@ -84,12 +84,12 @@ def main():
  # log = log_test
  # (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "600", ["--use-invs"], skip = skip_list());
 
+ (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "600", ["--use-invs"]);
+ print(str(safe_compare) + "/" + str(num_compare) + " Safe");
+
  log_z3 = runZ3()
  log_chc = runCHC()
 
- (log_haskell, safe_compare, num_compare) = eval.test_pos_folder("tests/LiquidInf/Paper/Eval/Compare", "10", ["--use-invs"]);
- print(str(safe_compare) + "/" + str(num_compare) + " Safe");
-
  eval.create_table(log_haskell)
  eval.create_simple_table(log_haskell)
 

tests_lh/LHTest.hs

@@ -339,6 +339,7 @@ posInfTests = testGroup "Tests"
  , posTestInference "tests_lh/test_files/Pos/Test48.hs"
  , posTestInference "tests_lh/test_files/Pos/Test49.hs"
  , posTestInference "tests_lh/test_files/Pos/Test50.hs"
+ , posTestInference "tests_lh/test_files/Pos/Test51.hs"
 
  , posTestInference "tests_lh/test_files/Pos/Sets1.hs"
  , posTestInference "tests_lh/test_files/Pos/Sets2.hs"

tests_lh/test_files/Pos/Test51.hs

@@ -0,0 +1,21 @@
+{-@ LIQUID "--no-termination" @-}
+
+module Test51 (main) where
+
+data Peano = Succ | Nil
+
+{-@ main :: Bool -> { b : Bool | b } @-}
+main :: Bool -> Bool
+main xs = case while xs loop (1, 0, 0, 0) of
+ (w', z', x', y') -> x' <= 1
+
+while :: Bool -> (a -> a) -> a -> a
+while ys body x = if ys then while False body (body x) else x
+
+{-@ loop :: (Int, Int, Int, Int) -> (Int, Int, Int, Int) @-}
+loop :: (Int, Int, Int, Int) -> (Int, Int, Int, Int)
+loop (w, z, x, y) =
+ ( if w `mod` 2 == 1 then w + 1 else w
+ , if z `mod` 2 == 0 then z + 1 else z
+ , if w `mod` 2 == 1 then x + 1 else x
+ , if z `mod` 2 == 0 then y + 1 else y)