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 := Obj.magic cb
57 let lexicon_callback = ref (fun _ _ -> ())
58 let set_lexicon_callback cb = lexicon_callback := Obj.magic 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 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
268 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
269 | SYMBOL "*" -> G.NCase1 (loc,"_")
270 | SYMBOL "*"; n=IDENT ->
275 [ IDENT "absurd"; t = tactic_term ->
277 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
279 | IDENT "apply"; t = tactic_term ->
281 | IDENT "applyP"; t = tactic_term ->
283 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
284 G.ApplyS (loc, t, params)
285 | IDENT "assumption" ->
287 | IDENT "autobatch"; params = auto_params ->
288 G.AutoBatch (loc,params)
289 | IDENT "cases"; what = tactic_term;
290 pattern = OPT pattern_spec;
291 specs = intros_spec ->
292 let pattern = match pattern with
293 | None -> None, [], Some N.UserInput
294 | Some pattern -> pattern
296 G.Cases (loc, what, pattern, specs)
297 | IDENT "clear"; ids = LIST1 IDENT ->
299 | IDENT "clearbody"; id = IDENT ->
301 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
302 G.Change (loc, what, t)
303 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
304 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
305 let times = match times with None -> 1 | Some i -> i in
306 G.Compose (loc, t1, t2, times, specs)
307 | IDENT "constructor"; n = int ->
308 G.Constructor (loc, n)
309 | IDENT "contradiction" ->
311 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
312 G.Cut (loc, ident, t)
313 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
314 let idents = match idents with None -> [] | Some idents -> idents in
315 G.Decompose (loc, idents)
316 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
317 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
318 G.Destruct (loc, xts)
319 | IDENT "elim"; what = tactic_term; using = using;
320 pattern = OPT pattern_spec;
321 ispecs = intros_spec ->
322 let pattern = match pattern with
323 | None -> None, [], Some N.UserInput
324 | Some pattern -> pattern
326 G.Elim (loc, what, using, pattern, ispecs)
327 | IDENT "elimType"; what = tactic_term; using = using;
328 (num, idents) = intros_spec ->
329 G.ElimType (loc, what, using, (num, idents))
330 | IDENT "exact"; t = tactic_term ->
334 | IDENT "fail" -> G.Fail loc
335 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
338 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
339 ("the pattern cannot specify the term to replace, only its"
340 ^ " paths in the hypotheses and in the conclusion")))
342 G.Fold (loc, kind, t, p)
345 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
346 let idents = match idents with None -> [] | Some idents -> idents in
347 G.FwdSimpl (loc, hyp, idents)
348 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
349 G.Generalize (loc,p,id)
350 | IDENT "id" -> G.IdTac loc
351 | IDENT "intro"; ident = OPT IDENT ->
352 let idents = match ident with None -> [] | Some id -> [Some id] in
353 G.Intros (loc, (Some 1, idents))
354 | IDENT "intros"; specs = intros_spec ->
355 G.Intros (loc, specs)
356 | IDENT "inversion"; t = tactic_term ->
359 linear = OPT [ IDENT "linear" ];
360 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
362 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
363 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
364 let linear = match linear with None -> false | Some _ -> true in
365 let to_what = match to_what with None -> [] | Some to_what -> to_what in
366 G.LApply (loc, linear, depth, to_what, what, ident)
367 | IDENT "left" -> G.Left loc
368 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
369 G.LetIn (loc, t, where)
370 | kind = reduction_kind; p = pattern_spec ->
371 G.Reduce (loc, kind, p)
372 | IDENT "reflexivity" ->
374 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
375 G.Replace (loc, p, t)
376 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
377 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
381 (HExtlib.Localized (loc,
382 (CicNotationParser.Parse_error
383 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
385 let n = match xnames with None -> [] | Some names -> names in
386 G.Rewrite (loc, d, t, p, n)
393 | IDENT "symmetry" ->
395 | IDENT "transitivity"; t = tactic_term ->
396 G.Transitivity (loc, t)
397 (* Produzioni Aggiunte *)
398 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
399 G.Assume (loc, id, t)
400 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
401 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
402 t' = tactic_term -> t']->
403 G.Suppose (loc, t, id, t1)
404 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
405 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
406 id2 = IDENT ; RPAREN ->
407 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
409 [ IDENT "using"; t=tactic_term -> `Term t
410 | params = auto_params -> `Auto params] ;
411 cont=by_continuation ->
413 BYC_done -> G.Bydone (loc, just)
414 | BYC_weproved (ty,id,t1) ->
415 G.By_just_we_proved(loc, just, ty, id, t1)
416 | BYC_letsuchthat (id1,t1,id2,t2) ->
417 G.ExistsElim (loc, just, id1, t1, id2, t2)
418 | BYC_wehaveand (id1,t1,id2,t2) ->
419 G.AndElim (loc, just, id1, t1, id2, t2))
420 | 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']->
421 G.We_need_to_prove (loc, t, id, t1)
422 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
423 G.We_proceed_by_cases_on (loc, t, t1)
424 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
425 G.We_proceed_by_induction_on (loc, t, t1)
426 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
427 G.Byinduction(loc, t, id)
428 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
429 G.Thesisbecomes(loc, t)
430 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
431 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
432 G.Case(loc,id,params)
433 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
435 termine = tactic_term;
439 [ IDENT "using"; t=tactic_term -> `Term t
440 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
441 | IDENT "proof" -> `Proof
442 | params = auto_params -> `Auto params];
443 cont = rewriting_step_continuation ->
444 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
445 | IDENT "obtain" ; name = IDENT;
446 termine = tactic_term;
450 [ IDENT "using"; t=tactic_term -> `Term t
451 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
452 | IDENT "proof" -> `Proof
453 | params = auto_params -> `Auto params];
454 cont = rewriting_step_continuation ->
455 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
459 [ IDENT "using"; t=tactic_term -> `Term t
460 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
461 | IDENT "proof" -> `Proof
462 | params = auto_params -> `Auto params];
463 cont = rewriting_step_continuation ->
464 G.RewritingStep(loc, None, t1, t2, cont)
468 [ IDENT "paramodulation"
481 i = auto_fixed_param -> i,""
482 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
483 string_of_int v | v = IDENT -> v ] -> i,v ];
484 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
485 (match tl with Some l -> l | None -> []),
491 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
492 | flavour = inline_flavour -> G.IPAs flavour
493 | IDENT "coercions" -> G.IPCoercions
494 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
495 | IDENT "procedural" -> G.IPProcedural
496 | IDENT "nodefaults" -> G.IPNoDefaults
497 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
498 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
499 | IDENT "comments" -> G.IPComments
500 | IDENT "cr" -> G.IPCR
505 [ 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)
506 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
507 "done" -> BYC_weproved (ty,None,t1)
509 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
510 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
511 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
512 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
513 BYC_wehaveand (id1,t1,id2,t2)
516 rewriting_step_continuation : [
523 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
526 | G.Seq (_, l) -> l @ [ t2 ]
532 [ tac = SELF; SYMBOL ";";
533 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
534 (G.Then (loc, tac, tacs))
537 [ IDENT "do"; count = int; tac = SELF ->
538 G.Do (loc, count, tac)
539 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
543 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
545 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
547 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
549 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
550 | LPAREN; tac = SELF; RPAREN -> tac
551 | tac = tactic -> tac
554 npunctuation_tactical:
556 [ SYMBOL "[" -> G.NBranch loc
557 | SYMBOL "|" -> G.NShift loc
558 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
559 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
560 | SYMBOL "]" -> G.NMerge loc
561 | SYMBOL ";" -> G.NSemicolon loc
562 | SYMBOL "." -> G.NDot loc
565 punctuation_tactical:
567 [ SYMBOL "[" -> G.Branch loc
568 | SYMBOL "|" -> G.Shift loc
569 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
570 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
571 | SYMBOL "]" -> G.Merge loc
572 | SYMBOL ";" -> G.Semicolon loc
573 | SYMBOL "." -> G.Dot loc
576 non_punctuation_tactical:
578 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
579 | IDENT "unfocus" -> G.Unfocus loc
580 | IDENT "skip" -> G.Skip loc
584 [ [ IDENT "ndefinition" ] -> `Definition
585 | [ IDENT "nfact" ] -> `Fact
586 | [ IDENT "nlemma" ] -> `Lemma
587 | [ IDENT "nremark" ] -> `Remark
588 | [ IDENT "ntheorem" ] -> `Theorem
592 [ [ IDENT "definition" ] -> `Definition
593 | [ IDENT "fact" ] -> `Fact
594 | [ IDENT "lemma" ] -> `Lemma
595 | [ IDENT "remark" ] -> `Remark
596 | [ IDENT "theorem" ] -> `Theorem
600 [ attr = theorem_flavour -> attr
601 | [ IDENT "axiom" ] -> `Axiom
602 | [ IDENT "variant" ] -> `Variant
607 params = LIST0 protected_binder_vars;
608 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
609 fst_constructors = LIST0 constructor SEP SYMBOL "|";
612 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
613 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
614 (name, true, typ, constructors) ] SEP "with" -> types
618 (fun (names, typ) acc ->
619 (List.map (fun name -> (name, typ)) names) @ acc)
622 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
623 let tl_ind_types = match tl with None -> [] | Some types -> types in
624 let ind_types = fst_ind_type :: tl_ind_types in
630 params = LIST0 protected_binder_vars;
631 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
635 SYMBOL ":" -> false,0
636 | SYMBOL ":"; SYMBOL ">" -> true,0
637 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
640 let b,n = coercion in
642 ] SEP SYMBOL ";"; SYMBOL "}" ->
645 (fun (names, typ) acc ->
646 (List.map (fun name -> (name, typ)) names) @ acc)
649 (params,name,typ,fields)
653 [ [ IDENT "check" ]; t = term ->
655 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
656 G.Eval (loc, kind, t)
657 | IDENT "inline"; suri = QSTRING; params = inline_params ->
658 G.Inline (loc, suri, params)
659 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
660 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
661 | IDENT "auto"; params = auto_params ->
662 G.AutoInteractive (loc,params)
663 | [ IDENT "whelp"; "match" ] ; t = term ->
665 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
667 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
669 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
671 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
676 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
677 let alpha = "[a-zA-Z]" in
678 let num = "[0-9]+" in
679 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
680 let decoration = "\\'" in
681 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
682 let rex = Str.regexp ("^"^ident^"$") in
683 if Str.string_match rex id 0 then
684 if (try ignore (UriManager.uri_of_string uri); true
685 with UriManager.IllFormedUri _ -> false) ||
686 (try ignore (NReference.reference_of_string uri); true
687 with NReference.IllFormedReference _ -> false)
689 L.Ident_alias (id, uri)
692 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
694 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
695 Printf.sprintf "Not a valid identifier: %s" id)))
696 | IDENT "symbol"; symbol = QSTRING;
697 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
698 SYMBOL "="; dsc = QSTRING ->
700 match instance with Some i -> i | None -> 0
702 L.Symbol_alias (symbol, instance, dsc)
704 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
705 SYMBOL "="; dsc = QSTRING ->
707 match instance with Some i -> i | None -> 0
709 L.Number_alias (instance, dsc)
713 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
715 N.IdentArg (List.length l, id)
719 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
720 | IDENT "right"; IDENT "associative" -> Gramext.RightA
721 | IDENT "non"; IDENT "associative" -> Gramext.NonA
725 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
728 [ dir = OPT direction; s = QSTRING;
729 assoc = OPT associativity; prec = precedence;
732 [ blob = UNPARSED_AST ->
733 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
734 (CicNotationParser.parse_level2_ast
735 (Ulexing.from_utf8_string blob))
736 | blob = UNPARSED_META ->
737 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
738 (CicNotationParser.parse_level2_meta
739 (Ulexing.from_utf8_string blob))
743 | None -> default_associativity
744 | Some assoc -> assoc
747 add_raw_attribute ~text:s
748 (CicNotationParser.parse_level1_pattern prec
749 (Ulexing.from_utf8_string s))
751 (dir, p1, assoc, prec, p2)
755 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
756 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
757 | IMPLICIT -> N.ImplicitPattern
758 | id = IDENT -> N.VarPattern id
759 | LPAREN; terms = LIST1 SELF; RPAREN ->
763 | terms -> N.ApplPattern terms)
767 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
773 IDENT "include" ; path = QSTRING ->
774 loc,path,true,L.WithPreferences
775 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
776 loc,path,false,L.WithPreferences
777 | IDENT "include'" ; path = QSTRING ->
778 loc,path,true,L.WithoutPreferences
781 grafite_ncommand: [ [
782 IDENT "nqed" -> G.NQed loc
783 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
784 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
785 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
786 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
788 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
789 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
790 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
791 | NLETCOREC ; defs = let_defs ->
792 nmk_rec_corec `CoInductive defs loc
793 | NLETREC ; defs = let_defs ->
794 nmk_rec_corec `Inductive defs loc
795 | IDENT "ninductive"; spec = inductive_spec ->
796 let (params, ind_types) = spec in
797 G.NObj (loc, N.Inductive (params, ind_types))
798 | IDENT "ncoinductive"; spec = inductive_spec ->
799 let (params, ind_types) = spec in
800 let ind_types = (* set inductive flags to false (coinductive) *)
801 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
804 G.NObj (loc, N.Inductive (params, ind_types))
805 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
806 strict = [ SYMBOL <:unicode<lt>> -> true
807 | SYMBOL <:unicode<leq>> -> false ];
811 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
812 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
813 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
814 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
815 | _ -> raise (Failure "only a sort can be constrained")
819 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
820 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
821 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
822 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
823 | _ -> raise (Failure "only a sort can be constrained")
825 G.NUnivConstraint (loc, strict,u1,u2)
826 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
827 G.UnificationHint (loc, t, n)
828 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
829 G.NObj (loc, N.Record (params,name,ty,fields))
833 IDENT "set"; n = QSTRING; v = QSTRING ->
835 | IDENT "drop" -> G.Drop loc
836 | IDENT "print"; s = IDENT -> G.Print (loc,s)
837 | IDENT "qed" -> G.Qed loc
838 | IDENT "variant" ; name = IDENT; SYMBOL ":";
839 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
842 (`Variant,name,typ,Some (N.Ident (newname, None))))
843 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
844 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
845 G.Obj (loc, N.Theorem (flavour, name, typ, body))
846 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
849 N.Theorem (flavour, name, N.Implicit, Some body))
850 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
851 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
852 | LETCOREC ; defs = let_defs ->
853 mk_rec_corec `CoInductive defs loc
854 | LETREC ; defs = let_defs ->
855 mk_rec_corec `Inductive defs loc
856 | IDENT "inductive"; spec = inductive_spec ->
857 let (params, ind_types) = spec in
858 G.Obj (loc, N.Inductive (params, ind_types))
859 | IDENT "coinductive"; spec = inductive_spec ->
860 let (params, ind_types) = spec in
861 let ind_types = (* set inductive flags to false (coinductive) *)
862 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
865 G.Obj (loc, N.Inductive (params, ind_types))
867 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
868 arity = OPT int ; saturations = OPT int;
869 composites = OPT (IDENT "nocomposites") ->
870 let arity = match arity with None -> 0 | Some x -> x in
871 let saturations = match saturations with None -> 0 | Some x -> x in
872 let composites = match composites with None -> true | Some _ -> false in
874 (loc, t, composites, arity, saturations)
875 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
876 G.PreferCoercion (loc, t)
877 | IDENT "pump" ; steps = int ->
879 | IDENT "inverter"; name = IDENT; IDENT "for";
880 indty = tactic_term; paramspec = inverter_param_list ->
882 (loc, name, indty, paramspec)
883 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
884 G.Obj (loc, N.Record (params,name,ty,fields))
885 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
886 let uris = List.map UriManager.uri_of_string uris in
887 G.Default (loc,what,uris)
888 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
889 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
890 refl = tactic_term -> refl ] ;
891 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
892 sym = tactic_term -> sym ] ;
893 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
894 trans = tactic_term -> trans ] ;
896 G.Relation (loc,id,a,aeq,refl,sym,trans)
899 IDENT "alias" ; spec = alias_spec ->
901 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
902 L.Notation (loc, dir, l1, assoc, prec, l2)
903 | IDENT "interpretation"; id = QSTRING;
904 (symbol, args, l3) = interpretation ->
905 L.Interpretation (loc, id, (symbol, args), l3)
908 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
909 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
910 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
911 G.Tactic (loc, Some tac, punct)
912 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
913 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
914 G.NTactic (loc, [tac; npunct_of_punct punct])
915 | tac = ntactic; punct = punctuation_tactical ->
916 G.NTactic (loc, [tac; npunct_of_punct punct])
917 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
918 G.NTactic (loc, [punct])
919 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
920 G.NonPunctuationTactical (loc, tac, punct)
921 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
922 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
923 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
924 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
925 punct = punctuation_tactical ->
926 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
927 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
931 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
939 fun ?(never_include=false) ~include_paths status ->
940 let stm = G.Executable (loc, ex) in
941 Obj.magic !grafite_callback status stm;
944 fun ?(never_include=false) ~include_paths status ->
945 let stm = G.Comment (loc, com) in
946 Obj.magic !grafite_callback status stm;
948 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
949 fun ?(never_include=false) ~include_paths status ->
951 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
953 Obj.magic !grafite_callback status stm;
954 let _root, buri, fullpath, _rrelpath =
955 Librarian.baseuri_of_script ~include_paths fname
958 if never_include then raise (NoInclusionPerformed fullpath)
959 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
962 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
965 | scom = lexicon_command ; SYMBOL "." ->
966 fun ?(never_include=false) ~include_paths status ->
967 !lexicon_callback status scom;
968 let status = LE.eval_command status scom in
970 | EOI -> raise End_of_file
977 let _ = initialize_parser () ;;
979 let exc_located_wrapper f =
983 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
984 | Stdpp.Exc_located (floc, Stream.Error msg) ->
985 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
986 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
988 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
989 | Stdpp.Exc_located (floc, exn) ->
991 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
993 let parse_statement lexbuf =
995 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
997 let statement () = Obj.magic !grafite_parser.statement
999 let history = ref [] ;;
1002 LexiconSync.push ();
1003 history := !grafite_parser :: !history;
1004 grafite_parser := initial_parser ();
1005 initialize_parser ()
1011 | [] -> assert false
1013 grafite_parser := gp;
1017 (* vim:set foldmethod=marker: *)