helm/ocaml/cic_notation/cicNotationParser.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 exception Parse_error of Token.flocation * string
  29
  30 module NotationLexer =
  31 struct
  32   type te = string * string
  33   let lexer = CicNotationLexer.notation_lexer
  34 end
  35 module NotationGrammar = Grammar.GMake (NotationLexer)
  36
  37 let level1_pattern = NotationGrammar.Entry.create "level1_pattern"
  38 let level2_pattern = NotationGrammar.Entry.create "level2_pattern"
  39 let level3_interpretation = NotationGrammar.Entry.create "level3_interpretation"
  40
  41 let return_term loc term = ()
  42
  43 (*let fail floc msg =*)
  44 (*  let (x, y) = CicAst.loc_of_floc floc in*)
  45 (*  failwith (sprintf "Error at characters %d - %d: %s" x y msg)*)
  46
  47 let int_of_string s =
  48   try
  49     Pervasives.int_of_string s
  50   with Failure _ ->
  51     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  52
  53 GEXTEND NotationGrammar
  54   GLOBAL: level1_pattern level2_pattern level3_interpretation;
  55 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
  56   level1_pattern: [ [ p = l1_pattern -> () ] ];
  57   l1_pattern: [ [ p = LIST1 l1_simple_pattern -> () ] ];
  58   literal: [
  59     [ s = SYMBOL -> ()
  60     | k = KEYWORD -> ()
  61     ]
  62   ];
  63   sep:       [ [ SYMBOL "\\SEP";      sep = literal -> () ] ];
  64   row_sep:   [ [ SYMBOL "\\ROWSEP";   sep = literal -> () ] ];
  65   field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
  66   l1_box_pattern: [
  67     [ SYMBOL "\\HBOX"; p = l1_simple_pattern -> ()
  68     | SYMBOL "\\VBOX"; p = l1_simple_pattern -> ()
  69     | SYMBOL "\\BREAK" -> ()
  70     ]
  71   ];
  72   l1_magic_pattern: [
  73     [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> ()
  74     | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> ()
  75     | SYMBOL "\\OPT";   p = l1_simple_pattern -> ()
  76     ]
  77   ];
  78   l1_pattern_variable: [
  79     [ id = IDENT -> ()
  80     | SYMBOL "\\NUM"; id = IDENT -> ()
  81     | SYMBOL "\\IDENT"; id = IDENT -> ()
  82     ]
  83   ];
  84   l1_simple_pattern:
  85     [ "layout" LEFTA
  86       [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> ()
  87       | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> ()
  88       | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> ()
  89       | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> ()
  90       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
  91         SYMBOL "]" ->
  92           ()
  93       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
  94         SYMBOL "]" ->
  95           ()
  96       | SYMBOL "\\ARRAY"; p = SELF; fsep = OPT field_sep; rsep = OPT row_sep ->
  97           ()
  98       | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> ()
  99       | SYMBOL "\\SQRT"; p = SELF -> ()
 100       | SYMBOL "\\ROOT"; arg = l1_pattern; SYMBOL "\\OF"; index = SELF -> ()
 101       ]
 102     | "simple" NONA
 103       [ m = l1_magic_pattern -> ()
 104       | v = l1_pattern_variable -> ()
 105       | b = l1_box_pattern -> ()
 106       | n = NUMBER -> ()
 107       | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> ()
 108       ]
 109     ];
 110 (* }}} *)
 111 (* {{{ Grammar for ast patterns, notation level 2 *)
 112   level2_pattern: [ [ p = l2_pattern -> () ] ];
 113   sort: [
 114     [ SYMBOL "\\PROP" -> ()
 115     | SYMBOL "\\SET" -> ()
 116     | SYMBOL "\\TYPE" -> ()
 117     ]
 118   ];
 119   explicit_subst: [
 120     [ (* TODO explicit substitution *)
 121     ]
 122   ];
 123   meta_subst: [
 124     [ (* TODO meta substitution *)
 125     ]
 126   ];
 127   possibly_typed_name: [
 128     [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" -> ()
 129     | i = IDENT -> ()
 130     ]
 131   ];
 132   match_pattern: [
 133     [ n = IDENT -> ()
 134     | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
 135         ()
 136     ]
 137   ];
 138   binder: [
 139     [ SYMBOL <:unicode<Pi>>     (* Π *) -> ()
 140     | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
 141     | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
 142     | SYMBOL <:unicode<lambda>> (* λ *) -> ()
 143     ]
 144   ];
 145   bound_names: [
 146     [ vars = LIST1 IDENT SEP SYMBOL ",";
 147       typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ] -> ()
 148     | LIST1 [
 149         SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
 150         typ = OPT [ SYMBOL ":"; p = l2_pattern -> () ]; SYMBOL ")" -> ()
 151       ] ->
 152         ()
 153     ]
 154   ];
 155   induction_kind: [
 156     [ IDENT "rec" -> ()
 157     | IDENT "corec" -> ()
 158     ]
 159   ];
 160   let_defs: [
 161     [ defs = LIST1 [
 162         name = IDENT; args = bound_names;
 163         index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
 164         ty = OPT [ SYMBOL ":" ; p = l2_pattern -> () ];
 165         SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
 166           ()
 167       ] SEP IDENT "and" ->
 168         ()
 169     ]
 170   ];
 171   l2_pattern_variable: [
 172     [ SYMBOL "\\NUM"; id = IDENT -> ()
 173     | SYMBOL "\\IDENT"; id = IDENT -> ()
 174     | SYMBOL "\\FRESH"; id = IDENT -> ()
 175     ]
 176   ];
 177   l2_magic_pattern: [
 178     [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
 179       LIST1 IDENT; SYMBOL "."; p1 = l2_pattern;
 180       OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = l2_pattern ->
 181         ()
 182     | SYMBOL "\\DEFAULT"; id = IDENT; p1 = l2_pattern; p2 = l2_pattern -> ()
 183     ]
 184   ];
 185   l2_pattern:
 186     [ "letin" NONA
 187       [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
 188         p1 = l2_pattern; "in"; p2 = l2_pattern ->
 189           ()
 190       | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
 191         body = l2_pattern ->
 192           ()
 193       ]
 194     | "binder" RIGHTA
 195       [ b = binder; bound_names; SYMBOL "."; body = l2_pattern -> () ]
 196     | "extension"
 197       [ ]
 198     | "apply" LEFTA
 199       [ p1 = l2_pattern; p2 = l2_pattern -> () ]
 200     | "simple" NONA
 201       [ i = IDENT -> ()
 202       | i = IDENT; s = explicit_subst -> ()
 203       | n = NUMBER -> ()
 204       | IMPLICIT -> ()
 205       | m = META -> ()
 206       | m = META; s = meta_subst -> ()
 207       | s = sort -> ()
 208       | s = SYMBOL -> ()
 209       | u = URI -> ()
 210       | outtyp = OPT [ SYMBOL "["; typ = l2_pattern; SYMBOL "]" ];
 211         IDENT "match"; t = l2_pattern;
 212         indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
 213         IDENT "with"; SYMBOL "[";
 214         patterns = LIST0 [
 215           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 216           rhs = l2_pattern ->
 217             ()
 218         ] SEP SYMBOL "|";
 219         SYMBOL "]" ->
 220           ()
 221       | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
 222           ()
 223       | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> ()
 224       | v = l2_pattern_variable -> ()
 225       | m = l2_magic_pattern -> ()
 226       ]
 227     ];
 228 (* }}} *)
 229 (* {{{ Grammar for interpretation, notation level 3 *)
 230   level3_interpretation: [ [ i = interpretation -> () ] ];
 231   argument: [
 232     [ i = IDENT -> ()
 233     | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
 234     | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
 235     ]
 236   ];
 237   l3_term: [
 238     [ u = URI -> ()
 239     | a = argument -> ()
 240     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
 241     ]
 242   ];
 243   interpretation: [
 244     [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
 245       t = l3_term ->
 246         ()
 247     ]
 248   ];
 249 (* }}} *)
 250 END
 251
 252 let exc_located_wrapper f =
 253   try
 254     f ()
 255   with
 256   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 257       raise (Parse_error (floc, msg))
 258   | Stdpp.Exc_located (floc, exn) ->
 259       raise (Parse_error (floc, (Printexc.to_string exn)))
 260
 261 let parse_syntax_pattern stream =
 262   exc_located_wrapper
 263     (fun () ->
 264       (NotationGrammar.Entry.parse level1_pattern
 265         (NotationGrammar.parsable stream)))
 266
 267 let parse_ast_pattern stream =
 268   exc_located_wrapper
 269     (fun () ->
 270       (NotationGrammar.Entry.parse level2_pattern
 271         (NotationGrammar.parsable stream)))
 272
 273 let parse_interpretation stream =
 274   exc_located_wrapper
 275     (fun () ->
 276       (NotationGrammar.Entry.parse level3_interpretation
 277         (NotationGrammar.parsable stream)))
 278
 279 (* vim:set encoding=utf8 foldmethod=marker: *)