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 [ IDENT "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 ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 541       let rex = Str.regexp ("^"^ident^"$") in
 542       if Str.string_match rex id 0 then
 543         if (try ignore (UriManager.uri_of_string uri); true
 544             with UriManager.IllFormedUri _ -> false)
 545         then
 546           LexiconAst.Ident_alias (id, uri)
 547         else
 548           raise
 549            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 550       else
 551         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 552           Printf.sprintf "Not a valid identifier: %s" id)))
 553     | IDENT "symbol"; symbol = QSTRING;
 554       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 555       SYMBOL "="; dsc = QSTRING ->
 556         let instance =
 557           match instance with Some i -> i | None -> 0
 558         in
 559         LexiconAst.Symbol_alias (symbol, instance, dsc)
 560     | IDENT "num";
 561       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 562       SYMBOL "="; dsc = QSTRING ->
 563         let instance =
 564           match instance with Some i -> i | None -> 0
 565         in
 566         LexiconAst.Number_alias (instance, dsc)
 567     ]
 568   ];
 569   argument: [
 570     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 571       id = IDENT ->
 572         Ast.IdentArg (List.length l, id)
 573     ]
 574   ];
 575   associativity: [
 576     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 577     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 578     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 579     ]
 580   ];
 581   precedence: [
 582     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 583   ];
 584   notation: [
 585     [ dir = OPT direction; s = QSTRING;
 586       assoc = OPT associativity; prec = precedence;
 587       IDENT "for";
 588       p2 =
 589         [ blob = UNPARSED_AST ->
 590             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 591               (CicNotationParser.parse_level2_ast
 592                 (Ulexing.from_utf8_string blob))
 593         | blob = UNPARSED_META ->
 594             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 595               (CicNotationParser.parse_level2_meta
 596                 (Ulexing.from_utf8_string blob))
 597         ] ->
 598           let assoc =
 599             match assoc with
 600             | None -> default_associativity
 601             | Some assoc -> assoc
 602           in
 603           let p1 =
 604             add_raw_attribute ~text:s
 605               (CicNotationParser.parse_level1_pattern prec
 606                 (Ulexing.from_utf8_string s))
 607           in
 608           (dir, p1, assoc, prec, p2)
 609     ]
 610   ];
 611   level3_term: [
 612     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 613     | id = IDENT -> Ast.VarPattern id
 614     | SYMBOL "_" -> Ast.ImplicitPattern
 615     | LPAREN; terms = LIST1 SELF; RPAREN ->
 616         (match terms with
 617         | [] -> assert false
 618         | [term] -> term
 619         | terms -> Ast.ApplPattern terms)
 620     ]
 621   ];
 622   interpretation: [
 623     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 624         (s, args, t)
 625     ]
 626   ];
 627
 628   include_command: [ [
 629       IDENT "include" ; path = QSTRING ->
 630         loc,path,LexiconAst.WithPreferences
 631     | IDENT "include'" ; path = QSTRING ->
 632         loc,path,LexiconAst.WithoutPreferences
 633    ]];
 634
 635   grafite_command: [ [
 636       IDENT "set"; n = QSTRING; v = QSTRING ->
 637         GrafiteAst.Set (loc, n, v)
 638     | IDENT "drop" -> GrafiteAst.Drop loc
 639     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 640     | IDENT "qed" -> GrafiteAst.Qed loc
 641     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 642       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 643         GrafiteAst.Obj (loc,
 644           Ast.Theorem
 645             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 646     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 647       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 648         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 649     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 650       body = term ->
 651         GrafiteAst.Obj (loc,
 652           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 653     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 654         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 655     | LETCOREC ; defs = CicNotationParser.let_defs ->
 656         mk_rec_corec `CoInductive defs loc
 657     | LETREC ; defs = CicNotationParser.let_defs ->
 658         mk_rec_corec `Inductive defs loc
 659     | IDENT "inductive"; spec = inductive_spec ->
 660         let (params, ind_types) = spec in
 661         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 662     | IDENT "coinductive"; spec = inductive_spec ->
 663         let (params, ind_types) = spec in
 664         let ind_types = (* set inductive flags to false (coinductive) *)
 665           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 666             ind_types
 667         in
 668         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 669     | IDENT "coercion" ;
 670       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 671       arity = OPT int ; saturations = OPT int;
 672       composites = OPT (IDENT "nocomposites") ->
 673         let arity = match arity with None -> 0 | Some x -> x in
 674         let saturations = match saturations with None -> 0 | Some x -> x in
 675         let composites = match composites with None -> true | Some _ -> false in
 676         GrafiteAst.Coercion
 677          (loc, t, composites, arity, saturations)
 678     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 679         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 680     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 681        let uris = List.map UriManager.uri_of_string uris in
 682         GrafiteAst.Default (loc,what,uris)
 683     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 684       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 685                    refl = tactic_term -> refl ] ;
 686       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 687                    sym = tactic_term -> sym ] ;
 688       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 689                    trans = tactic_term -> trans ] ;
 690       "as" ; id = IDENT ->
 691        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 692   ]];
 693   lexicon_command: [ [
 694       IDENT "alias" ; spec = alias_spec ->
 695         LexiconAst.Alias (loc, spec)
 696     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 697         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 698     | IDENT "interpretation"; id = QSTRING;
 699       (symbol, args, l3) = interpretation ->
 700         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 701   ]];
 702   executable: [
 703     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 704     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 705         GrafiteAst.Tactic (loc, Some tac, punct)
 706     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 707     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 708         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 709     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 710     ]
 711   ];
 712   comment: [
 713     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 714        GrafiteAst.Code (loc, ex)
 715     | str = NOTE ->
 716        GrafiteAst.Note (loc, str)
 717     ]
 718   ];
 719   statement: [
 720     [ ex = executable ->
 721        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 722     | com = comment ->
 723        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 724     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 725        !out fname;
 726        fun ?(never_include=false) ~include_paths status ->
 727         let _root, buri, fullpath, _rrelpath =
 728           Librarian.baseuri_of_script ~include_paths fname
 729         in
 730         let status =
 731          if never_include then raise (NoInclusionPerformed fullpath)
 732          else LexiconEngine.eval_command status
 733                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 734         in
 735          status,
 736           LSome
 737           (GrafiteAst.Executable
 738            (loc,GrafiteAst.Command
 739             (loc,GrafiteAst.Include (iloc,buri))))
 740     | scom = lexicon_command ; SYMBOL "." ->
 741        fun ?(never_include=false) ~include_paths status ->
 742         let status = LexiconEngine.eval_command status scom in
 743          status,LNone loc
 744     | EOI -> raise End_of_file
 745     ]
 746   ];
 747 END
 748
 749 let exc_located_wrapper f =
 750   try
 751     f ()
 752   with
 753   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 754   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 755       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 756   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 757       raise
 758        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 759   | Stdpp.Exc_located (floc, exn) ->
 760       raise
 761        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 762
 763 let parse_statement lexbuf =
 764   exc_located_wrapper
 765     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
 766