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
43 ?never_include:bool -> include_paths:string list -> LE.status ->
44 LE.status * ast_statement localized_option
46 type parser_status = {
48 term : N.term Grammar.Entry.e;
49 statement : statement Grammar.Entry.e;
52 let grafite_callback = ref (fun _ _ -> ())
53 let set_grafite_callback cb = grafite_callback := cb
55 let lexicon_callback = ref (fun _ _ -> ())
56 let set_lexicon_callback cb = lexicon_callback := cb
58 let initial_parser () =
59 let grammar = CicNotationParser.level2_ast_grammar () in
60 let term = CicNotationParser.term () in
61 let statement = Grammar.Entry.create grammar "statement" in
62 { grammar = grammar; term = term; statement = statement }
65 let grafite_parser = ref (initial_parser ())
67 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
69 let default_associativity = Gramext.NonA
71 let mk_rec_corec ng ind_kind defs loc =
72 (* In case of mutual definitions here we produce just
73 the syntax tree for the first one. The others will be
74 generated from the completely specified term just before
75 insertion in the environment. We use the flavour
76 `MutualDefinition to rememer this. *)
79 | (params,(N.Ident (name, None), Some ty),_,_) :: _ ->
82 (fun var ty -> N.Binder (`Pi,var,ty)
86 | (_,(N.Ident (name, None), None),_,_) :: _ ->
90 let body = N.Ident (name,None) in
92 if List.length defs = 1 then
98 G.NObj (loc, N.Theorem(flavour, name, ty,
99 Some (N.LetRec (ind_kind, defs, body))))
101 G.Obj (loc, N.Theorem(flavour, name, ty,
102 Some (N.LetRec (ind_kind, defs, body))))
104 type by_continuation =
106 | BYC_weproved of N.term * string option * N.term option
107 | BYC_letsuchthat of string * N.term * string * N.term
108 | BYC_wehaveand of string * N.term * string * N.term
110 let initialize_parser () =
111 (* {{{ parser initialization *)
112 let term = !grafite_parser.term in
113 let statement = !grafite_parser.statement in
114 let let_defs = CicNotationParser.let_defs () in
115 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
117 GLOBAL: term statement;
118 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
119 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
122 | id = IDENT -> Some id ]
124 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
126 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
129 [ IDENT "normalize" -> `Normalize
130 | IDENT "simplify" -> `Simpl
131 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
132 | IDENT "whd" -> `Whd ]
135 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
136 let delta = match delta with None -> true | _ -> false in
138 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
139 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
140 let delta = match delta with None -> true | _ -> false in
143 sequent_pattern_spec: [
147 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
148 (id,match path with Some p -> p | None -> N.UserInput) ];
149 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
151 match goal_path, hyp_paths with
152 None, [] -> Some N.UserInput
154 | Some goal_path, _ -> Some goal_path
163 [ "match" ; wanted = tactic_term ;
164 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
166 | sps = sequent_pattern_spec ->
169 let wanted,hyp_paths,goal_path =
170 match wanted_and_sps with
171 wanted,None -> wanted, [], Some N.UserInput
172 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
174 wanted, hyp_paths, goal_path ] ->
176 None -> None,[],Some N.UserInput
179 inverter_param_list: [
180 [ params = tactic_term ->
181 let deannotate = function
182 | N.AttributedTerm (_,t) | t -> t
183 in match deannotate params with
184 | N.Implicit -> [false]
185 | N.UserInput -> [true]
187 List.map (fun x -> match deannotate x with
188 | N.Implicit -> false
189 | N.UserInput -> true
190 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
191 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
194 [ SYMBOL ">" -> `LeftToRight
195 | SYMBOL "<" -> `RightToLeft ]
197 int: [ [ num = NUMBER -> int_of_string num ] ];
199 [ idents = OPT ident_list0 ->
200 match idents with None -> [] | Some idents -> idents
204 [ OPT [ IDENT "names" ];
205 num = OPT [ num = int -> num ];
206 idents = intros_names ->
210 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
212 [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
216 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
217 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
218 SYMBOL <:unicode<def>> ; bo = tactic_term ->
220 SYMBOL <:unicode<vdash>>;
221 concl = tactic_term -> (List.rev hyps,concl) ] ->
222 G.NAssert (loc, seqs)
223 | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
224 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
225 G.NCases (loc, what, where)
226 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
227 G.NChange (loc, what, with_what)
228 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
229 G.NElim (loc, what, where)
230 | IDENT "ngeneralize"; p=pattern_spec ->
231 G.NGeneralize (loc, p)
232 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
233 where = pattern_spec ->
234 G.NLetIn (loc,where,t,name)
235 | kind = nreduction_kind; p = pattern_spec ->
236 G.NReduce (loc, kind, p)
237 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
238 G.NRewrite (loc, dir, what, where)
239 | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
240 | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
241 | SYMBOL "*" -> G.NCase1 (loc,"_")
242 | SYMBOL "*"; n=IDENT ->
247 [ IDENT "absurd"; t = tactic_term ->
249 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
251 | IDENT "apply"; t = tactic_term ->
253 | IDENT "applyP"; t = tactic_term ->
255 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
256 G.ApplyS (loc, t, params)
257 | IDENT "assumption" ->
259 | IDENT "autobatch"; params = auto_params ->
260 G.AutoBatch (loc,params)
261 | IDENT "cases"; what = tactic_term;
262 pattern = OPT pattern_spec;
263 specs = intros_spec ->
264 let pattern = match pattern with
265 | None -> None, [], Some N.UserInput
266 | Some pattern -> pattern
268 G.Cases (loc, what, pattern, specs)
269 | IDENT "clear"; ids = LIST1 IDENT ->
271 | IDENT "clearbody"; id = IDENT ->
273 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
274 G.Change (loc, what, t)
275 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
276 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
277 let times = match times with None -> 1 | Some i -> i in
278 G.Compose (loc, t1, t2, times, specs)
279 | IDENT "constructor"; n = int ->
280 G.Constructor (loc, n)
281 | IDENT "contradiction" ->
283 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
284 G.Cut (loc, ident, t)
285 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
286 let idents = match idents with None -> [] | Some idents -> idents in
287 G.Decompose (loc, idents)
288 | IDENT "demodulate"; p = auto_params -> G.Demodulate (loc, p)
289 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
290 G.Destruct (loc, xts)
291 | IDENT "elim"; what = tactic_term; using = using;
292 pattern = OPT pattern_spec;
293 ispecs = intros_spec ->
294 let pattern = match pattern with
295 | None -> None, [], Some N.UserInput
296 | Some pattern -> pattern
298 G.Elim (loc, what, using, pattern, ispecs)
299 | IDENT "elimType"; what = tactic_term; using = using;
300 (num, idents) = intros_spec ->
301 G.ElimType (loc, what, using, (num, idents))
302 | IDENT "exact"; t = tactic_term ->
306 | IDENT "fail" -> G.Fail loc
307 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
310 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
311 ("the pattern cannot specify the term to replace, only its"
312 ^ " paths in the hypotheses and in the conclusion")))
314 G.Fold (loc, kind, t, p)
317 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
318 let idents = match idents with None -> [] | Some idents -> idents in
319 G.FwdSimpl (loc, hyp, idents)
320 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
321 G.Generalize (loc,p,id)
322 | IDENT "id" -> G.IdTac loc
323 | IDENT "intro"; ident = OPT IDENT ->
324 let idents = match ident with None -> [] | Some id -> [Some id] in
325 G.Intros (loc, (Some 1, idents))
326 | IDENT "intros"; specs = intros_spec ->
327 G.Intros (loc, specs)
328 | IDENT "inversion"; t = tactic_term ->
331 linear = OPT [ IDENT "linear" ];
332 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
334 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
335 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
336 let linear = match linear with None -> false | Some _ -> true in
337 let to_what = match to_what with None -> [] | Some to_what -> to_what in
338 G.LApply (loc, linear, depth, to_what, what, ident)
339 | IDENT "left" -> G.Left loc
340 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
341 G.LetIn (loc, t, where)
342 | kind = reduction_kind; p = pattern_spec ->
343 G.Reduce (loc, kind, p)
344 | IDENT "reflexivity" ->
346 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
347 G.Replace (loc, p, t)
348 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
349 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
353 (HExtlib.Localized (loc,
354 (CicNotationParser.Parse_error
355 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
357 let n = match xnames with None -> [] | Some names -> names in
358 G.Rewrite (loc, d, t, p, n)
365 | IDENT "symmetry" ->
367 | IDENT "transitivity"; t = tactic_term ->
368 G.Transitivity (loc, t)
369 (* Produzioni Aggiunte *)
370 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
371 G.Assume (loc, id, t)
372 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
373 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
374 t' = tactic_term -> t']->
375 G.Suppose (loc, t, id, t1)
376 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
377 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
378 id2 = IDENT ; RPAREN ->
379 G.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
381 [ IDENT "using"; t=tactic_term -> `Term t
382 | params = auto_params -> `Auto params] ;
383 cont=by_continuation ->
385 BYC_done -> G.Bydone (loc, just)
386 | BYC_weproved (ty,id,t1) ->
387 G.By_just_we_proved(loc, just, ty, id, t1)
388 | BYC_letsuchthat (id1,t1,id2,t2) ->
389 G.ExistsElim (loc, just, id1, t1, id2, t2)
390 | BYC_wehaveand (id1,t1,id2,t2) ->
391 G.AndElim (loc, just, id1, t1, id2, t2))
392 | 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']->
393 G.We_need_to_prove (loc, t, id, t1)
394 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
395 G.We_proceed_by_cases_on (loc, t, t1)
396 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
397 G.We_proceed_by_induction_on (loc, t, t1)
398 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
399 G.Byinduction(loc, t, id)
400 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
401 G.Thesisbecomes(loc, t)
402 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
403 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
404 G.Case(loc,id,params)
405 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
407 termine = tactic_term;
411 [ IDENT "using"; t=tactic_term -> `Term t
412 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
413 | IDENT "proof" -> `Proof
414 | params = auto_params -> `Auto params];
415 cont = rewriting_step_continuation ->
416 G.RewritingStep(loc, Some (None,termine), t1, t2, cont)
417 | IDENT "obtain" ; name = IDENT;
418 termine = tactic_term;
422 [ IDENT "using"; t=tactic_term -> `Term t
423 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
424 | IDENT "proof" -> `Proof
425 | params = auto_params -> `Auto params];
426 cont = rewriting_step_continuation ->
427 G.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
431 [ IDENT "using"; t=tactic_term -> `Term t
432 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
433 | IDENT "proof" -> `Proof
434 | params = auto_params -> `Auto params];
435 cont = rewriting_step_continuation ->
436 G.RewritingStep(loc, None, t1, t2, cont)
440 [ IDENT "paramodulation"
453 i = auto_fixed_param -> i,""
454 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
455 string_of_int v | v = IDENT -> v ] -> i,v ];
456 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
457 (match tl with Some l -> l | None -> []),
463 [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix
464 | flavour = inline_flavour -> G.IPAs flavour
465 | IDENT "procedural" -> G.IPProcedural
466 | IDENT "nodefaults" -> G.IPNoDefaults
467 | IDENT "depth"; SYMBOL "="; depth = int -> G.IPDepth depth
468 | IDENT "level"; SYMBOL "="; level = int -> G.IPLevel level
469 | IDENT "comments" -> G.IPComments
470 | IDENT "coercions" -> G.IPCoercions
471 | IDENT "debug"; SYMBOL "="; debug = int -> G.IPDebug debug
476 [ 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)
477 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
478 "done" -> BYC_weproved (ty,None,t1)
480 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
481 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
482 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
483 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
484 BYC_wehaveand (id1,t1,id2,t2)
487 rewriting_step_continuation : [
494 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
497 | G.Seq (_, l) -> l @ [ t2 ]
503 [ tac = SELF; SYMBOL ";";
504 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
505 (G.Then (loc, tac, tacs))
508 [ IDENT "do"; count = int; tac = SELF ->
509 G.Do (loc, count, tac)
510 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
514 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
516 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
518 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
520 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
521 | LPAREN; tac = SELF; RPAREN -> tac
522 | tac = tactic -> tac
525 punctuation_tactical:
527 [ SYMBOL "[" -> G.Branch loc
528 | SYMBOL "|" -> G.Shift loc
529 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.Pos (loc, i)
530 | SYMBOL "*"; SYMBOL ":" -> G.Wildcard loc
531 | SYMBOL "]" -> G.Merge loc
532 | SYMBOL ";" -> G.Semicolon loc
533 | SYMBOL "." -> G.Dot loc
536 non_punctuation_tactical:
538 [ IDENT "focus"; goals = LIST1 int -> G.Focus (loc, goals)
539 | IDENT "unfocus" -> G.Unfocus loc
540 | IDENT "skip" -> G.Skip loc
544 [ [ IDENT "ndefinition" ] -> `Definition
545 | [ IDENT "nfact" ] -> `Fact
546 | [ IDENT "nlemma" ] -> `Lemma
547 | [ IDENT "nremark" ] -> `Remark
548 | [ IDENT "ntheorem" ] -> `Theorem
552 [ [ IDENT "definition" ] -> `Definition
553 | [ IDENT "fact" ] -> `Fact
554 | [ IDENT "lemma" ] -> `Lemma
555 | [ IDENT "remark" ] -> `Remark
556 | [ IDENT "theorem" ] -> `Theorem
560 [ attr = theorem_flavour -> attr
561 | [ IDENT "axiom" ] -> `Axiom
562 | [ IDENT "variant" ] -> `Variant
567 params = LIST0 protected_binder_vars;
568 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
569 fst_constructors = LIST0 constructor SEP SYMBOL "|";
572 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
573 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
574 (name, true, typ, constructors) ] SEP "with" -> types
578 (fun (names, typ) acc ->
579 (List.map (fun name -> (name, typ)) names) @ acc)
582 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
583 let tl_ind_types = match tl with None -> [] | Some types -> types in
584 let ind_types = fst_ind_type :: tl_ind_types in
590 params = LIST0 protected_binder_vars;
591 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
595 SYMBOL ":" -> false,0
596 | SYMBOL ":"; SYMBOL ">" -> true,0
597 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
600 let b,n = coercion in
602 ] SEP SYMBOL ";"; SYMBOL "}" ->
605 (fun (names, typ) acc ->
606 (List.map (fun name -> (name, typ)) names) @ acc)
609 (params,name,typ,fields)
613 [ [ IDENT "check" ]; t = term ->
615 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
616 G.Eval (loc, kind, t)
617 | IDENT "inline"; suri = QSTRING; params = inline_params ->
618 G.Inline (loc, suri, params)
619 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
620 if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
621 | IDENT "auto"; params = auto_params ->
622 G.AutoInteractive (loc,params)
623 | [ IDENT "whelp"; "match" ] ; t = term ->
625 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
627 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
629 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
631 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
636 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
637 let alpha = "[a-zA-Z]" in
638 let num = "[0-9]+" in
639 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
640 let decoration = "\\'" in
641 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
642 let rex = Str.regexp ("^"^ident^"$") in
643 if Str.string_match rex id 0 then
644 if (try ignore (UriManager.uri_of_string uri); true
645 with UriManager.IllFormedUri _ -> false) ||
646 (try ignore (NReference.reference_of_string uri); true
647 with NReference.IllFormedReference _ -> false)
649 L.Ident_alias (id, uri)
652 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
654 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
655 Printf.sprintf "Not a valid identifier: %s" id)))
656 | IDENT "symbol"; symbol = QSTRING;
657 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
658 SYMBOL "="; dsc = QSTRING ->
660 match instance with Some i -> i | None -> 0
662 L.Symbol_alias (symbol, instance, dsc)
664 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
665 SYMBOL "="; dsc = QSTRING ->
667 match instance with Some i -> i | None -> 0
669 L.Number_alias (instance, dsc)
673 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
675 N.IdentArg (List.length l, id)
679 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
680 | IDENT "right"; IDENT "associative" -> Gramext.RightA
681 | IDENT "non"; IDENT "associative" -> Gramext.NonA
685 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
688 [ dir = OPT direction; s = QSTRING;
689 assoc = OPT associativity; prec = precedence;
692 [ blob = UNPARSED_AST ->
693 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
694 (CicNotationParser.parse_level2_ast
695 (Ulexing.from_utf8_string blob))
696 | blob = UNPARSED_META ->
697 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
698 (CicNotationParser.parse_level2_meta
699 (Ulexing.from_utf8_string blob))
703 | None -> default_associativity
704 | Some assoc -> assoc
707 add_raw_attribute ~text:s
708 (CicNotationParser.parse_level1_pattern prec
709 (Ulexing.from_utf8_string s))
711 (dir, p1, assoc, prec, p2)
715 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
716 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
717 | IMPLICIT -> N.ImplicitPattern
718 | id = IDENT -> N.VarPattern id
719 | LPAREN; terms = LIST1 SELF; RPAREN ->
723 | terms -> N.ApplPattern terms)
727 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
733 IDENT "include" ; path = QSTRING ->
734 loc,path,true,L.WithPreferences
735 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
736 loc,path,false,L.WithPreferences
737 | IDENT "include'" ; path = QSTRING ->
738 loc,path,true,L.WithoutPreferences
742 IDENT "set"; n = QSTRING; v = QSTRING ->
744 | IDENT "drop" -> G.Drop loc
745 | IDENT "print"; s = IDENT -> G.Print (loc,s)
746 | IDENT "qed" -> G.Qed loc
747 | IDENT "nqed" -> G.NQed loc
748 | IDENT "variant" ; name = IDENT; SYMBOL ":";
749 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
752 (`Variant,name,typ,Some (N.Ident (newname, None))))
753 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
754 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
755 G.NObj (loc, N.Theorem (nflavour, name, typ, body))
756 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
758 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit, Some body))
759 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
760 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
761 G.Obj (loc, N.Theorem (flavour, name, typ, body))
762 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
765 N.Theorem (flavour, name, N.Implicit, Some body))
766 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
767 G.Obj (loc, N.Theorem (`Axiom, name, typ, None))
768 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
769 G.NObj (loc, N.Theorem (`Axiom, name, typ, None))
770 | LETCOREC ; defs = let_defs ->
771 mk_rec_corec false `CoInductive defs loc
772 | LETREC ; defs = let_defs ->
773 mk_rec_corec false `Inductive defs loc
774 | NLETCOREC ; defs = let_defs ->
775 mk_rec_corec true `CoInductive defs loc
776 | NLETREC ; defs = let_defs ->
777 mk_rec_corec true `Inductive defs loc
778 | IDENT "inductive"; spec = inductive_spec ->
779 let (params, ind_types) = spec in
780 G.Obj (loc, N.Inductive (params, ind_types))
781 | IDENT "ninductive"; spec = inductive_spec ->
782 let (params, ind_types) = spec in
783 G.NObj (loc, N.Inductive (params, ind_types))
784 | IDENT "coinductive"; spec = inductive_spec ->
785 let (params, ind_types) = spec in
786 let ind_types = (* set inductive flags to false (coinductive) *)
787 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
790 G.Obj (loc, N.Inductive (params, ind_types))
791 | IDENT "ncoinductive"; spec = inductive_spec ->
792 let (params, ind_types) = spec in
793 let ind_types = (* set inductive flags to false (coinductive) *)
794 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
797 G.NObj (loc, N.Inductive (params, ind_types))
798 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
799 strict = [ SYMBOL <:unicode<lt>> -> true
800 | SYMBOL <:unicode<leq>> -> false ];
804 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
805 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
806 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
807 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
808 | _ -> raise (Failure "only a sort can be constrained")
812 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NType i)) ->
813 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
814 | CicNotationPt.AttributedTerm (_, CicNotationPt.Sort (`NCProp i)) ->
815 NUri.uri_of_string ("cic:/matita/pts/CProp"^i^".univ")
816 | _ -> raise (Failure "only a sort can be constrained")
818 G.NUnivConstraint (loc, strict,u1,u2)
820 t = [ u = URI -> N.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
821 arity = OPT int ; saturations = OPT int;
822 composites = OPT (IDENT "nocomposites") ->
823 let arity = match arity with None -> 0 | Some x -> x in
824 let saturations = match saturations with None -> 0 | Some x -> x in
825 let composites = match composites with None -> true | Some _ -> false in
827 (loc, t, composites, arity, saturations)
828 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
829 G.PreferCoercion (loc, t)
830 | IDENT "pump" ; steps = int ->
832 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
833 G.UnificationHint (loc, t, n)
834 | IDENT "inverter"; name = IDENT; IDENT "for";
835 indty = tactic_term; paramspec = inverter_param_list ->
837 (loc, name, indty, paramspec)
838 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
839 G.Obj (loc, N.Record (params,name,ty,fields))
840 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
841 G.NObj (loc, N.Record (params,name,ty,fields))
842 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
843 let uris = List.map UriManager.uri_of_string uris in
844 G.Default (loc,what,uris)
845 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
846 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
847 refl = tactic_term -> refl ] ;
848 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
849 sym = tactic_term -> sym ] ;
850 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
851 trans = tactic_term -> trans ] ;
853 G.Relation (loc,id,a,aeq,refl,sym,trans)
856 IDENT "alias" ; spec = alias_spec ->
858 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
859 L.Notation (loc, dir, l1, assoc, prec, l2)
860 | IDENT "interpretation"; id = QSTRING;
861 (symbol, args, l3) = interpretation ->
862 L.Interpretation (loc, id, (symbol, args), l3)
865 [ cmd = grafite_command; SYMBOL "." -> G.Command (loc, cmd)
866 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
867 G.Tactic (loc, Some tac, punct)
868 | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
869 | tac = ntactic; punct = punctuation_tactical ->
870 G.NTactic (loc, tac, punct)
871 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
872 G.NTactic (loc, G.NId loc, punct)
873 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
874 G.NonPunctuationTactical (loc, tac, punct)
875 | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
876 G.NNonPunctuationTactical (loc, tac, punct)
877 | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
881 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
889 fun ?(never_include=false) ~include_paths status ->
890 let stm = G.Executable (loc, ex) in
891 !grafite_callback status stm;
894 fun ?(never_include=false) ~include_paths status ->
895 let stm = G.Comment (loc, com) in
896 !grafite_callback status stm;
898 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
899 fun ?(never_include=false) ~include_paths status ->
901 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, fname)))
903 !grafite_callback status stm;
904 let _root, buri, fullpath, _rrelpath =
905 Librarian.baseuri_of_script ~include_paths fname
908 if never_include then raise (NoInclusionPerformed fullpath)
909 else LE.eval_command status (L.Include (iloc,buri,mode,fullpath))
912 G.Executable (loc, G.Command (loc, G.Include (iloc, normal, buri)))
915 | scom = lexicon_command ; SYMBOL "." ->
916 fun ?(never_include=false) ~include_paths status ->
917 !lexicon_callback status scom;
918 let status = LE.eval_command status scom in
920 | EOI -> raise End_of_file
927 let _ = initialize_parser () ;;
929 let exc_located_wrapper f =
933 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
934 | Stdpp.Exc_located (floc, Stream.Error msg) ->
935 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
936 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
938 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
939 | Stdpp.Exc_located (floc, exn) ->
941 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
943 let parse_statement lexbuf =
945 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
947 let statement () = !grafite_parser.statement
949 let history = ref [] ;;
953 history := !grafite_parser :: !history;
954 grafite_parser := initial_parser ();
963 grafite_parser := gp;
967 (* vim:set foldmethod=marker: *)