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 ] ];
122 | id = IDENT -> Some id ]
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 ]
135 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
136 let delta = match delta with None -> true | _ -> false in
138 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
139 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
140 let delta = match delta with None -> true | _ -> false in
143 sequent_pattern_spec: [
147 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
148 (id,match path with Some p -> p | None -> N.UserInput) ];
149 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
151 match goal_path, hyp_paths with
152 None, [] -> Some N.UserInput
154 | Some goal_path, _ -> Some goal_path
163 [ "match" ; wanted = tactic_term ;
164 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
166 | sps = sequent_pattern_spec ->
169 let wanted,hyp_paths,goal_path =
170 match wanted_and_sps with
171 wanted,None -> wanted, [], Some N.UserInput
172 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
174 wanted, hyp_paths, goal_path ] ->
176 None -> None,[],Some N.UserInput
179 inverter_param_list: [
180 [ params = tactic_term ->
181 let deannotate = function
182 | N.AttributedTerm (_,t) | t -> t
183 in match deannotate params with
184 | N.Implicit -> [false]
185 | N.UserInput -> [true]
187 List.map (fun x -> match deannotate x with
188 | N.Implicit -> false
189 | N.UserInput -> true
190 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
191 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
194 [ SYMBOL ">" -> `LeftToRight
195 | SYMBOL "<" -> `RightToLeft ]
197 int: [ [ num = NUMBER -> int_of_string num ] ];
199 [ idents = OPT ident_list0 ->
200 match idents with None -> [] | Some idents -> idents
204 [ OPT [ IDENT "names" ];
205 num = OPT [ num = int -> num ];
206 idents = intros_names ->
210 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
212 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
216 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
217 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
218 SYMBOL <:unicode<def>> ; bo = tactic_term ->
220 SYMBOL <:unicode<vdash>>;
221 concl = tactic_term -> (List.rev hyps,concl) ] ->
222 G.NAssert (loc, seqs)
223 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
224 G.NCases (loc, what, where)
225 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
226 G.NChange (loc, what, with_what)
227 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
228 G.NElim (loc, what, where)
229 | IDENT "ngeneralize"; p=pattern_spec ->
230 G.NGeneralize (loc, p)
231 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
232 where = pattern_spec ->
233 G.NLetIn (loc,where,t,name)
234 | kind = nreduction_kind; p = pattern_spec ->
235 G.NReduce (loc, kind, p)
236 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
237 G.NRewrite (loc, dir, what, where)
238 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
239 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
240 | SYMBOL "*" -> G.NCase1 (loc,"_")
241 | SYMBOL "*"; n=IDENT ->
246 [ IDENT "absurd"; t = tactic_term ->
248 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
250 | IDENT "apply"; t = tactic_term ->
252 | IDENT "applyP"; t = tactic_term ->
254 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
255 G.ApplyS (loc, t, params)
256 | IDENT "assumption" ->
258 | IDENT "autobatch"; params = auto_params ->
259 G.AutoBatch (loc,params)
260 | IDENT "cases"; what = tactic_term;
261 pattern = OPT pattern_spec;
262 specs = intros_spec ->
263 let pattern = match pattern with
264 | None -> None, [], Some N.UserInput
265 | Some pattern -> pattern
267 G.Cases (loc, what, pattern, specs)
268 | IDENT "clear"; ids = LIST1 IDENT ->
270 | IDENT "clearbody"; id = IDENT ->
272 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
273 G.Change (loc, what, t)
274 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
275 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
276 let times = match times with None -> 1 | Some i -> i in
277 G.Compose (loc, t1, t2, times, specs)
278 | IDENT "constructor"; n = int ->
279 G.Constructor (loc, n)
280 | IDENT "contradiction" ->
282 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
283 G.Cut (loc, ident, t)
284 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
285 let idents = match idents with None -> [] | Some idents -> idents in
286 G.Decompose (loc, idents)
287 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
288 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
289 G.Destruct (loc, xts)
290 | IDENT "elim"; what = tactic_term; using = using;
291 pattern = OPT pattern_spec;
292 ispecs = intros_spec ->
293 let pattern = match pattern with
294 | None -> None, [], Some N.UserInput
295 | Some pattern -> pattern
297 G.Elim (loc, what, using, pattern, ispecs)
298 | IDENT "elimType"; what = tactic_term; using = using;
299 (num, idents) = intros_spec ->
300 G.ElimType (loc, what, using, (num, idents))
301 | IDENT "exact"; t = tactic_term ->
305 | IDENT "fail" -> G.Fail loc
306 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
309 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
310 ("the pattern cannot specify the term to replace, only its"
311 ^ " paths in the hypotheses and in the conclusion")))
313 G.Fold (loc, kind, t, p)
316 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
317 let idents = match idents with None -> [] | Some idents -> idents in
318 G.FwdSimpl (loc, hyp, idents)
319 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
320 G.Generalize (loc,p,id)
321 | IDENT "id" -> G.IdTac loc
322 | IDENT "intro"; ident = OPT IDENT ->
323 let idents = match ident with None -> [] | Some id -> [Some id] in
324 G.Intros (loc, (Some 1, idents))
325 | IDENT "intros"; specs = intros_spec ->
326 G.Intros (loc, specs)
327 | IDENT "inversion"; t = tactic_term ->
330 linear = OPT [ IDENT "linear" ];
331 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
333 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
334 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
335 let linear = match linear with None -> false | Some _ -> true in
336 let to_what = match to_what with None -> [] | Some to_what -> to_what in
337 G.LApply (loc, linear, depth, to_what, what, ident)
338 | IDENT "left" -> G.Left loc
339 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
340 G.LetIn (loc, t, where)
341 | kind = reduction_kind; p = pattern_spec ->
342 G.Reduce (loc, kind, p)
343 | IDENT "reflexivity" ->
345 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
346 G.Replace (loc, p, t)
347 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
348 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
352 (HExtlib.Localized (loc,
353 (CicNotationParser.Parse_error
354 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
356 let n = match xnames with None -> [] | Some names -> names in
357 G.Rewrite (loc, d, t, p, n)
364 | IDENT "symmetry" ->
366 | IDENT "transitivity"; t = tactic_term ->
367 G.Transitivity (loc, t)
368 (* Produzioni Aggiunte *)
369 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
370 G.Assume (loc, id, t)
371 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
372 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
373 t' = tactic_term -> t']->
374 G.Suppose (loc, t, id, t1)
375 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
376 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
377 id2 = IDENT ; RPAREN ->
378 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
380 [ IDENT "using"; t=tactic_term -> `Term t
381 | params = auto_params -> `Auto params] ;
382 cont=by_continuation ->
384 BYC_done -> G.Bydone (loc, just)
385 | BYC_weproved (ty,id,t1) ->
386 G.By_just_we_proved(loc, just, ty, id, t1)
387 | BYC_letsuchthat (id1,t1,id2,t2) ->
388 G.ExistsElim (loc, just, id1, t1, id2, t2)
389 | BYC_wehaveand (id1,t1,id2,t2) ->
390 G.AndElim (loc, just, id1, t1, id2, t2))
391 | 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']->
392 G.We_need_to_prove (loc, t, id, t1)
393 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
394 G.We_proceed_by_cases_on (loc, t, t1)
395 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
396 G.We_proceed_by_induction_on (loc, t, t1)
397 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
398 G.Byinduction(loc, t, id)
399 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
400 G.Thesisbecomes(loc, t)
401 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
402 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
403 G.Case(loc,id,params)
404 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
406 termine = tactic_term;
410 [ IDENT "using"; t=tactic_term -> `Term t
411 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
412 | IDENT "proof" -> `Proof
413 | params = auto_params -> `Auto params];
414 cont = rewriting_step_continuation ->
415 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
416 | IDENT "obtain" ; name = IDENT;
417 termine = tactic_term;
421 [ IDENT "using"; t=tactic_term -> `Term t
422 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
423 | IDENT "proof" -> `Proof
424 | params = auto_params -> `Auto params];
425 cont = rewriting_step_continuation ->
426 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
430 [ IDENT "using"; t=tactic_term -> `Term t
431 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
432 | IDENT "proof" -> `Proof
433 | params = auto_params -> `Auto params];
434 cont = rewriting_step_continuation ->
435 G.RewritingStep(loc, None, t1, t2, cont)
439 [ IDENT "paramodulation"
452 i = auto_fixed_param -> i,""
453 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
454 string_of_int v | v = IDENT -> v ] -> i,v ];
455 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
456 (match tl with Some l -> l | None -> []),
462 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
463 | flavour = inline_flavour -> G.IPAs flavour
464 | IDENT "procedural" -> G.IPProcedural
465 | IDENT "nodefaults" -> G.IPNoDefaults
466 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
467 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
472 [ 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)
473 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
474 "done" -> BYC_weproved (ty,None,t1)
476 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
477 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
478 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
479 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
480 BYC_wehaveand (id1,t1,id2,t2)
483 rewriting_step_continuation : [
490 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
493 | G.Seq (_, l) -> l @ [ t2 ]
499 [ tac = SELF; SYMBOL ";";
500 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
501 (G.Then (loc, tac, tacs))
504 [ IDENT "do"; count = int; tac = SELF ->
505 G.Do (loc, count, tac)
506 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
510 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
512 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
514 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
516 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
517 | LPAREN; tac = SELF; RPAREN -> tac
518 | tac = tactic -> tac
521 punctuation_tactical:
523 [ SYMBOL "[" -> G.Branch loc
524 | SYMBOL "|" -> G.Shift loc
525 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
526 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
527 | SYMBOL "]" -> G.Merge loc
528 | SYMBOL ";" -> G.Semicolon loc
529 | SYMBOL "." -> G.Dot loc
532 non_punctuation_tactical:
534 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
535 | IDENT "unfocus" -> G.Unfocus loc
536 | IDENT "skip" -> G.Skip loc
540 [ [ IDENT "ndefinition" ] -> `Definition
541 | [ IDENT "nfact" ] -> `Fact
542 | [ IDENT "nlemma" ] -> `Lemma
543 | [ IDENT "nremark" ] -> `Remark
544 | [ IDENT "ntheorem" ] -> `Theorem
548 [ [ IDENT "definition" ] -> `Definition
549 | [ IDENT "fact" ] -> `Fact
550 | [ IDENT "lemma" ] -> `Lemma
551 | [ IDENT "remark" ] -> `Remark
552 | [ IDENT "theorem" ] -> `Theorem
556 [ attr = theorem_flavour -> attr
557 | [ IDENT "axiom" ] -> `Axiom
558 | [ IDENT "variant" ] -> `Variant
563 params = LIST0 protected_binder_vars;
564 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
565 fst_constructors = LIST0 constructor SEP SYMBOL "|";
568 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
569 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
570 (name, true, typ, constructors) ] SEP "with" -> types
574 (fun (names, typ) acc ->
575 (List.map (fun name -> (name, typ)) names) @ acc)
578 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
579 let tl_ind_types = match tl with None -> [] | Some types -> types in
580 let ind_types = fst_ind_type :: tl_ind_types in
586 params = LIST0 protected_binder_vars;
587 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
591 SYMBOL ":" -> false,0
592 | SYMBOL ":"; SYMBOL ">" -> true,0
593 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
596 let b,n = coercion in
598 ] SEP SYMBOL ";"; SYMBOL "}" ->
601 (fun (names, typ) acc ->
602 (List.map (fun name -> (name, typ)) names) @ acc)
605 (params,name,typ,fields)
609 [ [ IDENT "check" ]; t = term ->
611 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
612 G.Eval (loc, kind, t)
613 | IDENT "inline"; suri = QSTRING; params = inline_params ->
614 G.Inline (loc, suri, params)
615 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
616 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
617 | IDENT "auto"; params = auto_params ->
618 G.AutoInteractive (loc,params)
619 | [ IDENT "whelp"; "match" ] ; t = term ->
621 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
623 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
625 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
627 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
632 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
633 let alpha = "[a-zA-Z]" in
634 let num = "[0-9]+" in
635 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
636 let decoration = "\\'" in
637 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
638 let rex = Str.regexp ("^"^ident^"$") in
639 if Str.string_match rex id 0 then
640 if (try ignore (UriManager.uri_of_string uri); true
641 with UriManager.IllFormedUri _ -> false) ||
642 (try ignore (NReference.reference_of_string uri); true
643 with NReference.IllFormedReference _ -> false)
645 L.Ident_alias (id, uri)
648 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
650 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
651 Printf.sprintf "Not a valid identifier: %s" id)))
652 | IDENT "symbol"; symbol = QSTRING;
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.Symbol_alias (symbol, instance, dsc)
660 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
661 SYMBOL "="; dsc = QSTRING ->
663 match instance with Some i -> i | None -> 0
665 L.Number_alias (instance, dsc)
669 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
671 N.IdentArg (List.length l, id)
675 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
676 | IDENT "right"; IDENT "associative" -> Gramext.RightA
677 | IDENT "non"; IDENT "associative" -> Gramext.NonA
681 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
684 [ dir = OPT direction; s = QSTRING;
685 assoc = OPT associativity; prec = precedence;
688 [ blob = UNPARSED_AST ->
689 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
690 (CicNotationParser.parse_level2_ast
691 (Ulexing.from_utf8_string blob))
692 | blob = UNPARSED_META ->
693 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
694 (CicNotationParser.parse_level2_meta
695 (Ulexing.from_utf8_string blob))
699 | None -> default_associativity
700 | Some assoc -> assoc
703 add_raw_attribute ~text:s
704 (CicNotationParser.parse_level1_pattern prec
705 (Ulexing.from_utf8_string s))
707 (dir, p1, assoc, prec, p2)
711 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
712 | IMPLICIT -> N.ImplicitPattern
713 | id = IDENT -> N.VarPattern id
714 | LPAREN; terms = LIST1 SELF; RPAREN ->
718 | terms -> N.ApplPattern terms)
722 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
728 IDENT "include" ; path = QSTRING ->
729 loc,path,L.WithPreferences
730 | IDENT "include'" ; path = QSTRING ->
731 loc,path,L.WithoutPreferences
735 IDENT "set"; n = QSTRING; v = QSTRING ->
737 | IDENT "drop" -> G.Drop loc
738 | IDENT "print"; s = IDENT -> G.Print (loc,s)
739 | IDENT "qed" -> G.Qed loc
740 | IDENT "nqed" -> G.NQed loc
741 | IDENT "variant" ; name = IDENT; SYMBOL ":";
742 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
745 (`Variant,name,typ,Some (N.Ident (newname, None))))
746 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
747 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
748 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
749 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
750 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
751 G.Obj (loc, N.Theorem (flavour, name, typ, body))
752 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
755 N.Theorem (flavour, name, N.Implicit, Some body))
756 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
757 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
758 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
759 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
760 | LETCOREC ; defs = let_defs ->
761 mk_rec_corec false `CoInductive defs loc
762 | LETREC ; defs = let_defs ->
763 mk_rec_corec false `Inductive defs loc
764 | NLETCOREC ; defs = let_defs ->
765 mk_rec_corec true `CoInductive defs loc
766 | NLETREC ; defs = let_defs ->
767 mk_rec_corec true `Inductive defs loc
768 | IDENT "inductive"; spec = inductive_spec ->
769 let (params, ind_types) = spec in
770 G.Obj (loc, N.Inductive (params, ind_types))
771 | IDENT "ninductive"; spec = inductive_spec ->
772 let (params, ind_types) = spec in
773 G.NObj (loc, N.Inductive (params, ind_types))
774 | IDENT "coinductive"; 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.Obj (loc, N.Inductive (params, ind_types))
781 | IDENT "ncoinductive"; spec = inductive_spec ->
782 let (params, ind_types) = spec in
783 let ind_types = (* set inductive flags to false (coinductive) *)
784 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
787 G.NObj (loc, N.Inductive (params, ind_types))
788 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
789 strict = [ SYMBOL <:unicode<lt>> -> true
790 | SYMBOL <:unicode<leq>> -> false ];
794 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
795 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
796 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
797 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
798 | _ -> raise (Failure "only a sort can be constrained")
802 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
803 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
804 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
805 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
806 | _ -> raise (Failure "only a sort can be constrained")
808 G.NUnivConstraint (loc, strict,u1,u2)
810 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
811 arity = OPT int ; saturations = OPT int;
812 composites = OPT (IDENT "nocomposites") ->
813 let arity = match arity with None -> 0 | Some x -> x in
814 let saturations = match saturations with None -> 0 | Some x -> x in
815 let composites = match composites with None -> true | Some _ -> false in
817 (loc, t, composites, arity, saturations)
818 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
819 G.PreferCoercion (loc, t)
820 | IDENT "pump" ; steps = int ->
822 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
823 G.UnificationHint (loc, t, n)
824 | IDENT "inverter"; name = IDENT; IDENT "for";
825 indty = tactic_term; paramspec = inverter_param_list ->
827 (loc, name, indty, paramspec)
828 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
829 G.Obj (loc, N.Record (params,name,ty,fields))
830 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
831 G.NObj (loc, N.Record (params,name,ty,fields))
832 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
833 let uris = List.map UriManager.uri_of_string uris in
834 G.Default (loc,what,uris)
835 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
836 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
837 refl = tactic_term -> refl ] ;
838 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
839 sym = tactic_term -> sym ] ;
840 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
841 trans = tactic_term -> trans ] ;
843 G.Relation (loc,id,a,aeq,refl,sym,trans)
846 IDENT "alias" ; spec = alias_spec ->
848 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
849 L.Notation (loc, dir, l1, assoc, prec, l2)
850 | IDENT "interpretation"; id = QSTRING;
851 (symbol, args, l3) = interpretation ->
852 L.Interpretation (loc, id, (symbol, args), l3)
855 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
856 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
857 G.Tactic (loc, Some tac, punct)
858 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
859 | tac = ntactic; punct = punctuation_tactical ->
860 G.NTactic (loc, tac, punct)
861 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
862 G.NTactic (loc, G.NId loc, punct)
863 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
864 G.NonPunctuationTactical (loc, tac, punct)
865 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
866 G.NNonPunctuationTactical (loc, tac, punct)
867 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
871 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
879 fun ?(never_include=false) ~include_paths status ->
880 let stm = G.Executable (loc, ex) in
881 !grafite_callback status stm;
884 fun ?(never_include=false) ~include_paths status ->
885 let stm = G.Comment (loc, com) in
886 !grafite_callback status stm;
888 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
889 fun ?(never_include=false) ~include_paths status ->
891 G.Executable (loc, G.Command (loc, G.Include (iloc, fname)))
893 !grafite_callback status stm;
894 let _root, buri, fullpath, _rrelpath =
895 Librarian.baseuri_of_script ~include_paths fname
898 G.Executable (loc, G.Command (loc, G.Include (iloc, buri)))
901 if never_include then raise (NoInclusionPerformed fullpath)
902 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
905 | scom = lexicon_command ; SYMBOL "." ->
906 fun ?(never_include=false) ~include_paths status ->
907 !lexicon_callback status scom;
908 let status = LE.eval_command status scom in
910 | EOI -> raise End_of_file
917 let _ = initialize_parser () ;;
919 let exc_located_wrapper f =
923 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
924 | Stdpp.Exc_located (floc, Stream.Error msg) ->
925 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
926 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
928 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
929 | Stdpp.Exc_located (floc, exn) ->
931 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
933 let parse_statement lexbuf =
935 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
937 let statement () = !grafite_parser.statement
939 let history = ref [] ;;
943 history := !grafite_parser :: !history;
944 grafite_parser := initial_parser ();
953 grafite_parser := gp;
957 (* vim:set foldmethod=marker: *)