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/
31 module LE = LexiconEngine
33 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
39 type ast_statement = G.statement
41 type 'status statement =
42 ?never_include:bool ->
43 (* do not call LexiconEngine to do includes, always raise NoInclusionPerformed *)
44 include_paths:string list -> (#LE.status as 'status) ->
45 'status * ast_statement localized_option
47 type 'status parser_status = {
49 term : N.term Grammar.Entry.e;
50 statement : #LE.status as 'status statement Grammar.Entry.e;
53 let grafite_callback = ref (fun _ -> ())
54 let set_grafite_callback cb = grafite_callback := cb
56 let lexicon_callback = ref (fun _ -> ())
57 let set_lexicon_callback cb = lexicon_callback := cb
59 let initial_parser () =
60 let grammar = CicNotationParser.level2_ast_grammar () in
61 let term = CicNotationParser.term () in
62 let statement = Grammar.Entry.create grammar "statement" in
63 { grammar = grammar; term = term; statement = statement }
66 let grafite_parser = ref (initial_parser ())
68 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
70 let default_associativity = Gramext.NonA
72 let mk_rec_corec ind_kind defs loc =
73 (* In case of mutual definitions here we produce just
74 the syntax tree for the first one. The others will be
75 generated from the completely specified term just before
76 insertion in the environment. We use the flavour
77 `MutualDefinition to rememer this. *)
80 | (params,(N.Ident (name, None), ty),_,_) :: _ ->
81 let ty = match ty with Some ty -> ty | None -> N.Implicit `JustOne in
84 (fun var ty -> N.Binder (`Pi,var,ty)
90 let body = N.Ident (name,None) in
92 if List.length defs = 1 then
97 (loc, N.Theorem(flavour, name, ty, Some (N.LetRec (ind_kind, defs, body)), `Regular))
99 let nmk_rec_corec ind_kind defs loc =
100 let loc,t = mk_rec_corec ind_kind defs loc in
104 let nnon_punct_of_punct = function
105 | G.Skip loc -> G.NSkip loc
106 | G.Unfocus loc -> G.NUnfocus loc
107 | G.Focus (loc,l) -> G.NFocus (loc,l)
112 | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p])
116 type by_continuation =
118 | BYC_weproved of N.term * string option * N.term option
119 | BYC_letsuchthat of string * N.term * string * N.term
120 | BYC_wehaveand of string * N.term * string * N.term
122 let initialize_parser () =
123 (* {{{ parser initialization *)
124 let term = !grafite_parser.term in
125 let statement = !grafite_parser.statement in
126 let let_defs = CicNotationParser.let_defs () in
127 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
129 GLOBAL: term statement;
130 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
131 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
134 | id = IDENT -> Some id ]
136 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
137 ident_list1: [ [ LPAREN; idents = LIST1 IDENT; RPAREN -> idents ] ];
139 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
142 [ IDENT "normalize" -> `Normalize
143 | IDENT "simplify" -> `Simpl
144 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
145 | IDENT "whd" -> `Whd ]
148 [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
149 let delta = match delta with None -> true | _ -> false in
151 (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
152 | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
153 let delta = match delta with None -> true | _ -> false in
156 sequent_pattern_spec: [
160 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
161 (id,match path with Some p -> p | None -> N.UserInput) ];
162 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
164 match goal_path, hyp_paths with
165 None, [] -> Some N.UserInput
167 | Some goal_path, _ -> Some goal_path
176 [ "match" ; wanted = tactic_term ;
177 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
179 | sps = sequent_pattern_spec ->
182 let wanted,hyp_paths,goal_path =
183 match wanted_and_sps with
184 wanted,None -> wanted, [], Some N.UserInput
185 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
187 wanted, hyp_paths, goal_path ] ->
189 None -> None,[],Some N.UserInput
192 inverter_param_list: [
193 [ params = tactic_term ->
194 let deannotate = function
195 | N.AttributedTerm (_,t) | t -> t
196 in match deannotate params with
197 | N.Implicit _ -> [false]
198 | N.UserInput -> [true]
200 List.map (fun x -> match deannotate x with
201 | N.Implicit _ -> false
202 | N.UserInput -> true
203 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
204 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ NotationPp.pp_term params)) ]
207 [ SYMBOL ">" -> `LeftToRight
208 | SYMBOL "<" -> `RightToLeft ]
210 int: [ [ num = NUMBER -> int_of_string num ] ];
212 [ idents = OPT ident_list0 ->
213 match idents with None -> [] | Some idents -> idents
217 [ OPT [ IDENT "names" ];
218 num = OPT [ num = int -> num ];
219 idents = intros_names ->
223 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
225 [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
226 | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
230 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
231 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
232 SYMBOL <:unicode<def>> ; bo = tactic_term ->
234 SYMBOL <:unicode<vdash>>;
235 concl = tactic_term -> (List.rev hyps,concl) ] ->
236 G.NTactic(loc,[G.NAssert (loc, seqs)])
237 | IDENT "nauto"; params = auto_params ->
238 G.NTactic(loc,[G.NAuto (loc, params)])
239 | SYMBOL "/"; num = OPT NUMBER ;
240 params = nauto_params; SYMBOL "/" ;
241 just = OPT [ IDENT "by"; by =
242 [ univ = tactic_term_list1 -> `Univ univ
243 | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
244 | SYMBOL "_" -> `Trace ] -> by ] ->
245 let depth = match num with Some n -> n | None -> "1" in
249 [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
250 | Some (`Univ univ) ->
252 [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
255 [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
258 G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
259 | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
260 | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
261 | IDENT "screenshot"; fname = QSTRING ->
262 G.NMacro(loc,G.Screenshot (loc, fname))
263 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
264 G.NTactic(loc,[G.NCases (loc, what, where)])
265 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
266 G.NTactic(loc,[G.NChange (loc, what, with_what)])
267 | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term ->
268 G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
269 | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
270 (* | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
271 | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
272 | IDENT "ndestruct"; just = OPT [ dom = ident_list1 -> dom ];
273 exclude = OPT [ IDENT "skip"; skip = ident_list1 -> skip ]
274 -> let exclude' = match exclude with None -> [] | Some l -> l in
275 G.NTactic(loc,[G.NDestruct (loc,just,exclude')])
276 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
277 G.NTactic(loc,[G.NElim (loc, what, where)])
278 | IDENT "ngeneralize"; p=pattern_spec ->
279 G.NTactic(loc,[G.NGeneralize (loc, p)])
280 | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
281 G.NTactic(loc,[G.NInversion (loc, what, where)])
282 | IDENT "nlapply"; t = tactic_term -> G.NTactic(loc,[G.NLApply (loc, t)])
283 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
284 where = pattern_spec ->
285 G.NTactic(loc,[G.NLetIn (loc,where,t,name)])
286 | kind = nreduction_kind; p = pattern_spec ->
287 G.NTactic(loc,[G.NReduce (loc, kind, p)])
288 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
289 G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
290 | IDENT "ntry"; tac = SELF ->
291 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
292 G.NTactic(loc,[ G.NTry (loc,tac)])
293 | IDENT "nrepeat"; tac = SELF ->
294 let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
295 G.NTactic(loc,[ G.NRepeat (loc,tac)])
296 | LPAREN; l = LIST1 SELF; RPAREN ->
299 (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
300 G.NTactic(loc,[G.NBlock (loc,l)])
301 | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
302 | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
303 | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
304 | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
305 | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
310 | IDENT "fast_paramod"
324 i = auto_fixed_param -> i,""
325 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
326 string_of_int v | v = IDENT -> v ] -> i,v ];
327 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] -> tl,
328 (* (match tl with Some l -> l | None -> []), *)
335 i = auto_fixed_param -> i,""
336 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
337 string_of_int v | v = IDENT -> v ] -> i,v ] ->
343 [ 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)
344 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
345 "done" -> BYC_weproved (ty,None,t1)
347 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
348 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
349 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
350 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
351 BYC_wehaveand (id1,t1,id2,t2)
354 rewriting_step_continuation : [
362 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
365 | G.Seq (_, l) -> l @ [ t2 ]
371 [ tac = SELF; SYMBOL ";";
372 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
373 (G.Then (loc, tac, tacs))
376 [ IDENT "do"; count = int; tac = SELF ->
377 G.Do (loc, count, tac)
378 | IDENT "repeat"; tac = SELF -> G.Repeat (loc, tac)
382 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
384 | IDENT "try"; tac = SELF -> G.Try (loc, tac)
386 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
388 | IDENT "progress"; tac = SELF -> G.Progress (loc, tac)
389 | LPAREN; tac = SELF; RPAREN -> tac
390 | tac = tactic -> tac
394 npunctuation_tactical:
396 [ SYMBOL "[" -> G.NBranch loc
397 | SYMBOL "|" -> G.NShift loc
398 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
399 | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
400 | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
401 | SYMBOL "]" -> G.NMerge loc
402 | SYMBOL ";" -> G.NSemicolon loc
403 | SYMBOL "." -> G.NDot loc
406 nnon_punctuation_tactical:
408 [ IDENT "focus"; goals = LIST1 int -> G.NFocus (loc, goals)
409 | IDENT "unfocus" -> G.NUnfocus loc
410 | IDENT "skip" -> G.NSkip loc
414 [ [ IDENT "ndefinition" ] -> `Definition
415 | [ IDENT "nfact" ] -> `Fact
416 | [ IDENT "nlemma" ] -> `Lemma
417 | [ IDENT "nremark" ] -> `Remark
418 | [ IDENT "ntheorem" ] -> `Theorem
422 [ [ IDENT "definition" ] -> `Definition
423 | [ IDENT "fact" ] -> `Fact
424 | [ IDENT "lemma" ] -> `Lemma
425 | [ IDENT "remark" ] -> `Remark
426 | [ IDENT "theorem" ] -> `Theorem
430 [ attr = theorem_flavour -> attr
431 | [ IDENT "axiom" ] -> `Axiom
432 | [ IDENT "variant" ] -> `Variant
437 params = LIST0 protected_binder_vars;
438 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
439 fst_constructors = LIST0 constructor SEP SYMBOL "|";
442 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
443 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
444 (name, true, typ, constructors) ] SEP "with" -> types
448 (fun (names, typ) acc ->
449 (List.map (fun name -> (name, typ)) names) @ acc)
452 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
453 let tl_ind_types = match tl with None -> [] | Some types -> types in
454 let ind_types = fst_ind_type :: tl_ind_types in
460 params = LIST0 protected_binder_vars;
461 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
465 SYMBOL ":" -> false,0
466 | SYMBOL ":"; SYMBOL ">" -> true,0
467 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
470 let b,n = coercion in
472 ] SEP SYMBOL ";"; SYMBOL "}" ->
475 (fun (names, typ) acc ->
476 (List.map (fun name -> (name, typ)) names) @ acc)
479 (params,name,typ,fields)
483 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
484 let alpha = "[a-zA-Z]" in
485 let num = "[0-9]+" in
486 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
487 let decoration = "\\'" in
488 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
489 let rex = Str.regexp ("^"^ident^"$") in
490 if Str.string_match rex id 0 then
491 if (try ignore (UriManager.uri_of_string uri); true
492 with UriManager.IllFormedUri _ -> false) ||
493 (try ignore (NReference.reference_of_string uri); true
494 with NReference.IllFormedReference _ -> false)
496 L.Ident_alias (id, uri)
499 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
501 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
502 Printf.sprintf "Not a valid identifier: %s" id)))
503 | IDENT "symbol"; symbol = QSTRING;
504 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
505 SYMBOL "="; dsc = QSTRING ->
507 match instance with Some i -> i | None -> 0
509 L.Symbol_alias (symbol, instance, dsc)
511 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
512 SYMBOL "="; dsc = QSTRING ->
514 match instance with Some i -> i | None -> 0
516 L.Number_alias (instance, dsc)
520 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
522 N.IdentArg (List.length l, id)
526 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
527 | IDENT "right"; IDENT "associative" -> Gramext.RightA
528 | IDENT "non"; IDENT "associative" -> Gramext.NonA
532 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
535 [ dir = OPT direction; s = QSTRING;
536 assoc = OPT associativity; prec = precedence;
539 [ blob = UNPARSED_AST ->
540 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
541 (CicNotationParser.parse_level2_ast
542 (Ulexing.from_utf8_string blob))
543 | blob = UNPARSED_META ->
544 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
545 (CicNotationParser.parse_level2_meta
546 (Ulexing.from_utf8_string blob))
550 | None -> default_associativity
551 | Some assoc -> assoc
554 add_raw_attribute ~text:s
555 (CicNotationParser.parse_level1_pattern prec
556 (Ulexing.from_utf8_string s))
558 (dir, p1, assoc, prec, p2)
562 [ u = URI -> N.UriPattern (UriManager.uri_of_string u)
563 | r = NREF -> N.NRefPattern (NReference.reference_of_string r)
564 | IMPLICIT -> N.ImplicitPattern
565 | id = IDENT -> N.VarPattern id
566 | LPAREN; terms = LIST1 SELF; RPAREN ->
570 | terms -> N.ApplPattern terms)
574 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
580 IDENT "include" ; path = QSTRING ->
581 loc,path,true,L.WithPreferences
582 | IDENT "include" ; IDENT "source" ; path = QSTRING ->
583 loc,path,false,L.WithPreferences
584 | IDENT "include'" ; path = QSTRING ->
585 loc,path,true,L.WithoutPreferences
588 grafite_ncommand: [ [
589 IDENT "nqed" -> G.NQed loc
590 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
591 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
592 G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
593 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
595 G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
596 | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
597 G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
598 | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
599 | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
600 paramspec = OPT inverter_param_list ;
601 outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] ->
602 G.NInverter (loc,name,indty,paramspec,outsort)
603 | NLETCOREC ; defs = let_defs ->
604 nmk_rec_corec `CoInductive defs loc
605 | NLETREC ; defs = let_defs ->
606 nmk_rec_corec `Inductive defs loc
607 | IDENT "ninductive"; spec = inductive_spec ->
608 let (params, ind_types) = spec in
609 G.NObj (loc, N.Inductive (params, ind_types))
610 | IDENT "ncoinductive"; spec = inductive_spec ->
611 let (params, ind_types) = spec in
612 let ind_types = (* set inductive flags to false (coinductive) *)
613 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
616 G.NObj (loc, N.Inductive (params, ind_types))
617 | IDENT "universe"; IDENT "constraint"; u1 = tactic_term;
618 SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
620 | NotationPt.AttributedTerm (_, NotationPt.Sort (`NType i)) ->
621 NUri.uri_of_string ("cic:/matita/pts/Type"^i^".univ")
622 | _ -> raise (Failure "only a Type[…] sort can be constrained")
626 G.NUnivConstraint (loc,u1,u2)
627 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
628 G.UnificationHint (loc, t, n)
629 | IDENT "ncoercion"; name = IDENT; SYMBOL ":"; ty = term;
630 SYMBOL <:unicode<def>>; t = term; "on";
631 id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
632 "to"; target = term ->
633 G.NCoercion(loc,name,t,ty,(id,source),target)
634 | IDENT "nrecord" ; (params,name,ty,fields) = record_spec ->
635 G.NObj (loc, N.Record (params,name,ty,fields))
636 | IDENT "ncopy" ; s = IDENT; IDENT "from"; u = URI; "with";
637 m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
638 G.NCopy (loc,s,NUri.uri_of_string u,
639 List.map (fun a,b -> NUri.uri_of_string a, NUri.uri_of_string b) m)
643 IDENT "alias" ; spec = alias_spec ->
645 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
646 L.Notation (loc, dir, l1, assoc, prec, l2)
647 | IDENT "interpretation"; id = QSTRING;
648 (symbol, args, l3) = interpretation ->
649 L.Interpretation (loc, id, (symbol, args), l3)
652 [ ncmd = grafite_ncommand; SYMBOL "." -> G.NCommand (loc, ncmd)
653 | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ;
654 punct = npunctuation_tactical -> cons_ntac tac punct
655 | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
656 G.NTactic (loc, [punct])
657 | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical;
658 SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
659 G.NTactic (loc, [tac; punct])
660 | SYMBOL "#" ; SYMBOL "#" ; tac = nnon_punctuation_tactical;
661 punct = npunctuation_tactical ->
662 G.NTactic (loc, [tac; punct])
666 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
674 fun ?(never_include=false) ~include_paths status ->
675 let stm = G.Executable (loc, ex) in
676 !grafite_callback stm;
679 fun ?(never_include=false) ~include_paths status ->
680 let stm = G.Comment (loc, com) in
681 !grafite_callback stm;
683 | (iloc,fname,normal,mode) = include_command ; SYMBOL "." ->
684 fun ?(never_include=false) ~include_paths status ->
685 let _root, buri, fullpath, _rrelpath =
686 Librarian.baseuri_of_script ~include_paths fname in
687 if never_include then raise (NoInclusionPerformed fullpath)
692 (loc, G.Command (loc, G.Include (iloc,fname))) in
693 !grafite_callback stm;
695 LE.eval_command status (L.Include (iloc,buri,mode,fullpath)) in
698 (loc,G.Command (loc,G.Include (iloc,buri)))
702 | scom = lexicon_command ; SYMBOL "." ->
703 fun ?(never_include=false) ~include_paths status ->
704 !lexicon_callback scom;
705 let status = LE.eval_command status scom in
707 | EOI -> raise End_of_file
714 let _ = initialize_parser () ;;
716 let exc_located_wrapper f =
720 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
721 | Stdpp.Exc_located (floc, Stream.Error msg) ->
722 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
723 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
725 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
726 | Stdpp.Exc_located (floc, exn) ->
728 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
730 let parse_statement lexbuf =
732 (fun () -> (Grammar.Entry.parse (Obj.magic !grafite_parser.statement) (Obj.magic lexbuf)))
734 let statement () = Obj.magic !grafite_parser.statement
736 let history = ref [] ;;
740 history := !grafite_parser :: !history;
741 grafite_parser := initial_parser ();
750 grafite_parser := gp;
754 (* vim:set foldmethod=marker: *)