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 type 'a localized_option =
35 | LNone of GrafiteAst.loc
38 (CicNotationPt.term, CicNotationPt.term,
39 CicNotationPt.term GrafiteAst.reduction,
40 CicNotationPt.term CicNotationPt.obj, string)
44 include_paths:string list ->
45 LexiconEngine.status ->
46 LexiconEngine.status * ast_statement localized_option
48 let grammar = CicNotationParser.level2_ast_grammar
50 let term = CicNotationParser.term
51 let statement = Grammar.Entry.create grammar "statement"
53 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
55 let default_precedence = 50
56 let default_associativity = Gramext.NonA
58 type by_continuation =
60 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
61 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
62 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
65 GLOBAL: term statement;
66 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
67 tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
69 [ id = IDENT -> Some id
70 | SYMBOL "_" -> None ]
72 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
74 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
77 [ IDENT "normalize" -> `Normalize
78 | IDENT "reduce" -> `Reduce
79 | IDENT "simplify" -> `Simpl
80 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
81 | IDENT "whd" -> `Whd ]
83 sequent_pattern_spec: [
87 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
88 (id,match path with Some p -> p | None -> Ast.UserInput) ];
89 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
91 match goal_path, hyp_paths with
92 None, [] -> Some Ast.UserInput
94 | Some goal_path, _ -> Some goal_path
103 [ "match" ; wanted = tactic_term ;
104 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
106 | sps = sequent_pattern_spec ->
109 let wanted,hyp_paths,goal_path =
110 match wanted_and_sps with
111 wanted,None -> wanted, [], Some Ast.UserInput
112 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
114 wanted, hyp_paths, goal_path ] ->
116 None -> None,[],Some Ast.UserInput
120 [ SYMBOL ">" -> `LeftToRight
121 | SYMBOL "<" -> `RightToLeft ]
123 int: [ [ num = NUMBER -> int_of_string num ] ];
125 [ idents = OPT ident_list0 ->
126 match idents with None -> [] | Some idents -> idents
130 [ OPT [ IDENT "names" ];
131 num = OPT [ num = int -> num ];
132 idents = intros_names ->
136 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
138 [ IDENT "absurd"; t = tactic_term ->
139 GrafiteAst.Absurd (loc, t)
140 | IDENT "apply"; t = tactic_term ->
141 GrafiteAst.Apply (loc, t)
142 | IDENT "applyS"; t = tactic_term ; params =
143 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
144 string_of_int v | v = IDENT -> v ] -> i,v ] ->
145 GrafiteAst.ApplyS (loc, t, params)
146 | IDENT "assumption" ->
147 GrafiteAst.Assumption loc
148 | IDENT "autobatch"; params = auto_params ->
149 GrafiteAst.AutoBatch (loc,params)
150 | IDENT "cases"; what = tactic_term;
151 specs = intros_spec ->
152 GrafiteAst.Cases (loc, what, specs)
153 | IDENT "clear"; ids = LIST1 IDENT ->
154 GrafiteAst.Clear (loc, ids)
155 | IDENT "clearbody"; id = IDENT ->
156 GrafiteAst.ClearBody (loc,id)
157 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
158 GrafiteAst.Change (loc, what, t)
159 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
160 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
161 let times = match times with None -> 1 | Some i -> i in
162 GrafiteAst.Compose (loc, t1, t2, times, specs)
163 | IDENT "constructor"; n = int ->
164 GrafiteAst.Constructor (loc, n)
165 | IDENT "contradiction" ->
166 GrafiteAst.Contradiction loc
167 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
168 GrafiteAst.Cut (loc, ident, t)
169 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
170 let idents = match idents with None -> [] | Some idents -> idents in
171 GrafiteAst.Decompose (loc, idents)
172 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
173 | IDENT "destruct"; t = tactic_term ->
174 GrafiteAst.Destruct (loc, t)
175 | IDENT "elim"; what = tactic_term; using = using;
176 pattern = OPT pattern_spec;
177 (num, idents) = intros_spec ->
178 let pattern = match pattern with
179 | None -> None, [], Some Ast.UserInput
180 | Some pattern -> pattern
182 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
183 | IDENT "elimType"; what = tactic_term; using = using;
184 (num, idents) = intros_spec ->
185 GrafiteAst.ElimType (loc, what, using, (num, idents))
186 | IDENT "exact"; t = tactic_term ->
187 GrafiteAst.Exact (loc, t)
189 GrafiteAst.Exists loc
190 | IDENT "fail" -> GrafiteAst.Fail loc
191 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
194 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
195 ("the pattern cannot specify the term to replace, only its"
196 ^ " paths in the hypotheses and in the conclusion")))
198 GrafiteAst.Fold (loc, kind, t, p)
200 GrafiteAst.Fourier loc
201 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
202 let idents = match idents with None -> [] | Some idents -> idents in
203 GrafiteAst.FwdSimpl (loc, hyp, idents)
204 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
205 GrafiteAst.Generalize (loc,p,id)
206 | IDENT "id" -> GrafiteAst.IdTac loc
207 | IDENT "intro"; ident = OPT IDENT ->
208 let idents = match ident with None -> [] | Some id -> [Some id] in
209 GrafiteAst.Intros (loc, (Some 1, idents))
210 | IDENT "intros"; specs = intros_spec ->
211 GrafiteAst.Intros (loc, specs)
212 | IDENT "inversion"; t = tactic_term ->
213 GrafiteAst.Inversion (loc, t)
215 linear = OPT [ IDENT "linear" ];
216 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
218 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
219 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
220 let linear = match linear with None -> false | Some _ -> true in
221 let to_what = match to_what with None -> [] | Some to_what -> to_what in
222 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
223 | IDENT "left" -> GrafiteAst.Left loc
224 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
225 GrafiteAst.LetIn (loc, t, where)
226 | kind = reduction_kind; p = pattern_spec ->
227 GrafiteAst.Reduce (loc, kind, p)
228 | IDENT "reflexivity" ->
229 GrafiteAst.Reflexivity loc
230 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
231 GrafiteAst.Replace (loc, p, t)
232 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
233 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
237 (HExtlib.Localized (loc,
238 (CicNotationParser.Parse_error
239 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
241 let n = match xnames with None -> [] | Some names -> names in
242 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" ] -> GrafiteAst.Hint loc
463 | IDENT "auto"; params = auto_params ->
464 GrafiteAst.AutoInteractive (loc,params)
465 | [ IDENT "whelp"; "match" ] ; t = term ->
466 GrafiteAst.WMatch (loc,t)
467 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
468 GrafiteAst.WInstance (loc,t)
469 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
470 GrafiteAst.WLocate (loc,id)
471 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
472 GrafiteAst.WElim (loc, t)
473 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
474 GrafiteAst.WHint (loc,t)
478 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
479 let alpha = "[a-zA-Z]" in
480 let num = "[0-9]+" in
481 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
482 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
483 let rex = Str.regexp ("^"^ident^"$") in
484 if Str.string_match rex id 0 then
485 if (try ignore (UriManager.uri_of_string uri); true
486 with UriManager.IllFormedUri _ -> false)
488 LexiconAst.Ident_alias (id, uri)
491 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
493 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
494 Printf.sprintf "Not a valid identifier: %s" id)))
495 | IDENT "symbol"; symbol = QSTRING;
496 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
497 SYMBOL "="; dsc = QSTRING ->
499 match instance with Some i -> i | None -> 0
501 LexiconAst.Symbol_alias (symbol, instance, dsc)
503 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
504 SYMBOL "="; dsc = QSTRING ->
506 match instance with Some i -> i | None -> 0
508 LexiconAst.Number_alias (instance, dsc)
512 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
514 Ast.IdentArg (List.length l, id)
518 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
519 | IDENT "right"; IDENT "associative" -> Gramext.RightA
520 | IDENT "non"; IDENT "associative" -> Gramext.NonA
524 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
527 [ dir = OPT direction; s = QSTRING;
528 assoc = OPT associativity; prec = OPT precedence;
531 [ blob = UNPARSED_AST ->
532 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
533 (CicNotationParser.parse_level2_ast
534 (Ulexing.from_utf8_string blob))
535 | blob = UNPARSED_META ->
536 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
537 (CicNotationParser.parse_level2_meta
538 (Ulexing.from_utf8_string blob))
542 | None -> default_associativity
543 | Some assoc -> assoc
547 | None -> default_precedence
551 add_raw_attribute ~text:s
552 (CicNotationParser.parse_level1_pattern
553 (Ulexing.from_utf8_string s))
555 (dir, p1, assoc, prec, p2)
559 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
560 | id = IDENT -> Ast.VarPattern id
561 | SYMBOL "_" -> Ast.ImplicitPattern
562 | LPAREN; terms = LIST1 SELF; RPAREN ->
566 | terms -> Ast.ApplPattern terms)
570 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
576 IDENT "include" ; path = QSTRING ->
577 loc,path,LexiconAst.WithPreferences
578 | IDENT "include'" ; path = QSTRING ->
579 loc,path,LexiconAst.WithoutPreferences
583 IDENT "set"; n = QSTRING; v = QSTRING ->
584 GrafiteAst.Set (loc, n, v)
585 | IDENT "drop" -> GrafiteAst.Drop loc
586 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
587 | IDENT "qed" -> GrafiteAst.Qed loc
588 | IDENT "variant" ; name = IDENT; SYMBOL ":";
589 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
592 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
593 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
594 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
595 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
596 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
599 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
600 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
601 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
602 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
603 defs = CicNotationParser.let_defs ->
604 (* In case of mutual definitions here we produce just
605 the syntax tree for the first one. The others will be
606 generated from the completely specified term just before
607 insertion in the environment. We use the flavour
608 `MutualDefinition to rememer this. *)
611 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
614 (fun var ty -> Ast.Binder (`Pi,var,ty)
618 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
622 let body = Ast.Ident (name,None) in
624 if List.length defs = 1 then
629 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
630 Some (Ast.LetRec (ind_kind, defs, body))))
631 | IDENT "inductive"; spec = inductive_spec ->
632 let (params, ind_types) = spec in
633 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
634 | IDENT "coinductive"; spec = inductive_spec ->
635 let (params, ind_types) = spec in
636 let ind_types = (* set inductive flags to false (coinductive) *)
637 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
640 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
641 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
642 let arity = match arity with None -> 0 | Some x -> x in
643 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
644 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
645 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
646 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
647 let uris = List.map UriManager.uri_of_string uris in
648 GrafiteAst.Default (loc,what,uris)
649 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
650 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
651 refl = tactic_term -> refl ] ;
652 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
653 sym = tactic_term -> sym ] ;
654 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
655 trans = tactic_term -> trans ] ;
657 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
660 IDENT "alias" ; spec = alias_spec ->
661 LexiconAst.Alias (loc, spec)
662 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
663 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
664 | IDENT "interpretation"; id = QSTRING;
665 (symbol, args, l3) = interpretation ->
666 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
669 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
670 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
671 GrafiteAst.Tactic (loc, Some tac, punct)
672 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
673 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
674 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
675 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
679 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
680 GrafiteAst.Code (loc, ex)
682 GrafiteAst.Note (loc, str)
687 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
689 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
690 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
691 fun ~include_paths status ->
693 DependenciesParser.baseuri_of_script ~include_paths fname
696 LexiconEngine.eval_command status
697 (LexiconAst.Include (iloc,buri,mode,fullpath))
702 (GrafiteAst.Executable
703 (loc,GrafiteAst.Command
704 (loc,GrafiteAst.Include (iloc,buri))))
705 | scom = lexicon_command ; SYMBOL "." ->
706 fun ~include_paths status ->
707 let status = LexiconEngine.eval_command status scom in
709 | EOI -> raise End_of_file
714 let exc_located_wrapper f =
718 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
719 | Stdpp.Exc_located (floc, Stream.Error msg) ->
720 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
721 | Stdpp.Exc_located (floc, exn) ->
723 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
725 let parse_statement lexbuf =
727 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))