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/
29 let set_callback f = out := f
31 module Ast = CicNotationPt
33 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
37 | LNone of GrafiteAst.loc
40 (CicNotationPt.term, CicNotationPt.term,
41 CicNotationPt.term GrafiteAst.reduction,
42 CicNotationPt.term CicNotationPt.obj, string)
46 ?never_include:bool ->
47 include_paths:string list ->
48 LexiconEngine.status ->
49 LexiconEngine.status * ast_statement localized_option
51 type parser_status = {
53 term : CicNotationPt.term Grammar.Entry.e;
54 statement : statement Grammar.Entry.e;
57 let initial_parser () =
58 let grammar = CicNotationParser.level2_ast_grammar () in
59 let term = CicNotationParser.term () in
60 let statement = Grammar.Entry.create grammar "statement" in
61 { grammar = grammar; term = term; statement = statement }
64 let grafite_parser = ref (initial_parser ())
66 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
68 let default_associativity = Gramext.NonA
70 let mk_rec_corec ind_kind defs loc =
71 (* In case of mutual definitions here we produce just
72 the syntax tree for the first one. The others will be
73 generated from the completely specified term just before
74 insertion in the environment. We use the flavour
75 `MutualDefinition to rememer this. *)
78 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
81 (fun var ty -> Ast.Binder (`Pi,var,ty)
85 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
89 let body = Ast.Ident (name,None) in
91 if List.length defs = 1 then
96 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
97 Some (Ast.LetRec (ind_kind, defs, body))))
99 type by_continuation =
101 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
102 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
103 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
105 let initialize_parser () =
106 (* {{{ parser initialization *)
107 let term = !grafite_parser.term in
108 let statement = !grafite_parser.statement in
109 let let_defs = CicNotationParser.let_defs () in
110 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
112 GLOBAL: term statement;
113 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
114 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
116 [ id = IDENT -> Some id
117 | SYMBOL "_" -> None ]
119 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
121 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
124 [ IDENT "normalize" -> `Normalize
125 | IDENT "simplify" -> `Simpl
126 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
127 | IDENT "whd" -> `Whd ]
129 sequent_pattern_spec: [
133 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
134 (id,match path with Some p -> p | None -> Ast.UserInput) ];
135 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
137 match goal_path, hyp_paths with
138 None, [] -> Some Ast.UserInput
140 | Some goal_path, _ -> Some goal_path
149 [ "match" ; wanted = tactic_term ;
150 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
152 | sps = sequent_pattern_spec ->
155 let wanted,hyp_paths,goal_path =
156 match wanted_and_sps with
157 wanted,None -> wanted, [], Some Ast.UserInput
158 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
160 wanted, hyp_paths, goal_path ] ->
162 None -> None,[],Some Ast.UserInput
166 [ SYMBOL ">" -> `LeftToRight
167 | SYMBOL "<" -> `RightToLeft ]
169 int: [ [ num = NUMBER -> int_of_string num ] ];
171 [ idents = OPT ident_list0 ->
172 match idents with None -> [] | Some idents -> idents
176 [ OPT [ IDENT "names" ];
177 num = OPT [ num = int -> num ];
178 idents = intros_names ->
182 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
184 [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
185 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
186 GrafiteAst.NCases (loc, what, where)
187 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
188 GrafiteAst.NChange (loc, what, with_what)
189 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
190 GrafiteAst.NElim (loc, what, where)
191 | IDENT "ngeneralize"; p=pattern_spec ->
192 GrafiteAst.NGeneralize (loc, p)
193 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
194 where = pattern_spec ->
195 GrafiteAst.NLetIn (loc,where,t,name)
196 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
197 GrafiteAst.NRewrite (loc, dir, what, where)
198 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
199 where = pattern_spec ->
200 let delta = match delta with None -> true | _ -> false in
201 GrafiteAst.NEval (loc, where, `Whd delta)
202 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
203 | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
204 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
205 | SYMBOL "*"; n=IDENT ->
206 GrafiteAst.NCase1 (loc,n)
210 [ IDENT "absurd"; t = tactic_term ->
211 GrafiteAst.Absurd (loc, t)
212 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
213 GrafiteAst.ApplyRule (loc, t)
214 | IDENT "apply"; t = tactic_term ->
215 GrafiteAst.Apply (loc, t)
216 | IDENT "applyP"; t = tactic_term ->
217 GrafiteAst.ApplyP (loc, t)
218 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
219 GrafiteAst.ApplyS (loc, t, params)
220 | IDENT "assumption" ->
221 GrafiteAst.Assumption loc
222 | IDENT "autobatch"; params = auto_params ->
223 GrafiteAst.AutoBatch (loc,params)
224 | IDENT "cases"; what = tactic_term;
225 pattern = OPT pattern_spec;
226 specs = intros_spec ->
227 let pattern = match pattern with
228 | None -> None, [], Some Ast.UserInput
229 | Some pattern -> pattern
231 GrafiteAst.Cases (loc, what, pattern, specs)
232 | IDENT "clear"; ids = LIST1 IDENT ->
233 GrafiteAst.Clear (loc, ids)
234 | IDENT "clearbody"; id = IDENT ->
235 GrafiteAst.ClearBody (loc,id)
236 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
237 GrafiteAst.Change (loc, what, t)
238 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
239 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
240 let times = match times with None -> 1 | Some i -> i in
241 GrafiteAst.Compose (loc, t1, t2, times, specs)
242 | IDENT "constructor"; n = int ->
243 GrafiteAst.Constructor (loc, n)
244 | IDENT "contradiction" ->
245 GrafiteAst.Contradiction loc
246 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
247 GrafiteAst.Cut (loc, ident, t)
248 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
249 let idents = match idents with None -> [] | Some idents -> idents in
250 GrafiteAst.Decompose (loc, idents)
251 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
252 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
253 GrafiteAst.Destruct (loc, xts)
254 | IDENT "elim"; what = tactic_term; using = using;
255 pattern = OPT pattern_spec;
256 ispecs = intros_spec ->
257 let pattern = match pattern with
258 | None -> None, [], Some Ast.UserInput
259 | Some pattern -> pattern
261 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
262 | IDENT "elimType"; what = tactic_term; using = using;
263 (num, idents) = intros_spec ->
264 GrafiteAst.ElimType (loc, what, using, (num, idents))
265 | IDENT "exact"; t = tactic_term ->
266 GrafiteAst.Exact (loc, t)
268 GrafiteAst.Exists loc
269 | IDENT "fail" -> GrafiteAst.Fail loc
270 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
273 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
274 ("the pattern cannot specify the term to replace, only its"
275 ^ " paths in the hypotheses and in the conclusion")))
277 GrafiteAst.Fold (loc, kind, t, p)
279 GrafiteAst.Fourier loc
280 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
281 let idents = match idents with None -> [] | Some idents -> idents in
282 GrafiteAst.FwdSimpl (loc, hyp, idents)
283 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
284 GrafiteAst.Generalize (loc,p,id)
285 | IDENT "id" -> GrafiteAst.IdTac loc
286 | IDENT "intro"; ident = OPT IDENT ->
287 let idents = match ident with None -> [] | Some id -> [Some id] in
288 GrafiteAst.Intros (loc, (Some 1, idents))
289 | IDENT "intros"; specs = intros_spec ->
290 GrafiteAst.Intros (loc, specs)
291 | IDENT "inversion"; t = tactic_term ->
292 GrafiteAst.Inversion (loc, t)
294 linear = OPT [ IDENT "linear" ];
295 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
297 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
298 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
299 let linear = match linear with None -> false | Some _ -> true in
300 let to_what = match to_what with None -> [] | Some to_what -> to_what in
301 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
302 | IDENT "left" -> GrafiteAst.Left loc
303 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
304 GrafiteAst.LetIn (loc, t, where)
305 | kind = reduction_kind; p = pattern_spec ->
306 GrafiteAst.Reduce (loc, kind, p)
307 | IDENT "reflexivity" ->
308 GrafiteAst.Reflexivity loc
309 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
310 GrafiteAst.Replace (loc, p, t)
311 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
312 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
316 (HExtlib.Localized (loc,
317 (CicNotationParser.Parse_error
318 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
320 let n = match xnames with None -> [] | Some names -> names in
321 GrafiteAst.Rewrite (loc, d, t, p, n)
328 | IDENT "symmetry" ->
329 GrafiteAst.Symmetry loc
330 | IDENT "transitivity"; t = tactic_term ->
331 GrafiteAst.Transitivity (loc, t)
332 (* Produzioni Aggiunte *)
333 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
334 GrafiteAst.Assume (loc, id, t)
335 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
336 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
337 t' = tactic_term -> t']->
338 GrafiteAst.Suppose (loc, t, id, t1)
339 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
340 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
341 id2 = IDENT ; RPAREN ->
342 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
344 [ IDENT "using"; t=tactic_term -> `Term t
345 | params = auto_params -> `Auto params] ;
346 cont=by_continuation ->
348 BYC_done -> GrafiteAst.Bydone (loc, just)
349 | BYC_weproved (ty,id,t1) ->
350 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
351 | BYC_letsuchthat (id1,t1,id2,t2) ->
352 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
353 | BYC_wehaveand (id1,t1,id2,t2) ->
354 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
355 | 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']->
356 GrafiteAst.We_need_to_prove (loc, t, id, t1)
357 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
358 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
359 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
360 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
361 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
362 GrafiteAst.Byinduction(loc, t, id)
363 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
364 GrafiteAst.Thesisbecomes(loc, t)
365 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
366 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
367 GrafiteAst.Case(loc,id,params)
368 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
370 termine = tactic_term;
374 [ IDENT "using"; t=tactic_term -> `Term t
375 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
376 | IDENT "proof" -> `Proof
377 | params = auto_params -> `Auto params];
378 cont = rewriting_step_continuation ->
379 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
380 | IDENT "obtain" ; name = IDENT;
381 termine = tactic_term;
385 [ IDENT "using"; t=tactic_term -> `Term t
386 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
387 | IDENT "proof" -> `Proof
388 | params = auto_params -> `Auto params];
389 cont = rewriting_step_continuation ->
390 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
394 [ IDENT "using"; t=tactic_term -> `Term t
395 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
396 | IDENT "proof" -> `Proof
397 | params = auto_params -> `Auto params];
398 cont = rewriting_step_continuation ->
399 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
403 [ IDENT "paramodulation"
415 i = auto_fixed_param -> i,""
416 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
417 string_of_int v | v = IDENT -> v ] -> i,v ];
418 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
419 (match tl with Some l -> l | None -> []),
424 [ 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)
425 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
426 "done" -> BYC_weproved (ty,None,t1)
428 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
429 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
430 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
431 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
432 BYC_wehaveand (id1,t1,id2,t2)
435 rewriting_step_continuation : [
442 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
445 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
448 GrafiteAst.Seq (loc, ts)
451 [ tac = SELF; SYMBOL ";";
452 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
453 (GrafiteAst.Then (loc, tac, tacs))
456 [ IDENT "do"; count = int; tac = SELF ->
457 GrafiteAst.Do (loc, count, tac)
458 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
462 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
463 GrafiteAst.First (loc, tacs)
464 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
466 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
467 GrafiteAst.Solve (loc, tacs)
468 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
469 | LPAREN; tac = SELF; RPAREN -> tac
470 | tac = tactic -> tac
473 punctuation_tactical:
475 [ SYMBOL "[" -> GrafiteAst.Branch loc
476 | SYMBOL "|" -> GrafiteAst.Shift loc
477 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
478 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
479 | SYMBOL "]" -> GrafiteAst.Merge loc
480 | SYMBOL ";" -> GrafiteAst.Semicolon loc
481 | SYMBOL "." -> GrafiteAst.Dot loc
484 non_punctuation_tactical:
486 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
487 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
488 | IDENT "skip" -> GrafiteAst.Skip loc
492 [ [ IDENT "ntheorem" ] -> `Theorem
496 [ [ IDENT "definition" ] -> `Definition
497 | [ IDENT "fact" ] -> `Fact
498 | [ IDENT "lemma" ] -> `Lemma
499 | [ IDENT "remark" ] -> `Remark
500 | [ IDENT "theorem" ] -> `Theorem
504 [ attr = theorem_flavour -> attr
505 | [ IDENT "axiom" ] -> `Axiom
506 | [ IDENT "mutual" ] -> `MutualDefinition
511 params = LIST0 protected_binder_vars;
512 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
513 fst_constructors = LIST0 constructor SEP SYMBOL "|";
516 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
517 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
518 (name, true, typ, constructors) ] SEP "with" -> types
522 (fun (names, typ) acc ->
523 (List.map (fun name -> (name, typ)) names) @ acc)
526 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
527 let tl_ind_types = match tl with None -> [] | Some types -> types in
528 let ind_types = fst_ind_type :: tl_ind_types in
534 params = LIST0 protected_binder_vars;
535 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
539 SYMBOL ":" -> false,0
540 | SYMBOL ":"; SYMBOL ">" -> true,0
541 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
544 let b,n = coercion in
546 ] SEP SYMBOL ";"; SYMBOL "}" ->
549 (fun (names, typ) acc ->
550 (List.map (fun name -> (name, typ)) names) @ acc)
553 (params,name,typ,fields)
557 [ [ IDENT "check" ]; t = term ->
558 GrafiteAst.Check (loc, t)
559 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
560 GrafiteAst.Eval (loc, kind, t)
562 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
563 suri = QSTRING; prefix = OPT QSTRING;
564 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
565 let style = match style with
566 | None -> GrafiteAst.Declarative
567 | Some depth -> GrafiteAst.Procedural depth
569 let prefix = match prefix with None -> "" | Some prefix -> prefix in
570 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
571 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
572 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
573 | IDENT "auto"; params = auto_params ->
574 GrafiteAst.AutoInteractive (loc,params)
575 | [ IDENT "whelp"; "match" ] ; t = term ->
576 GrafiteAst.WMatch (loc,t)
577 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
578 GrafiteAst.WInstance (loc,t)
579 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
580 GrafiteAst.WLocate (loc,id)
581 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
582 GrafiteAst.WElim (loc, t)
583 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
584 GrafiteAst.WHint (loc,t)
588 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
589 let alpha = "[a-zA-Z]" in
590 let num = "[0-9]+" in
591 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
592 let decoration = "\\'" in
593 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
594 let rex = Str.regexp ("^"^ident^"$") in
595 if Str.string_match rex id 0 then
596 if (try ignore (UriManager.uri_of_string uri); true
597 with UriManager.IllFormedUri _ -> false)
599 LexiconAst.Ident_alias (id, uri)
602 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
604 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
605 Printf.sprintf "Not a valid identifier: %s" id)))
606 | IDENT "symbol"; symbol = QSTRING;
607 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
608 SYMBOL "="; dsc = QSTRING ->
610 match instance with Some i -> i | None -> 0
612 LexiconAst.Symbol_alias (symbol, instance, dsc)
614 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
615 SYMBOL "="; dsc = QSTRING ->
617 match instance with Some i -> i | None -> 0
619 LexiconAst.Number_alias (instance, dsc)
623 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
625 Ast.IdentArg (List.length l, id)
629 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
630 | IDENT "right"; IDENT "associative" -> Gramext.RightA
631 | IDENT "non"; IDENT "associative" -> Gramext.NonA
635 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
638 [ dir = OPT direction; s = QSTRING;
639 assoc = OPT associativity; prec = precedence;
642 [ blob = UNPARSED_AST ->
643 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
644 (CicNotationParser.parse_level2_ast
645 (Ulexing.from_utf8_string blob))
646 | blob = UNPARSED_META ->
647 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
648 (CicNotationParser.parse_level2_meta
649 (Ulexing.from_utf8_string blob))
653 | None -> default_associativity
654 | Some assoc -> assoc
657 add_raw_attribute ~text:s
658 (CicNotationParser.parse_level1_pattern prec
659 (Ulexing.from_utf8_string s))
661 (dir, p1, assoc, prec, p2)
665 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
666 | id = IDENT -> Ast.VarPattern id
667 | SYMBOL "_" -> Ast.ImplicitPattern
668 | LPAREN; terms = LIST1 SELF; RPAREN ->
672 | terms -> Ast.ApplPattern terms)
676 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
682 IDENT "include" ; path = QSTRING ->
683 loc,path,LexiconAst.WithPreferences
684 | IDENT "include'" ; path = QSTRING ->
685 loc,path,LexiconAst.WithoutPreferences
689 IDENT "set"; n = QSTRING; v = QSTRING ->
690 GrafiteAst.Set (loc, n, v)
691 | IDENT "drop" -> GrafiteAst.Drop loc
692 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
693 | IDENT "qed" -> GrafiteAst.Qed loc
694 | IDENT "variant" ; name = IDENT; SYMBOL ":";
695 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
698 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
699 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
700 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
701 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
702 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
703 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
704 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
705 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
708 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
709 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
710 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
711 | LETCOREC ; defs = let_defs ->
712 mk_rec_corec `CoInductive defs loc
713 | LETREC ; defs = let_defs ->
714 mk_rec_corec `Inductive defs loc
715 | IDENT "inductive"; spec = inductive_spec ->
716 let (params, ind_types) = spec in
717 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
718 | IDENT "coinductive"; spec = inductive_spec ->
719 let (params, ind_types) = spec in
720 let ind_types = (* set inductive flags to false (coinductive) *)
721 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
724 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
726 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
727 arity = OPT int ; saturations = OPT int;
728 composites = OPT (IDENT "nocomposites") ->
729 let arity = match arity with None -> 0 | Some x -> x in
730 let saturations = match saturations with None -> 0 | Some x -> x in
731 let composites = match composites with None -> true | Some _ -> false in
733 (loc, t, composites, arity, saturations)
734 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
735 GrafiteAst.PreferCoercion (loc, t)
736 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
737 GrafiteAst.UnificationHint (loc, t, n)
738 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
739 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
740 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
741 let uris = List.map UriManager.uri_of_string uris in
742 GrafiteAst.Default (loc,what,uris)
743 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
744 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
745 refl = tactic_term -> refl ] ;
746 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
747 sym = tactic_term -> sym ] ;
748 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
749 trans = tactic_term -> trans ] ;
751 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
754 IDENT "alias" ; spec = alias_spec ->
755 LexiconAst.Alias (loc, spec)
756 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
757 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
758 | IDENT "interpretation"; id = QSTRING;
759 (symbol, args, l3) = interpretation ->
760 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
763 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
764 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
765 GrafiteAst.Tactic (loc, Some tac, punct)
766 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
767 | tac = ntactic; punct = punctuation_tactical ->
768 GrafiteAst.NTactic (loc, tac, punct)
769 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
770 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
771 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
772 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
773 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
777 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
778 GrafiteAst.Code (loc, ex)
780 GrafiteAst.Note (loc, str)
785 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
787 fun ?(never_include=false) ~include_paths status ->
788 status,LSome (GrafiteAst.Comment (loc, com))
789 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
791 fun ?(never_include=false) ~include_paths status ->
792 let _root, buri, fullpath, _rrelpath =
793 Librarian.baseuri_of_script ~include_paths fname
796 if never_include then raise (NoInclusionPerformed fullpath)
797 else LexiconEngine.eval_command status
798 (LexiconAst.Include (iloc,buri,mode,fullpath))
802 (GrafiteAst.Executable
803 (loc,GrafiteAst.Command
804 (loc,GrafiteAst.Include (iloc,buri))))
805 | scom = lexicon_command ; SYMBOL "." ->
806 fun ?(never_include=false) ~include_paths status ->
807 let status = LexiconEngine.eval_command status scom in
809 | EOI -> raise End_of_file
816 let _ = initialize_parser () ;;
818 let exc_located_wrapper f =
822 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
823 | Stdpp.Exc_located (floc, Stream.Error msg) ->
824 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
825 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
827 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
828 | Stdpp.Exc_located (floc, exn) ->
830 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
832 let parse_statement lexbuf =
834 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
836 let statement () = !grafite_parser.statement
838 let history = ref [] ;;
842 history := !grafite_parser :: !history;
843 grafite_parser := initial_parser ();
852 grafite_parser := gp;
856 (* vim:set foldmethod=marker: *)