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