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