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