matita/matita/contribs/lambdadelta/bin/xhtbl/textParser.mly

   1 %{
   2
   3 module S = Str
   4 module L = List
   5 module T = Table
   6
   7 let split s =
   8    S.split (S.regexp "[ \r\n\t]+") s
   9
  10 let mk_css_atom s rs =
  11    let cs = split s in
  12    let map (b, (x1, x2)) = cs, b, x1, x2 in
  13    L.map map rs
  14
  15 let mk_string_atom s rs =
  16    let map (b, (x1, x2)) = s, b, x1, x2 in
  17    L.map map rs
  18
  19 %}
  20
  21 %token <int> NUM
  22 %token <string> TEXT
  23 %token SPACE NAME TABLE CSS URI EXT SR OC CC OB CB PS CF OP CP AT EOF
  24
  25 %start script
  26 %type <(string * string) list * (string * Table.table * Table.css Attr.atoms * Table.uri Attr.atoms * Table.ext Attr.atoms) list> script
  27
  28 %%
  29
  30 space:
  31    | SPACE TEXT TEXT { $2, $3 }
  32 ;
  33
  34 spaces:
  35    |              { []       }
  36    | space spaces { $1 :: $2 }
  37 ;
  38
  39 text:
  40    | TEXT                  { T.Plain $1             }
  41    | AT OP TEXT TEXT CP    { T.Link (true, $3, $4)  }
  42    | AT AT OP TEXT TEXT CP { T.Link (false, $4, $5) }
  43    | AT TEXT               { T.Link (true, $2, $2)  }
  44    | AT AT TEXT            { T.Link (false, $3, $3) }
  45 ;
  46
  47 texts:
  48   | text          { [$1]                    }
  49   | text PS texts { $1 :: T.Plain " " :: $3 }
  50   | text CF texts { $1 :: $3                }
  51 ;
  52
  53 key:
  54    | texts { T.Text $1        }
  55    | SR    { T.Glue None      }
  56    | NUM   { T.Glue (Some $1) }
  57 ;
  58
  59 css:
  60    |          { []       }
  61    | CSS TEXT { split $2 }
  62 ;
  63
  64 uri:
  65    |          { "" }
  66    | URI TEXT { $2 }
  67 ;
  68
  69 ext:
  70    |          { "" }
  71    | EXT TEXT { $2 }
  72 ;
  73
  74 table:
  75    | css uri ext name key     { T.mk_key        $5 $1 $2 $3 $4 }
  76    | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 "" }
  77    | css uri ext OB tables CB { T.mk_line true  $5 $1 $2 $3 "" }
  78 ;
  79
  80 tables:
  81    |              { []       }
  82    | table tables { $1 :: $2 }
  83 ;
  84
  85 name:
  86    |           { "" }
  87    | NAME TEXT { $2 }
  88 ;
  89
  90 interval:
  91    | NUM     { Some $1, Some $1 }
  92    | SR      { None, None       }
  93    | NUM NUM { Some $1, Some $2 }
  94    | NUM SR  { Some $1, None    }
  95    | SR NUM  { None, Some $2    }
  96    | SR SR   { None, None       }
  97 ;
  98
  99 range:
 100    | OB interval CB { true, $2  }
 101    | OC interval CC { false, $2 }
 102 ;
 103
 104 ranges:
 105    |              { []       }
 106    | range ranges { $1 :: $2 }
 107 ;
 108
 109 catom:
 110    | CSS TEXT ranges { mk_css_atom $2 $3 }
 111 ;
 112
 113 catoms:
 114    |              { []      }
 115    | catom catoms { $1 @ $2 }
 116 ;
 117
 118 uatom:
 119    | URI TEXT ranges { mk_string_atom $2 $3 }
 120 ;
 121
 122 uatoms:
 123    |              { []      }
 124    | uatom uatoms { $1 @ $2 }
 125 ;
 126
 127 xatom:
 128    | EXT TEXT ranges { mk_string_atom $2 $3 }
 129 ;
 130
 131 xatoms:
 132    |              { []      }
 133    | xatom xatoms { $1 @ $2 }
 134 ;
 135
 136 directive:
 137    | name TABLE table catoms uatoms xatoms { $1, $3, $4, $5, $6 }
 138 ;
 139
 140 directives:
 141    |                      { []       }
 142    | directive directives { $1 :: $2 }
 143 ;
 144
 145 script:
 146    | spaces directives EOF { $1, $2 }
 147 ;