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 "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" -> GrafiteAst.Demodulate loc
173 | IDENT "destruct"; t = tactic_term ->
174 GrafiteAst.Destruct (loc, t)
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)
251 | IDENT "symmetry" ->
252 GrafiteAst.Symmetry loc
253 | IDENT "transitivity"; t = tactic_term ->
254 GrafiteAst.Transitivity (loc, t)
255 (* Produzioni Aggiunte *)
256 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
257 GrafiteAst.Assume (loc, id, t)
258 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
259 GrafiteAst.Suppose (loc, t, id, t1)
260 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
261 cont=by_continuation ->
262 let t' = match t with LNone _ -> None | LSome t -> Some t in
264 BYC_done -> GrafiteAst.Bydone (loc, t')
265 | BYC_weproved (ty,id,t1) ->
266 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
267 | BYC_letsuchthat (id1,t1,id2,t2) ->
270 raise (HExtlib.Localized
271 (floc,CicNotationParser.Parse_error
272 "tactic_term expected here"))
273 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
274 | BYC_wehaveand (id1,t1,id2,t2) ->
277 raise (HExtlib.Localized
278 (floc,CicNotationParser.Parse_error
279 "tactic_term expected here"))
280 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
281 | 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']->
282 GrafiteAst.We_need_to_prove (loc, t, id, t1)
283 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
284 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
285 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
286 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
287 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
288 GrafiteAst.Byinduction(loc, t, id)
289 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
290 GrafiteAst.Thesisbecomes(loc, t)
291 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
292 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
293 GrafiteAst.Case(loc,id,params)
294 | 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 ->
295 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
296 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
297 cont=rewriting_step_continuation ->
298 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
303 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
304 string_of_int v | v = IDENT -> v ] -> i,v ] ->
309 [ LPAREN; params = auto_params; RPAREN -> params
314 [ 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)
315 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
316 IDENT "done" -> BYC_weproved (ty,None,t1)
317 | IDENT "done" -> BYC_done
318 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
319 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
320 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
321 BYC_wehaveand (id1,t1,id2,t2)
324 rewriting_step_continuation : [
325 [ IDENT "done" -> true
331 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
334 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
337 GrafiteAst.Seq (loc, ts)
340 [ tac = SELF; SYMBOL ";";
341 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
342 (GrafiteAst.Then (loc, tac, tacs))
345 [ IDENT "do"; count = int; tac = SELF ->
346 GrafiteAst.Do (loc, count, tac)
347 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
351 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
352 GrafiteAst.First (loc, tacs)
353 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
355 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
356 GrafiteAst.Solve (loc, tacs)
357 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
358 | LPAREN; tac = SELF; RPAREN -> tac
359 | tac = tactic -> tac
362 punctuation_tactical:
364 [ SYMBOL "[" -> GrafiteAst.Branch loc
365 | SYMBOL "|" -> GrafiteAst.Shift loc
366 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
367 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
368 | SYMBOL "]" -> GrafiteAst.Merge loc
369 | SYMBOL ";" -> GrafiteAst.Semicolon loc
370 | SYMBOL "." -> GrafiteAst.Dot loc
373 non_punctuation_tactical:
375 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
376 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
377 | IDENT "skip" -> GrafiteAst.Skip loc
381 [ [ IDENT "definition" ] -> `Definition
382 | [ IDENT "fact" ] -> `Fact
383 | [ IDENT "lemma" ] -> `Lemma
384 | [ IDENT "remark" ] -> `Remark
385 | [ IDENT "theorem" ] -> `Theorem
389 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
390 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
391 fst_constructors = LIST0 constructor SEP SYMBOL "|";
394 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
395 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
396 (name, true, typ, constructors) ] SEP "with" -> types
400 (fun (names, typ) acc ->
401 (List.map (fun name -> (name, typ)) names) @ acc)
404 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
405 let tl_ind_types = match tl with None -> [] | Some types -> types in
406 let ind_types = fst_ind_type :: tl_ind_types in
411 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
412 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
416 SYMBOL ":" -> false,0
417 | SYMBOL ":"; SYMBOL ">" -> true,0
418 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
421 let b,n = coercion in
423 ] SEP SYMBOL ";"; SYMBOL "}" ->
426 (fun (names, typ) acc ->
427 (List.map (fun name -> (name, typ)) names) @ acc)
430 (params,name,typ,fields)
434 [ [ IDENT "check" ]; t = term ->
435 GrafiteAst.Check (loc, t)
437 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
438 suri = QSTRING; prefix = OPT QSTRING ->
439 let style = match style with
440 | None -> GrafiteAst.Declarative
441 | Some depth -> GrafiteAst.Procedural depth
443 let prefix = match prefix with None -> "" | Some prefix -> prefix in
444 GrafiteAst.Inline (loc,style,suri,prefix)
445 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
446 | IDENT "auto"; params = auto_params ->
447 GrafiteAst.AutoInteractive (loc,params)
448 | [ IDENT "whelp"; "match" ] ; t = term ->
449 GrafiteAst.WMatch (loc,t)
450 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
451 GrafiteAst.WInstance (loc,t)
452 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
453 GrafiteAst.WLocate (loc,id)
454 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
455 GrafiteAst.WElim (loc, t)
456 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
457 GrafiteAst.WHint (loc,t)
461 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
462 let alpha = "[a-zA-Z]" in
463 let num = "[0-9]+" in
464 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
465 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
466 let rex = Str.regexp ("^"^ident^"$") in
467 if Str.string_match rex id 0 then
468 if (try ignore (UriManager.uri_of_string uri); true
469 with UriManager.IllFormedUri _ -> false)
471 LexiconAst.Ident_alias (id, uri)
474 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
476 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
477 Printf.sprintf "Not a valid identifier: %s" id)))
478 | IDENT "symbol"; symbol = QSTRING;
479 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
480 SYMBOL "="; dsc = QSTRING ->
482 match instance with Some i -> i | None -> 0
484 LexiconAst.Symbol_alias (symbol, instance, dsc)
486 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
487 SYMBOL "="; dsc = QSTRING ->
489 match instance with Some i -> i | None -> 0
491 LexiconAst.Number_alias (instance, dsc)
495 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
497 Ast.IdentArg (List.length l, id)
501 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
502 | IDENT "right"; IDENT "associative" -> Gramext.RightA
503 | IDENT "non"; IDENT "associative" -> Gramext.NonA
507 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
510 [ dir = OPT direction; s = QSTRING;
511 assoc = OPT associativity; prec = OPT precedence;
514 [ blob = UNPARSED_AST ->
515 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
516 (CicNotationParser.parse_level2_ast
517 (Ulexing.from_utf8_string blob))
518 | blob = UNPARSED_META ->
519 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
520 (CicNotationParser.parse_level2_meta
521 (Ulexing.from_utf8_string blob))
525 | None -> default_associativity
526 | Some assoc -> assoc
530 | None -> default_precedence
534 add_raw_attribute ~text:s
535 (CicNotationParser.parse_level1_pattern
536 (Ulexing.from_utf8_string s))
538 (dir, p1, assoc, prec, p2)
542 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
543 | id = IDENT -> Ast.VarPattern id
544 | SYMBOL "_" -> Ast.ImplicitPattern
545 | LPAREN; terms = LIST1 SELF; RPAREN ->
549 | terms -> Ast.ApplPattern terms)
553 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
559 IDENT "include" ; path = QSTRING ->
560 loc,path,LexiconAst.WithPreferences
561 | IDENT "include'" ; path = QSTRING ->
562 loc,path,LexiconAst.WithoutPreferences
566 IDENT "set"; n = QSTRING; v = QSTRING ->
567 GrafiteAst.Set (loc, n, v)
568 | IDENT "drop" -> GrafiteAst.Drop loc
569 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
570 | IDENT "qed" -> GrafiteAst.Qed loc
571 | IDENT "variant" ; name = IDENT; SYMBOL ":";
572 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
575 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
576 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
577 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
578 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
579 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
582 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
583 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
584 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
585 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
586 defs = CicNotationParser.let_defs ->
587 (* In case of mutual definitions here we produce just
588 the syntax tree for the first one. The others will be
589 generated from the completely specified term just before
590 insertion in the environment. We use the flavour
591 `MutualDefinition to rememer this. *)
594 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
597 (fun var ty -> Ast.Binder (`Pi,var,ty)
601 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
605 let body = Ast.Ident (name,None) in
607 if List.length defs = 1 then
612 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
613 Some (Ast.LetRec (ind_kind, defs, body))))
614 | IDENT "inductive"; spec = inductive_spec ->
615 let (params, ind_types) = spec in
616 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
617 | IDENT "coinductive"; spec = inductive_spec ->
618 let (params, ind_types) = spec in
619 let ind_types = (* set inductive flags to false (coinductive) *)
620 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
623 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
624 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
625 let arity = match arity with None -> 0 | Some x -> x in
626 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
627 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
628 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
629 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
630 let uris = List.map UriManager.uri_of_string uris in
631 GrafiteAst.Default (loc,what,uris)
632 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
633 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
634 refl = tactic_term -> refl ] ;
635 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
636 sym = tactic_term -> sym ] ;
637 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
638 trans = tactic_term -> trans ] ;
640 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
643 IDENT "alias" ; spec = alias_spec ->
644 LexiconAst.Alias (loc, spec)
645 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
646 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
647 | IDENT "interpretation"; id = QSTRING;
648 (symbol, args, l3) = interpretation ->
649 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
652 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
653 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
654 GrafiteAst.Tactic (loc, Some tac, punct)
655 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
656 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
657 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
658 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
662 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
663 GrafiteAst.Code (loc, ex)
665 GrafiteAst.Note (loc, str)
670 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
672 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
673 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
674 fun ~include_paths status ->
676 DependenciesParser.baseuri_of_script ~include_paths fname
679 LexiconEngine.eval_command status
680 (LexiconAst.Include (iloc,buri,mode,fullpath))
685 (GrafiteAst.Executable
686 (loc,GrafiteAst.Command
687 (loc,GrafiteAst.Include (iloc,buri))))
688 | scom = lexicon_command ; SYMBOL "." ->
689 fun ~include_paths status ->
690 let status = LexiconEngine.eval_command status scom in
692 | EOI -> raise End_of_file
697 let exc_located_wrapper f =
701 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
702 | Stdpp.Exc_located (floc, Stream.Error msg) ->
703 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
704 | Stdpp.Exc_located (floc, exn) ->
706 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
708 let parse_statement lexbuf =
710 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))