Remove legacy term constructors for nested records.

src/Verifier/SAW/ExternalFormat.hs

@@ -87,11 +87,6 @@ scWriteExternal t0 =
             PairType x y        -> unwords ["PairT", show x, show y]
             PairLeft e          -> unwords ["ProjL", show e]
             PairRight e         -> unwords ["ProjR", show e]
-            EmptyValue          -> unwords ["Empty"]
-            EmptyType           -> unwords ["EmptyT"]
-            FieldValue f x y    -> unwords ["OldRecord", show f, show x, show y]
-            FieldType f x y     -> unwords ["OldRecordT", show f, show x, show y]
-            RecordSelector e i  -> unwords ["OldRecordSel", show e, show i]
             CtorApp i ps es     ->
               unwords ("Ctor" : show i : map show ps ++ argsep : map show es)
             DataTypeApp i ps es ->
@@ -142,11 +137,6 @@ scReadExternal sc input =
         ["PairT", x, y]     -> FTermF (PairType (read x) (read y))
         ["ProjL", x]        -> FTermF (PairLeft (read x))
         ["ProjR", x]        -> FTermF (PairRight (read x))
-        ["Empty"]           -> FTermF EmptyValue
-        ["EmptyT"]          -> FTermF EmptyType
-        ["OldRecord",f,x,y] -> FTermF (FieldValue (read f) (read x) (read y))
-        ["OldRecordT",f,x,y] -> FTermF (FieldType (read f) (read x) (read y))
-        ["OldRecordSel", e, i] -> FTermF (RecordSelector (read e) (read i))
         ("Ctor" : i : (separateArgs -> Just (ps, es))) ->
           FTermF (CtorApp (parseIdent i) (map read ps) (map read es))
         ("Data" : i : (separateArgs -> Just (ps, es))) ->

src/Verifier/SAW/Recognizer.hs

@@ -31,14 +31,9 @@ module Verifier.SAW.Recognizer
   , asTupleType
   , asTupleValue
   , asTupleSelector
-  , asFieldType
-  , asFieldValue
   , asRecordType
   , asRecordValue
   , asRecordSelector
-  , asOldRecordType
-  , asOldRecordValue
-  , asOldRecordSelector
   , asCtorParams
   , asCtor
   , asCtorOrNat
@@ -203,68 +198,25 @@ asTupleSelector t = do
     PairRight y -> do (x, i) <- asTupleSelector y; return (x, i+1)
     _           -> fail "asTupleSelector"
 
-asFieldType :: (Monad m) => Recognizer m Term (Term, Term, Term)
-asFieldType t = do
-  ftf <- asFTermF t
-  case ftf of
-    FieldType x y z -> return (x, y, z)
-    _               -> fail "asFieldType"
-
-asFieldValue :: (Monad m) => Recognizer m Term (Term, Term, Term)
-asFieldValue t = do
-  ftf <- asFTermF t
-  case ftf of
-    FieldValue x y z -> return (x, y, z)
-    _                -> fail "asFieldValue"
-
 asRecordType :: (Monad m) => Recognizer m Term (Map FieldName Term)
 asRecordType t = do
   ftf <- asFTermF t
   case ftf of
     RecordType elems -> return $ Map.fromList elems
     _                -> fail $ "asRecordType: " ++ showTerm t
 
--- | Old version of 'asRecordType', that works on old-style record types
-asOldRecordType :: (Monad m) => Recognizer m Term (Map FieldName Term)
-asOldRecordType t = do
-  ftf <- asFTermF t
-  case ftf of
-    EmptyType       -> return Map.empty
-    FieldType f x y -> do m <- asRecordType y
-                          s <- asStringLit f
-                          return (Map.insert s x m)
-    _               -> fail $ "asRecordType: " ++ showTerm t
-
-
 asRecordValue :: (Monad m) => Recognizer m Term (Map FieldName Term)
 asRecordValue t = do
   ftf <- asFTermF t
   case ftf of
     RecordValue elems -> return $ Map.fromList elems
     _                 -> fail $ "asRecordValue: " ++ showTerm t
 
--- | Old version of 'asRecordValue', that uses 'EmptyValue' and 'FieldValue'
-asOldRecordValue :: (Monad m) => Recognizer m Term (Map FieldName Term)
-asOldRecordValue t = do
-  ftf <- asFTermF t
-  case ftf of
-    EmptyValue       -> return Map.empty
-    FieldValue f x y -> do m <- asRecordValue y
-                           s <- asStringLit f
-                           return (Map.insert s x m)
-    _                -> fail $ "asRecordValue: " ++ showTerm t
-
 asRecordSelector :: (Monad m) => Recognizer m Term (Term, FieldName)
 asRecordSelector t = do
   RecordProj u s <- asFTermF t
   return (u, s)
 
-asOldRecordSelector :: (Monad m) => Recognizer m Term (Term, FieldName)
-asOldRecordSelector t = do
-  RecordSelector u i <- asFTermF t
-  s <- asStringLit i
-  return (u, s)
-
 -- | Test whether a term is an application of a constructor, and, if so, return
 -- the constructor, its parameters, and its arguments
 asCtorParams :: (Monad f) => Recognizer f Term (Ident, [Term], [Term])

src/Verifier/SAW/Rewriter.hs

@@ -588,11 +588,6 @@ rewriteSharedTermTypeSafe sc ss t0 =
           PairType{}       -> return ftf -- doesn't matter
           PairLeft{}       -> traverse rewriteAll ftf
           PairRight{}      -> traverse rewriteAll ftf
-          EmptyValue       -> return ftf
-          EmptyType        -> return ftf
-          FieldValue{}     -> traverse rewriteAll ftf
-          FieldType{}      -> return ftf -- doesn't matter
-          RecordSelector{} -> traverse rewriteAll ftf
 
           -- NOTE: we don't rewrite arguments of constructors, datatypes, or
           -- recursors because of dependent types, as we could potentially cause

src/Verifier/SAW/SCTypeCheck.hs

@@ -398,16 +398,6 @@ instance TypeInfer (FlatTermF TypedTerm) where
     do sx <- ensureSort tx
        sy <- ensureSort ty
        liftTCM scSort (max sx sy)
-  typeInfer EmptyValue = liftTCM scEmptyType
-  typeInfer EmptyType = liftTCM scSort (mkSort 0)
-  typeInfer (FieldValue f (TypedTerm _ tx) (TypedTerm _ ty)) =
-    do checkField f
-       liftTCM scFieldType (typedVal f) tx ty
-  typeInfer (FieldType f (TypedTerm _ tx) (TypedTerm _ ty)) =
-    do checkField f
-       sx <- ensureSort tx
-       sy <- ensureSort ty
-       liftTCM scSort (max sx sy)
   typeInfer (PairLeft (TypedTerm _ tp)) =
     case asPairType tp of
       Just (t1, _) -> typeCheckWHNF t1
@@ -416,18 +406,6 @@ instance TypeInfer (FlatTermF TypedTerm) where
     case asPairType tp of
       Just (_, t2) -> typeCheckWHNF t2
       _ -> throwTCError (NotTupleType tp)
-  typeInfer (RecordSelector t@(TypedTerm _ tp) f@(TypedTerm f_trm _)) =
-    do checkField f
-       maybe_str <- asStringLit <$> typeCheckWHNF f_trm
-       f_str <- case maybe_str of
-         Just x -> return x
-         Nothing -> throwTCError (NotStringLit f_trm)
-       case asRecordType tp of
-         Just m ->
-           case Map.lookup f_str m of
-             Nothing -> throwTCError $ BadRecordField f_str tp
-             Just f_tp -> typeCheckWHNF f_tp
-         _ -> throwTCError (NotRecordType t)
 
   typeInfer (DataTypeApp d params args) =
     -- Look up the DataType structure, check the length of the params and args,
@@ -543,12 +521,6 @@ isSubtype t1' t2' = areConvertible t1' t2'
 areConvertible :: Term -> Term -> TCM Bool
 areConvertible t1 t2 = liftTCM scConvertibleEval scTypeCheckWHNF True t1 t2
 
--- | Check that a term has type @String@
-checkField :: TypedTerm -> TCM ()
-checkField t =
-  do string_tp <- liftTCM scStringType
-     checkSubtype t string_tp
-
 -- | Infer the type of a recursor application
 inferRecursorApp :: Ident -> [TypedTerm] -> TypedTerm ->
                     [(Ident,TypedTerm)] -> [TypedTerm] -> TypedTerm ->

src/Verifier/SAW/SharedTerm.hs

@@ -79,9 +79,6 @@ module Verifier.SAW.SharedTerm
   , scRecord
   , scRecordSelect
   , scRecordType
-  , scOldRecord
-  , scOldRecordSelect
-  , scOldRecordType
   , scDataTypeAppParams
   , scDataTypeApp
   , scCtorAppParams
@@ -122,10 +119,6 @@ module Verifier.SAW.SharedTerm
   , scPairType
   , scPairLeft
   , scPairRight
-  , scEmptyValue
-  , scEmptyType
-  , scFieldValue
-  , scFieldType
   , scTuple
   , scTupleType
   , scTupleSelector
@@ -581,7 +574,6 @@ data WHNFElim
   = ElimApp Term
   | ElimProj String
   | ElimPair Bool
-  | ElimOldProj FieldName
   | ElimRecursor Ident [Term] Term [(Ident,Term)] [Term]
 
 -- | Test if a term is a constructor application that should be converted to a
@@ -620,20 +612,13 @@ scWhnf sc t0 =
     go xs                     (convertsToNat    -> Just k) = scFlatTermF sc (NatLit k) >>= go xs
     go xs                     (asApp            -> Just (t, x)) = go (ElimApp x : xs) t
     go xs                     (asRecordSelector -> Just (t, n)) = go (ElimProj n : xs) t
-    go xs                     (asOldRecordSelector -> Just (t, n)) = go (ElimOldProj n : xs) t
     go xs                     (asPairSelector -> Just (t, i)) = go (ElimPair i : xs) t
     go (ElimApp x : xs)       (asLambda -> Just (_, _, body))   = instantiateVar sc 0 x body >>= go xs
     go (ElimPair i : xs)      (asPairValue -> Just (a, b))      = go xs (if i then b else a)
     go (ElimProj fld : xs)    (asRecordValue -> Just elems)     = case Map.lookup fld elems of
                                                                     Just t -> go xs t
                                                                     Nothing ->
                                                                       error "scWhnf: field missing in record"
-    go (ElimOldProj i : xs)   (asFieldValue -> Just (s, a, b))  = do s' <- memo s
-                                                                     b' <- memo b
-                                                                     t' <- scFieldValue sc s' a b'
-                                                                     case asRecordValue t' of
-                                                                       Just tm -> go xs ((Map.!) tm i)
-                                                                       Nothing -> foldM reapply t' xs
     go (ElimRecursor d ps
         p_ret cs_fs _ : xs)   (asCtorOrNat ->
                                Just (c, _, args))               = (scReduceRecursor sc d ps
@@ -646,19 +631,10 @@ scWhnf sc t0 =
     go xs                     (asPairValue -> Just (a, b))      = do b' <- memo b
                                                                      t' <- scPairValue sc a b'
                                                                      foldM reapply t' xs
-    go xs                     (asFieldValue -> Just (s, a, b))  = do s' <- memo s
-                                                                     b' <- memo b
-                                                                     t' <- scFieldValue sc s' a b'
-                                                                     foldM reapply t' xs
     go xs                     (asPairType -> Just (a, b))       = do a' <- memo a
                                                                      b' <- memo b
                                                                      t' <- scPairType sc a' b'
                                                                      foldM reapply t' xs
-    go xs                     (asFieldType -> Just (s, a, b))   = do s' <- memo s
-                                                                     a' <- memo a
-                                                                     b' <- memo b
-                                                                     t' <- scFieldType sc s' a' b'
-                                                                     foldM reapply t' xs
     go xs                     (asRecordType -> Just elems)   = do elems' <-
                                                                     mapM (\(i,t) -> (i,) <$> memo t) (Map.assocs elems)
                                                                   t' <- scRecordType sc elems'
@@ -677,7 +653,6 @@ scWhnf sc t0 =
     reapply t (ElimApp x) = scApply sc t x
     reapply t (ElimProj i) = scRecordSelect sc t i
     reapply t (ElimPair i) = scPairSelector sc t i
-    reapply t (ElimOldProj i) = scOldRecordSelect sc t i
     reapply t (ElimRecursor d ps p_ret cs_fs ixs) =
       scFlatTermF sc (RecursorApp d ps p_ret cs_fs ixs t)
 
@@ -831,22 +806,6 @@ scTypeOf' sc env t0 = State.evalStateT (memo t0) Map.empty
         PairRight t -> do
           STApp{ stAppTermF = FTermF (PairType _ t2) } <- memo t >>= liftIO . scWhnf sc
           return t2
-        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
-          f' <- asStringLit =<< liftIO (scWhnf sc f)
-          t' <- memo t >>= liftIO . scWhnf sc
-          m <- asRecordType t'
-          let Just tp = Map.lookup f' m
-          return tp
         CtorApp c params args -> do
           t <- lift $ scTypeOfCtor sc c
           lift $ foldM (reducePi sc) t (params ++ args)
@@ -1089,31 +1048,12 @@ scVector sc e xs = scFlatTermF sc (ArrayValue e (V.fromList xs))
 scRecord :: SharedContext -> Map FieldName Term -> IO Term
 scRecord sc m = scFlatTermF sc (RecordValue $ Map.assocs m)
 
-scOldRecord :: SharedContext -> Map FieldName Term -> IO Term
-scOldRecord sc m = go (Map.assocs m)
-  where go [] = scEmptyValue sc
-        go ((f, x) : xs) = do l <- scString sc f
-                              r <- go xs
-                              scFieldValue sc l x r
-
 scRecordSelect :: SharedContext -> Term -> FieldName -> IO Term
 scRecordSelect sc t fname = scFlatTermF sc (RecordProj t fname)
 
-scOldRecordSelect :: SharedContext -> Term -> FieldName -> IO Term
-scOldRecordSelect sc t fname = do
-  l <- scString sc fname
-  scFlatTermF sc (RecordSelector t l)
-
 scRecordType :: SharedContext -> [(String,Term)] -> IO Term
 scRecordType sc elem_tps = scFlatTermF sc (RecordType elem_tps)
 
-scOldRecordType :: SharedContext -> Map FieldName Term -> IO Term
-scOldRecordType sc m = go (Map.assocs m)
-  where go [] = scEmptyType sc
-        go ((f, x) : xs) = do l <- scString sc f
-                              r <- go xs
-                              scFieldType sc l x r
-
 scUnitValue :: SharedContext -> IO Term
 scUnitValue sc = scFlatTermF sc UnitValue
 
@@ -1126,18 +1066,6 @@ scPairValue sc x y = scFlatTermF sc (PairValue x y)
 scPairType :: SharedContext -> Term -> Term -> IO Term
 scPairType sc x y = scFlatTermF sc (PairType x y)
 
-scEmptyValue :: SharedContext -> IO Term
-scEmptyValue sc = scFlatTermF sc EmptyValue
-
-scEmptyType :: SharedContext -> IO Term
-scEmptyType sc = scFlatTermF sc EmptyType
-
-scFieldValue :: SharedContext -> Term -> Term -> Term -> IO Term
-scFieldValue sc f x y = scFlatTermF sc (FieldValue f x y)
-
-scFieldType :: SharedContext -> Term -> Term -> Term -> IO Term
-scFieldType sc f x y = scFlatTermF sc (FieldType f x y)
-
 scTuple :: SharedContext -> [Term] -> IO Term
 scTuple sc [] = scUnitValue sc
 scTuple sc (t : ts) = scPairValue sc t =<< scTuple sc ts

src/Verifier/SAW/Simulator.hs

@@ -144,19 +144,6 @@ evalTermF cfg lam recEval tf env =
                                   return $ VPairType vx vy
         PairLeft x          -> valPairLeft =<< recEval x
         PairRight x         -> valPairRight =<< recEval x
-        EmptyValue          -> return VEmpty
-        EmptyType           -> return VEmptyType
-        FieldValue f x y    -> do VString s <- recEval f
-                                  tx <- recEvalDelay x
-                                  vy <- recEval y
-                                  return $ VField s tx vy
-        FieldType f x y     -> do VString s <- recEval f
-                                  vx <- recEval x
-                                  vy <- recEval y
-                                  return $ VFieldType s vx vy
-        RecordSelector t k  -> do vt <- recEval t
-                                  VString s <- recEval k
-                                  valRecordSelect s vt
         CtorApp ident ps ts -> do v <- simGlobal cfg ident
                                   ps' <- mapM recEvalDelay ps
                                   ts' <- mapM recEvalDelay ts

src/Verifier/SAW/Simulator/Prims.hs

@@ -506,11 +506,6 @@ eqOp bp =
       do b1 <- go' x1 y1
          b2 <- go' x2 y2
          bpAnd bp b1 b2
-    go VEmpty VEmpty = return (bpTrue bp)
-    go (VField xf x1 x2) (VField yf y1 y2) | xf == yf =
-      do b1 <- go' x1 y1
-         b2 <- go x2 y2
-         bpAnd bp b1 b2
     go (VWord w1) (VWord w2) = bpBvEq bp w1 w2
     go (VVector v1) (VVector v2) =
       do bs <- sequence $ zipWith go' (V.toList v1) (V.toList v2)
@@ -1094,9 +1089,6 @@ muxValue bp b = value
                                                   value x y
     value VUnit             VUnit             = return VUnit
     value (VPair x1 x2)     (VPair y1 y2)     = VPair <$> thunk x1 y1 <*> thunk x2 y2
-    value VEmpty            VEmpty            = return VEmpty
-    value (VField xf x1 x2) (VField yf y1 y2) | xf == yf
-                                              = VField xf <$> thunk x1 y1 <*> value x2 y2
     value (VRecordValue elems1) (VRecordValue
                                  (alistAllFields (map fst elems1) ->
                                   Just elems2)) =