git.oblomov.eu Git - ohcount/blob - src/parsers/coq.rl

   1 /************************* Required for every parser *************************/
   2 #ifndef OHCOUNT_COQ_PARSER_H
   3 #define OHCOUNT_COQ_PARSER_H
   4
   5 #include "../parser_macros.h"
   6
   7 // the name of the language
   8 const char *COQ_LANG = LANG_COQ;
   9
  10 // the languages entities
  11 const char *coq_entities[] = {
  12   "space", "comment", "string", "any"
  13 };
  14
  15 // constants associated with the entities
  16 enum {
  17   COQ_SPACE = 0, COQ_COMMENT, COQ_STRING, COQ_ANY
  18 };
  19
  20 /*****************************************************************************/
  21
  22 %%{
  23   machine coq;
  24   write data;
  25   include common "common.rl";
  26
  27   # Line counting machine
  28
  29   action coq_ccallback {
  30     switch(entity) {
  31     case COQ_SPACE:
  32       ls
  33       break;
  34     case COQ_ANY:
  35       code
  36       break;
  37     case INTERNAL_NL:
  38       std_internal_newline(COQ_LANG)
  39       break;
  40     case NEWLINE:
  41       std_newline(COQ_LANG)
  42     }
  43   }
  44
  45   action coq_comment_nc_res { nest_count = 0; }
  46   action coq_comment_nc_inc { nest_count++; }
  47   action coq_comment_nc_dec { nest_count--; }
  48
  49   coq_nested_block_comment =
  50     '(*' >coq_comment_nc_res @comment (
  51       newline %{ entity = INTERNAL_NL; } %coq_ccallback
  52       |
  53       ws
  54       |
  55       '(*' @coq_comment_nc_inc @comment
  56       |
  57       '*)' @coq_comment_nc_dec @comment
  58       |
  59       (nonnewline - ws) @comment
  60     )* :>> ('*)' when { nest_count == 0 }) @comment;
  61
  62   coq_comment = coq_nested_block_comment;
  63
  64   coq_string =
  65     '"' @code (
  66       newline %{ entity = INTERNAL_NL; } %coq_ccallback
  67       |
  68       ws
  69       |
  70       [^"] @code
  71     )* '"';
  72
  73   coq_line := |*
  74     spaces          ${ entity = COQ_SPACE; } => coq_ccallback;
  75     coq_comment;
  76     coq_string;
  77     newline         ${ entity = NEWLINE;   } => coq_ccallback;
  78     ^space          ${ entity = COQ_ANY;   } => coq_ccallback;
  79   *|;
  80
  81   # Entity machine
  82
  83   action coq_ecallback {
  84     callback(COQ_LANG, coq_entities[entity], cint(ts), cint(te), userdata);
  85   }
  86
  87   coq_comment_entity = '(*' >coq_comment_nc_res (
  88     '(*' @coq_comment_nc_inc
  89     |
  90     '*)' @coq_comment_nc_dec
  91     |
  92     any
  93   )* :>> ('*)' when { nest_count == 0 });
  94
  95   coq_entity := |*
  96     space+             ${ entity = COQ_SPACE;   } => coq_ecallback;
  97     coq_comment_entity ${ entity = COQ_COMMENT; } => coq_ecallback;
  98     # TODO:
  99     ^space;
 100   *|;
 101 }%%
 102
 103 /************************* Required for every parser *************************/
 104
 105 /* Parses a string buffer with Coq code.
 106  *
 107  * @param *buffer The string to parse.
 108  * @param length The length of the string to parse.
 109  * @param count Integer flag specifying whether or not to count lines. If yes,
 110  *   uses the Ragel machine optimized for counting. Otherwise uses the Ragel
 111  *   machine optimized for returning entity positions.
 112  * @param *callback Callback function. If count is set, callback is called for
 113  *   every line of code, comment, or blank with 'lcode', 'lcomment', and
 114  *   'lblank' respectively. Otherwise callback is called for each entity found.
 115  */
 116 void parse_coq(char *buffer, int length, int count,
 117                void (*callback) (const char *lang, const char *entity, int s,
 118                                  int e, void *udata),
 119                void *userdata
 120   ) {
 121   init
 122
 123   int nest_count = 0;
 124
 125   %% write init;
 126   cs = (count) ? coq_en_coq_line : coq_en_coq_entity;
 127   %% write exec;
 128
 129   // if no newline at EOF; callback contents of last line
 130   if (count) { process_last_line(COQ_LANG) }
 131 }
 132
 133 #endif
 134
 135 /*****************************************************************************/