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   inductive_spec: [ [
 456     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
 457     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
 458     fst_constructors = LIST0 constructor SEP SYMBOL "|";
 459     tl = OPT [ "with";
 460       types = LIST1 [
 461         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
 462        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
 463           (name, true, typ, constructors) ] SEP "with" -> types
 464     ] ->
 465       let params =
 466         List.fold_right
 467           (fun (names, typ) acc ->
 468             (List.map (fun name -> (name, typ)) names) @ acc)
 469           params []
 470       in
 471       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
 472       let tl_ind_types = match tl with None -> [] | Some types -> types in
 473       let ind_types = fst_ind_type :: tl_ind_types in
 474       (params, ind_types)
 475   ] ];
 476
 477   record_spec: [ [
 478     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
 479      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
 480      fields = LIST0 [
 481        name = IDENT ;
 482        coercion = [
 483            SYMBOL ":" -> false,0
 484          | SYMBOL ":"; SYMBOL ">" -> true,0
 485          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
 486        ];
 487        ty = term ->
 488          let b,n = coercion in
 489          (name,ty,b,n)
 490      ] SEP SYMBOL ";"; SYMBOL "}" ->
 491       let params =
 492         List.fold_right
 493           (fun (names, typ) acc ->
 494             (List.map (fun name -> (name, typ)) names) @ acc)
 495           params []
 496       in
 497       (params,name,typ,fields)
 498   ] ];
 499
 500   macro: [
 501     [ [ IDENT "check"   ]; t = term ->
 502         GrafiteAst.Check (loc, t)
 503     | [ IDENT "inline"];
 504         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 505         suri = QSTRING; prefix = OPT QSTRING ->
 506          let style = match style with
 507             | None       -> GrafiteAst.Declarative
 508             | Some depth -> GrafiteAst.Procedural depth
 509          in
 510          let prefix = match prefix with None -> "" | Some prefix -> prefix in
 511          GrafiteAst.Inline (loc,style,suri,prefix)
 512     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  ->
 513          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
 514     | IDENT "auto"; params = auto_params ->
 515         GrafiteAst.AutoInteractive (loc,params)
 516     | [ IDENT "whelp"; "match" ] ; t = term ->
 517         GrafiteAst.WMatch (loc,t)
 518     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
 519         GrafiteAst.WInstance (loc,t)
 520     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
 521         GrafiteAst.WLocate (loc,id)
 522     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
 523         GrafiteAst.WElim (loc, t)
 524     | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
 525         GrafiteAst.WHint (loc,t)
 526     ]
 527   ];
 528   alias_spec: [
 529     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
 530       let alpha = "[a-zA-Z]" in
 531       let num = "[0-9]+" in
 532       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
 533       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
 534       let rex = Str.regexp ("^"^ident^"$") in
 535       if Str.string_match rex id 0 then
 536         if (try ignore (UriManager.uri_of_string uri); true
 537             with UriManager.IllFormedUri _ -> false)
 538         then
 539           LexiconAst.Ident_alias (id, uri)
 540         else
 541           raise
 542            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
 543       else
 544         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
 545           Printf.sprintf "Not a valid identifier: %s" id)))
 546     | IDENT "symbol"; symbol = QSTRING;
 547       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
 548       SYMBOL "="; dsc = QSTRING ->
 549         let instance =
 550           match instance with Some i -> i | None -> 0
 551         in
 552         LexiconAst.Symbol_alias (symbol, instance, dsc)
 553     | IDENT "num";
 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.Number_alias (instance, dsc)
 560     ]
 561   ];
 562   argument: [
 563     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
 564       id = IDENT ->
 565         Ast.IdentArg (List.length l, id)
 566     ]
 567   ];
 568   associativity: [
 569     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
 570     | IDENT "right"; IDENT "associative" -> Gramext.RightA
 571     | IDENT "non"; IDENT "associative" -> Gramext.NonA
 572     ]
 573   ];
 574   precedence: [
 575     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
 576   ];
 577   notation: [
 578     [ dir = OPT direction; s = QSTRING;
 579       assoc = OPT associativity; prec = precedence;
 580       IDENT "for";
 581       p2 =
 582         [ blob = UNPARSED_AST ->
 583             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
 584               (CicNotationParser.parse_level2_ast
 585                 (Ulexing.from_utf8_string blob))
 586         | blob = UNPARSED_META ->
 587             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
 588               (CicNotationParser.parse_level2_meta
 589                 (Ulexing.from_utf8_string blob))
 590         ] ->
 591           let assoc =
 592             match assoc with
 593             | None -> default_associativity
 594             | Some assoc -> assoc
 595           in
 596           let p1 =
 597             add_raw_attribute ~text:s
 598               (CicNotationParser.parse_level1_pattern prec
 599                 (Ulexing.from_utf8_string s))
 600           in
 601           (dir, p1, assoc, prec, p2)
 602     ]
 603   ];
 604   level3_term: [
 605     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
 606     | id = IDENT -> Ast.VarPattern id
 607     | SYMBOL "_" -> Ast.ImplicitPattern
 608     | LPAREN; terms = LIST1 SELF; RPAREN ->
 609         (match terms with
 610         | [] -> assert false
 611         | [term] -> term
 612         | terms -> Ast.ApplPattern terms)
 613     ]
 614   ];
 615   interpretation: [
 616     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
 617         (s, args, t)
 618     ]
 619   ];
 620
 621   include_command: [ [
 622       IDENT "include" ; path = QSTRING ->
 623         loc,path,LexiconAst.WithPreferences
 624     | IDENT "include'" ; path = QSTRING ->
 625         loc,path,LexiconAst.WithoutPreferences
 626    ]];
 627
 628   grafite_command: [ [
 629       IDENT "set"; n = QSTRING; v = QSTRING ->
 630         GrafiteAst.Set (loc, n, v)
 631     | IDENT "drop" -> GrafiteAst.Drop loc
 632     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
 633     | IDENT "qed" -> GrafiteAst.Qed loc
 634     | IDENT "variant" ; name = IDENT; SYMBOL ":";
 635       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
 636         GrafiteAst.Obj (loc,
 637           Ast.Theorem
 638             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
 639     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
 640       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
 641         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
 642     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
 643       body = term ->
 644         GrafiteAst.Obj (loc,
 645           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
 646     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
 647         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
 648     | LETCOREC ; defs = CicNotationParser.let_defs ->
 649         mk_rec_corec `CoInductive defs loc
 650     | LETREC ; defs = CicNotationParser.let_defs ->
 651         mk_rec_corec `Inductive defs loc
 652     | IDENT "inductive"; spec = inductive_spec ->
 653         let (params, ind_types) = spec in
 654         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 655     | IDENT "coinductive"; spec = inductive_spec ->
 656         let (params, ind_types) = spec in
 657         let ind_types = (* set inductive flags to false (coinductive) *)
 658           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
 659             ind_types
 660         in
 661         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
 662     | IDENT "coercion" ;
 663       t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
 664       arity = OPT int ; saturations = OPT int;
 665       composites = OPT (IDENT "nocomposites") ->
 666         let arity = match arity with None -> 0 | Some x -> x in
 667         let saturations = match saturations with None -> 0 | Some x -> x in
 668         let composites = match composites with None -> true | Some _ -> false in
 669         GrafiteAst.Coercion
 670          (loc, t, composites, arity, saturations)
 671     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
 672         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
 673     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
 674        let uris = List.map UriManager.uri_of_string uris in
 675         GrafiteAst.Default (loc,what,uris)
 676     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
 677       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
 678                    refl = tactic_term -> refl ] ;
 679       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
 680                    sym = tactic_term -> sym ] ;
 681       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
 682                    trans = tactic_term -> trans ] ;
 683       "as" ; id = IDENT ->
 684        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
 685   ]];
 686   lexicon_command: [ [
 687       IDENT "alias" ; spec = alias_spec ->
 688         LexiconAst.Alias (loc, spec)
 689     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
 690         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
 691     | IDENT "interpretation"; id = QSTRING;
 692       (symbol, args, l3) = interpretation ->
 693         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
 694   ]];
 695   executable: [
 696     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
 697     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
 698         GrafiteAst.Tactic (loc, Some tac, punct)
 699     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
 700     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
 701         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
 702     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
 703     ]
 704   ];
 705   comment: [
 706     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
 707        GrafiteAst.Code (loc, ex)
 708     | str = NOTE ->
 709        GrafiteAst.Note (loc, str)
 710     ]
 711   ];
 712   statement: [
 713     [ ex = executable ->
 714        fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
 715     | com = comment ->
 716        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
 717     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
 718        !out fname;
 719        fun ?(never_include=false) ~include_paths status ->
 720         let _root, buri, fullpath, _rrelpath =
 721           Librarian.baseuri_of_script ~include_paths fname
 722         in
 723         let status =
 724          if never_include then raise (NoInclusionPerformed fullpath)
 725          else LexiconEngine.eval_command status
 726                 (LexiconAst.Include (iloc,buri,mode,fullpath))
 727         in
 728          status,
 729           LSome
 730           (GrafiteAst.Executable
 731            (loc,GrafiteAst.Command
 732             (loc,GrafiteAst.Include (iloc,buri))))
 733     | scom = lexicon_command ; SYMBOL "." ->
 734        fun ?(never_include=false) ~include_paths status ->
 735         let status = LexiconEngine.eval_command status scom in
 736          status,LNone loc
 737     | EOI -> raise End_of_file
 738     ]
 739   ];
 740 END
 741
 742 let exc_located_wrapper f =
 743   try
 744     f ()
 745   with
 746   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
 747   | Stdpp.Exc_located (floc, Stream.Error msg) ->
 748       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
 749   | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
 750       raise
 751        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 752   | Stdpp.Exc_located (floc, exn) ->
 753       raise
 754        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 755
 756 let parse_statement lexbuf =
 757   exc_located_wrapper
 758     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))
 759