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 Level1Lexer =
  31 struct
  32   type te = string * string
  33   let lexer = CicNotationLexer.syntax_pattern_lexer
  34 end
  35 module Level1Parser = Grammar.GMake (Level1Lexer)
  36
  37 module Level2Lexer =
  38 struct
  39   type te = string * string
  40   let lexer = CicNotationLexer.ast_pattern_lexer
  41 end
  42 module Level2Parser = Grammar.GMake (Level2Lexer)
  43
  44 module Level3Lexer =
  45 struct
  46   type te = string * string
  47   let lexer = CicNotationLexer.ast_pattern_lexer
  48 end
  49 module Level3Parser = Grammar.GMake (Level3Lexer)
  50
  51 let level1_pattern = Level1Parser.Entry.create "level1_pattern"
  52 let level2_pattern = Level2Parser.Entry.create "level2_pattern"
  53 let level3_interpretation = Level3Parser.Entry.create "level3_interpretation"
  54
  55 let return_term loc term = ()
  56
  57 (*let fail floc msg =*)
  58 (*  let (x, y) = CicAst.loc_of_floc floc in*)
  59 (*  failwith (sprintf "Error at characters %d - %d: %s" x y msg)*)
  60
  61 let int_of_string s =
  62   try
  63     Pervasives.int_of_string s
  64   with Failure _ ->
  65     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  66
  67 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
  68 GEXTEND Level1Parser
  69   GLOBAL: level1_pattern;
  70   level1_pattern: [ [ p = pattern -> () ] ];
  71   pattern: [ [ p = LIST1 simple_pattern -> () ] ];
  72   literal: [
  73     [ s = SYMBOL -> ()
  74     | k = KEYWORD -> ()
  75     ]
  76   ];
  77   sep:       [ [ SYMBOL "\\SEP";      sep = literal -> () ] ];
  78   row_sep:   [ [ SYMBOL "\\ROWSEP";   sep = literal -> () ] ];
  79   field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> () ] ];
  80   box_pattern: [
  81     [ SYMBOL "\\HBOX"; p = simple_pattern -> ()
  82     | SYMBOL "\\VBOX"; p = simple_pattern -> ()
  83     | SYMBOL "\\BREAK" -> ()
  84     ]
  85   ];
  86   magic_pattern: [
  87     [ SYMBOL "\\LIST0"; p = simple_pattern; sep = OPT sep -> ()
  88     | SYMBOL "\\LIST1"; p = simple_pattern; sep = OPT sep -> ()
  89     | SYMBOL "\\OPT"; p = simple_pattern -> ()
  90     ]
  91   ];
  92   pattern_variable: [
  93     [ id = IDENT -> ()
  94     | SYMBOL "\\NUM"; id = IDENT -> ()
  95     | SYMBOL "\\IDENT"; id = IDENT -> ()
  96     ]
  97   ];
  98   simple_pattern:
  99     [ "layout" LEFTA
 100       [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> ()
 101       | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> ()
 102       | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> ()
 103       | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> ()
 104       | SYMBOL "["; p1 = pattern; SYMBOL "\\OVER"; p2 = pattern; SYMBOL "]" ->
 105           ()
 106       | SYMBOL "["; p1 = pattern; SYMBOL "\\ATOP"; p2 = pattern; SYMBOL "]" ->
 107           ()
 108       | SYMBOL "\\ARRAY"; p = SELF; fsep = OPT field_sep; rsep = OPT row_sep ->
 109           ()
 110       | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> ()
 111       | SYMBOL "\\SQRT"; p = SELF -> ()
 112       | SYMBOL "\\ROOT"; arg = pattern; SYMBOL "\\OF"; index = SELF -> ()
 113       ]
 114     | "simple" NONA
 115       [ m = magic_pattern -> ()
 116       | v = pattern_variable -> ()
 117       | b = box_pattern -> ()
 118       | n = NUMBER -> ()
 119       | SYMBOL "["; p = pattern; SYMBOL "]" -> ()
 120       ]
 121     ];
 122 END
 123 (* }}} *)
 124
 125 (* {{{ Grammar for ast patterns, notation level 2 *)
 126 GEXTEND Level2Parser
 127   GLOBAL: level2_pattern;
 128   level2_pattern: [ [ p = pattern -> () ] ];
 129   sort: [
 130     [ SYMBOL "\\PROP" -> ()
 131     | SYMBOL "\\SET" -> ()
 132     | SYMBOL "\\TYPE" -> ()
 133     ]
 134   ];
 135   explicit_subst: [
 136     [ (* TODO explicit substitution *)
 137     ]
 138   ];
 139   meta_subst: [
 140     [ (* TODO meta substitution *)
 141     ]
 142   ];
 143   possibly_typed_name: [
 144     [ SYMBOL "("; i = IDENT; SYMBOL ":"; typ = pattern; SYMBOL ")" -> ()
 145     | i = IDENT -> ()
 146     ]
 147   ];
 148   match_pattern: [
 149     [ n = IDENT -> ()
 150     | SYMBOL "("; head = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
 151         ()
 152     ]
 153   ];
 154   binder: [
 155     [ SYMBOL <:unicode<Pi>>     (* Π *) -> ()
 156     | SYMBOL <:unicode<exists>> (* ∃ *) -> ()
 157     | SYMBOL <:unicode<forall>> (* ∀ *) -> ()
 158     | SYMBOL <:unicode<lambda>> (* λ *) -> ()
 159     ]
 160   ];
 161   bound_names: [
 162     [ vars = LIST1 IDENT SEP SYMBOL ",";
 163       typ = OPT [ SYMBOL ":"; p = pattern -> () ] -> ()
 164     | LIST1 [
 165         SYMBOL "("; vars = LIST1 IDENT SEP SYMBOL ",";
 166         typ = OPT [ SYMBOL ":"; p = pattern -> () ]; SYMBOL ")" -> ()
 167       ] ->
 168         ()
 169     ]
 170   ];
 171   induction_kind: [
 172     [ IDENT "rec" -> ()
 173     | IDENT "corec" -> ()
 174     ]
 175   ];
 176   let_defs: [
 177     [ defs = LIST1 [
 178         name = IDENT; args = bound_names;
 179         index_name = OPT [ IDENT "on"; idx = IDENT -> () ];
 180         ty = OPT [ SYMBOL ":" ; p = pattern -> () ];
 181         SYMBOL <:unicode<def>> (* ≝ *); body = pattern ->
 182           ()
 183       ] SEP IDENT "and" ->
 184         ()
 185     ]
 186   ];
 187   pattern_variable: [
 188     [ SYMBOL "\\NUM"; id = IDENT -> ()
 189     | SYMBOL "\\IDENT"; id = IDENT -> ()
 190     | SYMBOL "\\FRESH"; id = IDENT -> ()
 191     ]
 192   ];
 193   magic_pattern: [
 194     [ SYMBOL "\\FOLD"; n = OPT NUMBER; [ IDENT "left" | IDENT "right" ];
 195       LIST1 IDENT; SYMBOL "."; p1 = pattern;
 196       OPT [ SYMBOL "\\LAMBDA"; LIST1 IDENT ]; p2 = pattern ->
 197         ()
 198     | SYMBOL "\\DEFAULT"; id = IDENT; p1 = pattern; p2 = pattern -> ()
 199     ]
 200   ];
 201   pattern:
 202     [ "letin" NONA
 203       [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
 204         p1 = pattern; "in"; p2 = pattern ->
 205           ()
 206       | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
 207         body = pattern ->
 208           ()
 209       ]
 210     | "binder" RIGHTA
 211       [ b = binder; bound_names; SYMBOL "."; body = pattern -> () ]
 212     | "extension"
 213       [ ]
 214     | "apply" LEFTA
 215       [ p1 = pattern; p2 = pattern -> () ]
 216     | "simple" NONA
 217       [ i = IDENT -> ()
 218       | i = IDENT; s = explicit_subst -> ()
 219       | n = NUMBER -> ()
 220       | IMPLICIT -> ()
 221       | m = META -> ()
 222       | m = META; s = meta_subst -> ()
 223       | s = sort -> ()
 224       | s = SYMBOL -> ()
 225       | u = URI -> ()
 226       | outtyp = OPT [ SYMBOL "["; typ = pattern; SYMBOL "]" ];
 227         IDENT "match"; t = pattern;
 228         indty_ident = OPT [ SYMBOL ":"; id = IDENT ];
 229         IDENT "with"; SYMBOL "[";
 230         patterns = LIST0 [
 231           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 232           rhs = pattern ->
 233             ()
 234         ] SEP SYMBOL "|";
 235         SYMBOL "]" ->
 236           ()
 237       | SYMBOL "("; p1 = pattern; SYMBOL ":"; p2 = pattern; SYMBOL ")" -> ()
 238       | SYMBOL "("; p = pattern; SYMBOL ")" -> ()
 239       | v = pattern_variable -> ()
 240       | m = magic_pattern -> ()
 241       ]
 242     ];
 243 END
 244 (* }}} *)
 245
 246 (* {{{ Grammar for interpretation, notation level 3 *)
 247 GEXTEND Level3Parser
 248   GLOBAL: level3_interpretation;
 249   level3_interpretation: [ [ i = interpretation -> () ] ];
 250   argument: [
 251     [ i = IDENT -> ()
 252     | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
 253     | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
 254     ]
 255   ];
 256   term: [
 257     [ u = URI -> ()
 258     | a = argument -> ()
 259     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
 260     ]
 261   ];
 262   interpretation: [
 263     [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
 264       t = term ->
 265         ()
 266     ]
 267   ];
 268 END
 269 (* }}} *)
 270
 271 let exc_located_wrapper f =
 272   try
 273     f ()
 274   with
 275   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 276       raise (Parse_error (floc, msg))
 277   | Stdpp.Exc_located (floc, exn) ->
 278       raise (Parse_error (floc, (Printexc.to_string exn)))
 279
 280 let parse_syntax_pattern stream =
 281   exc_located_wrapper
 282     (fun () ->
 283       (Level1Parser.Entry.parse level1_pattern (Level1Parser.parsable stream)))
 284
 285 let parse_ast_pattern stream =
 286   exc_located_wrapper
 287     (fun () ->
 288       (Level2Parser.Entry.parse level2_pattern (Level2Parser.parsable stream)))
 289
 290 let parse_interpretation stream =
 291   exc_located_wrapper
 292     (fun () ->
 293       (Level3Parser.Entry.parse level3_interpretation
 294         (Level3Parser.parsable stream)))
 295
 296 (* vim:set encoding=utf8 foldmethod=marker: *)