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 let grammar = CicNotationParser.level2_ast_grammar
53 let term = CicNotationParser.term
54 let statement = Grammar.Entry.create grammar "statement"
56 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
58 let default_associativity = Gramext.NonA
60 let mk_rec_corec ind_kind defs loc =
61 (* In case of mutual definitions here we produce just
62 the syntax tree for the first one. The others will be
63 generated from the completely specified term just before
64 insertion in the environment. We use the flavour
65 `MutualDefinition to rememer this. *)
68 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
71 (fun var ty -> Ast.Binder (`Pi,var,ty)
75 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
79 let body = Ast.Ident (name,None) in
81 if List.length defs = 1 then
86 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
87 Some (Ast.LetRec (ind_kind, defs, body))))
89 type by_continuation =
91 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
92 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
93 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
96 GLOBAL: term statement;
97 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
98 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
100 [ id = IDENT -> Some id
101 | SYMBOL "_" -> None ]
103 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
105 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
108 [ IDENT "normalize" -> `Normalize
109 | IDENT "simplify" -> `Simpl
110 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
111 | IDENT "whd" -> `Whd ]
113 sequent_pattern_spec: [
117 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
118 (id,match path with Some p -> p | None -> Ast.UserInput) ];
119 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
121 match goal_path, hyp_paths with
122 None, [] -> Some Ast.UserInput
124 | Some goal_path, _ -> Some goal_path
133 [ "match" ; wanted = tactic_term ;
134 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
136 | sps = sequent_pattern_spec ->
139 let wanted,hyp_paths,goal_path =
140 match wanted_and_sps with
141 wanted,None -> wanted, [], Some Ast.UserInput
142 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
144 wanted, hyp_paths, goal_path ] ->
146 None -> None,[],Some Ast.UserInput
150 [ SYMBOL ">" -> `LeftToRight
151 | SYMBOL "<" -> `RightToLeft ]
153 int: [ [ num = NUMBER -> int_of_string num ] ];
155 [ idents = OPT ident_list0 ->
156 match idents with None -> [] | Some idents -> idents
160 [ OPT [ IDENT "names" ];
161 num = OPT [ num = int -> num ];
162 idents = intros_names ->
166 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
168 [ IDENT "absurd"; t = tactic_term ->
169 GrafiteAst.Absurd (loc, t)
170 | IDENT "apply"; t = tactic_term ->
171 GrafiteAst.Apply (loc, t)
172 | IDENT "applyP"; t = tactic_term ->
173 GrafiteAst.ApplyP (loc, t)
174 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
175 GrafiteAst.ApplyS (loc, t, params)
176 | IDENT "assumption" ->
177 GrafiteAst.Assumption loc
178 | IDENT "autobatch"; params = auto_params ->
179 GrafiteAst.AutoBatch (loc,params)
180 | IDENT "cases"; what = tactic_term;
181 pattern = OPT pattern_spec;
182 specs = intros_spec ->
183 let pattern = match pattern with
184 | None -> None, [], Some Ast.UserInput
185 | Some pattern -> pattern
187 GrafiteAst.Cases (loc, what, pattern, specs)
188 | IDENT "clear"; ids = LIST1 IDENT ->
189 GrafiteAst.Clear (loc, ids)
190 | IDENT "clearbody"; id = IDENT ->
191 GrafiteAst.ClearBody (loc,id)
192 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
193 GrafiteAst.Change (loc, what, t)
194 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
195 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
196 let times = match times with None -> 1 | Some i -> i in
197 GrafiteAst.Compose (loc, t1, t2, times, specs)
198 | IDENT "constructor"; n = int ->
199 GrafiteAst.Constructor (loc, n)
200 | IDENT "contradiction" ->
201 GrafiteAst.Contradiction loc
202 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
203 GrafiteAst.Cut (loc, ident, t)
204 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
205 let idents = match idents with None -> [] | Some idents -> idents in
206 GrafiteAst.Decompose (loc, idents)
207 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
208 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
209 GrafiteAst.Destruct (loc, xts)
210 | IDENT "elim"; what = tactic_term; using = using;
211 pattern = OPT pattern_spec;
212 (num, idents) = intros_spec ->
213 let pattern = match pattern with
214 | None -> None, [], Some Ast.UserInput
215 | Some pattern -> pattern
217 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
218 | IDENT "elimType"; what = tactic_term; using = using;
219 (num, idents) = intros_spec ->
220 GrafiteAst.ElimType (loc, what, using, (num, idents))
221 | IDENT "exact"; t = tactic_term ->
222 GrafiteAst.Exact (loc, t)
224 GrafiteAst.Exists loc
225 | IDENT "fail" -> GrafiteAst.Fail loc
226 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
229 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
230 ("the pattern cannot specify the term to replace, only its"
231 ^ " paths in the hypotheses and in the conclusion")))
233 GrafiteAst.Fold (loc, kind, t, p)
235 GrafiteAst.Fourier loc
236 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
237 let idents = match idents with None -> [] | Some idents -> idents in
238 GrafiteAst.FwdSimpl (loc, hyp, idents)
239 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
240 GrafiteAst.Generalize (loc,p,id)
241 | IDENT "id" -> GrafiteAst.IdTac loc
242 | IDENT "intro"; ident = OPT IDENT ->
243 let idents = match ident with None -> [] | Some id -> [Some id] in
244 GrafiteAst.Intros (loc, (Some 1, idents))
245 | IDENT "intros"; specs = intros_spec ->
246 GrafiteAst.Intros (loc, specs)
247 | IDENT "inversion"; t = tactic_term ->
248 GrafiteAst.Inversion (loc, t)
250 linear = OPT [ IDENT "linear" ];
251 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
253 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
254 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
255 let linear = match linear with None -> false | Some _ -> true in
256 let to_what = match to_what with None -> [] | Some to_what -> to_what in
257 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
258 | IDENT "left" -> GrafiteAst.Left loc
259 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
260 GrafiteAst.LetIn (loc, t, where)
261 | kind = reduction_kind; p = pattern_spec ->
262 GrafiteAst.Reduce (loc, kind, p)
263 | IDENT "reflexivity" ->
264 GrafiteAst.Reflexivity loc
265 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
266 GrafiteAst.Replace (loc, p, t)
267 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
268 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
272 (HExtlib.Localized (loc,
273 (CicNotationParser.Parse_error
274 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
276 let n = match xnames with None -> [] | Some names -> names in
277 GrafiteAst.Rewrite (loc, d, t, p, n)
284 | IDENT "symmetry" ->
285 GrafiteAst.Symmetry loc
286 | IDENT "transitivity"; t = tactic_term ->
287 GrafiteAst.Transitivity (loc, t)
288 (* Produzioni Aggiunte *)
289 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
290 GrafiteAst.Assume (loc, id, t)
291 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
292 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
293 t' = tactic_term -> t']->
294 GrafiteAst.Suppose (loc, t, id, t1)
295 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
296 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
297 id2 = IDENT ; RPAREN ->
298 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
300 [ IDENT "using"; t=tactic_term -> `Term t
301 | params = auto_params -> `Auto params] ;
302 cont=by_continuation ->
304 BYC_done -> GrafiteAst.Bydone (loc, just)
305 | BYC_weproved (ty,id,t1) ->
306 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
307 | BYC_letsuchthat (id1,t1,id2,t2) ->
308 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
309 | BYC_wehaveand (id1,t1,id2,t2) ->
310 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
311 | 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']->
312 GrafiteAst.We_need_to_prove (loc, t, id, t1)
313 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
314 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
315 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
316 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
317 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
318 GrafiteAst.Byinduction(loc, t, id)
319 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
320 GrafiteAst.Thesisbecomes(loc, t)
321 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
322 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
323 GrafiteAst.Case(loc,id,params)
324 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
326 termine = tactic_term;
330 [ IDENT "using"; t=tactic_term -> `Term t
331 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
332 | IDENT "proof" -> `Proof
333 | params = auto_params -> `Auto params];
334 cont = rewriting_step_continuation ->
335 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
336 | IDENT "obtain" ; name = IDENT;
337 termine = tactic_term;
341 [ IDENT "using"; t=tactic_term -> `Term t
342 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
343 | IDENT "proof" -> `Proof
344 | params = auto_params -> `Auto params];
345 cont = rewriting_step_continuation ->
346 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
350 [ IDENT "using"; t=tactic_term -> `Term t
351 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
352 | IDENT "proof" -> `Proof
353 | params = auto_params -> `Auto params];
354 cont = rewriting_step_continuation ->
355 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
359 [ IDENT "paramodulation"
371 i = auto_fixed_param -> i,""
372 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
373 string_of_int v | v = IDENT -> v ] -> i,v ];
374 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
375 (match tl with Some l -> l | None -> []),
380 [ 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)
381 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
382 "done" -> BYC_weproved (ty,None,t1)
384 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
385 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
386 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
387 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
388 BYC_wehaveand (id1,t1,id2,t2)
391 rewriting_step_continuation : [
398 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
401 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
404 GrafiteAst.Seq (loc, ts)
407 [ tac = SELF; SYMBOL ";";
408 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
409 (GrafiteAst.Then (loc, tac, tacs))
412 [ IDENT "do"; count = int; tac = SELF ->
413 GrafiteAst.Do (loc, count, tac)
414 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
418 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
419 GrafiteAst.First (loc, tacs)
420 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
422 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
423 GrafiteAst.Solve (loc, tacs)
424 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
425 | LPAREN; tac = SELF; RPAREN -> tac
426 | tac = tactic -> tac
429 punctuation_tactical:
431 [ SYMBOL "[" -> GrafiteAst.Branch loc
432 | SYMBOL "|" -> GrafiteAst.Shift loc
433 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
434 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
435 | SYMBOL "]" -> GrafiteAst.Merge loc
436 | SYMBOL ";" -> GrafiteAst.Semicolon loc
437 | SYMBOL "." -> GrafiteAst.Dot loc
440 non_punctuation_tactical:
442 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
443 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
444 | IDENT "skip" -> GrafiteAst.Skip loc
448 [ [ IDENT "definition" ] -> `Definition
449 | [ IDENT "fact" ] -> `Fact
450 | [ IDENT "lemma" ] -> `Lemma
451 | [ IDENT "remark" ] -> `Remark
452 | [ IDENT "theorem" ] -> `Theorem
456 [ attr = theorem_flavour -> attr
457 | [ IDENT "axiom" ] -> `Axiom
458 | [ IDENT "mutual" ] -> `MutualDefinition
462 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
463 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
464 fst_constructors = LIST0 constructor SEP SYMBOL "|";
467 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
468 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
469 (name, true, typ, constructors) ] SEP "with" -> types
473 (fun (names, typ) acc ->
474 (List.map (fun name -> (name, typ)) names) @ acc)
477 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
478 let tl_ind_types = match tl with None -> [] | Some types -> types in
479 let ind_types = fst_ind_type :: tl_ind_types in
484 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
485 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
489 SYMBOL ":" -> false,0
490 | SYMBOL ":"; SYMBOL ">" -> true,0
491 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
494 let b,n = coercion in
496 ] SEP SYMBOL ";"; SYMBOL "}" ->
499 (fun (names, typ) acc ->
500 (List.map (fun name -> (name, typ)) names) @ acc)
503 (params,name,typ,fields)
507 [ [ IDENT "check" ]; t = term ->
508 GrafiteAst.Check (loc, t)
510 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
511 suri = QSTRING; prefix = OPT QSTRING;
512 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
513 let style = match style with
514 | None -> GrafiteAst.Declarative
515 | Some depth -> GrafiteAst.Procedural depth
517 let prefix = match prefix with None -> "" | Some prefix -> prefix in
518 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
519 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
520 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
521 | IDENT "auto"; params = auto_params ->
522 GrafiteAst.AutoInteractive (loc,params)
523 | [ IDENT "whelp"; "match" ] ; t = term ->
524 GrafiteAst.WMatch (loc,t)
525 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
526 GrafiteAst.WInstance (loc,t)
527 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
528 GrafiteAst.WLocate (loc,id)
529 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
530 GrafiteAst.WElim (loc, t)
531 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
532 GrafiteAst.WHint (loc,t)
536 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
537 let alpha = "[a-zA-Z]" in
538 let num = "[0-9]+" in
539 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
540 let decoration = "\\'" in
541 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
542 let rex = Str.regexp ("^"^ident^"$") in
543 if Str.string_match rex id 0 then
544 if (try ignore (UriManager.uri_of_string uri); true
545 with UriManager.IllFormedUri _ -> false)
547 LexiconAst.Ident_alias (id, uri)
550 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
552 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
553 Printf.sprintf "Not a valid identifier: %s" id)))
554 | IDENT "symbol"; symbol = QSTRING;
555 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
556 SYMBOL "="; dsc = QSTRING ->
558 match instance with Some i -> i | None -> 0
560 LexiconAst.Symbol_alias (symbol, instance, dsc)
562 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
563 SYMBOL "="; dsc = QSTRING ->
565 match instance with Some i -> i | None -> 0
567 LexiconAst.Number_alias (instance, dsc)
571 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
573 Ast.IdentArg (List.length l, id)
577 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
578 | IDENT "right"; IDENT "associative" -> Gramext.RightA
579 | IDENT "non"; IDENT "associative" -> Gramext.NonA
583 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
586 [ dir = OPT direction; s = QSTRING;
587 assoc = OPT associativity; prec = precedence;
590 [ blob = UNPARSED_AST ->
591 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
592 (CicNotationParser.parse_level2_ast
593 (Ulexing.from_utf8_string blob))
594 | blob = UNPARSED_META ->
595 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
596 (CicNotationParser.parse_level2_meta
597 (Ulexing.from_utf8_string blob))
601 | None -> default_associativity
602 | Some assoc -> assoc
605 add_raw_attribute ~text:s
606 (CicNotationParser.parse_level1_pattern prec
607 (Ulexing.from_utf8_string s))
609 (dir, p1, assoc, prec, p2)
613 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
614 | id = IDENT -> Ast.VarPattern id
615 | SYMBOL "_" -> Ast.ImplicitPattern
616 | LPAREN; terms = LIST1 SELF; RPAREN ->
620 | terms -> Ast.ApplPattern terms)
624 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
630 IDENT "include" ; path = QSTRING ->
631 loc,path,LexiconAst.WithPreferences
632 | IDENT "include'" ; path = QSTRING ->
633 loc,path,LexiconAst.WithoutPreferences
637 IDENT "set"; n = QSTRING; v = QSTRING ->
638 GrafiteAst.Set (loc, n, v)
639 | IDENT "drop" -> GrafiteAst.Drop loc
640 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
641 | IDENT "qed" -> GrafiteAst.Qed loc
642 | IDENT "variant" ; name = IDENT; SYMBOL ":";
643 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
646 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
647 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
648 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
649 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
650 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
653 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
654 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
655 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
656 | LETCOREC ; defs = CicNotationParser.let_defs ->
657 mk_rec_corec `CoInductive defs loc
658 | LETREC ; defs = CicNotationParser.let_defs ->
659 mk_rec_corec `Inductive defs loc
660 | IDENT "inductive"; spec = inductive_spec ->
661 let (params, ind_types) = spec in
662 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
663 | IDENT "coinductive"; spec = inductive_spec ->
664 let (params, ind_types) = spec in
665 let ind_types = (* set inductive flags to false (coinductive) *)
666 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
669 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
671 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
672 arity = OPT int ; saturations = OPT int;
673 composites = OPT (IDENT "nocomposites") ->
674 let arity = match arity with None -> 0 | Some x -> x in
675 let saturations = match saturations with None -> 0 | Some x -> x in
676 let composites = match composites with None -> true | Some _ -> false in
678 (loc, t, composites, arity, saturations)
679 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
680 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
681 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
682 let uris = List.map UriManager.uri_of_string uris in
683 GrafiteAst.Default (loc,what,uris)
684 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
685 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
686 refl = tactic_term -> refl ] ;
687 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
688 sym = tactic_term -> sym ] ;
689 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
690 trans = tactic_term -> trans ] ;
692 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
695 IDENT "alias" ; spec = alias_spec ->
696 LexiconAst.Alias (loc, spec)
697 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
698 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
699 | IDENT "interpretation"; id = QSTRING;
700 (symbol, args, l3) = interpretation ->
701 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
704 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
705 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
706 GrafiteAst.Tactic (loc, Some tac, punct)
707 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
708 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
709 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
710 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
714 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
715 GrafiteAst.Code (loc, ex)
717 GrafiteAst.Note (loc, str)
722 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
724 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
725 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
727 fun ?(never_include=false) ~include_paths status ->
728 let _root, buri, fullpath, _rrelpath =
729 Librarian.baseuri_of_script ~include_paths fname
732 if never_include then raise (NoInclusionPerformed fullpath)
733 else LexiconEngine.eval_command status
734 (LexiconAst.Include (iloc,buri,mode,fullpath))
738 (GrafiteAst.Executable
739 (loc,GrafiteAst.Command
740 (loc,GrafiteAst.Include (iloc,buri))))
741 | scom = lexicon_command ; SYMBOL "." ->
742 fun ?(never_include=false) ~include_paths status ->
743 let status = LexiconEngine.eval_command status scom in
745 | EOI -> raise End_of_file
750 let exc_located_wrapper f =
754 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
755 | Stdpp.Exc_located (floc, Stream.Error msg) ->
756 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
757 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
759 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
760 | Stdpp.Exc_located (floc, exn) ->
762 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
764 let parse_statement lexbuf =
766 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))