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_precedence = 50
59 let default_associativity = Gramext.NonA
61 type by_continuation =
63 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
64 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
65 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
68 GLOBAL: term statement;
69 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
70 tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
72 [ id = IDENT -> Some id
73 | SYMBOL "_" -> None ]
75 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
77 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
80 [ IDENT "normalize" -> `Normalize
81 | IDENT "reduce" -> `Reduce
82 | IDENT "simplify" -> `Simpl
83 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
84 | IDENT "whd" -> `Whd ]
86 sequent_pattern_spec: [
90 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
91 (id,match path with Some p -> p | None -> Ast.UserInput) ];
92 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
94 match goal_path, hyp_paths with
95 None, [] -> Some Ast.UserInput
97 | Some goal_path, _ -> Some goal_path
106 [ "match" ; wanted = tactic_term ;
107 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
109 | sps = sequent_pattern_spec ->
112 let wanted,hyp_paths,goal_path =
113 match wanted_and_sps with
114 wanted,None -> wanted, [], Some Ast.UserInput
115 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
117 wanted, hyp_paths, goal_path ] ->
119 None -> None,[],Some Ast.UserInput
123 [ SYMBOL ">" -> `LeftToRight
124 | SYMBOL "<" -> `RightToLeft ]
126 int: [ [ num = NUMBER -> int_of_string num ] ];
128 [ idents = OPT ident_list0 ->
129 match idents with None -> [] | Some idents -> idents
133 [ OPT [ IDENT "names" ];
134 num = OPT [ num = int -> num ];
135 idents = intros_names ->
139 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
141 [ IDENT "absurd"; t = tactic_term ->
142 GrafiteAst.Absurd (loc, t)
143 | IDENT "apply"; t = tactic_term ->
144 GrafiteAst.Apply (loc, t)
145 | IDENT "applyS"; t = tactic_term ; params =
146 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
147 string_of_int v | v = IDENT -> v ] -> i,v ] ->
148 GrafiteAst.ApplyS (loc, t, params)
149 | IDENT "assumption" ->
150 GrafiteAst.Assumption loc
151 | IDENT "autobatch"; params = auto_params ->
152 GrafiteAst.AutoBatch (loc,params)
153 | IDENT "cases"; what = tactic_term;
154 specs = intros_spec ->
155 GrafiteAst.Cases (loc, what, specs)
156 | IDENT "clear"; ids = LIST1 IDENT ->
157 GrafiteAst.Clear (loc, ids)
158 | IDENT "clearbody"; id = IDENT ->
159 GrafiteAst.ClearBody (loc,id)
160 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
161 GrafiteAst.Change (loc, what, t)
162 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
163 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
164 let times = match times with None -> 1 | Some i -> i in
165 GrafiteAst.Compose (loc, t1, t2, times, specs)
166 | IDENT "constructor"; n = int ->
167 GrafiteAst.Constructor (loc, n)
168 | IDENT "contradiction" ->
169 GrafiteAst.Contradiction loc
170 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
171 GrafiteAst.Cut (loc, ident, t)
172 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
173 let idents = match idents with None -> [] | Some idents -> idents in
174 GrafiteAst.Decompose (loc, idents)
175 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
176 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
177 GrafiteAst.Destruct (loc, xts)
178 | IDENT "elim"; what = tactic_term; using = using;
179 pattern = OPT pattern_spec;
180 (num, idents) = intros_spec ->
181 let pattern = match pattern with
182 | None -> None, [], Some Ast.UserInput
183 | Some pattern -> pattern
185 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
186 | IDENT "elimType"; what = tactic_term; using = using;
187 (num, idents) = intros_spec ->
188 GrafiteAst.ElimType (loc, what, using, (num, idents))
189 | IDENT "exact"; t = tactic_term ->
190 GrafiteAst.Exact (loc, t)
192 GrafiteAst.Exists loc
193 | IDENT "fail" -> GrafiteAst.Fail loc
194 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
197 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
198 ("the pattern cannot specify the term to replace, only its"
199 ^ " paths in the hypotheses and in the conclusion")))
201 GrafiteAst.Fold (loc, kind, t, p)
203 GrafiteAst.Fourier loc
204 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
205 let idents = match idents with None -> [] | Some idents -> idents in
206 GrafiteAst.FwdSimpl (loc, hyp, idents)
207 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
208 GrafiteAst.Generalize (loc,p,id)
209 | IDENT "id" -> GrafiteAst.IdTac loc
210 | IDENT "intro"; ident = OPT IDENT ->
211 let idents = match ident with None -> [] | Some id -> [Some id] in
212 GrafiteAst.Intros (loc, (Some 1, idents))
213 | IDENT "intros"; specs = intros_spec ->
214 GrafiteAst.Intros (loc, specs)
215 | IDENT "inversion"; t = tactic_term ->
216 GrafiteAst.Inversion (loc, t)
218 linear = OPT [ IDENT "linear" ];
219 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
221 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
222 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
223 let linear = match linear with None -> false | Some _ -> true in
224 let to_what = match to_what with None -> [] | Some to_what -> to_what in
225 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
226 | IDENT "left" -> GrafiteAst.Left loc
227 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
228 GrafiteAst.LetIn (loc, t, where)
229 | kind = reduction_kind; p = pattern_spec ->
230 GrafiteAst.Reduce (loc, kind, p)
231 | IDENT "reflexivity" ->
232 GrafiteAst.Reflexivity loc
233 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
234 GrafiteAst.Replace (loc, p, t)
235 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
236 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
240 (HExtlib.Localized (loc,
241 (CicNotationParser.Parse_error
242 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
244 let n = match xnames with None -> [] | Some names -> names in
245 GrafiteAst.Rewrite (loc, d, t, p, n)
252 | IDENT "symmetry" ->
253 GrafiteAst.Symmetry loc
254 | IDENT "transitivity"; t = tactic_term ->
255 GrafiteAst.Transitivity (loc, t)
256 (* Produzioni Aggiunte *)
257 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
258 GrafiteAst.Assume (loc, id, t)
259 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
260 GrafiteAst.Suppose (loc, t, id, t1)
261 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
262 cont=by_continuation ->
263 let t' = match t with LNone _ -> None | LSome t -> Some t in
265 BYC_done -> GrafiteAst.Bydone (loc, t')
266 | BYC_weproved (ty,id,t1) ->
267 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
268 | BYC_letsuchthat (id1,t1,id2,t2) ->
271 raise (HExtlib.Localized
272 (floc,CicNotationParser.Parse_error
273 "tactic_term expected here"))
274 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
275 | BYC_wehaveand (id1,t1,id2,t2) ->
278 raise (HExtlib.Localized
279 (floc,CicNotationParser.Parse_error
280 "tactic_term expected here"))
281 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
282 | 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']->
283 GrafiteAst.We_need_to_prove (loc, t, id, t1)
284 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
285 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
286 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
287 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
288 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
289 GrafiteAst.Byinduction(loc, t, id)
290 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
291 GrafiteAst.Thesisbecomes(loc, t)
292 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
293 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
294 GrafiteAst.Case(loc,id,params)
296 [ IDENT "conclude" -> None
297 | IDENT "obtain" ; name = IDENT -> Some name ] ;
298 termine = tactic_term ;
303 [ t=tactic_term -> `Term t
304 | SYMBOL "_" ; params = auto_params' -> `Auto params
305 | IDENT "proof" -> `Proof] ;
306 cont = rewriting_step_continuation ->
307 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
312 [ t=tactic_term -> `Term t
313 | SYMBOL "_" ; params = auto_params' -> `Auto params
314 | IDENT "proof" -> `Proof] ;
315 cont=rewriting_step_continuation ->
316 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
321 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
322 string_of_int v | v = IDENT -> v ] -> i,v ] ->
327 [ LPAREN; params = auto_params; RPAREN -> params
332 [ IDENT "we" ; IDENT "proved" ; 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)
333 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
334 IDENT "done" -> BYC_weproved (ty,None,t1)
335 | IDENT "done" -> BYC_done
336 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
337 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
338 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
339 BYC_wehaveand (id1,t1,id2,t2)
342 rewriting_step_continuation : [
343 [ IDENT "done" -> true
349 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
352 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
355 GrafiteAst.Seq (loc, ts)
358 [ tac = SELF; SYMBOL ";";
359 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
360 (GrafiteAst.Then (loc, tac, tacs))
363 [ IDENT "do"; count = int; tac = SELF ->
364 GrafiteAst.Do (loc, count, tac)
365 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
369 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
370 GrafiteAst.First (loc, tacs)
371 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
373 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
374 GrafiteAst.Solve (loc, tacs)
375 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
376 | LPAREN; tac = SELF; RPAREN -> tac
377 | tac = tactic -> tac
380 punctuation_tactical:
382 [ SYMBOL "[" -> GrafiteAst.Branch loc
383 | SYMBOL "|" -> GrafiteAst.Shift loc
384 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
385 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
386 | SYMBOL "]" -> GrafiteAst.Merge loc
387 | SYMBOL ";" -> GrafiteAst.Semicolon loc
388 | SYMBOL "." -> GrafiteAst.Dot loc
391 non_punctuation_tactical:
393 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
394 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
395 | IDENT "skip" -> GrafiteAst.Skip loc
399 [ [ IDENT "definition" ] -> `Definition
400 | [ IDENT "fact" ] -> `Fact
401 | [ IDENT "lemma" ] -> `Lemma
402 | [ IDENT "remark" ] -> `Remark
403 | [ IDENT "theorem" ] -> `Theorem
407 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
408 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
409 fst_constructors = LIST0 constructor SEP SYMBOL "|";
412 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
413 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
414 (name, true, typ, constructors) ] SEP "with" -> types
418 (fun (names, typ) acc ->
419 (List.map (fun name -> (name, typ)) names) @ acc)
422 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
423 let tl_ind_types = match tl with None -> [] | Some types -> types in
424 let ind_types = fst_ind_type :: tl_ind_types in
429 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
430 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
434 SYMBOL ":" -> false,0
435 | SYMBOL ":"; SYMBOL ">" -> true,0
436 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
439 let b,n = coercion in
441 ] SEP SYMBOL ";"; SYMBOL "}" ->
444 (fun (names, typ) acc ->
445 (List.map (fun name -> (name, typ)) names) @ acc)
448 (params,name,typ,fields)
452 [ [ IDENT "check" ]; t = term ->
453 GrafiteAst.Check (loc, t)
455 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
456 suri = QSTRING; prefix = OPT QSTRING ->
457 let style = match style with
458 | None -> GrafiteAst.Declarative
459 | Some depth -> GrafiteAst.Procedural depth
461 let prefix = match prefix with None -> "" | Some prefix -> prefix in
462 GrafiteAst.Inline (loc,style,suri,prefix)
463 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
464 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
465 | IDENT "auto"; params = auto_params ->
466 GrafiteAst.AutoInteractive (loc,params)
467 | [ IDENT "whelp"; "match" ] ; t = term ->
468 GrafiteAst.WMatch (loc,t)
469 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
470 GrafiteAst.WInstance (loc,t)
471 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
472 GrafiteAst.WLocate (loc,id)
473 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
474 GrafiteAst.WElim (loc, t)
475 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
476 GrafiteAst.WHint (loc,t)
480 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
481 let alpha = "[a-zA-Z]" in
482 let num = "[0-9]+" in
483 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
484 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
485 let rex = Str.regexp ("^"^ident^"$") in
486 if Str.string_match rex id 0 then
487 if (try ignore (UriManager.uri_of_string uri); true
488 with UriManager.IllFormedUri _ -> false)
490 LexiconAst.Ident_alias (id, uri)
493 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
495 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
496 Printf.sprintf "Not a valid identifier: %s" id)))
497 | IDENT "symbol"; symbol = QSTRING;
498 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
499 SYMBOL "="; dsc = QSTRING ->
501 match instance with Some i -> i | None -> 0
503 LexiconAst.Symbol_alias (symbol, instance, dsc)
505 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
506 SYMBOL "="; dsc = QSTRING ->
508 match instance with Some i -> i | None -> 0
510 LexiconAst.Number_alias (instance, dsc)
514 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
516 Ast.IdentArg (List.length l, id)
520 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
521 | IDENT "right"; IDENT "associative" -> Gramext.RightA
522 | IDENT "non"; IDENT "associative" -> Gramext.NonA
526 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
529 [ dir = OPT direction; s = QSTRING;
530 assoc = OPT associativity; prec = OPT precedence;
533 [ blob = UNPARSED_AST ->
534 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
535 (CicNotationParser.parse_level2_ast
536 (Ulexing.from_utf8_string blob))
537 | blob = UNPARSED_META ->
538 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
539 (CicNotationParser.parse_level2_meta
540 (Ulexing.from_utf8_string blob))
544 | None -> default_associativity
545 | Some assoc -> assoc
549 | None -> default_precedence
553 add_raw_attribute ~text:s
554 (CicNotationParser.parse_level1_pattern
555 (Ulexing.from_utf8_string s))
557 (dir, p1, assoc, prec, p2)
561 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
562 | id = IDENT -> Ast.VarPattern id
563 | SYMBOL "_" -> Ast.ImplicitPattern
564 | LPAREN; terms = LIST1 SELF; RPAREN ->
568 | terms -> Ast.ApplPattern terms)
572 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
578 IDENT "include" ; path = QSTRING ->
579 loc,path,LexiconAst.WithPreferences
580 | IDENT "include'" ; path = QSTRING ->
581 loc,path,LexiconAst.WithoutPreferences
585 IDENT "set"; n = QSTRING; v = QSTRING ->
586 GrafiteAst.Set (loc, n, v)
587 | IDENT "drop" -> GrafiteAst.Drop loc
588 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
589 | IDENT "qed" -> GrafiteAst.Qed loc
590 | IDENT "variant" ; name = IDENT; SYMBOL ":";
591 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
594 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
595 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
596 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
597 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
598 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
601 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
602 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
603 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
604 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
605 defs = CicNotationParser.let_defs ->
606 (* In case of mutual definitions here we produce just
607 the syntax tree for the first one. The others will be
608 generated from the completely specified term just before
609 insertion in the environment. We use the flavour
610 `MutualDefinition to rememer this. *)
613 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
616 (fun var ty -> Ast.Binder (`Pi,var,ty)
620 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
624 let body = Ast.Ident (name,None) in
626 if List.length defs = 1 then
631 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
632 Some (Ast.LetRec (ind_kind, defs, body))))
633 | IDENT "inductive"; spec = inductive_spec ->
634 let (params, ind_types) = spec in
635 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
636 | IDENT "coinductive"; spec = inductive_spec ->
637 let (params, ind_types) = spec in
638 let ind_types = (* set inductive flags to false (coinductive) *)
639 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
642 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
643 | IDENT "coercion" ; suri = URI ; arity = OPT int ;
644 saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
645 let arity = match arity with None -> 0 | Some x -> x in
646 let saturations = match saturations with None -> 0 | Some x -> x in
647 let composites = match composites with None -> true | Some _ -> false in
649 (loc, UriManager.uri_of_string suri, composites, arity, saturations)
650 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
651 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
652 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
653 let uris = List.map UriManager.uri_of_string uris in
654 GrafiteAst.Default (loc,what,uris)
655 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
656 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
657 refl = tactic_term -> refl ] ;
658 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
659 sym = tactic_term -> sym ] ;
660 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
661 trans = tactic_term -> trans ] ;
663 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
666 IDENT "alias" ; spec = alias_spec ->
667 LexiconAst.Alias (loc, spec)
668 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
669 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
670 | IDENT "interpretation"; id = QSTRING;
671 (symbol, args, l3) = interpretation ->
672 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
675 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
676 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
677 GrafiteAst.Tactic (loc, Some tac, punct)
678 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
679 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
680 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
681 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
685 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
686 GrafiteAst.Code (loc, ex)
688 GrafiteAst.Note (loc, str)
693 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
695 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
696 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
697 fun ?(never_include=false) ~include_paths status ->
698 let _root, buri, fullpath, _rrelpath =
699 Librarian.baseuri_of_script ~include_paths fname
702 if never_include then raise (NoInclusionPerformed fullpath)
703 else LexiconEngine.eval_command status
704 (LexiconAst.Include (iloc,buri,mode,fullpath))
709 (GrafiteAst.Executable
710 (loc,GrafiteAst.Command
711 (loc,GrafiteAst.Include (iloc,buri))))
712 | scom = lexicon_command ; SYMBOL "." ->
713 fun ?(never_include=false) ~include_paths status ->
714 let status = LexiconEngine.eval_command status scom in
716 | EOI -> raise End_of_file
721 let exc_located_wrapper f =
725 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
726 | Stdpp.Exc_located (floc, Stream.Error msg) ->
727 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
728 | Stdpp.Exc_located (floc, exn) ->
730 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
732 let parse_statement lexbuf =
734 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))