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 [ IDENT "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 ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
541 let rex = Str.regexp ("^"^ident^"$") in
542 if Str.string_match rex id 0 then
543 if (try ignore (UriManager.uri_of_string uri); true
544 with UriManager.IllFormedUri _ -> false)
546 LexiconAst.Ident_alias (id, uri)
549 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
551 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
552 Printf.sprintf "Not a valid identifier: %s" id)))
553 | IDENT "symbol"; symbol = QSTRING;
554 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
555 SYMBOL "="; dsc = QSTRING ->
557 match instance with Some i -> i | None -> 0
559 LexiconAst.Symbol_alias (symbol, instance, dsc)
561 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
562 SYMBOL "="; dsc = QSTRING ->
564 match instance with Some i -> i | None -> 0
566 LexiconAst.Number_alias (instance, dsc)
570 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
572 Ast.IdentArg (List.length l, id)
576 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
577 | IDENT "right"; IDENT "associative" -> Gramext.RightA
578 | IDENT "non"; IDENT "associative" -> Gramext.NonA
582 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
585 [ dir = OPT direction; s = QSTRING;
586 assoc = OPT associativity; prec = precedence;
589 [ blob = UNPARSED_AST ->
590 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
591 (CicNotationParser.parse_level2_ast
592 (Ulexing.from_utf8_string blob))
593 | blob = UNPARSED_META ->
594 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
595 (CicNotationParser.parse_level2_meta
596 (Ulexing.from_utf8_string blob))
600 | None -> default_associativity
601 | Some assoc -> assoc
604 add_raw_attribute ~text:s
605 (CicNotationParser.parse_level1_pattern prec
606 (Ulexing.from_utf8_string s))
608 (dir, p1, assoc, prec, p2)
612 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
613 | id = IDENT -> Ast.VarPattern id
614 | SYMBOL "_" -> Ast.ImplicitPattern
615 | LPAREN; terms = LIST1 SELF; RPAREN ->
619 | terms -> Ast.ApplPattern terms)
623 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
629 IDENT "include" ; path = QSTRING ->
630 loc,path,LexiconAst.WithPreferences
631 | IDENT "include'" ; path = QSTRING ->
632 loc,path,LexiconAst.WithoutPreferences
636 IDENT "set"; n = QSTRING; v = QSTRING ->
637 GrafiteAst.Set (loc, n, v)
638 | IDENT "drop" -> GrafiteAst.Drop loc
639 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
640 | IDENT "qed" -> GrafiteAst.Qed loc
641 | IDENT "variant" ; name = IDENT; SYMBOL ":";
642 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
645 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
646 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
647 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
648 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
649 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
652 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
653 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
654 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
655 | LETCOREC ; defs = CicNotationParser.let_defs ->
656 mk_rec_corec `CoInductive defs loc
657 | LETREC ; defs = CicNotationParser.let_defs ->
658 mk_rec_corec `Inductive defs loc
659 | IDENT "inductive"; spec = inductive_spec ->
660 let (params, ind_types) = spec in
661 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
662 | IDENT "coinductive"; spec = inductive_spec ->
663 let (params, ind_types) = spec in
664 let ind_types = (* set inductive flags to false (coinductive) *)
665 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
668 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
670 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
671 arity = OPT int ; saturations = OPT int;
672 composites = OPT (IDENT "nocomposites") ->
673 let arity = match arity with None -> 0 | Some x -> x in
674 let saturations = match saturations with None -> 0 | Some x -> x in
675 let composites = match composites with None -> true | Some _ -> false in
677 (loc, t, composites, arity, saturations)
678 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
679 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
680 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
681 let uris = List.map UriManager.uri_of_string uris in
682 GrafiteAst.Default (loc,what,uris)
683 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
684 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
685 refl = tactic_term -> refl ] ;
686 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
687 sym = tactic_term -> sym ] ;
688 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
689 trans = tactic_term -> trans ] ;
691 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
694 IDENT "alias" ; spec = alias_spec ->
695 LexiconAst.Alias (loc, spec)
696 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
697 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
698 | IDENT "interpretation"; id = QSTRING;
699 (symbol, args, l3) = interpretation ->
700 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
703 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
704 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
705 GrafiteAst.Tactic (loc, Some tac, punct)
706 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
707 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
708 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
709 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
713 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
714 GrafiteAst.Code (loc, ex)
716 GrafiteAst.Note (loc, str)
721 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
723 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
724 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
726 fun ?(never_include=false) ~include_paths status ->
727 let _root, buri, fullpath, _rrelpath =
728 Librarian.baseuri_of_script ~include_paths fname
731 if never_include then raise (NoInclusionPerformed fullpath)
732 else LexiconEngine.eval_command status
733 (LexiconAst.Include (iloc,buri,mode,fullpath))
737 (GrafiteAst.Executable
738 (loc,GrafiteAst.Command
739 (loc,GrafiteAst.Include (iloc,buri))))
740 | scom = lexicon_command ; SYMBOL "." ->
741 fun ?(never_include=false) ~include_paths status ->
742 let status = LexiconEngine.eval_command status scom in
744 | EOI -> raise End_of_file
749 let exc_located_wrapper f =
753 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
754 | Stdpp.Exc_located (floc, Stream.Error msg) ->
755 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
756 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
758 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
759 | Stdpp.Exc_located (floc, exn) ->
761 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
763 let parse_statement lexbuf =
765 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))