helm/software/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  = CicNotationPt
  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 =
  40   (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement
  41
  42 type statement =
  43   ?never_include:bool -> include_paths:string list -> LE.status ->
  44     LE.status * ast_statement localized_option
  45
  46 type parser_status = {
  47   grammar : Grammar.g;
  48   term : N.term Grammar.Entry.e;
  49   statement : statement Grammar.Entry.e;
  50 }
  51
  52 let grafite_callback = ref (fun _ _ -> ())
  53 let set_grafite_callback cb = grafite_callback := cb
  54
  55 let lexicon_callback = ref (fun _ _ -> ())
  56 let set_lexicon_callback cb = lexicon_callback := cb
  57
  58 let initial_parser () =
  59   let grammar = CicNotationParser.level2_ast_grammar () in
  60   let term = CicNotationParser.term () in
  61   let statement = Grammar.Entry.create grammar "statement" in
  62   { grammar = grammar; term = term; statement = statement }
  63 ;;
  64
  65 let grafite_parser = ref (initial_parser ())
  66
  67 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
  68
  69 let default_associativity = Gramext.NonA
  70
  71 let mk_rec_corec ng ind_kind defs loc =
  72  (* In case of mutual definitions here we produce just
  73     the syntax tree for the first one. The others will be
  74     generated from the completely specified term just before
  75     insertion in the environment. We use the flavour
  76     `MutualDefinition to rememer this. *)
  77   let name,ty =
  78     match defs with
  79     | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
  80         let ty =
  81          List.fold_right
  82           (fun var ty -> N.Binder (`Pi,var,ty)
  83           ) params ty
  84         in
  85          name,ty
  86     | (_,(N.Ident (name, None), None),_,_) :: _ ->
  87         name, N.Implicit
  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    if ng then
  98     G.NObj (loc, N.Theorem(flavour, name, ty,
  99      Some (N.LetRec (ind_kind, defs, body))))
 100    else
 101     G.Obj (loc, N.Theorem(flavour, name, ty,
 102      Some (N.LetRec (ind_kind, defs, body))))
 103
 104 type by_continuation =
 105    BYC_done
 106  | BYC_weproved of N.term * string option * N.term option
 107  | BYC_letsuchthat of string * N.term * string * N.term
 108  | BYC_wehaveand of string * N.term * string * N.term
 109
 110 let initialize_parser () =
 111   (* {{{ parser initialization *)
 112   let term = !grafite_parser.term in
 113   let statement = !grafite_parser.statement in
 114   let let_defs = CicNotationParser.let_defs () in
 115   let protected_binder_vars = CicNotationParser.protected_binder_vars () in
 116 EXTEND
 117   GLOBAL: term statement;
 118   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
 119   tactic_term: [ [ t = term LEVEL "90" -> t ] ];
 120   new_name: [
 121     [ id = IDENT -> Some id
 122     | SYMBOL "_" -> None ]
 123     ];
 124   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
 125   tactic_term_list1: [
 126     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
 127   ];
 128   reduction_kind: [
 129     [ IDENT "normalize" -> `Normalize
 130     | IDENT "simplify" -> `Simpl
 131     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
 132     | IDENT "whd" -> `Whd ]
 133   ];
 134   sequent_pattern_spec: [
 135    [ hyp_paths =
 136       LIST0
 137        [ id = IDENT ;
 138          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
 139          (id,match path with Some p -> p | None -> N.UserInput) ];
 140      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
 141       let goal_path =
 142        match goal_path, hyp_paths with
 143           None, [] -> Some N.UserInput
 144         | None, _::_ -> None
 145         | Some goal_path, _ -> Some goal_path
 146       in
 147        hyp_paths,goal_path
 148    ]
 149   ];
 150   pattern_spec: [
 151     [ res = OPT [
 152        "in";
 153        wanted_and_sps =
 154         [ "match" ; wanted = tactic_term ;
 155           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
 156            Some wanted,sps
 157         | sps = sequent_pattern_spec ->
 158            None,Some sps
 159         ] ->
 160          let wanted,hyp_paths,goal_path =
 161           match wanted_and_sps with
 162              wanted,None -> wanted, [], Some N.UserInput
 163            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
 164          in
 165           wanted, hyp_paths, goal_path ] ->
 166       match res with
 167          None -> None,[],Some N.UserInput
 168        | Some ps -> ps]
 169   ];
 170   inverter_param_list: [
 171     [ params = tactic_term ->
 172       let deannotate = function
 173         | N.AttributedTerm (_,t) | t -> t
 174       in match deannotate params with
 175       | N.Implicit -> [false]
 176       | N.UserInput -> [true]
 177       | N.Appl l ->
 178          List.map (fun x -> match deannotate x with
 179            | N.Implicit -> false
 180            | N.UserInput -> true
 181            | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
 182       | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
 183   ];
 184   direction: [
 185     [ SYMBOL ">" -> `LeftToRight
 186     | SYMBOL "<" -> `RightToLeft ]
 187   ];
 188   int: [ [ num = NUMBER -> int_of_string num ] ];
 189   intros_names: [
 190    [ idents = OPT ident_list0 ->
 191       match idents with None -> [] | Some idents -> idents
 192    ]
 193   ];
 194   intros_spec: [
 195     [ OPT [ IDENT "names" ];
 196       num = OPT [ num = int -> num ];
 197       idents = intros_names ->
 198         num, idents
 199     ]
 200   ];
 201   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
 202   ntactic: [
 203     [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
 204     | IDENT "nassert";
 205        seqs = LIST0 [
 206         hyps = LIST0
 207          [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
 208          | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
 209                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
 210             id,`Def (bo,ty)];
 211         SYMBOL <:unicode<vdash>>;
 212         concl = tactic_term -> (List.rev hyps,concl) ] ->
 213          G.NAssert (loc, seqs)
 214     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
 215         G.NCases (loc, what, where)
 216     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
 217         G.NChange (loc, what, with_what)
 218     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
 219         G.NElim (loc, what, where)
 220     | IDENT "ngeneralize"; p=pattern_spec ->
 221         G.NGeneralize (loc, p)
 222     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
 223         where = pattern_spec ->
 224         G.NLetIn (loc,where,t,name)
 225     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
 226         G.NRewrite (loc, dir, what, where)
 227     | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
 228       where = pattern_spec ->
 229         let delta = match delta with None -> true | _ -> false in
 230         G.NEval (loc, where, `Whd delta)
 231     | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
 232     | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
 233     | SYMBOL "*" -> G.NCase1 (loc,"_")
 234     | SYMBOL "*"; n=IDENT ->
 235         G.NCase1 (loc,n)
 236     ]
 237   ];
 238   tactic: [
 239     [ IDENT "absurd"; t = tactic_term ->
 240         G.Absurd (loc, t)
 241     | IDENT "apply"; IDENT "rule"; t = tactic_term ->
 242         G.ApplyRule (loc, t)
 243     | IDENT "apply"; t = tactic_term ->
 244         G.Apply (loc, t)
 245     | IDENT "applyP"; t = tactic_term ->
 246         G.ApplyP (loc, t)
 247     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
 248         G.ApplyS (loc, t, params)
 249     | IDENT "assumption" ->
 250         G.Assumption loc
 251     | IDENT "autobatch";  params = auto_params ->
 252         G.AutoBatch (loc,params)
 253     | IDENT "cases"; what = tactic_term;
 254       pattern = OPT pattern_spec;
 255       specs = intros_spec ->
 256         let pattern = match pattern with
 257            | None         -> None, [], Some N.UserInput
 258            | Some pattern -> pattern
 259         in
 260         G.Cases (loc, what, pattern, specs)
 261     | IDENT "clear"; ids = LIST1 IDENT ->
 262         G.Clear (loc, ids)
 263     | IDENT "clearbody"; id = IDENT ->
 264         G.ClearBody (loc,id)
 265     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
 266         G.Change (loc, what, t)
 267     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
 268       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
 269         let times = match times with None -> 1 | Some i -> i in
 270         G.Compose (loc, t1, t2, times, specs)
 271     | IDENT "constructor"; n = int ->
 272         G.Constructor (loc, n)
 273     | IDENT "contradiction" ->
 274         G.Contradiction loc
 275     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
 276         G.Cut (loc, ident, t)
 277     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 278         let idents = match idents with None -> [] | Some idents -> idents in
 279         G.Decompose (loc, idents)
 280     | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
 281     | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
 282         G.Destruct (loc, xts)
 283     | IDENT "elim"; what = tactic_term; using = using;
 284        pattern = OPT pattern_spec;
 285        ispecs = intros_spec ->
 286         let pattern = match pattern with
 287            | None         -> None, [], Some N.UserInput
 288            | Some pattern -> pattern
 289           in
 290           G.Elim (loc, what, using, pattern, ispecs)
 291     | IDENT "elimType"; what = tactic_term; using = using;
 292       (num, idents) = intros_spec ->
 293         G.ElimType (loc, what, using, (num, idents))
 294     | IDENT "exact"; t = tactic_term ->
 295         G.Exact (loc, t)
 296     | IDENT "exists" ->
 297         G.Exists loc
 298     | IDENT "fail" -> G.Fail loc
 299     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
 300         let (pt,_,_) = p in
 301           if pt <> None then
 302             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
 303               ("the pattern cannot specify the term to replace, only its"
 304               ^ " paths in the hypotheses and in the conclusion")))
 305        else
 306          G.Fold (loc, kind, t, p)
 307     | IDENT "fourier" ->
 308         G.Fourier loc
 309     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
 310         let idents = match idents with None -> [] | Some idents -> idents in
 311         G.FwdSimpl (loc, hyp, idents)
 312     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
 313        G.Generalize (loc,p,id)
 314     | IDENT "id" -> G.IdTac loc
 315     | IDENT "intro"; ident = OPT IDENT ->
 316         let idents = match ident with None -> [] | Some id -> [Some id] in
 317         G.Intros (loc, (Some 1, idents))
 318     | IDENT "intros"; specs = intros_spec ->
 319         G.Intros (loc, specs)
 320     | IDENT "inversion"; t = tactic_term ->
 321         G.Inversion (loc, t)
 322     | IDENT "lapply";
 323       linear = OPT [ IDENT "linear" ];
 324       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
 325       what = tactic_term;
 326       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
 327       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
 328         let linear = match linear with None -> false | Some _ -> true in
 329         let to_what = match to_what with None -> [] | Some to_what -> to_what in
 330         G.LApply (loc, linear, depth, to_what, what, ident)
 331     | IDENT "left" -> G.Left loc
 332     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
 333         G.LetIn (loc, t, where)
 334     | kind = reduction_kind; p = pattern_spec ->
 335         G.Reduce (loc, kind, p)
 336     | IDENT "reflexivity" ->
 337         G.Reflexivity loc
 338     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
 339         G.Replace (loc, p, t)
 340     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
 341        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
 342        let (pt,_,_) = p in
 343         if pt <> None then
 344          raise
 345           (HExtlib.Localized (loc,
 346            (CicNotationParser.Parse_error
 347             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
 348         else
 349          let n = match xnames with None -> [] | Some names -> names in
 350          G.Rewrite (loc, d, t, p, n)
 351     | IDENT "right" ->
 352         G.Right loc
 353     | IDENT "ring" ->
 354         G.Ring loc
 355     | IDENT "split" ->
 356         G.Split loc
 357     | IDENT "symmetry" ->
 358         G.Symmetry loc
 359     | IDENT "transitivity"; t = tactic_term ->
 360         G.Transitivity (loc, t)
 361      (* Produzioni Aggiunte *)
 362     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
 363         G.Assume (loc, id, t)
 364     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
 365       t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
 366                 t' = tactic_term -> t']->
 367         G.Suppose (loc, t, id, t1)
 368     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 369       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 370       id2 = IDENT ; RPAREN ->
 371         G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
 372     | just =
 373        [ IDENT "using"; t=tactic_term -> `Term t
 374        | params = auto_params -> `Auto params] ;
 375       cont=by_continuation ->
 376        (match cont with
 377            BYC_done -> G.Bydone (loc, just)
 378          | BYC_weproved (ty,id,t1) ->
 379             G.By_just_we_proved(loc, just, ty, id, t1)
 380          | BYC_letsuchthat (id1,t1,id2,t2) ->
 381             G.ExistsElim (loc, just, id1, t1, id2, t2)
 382          | BYC_wehaveand (id1,t1,id2,t2) ->
 383             G.AndElim (loc, just, id1, t1, id2, t2))
 384     | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
 385         G.We_need_to_prove (loc, t, id, t1)
 386     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 387         G.We_proceed_by_cases_on (loc, t, t1)
 388     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
 389         G.We_proceed_by_induction_on (loc, t, t1)
 390     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
 391         G.Byinduction(loc, t, id)
 392     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
 393         G.Thesisbecomes(loc, t)
 394     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
 395         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
 396          G.Case(loc,id,params)
 397       (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
 398     | IDENT "conclude";
 399       termine = tactic_term;
 400       SYMBOL "=" ;
 401       t1=tactic_term ;
 402       t2 =
 403        [ IDENT "using"; t=tactic_term -> `Term t
 404        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 405        | IDENT "proof" -> `Proof
 406        | params = auto_params -> `Auto params];
 407       cont = rewriting_step_continuation ->
 408        G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
 409     | IDENT "obtain" ; name = IDENT;
 410       termine = tactic_term;
 411       SYMBOL "=" ;
 412       t1=tactic_term ;
 413       t2 =
 414        [ IDENT "using"; t=tactic_term -> `Term t
 415        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 416        | IDENT "proof" -> `Proof
 417        | params = auto_params -> `Auto params];
 418       cont = rewriting_step_continuation ->
 419        G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
 420     | SYMBOL "=" ;
 421       t1=tactic_term ;
 422       t2 =
 423        [ IDENT "using"; t=tactic_term -> `Term t
 424        | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
 425        | IDENT "proof" -> `Proof
 426        | params = auto_params -> `Auto params];
 427       cont = rewriting_step_continuation ->
 428        G.RewritingStep(loc, None, t1, t2, cont)
 429   ]
 430 ];
 431   auto_fixed_param: [
 432    [ IDENT "paramodulation"
 433    | IDENT "depth"
 434    | IDENT "width"
 435    | IDENT "size"
 436    | IDENT "timeout"
 437    | IDENT "library"
 438    | IDENT "type"
 439    | IDENT "all"
 440    ]
 441 ];
 442   auto_params: [
 443    [ params =
 444       LIST0 [
 445          i = auto_fixed_param -> i,""
 446        | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
 447               string_of_int v | v = IDENT -> v ] -> i,v ];
 448       tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
 449       (match tl with Some l -> l | None -> []),
 450       params
 451    ]
 452 ];
 453   inline_params:[
 454    [ params = LIST0
 455       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
 456       | flavour = inline_flavour -> G.IPAs flavour
 457       | IDENT "procedural" -> G.IPProcedural
 458       | IDENT "nodefaults" -> G.IPNoDefaults
 459       | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
 460       | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
 461       ] -> params
 462    ]
 463 ];
 464   by_continuation: [
 465     [ 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)
 466     | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
 467             "done" -> BYC_weproved (ty,None,t1)
 468     | "done" -> BYC_done
 469     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
 470       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
 471       id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
 472     | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
 473               BYC_wehaveand (id1,t1,id2,t2)
 474     ]
 475 ];
 476   rewriting_step_continuation : [
 477     [ "done" -> true
 478     | -> false
 479     ]
 480 ];
 481   atomic_tactical:
 482     [ "sequence" LEFTA
 483       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
 484           let ts =
 485             match t1 with
 486             | G.Seq (_, l) -> l @ [ t2 ]
 487             | _ -> [ t1; t2 ]
 488           in
 489           G.Seq (loc, ts)
 490       ]
 491     | "then" NONA
 492       [ tac = SELF; SYMBOL ";";
 493         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 494           (G.Then (loc, tac, tacs))
 495       ]
 496     | "loops" RIGHTA
 497       [ IDENT "do"; count = int; tac = SELF ->
 498           G.Do (loc, count, tac)
 499       | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
 500       ]
 501     | "simple" NONA
 502       [ IDENT "first";
 503         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 504           G.First (loc, tacs)
 505       | IDENT "try"; tac = SELF -> G.Try (loc, tac)
 506       | IDENT "solve";
 507         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
 508           G.Solve (loc, tacs)
 509       | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
 510       | LPAREN; tac = SELF; RPAREN -> tac
 511       | tac = tactic -> tac
 512         ]
 513       ];
 514   punctuation_tactical:
 515     [
 516       [ SYMBOL "[" -> G.Branch loc
 517       | SYMBOL "|" -> G.Shift loc
 518       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
 519       | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
 520       | SYMBOL "]" -> G.Merge loc
 521       | SYMBOL ";" -> G.Semicolon loc
 522       | SYMBOL "." -> G.Dot loc
 523       ]
 524     ];
 525   non_punctuation_tactical:
 526     [ "simple" NONA
 527       [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
 528       | IDENT "unfocus" -> G.Unfocus loc
 529       | IDENT "skip" -> G.Skip loc
 530       ]
 531       ];
 532   ntheorem_flavour: [
 533     [ [ IDENT "ndefinition"  ] -> `Definition
 534     | [ IDENT "nfact"        ] -> `Fact
 535     | [ IDENT "nlemma"       ] -> `Lemma
 536     | [ IDENT "nremark"      ] -> `Remark
 537     | [ IDENT "ntheorem"     ] -> `Theorem
 538     ]
 539   ];
 540   theorem_flavour: [
 541     [ [ IDENT "definition"  ] -> `Definition
 542     | [ IDENT "fact"        ] -> `Fact
 543     | [ IDENT "lemma"       ] -> `Lemma
 544     | [ IDENT "remark"      ] -> `Remark
 545     | [ IDENT "theorem"     ] -> `Theorem
 546     ]
 547   ];
 548   inline_flavour: [
 549      [ attr = theorem_flavour -> attr
 550      | [ IDENT "axiom"     ]  -> `Axiom
 551      | [ IDENT "variant"   ]  -> `Variant
 552      ]
 553   ];
 554   inductive_spec: [ [
 555     fst_name = IDENT;
 556       params = LIST0 protected_binder_vars;
 557     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 558     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 559     tl = OPT [ "with";
 560         types = LIST1 [
 561           name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 562          OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 563             (name, true, typ, constructors) ] SEP "with" -> types
 564       ] ->
 565         let params =
 566           List.fold_right
 567             (fun (names, typ) acc ->
 568               (List.map (fun name -> (name, typ)) names) @ acc)
 569             params []
 570         in
 571         let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 572         let tl_ind_types = match tl with None -> [] | Some types -> types in
 573         let ind_types = fst_ind_type :: tl_ind_types in
 574         (params, ind_types)
 575     ] ];
 576
 577     record_spec: [ [
 578       name = IDENT;
 579       params = LIST0 protected_binder_vars;
 580        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 581        fields = LIST0 [
 582          name = IDENT ;
 583          coercion = [
 584              SYMBOL ":" -> false,0
 585            | SYMBOL ":"; SYMBOL ">" -> true,0
 586            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 587          ];
 588          ty = term ->
 589            let b,n = coercion in
 590            (name,ty,b,n)
 591        ] SEP SYMBOL ";"; SYMBOL "}" ->
 592         let params =
 593           List.fold_right
 594             (fun (names, typ) acc ->
 595               (List.map (fun name -> (name, typ)) names) @ acc)
 596             params []
 597         in
 598         (params,name,typ,fields)
 599     ] ];
 600
 601     macro: [
 602       [ [ IDENT "check"   ]; t = term ->
 603           G.Check (loc, t)
 604       | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
 605           G.Eval (loc, kind, t)
 606       | IDENT "inline"; suri = QSTRING; params = inline_params ->
 607            G.Inline (loc, suri, params)
 608       | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 609            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
 610       | IDENT "auto"; params = auto_params ->
 611           G.AutoInteractive (loc,params)
 612       | [ IDENT "whelp"; "match" ] ; t = term ->
 613           G.WMatch (loc,t)
 614       | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 615           G.WInstance (loc,t)
 616       | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 617           G.WLocate (loc,id)
 618       | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 619           G.WElim (loc, t)
 620       | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 621           G.WHint (loc,t)
 622       ]
 623     ];
 624     alias_spec: [
 625       [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 626         let alpha = "[a-zA-Z]" in
 627         let num = "[0-9]+" in
 628         let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 629         let decoration = "\\'" in
 630         let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
 631         let rex = Str.regexp ("^"^ident^"$") in
 632         if Str.string_match rex id 0 then
 633           if (try ignore (UriManager.uri_of_string uri); true
 634               with UriManager.IllFormedUri _ -> false) ||
 635              (try ignore (NReference.reference_of_string uri); true
 636               with NReference.IllFormedReference _ -> false)
 637           then
 638             L.Ident_alias (id, uri)
 639           else
 640             raise
 641              (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 642         else
 643           raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 644             Printf.sprintf "Not a valid identifier: %s" id)))
 645       | IDENT "symbol"; symbol = QSTRING;
 646         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 647         SYMBOL "="; dsc = QSTRING ->
 648           let instance =
 649             match instance with Some i -> i | None -> 0
 650           in
 651           L.Symbol_alias (symbol, instance, dsc)
 652       | IDENT "num";
 653         instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 654         SYMBOL "="; dsc = QSTRING ->
 655           let instance =
 656             match instance with Some i -> i | None -> 0
 657           in
 658           L.Number_alias (instance, dsc)
 659       ]
 660     ];
 661     argument: [
 662       [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 663         id = IDENT ->
 664           N.IdentArg (List.length l, id)
 665       ]
 666     ];
 667     associativity: [
 668       [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 669       | IDENT "right"; IDENT "associative" -> Gramext.RightA
 670       | IDENT "non"; IDENT "associative" -> Gramext.NonA
 671       ]
 672     ];
 673     precedence: [
 674       [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 675     ];
 676     notation: [
 677       [ dir = OPT direction; s = QSTRING;
 678         assoc = OPT associativity; prec = precedence;
 679         IDENT "for";
 680         p2 =
 681           [ blob = UNPARSED_AST ->
 682               add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 683                 (CicNotationParser.parse_level2_ast
 684                   (Ulexing.from_utf8_string blob))
 685           | blob = UNPARSED_META ->
 686               add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 687                 (CicNotationParser.parse_level2_meta
 688                   (Ulexing.from_utf8_string blob))
 689           ] ->
 690             let assoc =
 691               match assoc with
 692               | None -> default_associativity
 693               | Some assoc -> assoc
 694             in
 695             let p1 =
 696               add_raw_attribute ~text:s
 697                 (CicNotationParser.parse_level1_pattern prec
 698                   (Ulexing.from_utf8_string s))
 699             in
 700             (dir, p1, assoc, prec, p2)
 701       ]
 702     ];
 703     level3_term: [
 704       [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
 705       | id = IDENT -> N.VarPattern id
 706       | SYMBOL "_" -> N.ImplicitPattern
 707       | LPAREN; terms = LIST1 SELF; RPAREN ->
 708           (match terms with
 709           | [] -> assert false
 710           | [term] -> term
 711           | terms -> N.ApplPattern terms)
 712       ]
 713     ];
 714     interpretation: [
 715       [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 716           (s, args, t)
 717       ]
 718     ];
 719
 720     include_command: [ [
 721         IDENT "include" ; path = QSTRING ->
 722           loc,path,L.WithPreferences
 723       | IDENT "include'" ; path = QSTRING ->
 724           loc,path,L.WithoutPreferences
 725      ]];
 726
 727   grafite_command: [ [
 728       IDENT "set"; n = QSTRING; v = QSTRING ->
 729         G.Set (loc, n, v)
 730     | IDENT "drop" -> G.Drop loc
 731     | IDENT "print"; s = IDENT -> G.Print (loc,s)
 732     | IDENT "qed" -> G.Qed loc
 733     | IDENT "nqed" -> G.NQed loc
 734     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 735       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 736         G.Obj (loc,
 737           N.Theorem
 738             (`Variant,name,typ,Some (N.Ident (newname, None))))
 739     | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 740       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 741         G.NObj (loc, N.Theorem (nflavour, name, typ, body))
 742     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 743       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 744         G.Obj (loc, N.Theorem (flavour, name, typ, body))
 745     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 746       body = term ->
 747         G.Obj (loc,
 748           N.Theorem (flavour, name, N.Implicit, Some body))
 749     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 750         G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
 751     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
 752         G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
 753     | LETCOREC ; defs = let_defs ->
 754         mk_rec_corec false `CoInductive defs loc
 755     | LETREC ; defs = let_defs ->
 756         mk_rec_corec false `Inductive defs loc
 757     | NLETCOREC ; defs = let_defs ->
 758         mk_rec_corec true `CoInductive defs loc
 759     | NLETREC ; defs = let_defs ->
 760         mk_rec_corec true `Inductive defs loc
 761     | IDENT "inductive"; spec = inductive_spec ->
 762         let (params, ind_types) = spec in
 763         G.Obj (loc, N.Inductive (params, ind_types))
 764     | IDENT "ninductive"; spec = inductive_spec ->
 765         let (params, ind_types) = spec in
 766         G.NObj (loc, N.Inductive (params, ind_types))
 767     | IDENT "coinductive"; spec = inductive_spec ->
 768         let (params, ind_types) = spec in
 769         let ind_types = (* set inductive flags to false (coinductive) *)
 770           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 771             ind_types
 772         in
 773         G.Obj (loc, N.Inductive (params, ind_types))
 774     | IDENT "ncoinductive"; spec = inductive_spec ->
 775         let (params, ind_types) = spec in
 776         let ind_types = (* set inductive flags to false (coinductive) *)
 777           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 778             ind_types
 779         in
 780         G.NObj (loc, N.Inductive (params, ind_types))
 781     | IDENT "coercion" ;
 782       t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 783       arity = OPT int ; saturations = OPT int;
 784       composites = OPT (IDENT "nocomposites") ->
 785         let arity = match arity with None -> 0 | Some x -> x in
 786         let saturations = match saturations with None -> 0 | Some x -> x in
 787         let composites = match composites with None -> true | Some _ -> false in
 788         G.Coercion
 789          (loc, t, composites, arity, saturations)
 790     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
 791         G.PreferCoercion (loc, t)
 792     | IDENT "pump" ; steps = int ->
 793         G.Pump(loc,steps)
 794     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
 795         G.UnificationHint (loc, t, n)
 796     | IDENT "inverter"; name = IDENT; IDENT "for";
 797         indty = tactic_term; paramspec = inverter_param_list ->
 798           G.Inverter
 799             (loc, name, indty, paramspec)
 800     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 801         G.Obj (loc, N.Record (params,name,ty,fields))
 802     | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
 803         G.NObj (loc, N.Record (params,name,ty,fields))
 804     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 805        let uris = List.map UriManager.uri_of_string uris in
 806         G.Default (loc,what,uris)
 807     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 808       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 809                    refl = tactic_term -> refl ] ;
 810       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 811                    sym = tactic_term -> sym ] ;
 812       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 813                    trans = tactic_term -> trans ] ;
 814       "as" ; id = IDENT ->
 815        G.Relation (loc,id,a,aeq,refl,sym,trans)
 816   ]];
 817   lexicon_command: [ [
 818       IDENT "alias" ; spec = alias_spec ->
 819         L.Alias (loc, spec)
 820     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 821         L.Notation (loc, dir, l1, assoc, prec, l2)
 822     | IDENT "interpretation"; id = QSTRING;
 823       (symbol, args, l3) = interpretation ->
 824         L.Interpretation (loc, id, (symbol, args), l3)
 825   ]];
 826   executable: [
 827     [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
 828     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 829         G.Tactic (loc, Some tac, punct)
 830     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
 831     | tac = ntactic; punct = punctuation_tactical ->
 832         G.NTactic (loc, tac, punct)
 833     | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
 834         G.NTactic (loc, G.NId loc, punct)
 835     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 836         G.NonPunctuationTactical (loc, tac, punct)
 837     | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
 838         G.NNonPunctuationTactical (loc, tac, punct)
 839     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
 840     ]
 841   ];
 842   comment: [
 843     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 844        G.Code (loc, ex)
 845     | str = NOTE ->
 846        G.Note (loc, str)
 847     ]
 848   ];
 849   statement: [
 850     [ ex = executable ->
 851        fun ?(never_include=false) ~include_paths status ->
 852           let stm = G.Executable (loc, ex) in
 853           !grafite_callback status stm;
 854           status, LSome stm
 855     | com = comment ->
 856        fun ?(never_include=false) ~include_paths status ->
 857           let stm = G.Comment (loc, com) in
 858           !grafite_callback status stm;
 859           status, LSome stm
 860     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 861        fun ?(never_include=false) ~include_paths status ->
 862           let stm =
 863              G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
 864           in
 865           !grafite_callback status stm;
 866           let _root, buri, fullpath, _rrelpath =
 867             Librarian.baseuri_of_script ~include_paths fname
 868           in
 869           let stm =
 870              G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
 871           in
 872           let status =
 873             if never_include then raise (NoInclusionPerformed fullpath)
 874             else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
 875           in
 876           status, LSome stm
 877     | scom = lexicon_command ; SYMBOL "." ->
 878        fun ?(never_include=false) ~include_paths status ->
 879           !lexicon_callback status scom;
 880           let status = LE.eval_command status scom in
 881           status, LNone loc
 882     | EOI -> raise End_of_file
 883     ]
 884   ];
 885 END
 886 (* }}} *)
 887 ;;
 888
 889 let _ = initialize_parser () ;;
 890
 891 let exc_located_wrapper f =
 892   try
 893     f ()
 894   with
 895   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 896   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 897       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 898   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 899       raise
 900        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 901   | Stdpp.Exc_located (floc, exn) ->
 902       raise
 903        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 904
 905 let parse_statement lexbuf =
 906   exc_located_wrapper
 907     (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
 908
 909 let statement () = !grafite_parser.statement
 910
 911 let history = ref [] ;;
 912
 913 let push () =
 914   LexiconSync.push ();
 915   history := !grafite_parser :: !history;
 916   grafite_parser := initial_parser ();
 917   initialize_parser ()
 918 ;;
 919
 920 let pop () =
 921   LexiconSync.pop ();
 922   match !history with
 923   | [] -> assert false
 924   | gp :: tail ->
 925       grafite_parser := gp;
 926       history := tail
 927 ;;
 928
 929 (* vim:set foldmethod=marker: *)
 930
 931