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 let pattern = Some what, [], Some Ast.UserInput in
169 GrafiteAst.Elim (loc, pattern, using, num, idents)
170 | IDENT "elim"; pattern = pattern_spec; using = using;
171 (num, idents) = intros_spec ->
172 GrafiteAst.Elim (loc, pattern, using, num, idents)
173 | IDENT "elimType"; what = tactic_term; using = using;
174 (num, idents) = intros_spec ->
175 GrafiteAst.ElimType (loc, what, using, num, idents)
176 | IDENT "exact"; t = tactic_term ->
177 GrafiteAst.Exact (loc, t)
179 GrafiteAst.Exists loc
180 | IDENT "fail" -> GrafiteAst.Fail loc
181 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
184 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
185 ("the pattern cannot specify the term to replace, only its"
186 ^ " paths in the hypotheses and in the conclusion")))
188 GrafiteAst.Fold (loc, kind, t, p)
190 GrafiteAst.Fourier loc
191 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
192 let idents = match idents with None -> [] | Some idents -> idents in
193 GrafiteAst.FwdSimpl (loc, hyp, idents)
194 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
195 GrafiteAst.Generalize (loc,p,id)
196 | IDENT "goal"; n = int ->
197 GrafiteAst.Goal (loc, n)
198 | IDENT "id" -> GrafiteAst.IdTac loc
199 | IDENT "intro"; ident = OPT IDENT ->
200 let idents = match ident with None -> [] | Some id -> [id] in
201 GrafiteAst.Intros (loc, Some 1, idents)
202 | IDENT "intros"; (num, idents) = intros_spec ->
203 GrafiteAst.Intros (loc, num, idents)
204 | IDENT "inversion"; t = tactic_term ->
205 GrafiteAst.Inversion (loc, t)
207 linear = OPT [ IDENT "linear" ];
208 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
210 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
211 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
212 let linear = match linear with None -> false | Some _ -> true in
213 let to_what = match to_what with None -> [] | Some to_what -> to_what in
214 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
215 | IDENT "left" -> GrafiteAst.Left loc
216 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
217 GrafiteAst.LetIn (loc, t, where)
218 | kind = reduction_kind; p = pattern_spec ->
219 GrafiteAst.Reduce (loc, kind, p)
220 | IDENT "reflexivity" ->
221 GrafiteAst.Reflexivity loc
222 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
223 GrafiteAst.Replace (loc, p, t)
224 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
225 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
229 (HExtlib.Localized (loc,
230 (CicNotationParser.Parse_error
231 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
233 let n = match xnames with None -> [] | Some names -> names in
234 GrafiteAst.Rewrite (loc, d, t, p, n)
243 | IDENT "symmetry" ->
244 GrafiteAst.Symmetry loc
245 | IDENT "transitivity"; t = tactic_term ->
246 GrafiteAst.Transitivity (loc, t)
247 (* Produzioni Aggiunte *)
248 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
249 GrafiteAst.Assume (loc, id, t)
250 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
251 GrafiteAst.Suppose (loc, t, id, t1)
252 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
253 cont=by_continuation ->
254 let t' = match t with LNone _ -> None | LSome t -> Some t in
256 BYC_done -> GrafiteAst.Bydone (loc, t')
257 | BYC_weproved (ty,id,t1) ->
258 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
259 | BYC_letsuchthat (id1,t1,id2,t2) ->
262 raise (HExtlib.Localized
263 (floc,CicNotationParser.Parse_error
264 "tactic_term expected here"))
265 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
266 | BYC_wehaveand (id1,t1,id2,t2) ->
269 raise (HExtlib.Localized
270 (floc,CicNotationParser.Parse_error
271 "tactic_term expected here"))
272 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
273 | 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']->
274 GrafiteAst.We_need_to_prove (loc, t, id, t1)
275 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
276 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
277 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
278 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
279 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
280 GrafiteAst.Byinduction(loc, t, id)
281 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
282 GrafiteAst.Thesisbecomes(loc, t)
283 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
284 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
285 GrafiteAst.Case(loc,id,params)
286 | 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 ->
287 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
288 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
289 cont=rewriting_step_continuation ->
290 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
295 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
296 string_of_int v | v = IDENT -> v ] -> i,v ] ->
301 [ LPAREN; params = auto_params; RPAREN -> params
306 [ 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)
307 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
308 IDENT "done" -> BYC_weproved (ty,None,t1)
309 | IDENT "done" -> BYC_done
310 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
311 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
312 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
313 BYC_wehaveand (id1,t1,id2,t2)
316 rewriting_step_continuation : [
317 [ IDENT "done" -> true
323 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
326 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
329 GrafiteAst.Seq (loc, ts)
332 [ tac = SELF; SYMBOL ";";
333 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
334 (GrafiteAst.Then (loc, tac, tacs))
337 [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
338 GrafiteAst.Do (loc, count, tac)
339 | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
343 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
344 GrafiteAst.First (loc, tacs)
345 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
347 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
348 GrafiteAst.Solve (loc, tacs)
349 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
350 | LPAREN; tac = SELF; RPAREN -> tac
351 | tac = tactic -> GrafiteAst.Tactic (loc, tac)
354 punctuation_tactical:
356 [ SYMBOL "[" -> GrafiteAst.Branch loc
357 | SYMBOL "|" -> GrafiteAst.Shift loc
358 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
359 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
360 | SYMBOL "]" -> GrafiteAst.Merge loc
361 | SYMBOL ";" -> GrafiteAst.Semicolon loc
362 | SYMBOL "." -> GrafiteAst.Dot loc
367 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
368 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
369 | IDENT "skip" -> GrafiteAst.Skip loc
370 | tac = atomic_tactical LEVEL "loops" -> tac
374 [ [ IDENT "definition" ] -> `Definition
375 | [ IDENT "fact" ] -> `Fact
376 | [ IDENT "lemma" ] -> `Lemma
377 | [ IDENT "remark" ] -> `Remark
378 | [ IDENT "theorem" ] -> `Theorem
382 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
383 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
384 fst_constructors = LIST0 constructor SEP SYMBOL "|";
387 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
388 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
389 (name, true, typ, constructors) ] SEP "with" -> types
393 (fun (names, typ) acc ->
394 (List.map (fun name -> (name, typ)) names) @ acc)
397 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
398 let tl_ind_types = match tl with None -> [] | Some types -> types in
399 let ind_types = fst_ind_type :: tl_ind_types in
404 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
405 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
409 SYMBOL ":" -> false,0
410 | SYMBOL ":"; SYMBOL ">" -> true,0
411 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
414 let b,n = coercion in
416 ] SEP SYMBOL ";"; SYMBOL "}" ->
419 (fun (names, typ) acc ->
420 (List.map (fun name -> (name, typ)) names) @ acc)
423 (params,name,typ,fields)
427 [ [ IDENT "check" ]; t = term ->
428 GrafiteAst.Check (loc, t)
430 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
431 suri = QSTRING; prefix = OPT QSTRING ->
432 let style = match style with
433 | None -> GrafiteAst.Declarative
434 | Some depth -> GrafiteAst.Procedural depth
436 let prefix = match prefix with None -> "" | Some prefix -> prefix in
437 GrafiteAst.Inline (loc,style,suri,prefix)
438 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
439 | [ IDENT "whelp"; "match" ] ; t = term ->
440 GrafiteAst.WMatch (loc,t)
441 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
442 GrafiteAst.WInstance (loc,t)
443 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
444 GrafiteAst.WLocate (loc,id)
445 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
446 GrafiteAst.WElim (loc, t)
447 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
448 GrafiteAst.WHint (loc,t)
452 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
453 let alpha = "[a-zA-Z]" in
454 let num = "[0-9]+" in
455 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
456 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
457 let rex = Str.regexp ("^"^ident^"$") in
458 if Str.string_match rex id 0 then
459 if (try ignore (UriManager.uri_of_string uri); true
460 with UriManager.IllFormedUri _ -> false)
462 LexiconAst.Ident_alias (id, uri)
465 (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
467 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
468 sprintf "Not a valid identifier: %s" id)))
469 | IDENT "symbol"; symbol = QSTRING;
470 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
471 SYMBOL "="; dsc = QSTRING ->
473 match instance with Some i -> i | None -> 0
475 LexiconAst.Symbol_alias (symbol, instance, dsc)
477 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
478 SYMBOL "="; dsc = QSTRING ->
480 match instance with Some i -> i | None -> 0
482 LexiconAst.Number_alias (instance, dsc)
486 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
488 Ast.IdentArg (List.length l, id)
492 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
493 | IDENT "right"; IDENT "associative" -> Gramext.RightA
494 | IDENT "non"; IDENT "associative" -> Gramext.NonA
498 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
501 [ dir = OPT direction; s = QSTRING;
502 assoc = OPT associativity; prec = OPT precedence;
505 [ blob = UNPARSED_AST ->
506 add_raw_attribute ~text:(sprintf "@{%s}" blob)
507 (CicNotationParser.parse_level2_ast
508 (Ulexing.from_utf8_string blob))
509 | blob = UNPARSED_META ->
510 add_raw_attribute ~text:(sprintf "${%s}" blob)
511 (CicNotationParser.parse_level2_meta
512 (Ulexing.from_utf8_string blob))
516 | None -> default_associativity
517 | Some assoc -> assoc
521 | None -> default_precedence
525 add_raw_attribute ~text:s
526 (CicNotationParser.parse_level1_pattern
527 (Ulexing.from_utf8_string s))
529 (dir, p1, assoc, prec, p2)
533 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
534 | id = IDENT -> Ast.VarPattern id
535 | SYMBOL "_" -> Ast.ImplicitPattern
536 | LPAREN; terms = LIST1 SELF; RPAREN ->
540 | terms -> Ast.ApplPattern terms)
544 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
550 IDENT "include" ; path = QSTRING ->
551 loc,path,LexiconAst.WithPreferences
552 | IDENT "include'" ; path = QSTRING ->
553 loc,path,LexiconAst.WithoutPreferences
557 IDENT "set"; n = QSTRING; v = QSTRING ->
558 GrafiteAst.Set (loc, n, v)
559 | IDENT "drop" -> GrafiteAst.Drop loc
560 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
561 | IDENT "qed" -> GrafiteAst.Qed loc
562 | IDENT "variant" ; name = IDENT; SYMBOL ":";
563 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
566 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
567 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
568 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
569 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
570 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
573 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
574 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
575 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
576 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
577 defs = CicNotationParser.let_defs ->
578 (* In case of mutual definitions here we produce just
579 the syntax tree for the first one. The others will be
580 generated from the completely specified term just before
581 insertion in the environment. We use the flavour
582 `MutualDefinition to rememer this. *)
585 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
588 (fun var ty -> Ast.Binder (`Pi,var,ty)
592 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
596 let body = Ast.Ident (name,None) in
598 if List.length defs = 1 then
603 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
604 Some (Ast.LetRec (ind_kind, defs, body))))
605 | IDENT "inductive"; spec = inductive_spec ->
606 let (params, ind_types) = spec in
607 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
608 | IDENT "coinductive"; spec = inductive_spec ->
609 let (params, ind_types) = spec in
610 let ind_types = (* set inductive flags to false (coinductive) *)
611 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
614 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
615 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
616 let arity = match arity with None -> 0 | Some x -> x in
617 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
618 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
619 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
620 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
621 let uris = List.map UriManager.uri_of_string uris in
622 GrafiteAst.Default (loc,what,uris)
623 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
624 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
625 refl = tactic_term -> refl ] ;
626 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
627 sym = tactic_term -> sym ] ;
628 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
629 trans = tactic_term -> trans ] ;
631 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
634 IDENT "alias" ; spec = alias_spec ->
635 LexiconAst.Alias (loc, spec)
636 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
637 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
638 | IDENT "interpretation"; id = QSTRING;
639 (symbol, args, l3) = interpretation ->
640 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
643 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
644 | tac = tactical; punct = punctuation_tactical ->
645 GrafiteAst.Tactical (loc, tac, Some punct)
646 | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
647 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
651 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
652 GrafiteAst.Code (loc, ex)
654 GrafiteAst.Note (loc, str)
659 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
661 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
662 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
663 fun ~include_paths status ->
665 DependenciesParser.baseuri_of_script ~include_paths fname
668 LexiconEngine.eval_command status
669 (LexiconAst.Include (iloc,buri,mode,fullpath))
673 (GrafiteAst.Executable
674 (loc,GrafiteAst.Command
675 (loc,GrafiteAst.Include (iloc,buri))))
676 | scom = lexicon_command ; SYMBOL "." ->
677 fun ~include_paths status ->
678 let status = LexiconEngine.eval_command status scom in
680 | EOI -> raise End_of_file
685 let exc_located_wrapper f =
689 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
690 | Stdpp.Exc_located (floc, Stream.Error msg) ->
691 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
692 | Stdpp.Exc_located (floc, exn) ->
694 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
696 let parse_statement lexbuf =
698 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))