1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module N = CicNotationPt
31 module LE = LexiconEngine
33 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
40 (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement
42 type 'status statement =
43 ?never_include:bool ->
44 (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
45 include_paths:string list -> (#LE.status as 'status) ->
46 'status * ast_statement localized_option
48 type 'status parser_status = {
50 term : N.term Grammar.Entry.e;
51 statement : #LE.status as 'status statement Grammar.Entry.e;
54 let grafite_callback = ref (fun _ -> ())
55 let set_grafite_callback cb = grafite_callback := cb
57 let lexicon_callback = ref (fun _ -> ())
58 let set_lexicon_callback cb = lexicon_callback := cb
60 let initial_parser () =
61 let grammar = CicNotationParser.level2_ast_grammar () in
62 let term = CicNotationParser.term () in
63 let statement = Grammar.Entry.create grammar "statement" in
64 { grammar = grammar; term = term; statement = statement }
67 let grafite_parser = ref (initial_parser ())
69 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
71 let default_associativity = Gramext.NonA
73 let mk_rec_corec ind_kind defs loc =
74 (* In case of mutual definitions here we produce just
75 the syntax tree for the first one. The others will be
76 generated from the completely specified term just before
77 insertion in the environment. We use the flavour
78 `MutualDefinition to rememer this. *)
81 | (params,(N.Ident (name, None), ty),_,_) :: _ ->
82 let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
85 (fun var ty -> N.Binder (`Pi,var,ty)
91 let body = N.Ident (name,None) in
93 if List.length defs = 1 then
98 (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
100 let nmk_rec_corec ind_kind defs loc =
101 let loc,t = mk_rec_corec ind_kind defs loc in
104 let mk_rec_corec ind_kind defs loc =
105 let loc,t = mk_rec_corec ind_kind defs loc in
108 let npunct_of_punct = function
109 | G.Branch loc -> G.NBranch loc
110 | G.Shift loc -> G.NShift loc
111 | G.Pos (loc, i) -> G.NPos (loc, i)
112 | G.Wildcard loc -> G.NWildcard loc
113 | G.Merge loc -> G.NMerge loc
114 | G.Semicolon loc -> G.NSemicolon loc
115 | G.Dot loc -> G.NDot loc
117 let nnon_punct_of_punct = function
118 | G.Skip loc -> G.NSkip loc
119 | G.Unfocus loc -> G.NUnfocus loc
120 | G.Focus (loc,l) -> G.NFocus (loc,l)
122 let npunct_of_punct = function
123 | G.Branch loc -> G.NBranch loc
124 | G.Shift loc -> G.NShift loc
125 | G.Pos (loc, i) -> G.NPos (loc, i)
126 | G.Wildcard loc -> G.NWildcard loc
127 | G.Merge loc -> G.NMerge loc
128 | G.Semicolon loc -> G.NSemicolon loc
129 | G.Dot loc -> G.NDot loc
132 type by_continuation =
134 | BYC_weproved of N.term * string option * N.term option
135 | BYC_letsuchthat of string * N.term * string * N.term
136 | BYC_wehaveand of string * N.term * string * N.term
138 let initialize_parser () =
139 (* {{{ parser initialization *)
140 let term = !grafite_parser.term in
141 let statement = !grafite_parser.statement in
142 let let_defs = CicNotationParser.let_defs () in
143 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
145 GLOBAL: term statement;
146 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
147 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
150 | id = IDENT -> Some id ]
152 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
154 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
157 [ IDENT "normalize" -> `Normalize
158 | IDENT "simplify" -> `Simpl
159 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
160 | IDENT "whd" -> `Whd ]
163 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
164 let delta = match delta with None -> true | _ -> false in
166 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
167 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
168 let delta = match delta with None -> true | _ -> false in
171 sequent_pattern_spec: [
175 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
176 (id,match path with Some p -> p | None -> N.UserInput) ];
177 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
179 match goal_path, hyp_paths with
180 None, [] -> Some N.UserInput
182 | Some goal_path, _ -> Some goal_path
191 [ "match" ; wanted = tactic_term ;
192 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
194 | sps = sequent_pattern_spec ->
197 let wanted,hyp_paths,goal_path =
198 match wanted_and_sps with
199 wanted,None -> wanted, [], Some N.UserInput
200 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
202 wanted, hyp_paths, goal_path ] ->
204 None -> None,[],Some N.UserInput
207 inverter_param_list: [
208 [ params = tactic_term ->
209 let deannotate = function
210 | N.AttributedTerm (_,t) | t -> t
211 in match deannotate params with
212 | N.Implicit _ -> [false]
213 | N.UserInput -> [true]
215 List.map (fun x -> match deannotate x with
216 | N.Implicit _ -> false
217 | N.UserInput -> true
218 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
219 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
222 [ SYMBOL ">" -> `LeftToRight
223 | SYMBOL "<" -> `RightToLeft ]
225 int: [ [ num = NUMBER -> int_of_string num ] ];
227 [ idents = OPT ident_list0 ->
228 match idents with None -> [] | Some idents -> idents
232 [ OPT [ IDENT "names" ];
233 num = OPT [ num = int -> num ];
234 idents = intros_names ->
238 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
240 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
241 | IDENT "napplyS"; t = tactic_term -> G.NSmartApply (loc, t)
245 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
246 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
247 SYMBOL <:unicode<def>> ; bo = tactic_term ->
249 SYMBOL <:unicode<vdash>>;
250 concl = tactic_term -> (List.rev hyps,concl) ] ->
251 G.NAssert (loc, seqs)
252 | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
253 | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ->
254 let depth = match num with Some n -> n | None -> "1" in
255 G.NAuto (loc, ([],["slir","";"depth",depth]))
256 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
257 G.NCases (loc, what, where)
258 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
259 G.NChange (loc, what, with_what)
260 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
262 (match num with None -> None | Some x -> Some (int_of_string x)),l)
263 | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
264 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
265 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
266 | IDENT "ndestruct" -> G.NDestruct loc
267 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
268 G.NElim (loc, what, where)
269 | IDENT "ngeneralize"; p=pattern_spec ->
270 G.NGeneralize (loc, p)
271 | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
272 G.NInversion (loc, what, where)
273 | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
274 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
275 where = pattern_spec ->
276 G.NLetIn (loc,where,t,name)
277 | kind = nreduction_kind; p = pattern_spec ->
278 G.NReduce (loc, kind, p)
279 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
280 G.NRewrite (loc, dir, what, where)
281 | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac)
282 | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
283 | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
284 | IDENT "nassumption" -> G.NAssumption loc
285 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
286 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
287 | SYMBOL "*" -> G.NCase1 (loc,"_")
288 | SYMBOL "*"; n=IDENT ->
293 [ IDENT "absurd"; t = tactic_term ->
295 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
297 | IDENT "apply"; t = tactic_term ->
299 | IDENT "applyP"; t = tactic_term ->
301 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
302 G.ApplyS (loc, t, params)
303 | IDENT "assumption" ->
305 | IDENT "autobatch"; params = auto_params ->
306 G.AutoBatch (loc,params)
307 | IDENT "cases"; what = tactic_term;
308 pattern = OPT pattern_spec;
309 specs = intros_spec ->
310 let pattern = match pattern with
311 | None -> None, [], Some N.UserInput
312 | Some pattern -> pattern
314 G.Cases (loc, what, pattern, specs)
315 | IDENT "clear"; ids = LIST1 IDENT ->
317 | IDENT "clearbody"; id = IDENT ->
319 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
320 G.Change (loc, what, t)
321 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
322 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
323 let times = match times with None -> 1 | Some i -> i in
324 G.Compose (loc, t1, t2, times, specs)
325 | IDENT "constructor"; n = int ->
326 G.Constructor (loc, n)
327 | IDENT "contradiction" ->
329 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
330 G.Cut (loc, ident, t)
331 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
332 let idents = match idents with None -> [] | Some idents -> idents in
333 G.Decompose (loc, idents)
334 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
335 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
336 G.Destruct (loc, xts)
337 | IDENT "elim"; what = tactic_term; using = using;
338 pattern = OPT pattern_spec;
339 ispecs = intros_spec ->
340 let pattern = match pattern with
341 | None -> None, [], Some N.UserInput
342 | Some pattern -> pattern
344 G.Elim (loc, what, using, pattern, ispecs)
345 | IDENT "elimType"; what = tactic_term; using = using;
346 (num, idents) = intros_spec ->
347 G.ElimType (loc, what, using, (num, idents))
348 | IDENT "exact"; t = tactic_term ->
352 | IDENT "fail" -> G.Fail loc
353 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
356 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
357 ("the pattern cannot specify the term to replace, only its"
358 ^ " paths in the hypotheses and in the conclusion")))
360 G.Fold (loc, kind, t, p)
363 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
364 let idents = match idents with None -> [] | Some idents -> idents in
365 G.FwdSimpl (loc, hyp, idents)
366 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
367 G.Generalize (loc,p,id)
368 | IDENT "id" -> G.IdTac loc
369 | IDENT "intro"; ident = OPT IDENT ->
370 let idents = match ident with None -> [] | Some id -> [Some id] in
371 G.Intros (loc, (Some 1, idents))
372 | IDENT "intros"; specs = intros_spec ->
373 G.Intros (loc, specs)
374 | IDENT "inversion"; t = tactic_term ->
377 linear = OPT [ IDENT "linear" ];
378 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
380 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
381 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
382 let linear = match linear with None -> false | Some _ -> true in
383 let to_what = match to_what with None -> [] | Some to_what -> to_what in
384 G.LApply (loc, linear, depth, to_what, what, ident)
385 | IDENT "left" -> G.Left loc
386 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
387 G.LetIn (loc, t, where)
388 | kind = reduction_kind; p = pattern_spec ->
389 G.Reduce (loc, kind, p)
390 | IDENT "reflexivity" ->
392 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
393 G.Replace (loc, p, t)
394 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
395 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
399 (HExtlib.Localized (loc,
400 (CicNotationParser.Parse_error
401 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
403 let n = match xnames with None -> [] | Some names -> names in
404 G.Rewrite (loc, d, t, p, n)
411 | IDENT "symmetry" ->
413 | IDENT "transitivity"; t = tactic_term ->
414 G.Transitivity (loc, t)
415 (* Produzioni Aggiunte *)
416 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
417 G.Assume (loc, id, t)
418 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
419 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
420 t' = tactic_term -> t']->
421 G.Suppose (loc, t, id, t1)
422 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
423 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
424 id2 = IDENT ; RPAREN ->
425 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
427 [ IDENT "using"; t=tactic_term -> `Term t
428 | params = auto_params -> `Auto params] ;
429 cont=by_continuation ->
431 BYC_done -> G.Bydone (loc, just)
432 | BYC_weproved (ty,id,t1) ->
433 G.By_just_we_proved(loc, just, ty, id, t1)
434 | BYC_letsuchthat (id1,t1,id2,t2) ->
435 G.ExistsElim (loc, just, id1, t1, id2, t2)
436 | BYC_wehaveand (id1,t1,id2,t2) ->
437 G.AndElim (loc, just, id1, t1, id2, t2))
438 | 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']->
439 G.We_need_to_prove (loc, t, id, t1)
440 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
441 G.We_proceed_by_cases_on (loc, t, t1)
442 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
443 G.We_proceed_by_induction_on (loc, t, t1)
444 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
445 G.Byinduction(loc, t, id)
446 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
447 G.Thesisbecomes(loc, t)
448 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
449 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
450 G.Case(loc,id,params)
451 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
453 termine = tactic_term;
457 [ IDENT "using"; t=tactic_term -> `Term t
458 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
459 | IDENT "proof" -> `Proof
460 | params = auto_params -> `Auto params];
461 cont = rewriting_step_continuation ->
462 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
463 | IDENT "obtain" ; name = IDENT;
464 termine = tactic_term;
468 [ IDENT "using"; t=tactic_term -> `Term t
469 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
470 | IDENT "proof" -> `Proof
471 | params = auto_params -> `Auto params];
472 cont = rewriting_step_continuation ->
473 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
477 [ IDENT "using"; t=tactic_term -> `Term t
478 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
479 | IDENT "proof" -> `Proof
480 | params = auto_params -> `Auto params];
481 cont = rewriting_step_continuation ->
482 G.RewritingStep(loc, None, t1, t2, cont)
486 [ IDENT "paramodulation"
488 | IDENT "fast_paramod"
503 i = auto_fixed_param -> i,""
504 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
505 string_of_int v | v = IDENT -> v ] -> i,v ];
506 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
507 (match tl with Some l -> l | None -> []),
513 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
514 | flavour = inline_flavour -> G.IPAs flavour
515 | IDENT "coercions" -> G.IPCoercions
516 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
517 | IDENT "procedural" -> G.IPProcedural
518 | IDENT "nodefaults" -> G.IPNoDefaults
519 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
520 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
521 | IDENT "comments" -> G.IPComments
522 | IDENT "cr" -> G.IPCR
527 [ 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)
528 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
529 "done" -> BYC_weproved (ty,None,t1)
531 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
532 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
533 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
534 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
535 BYC_wehaveand (id1,t1,id2,t2)
538 rewriting_step_continuation : [
545 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
548 | G.Seq (_, l) -> l @ [ t2 ]
554 [ tac = SELF; SYMBOL ";";
555 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
556 (G.Then (loc, tac, tacs))
559 [ IDENT "do"; count = int; tac = SELF ->
560 G.Do (loc, count, tac)
561 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
565 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
567 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
569 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
571 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
572 | LPAREN; tac = SELF; RPAREN -> tac
573 | tac = tactic -> tac
576 npunctuation_tactical:
578 [ SYMBOL "[" -> G.NBranch loc
579 | SYMBOL "|" -> G.NShift loc
580 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
581 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
582 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
583 | SYMBOL "]" -> G.NMerge loc
584 | SYMBOL ";" -> G.NSemicolon loc
585 | SYMBOL "." -> G.NDot loc
588 punctuation_tactical:
590 [ SYMBOL "[" -> G.Branch loc
591 | SYMBOL "|" -> G.Shift loc
592 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
593 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
594 | SYMBOL "]" -> G.Merge loc
595 | SYMBOL ";" -> G.Semicolon loc
596 | SYMBOL "." -> G.Dot loc
599 non_punctuation_tactical:
601 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
602 | IDENT "unfocus" -> G.Unfocus loc
603 | IDENT "skip" -> G.Skip loc
607 [ [ IDENT "ndefinition" ] -> `Definition
608 | [ IDENT "nfact" ] -> `Fact
609 | [ IDENT "nlemma" ] -> `Lemma
610 | [ IDENT "nremark" ] -> `Remark
611 | [ IDENT "ntheorem" ] -> `Theorem
615 [ [ IDENT "definition" ] -> `Definition
616 | [ IDENT "fact" ] -> `Fact
617 | [ IDENT "lemma" ] -> `Lemma
618 | [ IDENT "remark" ] -> `Remark
619 | [ IDENT "theorem" ] -> `Theorem
623 [ attr = theorem_flavour -> attr
624 | [ IDENT "axiom" ] -> `Axiom
625 | [ IDENT "variant" ] -> `Variant
630 params = LIST0 protected_binder_vars;
631 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
632 fst_constructors = LIST0 constructor SEP SYMBOL "|";
635 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
636 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
637 (name, true, typ, constructors) ] SEP "with" -> types
641 (fun (names, typ) acc ->
642 (List.map (fun name -> (name, typ)) names) @ acc)
645 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
646 let tl_ind_types = match tl with None -> [] | Some types -> types in
647 let ind_types = fst_ind_type :: tl_ind_types in
653 params = LIST0 protected_binder_vars;
654 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
658 SYMBOL ":" -> false,0
659 | SYMBOL ":"; SYMBOL ">" -> true,0
660 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
663 let b,n = coercion in
665 ] SEP SYMBOL ";"; SYMBOL "}" ->
668 (fun (names, typ) acc ->
669 (List.map (fun name -> (name, typ)) names) @ acc)
672 (params,name,typ,fields)
676 [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
677 | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
682 [ [ IDENT "check" ]; t = term ->
684 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
685 G.Eval (loc, kind, t)
686 | IDENT "inline"; suri = QSTRING; params = inline_params ->
687 G.Inline (loc, suri, params)
688 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
689 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
690 | IDENT "auto"; params = auto_params ->
691 G.AutoInteractive (loc,params)
692 | [ IDENT "whelp"; "match" ] ; t = term ->
694 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
696 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
698 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
700 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
705 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
706 let alpha = "[a-zA-Z]" in
707 let num = "[0-9]+" in
708 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
709 let decoration = "\\'" in
710 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
711 let rex = Str.regexp ("^"^ident^"$") in
712 if Str.string_match rex id 0 then
713 if (try ignore (UriManager.uri_of_string uri); true
714 with UriManager.IllFormedUri _ -> false) ||
715 (try ignore (NReference.reference_of_string uri); true
716 with NReference.IllFormedReference _ -> false)
718 L.Ident_alias (id, uri)
721 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
723 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
724 Printf.sprintf "Not a valid identifier: %s" id)))
725 | IDENT "symbol"; symbol = QSTRING;
726 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
727 SYMBOL "="; dsc = QSTRING ->
729 match instance with Some i -> i | None -> 0
731 L.Symbol_alias (symbol, instance, dsc)
733 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
734 SYMBOL "="; dsc = QSTRING ->
736 match instance with Some i -> i | None -> 0
738 L.Number_alias (instance, dsc)
742 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
744 N.IdentArg (List.length l, id)
748 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
749 | IDENT "right"; IDENT "associative" -> Gramext.RightA
750 | IDENT "non"; IDENT "associative" -> Gramext.NonA
754 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
757 [ dir = OPT direction; s = QSTRING;
758 assoc = OPT associativity; prec = precedence;
761 [ blob = UNPARSED_AST ->
762 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
763 (CicNotationParser.parse_level2_ast
764 (Ulexing.from_utf8_string blob))
765 | blob = UNPARSED_META ->
766 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
767 (CicNotationParser.parse_level2_meta
768 (Ulexing.from_utf8_string blob))
772 | None -> default_associativity
773 | Some assoc -> assoc
776 add_raw_attribute ~text:s
777 (CicNotationParser.parse_level1_pattern prec
778 (Ulexing.from_utf8_string s))
780 (dir, p1, assoc, prec, p2)
784 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
785 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
786 | IMPLICIT -> N.ImplicitPattern
787 | id = IDENT -> N.VarPattern id
788 | LPAREN; terms = LIST1 SELF; RPAREN ->
792 | terms -> N.ApplPattern terms)
796 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
802 IDENT "include" ; path = QSTRING ->
803 loc,path,true,L.WithPreferences
804 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
805 loc,path,false,L.WithPreferences
806 | IDENT "include'" ; path = QSTRING ->
807 loc,path,true,L.WithoutPreferences
810 grafite_ncommand: [ [
811 IDENT "nqed" -> G.NQed loc
812 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
813 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
814 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
815 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
817 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
818 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
819 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
820 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
821 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
822 paramspec = OPT inverter_param_list ;
823 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
824 G.NInverter (loc,name,indty,paramspec,outsort)
825 | NLETCOREC ; defs = let_defs ->
826 nmk_rec_corec `CoInductive defs loc
827 | NLETREC ; defs = let_defs ->
828 nmk_rec_corec `Inductive defs loc
829 | IDENT "ninductive"; spec = inductive_spec ->
830 let (params, ind_types) = spec in
831 G.NObj (loc, N.Inductive (params, ind_types))
832 | IDENT "ncoinductive"; spec = inductive_spec ->
833 let (params, ind_types) = spec in
834 let ind_types = (* set inductive flags to false (coinductive) *)
835 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
838 G.NObj (loc, N.Inductive (params, ind_types))
839 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
840 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
842 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
843 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
844 | _ -> raise (Failure "only a Type[…] sort can be constrained")
848 G.NUnivConstraint (loc,u1,u2)
849 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
850 G.UnificationHint (loc, t, n)
851 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
852 SYMBOL <:unicode<def>>; t = term; "on";
853 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
854 "to"; target = term ->
855 G.NCoercion(loc,name,t,ty,(id,source),target)
856 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
857 G.NObj (loc, N.Record (params,name,ty,fields))
858 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
859 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
860 G.NCopy (loc,s,NUri.uri_of_string u,
861 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
865 IDENT "set"; n = QSTRING; v = QSTRING ->
867 | IDENT "drop" -> G.Drop loc
868 | IDENT "print"; s = IDENT -> G.Print (loc,s)
869 | IDENT "qed" -> G.Qed loc
870 | IDENT "variant" ; name = IDENT; SYMBOL ":";
871 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
874 (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
875 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
876 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
877 G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
878 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
881 N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
882 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
883 G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
884 | LETCOREC ; defs = let_defs ->
885 mk_rec_corec `CoInductive defs loc
886 | LETREC ; defs = let_defs ->
887 mk_rec_corec `Inductive defs loc
888 | IDENT "inductive"; spec = inductive_spec ->
889 let (params, ind_types) = spec in
890 G.Obj (loc, N.Inductive (params, ind_types))
891 | IDENT "coinductive"; spec = inductive_spec ->
892 let (params, ind_types) = spec in
893 let ind_types = (* set inductive flags to false (coinductive) *)
894 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
897 G.Obj (loc, N.Inductive (params, ind_types))
899 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
900 arity = OPT int ; saturations = OPT int;
901 composites = OPT (IDENT "nocomposites") ->
902 let arity = match arity with None -> 0 | Some x -> x in
903 let saturations = match saturations with None -> 0 | Some x -> x in
904 let composites = match composites with None -> true | Some _ -> false in
906 (loc, t, composites, arity, saturations)
907 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
908 G.PreferCoercion (loc, t)
909 | IDENT "pump" ; steps = int ->
911 | IDENT "inverter"; name = IDENT; IDENT "for";
912 indty = tactic_term; paramspec = inverter_param_list ->
914 (loc, name, indty, paramspec)
915 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
916 G.Obj (loc, N.Record (params,name,ty,fields))
917 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
918 let uris = List.map UriManager.uri_of_string uris in
919 G.Default (loc,what,uris)
920 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
921 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
922 refl = tactic_term -> refl ] ;
923 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
924 sym = tactic_term -> sym ] ;
925 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
926 trans = tactic_term -> trans ] ;
928 G.Relation (loc,id,a,aeq,refl,sym,trans)
931 IDENT "alias" ; spec = alias_spec ->
933 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
934 L.Notation (loc, dir, l1, assoc, prec, l2)
935 | IDENT "interpretation"; id = QSTRING;
936 (symbol, args, l3) = interpretation ->
937 L.Interpretation (loc, id, (symbol, args), l3)
940 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
941 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
942 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
943 G.Tactic (loc, Some tac, punct)
944 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
945 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
946 G.NTactic (loc, [tac; npunct_of_punct punct])
947 | tac = ntactic; punct = punctuation_tactical ->
948 G.NTactic (loc, [tac; npunct_of_punct punct])
949 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
950 G.NTactic (loc, [punct])
951 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
952 G.NonPunctuationTactical (loc, tac, punct)
953 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
954 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
955 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
956 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
957 punct = punctuation_tactical ->
958 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
959 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
960 | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
964 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
972 fun ?(never_include=false) ~include_paths status ->
973 let stm = G.Executable (loc, ex) in
974 !grafite_callback stm;
977 fun ?(never_include=false) ~include_paths status ->
978 let stm = G.Comment (loc, com) in
979 !grafite_callback stm;
981 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
982 fun ?(never_include=false) ~include_paths status ->
983 let _root, buri, fullpath, _rrelpath =
984 Librarian.baseuri_of_script ~include_paths fname in
985 if never_include then raise (NoInclusionPerformed fullpath)
990 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
991 !grafite_callback stm;
993 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
996 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
1000 | scom = lexicon_command ; SYMBOL "." ->
1001 fun ?(never_include=false) ~include_paths status ->
1002 !lexicon_callback scom;
1003 let status = LE.eval_command status scom in
1005 | EOI -> raise End_of_file
1012 let _ = initialize_parser () ;;
1014 let exc_located_wrapper f =
1018 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1019 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1020 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1021 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1023 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1024 | Stdpp.Exc_located (floc, exn) ->
1026 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1028 let parse_statement lexbuf =
1030 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1032 let statement () = Obj.magic !grafite_parser.statement
1034 let history = ref [] ;;
1037 LexiconSync.push ();
1038 history := !grafite_parser :: !history;
1039 grafite_parser := initial_parser ();
1040 initialize_parser ()
1046 | [] -> assert false
1048 grafite_parser := gp;
1052 (* vim:set foldmethod=marker: *)