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 let notation = NotationGrammar.Entry.create "notation" (* level1 <-> level 2 *)
  41 let interpretation =
  42   NotationGrammar.Entry.create "interpretation" (* level2 <-> level 3 *)
  43
  44 let return_term loc term = ()
  45
  46 let loc_of_floc = function
  47   | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
  48       (loc_begin, loc_end)
  49
  50 let fail floc msg =
  51   let (x, y) = loc_of_floc floc in
  52   failwith (sprintf "Error at characters %d - %d: %s" x y msg)
  53
  54 let int_of_string s =
  55   try
  56     Pervasives.int_of_string s
  57   with Failure _ ->
  58     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  59
  60 open CicNotationPt
  61
  62 let boxify = function
  63   | [ a ] -> a
  64   | l -> Layout (Box (H, l))
  65
  66 let fold_binder binder pt_names body =
  67   let fold_cluster binder names ty body =
  68     List.fold_right
  69       (fun name body -> Binder (binder, (Cic.Name name, ty), body))
  70       names body
  71   in
  72   List.fold_right
  73     (fun (names, ty) body -> fold_cluster binder names ty body)
  74     pt_names body
  75
  76 GEXTEND NotationGrammar
  77   GLOBAL: level1_pattern level2_pattern level3_interpretation notation
  78           interpretation;
  79 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
  80   level1_pattern: [ [ p = l1_pattern -> boxify p ] ];
  81   l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
  82   literal: [
  83     [ s = SYMBOL -> `Symbol s
  84     | k = KEYWORD -> `Keyword k
  85     | n = NUMBER -> `Number n
  86     ]
  87   ];
  88   sep:       [ [ SYMBOL "\\SEP";      sep = literal -> sep ] ];
  89 (*   row_sep:   [ [ SYMBOL "\\ROWSEP";   sep = literal -> sep ] ];
  90   field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> sep ] ]; *)
  91   l1_magic_pattern: [
  92     [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep)
  93     | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep)
  94     | SYMBOL "\\OPT";   p = l1_simple_pattern -> Opt p
  95     ]
  96   ];
  97   l1_pattern_variable: [
  98     [ id = IDENT -> TermVar id
  99     | SYMBOL "\\TERM"; id = IDENT -> TermVar id
 100     | SYMBOL "\\NUM"; id = IDENT -> NumVar id
 101     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
 102     ]
 103   ];
 104   l1_simple_pattern:
 105     [ "layout" LEFTA
 106       [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF -> Layout (Sub (p1, p2))
 107       | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF -> Layout (Sup (p1, p2))
 108       | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF -> Layout (Below (p1, p2))
 109       | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF -> Layout (Above (p1, p2))
 110       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
 111         SYMBOL "]" ->
 112           Layout (Frac (boxify p1, boxify p2))
 113       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
 114         SYMBOL "]" ->
 115           Layout (Atop (boxify p1, boxify p2))
 116 (*       | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
 117           Array (p, csep, rsep) *)
 118       | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF -> Layout (Frac (p1, p2))
 119       | SYMBOL "\\SQRT"; p = SELF -> Layout (Sqrt p)
 120       | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
 121           Layout (Root (arg, Layout (Box (H, index))))
 122       | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
 123           Layout (Box (H, p))
 124       | SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
 125           Layout (Box (V, p))
 126       | SYMBOL "\\BREAK" -> Layout Break
 127       | SYMBOL "["; p = l1_pattern; SYMBOL "]" -> Layout (Box (H, p))
 128       | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
 129           Variable (Ascription (Layout (Box (H, p)), id))
 130       ]
 131     | "simple" NONA
 132       [ m = l1_magic_pattern -> Magic m
 133       | v = l1_pattern_variable -> Variable v
 134       ]
 135     ];
 136 (* }}} *)
 137 (* {{{ Grammar for ast patterns, notation level 2 *)
 138   level2_pattern: [ [ p = l2_pattern -> p ] ];
 139   sort: [
 140     [ SYMBOL "\\PROP" -> `Prop
 141     | SYMBOL "\\SET" -> `Set
 142     | SYMBOL "\\TYPE" -> `Type
 143     ]
 144   ];
 145   explicit_subst: [
 146     [ (* TODO explicit substitution *)
 147     ]
 148   ];
 149   meta_subst: [
 150     [ (* TODO meta substitution *)
 151     ]
 152   ];
 153   possibly_typed_name: [
 154     [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
 155         Cic.Name id, Some typ
 156     | id = IDENT -> Cic.Name id, None
 157     ]
 158   ];
 159   match_pattern: [
 160     [ id = IDENT -> id, []
 161     | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
 162         id, vars
 163     ]
 164   ];
 165   binder: [
 166     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
 167     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
 168     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
 169     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
 170     ]
 171   ];
 172   bound_names: [
 173     [ vars = LIST1 IDENT SEP SYMBOL ",";
 174       ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
 175         [ vars, ty ]
 176     | clusters = LIST1 [
 177         SYMBOL "(";
 178         vars = LIST1 IDENT SEP SYMBOL ",";
 179         ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
 180         SYMBOL ")" ->
 181           vars, ty
 182       ] ->
 183         clusters
 184     ]
 185   ];
 186   induction_kind: [
 187     [ IDENT "rec" -> `Inductive
 188     | IDENT "corec" -> `CoInductive
 189     ]
 190   ];
 191   let_defs: [
 192     [ defs = LIST1 [
 193         name = IDENT; args = bound_names;
 194         index_name = OPT [ IDENT "on"; id = IDENT -> id ];
 195         ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
 196         SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
 197           let body = fold_binder `Lambda args body in
 198           let ty =
 199             match ty with
 200             | None -> None
 201             | Some ty -> Some (fold_binder `Pi args ty)
 202           in
 203           let rec position_of name p = function
 204             | [] -> None, p
 205             | n :: _ when n = name -> Some p, p
 206             | _ :: tl -> position_of name (p + 1) tl
 207           in
 208           let rec find_arg name n = function
 209             | [] -> fail loc (sprintf "Argument %s not found" name)
 210             | (l,_) :: tl ->
 211                 (match position_of name 0 l with
 212                 | None, len -> find_arg name (n + len) tl
 213                 | Some where, len -> n + where)
 214           in
 215           let index =
 216             match index_name with
 217             | None -> 0
 218             | Some name -> find_arg name 0 args
 219           in
 220           (Cic.Name name, ty), body, index
 221       ] SEP IDENT "and" ->
 222         defs
 223     ]
 224   ];
 225   l2_pattern_variable: [
 226     [ SYMBOL "\\NUM"; id = IDENT -> NumVar id
 227     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
 228     | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
 229     ]
 230   ];
 231   l2_magic_pattern: [
 232     [ SYMBOL "\\FOLD";
 233       kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
 234       base = l2_pattern;
 235       SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern ->
 236         Fold (kind, base, [id], recursive)
 237     | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern ->
 238         Default (some, none)
 239     ]
 240   ];
 241   l2_pattern:
 242     [ "letin" NONA
 243       [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
 244         p1 = l2_pattern; "in"; p2 = l2_pattern ->
 245           LetIn (var, p1, p2)
 246       | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
 247         body = l2_pattern ->
 248           LetRec (k, defs, body)
 249       ]
 250     | "binder" RIGHTA
 251       [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
 252           fold_binder b names body
 253       ]
 254     | "extension"
 255       [ ]
 256     | "apply" LEFTA
 257       [ p1 = l2_pattern; p2 = l2_pattern ->
 258           let rec aux = function
 259             | Appl (hd :: tl) -> aux hd @ tl
 260             | term -> [term]
 261           in
 262           Appl (aux p1 @ [p2])
 263       ]
 264     | "simple" NONA
 265       [ id = IDENT -> Ident (id, None)
 266       | id = IDENT; s = explicit_subst -> Ident (id, Some s)
 267       | u = URI -> Uri (u, None)
 268       | n = NUMBER -> Num (n, 0)
 269       | IMPLICIT -> Implicit
 270       | m = META -> Meta (int_of_string m, [])
 271       | m = META; s = meta_subst -> Meta (int_of_string m, s)
 272       | s = sort -> Sort s
 273       | s = SYMBOL -> Symbol (s, 0)
 274       | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
 275         IDENT "match"; t = l2_pattern;
 276         indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
 277         IDENT "with"; SYMBOL "[";
 278         patterns = LIST0 [
 279           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 280           rhs = l2_pattern ->
 281             lhs, rhs
 282         ] SEP SYMBOL "|";
 283         SYMBOL "]" ->
 284           Case (t, indty_ident, outtyp, patterns)
 285       | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
 286           Appl [ Symbol ("cast", 0); p1; p2 ]
 287       | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p
 288       | v = l2_pattern_variable -> Variable v
 289       | m = l2_magic_pattern -> Magic m
 290       ]
 291     ];
 292 (* }}} *)
 293 (* {{{ Grammar for interpretation, notation level 3 *)
 294   level3_interpretation: [ [ i = interpretation -> () ] ];
 295   argument: [
 296     [ i = IDENT -> ()
 297     | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> ()
 298     | SYMBOL <:unicode<eta>> (* η *); i = IDENT; SYMBOL "."; a = SELF -> ()
 299     ]
 300   ];
 301   l3_term: [
 302     [ u = URI -> ()
 303     | a = argument -> ()
 304     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" -> ()
 305     ]
 306   ];
 307 (* }}} *)
 308 (* {{{ Notation glues *)
 309   associativity: [
 310     [ IDENT "left";  IDENT "associative" -> `Left
 311     | IDENT "right"; IDENT "associative" -> `Right
 312     ]
 313   ];
 314   precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ];
 315   notation: [
 316     [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern;
 317       assoc = OPT associativity; prec = OPT precedence ->
 318         ()
 319     ]
 320   ];
 321   interpretation: [
 322     [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
 323       t = l3_term ->
 324         ()
 325     ]
 326   ];
 327 (* }}} *)
 328 END
 329
 330 let exc_located_wrapper f =
 331   try
 332     f ()
 333   with
 334   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 335       raise (Parse_error (floc, msg))
 336   | Stdpp.Exc_located (floc, exn) ->
 337       raise (Parse_error (floc, (Printexc.to_string exn)))
 338
 339 let parse_syntax_pattern stream =
 340   exc_located_wrapper
 341     (fun () ->
 342       (NotationGrammar.Entry.parse level1_pattern
 343         (NotationGrammar.parsable stream)))
 344
 345 let parse_ast_pattern stream =
 346   exc_located_wrapper
 347     (fun () ->
 348       (NotationGrammar.Entry.parse level2_pattern
 349         (NotationGrammar.parsable stream)))
 350
 351 let parse_interpretation stream =
 352   exc_located_wrapper
 353     (fun () ->
 354       (NotationGrammar.Entry.parse level3_interpretation
 355         (NotationGrammar.parsable stream)))
 356
 357 (* vim:set encoding=utf8 foldmethod=marker: *)