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 "simplify" -> `Simpl
82 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
83 | IDENT "whd" -> `Whd ]
85 sequent_pattern_spec: [
89 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
90 (id,match path with Some p -> p | None -> Ast.UserInput) ];
91 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
93 match goal_path, hyp_paths with
94 None, [] -> Some Ast.UserInput
96 | Some goal_path, _ -> Some goal_path
105 [ "match" ; wanted = tactic_term ;
106 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
108 | sps = sequent_pattern_spec ->
111 let wanted,hyp_paths,goal_path =
112 match wanted_and_sps with
113 wanted,None -> wanted, [], Some Ast.UserInput
114 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
116 wanted, hyp_paths, goal_path ] ->
118 None -> None,[],Some Ast.UserInput
122 [ SYMBOL ">" -> `LeftToRight
123 | SYMBOL "<" -> `RightToLeft ]
125 int: [ [ num = NUMBER -> int_of_string num ] ];
127 [ idents = OPT ident_list0 ->
128 match idents with None -> [] | Some idents -> idents
132 [ OPT [ IDENT "names" ];
133 num = OPT [ num = int -> num ];
134 idents = intros_names ->
138 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
140 [ IDENT "absurd"; t = tactic_term ->
141 GrafiteAst.Absurd (loc, t)
142 | IDENT "apply"; t = tactic_term ->
143 GrafiteAst.Apply (loc, t)
144 | IDENT "applyS"; t = tactic_term ; params =
145 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
146 string_of_int v | v = IDENT -> v ] -> i,v ] ->
147 GrafiteAst.ApplyS (loc, t, params)
148 | IDENT "assumption" ->
149 GrafiteAst.Assumption loc
150 | IDENT "autobatch"; params = auto_params ->
151 GrafiteAst.AutoBatch (loc,params)
152 | IDENT "cases"; what = tactic_term;
153 specs = intros_spec ->
154 GrafiteAst.Cases (loc, what, specs)
155 | IDENT "clear"; ids = LIST1 IDENT ->
156 GrafiteAst.Clear (loc, ids)
157 | IDENT "clearbody"; id = IDENT ->
158 GrafiteAst.ClearBody (loc,id)
159 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
160 GrafiteAst.Change (loc, what, t)
161 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
162 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
163 let times = match times with None -> 1 | Some i -> i in
164 GrafiteAst.Compose (loc, t1, t2, times, specs)
165 | IDENT "constructor"; n = int ->
166 GrafiteAst.Constructor (loc, n)
167 | IDENT "contradiction" ->
168 GrafiteAst.Contradiction loc
169 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
170 GrafiteAst.Cut (loc, ident, t)
171 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
172 let idents = match idents with None -> [] | Some idents -> idents in
173 GrafiteAst.Decompose (loc, idents)
174 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
175 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
176 GrafiteAst.Destruct (loc, xts)
177 | IDENT "elim"; what = tactic_term; using = using;
178 pattern = OPT pattern_spec;
179 (num, idents) = intros_spec ->
180 let pattern = match pattern with
181 | None -> None, [], Some Ast.UserInput
182 | Some pattern -> pattern
184 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
185 | IDENT "elimType"; what = tactic_term; using = using;
186 (num, idents) = intros_spec ->
187 GrafiteAst.ElimType (loc, what, using, (num, idents))
188 | IDENT "exact"; t = tactic_term ->
189 GrafiteAst.Exact (loc, t)
191 GrafiteAst.Exists loc
192 | IDENT "fail" -> GrafiteAst.Fail loc
193 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
196 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
197 ("the pattern cannot specify the term to replace, only its"
198 ^ " paths in the hypotheses and in the conclusion")))
200 GrafiteAst.Fold (loc, kind, t, p)
202 GrafiteAst.Fourier loc
203 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
204 let idents = match idents with None -> [] | Some idents -> idents in
205 GrafiteAst.FwdSimpl (loc, hyp, idents)
206 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
207 GrafiteAst.Generalize (loc,p,id)
208 | IDENT "id" -> GrafiteAst.IdTac loc
209 | IDENT "intro"; ident = OPT IDENT ->
210 let idents = match ident with None -> [] | Some id -> [Some id] in
211 GrafiteAst.Intros (loc, (Some 1, idents))
212 | IDENT "intros"; specs = intros_spec ->
213 GrafiteAst.Intros (loc, specs)
214 | IDENT "inversion"; t = tactic_term ->
215 GrafiteAst.Inversion (loc, t)
217 linear = OPT [ IDENT "linear" ];
218 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
220 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
221 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
222 let linear = match linear with None -> false | Some _ -> true in
223 let to_what = match to_what with None -> [] | Some to_what -> to_what in
224 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
225 | IDENT "left" -> GrafiteAst.Left loc
226 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
227 GrafiteAst.LetIn (loc, t, where)
228 | kind = reduction_kind; p = pattern_spec ->
229 GrafiteAst.Reduce (loc, kind, p)
230 | IDENT "reflexivity" ->
231 GrafiteAst.Reflexivity loc
232 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
233 GrafiteAst.Replace (loc, p, t)
234 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
235 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
239 (HExtlib.Localized (loc,
240 (CicNotationParser.Parse_error
241 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
243 let n = match xnames with None -> [] | Some names -> names in
244 GrafiteAst.Rewrite (loc, d, t, p, n)
251 | IDENT "symmetry" ->
252 GrafiteAst.Symmetry loc
253 | IDENT "transitivity"; t = tactic_term ->
254 GrafiteAst.Transitivity (loc, t)
255 (* Produzioni Aggiunte *)
256 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
257 GrafiteAst.Assume (loc, id, t)
258 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
259 GrafiteAst.Suppose (loc, t, id, t1)
260 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
261 cont=by_continuation ->
262 let t' = match t with LNone _ -> None | LSome t -> Some t in
264 BYC_done -> GrafiteAst.Bydone (loc, t')
265 | BYC_weproved (ty,id,t1) ->
266 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
267 | BYC_letsuchthat (id1,t1,id2,t2) ->
270 raise (HExtlib.Localized
271 (floc,CicNotationParser.Parse_error
272 "tactic_term expected here"))
273 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
274 | BYC_wehaveand (id1,t1,id2,t2) ->
277 raise (HExtlib.Localized
278 (floc,CicNotationParser.Parse_error
279 "tactic_term expected here"))
280 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
281 | 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']->
282 GrafiteAst.We_need_to_prove (loc, t, id, t1)
283 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
284 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
285 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
286 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
287 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
288 GrafiteAst.Byinduction(loc, t, id)
289 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
290 GrafiteAst.Thesisbecomes(loc, t)
291 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
292 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
293 GrafiteAst.Case(loc,id,params)
295 [ IDENT "conclude" -> None
296 | IDENT "obtain" ; name = IDENT -> Some name ] ;
297 termine = tactic_term ;
302 [ t=tactic_term -> `Term t
303 | SYMBOL "_" ; params = auto_params' -> `Auto params
304 | IDENT "proof" -> `Proof] ;
305 cont = rewriting_step_continuation ->
306 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
311 [ t=tactic_term -> `Term t
312 | SYMBOL "_" ; params = auto_params' -> `Auto params
313 | IDENT "proof" -> `Proof] ;
314 cont=rewriting_step_continuation ->
315 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
320 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
321 string_of_int v | v = IDENT -> v ] -> i,v ] ->
326 [ LPAREN; params = auto_params; RPAREN -> params
331 [ 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)
332 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
333 IDENT "done" -> BYC_weproved (ty,None,t1)
334 | IDENT "done" -> BYC_done
335 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
336 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
337 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
338 BYC_wehaveand (id1,t1,id2,t2)
341 rewriting_step_continuation : [
342 [ IDENT "done" -> true
348 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
351 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
354 GrafiteAst.Seq (loc, ts)
357 [ tac = SELF; SYMBOL ";";
358 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
359 (GrafiteAst.Then (loc, tac, tacs))
362 [ IDENT "do"; count = int; tac = SELF ->
363 GrafiteAst.Do (loc, count, tac)
364 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
368 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
369 GrafiteAst.First (loc, tacs)
370 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
372 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
373 GrafiteAst.Solve (loc, tacs)
374 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
375 | LPAREN; tac = SELF; RPAREN -> tac
376 | tac = tactic -> tac
379 punctuation_tactical:
381 [ SYMBOL "[" -> GrafiteAst.Branch loc
382 | SYMBOL "|" -> GrafiteAst.Shift loc
383 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
384 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
385 | SYMBOL "]" -> GrafiteAst.Merge loc
386 | SYMBOL ";" -> GrafiteAst.Semicolon loc
387 | SYMBOL "." -> GrafiteAst.Dot loc
390 non_punctuation_tactical:
392 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
393 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
394 | IDENT "skip" -> GrafiteAst.Skip loc
398 [ [ IDENT "definition" ] -> `Definition
399 | [ IDENT "fact" ] -> `Fact
400 | [ IDENT "lemma" ] -> `Lemma
401 | [ IDENT "remark" ] -> `Remark
402 | [ IDENT "theorem" ] -> `Theorem
406 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
407 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
408 fst_constructors = LIST0 constructor SEP SYMBOL "|";
411 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
412 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
413 (name, true, typ, constructors) ] SEP "with" -> types
417 (fun (names, typ) acc ->
418 (List.map (fun name -> (name, typ)) names) @ acc)
421 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
422 let tl_ind_types = match tl with None -> [] | Some types -> types in
423 let ind_types = fst_ind_type :: tl_ind_types in
428 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
429 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
433 SYMBOL ":" -> false,0
434 | SYMBOL ":"; SYMBOL ">" -> true,0
435 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
438 let b,n = coercion in
440 ] SEP SYMBOL ";"; SYMBOL "}" ->
443 (fun (names, typ) acc ->
444 (List.map (fun name -> (name, typ)) names) @ acc)
447 (params,name,typ,fields)
451 [ [ IDENT "check" ]; t = term ->
452 GrafiteAst.Check (loc, t)
454 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
455 suri = QSTRING; prefix = OPT QSTRING ->
456 let style = match style with
457 | None -> GrafiteAst.Declarative
458 | Some depth -> GrafiteAst.Procedural depth
460 let prefix = match prefix with None -> "" | Some prefix -> prefix in
461 GrafiteAst.Inline (loc,style,suri,prefix)
462 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
463 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
464 | IDENT "auto"; params = auto_params ->
465 GrafiteAst.AutoInteractive (loc,params)
466 | [ IDENT "whelp"; "match" ] ; t = term ->
467 GrafiteAst.WMatch (loc,t)
468 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
469 GrafiteAst.WInstance (loc,t)
470 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
471 GrafiteAst.WLocate (loc,id)
472 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
473 GrafiteAst.WElim (loc, t)
474 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
475 GrafiteAst.WHint (loc,t)
479 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
480 let alpha = "[a-zA-Z]" in
481 let num = "[0-9]+" in
482 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
483 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
484 let rex = Str.regexp ("^"^ident^"$") in
485 if Str.string_match rex id 0 then
486 if (try ignore (UriManager.uri_of_string uri); true
487 with UriManager.IllFormedUri _ -> false)
489 LexiconAst.Ident_alias (id, uri)
492 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
494 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
495 Printf.sprintf "Not a valid identifier: %s" id)))
496 | IDENT "symbol"; symbol = QSTRING;
497 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
498 SYMBOL "="; dsc = QSTRING ->
500 match instance with Some i -> i | None -> 0
502 LexiconAst.Symbol_alias (symbol, instance, dsc)
504 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
505 SYMBOL "="; dsc = QSTRING ->
507 match instance with Some i -> i | None -> 0
509 LexiconAst.Number_alias (instance, dsc)
513 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
515 Ast.IdentArg (List.length l, id)
519 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
520 | IDENT "right"; IDENT "associative" -> Gramext.RightA
521 | IDENT "non"; IDENT "associative" -> Gramext.NonA
525 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
528 [ dir = OPT direction; s = QSTRING;
529 assoc = OPT associativity; prec = OPT precedence;
532 [ blob = UNPARSED_AST ->
533 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
534 (CicNotationParser.parse_level2_ast
535 (Ulexing.from_utf8_string blob))
536 | blob = UNPARSED_META ->
537 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
538 (CicNotationParser.parse_level2_meta
539 (Ulexing.from_utf8_string blob))
543 | None -> default_associativity
544 | Some assoc -> assoc
548 | None -> default_precedence
552 add_raw_attribute ~text:s
553 (CicNotationParser.parse_level1_pattern
554 (Ulexing.from_utf8_string s))
556 (dir, p1, assoc, prec, p2)
560 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
561 | id = IDENT -> Ast.VarPattern id
562 | SYMBOL "_" -> Ast.ImplicitPattern
563 | LPAREN; terms = LIST1 SELF; RPAREN ->
567 | terms -> Ast.ApplPattern terms)
571 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
577 IDENT "include" ; path = QSTRING ->
578 loc,path,LexiconAst.WithPreferences
579 | IDENT "include'" ; path = QSTRING ->
580 loc,path,LexiconAst.WithoutPreferences
584 IDENT "set"; n = QSTRING; v = QSTRING ->
585 GrafiteAst.Set (loc, n, v)
586 | IDENT "drop" -> GrafiteAst.Drop loc
587 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
588 | IDENT "qed" -> GrafiteAst.Qed loc
589 | IDENT "variant" ; name = IDENT; SYMBOL ":";
590 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
593 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
594 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
595 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
596 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
597 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
600 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
601 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
602 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
603 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
604 defs = CicNotationParser.let_defs ->
605 (* In case of mutual definitions here we produce just
606 the syntax tree for the first one. The others will be
607 generated from the completely specified term just before
608 insertion in the environment. We use the flavour
609 `MutualDefinition to rememer this. *)
612 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
615 (fun var ty -> Ast.Binder (`Pi,var,ty)
619 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
623 let body = Ast.Ident (name,None) in
625 if List.length defs = 1 then
630 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
631 Some (Ast.LetRec (ind_kind, defs, body))))
632 | IDENT "inductive"; spec = inductive_spec ->
633 let (params, ind_types) = spec in
634 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
635 | IDENT "coinductive"; spec = inductive_spec ->
636 let (params, ind_types) = spec in
637 let ind_types = (* set inductive flags to false (coinductive) *)
638 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
641 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
642 | IDENT "coercion" ; suri = URI ; arity = OPT int ;
643 saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
644 let arity = match arity with None -> 0 | Some x -> x in
645 let saturations = match saturations with None -> 0 | Some x -> x in
646 let composites = match composites with None -> true | Some _ -> false in
648 (loc, UriManager.uri_of_string suri, composites, arity, saturations)
649 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
650 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
651 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
652 let uris = List.map UriManager.uri_of_string uris in
653 GrafiteAst.Default (loc,what,uris)
654 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
655 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
656 refl = tactic_term -> refl ] ;
657 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
658 sym = tactic_term -> sym ] ;
659 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
660 trans = tactic_term -> trans ] ;
662 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
665 IDENT "alias" ; spec = alias_spec ->
666 LexiconAst.Alias (loc, spec)
667 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
668 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
669 | IDENT "interpretation"; id = QSTRING;
670 (symbol, args, l3) = interpretation ->
671 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
674 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
675 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
676 GrafiteAst.Tactic (loc, Some tac, punct)
677 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
678 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
679 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
680 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
684 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
685 GrafiteAst.Code (loc, ex)
687 GrafiteAst.Note (loc, str)
692 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
694 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
695 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
696 fun ?(never_include=false) ~include_paths status ->
697 let _root, buri, fullpath, _rrelpath =
698 Librarian.baseuri_of_script ~include_paths fname
701 if never_include then raise (NoInclusionPerformed fullpath)
702 else LexiconEngine.eval_command status
703 (LexiconAst.Include (iloc,buri,mode,fullpath))
708 (GrafiteAst.Executable
709 (loc,GrafiteAst.Command
710 (loc,GrafiteAst.Include (iloc,buri))))
711 | scom = lexicon_command ; SYMBOL "." ->
712 fun ?(never_include=false) ~include_paths status ->
713 let status = LexiconEngine.eval_command status scom in
715 | EOI -> raise End_of_file
720 let exc_located_wrapper f =
724 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
725 | Stdpp.Exc_located (floc, Stream.Error msg) ->
726 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
727 | Stdpp.Exc_located (floc, exn) ->
729 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
731 let parse_statement lexbuf =
733 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))