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 ] ];
68 ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
70 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
73 [ IDENT "normalize" -> `Normalize
74 | IDENT "reduce" -> `Reduce
75 | IDENT "simplify" -> `Simpl
76 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
77 | IDENT "whd" -> `Whd ]
79 sequent_pattern_spec: [
83 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
84 (id,match path with Some p -> p | None -> Ast.UserInput) ];
85 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
87 match goal_path, hyp_paths with
88 None, [] -> Some Ast.UserInput
90 | Some goal_path, _ -> Some goal_path
99 [ "match" ; wanted = tactic_term ;
100 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
102 | sps = sequent_pattern_spec ->
105 let wanted,hyp_paths,goal_path =
106 match wanted_and_sps with
107 wanted,None -> wanted, [], Some Ast.UserInput
108 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
110 wanted, hyp_paths, goal_path ] ->
112 None -> None,[],Some Ast.UserInput
116 [ SYMBOL ">" -> `LeftToRight
117 | SYMBOL "<" -> `RightToLeft ]
119 int: [ [ num = NUMBER -> int_of_string num ] ];
121 [ idents = OPT ident_list0 ->
122 match idents with None -> [] | Some idents -> idents
126 [ OPT [ IDENT "names" ];
127 num = OPT [ num = int -> num ];
128 idents = intros_names ->
132 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
134 [ IDENT "absurd"; t = tactic_term ->
135 GrafiteAst.Absurd (loc, t)
136 | IDENT "apply"; t = tactic_term ->
137 GrafiteAst.Apply (loc, t)
138 | IDENT "applyS"; t = tactic_term ; params =
139 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
140 string_of_int v | v = IDENT -> v ] -> i,v ] ->
141 GrafiteAst.ApplyS (loc, t, params)
142 | IDENT "assumption" ->
143 GrafiteAst.Assumption loc
144 | IDENT "auto"; params = auto_params ->
145 GrafiteAst.Auto (loc,params)
146 | IDENT "cases"; what = tactic_term;
147 (num, idents) = intros_spec ->
148 GrafiteAst.Cases (loc, what, idents)
149 | IDENT "clear"; ids = LIST1 IDENT ->
150 GrafiteAst.Clear (loc, ids)
151 | IDENT "clearbody"; id = IDENT ->
152 GrafiteAst.ClearBody (loc,id)
153 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
154 GrafiteAst.Change (loc, what, t)
155 | IDENT "constructor"; n = int ->
156 GrafiteAst.Constructor (loc, n)
157 | IDENT "contradiction" ->
158 GrafiteAst.Contradiction loc
159 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
160 GrafiteAst.Cut (loc, ident, t)
161 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
162 let idents = match idents with None -> [] | Some idents -> idents in
163 GrafiteAst.Decompose (loc, idents)
164 | IDENT "demodulate" -> GrafiteAst.Demodulate loc
165 | IDENT "destruct"; t = tactic_term ->
166 GrafiteAst.Destruct (loc, t)
167 | IDENT "elim"; what = tactic_term; using = using;
168 pattern = OPT pattern_spec;
169 (num, idents) = intros_spec ->
170 let pattern = match pattern with
171 | None -> None, [], Some Ast.UserInput
172 | Some pattern -> pattern
174 GrafiteAst.Elim (loc, what, using, pattern, num, idents)
175 | IDENT "elimType"; what = tactic_term; using = using;
176 (num, idents) = intros_spec ->
177 GrafiteAst.ElimType (loc, what, using, num, idents)
178 | IDENT "exact"; t = tactic_term ->
179 GrafiteAst.Exact (loc, t)
181 GrafiteAst.Exists loc
182 | IDENT "fail" -> GrafiteAst.Fail loc
183 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
186 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
187 ("the pattern cannot specify the term to replace, only its"
188 ^ " paths in the hypotheses and in the conclusion")))
190 GrafiteAst.Fold (loc, kind, t, p)
192 GrafiteAst.Fourier loc
193 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
194 let idents = match idents with None -> [] | Some idents -> idents in
195 GrafiteAst.FwdSimpl (loc, hyp, idents)
196 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
197 GrafiteAst.Generalize (loc,p,id)
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 ->
338 GrafiteAst.Do (loc, count, tac)
339 | IDENT "repeat"; tac = SELF -> 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 -> 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
365 non_punctuation_tactical:
367 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
368 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
369 | IDENT "skip" -> GrafiteAst.Skip loc
373 [ [ IDENT "definition" ] -> `Definition
374 | [ IDENT "fact" ] -> `Fact
375 | [ IDENT "lemma" ] -> `Lemma
376 | [ IDENT "remark" ] -> `Remark
377 | [ IDENT "theorem" ] -> `Theorem
381 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
382 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
383 fst_constructors = LIST0 constructor SEP SYMBOL "|";
386 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
387 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
388 (name, true, typ, constructors) ] SEP "with" -> types
392 (fun (names, typ) acc ->
393 (List.map (fun name -> (name, typ)) names) @ acc)
396 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
397 let tl_ind_types = match tl with None -> [] | Some types -> types in
398 let ind_types = fst_ind_type :: tl_ind_types in
403 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
404 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
408 SYMBOL ":" -> false,0
409 | SYMBOL ":"; SYMBOL ">" -> true,0
410 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
413 let b,n = coercion in
415 ] SEP SYMBOL ";"; SYMBOL "}" ->
418 (fun (names, typ) acc ->
419 (List.map (fun name -> (name, typ)) names) @ acc)
422 (params,name,typ,fields)
426 [ [ IDENT "check" ]; t = term ->
427 GrafiteAst.Check (loc, t)
429 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
430 suri = QSTRING; prefix = OPT QSTRING ->
431 let style = match style with
432 | None -> GrafiteAst.Declarative
433 | Some depth -> GrafiteAst.Procedural depth
435 let prefix = match prefix with None -> "" | Some prefix -> prefix in
436 GrafiteAst.Inline (loc,style,suri,prefix)
437 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
438 | [ IDENT "whelp"; "match" ] ; t = term ->
439 GrafiteAst.WMatch (loc,t)
440 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
441 GrafiteAst.WInstance (loc,t)
442 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
443 GrafiteAst.WLocate (loc,id)
444 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
445 GrafiteAst.WElim (loc, t)
446 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
447 GrafiteAst.WHint (loc,t)
451 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
452 let alpha = "[a-zA-Z]" in
453 let num = "[0-9]+" in
454 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
455 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
456 let rex = Str.regexp ("^"^ident^"$") in
457 if Str.string_match rex id 0 then
458 if (try ignore (UriManager.uri_of_string uri); true
459 with UriManager.IllFormedUri _ -> false)
461 LexiconAst.Ident_alias (id, uri)
464 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
466 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
467 Printf.sprintf "Not a valid identifier: %s" id)))
468 | IDENT "symbol"; symbol = QSTRING;
469 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
470 SYMBOL "="; dsc = QSTRING ->
472 match instance with Some i -> i | None -> 0
474 LexiconAst.Symbol_alias (symbol, instance, dsc)
476 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
477 SYMBOL "="; dsc = QSTRING ->
479 match instance with Some i -> i | None -> 0
481 LexiconAst.Number_alias (instance, dsc)
485 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
487 Ast.IdentArg (List.length l, id)
491 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
492 | IDENT "right"; IDENT "associative" -> Gramext.RightA
493 | IDENT "non"; IDENT "associative" -> Gramext.NonA
497 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
500 [ dir = OPT direction; s = QSTRING;
501 assoc = OPT associativity; prec = OPT precedence;
504 [ blob = UNPARSED_AST ->
505 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
506 (CicNotationParser.parse_level2_ast
507 (Ulexing.from_utf8_string blob))
508 | blob = UNPARSED_META ->
509 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
510 (CicNotationParser.parse_level2_meta
511 (Ulexing.from_utf8_string blob))
515 | None -> default_associativity
516 | Some assoc -> assoc
520 | None -> default_precedence
524 add_raw_attribute ~text:s
525 (CicNotationParser.parse_level1_pattern
526 (Ulexing.from_utf8_string s))
528 (dir, p1, assoc, prec, p2)
532 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
533 | id = IDENT -> Ast.VarPattern id
534 | SYMBOL "_" -> Ast.ImplicitPattern
535 | LPAREN; terms = LIST1 SELF; RPAREN ->
539 | terms -> Ast.ApplPattern terms)
543 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
549 IDENT "include" ; path = QSTRING ->
550 loc,path,LexiconAst.WithPreferences
551 | IDENT "include'" ; path = QSTRING ->
552 loc,path,LexiconAst.WithoutPreferences
556 IDENT "set"; n = QSTRING; v = QSTRING ->
557 GrafiteAst.Set (loc, n, v)
558 | IDENT "drop" -> GrafiteAst.Drop loc
559 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
560 | IDENT "qed" -> GrafiteAst.Qed loc
561 | IDENT "variant" ; name = IDENT; SYMBOL ":";
562 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
565 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
566 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
567 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
568 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
569 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
572 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
573 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
574 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
575 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
576 defs = CicNotationParser.let_defs ->
577 (* In case of mutual definitions here we produce just
578 the syntax tree for the first one. The others will be
579 generated from the completely specified term just before
580 insertion in the environment. We use the flavour
581 `MutualDefinition to rememer this. *)
584 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
587 (fun var ty -> Ast.Binder (`Pi,var,ty)
591 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
595 let body = Ast.Ident (name,None) in
597 if List.length defs = 1 then
602 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
603 Some (Ast.LetRec (ind_kind, defs, body))))
604 | IDENT "inductive"; spec = inductive_spec ->
605 let (params, ind_types) = spec in
606 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
607 | IDENT "coinductive"; spec = inductive_spec ->
608 let (params, ind_types) = spec in
609 let ind_types = (* set inductive flags to false (coinductive) *)
610 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
613 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
614 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
615 let arity = match arity with None -> 0 | Some x -> x in
616 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
617 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
618 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
619 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
620 let uris = List.map UriManager.uri_of_string uris in
621 GrafiteAst.Default (loc,what,uris)
622 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
623 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
624 refl = tactic_term -> refl ] ;
625 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
626 sym = tactic_term -> sym ] ;
627 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
628 trans = tactic_term -> trans ] ;
630 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
633 IDENT "alias" ; spec = alias_spec ->
634 LexiconAst.Alias (loc, spec)
635 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
636 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
637 | IDENT "interpretation"; id = QSTRING;
638 (symbol, args, l3) = interpretation ->
639 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
642 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
643 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
644 GrafiteAst.Tactic (loc, Some tac, punct)
645 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
646 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
647 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
648 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
652 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
653 GrafiteAst.Code (loc, ex)
655 GrafiteAst.Note (loc, str)
660 fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
662 fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
663 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
664 fun ~include_paths status ->
666 DependenciesParser.baseuri_of_script ~include_paths fname
669 LexiconEngine.eval_command status
670 (LexiconAst.Include (iloc,buri,mode,fullpath))
675 (GrafiteAst.Executable
676 (loc,GrafiteAst.Command
677 (loc,GrafiteAst.Include (iloc,buri))))
678 | scom = lexicon_command ; SYMBOL "." ->
679 fun ~include_paths status ->
680 let status = LexiconEngine.eval_command status scom in
682 | EOI -> raise End_of_file
687 let exc_located_wrapper f =
691 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
692 | Stdpp.Exc_located (floc, Stream.Error msg) ->
693 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
694 | Stdpp.Exc_located (floc, exn) ->
696 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
698 let parse_statement lexbuf =
700 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))