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/
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 npunct_of_punct = function
105 | G.Branch loc -> G.NBranch loc
106 | G.Shift loc -> G.NShift loc
107 | G.Pos (loc, i) -> G.NPos (loc, i)
108 | G.Wildcard loc -> G.NWildcard loc
109 | G.Merge loc -> G.NMerge loc
110 | G.Semicolon loc -> G.NSemicolon loc
111 | G.Dot loc -> G.NDot loc
113 let nnon_punct_of_punct = function
114 | G.Skip loc -> G.NSkip loc
115 | G.Unfocus loc -> G.NUnfocus loc
116 | G.Focus (loc,l) -> G.NFocus (loc,l)
118 let npunct_of_punct = function
119 | G.Branch loc -> G.NBranch loc
120 | G.Shift loc -> G.NShift loc
121 | G.Pos (loc, i) -> G.NPos (loc, i)
122 | G.Wildcard loc -> G.NWildcard loc
123 | G.Merge loc -> G.NMerge loc
124 | G.Semicolon loc -> G.NSemicolon loc
125 | G.Dot loc -> G.NDot loc
129 | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p])
133 type by_continuation =
135 | BYC_weproved of N.term * string option * N.term option
136 | BYC_letsuchthat of string * N.term * string * N.term
137 | BYC_wehaveand of string * N.term * string * N.term
139 let initialize_parser () =
140 (* {{{ parser initialization *)
141 let term = !grafite_parser.term in
142 let statement = !grafite_parser.statement in
143 let let_defs = CicNotationParser.let_defs () in
144 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
146 GLOBAL: term statement;
147 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
148 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
151 | id = IDENT -> Some id ]
153 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
154 ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
156 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
159 [ IDENT "normalize" -> `Normalize
160 | IDENT "simplify" -> `Simpl
161 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
162 | IDENT "whd" -> `Whd ]
165 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
166 let delta = match delta with None -> true | _ -> false in
168 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
169 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
170 let delta = match delta with None -> true | _ -> false in
173 sequent_pattern_spec: [
177 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
178 (id,match path with Some p -> p | None -> N.UserInput) ];
179 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
181 match goal_path, hyp_paths with
182 None, [] -> Some N.UserInput
184 | Some goal_path, _ -> Some goal_path
193 [ "match" ; wanted = tactic_term ;
194 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
196 | sps = sequent_pattern_spec ->
199 let wanted,hyp_paths,goal_path =
200 match wanted_and_sps with
201 wanted,None -> wanted, [], Some N.UserInput
202 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
204 wanted, hyp_paths, goal_path ] ->
206 None -> None,[],Some N.UserInput
209 inverter_param_list: [
210 [ params = tactic_term ->
211 let deannotate = function
212 | N.AttributedTerm (_,t) | t -> t
213 in match deannotate params with
214 | N.Implicit _ -> [false]
215 | N.UserInput -> [true]
217 List.map (fun x -> match deannotate x with
218 | N.Implicit _ -> false
219 | N.UserInput -> true
220 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
221 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ]
224 [ SYMBOL ">" -> `LeftToRight
225 | SYMBOL "<" -> `RightToLeft ]
227 int: [ [ num = NUMBER -> int_of_string num ] ];
229 [ idents = OPT ident_list0 ->
230 match idents with None -> [] | Some idents -> idents
234 [ OPT [ IDENT "names" ];
235 num = OPT [ num = int -> num ];
236 idents = intros_names ->
240 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
242 [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
243 | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
247 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
248 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
249 SYMBOL <:unicode<def>> ; bo = tactic_term ->
251 SYMBOL <:unicode<vdash>>;
252 concl = tactic_term -> (List.rev hyps,concl) ] ->
253 G.NTactic(loc,[G.NAssert (loc, seqs)])
254 | IDENT "nauto"; params = auto_params ->
255 G.NTactic(loc,[G.NAuto (loc, params)])
256 | SYMBOL "/"; num = OPT NUMBER ;
257 params = nauto_params; SYMBOL "/" ;
258 just = OPT [ IDENT "by"; by =
259 [ univ = tactic_term_list1 -> `Univ univ
260 | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
261 | SYMBOL "_" -> `Trace ] -> by ] ->
262 let depth = match num with Some n -> n | None -> "1" in
266 [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
267 | Some (`Univ univ) ->
269 [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
272 [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
275 G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
276 | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
277 | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
278 | IDENT "screenshot"; fname = QSTRING ->
279 G.NMacro(loc,G.Screenshot (loc, fname))
280 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
281 G.NTactic(loc,[G.NCases (loc, what, where)])
282 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
283 G.NTactic(loc,[G.NChange (loc, what, with_what)])
284 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
285 G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
286 | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
287 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
288 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
289 | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
290 exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
291 -> let exclude' = match exclude with None -> [] | Some l -> l in
292 G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
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)
520 | IDENT "fast_paramod"
534 i = auto_fixed_param -> i,""
535 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
536 string_of_int v | v = IDENT -> v ] -> i,v ];
537 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
538 (* (match tl with Some l -> l | None -> []), *)
545 i = auto_fixed_param -> i,""
546 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
547 string_of_int v | v = IDENT -> v ] -> i,v ] ->
554 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
555 | flavour = inline_flavour -> G.IPAs flavour
556 | IDENT "coercions" -> G.IPCoercions
557 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
558 | IDENT "procedural" -> G.IPProcedural
559 | IDENT "nodefaults" -> G.IPNoDefaults
560 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
561 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
562 | IDENT "comments" -> G.IPComments
563 | IDENT "cr" -> G.IPCR
568 [ 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)
569 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
570 "done" -> BYC_weproved (ty,None,t1)
572 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
573 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
574 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
575 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
576 BYC_wehaveand (id1,t1,id2,t2)
579 rewriting_step_continuation : [
586 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
589 | G.Seq (_, l) -> l @ [ t2 ]
595 [ tac = SELF; SYMBOL ";";
596 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
597 (G.Then (loc, tac, tacs))
600 [ IDENT "do"; count = int; tac = SELF ->
601 G.Do (loc, count, tac)
602 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
606 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
608 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
610 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
612 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
613 | LPAREN; tac = SELF; RPAREN -> tac
614 | tac = tactic -> tac
617 npunctuation_tactical:
619 [ SYMBOL "[" -> G.NBranch loc
620 | SYMBOL "|" -> G.NShift loc
621 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
622 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
623 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
624 | SYMBOL "]" -> G.NMerge loc
625 | SYMBOL ";" -> G.NSemicolon loc
626 | SYMBOL "." -> G.NDot loc
629 punctuation_tactical:
631 [ SYMBOL "[" -> G.Branch loc
632 | SYMBOL "|" -> G.Shift loc
633 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
634 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
635 | SYMBOL "]" -> G.Merge loc
636 | SYMBOL ";" -> G.Semicolon loc
637 | SYMBOL "." -> G.Dot loc
640 non_punctuation_tactical:
642 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
643 | IDENT "unfocus" -> G.Unfocus loc
644 | IDENT "skip" -> G.Skip loc
648 [ [ IDENT "ndefinition" ] -> `Definition
649 | [ IDENT "nfact" ] -> `Fact
650 | [ IDENT "nlemma" ] -> `Lemma
651 | [ IDENT "nremark" ] -> `Remark
652 | [ IDENT "ntheorem" ] -> `Theorem
656 [ [ IDENT "definition" ] -> `Definition
657 | [ IDENT "fact" ] -> `Fact
658 | [ IDENT "lemma" ] -> `Lemma
659 | [ IDENT "remark" ] -> `Remark
660 | [ IDENT "theorem" ] -> `Theorem
664 [ attr = theorem_flavour -> attr
665 | [ IDENT "axiom" ] -> `Axiom
666 | [ IDENT "variant" ] -> `Variant
671 params = LIST0 protected_binder_vars;
672 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
673 fst_constructors = LIST0 constructor SEP SYMBOL "|";
676 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
677 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
678 (name, true, typ, constructors) ] SEP "with" -> types
682 (fun (names, typ) acc ->
683 (List.map (fun name -> (name, typ)) names) @ acc)
686 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
687 let tl_ind_types = match tl with None -> [] | Some types -> types in
688 let ind_types = fst_ind_type :: tl_ind_types in
694 params = LIST0 protected_binder_vars;
695 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
699 SYMBOL ":" -> false,0
700 | SYMBOL ":"; SYMBOL ">" -> true,0
701 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
704 let b,n = coercion in
706 ] SEP SYMBOL ";"; SYMBOL "}" ->
709 (fun (names, typ) acc ->
710 (List.map (fun name -> (name, typ)) names) @ acc)
713 (params,name,typ,fields)
717 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
718 let alpha = "[a-zA-Z]" in
719 let num = "[0-9]+" in
720 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
721 let decoration = "\\'" in
722 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
723 let rex = Str.regexp ("^"^ident^"$") in
724 if Str.string_match rex id 0 then
725 if (try ignore (UriManager.uri_of_string uri); true
726 with UriManager.IllFormedUri _ -> false) ||
727 (try ignore (NReference.reference_of_string uri); true
728 with NReference.IllFormedReference _ -> false)
730 L.Ident_alias (id, uri)
733 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
735 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
736 Printf.sprintf "Not a valid identifier: %s" id)))
737 | IDENT "symbol"; symbol = QSTRING;
738 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
739 SYMBOL "="; dsc = QSTRING ->
741 match instance with Some i -> i | None -> 0
743 L.Symbol_alias (symbol, instance, dsc)
745 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
746 SYMBOL "="; dsc = QSTRING ->
748 match instance with Some i -> i | None -> 0
750 L.Number_alias (instance, dsc)
754 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
756 N.IdentArg (List.length l, id)
760 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
761 | IDENT "right"; IDENT "associative" -> Gramext.RightA
762 | IDENT "non"; IDENT "associative" -> Gramext.NonA
766 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
769 [ dir = OPT direction; s = QSTRING;
770 assoc = OPT associativity; prec = precedence;
773 [ blob = UNPARSED_AST ->
774 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
775 (CicNotationParser.parse_level2_ast
776 (Ulexing.from_utf8_string blob))
777 | blob = UNPARSED_META ->
778 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
779 (CicNotationParser.parse_level2_meta
780 (Ulexing.from_utf8_string blob))
784 | None -> default_associativity
785 | Some assoc -> assoc
788 add_raw_attribute ~text:s
789 (CicNotationParser.parse_level1_pattern prec
790 (Ulexing.from_utf8_string s))
792 (dir, p1, assoc, prec, p2)
796 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
797 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
798 | IMPLICIT -> N.ImplicitPattern
799 | id = IDENT -> N.VarPattern id
800 | LPAREN; terms = LIST1 SELF; RPAREN ->
804 | terms -> N.ApplPattern terms)
808 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
814 IDENT "include" ; path = QSTRING ->
815 loc,path,true,L.WithPreferences
816 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
817 loc,path,false,L.WithPreferences
818 | IDENT "include'" ; path = QSTRING ->
819 loc,path,true,L.WithoutPreferences
822 grafite_ncommand: [ [
823 IDENT "nqed" -> G.NQed loc
824 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
825 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
826 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
827 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
829 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
830 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
831 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
832 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
833 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
834 paramspec = OPT inverter_param_list ;
835 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
836 G.NInverter (loc,name,indty,paramspec,outsort)
837 | NLETCOREC ; defs = let_defs ->
838 nmk_rec_corec `CoInductive defs loc
839 | NLETREC ; defs = let_defs ->
840 nmk_rec_corec `Inductive defs loc
841 | IDENT "ninductive"; spec = inductive_spec ->
842 let (params, ind_types) = spec in
843 G.NObj (loc, N.Inductive (params, ind_types))
844 | IDENT "ncoinductive"; spec = inductive_spec ->
845 let (params, ind_types) = spec in
846 let ind_types = (* set inductive flags to false (coinductive) *)
847 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
850 G.NObj (loc, N.Inductive (params, ind_types))
851 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
852 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
854 | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
855 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
856 | _ -> raise (Failure "only a Type[…] sort can be constrained")
860 G.NUnivConstraint (loc,u1,u2)
861 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
862 G.UnificationHint (loc, t, n)
863 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
864 SYMBOL <:unicode<def>>; t = term; "on";
865 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
866 "to"; target = term ->
867 G.NCoercion(loc,name,t,ty,(id,source),target)
868 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
869 G.NObj (loc, N.Record (params,name,ty,fields))
870 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
871 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
872 G.NCopy (loc,s,NUri.uri_of_string u,
873 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
877 IDENT "set"; n = QSTRING; v = QSTRING ->
879 | IDENT "drop" -> G.Drop loc
880 | IDENT "print"; s = IDENT -> G.Print (loc,s)
883 IDENT "alias" ; spec = alias_spec ->
885 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
886 L.Notation (loc, dir, l1, assoc, prec, l2)
887 | IDENT "interpretation"; id = QSTRING;
888 (symbol, args, l3) = interpretation ->
889 L.Interpretation (loc, id, (symbol, args), l3)
892 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
893 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
894 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
895 G.Tactic (loc, Some tac, punct)
896 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
897 | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ;
898 punct = punctuation_tactical ->
899 cons_ntac tac (npunct_of_punct punct)
901 | tac = ntactic; punct = punctuation_tactical ->
902 cons_ntac tac (npunct_of_punct punct)
904 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
905 G.NTactic (loc, [punct])
906 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
907 G.NonPunctuationTactical (loc, tac, punct)
908 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
909 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
910 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
911 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
912 punct = punctuation_tactical ->
913 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
917 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
925 fun ?(never_include=false) ~include_paths status ->
926 let stm = G.Executable (loc, ex) in
927 !grafite_callback stm;
930 fun ?(never_include=false) ~include_paths status ->
931 let stm = G.Comment (loc, com) in
932 !grafite_callback stm;
934 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
935 fun ?(never_include=false) ~include_paths status ->
936 let _root, buri, fullpath, _rrelpath =
937 Librarian.baseuri_of_script ~include_paths fname in
938 if never_include then raise (NoInclusionPerformed fullpath)
943 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
944 !grafite_callback stm;
946 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
949 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
953 | scom = lexicon_command ; SYMBOL "." ->
954 fun ?(never_include=false) ~include_paths status ->
955 !lexicon_callback scom;
956 let status = LE.eval_command status scom in
958 | EOI -> raise End_of_file
965 let _ = initialize_parser () ;;
967 let exc_located_wrapper f =
971 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
972 | Stdpp.Exc_located (floc, Stream.Error msg) ->
973 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
974 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
976 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
977 | Stdpp.Exc_located (floc, exn) ->
979 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
981 let parse_statement lexbuf =
983 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
985 let statement () = Obj.magic !grafite_parser.statement
987 let history = ref [] ;;
991 history := !grafite_parser :: !history;
992 grafite_parser := initial_parser ();
1001 grafite_parser := gp;
1005 (* vim:set foldmethod=marker: *)