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 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))))
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 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
257 G.NElim (loc, what, where)
258 | IDENT "ngeneralize"; p=pattern_spec ->
259 G.NGeneralize (loc, p)
260 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
261 where = pattern_spec ->
262 G.NLetIn (loc,where,t,name)
263 | kind = nreduction_kind; p = pattern_spec ->
264 G.NReduce (loc, kind, p)
265 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
266 G.NRewrite (loc, dir, what, where)
267 | IDENT "ntry"; LPAREN ; tac = SELF ; RPAREN -> G.NTry (loc,tac)
268 | IDENT "nassumption" -> G.NAssumption loc
269 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
270 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
271 | SYMBOL "*" -> G.NCase1 (loc,"_")
272 | SYMBOL "*"; n=IDENT ->
277 [ IDENT "absurd"; t = tactic_term ->
279 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
281 | IDENT "apply"; t = tactic_term ->
283 | IDENT "applyP"; t = tactic_term ->
285 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
286 G.ApplyS (loc, t, params)
287 | IDENT "assumption" ->
289 | IDENT "autobatch"; params = auto_params ->
290 G.AutoBatch (loc,params)
291 | IDENT "cases"; what = tactic_term;
292 pattern = OPT pattern_spec;
293 specs = intros_spec ->
294 let pattern = match pattern with
295 | None -> None, [], Some N.UserInput
296 | Some pattern -> pattern
298 G.Cases (loc, what, pattern, specs)
299 | IDENT "clear"; ids = LIST1 IDENT ->
301 | IDENT "clearbody"; id = IDENT ->
303 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
304 G.Change (loc, what, t)
305 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
306 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
307 let times = match times with None -> 1 | Some i -> i in
308 G.Compose (loc, t1, t2, times, specs)
309 | IDENT "constructor"; n = int ->
310 G.Constructor (loc, n)
311 | IDENT "contradiction" ->
313 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
314 G.Cut (loc, ident, t)
315 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
316 let idents = match idents with None -> [] | Some idents -> idents in
317 G.Decompose (loc, idents)
318 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
319 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
320 G.Destruct (loc, xts)
321 | IDENT "elim"; what = tactic_term; using = using;
322 pattern = OPT pattern_spec;
323 ispecs = intros_spec ->
324 let pattern = match pattern with
325 | None -> None, [], Some N.UserInput
326 | Some pattern -> pattern
328 G.Elim (loc, what, using, pattern, ispecs)
329 | IDENT "elimType"; what = tactic_term; using = using;
330 (num, idents) = intros_spec ->
331 G.ElimType (loc, what, using, (num, idents))
332 | IDENT "exact"; t = tactic_term ->
336 | IDENT "fail" -> G.Fail loc
337 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
340 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
341 ("the pattern cannot specify the term to replace, only its"
342 ^ " paths in the hypotheses and in the conclusion")))
344 G.Fold (loc, kind, t, p)
347 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
348 let idents = match idents with None -> [] | Some idents -> idents in
349 G.FwdSimpl (loc, hyp, idents)
350 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
351 G.Generalize (loc,p,id)
352 | IDENT "id" -> G.IdTac loc
353 | IDENT "intro"; ident = OPT IDENT ->
354 let idents = match ident with None -> [] | Some id -> [Some id] in
355 G.Intros (loc, (Some 1, idents))
356 | IDENT "intros"; specs = intros_spec ->
357 G.Intros (loc, specs)
358 | IDENT "inversion"; t = tactic_term ->
361 linear = OPT [ IDENT "linear" ];
362 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
364 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
365 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
366 let linear = match linear with None -> false | Some _ -> true in
367 let to_what = match to_what with None -> [] | Some to_what -> to_what in
368 G.LApply (loc, linear, depth, to_what, what, ident)
369 | IDENT "left" -> G.Left loc
370 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
371 G.LetIn (loc, t, where)
372 | kind = reduction_kind; p = pattern_spec ->
373 G.Reduce (loc, kind, p)
374 | IDENT "reflexivity" ->
376 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
377 G.Replace (loc, p, t)
378 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
379 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
383 (HExtlib.Localized (loc,
384 (CicNotationParser.Parse_error
385 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
387 let n = match xnames with None -> [] | Some names -> names in
388 G.Rewrite (loc, d, t, p, n)
395 | IDENT "symmetry" ->
397 | IDENT "transitivity"; t = tactic_term ->
398 G.Transitivity (loc, t)
399 (* Produzioni Aggiunte *)
400 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
401 G.Assume (loc, id, t)
402 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
403 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
404 t' = tactic_term -> t']->
405 G.Suppose (loc, t, id, t1)
406 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
407 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
408 id2 = IDENT ; RPAREN ->
409 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
411 [ IDENT "using"; t=tactic_term -> `Term t
412 | params = auto_params -> `Auto params] ;
413 cont=by_continuation ->
415 BYC_done -> G.Bydone (loc, just)
416 | BYC_weproved (ty,id,t1) ->
417 G.By_just_we_proved(loc, just, ty, id, t1)
418 | BYC_letsuchthat (id1,t1,id2,t2) ->
419 G.ExistsElim (loc, just, id1, t1, id2, t2)
420 | BYC_wehaveand (id1,t1,id2,t2) ->
421 G.AndElim (loc, just, id1, t1, id2, t2))
422 | 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']->
423 G.We_need_to_prove (loc, t, id, t1)
424 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
425 G.We_proceed_by_cases_on (loc, t, t1)
426 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
427 G.We_proceed_by_induction_on (loc, t, t1)
428 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
429 G.Byinduction(loc, t, id)
430 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
431 G.Thesisbecomes(loc, t)
432 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
433 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
434 G.Case(loc,id,params)
435 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
437 termine = tactic_term;
441 [ IDENT "using"; t=tactic_term -> `Term t
442 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
443 | IDENT "proof" -> `Proof
444 | params = auto_params -> `Auto params];
445 cont = rewriting_step_continuation ->
446 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
447 | IDENT "obtain" ; name = IDENT;
448 termine = tactic_term;
452 [ IDENT "using"; t=tactic_term -> `Term t
453 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
454 | IDENT "proof" -> `Proof
455 | params = auto_params -> `Auto params];
456 cont = rewriting_step_continuation ->
457 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
461 [ IDENT "using"; t=tactic_term -> `Term t
462 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
463 | IDENT "proof" -> `Proof
464 | params = auto_params -> `Auto params];
465 cont = rewriting_step_continuation ->
466 G.RewritingStep(loc, None, t1, t2, cont)
470 [ IDENT "paramodulation"
483 i = auto_fixed_param -> i,""
484 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
485 string_of_int v | v = IDENT -> v ] -> i,v ];
486 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
487 (match tl with Some l -> l | None -> []),
493 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
494 | flavour = inline_flavour -> G.IPAs flavour
495 | IDENT "coercions" -> G.IPCoercions
496 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
497 | IDENT "procedural" -> G.IPProcedural
498 | IDENT "nodefaults" -> G.IPNoDefaults
499 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
500 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
501 | IDENT "comments" -> G.IPComments
502 | IDENT "cr" -> G.IPCR
507 [ 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)
508 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
509 "done" -> BYC_weproved (ty,None,t1)
511 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
512 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
513 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
514 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
515 BYC_wehaveand (id1,t1,id2,t2)
518 rewriting_step_continuation : [
525 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
528 | G.Seq (_, l) -> l @ [ t2 ]
534 [ tac = SELF; SYMBOL ";";
535 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
536 (G.Then (loc, tac, tacs))
539 [ IDENT "do"; count = int; tac = SELF ->
540 G.Do (loc, count, tac)
541 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
545 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
547 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
549 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
551 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
552 | LPAREN; tac = SELF; RPAREN -> tac
553 | tac = tactic -> tac
556 npunctuation_tactical:
558 [ SYMBOL "[" -> G.NBranch loc
559 | SYMBOL "|" -> G.NShift loc
560 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
561 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
562 | SYMBOL "]" -> G.NMerge loc
563 | SYMBOL ";" -> G.NSemicolon loc
564 | SYMBOL "." -> G.NDot loc
567 punctuation_tactical:
569 [ SYMBOL "[" -> G.Branch loc
570 | SYMBOL "|" -> G.Shift loc
571 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
572 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
573 | SYMBOL "]" -> G.Merge loc
574 | SYMBOL ";" -> G.Semicolon loc
575 | SYMBOL "." -> G.Dot loc
578 non_punctuation_tactical:
580 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
581 | IDENT "unfocus" -> G.Unfocus loc
582 | IDENT "skip" -> G.Skip loc
586 [ [ IDENT "ndefinition" ] -> `Definition
587 | [ IDENT "nfact" ] -> `Fact
588 | [ IDENT "nlemma" ] -> `Lemma
589 | [ IDENT "nremark" ] -> `Remark
590 | [ IDENT "ntheorem" ] -> `Theorem
594 [ [ IDENT "definition" ] -> `Definition
595 | [ IDENT "fact" ] -> `Fact
596 | [ IDENT "lemma" ] -> `Lemma
597 | [ IDENT "remark" ] -> `Remark
598 | [ IDENT "theorem" ] -> `Theorem
602 [ attr = theorem_flavour -> attr
603 | [ IDENT "axiom" ] -> `Axiom
604 | [ IDENT "variant" ] -> `Variant
609 params = LIST0 protected_binder_vars;
610 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
611 fst_constructors = LIST0 constructor SEP SYMBOL "|";
614 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
615 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
616 (name, true, typ, constructors) ] SEP "with" -> types
620 (fun (names, typ) acc ->
621 (List.map (fun name -> (name, typ)) names) @ acc)
624 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
625 let tl_ind_types = match tl with None -> [] | Some types -> types in
626 let ind_types = fst_ind_type :: tl_ind_types in
632 params = LIST0 protected_binder_vars;
633 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
637 SYMBOL ":" -> false,0
638 | SYMBOL ":"; SYMBOL ">" -> true,0
639 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
642 let b,n = coercion in
644 ] SEP SYMBOL ";"; SYMBOL "}" ->
647 (fun (names, typ) acc ->
648 (List.map (fun name -> (name, typ)) names) @ acc)
651 (params,name,typ,fields)
655 [ [ IDENT "check" ]; t = term ->
657 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
658 G.Eval (loc, kind, t)
659 | IDENT "inline"; suri = QSTRING; params = inline_params ->
660 G.Inline (loc, suri, params)
661 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
662 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
663 | IDENT "auto"; params = auto_params ->
664 G.AutoInteractive (loc,params)
665 | [ IDENT "whelp"; "match" ] ; t = term ->
667 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
669 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
671 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
673 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
678 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
679 let alpha = "[a-zA-Z]" in
680 let num = "[0-9]+" in
681 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
682 let decoration = "\\'" in
683 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
684 let rex = Str.regexp ("^"^ident^"$") in
685 if Str.string_match rex id 0 then
686 if (try ignore (UriManager.uri_of_string uri); true
687 with UriManager.IllFormedUri _ -> false) ||
688 (try ignore (NReference.reference_of_string uri); true
689 with NReference.IllFormedReference _ -> false)
691 L.Ident_alias (id, uri)
694 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
696 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
697 Printf.sprintf "Not a valid identifier: %s" id)))
698 | IDENT "symbol"; symbol = QSTRING;
699 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
700 SYMBOL "="; dsc = QSTRING ->
702 match instance with Some i -> i | None -> 0
704 L.Symbol_alias (symbol, instance, dsc)
706 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
707 SYMBOL "="; dsc = QSTRING ->
709 match instance with Some i -> i | None -> 0
711 L.Number_alias (instance, dsc)
715 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
717 N.IdentArg (List.length l, id)
721 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
722 | IDENT "right"; IDENT "associative" -> Gramext.RightA
723 | IDENT "non"; IDENT "associative" -> Gramext.NonA
727 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
730 [ dir = OPT direction; s = QSTRING;
731 assoc = OPT associativity; prec = precedence;
734 [ blob = UNPARSED_AST ->
735 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
736 (CicNotationParser.parse_level2_ast
737 (Ulexing.from_utf8_string blob))
738 | blob = UNPARSED_META ->
739 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
740 (CicNotationParser.parse_level2_meta
741 (Ulexing.from_utf8_string blob))
745 | None -> default_associativity
746 | Some assoc -> assoc
749 add_raw_attribute ~text:s
750 (CicNotationParser.parse_level1_pattern prec
751 (Ulexing.from_utf8_string s))
753 (dir, p1, assoc, prec, p2)
757 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
758 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
759 | IMPLICIT -> N.ImplicitPattern
760 | id = IDENT -> N.VarPattern id
761 | LPAREN; terms = LIST1 SELF; RPAREN ->
765 | terms -> N.ApplPattern terms)
769 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
775 IDENT "include" ; path = QSTRING ->
776 loc,path,true,L.WithPreferences
777 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
778 loc,path,false,L.WithPreferences
779 | IDENT "include'" ; path = QSTRING ->
780 loc,path,true,L.WithoutPreferences
783 grafite_ncommand: [ [
784 IDENT "nqed" -> G.NQed loc
785 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
786 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
787 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
788 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
790 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
791 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
792 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
793 | NLETCOREC ; defs = let_defs ->
794 nmk_rec_corec `CoInductive defs loc
795 | NLETREC ; defs = let_defs ->
796 nmk_rec_corec `Inductive defs loc
797 | IDENT "ninductive"; spec = inductive_spec ->
798 let (params, ind_types) = spec in
799 G.NObj (loc, N.Inductive (params, ind_types))
800 | IDENT "ncoinductive"; spec = inductive_spec ->
801 let (params, ind_types) = spec in
802 let ind_types = (* set inductive flags to false (coinductive) *)
803 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
806 G.NObj (loc, N.Inductive (params, ind_types))
807 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
808 strict = [ SYMBOL <:unicode<lt>> -> true
809 | SYMBOL <:unicode<leq>> -> false ];
813 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
814 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
815 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
816 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
817 | _ -> raise (Failure "only a sort can be constrained")
821 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
822 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
823 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
824 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
825 | _ -> raise (Failure "only a sort can be constrained")
827 G.NUnivConstraint (loc, strict,u1,u2)
828 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
829 G.UnificationHint (loc, t, n)
830 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
831 G.NObj (loc, N.Record (params,name,ty,fields))
835 IDENT "set"; n = QSTRING; v = QSTRING ->
837 | IDENT "drop" -> G.Drop loc
838 | IDENT "print"; s = IDENT -> G.Print (loc,s)
839 | IDENT "qed" -> G.Qed loc
840 | IDENT "variant" ; name = IDENT; SYMBOL ":";
841 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
844 (`Variant,name,typ,Some (N.Ident (newname, None))))
845 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
846 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
847 G.Obj (loc, N.Theorem (flavour, name, typ, body))
848 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
851 N.Theorem (flavour, name, N.Implicit, Some body))
852 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
853 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
854 | LETCOREC ; defs = let_defs ->
855 mk_rec_corec `CoInductive defs loc
856 | LETREC ; defs = let_defs ->
857 mk_rec_corec `Inductive defs loc
858 | IDENT "inductive"; spec = inductive_spec ->
859 let (params, ind_types) = spec in
860 G.Obj (loc, N.Inductive (params, ind_types))
861 | IDENT "coinductive"; spec = inductive_spec ->
862 let (params, ind_types) = spec in
863 let ind_types = (* set inductive flags to false (coinductive) *)
864 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
867 G.Obj (loc, N.Inductive (params, ind_types))
869 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
870 arity = OPT int ; saturations = OPT int;
871 composites = OPT (IDENT "nocomposites") ->
872 let arity = match arity with None -> 0 | Some x -> x in
873 let saturations = match saturations with None -> 0 | Some x -> x in
874 let composites = match composites with None -> true | Some _ -> false in
876 (loc, t, composites, arity, saturations)
877 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
878 G.PreferCoercion (loc, t)
879 | IDENT "pump" ; steps = int ->
881 | IDENT "inverter"; name = IDENT; IDENT "for";
882 indty = tactic_term; paramspec = inverter_param_list ->
884 (loc, name, indty, paramspec)
885 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
886 G.Obj (loc, N.Record (params,name,ty,fields))
887 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
888 let uris = List.map UriManager.uri_of_string uris in
889 G.Default (loc,what,uris)
890 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
891 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
892 refl = tactic_term -> refl ] ;
893 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
894 sym = tactic_term -> sym ] ;
895 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
896 trans = tactic_term -> trans ] ;
898 G.Relation (loc,id,a,aeq,refl,sym,trans)
901 IDENT "alias" ; spec = alias_spec ->
903 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
904 L.Notation (loc, dir, l1, assoc, prec, l2)
905 | IDENT "interpretation"; id = QSTRING;
906 (symbol, args, l3) = interpretation ->
907 L.Interpretation (loc, id, (symbol, args), l3)
910 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
911 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
912 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
913 G.Tactic (loc, Some tac, punct)
914 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
915 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
916 G.NTactic (loc, [tac; npunct_of_punct punct])
917 | tac = ntactic; punct = punctuation_tactical ->
918 G.NTactic (loc, [tac; npunct_of_punct punct])
919 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
920 G.NTactic (loc, [punct])
921 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
922 G.NonPunctuationTactical (loc, tac, punct)
923 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
924 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
925 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
926 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
927 punct = punctuation_tactical ->
928 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
929 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
933 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
941 fun ?(never_include=false) ~include_paths status ->
942 let stm = G.Executable (loc, ex) in
943 !grafite_callback stm;
946 fun ?(never_include=false) ~include_paths status ->
947 let stm = G.Comment (loc, com) in
948 !grafite_callback stm;
950 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
951 fun ?(never_include=false) ~include_paths status ->
953 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
955 !grafite_callback stm;
956 let _root, buri, fullpath, _rrelpath =
957 Librarian.baseuri_of_script ~include_paths fname
960 if never_include then raise (NoInclusionPerformed fullpath)
961 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
964 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
967 | scom = lexicon_command ; SYMBOL "." ->
968 fun ?(never_include=false) ~include_paths status ->
969 !lexicon_callback scom;
970 let status = LE.eval_command status scom in
972 | EOI -> raise End_of_file
979 let _ = initialize_parser () ;;
981 let exc_located_wrapper f =
985 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
986 | Stdpp.Exc_located (floc, Stream.Error msg) ->
987 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
988 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
990 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
991 | Stdpp.Exc_located (floc, exn) ->
993 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
995 let parse_statement lexbuf =
997 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
999 let statement () = Obj.magic !grafite_parser.statement
1001 let history = ref [] ;;
1004 LexiconSync.push ();
1005 history := !grafite_parser :: !history;
1006 grafite_parser := initial_parser ();
1007 initialize_parser ()
1013 | [] -> assert false
1015 grafite_parser := gp;
1019 (* vim:set foldmethod=marker: *)