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 exception NoInclusionPerformed of string (* full path *)
35 type 'a localized_option =
37 | LNone of GrafiteAst.loc
40 (CicNotationPt.term, CicNotationPt.term,
41 CicNotationPt.term GrafiteAst.reduction,
42 CicNotationPt.term CicNotationPt.obj, string)
46 ?never_include:bool ->
47 include_paths:string list ->
48 LexiconEngine.status ->
49 LexiconEngine.status * ast_statement localized_option
51 let grammar = CicNotationParser.level2_ast_grammar
53 let term = CicNotationParser.term
54 let statement = Grammar.Entry.create grammar "statement"
56 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
58 let default_precedence = 50
59 let default_associativity = Gramext.NonA
61 type by_continuation =
63 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
64 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
65 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
68 GLOBAL: term statement;
69 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
70 tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
72 [ id = IDENT -> Some id
73 | SYMBOL "_" -> None ]
75 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
77 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
80 [ IDENT "normalize" -> `Normalize
81 | IDENT "simplify" -> `Simpl
82 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
83 | IDENT "whd" -> `Whd ]
85 sequent_pattern_spec: [
89 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
90 (id,match path with Some p -> p | None -> Ast.UserInput) ];
91 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
93 match goal_path, hyp_paths with
94 None, [] -> Some Ast.UserInput
96 | Some goal_path, _ -> Some goal_path
105 [ "match" ; wanted = tactic_term ;
106 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
108 | sps = sequent_pattern_spec ->
111 let wanted,hyp_paths,goal_path =
112 match wanted_and_sps with
113 wanted,None -> wanted, [], Some Ast.UserInput
114 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
116 wanted, hyp_paths, goal_path ] ->
118 None -> None,[],Some Ast.UserInput
122 [ SYMBOL ">" -> `LeftToRight
123 | SYMBOL "<" -> `RightToLeft ]
125 int: [ [ num = NUMBER -> int_of_string num ] ];
127 [ idents = OPT ident_list0 ->
128 match idents with None -> [] | Some idents -> idents
132 [ OPT [ IDENT "names" ];
133 num = OPT [ num = int -> num ];
134 idents = intros_names ->
138 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
140 [ IDENT "absurd"; t = tactic_term ->
141 GrafiteAst.Absurd (loc, t)
142 | IDENT "apply"; t = tactic_term ->
143 GrafiteAst.Apply (loc, t)
144 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
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"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
173 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
174 GrafiteAst.Destruct (loc, xts)
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)
249 | IDENT "symmetry" ->
250 GrafiteAst.Symmetry loc
251 | IDENT "transitivity"; t = tactic_term ->
252 GrafiteAst.Transitivity (loc, t)
253 (* Produzioni Aggiunte *)
254 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
255 GrafiteAst.Assume (loc, id, t)
256 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
257 GrafiteAst.Suppose (loc, t, id, t1)
258 | "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
259 cont=by_continuation ->
260 let t' = match t with LNone _ -> None | LSome t -> Some t in
262 BYC_done -> GrafiteAst.Bydone (loc, t')
263 | BYC_weproved (ty,id,t1) ->
264 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
265 | BYC_letsuchthat (id1,t1,id2,t2) ->
268 raise (HExtlib.Localized
269 (floc,CicNotationParser.Parse_error
270 "tactic_term expected here"))
271 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
272 | BYC_wehaveand (id1,t1,id2,t2) ->
275 raise (HExtlib.Localized
276 (floc,CicNotationParser.Parse_error
277 "tactic_term expected here"))
278 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
279 | 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']->
280 GrafiteAst.We_need_to_prove (loc, t, id, t1)
281 | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
282 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
283 | IDENT "we" ; IDENT "proceed" ; "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
284 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
285 | "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
286 GrafiteAst.Byinduction(loc, t, id)
287 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
288 GrafiteAst.Thesisbecomes(loc, t)
289 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
290 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
291 GrafiteAst.Case(loc,id,params)
294 [ IDENT "conclude" -> None
295 | IDENT "obtain" ; name = IDENT -> Some name ] ;
296 termine = tactic_term -> start, termine];
300 [ IDENT "exact"; t=tactic_term -> `Term t
301 | IDENT "using"; term=tactic_term -> `SolveWith term
302 | IDENT "proof" -> `Proof
303 | params = auto_params -> `Auto params];
304 cont = rewriting_step_continuation ->
305 GrafiteAst.RewritingStep(loc, start, t1, t2, cont)
310 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
311 string_of_int v | v = IDENT -> v ] -> i,v ];
312 tl = OPT [ "by"; tl = LIST1 tactic_term -> tl] ->
313 (match tl with Some l -> l | None -> []),
318 [ 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)
319 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
320 "done" -> BYC_weproved (ty,None,t1)
322 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
323 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
324 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
325 BYC_wehaveand (id1,t1,id2,t2)
328 rewriting_step_continuation : [
335 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
338 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
341 GrafiteAst.Seq (loc, ts)
344 [ tac = SELF; SYMBOL ";";
345 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
346 (GrafiteAst.Then (loc, tac, tacs))
349 [ IDENT "do"; count = int; tac = SELF ->
350 GrafiteAst.Do (loc, count, tac)
351 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
355 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
356 GrafiteAst.First (loc, tacs)
357 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
359 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
360 GrafiteAst.Solve (loc, tacs)
361 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
362 | LPAREN; tac = SELF; RPAREN -> tac
363 | tac = tactic -> tac
366 punctuation_tactical:
368 [ SYMBOL "[" -> GrafiteAst.Branch loc
369 | SYMBOL "|" -> GrafiteAst.Shift loc
370 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
371 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
372 | SYMBOL "]" -> GrafiteAst.Merge loc
373 | SYMBOL ";" -> GrafiteAst.Semicolon loc
374 | SYMBOL "." -> GrafiteAst.Dot loc
377 non_punctuation_tactical:
379 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
380 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
381 | IDENT "skip" -> GrafiteAst.Skip loc
385 [ [ IDENT "definition" ] -> `Definition
386 | [ IDENT "fact" ] -> `Fact
387 | [ IDENT "lemma" ] -> `Lemma
388 | [ IDENT "remark" ] -> `Remark
389 | [ IDENT "theorem" ] -> `Theorem
393 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
394 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
395 fst_constructors = LIST0 constructor SEP SYMBOL "|";
398 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
399 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
400 (name, true, typ, constructors) ] SEP "with" -> types
404 (fun (names, typ) acc ->
405 (List.map (fun name -> (name, typ)) names) @ acc)
408 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
409 let tl_ind_types = match tl with None -> [] | Some types -> types in
410 let ind_types = fst_ind_type :: tl_ind_types in
415 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
416 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
420 SYMBOL ":" -> false,0
421 | SYMBOL ":"; SYMBOL ">" -> true,0
422 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
425 let b,n = coercion in
427 ] SEP SYMBOL ";"; SYMBOL "}" ->
430 (fun (names, typ) acc ->
431 (List.map (fun name -> (name, typ)) names) @ acc)
434 (params,name,typ,fields)
438 [ [ IDENT "check" ]; t = term ->
439 GrafiteAst.Check (loc, t)
441 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
442 suri = QSTRING; prefix = OPT QSTRING ->
443 let style = match style with
444 | None -> GrafiteAst.Declarative
445 | Some depth -> GrafiteAst.Procedural depth
447 let prefix = match prefix with None -> "" | Some prefix -> prefix in
448 GrafiteAst.Inline (loc,style,suri,prefix)
449 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
450 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
451 | IDENT "auto"; params = auto_params ->
452 GrafiteAst.AutoInteractive (loc,params)
453 | [ IDENT "whelp"; "match" ] ; t = term ->
454 GrafiteAst.WMatch (loc,t)
455 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
456 GrafiteAst.WInstance (loc,t)
457 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
458 GrafiteAst.WLocate (loc,id)
459 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
460 GrafiteAst.WElim (loc, t)
461 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
462 GrafiteAst.WHint (loc,t)
466 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
467 let alpha = "[a-zA-Z]" in
468 let num = "[0-9]+" in
469 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
470 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
471 let rex = Str.regexp ("^"^ident^"$") in
472 if Str.string_match rex id 0 then
473 if (try ignore (UriManager.uri_of_string uri); true
474 with UriManager.IllFormedUri _ -> false)
476 LexiconAst.Ident_alias (id, uri)
479 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
481 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
482 Printf.sprintf "Not a valid identifier: %s" id)))
483 | IDENT "symbol"; symbol = QSTRING;
484 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
485 SYMBOL "="; dsc = QSTRING ->
487 match instance with Some i -> i | None -> 0
489 LexiconAst.Symbol_alias (symbol, instance, dsc)
491 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
492 SYMBOL "="; dsc = QSTRING ->
494 match instance with Some i -> i | None -> 0
496 LexiconAst.Number_alias (instance, dsc)
500 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
502 Ast.IdentArg (List.length l, id)
506 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
507 | IDENT "right"; IDENT "associative" -> Gramext.RightA
508 | IDENT "non"; IDENT "associative" -> Gramext.NonA
512 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
515 [ dir = OPT direction; s = QSTRING;
516 assoc = OPT associativity; prec = OPT precedence;
519 [ blob = UNPARSED_AST ->
520 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
521 (CicNotationParser.parse_level2_ast
522 (Ulexing.from_utf8_string blob))
523 | blob = UNPARSED_META ->
524 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
525 (CicNotationParser.parse_level2_meta
526 (Ulexing.from_utf8_string blob))
530 | None -> default_associativity
531 | Some assoc -> assoc
535 | None -> default_precedence
539 add_raw_attribute ~text:s
540 (CicNotationParser.parse_level1_pattern
541 (Ulexing.from_utf8_string s))
543 (dir, p1, assoc, prec, p2)
547 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
548 | id = IDENT -> Ast.VarPattern id
549 | SYMBOL "_" -> Ast.ImplicitPattern
550 | LPAREN; terms = LIST1 SELF; RPAREN ->
554 | terms -> Ast.ApplPattern terms)
558 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
564 IDENT "include" ; path = QSTRING ->
565 loc,path,LexiconAst.WithPreferences
566 | IDENT "include'" ; path = QSTRING ->
567 loc,path,LexiconAst.WithoutPreferences
571 IDENT "set"; n = QSTRING; v = QSTRING ->
572 GrafiteAst.Set (loc, n, v)
573 | IDENT "drop" -> GrafiteAst.Drop loc
574 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
575 | IDENT "qed" -> GrafiteAst.Qed loc
576 | IDENT "variant" ; name = IDENT; SYMBOL ":";
577 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
580 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
581 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
582 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
583 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
584 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
587 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
588 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
589 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
590 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
591 defs = CicNotationParser.let_defs ->
592 (* In case of mutual definitions here we produce just
593 the syntax tree for the first one. The others will be
594 generated from the completely specified term just before
595 insertion in the environment. We use the flavour
596 `MutualDefinition to rememer this. *)
599 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
602 (fun var ty -> Ast.Binder (`Pi,var,ty)
606 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
610 let body = Ast.Ident (name,None) in
612 if List.length defs = 1 then
617 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
618 Some (Ast.LetRec (ind_kind, defs, body))))
619 | IDENT "inductive"; spec = inductive_spec ->
620 let (params, ind_types) = spec in
621 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
622 | IDENT "coinductive"; spec = inductive_spec ->
623 let (params, ind_types) = spec in
624 let ind_types = (* set inductive flags to false (coinductive) *)
625 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
628 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
629 | IDENT "coercion" ; suri = URI ; arity = OPT int ;
630 saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
631 let arity = match arity with None -> 0 | Some x -> x in
632 let saturations = match saturations with None -> 0 | Some x -> x in
633 let composites = match composites with None -> true | Some _ -> false in
635 (loc, UriManager.uri_of_string suri, composites, arity, saturations)
636 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
637 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
638 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
639 let uris = List.map UriManager.uri_of_string uris in
640 GrafiteAst.Default (loc,what,uris)
641 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
642 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; "by" ;
643 refl = tactic_term -> refl ] ;
644 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; "by" ;
645 sym = tactic_term -> sym ] ;
646 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; "by" ;
647 trans = tactic_term -> trans ] ;
649 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
652 IDENT "alias" ; spec = alias_spec ->
653 LexiconAst.Alias (loc, spec)
654 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
655 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
656 | IDENT "interpretation"; id = QSTRING;
657 (symbol, args, l3) = interpretation ->
658 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
661 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
662 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
663 GrafiteAst.Tactic (loc, Some tac, punct)
664 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
665 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
666 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
667 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
671 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
672 GrafiteAst.Code (loc, ex)
674 GrafiteAst.Note (loc, str)
679 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
681 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
682 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
683 fun ?(never_include=false) ~include_paths status ->
684 let _root, buri, fullpath, _rrelpath =
685 Librarian.baseuri_of_script ~include_paths fname
688 if never_include then raise (NoInclusionPerformed fullpath)
689 else LexiconEngine.eval_command status
690 (LexiconAst.Include (iloc,buri,mode,fullpath))
695 (GrafiteAst.Executable
696 (loc,GrafiteAst.Command
697 (loc,GrafiteAst.Include (iloc,buri))))
698 | scom = lexicon_command ; SYMBOL "." ->
699 fun ?(never_include=false) ~include_paths status ->
700 let status = LexiconEngine.eval_command status scom in
702 | EOI -> raise End_of_file
707 let exc_located_wrapper f =
711 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
712 | Stdpp.Exc_located (floc, Stream.Error msg) ->
713 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
714 | Stdpp.Exc_located (floc, exn) ->
716 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
718 let parse_statement lexbuf =
720 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))