matita/components/grafite_parser/grafiteParser.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 (* $Id$ *)
  27
  28 module N  = NotationPt
  29 module G  = GrafiteAst
  30 module L  = LexiconAst
  31 module LE = LexiconEngine
  32
  33 exception NoInclusionPerformed of string (* full path *)
  34
  35 type 'a localized_option =
  36    LSome of 'a
  37  | LNone of G.loc
  38
  39 type ast_statement = G.statement
  40
  41 type 'status statement =
  42   ?never_include:bool ->
  43     (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
  44   include_paths:string list -> (#LE.status as 'status) ->
  45     'status * ast_statement localized_option
  46
  47 type 'status parser_status = {
  48   grammar : Grammar.g;
  49   term : N.term Grammar.Entry.e;
  50   statement : #LE.status as 'status statement Grammar.Entry.e;
  51 }
  52
  53 let grafite_callback = ref (fun _ -> ())
  54 let set_grafite_callback cb = grafite_callback := cb
  55
  56 let lexicon_callback = ref (fun _ -> ())
  57 let set_lexicon_callback cb = lexicon_callback := cb
  58
  59 let initial_parser () =
  60   let grammar = CicNotationParser.level2_ast_grammar () in
  61   let term = CicNotationParser.term () in
  62   let statement = Grammar.Entry.create grammar "statement" in
  63   { grammar = grammar; term = term; statement = statement }
  64 ;;
  65
  66 let grafite_parser = ref (initial_parser ())
  67
  68 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
  69
  70 let default_associativity = Gramext.NonA
  71
  72 let mk_rec_corec ind_kind defs loc =
  73  (* In case of mutual definitions here we produce just
  74     the syntax tree for the first one. The others will be
  75     generated from the completely specified term just before
  76     insertion in the environment. We use the flavour
  77     `MutualDefinition to rememer this. *)
  78   let name,ty =
  79     match defs with
  80     | (params,(N.Ident (name, None), ty),_,_) :: _ ->
  81         let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
  82         let ty =
  83          List.fold_right
  84           (fun var ty -> N.Binder (`Pi,var,ty)
  85           ) params ty
  86         in
  87          name,ty
  88     | _ -> assert false
  89   in
  90   let body = N.Ident (name,None) in
  91   let flavour =
  92    if List.length defs = 1 then
  93     `Definition
  94    else
  95     `MutualDefinition
  96   in
  97    (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
  98
  99 let nmk_rec_corec ind_kind defs loc =
 100  let loc,t = mk_rec_corec ind_kind defs loc in
 101   G.NObj (loc,t)
 102
 103 (*
 104 let nnon_punct_of_punct = function
 105   | G.Skip loc -> G.NSkip loc
 106   | G.Unfocus loc -> G.NUnfocus loc
 107   | G.Focus (loc,l) -> G.NFocus (loc,l)
 108 ;; *)
 109
 110 let cons_ntac t p =
 111   match t with
 112   | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p])
 113   | x -> x
 114 ;;
 115
 116 type by_continuation =
 117    BYC_done
 118  | BYC_weproved of N.term * string option * N.term option
 119  | BYC_letsuchthat of string * N.term * string * N.term
 120  | BYC_wehaveand of string * N.term * string * N.term
 121
 122 let initialize_parser () =
 123   (* {{{ parser initialization *)
 124   let term = !grafite_parser.term in
 125   let statement = !grafite_parser.statement in
 126   let let_defs = CicNotationParser.let_defs () in
 127   let protected_binder_vars = CicNotationParser.protected_binder_vars () in
 128 EXTEND
 129   GLOBAL: term statement;
 130   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
 131   tactic_term: [ [ t = term LEVEL "90" -> t ] ];
 132   new_name: [
 133     [ SYMBOL "_" -> None
 134     | id = IDENT -> Some id ]
 135     ];
 136   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
 137   ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
 138   tactic_term_list1: [
 139     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
 140   ];
 141   reduction_kind: [
 142     [ IDENT "normalize" -> `Normalize
 143     | IDENT "simplify" -> `Simpl
 144     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
 145     | IDENT "whd" -> `Whd ]
 146   ];
 147   nreduction_kind: [
 148     [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
 149        let delta = match delta with None -> true | _ -> false in
 150         `Normalize delta
 151     (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
 152     | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
 153        let delta = match delta with None -> true | _ -> false in
 154         `Whd delta]
 155   ];
 156   sequent_pattern_spec: [
 157    [ hyp_paths =
 158       LIST0
 159        [ id = IDENT ;
 160          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
 161          (id,match path with Some p -> p | None -> N.UserInput) ];
 162      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
 163       let goal_path =
 164        match goal_path, hyp_paths with
 165           None, [] -> Some N.UserInput
 166         | None, _::_ -> None
 167         | Some goal_path, _ -> Some goal_path
 168       in
 169        hyp_paths,goal_path
 170    ]
 171   ];
 172   pattern_spec: [
 173     [ res = OPT [
 174        "in";
 175        wanted_and_sps =
 176         [ "match" ; wanted = tactic_term ;
 177           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 178            Some wanted,sps
 179         | sps = sequent_pattern_spec ->
 180            None,Some sps
 181         ] ->
 182          let wanted,hyp_paths,goal_path =
 183           match wanted_and_sps with
 184              wanted,None -> wanted, [], Some N.UserInput
 185            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 186          in
 187           wanted, hyp_paths, goal_path ] ->
 188       match res with
 189          None -> None,[],Some N.UserInput
 190        | Some ps -> ps]
 191   ];
 192   inverter_param_list: [
 193     [ params = tactic_term ->
 194       let deannotate = function
 195         | N.AttributedTerm (_,t) | t -> t
 196       in match deannotate params with
 197       | N.Implicit _ -> [false]
 198       | N.UserInput -> [true]
 199       | N.Appl l ->
 200          List.map (fun x -> match deannotate x with
 201            | N.Implicit _ -> false
 202            | N.UserInput -> true
 203            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
 204       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ]
 205   ];
 206   direction: [
 207     [ SYMBOL ">" -> `LeftToRight
 208     | SYMBOL "<" -> `RightToLeft ]
 209   ];
 210   int: [ [ num = NUMBER -> int_of_string num ] ];
 211   intros_names: [
 212    [ idents = OPT ident_list0 ->
 213       match idents with None -> [] | Some idents -> idents
 214    ]
 215   ];
 216   intros_spec: [
 217     [ OPT [ IDENT "names" ];
 218       num = OPT [ num = int -> num ];
 219       idents = intros_names ->
 220         num, idents
 221     ]
 222   ];
 223   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 224   ntactic: [
 225     [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
 226     | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
 227     | IDENT "nassert";
 228        seqs = LIST0 [
 229         hyps = LIST0
 230          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 231          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 232                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 233             id,`Def (bo,ty)];
 234         SYMBOL <:unicode<vdash>>;
 235         concl = tactic_term -> (List.rev hyps,concl) ] ->
 236          G.NTactic(loc,[G.NAssert (loc, seqs)])
 237     | IDENT "nauto"; params = auto_params ->
 238         G.NTactic(loc,[G.NAuto (loc, params)])
 239     | SYMBOL "/"; num = OPT NUMBER ;
 240        params = nauto_params; SYMBOL "/" ;
 241        just = OPT [ IDENT "by"; by =
 242          [ univ = tactic_term_list1 -> `Univ univ
 243          | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
 244          | SYMBOL "_" -> `Trace ] -> by ] ->
 245        let depth = match num with Some n -> n | None -> "1" in
 246        (match just with
 247        | None ->
 248            G.NTactic(loc,
 249             [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
 250        | Some (`Univ univ) ->
 251            G.NTactic(loc,
 252             [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
 253        | Some `EmptyUniv ->
 254            G.NTactic(loc,
 255             [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
 256        | Some `Trace ->
 257            G.NMacro(loc,
 258              G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
 259     | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
 260     | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
 261     | IDENT "screenshot"; fname = QSTRING ->
 262         G.NMacro(loc,G.Screenshot (loc, fname))
 263     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 264         G.NTactic(loc,[G.NCases (loc, what, where)])
 265     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 266         G.NTactic(loc,[G.NChange (loc, what, with_what)])
 267     | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
 268         G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
 269     | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
 270 (*  | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
 271     | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
 272     | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
 273       exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
 274         -> let exclude' = match exclude with None -> [] | Some l -> l in
 275            G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
 276     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 277         G.NTactic(loc,[G.NElim (loc, what, where)])
 278     | IDENT "ngeneralize"; p=pattern_spec ->
 279         G.NTactic(loc,[G.NGeneralize (loc, p)])
 280     | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
 281         G.NTactic(loc,[G.NInversion (loc, what, where)])
 282     | IDENT "nlapply"; t = tactic_term -> G.NTactic(loc,[G.NLApply (loc, t)])
 283     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 284         where = pattern_spec ->
 285         G.NTactic(loc,[G.NLetIn (loc,where,t,name)])
 286     | kind = nreduction_kind; p = pattern_spec ->
 287         G.NTactic(loc,[G.NReduce (loc, kind, p)])
 288     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 289         G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
 290     | IDENT "ntry"; tac = SELF ->
 291         let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
 292         G.NTactic(loc,[ G.NTry (loc,tac)])
 293     | IDENT "nrepeat"; tac = SELF ->
 294         let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
 295         G.NTactic(loc,[ G.NRepeat (loc,tac)])
 296     | LPAREN; l = LIST1 SELF; RPAREN ->
 297         let l =
 298           List.flatten
 299             (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
 300         G.NTactic(loc,[G.NBlock (loc,l)])
 301     | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
 302     | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
 303     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
 304     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
 305     | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
 306     ]
 307   ];
 308   auto_fixed_param: [
 309    [ IDENT "demod"
 310    | IDENT "fast_paramod"
 311    | IDENT "paramod"
 312    | IDENT "depth"
 313    | IDENT "width"
 314    | IDENT "size"
 315    | IDENT "timeout"
 316    | IDENT "library"
 317    | IDENT "type"
 318    | IDENT "all"
 319    ]
 320 ];
 321   auto_params: [
 322     [ params =
 323       LIST0 [
 324          i = auto_fixed_param -> i,""
 325        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 326               string_of_int v | v = IDENT -> v ] -> i,v ];
 327       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
 328       (* (match tl with Some l -> l | None -> []), *)
 329       params
 330    ]
 331 ];
 332   nauto_params: [
 333     [ params =
 334       LIST0 [
 335          i = auto_fixed_param -> i,""
 336        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 337               string_of_int v | v = IDENT -> v ] -> i,v ] ->
 338       params
 339    ]
 340 ];
 341
 342   by_continuation: [
 343     [ WEPROVED; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1)
 344     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 345             "done" -> BYC_weproved (ty,None,t1)
 346     | "done" -> BYC_done
 347     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 348       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 349       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 350     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 351               BYC_wehaveand (id1,t1,id2,t2)
 352     ]
 353 ];
 354   rewriting_step_continuation : [
 355     [ "done" -> true
 356     | -> false
 357     ]
 358 ];
 359 (* MATITA 1.0
 360   atomic_tactical:
 361     [ "sequence" LEFTA
 362       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 363           let ts =
 364             match t1 with
 365             | G.Seq (_, l) -> l @ [ t2 ]
 366             | _ -> [ t1; t2 ]
 367           in
 368           G.Seq (loc, ts)
 369       ]
 370     | "then" NONA
 371       [ tac = SELF; SYMBOL ";";
 372         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 373           (G.Then (loc, tac, tacs))
 374       ]
 375     | "loops" RIGHTA
 376       [ IDENT "do"; count = int; tac = SELF ->
 377           G.Do (loc, count, tac)
 378       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 379       ]
 380     | "simple" NONA
 381       [ IDENT "first";
 382         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 383           G.First (loc, tacs)
 384       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 385       | IDENT "solve";
 386         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 387           G.Solve (loc, tacs)
 388       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 389       | LPAREN; tac = SELF; RPAREN -> tac
 390       | tac = tactic -> tac
 391         ]
 392       ];
 393 *)
 394   npunctuation_tactical:
 395     [
 396       [ SYMBOL "[" -> G.NBranch loc
 397       | SYMBOL "|" -> G.NShift loc
 398       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
 399       | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
 400       | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
 401       | SYMBOL "]" -> G.NMerge loc
 402       | SYMBOL ";" -> G.NSemicolon loc
 403       | SYMBOL "." -> G.NDot loc
 404       ]
 405     ];
 406   nnon_punctuation_tactical:
 407     [ "simple" NONA
 408       [ IDENT "focus"; goals = LIST1 int -> G.NFocus (loc, goals)
 409       | IDENT "unfocus" -> G.NUnfocus loc
 410       | IDENT "skip" -> G.NSkip loc
 411       ]
 412       ];
 413   ntheorem_flavour: [
 414     [ [ IDENT "ndefinition"  ] -> `Definition
 415     | [ IDENT "nfact"        ] -> `Fact
 416     | [ IDENT "nlemma"       ] -> `Lemma
 417     | [ IDENT "nremark"      ] -> `Remark
 418     | [ IDENT "ntheorem"     ] -> `Theorem
 419     ]
 420   ];
 421   theorem_flavour: [
 422     [ [ IDENT "definition"  ] -> `Definition
 423     | [ IDENT "fact"        ] -> `Fact
 424     | [ IDENT "lemma"       ] -> `Lemma
 425     | [ IDENT "remark"      ] -> `Remark
 426     | [ IDENT "theorem"     ] -> `Theorem
 427     ]
 428   ];
 429   inline_flavour: [
 430      [ attr = theorem_flavour -> attr
 431      | [ IDENT "axiom"     ]  -> `Axiom
 432      | [ IDENT "variant"   ]  -> `Variant
 433      ]
 434   ];
 435   inductive_spec: [ [
 436     fst_name = IDENT;
 437       params = LIST0 protected_binder_vars;
 438     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 439     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 440     tl = OPT [ "with";
 441         types = LIST1 [
 442           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 443          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 444             (name, true, typ, constructors) ] SEP "with" -> types
 445       ] ->
 446         let params =
 447           List.fold_right
 448             (fun (names, typ) acc ->
 449               (List.map (fun name -> (name, typ)) names) @ acc)
 450             params []
 451         in
 452         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 453         let tl_ind_types = match tl with None -> [] | Some types -> types in
 454         let ind_types = fst_ind_type :: tl_ind_types in
 455         (params, ind_types)
 456     ] ];
 457
 458     record_spec: [ [
 459       name = IDENT;
 460       params = LIST0 protected_binder_vars;
 461        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 462        fields = LIST0 [
 463          name = IDENT ;
 464          coercion = [
 465              SYMBOL ":" -> false,0
 466            | SYMBOL ":"; SYMBOL ">" -> true,0
 467            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 468          ];
 469          ty = term ->
 470            let b,n = coercion in
 471            (name,ty,b,n)
 472        ] SEP SYMBOL ";"; SYMBOL "}" ->
 473         let params =
 474           List.fold_right
 475             (fun (names, typ) acc ->
 476               (List.map (fun name -> (name, typ)) names) @ acc)
 477             params []
 478         in
 479         (params,name,typ,fields)
 480     ] ];
 481
 482     alias_spec: [
 483       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 484         let alpha = "[a-zA-Z]" in
 485         let num = "[0-9]+" in
 486         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 487         let decoration = "\\'" in
 488         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 489         let rex = Str.regexp ("^"^ident^"$") in
 490         if Str.string_match rex id 0 then
 491           if (try ignore (UriManager.uri_of_string uri); true
 492               with UriManager.IllFormedUri _ -> false) ||
 493              (try ignore (NReference.reference_of_string uri); true
 494               with NReference.IllFormedReference _ -> false)
 495           then
 496             L.Ident_alias (id, uri)
 497           else
 498             raise
 499              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 500         else
 501           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 502             Printf.sprintf "Not a valid identifier: %s" id)))
 503       | IDENT "symbol"; symbol = QSTRING;
 504         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 505         SYMBOL "="; dsc = QSTRING ->
 506           let instance =
 507             match instance with Some i -> i | None -> 0
 508           in
 509           L.Symbol_alias (symbol, instance, dsc)
 510       | IDENT "num";
 511         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 512         SYMBOL "="; dsc = QSTRING ->
 513           let instance =
 514             match instance with Some i -> i | None -> 0
 515           in
 516           L.Number_alias (instance, dsc)
 517       ]
 518      ];
 519     argument: [
 520       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 521         id = IDENT ->
 522           N.IdentArg (List.length l, id)
 523       ]
 524     ];
 525     associativity: [
 526       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 527       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 528       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 529       ]
 530     ];
 531     precedence: [
 532       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 533     ];
 534     notation: [
 535       [ dir = OPT direction; s = QSTRING;
 536         assoc = OPT associativity; prec = precedence;
 537         IDENT "for";
 538         p2 =
 539           [ blob = UNPARSED_AST ->
 540               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 541                 (CicNotationParser.parse_level2_ast
 542                   (Ulexing.from_utf8_string blob))
 543           | blob = UNPARSED_META ->
 544               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 545                 (CicNotationParser.parse_level2_meta
 546                   (Ulexing.from_utf8_string blob))
 547           ] ->
 548             let assoc =
 549               match assoc with
 550               | None -> default_associativity
 551               | Some assoc -> assoc
 552             in
 553             let p1 =
 554               add_raw_attribute ~text:s
 555                 (CicNotationParser.parse_level1_pattern prec
 556                   (Ulexing.from_utf8_string s))
 557             in
 558             (dir, p1, assoc, prec, p2)
 559       ]
 560     ];
 561     level3_term: [
 562       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 563       | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
 564       | IMPLICIT -> N.ImplicitPattern
 565       | id = IDENT -> N.VarPattern id
 566       | LPAREN; terms = LIST1 SELF; RPAREN ->
 567           (match terms with
 568           | [] -> assert false
 569           | [term] -> term
 570           | terms -> N.ApplPattern terms)
 571       ]
 572     ];
 573     interpretation: [
 574       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 575           (s, args, t)
 576       ]
 577     ];
 578
 579     include_command: [ [
 580         IDENT "include" ; path = QSTRING ->
 581           loc,path,true,L.WithPreferences
 582       | IDENT "include" ; IDENT "source" ; path = QSTRING ->
 583           loc,path,false,L.WithPreferences
 584       | IDENT "include'" ; path = QSTRING ->
 585           loc,path,true,L.WithoutPreferences
 586      ]];
 587
 588   grafite_ncommand: [ [
 589       IDENT "nqed" -> G.NQed loc
 590     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 591       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 592         G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
 593     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 594       body = term ->
 595         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
 596     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 597         G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
 598     | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
 599     | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
 600       paramspec = OPT inverter_param_list ;
 601       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
 602         G.NInverter (loc,name,indty,paramspec,outsort)
 603     | NLETCOREC ; defs = let_defs ->
 604         nmk_rec_corec `CoInductive defs loc
 605     | NLETREC ; defs = let_defs ->
 606         nmk_rec_corec `Inductive defs loc
 607     | IDENT "ninductive"; spec = inductive_spec ->
 608         let (params, ind_types) = spec in
 609         G.NObj (loc, N.Inductive (params, ind_types))
 610     | IDENT "ncoinductive"; spec = inductive_spec ->
 611         let (params, ind_types) = spec in
 612         let ind_types = (* set inductive flags to false (coinductive) *)
 613           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 614             ind_types
 615         in
 616         G.NObj (loc, N.Inductive (params, ind_types))
 617     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
 618         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
 619         let urify = function
 620           | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
 621               NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
 622           | _ -> raise (Failure "only a Type[…] sort can be constrained")
 623         in
 624         let u1 = urify u1 in
 625         let u2 = urify u2 in
 626          G.NUnivConstraint (loc,u1,u2)
 627     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 628         G.UnificationHint (loc, t, n)
 629     | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
 630         SYMBOL <:unicode<def>>; t = term; "on";
 631         id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
 632         "to"; target = term ->
 633           G.NCoercion(loc,name,t,ty,(id,source),target)
 634     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 635         G.NObj (loc, N.Record (params,name,ty,fields))
 636     | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
 637       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
 638         G.NCopy (loc,s,NUri.uri_of_string u,
 639           List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
 640   ]];
 641
 642   lexicon_command: [ [
 643       IDENT "alias" ; spec = alias_spec ->
 644         L.Alias (loc, spec)
 645     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 646         L.Notation (loc, dir, l1, assoc, prec, l2)
 647     | IDENT "interpretation"; id = QSTRING;
 648       (symbol, args, l3) = interpretation ->
 649         L.Interpretation (loc, id, (symbol, args), l3)
 650   ]];
 651   executable: [
 652     [ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
 653     | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ;
 654       punct = npunctuation_tactical -> cons_ntac tac punct
 655     | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
 656         G.NTactic (loc, [punct])
 657     | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical;
 658         SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
 659           G.NTactic (loc, [tac; punct])
 660     | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical;
 661         punct = npunctuation_tactical ->
 662           G.NTactic (loc, [tac; punct])
 663     ]
 664   ];
 665   comment: [
 666     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 667        G.Code (loc, ex)
 668     | str = NOTE ->
 669        G.Note (loc, str)
 670     ]
 671   ];
 672   statement: [
 673     [ ex = executable ->
 674        fun ?(never_include=false) ~include_paths status ->
 675           let stm = G.Executable (loc, ex) in
 676           !grafite_callback stm;
 677           status, LSome stm
 678     | com = comment ->
 679        fun ?(never_include=false) ~include_paths status ->
 680           let stm = G.Comment (loc, com) in
 681           !grafite_callback stm;
 682           status, LSome stm
 683     | (iloc,fname,normal,mode) = include_command ; SYMBOL "."  ->
 684        fun ?(never_include=false) ~include_paths status ->
 685         let _root, buri, fullpath, _rrelpath =
 686           Librarian.baseuri_of_script ~include_paths fname in
 687         if never_include then raise (NoInclusionPerformed fullpath)
 688         else
 689          begin
 690           let stm =
 691            G.Executable
 692             (loc, G.Command (loc, G.Include (iloc,fname))) in
 693           !grafite_callback stm;
 694           let status =
 695            LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
 696           let stm =
 697            G.Executable
 698             (loc,G.Command (loc,G.Include (iloc,buri)))
 699           in
 700            status, LSome stm
 701          end
 702     | scom = lexicon_command ; SYMBOL "." ->
 703        fun ?(never_include=false) ~include_paths status ->
 704           !lexicon_callback scom;
 705           let status = LE.eval_command status scom in
 706           status, LNone loc
 707     | EOI -> raise End_of_file
 708     ]
 709   ];
 710 END
 711 (* }}} *)
 712 ;;
 713
 714 let _ = initialize_parser () ;;
 715
 716 let exc_located_wrapper f =
 717   try
 718     f ()
 719   with
 720   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 721   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 722       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 723   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 724       raise
 725        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 726   | Stdpp.Exc_located (floc, exn) ->
 727       raise
 728        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 729
 730 let parse_statement lexbuf =
 731   exc_located_wrapper
 732     (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
 733
 734 let statement () = Obj.magic !grafite_parser.statement
 735
 736 let history = ref [] ;;
 737
 738 let push () =
 739   LexiconSync.push ();
 740   history := !grafite_parser :: !history;
 741   grafite_parser := initial_parser ();
 742   initialize_parser ()
 743 ;;
 744
 745 let pop () =
 746   LexiconSync.pop ();
 747   match !history with
 748   | [] -> assert false
 749   | gp :: tail ->
 750       grafite_parser := gp;
 751       history := tail
 752 ;;
 753
 754 (* vim:set foldmethod=marker: *)
 755
 756