diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore index 54cb30f307..69b1e9f61c 100644 --- a/cryptol-saw-core/saw/Cryptol.sawcore +++ b/cryptol-saw-core/saw/Cryptol.sawcore @@ -22,10 +22,10 @@ bvExp n x y = foldr Bool (Vec n Bool) n (reverse n Bool y); updFst : (a b : sort 0) -> (a -> a) -> #(a, b) -> #(a, b); -updFst a b f x = (f x.(0), x.(1)); +updFst a b f x = (f x.0, x.1); updSnd : (a b : sort 0) -> (b -> b) -> #(a, b) -> #(a, b); -updSnd a b f x = (x.(0), f x.(1)); +updSnd a b f x = (x.0, f x.1); -------------------------------------------------------------------------------- -- Extended natural numbers diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index af116f2296..80b8271bc9 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/saw-core/prelude/Prelude.sawcore @@ -52,13 +52,13 @@ primitive consTuple : (t : sort 0) -> (ts : TypeList) -> t -> Tuple ts -> Tuple -- Pair types fst : (a b : sort 0) -> #(a, b) -> a; -fst a b tup = tup.(0); +fst a b tup = tup.0; snd : (a b : sort 0) -> #(a, b) -> b; -snd a b tup = tup.(1); +snd a b tup = tup.1; uncurry (a b c : sort 0) (f : a -> b -> c) : #(a, b) -> c - = (\ (x : #(a, b)) -> f x.(0) x.(1)); + = (\ (x : #(a, b)) -> f x.0 x.1); -------------------------------------------------------------------------------- -- String values @@ -875,10 +875,10 @@ expNat b e = primitive divModNat : Nat -> Nat -> #(Nat, Nat); divNat : Nat -> Nat -> Nat; -divNat x y = (divModNat x y).(0); +divNat x y = (divModNat x y).0; modNat : Nat -> Nat -> Nat; -modNat x y = (divModNat x y).(1); +modNat x y = (divModNat x y).1; -- There are implicit constructors from integer literals. @@ -1504,7 +1504,7 @@ foldList a = either #() #(a, List a) (List a) (\ (_ : #()) -> Nil a) (\ (tup : #(a, List a)) -> - Cons a tup.(0) tup.(1)); + Cons a tup.0 tup.1); -- A list of types, i.e. `List (sort 0)` if `List` was universe polymorphic data ListSort : sort 1 @@ -1563,8 +1563,8 @@ foldW64List = (\ (_:#()) -> W64Nil) (\ (bv_l : #(Sigma (Vec 64 Bool) (\ (_:Vec 64 Bool) -> #()), W64List)) -> W64Cons (Sigma_proj1 (Vec 64 Bool) - (\ (_:Vec 64 Bool) -> #()) bv_l.(0)) - bv_l.(1)); + (\ (_:Vec 64 Bool) -> #()) bv_l.0) + bv_l.1); -------------------------------------------------------------------------------- @@ -2088,7 +2088,7 @@ composeM a b c f g x = bindM b c (f x) g; tupleCompMFunBoth : (a b c: sort 0) -> (a -> CompM b) -> #(c, a) -> CompM #(c, b); tupleCompMFunBoth a b c f = \ (x : #(c, a)) -> - bindM b #(c, b) (f x.(1)) (\ (y:b) -> returnM #(c, b) (x.(0), y)); + bindM b #(c, b) (f x.1) (\ (y:b) -> returnM #(c, b) (x.0, y)); -- Tuple a valu onto the output of a monadic function tupleCompMFunOut : (a b c: sort 0) -> c -> (a -> CompM b) -> (a -> CompM #(c, b)); @@ -2454,7 +2454,7 @@ multiFixM : (lrts:LetRecTypes) -> lrtPi lrts (lrtTupleType lrts) -> multiArgFixM : (lrt:LetRecType) -> (lrtToType lrt -> lrtToType lrt) -> lrtToType lrt; multiArgFixM lrt F = - (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).(0); + (multiFixM (LRT_Cons lrt LRT_Nil) (\ (f:lrtToType lrt) -> (F f, ()))).0; -- Test computations diff --git a/saw-core/src/Verifier/SAW/Grammar.y b/saw-core/src/Verifier/SAW/Grammar.y index d4accae2d2..1eb5a34c36 100644 --- a/saw-core/src/Verifier/SAW/Grammar.y +++ b/saw-core/src/Verifier/SAW/Grammar.y @@ -181,13 +181,12 @@ AtomTerm | 'isort' nat { Sort (pos $1) (mkSort (tokNat (val $2))) True } | AtomTerm '.' Ident { RecordProj $1 (val $3) } | AtomTerm '.' IdentRec {% parseRecursorProj $1 $3 } - | AtomTerm '.' nat {% parseTupleSelector $1 (fmap tokNat $3) } + | AtomTerm '.' nat { mkTupleSelector $1 (tokNat (val $3)) } | '(' sepBy(Term, ',') ')' { mkTupleValue (pos $1) $2 } | '#' '(' sepBy(Term, ',') ')' { mkTupleType (pos $1) $3 } | '[' sepBy(Term, ',') ']' { VecLit (pos $1) $2 } | '{' sepBy(FieldValue, ',') '}' { RecordValue (pos $1) $2 } | '#' '{' sepBy(FieldType, ',') '}' { RecordType (pos $1) $3 } - | AtomTerm '.' '(' nat ')' { mkTupleSelector $1 (tokNat (val $4)) } Ident :: { PosPair Text } Ident : ident { fmap (Text.pack . tokIdent) $1 } @@ -343,12 +342,6 @@ parseRecursorProj t _ = do addParseError (pos t) "Malformed recursor projection" return (badTerm (pos t)) -parseTupleSelector :: Term -> PosPair Natural -> Parser Term -parseTupleSelector t i = - if val i >= 1 then return (mkTupleSelector t (val i)) else - do addParseError (pos t) "non-positive tuple projection index" - return (badTerm (pos t)) - -- | Create a module name given a list of strings with the top-most -- module name given first. mkPosModuleName :: [PosPair Text] -> PosPair ModuleName