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