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 exception Level_not_found of int
  30
  31 let grammar = Grammar.gcreate CicNotationLexer.notation_lexer
  32
  33 let level1_pattern = Grammar.Entry.create grammar "level1_pattern"
  34 let level2_pattern = Grammar.Entry.create grammar "level2_pattern"
  35 let level3_term = Grammar.Entry.create grammar "level3_term"
  36 let notation = Grammar.Entry.create grammar "notation" (* level1 <-> level 2 *)
  37 let interpretation =
  38   Grammar.Entry.create grammar "interpretation" (* level2 <-> level 3 *)
  39
  40 let return_term loc term = ()
  41
  42 let loc_of_floc = function
  43   | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
  44       (loc_begin, loc_end)
  45
  46 let fail floc msg =
  47   let (x, y) = loc_of_floc floc in
  48   failwith (sprintf "Error at characters %d - %d: %s" x y msg)
  49
  50 let int_of_string s =
  51   try
  52     Pervasives.int_of_string s
  53   with Failure _ ->
  54     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
  55
  56 open CicNotationPt
  57
  58 let boxify = function
  59   | [ a ] -> a
  60   | l -> Layout (Box (H, l))
  61
  62 let fold_binder binder pt_names body =
  63   let fold_cluster binder names ty body =
  64     List.fold_right
  65       (fun name body -> Binder (binder, (Cic.Name name, ty), body))
  66       names body
  67   in
  68   List.fold_right
  69     (fun (names, ty) body -> fold_cluster binder names ty body)
  70     pt_names body
  71
  72 let return_term loc term = AttributedTerm (`Loc loc, term)
  73
  74 EXTEND
  75   GLOBAL: level1_pattern level2_pattern level3_term
  76           notation interpretation;
  77 (* {{{ Grammar for concrete syntax patterns, notation level 1 *)
  78   level1_pattern: [ [ p = l1_pattern; EOI -> boxify p ] ];
  79   l1_pattern: [ [ p = LIST0 l1_simple_pattern -> p ] ];
  80   literal: [
  81     [ s = SYMBOL -> `Symbol s
  82     | k = KEYWORD -> `Keyword k
  83     | n = NUMBER -> `Number n
  84     ]
  85   ];
  86   sep:       [ [ SYMBOL "\\SEP";      sep = literal -> sep ] ];
  87 (*   row_sep:   [ [ SYMBOL "\\ROWSEP";   sep = literal -> sep ] ];
  88   field_sep: [ [ SYMBOL "\\FIELDSEP"; sep = literal -> sep ] ]; *)
  89   l1_magic_pattern: [
  90     [ SYMBOL "\\LIST0"; p = l1_simple_pattern; sep = OPT sep -> List0 (p, sep)
  91     | SYMBOL "\\LIST1"; p = l1_simple_pattern; sep = OPT sep -> List1 (p, sep)
  92     | SYMBOL "\\OPT";   p = l1_simple_pattern -> Opt p
  93     ]
  94   ];
  95   l1_pattern_variable: [
  96     [ id = IDENT -> TermVar id
  97     | SYMBOL "\\TERM"; id = IDENT -> TermVar id
  98     | SYMBOL "\\NUM"; id = IDENT -> NumVar id
  99     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
 100     ]
 101   ];
 102   l1_simple_pattern:
 103     [ "layout" LEFTA
 104       [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF ->
 105           return_term loc (Layout (Sub (p1, p2)))
 106       | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF ->
 107           return_term loc (Layout (Sup (p1, p2)))
 108       | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF ->
 109           return_term loc (Layout (Below (p1, p2)))
 110       | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF ->
 111           return_term loc (Layout (Above (p1, p2)))
 112       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\OVER"; p2 = l1_pattern;
 113         SYMBOL "]" ->
 114           return_term loc (Layout (Over (boxify p1, boxify p2)))
 115       | SYMBOL "["; p1 = l1_pattern; SYMBOL "\\ATOP"; p2 = l1_pattern;
 116         SYMBOL "]" ->
 117           return_term loc (Layout (Atop (boxify p1, boxify p2)))
 118 (*       | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
 119           return_term loc (Array (p, csep, rsep)) *)
 120       | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF ->
 121           return_term loc (Layout (Frac (p1, p2)))
 122       | SYMBOL "\\SQRT"; p = SELF -> return_term loc (Layout (Sqrt p))
 123       | SYMBOL "\\ROOT"; index = l1_pattern; SYMBOL "\\OF"; arg = SELF ->
 124           return_term loc (Layout (Root (arg, Layout (Box (H, index)))))
 125       | SYMBOL "\\HBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
 126           return_term loc (Layout (Box (H, p)))
 127       | SYMBOL "\\VBOX"; SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
 128           return_term loc (Layout (Box (V, p)))
 129       | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
 130       | SYMBOL "["; p = l1_pattern; SYMBOL "]" ->
 131           return_term loc (boxify p)
 132       | SYMBOL "["; p = l1_pattern; SYMBOL "\\AS"; id = IDENT; SYMBOL "]" ->
 133           return_term loc (Variable (Ascription (Layout (Box (H, p)), id)))
 134       ]
 135     | "simple" NONA
 136       [ m = l1_magic_pattern -> return_term loc (Magic m)
 137       | v = l1_pattern_variable -> return_term loc (Variable v)
 138       | l = literal -> return_term loc (Literal l)
 139       ]
 140     ];
 141 (* }}} *)
 142 (* {{{ Grammar for ast patterns, notation level 2 *)
 143   level2_pattern: [ [ p = l2_pattern -> p ] ];
 144   sort: [
 145     [ SYMBOL "\\PROP" -> `Prop
 146     | SYMBOL "\\SET" -> `Set
 147     | SYMBOL "\\TYPE" -> `Type
 148     ]
 149   ];
 150   explicit_subst: [
 151     [ (* TODO explicit substitution *)
 152     ]
 153   ];
 154   meta_subst: [
 155     [ (* TODO meta substitution *)
 156     ]
 157   ];
 158   possibly_typed_name: [
 159     [ SYMBOL "("; id = IDENT; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
 160         Cic.Name id, Some typ
 161     | id = IDENT -> Cic.Name id, None
 162     ]
 163   ];
 164   match_pattern: [
 165     [ id = IDENT -> id, []
 166     | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
 167         id, vars
 168     ]
 169   ];
 170   binder: [
 171     [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
 172     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
 173     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
 174     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
 175     ]
 176   ];
 177   bound_names: [
 178     [ vars = LIST1 IDENT SEP SYMBOL ",";
 179       ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
 180         [ vars, ty ]
 181     | clusters = LIST1 [
 182         SYMBOL "(";
 183         vars = LIST1 IDENT SEP SYMBOL ",";
 184         ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
 185         SYMBOL ")" ->
 186           vars, ty
 187       ] ->
 188         clusters
 189     ]
 190   ];
 191   induction_kind: [
 192     [ IDENT "rec" -> `Inductive
 193     | IDENT "corec" -> `CoInductive
 194     ]
 195   ];
 196   let_defs: [
 197     [ defs = LIST1 [
 198         name = IDENT; args = bound_names;
 199         index_name = OPT [ IDENT "on"; id = IDENT -> id ];
 200         ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
 201         SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
 202           let body = fold_binder `Lambda args body in
 203           let ty =
 204             match ty with
 205             | None -> None
 206             | Some ty -> Some (fold_binder `Pi args ty)
 207           in
 208           let rec position_of name p = function
 209             | [] -> None, p
 210             | n :: _ when n = name -> Some p, p
 211             | _ :: tl -> position_of name (p + 1) tl
 212           in
 213           let rec find_arg name n = function
 214             | [] -> fail loc (sprintf "Argument %s not found" name)
 215             | (l,_) :: tl ->
 216                 (match position_of name 0 l with
 217                 | None, len -> find_arg name (n + len) tl
 218                 | Some where, len -> n + where)
 219           in
 220           let index =
 221             match index_name with
 222             | None -> 0
 223             | Some name -> find_arg name 0 args
 224           in
 225           (Cic.Name name, ty), body, index
 226       ] SEP IDENT "and" ->
 227         defs
 228     ]
 229   ];
 230   l2_pattern_variable: [
 231     [ SYMBOL "\\NUM"; id = IDENT -> NumVar id
 232     | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
 233     | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
 234     ]
 235   ];
 236   l2_magic_pattern: [
 237     [ SYMBOL "\\FOLD";
 238       kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
 239       base = l2_pattern;
 240       SYMBOL "\\LAMBDA"; id = IDENT; recursive = l2_pattern ->
 241         Fold (kind, base, [id], recursive)
 242     | SYMBOL "\\DEFAULT"; some = l2_pattern; none = l2_pattern ->
 243         Default (some, none)
 244     ]
 245   ];
 246   l2_pattern:
 247     [ "0" [ ]
 248     | "10" NONA (* let in *)
 249       [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
 250         p1 = l2_pattern; "in"; p2 = l2_pattern ->
 251           return_term loc (LetIn (var, p1, p2))
 252       | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
 253         body = l2_pattern ->
 254           return_term loc (LetRec (k, defs, body))
 255       ]
 256     | "20" RIGHTA (* binder *)
 257       [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
 258           return_term loc (fold_binder b names body)
 259       ]
 260     | "30" [ ]
 261     | "40" [ ]
 262     | "50" [ ]
 263     | "60" [ ]
 264     | "70" LEFTA (* apply *)
 265       [ p1 = l2_pattern; p2 = l2_pattern ->
 266           let rec aux = function
 267             | Appl (hd :: tl)
 268             | AttributedTerm (_, Appl (hd :: tl)) ->
 269                 aux hd @ tl
 270             | term -> [term]
 271           in
 272           return_term loc (Appl (aux p1 @ [p2]))
 273       ]
 274     | "80" [ ]
 275     | "90" NONA (* simple *)
 276       [ id = IDENT -> return_term loc (Ident (id, None))
 277       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
 278       | u = URI -> return_term loc (Uri (u, None))
 279       | n = NUMBER -> return_term loc (Num (n, 0))
 280       | IMPLICIT -> return_term loc (Implicit)
 281       | m = META -> return_term loc (Meta (int_of_string m, []))
 282       | m = META; s = meta_subst -> return_term loc (Meta (int_of_string m, s))
 283       | s = sort -> return_term loc (Sort s)
 284       | s = SYMBOL -> return_term loc (Symbol (s, 0))
 285       | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
 286         IDENT "match"; t = l2_pattern;
 287         indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
 288         IDENT "with"; SYMBOL "[";
 289         patterns = LIST0 [
 290           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
 291           rhs = l2_pattern ->
 292             lhs, rhs
 293         ] SEP SYMBOL "|";
 294         SYMBOL "]" ->
 295           return_term loc (Case (t, indty_ident, outtyp, patterns))
 296       | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
 297           return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ])
 298       | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p
 299       | v = l2_pattern_variable -> return_term loc (Variable v)
 300       | m = l2_magic_pattern -> return_term loc (Magic m)
 301       ]
 302     | "100" [ ]
 303     ];
 304 (* }}} *)
 305 (* {{{ Grammar for interpretation, notation level 3 *)
 306   argument: [
 307     [ id = IDENT -> IdentArg id
 308     | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a)
 309     | SYMBOL <:unicode<eta>> (* η *); id = IDENT; SYMBOL "."; a = SELF ->
 310         EtaArg (Some id, a)
 311     ]
 312   ];
 313   level3_term: [
 314     [ u = URI -> UriPattern u
 315     | a = argument -> ArgPattern a
 316     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
 317         (match terms with
 318         | [] -> assert false
 319         | [term] -> term
 320         | terms -> ApplPattern terms)
 321     ]
 322   ];
 323 (* }}} *)
 324 (* {{{ Notation glues *)
 325   associativity: [
 326     [ IDENT "left";  IDENT "associative" -> `Left
 327     | IDENT "right"; IDENT "associative" -> `Right
 328     ]
 329   ];
 330   precedence: [ [ IDENT "at"; IDENT "precedence"; n = NUMBER -> n ] ];
 331   notation: [
 332     [ IDENT "notation"; p1 = level1_pattern; IDENT "for"; p2 = level2_pattern;
 333       assoc = OPT associativity; prec = OPT precedence ->
 334         ()
 335     ]
 336   ];
 337   interpretation: [
 338     [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
 339       t = level3_term ->
 340         ()
 341     ]
 342   ];
 343 (* }}} *)
 344 END
 345
 346 let exc_located_wrapper f =
 347   try
 348     f ()
 349   with
 350   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 351       raise (Parse_error (floc, msg))
 352   | Stdpp.Exc_located (floc, exn) ->
 353       raise (Parse_error (floc, (Printexc.to_string exn)))
 354
 355 let parse_syntax_pattern stream =
 356   exc_located_wrapper (fun () -> Grammar.Entry.parse level1_pattern stream)
 357
 358 let parse_ast_pattern stream =
 359   exc_located_wrapper (fun () -> Grammar.Entry.parse level2_pattern stream)
 360
 361 let parse_interpretation stream =
 362   exc_located_wrapper (fun () -> Grammar.Entry.parse level3_term stream)
 363
 364 (** {2 Grammar extension} *)
 365
 366 type associativity_kind = [ `Left | `Right | `None ]
 367
 368 let symbol s = Gramext.Stoken ("SYMBOL", s)
 369 let ident s = Gramext.Stoken ("IDENT", s)
 370 let number s = Gramext.Stoken ("NUMBER", s)
 371 let term = Gramext.Sself
 372
 373 type env_type = (string * (value_type * value)) list
 374
 375 let make_action action =
 376   let rec aux (vl : env_type) =
 377     function
 378       [] -> Gramext.action (fun (loc: location) -> action vl loc)
 379     | None :: tl -> Gramext.action (fun _ -> aux vl tl)
 380     | Some (name, typ) :: tl ->
 381         (* i tipi servono? Magari servono solo quando si verifica la
 382          * correttezza della notazione?
 383          *)
 384         Gramext.action (fun (v: value) -> aux ((name, (typ, v))::vl) tl)
 385   in
 386     aux []
 387
 388 let flatten_opt =
 389   let rec aux acc =
 390     function
 391       [] -> List.rev acc
 392     | None::tl -> aux acc tl
 393     | Some hd::tl -> aux (hd::acc) tl
 394   in
 395   aux []
 396
 397   (* given a level 1 pattern computes the new RHS of "term" grammar entry *)
 398 let extract_term_production pattern =
 399   let rec aux = function
 400     | Literal l -> aux_literal l
 401     | Layout l -> aux_layout l
 402     | Magic m -> aux_magic m
 403     | Variable v -> aux_variable v
 404     | _ -> assert false
 405   and aux_literal = function
 406     | `Symbol s -> [None, symbol s]
 407     | `Keyword s -> [None, ident s]
 408     | `Number s -> [None, number s]
 409   and aux_layout = function
 410     | Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
 411     | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
 412     | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
 413     | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
 414     | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
 415     | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
 416     | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
 417     | Root (p1, p2) ->
 418         [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
 419     | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
 420     | Break -> []
 421     | Box (_, pl) -> List.flatten (List.map aux pl)
 422   and aux_magic = function
 423     | Opt p ->
 424         let p_bindings, p_atoms = List.split (aux p) in
 425         let p_names = flatten_opt p_bindings in
 426         [ None,
 427           Gramext.srules
 428             [ [ Gramext.Sopt
 429                   (Gramext.srules
 430                     [ p_atoms,
 431                       (make_action
 432                         (fun (env : env_type) (loc : location) -> env)
 433                         p_bindings)])],
 434               Gramext.action
 435                 (fun (env_opt : env_type option) (loc : location) ->
 436                   match env_opt with
 437                     Some env ->
 438                       List.map
 439                         (fun (name, (typ, v)) ->
 440                           (name, (OptType typ, OptValue (Some v))))
 441                         env
 442                   | None ->
 443                       List.map
 444                         (fun (name, typ) ->
 445                           (name, (OptType typ, OptValue None)))
 446                         p_names) ]]
 447     | _ -> assert false
 448   and aux_variable = function
 449     | NumVar s -> [Some (s, NumType), number ""]
 450     | TermVar s -> [Some (s, TermType), term]
 451     | IdentVar s -> [Some (s, StringType), ident ""]
 452     | Ascription (p, s) -> assert false (* TODO *)
 453     | FreshVar _ -> assert false
 454   in
 455   aux pattern
 456
 457 let level_of_int precedence =
 458   (* TODO "mod" test to be removed as soon as we add all 100 levels *)
 459   if precedence mod 10 <> 0 || precedence < 0 || precedence > 100 then
 460     raise (Level_not_found precedence);
 461   string_of_int precedence
 462
 463 type rule_id = term Grammar.Entry.e * Token.t Gramext.g_symbol list
 464
 465 let extend level1_pattern ?(precedence = 0) ?associativity action =
 466   let p_bindings, p_atoms =
 467     List.split (extract_term_production level1_pattern)
 468   in
 469   let level = level_of_int precedence in
 470   let p_names = flatten_opt p_bindings in
 471   let entry = Grammar.Entry.obj (level2_pattern: 'a Grammar.Entry.e) in
 472   let _ =
 473     Grammar.extend
 474       [ entry, Some (Gramext.Level level),
 475         [ Some level,  (* TODO should we put None here? *)
 476           associativity,
 477           [ p_atoms,
 478             (make_action
 479               (fun (env: env_type)(loc: location) -> TermValue (action env loc))
 480               p_bindings) ]]]
 481   in
 482   (level2_pattern, p_atoms)
 483
 484 let delete (entry, atoms) = Grammar.delete_rule entry atoms
 485
 486 let print_level2_pattern () =
 487   Grammar.print_entry Format.std_formatter (Grammar.Entry.obj level2_pattern);
 488   Format.pp_print_flush Format.std_formatter ()
 489
 490 (* vim:set encoding=utf8 foldmethod=marker: *)