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"; tac = SELF -> G.NTry (loc,tac)
268 | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
269 | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
270 | IDENT "nassumption" -> G.NAssumption loc
271 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
272 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
273 | SYMBOL "*" -> G.NCase1 (loc,"_")
274 | SYMBOL "*"; n=IDENT ->
279 [ IDENT "absurd"; t = tactic_term ->
281 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
283 | IDENT "apply"; t = tactic_term ->
285 | IDENT "applyP"; t = tactic_term ->
287 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
288 G.ApplyS (loc, t, params)
289 | IDENT "assumption" ->
291 | IDENT "autobatch"; params = auto_params ->
292 G.AutoBatch (loc,params)
293 | IDENT "cases"; what = tactic_term;
294 pattern = OPT pattern_spec;
295 specs = intros_spec ->
296 let pattern = match pattern with
297 | None -> None, [], Some N.UserInput
298 | Some pattern -> pattern
300 G.Cases (loc, what, pattern, specs)
301 | IDENT "clear"; ids = LIST1 IDENT ->
303 | IDENT "clearbody"; id = IDENT ->
305 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
306 G.Change (loc, what, t)
307 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
308 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
309 let times = match times with None -> 1 | Some i -> i in
310 G.Compose (loc, t1, t2, times, specs)
311 | IDENT "constructor"; n = int ->
312 G.Constructor (loc, n)
313 | IDENT "contradiction" ->
315 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
316 G.Cut (loc, ident, t)
317 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
318 let idents = match idents with None -> [] | Some idents -> idents in
319 G.Decompose (loc, idents)
320 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
321 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
322 G.Destruct (loc, xts)
323 | IDENT "elim"; what = tactic_term; using = using;
324 pattern = OPT pattern_spec;
325 ispecs = intros_spec ->
326 let pattern = match pattern with
327 | None -> None, [], Some N.UserInput
328 | Some pattern -> pattern
330 G.Elim (loc, what, using, pattern, ispecs)
331 | IDENT "elimType"; what = tactic_term; using = using;
332 (num, idents) = intros_spec ->
333 G.ElimType (loc, what, using, (num, idents))
334 | IDENT "exact"; t = tactic_term ->
338 | IDENT "fail" -> G.Fail loc
339 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
342 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
343 ("the pattern cannot specify the term to replace, only its"
344 ^ " paths in the hypotheses and in the conclusion")))
346 G.Fold (loc, kind, t, p)
349 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
350 let idents = match idents with None -> [] | Some idents -> idents in
351 G.FwdSimpl (loc, hyp, idents)
352 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
353 G.Generalize (loc,p,id)
354 | IDENT "id" -> G.IdTac loc
355 | IDENT "intro"; ident = OPT IDENT ->
356 let idents = match ident with None -> [] | Some id -> [Some id] in
357 G.Intros (loc, (Some 1, idents))
358 | IDENT "intros"; specs = intros_spec ->
359 G.Intros (loc, specs)
360 | IDENT "inversion"; t = tactic_term ->
363 linear = OPT [ IDENT "linear" ];
364 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
366 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
367 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
368 let linear = match linear with None -> false | Some _ -> true in
369 let to_what = match to_what with None -> [] | Some to_what -> to_what in
370 G.LApply (loc, linear, depth, to_what, what, ident)
371 | IDENT "left" -> G.Left loc
372 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
373 G.LetIn (loc, t, where)
374 | kind = reduction_kind; p = pattern_spec ->
375 G.Reduce (loc, kind, p)
376 | IDENT "reflexivity" ->
378 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
379 G.Replace (loc, p, t)
380 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
381 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
385 (HExtlib.Localized (loc,
386 (CicNotationParser.Parse_error
387 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
389 let n = match xnames with None -> [] | Some names -> names in
390 G.Rewrite (loc, d, t, p, n)
397 | IDENT "symmetry" ->
399 | IDENT "transitivity"; t = tactic_term ->
400 G.Transitivity (loc, t)
401 (* Produzioni Aggiunte *)
402 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
403 G.Assume (loc, id, t)
404 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
405 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
406 t' = tactic_term -> t']->
407 G.Suppose (loc, t, id, t1)
408 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
409 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
410 id2 = IDENT ; RPAREN ->
411 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
413 [ IDENT "using"; t=tactic_term -> `Term t
414 | params = auto_params -> `Auto params] ;
415 cont=by_continuation ->
417 BYC_done -> G.Bydone (loc, just)
418 | BYC_weproved (ty,id,t1) ->
419 G.By_just_we_proved(loc, just, ty, id, t1)
420 | BYC_letsuchthat (id1,t1,id2,t2) ->
421 G.ExistsElim (loc, just, id1, t1, id2, t2)
422 | BYC_wehaveand (id1,t1,id2,t2) ->
423 G.AndElim (loc, just, id1, t1, id2, t2))
424 | 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']->
425 G.We_need_to_prove (loc, t, id, t1)
426 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
427 G.We_proceed_by_cases_on (loc, t, t1)
428 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
429 G.We_proceed_by_induction_on (loc, t, t1)
430 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
431 G.Byinduction(loc, t, id)
432 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
433 G.Thesisbecomes(loc, t)
434 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
435 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
436 G.Case(loc,id,params)
437 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
439 termine = tactic_term;
443 [ IDENT "using"; t=tactic_term -> `Term t
444 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
445 | IDENT "proof" -> `Proof
446 | params = auto_params -> `Auto params];
447 cont = rewriting_step_continuation ->
448 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
449 | IDENT "obtain" ; name = IDENT;
450 termine = tactic_term;
454 [ IDENT "using"; t=tactic_term -> `Term t
455 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
456 | IDENT "proof" -> `Proof
457 | params = auto_params -> `Auto params];
458 cont = rewriting_step_continuation ->
459 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
463 [ IDENT "using"; t=tactic_term -> `Term t
464 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
465 | IDENT "proof" -> `Proof
466 | params = auto_params -> `Auto params];
467 cont = rewriting_step_continuation ->
468 G.RewritingStep(loc, None, t1, t2, cont)
472 [ IDENT "paramodulation"
485 i = auto_fixed_param -> i,""
486 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
487 string_of_int v | v = IDENT -> v ] -> i,v ];
488 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
489 (match tl with Some l -> l | None -> []),
495 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
496 | flavour = inline_flavour -> G.IPAs flavour
497 | IDENT "coercions" -> G.IPCoercions
498 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
499 | IDENT "procedural" -> G.IPProcedural
500 | IDENT "nodefaults" -> G.IPNoDefaults
501 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
502 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
503 | IDENT "comments" -> G.IPComments
504 | IDENT "cr" -> G.IPCR
509 [ 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)
510 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
511 "done" -> BYC_weproved (ty,None,t1)
513 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
514 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
515 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
516 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
517 BYC_wehaveand (id1,t1,id2,t2)
520 rewriting_step_continuation : [
527 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
530 | G.Seq (_, l) -> l @ [ t2 ]
536 [ tac = SELF; SYMBOL ";";
537 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
538 (G.Then (loc, tac, tacs))
541 [ IDENT "do"; count = int; tac = SELF ->
542 G.Do (loc, count, tac)
543 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
547 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
549 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
551 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
553 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
554 | LPAREN; tac = SELF; RPAREN -> tac
555 | tac = tactic -> tac
558 npunctuation_tactical:
560 [ SYMBOL "[" -> G.NBranch loc
561 | SYMBOL "|" -> G.NShift loc
562 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
563 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
564 | SYMBOL "]" -> G.NMerge loc
565 | SYMBOL ";" -> G.NSemicolon loc
566 | SYMBOL "." -> G.NDot loc
569 punctuation_tactical:
571 [ SYMBOL "[" -> G.Branch loc
572 | SYMBOL "|" -> G.Shift loc
573 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
574 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
575 | SYMBOL "]" -> G.Merge loc
576 | SYMBOL ";" -> G.Semicolon loc
577 | SYMBOL "." -> G.Dot loc
580 non_punctuation_tactical:
582 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
583 | IDENT "unfocus" -> G.Unfocus loc
584 | IDENT "skip" -> G.Skip loc
588 [ [ IDENT "ndefinition" ] -> `Definition
589 | [ IDENT "nfact" ] -> `Fact
590 | [ IDENT "nlemma" ] -> `Lemma
591 | [ IDENT "nremark" ] -> `Remark
592 | [ IDENT "ntheorem" ] -> `Theorem
596 [ [ IDENT "definition" ] -> `Definition
597 | [ IDENT "fact" ] -> `Fact
598 | [ IDENT "lemma" ] -> `Lemma
599 | [ IDENT "remark" ] -> `Remark
600 | [ IDENT "theorem" ] -> `Theorem
604 [ attr = theorem_flavour -> attr
605 | [ IDENT "axiom" ] -> `Axiom
606 | [ IDENT "variant" ] -> `Variant
611 params = LIST0 protected_binder_vars;
612 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
613 fst_constructors = LIST0 constructor SEP SYMBOL "|";
616 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
617 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
618 (name, true, typ, constructors) ] SEP "with" -> types
622 (fun (names, typ) acc ->
623 (List.map (fun name -> (name, typ)) names) @ acc)
626 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
627 let tl_ind_types = match tl with None -> [] | Some types -> types in
628 let ind_types = fst_ind_type :: tl_ind_types in
634 params = LIST0 protected_binder_vars;
635 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
639 SYMBOL ":" -> false,0
640 | SYMBOL ":"; SYMBOL ">" -> true,0
641 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
644 let b,n = coercion in
646 ] SEP SYMBOL ";"; SYMBOL "}" ->
649 (fun (names, typ) acc ->
650 (List.map (fun name -> (name, typ)) names) @ acc)
653 (params,name,typ,fields)
657 [ [ IDENT "check" ]; t = term ->
659 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
660 G.Eval (loc, kind, t)
661 | IDENT "inline"; suri = QSTRING; params = inline_params ->
662 G.Inline (loc, suri, params)
663 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
664 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
665 | IDENT "auto"; params = auto_params ->
666 G.AutoInteractive (loc,params)
667 | [ IDENT "whelp"; "match" ] ; t = term ->
669 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
671 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
673 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
675 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
680 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
681 let alpha = "[a-zA-Z]" in
682 let num = "[0-9]+" in
683 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
684 let decoration = "\\'" in
685 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
686 let rex = Str.regexp ("^"^ident^"$") in
687 if Str.string_match rex id 0 then
688 if (try ignore (UriManager.uri_of_string uri); true
689 with UriManager.IllFormedUri _ -> false) ||
690 (try ignore (NReference.reference_of_string uri); true
691 with NReference.IllFormedReference _ -> false)
693 L.Ident_alias (id, uri)
696 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
698 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
699 Printf.sprintf "Not a valid identifier: %s" id)))
700 | IDENT "symbol"; symbol = QSTRING;
701 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
702 SYMBOL "="; dsc = QSTRING ->
704 match instance with Some i -> i | None -> 0
706 L.Symbol_alias (symbol, instance, dsc)
708 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
709 SYMBOL "="; dsc = QSTRING ->
711 match instance with Some i -> i | None -> 0
713 L.Number_alias (instance, dsc)
717 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
719 N.IdentArg (List.length l, id)
723 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
724 | IDENT "right"; IDENT "associative" -> Gramext.RightA
725 | IDENT "non"; IDENT "associative" -> Gramext.NonA
729 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
732 [ dir = OPT direction; s = QSTRING;
733 assoc = OPT associativity; prec = precedence;
736 [ blob = UNPARSED_AST ->
737 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
738 (CicNotationParser.parse_level2_ast
739 (Ulexing.from_utf8_string blob))
740 | blob = UNPARSED_META ->
741 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
742 (CicNotationParser.parse_level2_meta
743 (Ulexing.from_utf8_string blob))
747 | None -> default_associativity
748 | Some assoc -> assoc
751 add_raw_attribute ~text:s
752 (CicNotationParser.parse_level1_pattern prec
753 (Ulexing.from_utf8_string s))
755 (dir, p1, assoc, prec, p2)
759 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
760 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
761 | IMPLICIT -> N.ImplicitPattern
762 | id = IDENT -> N.VarPattern id
763 | LPAREN; terms = LIST1 SELF; RPAREN ->
767 | terms -> N.ApplPattern terms)
771 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
777 IDENT "include" ; path = QSTRING ->
778 loc,path,true,L.WithPreferences
779 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
780 loc,path,false,L.WithPreferences
781 | IDENT "include'" ; path = QSTRING ->
782 loc,path,true,L.WithoutPreferences
785 grafite_ncommand: [ [
786 IDENT "nqed" -> G.NQed loc
787 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
788 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
789 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
790 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
792 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
793 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
794 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
795 | NLETCOREC ; defs = let_defs ->
796 nmk_rec_corec `CoInductive defs loc
797 | NLETREC ; defs = let_defs ->
798 nmk_rec_corec `Inductive defs loc
799 | IDENT "ninductive"; spec = inductive_spec ->
800 let (params, ind_types) = spec in
801 G.NObj (loc, N.Inductive (params, ind_types))
802 | IDENT "ncoinductive"; spec = inductive_spec ->
803 let (params, ind_types) = spec in
804 let ind_types = (* set inductive flags to false (coinductive) *)
805 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
808 G.NObj (loc, N.Inductive (params, ind_types))
809 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
810 strict = [ SYMBOL <:unicode<lt>> -> true
811 | SYMBOL <:unicode<leq>> -> false ];
815 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
816 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
817 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
818 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
819 | _ -> raise (Failure "only a sort can be constrained")
823 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
824 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
825 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
826 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
827 | _ -> raise (Failure "only a sort can be constrained")
829 G.NUnivConstraint (loc, strict,u1,u2)
830 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
831 G.UnificationHint (loc, t, n)
832 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
833 SYMBOL <:unicode<def>>; t = term; "on";
834 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
835 "to"; target = term ->
836 G.NCoercion(loc,name,t,ty,(id,source),target)
837 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
838 G.NObj (loc, N.Record (params,name,ty,fields))
839 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
840 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
841 G.NCopy (loc,s,NUri.uri_of_string u,
842 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
846 IDENT "set"; n = QSTRING; v = QSTRING ->
848 | IDENT "drop" -> G.Drop loc
849 | IDENT "print"; s = IDENT -> G.Print (loc,s)
850 | IDENT "qed" -> G.Qed loc
851 | IDENT "variant" ; name = IDENT; SYMBOL ":";
852 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
855 (`Variant,name,typ,Some (N.Ident (newname, None))))
856 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
857 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
858 G.Obj (loc, N.Theorem (flavour, name, typ, body))
859 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
862 N.Theorem (flavour, name, N.Implicit, Some body))
863 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
864 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
865 | LETCOREC ; defs = let_defs ->
866 mk_rec_corec `CoInductive defs loc
867 | LETREC ; defs = let_defs ->
868 mk_rec_corec `Inductive defs loc
869 | IDENT "inductive"; spec = inductive_spec ->
870 let (params, ind_types) = spec in
871 G.Obj (loc, N.Inductive (params, ind_types))
872 | IDENT "coinductive"; spec = inductive_spec ->
873 let (params, ind_types) = spec in
874 let ind_types = (* set inductive flags to false (coinductive) *)
875 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
878 G.Obj (loc, N.Inductive (params, ind_types))
880 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
881 arity = OPT int ; saturations = OPT int;
882 composites = OPT (IDENT "nocomposites") ->
883 let arity = match arity with None -> 0 | Some x -> x in
884 let saturations = match saturations with None -> 0 | Some x -> x in
885 let composites = match composites with None -> true | Some _ -> false in
887 (loc, t, composites, arity, saturations)
888 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
889 G.PreferCoercion (loc, t)
890 | IDENT "pump" ; steps = int ->
892 | IDENT "inverter"; name = IDENT; IDENT "for";
893 indty = tactic_term; paramspec = inverter_param_list ->
895 (loc, name, indty, paramspec)
896 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
897 G.Obj (loc, N.Record (params,name,ty,fields))
898 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
899 let uris = List.map UriManager.uri_of_string uris in
900 G.Default (loc,what,uris)
901 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
902 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
903 refl = tactic_term -> refl ] ;
904 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
905 sym = tactic_term -> sym ] ;
906 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
907 trans = tactic_term -> trans ] ;
909 G.Relation (loc,id,a,aeq,refl,sym,trans)
912 IDENT "alias" ; spec = alias_spec ->
914 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
915 L.Notation (loc, dir, l1, assoc, prec, l2)
916 | IDENT "interpretation"; id = QSTRING;
917 (symbol, args, l3) = interpretation ->
918 L.Interpretation (loc, id, (symbol, args), l3)
921 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
922 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
923 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
924 G.Tactic (loc, Some tac, punct)
925 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
926 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
927 G.NTactic (loc, [tac; npunct_of_punct punct])
928 | tac = ntactic; punct = punctuation_tactical ->
929 G.NTactic (loc, [tac; npunct_of_punct punct])
930 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
931 G.NTactic (loc, [punct])
932 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
933 G.NonPunctuationTactical (loc, tac, punct)
934 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
935 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
936 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
937 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
938 punct = punctuation_tactical ->
939 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
940 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
944 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
952 fun ?(never_include=false) ~include_paths status ->
953 let stm = G.Executable (loc, ex) in
954 !grafite_callback stm;
957 fun ?(never_include=false) ~include_paths status ->
958 let stm = G.Comment (loc, com) in
959 !grafite_callback stm;
961 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
962 fun ?(never_include=false) ~include_paths status ->
963 let _root, buri, fullpath, _rrelpath =
964 Librarian.baseuri_of_script ~include_paths fname in
965 if never_include then raise (NoInclusionPerformed fullpath)
970 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
971 !grafite_callback stm;
973 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
976 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
980 | scom = lexicon_command ; SYMBOL "." ->
981 fun ?(never_include=false) ~include_paths status ->
982 !lexicon_callback scom;
983 let status = LE.eval_command status scom in
985 | EOI -> raise End_of_file
992 let _ = initialize_parser () ;;
994 let exc_located_wrapper f =
998 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
999 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1000 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1001 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1003 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1004 | Stdpp.Exc_located (floc, exn) ->
1006 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1008 let parse_statement lexbuf =
1010 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1012 let statement () = Obj.magic !grafite_parser.statement
1014 let history = ref [] ;;
1017 LexiconSync.push ();
1018 history := !grafite_parser :: !history;
1019 grafite_parser := initial_parser ();
1020 initialize_parser ()
1026 | [] -> assert false
1028 grafite_parser := gp;
1032 (* vim:set foldmethod=marker: *)