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
42 type 'status statement =
43 ?never_include:bool ->
44 (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
45 include_paths:string list -> (#LE.status as 'status) ->
46 'status * ast_statement localized_option
48 type 'status parser_status = {
50 term : N.term Grammar.Entry.e;
51 statement : #LE.status as 'status statement Grammar.Entry.e;
54 let grafite_callback = ref (fun _ -> ())
55 let set_grafite_callback cb = grafite_callback := cb
57 let lexicon_callback = ref (fun _ -> ())
58 let set_lexicon_callback cb = lexicon_callback := cb
60 let initial_parser () =
61 let grammar = CicNotationParser.level2_ast_grammar () in
62 let term = CicNotationParser.term () in
63 let statement = Grammar.Entry.create grammar "statement" in
64 { grammar = grammar; term = term; statement = statement }
67 let grafite_parser = ref (initial_parser ())
69 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
71 let default_associativity = Gramext.NonA
73 let mk_rec_corec ind_kind defs loc =
74 (* In case of mutual definitions here we produce just
75 the syntax tree for the first one. The others will be
76 generated from the completely specified term just before
77 insertion in the environment. We use the flavour
78 `MutualDefinition to rememer this. *)
81 | (params,(N.Ident (name, None), ty),_,_) :: _ ->
82 let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
85 (fun var ty -> N.Binder (`Pi,var,ty)
91 let body = N.Ident (name,None) in
93 if List.length defs = 1 then
98 (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
100 let nmk_rec_corec ind_kind defs loc =
101 let loc,t = mk_rec_corec ind_kind defs loc in
104 let mk_rec_corec ind_kind defs loc =
105 let loc,t = mk_rec_corec ind_kind defs loc in
108 let npunct_of_punct = function
109 | G.Branch loc -> G.NBranch loc
110 | G.Shift loc -> G.NShift loc
111 | G.Pos (loc, i) -> G.NPos (loc, i)
112 | G.Wildcard loc -> G.NWildcard loc
113 | G.Merge loc -> G.NMerge loc
114 | G.Semicolon loc -> G.NSemicolon loc
115 | G.Dot loc -> G.NDot loc
117 let nnon_punct_of_punct = function
118 | G.Skip loc -> G.NSkip loc
119 | G.Unfocus loc -> G.NUnfocus loc
120 | G.Focus (loc,l) -> G.NFocus (loc,l)
122 let npunct_of_punct = function
123 | G.Branch loc -> G.NBranch loc
124 | G.Shift loc -> G.NShift loc
125 | G.Pos (loc, i) -> G.NPos (loc, i)
126 | G.Wildcard loc -> G.NWildcard loc
127 | G.Merge loc -> G.NMerge loc
128 | G.Semicolon loc -> G.NSemicolon loc
129 | G.Dot loc -> G.NDot loc
132 type by_continuation =
134 | BYC_weproved of N.term * string option * N.term option
135 | BYC_letsuchthat of string * N.term * string * N.term
136 | BYC_wehaveand of string * N.term * string * N.term
138 let initialize_parser () =
139 (* {{{ parser initialization *)
140 let term = !grafite_parser.term in
141 let statement = !grafite_parser.statement in
142 let let_defs = CicNotationParser.let_defs () in
143 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
145 GLOBAL: term statement;
146 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
147 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
150 | id = IDENT -> Some id ]
152 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
154 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
157 [ IDENT "normalize" -> `Normalize
158 | IDENT "simplify" -> `Simpl
159 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
160 | IDENT "whd" -> `Whd ]
163 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
164 let delta = match delta with None -> true | _ -> false in
166 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
167 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
168 let delta = match delta with None -> true | _ -> false in
171 sequent_pattern_spec: [
175 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
176 (id,match path with Some p -> p | None -> N.UserInput) ];
177 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
179 match goal_path, hyp_paths with
180 None, [] -> Some N.UserInput
182 | Some goal_path, _ -> Some goal_path
191 [ "match" ; wanted = tactic_term ;
192 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
194 | sps = sequent_pattern_spec ->
197 let wanted,hyp_paths,goal_path =
198 match wanted_and_sps with
199 wanted,None -> wanted, [], Some N.UserInput
200 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
202 wanted, hyp_paths, goal_path ] ->
204 None -> None,[],Some N.UserInput
207 inverter_param_list: [
208 [ params = tactic_term ->
209 let deannotate = function
210 | N.AttributedTerm (_,t) | t -> t
211 in match deannotate params with
212 | N.Implicit _ -> [false]
213 | N.UserInput -> [true]
215 List.map (fun x -> match deannotate x with
216 | N.Implicit _ -> false
217 | N.UserInput -> true
218 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
219 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
222 [ SYMBOL ">" -> `LeftToRight
223 | SYMBOL "<" -> `RightToLeft ]
225 int: [ [ num = NUMBER -> int_of_string num ] ];
227 [ idents = OPT ident_list0 ->
228 match idents with None -> [] | Some idents -> idents
232 [ OPT [ IDENT "names" ];
233 num = OPT [ num = int -> num ];
234 idents = intros_names ->
238 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
240 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
241 | IDENT "napplyS"; t = tactic_term -> G.NSmartApply (loc, t)
245 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
246 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
247 SYMBOL <:unicode<def>> ; bo = tactic_term ->
249 SYMBOL <:unicode<vdash>>;
250 concl = tactic_term -> (List.rev hyps,concl) ] ->
251 G.NAssert (loc, seqs)
252 | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
253 | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ->
254 let depth = match num with Some n -> n | None -> "1" in
255 G.NAuto (loc, ([],["slir","";"depth",depth]))
256 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
257 G.NCases (loc, what, where)
258 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
259 G.NChange (loc, what, with_what)
260 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
262 (match num with None -> None | Some x -> Some (int_of_string x)),l)
263 | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
264 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
265 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
266 | IDENT "ndestruct" -> G.NDestruct loc
267 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
268 G.NElim (loc, what, where)
269 | IDENT "ngeneralize"; p=pattern_spec ->
270 G.NGeneralize (loc, p)
271 | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
272 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
273 where = pattern_spec ->
274 G.NLetIn (loc,where,t,name)
275 | kind = nreduction_kind; p = pattern_spec ->
276 G.NReduce (loc, kind, p)
277 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
278 G.NRewrite (loc, dir, what, where)
279 | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac)
280 | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
281 | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
282 | IDENT "nassumption" -> G.NAssumption loc
283 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
284 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
285 | SYMBOL "*" -> G.NCase1 (loc,"_")
286 | SYMBOL "*"; n=IDENT ->
291 [ IDENT "absurd"; t = tactic_term ->
293 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
295 | IDENT "apply"; t = tactic_term ->
297 | IDENT "applyP"; t = tactic_term ->
299 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
300 G.ApplyS (loc, t, params)
301 | IDENT "assumption" ->
303 | IDENT "autobatch"; params = auto_params ->
304 G.AutoBatch (loc,params)
305 | IDENT "cases"; what = tactic_term;
306 pattern = OPT pattern_spec;
307 specs = intros_spec ->
308 let pattern = match pattern with
309 | None -> None, [], Some N.UserInput
310 | Some pattern -> pattern
312 G.Cases (loc, what, pattern, specs)
313 | IDENT "clear"; ids = LIST1 IDENT ->
315 | IDENT "clearbody"; id = IDENT ->
317 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
318 G.Change (loc, what, t)
319 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
320 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
321 let times = match times with None -> 1 | Some i -> i in
322 G.Compose (loc, t1, t2, times, specs)
323 | IDENT "constructor"; n = int ->
324 G.Constructor (loc, n)
325 | IDENT "contradiction" ->
327 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
328 G.Cut (loc, ident, t)
329 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
330 let idents = match idents with None -> [] | Some idents -> idents in
331 G.Decompose (loc, idents)
332 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
333 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
334 G.Destruct (loc, xts)
335 | IDENT "elim"; what = tactic_term; using = using;
336 pattern = OPT pattern_spec;
337 ispecs = intros_spec ->
338 let pattern = match pattern with
339 | None -> None, [], Some N.UserInput
340 | Some pattern -> pattern
342 G.Elim (loc, what, using, pattern, ispecs)
343 | IDENT "elimType"; what = tactic_term; using = using;
344 (num, idents) = intros_spec ->
345 G.ElimType (loc, what, using, (num, idents))
346 | IDENT "exact"; t = tactic_term ->
350 | IDENT "fail" -> G.Fail loc
351 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
354 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
355 ("the pattern cannot specify the term to replace, only its"
356 ^ " paths in the hypotheses and in the conclusion")))
358 G.Fold (loc, kind, t, p)
361 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
362 let idents = match idents with None -> [] | Some idents -> idents in
363 G.FwdSimpl (loc, hyp, idents)
364 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
365 G.Generalize (loc,p,id)
366 | IDENT "id" -> G.IdTac loc
367 | IDENT "intro"; ident = OPT IDENT ->
368 let idents = match ident with None -> [] | Some id -> [Some id] in
369 G.Intros (loc, (Some 1, idents))
370 | IDENT "intros"; specs = intros_spec ->
371 G.Intros (loc, specs)
372 | IDENT "inversion"; t = tactic_term ->
375 linear = OPT [ IDENT "linear" ];
376 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
378 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
379 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
380 let linear = match linear with None -> false | Some _ -> true in
381 let to_what = match to_what with None -> [] | Some to_what -> to_what in
382 G.LApply (loc, linear, depth, to_what, what, ident)
383 | IDENT "left" -> G.Left loc
384 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
385 G.LetIn (loc, t, where)
386 | kind = reduction_kind; p = pattern_spec ->
387 G.Reduce (loc, kind, p)
388 | IDENT "reflexivity" ->
390 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
391 G.Replace (loc, p, t)
392 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
393 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
397 (HExtlib.Localized (loc,
398 (CicNotationParser.Parse_error
399 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
401 let n = match xnames with None -> [] | Some names -> names in
402 G.Rewrite (loc, d, t, p, n)
409 | IDENT "symmetry" ->
411 | IDENT "transitivity"; t = tactic_term ->
412 G.Transitivity (loc, t)
413 (* Produzioni Aggiunte *)
414 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
415 G.Assume (loc, id, t)
416 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
417 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
418 t' = tactic_term -> t']->
419 G.Suppose (loc, t, id, t1)
420 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
421 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
422 id2 = IDENT ; RPAREN ->
423 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
425 [ IDENT "using"; t=tactic_term -> `Term t
426 | params = auto_params -> `Auto params] ;
427 cont=by_continuation ->
429 BYC_done -> G.Bydone (loc, just)
430 | BYC_weproved (ty,id,t1) ->
431 G.By_just_we_proved(loc, just, ty, id, t1)
432 | BYC_letsuchthat (id1,t1,id2,t2) ->
433 G.ExistsElim (loc, just, id1, t1, id2, t2)
434 | BYC_wehaveand (id1,t1,id2,t2) ->
435 G.AndElim (loc, just, id1, t1, id2, t2))
436 | 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']->
437 G.We_need_to_prove (loc, t, id, t1)
438 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
439 G.We_proceed_by_cases_on (loc, t, t1)
440 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
441 G.We_proceed_by_induction_on (loc, t, t1)
442 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
443 G.Byinduction(loc, t, id)
444 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
445 G.Thesisbecomes(loc, t)
446 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
447 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
448 G.Case(loc,id,params)
449 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
451 termine = tactic_term;
455 [ IDENT "using"; t=tactic_term -> `Term t
456 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
457 | IDENT "proof" -> `Proof
458 | params = auto_params -> `Auto params];
459 cont = rewriting_step_continuation ->
460 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
461 | IDENT "obtain" ; name = IDENT;
462 termine = tactic_term;
466 [ IDENT "using"; t=tactic_term -> `Term t
467 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
468 | IDENT "proof" -> `Proof
469 | params = auto_params -> `Auto params];
470 cont = rewriting_step_continuation ->
471 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
475 [ IDENT "using"; t=tactic_term -> `Term t
476 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
477 | IDENT "proof" -> `Proof
478 | params = auto_params -> `Auto params];
479 cont = rewriting_step_continuation ->
480 G.RewritingStep(loc, None, t1, t2, cont)
484 [ IDENT "paramodulation"
485 | IDENT "fast_paramod"
500 i = auto_fixed_param -> i,""
501 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
502 string_of_int v | v = IDENT -> v ] -> i,v ];
503 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
504 (match tl with Some l -> l | None -> []),
510 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
511 | flavour = inline_flavour -> G.IPAs flavour
512 | IDENT "coercions" -> G.IPCoercions
513 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
514 | IDENT "procedural" -> G.IPProcedural
515 | IDENT "nodefaults" -> G.IPNoDefaults
516 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
517 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
518 | IDENT "comments" -> G.IPComments
519 | IDENT "cr" -> G.IPCR
524 [ 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)
525 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
526 "done" -> BYC_weproved (ty,None,t1)
528 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
529 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
530 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
531 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
532 BYC_wehaveand (id1,t1,id2,t2)
535 rewriting_step_continuation : [
542 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
545 | G.Seq (_, l) -> l @ [ t2 ]
551 [ tac = SELF; SYMBOL ";";
552 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
553 (G.Then (loc, tac, tacs))
556 [ IDENT "do"; count = int; tac = SELF ->
557 G.Do (loc, count, tac)
558 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
562 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
564 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
566 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
568 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
569 | LPAREN; tac = SELF; RPAREN -> tac
570 | tac = tactic -> tac
573 npunctuation_tactical:
575 [ SYMBOL "[" -> G.NBranch loc
576 | SYMBOL "|" -> G.NShift loc
577 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
578 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
579 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
580 | SYMBOL "]" -> G.NMerge loc
581 | SYMBOL ";" -> G.NSemicolon loc
582 | SYMBOL "." -> G.NDot loc
585 punctuation_tactical:
587 [ SYMBOL "[" -> G.Branch loc
588 | SYMBOL "|" -> G.Shift loc
589 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
590 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
591 | SYMBOL "]" -> G.Merge loc
592 | SYMBOL ";" -> G.Semicolon loc
593 | SYMBOL "." -> G.Dot loc
596 non_punctuation_tactical:
598 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
599 | IDENT "unfocus" -> G.Unfocus loc
600 | IDENT "skip" -> G.Skip loc
604 [ [ IDENT "ndefinition" ] -> `Definition
605 | [ IDENT "nfact" ] -> `Fact
606 | [ IDENT "nlemma" ] -> `Lemma
607 | [ IDENT "nremark" ] -> `Remark
608 | [ IDENT "ntheorem" ] -> `Theorem
612 [ [ IDENT "definition" ] -> `Definition
613 | [ IDENT "fact" ] -> `Fact
614 | [ IDENT "lemma" ] -> `Lemma
615 | [ IDENT "remark" ] -> `Remark
616 | [ IDENT "theorem" ] -> `Theorem
620 [ attr = theorem_flavour -> attr
621 | [ IDENT "axiom" ] -> `Axiom
622 | [ IDENT "variant" ] -> `Variant
627 params = LIST0 protected_binder_vars;
628 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
629 fst_constructors = LIST0 constructor SEP SYMBOL "|";
632 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
633 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
634 (name, true, typ, constructors) ] SEP "with" -> types
638 (fun (names, typ) acc ->
639 (List.map (fun name -> (name, typ)) names) @ acc)
642 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
643 let tl_ind_types = match tl with None -> [] | Some types -> types in
644 let ind_types = fst_ind_type :: tl_ind_types in
650 params = LIST0 protected_binder_vars;
651 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
655 SYMBOL ":" -> false,0
656 | SYMBOL ":"; SYMBOL ">" -> true,0
657 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
660 let b,n = coercion in
662 ] SEP SYMBOL ";"; SYMBOL "}" ->
665 (fun (names, typ) acc ->
666 (List.map (fun name -> (name, typ)) names) @ acc)
669 (params,name,typ,fields)
673 [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
674 | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
679 [ [ IDENT "check" ]; t = term ->
681 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
682 G.Eval (loc, kind, t)
683 | IDENT "inline"; suri = QSTRING; params = inline_params ->
684 G.Inline (loc, suri, params)
685 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
686 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
687 | IDENT "auto"; params = auto_params ->
688 G.AutoInteractive (loc,params)
689 | [ IDENT "whelp"; "match" ] ; t = term ->
691 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
693 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
695 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
697 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
702 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
703 let alpha = "[a-zA-Z]" in
704 let num = "[0-9]+" in
705 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
706 let decoration = "\\'" in
707 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
708 let rex = Str.regexp ("^"^ident^"$") in
709 if Str.string_match rex id 0 then
710 if (try ignore (UriManager.uri_of_string uri); true
711 with UriManager.IllFormedUri _ -> false) ||
712 (try ignore (NReference.reference_of_string uri); true
713 with NReference.IllFormedReference _ -> false)
715 L.Ident_alias (id, uri)
718 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
720 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
721 Printf.sprintf "Not a valid identifier: %s" id)))
722 | IDENT "symbol"; symbol = QSTRING;
723 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
724 SYMBOL "="; dsc = QSTRING ->
726 match instance with Some i -> i | None -> 0
728 L.Symbol_alias (symbol, instance, dsc)
730 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
731 SYMBOL "="; dsc = QSTRING ->
733 match instance with Some i -> i | None -> 0
735 L.Number_alias (instance, dsc)
739 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
741 N.IdentArg (List.length l, id)
745 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
746 | IDENT "right"; IDENT "associative" -> Gramext.RightA
747 | IDENT "non"; IDENT "associative" -> Gramext.NonA
751 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
754 [ dir = OPT direction; s = QSTRING;
755 assoc = OPT associativity; prec = precedence;
758 [ blob = UNPARSED_AST ->
759 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
760 (CicNotationParser.parse_level2_ast
761 (Ulexing.from_utf8_string blob))
762 | blob = UNPARSED_META ->
763 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
764 (CicNotationParser.parse_level2_meta
765 (Ulexing.from_utf8_string blob))
769 | None -> default_associativity
770 | Some assoc -> assoc
773 add_raw_attribute ~text:s
774 (CicNotationParser.parse_level1_pattern prec
775 (Ulexing.from_utf8_string s))
777 (dir, p1, assoc, prec, p2)
781 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
782 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
783 | IMPLICIT -> N.ImplicitPattern
784 | id = IDENT -> N.VarPattern id
785 | LPAREN; terms = LIST1 SELF; RPAREN ->
789 | terms -> N.ApplPattern terms)
793 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
799 IDENT "include" ; path = QSTRING ->
800 loc,path,true,L.WithPreferences
801 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
802 loc,path,false,L.WithPreferences
803 | IDENT "include'" ; path = QSTRING ->
804 loc,path,true,L.WithoutPreferences
807 grafite_ncommand: [ [
808 IDENT "nqed" -> G.NQed loc
809 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
810 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
811 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
812 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
814 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
815 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
816 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
817 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
818 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
819 paramspec = OPT inverter_param_list ;
820 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
821 G.NInverter (loc,name,indty,paramspec,outsort)
822 | NLETCOREC ; defs = let_defs ->
823 nmk_rec_corec `CoInductive defs loc
824 | NLETREC ; defs = let_defs ->
825 nmk_rec_corec `Inductive defs loc
826 | IDENT "ninductive"; spec = inductive_spec ->
827 let (params, ind_types) = spec in
828 G.NObj (loc, N.Inductive (params, ind_types))
829 | IDENT "ncoinductive"; spec = inductive_spec ->
830 let (params, ind_types) = spec in
831 let ind_types = (* set inductive flags to false (coinductive) *)
832 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
835 G.NObj (loc, N.Inductive (params, ind_types))
836 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
837 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
839 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
840 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
841 | _ -> raise (Failure "only a Type[…] sort can be constrained")
845 G.NUnivConstraint (loc,u1,u2)
846 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
847 G.UnificationHint (loc, t, n)
848 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
849 SYMBOL <:unicode<def>>; t = term; "on";
850 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
851 "to"; target = term ->
852 G.NCoercion(loc,name,t,ty,(id,source),target)
853 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
854 G.NObj (loc, N.Record (params,name,ty,fields))
855 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
856 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
857 G.NCopy (loc,s,NUri.uri_of_string u,
858 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
862 IDENT "set"; n = QSTRING; v = QSTRING ->
864 | IDENT "drop" -> G.Drop loc
865 | IDENT "print"; s = IDENT -> G.Print (loc,s)
866 | IDENT "qed" -> G.Qed loc
867 | IDENT "variant" ; name = IDENT; SYMBOL ":";
868 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
871 (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
872 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
873 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
874 G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
875 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
878 N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
879 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
880 G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
881 | LETCOREC ; defs = let_defs ->
882 mk_rec_corec `CoInductive defs loc
883 | LETREC ; defs = let_defs ->
884 mk_rec_corec `Inductive defs loc
885 | IDENT "inductive"; spec = inductive_spec ->
886 let (params, ind_types) = spec in
887 G.Obj (loc, N.Inductive (params, ind_types))
888 | IDENT "coinductive"; spec = inductive_spec ->
889 let (params, ind_types) = spec in
890 let ind_types = (* set inductive flags to false (coinductive) *)
891 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
894 G.Obj (loc, N.Inductive (params, ind_types))
896 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
897 arity = OPT int ; saturations = OPT int;
898 composites = OPT (IDENT "nocomposites") ->
899 let arity = match arity with None -> 0 | Some x -> x in
900 let saturations = match saturations with None -> 0 | Some x -> x in
901 let composites = match composites with None -> true | Some _ -> false in
903 (loc, t, composites, arity, saturations)
904 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
905 G.PreferCoercion (loc, t)
906 | IDENT "pump" ; steps = int ->
908 | IDENT "inverter"; name = IDENT; IDENT "for";
909 indty = tactic_term; paramspec = inverter_param_list ->
911 (loc, name, indty, paramspec)
912 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
913 G.Obj (loc, N.Record (params,name,ty,fields))
914 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
915 let uris = List.map UriManager.uri_of_string uris in
916 G.Default (loc,what,uris)
917 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
918 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
919 refl = tactic_term -> refl ] ;
920 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
921 sym = tactic_term -> sym ] ;
922 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
923 trans = tactic_term -> trans ] ;
925 G.Relation (loc,id,a,aeq,refl,sym,trans)
928 IDENT "alias" ; spec = alias_spec ->
930 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
931 L.Notation (loc, dir, l1, assoc, prec, l2)
932 | IDENT "interpretation"; id = QSTRING;
933 (symbol, args, l3) = interpretation ->
934 L.Interpretation (loc, id, (symbol, args), l3)
937 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
938 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
939 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
940 G.Tactic (loc, Some tac, punct)
941 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
942 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
943 G.NTactic (loc, [tac; npunct_of_punct punct])
944 | tac = ntactic; punct = punctuation_tactical ->
945 G.NTactic (loc, [tac; npunct_of_punct punct])
946 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
947 G.NTactic (loc, [punct])
948 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
949 G.NonPunctuationTactical (loc, tac, punct)
950 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
951 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
952 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
953 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
954 punct = punctuation_tactical ->
955 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
956 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
957 | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
961 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
969 fun ?(never_include=false) ~include_paths status ->
970 let stm = G.Executable (loc, ex) in
971 !grafite_callback stm;
974 fun ?(never_include=false) ~include_paths status ->
975 let stm = G.Comment (loc, com) in
976 !grafite_callback stm;
978 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
979 fun ?(never_include=false) ~include_paths status ->
980 let _root, buri, fullpath, _rrelpath =
981 Librarian.baseuri_of_script ~include_paths fname in
982 if never_include then raise (NoInclusionPerformed fullpath)
987 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
988 !grafite_callback stm;
990 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
993 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
997 | scom = lexicon_command ; SYMBOL "." ->
998 fun ?(never_include=false) ~include_paths status ->
999 !lexicon_callback scom;
1000 let status = LE.eval_command status scom in
1002 | EOI -> raise End_of_file
1009 let _ = initialize_parser () ;;
1011 let exc_located_wrapper f =
1015 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1016 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1017 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1018 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1020 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1021 | Stdpp.Exc_located (floc, exn) ->
1023 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1025 let parse_statement lexbuf =
1027 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1029 let statement () = Obj.magic !grafite_parser.statement
1031 let history = ref [] ;;
1034 LexiconSync.push ();
1035 history := !grafite_parser :: !history;
1036 grafite_parser := initial_parser ();
1037 initialize_parser ()
1043 | [] -> assert false
1045 grafite_parser := gp;
1049 (* vim:set foldmethod=marker: *)