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