From e29f98f682fc83cc63fa9d6b398490e846e38bc8 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 18 Mar 2022 12:55:28 -0700 Subject: [PATCH] Restore special cases to tuple operations in Heapster/SAWTranslation. This avoids construction of 1-tuples. This makes many of the example proof scripts work again. --- .../src/Verifier/SAW/Heapster/SAWTranslation.hs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs index 02e3c17010..71e00cbea8 100644 --- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs +++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs @@ -133,18 +133,27 @@ typeTransType1 (TypeTrans [] _) = unitTypeOpenTerm typeTransType1 (TypeTrans [tp] _) = tp typeTransType1 _ = error ("typeTransType1" ++ nlPrettyCallStack callStack) --- | Build the tuple type @#(T1, T2, ... Tn-1, Tn)@ of @n@ types. +-- | Build the tuple type @#(T1, T2, ... Tn-1, Tn)@ of @n@ types, with +-- the special case that 0 types maps to the unit type @#()@ (and 1 +-- type just maps to itself). tupleOfTypes :: [OpenTerm] -> OpenTerm +tupleOfTypes [] = unitTypeOpenTerm +tupleOfTypes [tp] = tp tupleOfTypes tps = tupleTypeOpenTerm tps --- | Build the tuple @(t1, t2, ..., tn-1, tn)@ of @n@ terms. +-- | Build the tuple @(t1, t2, ..., tn-1, tn)@ of @n@ terms, with the +-- special case that 0 types maps to the unit value @()@ (and 1 value +-- just maps to itself). tupleOfTerms :: [OpenTerm] -> OpenTerm +tupleOfTerms [] = unitOpenTerm +tupleOfTerms [t] = t tupleOfTerms ts = tupleOpenTerm ts -- | Project the @i@th element from a term of type @'tupleOfTypes' tps@. Note -- that this requires knowing the length of @tps@. projTupleOfTypes :: [OpenTerm] -> Integer -> OpenTerm -> OpenTerm projTupleOfTypes tps i tup + | i == 0 && length tps == 1 = tup | i < toInteger (length tps) = projTupleOpenTerm i tup | otherwise = error "projTupleOfTypes: invalid tuple index"