From 5c0f54e0816197af477ef4997e3c738bab96210e Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 5 Dec 2018 13:29:17 -0800 Subject: [PATCH] Nested tuples no longer put an extra unit type at the end. This makes the tuple type representation match other systems like lean more closely. --- prelude/Prelude.sawcore | 14 +++++++------- src/Verifier/SAW/SharedTerm.hs | 13 ++++++++++--- src/Verifier/SAW/Simulator/Value.hs | 9 ++++++--- src/Verifier/SAW/UntypedAST.hs | 10 +++++++--- 4 files changed, 30 insertions(+), 16 deletions(-) diff --git a/prelude/Prelude.sawcore b/prelude/Prelude.sawcore index 1d9088a0..d84bbb13 100644 --- a/prelude/Prelude.sawcore +++ b/prelude/Prelude.sawcore @@ -69,8 +69,8 @@ fst a b tup = tup.(1); snd : (a b : sort 0) -> a * b -> b; snd a b tup = tup.(2); -uncurry (a b c : sort 0) (f : a -> b -> c) : (#(a, b) -> c) - = (\ (x : #(a, b)) -> f x.1 x.2); +uncurry (a b c : sort 0) (f : a -> b -> c) : a * b -> c + = (\ (x : a * b) -> f x.(1) x.(2)); -------------------------------------------------------------------------------- @@ -859,13 +859,13 @@ expNat b e = Nat_cases Nat 1 (\ (e':Nat) -> \ (exp_b_e:Nat) -> mulNat b exp_b_e) e; -- | Natural division and modulus -primitive divModNat : Nat -> Nat -> #(Nat, Nat); +primitive divModNat : Nat -> Nat -> Nat * Nat; divNat : Nat -> Nat -> Nat; -divNat x y = (divModNat x y).1; +divNat x y = (divModNat x y).(1); modNat : Nat -> Nat -> Nat; -modNat x y = (divModNat x y).2; +modNat x y = (divModNat x y).(2); -- There are implicit constructors from integer literals. @@ -923,7 +923,7 @@ single = replicate 1; axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a x) i) x; -- Zip together two lists (truncating the longer of the two). -primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) #(a, b); +primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b); primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b; @@ -1089,7 +1089,7 @@ bvCarry n x y = bvult n (bvAdd n x y) x; bvSCarry : (n : Nat) -> bitvector (Succ n) -> bitvector (Succ n) -> Bool; bvSCarry n x y = and (boolEq (msb n x) (msb n y)) (xor (msb n x) (msb n (bvAdd (Succ n) x y))); -bvAddWithCarry : (n : Nat) -> bitvector n -> bitvector n -> #(Bool, bitvector n); +bvAddWithCarry : (n : Nat) -> bitvector n -> bitvector n -> Bool * bitvector n; bvAddWithCarry n x y = (bvCarry n x y, bvAdd n x y); axiom bvAddZeroL : (n : Nat) -> (x : bitvector n) -> Eq (bitvector n) (bvAdd n (bvNat n 0) x) x; diff --git a/src/Verifier/SAW/SharedTerm.hs b/src/Verifier/SAW/SharedTerm.hs index aece2d62..4e11f06d 100644 --- a/src/Verifier/SAW/SharedTerm.hs +++ b/src/Verifier/SAW/SharedTerm.hs @@ -1068,10 +1068,12 @@ scPairType sc x y = scFlatTermF sc (PairType x y) scTuple :: SharedContext -> [Term] -> IO Term scTuple sc [] = scUnitValue sc +scTuple _ [t] = return t scTuple sc (t : ts) = scPairValue sc t =<< scTuple sc ts scTupleType :: SharedContext -> [Term] -> IO Term scTupleType sc [] = scUnitType sc +scTupleType _ [t] = return t scTupleType sc (t : ts) = scPairType sc t =<< scTupleType sc ts scPairLeft :: SharedContext -> Term -> IO Term @@ -1084,11 +1086,16 @@ scPairSelector :: SharedContext -> Term -> Bool -> IO Term scPairSelector sc t False = scPairLeft sc t scPairSelector sc t True = scPairRight sc t -scTupleSelector :: SharedContext -> Term -> Int -> IO Term -scTupleSelector sc t i +scTupleSelector :: + SharedContext -> Term -> + Int {- ^ 1-based index -} -> + Int {- ^ tuple size -} -> + IO Term +scTupleSelector sc t i n + | n == 1 = return t | i == 1 = scPairLeft sc t | i > 1 = do t' <- scPairRight sc t - scTupleSelector sc t' (i - 1) + scTupleSelector sc t' (i - 1) (n - 1) | otherwise = fail "scTupleSelector: non-positive index" scFun :: SharedContext -> Term -> Term -> IO Term diff --git a/src/Verifier/SAW/Simulator/Value.hs b/src/Verifier/SAW/Simulator/Value.hs index d0104d45..370fe4da 100644 --- a/src/Verifier/SAW/Simulator/Value.hs +++ b/src/Verifier/SAW/Simulator/Value.hs @@ -171,11 +171,14 @@ instance Show Nil where vTuple :: VMonad l => [Thunk l] -> Value l vTuple [] = VUnit -vTuple (x:xs) = VPair x (ready (vTuple xs)) +vTuple [_] = error "vTuple: unsupported 1-tuple" +vTuple [x, y] = VPair x y +vTuple (x : xs) = VPair x (ready (vTuple xs)) vTupleType :: VMonad l => [Value l] -> Value l vTupleType [] = VUnitType -vTupleType (t:ts) = VPairType t (vTupleType ts) +vTupleType [t] = t +vTupleType (t : ts) = VPairType t (vTupleType ts) valPairLeft :: (VMonad l, Show (Extra l)) => Value l -> MValue l valPairLeft (VPair t1 _) = force t1 @@ -229,7 +232,7 @@ asFiniteTypeValue v = t2 <- asFiniteTypeValue v2 case t2 of FTTuple ts -> return (FTTuple (t1 : ts)) - _ -> Nothing + _ -> return (FTTuple [t1, t2]) VRecordType elem_tps -> FTRec <$> Map.fromList <$> mapM (\(fld,tp) -> (fld,) <$> asFiniteTypeValue tp) elem_tps diff --git a/src/Verifier/SAW/UntypedAST.hs b/src/Verifier/SAW/UntypedAST.hs index 449d4ec1..c1df8a56 100644 --- a/src/Verifier/SAW/UntypedAST.hs +++ b/src/Verifier/SAW/UntypedAST.hs @@ -217,17 +217,21 @@ asApp = go [] where go l (App t u) = go (u:l) t go l t = (t,l) --- | Build a tuple value @(x1, .., xn)@. TODO: unary tuples? +-- | Build a tuple value @(x1, .., xn)@. mkTupleValue :: Pos -> [Term] -> Term mkTupleValue p [] = UnitValue p +mkTupleValue _ [x] = x mkTupleValue p (x:xs) = PairValue (pos x) x (mkTupleValue p xs) --- | Build a tuple type @#(x1, .., xn)@. TODO: unary tuples? +-- | Build a tuple type @#(x1, .., xn)@. mkTupleType :: Pos -> [Term] -> Term mkTupleType p [] = UnitType p +mkTupleType _ [x] = x mkTupleType p (x:xs) = PairType (pos x) x (mkTupleType p xs) --- | Build a projection @t.i@ of a tuple +-- | Build a projection @t.i@ of a tuple. NOTE: This function does not +-- work to access the last component in a tuple, since it always +-- generates a @PairLeft@. mkTupleSelector :: Term -> Integer -> Term mkTupleSelector t i | i == 1 = PairLeft t