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