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