Convert SAWCore to use nested representation for records.

The core term representation now uses Empty and Field
values/types to represent records of all sizes.

The new Field value constructor is printed as "{t=x, ...=y}"
and the Field type constructor is printed as "{t:a, ...:b}",
where "t" is the field name. Record projections are represented
just as they were before.

Record values like "{s = x, t = y}" are encoded as
"{s = x, ... = {t = y, ... = {}}}"; similarly for record types.

Currently the record field order matters. For now the plan is to
use only records whose fields are in sorted (alphabetical) order.

Remaining steps:
- Fix pretty printer to recover standard record syntax
- Fix parser to allow writing low-level record values and types

src/Verifier/SAW/ExternalFormat.hs

@@ -69,8 +69,10 @@ scWriteExternal t0 =
             PairType x y       -> unwords ["PairT", show x, show y]
             PairLeft e         -> unwords ["ProjL", show e]
             PairRight e        -> unwords ["ProjR", show e]
-            RecordValue m      -> unwords ("Record" : map writeField (Map.assocs m))
-            RecordType m       -> unwords ("RecordT" : map writeField (Map.assocs m))
+            EmptyValue         -> unwords ["Empty"]
+            EmptyType          -> unwords ["EmptyT"]
+            FieldValue f x y   -> unwords ["Record", f, show x, show y]
+            FieldType f x y    -> unwords ["RecordT", f, show x, show y]
             RecordSelector e i -> unwords ["RecordSel", show e, i]
             CtorApp i es       -> unwords ("Ctor" : show i : map show es)
             DataTypeApp i es   -> unwords ("Data" : show i : map show es)
@@ -81,8 +83,6 @@ scWriteExternal t0 =
             DoubleLit x        -> unwords ["Double", show x]
             StringLit s        -> unwords ["String", show s]
             ExtCns ext         -> unwords ("ExtCns" : writeExtCns ext)
-    writeField :: (String, Int) -> String
-    writeField (s, e) = unwords [s, show e]
     writeDefs = error "unsupported Let expression"
     writeExtCns ec = [show (ecVarIndex ec), ecName ec, show (ecType ec)]
 
@@ -116,8 +116,10 @@ scReadExternal sc input =
         ["PairT", x, y]     -> FTermF (PairType (read x) (read y))
         ["ProjL", x]        -> FTermF (PairLeft (read x))
         ["ProjR", x]        -> FTermF (PairRight (read x))
-        ("Record" : fs)     -> FTermF (RecordValue (readMap fs))
-        ("RecordT" : fs)    -> FTermF (RecordType (readMap fs))
+        ["Empty"]           -> FTermF EmptyValue
+        ["EmptyT"]          -> FTermF EmptyType
+        ["Record",f,x,y]    -> FTermF (FieldValue f (read x) (read y))
+        ["RecordT",f,x,y]   -> FTermF (FieldType f (read x) (read y))
         ["RecordSel", e, i] -> FTermF (RecordSelector (read e) i)
         ("Ctor" : i : es)   -> FTermF (CtorApp (parseIdent i) (map read es))
         ("Data" : i : es)   -> FTermF (DataTypeApp (parseIdent i) (map read es))
@@ -129,8 +131,4 @@ scReadExternal sc input =
         ["String", s]       -> FTermF (StringLit (read s))
         ["ExtCns", i, n, t] -> FTermF (ExtCns (EC (read i) n (read t)))
         _ -> error $ "Parse error: " ++ unwords tokens
-    readMap :: [String] -> Map FieldName Int
-    readMap [] = Map.empty
-    readMap (i : e : fs) = Map.insert i (read e) (readMap fs)
-    readMap _ = error $ "scReadExternal: Parse error"
 

src/Verifier/SAW/Grammar.y

@@ -144,7 +144,7 @@ AtomPat :: { Pat }
 AtomPat : SimplePat                 { PSimple $1 }
         | ConDotList                { PCtor (identFromList1 $1) [] }
         | '(' sepBy(Pat, ',') ')'   { parseParen (\_ v -> v) mkPTuple (pos $1) $2 }
-        | '{' recList('=', Pat) '}' { PRecord (pos $1) $2 }
+        | '{' recList('=', Pat) '}' { mkPRecord (pos $1) $2 }
 
 SimplePat :: { SimplePat }
 SimplePat : unvar { PUnused (fmap tokVar $1) }
@@ -198,8 +198,8 @@ AtomTerm : nat                          { NatLit (pos $1) (tokNat (val $1)) }
          |     '(' sepBy(Term, ',') ')'     { parseParen Paren mkTupleValue (pos $1) $2 }
          | '#' '(' sepBy(Term, ',') ')'    {% parseTParen (pos $1) $3 }
          |     '[' sepBy(Term, ',') ']'     { VecLit (pos $1) $2 }
-         |     '{' recList('=',   Term) '}' { RecordValue (pos $1) $2 }
-         | '#' '{' recList('::', LTerm) '}' { RecordType  (pos $1) $3 }
+         |     '{' recList('=',   Term) '}' { mkRecordValue (pos $1) $2 }
+         | '#' '{' recList('::', LTerm) '}' { mkRecordType  (pos $1) $3 }
 
 PiArg :: { PiArg }
 PiArg : ParamType AppArg {% mkPiArg ($1, $2) }
@@ -395,11 +395,14 @@ termAsPat ex = do
         return (PPair p <$> px <*> py)
       (UnitType{}, _) -> badPat "Tuple types"
       (PairType{}, _) -> badPat "Tuple types"
-      (RecordValue p l,[]) ->
-          fmap (fmap (PRecord p . zip flds) . sequence) $ mapM termAsPat terms
-        where (flds,terms) = unzip l
+      (EmptyValue p, []) -> return $ Just (PEmpty p)
+      (FieldValue (fp, x) y, []) -> do
+        px <- termAsPat x
+        py <- termAsPat y
+        return (curry PField fp <$> px <*> py)
       (RecordSelector{}, []) -> badPat "Record selector"
-      (RecordType{},[]) -> badPat "Record type"
+      (EmptyType{},[]) -> badPat "Record type"
+      (FieldType{},[]) -> badPat "Record type"
 
       (TypeConstraint{}, []) -> badPat "Type constraint"
       (Paren{}, _) -> error "internal: Unexpected paren"

src/Verifier/SAW/PrettySExp.hs

@@ -93,8 +93,10 @@ ppSharedTermSExpWith cfg tm = doc
               FTermF (PairType{}) -> text "Tuple"
               FTermF (PairLeft{}) -> text "proj" <> (braces (int 1))
               FTermF (PairRight{}) -> text "proj" <> (braces (int 2))
-              FTermF (RecordValue _) -> text "record"
-              FTermF (RecordType _) -> text "Record"
+              FTermF (EmptyValue{}) -> text "record"
+              FTermF (FieldValue{}) -> text "record"
+              FTermF (EmptyType{}) -> text "Record"
+              FTermF (FieldType{}) -> text "Record"
               FTermF (RecordSelector _ fld) ->
                 text "proj" <> (braces (text fld))
               FTermF (CtorApp n _) -> text (show n)

src/Verifier/SAW/Recognizer.hs

@@ -14,7 +14,7 @@ Stability   : experimental
 Portability : non-portable (language extensions)
 -}
 
-module Verifier.SAW.Recognizer 
+module Verifier.SAW.Recognizer
   ( Recognizer
   , (<:), emptyl, endl
   , (:*:)(..)
@@ -58,6 +58,7 @@ import Control.Applicative
 import Control.Lens
 import Control.Monad
 import Data.Map (Map)
+import qualified Data.Map as Map
 import Verifier.SAW.Prim
 import Verifier.SAW.TypedAST
 
@@ -172,10 +173,23 @@ asTupleSelector t = do
     _           -> fail "asTupleSelector"
 
 asRecordType :: (Monad m, Termlike t) => Recognizer m t (Map FieldName t)
-asRecordType t = do RecordType m <- asFTermF t; return m
+asRecordType t = do
+  ftf <- asFTermF t
+  case ftf of
+    EmptyType       -> return Map.empty
+    FieldType f x y -> do m <- asRecordType y; return (Map.insert f x m)
+    _               -> fail $ "asRecordType: " ++ show (Term (FTermF (fmap toTerm ftf)))
+
+toTerm :: Termlike t => t -> Term
+toTerm t = Term (fmap toTerm (unwrapTermF t))
 
 asRecordValue :: (Monad m, Termlike t) => Recognizer m t (Map FieldName t)
-asRecordValue t = do RecordValue m <- asFTermF t; return m
+asRecordValue t = do
+  ftf <- asFTermF t
+  case ftf of
+    EmptyValue       -> return Map.empty
+    FieldValue f x y -> do m <- asRecordValue y; return (Map.insert f x m)
+    _                -> fail $ "asRecordValue: " ++ show (Term (FTermF (fmap toTerm ftf)))
 
 asRecordSelector :: (Monad m, Termlike t) => Recognizer m t (t, FieldName)
 asRecordSelector t = do RecordSelector u i <- asFTermF t; return (u,i)
@@ -184,7 +198,7 @@ asCtor :: (Monad f, Termlike t) => Recognizer f t (Ident, [t])
 asCtor t = do CtorApp c l <- asFTermF t; return (c,l)
 
 asDataType :: (Monad f, Termlike t) => Recognizer f t (Ident, [t])
-asDataType t = do DataTypeApp c l <- asFTermF t; return (c,l) 
+asDataType t = do DataTypeApp c l <- asFTermF t; return (c,l)
 
 isDataType :: (Monad f, Termlike t) => Ident -> Recognizer f [t] a -> Recognizer f t a
 isDataType i p t = do

src/Verifier/SAW/Rewriter.hs

@@ -207,10 +207,11 @@ ruleOfDefEqn ident (DefEqn pats rhs@(Term _rtf)) =
             (j, m) <- get
             put (j + 1, Map.insert j (incVars 0 (j - i) tp) m)
             return $ Term $ LocalVar (n - 1 - j)
-          PUnit     -> return $ Term (FTermF UnitValue)
-          PPair x y -> (Term . FTermF) <$> (PairValue <$> termOfPat x <*> termOfPat y)
-          PRecord ps -> (Term . FTermF . RecordValue) <$> traverse termOfPat ps
-          PCtor c ps -> (Term . FTermF . CtorApp c) <$> traverse termOfPat ps
+          PUnit        -> return $ Term (FTermF UnitValue)
+          PPair x y    -> (Term . FTermF) <$> (PairValue <$> termOfPat x <*> termOfPat y)
+          PEmpty       -> return $ Term (FTermF EmptyValue)
+          PField f x y -> (Term . FTermF) <$> (FieldValue f <$> termOfPat x <*> termOfPat y)
+          PCtor c ps   -> (Term . FTermF . CtorApp c) <$> traverse termOfPat ps
 
     (args, (_, varmap)) = runState (traverse termOfPat pats) (nBound, Map.empty)
 
@@ -446,9 +447,11 @@ rewriteSharedTermTypeSafe sc ss t0 =
           PairType{}       -> return ftf -- doesn't matter
           PairLeft{}       -> traverse rewriteAll ftf
           PairRight{}      -> traverse rewriteAll ftf
-          RecordValue{}    -> traverse rewriteAll ftf
+          EmptyValue       -> return ftf
+          EmptyType        -> return ftf
+          FieldValue{}     -> traverse rewriteAll ftf
+          FieldType{}      -> return ftf -- doesn't matter
           RecordSelector{} -> traverse rewriteAll ftf
-          RecordType{}     -> return ftf -- doesn't matter
           CtorApp{}        -> return ftf --FIXME
           DataTypeApp{}    -> return ftf -- could treat same as CtorApp
           Sort{}           -> return ftf -- doesn't matter

src/Verifier/SAW/SCTypeCheck.hs

@@ -22,7 +22,7 @@ import Control.Lens
 import Control.Monad.Trans.Except
 import Control.Monad.State.Strict as State
 
-import Data.Foldable (maximum, and)
+import Data.Foldable (and)
 import Data.Map (Map)
 import qualified Data.Map as Map
 #if !MIN_VERSION_base(4,8,0)
@@ -175,6 +175,16 @@ scTypeCheck' sc env t0 = State.evalStateT (memo t0) Map.empty
           sx <- sort x
           sy <- sort y
           io $ scSort sc (max sx sy)
+        EmptyValue -> io $ scEmptyType sc
+        EmptyType -> io $ scSort sc (mkSort 0)
+        FieldValue f x y -> do
+          tx <- memo x
+          ty <- memo y
+          io $ scFieldType sc f tx ty
+        FieldType _ x y -> do
+          sx <- sort x
+          sy <- sort y
+          io $ scSort sc (max sx sy)
         PairLeft t -> do
           ty <- memo t
           case ty of
@@ -185,17 +195,14 @@ scTypeCheck' sc env t0 = State.evalStateT (memo t0) Map.empty
           case ty of
             STApp _ (FTermF (PairType _ t2)) -> whnf t2
             _ -> throwTCError (NotTupleType ty)
-        RecordValue m -> io . scRecordType sc =<< traverse memo m
         RecordSelector t f -> do
           ty <- memo t
-          case ty of
-            STApp _ (FTermF (RecordType m)) -> 
+          case asRecordType ty of
+            Just m ->
               case Map.lookup f m of
                 Nothing -> throwTCError $ BadRecordField f ty
                 Just tp -> whnf tp
             _ -> throwTCError (NotRecordType ty)
-        RecordType m | Map.null m -> io $ scSort sc (mkSort 0)
-        RecordType m -> io . scSort sc . maximum =<< traverse sort m
         CtorApp c args -> do
           t <- io $ scTypeOfCtor sc c
           _ <- sort t -- TODO: do we care about the level?

src/Verifier/SAW/SharedTerm.hs

@@ -82,6 +82,10 @@ module Verifier.SAW.SharedTerm
   , scPairType
   , scPairLeft
   , scPairRight
+  , scEmptyValue
+  , scEmptyType
+  , scFieldValue
+  , scFieldType
   , scTuple
   , scTupleType
   , scTupleSelector
@@ -174,7 +178,7 @@ import Control.Monad.Ref
 import Control.Monad.State.Strict as State
 import Data.Bits
 import qualified Data.Foldable as Fold
-import Data.Foldable (foldl', foldlM, foldrM, maximum)
+import Data.Foldable (foldl', foldlM, foldrM)
 import Data.Hashable (Hashable(..))
 import Data.HashMap.Strict (HashMap)
 import qualified Data.HashMap.Strict as HMap
@@ -416,10 +420,15 @@ scWhnf sc = go []
                           case asPairValue v of
                             Just (v1, v2) -> matchAll [p1, p2] [Left v1, Left v2]
                             _ -> return Nothing
-        PRecord pm  -> do v <- scWhnf sc x
-                          case asRecordValue v of
-                            Just xm | Map.keys xm == Map.keys pm -> matchAll (Map.elems pm) (map Left $ Map.elems xm)
+        PEmpty      -> do v <- scWhnf sc x
+                          case asFTermF v of
+                            Just EmptyValue -> return $ Just Map.empty
                             _ -> return Nothing
+        PField f p1 p2 -> do v <- scWhnf sc x
+                             case asFTermF v of
+                               Just (FieldValue f' v1 v2) | f == f' ->
+                                 matchAll [p1, p2] [Left v1, Left v2]
+                               _ -> return Nothing
         PCtor i ps  -> do v <- scWhnf sc x
                           case asCtor v of
                             Just (s, xs) | i == s -> matchAll ps (map Left xs)
@@ -544,8 +553,8 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
     ftermf tf =
       case tf of
         GlobalDef d -> lift $ scTypeOfGlobal sc d
-        UnitValue -> lift $ scUnitValue sc
-        UnitType -> lift $ scUnitType sc
+        UnitValue -> lift $ scUnitType sc
+        UnitType -> lift $ scSort sc (mkSort 0)
         PairValue x y -> do
           tx <- memo x
           ty <- memo y
@@ -560,12 +569,21 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
         PairRight t -> do
           STApp _ (FTermF (PairType _ t2)) <- memo t >>= liftIO . scWhnf sc
           return t2
-        RecordValue m -> lift . scRecordType sc =<< traverse memo m
+        EmptyValue -> lift $ scEmptyType sc
+        EmptyType -> lift $ scSort sc (mkSort 0)
+        FieldValue f x y -> do
+          tx <- memo x
+          ty <- memo y
+          lift $ scFieldType sc f tx ty
+        FieldType _ x y -> do
+          sx <- sort x
+          sy <- sort y
+          lift $ scSort sc (max sx sy)
         RecordSelector t f -> do
-          STApp _ (FTermF (RecordType m)) <- memo t >>= liftIO . scWhnf sc
+          t' <- memo t >>= liftIO . scWhnf sc
+          m <- asRecordType t'
           let Just tp = Map.lookup f m
           return tp
-        RecordType m -> lift . scSort sc . maximum =<< traverse sort m
         CtorApp c args -> do
           t <- lift $ scTypeOfCtor sc c
           lift $ foldM (reducePi sc) t args
@@ -896,13 +914,17 @@ scVector :: SharedContext s -> SharedTerm s -> [SharedTerm s] -> IO (SharedTerm
 scVector sc e xs = scFlatTermF sc (ArrayValue e (V.fromList xs))
 
 scRecord :: SharedContext s -> Map FieldName (SharedTerm s) -> IO (SharedTerm s)
-scRecord sc m = scFlatTermF sc (RecordValue m)
+scRecord sc m = go (Map.assocs m)
+  where go [] = scEmptyValue sc
+        go ((f, x) : xs) = scFieldValue sc f x =<< go xs
 
 scRecordSelect :: SharedContext s -> SharedTerm s -> FieldName -> IO (SharedTerm s)
 scRecordSelect sc t fname = scFlatTermF sc (RecordSelector t fname)
 
 scRecordType :: SharedContext s -> Map FieldName (SharedTerm s) -> IO (SharedTerm s)
-scRecordType sc m = scFlatTermF sc (RecordType m)
+scRecordType sc m = go (Map.assocs m)
+  where go [] = scEmptyType sc
+        go ((f, x) : xs) = scFieldType sc f x =<< go xs
 
 scUnitValue :: SharedContext s -> IO (SharedTerm s)
 scUnitValue sc = scFlatTermF sc UnitValue
@@ -916,6 +938,18 @@ scPairValue sc x y = scFlatTermF sc (PairValue x y)
 scPairType :: SharedContext s -> SharedTerm s -> SharedTerm s -> IO (SharedTerm s)
 scPairType sc x y = scFlatTermF sc (PairType x y)
 
+scEmptyValue :: SharedContext s -> IO (SharedTerm s)
+scEmptyValue sc = scFlatTermF sc EmptyValue
+
+scEmptyType :: SharedContext s -> IO (SharedTerm s)
+scEmptyType sc = scFlatTermF sc EmptyType
+
+scFieldValue :: SharedContext s -> FieldName -> SharedTerm s -> SharedTerm s -> IO (SharedTerm s)
+scFieldValue sc f x y = scFlatTermF sc (FieldValue f x y)
+
+scFieldType :: SharedContext s -> FieldName -> SharedTerm s -> SharedTerm s -> IO (SharedTerm s)
+scFieldType sc f x y = scFlatTermF sc (FieldType f x y)
+
 scTuple :: SharedContext s -> [SharedTerm s] -> IO (SharedTerm s)
 scTuple sc [] = scUnitValue sc
 scTuple sc (t : ts) = scPairValue sc t =<< scTuple sc ts

src/Verifier/SAW/Simulator.hs

@@ -79,7 +79,14 @@ matchThunk p x =
                       case v of
                         VPair x1 x2 -> matchThunks [p1, p2] [x1, x2]
                         _ -> return Nothing
-    PRecord _   -> fail "matchThunk PRecord unimplemented"
+    PEmpty      -> do v <- force x
+                      case v of
+                        VEmpty -> matchThunks [] []
+                        _ -> return Nothing
+    PField f p1 p2 -> do v <- force x
+                         case v of
+                           VField f' x1 x2 | f == f' -> matchThunks [p1, p2] [x1, ready x2]
+                           _ -> return Nothing
     PCtor i ps  -> do v <- force x
                       case v of
                         VCtorApp s xv | i == s -> matchThunks ps (V.toList xv)
@@ -181,9 +188,15 @@ evalTermF cfg lam rec tf env =
                                   return $ VPairType vx vy
         PairLeft x          -> valPairLeft =<< rec x
         PairRight x         -> valPairRight =<< rec x
-        RecordValue tm      -> liftM VRecord $ mapM rec' tm
+        EmptyValue          -> return VEmpty
+        EmptyType           -> return VEmptyType
+        FieldValue f x y    -> do tx <- rec' x
+                                  ty <- rec y
+                                  return $ VField f tx ty
+        FieldType f x y     -> do vx <- rec x
+                                  vy <- rec y
+                                  return $ VFieldType f vx vy
         RecordSelector t k  -> valRecordSelect k =<< rec t
-        RecordType tm       -> liftM VRecordType $ mapM rec tm
         CtorApp ident ts    -> do v <- simGlobal cfg ident
                                   xs <- mapM rec' ts
                                   foldM apply v xs