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 "constructor"; n = int ->
160 GrafiteAst.Constructor (loc, n)
161 | IDENT "contradiction" ->
162 GrafiteAst.Contradiction loc
163 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
164 GrafiteAst.Cut (loc, ident, t)
165 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
166 let idents = match idents with None -> [] | Some idents -> idents in
167 GrafiteAst.Decompose (loc, idents)
168 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
169 | IDENT "destruct"; t = tactic_term ->
170 GrafiteAst.Destruct (loc, t)
171 | IDENT "elim"; what = tactic_term; using = using;
172 pattern = OPT pattern_spec;
173 (num, idents) = intros_spec ->
174 let pattern = match pattern with
175 | None -> None, [], Some Ast.UserInput
176 | Some pattern -> pattern
178 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
179 | IDENT "elimType"; what = tactic_term; using = using;
180 (num, idents) = intros_spec ->
181 GrafiteAst.ElimType (loc, what, using, (num, idents))
182 | IDENT "exact"; t = tactic_term ->
183 GrafiteAst.Exact (loc, t)
185 GrafiteAst.Exists loc
186 | IDENT "fail" -> GrafiteAst.Fail loc
187 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
190 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
191 ("the pattern cannot specify the term to replace, only its"
192 ^ " paths in the hypotheses and in the conclusion")))
194 GrafiteAst.Fold (loc, kind, t, p)
196 GrafiteAst.Fourier loc
197 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
198 let idents = match idents with None -> [] | Some idents -> idents in
199 GrafiteAst.FwdSimpl (loc, hyp, idents)
200 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
201 GrafiteAst.Generalize (loc,p,id)
202 | IDENT "id" -> GrafiteAst.IdTac loc
203 | IDENT "intro"; ident = OPT IDENT ->
204 let idents = match ident with None -> [] | Some id -> [Some id] in
205 GrafiteAst.Intros (loc, (Some 1, idents))
206 | IDENT "intros"; specs = intros_spec ->
207 GrafiteAst.Intros (loc, specs)
208 | IDENT "inversion"; t = tactic_term ->
209 GrafiteAst.Inversion (loc, t)
211 linear = OPT [ IDENT "linear" ];
212 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
214 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
215 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
216 let linear = match linear with None -> false | Some _ -> true in
217 let to_what = match to_what with None -> [] | Some to_what -> to_what in
218 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
219 | IDENT "left" -> GrafiteAst.Left loc
220 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
221 GrafiteAst.LetIn (loc, t, where)
222 | kind = reduction_kind; p = pattern_spec ->
223 GrafiteAst.Reduce (loc, kind, p)
224 | IDENT "reflexivity" ->
225 GrafiteAst.Reflexivity loc
226 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
227 GrafiteAst.Replace (loc, p, t)
228 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
229 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
233 (HExtlib.Localized (loc,
234 (CicNotationParser.Parse_error
235 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
237 let n = match xnames with None -> [] | Some names -> names in
238 GrafiteAst.Rewrite (loc, d, t, p, n)
247 | IDENT "symmetry" ->
248 GrafiteAst.Symmetry loc
249 | IDENT "transitivity"; t = tactic_term ->
250 GrafiteAst.Transitivity (loc, t)
251 (* Produzioni Aggiunte *)
252 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
253 GrafiteAst.Assume (loc, id, t)
254 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
255 GrafiteAst.Suppose (loc, t, id, t1)
256 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
257 cont=by_continuation ->
258 let t' = match t with LNone _ -> None | LSome t -> Some t in
260 BYC_done -> GrafiteAst.Bydone (loc, t')
261 | BYC_weproved (ty,id,t1) ->
262 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
263 | BYC_letsuchthat (id1,t1,id2,t2) ->
266 raise (HExtlib.Localized
267 (floc,CicNotationParser.Parse_error
268 "tactic_term expected here"))
269 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
270 | BYC_wehaveand (id1,t1,id2,t2) ->
273 raise (HExtlib.Localized
274 (floc,CicNotationParser.Parse_error
275 "tactic_term expected here"))
276 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
277 | 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']->
278 GrafiteAst.We_need_to_prove (loc, t, id, t1)
279 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
280 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
281 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
282 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
283 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
284 GrafiteAst.Byinduction(loc, t, id)
285 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
286 GrafiteAst.Thesisbecomes(loc, t)
287 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
288 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
289 GrafiteAst.Case(loc,id,params)
290 | 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 ->
291 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
292 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
293 cont=rewriting_step_continuation ->
294 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
299 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
300 string_of_int v | v = IDENT -> v ] -> i,v ] ->
305 [ LPAREN; params = auto_params; RPAREN -> params
310 [ 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)
311 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
312 IDENT "done" -> BYC_weproved (ty,None,t1)
313 | IDENT "done" -> BYC_done
314 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
315 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
316 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
317 BYC_wehaveand (id1,t1,id2,t2)
320 rewriting_step_continuation : [
321 [ IDENT "done" -> true
327 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
330 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
333 GrafiteAst.Seq (loc, ts)
336 [ tac = SELF; SYMBOL ";";
337 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
338 (GrafiteAst.Then (loc, tac, tacs))
341 [ IDENT "do"; count = int; tac = SELF ->
342 GrafiteAst.Do (loc, count, tac)
343 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
347 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
348 GrafiteAst.First (loc, tacs)
349 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
351 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
352 GrafiteAst.Solve (loc, tacs)
353 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
354 | LPAREN; tac = SELF; RPAREN -> tac
355 | tac = tactic -> tac
358 punctuation_tactical:
360 [ SYMBOL "[" -> GrafiteAst.Branch loc
361 | SYMBOL "|" -> GrafiteAst.Shift loc
362 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
363 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
364 | SYMBOL "]" -> GrafiteAst.Merge loc
365 | SYMBOL ";" -> GrafiteAst.Semicolon loc
366 | SYMBOL "." -> GrafiteAst.Dot loc
369 non_punctuation_tactical:
371 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
372 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
373 | IDENT "skip" -> GrafiteAst.Skip loc
377 [ [ IDENT "definition" ] -> `Definition
378 | [ IDENT "fact" ] -> `Fact
379 | [ IDENT "lemma" ] -> `Lemma
380 | [ IDENT "remark" ] -> `Remark
381 | [ IDENT "theorem" ] -> `Theorem
385 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
386 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
387 fst_constructors = LIST0 constructor SEP SYMBOL "|";
390 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
391 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
392 (name, true, typ, constructors) ] SEP "with" -> types
396 (fun (names, typ) acc ->
397 (List.map (fun name -> (name, typ)) names) @ acc)
400 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
401 let tl_ind_types = match tl with None -> [] | Some types -> types in
402 let ind_types = fst_ind_type :: tl_ind_types in
407 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
408 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
412 SYMBOL ":" -> false,0
413 | SYMBOL ":"; SYMBOL ">" -> true,0
414 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
417 let b,n = coercion in
419 ] SEP SYMBOL ";"; SYMBOL "}" ->
422 (fun (names, typ) acc ->
423 (List.map (fun name -> (name, typ)) names) @ acc)
426 (params,name,typ,fields)
430 [ [ IDENT "check" ]; t = term ->
431 GrafiteAst.Check (loc, t)
433 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
434 suri = QSTRING; prefix = OPT QSTRING ->
435 let style = match style with
436 | None -> GrafiteAst.Declarative
437 | Some depth -> GrafiteAst.Procedural depth
439 let prefix = match prefix with None -> "" | Some prefix -> prefix in
440 GrafiteAst.Inline (loc,style,suri,prefix)
441 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
442 | IDENT "auto"; params = auto_params ->
443 GrafiteAst.AutoInteractive (loc,params)
444 | [ IDENT "whelp"; "match" ] ; t = term ->
445 GrafiteAst.WMatch (loc,t)
446 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
447 GrafiteAst.WInstance (loc,t)
448 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
449 GrafiteAst.WLocate (loc,id)
450 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
451 GrafiteAst.WElim (loc, t)
452 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
453 GrafiteAst.WHint (loc,t)
457 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
458 let alpha = "[a-zA-Z]" in
459 let num = "[0-9]+" in
460 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
461 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
462 let rex = Str.regexp ("^"^ident^"$") in
463 if Str.string_match rex id 0 then
464 if (try ignore (UriManager.uri_of_string uri); true
465 with UriManager.IllFormedUri _ -> false)
467 LexiconAst.Ident_alias (id, uri)
470 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
472 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
473 Printf.sprintf "Not a valid identifier: %s" id)))
474 | IDENT "symbol"; symbol = QSTRING;
475 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
476 SYMBOL "="; dsc = QSTRING ->
478 match instance with Some i -> i | None -> 0
480 LexiconAst.Symbol_alias (symbol, instance, dsc)
482 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
483 SYMBOL "="; dsc = QSTRING ->
485 match instance with Some i -> i | None -> 0
487 LexiconAst.Number_alias (instance, dsc)
491 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
493 Ast.IdentArg (List.length l, id)
497 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
498 | IDENT "right"; IDENT "associative" -> Gramext.RightA
499 | IDENT "non"; IDENT "associative" -> Gramext.NonA
503 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
506 [ dir = OPT direction; s = QSTRING;
507 assoc = OPT associativity; prec = OPT precedence;
510 [ blob = UNPARSED_AST ->
511 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
512 (CicNotationParser.parse_level2_ast
513 (Ulexing.from_utf8_string blob))
514 | blob = UNPARSED_META ->
515 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
516 (CicNotationParser.parse_level2_meta
517 (Ulexing.from_utf8_string blob))
521 | None -> default_associativity
522 | Some assoc -> assoc
526 | None -> default_precedence
530 add_raw_attribute ~text:s
531 (CicNotationParser.parse_level1_pattern
532 (Ulexing.from_utf8_string s))
534 (dir, p1, assoc, prec, p2)
538 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
539 | id = IDENT -> Ast.VarPattern id
540 | SYMBOL "_" -> Ast.ImplicitPattern
541 | LPAREN; terms = LIST1 SELF; RPAREN ->
545 | terms -> Ast.ApplPattern terms)
549 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
555 IDENT "include" ; path = QSTRING ->
556 loc,path,LexiconAst.WithPreferences
557 | IDENT "include'" ; path = QSTRING ->
558 loc,path,LexiconAst.WithoutPreferences
562 IDENT "set"; n = QSTRING; v = QSTRING ->
563 GrafiteAst.Set (loc, n, v)
564 | IDENT "drop" -> GrafiteAst.Drop loc
565 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
566 | IDENT "qed" -> GrafiteAst.Qed loc
567 | IDENT "variant" ; name = IDENT; SYMBOL ":";
568 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
571 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
572 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
573 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
574 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
575 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
578 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
579 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
580 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
581 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
582 defs = CicNotationParser.let_defs ->
583 (* In case of mutual definitions here we produce just
584 the syntax tree for the first one. The others will be
585 generated from the completely specified term just before
586 insertion in the environment. We use the flavour
587 `MutualDefinition to rememer this. *)
590 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
593 (fun var ty -> Ast.Binder (`Pi,var,ty)
597 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
601 let body = Ast.Ident (name,None) in
603 if List.length defs = 1 then
608 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
609 Some (Ast.LetRec (ind_kind, defs, body))))
610 | IDENT "inductive"; spec = inductive_spec ->
611 let (params, ind_types) = spec in
612 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
613 | IDENT "coinductive"; spec = inductive_spec ->
614 let (params, ind_types) = spec in
615 let ind_types = (* set inductive flags to false (coinductive) *)
616 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
619 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
620 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
621 let arity = match arity with None -> 0 | Some x -> x in
622 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
623 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
624 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
625 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
626 let uris = List.map UriManager.uri_of_string uris in
627 GrafiteAst.Default (loc,what,uris)
628 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
629 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
630 refl = tactic_term -> refl ] ;
631 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
632 sym = tactic_term -> sym ] ;
633 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
634 trans = tactic_term -> trans ] ;
636 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
639 IDENT "alias" ; spec = alias_spec ->
640 LexiconAst.Alias (loc, spec)
641 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
642 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
643 | IDENT "interpretation"; id = QSTRING;
644 (symbol, args, l3) = interpretation ->
645 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
648 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
649 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
650 GrafiteAst.Tactic (loc, Some tac, punct)
651 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
652 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
653 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
654 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
658 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
659 GrafiteAst.Code (loc, ex)
661 GrafiteAst.Note (loc, str)
666 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
668 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
669 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
670 fun ~include_paths status ->
672 DependenciesParser.baseuri_of_script ~include_paths fname
675 LexiconEngine.eval_command status
676 (LexiconAst.Include (iloc,buri,mode,fullpath))
681 (GrafiteAst.Executable
682 (loc,GrafiteAst.Command
683 (loc,GrafiteAst.Include (iloc,buri))))
684 | scom = lexicon_command ; SYMBOL "." ->
685 fun ~include_paths status ->
686 let status = LexiconEngine.eval_command status scom in
688 | EOI -> raise End_of_file
693 let exc_located_wrapper f =
697 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
698 | Stdpp.Exc_located (floc, Stream.Error msg) ->
699 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
700 | Stdpp.Exc_located (floc, exn) ->
702 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
704 let parse_statement lexbuf =
706 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))