Merge pull request #160 from GaloisInc/text-untyped-ast

Convert more uses of `String` to `Text`.

saw-core/src/Verifier/SAW/Grammar.y

@@ -26,6 +26,7 @@ import Control.Monad.State (State, get, gets, modify, put, runState, evalState)
 import Control.Monad.Except (ExceptT, throwError, runExceptT)
 import qualified Data.ByteString.Lazy.UTF8 as B
 import Data.Maybe (isJust)
+import Data.Text (Text)
 import qualified Data.Text as Text
 import Data.Traversable
 import Data.Word
@@ -171,12 +172,12 @@ AppTerm : AtomTerm                 { $1 }
 AtomTerm :: { Term }
 AtomTerm
   : nat                          { NatLit (pos $1) (tokNat (val $1)) }
-  | string                       { StringLit (pos $1) (tokString (val $1)) }
+  | string                       { StringLit (pos $1) (Text.pack (tokString (val $1))) }
   | Ident                        { Name $1 }
   | IdentRec                     { Recursor Nothing $1 }
   | 'Prop'                       { Sort (pos $1) propSort }
   | 'sort' nat                   { Sort (pos $1) (mkSort (tokNat (val $2))) }
-  | AtomTerm '.' Ident           { RecordProj $1 (Text.pack (val $3)) }
+  | AtomTerm '.' Ident           { RecordProj $1 (val $3) }
   | AtomTerm '.' IdentRec        {% parseRecursorProj $1 $3 }
   | AtomTerm '.' nat             {% parseTupleSelector $1 (fmap tokNat $3) }
   | '(' sepBy(Term, ',') ')'     { mkTupleValue (pos $1) $2 }
@@ -186,17 +187,17 @@ AtomTerm
   | '#' '{' sepBy(FieldType, ',') '}'  { RecordType  (pos $1) $3 }
   | AtomTerm '.' '(' nat ')'           {% mkTupleProj $1 (tokNat (val $4)) }
 
-Ident :: { PosPair String }
-Ident : ident { fmap tokIdent $1 }
+Ident :: { PosPair Text }
+Ident : ident { fmap (Text.pack . tokIdent) $1 }
 
-IdentRec :: { PosPair String }
-IdentRec : identrec { fmap tokRecursor $1 }
+IdentRec :: { PosPair Text }
+IdentRec : identrec { fmap (Text.pack . tokRecursor) $1 }
 
 FieldValue :: { (PosPair FieldName, Term) }
-FieldValue : Ident '=' Term { (fmap Text.pack $1, $3) }
+FieldValue : Ident '=' Term { ($1, $3) }
 
 FieldType :: { (PosPair FieldName, Term) }
-FieldType : Ident ':' LTerm { (fmap Text.pack $1, $3) }
+FieldType : Ident ':' LTerm { ($1, $3) }
 
 opt(q) :: { Maybe q }
   : { Nothing }
@@ -341,7 +342,7 @@ parseModuleName (RecordProj t str) = (++ [Text.unpack str]) <$> parseModuleName
 parseModuleName _ = Nothing
 
 -- | Parse a qualified recursor @M1.M2...Mn.d#rec@
-parseRecursorProj :: Term -> PosPair String -> Parser Term
+parseRecursorProj :: Term -> PosPair Text -> Parser Term
 parseRecursorProj (parseModuleName -> Just mnm) i =
   return $ Recursor (Just $ mkModuleName mnm) i
 parseRecursorProj t _ =
@@ -356,9 +357,9 @@ parseTupleSelector t i =
 
 -- | Create a module name given a list of strings with the top-most
 -- module name given first.
-mkPosModuleName :: [PosPair String] -> PosPair ModuleName
+mkPosModuleName :: [PosPair Text] -> PosPair ModuleName
 mkPosModuleName [] = error "internal: Unexpected empty module name"
-mkPosModuleName l = PosPair p (mkModuleName nms)
+mkPosModuleName l = PosPair p (mkModuleName (fmap Text.unpack nms))
   where nms = fmap val l
         p = pos (last l)
 }

saw-core/src/Verifier/SAW/Module.hs

@@ -80,6 +80,7 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.HashMap.Strict (HashMap)
 import qualified Data.HashMap.Strict as HMap
+import Data.Text (Text)
 import GHC.Generics (Generic)
 
 import qualified Language.Haskell.TH.Syntax as TH
@@ -232,7 +233,7 @@ instance Show DataType where
 data ModuleDecl = TypeDecl DataType
                 | DefDecl Def
 
--- | The different sorts of things that a 'String' name can be resolved to
+-- | The different sorts of things that a 'Text' name can be resolved to
 data ResolvedName
   = ResolvedCtor Ctor
   | ResolvedDataType DataType
@@ -245,14 +246,14 @@ resolvedNameIdent (ResolvedDataType dt) = dtName dt
 resolvedNameIdent (ResolvedDef d) = defIdent d
 
 -- | Modules define namespaces of datatypes, constructors, and definitions,
--- i.e., mappings from 'String' names to these objects. A module is allowed to
--- map a 'String' name to an object defined in a different module. Modules also
+-- i.e., mappings from 'Text' names to these objects. A module is allowed to
+-- map a 'Text' name to an object defined in a different module. Modules also
 -- keep a record of the top-level declarations and the imports that were used to
 -- build them.
 data Module = Module {
           moduleName    :: !ModuleName
         , moduleImports :: !(Map ModuleName Module)
-        , moduleResolveMap :: !(Map String ResolvedName)
+        , moduleResolveMap :: !(Map Text ResolvedName)
         , moduleRDecls   :: [ModuleDecl] -- ^ All declarations in reverse order they were added.
         }
 
@@ -269,35 +270,35 @@ emptyModule nm =
          }
 
 
--- | Resolve a 'String' name in the namespace defined by a 'Module', to either a
+-- | Resolve a 'Text' name in the namespace defined by a 'Module', to either a
 -- 'Ctor', 'DataType', or 'Def'
-resolveName :: Module -> String -> Maybe ResolvedName
+resolveName :: Module -> Text -> Maybe ResolvedName
 resolveName m str = Map.lookup str (moduleResolveMap m)
 
--- | Resolve a 'String' name to a 'Ctor'
-findCtor :: Module -> String -> Maybe Ctor
+-- | Resolve a 'Text' name to a 'Ctor'
+findCtor :: Module -> Text -> Maybe Ctor
 findCtor m str =
   resolveName m str >>= \case { ResolvedCtor ctor -> Just ctor; _ -> Nothing }
 
--- | Resolve a 'String' name to a 'DataType'
-findDataType :: Module -> String -> Maybe DataType
+-- | Resolve a 'Text' name to a 'DataType'
+findDataType :: Module -> Text -> Maybe DataType
 findDataType m str =
   resolveName m str >>= \case { ResolvedDataType d -> Just d; _ -> Nothing }
 
--- | Resolve a 'String' name to a 'Def'
-findDef :: Module -> String -> Maybe Def
+-- | Resolve a 'Text' name to a 'Def'
+findDef :: Module -> Text -> Maybe Def
 findDef m str =
   resolveName m str >>= \case { ResolvedDef d -> Just d; _ -> Nothing }
 
 
--- | Insert a 'ResolvedName' into a 'Module', adding a mapping from the 'String'
+-- | Insert a 'ResolvedName' into a 'Module', adding a mapping from the 'Text'
 -- name of that resolved name to it. Signal an error in the case of a name
--- clash, i.e., an existing binding for the same 'String' name.
+-- clash, i.e., an existing binding for the same 'Text' name.
 insResolvedName :: Module -> ResolvedName -> Module
 insResolvedName m nm =
-  let str = identName $ resolvedNameIdent nm in
+  let str = identBaseName $ resolvedNameIdent nm in
   if Map.member str (moduleResolveMap m) then
-    internalError ("Duplicate name " ++ str ++ " being inserted into module "
+    internalError ("Duplicate name " ++ show str ++ " being inserted into module "
                    ++ show (moduleName m))
   else
     m { moduleResolveMap = Map.insert str nm (moduleResolveMap m) }
@@ -329,7 +330,7 @@ beginDataType m dt =
 
 -- | Complete a datatype, by adding its constructors
 completeDataType :: Module -> Ident -> [Ctor] -> Module
-completeDataType m (identName -> str) ctors =
+completeDataType m (identBaseName -> str) ctors =
   case resolveName m str of
     Just (ResolvedDataType dt)
       | null (dtCtors dt) ->
@@ -339,11 +340,11 @@ completeDataType m (identName -> str) ctors =
               Map.insert str (ResolvedDataType dt') (moduleResolveMap m),
               moduleRDecls = TypeDecl dt' : moduleRDecls m }
     Just (ResolvedDataType _) ->
-      internalError $ "completeDataType: datatype already completed: " ++ str
+      internalError $ "completeDataType: datatype already completed: " ++ show str
     Just _ ->
-      internalError $ "completeDataType: not a datatype: " ++ str
+      internalError $ "completeDataType: not a datatype: " ++ show str
     Nothing ->
-      internalError $ "completeDataType: datatype not found: " ++ str
+      internalError $ "completeDataType: datatype not found: " ++ show str
 
 
 -- | Insert a definition into a module
@@ -413,12 +414,12 @@ type ModuleMap = HashMap ModuleName Module
 -- | Resolve an 'Ident' to a 'Ctor' in a 'ModuleMap'
 findCtorInMap :: ModuleMap -> Ident -> Maybe Ctor
 findCtorInMap m i =
-  HMap.lookup (identModule i) m >>= flip findCtor (identName i)
+  HMap.lookup (identModule i) m >>= flip findCtor (identBaseName i)
 
 -- | Resolve an 'Ident' to a 'DataType' in a 'ModuleMap'
 findDataTypeInMap :: ModuleMap -> Ident -> Maybe DataType
 findDataTypeInMap m i =
-  HMap.lookup (identModule i) m >>= flip findDataType (identName i)
+  HMap.lookup (identModule i) m >>= flip findDataType (identBaseName i)
 
 -- | Get all definitions defined in any module in an entire module map. Note
 -- that the returned list might have redundancies if a definition is visible /

saw-core/src/Verifier/SAW/Name.hs

@@ -25,6 +25,7 @@ module Verifier.SAW.Name
   , moduleNamePieces
    -- * Identifiers
   , Ident(identModule, identBaseName), identName, mkIdent
+  , mkIdentText
   , parseIdent
   , isIdent
   , identText
@@ -133,6 +134,9 @@ instance Read Ident where
 mkIdent :: ModuleName -> String -> Ident
 mkIdent m s = Ident m (Text.pack s)
 
+mkIdentText :: ModuleName -> Text -> Ident
+mkIdentText m s = Ident m s
+
 -- | Parse a fully qualified identifier.
 parseIdent :: String -> Ident
 parseIdent s0 =

saw-core/src/Verifier/SAW/ParserUtils.hs

@@ -32,6 +32,8 @@ import qualified Data.ByteString.Lazy as BL
 #if !MIN_VERSION_template_haskell(2,8,0)
 import qualified Data.ByteString.Lazy.UTF8 as UTF8
 #endif
+import Data.Text (Text)
+import qualified Data.Text as Text
 import Language.Haskell.TH
 #if MIN_VERSION_template_haskell(2,7,0)
 import Language.Haskell.TH.Syntax (qAddDependentFile)
@@ -135,13 +137,13 @@ declareTermApplyFun nm n tf =
 --
 -- The number of 'Term's to take as arguments is given by the arity of @tp@,
 -- i.e., the number of nested pi-abstractions it contains at top level.
-declareTypedNameFun :: Q Exp -> ModuleName -> String -> Bool -> Un.Term ->
+declareTypedNameFun :: Q Exp -> ModuleName -> Text -> Bool -> Un.Term ->
                        DecWriter ()
 declareTypedNameFun sc_fun mnm nm apply_p tp =
-  let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ nm in
+  let th_nm = (if apply_p then "scApply" else "sc") ++ show mnm ++ "_" ++ Text.unpack nm in
   declareTermApplyFun th_nm (length $ fst $ Un.asPiList tp) $ \sc ts ->
   [| $(sc_fun) $(varE sc)
-   (mkIdent mnm $(stringE nm))
+   (mkIdent mnm $(stringE (Text.unpack nm)))
    $(ts) |]
 
 -- | Declare a Haskell function
@@ -150,7 +152,7 @@ declareTypedNameFun sc_fun mnm nm apply_p tp =
 --
 -- for declared name (primitive, axiom, or definition) @d@ with type @tp@ in
 -- module @MMM@
-declareDefFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareDefFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareDefFun mnm d tp =
   declareTypedNameFun [| scGlobalApply |] mnm d True tp
 
@@ -159,7 +161,7 @@ declareDefFun mnm d tp =
 -- > scMMM_d :: SharedContext -> Term -> ... -> Term -> IO Term
 --
 -- for datatype @d@ with parameters @p_ctx@ and type @tp@ in module @MMM@
-declareDataTypeFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareDataTypeFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareDataTypeFun mnm d tp =
   declareTypedNameFun [| scDataTypeApp |] mnm d False tp
 
@@ -168,7 +170,7 @@ declareDataTypeFun mnm d tp =
 -- > scApplyMMM_c :: SharedContext -> Term -> ... -> Term -> IO Term
 --
 -- for constructor @c@ with type (including parameters) @tp@ in module @MMM@
-declareCtorFun :: ModuleName -> String -> Un.Term -> DecWriter ()
+declareCtorFun :: ModuleName -> Text -> Un.Term -> DecWriter ()
 declareCtorFun mnm c tp =
   declareTypedNameFun [| scCtorApp |] mnm c True tp
 

saw-core/src/Verifier/SAW/SCTypeCheck.hs

@@ -49,6 +49,7 @@ import Control.Monad.Reader
 import Data.List ( (\\) )
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 #if !MIN_VERSION_base(4,8,0)
 import Data.Traversable (Traversable(..))
 #endif
@@ -148,7 +149,7 @@ data TCError
   | NotRecordType TypedTerm
   | BadRecordField FieldName Term
   | DanglingVar Int
-  | UnboundName String
+  | UnboundName Text
   | SubtypeFailure TypedTerm Term
   | EmptyVectorLit
   | NoSuchDataType Ident
@@ -157,7 +158,7 @@ data TCError
   | BadParamsOrArgsLength Bool Ident [Term] [Term]
   | BadConstType NameInfo Term Term
   | MalformedRecursor Term String
-  | DeclError String String
+  | DeclError Text String
   | ErrorPos Pos TCError
   | ErrorCtx LocalName Term TCError
 
@@ -202,7 +203,7 @@ prettyTCError e = runReader (helper e) ([], Nothing) where
                 , ishow ty ]
   helper (DanglingVar n) =
       ppWithPos [ return ("Dangling bound variable index: " ++ show n)]
-  helper (UnboundName str) = ppWithPos [ return ("Unbound name: " ++ str)]
+  helper (UnboundName str) = ppWithPos [ return ("Unbound name: " ++ show str)]
   helper (SubtypeFailure trm tp2) =
       ppWithPos [ return "Inferred type", ishow (typedType trm),
                   return "Not a subtype of expected type", ishow tp2,
@@ -228,7 +229,7 @@ prettyTCError e = runReader (helper e) ([], Nothing) where
       ppWithPos [ return "Malformed recursor application",
                   ishow trm, return reason ]
   helper (DeclError nm reason) =
-    ppWithPos [ return ("Malformed declaration for " ++ nm), return reason ]
+    ppWithPos [ return ("Malformed declaration for " ++ show nm), return reason ]
   helper (ErrorPos p err) =
     local (\(ctx,_) -> (ctx, Just p)) $ helper err
   helper (ErrorCtx x _ err) =

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -510,7 +510,7 @@ scFindModule sc name =
 -- | Look up a definition by its identifier
 scFindDef :: SharedContext -> Ident -> IO (Maybe Def)
 scFindDef sc i =
-  findDef <$> scFindModule sc (identModule i) <*> return (identName i)
+  findDef <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a 'Def' by its identifier, throwing an error if it is not found
 scRequireDef :: SharedContext -> Ident -> IO Def
@@ -523,7 +523,7 @@ scRequireDef sc i =
 -- | Look up a datatype by its identifier
 scFindDataType :: SharedContext -> Ident -> IO (Maybe DataType)
 scFindDataType sc i =
-  findDataType <$> scFindModule sc (identModule i) <*> return (identName i)
+  findDataType <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a datatype by its identifier, throwing an error if it is not found
 scRequireDataType :: SharedContext -> Ident -> IO DataType
@@ -536,7 +536,7 @@ scRequireDataType sc i =
 -- | Look up a constructor by its identifier
 scFindCtor :: SharedContext -> Ident -> IO (Maybe Ctor)
 scFindCtor sc i =
-  findCtor <$> scFindModule sc (identModule i) <*> return (identName i)
+  findCtor <$> scFindModule sc (identModule i) <*> pure (identBaseName i)
 
 -- | Look up a constructor by its identifier, throwing an error if not found
 scRequireCtor :: SharedContext -> Ident -> IO Ctor