1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module N = CicNotationPt
31 module LE = LexiconEngine
33 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
40 (N.term, N.term, N.term G.reduction, N.term N.obj, string) G.statement
42 type 'status statement =
43 ?never_include:bool ->
44 (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
45 include_paths:string list -> (#LE.status as 'status) ->
46 'status * ast_statement localized_option
48 type 'status parser_status = {
50 term : N.term Grammar.Entry.e;
51 statement : #LE.status as 'status statement Grammar.Entry.e;
54 let grafite_callback = ref (fun _ -> ())
55 let set_grafite_callback cb = grafite_callback := cb
57 let lexicon_callback = ref (fun _ -> ())
58 let set_lexicon_callback cb = lexicon_callback := cb
60 let initial_parser () =
61 let grammar = CicNotationParser.level2_ast_grammar () in
62 let term = CicNotationParser.term () in
63 let statement = Grammar.Entry.create grammar "statement" in
64 { grammar = grammar; term = term; statement = statement }
67 let grafite_parser = ref (initial_parser ())
69 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
71 let default_associativity = Gramext.NonA
73 let mk_rec_corec ind_kind defs loc =
74 (* In case of mutual definitions here we produce just
75 the syntax tree for the first one. The others will be
76 generated from the completely specified term just before
77 insertion in the environment. We use the flavour
78 `MutualDefinition to rememer this. *)
81 | (params,(N.Ident (name, None), ty),_,_) :: _ ->
82 let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
85 (fun var ty -> N.Binder (`Pi,var,ty)
91 let body = N.Ident (name,None) in
93 if List.length defs = 1 then
98 (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body))))
100 let nmk_rec_corec ind_kind defs loc =
101 let loc,t = mk_rec_corec ind_kind defs loc in
104 let mk_rec_corec ind_kind defs loc =
105 let loc,t = mk_rec_corec ind_kind defs loc in
108 let npunct_of_punct = function
109 | G.Branch loc -> G.NBranch loc
110 | G.Shift loc -> G.NShift loc
111 | G.Pos (loc, i) -> G.NPos (loc, i)
112 | G.Wildcard loc -> G.NWildcard loc
113 | G.Merge loc -> G.NMerge loc
114 | G.Semicolon loc -> G.NSemicolon loc
115 | G.Dot loc -> G.NDot loc
117 let nnon_punct_of_punct = function
118 | G.Skip loc -> G.NSkip loc
119 | G.Unfocus loc -> G.NUnfocus loc
120 | G.Focus (loc,l) -> G.NFocus (loc,l)
122 let npunct_of_punct = function
123 | G.Branch loc -> G.NBranch loc
124 | G.Shift loc -> G.NShift loc
125 | G.Pos (loc, i) -> G.NPos (loc, i)
126 | G.Wildcard loc -> G.NWildcard loc
127 | G.Merge loc -> G.NMerge loc
128 | G.Semicolon loc -> G.NSemicolon loc
129 | G.Dot loc -> G.NDot loc
132 type by_continuation =
134 | BYC_weproved of N.term * string option * N.term option
135 | BYC_letsuchthat of string * N.term * string * N.term
136 | BYC_wehaveand of string * N.term * string * N.term
138 let initialize_parser () =
139 (* {{{ parser initialization *)
140 let term = !grafite_parser.term in
141 let statement = !grafite_parser.statement in
142 let let_defs = CicNotationParser.let_defs () in
143 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
145 GLOBAL: term statement;
146 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
147 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
150 | id = IDENT -> Some id ]
152 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
154 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
157 [ IDENT "normalize" -> `Normalize
158 | IDENT "simplify" -> `Simpl
159 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
160 | IDENT "whd" -> `Whd ]
163 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
164 let delta = match delta with None -> true | _ -> false in
166 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
167 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
168 let delta = match delta with None -> true | _ -> false in
171 sequent_pattern_spec: [
175 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
176 (id,match path with Some p -> p | None -> N.UserInput) ];
177 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
179 match goal_path, hyp_paths with
180 None, [] -> Some N.UserInput
182 | Some goal_path, _ -> Some goal_path
191 [ "match" ; wanted = tactic_term ;
192 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
194 | sps = sequent_pattern_spec ->
197 let wanted,hyp_paths,goal_path =
198 match wanted_and_sps with
199 wanted,None -> wanted, [], Some N.UserInput
200 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
202 wanted, hyp_paths, goal_path ] ->
204 None -> None,[],Some N.UserInput
207 inverter_param_list: [
208 [ params = tactic_term ->
209 let deannotate = function
210 | N.AttributedTerm (_,t) | t -> t
211 in match deannotate params with
212 | N.Implicit _ -> [false]
213 | N.UserInput -> [true]
215 List.map (fun x -> match deannotate x with
216 | N.Implicit _ -> false
217 | N.UserInput -> true
218 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
219 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
222 [ SYMBOL ">" -> `LeftToRight
223 | SYMBOL "<" -> `RightToLeft ]
225 int: [ [ num = NUMBER -> int_of_string num ] ];
227 [ idents = OPT ident_list0 ->
228 match idents with None -> [] | Some idents -> idents
232 [ OPT [ IDENT "names" ];
233 num = OPT [ num = int -> num ];
234 idents = intros_names ->
238 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
240 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
244 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
245 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
246 SYMBOL <:unicode<def>> ; bo = tactic_term ->
248 SYMBOL <:unicode<vdash>>;
249 concl = tactic_term -> (List.rev hyps,concl) ] ->
250 G.NAssert (loc, seqs)
251 | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
252 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
253 G.NCases (loc, what, where)
254 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
255 G.NChange (loc, what, with_what)
256 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
258 (match num with None -> None | Some x -> Some (int_of_string x)),l)
259 | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
260 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
261 G.NElim (loc, what, where)
262 | IDENT "ngeneralize"; p=pattern_spec ->
263 G.NGeneralize (loc, p)
264 | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
265 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
266 where = pattern_spec ->
267 G.NLetIn (loc,where,t,name)
268 | kind = nreduction_kind; p = pattern_spec ->
269 G.NReduce (loc, kind, p)
270 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
271 G.NRewrite (loc, dir, what, where)
272 | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac)
273 | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
274 | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
275 | IDENT "nassumption" -> G.NAssumption loc
276 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
277 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
278 | SYMBOL "*" -> G.NCase1 (loc,"_")
279 | SYMBOL "*"; n=IDENT ->
284 [ IDENT "absurd"; t = tactic_term ->
286 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
288 | IDENT "apply"; t = tactic_term ->
290 | IDENT "applyP"; t = tactic_term ->
292 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
293 G.ApplyS (loc, t, params)
294 | IDENT "assumption" ->
296 | IDENT "autobatch"; params = auto_params ->
297 G.AutoBatch (loc,params)
298 | IDENT "cases"; what = tactic_term;
299 pattern = OPT pattern_spec;
300 specs = intros_spec ->
301 let pattern = match pattern with
302 | None -> None, [], Some N.UserInput
303 | Some pattern -> pattern
305 G.Cases (loc, what, pattern, specs)
306 | IDENT "clear"; ids = LIST1 IDENT ->
308 | IDENT "clearbody"; id = IDENT ->
310 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
311 G.Change (loc, what, t)
312 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
313 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
314 let times = match times with None -> 1 | Some i -> i in
315 G.Compose (loc, t1, t2, times, specs)
316 | IDENT "constructor"; n = int ->
317 G.Constructor (loc, n)
318 | IDENT "contradiction" ->
320 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
321 G.Cut (loc, ident, t)
322 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
323 let idents = match idents with None -> [] | Some idents -> idents in
324 G.Decompose (loc, idents)
325 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
326 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
327 G.Destruct (loc, xts)
328 | IDENT "elim"; what = tactic_term; using = using;
329 pattern = OPT pattern_spec;
330 ispecs = intros_spec ->
331 let pattern = match pattern with
332 | None -> None, [], Some N.UserInput
333 | Some pattern -> pattern
335 G.Elim (loc, what, using, pattern, ispecs)
336 | IDENT "elimType"; what = tactic_term; using = using;
337 (num, idents) = intros_spec ->
338 G.ElimType (loc, what, using, (num, idents))
339 | IDENT "exact"; t = tactic_term ->
343 | IDENT "fail" -> G.Fail loc
344 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
347 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
348 ("the pattern cannot specify the term to replace, only its"
349 ^ " paths in the hypotheses and in the conclusion")))
351 G.Fold (loc, kind, t, p)
354 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
355 let idents = match idents with None -> [] | Some idents -> idents in
356 G.FwdSimpl (loc, hyp, idents)
357 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
358 G.Generalize (loc,p,id)
359 | IDENT "id" -> G.IdTac loc
360 | IDENT "intro"; ident = OPT IDENT ->
361 let idents = match ident with None -> [] | Some id -> [Some id] in
362 G.Intros (loc, (Some 1, idents))
363 | IDENT "intros"; specs = intros_spec ->
364 G.Intros (loc, specs)
365 | IDENT "inversion"; t = tactic_term ->
368 linear = OPT [ IDENT "linear" ];
369 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
371 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
372 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
373 let linear = match linear with None -> false | Some _ -> true in
374 let to_what = match to_what with None -> [] | Some to_what -> to_what in
375 G.LApply (loc, linear, depth, to_what, what, ident)
376 | IDENT "left" -> G.Left loc
377 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
378 G.LetIn (loc, t, where)
379 | kind = reduction_kind; p = pattern_spec ->
380 G.Reduce (loc, kind, p)
381 | IDENT "reflexivity" ->
383 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
384 G.Replace (loc, p, t)
385 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
386 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
390 (HExtlib.Localized (loc,
391 (CicNotationParser.Parse_error
392 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
394 let n = match xnames with None -> [] | Some names -> names in
395 G.Rewrite (loc, d, t, p, n)
402 | IDENT "symmetry" ->
404 | IDENT "transitivity"; t = tactic_term ->
405 G.Transitivity (loc, t)
406 (* Produzioni Aggiunte *)
407 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
408 G.Assume (loc, id, t)
409 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
410 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
411 t' = tactic_term -> t']->
412 G.Suppose (loc, t, id, t1)
413 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
414 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
415 id2 = IDENT ; RPAREN ->
416 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
418 [ IDENT "using"; t=tactic_term -> `Term t
419 | params = auto_params -> `Auto params] ;
420 cont=by_continuation ->
422 BYC_done -> G.Bydone (loc, just)
423 | BYC_weproved (ty,id,t1) ->
424 G.By_just_we_proved(loc, just, ty, id, t1)
425 | BYC_letsuchthat (id1,t1,id2,t2) ->
426 G.ExistsElim (loc, just, id1, t1, id2, t2)
427 | BYC_wehaveand (id1,t1,id2,t2) ->
428 G.AndElim (loc, just, id1, t1, id2, t2))
429 | 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']->
430 G.We_need_to_prove (loc, t, id, t1)
431 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
432 G.We_proceed_by_cases_on (loc, t, t1)
433 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
434 G.We_proceed_by_induction_on (loc, t, t1)
435 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
436 G.Byinduction(loc, t, id)
437 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
438 G.Thesisbecomes(loc, t)
439 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
440 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
441 G.Case(loc,id,params)
442 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
444 termine = tactic_term;
448 [ IDENT "using"; t=tactic_term -> `Term t
449 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
450 | IDENT "proof" -> `Proof
451 | params = auto_params -> `Auto params];
452 cont = rewriting_step_continuation ->
453 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
454 | IDENT "obtain" ; name = IDENT;
455 termine = tactic_term;
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, Some (Some name,termine), t1, t2, cont)
468 [ IDENT "using"; t=tactic_term -> `Term t
469 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
470 | IDENT "proof" -> `Proof
471 | params = auto_params -> `Auto params];
472 cont = rewriting_step_continuation ->
473 G.RewritingStep(loc, None, t1, t2, cont)
477 [ IDENT "paramodulation"
490 i = auto_fixed_param -> i,""
491 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
492 string_of_int v | v = IDENT -> v ] -> i,v ];
493 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
494 (match tl with Some l -> l | None -> []),
500 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
501 | flavour = inline_flavour -> G.IPAs flavour
502 | IDENT "coercions" -> G.IPCoercions
503 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
504 | IDENT "procedural" -> G.IPProcedural
505 | IDENT "nodefaults" -> G.IPNoDefaults
506 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
507 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
508 | IDENT "comments" -> G.IPComments
509 | IDENT "cr" -> G.IPCR
514 [ 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)
515 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
516 "done" -> BYC_weproved (ty,None,t1)
518 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
519 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
520 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
521 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
522 BYC_wehaveand (id1,t1,id2,t2)
525 rewriting_step_continuation : [
532 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
535 | G.Seq (_, l) -> l @ [ t2 ]
541 [ tac = SELF; SYMBOL ";";
542 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
543 (G.Then (loc, tac, tacs))
546 [ IDENT "do"; count = int; tac = SELF ->
547 G.Do (loc, count, tac)
548 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
552 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
554 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
556 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
558 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
559 | LPAREN; tac = SELF; RPAREN -> tac
560 | tac = tactic -> tac
563 npunctuation_tactical:
565 [ SYMBOL "[" -> G.NBranch loc
566 | SYMBOL "|" -> G.NShift loc
567 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
568 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
569 | SYMBOL "]" -> G.NMerge loc
570 | SYMBOL ";" -> G.NSemicolon loc
571 | SYMBOL "." -> G.NDot loc
574 punctuation_tactical:
576 [ SYMBOL "[" -> G.Branch loc
577 | SYMBOL "|" -> G.Shift loc
578 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
579 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
580 | SYMBOL "]" -> G.Merge loc
581 | SYMBOL ";" -> G.Semicolon loc
582 | SYMBOL "." -> G.Dot loc
585 non_punctuation_tactical:
587 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
588 | IDENT "unfocus" -> G.Unfocus loc
589 | IDENT "skip" -> G.Skip loc
593 [ [ IDENT "ndefinition" ] -> `Definition
594 | [ IDENT "nfact" ] -> `Fact
595 | [ IDENT "nlemma" ] -> `Lemma
596 | [ IDENT "nremark" ] -> `Remark
597 | [ IDENT "ntheorem" ] -> `Theorem
601 [ [ IDENT "definition" ] -> `Definition
602 | [ IDENT "fact" ] -> `Fact
603 | [ IDENT "lemma" ] -> `Lemma
604 | [ IDENT "remark" ] -> `Remark
605 | [ IDENT "theorem" ] -> `Theorem
609 [ attr = theorem_flavour -> attr
610 | [ IDENT "axiom" ] -> `Axiom
611 | [ IDENT "variant" ] -> `Variant
616 params = LIST0 protected_binder_vars;
617 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
618 fst_constructors = LIST0 constructor SEP SYMBOL "|";
621 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
622 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
623 (name, true, typ, constructors) ] SEP "with" -> types
627 (fun (names, typ) acc ->
628 (List.map (fun name -> (name, typ)) names) @ acc)
631 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
632 let tl_ind_types = match tl with None -> [] | Some types -> types in
633 let ind_types = fst_ind_type :: tl_ind_types in
639 params = LIST0 protected_binder_vars;
640 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
644 SYMBOL ":" -> false,0
645 | SYMBOL ":"; SYMBOL ">" -> true,0
646 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
649 let b,n = coercion in
651 ] SEP SYMBOL ";"; SYMBOL "}" ->
654 (fun (names, typ) acc ->
655 (List.map (fun name -> (name, typ)) names) @ acc)
658 (params,name,typ,fields)
662 [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
667 [ [ IDENT "check" ]; t = term ->
669 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
670 G.Eval (loc, kind, t)
671 | IDENT "inline"; suri = QSTRING; params = inline_params ->
672 G.Inline (loc, suri, params)
673 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
674 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
675 | IDENT "auto"; params = auto_params ->
676 G.AutoInteractive (loc,params)
677 | [ IDENT "whelp"; "match" ] ; t = term ->
679 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
681 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
683 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
685 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
690 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
691 let alpha = "[a-zA-Z]" in
692 let num = "[0-9]+" in
693 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
694 let decoration = "\\'" in
695 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
696 let rex = Str.regexp ("^"^ident^"$") in
697 if Str.string_match rex id 0 then
698 if (try ignore (UriManager.uri_of_string uri); true
699 with UriManager.IllFormedUri _ -> false) ||
700 (try ignore (NReference.reference_of_string uri); true
701 with NReference.IllFormedReference _ -> false)
703 L.Ident_alias (id, uri)
706 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
708 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
709 Printf.sprintf "Not a valid identifier: %s" id)))
710 | IDENT "symbol"; symbol = QSTRING;
711 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
712 SYMBOL "="; dsc = QSTRING ->
714 match instance with Some i -> i | None -> 0
716 L.Symbol_alias (symbol, instance, dsc)
718 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
719 SYMBOL "="; dsc = QSTRING ->
721 match instance with Some i -> i | None -> 0
723 L.Number_alias (instance, dsc)
727 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
729 N.IdentArg (List.length l, id)
733 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
734 | IDENT "right"; IDENT "associative" -> Gramext.RightA
735 | IDENT "non"; IDENT "associative" -> Gramext.NonA
739 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
742 [ dir = OPT direction; s = QSTRING;
743 assoc = OPT associativity; prec = precedence;
746 [ blob = UNPARSED_AST ->
747 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
748 (CicNotationParser.parse_level2_ast
749 (Ulexing.from_utf8_string blob))
750 | blob = UNPARSED_META ->
751 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
752 (CicNotationParser.parse_level2_meta
753 (Ulexing.from_utf8_string blob))
757 | None -> default_associativity
758 | Some assoc -> assoc
761 add_raw_attribute ~text:s
762 (CicNotationParser.parse_level1_pattern prec
763 (Ulexing.from_utf8_string s))
765 (dir, p1, assoc, prec, p2)
769 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
770 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
771 | IMPLICIT -> N.ImplicitPattern
772 | id = IDENT -> N.VarPattern id
773 | LPAREN; terms = LIST1 SELF; RPAREN ->
777 | terms -> N.ApplPattern terms)
781 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
787 IDENT "include" ; path = QSTRING ->
788 loc,path,true,L.WithPreferences
789 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
790 loc,path,false,L.WithPreferences
791 | IDENT "include'" ; path = QSTRING ->
792 loc,path,true,L.WithoutPreferences
795 grafite_ncommand: [ [
796 IDENT "nqed" -> G.NQed loc
797 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
798 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
799 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
800 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
802 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body))
803 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
804 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
805 | NLETCOREC ; defs = let_defs ->
806 nmk_rec_corec `CoInductive defs loc
807 | NLETREC ; defs = let_defs ->
808 nmk_rec_corec `Inductive defs loc
809 | IDENT "ninductive"; spec = inductive_spec ->
810 let (params, ind_types) = spec in
811 G.NObj (loc, N.Inductive (params, ind_types))
812 | IDENT "ncoinductive"; spec = inductive_spec ->
813 let (params, ind_types) = spec in
814 let ind_types = (* set inductive flags to false (coinductive) *)
815 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
818 G.NObj (loc, N.Inductive (params, ind_types))
819 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
820 strict = [ SYMBOL <:unicode<lt>> -> true
821 | SYMBOL <:unicode<leq>> -> false ];
825 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
826 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
827 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
828 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
829 | _ -> raise (Failure "only a sort can be constrained")
833 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
834 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
835 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
836 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
837 | _ -> raise (Failure "only a sort can be constrained")
839 G.NUnivConstraint (loc, strict,u1,u2)
840 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
841 G.UnificationHint (loc, t, n)
842 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
843 SYMBOL <:unicode<def>>; t = term; "on";
844 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
845 "to"; target = term ->
846 G.NCoercion(loc,name,t,ty,(id,source),target)
847 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
848 G.NObj (loc, N.Record (params,name,ty,fields))
849 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
850 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
851 G.NCopy (loc,s,NUri.uri_of_string u,
852 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
856 IDENT "set"; n = QSTRING; v = QSTRING ->
858 | IDENT "drop" -> G.Drop loc
859 | IDENT "print"; s = IDENT -> G.Print (loc,s)
860 | IDENT "qed" -> G.Qed loc
861 | IDENT "variant" ; name = IDENT; SYMBOL ":";
862 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
865 (`Variant,name,typ,Some (N.Ident (newname, None))))
866 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
867 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
868 G.Obj (loc, N.Theorem (flavour, name, typ, body))
869 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
872 N.Theorem (flavour, name, N.Implicit `JustOne, Some body))
873 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
874 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
875 | LETCOREC ; defs = let_defs ->
876 mk_rec_corec `CoInductive defs loc
877 | LETREC ; defs = let_defs ->
878 mk_rec_corec `Inductive defs loc
879 | IDENT "inductive"; spec = inductive_spec ->
880 let (params, ind_types) = spec in
881 G.Obj (loc, N.Inductive (params, ind_types))
882 | IDENT "coinductive"; spec = inductive_spec ->
883 let (params, ind_types) = spec in
884 let ind_types = (* set inductive flags to false (coinductive) *)
885 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
888 G.Obj (loc, N.Inductive (params, ind_types))
890 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
891 arity = OPT int ; saturations = OPT int;
892 composites = OPT (IDENT "nocomposites") ->
893 let arity = match arity with None -> 0 | Some x -> x in
894 let saturations = match saturations with None -> 0 | Some x -> x in
895 let composites = match composites with None -> true | Some _ -> false in
897 (loc, t, composites, arity, saturations)
898 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
899 G.PreferCoercion (loc, t)
900 | IDENT "pump" ; steps = int ->
902 | IDENT "inverter"; name = IDENT; IDENT "for";
903 indty = tactic_term; paramspec = inverter_param_list ->
905 (loc, name, indty, paramspec)
906 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
907 G.Obj (loc, N.Record (params,name,ty,fields))
908 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
909 let uris = List.map UriManager.uri_of_string uris in
910 G.Default (loc,what,uris)
911 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
912 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
913 refl = tactic_term -> refl ] ;
914 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
915 sym = tactic_term -> sym ] ;
916 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
917 trans = tactic_term -> trans ] ;
919 G.Relation (loc,id,a,aeq,refl,sym,trans)
922 IDENT "alias" ; spec = alias_spec ->
924 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
925 L.Notation (loc, dir, l1, assoc, prec, l2)
926 | IDENT "interpretation"; id = QSTRING;
927 (symbol, args, l3) = interpretation ->
928 L.Interpretation (loc, id, (symbol, args), l3)
931 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
932 | ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
933 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
934 G.Tactic (loc, Some tac, punct)
935 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
936 | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
937 G.NTactic (loc, [tac; npunct_of_punct punct])
938 | tac = ntactic; punct = punctuation_tactical ->
939 G.NTactic (loc, [tac; npunct_of_punct punct])
940 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
941 G.NTactic (loc, [punct])
942 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
943 G.NonPunctuationTactical (loc, tac, punct)
944 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
945 SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
946 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
947 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical;
948 punct = punctuation_tactical ->
949 G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
950 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
951 | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
955 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
963 fun ?(never_include=false) ~include_paths status ->
964 let stm = G.Executable (loc, ex) in
965 !grafite_callback stm;
968 fun ?(never_include=false) ~include_paths status ->
969 let stm = G.Comment (loc, com) in
970 !grafite_callback stm;
972 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
973 fun ?(never_include=false) ~include_paths status ->
974 let _root, buri, fullpath, _rrelpath =
975 Librarian.baseuri_of_script ~include_paths fname in
976 if never_include then raise (NoInclusionPerformed fullpath)
981 (loc, G.Command (loc, G.Include (iloc,normal,`OldAndNew,fname))) in
982 !grafite_callback stm;
984 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
987 (loc,G.Command (loc,G.Include (iloc,normal,`OldAndNew,buri)))
991 | scom = lexicon_command ; SYMBOL "." ->
992 fun ?(never_include=false) ~include_paths status ->
993 !lexicon_callback scom;
994 let status = LE.eval_command status scom in
996 | EOI -> raise End_of_file
1003 let _ = initialize_parser () ;;
1005 let exc_located_wrapper f =
1009 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
1010 | Stdpp.Exc_located (floc, Stream.Error msg) ->
1011 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
1012 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
1014 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1015 | Stdpp.Exc_located (floc, exn) ->
1017 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
1019 let parse_statement lexbuf =
1021 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
1023 let statement () = Obj.magic !grafite_parser.statement
1025 let history = ref [] ;;
1028 LexiconSync.push ();
1029 history := !grafite_parser :: !history;
1030 grafite_parser := initial_parser ();
1031 initialize_parser ()
1037 | [] -> assert false
1039 grafite_parser := gp;
1043 (* vim:set foldmethod=marker: *)