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 ] ];
158 ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
160 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
163 [ IDENT "normalize" -> `Normalize
164 | IDENT "simplify" -> `Simpl
165 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
166 | IDENT "whd" -> `Whd ]
169 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
170 let delta = match delta with None -> true | _ -> false in
172 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
173 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
174 let delta = match delta with None -> true | _ -> false in
177 sequent_pattern_spec: [
181 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
182 (id,match path with Some p -> p | None -> N.UserInput) ];
183 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
185 match goal_path, hyp_paths with
186 None, [] -> Some N.UserInput
188 | Some goal_path, _ -> Some goal_path
197 [ "match" ; wanted = tactic_term ;
198 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
200 | sps = sequent_pattern_spec ->
203 let wanted,hyp_paths,goal_path =
204 match wanted_and_sps with
205 wanted,None -> wanted, [], Some N.UserInput
206 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
208 wanted, hyp_paths, goal_path ] ->
210 None -> None,[],Some N.UserInput
213 inverter_param_list: [
214 [ params = tactic_term ->
215 let deannotate = function
216 | N.AttributedTerm (_,t) | t -> t
217 in match deannotate params with
218 | N.Implicit _ -> [false]
219 | N.UserInput -> [true]
221 List.map (fun x -> match deannotate x with
222 | N.Implicit _ -> false
223 | N.UserInput -> true
224 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
225 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
228 [ SYMBOL ">" -> `LeftToRight
229 | SYMBOL "<" -> `RightToLeft ]
231 int: [ [ num = NUMBER -> int_of_string num ] ];
233 [ idents = OPT ident_list0 ->
234 match idents with None -> [] | Some idents -> idents
238 [ OPT [ IDENT "names" ];
239 num = OPT [ num = int -> num ];
240 idents = intros_names ->
244 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
246 [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
247 | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
251 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
252 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
253 SYMBOL <:unicode<def>> ; bo = tactic_term ->
255 SYMBOL <:unicode<vdash>>;
256 concl = tactic_term -> (List.rev hyps,concl) ] ->
257 G.NTactic(loc,[G.NAssert (loc, seqs)])
258 | IDENT "nauto"; params = auto_params ->
259 G.NTactic(loc,[G.NAuto (loc, params)])
260 | SYMBOL "/"; num = OPT NUMBER ;
261 params = nauto_params; SYMBOL "/" ;
262 just = OPT [ IDENT "by"; by =
263 [ univ = tactic_term_list1 -> `Univ univ
264 | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
265 | SYMBOL "_" -> `Trace ] -> by ] ->
266 let depth = match num with Some n -> n | None -> "1" in
270 [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
271 | Some (`Univ univ) ->
273 [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
276 [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
279 G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
280 | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
281 | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
282 | IDENT "screenshot"; fname = QSTRING ->
283 G.NMacro(loc,G.Screenshot (loc, fname))
284 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
285 G.NTactic(loc,[G.NCases (loc, what, where)])
286 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
287 G.NTactic(loc,[G.NChange (loc, what, with_what)])
288 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
289 G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
290 | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
291 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
292 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
293 | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
294 exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
295 -> let exclude' = match exclude with None -> [] | Some l -> l in
296 G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
297 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
298 G.NTactic(loc,[G.NElim (loc, what, where)])
299 | IDENT "ngeneralize"; p=pattern_spec ->
300 G.NTactic(loc,[G.NGeneralize (loc, p)])
301 | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
302 G.NTactic(loc,[G.NInversion (loc, what, where)])
303 | IDENT "nlapply"; t = tactic_term -> G.NTactic(loc,[G.NLApply (loc, t)])
304 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
305 where = pattern_spec ->
306 G.NTactic(loc,[G.NLetIn (loc,where,t,name)])
307 | kind = nreduction_kind; p = pattern_spec ->
308 G.NTactic(loc,[G.NReduce (loc, kind, p)])
309 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
310 G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
311 | IDENT "ntry"; tac = SELF ->
312 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
313 G.NTactic(loc,[ G.NTry (loc,tac)])
314 | IDENT "nrepeat"; tac = SELF ->
315 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
316 G.NTactic(loc,[ G.NRepeat (loc,tac)])
317 | LPAREN; l = LIST1 SELF; RPAREN ->
320 (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
321 G.NTactic(loc,[G.NBlock (loc,l)])
322 | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
323 | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
324 | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
325 | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
326 | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
330 [ IDENT "absurd"; t = tactic_term ->
332 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
334 | IDENT "apply"; t = tactic_term ->
336 | IDENT "applyP"; t = tactic_term ->
338 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
339 G.ApplyS (loc, t, params)
340 | IDENT "assumption" ->
342 | IDENT "autobatch"; params = auto_params ->
343 G.AutoBatch (loc,params)
344 | IDENT "cases"; what = tactic_term;
345 pattern = OPT pattern_spec;
346 specs = intros_spec ->
347 let pattern = match pattern with
348 | None -> None, [], Some N.UserInput
349 | Some pattern -> pattern
351 G.Cases (loc, what, pattern, specs)
352 | IDENT "clear"; ids = LIST1 IDENT ->
354 | IDENT "clearbody"; id = IDENT ->
356 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
357 G.Change (loc, what, t)
358 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
359 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
360 let times = match times with None -> 1 | Some i -> i in
361 G.Compose (loc, t1, t2, times, specs)
362 | IDENT "constructor"; n = int ->
363 G.Constructor (loc, n)
364 | IDENT "contradiction" ->
366 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
367 G.Cut (loc, ident, t)
368 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
369 let idents = match idents with None -> [] | Some idents -> idents in
370 G.Decompose (loc, idents)
371 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
372 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
373 G.Destruct (loc, xts)
374 | IDENT "elim"; what = tactic_term; using = using;
375 pattern = OPT pattern_spec;
376 ispecs = intros_spec ->
377 let pattern = match pattern with
378 | None -> None, [], Some N.UserInput
379 | Some pattern -> pattern
381 G.Elim (loc, what, using, pattern, ispecs)
382 | IDENT "elimType"; what = tactic_term; using = using;
383 (num, idents) = intros_spec ->
384 G.ElimType (loc, what, using, (num, idents))
385 | IDENT "exact"; t = tactic_term ->
389 | IDENT "fail" -> G.Fail loc
390 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
393 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
394 ("the pattern cannot specify the term to replace, only its"
395 ^ " paths in the hypotheses and in the conclusion")))
397 G.Fold (loc, kind, t, p)
400 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
401 let idents = match idents with None -> [] | Some idents -> idents in
402 G.FwdSimpl (loc, hyp, idents)
403 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
404 G.Generalize (loc,p,id)
405 | IDENT "id" -> G.IdTac loc
406 | IDENT "intro"; ident = OPT IDENT ->
407 let idents = match ident with None -> [] | Some id -> [Some id] in
408 G.Intros (loc, (Some 1, idents))
409 | IDENT "intros"; specs = intros_spec ->
410 G.Intros (loc, specs)
411 | IDENT "inversion"; t = tactic_term ->
414 linear = OPT [ IDENT "linear" ];
415 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
417 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
418 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
419 let linear = match linear with None -> false | Some _ -> true in
420 let to_what = match to_what with None -> [] | Some to_what -> to_what in
421 G.LApply (loc, linear, depth, to_what, what, ident)
422 | IDENT "left" -> G.Left loc
423 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
424 G.LetIn (loc, t, where)
425 | kind = reduction_kind; p = pattern_spec ->
426 G.Reduce (loc, kind, p)
427 | IDENT "reflexivity" ->
429 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
430 G.Replace (loc, p, t)
431 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
432 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
436 (HExtlib.Localized (loc,
437 (CicNotationParser.Parse_error
438 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
440 let n = match xnames with None -> [] | Some names -> names in
441 G.Rewrite (loc, d, t, p, n)
448 | IDENT "symmetry" ->
450 | IDENT "transitivity"; t = tactic_term ->
451 G.Transitivity (loc, t)
452 (* Produzioni Aggiunte *)
453 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
454 G.Assume (loc, id, t)
455 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
456 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
457 t' = tactic_term -> t']->
458 G.Suppose (loc, t, id, t1)
459 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
460 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
461 id2 = IDENT ; RPAREN ->
462 G.ExistsElim (loc, `Auto (None,[]), id1, t1, id2, t2)
464 [ IDENT "using"; t=tactic_term -> `Term t
465 | params = auto_params -> `Auto params] ;
466 cont=by_continuation ->
468 BYC_done -> G.Bydone (loc, just)
469 | BYC_weproved (ty,id,t1) ->
470 G.By_just_we_proved(loc, just, ty, id, t1)
471 | BYC_letsuchthat (id1,t1,id2,t2) ->
472 G.ExistsElim (loc, just, id1, t1, id2, t2)
473 | BYC_wehaveand (id1,t1,id2,t2) ->
474 G.AndElim (loc, just, id1, t1, id2, t2))
475 | 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']->
476 G.We_need_to_prove (loc, t, id, t1)
477 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
478 G.We_proceed_by_cases_on (loc, t, t1)
479 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
480 G.We_proceed_by_induction_on (loc, t, t1)
481 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
482 G.Byinduction(loc, t, id)
483 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
484 G.Thesisbecomes(loc, t)
485 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
486 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
487 G.Case(loc,id,params)
488 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
490 termine = tactic_term;
494 [ IDENT "using"; t=tactic_term -> `Term t
495 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
496 | IDENT "proof" -> `Proof
497 | params = auto_params -> `Auto params];
498 cont = rewriting_step_continuation ->
499 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
500 | IDENT "obtain" ; name = IDENT;
501 termine = tactic_term;
505 [ IDENT "using"; t=tactic_term -> `Term t
506 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
507 | IDENT "proof" -> `Proof
508 | params = auto_params -> `Auto params];
509 cont = rewriting_step_continuation ->
510 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
514 [ IDENT "using"; t=tactic_term -> `Term t
515 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
516 | IDENT "proof" -> `Proof
517 | params = auto_params -> `Auto params];
518 cont = rewriting_step_continuation ->
519 G.RewritingStep(loc, None, t1, t2, cont)
523 [ IDENT "paramodulation"
525 | IDENT "fast_paramod"
540 i = auto_fixed_param -> i,""
541 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
542 string_of_int v | v = IDENT -> v ] -> i,v ];
543 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
544 (* (match tl with Some l -> l | None -> []), *)
551 i = auto_fixed_param -> i,""
552 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
553 string_of_int v | v = IDENT -> v ] -> i,v ] ->
560 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
561 | flavour = inline_flavour -> G.IPAs flavour
562 | IDENT "coercions" -> G.IPCoercions
563 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
564 | IDENT "procedural" -> G.IPProcedural
565 | IDENT "nodefaults" -> G.IPNoDefaults
566 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
567 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
568 | IDENT "comments" -> G.IPComments
569 | IDENT "cr" -> G.IPCR
574 [ 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)
575 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
576 "done" -> BYC_weproved (ty,None,t1)
578 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
579 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
580 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
581 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
582 BYC_wehaveand (id1,t1,id2,t2)
585 rewriting_step_continuation : [
592 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
595 | G.Seq (_, l) -> l @ [ t2 ]
601 [ tac = SELF; SYMBOL ";";
602 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
603 (G.Then (loc, tac, tacs))
606 [ IDENT "do"; count = int; tac = SELF ->
607 G.Do (loc, count, tac)
608 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
612 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
614 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
616 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
618 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
619 | LPAREN; tac = SELF; RPAREN -> tac
620 | tac = tactic -> tac
623 npunctuation_tactical:
625 [ SYMBOL "[" -> G.NBranch loc
626 | SYMBOL "|" -> G.NShift loc
627 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
628 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
629 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
630 | SYMBOL "]" -> G.NMerge loc
631 | SYMBOL ";" -> G.NSemicolon loc
632 | SYMBOL "." -> G.NDot loc
635 punctuation_tactical:
637 [ SYMBOL "[" -> G.Branch loc
638 | SYMBOL "|" -> G.Shift loc
639 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
640 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
641 | SYMBOL "]" -> G.Merge loc
642 | SYMBOL ";" -> G.Semicolon loc
643 | SYMBOL "." -> G.Dot loc
646 non_punctuation_tactical:
648 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
649 | IDENT "unfocus" -> G.Unfocus loc
650 | IDENT "skip" -> G.Skip loc
654 [ [ IDENT "ndefinition" ] -> `Definition
655 | [ IDENT "nfact" ] -> `Fact
656 | [ IDENT "nlemma" ] -> `Lemma
657 | [ IDENT "nremark" ] -> `Remark
658 | [ IDENT "ntheorem" ] -> `Theorem
662 [ [ IDENT "definition" ] -> `Definition
663 | [ IDENT "fact" ] -> `Fact
664 | [ IDENT "lemma" ] -> `Lemma
665 | [ IDENT "remark" ] -> `Remark
666 | [ IDENT "theorem" ] -> `Theorem
670 [ attr = theorem_flavour -> attr
671 | [ IDENT "axiom" ] -> `Axiom
672 | [ IDENT "variant" ] -> `Variant
677 params = LIST0 protected_binder_vars;
678 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
679 fst_constructors = LIST0 constructor SEP SYMBOL "|";
682 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
683 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
684 (name, true, typ, constructors) ] SEP "with" -> types
688 (fun (names, typ) acc ->
689 (List.map (fun name -> (name, typ)) names) @ acc)
692 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
693 let tl_ind_types = match tl with None -> [] | Some types -> types in
694 let ind_types = fst_ind_type :: tl_ind_types in
700 params = LIST0 protected_binder_vars;
701 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
705 SYMBOL ":" -> false,0
706 | SYMBOL ":"; SYMBOL ">" -> true,0
707 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
710 let b,n = coercion in
712 ] SEP SYMBOL ";"; SYMBOL "}" ->
715 (fun (names, typ) acc ->
716 (List.map (fun name -> (name, typ)) names) @ acc)
719 (params,name,typ,fields)
723 [ [ IDENT "check" ]; t = term ->
725 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
726 G.Eval (loc, kind, t)
727 | IDENT "inline"; suri = QSTRING; params = inline_params ->
728 G.Inline (loc, suri, params)
729 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
730 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
731 | IDENT "auto"; params = auto_params ->
732 G.AutoInteractive (loc,params)
733 | [ IDENT "whelp"; "match" ] ; t = term ->
735 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
737 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
739 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
741 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
746 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
747 let alpha = "[a-zA-Z]" in
748 let num = "[0-9]+" in
749 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
750 let decoration = "\\'" in
751 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
752 let rex = Str.regexp ("^"^ident^"$") in
753 if Str.string_match rex id 0 then
754 if (try ignore (UriManager.uri_of_string uri); true
755 with UriManager.IllFormedUri _ -> false) ||
756 (try ignore (NReference.reference_of_string uri); true
757 with NReference.IllFormedReference _ -> false)
759 L.Ident_alias (id, uri)
762 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
764 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
765 Printf.sprintf "Not a valid identifier: %s" id)))
766 | IDENT "symbol"; symbol = QSTRING;
767 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
768 SYMBOL "="; dsc = QSTRING ->
770 match instance with Some i -> i | None -> 0
772 L.Symbol_alias (symbol, instance, dsc)
774 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
775 SYMBOL "="; dsc = QSTRING ->
777 match instance with Some i -> i | None -> 0
779 L.Number_alias (instance, dsc)
783 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
785 N.IdentArg (List.length l, id)
789 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
790 | IDENT "right"; IDENT "associative" -> Gramext.RightA
791 | IDENT "non"; IDENT "associative" -> Gramext.NonA
795 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
798 [ dir = OPT direction; s = QSTRING;
799 assoc = OPT associativity; prec = precedence;
802 [ blob = UNPARSED_AST ->
803 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
804 (CicNotationParser.parse_level2_ast
805 (Ulexing.from_utf8_string blob))
806 | blob = UNPARSED_META ->
807 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
808 (CicNotationParser.parse_level2_meta
809 (Ulexing.from_utf8_string blob))
813 | None -> default_associativity
814 | Some assoc -> assoc
817 add_raw_attribute ~text:s
818 (CicNotationParser.parse_level1_pattern prec
819 (Ulexing.from_utf8_string s))
821 (dir, p1, assoc, prec, p2)
825 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
826 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
827 | IMPLICIT -> N.ImplicitPattern
828 | id = IDENT -> N.VarPattern id
829 | LPAREN; terms = LIST1 SELF; RPAREN ->
833 | terms -> N.ApplPattern terms)
837 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
843 IDENT "include" ; path = QSTRING ->
844 loc,path,true,L.WithPreferences
845 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
846 loc,path,false,L.WithPreferences
847 | IDENT "include'" ; path = QSTRING ->
848 loc,path,true,L.WithoutPreferences
851 grafite_ncommand: [ [
852 IDENT "nqed" -> G.NQed loc
853 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
854 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
855 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
856 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
858 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
859 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
860 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
861 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
862 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
863 paramspec = OPT inverter_param_list ;
864 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
865 G.NInverter (loc,name,indty,paramspec,outsort)
866 | NLETCOREC ; defs = let_defs ->
867 nmk_rec_corec `CoInductive defs loc
868 | NLETREC ; defs = let_defs ->
869 nmk_rec_corec `Inductive defs loc
870 | IDENT "ninductive"; spec = inductive_spec ->
871 let (params, ind_types) = spec in
872 G.NObj (loc, N.Inductive (params, ind_types))
873 | IDENT "ncoinductive"; spec = inductive_spec ->
874 let (params, ind_types) = spec in
875 let ind_types = (* set inductive flags to false (coinductive) *)
876 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
879 G.NObj (loc, N.Inductive (params, ind_types))
880 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
881 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
883 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
884 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
885 | _ -> raise (Failure "only a Type[…] sort can be constrained")
889 G.NUnivConstraint (loc,u1,u2)
890 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
891 G.UnificationHint (loc, t, n)
892 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
893 SYMBOL <:unicode<def>>; t = term; "on";
894 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
895 "to"; target = term ->
896 G.NCoercion(loc,name,t,ty,(id,source),target)
897 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
898 G.NObj (loc, N.Record (params,name,ty,fields))
899 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
900 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
901 G.NCopy (loc,s,NUri.uri_of_string u,
902 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
906 IDENT "set"; n = QSTRING; v = QSTRING ->
908 | IDENT "drop" -> G.Drop loc
909 | IDENT "print"; s = IDENT -> G.Print (loc,s)
910 | IDENT "qed" -> G.Qed loc
911 | IDENT "variant" ; name = IDENT; SYMBOL ":";
912 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
915 (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
916 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
917 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
918 G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
919 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
922 N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
923 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
924 G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
925 | LETCOREC ; defs = let_defs ->
926 mk_rec_corec `CoInductive defs loc
927 | LETREC ; defs = let_defs ->
928 mk_rec_corec `Inductive defs loc
929 | IDENT "inductive"; spec = inductive_spec ->
930 let (params, ind_types) = spec in
931 G.Obj (loc, N.Inductive (params, ind_types))
932 | IDENT "coinductive"; spec = inductive_spec ->
933 let (params, ind_types) = spec in
934 let ind_types = (* set inductive flags to false (coinductive) *)
935 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
938 G.Obj (loc, N.Inductive (params, ind_types))
940 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
941 arity = OPT int ; saturations = OPT int;
942 composites = OPT (IDENT "nocomposites") ->
943 let arity = match arity with None -> 0 | Some x -> x in
944 let saturations = match saturations with None -> 0 | Some x -> x in
945 let composites = match composites with None -> true | Some _ -> false in
947 (loc, t, composites, arity, saturations)
948 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
949 G.PreferCoercion (loc, t)
950 | IDENT "pump" ; steps = int ->
952 | IDENT "inverter"; name = IDENT; IDENT "for";
953 indty = tactic_term; paramspec = inverter_param_list ->
955 (loc, name, indty, paramspec)
956 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
957 G.Obj (loc, N.Record (params,name,ty,fields))
958 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
959 let uris = List.map UriManager.uri_of_string uris in
960 G.Default (loc,what,uris)
961 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
962 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
963 refl = tactic_term -> refl ] ;
964 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
965 sym = tactic_term -> sym ] ;
966 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
967 trans = tactic_term -> trans ] ;
969 G.Relation (loc,id,a,aeq,refl,sym,trans)
972 IDENT "alias" ; spec = alias_spec ->
974 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
975 L.Notation (loc, dir, l1, assoc, prec, l2)
976 | IDENT "interpretation"; id = QSTRING;
977 (symbol, args, l3) = interpretation ->
978 L.Interpretation (loc, id, (symbol, args), l3)
981 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
982 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
983 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
984 G.Tactic (loc, Some tac, punct)
985 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
986 | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ;
987 punct = punctuation_tactical ->
988 cons_ntac tac (npunct_of_punct punct)
990 | tac = ntactic; punct = punctuation_tactical ->
991 cons_ntac tac (npunct_of_punct punct)
993 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
994 G.NTactic (loc, [punct])
995 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
996 G.NonPunctuationTactical (loc, tac, punct)
997 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
998 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
999 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
1000 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
1001 punct = punctuation_tactical ->
1002 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
1003 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
1007 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
1014 [ ex = executable ->
1015 fun ?(never_include=false) ~include_paths status ->
1016 let stm = G.Executable (loc, ex) in
1017 !grafite_callback stm;
1020 fun ?(never_include=false) ~include_paths status ->
1021 let stm = G.Comment (loc, com) in
1022 !grafite_callback stm;
1024 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
1025 fun ?(never_include=false) ~include_paths status ->
1026 let _root, buri, fullpath, _rrelpath =
1027 Librarian.baseuri_of_script ~include_paths fname in
1028 if never_include then raise (NoInclusionPerformed fullpath)
1033 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
1034 !grafite_callback stm;
1036 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
1039 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
1043 | scom = lexicon_command ; SYMBOL "." ->
1044 fun ?(never_include=false) ~include_paths status ->
1045 !lexicon_callback scom;
1046 let status = LE.eval_command status scom in
1048 | EOI -> raise End_of_file
1055 let _ = initialize_parser () ;;
1057 let exc_located_wrapper f =
1061 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1062 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1063 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1064 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1066 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1067 | Stdpp.Exc_located (floc, exn) ->
1069 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1071 let parse_statement lexbuf =
1073 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1075 let statement () = Obj.magic !grafite_parser.statement
1077 let history = ref [] ;;
1080 LexiconSync.push ();
1081 history := !grafite_parser :: !history;
1082 grafite_parser := initial_parser ();
1083 initialize_parser ()
1089 | [] -> assert false
1091 grafite_parser := gp;
1095 (* vim:set foldmethod=marker: *)