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"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
161 let idents = match idents with None -> [] | Some idents -> idents in
162 GrafiteAst.Decompose (loc, idents)
163 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
164 | IDENT "destruct"; t = tactic_term ->
165 GrafiteAst.Destruct (loc, t)
166 | IDENT "elim"; what = tactic_term; using = using;
167 (num, idents) = intros_spec ->
168 GrafiteAst.Elim (loc, what, using, num, idents)
169 | IDENT "elimType"; what = tactic_term; using = using;
170 (num, idents) = intros_spec ->
171 GrafiteAst.ElimType (loc, what, using, num, idents)
172 | IDENT "exact"; t = tactic_term ->
173 GrafiteAst.Exact (loc, t)
175 GrafiteAst.Exists loc
176 | IDENT "fail" -> GrafiteAst.Fail loc
177 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
180 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
181 ("the pattern cannot specify the term to replace, only its"
182 ^ " paths in the hypotheses and in the conclusion")))
184 GrafiteAst.Fold (loc, kind, t, p)
186 GrafiteAst.Fourier loc
187 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
188 let idents = match idents with None -> [] | Some idents -> idents in
189 GrafiteAst.FwdSimpl (loc, hyp, idents)
190 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
191 GrafiteAst.Generalize (loc,p,id)
192 | IDENT "goal"; n = int ->
193 GrafiteAst.Goal (loc, n)
194 | IDENT "id" -> GrafiteAst.IdTac loc
195 | IDENT "intro"; ident = OPT IDENT ->
196 let idents = match ident with None -> [] | Some id -> [id] in
197 GrafiteAst.Intros (loc, Some 1, idents)
198 | IDENT "intros"; (num, idents) = intros_spec ->
199 GrafiteAst.Intros (loc, num, idents)
200 | IDENT "inversion"; t = tactic_term ->
201 GrafiteAst.Inversion (loc, t)
203 linear = OPT [ IDENT "linear" ];
204 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
206 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
207 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
208 let linear = match linear with None -> false | Some _ -> true in
209 let to_what = match to_what with None -> [] | Some to_what -> to_what in
210 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
211 | IDENT "left" -> GrafiteAst.Left loc
212 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
213 GrafiteAst.LetIn (loc, t, where)
214 | kind = reduction_kind; p = pattern_spec ->
215 GrafiteAst.Reduce (loc, kind, p)
216 | IDENT "reflexivity" ->
217 GrafiteAst.Reflexivity loc
218 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
219 GrafiteAst.Replace (loc, p, t)
220 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
221 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
225 (HExtlib.Localized (loc,
226 (CicNotationParser.Parse_error
227 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
229 let n = match xnames with None -> [] | Some names -> names in
230 GrafiteAst.Rewrite (loc, d, t, p, n)
239 | IDENT "symmetry" ->
240 GrafiteAst.Symmetry loc
241 | IDENT "transitivity"; t = tactic_term ->
242 GrafiteAst.Transitivity (loc, t)
243 (* Produzioni Aggiunte *)
244 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
245 GrafiteAst.Assume (loc, id, t)
246 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
247 GrafiteAst.Suppose (loc, t, id, t1)
248 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
249 cont=by_continuation ->
250 let t' = match t with LNone _ -> None | LSome t -> Some t in
252 BYC_done -> GrafiteAst.Bydone (loc, t')
253 | BYC_weproved (ty,id,t1) ->
254 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
255 | BYC_letsuchthat (id1,t1,id2,t2) ->
258 raise (HExtlib.Localized
259 (floc,CicNotationParser.Parse_error
260 "tactic_term expected here"))
261 | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
262 | BYC_wehaveand (id1,t1,id2,t2) ->
265 raise (HExtlib.Localized
266 (floc,CicNotationParser.Parse_error
267 "tactic_term expected here"))
268 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
269 | 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']->
270 GrafiteAst.We_need_to_prove (loc, t, id, t1)
271 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
272 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
273 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
274 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
275 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
276 GrafiteAst.Byinduction(loc, t, id)
277 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
278 GrafiteAst.Thesisbecomes(loc, t)
279 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
280 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
281 GrafiteAst.Case(loc,id,params)
282 | 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 ->
283 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
284 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
285 cont=rewriting_step_continuation ->
286 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
291 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
292 string_of_int v | v = IDENT -> v ] -> i,v ] ->
297 [ LPAREN; params = auto_params; RPAREN -> params
302 [ 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)
303 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
304 IDENT "done" -> BYC_weproved (ty,None,t1)
305 | IDENT "done" -> BYC_done
306 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
307 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
308 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
309 BYC_wehaveand (id1,t1,id2,t2)
312 rewriting_step_continuation : [
313 [ IDENT "done" -> true
319 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
322 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
325 GrafiteAst.Seq (loc, ts)
328 [ tac = SELF; SYMBOL ";";
329 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
330 (GrafiteAst.Then (loc, tac, tacs))
333 [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
334 GrafiteAst.Do (loc, count, tac)
335 | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
339 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
340 GrafiteAst.First (loc, tacs)
341 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
343 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
344 GrafiteAst.Solve (loc, tacs)
345 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
346 | LPAREN; tac = SELF; RPAREN -> tac
347 | tac = tactic -> GrafiteAst.Tactic (loc, tac)
350 punctuation_tactical:
352 [ SYMBOL "[" -> GrafiteAst.Branch loc
353 | SYMBOL "|" -> GrafiteAst.Shift loc
354 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
355 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
356 | SYMBOL "]" -> GrafiteAst.Merge loc
357 | SYMBOL ";" -> GrafiteAst.Semicolon loc
358 | SYMBOL "." -> GrafiteAst.Dot loc
363 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
364 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
365 | IDENT "skip" -> GrafiteAst.Skip loc
366 | tac = atomic_tactical LEVEL "loops" -> tac
370 [ [ IDENT "definition" ] -> `Definition
371 | [ IDENT "fact" ] -> `Fact
372 | [ IDENT "lemma" ] -> `Lemma
373 | [ IDENT "remark" ] -> `Remark
374 | [ IDENT "theorem" ] -> `Theorem
378 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
379 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
380 fst_constructors = LIST0 constructor SEP SYMBOL "|";
383 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
384 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
385 (name, true, typ, constructors) ] SEP "with" -> types
389 (fun (names, typ) acc ->
390 (List.map (fun name -> (name, typ)) names) @ acc)
393 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
394 let tl_ind_types = match tl with None -> [] | Some types -> types in
395 let ind_types = fst_ind_type :: tl_ind_types in
400 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
401 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
405 SYMBOL ":" -> false,0
406 | SYMBOL ":"; SYMBOL ">" -> true,0
407 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
410 let b,n = coercion in
412 ] SEP SYMBOL ";"; SYMBOL "}" ->
415 (fun (names, typ) acc ->
416 (List.map (fun name -> (name, typ)) names) @ acc)
419 (params,name,typ,fields)
423 [ [ IDENT "check" ]; t = term ->
424 GrafiteAst.Check (loc, t)
426 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
427 suri = QSTRING; prefix = OPT QSTRING ->
428 let style = match style with
429 | None -> GrafiteAst.Declarative
430 | Some depth -> GrafiteAst.Procedural depth
432 let prefix = match prefix with None -> "" | Some prefix -> prefix in
433 GrafiteAst.Inline (loc,style,suri,prefix)
434 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
435 | [ IDENT "whelp"; "match" ] ; t = term ->
436 GrafiteAst.WMatch (loc,t)
437 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
438 GrafiteAst.WInstance (loc,t)
439 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
440 GrafiteAst.WLocate (loc,id)
441 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
442 GrafiteAst.WElim (loc, t)
443 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
444 GrafiteAst.WHint (loc,t)
448 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
449 let alpha = "[a-zA-Z]" in
450 let num = "[0-9]+" in
451 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
452 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
453 let rex = Str.regexp ("^"^ident^"$") in
454 if Str.string_match rex id 0 then
455 if (try ignore (UriManager.uri_of_string uri); true
456 with UriManager.IllFormedUri _ -> false)
458 LexiconAst.Ident_alias (id, uri)
461 (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
463 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
464 sprintf "Not a valid identifier: %s" id)))
465 | IDENT "symbol"; symbol = QSTRING;
466 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
467 SYMBOL "="; dsc = QSTRING ->
469 match instance with Some i -> i | None -> 0
471 LexiconAst.Symbol_alias (symbol, instance, dsc)
473 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
474 SYMBOL "="; dsc = QSTRING ->
476 match instance with Some i -> i | None -> 0
478 LexiconAst.Number_alias (instance, dsc)
482 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
484 Ast.IdentArg (List.length l, id)
488 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
489 | IDENT "right"; IDENT "associative" -> Gramext.RightA
490 | IDENT "non"; IDENT "associative" -> Gramext.NonA
494 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
497 [ dir = OPT direction; s = QSTRING;
498 assoc = OPT associativity; prec = OPT precedence;
501 [ blob = UNPARSED_AST ->
502 add_raw_attribute ~text:(sprintf "@{%s}" blob)
503 (CicNotationParser.parse_level2_ast
504 (Ulexing.from_utf8_string blob))
505 | blob = UNPARSED_META ->
506 add_raw_attribute ~text:(sprintf "${%s}" blob)
507 (CicNotationParser.parse_level2_meta
508 (Ulexing.from_utf8_string blob))
512 | None -> default_associativity
513 | Some assoc -> assoc
517 | None -> default_precedence
521 add_raw_attribute ~text:s
522 (CicNotationParser.parse_level1_pattern
523 (Ulexing.from_utf8_string s))
525 (dir, p1, assoc, prec, p2)
529 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
530 | id = IDENT -> Ast.VarPattern id
531 | SYMBOL "_" -> Ast.ImplicitPattern
532 | LPAREN; terms = LIST1 SELF; RPAREN ->
536 | terms -> Ast.ApplPattern terms)
540 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
546 IDENT "include" ; path = QSTRING ->
547 loc,path,LexiconAst.WithPreferences
548 | IDENT "include'" ; path = QSTRING ->
549 loc,path,LexiconAst.WithoutPreferences
553 IDENT "set"; n = QSTRING; v = QSTRING ->
554 GrafiteAst.Set (loc, n, v)
555 | IDENT "drop" -> GrafiteAst.Drop loc
556 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
557 | IDENT "qed" -> GrafiteAst.Qed loc
558 | IDENT "variant" ; name = IDENT; SYMBOL ":";
559 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
562 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
563 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
564 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
565 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
566 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
569 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
570 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
571 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
572 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
573 defs = CicNotationParser.let_defs ->
574 (* In case of mutual definitions here we produce just
575 the syntax tree for the first one. The others will be
576 generated from the completely specified term just before
577 insertion in the environment. We use the flavour
578 `MutualDefinition to rememer this. *)
581 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
584 (fun var ty -> Ast.Binder (`Pi,var,ty)
588 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
592 let body = Ast.Ident (name,None) in
594 if List.length defs = 1 then
599 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
600 Some (Ast.LetRec (ind_kind, defs, body))))
601 | IDENT "inductive"; spec = inductive_spec ->
602 let (params, ind_types) = spec in
603 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
604 | IDENT "coinductive"; spec = inductive_spec ->
605 let (params, ind_types) = spec in
606 let ind_types = (* set inductive flags to false (coinductive) *)
607 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
610 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
611 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
612 let arity = match arity with None -> 0 | Some x -> x in
613 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
614 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
615 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
616 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
617 let uris = List.map UriManager.uri_of_string uris in
618 GrafiteAst.Default (loc,what,uris)
619 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
620 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
621 refl = tactic_term -> refl ] ;
622 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
623 sym = tactic_term -> sym ] ;
624 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
625 trans = tactic_term -> trans ] ;
627 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
630 IDENT "alias" ; spec = alias_spec ->
631 LexiconAst.Alias (loc, spec)
632 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
633 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
634 | IDENT "interpretation"; id = QSTRING;
635 (symbol, args, l3) = interpretation ->
636 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
639 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
640 | tac = tactical; punct = punctuation_tactical ->
641 GrafiteAst.Tactical (loc, tac, Some punct)
642 | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
643 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
647 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
648 GrafiteAst.Code (loc, ex)
650 GrafiteAst.Note (loc, str)
655 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
657 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
658 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
659 fun ~include_paths status ->
661 DependenciesParser.baseuri_of_script ~include_paths fname
664 LexiconEngine.eval_command status
665 (LexiconAst.Include (iloc,buri,mode,fullpath))
669 (GrafiteAst.Executable
670 (loc,GrafiteAst.Command
671 (loc,GrafiteAst.Include (iloc,buri))))
672 | scom = lexicon_command ; SYMBOL "." ->
673 fun ~include_paths status ->
674 let status = LexiconEngine.eval_command status scom in
676 | EOI -> raise End_of_file
681 let exc_located_wrapper f =
685 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
686 | Stdpp.Exc_located (floc, Stream.Error msg) ->
687 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
688 | Stdpp.Exc_located (floc, exn) ->
690 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
692 let parse_statement lexbuf =
694 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))