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/
30 module Ast = CicNotationPt
32 type 'a localized_option =
34 | LNone of GrafiteAst.loc
37 (CicNotationPt.term, CicNotationPt.term,
38 CicNotationPt.term GrafiteAst.reduction,
39 CicNotationPt.term CicNotationPt.obj, string)
43 include_paths:string list ->
44 LexiconEngine.status ->
45 LexiconEngine.status * ast_statement localized_option
47 let grammar = CicNotationParser.level2_ast_grammar
49 let term = CicNotationParser.term
50 let statement = Grammar.Entry.create grammar "statement"
52 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
54 let default_precedence = 50
55 let default_associativity = Gramext.NonA
57 type by_continuation =
59 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
60 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
61 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
64 GLOBAL: term statement;
65 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
66 tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
67 ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
69 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
72 [ IDENT "normalize" -> `Normalize
73 | IDENT "reduce" -> `Reduce
74 | IDENT "simplify" -> `Simpl
75 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
76 | IDENT "whd" -> `Whd ]
78 sequent_pattern_spec: [
82 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
83 (id,match path with Some p -> p | None -> Ast.UserInput) ];
84 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
86 match goal_path, hyp_paths with
87 None, [] -> Some Ast.UserInput
89 | Some goal_path, _ -> Some goal_path
98 [ "match" ; wanted = tactic_term ;
99 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
101 | sps = sequent_pattern_spec ->
104 let wanted,hyp_paths,goal_path =
105 match wanted_and_sps with
106 wanted,None -> wanted, [], Some Ast.UserInput
107 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
109 wanted, hyp_paths, goal_path ] ->
111 None -> None,[],Some Ast.UserInput
115 [ SYMBOL ">" -> `LeftToRight
116 | SYMBOL "<" -> `RightToLeft ]
118 int: [ [ num = NUMBER -> int_of_string num ] ];
120 [ idents = OPT ident_list0 ->
121 match idents with None -> [] | Some idents -> idents
125 [ OPT [ IDENT "names" ];
126 num = OPT [ num = int -> num ];
127 idents = intros_names ->
131 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
133 [ IDENT "absurd"; t = tactic_term ->
134 GrafiteAst.Absurd (loc, t)
135 | IDENT "apply"; t = tactic_term ->
136 GrafiteAst.Apply (loc, t)
137 | IDENT "applyS"; t = tactic_term ; params =
138 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
139 string_of_int v | v = IDENT -> v ] -> i,v ] ->
140 GrafiteAst.ApplyS (loc, t, params)
141 | IDENT "assumption" ->
142 GrafiteAst.Assumption loc
143 | IDENT "auto"; params = auto_params ->
144 GrafiteAst.Auto (loc,params)
145 | IDENT "cases"; what = tactic_term;
146 (num, idents) = intros_spec ->
147 GrafiteAst.Cases (loc, what, idents)
148 | IDENT "clear"; ids = LIST1 IDENT ->
149 GrafiteAst.Clear (loc, ids)
150 | IDENT "clearbody"; id = IDENT ->
151 GrafiteAst.ClearBody (loc,id)
152 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
153 GrafiteAst.Change (loc, what, t)
154 | IDENT "constructor"; n = int ->
155 GrafiteAst.Constructor (loc, n)
156 | IDENT "contradiction" ->
157 GrafiteAst.Contradiction loc
158 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
159 GrafiteAst.Cut (loc, ident, t)
160 | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
161 idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
162 let types = match types with None -> [] | Some types -> types in
163 let idents = match idents with None -> [] | Some idents -> idents in
164 let to_spec id = GrafiteAst.Ident id in
165 GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
166 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
167 | IDENT "destruct"; t = tactic_term ->
168 GrafiteAst.Destruct (loc, t)
169 | IDENT "elim"; what = tactic_term; using = using;
170 (num, idents) = intros_spec ->
171 GrafiteAst.Elim (loc, what, using, num, idents)
172 | IDENT "elimType"; what = tactic_term; using = using;
173 (num, idents) = intros_spec ->
174 GrafiteAst.ElimType (loc, what, using, num, idents)
175 | IDENT "exact"; t = tactic_term ->
176 GrafiteAst.Exact (loc, t)
178 GrafiteAst.Exists loc
179 | IDENT "fail" -> GrafiteAst.Fail loc
180 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
183 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
184 ("the pattern cannot specify the term to replace, only its"
185 ^ " paths in the hypotheses and in the conclusion")))
187 GrafiteAst.Fold (loc, kind, t, p)
189 GrafiteAst.Fourier loc
190 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
191 let idents = match idents with None -> [] | Some idents -> idents in
192 GrafiteAst.FwdSimpl (loc, hyp, idents)
193 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
194 GrafiteAst.Generalize (loc,p,id)
195 | IDENT "goal"; n = int ->
196 GrafiteAst.Goal (loc, n)
197 | IDENT "id" -> GrafiteAst.IdTac loc
198 | IDENT "intro"; ident = OPT IDENT ->
199 let idents = match ident with None -> [] | Some id -> [id] in
200 GrafiteAst.Intros (loc, Some 1, idents)
201 | IDENT "intros"; (num, idents) = intros_spec ->
202 GrafiteAst.Intros (loc, num, idents)
203 | IDENT "inversion"; t = tactic_term ->
204 GrafiteAst.Inversion (loc, t)
206 linear = OPT [ IDENT "linear" ];
207 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
209 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
210 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
211 let linear = match linear with None -> false | Some _ -> true in
212 let to_what = match to_what with None -> [] | Some to_what -> to_what in
213 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
214 | IDENT "left" -> GrafiteAst.Left loc
215 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
216 GrafiteAst.LetIn (loc, t, where)
217 | kind = reduction_kind; p = pattern_spec ->
218 GrafiteAst.Reduce (loc, kind, p)
219 | IDENT "reflexivity" ->
220 GrafiteAst.Reflexivity loc
221 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
222 GrafiteAst.Replace (loc, p, t)
223 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
224 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
228 (HExtlib.Localized (loc,
229 (CicNotationParser.Parse_error
230 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
232 let n = match xnames with None -> [] | Some names -> names in
233 GrafiteAst.Rewrite (loc, d, t, p, n)
242 | IDENT "symmetry" ->
243 GrafiteAst.Symmetry loc
244 | IDENT "transitivity"; t = tactic_term ->
245 GrafiteAst.Transitivity (loc, t)
246 (* Produzioni Aggiunte *)
247 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
248 GrafiteAst.Assume (loc, id, t)
249 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
250 GrafiteAst.Suppose (loc, t, id, t1)
251 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
252 cont=by_continuation ->
253 let t' = match t with LNone _ -> None | LSome t -> Some t in
255 BYC_done -> GrafiteAst.Bydone (loc, t')
256 | BYC_weproved (ty,id,t1) ->
257 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
258 | BYC_letsuchthat (id1,t1,id2,t2) ->
261 raise (HExtlib.Localized
262 (floc,CicNotationParser.Parse_error
263 "tactic_term expected here"))
264 | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
265 | BYC_wehaveand (id1,t1,id2,t2) ->
268 raise (HExtlib.Localized
269 (floc,CicNotationParser.Parse_error
270 "tactic_term expected here"))
271 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
272 | 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']->
273 GrafiteAst.We_need_to_prove (loc, t, id, t1)
274 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
275 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
276 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
277 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
278 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
279 GrafiteAst.Byinduction(loc, t, id)
280 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
281 GrafiteAst.Thesisbecomes(loc, t)
282 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
283 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
284 GrafiteAst.Case(loc,id,params)
285 | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation ->
286 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
287 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
288 cont=rewriting_step_continuation ->
289 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
294 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
295 string_of_int v | v = IDENT -> v ] -> i,v ] ->
300 [ LPAREN; params = auto_params; RPAREN -> params
305 [ 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)
306 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
307 IDENT "done" -> BYC_weproved (ty,None,t1)
308 | IDENT "done" -> BYC_done
309 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
310 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
311 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
312 BYC_wehaveand (id1,t1,id2,t2)
315 rewriting_step_continuation : [
316 [ IDENT "done" -> true
322 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
325 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
328 GrafiteAst.Seq (loc, ts)
331 [ tac = SELF; SYMBOL ";";
332 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
333 (GrafiteAst.Then (loc, tac, tacs))
336 [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
337 GrafiteAst.Do (loc, count, tac)
338 | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
342 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
343 GrafiteAst.First (loc, tacs)
344 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
346 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
347 GrafiteAst.Solve (loc, tacs)
348 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
349 | LPAREN; tac = SELF; RPAREN -> tac
350 | tac = tactic -> GrafiteAst.Tactic (loc, tac)
353 punctuation_tactical:
355 [ SYMBOL "[" -> GrafiteAst.Branch loc
356 | SYMBOL "|" -> GrafiteAst.Shift loc
357 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
358 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
359 | SYMBOL "]" -> GrafiteAst.Merge loc
360 | SYMBOL ";" -> GrafiteAst.Semicolon loc
361 | SYMBOL "." -> GrafiteAst.Dot loc
366 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
367 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
368 | IDENT "skip" -> GrafiteAst.Skip loc
369 | tac = atomic_tactical LEVEL "loops" -> tac
373 [ [ IDENT "definition" ] -> `Definition
374 | [ IDENT "fact" ] -> `Fact
375 | [ IDENT "lemma" ] -> `Lemma
376 | [ IDENT "remark" ] -> `Remark
377 | [ IDENT "theorem" ] -> `Theorem
381 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
382 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
383 fst_constructors = LIST0 constructor SEP SYMBOL "|";
386 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
387 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
388 (name, true, typ, constructors) ] SEP "with" -> types
392 (fun (names, typ) acc ->
393 (List.map (fun name -> (name, typ)) names) @ acc)
396 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
397 let tl_ind_types = match tl with None -> [] | Some types -> types in
398 let ind_types = fst_ind_type :: tl_ind_types in
403 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
404 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
408 SYMBOL ":" -> false,0
409 | SYMBOL ":"; SYMBOL ">" -> true,0
410 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
413 let b,n = coercion in
415 ] SEP SYMBOL ";"; SYMBOL "}" ->
418 (fun (names, typ) acc ->
419 (List.map (fun name -> (name, typ)) names) @ acc)
422 (params,name,typ,fields)
426 [ [ IDENT "check" ]; t = term ->
427 GrafiteAst.Check (loc, t)
429 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
430 suri = QSTRING; prefix = OPT QSTRING ->
431 let style = match style with
432 | None -> GrafiteAst.Declarative
433 | Some depth -> GrafiteAst.Procedural depth
435 let prefix = match prefix with None -> "" | Some prefix -> prefix in
436 GrafiteAst.Inline (loc,style,suri,prefix)
437 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
438 | [ IDENT "whelp"; "match" ] ; t = term ->
439 GrafiteAst.WMatch (loc,t)
440 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
441 GrafiteAst.WInstance (loc,t)
442 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
443 GrafiteAst.WLocate (loc,id)
444 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
445 GrafiteAst.WElim (loc, t)
446 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
447 GrafiteAst.WHint (loc,t)
451 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
452 let alpha = "[a-zA-Z]" in
453 let num = "[0-9]+" in
454 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
455 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
456 let rex = Str.regexp ("^"^ident^"$") in
457 if Str.string_match rex id 0 then
458 if (try ignore (UriManager.uri_of_string uri); true
459 with UriManager.IllFormedUri _ -> false)
461 LexiconAst.Ident_alias (id, uri)
464 (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
466 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
467 sprintf "Not a valid identifier: %s" id)))
468 | IDENT "symbol"; symbol = QSTRING;
469 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
470 SYMBOL "="; dsc = QSTRING ->
472 match instance with Some i -> i | None -> 0
474 LexiconAst.Symbol_alias (symbol, instance, dsc)
476 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
477 SYMBOL "="; dsc = QSTRING ->
479 match instance with Some i -> i | None -> 0
481 LexiconAst.Number_alias (instance, dsc)
485 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
487 Ast.IdentArg (List.length l, id)
491 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
492 | IDENT "right"; IDENT "associative" -> Gramext.RightA
493 | IDENT "non"; IDENT "associative" -> Gramext.NonA
497 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
500 [ dir = OPT direction; s = QSTRING;
501 assoc = OPT associativity; prec = OPT precedence;
504 [ blob = UNPARSED_AST ->
505 add_raw_attribute ~text:(sprintf "@{%s}" blob)
506 (CicNotationParser.parse_level2_ast
507 (Ulexing.from_utf8_string blob))
508 | blob = UNPARSED_META ->
509 add_raw_attribute ~text:(sprintf "${%s}" blob)
510 (CicNotationParser.parse_level2_meta
511 (Ulexing.from_utf8_string blob))
515 | None -> default_associativity
516 | Some assoc -> assoc
520 | None -> default_precedence
524 add_raw_attribute ~text:s
525 (CicNotationParser.parse_level1_pattern
526 (Ulexing.from_utf8_string s))
528 (dir, p1, assoc, prec, p2)
532 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
533 | id = IDENT -> Ast.VarPattern id
534 | SYMBOL "_" -> Ast.ImplicitPattern
535 | LPAREN; terms = LIST1 SELF; RPAREN ->
539 | terms -> Ast.ApplPattern terms)
543 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
549 IDENT "include" ; path = QSTRING ->
550 loc,path,LexiconAst.WithPreferences
551 | IDENT "include'" ; path = QSTRING ->
552 loc,path,LexiconAst.WithoutPreferences
556 IDENT "set"; n = QSTRING; v = QSTRING ->
557 GrafiteAst.Set (loc, n, v)
558 | IDENT "drop" -> GrafiteAst.Drop loc
559 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
560 | IDENT "qed" -> GrafiteAst.Qed loc
561 | IDENT "variant" ; name = IDENT; SYMBOL ":";
562 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
565 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
566 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
567 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
568 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
569 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
572 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
573 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
574 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
575 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
576 defs = CicNotationParser.let_defs ->
577 (* In case of mutual definitions here we produce just
578 the syntax tree for the first one. The others will be
579 generated from the completely specified term just before
580 insertion in the environment. We use the flavour
581 `MutualDefinition to rememer this. *)
584 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
587 (fun var ty -> Ast.Binder (`Pi,var,ty)
591 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
595 let body = Ast.Ident (name,None) in
597 if List.length defs = 1 then
602 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
603 Some (Ast.LetRec (ind_kind, defs, body))))
604 | IDENT "inductive"; spec = inductive_spec ->
605 let (params, ind_types) = spec in
606 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
607 | IDENT "coinductive"; spec = inductive_spec ->
608 let (params, ind_types) = spec in
609 let ind_types = (* set inductive flags to false (coinductive) *)
610 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
613 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
614 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
615 let arity = match arity with None -> 0 | Some x -> x in
616 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
617 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
618 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
619 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
620 let uris = List.map UriManager.uri_of_string uris in
621 GrafiteAst.Default (loc,what,uris)
622 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
623 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
624 refl = tactic_term -> refl ] ;
625 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
626 sym = tactic_term -> sym ] ;
627 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
628 trans = tactic_term -> trans ] ;
630 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
633 IDENT "alias" ; spec = alias_spec ->
634 LexiconAst.Alias (loc, spec)
635 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
636 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
637 | IDENT "interpretation"; id = QSTRING;
638 (symbol, args, l3) = interpretation ->
639 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
642 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
643 | tac = tactical; punct = punctuation_tactical ->
644 GrafiteAst.Tactical (loc, tac, Some punct)
645 | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
646 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
650 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
651 GrafiteAst.Code (loc, ex)
653 GrafiteAst.Note (loc, str)
658 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
660 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
661 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
662 fun ~include_paths status ->
664 DependenciesParser.baseuri_of_script ~include_paths fname
667 LexiconEngine.eval_command status
668 (LexiconAst.Include (iloc,buri,mode,fullpath))
672 (GrafiteAst.Executable
673 (loc,GrafiteAst.Command
674 (loc,GrafiteAst.Include (iloc,buri))))
675 | scom = lexicon_command ; SYMBOL "." ->
676 fun ~include_paths status ->
677 let status = LexiconEngine.eval_command status scom in
679 | EOI -> raise End_of_file
684 let exc_located_wrapper f =
688 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
689 | Stdpp.Exc_located (floc, Stream.Error msg) ->
690 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
691 | Stdpp.Exc_located (floc, exn) ->
693 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
695 let parse_statement lexbuf =
697 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))