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"
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 -> []),
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)
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)
465 rewriting_step_continuation : [
472 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
475 | G.Seq (_, l) -> l @ [ t2 ]
481 [ tac = SELF; SYMBOL ";";
482 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
483 (G.Then (loc, tac, tacs))
486 [ IDENT "do"; count = int; tac = SELF ->
487 G.Do (loc, count, tac)
488 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
492 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
494 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
496 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
498 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
499 | LPAREN; tac = SELF; RPAREN -> tac
500 | tac = tactic -> tac
503 punctuation_tactical:
505 [ SYMBOL "[" -> G.Branch loc
506 | SYMBOL "|" -> G.Shift loc
507 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
508 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
509 | SYMBOL "]" -> G.Merge loc
510 | SYMBOL ";" -> G.Semicolon loc
511 | SYMBOL "." -> G.Dot loc
514 non_punctuation_tactical:
516 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
517 | IDENT "unfocus" -> G.Unfocus loc
518 | IDENT "skip" -> G.Skip loc
522 [ [ IDENT "ndefinition" ] -> `Definition
523 | [ IDENT "nfact" ] -> `Fact
524 | [ IDENT "nlemma" ] -> `Lemma
525 | [ IDENT "nremark" ] -> `Remark
526 | [ IDENT "ntheorem" ] -> `Theorem
530 [ [ IDENT "definition" ] -> `Definition
531 | [ IDENT "fact" ] -> `Fact
532 | [ IDENT "lemma" ] -> `Lemma
533 | [ IDENT "remark" ] -> `Remark
534 | [ IDENT "theorem" ] -> `Theorem
538 [ attr = theorem_flavour -> attr
539 | [ IDENT "axiom" ] -> `Axiom
540 | [ IDENT "mutual" ] -> `MutualDefinition
545 params = LIST0 protected_binder_vars;
546 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
547 fst_constructors = LIST0 constructor SEP SYMBOL "|";
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
556 (fun (names, typ) acc ->
557 (List.map (fun name -> (name, typ)) names) @ acc)
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
568 params = LIST0 protected_binder_vars;
569 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
573 SYMBOL ":" -> false,0
574 | SYMBOL ":"; SYMBOL ">" -> true,0
575 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
578 let b,n = coercion in
580 ] SEP SYMBOL ";"; SYMBOL "}" ->
583 (fun (names, typ) acc ->
584 (List.map (fun name -> (name, typ)) names) @ acc)
587 (params,name,typ,fields)
591 [ [ IDENT "check" ]; t = term ->
593 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
594 G.Eval (loc, kind, t)
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 -> G.Declarative
601 | Some depth -> G.Procedural depth
603 let prefix = match prefix with None -> "" | Some prefix -> prefix in
604 G.Inline (loc,style,suri,prefix, flavour)
605 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
606 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
607 | IDENT "auto"; params = auto_params ->
608 G.AutoInteractive (loc,params)
609 | [ IDENT "whelp"; "match" ] ; t = term ->
611 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
613 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
615 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
617 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
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 (try ignore (NReference.reference_of_string uri); true
633 with NReference.IllFormedReference _ -> false)
635 L.Ident_alias (id, uri)
638 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
640 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
641 Printf.sprintf "Not a valid identifier: %s" id)))
642 | IDENT "symbol"; symbol = QSTRING;
643 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
644 SYMBOL "="; dsc = QSTRING ->
646 match instance with Some i -> i | None -> 0
648 L.Symbol_alias (symbol, instance, dsc)
650 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
651 SYMBOL "="; dsc = QSTRING ->
653 match instance with Some i -> i | None -> 0
655 L.Number_alias (instance, dsc)
659 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
661 N.IdentArg (List.length l, id)
665 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
666 | IDENT "right"; IDENT "associative" -> Gramext.RightA
667 | IDENT "non"; IDENT "associative" -> Gramext.NonA
671 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
674 [ dir = OPT direction; s = QSTRING;
675 assoc = OPT associativity; prec = precedence;
678 [ blob = UNPARSED_AST ->
679 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
680 (CicNotationParser.parse_level2_ast
681 (Ulexing.from_utf8_string blob))
682 | blob = UNPARSED_META ->
683 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
684 (CicNotationParser.parse_level2_meta
685 (Ulexing.from_utf8_string blob))
689 | None -> default_associativity
690 | Some assoc -> assoc
693 add_raw_attribute ~text:s
694 (CicNotationParser.parse_level1_pattern prec
695 (Ulexing.from_utf8_string s))
697 (dir, p1, assoc, prec, p2)
701 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
702 | id = IDENT -> N.VarPattern id
703 | SYMBOL "_" -> N.ImplicitPattern
704 | LPAREN; terms = LIST1 SELF; RPAREN ->
708 | terms -> N.ApplPattern terms)
712 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
718 IDENT "include" ; path = QSTRING ->
719 loc,path,L.WithPreferences
720 | IDENT "include'" ; path = QSTRING ->
721 loc,path,L.WithoutPreferences
725 IDENT "set"; n = QSTRING; v = QSTRING ->
727 | IDENT "drop" -> G.Drop loc
728 | IDENT "print"; s = IDENT -> G.Print (loc,s)
729 | IDENT "qed" -> G.Qed loc
730 | IDENT "nqed" -> G.NQed loc
731 | IDENT "variant" ; name = IDENT; SYMBOL ":";
732 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
735 (`Variant,name,typ,Some (N.Ident (newname, None))))
736 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
737 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
738 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
739 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
740 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
741 G.Obj (loc, N.Theorem (flavour, name, typ, body))
742 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
745 N.Theorem (flavour, name, N.Implicit, Some body))
746 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
747 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
748 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
749 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
750 | LETCOREC ; defs = let_defs ->
751 mk_rec_corec false `CoInductive defs loc
752 | LETREC ; defs = let_defs ->
753 mk_rec_corec false `Inductive defs loc
754 | NLETCOREC ; defs = let_defs ->
755 mk_rec_corec true `CoInductive defs loc
756 | NLETREC ; defs = let_defs ->
757 mk_rec_corec true `Inductive defs loc
758 | IDENT "inductive"; spec = inductive_spec ->
759 let (params, ind_types) = spec in
760 G.Obj (loc, N.Inductive (params, ind_types))
761 | IDENT "ninductive"; spec = inductive_spec ->
762 let (params, ind_types) = spec in
763 G.NObj (loc, N.Inductive (params, ind_types))
764 | IDENT "coinductive"; spec = inductive_spec ->
765 let (params, ind_types) = spec in
766 let ind_types = (* set inductive flags to false (coinductive) *)
767 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
770 G.Obj (loc, N.Inductive (params, ind_types))
771 | IDENT "ncoinductive"; spec = inductive_spec ->
772 let (params, ind_types) = spec in
773 let ind_types = (* set inductive flags to false (coinductive) *)
774 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
777 G.NObj (loc, N.Inductive (params, ind_types))
779 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
780 arity = OPT int ; saturations = OPT int;
781 composites = OPT (IDENT "nocomposites") ->
782 let arity = match arity with None -> 0 | Some x -> x in
783 let saturations = match saturations with None -> 0 | Some x -> x in
784 let composites = match composites with None -> true | Some _ -> false in
786 (loc, t, composites, arity, saturations)
787 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
788 G.PreferCoercion (loc, t)
789 | IDENT "pump" ; steps = int ->
791 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
792 G.UnificationHint (loc, t, n)
793 | IDENT "inverter"; name = IDENT; IDENT "for";
794 indty = tactic_term; paramspec = inverter_param_list ->
796 (loc, name, indty, paramspec)
797 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
798 G.Obj (loc, N.Record (params,name,ty,fields))
799 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
800 G.NObj (loc, N.Record (params,name,ty,fields))
801 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
802 let uris = List.map UriManager.uri_of_string uris in
803 G.Default (loc,what,uris)
804 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
805 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
806 refl = tactic_term -> refl ] ;
807 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
808 sym = tactic_term -> sym ] ;
809 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
810 trans = tactic_term -> trans ] ;
812 G.Relation (loc,id,a,aeq,refl,sym,trans)
815 IDENT "alias" ; spec = alias_spec ->
817 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
818 L.Notation (loc, dir, l1, assoc, prec, l2)
819 | IDENT "interpretation"; id = QSTRING;
820 (symbol, args, l3) = interpretation ->
821 L.Interpretation (loc, id, (symbol, args), l3)
824 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
825 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
826 G.Tactic (loc, Some tac, punct)
827 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
828 | tac = ntactic; punct = punctuation_tactical ->
829 G.NTactic (loc, tac, punct)
830 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
831 G.NTactic (loc, G.NId loc, punct)
832 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
833 G.NonPunctuationTactical (loc, tac, punct)
834 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
838 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
846 fun ?(never_include=false) ~include_paths status ->
847 let stm = G.Executable (loc, ex) in
848 !grafite_callback status stm;
851 fun ?(never_include=false) ~include_paths status ->
852 let stm = G.Comment (loc, com) in
853 !grafite_callback status stm;
855 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
856 fun ?(never_include=false) ~include_paths status ->
858 G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
860 !grafite_callback status stm;
861 let _root, buri, fullpath, _rrelpath =
862 Librarian.baseuri_of_script ~include_paths fname
865 G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
868 if never_include then raise (NoInclusionPerformed fullpath)
869 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
872 | scom = lexicon_command ; SYMBOL "." ->
873 fun ?(never_include=false) ~include_paths status ->
874 !lexicon_callback status scom;
875 let status = LE.eval_command status scom in
877 | EOI -> raise End_of_file
884 let _ = initialize_parser () ;;
886 let exc_located_wrapper f =
890 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
891 | Stdpp.Exc_located (floc, Stream.Error msg) ->
892 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
893 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
895 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
896 | Stdpp.Exc_located (floc, exn) ->
898 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
900 let parse_statement lexbuf =
902 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
904 let statement () = !grafite_parser.statement
906 let history = ref [] ;;
910 history := !grafite_parser :: !history;
911 grafite_parser := initial_parser ();
920 grafite_parser := gp;
924 (* vim:set foldmethod=marker: *)