1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module N = CicNotationPt
31 module LE = LexiconEngine
33 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
40 (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement
43 ?never_include:bool -> include_paths:string list -> LE.status ->
44 LE.status * ast_statement localized_option
46 type parser_status = {
48 term : N.term Grammar.Entry.e;
49 statement : statement Grammar.Entry.e;
52 let grafite_callback = ref (fun _ _ -> ())
53 let set_grafite_callback cb = grafite_callback := cb
55 let lexicon_callback = ref (fun _ _ -> ())
56 let set_lexicon_callback cb = lexicon_callback := cb
58 let initial_parser () =
59 let grammar = CicNotationParser.level2_ast_grammar () in
60 let term = CicNotationParser.term () in
61 let statement = Grammar.Entry.create grammar "statement" in
62 { grammar = grammar; term = term; statement = statement }
65 let grafite_parser = ref (initial_parser ())
67 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
69 let default_associativity = Gramext.NonA
71 let mk_rec_corec ng ind_kind defs loc =
72 (* In case of mutual definitions here we produce just
73 the syntax tree for the first one. The others will be
74 generated from the completely specified term just before
75 insertion in the environment. We use the flavour
76 `MutualDefinition to rememer this. *)
79 | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
82 (fun var ty -> N.Binder (`Pi,var,ty)
86 | (_,(N.Ident (name, None), None),_,_) :: _ ->
90 let body = N.Ident (name,None) in
92 if List.length defs = 1 then
98 G.NObj (loc, N.Theorem(flavour, name, ty,
99 Some (N.LetRec (ind_kind, defs, body))))
101 G.Obj (loc, N.Theorem(flavour, name, ty,
102 Some (N.LetRec (ind_kind, defs, body))))
104 type by_continuation =
106 | BYC_weproved of N.term * string option * N.term option
107 | BYC_letsuchthat of string * N.term * string * N.term
108 | BYC_wehaveand of string * N.term * string * N.term
110 let initialize_parser () =
111 (* {{{ parser initialization *)
112 let term = !grafite_parser.term in
113 let statement = !grafite_parser.statement in
114 let let_defs = CicNotationParser.let_defs () in
115 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
117 GLOBAL: term statement;
118 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
119 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
121 [ id = IDENT -> Some id
122 | SYMBOL "_" -> None ]
124 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
126 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
129 [ IDENT "normalize" -> `Normalize
130 | IDENT "simplify" -> `Simpl
131 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
132 | IDENT "whd" -> `Whd ]
134 sequent_pattern_spec: [
138 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
139 (id,match path with Some p -> p | None -> N.UserInput) ];
140 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
142 match goal_path, hyp_paths with
143 None, [] -> Some N.UserInput
145 | Some goal_path, _ -> Some goal_path
154 [ "match" ; wanted = tactic_term ;
155 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
157 | sps = sequent_pattern_spec ->
160 let wanted,hyp_paths,goal_path =
161 match wanted_and_sps with
162 wanted,None -> wanted, [], Some N.UserInput
163 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
165 wanted, hyp_paths, goal_path ] ->
167 None -> None,[],Some N.UserInput
170 inverter_param_list: [
171 [ params = tactic_term ->
172 let deannotate = function
173 | N.AttributedTerm (_,t) | t -> t
174 in match deannotate params with
175 | N.Implicit -> [false]
176 | N.UserInput -> [true]
178 List.map (fun x -> match deannotate x with
179 | N.Implicit -> false
180 | N.UserInput -> true
181 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
182 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
185 [ SYMBOL ">" -> `LeftToRight
186 | SYMBOL "<" -> `RightToLeft ]
188 int: [ [ num = NUMBER -> int_of_string num ] ];
190 [ idents = OPT ident_list0 ->
191 match idents with None -> [] | Some idents -> idents
195 [ OPT [ IDENT "names" ];
196 num = OPT [ num = int -> num ];
197 idents = intros_names ->
201 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
203 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
207 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
208 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
209 SYMBOL <:unicode<def>> ; bo = tactic_term ->
211 SYMBOL <:unicode<vdash>>;
212 concl = tactic_term -> (List.rev hyps,concl) ] ->
213 G.NAssert (loc, seqs)
214 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
215 G.NCases (loc, what, where)
216 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
217 G.NChange (loc, what, with_what)
218 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
219 G.NElim (loc, what, where)
220 | IDENT "ngeneralize"; p=pattern_spec ->
221 G.NGeneralize (loc, p)
222 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
223 where = pattern_spec ->
224 G.NLetIn (loc,where,t,name)
225 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
226 G.NRewrite (loc, dir, what, where)
227 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
228 where = pattern_spec ->
229 let delta = match delta with None -> true | _ -> false in
230 G.NEval (loc, where, `Whd delta)
231 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
232 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
233 | SYMBOL "*" -> G.NCase1 (loc,"_")
234 | SYMBOL "*"; n=IDENT ->
239 [ IDENT "absurd"; t = tactic_term ->
241 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
243 | IDENT "apply"; t = tactic_term ->
245 | IDENT "applyP"; t = tactic_term ->
247 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
248 G.ApplyS (loc, t, params)
249 | IDENT "assumption" ->
251 | IDENT "autobatch"; params = auto_params ->
252 G.AutoBatch (loc,params)
253 | IDENT "cases"; what = tactic_term;
254 pattern = OPT pattern_spec;
255 specs = intros_spec ->
256 let pattern = match pattern with
257 | None -> None, [], Some N.UserInput
258 | Some pattern -> pattern
260 G.Cases (loc, what, pattern, specs)
261 | IDENT "clear"; ids = LIST1 IDENT ->
263 | IDENT "clearbody"; id = IDENT ->
265 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
266 G.Change (loc, what, t)
267 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
268 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
269 let times = match times with None -> 1 | Some i -> i in
270 G.Compose (loc, t1, t2, times, specs)
271 | IDENT "constructor"; n = int ->
272 G.Constructor (loc, n)
273 | IDENT "contradiction" ->
275 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
276 G.Cut (loc, ident, t)
277 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
278 let idents = match idents with None -> [] | Some idents -> idents in
279 G.Decompose (loc, idents)
280 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
281 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
282 G.Destruct (loc, xts)
283 | IDENT "elim"; what = tactic_term; using = using;
284 pattern = OPT pattern_spec;
285 ispecs = intros_spec ->
286 let pattern = match pattern with
287 | None -> None, [], Some N.UserInput
288 | Some pattern -> pattern
290 G.Elim (loc, what, using, pattern, ispecs)
291 | IDENT "elimType"; what = tactic_term; using = using;
292 (num, idents) = intros_spec ->
293 G.ElimType (loc, what, using, (num, idents))
294 | IDENT "exact"; t = tactic_term ->
298 | IDENT "fail" -> G.Fail loc
299 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
302 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
303 ("the pattern cannot specify the term to replace, only its"
304 ^ " paths in the hypotheses and in the conclusion")))
306 G.Fold (loc, kind, t, p)
309 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
310 let idents = match idents with None -> [] | Some idents -> idents in
311 G.FwdSimpl (loc, hyp, idents)
312 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
313 G.Generalize (loc,p,id)
314 | IDENT "id" -> G.IdTac loc
315 | IDENT "intro"; ident = OPT IDENT ->
316 let idents = match ident with None -> [] | Some id -> [Some id] in
317 G.Intros (loc, (Some 1, idents))
318 | IDENT "intros"; specs = intros_spec ->
319 G.Intros (loc, specs)
320 | IDENT "inversion"; t = tactic_term ->
323 linear = OPT [ IDENT "linear" ];
324 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
326 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
327 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
328 let linear = match linear with None -> false | Some _ -> true in
329 let to_what = match to_what with None -> [] | Some to_what -> to_what in
330 G.LApply (loc, linear, depth, to_what, what, ident)
331 | IDENT "left" -> G.Left loc
332 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
333 G.LetIn (loc, t, where)
334 | kind = reduction_kind; p = pattern_spec ->
335 G.Reduce (loc, kind, p)
336 | IDENT "reflexivity" ->
338 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
339 G.Replace (loc, p, t)
340 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
341 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
345 (HExtlib.Localized (loc,
346 (CicNotationParser.Parse_error
347 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
349 let n = match xnames with None -> [] | Some names -> names in
350 G.Rewrite (loc, d, t, p, n)
357 | IDENT "symmetry" ->
359 | IDENT "transitivity"; t = tactic_term ->
360 G.Transitivity (loc, t)
361 (* Produzioni Aggiunte *)
362 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
363 G.Assume (loc, id, t)
364 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
365 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
366 t' = tactic_term -> t']->
367 G.Suppose (loc, t, id, t1)
368 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
369 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
370 id2 = IDENT ; RPAREN ->
371 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
373 [ IDENT "using"; t=tactic_term -> `Term t
374 | params = auto_params -> `Auto params] ;
375 cont=by_continuation ->
377 BYC_done -> G.Bydone (loc, just)
378 | BYC_weproved (ty,id,t1) ->
379 G.By_just_we_proved(loc, just, ty, id, t1)
380 | BYC_letsuchthat (id1,t1,id2,t2) ->
381 G.ExistsElim (loc, just, id1, t1, id2, t2)
382 | BYC_wehaveand (id1,t1,id2,t2) ->
383 G.AndElim (loc, just, id1, t1, id2, t2))
384 | 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']->
385 G.We_need_to_prove (loc, t, id, t1)
386 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
387 G.We_proceed_by_cases_on (loc, t, t1)
388 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
389 G.We_proceed_by_induction_on (loc, t, t1)
390 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
391 G.Byinduction(loc, t, id)
392 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
393 G.Thesisbecomes(loc, t)
394 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
395 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
396 G.Case(loc,id,params)
397 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
399 termine = tactic_term;
403 [ IDENT "using"; t=tactic_term -> `Term t
404 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
405 | IDENT "proof" -> `Proof
406 | params = auto_params -> `Auto params];
407 cont = rewriting_step_continuation ->
408 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
409 | IDENT "obtain" ; name = IDENT;
410 termine = tactic_term;
414 [ IDENT "using"; t=tactic_term -> `Term t
415 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
416 | IDENT "proof" -> `Proof
417 | params = auto_params -> `Auto params];
418 cont = rewriting_step_continuation ->
419 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
423 [ IDENT "using"; t=tactic_term -> `Term t
424 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
425 | IDENT "proof" -> `Proof
426 | params = auto_params -> `Auto params];
427 cont = rewriting_step_continuation ->
428 G.RewritingStep(loc, None, t1, t2, cont)
432 [ IDENT "paramodulation"
446 i = auto_fixed_param -> i,""
447 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
448 string_of_int v | v = IDENT -> v ] -> i,v ];
449 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
450 (match tl with Some l -> l | None -> []),
455 [ 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)
456 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
457 "done" -> BYC_weproved (ty,None,t1)
459 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
460 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
461 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
462 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
463 BYC_wehaveand (id1,t1,id2,t2)
466 rewriting_step_continuation : [
473 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
476 | G.Seq (_, l) -> l @ [ t2 ]
482 [ tac = SELF; SYMBOL ";";
483 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
484 (G.Then (loc, tac, tacs))
487 [ IDENT "do"; count = int; tac = SELF ->
488 G.Do (loc, count, tac)
489 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
493 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
495 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
497 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
499 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
500 | LPAREN; tac = SELF; RPAREN -> tac
501 | tac = tactic -> tac
504 punctuation_tactical:
506 [ SYMBOL "[" -> G.Branch loc
507 | SYMBOL "|" -> G.Shift loc
508 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
509 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
510 | SYMBOL "]" -> G.Merge loc
511 | SYMBOL ";" -> G.Semicolon loc
512 | SYMBOL "." -> G.Dot loc
515 non_punctuation_tactical:
517 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
518 | IDENT "unfocus" -> G.Unfocus loc
519 | IDENT "skip" -> G.Skip loc
523 [ [ IDENT "ndefinition" ] -> `Definition
524 | [ IDENT "nfact" ] -> `Fact
525 | [ IDENT "nlemma" ] -> `Lemma
526 | [ IDENT "nremark" ] -> `Remark
527 | [ IDENT "ntheorem" ] -> `Theorem
531 [ [ IDENT "definition" ] -> `Definition
532 | [ IDENT "fact" ] -> `Fact
533 | [ IDENT "lemma" ] -> `Lemma
534 | [ IDENT "remark" ] -> `Remark
535 | [ IDENT "theorem" ] -> `Theorem
539 [ attr = theorem_flavour -> attr
540 | [ IDENT "axiom" ] -> `Axiom
541 | [ IDENT "mutual" ] -> `MutualDefinition
546 params = LIST0 protected_binder_vars;
547 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
548 fst_constructors = LIST0 constructor SEP SYMBOL "|";
551 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
552 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
553 (name, true, typ, constructors) ] SEP "with" -> types
557 (fun (names, typ) acc ->
558 (List.map (fun name -> (name, typ)) names) @ acc)
561 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
562 let tl_ind_types = match tl with None -> [] | Some types -> types in
563 let ind_types = fst_ind_type :: tl_ind_types in
569 params = LIST0 protected_binder_vars;
570 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
574 SYMBOL ":" -> false,0
575 | SYMBOL ":"; SYMBOL ">" -> true,0
576 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
579 let b,n = coercion in
581 ] SEP SYMBOL ";"; SYMBOL "}" ->
584 (fun (names, typ) acc ->
585 (List.map (fun name -> (name, typ)) names) @ acc)
588 (params,name,typ,fields)
592 [ [ IDENT "check" ]; t = term ->
594 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
595 G.Eval (loc, kind, t)
597 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
598 suri = QSTRING; prefix = OPT QSTRING;
599 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
600 let style = match style with
601 | None -> G.Declarative
602 | Some depth -> G.Procedural depth
604 let prefix = match prefix with None -> "" | Some prefix -> prefix in
605 G.Inline (loc,style,suri,prefix, flavour)
606 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
607 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
608 | IDENT "auto"; params = auto_params ->
609 G.AutoInteractive (loc,params)
610 | [ IDENT "whelp"; "match" ] ; t = term ->
612 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
614 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
616 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
618 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
623 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
624 let alpha = "[a-zA-Z]" in
625 let num = "[0-9]+" in
626 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
627 let decoration = "\\'" in
628 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
629 let rex = Str.regexp ("^"^ident^"$") in
630 if Str.string_match rex id 0 then
631 if (try ignore (UriManager.uri_of_string uri); true
632 with UriManager.IllFormedUri _ -> false) ||
633 (try ignore (NReference.reference_of_string uri); true
634 with NReference.IllFormedReference _ -> false)
636 L.Ident_alias (id, uri)
639 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
641 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
642 Printf.sprintf "Not a valid identifier: %s" id)))
643 | IDENT "symbol"; symbol = QSTRING;
644 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
645 SYMBOL "="; dsc = QSTRING ->
647 match instance with Some i -> i | None -> 0
649 L.Symbol_alias (symbol, instance, dsc)
651 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
652 SYMBOL "="; dsc = QSTRING ->
654 match instance with Some i -> i | None -> 0
656 L.Number_alias (instance, dsc)
660 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
662 N.IdentArg (List.length l, id)
666 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
667 | IDENT "right"; IDENT "associative" -> Gramext.RightA
668 | IDENT "non"; IDENT "associative" -> Gramext.NonA
672 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
675 [ dir = OPT direction; s = QSTRING;
676 assoc = OPT associativity; prec = precedence;
679 [ blob = UNPARSED_AST ->
680 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
681 (CicNotationParser.parse_level2_ast
682 (Ulexing.from_utf8_string blob))
683 | blob = UNPARSED_META ->
684 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
685 (CicNotationParser.parse_level2_meta
686 (Ulexing.from_utf8_string blob))
690 | None -> default_associativity
691 | Some assoc -> assoc
694 add_raw_attribute ~text:s
695 (CicNotationParser.parse_level1_pattern prec
696 (Ulexing.from_utf8_string s))
698 (dir, p1, assoc, prec, p2)
702 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
703 | id = IDENT -> N.VarPattern id
704 | SYMBOL "_" -> N.ImplicitPattern
705 | LPAREN; terms = LIST1 SELF; RPAREN ->
709 | terms -> N.ApplPattern terms)
713 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
719 IDENT "include" ; path = QSTRING ->
720 loc,path,L.WithPreferences
721 | IDENT "include'" ; path = QSTRING ->
722 loc,path,L.WithoutPreferences
726 IDENT "set"; n = QSTRING; v = QSTRING ->
728 | IDENT "drop" -> G.Drop loc
729 | IDENT "print"; s = IDENT -> G.Print (loc,s)
730 | IDENT "qed" -> G.Qed loc
731 | IDENT "nqed" -> G.NQed loc
732 | IDENT "variant" ; name = IDENT; SYMBOL ":";
733 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
736 (`Variant,name,typ,Some (N.Ident (newname, None))))
737 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
738 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
739 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
740 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
741 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
742 G.Obj (loc, N.Theorem (flavour, name, typ, body))
743 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
746 N.Theorem (flavour, name, N.Implicit, Some body))
747 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
748 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
749 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
750 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
751 | LETCOREC ; defs = let_defs ->
752 mk_rec_corec false `CoInductive defs loc
753 | LETREC ; defs = let_defs ->
754 mk_rec_corec false `Inductive defs loc
755 | NLETCOREC ; defs = let_defs ->
756 mk_rec_corec true `CoInductive defs loc
757 | NLETREC ; defs = let_defs ->
758 mk_rec_corec true `Inductive defs loc
759 | IDENT "inductive"; spec = inductive_spec ->
760 let (params, ind_types) = spec in
761 G.Obj (loc, N.Inductive (params, ind_types))
762 | IDENT "ninductive"; spec = inductive_spec ->
763 let (params, ind_types) = spec in
764 G.NObj (loc, N.Inductive (params, ind_types))
765 | IDENT "coinductive"; spec = inductive_spec ->
766 let (params, ind_types) = spec in
767 let ind_types = (* set inductive flags to false (coinductive) *)
768 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
771 G.Obj (loc, N.Inductive (params, ind_types))
772 | IDENT "ncoinductive"; spec = inductive_spec ->
773 let (params, ind_types) = spec in
774 let ind_types = (* set inductive flags to false (coinductive) *)
775 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
778 G.NObj (loc, N.Inductive (params, ind_types))
780 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
781 arity = OPT int ; saturations = OPT int;
782 composites = OPT (IDENT "nocomposites") ->
783 let arity = match arity with None -> 0 | Some x -> x in
784 let saturations = match saturations with None -> 0 | Some x -> x in
785 let composites = match composites with None -> true | Some _ -> false in
787 (loc, t, composites, arity, saturations)
788 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
789 G.PreferCoercion (loc, t)
790 | IDENT "pump" ; steps = int ->
792 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
793 G.UnificationHint (loc, t, n)
794 | IDENT "inverter"; name = IDENT; IDENT "for";
795 indty = tactic_term; paramspec = inverter_param_list ->
797 (loc, name, indty, paramspec)
798 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
799 G.Obj (loc, N.Record (params,name,ty,fields))
800 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
801 let uris = List.map UriManager.uri_of_string uris in
802 G.Default (loc,what,uris)
803 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
804 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
805 refl = tactic_term -> refl ] ;
806 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
807 sym = tactic_term -> sym ] ;
808 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
809 trans = tactic_term -> trans ] ;
811 G.Relation (loc,id,a,aeq,refl,sym,trans)
814 IDENT "alias" ; spec = alias_spec ->
816 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
817 L.Notation (loc, dir, l1, assoc, prec, l2)
818 | IDENT "interpretation"; id = QSTRING;
819 (symbol, args, l3) = interpretation ->
820 L.Interpretation (loc, id, (symbol, args), l3)
823 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
824 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
825 G.Tactic (loc, Some tac, punct)
826 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
827 | tac = ntactic; punct = punctuation_tactical ->
828 G.NTactic (loc, tac, punct)
829 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
830 G.NTactic (loc, G.NId loc, punct)
831 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
832 G.NonPunctuationTactical (loc, tac, punct)
833 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
837 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
845 fun ?(never_include=false) ~include_paths status ->
846 let stm = G.Executable (loc, ex) in
847 !grafite_callback status stm;
850 fun ?(never_include=false) ~include_paths status ->
851 let stm = G.Comment (loc, com) in
852 !grafite_callback status stm;
854 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
855 fun ?(never_include=false) ~include_paths status ->
857 G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
859 !grafite_callback status stm;
860 let _root, buri, fullpath, _rrelpath =
861 Librarian.baseuri_of_script ~include_paths fname
864 G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
867 if never_include then raise (NoInclusionPerformed fullpath)
868 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
871 | scom = lexicon_command ; SYMBOL "." ->
872 fun ?(never_include=false) ~include_paths status ->
873 !lexicon_callback status scom;
874 let status = LE.eval_command status scom in
876 | EOI -> raise End_of_file
883 let _ = initialize_parser () ;;
885 let exc_located_wrapper f =
889 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
890 | Stdpp.Exc_located (floc, Stream.Error msg) ->
891 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
892 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
894 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
895 | Stdpp.Exc_located (floc, exn) ->
897 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
899 let parse_statement lexbuf =
901 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
903 let statement () = !grafite_parser.statement
905 let history = ref [] ;;
909 history := !grafite_parser :: !history;
910 grafite_parser := initial_parser ();
919 grafite_parser := gp;
923 (* vim:set foldmethod=marker: *)