helm/software/components/grafite_parser/grafiteParser.ml

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