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