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