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
133 | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p])
137 type by_continuation =
139 | BYC_weproved of N.term * string option * N.term option
140 | BYC_letsuchthat of string * N.term * string * N.term
141 | BYC_wehaveand of string * N.term * string * N.term
143 let initialize_parser () =
144 (* {{{ parser initialization *)
145 let term = !grafite_parser.term in
146 let statement = !grafite_parser.statement in
147 let let_defs = CicNotationParser.let_defs () in
148 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
150 GLOBAL: term statement;
151 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
152 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
155 | id = IDENT -> Some id ]
157 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
159 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
162 [ IDENT "normalize" -> `Normalize
163 | IDENT "simplify" -> `Simpl
164 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
165 | IDENT "whd" -> `Whd ]
168 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
169 let delta = match delta with None -> true | _ -> false in
171 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
172 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
173 let delta = match delta with None -> true | _ -> false in
176 sequent_pattern_spec: [
180 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
181 (id,match path with Some p -> p | None -> N.UserInput) ];
182 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
184 match goal_path, hyp_paths with
185 None, [] -> Some N.UserInput
187 | Some goal_path, _ -> Some goal_path
196 [ "match" ; wanted = tactic_term ;
197 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
199 | sps = sequent_pattern_spec ->
202 let wanted,hyp_paths,goal_path =
203 match wanted_and_sps with
204 wanted,None -> wanted, [], Some N.UserInput
205 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
207 wanted, hyp_paths, goal_path ] ->
209 None -> None,[],Some N.UserInput
212 inverter_param_list: [
213 [ params = tactic_term ->
214 let deannotate = function
215 | N.AttributedTerm (_,t) | t -> t
216 in match deannotate params with
217 | N.Implicit _ -> [false]
218 | N.UserInput -> [true]
220 List.map (fun x -> match deannotate x with
221 | N.Implicit _ -> false
222 | N.UserInput -> true
223 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
224 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
227 [ SYMBOL ">" -> `LeftToRight
228 | SYMBOL "<" -> `RightToLeft ]
230 int: [ [ num = NUMBER -> int_of_string num ] ];
232 [ idents = OPT ident_list0 ->
233 match idents with None -> [] | Some idents -> idents
237 [ OPT [ IDENT "names" ];
238 num = OPT [ num = int -> num ];
239 idents = intros_names ->
243 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
245 [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
246 | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
250 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
251 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
252 SYMBOL <:unicode<def>> ; bo = tactic_term ->
254 SYMBOL <:unicode<vdash>>;
255 concl = tactic_term -> (List.rev hyps,concl) ] ->
256 G.NTactic(loc,[G.NAssert (loc, seqs)])
257 | IDENT "nauto"; params = auto_params ->
258 G.NTactic(loc,[G.NAuto (loc, params)])
259 | SYMBOL "/"; num = OPT NUMBER ;
260 params = nauto_params; SYMBOL "/" ;
261 just = OPT [ IDENT "by"; by =
262 [ univ = tactic_term_list1 -> `Univ univ
263 | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
264 | SYMBOL "_" -> `Trace ] -> by ] ->
265 let depth = match num with Some n -> n | None -> "1" in
269 [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
270 | Some (`Univ univ) ->
272 [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
275 [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
278 G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
279 | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
280 | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
281 | IDENT "screenshot"; fname = QSTRING ->
282 G.NMacro(loc,G.Screenshot (loc, fname))
283 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
284 G.NTactic(loc,[G.NCases (loc, what, where)])
285 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
286 G.NTactic(loc,[G.NChange (loc, what, with_what)])
287 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
288 G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
289 | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
290 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
291 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
292 | IDENT "ndestruct" -> G.NTactic(loc,[G.NDestruct loc])
293 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
294 G.NTactic(loc,[G.NElim (loc, what, where)])
295 | IDENT "ngeneralize"; p=pattern_spec ->
296 G.NTactic(loc,[G.NGeneralize (loc, p)])
297 | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
298 G.NTactic(loc,[G.NInversion (loc, what, where)])
299 | IDENT "nlapply"; t = tactic_term -> G.NTactic(loc,[G.NLApply (loc, t)])
300 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
301 where = pattern_spec ->
302 G.NTactic(loc,[G.NLetIn (loc,where,t,name)])
303 | kind = nreduction_kind; p = pattern_spec ->
304 G.NTactic(loc,[G.NReduce (loc, kind, p)])
305 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
306 G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
307 | IDENT "ntry"; tac = SELF ->
308 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
309 G.NTactic(loc,[ G.NTry (loc,tac)])
310 | IDENT "nrepeat"; tac = SELF ->
311 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
312 G.NTactic(loc,[ G.NRepeat (loc,tac)])
313 | LPAREN; l = LIST1 SELF; RPAREN ->
316 (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
317 G.NTactic(loc,[G.NBlock (loc,l)])
318 | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
319 | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
320 | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
321 | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
322 | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
326 [ IDENT "absurd"; t = tactic_term ->
328 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
330 | IDENT "apply"; t = tactic_term ->
332 | IDENT "applyP"; t = tactic_term ->
334 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
335 G.ApplyS (loc, t, params)
336 | IDENT "assumption" ->
338 | IDENT "autobatch"; params = auto_params ->
339 G.AutoBatch (loc,params)
340 | IDENT "cases"; what = tactic_term;
341 pattern = OPT pattern_spec;
342 specs = intros_spec ->
343 let pattern = match pattern with
344 | None -> None, [], Some N.UserInput
345 | Some pattern -> pattern
347 G.Cases (loc, what, pattern, specs)
348 | IDENT "clear"; ids = LIST1 IDENT ->
350 | IDENT "clearbody"; id = IDENT ->
352 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
353 G.Change (loc, what, t)
354 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
355 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
356 let times = match times with None -> 1 | Some i -> i in
357 G.Compose (loc, t1, t2, times, specs)
358 | IDENT "constructor"; n = int ->
359 G.Constructor (loc, n)
360 | IDENT "contradiction" ->
362 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
363 G.Cut (loc, ident, t)
364 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
365 let idents = match idents with None -> [] | Some idents -> idents in
366 G.Decompose (loc, idents)
367 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
368 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
369 G.Destruct (loc, xts)
370 | IDENT "elim"; what = tactic_term; using = using;
371 pattern = OPT pattern_spec;
372 ispecs = intros_spec ->
373 let pattern = match pattern with
374 | None -> None, [], Some N.UserInput
375 | Some pattern -> pattern
377 G.Elim (loc, what, using, pattern, ispecs)
378 | IDENT "elimType"; what = tactic_term; using = using;
379 (num, idents) = intros_spec ->
380 G.ElimType (loc, what, using, (num, idents))
381 | IDENT "exact"; t = tactic_term ->
385 | IDENT "fail" -> G.Fail loc
386 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
389 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
390 ("the pattern cannot specify the term to replace, only its"
391 ^ " paths in the hypotheses and in the conclusion")))
393 G.Fold (loc, kind, t, p)
396 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
397 let idents = match idents with None -> [] | Some idents -> idents in
398 G.FwdSimpl (loc, hyp, idents)
399 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
400 G.Generalize (loc,p,id)
401 | IDENT "id" -> G.IdTac loc
402 | IDENT "intro"; ident = OPT IDENT ->
403 let idents = match ident with None -> [] | Some id -> [Some id] in
404 G.Intros (loc, (Some 1, idents))
405 | IDENT "intros"; specs = intros_spec ->
406 G.Intros (loc, specs)
407 | IDENT "inversion"; t = tactic_term ->
410 linear = OPT [ IDENT "linear" ];
411 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
413 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
414 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
415 let linear = match linear with None -> false | Some _ -> true in
416 let to_what = match to_what with None -> [] | Some to_what -> to_what in
417 G.LApply (loc, linear, depth, to_what, what, ident)
418 | IDENT "left" -> G.Left loc
419 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
420 G.LetIn (loc, t, where)
421 | kind = reduction_kind; p = pattern_spec ->
422 G.Reduce (loc, kind, p)
423 | IDENT "reflexivity" ->
425 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
426 G.Replace (loc, p, t)
427 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
428 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
432 (HExtlib.Localized (loc,
433 (CicNotationParser.Parse_error
434 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
436 let n = match xnames with None -> [] | Some names -> names in
437 G.Rewrite (loc, d, t, p, n)
444 | IDENT "symmetry" ->
446 | IDENT "transitivity"; t = tactic_term ->
447 G.Transitivity (loc, t)
448 (* Produzioni Aggiunte *)
449 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
450 G.Assume (loc, id, t)
451 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
452 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
453 t' = tactic_term -> t']->
454 G.Suppose (loc, t, id, t1)
455 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
456 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
457 id2 = IDENT ; RPAREN ->
458 G.ExistsElim (loc, `Auto (None,[]), id1, t1, id2, t2)
460 [ IDENT "using"; t=tactic_term -> `Term t
461 | params = auto_params -> `Auto params] ;
462 cont=by_continuation ->
464 BYC_done -> G.Bydone (loc, just)
465 | BYC_weproved (ty,id,t1) ->
466 G.By_just_we_proved(loc, just, ty, id, t1)
467 | BYC_letsuchthat (id1,t1,id2,t2) ->
468 G.ExistsElim (loc, just, id1, t1, id2, t2)
469 | BYC_wehaveand (id1,t1,id2,t2) ->
470 G.AndElim (loc, just, id1, t1, id2, t2))
471 | 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']->
472 G.We_need_to_prove (loc, t, id, t1)
473 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
474 G.We_proceed_by_cases_on (loc, t, t1)
475 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
476 G.We_proceed_by_induction_on (loc, t, t1)
477 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
478 G.Byinduction(loc, t, id)
479 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
480 G.Thesisbecomes(loc, t)
481 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
482 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
483 G.Case(loc,id,params)
484 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
486 termine = tactic_term;
490 [ IDENT "using"; t=tactic_term -> `Term t
491 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
492 | IDENT "proof" -> `Proof
493 | params = auto_params -> `Auto params];
494 cont = rewriting_step_continuation ->
495 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
496 | IDENT "obtain" ; name = IDENT;
497 termine = tactic_term;
501 [ IDENT "using"; t=tactic_term -> `Term t
502 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
503 | IDENT "proof" -> `Proof
504 | params = auto_params -> `Auto params];
505 cont = rewriting_step_continuation ->
506 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
510 [ IDENT "using"; t=tactic_term -> `Term t
511 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
512 | IDENT "proof" -> `Proof
513 | params = auto_params -> `Auto params];
514 cont = rewriting_step_continuation ->
515 G.RewritingStep(loc, None, t1, t2, cont)
519 [ IDENT "paramodulation"
521 | IDENT "fast_paramod"
536 i = auto_fixed_param -> i,""
537 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
538 string_of_int v | v = IDENT -> v ] -> i,v ];
539 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
540 (* (match tl with Some l -> l | None -> []), *)
547 i = auto_fixed_param -> i,""
548 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
549 string_of_int v | v = IDENT -> v ] -> i,v ] ->
556 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
557 | flavour = inline_flavour -> G.IPAs flavour
558 | IDENT "coercions" -> G.IPCoercions
559 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
560 | IDENT "procedural" -> G.IPProcedural
561 | IDENT "nodefaults" -> G.IPNoDefaults
562 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
563 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
564 | IDENT "comments" -> G.IPComments
565 | IDENT "cr" -> G.IPCR
570 [ 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)
571 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
572 "done" -> BYC_weproved (ty,None,t1)
574 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
575 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
576 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
577 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
578 BYC_wehaveand (id1,t1,id2,t2)
581 rewriting_step_continuation : [
588 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
591 | G.Seq (_, l) -> l @ [ t2 ]
597 [ tac = SELF; SYMBOL ";";
598 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
599 (G.Then (loc, tac, tacs))
602 [ IDENT "do"; count = int; tac = SELF ->
603 G.Do (loc, count, tac)
604 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
608 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
610 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
612 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
614 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
615 | LPAREN; tac = SELF; RPAREN -> tac
616 | tac = tactic -> tac
619 npunctuation_tactical:
621 [ SYMBOL "[" -> G.NBranch loc
622 | SYMBOL "|" -> G.NShift loc
623 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
624 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
625 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
626 | SYMBOL "]" -> G.NMerge loc
627 | SYMBOL ";" -> G.NSemicolon loc
628 | SYMBOL "." -> G.NDot loc
631 punctuation_tactical:
633 [ SYMBOL "[" -> G.Branch loc
634 | SYMBOL "|" -> G.Shift loc
635 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
636 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
637 | SYMBOL "]" -> G.Merge loc
638 | SYMBOL ";" -> G.Semicolon loc
639 | SYMBOL "." -> G.Dot loc
642 non_punctuation_tactical:
644 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
645 | IDENT "unfocus" -> G.Unfocus loc
646 | IDENT "skip" -> G.Skip loc
650 [ [ IDENT "ndefinition" ] -> `Definition
651 | [ IDENT "nfact" ] -> `Fact
652 | [ IDENT "nlemma" ] -> `Lemma
653 | [ IDENT "nremark" ] -> `Remark
654 | [ IDENT "ntheorem" ] -> `Theorem
658 [ [ IDENT "definition" ] -> `Definition
659 | [ IDENT "fact" ] -> `Fact
660 | [ IDENT "lemma" ] -> `Lemma
661 | [ IDENT "remark" ] -> `Remark
662 | [ IDENT "theorem" ] -> `Theorem
666 [ attr = theorem_flavour -> attr
667 | [ IDENT "axiom" ] -> `Axiom
668 | [ IDENT "variant" ] -> `Variant
673 params = LIST0 protected_binder_vars;
674 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
675 fst_constructors = LIST0 constructor SEP SYMBOL "|";
678 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
679 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
680 (name, true, typ, constructors) ] SEP "with" -> types
684 (fun (names, typ) acc ->
685 (List.map (fun name -> (name, typ)) names) @ acc)
688 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
689 let tl_ind_types = match tl with None -> [] | Some types -> types in
690 let ind_types = fst_ind_type :: tl_ind_types in
696 params = LIST0 protected_binder_vars;
697 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
701 SYMBOL ":" -> false,0
702 | SYMBOL ":"; SYMBOL ">" -> true,0
703 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
706 let b,n = coercion in
708 ] SEP SYMBOL ";"; SYMBOL "}" ->
711 (fun (names, typ) acc ->
712 (List.map (fun name -> (name, typ)) names) @ acc)
715 (params,name,typ,fields)
719 [ [ IDENT "check" ]; t = term ->
721 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
722 G.Eval (loc, kind, t)
723 | IDENT "inline"; suri = QSTRING; params = inline_params ->
724 G.Inline (loc, suri, params)
725 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
726 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
727 | IDENT "auto"; params = auto_params ->
728 G.AutoInteractive (loc,params)
729 | [ IDENT "whelp"; "match" ] ; t = term ->
731 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
733 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
735 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
737 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
742 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
743 let alpha = "[a-zA-Z]" in
744 let num = "[0-9]+" in
745 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
746 let decoration = "\\'" in
747 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
748 let rex = Str.regexp ("^"^ident^"$") in
749 if Str.string_match rex id 0 then
750 if (try ignore (UriManager.uri_of_string uri); true
751 with UriManager.IllFormedUri _ -> false) ||
752 (try ignore (NReference.reference_of_string uri); true
753 with NReference.IllFormedReference _ -> false)
755 L.Ident_alias (id, uri)
758 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
760 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
761 Printf.sprintf "Not a valid identifier: %s" id)))
762 | IDENT "symbol"; symbol = QSTRING;
763 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
764 SYMBOL "="; dsc = QSTRING ->
766 match instance with Some i -> i | None -> 0
768 L.Symbol_alias (symbol, instance, dsc)
770 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
771 SYMBOL "="; dsc = QSTRING ->
773 match instance with Some i -> i | None -> 0
775 L.Number_alias (instance, dsc)
779 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
781 N.IdentArg (List.length l, id)
785 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
786 | IDENT "right"; IDENT "associative" -> Gramext.RightA
787 | IDENT "non"; IDENT "associative" -> Gramext.NonA
791 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
794 [ dir = OPT direction; s = QSTRING;
795 assoc = OPT associativity; prec = precedence;
798 [ blob = UNPARSED_AST ->
799 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
800 (CicNotationParser.parse_level2_ast
801 (Ulexing.from_utf8_string blob))
802 | blob = UNPARSED_META ->
803 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
804 (CicNotationParser.parse_level2_meta
805 (Ulexing.from_utf8_string blob))
809 | None -> default_associativity
810 | Some assoc -> assoc
813 add_raw_attribute ~text:s
814 (CicNotationParser.parse_level1_pattern prec
815 (Ulexing.from_utf8_string s))
817 (dir, p1, assoc, prec, p2)
821 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
822 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
823 | IMPLICIT -> N.ImplicitPattern
824 | id = IDENT -> N.VarPattern id
825 | LPAREN; terms = LIST1 SELF; RPAREN ->
829 | terms -> N.ApplPattern terms)
833 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
839 IDENT "include" ; path = QSTRING ->
840 loc,path,true,L.WithPreferences
841 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
842 loc,path,false,L.WithPreferences
843 | IDENT "include'" ; path = QSTRING ->
844 loc,path,true,L.WithoutPreferences
847 grafite_ncommand: [ [
848 IDENT "nqed" -> G.NQed loc
849 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
850 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
851 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
852 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
854 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
855 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
856 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
857 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
858 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
859 paramspec = OPT inverter_param_list ;
860 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
861 G.NInverter (loc,name,indty,paramspec,outsort)
862 | NLETCOREC ; defs = let_defs ->
863 nmk_rec_corec `CoInductive defs loc
864 | NLETREC ; defs = let_defs ->
865 nmk_rec_corec `Inductive defs loc
866 | IDENT "ninductive"; spec = inductive_spec ->
867 let (params, ind_types) = spec in
868 G.NObj (loc, N.Inductive (params, ind_types))
869 | IDENT "ncoinductive"; spec = inductive_spec ->
870 let (params, ind_types) = spec in
871 let ind_types = (* set inductive flags to false (coinductive) *)
872 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
875 G.NObj (loc, N.Inductive (params, ind_types))
876 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
877 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
879 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
880 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
881 | _ -> raise (Failure "only a Type[…] sort can be constrained")
885 G.NUnivConstraint (loc,u1,u2)
886 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
887 G.UnificationHint (loc, t, n)
888 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
889 SYMBOL <:unicode<def>>; t = term; "on";
890 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
891 "to"; target = term ->
892 G.NCoercion(loc,name,t,ty,(id,source),target)
893 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
894 G.NObj (loc, N.Record (params,name,ty,fields))
895 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
896 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
897 G.NCopy (loc,s,NUri.uri_of_string u,
898 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
902 IDENT "set"; n = QSTRING; v = QSTRING ->
904 | IDENT "drop" -> G.Drop loc
905 | IDENT "print"; s = IDENT -> G.Print (loc,s)
906 | IDENT "qed" -> G.Qed loc
907 | IDENT "variant" ; name = IDENT; SYMBOL ":";
908 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
911 (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
912 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
913 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
914 G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
915 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
918 N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
919 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
920 G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
921 | LETCOREC ; defs = let_defs ->
922 mk_rec_corec `CoInductive defs loc
923 | LETREC ; defs = let_defs ->
924 mk_rec_corec `Inductive defs loc
925 | IDENT "inductive"; spec = inductive_spec ->
926 let (params, ind_types) = spec in
927 G.Obj (loc, N.Inductive (params, ind_types))
928 | IDENT "coinductive"; spec = inductive_spec ->
929 let (params, ind_types) = spec in
930 let ind_types = (* set inductive flags to false (coinductive) *)
931 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
934 G.Obj (loc, N.Inductive (params, ind_types))
936 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
937 arity = OPT int ; saturations = OPT int;
938 composites = OPT (IDENT "nocomposites") ->
939 let arity = match arity with None -> 0 | Some x -> x in
940 let saturations = match saturations with None -> 0 | Some x -> x in
941 let composites = match composites with None -> true | Some _ -> false in
943 (loc, t, composites, arity, saturations)
944 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
945 G.PreferCoercion (loc, t)
946 | IDENT "pump" ; steps = int ->
948 | IDENT "inverter"; name = IDENT; IDENT "for";
949 indty = tactic_term; paramspec = inverter_param_list ->
951 (loc, name, indty, paramspec)
952 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
953 G.Obj (loc, N.Record (params,name,ty,fields))
954 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
955 let uris = List.map UriManager.uri_of_string uris in
956 G.Default (loc,what,uris)
957 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
958 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
959 refl = tactic_term -> refl ] ;
960 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
961 sym = tactic_term -> sym ] ;
962 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
963 trans = tactic_term -> trans ] ;
965 G.Relation (loc,id,a,aeq,refl,sym,trans)
968 IDENT "alias" ; spec = alias_spec ->
970 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
971 L.Notation (loc, dir, l1, assoc, prec, l2)
972 | IDENT "interpretation"; id = QSTRING;
973 (symbol, args, l3) = interpretation ->
974 L.Interpretation (loc, id, (symbol, args), l3)
977 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
978 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
979 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
980 G.Tactic (loc, Some tac, punct)
981 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
982 | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ;
983 punct = punctuation_tactical ->
984 cons_ntac tac (npunct_of_punct punct)
986 | tac = ntactic; punct = punctuation_tactical ->
987 cons_ntac tac (npunct_of_punct punct)
989 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
990 G.NTactic (loc, [punct])
991 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
992 G.NonPunctuationTactical (loc, tac, punct)
993 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
994 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
995 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
996 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
997 punct = punctuation_tactical ->
998 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
999 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
1003 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
1010 [ ex = executable ->
1011 fun ?(never_include=false) ~include_paths status ->
1012 let stm = G.Executable (loc, ex) in
1013 !grafite_callback stm;
1016 fun ?(never_include=false) ~include_paths status ->
1017 let stm = G.Comment (loc, com) in
1018 !grafite_callback stm;
1020 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
1021 fun ?(never_include=false) ~include_paths status ->
1022 let _root, buri, fullpath, _rrelpath =
1023 Librarian.baseuri_of_script ~include_paths fname in
1024 if never_include then raise (NoInclusionPerformed fullpath)
1029 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
1030 !grafite_callback stm;
1032 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
1035 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
1039 | scom = lexicon_command ; SYMBOL "." ->
1040 fun ?(never_include=false) ~include_paths status ->
1041 !lexicon_callback scom;
1042 let status = LE.eval_command status scom in
1044 | EOI -> raise End_of_file
1051 let _ = initialize_parser () ;;
1053 let exc_located_wrapper f =
1057 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1058 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1059 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1060 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1062 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1063 | Stdpp.Exc_located (floc, exn) ->
1065 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1067 let parse_statement lexbuf =
1069 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1071 let statement () = Obj.magic !grafite_parser.statement
1073 let history = ref [] ;;
1076 LexiconSync.push ();
1077 history := !grafite_parser :: !history;
1078 grafite_parser := initial_parser ();
1079 initialize_parser ()
1085 | [] -> assert false
1087 grafite_parser := gp;
1091 (* vim:set foldmethod=marker: *)