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)
244 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
245 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
246 SYMBOL <:unicode<def>> ; bo = tactic_term ->
248 SYMBOL <:unicode<vdash>>;
249 concl = tactic_term -> (List.rev hyps,concl) ] ->
250 G.NAssert (loc, seqs)
251 | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
252 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
253 G.NCases (loc, what, where)
254 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
255 G.NChange (loc, what, with_what)
256 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
258 (match num with None -> None | Some x -> Some (int_of_string x)),l)
259 | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
260 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
261 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
262 | IDENT "ndestruct" -> G.NDestruct loc
263 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
264 G.NElim (loc, what, where)
265 | IDENT "ngeneralize"; p=pattern_spec ->
266 G.NGeneralize (loc, p)
267 | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
268 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
269 where = pattern_spec ->
270 G.NLetIn (loc,where,t,name)
271 | kind = nreduction_kind; p = pattern_spec ->
272 G.NReduce (loc, kind, p)
273 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
274 G.NRewrite (loc, dir, what, where)
275 | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac)
276 | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
277 | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
278 | IDENT "nassumption" -> G.NAssumption loc
279 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
280 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
281 | SYMBOL "*" -> G.NCase1 (loc,"_")
282 | SYMBOL "*"; n=IDENT ->
287 [ IDENT "absurd"; t = tactic_term ->
289 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
291 | IDENT "apply"; t = tactic_term ->
293 | IDENT "applyP"; t = tactic_term ->
295 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
296 G.ApplyS (loc, t, params)
297 | IDENT "assumption" ->
299 | IDENT "autobatch"; params = auto_params ->
300 G.AutoBatch (loc,params)
301 | IDENT "cases"; what = tactic_term;
302 pattern = OPT pattern_spec;
303 specs = intros_spec ->
304 let pattern = match pattern with
305 | None -> None, [], Some N.UserInput
306 | Some pattern -> pattern
308 G.Cases (loc, what, pattern, specs)
309 | IDENT "clear"; ids = LIST1 IDENT ->
311 | IDENT "clearbody"; id = IDENT ->
313 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
314 G.Change (loc, what, t)
315 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
316 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
317 let times = match times with None -> 1 | Some i -> i in
318 G.Compose (loc, t1, t2, times, specs)
319 | IDENT "constructor"; n = int ->
320 G.Constructor (loc, n)
321 | IDENT "contradiction" ->
323 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
324 G.Cut (loc, ident, t)
325 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
326 let idents = match idents with None -> [] | Some idents -> idents in
327 G.Decompose (loc, idents)
328 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
329 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
330 G.Destruct (loc, xts)
331 | IDENT "elim"; what = tactic_term; using = using;
332 pattern = OPT pattern_spec;
333 ispecs = intros_spec ->
334 let pattern = match pattern with
335 | None -> None, [], Some N.UserInput
336 | Some pattern -> pattern
338 G.Elim (loc, what, using, pattern, ispecs)
339 | IDENT "elimType"; what = tactic_term; using = using;
340 (num, idents) = intros_spec ->
341 G.ElimType (loc, what, using, (num, idents))
342 | IDENT "exact"; t = tactic_term ->
346 | IDENT "fail" -> G.Fail loc
347 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
350 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
351 ("the pattern cannot specify the term to replace, only its"
352 ^ " paths in the hypotheses and in the conclusion")))
354 G.Fold (loc, kind, t, p)
357 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
358 let idents = match idents with None -> [] | Some idents -> idents in
359 G.FwdSimpl (loc, hyp, idents)
360 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
361 G.Generalize (loc,p,id)
362 | IDENT "id" -> G.IdTac loc
363 | IDENT "intro"; ident = OPT IDENT ->
364 let idents = match ident with None -> [] | Some id -> [Some id] in
365 G.Intros (loc, (Some 1, idents))
366 | IDENT "intros"; specs = intros_spec ->
367 G.Intros (loc, specs)
368 | IDENT "inversion"; t = tactic_term ->
371 linear = OPT [ IDENT "linear" ];
372 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
374 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
375 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
376 let linear = match linear with None -> false | Some _ -> true in
377 let to_what = match to_what with None -> [] | Some to_what -> to_what in
378 G.LApply (loc, linear, depth, to_what, what, ident)
379 | IDENT "left" -> G.Left loc
380 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
381 G.LetIn (loc, t, where)
382 | kind = reduction_kind; p = pattern_spec ->
383 G.Reduce (loc, kind, p)
384 | IDENT "reflexivity" ->
386 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
387 G.Replace (loc, p, t)
388 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
389 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
393 (HExtlib.Localized (loc,
394 (CicNotationParser.Parse_error
395 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
397 let n = match xnames with None -> [] | Some names -> names in
398 G.Rewrite (loc, d, t, p, n)
405 | IDENT "symmetry" ->
407 | IDENT "transitivity"; t = tactic_term ->
408 G.Transitivity (loc, t)
409 (* Produzioni Aggiunte *)
410 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
411 G.Assume (loc, id, t)
412 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
413 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
414 t' = tactic_term -> t']->
415 G.Suppose (loc, t, id, t1)
416 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
417 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
418 id2 = IDENT ; RPAREN ->
419 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
421 [ IDENT "using"; t=tactic_term -> `Term t
422 | params = auto_params -> `Auto params] ;
423 cont=by_continuation ->
425 BYC_done -> G.Bydone (loc, just)
426 | BYC_weproved (ty,id,t1) ->
427 G.By_just_we_proved(loc, just, ty, id, t1)
428 | BYC_letsuchthat (id1,t1,id2,t2) ->
429 G.ExistsElim (loc, just, id1, t1, id2, t2)
430 | BYC_wehaveand (id1,t1,id2,t2) ->
431 G.AndElim (loc, just, id1, t1, id2, t2))
432 | 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']->
433 G.We_need_to_prove (loc, t, id, t1)
434 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
435 G.We_proceed_by_cases_on (loc, t, t1)
436 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
437 G.We_proceed_by_induction_on (loc, t, t1)
438 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
439 G.Byinduction(loc, t, id)
440 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
441 G.Thesisbecomes(loc, t)
442 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
443 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
444 G.Case(loc,id,params)
445 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
447 termine = tactic_term;
451 [ IDENT "using"; t=tactic_term -> `Term t
452 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
453 | IDENT "proof" -> `Proof
454 | params = auto_params -> `Auto params];
455 cont = rewriting_step_continuation ->
456 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
457 | IDENT "obtain" ; name = IDENT;
458 termine = tactic_term;
462 [ IDENT "using"; t=tactic_term -> `Term t
463 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
464 | IDENT "proof" -> `Proof
465 | params = auto_params -> `Auto params];
466 cont = rewriting_step_continuation ->
467 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
471 [ IDENT "using"; t=tactic_term -> `Term t
472 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
473 | IDENT "proof" -> `Proof
474 | params = auto_params -> `Auto params];
475 cont = rewriting_step_continuation ->
476 G.RewritingStep(loc, None, t1, t2, cont)
480 [ IDENT "paramodulation"
481 | IDENT "fast_paramod"
495 i = auto_fixed_param -> i,""
496 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
497 string_of_int v | v = IDENT -> v ] -> i,v ];
498 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
499 (match tl with Some l -> l | None -> []),
505 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
506 | flavour = inline_flavour -> G.IPAs flavour
507 | IDENT "coercions" -> G.IPCoercions
508 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
509 | IDENT "procedural" -> G.IPProcedural
510 | IDENT "nodefaults" -> G.IPNoDefaults
511 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
512 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
513 | IDENT "comments" -> G.IPComments
514 | IDENT "cr" -> G.IPCR
519 [ 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)
520 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
521 "done" -> BYC_weproved (ty,None,t1)
523 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
524 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
525 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
526 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
527 BYC_wehaveand (id1,t1,id2,t2)
530 rewriting_step_continuation : [
537 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
540 | G.Seq (_, l) -> l @ [ t2 ]
546 [ tac = SELF; SYMBOL ";";
547 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
548 (G.Then (loc, tac, tacs))
551 [ IDENT "do"; count = int; tac = SELF ->
552 G.Do (loc, count, tac)
553 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
557 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
559 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
561 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
563 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
564 | LPAREN; tac = SELF; RPAREN -> tac
565 | tac = tactic -> tac
568 npunctuation_tactical:
570 [ SYMBOL "[" -> G.NBranch loc
571 | SYMBOL "|" -> G.NShift loc
572 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
573 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
574 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
575 | SYMBOL "]" -> G.NMerge loc
576 | SYMBOL ";" -> G.NSemicolon loc
577 | SYMBOL "." -> G.NDot loc
580 punctuation_tactical:
582 [ SYMBOL "[" -> G.Branch loc
583 | SYMBOL "|" -> G.Shift loc
584 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
585 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
586 | SYMBOL "]" -> G.Merge loc
587 | SYMBOL ";" -> G.Semicolon loc
588 | SYMBOL "." -> G.Dot loc
591 non_punctuation_tactical:
593 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
594 | IDENT "unfocus" -> G.Unfocus loc
595 | IDENT "skip" -> G.Skip loc
599 [ [ IDENT "ndefinition" ] -> `Definition
600 | [ IDENT "nfact" ] -> `Fact
601 | [ IDENT "nlemma" ] -> `Lemma
602 | [ IDENT "nremark" ] -> `Remark
603 | [ IDENT "ntheorem" ] -> `Theorem
607 [ [ IDENT "definition" ] -> `Definition
608 | [ IDENT "fact" ] -> `Fact
609 | [ IDENT "lemma" ] -> `Lemma
610 | [ IDENT "remark" ] -> `Remark
611 | [ IDENT "theorem" ] -> `Theorem
615 [ attr = theorem_flavour -> attr
616 | [ IDENT "axiom" ] -> `Axiom
617 | [ IDENT "variant" ] -> `Variant
622 params = LIST0 protected_binder_vars;
623 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
624 fst_constructors = LIST0 constructor SEP SYMBOL "|";
627 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
628 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
629 (name, true, typ, constructors) ] SEP "with" -> types
633 (fun (names, typ) acc ->
634 (List.map (fun name -> (name, typ)) names) @ acc)
637 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
638 let tl_ind_types = match tl with None -> [] | Some types -> types in
639 let ind_types = fst_ind_type :: tl_ind_types in
645 params = LIST0 protected_binder_vars;
646 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
650 SYMBOL ":" -> false,0
651 | SYMBOL ":"; SYMBOL ">" -> true,0
652 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
655 let b,n = coercion in
657 ] SEP SYMBOL ";"; SYMBOL "}" ->
660 (fun (names, typ) acc ->
661 (List.map (fun name -> (name, typ)) names) @ acc)
664 (params,name,typ,fields)
668 [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
669 | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
674 [ [ IDENT "check" ]; t = term ->
676 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
677 G.Eval (loc, kind, t)
678 | IDENT "inline"; suri = QSTRING; params = inline_params ->
679 G.Inline (loc, suri, params)
680 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
681 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
682 | IDENT "auto"; params = auto_params ->
683 G.AutoInteractive (loc,params)
684 | [ IDENT "whelp"; "match" ] ; t = term ->
686 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
688 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
690 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
692 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
697 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
698 let alpha = "[a-zA-Z]" in
699 let num = "[0-9]+" in
700 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
701 let decoration = "\\'" in
702 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
703 let rex = Str.regexp ("^"^ident^"$") in
704 if Str.string_match rex id 0 then
705 if (try ignore (UriManager.uri_of_string uri); true
706 with UriManager.IllFormedUri _ -> false) ||
707 (try ignore (NReference.reference_of_string uri); true
708 with NReference.IllFormedReference _ -> false)
710 L.Ident_alias (id, uri)
713 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
715 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
716 Printf.sprintf "Not a valid identifier: %s" id)))
717 | IDENT "symbol"; symbol = QSTRING;
718 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
719 SYMBOL "="; dsc = QSTRING ->
721 match instance with Some i -> i | None -> 0
723 L.Symbol_alias (symbol, instance, dsc)
725 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
726 SYMBOL "="; dsc = QSTRING ->
728 match instance with Some i -> i | None -> 0
730 L.Number_alias (instance, dsc)
734 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
736 N.IdentArg (List.length l, id)
740 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
741 | IDENT "right"; IDENT "associative" -> Gramext.RightA
742 | IDENT "non"; IDENT "associative" -> Gramext.NonA
746 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
749 [ dir = OPT direction; s = QSTRING;
750 assoc = OPT associativity; prec = precedence;
753 [ blob = UNPARSED_AST ->
754 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
755 (CicNotationParser.parse_level2_ast
756 (Ulexing.from_utf8_string blob))
757 | blob = UNPARSED_META ->
758 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
759 (CicNotationParser.parse_level2_meta
760 (Ulexing.from_utf8_string blob))
764 | None -> default_associativity
765 | Some assoc -> assoc
768 add_raw_attribute ~text:s
769 (CicNotationParser.parse_level1_pattern prec
770 (Ulexing.from_utf8_string s))
772 (dir, p1, assoc, prec, p2)
776 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
777 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
778 | IMPLICIT -> N.ImplicitPattern
779 | id = IDENT -> N.VarPattern id
780 | LPAREN; terms = LIST1 SELF; RPAREN ->
784 | terms -> N.ApplPattern terms)
788 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
794 IDENT "include" ; path = QSTRING ->
795 loc,path,true,L.WithPreferences
796 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
797 loc,path,false,L.WithPreferences
798 | IDENT "include'" ; path = QSTRING ->
799 loc,path,true,L.WithoutPreferences
802 grafite_ncommand: [ [
803 IDENT "nqed" -> G.NQed loc
804 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
805 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
806 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
807 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
809 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
810 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
811 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
812 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
813 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
814 paramspec = OPT inverter_param_list ;
815 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
816 G.NInverter (loc,name,indty,paramspec,outsort)
817 | NLETCOREC ; defs = let_defs ->
818 nmk_rec_corec `CoInductive defs loc
819 | NLETREC ; defs = let_defs ->
820 nmk_rec_corec `Inductive defs loc
821 | IDENT "ninductive"; spec = inductive_spec ->
822 let (params, ind_types) = spec in
823 G.NObj (loc, N.Inductive (params, ind_types))
824 | IDENT "ncoinductive"; spec = inductive_spec ->
825 let (params, ind_types) = spec in
826 let ind_types = (* set inductive flags to false (coinductive) *)
827 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
830 G.NObj (loc, N.Inductive (params, ind_types))
831 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
832 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
834 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
835 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
836 | _ -> raise (Failure "only a Type[…] sort can be constrained")
840 G.NUnivConstraint (loc,u1,u2)
841 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
842 G.UnificationHint (loc, t, n)
843 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
844 SYMBOL <:unicode<def>>; t = term; "on";
845 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
846 "to"; target = term ->
847 G.NCoercion(loc,name,t,ty,(id,source),target)
848 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
849 G.NObj (loc, N.Record (params,name,ty,fields))
850 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
851 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
852 G.NCopy (loc,s,NUri.uri_of_string u,
853 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
857 IDENT "set"; n = QSTRING; v = QSTRING ->
859 | IDENT "drop" -> G.Drop loc
860 | IDENT "print"; s = IDENT -> G.Print (loc,s)
861 | IDENT "qed" -> G.Qed loc
862 | IDENT "variant" ; name = IDENT; SYMBOL ":";
863 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
866 (`Variant,name,typ,Some (N.Ident (newname, None)), `Regular))
867 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
868 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
869 G.Obj (loc, N.Theorem (flavour, name, typ, body,`Regular))
870 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
873 N.Theorem (flavour, name, N.Implicit `JustOne, Some body,`Regular))
874 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
875 G.Obj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
876 | LETCOREC ; defs = let_defs ->
877 mk_rec_corec `CoInductive defs loc
878 | LETREC ; defs = let_defs ->
879 mk_rec_corec `Inductive defs loc
880 | IDENT "inductive"; spec = inductive_spec ->
881 let (params, ind_types) = spec in
882 G.Obj (loc, N.Inductive (params, ind_types))
883 | IDENT "coinductive"; spec = inductive_spec ->
884 let (params, ind_types) = spec in
885 let ind_types = (* set inductive flags to false (coinductive) *)
886 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
889 G.Obj (loc, N.Inductive (params, ind_types))
891 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
892 arity = OPT int ; saturations = OPT int;
893 composites = OPT (IDENT "nocomposites") ->
894 let arity = match arity with None -> 0 | Some x -> x in
895 let saturations = match saturations with None -> 0 | Some x -> x in
896 let composites = match composites with None -> true | Some _ -> false in
898 (loc, t, composites, arity, saturations)
899 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
900 G.PreferCoercion (loc, t)
901 | IDENT "pump" ; steps = int ->
903 | IDENT "inverter"; name = IDENT; IDENT "for";
904 indty = tactic_term; paramspec = inverter_param_list ->
906 (loc, name, indty, paramspec)
907 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
908 G.Obj (loc, N.Record (params,name,ty,fields))
909 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
910 let uris = List.map UriManager.uri_of_string uris in
911 G.Default (loc,what,uris)
912 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
913 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
914 refl = tactic_term -> refl ] ;
915 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
916 sym = tactic_term -> sym ] ;
917 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
918 trans = tactic_term -> trans ] ;
920 G.Relation (loc,id,a,aeq,refl,sym,trans)
923 IDENT "alias" ; spec = alias_spec ->
925 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
926 L.Notation (loc, dir, l1, assoc, prec, l2)
927 | IDENT "interpretation"; id = QSTRING;
928 (symbol, args, l3) = interpretation ->
929 L.Interpretation (loc, id, (symbol, args), l3)
932 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
933 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
934 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
935 G.Tactic (loc, Some tac, punct)
936 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
937 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
938 G.NTactic (loc, [tac; npunct_of_punct punct])
939 | tac = ntactic; punct = punctuation_tactical ->
940 G.NTactic (loc, [tac; npunct_of_punct punct])
941 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
942 G.NTactic (loc, [punct])
943 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
944 G.NonPunctuationTactical (loc, tac, punct)
945 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
946 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
947 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
948 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
949 punct = punctuation_tactical ->
950 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
951 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
952 | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
956 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
964 fun ?(never_include=false) ~include_paths status ->
965 let stm = G.Executable (loc, ex) in
966 !grafite_callback stm;
969 fun ?(never_include=false) ~include_paths status ->
970 let stm = G.Comment (loc, com) in
971 !grafite_callback stm;
973 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
974 fun ?(never_include=false) ~include_paths status ->
975 let _root, buri, fullpath, _rrelpath =
976 Librarian.baseuri_of_script ~include_paths fname in
977 if never_include then raise (NoInclusionPerformed fullpath)
982 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
983 !grafite_callback stm;
985 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
988 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
992 | scom = lexicon_command ; SYMBOL "." ->
993 fun ?(never_include=false) ~include_paths status ->
994 !lexicon_callback scom;
995 let status = LE.eval_command status scom in
997 | EOI -> raise End_of_file
1004 let _ = initialize_parser () ;;
1006 let exc_located_wrapper f =
1010 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1011 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1012 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1013 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1015 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1016 | Stdpp.Exc_located (floc, exn) ->
1018 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1020 let parse_statement lexbuf =
1022 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1024 let statement () = Obj.magic !grafite_parser.statement
1026 let history = ref [] ;;
1029 LexiconSync.push ();
1030 history := !grafite_parser :: !history;
1031 grafite_parser := initial_parser ();
1032 initialize_parser ()
1038 | [] -> assert false
1040 grafite_parser := gp;
1044 (* vim:set foldmethod=marker: *)