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)
188 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
189 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
190 SYMBOL <:unicode<def>> ; bo = tactic_term ->
192 SYMBOL <:unicode<vdash>>;
193 concl = tactic_term -> (List.rev hyps,concl) ] ->
194 GrafiteAst.NAssert (loc, seqs)
195 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
196 GrafiteAst.NCases (loc, what, where)
197 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
198 GrafiteAst.NChange (loc, what, with_what)
199 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
200 GrafiteAst.NElim (loc, what, where)
201 | IDENT "ngeneralize"; p=pattern_spec ->
202 GrafiteAst.NGeneralize (loc, p)
203 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
204 where = pattern_spec ->
205 GrafiteAst.NLetIn (loc,where,t,name)
206 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
207 GrafiteAst.NRewrite (loc, dir, what, where)
208 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
209 where = pattern_spec ->
210 let delta = match delta with None -> true | _ -> false in
211 GrafiteAst.NEval (loc, where, `Whd delta)
212 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
213 | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
214 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
215 | SYMBOL "*"; n=IDENT ->
216 GrafiteAst.NCase1 (loc,n)
220 [ IDENT "absurd"; t = tactic_term ->
221 GrafiteAst.Absurd (loc, t)
222 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
223 GrafiteAst.ApplyRule (loc, t)
224 | IDENT "apply"; t = tactic_term ->
225 GrafiteAst.Apply (loc, t)
226 | IDENT "applyP"; t = tactic_term ->
227 GrafiteAst.ApplyP (loc, t)
228 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
229 GrafiteAst.ApplyS (loc, t, params)
230 | IDENT "assumption" ->
231 GrafiteAst.Assumption loc
232 | IDENT "autobatch"; params = auto_params ->
233 GrafiteAst.AutoBatch (loc,params)
234 | IDENT "cases"; what = tactic_term;
235 pattern = OPT pattern_spec;
236 specs = intros_spec ->
237 let pattern = match pattern with
238 | None -> None, [], Some Ast.UserInput
239 | Some pattern -> pattern
241 GrafiteAst.Cases (loc, what, pattern, specs)
242 | IDENT "clear"; ids = LIST1 IDENT ->
243 GrafiteAst.Clear (loc, ids)
244 | IDENT "clearbody"; id = IDENT ->
245 GrafiteAst.ClearBody (loc,id)
246 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
247 GrafiteAst.Change (loc, what, t)
248 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
249 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
250 let times = match times with None -> 1 | Some i -> i in
251 GrafiteAst.Compose (loc, t1, t2, times, specs)
252 | IDENT "constructor"; n = int ->
253 GrafiteAst.Constructor (loc, n)
254 | IDENT "contradiction" ->
255 GrafiteAst.Contradiction loc
256 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
257 GrafiteAst.Cut (loc, ident, t)
258 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
259 let idents = match idents with None -> [] | Some idents -> idents in
260 GrafiteAst.Decompose (loc, idents)
261 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
262 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
263 GrafiteAst.Destruct (loc, xts)
264 | IDENT "elim"; what = tactic_term; using = using;
265 pattern = OPT pattern_spec;
266 ispecs = intros_spec ->
267 let pattern = match pattern with
268 | None -> None, [], Some Ast.UserInput
269 | Some pattern -> pattern
271 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
272 | IDENT "elimType"; what = tactic_term; using = using;
273 (num, idents) = intros_spec ->
274 GrafiteAst.ElimType (loc, what, using, (num, idents))
275 | IDENT "exact"; t = tactic_term ->
276 GrafiteAst.Exact (loc, t)
278 GrafiteAst.Exists loc
279 | IDENT "fail" -> GrafiteAst.Fail loc
280 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
283 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
284 ("the pattern cannot specify the term to replace, only its"
285 ^ " paths in the hypotheses and in the conclusion")))
287 GrafiteAst.Fold (loc, kind, t, p)
289 GrafiteAst.Fourier loc
290 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
291 let idents = match idents with None -> [] | Some idents -> idents in
292 GrafiteAst.FwdSimpl (loc, hyp, idents)
293 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
294 GrafiteAst.Generalize (loc,p,id)
295 | IDENT "id" -> GrafiteAst.IdTac loc
296 | IDENT "intro"; ident = OPT IDENT ->
297 let idents = match ident with None -> [] | Some id -> [Some id] in
298 GrafiteAst.Intros (loc, (Some 1, idents))
299 | IDENT "intros"; specs = intros_spec ->
300 GrafiteAst.Intros (loc, specs)
301 | IDENT "inversion"; t = tactic_term ->
302 GrafiteAst.Inversion (loc, t)
304 linear = OPT [ IDENT "linear" ];
305 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
307 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
308 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
309 let linear = match linear with None -> false | Some _ -> true in
310 let to_what = match to_what with None -> [] | Some to_what -> to_what in
311 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
312 | IDENT "left" -> GrafiteAst.Left loc
313 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
314 GrafiteAst.LetIn (loc, t, where)
315 | kind = reduction_kind; p = pattern_spec ->
316 GrafiteAst.Reduce (loc, kind, p)
317 | IDENT "reflexivity" ->
318 GrafiteAst.Reflexivity loc
319 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
320 GrafiteAst.Replace (loc, p, t)
321 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
322 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
326 (HExtlib.Localized (loc,
327 (CicNotationParser.Parse_error
328 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
330 let n = match xnames with None -> [] | Some names -> names in
331 GrafiteAst.Rewrite (loc, d, t, p, n)
338 | IDENT "symmetry" ->
339 GrafiteAst.Symmetry loc
340 | IDENT "transitivity"; t = tactic_term ->
341 GrafiteAst.Transitivity (loc, t)
342 (* Produzioni Aggiunte *)
343 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
344 GrafiteAst.Assume (loc, id, t)
345 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
346 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
347 t' = tactic_term -> t']->
348 GrafiteAst.Suppose (loc, t, id, t1)
349 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
350 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
351 id2 = IDENT ; RPAREN ->
352 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
354 [ IDENT "using"; t=tactic_term -> `Term t
355 | params = auto_params -> `Auto params] ;
356 cont=by_continuation ->
358 BYC_done -> GrafiteAst.Bydone (loc, just)
359 | BYC_weproved (ty,id,t1) ->
360 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
361 | BYC_letsuchthat (id1,t1,id2,t2) ->
362 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
363 | BYC_wehaveand (id1,t1,id2,t2) ->
364 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
365 | 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']->
366 GrafiteAst.We_need_to_prove (loc, t, id, t1)
367 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
368 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
369 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
370 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
371 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
372 GrafiteAst.Byinduction(loc, t, id)
373 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
374 GrafiteAst.Thesisbecomes(loc, t)
375 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
376 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
377 GrafiteAst.Case(loc,id,params)
378 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
380 termine = tactic_term;
384 [ IDENT "using"; t=tactic_term -> `Term t
385 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
386 | IDENT "proof" -> `Proof
387 | params = auto_params -> `Auto params];
388 cont = rewriting_step_continuation ->
389 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
390 | IDENT "obtain" ; name = IDENT;
391 termine = tactic_term;
395 [ IDENT "using"; t=tactic_term -> `Term t
396 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
397 | IDENT "proof" -> `Proof
398 | params = auto_params -> `Auto params];
399 cont = rewriting_step_continuation ->
400 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
404 [ IDENT "using"; t=tactic_term -> `Term t
405 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
406 | IDENT "proof" -> `Proof
407 | params = auto_params -> `Auto params];
408 cont = rewriting_step_continuation ->
409 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
413 [ IDENT "paramodulation"
427 i = auto_fixed_param -> i,""
428 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
429 string_of_int v | v = IDENT -> v ] -> i,v ];
430 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
431 (match tl with Some l -> l | None -> []),
436 [ 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)
437 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
438 "done" -> BYC_weproved (ty,None,t1)
440 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
441 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
442 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
443 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
444 BYC_wehaveand (id1,t1,id2,t2)
447 rewriting_step_continuation : [
454 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
457 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
460 GrafiteAst.Seq (loc, ts)
463 [ tac = SELF; SYMBOL ";";
464 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
465 (GrafiteAst.Then (loc, tac, tacs))
468 [ IDENT "do"; count = int; tac = SELF ->
469 GrafiteAst.Do (loc, count, tac)
470 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
474 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
475 GrafiteAst.First (loc, tacs)
476 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
478 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
479 GrafiteAst.Solve (loc, tacs)
480 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
481 | LPAREN; tac = SELF; RPAREN -> tac
482 | tac = tactic -> tac
485 punctuation_tactical:
487 [ SYMBOL "[" -> GrafiteAst.Branch loc
488 | SYMBOL "|" -> GrafiteAst.Shift loc
489 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
490 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
491 | SYMBOL "]" -> GrafiteAst.Merge loc
492 | SYMBOL ";" -> GrafiteAst.Semicolon loc
493 | SYMBOL "." -> GrafiteAst.Dot loc
496 non_punctuation_tactical:
498 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
499 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
500 | IDENT "skip" -> GrafiteAst.Skip loc
504 [ [ IDENT "ntheorem" ] -> `Theorem
508 [ [ IDENT "definition" ] -> `Definition
509 | [ IDENT "fact" ] -> `Fact
510 | [ IDENT "lemma" ] -> `Lemma
511 | [ IDENT "remark" ] -> `Remark
512 | [ IDENT "theorem" ] -> `Theorem
516 [ attr = theorem_flavour -> attr
517 | [ IDENT "axiom" ] -> `Axiom
518 | [ IDENT "mutual" ] -> `MutualDefinition
523 params = LIST0 protected_binder_vars;
524 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
525 fst_constructors = LIST0 constructor SEP SYMBOL "|";
528 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
529 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
530 (name, true, typ, constructors) ] SEP "with" -> types
534 (fun (names, typ) acc ->
535 (List.map (fun name -> (name, typ)) names) @ acc)
538 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
539 let tl_ind_types = match tl with None -> [] | Some types -> types in
540 let ind_types = fst_ind_type :: tl_ind_types in
546 params = LIST0 protected_binder_vars;
547 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
551 SYMBOL ":" -> false,0
552 | SYMBOL ":"; SYMBOL ">" -> true,0
553 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
556 let b,n = coercion in
558 ] SEP SYMBOL ";"; SYMBOL "}" ->
561 (fun (names, typ) acc ->
562 (List.map (fun name -> (name, typ)) names) @ acc)
565 (params,name,typ,fields)
569 [ [ IDENT "check" ]; t = term ->
570 GrafiteAst.Check (loc, t)
571 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
572 GrafiteAst.Eval (loc, kind, t)
574 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
575 suri = QSTRING; prefix = OPT QSTRING;
576 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
577 let style = match style with
578 | None -> GrafiteAst.Declarative
579 | Some depth -> GrafiteAst.Procedural depth
581 let prefix = match prefix with None -> "" | Some prefix -> prefix in
582 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
583 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
584 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
585 | IDENT "auto"; params = auto_params ->
586 GrafiteAst.AutoInteractive (loc,params)
587 | [ IDENT "whelp"; "match" ] ; t = term ->
588 GrafiteAst.WMatch (loc,t)
589 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
590 GrafiteAst.WInstance (loc,t)
591 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
592 GrafiteAst.WLocate (loc,id)
593 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
594 GrafiteAst.WElim (loc, t)
595 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
596 GrafiteAst.WHint (loc,t)
600 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
601 let alpha = "[a-zA-Z]" in
602 let num = "[0-9]+" in
603 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
604 let decoration = "\\'" in
605 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
606 let rex = Str.regexp ("^"^ident^"$") in
607 if Str.string_match rex id 0 then
608 if (try ignore (UriManager.uri_of_string uri); true
609 with UriManager.IllFormedUri _ -> false)
611 LexiconAst.Ident_alias (id, uri)
614 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
616 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
617 Printf.sprintf "Not a valid identifier: %s" id)))
618 | IDENT "symbol"; symbol = QSTRING;
619 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
620 SYMBOL "="; dsc = QSTRING ->
622 match instance with Some i -> i | None -> 0
624 LexiconAst.Symbol_alias (symbol, instance, dsc)
626 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
627 SYMBOL "="; dsc = QSTRING ->
629 match instance with Some i -> i | None -> 0
631 LexiconAst.Number_alias (instance, dsc)
635 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
637 Ast.IdentArg (List.length l, id)
641 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
642 | IDENT "right"; IDENT "associative" -> Gramext.RightA
643 | IDENT "non"; IDENT "associative" -> Gramext.NonA
647 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
650 [ dir = OPT direction; s = QSTRING;
651 assoc = OPT associativity; prec = precedence;
654 [ blob = UNPARSED_AST ->
655 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
656 (CicNotationParser.parse_level2_ast
657 (Ulexing.from_utf8_string blob))
658 | blob = UNPARSED_META ->
659 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
660 (CicNotationParser.parse_level2_meta
661 (Ulexing.from_utf8_string blob))
665 | None -> default_associativity
666 | Some assoc -> assoc
669 add_raw_attribute ~text:s
670 (CicNotationParser.parse_level1_pattern prec
671 (Ulexing.from_utf8_string s))
673 (dir, p1, assoc, prec, p2)
677 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
678 | id = IDENT -> Ast.VarPattern id
679 | SYMBOL "_" -> Ast.ImplicitPattern
680 | LPAREN; terms = LIST1 SELF; RPAREN ->
684 | terms -> Ast.ApplPattern terms)
688 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
694 IDENT "include" ; path = QSTRING ->
695 loc,path,LexiconAst.WithPreferences
696 | IDENT "include'" ; path = QSTRING ->
697 loc,path,LexiconAst.WithoutPreferences
701 IDENT "set"; n = QSTRING; v = QSTRING ->
702 GrafiteAst.Set (loc, n, v)
703 | IDENT "drop" -> GrafiteAst.Drop loc
704 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
705 | IDENT "qed" -> GrafiteAst.Qed loc
706 | IDENT "variant" ; name = IDENT; SYMBOL ":";
707 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
710 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
711 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
712 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
713 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
714 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
715 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
716 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
717 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
720 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
721 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
722 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
723 | LETCOREC ; defs = let_defs ->
724 mk_rec_corec `CoInductive defs loc
725 | LETREC ; defs = let_defs ->
726 mk_rec_corec `Inductive defs loc
727 | IDENT "inductive"; spec = inductive_spec ->
728 let (params, ind_types) = spec in
729 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
730 | IDENT "coinductive"; spec = inductive_spec ->
731 let (params, ind_types) = spec in
732 let ind_types = (* set inductive flags to false (coinductive) *)
733 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
736 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
738 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
739 arity = OPT int ; saturations = OPT int;
740 composites = OPT (IDENT "nocomposites") ->
741 let arity = match arity with None -> 0 | Some x -> x in
742 let saturations = match saturations with None -> 0 | Some x -> x in
743 let composites = match composites with None -> true | Some _ -> false in
745 (loc, t, composites, arity, saturations)
746 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
747 GrafiteAst.PreferCoercion (loc, t)
748 | IDENT "pump" ; steps = int ->
749 GrafiteAst.Pump(loc,steps)
750 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
751 GrafiteAst.UnificationHint (loc, t, n)
752 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
753 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
754 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
755 let uris = List.map UriManager.uri_of_string uris in
756 GrafiteAst.Default (loc,what,uris)
757 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
758 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
759 refl = tactic_term -> refl ] ;
760 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
761 sym = tactic_term -> sym ] ;
762 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
763 trans = tactic_term -> trans ] ;
765 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
768 IDENT "alias" ; spec = alias_spec ->
769 LexiconAst.Alias (loc, spec)
770 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
771 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
772 | IDENT "interpretation"; id = QSTRING;
773 (symbol, args, l3) = interpretation ->
774 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
777 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
778 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
779 GrafiteAst.Tactic (loc, Some tac, punct)
780 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
781 | tac = ntactic; punct = punctuation_tactical ->
782 GrafiteAst.NTactic (loc, tac, punct)
783 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
784 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
785 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
786 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
787 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
791 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
792 GrafiteAst.Code (loc, ex)
794 GrafiteAst.Note (loc, str)
799 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
801 fun ?(never_include=false) ~include_paths status ->
802 status,LSome (GrafiteAst.Comment (loc, com))
803 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
805 fun ?(never_include=false) ~include_paths status ->
806 let _root, buri, fullpath, _rrelpath =
807 Librarian.baseuri_of_script ~include_paths fname
810 if never_include then raise (NoInclusionPerformed fullpath)
811 else LexiconEngine.eval_command status
812 (LexiconAst.Include (iloc,buri,mode,fullpath))
816 (GrafiteAst.Executable
817 (loc,GrafiteAst.Command
818 (loc,GrafiteAst.Include (iloc,buri))))
819 | scom = lexicon_command ; SYMBOL "." ->
820 fun ?(never_include=false) ~include_paths status ->
821 let status = LexiconEngine.eval_command status scom in
823 | EOI -> raise End_of_file
830 let _ = initialize_parser () ;;
832 let exc_located_wrapper f =
836 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
837 | Stdpp.Exc_located (floc, Stream.Error msg) ->
838 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
839 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
841 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
842 | Stdpp.Exc_located (floc, exn) ->
844 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
846 let parse_statement lexbuf =
848 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
850 let statement () = !grafite_parser.statement
852 let history = ref [] ;;
856 history := !grafite_parser :: !history;
857 grafite_parser := initial_parser ();
866 grafite_parser := gp;
870 (* vim:set foldmethod=marker: *)