Extend saw-core parser to handle pattern matches on nested record con…

…structors

src/Verifier/SAW/Grammar.y

@@ -142,16 +142,24 @@ Pat : AtomPat           { $1 }
     | ConDotList list1(AtomPat) { PCtor (identFromList1 $1) $2 }
 
 AtomPat :: { Pat }
-AtomPat : SimplePat                 { PSimple $1 }
-        | ConDotList                { PCtor (identFromList1 $1) [] }
-        | '(' sepBy(Pat, ',') ')'   { parseParen (\_ v -> v) mkPTuple (pos $1) $2 }
-        | '(' Pat '|' Pat ')'       { PPair (pos $1) $2 $4 }
-        | '{' recList('=', Pat) '}' { mkPRecord (pos $1) $2 }
+AtomPat : SimplePat                    { PSimple $1 }
+        | ConDotList                   { PCtor (identFromList1 $1) [] }
+        | '(' sepBy(Pat, ',') ')'      { parseParen (\_ v -> v) mkPTuple (pos $1) $2 }
+        | '(' Pat '|' Pat ')'          { PPair (pos $1) $2 $4 }
+        | '{' sepBy(FieldPat, ',') '}' { mkPRecord (pos $1) $2 }
+        | '{' FieldPat '|' Pat '}'     { PField $2 $4 }
 
 SimplePat :: { SimplePat }
 SimplePat : unvar { PUnused (fmap tokVar $1) }
           | Var   { PVar $1 }
 
+LabelPat :: { Pat }
+LabelPat : FieldName   { mkFieldNamePat $1 }
+         | '(' Pat ')' { $2 }
+
+FieldPat :: { (Pat, Pat) }
+FieldPat : LabelPat '=' Pat { ($1, $3) }
+
 Term :: { Term }
 Term : TTerm { $1 }
      | 'let' '{' list(SAWEqDecl) '}' 'in' Term { LetTerm (pos $1) $3 $6 }

src/Verifier/SAW/UntypedAST.hs

@@ -31,6 +31,7 @@ module Verifier.SAW.UntypedAST
   , Pat(..), ppPat
   , mkPTuple
   , mkPRecord
+  , mkFieldNamePat
   , SimplePat(..)
   , FieldName
   , Ident, localIdent, asLocalIdent, mkIdent, identModule, setIdentModule
@@ -153,9 +154,8 @@ data Pat
 mkPTuple :: Pos -> [Pat] -> Pat
 mkPTuple p = foldr (PPair p) (PUnit p)
 
-mkPRecord :: Pos -> [(PosPair FieldName, Pat)] -> Pat
-mkPRecord p xs = foldr PField (PEmpty p) xs'
-  where xs' = [ (mkFieldNamePat x, y) | (x, y) <- xs ]
+mkPRecord :: Pos -> [(Pat, Pat)] -> Pat
+mkPRecord p = foldr PField (PEmpty p)
 
 mkFieldNamePat :: PosPair FieldName -> Pat
 mkFieldNamePat (PosPair p s) = PString p s