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"
425 i = auto_fixed_param -> i,""
426 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
427 string_of_int v | v = IDENT -> v ] -> i,v ];
428 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
429 (match tl with Some l -> l | None -> []),
434 [ 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)
435 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
436 "done" -> BYC_weproved (ty,None,t1)
438 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
439 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
440 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
441 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
442 BYC_wehaveand (id1,t1,id2,t2)
445 rewriting_step_continuation : [
452 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
455 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
458 GrafiteAst.Seq (loc, ts)
461 [ tac = SELF; SYMBOL ";";
462 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
463 (GrafiteAst.Then (loc, tac, tacs))
466 [ IDENT "do"; count = int; tac = SELF ->
467 GrafiteAst.Do (loc, count, tac)
468 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
472 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
473 GrafiteAst.First (loc, tacs)
474 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
476 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
477 GrafiteAst.Solve (loc, tacs)
478 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
479 | LPAREN; tac = SELF; RPAREN -> tac
480 | tac = tactic -> tac
483 punctuation_tactical:
485 [ SYMBOL "[" -> GrafiteAst.Branch loc
486 | SYMBOL "|" -> GrafiteAst.Shift loc
487 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
488 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
489 | SYMBOL "]" -> GrafiteAst.Merge loc
490 | SYMBOL ";" -> GrafiteAst.Semicolon loc
491 | SYMBOL "." -> GrafiteAst.Dot loc
494 non_punctuation_tactical:
496 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
497 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
498 | IDENT "skip" -> GrafiteAst.Skip loc
502 [ [ IDENT "ntheorem" ] -> `Theorem
506 [ [ IDENT "definition" ] -> `Definition
507 | [ IDENT "fact" ] -> `Fact
508 | [ IDENT "lemma" ] -> `Lemma
509 | [ IDENT "remark" ] -> `Remark
510 | [ IDENT "theorem" ] -> `Theorem
514 [ attr = theorem_flavour -> attr
515 | [ IDENT "axiom" ] -> `Axiom
516 | [ IDENT "mutual" ] -> `MutualDefinition
521 params = LIST0 protected_binder_vars;
522 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
523 fst_constructors = LIST0 constructor SEP SYMBOL "|";
526 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
527 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
528 (name, true, typ, constructors) ] SEP "with" -> types
532 (fun (names, typ) acc ->
533 (List.map (fun name -> (name, typ)) names) @ acc)
536 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
537 let tl_ind_types = match tl with None -> [] | Some types -> types in
538 let ind_types = fst_ind_type :: tl_ind_types in
544 params = LIST0 protected_binder_vars;
545 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
549 SYMBOL ":" -> false,0
550 | SYMBOL ":"; SYMBOL ">" -> true,0
551 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
554 let b,n = coercion in
556 ] SEP SYMBOL ";"; SYMBOL "}" ->
559 (fun (names, typ) acc ->
560 (List.map (fun name -> (name, typ)) names) @ acc)
563 (params,name,typ,fields)
567 [ [ IDENT "check" ]; t = term ->
568 GrafiteAst.Check (loc, t)
569 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
570 GrafiteAst.Eval (loc, kind, t)
572 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
573 suri = QSTRING; prefix = OPT QSTRING;
574 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
575 let style = match style with
576 | None -> GrafiteAst.Declarative
577 | Some depth -> GrafiteAst.Procedural depth
579 let prefix = match prefix with None -> "" | Some prefix -> prefix in
580 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
581 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
582 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
583 | IDENT "auto"; params = auto_params ->
584 GrafiteAst.AutoInteractive (loc,params)
585 | [ IDENT "whelp"; "match" ] ; t = term ->
586 GrafiteAst.WMatch (loc,t)
587 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
588 GrafiteAst.WInstance (loc,t)
589 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
590 GrafiteAst.WLocate (loc,id)
591 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
592 GrafiteAst.WElim (loc, t)
593 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
594 GrafiteAst.WHint (loc,t)
598 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
599 let alpha = "[a-zA-Z]" in
600 let num = "[0-9]+" in
601 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
602 let decoration = "\\'" in
603 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
604 let rex = Str.regexp ("^"^ident^"$") in
605 if Str.string_match rex id 0 then
606 if (try ignore (UriManager.uri_of_string uri); true
607 with UriManager.IllFormedUri _ -> false)
609 LexiconAst.Ident_alias (id, uri)
612 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
614 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
615 Printf.sprintf "Not a valid identifier: %s" id)))
616 | IDENT "symbol"; symbol = QSTRING;
617 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
618 SYMBOL "="; dsc = QSTRING ->
620 match instance with Some i -> i | None -> 0
622 LexiconAst.Symbol_alias (symbol, instance, dsc)
624 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
625 SYMBOL "="; dsc = QSTRING ->
627 match instance with Some i -> i | None -> 0
629 LexiconAst.Number_alias (instance, dsc)
633 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
635 Ast.IdentArg (List.length l, id)
639 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
640 | IDENT "right"; IDENT "associative" -> Gramext.RightA
641 | IDENT "non"; IDENT "associative" -> Gramext.NonA
645 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
648 [ dir = OPT direction; s = QSTRING;
649 assoc = OPT associativity; prec = precedence;
652 [ blob = UNPARSED_AST ->
653 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
654 (CicNotationParser.parse_level2_ast
655 (Ulexing.from_utf8_string blob))
656 | blob = UNPARSED_META ->
657 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
658 (CicNotationParser.parse_level2_meta
659 (Ulexing.from_utf8_string blob))
663 | None -> default_associativity
664 | Some assoc -> assoc
667 add_raw_attribute ~text:s
668 (CicNotationParser.parse_level1_pattern prec
669 (Ulexing.from_utf8_string s))
671 (dir, p1, assoc, prec, p2)
675 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
676 | id = IDENT -> Ast.VarPattern id
677 | SYMBOL "_" -> Ast.ImplicitPattern
678 | LPAREN; terms = LIST1 SELF; RPAREN ->
682 | terms -> Ast.ApplPattern terms)
686 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
692 IDENT "include" ; path = QSTRING ->
693 loc,path,LexiconAst.WithPreferences
694 | IDENT "include'" ; path = QSTRING ->
695 loc,path,LexiconAst.WithoutPreferences
699 IDENT "set"; n = QSTRING; v = QSTRING ->
700 GrafiteAst.Set (loc, n, v)
701 | IDENT "drop" -> GrafiteAst.Drop loc
702 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
703 | IDENT "qed" -> GrafiteAst.Qed loc
704 | IDENT "variant" ; name = IDENT; SYMBOL ":";
705 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
708 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
709 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
710 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
711 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
712 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
713 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
714 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
715 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
718 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
719 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
720 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
721 | LETCOREC ; defs = let_defs ->
722 mk_rec_corec `CoInductive defs loc
723 | LETREC ; defs = let_defs ->
724 mk_rec_corec `Inductive defs loc
725 | IDENT "inductive"; spec = inductive_spec ->
726 let (params, ind_types) = spec in
727 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
728 | IDENT "coinductive"; spec = inductive_spec ->
729 let (params, ind_types) = spec in
730 let ind_types = (* set inductive flags to false (coinductive) *)
731 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
734 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
736 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
737 arity = OPT int ; saturations = OPT int;
738 composites = OPT (IDENT "nocomposites") ->
739 let arity = match arity with None -> 0 | Some x -> x in
740 let saturations = match saturations with None -> 0 | Some x -> x in
741 let composites = match composites with None -> true | Some _ -> false in
743 (loc, t, composites, arity, saturations)
744 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
745 GrafiteAst.PreferCoercion (loc, t)
746 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
747 GrafiteAst.UnificationHint (loc, t, n)
748 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
749 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
750 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
751 let uris = List.map UriManager.uri_of_string uris in
752 GrafiteAst.Default (loc,what,uris)
753 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
754 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
755 refl = tactic_term -> refl ] ;
756 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
757 sym = tactic_term -> sym ] ;
758 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
759 trans = tactic_term -> trans ] ;
761 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
764 IDENT "alias" ; spec = alias_spec ->
765 LexiconAst.Alias (loc, spec)
766 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
767 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
768 | IDENT "interpretation"; id = QSTRING;
769 (symbol, args, l3) = interpretation ->
770 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
773 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
774 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
775 GrafiteAst.Tactic (loc, Some tac, punct)
776 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
777 | tac = ntactic; punct = punctuation_tactical ->
778 GrafiteAst.NTactic (loc, tac, punct)
779 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
780 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
781 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
782 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
783 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
787 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
788 GrafiteAst.Code (loc, ex)
790 GrafiteAst.Note (loc, str)
795 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
797 fun ?(never_include=false) ~include_paths status ->
798 status,LSome (GrafiteAst.Comment (loc, com))
799 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
801 fun ?(never_include=false) ~include_paths status ->
802 let _root, buri, fullpath, _rrelpath =
803 Librarian.baseuri_of_script ~include_paths fname
806 if never_include then raise (NoInclusionPerformed fullpath)
807 else LexiconEngine.eval_command status
808 (LexiconAst.Include (iloc,buri,mode,fullpath))
812 (GrafiteAst.Executable
813 (loc,GrafiteAst.Command
814 (loc,GrafiteAst.Include (iloc,buri))))
815 | scom = lexicon_command ; SYMBOL "." ->
816 fun ?(never_include=false) ~include_paths status ->
817 let status = LexiconEngine.eval_command status scom in
819 | EOI -> raise End_of_file
826 let _ = initialize_parser () ;;
828 let exc_located_wrapper f =
832 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
833 | Stdpp.Exc_located (floc, Stream.Error msg) ->
834 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
835 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
837 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
838 | Stdpp.Exc_located (floc, exn) ->
840 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
842 let parse_statement lexbuf =
844 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
846 let statement () = !grafite_parser.statement
848 let history = ref [] ;;
852 history := !grafite_parser :: !history;
853 grafite_parser := initial_parser ();
862 grafite_parser := gp;
866 (* vim:set foldmethod=marker: *)