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 -> []),
455 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
456 | flavour = inline_flavour -> G.IPAs flavour
457 | IDENT "procedural" -> G.IPProcedural
458 | IDENT "nodefaults" -> G.IPNoDefaults
459 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
460 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
465 [ 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)
466 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
467 "done" -> BYC_weproved (ty,None,t1)
469 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
470 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
471 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
472 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
473 BYC_wehaveand (id1,t1,id2,t2)
476 rewriting_step_continuation : [
483 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
486 | G.Seq (_, l) -> l @ [ t2 ]
492 [ tac = SELF; SYMBOL ";";
493 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
494 (G.Then (loc, tac, tacs))
497 [ IDENT "do"; count = int; tac = SELF ->
498 G.Do (loc, count, tac)
499 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
503 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
505 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
507 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
509 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
510 | LPAREN; tac = SELF; RPAREN -> tac
511 | tac = tactic -> tac
514 punctuation_tactical:
516 [ SYMBOL "[" -> G.Branch loc
517 | SYMBOL "|" -> G.Shift loc
518 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
519 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
520 | SYMBOL "]" -> G.Merge loc
521 | SYMBOL ";" -> G.Semicolon loc
522 | SYMBOL "." -> G.Dot loc
525 non_punctuation_tactical:
527 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
528 | IDENT "unfocus" -> G.Unfocus loc
529 | IDENT "skip" -> G.Skip loc
533 [ [ IDENT "ndefinition" ] -> `Definition
534 | [ IDENT "nfact" ] -> `Fact
535 | [ IDENT "nlemma" ] -> `Lemma
536 | [ IDENT "nremark" ] -> `Remark
537 | [ IDENT "ntheorem" ] -> `Theorem
541 [ [ IDENT "definition" ] -> `Definition
542 | [ IDENT "fact" ] -> `Fact
543 | [ IDENT "lemma" ] -> `Lemma
544 | [ IDENT "remark" ] -> `Remark
545 | [ IDENT "theorem" ] -> `Theorem
549 [ attr = theorem_flavour -> attr
550 | [ IDENT "axiom" ] -> `Axiom
551 | [ IDENT "variant" ] -> `Variant
556 params = LIST0 protected_binder_vars;
557 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
558 fst_constructors = LIST0 constructor SEP SYMBOL "|";
561 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
562 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
563 (name, true, typ, constructors) ] SEP "with" -> types
567 (fun (names, typ) acc ->
568 (List.map (fun name -> (name, typ)) names) @ acc)
571 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
572 let tl_ind_types = match tl with None -> [] | Some types -> types in
573 let ind_types = fst_ind_type :: tl_ind_types in
579 params = LIST0 protected_binder_vars;
580 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
584 SYMBOL ":" -> false,0
585 | SYMBOL ":"; SYMBOL ">" -> true,0
586 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
589 let b,n = coercion in
591 ] SEP SYMBOL ";"; SYMBOL "}" ->
594 (fun (names, typ) acc ->
595 (List.map (fun name -> (name, typ)) names) @ acc)
598 (params,name,typ,fields)
602 [ [ IDENT "check" ]; t = term ->
604 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
605 G.Eval (loc, kind, t)
606 | IDENT "inline"; suri = QSTRING; params = inline_params ->
607 G.Inline (loc, suri, params)
608 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
609 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
610 | IDENT "auto"; params = auto_params ->
611 G.AutoInteractive (loc,params)
612 | [ IDENT "whelp"; "match" ] ; t = term ->
614 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
616 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
618 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
620 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
625 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
626 let alpha = "[a-zA-Z]" in
627 let num = "[0-9]+" in
628 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
629 let decoration = "\\'" in
630 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
631 let rex = Str.regexp ("^"^ident^"$") in
632 if Str.string_match rex id 0 then
633 if (try ignore (UriManager.uri_of_string uri); true
634 with UriManager.IllFormedUri _ -> false) ||
635 (try ignore (NReference.reference_of_string uri); true
636 with NReference.IllFormedReference _ -> false)
638 L.Ident_alias (id, uri)
641 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
643 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
644 Printf.sprintf "Not a valid identifier: %s" id)))
645 | IDENT "symbol"; symbol = QSTRING;
646 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
647 SYMBOL "="; dsc = QSTRING ->
649 match instance with Some i -> i | None -> 0
651 L.Symbol_alias (symbol, instance, dsc)
653 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
654 SYMBOL "="; dsc = QSTRING ->
656 match instance with Some i -> i | None -> 0
658 L.Number_alias (instance, dsc)
662 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
664 N.IdentArg (List.length l, id)
668 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
669 | IDENT "right"; IDENT "associative" -> Gramext.RightA
670 | IDENT "non"; IDENT "associative" -> Gramext.NonA
674 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
677 [ dir = OPT direction; s = QSTRING;
678 assoc = OPT associativity; prec = precedence;
681 [ blob = UNPARSED_AST ->
682 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
683 (CicNotationParser.parse_level2_ast
684 (Ulexing.from_utf8_string blob))
685 | blob = UNPARSED_META ->
686 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
687 (CicNotationParser.parse_level2_meta
688 (Ulexing.from_utf8_string blob))
692 | None -> default_associativity
693 | Some assoc -> assoc
696 add_raw_attribute ~text:s
697 (CicNotationParser.parse_level1_pattern prec
698 (Ulexing.from_utf8_string s))
700 (dir, p1, assoc, prec, p2)
704 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
705 | id = IDENT -> N.VarPattern id
706 | SYMBOL "_" -> N.ImplicitPattern
707 | LPAREN; terms = LIST1 SELF; RPAREN ->
711 | terms -> N.ApplPattern terms)
715 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
721 IDENT "include" ; path = QSTRING ->
722 loc,path,L.WithPreferences
723 | IDENT "include'" ; path = QSTRING ->
724 loc,path,L.WithoutPreferences
728 IDENT "set"; n = QSTRING; v = QSTRING ->
730 | IDENT "drop" -> G.Drop loc
731 | IDENT "print"; s = IDENT -> G.Print (loc,s)
732 | IDENT "qed" -> G.Qed loc
733 | IDENT "nqed" -> G.NQed loc
734 | IDENT "variant" ; name = IDENT; SYMBOL ":";
735 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
738 (`Variant,name,typ,Some (N.Ident (newname, None))))
739 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
740 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
741 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
742 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
743 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
744 G.Obj (loc, N.Theorem (flavour, name, typ, body))
745 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
748 N.Theorem (flavour, name, N.Implicit, Some body))
749 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
750 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
751 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
752 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
753 | LETCOREC ; defs = let_defs ->
754 mk_rec_corec false `CoInductive defs loc
755 | LETREC ; defs = let_defs ->
756 mk_rec_corec false `Inductive defs loc
757 | NLETCOREC ; defs = let_defs ->
758 mk_rec_corec true `CoInductive defs loc
759 | NLETREC ; defs = let_defs ->
760 mk_rec_corec true `Inductive defs loc
761 | IDENT "inductive"; spec = inductive_spec ->
762 let (params, ind_types) = spec in
763 G.Obj (loc, N.Inductive (params, ind_types))
764 | IDENT "ninductive"; spec = inductive_spec ->
765 let (params, ind_types) = spec in
766 G.NObj (loc, N.Inductive (params, ind_types))
767 | IDENT "coinductive"; spec = inductive_spec ->
768 let (params, ind_types) = spec in
769 let ind_types = (* set inductive flags to false (coinductive) *)
770 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
773 G.Obj (loc, N.Inductive (params, ind_types))
774 | IDENT "ncoinductive"; spec = inductive_spec ->
775 let (params, ind_types) = spec in
776 let ind_types = (* set inductive flags to false (coinductive) *)
777 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
780 G.NObj (loc, N.Inductive (params, ind_types))
782 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
783 arity = OPT int ; saturations = OPT int;
784 composites = OPT (IDENT "nocomposites") ->
785 let arity = match arity with None -> 0 | Some x -> x in
786 let saturations = match saturations with None -> 0 | Some x -> x in
787 let composites = match composites with None -> true | Some _ -> false in
789 (loc, t, composites, arity, saturations)
790 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
791 G.PreferCoercion (loc, t)
792 | IDENT "pump" ; steps = int ->
794 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
795 G.UnificationHint (loc, t, n)
796 | IDENT "inverter"; name = IDENT; IDENT "for";
797 indty = tactic_term; paramspec = inverter_param_list ->
799 (loc, name, indty, paramspec)
800 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
801 G.Obj (loc, N.Record (params,name,ty,fields))
802 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
803 G.NObj (loc, N.Record (params,name,ty,fields))
804 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
805 let uris = List.map UriManager.uri_of_string uris in
806 G.Default (loc,what,uris)
807 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
808 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
809 refl = tactic_term -> refl ] ;
810 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
811 sym = tactic_term -> sym ] ;
812 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
813 trans = tactic_term -> trans ] ;
815 G.Relation (loc,id,a,aeq,refl,sym,trans)
818 IDENT "alias" ; spec = alias_spec ->
820 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
821 L.Notation (loc, dir, l1, assoc, prec, l2)
822 | IDENT "interpretation"; id = QSTRING;
823 (symbol, args, l3) = interpretation ->
824 L.Interpretation (loc, id, (symbol, args), l3)
827 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
828 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
829 G.Tactic (loc, Some tac, punct)
830 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
831 | tac = ntactic; punct = punctuation_tactical ->
832 G.NTactic (loc, tac, punct)
833 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
834 G.NTactic (loc, G.NId loc, punct)
835 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
836 G.NonPunctuationTactical (loc, tac, punct)
837 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
841 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
849 fun ?(never_include=false) ~include_paths status ->
850 let stm = G.Executable (loc, ex) in
851 !grafite_callback status stm;
854 fun ?(never_include=false) ~include_paths status ->
855 let stm = G.Comment (loc, com) in
856 !grafite_callback status stm;
858 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
859 fun ?(never_include=false) ~include_paths status ->
861 G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
863 !grafite_callback status stm;
864 let _root, buri, fullpath, _rrelpath =
865 Librarian.baseuri_of_script ~include_paths fname
868 G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
871 if never_include then raise (NoInclusionPerformed fullpath)
872 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
875 | scom = lexicon_command ; SYMBOL "." ->
876 fun ?(never_include=false) ~include_paths status ->
877 !lexicon_callback status scom;
878 let status = LE.eval_command status scom in
880 | EOI -> raise End_of_file
887 let _ = initialize_parser () ;;
889 let exc_located_wrapper f =
893 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
894 | Stdpp.Exc_located (floc, Stream.Error msg) ->
895 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
896 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
898 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
899 | Stdpp.Exc_located (floc, exn) ->
901 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
903 let parse_statement lexbuf =
905 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
907 let statement () = !grafite_parser.statement
909 let history = ref [] ;;
913 history := !grafite_parser :: !history;
914 grafite_parser := initial_parser ();
923 grafite_parser := gp;
927 (* vim:set foldmethod=marker: *)