Extend saw-core parser with syntax for nested-record constructors

The syntax "{ label = x | r }" denotes the record "r" extended with
a field named "label" with value "x". Similarly, "#{ label :: a | t }"
denotes the record type "t" extended with a field named "label" of type
"a".

A parenthesized expression of type String may be used in place of a
label, such as "{ (s) = x | r }". This makes it possible to dynamically
construct records with arbitrary field names. This syntax can also be
used with ordinary record expressions like "{ (s) = x, b = y }" or with
record selectors like "r.(s)".

src/Verifier/SAW/Grammar.y

@@ -188,7 +188,7 @@ AppArg : RecTerm { $1 }
 RecTerm :: { Term }
 RecTerm : AtomTerm              { $1 }
         | ConDotList '.' Var    { Var (identFromList1 ($3 : $1)) }
-        | RecTerm '.' FieldName { RecordSelector $1 (mkFieldNameTerm $3) }
+        | RecTerm '.' Label     { RecordSelector $1 $3 }
         | RecTerm '.' nat       { mkTupleSelector $1 (fmap tokNat $3) }
 
 AtomTerm :: { Term }
@@ -197,13 +197,15 @@ AtomTerm : nat                          { NatLit (pos $1) (tokNat (val $1)) }
          | Var                          { Var (fmap localIdent $1) }
          | unvar                        { Unused (fmap tokVar $1) }
          | 'sort' nat                   { Sort (pos $1) (mkSort (tokNat (val $2))) }
-         |     '(' sepBy(Term, ',') ')'     { parseParen Paren mkTupleValue (pos $1) $2 }
-         | '#' '(' sepBy(Term, ',') ')'    {% parseTParen (pos $1) $3 }
-         |     '[' sepBy(Term, ',') ']'     { VecLit (pos $1) $2 }
-         |     '{' recList('=',   Term) '}' { mkRecordValue (pos $1) $2 }
-         | '#' '{' recList('::', LTerm) '}' { mkRecordType  (pos $1) $3 }
-         |     '(' Term '|' Term ')'        { PairValue (pos $1) $2 $4 }
-         | '#' '(' Term '|' Term ')'        { PairType (pos $1) $3 $5 }
+         |     '(' sepBy(Term, ',') ')'       { parseParen Paren mkTupleValue (pos $1) $2 }
+         | '#' '(' sepBy(Term, ',') ')'       {% parseTParen (pos $1) $3 }
+         |     '[' sepBy(Term, ',') ']'       { VecLit (pos $1) $2 }
+         |     '{' sepBy(FieldValue, ',') '}' { mkRecordValue (pos $1) $2 }
+         | '#' '{' sepBy(FieldType, ',') '}'  { mkRecordType  (pos $1) $3 }
+         |     '(' Term '|' Term ')'          { PairValue (pos $1) $2 $4 }
+         | '#' '(' Term '|' Term ')'          { PairType (pos $1) $3 $5 }
+         |     '{' FieldValue '|' Term '}'    { FieldValue $2 $4 }
+         | '#' '{' FieldType '|' Term '}'     { FieldType $3 $5 }
 
 PiArg :: { PiArg }
 PiArg : ParamType AppArg {% mkPiArg ($1, $2) }
@@ -226,6 +228,16 @@ Var : var { fmap tokVar $1 }
 FieldName :: { PosPair FieldName }
 FieldName : var { fmap tokVar $1 }
 
+Label :: { Term }
+Label : FieldName    { mkFieldNameTerm $1 }
+      | '(' Term ')' { $2 }
+
+FieldValue :: { (Term, Term) }
+FieldValue : Label '=' Term { ($1, $3) }
+
+FieldType :: { (Term, Term) }
+FieldType : Label '::' LTerm { ($1, $3) }
+
 opt(q) : { Nothing }
        | q { Just $1 }
 

src/Verifier/SAW/UntypedAST.hs

@@ -290,13 +290,11 @@ mkTupleSelector t i =
     EQ -> PairLeft (_pos i) t
     GT -> mkTupleSelector (PairRight (_pos i) t) i{ val = val i - 1 }
 
-mkRecordValue :: Pos -> [(PosPair FieldName, Term)] -> Term
-mkRecordValue p xs = foldr FieldValue (EmptyValue p) xs'
-  where xs' = [ (mkFieldNameTerm x, y) | (x, y) <- xs ]
+mkRecordValue :: Pos -> [(Term, Term)] -> Term
+mkRecordValue p = foldr FieldValue (EmptyValue p)
 
-mkRecordType :: Pos -> [(PosPair FieldName, Term)] -> Term
-mkRecordType p xs = foldr FieldType (EmptyType p) xs'
-  where xs' = [ (mkFieldNameTerm x, y) | (x, y) <- xs ]
+mkRecordType :: Pos -> [(Term, Term)] -> Term
+mkRecordType p = foldr FieldType (EmptyType p)
 
 mkFieldNameTerm :: PosPair FieldName -> Term
 mkFieldNameTerm (PosPair p s) = StringLit p s