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