Overload Token/Rule Types since they are currently not used simultano…

…usly Co-authored-by: Matus Tejiscak <ziman@functor.sk>
idris-lang · May 24, 2020 · dfd24ac · dfd24ac
1 parent a6b3565
commit dfd24ac
Show file tree

Hide file tree

Showing 13 changed files with 225 additions and 226 deletions.
diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr
@@ -20,15 +20,15 @@ import Utils.String
 symbols : List String
 symbols = ["(", ":", ")"]
 
-ideTokens : TokenMap SourceToken
+ideTokens : TokenMap Token
 ideTokens =
     map (\x => (exact x, Symbol)) symbols ++
     [(digits, \x => IntegerLit (cast x)),
      (stringLit, \x => StringLit (stripQuotes x)),
      (identAllowDashes, \x => Ident x),
      (space, Comment)]
 
-idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
+idelex : String -> Either (Int, Int, String) (List (TokenData Token))
 idelex str
     = case lex ideTokens str of
            -- Add the EndInput token so that we'll have a line and column
@@ -37,12 +37,12 @@ idelex str
                                       [MkToken l c EndInput])
            (_, fail) => Left fail
     where
-      notComment : TokenData SourceToken -> Bool
+      notComment : TokenData Token -> Bool
       notComment t = case tok t of
                           Comment _ => False
                           _ => True
 
-sexp : SourceRule SExp
+sexp : Rule SExp
 sexp
     = do symbol ":"; exactIdent "True"
          pure (BoolAtom True)
@@ -59,14 +59,14 @@ sexp
          symbol ")"
          pure (SExpList xs)
 
-ideParser : {e : _} -> String -> Grammar (TokenData SourceToken) e ty -> Either (ParseError SourceToken) ty
+ideParser : {e : _} -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty
 ideParser str p
     = do toks   <- mapError LexFail $ idelex str
          parsed <- mapError toGenericParsingError $ parse p toks
          Right (fst parsed)
 
 
 export
-parseSExp : String -> Either (ParseError SourceToken) SExp
+parseSExp : String -> Either (ParseError Token) SExp
 parseSExp inp
     = ideParser inp (do c <- sexp; eoi; pure c)
diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
@@ -113,7 +113,7 @@ data DescField : Type where
   PPreclean    : FC -> String -> DescField
   PPostclean   : FC -> String -> DescField
 
-field : String -> PackageRule DescField
+field : String -> Rule DescField
 field fname
       = strField PVersion "version"
     <|> strField PAuthors "authors"
@@ -151,15 +151,15 @@ field fname
            e <- getString
            pure (PExec e)
   where
-    strField : (FC -> String -> DescField) -> String -> PackageRule DescField
+    strField : (FC -> String -> DescField) -> String -> Rule DescField
     strField p f
         = do start <- location
              exactProperty f
              str <- getString
              end <- location
              pure $ p (MkFC fname start end) str
 
-parsePkgDesc : String -> PackageRule (String, List DescField)
+parsePkgDesc : String -> Rule (String, List DescField)
 parsePkgDesc fname
     = do name <- packageName
          fields <- many (field fname)
@@ -416,7 +416,7 @@ clean pkg
              delete $ ttFile ++ ".ttc"
              delete $ ttFile ++ ".ttm"
 
-getParseErrorLoc : String -> ParseError PackageToken -> FC
+getParseErrorLoc : String -> ParseError Token -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
 getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
 getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case