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 pattern = OPT pattern_spec;
168 (num, idents) = intros_spec ->
169 let pattern = match pattern with
170 | None -> None, [], Some Ast.UserInput
171 | Some pattern -> pattern
173 GrafiteAst.Elim (loc, what, using, pattern, num, idents)
174 | IDENT "elimType"; what = tactic_term; using = using;
175 (num, idents) = intros_spec ->
176 GrafiteAst.ElimType (loc, what, using, num, idents)
177 | IDENT "exact"; t = tactic_term ->
178 GrafiteAst.Exact (loc, t)
180 GrafiteAst.Exists loc
181 | IDENT "fail" -> GrafiteAst.Fail loc
182 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
185 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
186 ("the pattern cannot specify the term to replace, only its"
187 ^ " paths in the hypotheses and in the conclusion")))
189 GrafiteAst.Fold (loc, kind, t, p)
191 GrafiteAst.Fourier loc
192 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
193 let idents = match idents with None -> [] | Some idents -> idents in
194 GrafiteAst.FwdSimpl (loc, hyp, idents)
195 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
196 GrafiteAst.Generalize (loc,p,id)
197 | IDENT "goal"; n = int ->
198 GrafiteAst.Goal (loc, n)
199 | IDENT "id" -> GrafiteAst.IdTac loc
200 | IDENT "intro"; ident = OPT IDENT ->
201 let idents = match ident with None -> [] | Some id -> [id] in
202 GrafiteAst.Intros (loc, Some 1, idents)
203 | IDENT "intros"; (num, idents) = intros_spec ->
204 GrafiteAst.Intros (loc, num, idents)
205 | IDENT "inversion"; t = tactic_term ->
206 GrafiteAst.Inversion (loc, t)
208 linear = OPT [ IDENT "linear" ];
209 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
211 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
212 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
213 let linear = match linear with None -> false | Some _ -> true in
214 let to_what = match to_what with None -> [] | Some to_what -> to_what in
215 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
216 | IDENT "left" -> GrafiteAst.Left loc
217 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
218 GrafiteAst.LetIn (loc, t, where)
219 | kind = reduction_kind; p = pattern_spec ->
220 GrafiteAst.Reduce (loc, kind, p)
221 | IDENT "reflexivity" ->
222 GrafiteAst.Reflexivity loc
223 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
224 GrafiteAst.Replace (loc, p, t)
225 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
226 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
230 (HExtlib.Localized (loc,
231 (CicNotationParser.Parse_error
232 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
234 let n = match xnames with None -> [] | Some names -> names in
235 GrafiteAst.Rewrite (loc, d, t, p, n)
244 | IDENT "symmetry" ->
245 GrafiteAst.Symmetry loc
246 | IDENT "transitivity"; t = tactic_term ->
247 GrafiteAst.Transitivity (loc, t)
248 (* Produzioni Aggiunte *)
249 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
250 GrafiteAst.Assume (loc, id, t)
251 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
252 GrafiteAst.Suppose (loc, t, id, t1)
253 | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
254 cont=by_continuation ->
255 let t' = match t with LNone _ -> None | LSome t -> Some t in
257 BYC_done -> GrafiteAst.Bydone (loc, t')
258 | BYC_weproved (ty,id,t1) ->
259 GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
260 | BYC_letsuchthat (id1,t1,id2,t2) ->
263 raise (HExtlib.Localized
264 (floc,CicNotationParser.Parse_error
265 "tactic_term expected here"))
266 | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
267 | BYC_wehaveand (id1,t1,id2,t2) ->
270 raise (HExtlib.Localized
271 (floc,CicNotationParser.Parse_error
272 "tactic_term expected here"))
273 | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
274 | 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']->
275 GrafiteAst.We_need_to_prove (loc, t, id, t1)
276 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
277 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
278 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
279 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
280 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
281 GrafiteAst.Byinduction(loc, t, id)
282 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
283 GrafiteAst.Thesisbecomes(loc, t)
284 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
285 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
286 GrafiteAst.Case(loc,id,params)
287 | 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 ->
288 GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
289 | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
290 cont=rewriting_step_continuation ->
291 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
296 LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
297 string_of_int v | v = IDENT -> v ] -> i,v ] ->
302 [ LPAREN; params = auto_params; RPAREN -> params
307 [ 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)
308 | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
309 IDENT "done" -> BYC_weproved (ty,None,t1)
310 | IDENT "done" -> BYC_done
311 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
312 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
313 | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
314 BYC_wehaveand (id1,t1,id2,t2)
317 rewriting_step_continuation : [
318 [ IDENT "done" -> true
324 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
327 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
330 GrafiteAst.Seq (loc, ts)
333 [ tac = SELF; SYMBOL ";";
334 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
335 (GrafiteAst.Then (loc, tac, tacs))
338 [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
339 GrafiteAst.Do (loc, count, tac)
340 | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
344 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
345 GrafiteAst.First (loc, tacs)
346 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
348 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
349 GrafiteAst.Solve (loc, tacs)
350 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
351 | LPAREN; tac = SELF; RPAREN -> tac
352 | tac = tactic -> GrafiteAst.Tactic (loc, tac)
355 punctuation_tactical:
357 [ SYMBOL "[" -> GrafiteAst.Branch loc
358 | SYMBOL "|" -> GrafiteAst.Shift loc
359 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
360 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
361 | SYMBOL "]" -> GrafiteAst.Merge loc
362 | SYMBOL ";" -> GrafiteAst.Semicolon loc
363 | SYMBOL "." -> GrafiteAst.Dot loc
368 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
369 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
370 | IDENT "skip" -> GrafiteAst.Skip loc
371 | tac = atomic_tactical LEVEL "loops" -> tac
375 [ [ IDENT "definition" ] -> `Definition
376 | [ IDENT "fact" ] -> `Fact
377 | [ IDENT "lemma" ] -> `Lemma
378 | [ IDENT "remark" ] -> `Remark
379 | [ IDENT "theorem" ] -> `Theorem
383 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
384 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
385 fst_constructors = LIST0 constructor SEP SYMBOL "|";
388 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
389 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
390 (name, true, typ, constructors) ] SEP "with" -> types
394 (fun (names, typ) acc ->
395 (List.map (fun name -> (name, typ)) names) @ acc)
398 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
399 let tl_ind_types = match tl with None -> [] | Some types -> types in
400 let ind_types = fst_ind_type :: tl_ind_types in
405 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
406 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
410 SYMBOL ":" -> false,0
411 | SYMBOL ":"; SYMBOL ">" -> true,0
412 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
415 let b,n = coercion in
417 ] SEP SYMBOL ";"; SYMBOL "}" ->
420 (fun (names, typ) acc ->
421 (List.map (fun name -> (name, typ)) names) @ acc)
424 (params,name,typ,fields)
428 [ [ IDENT "check" ]; t = term ->
429 GrafiteAst.Check (loc, t)
431 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
432 suri = QSTRING; prefix = OPT QSTRING ->
433 let style = match style with
434 | None -> GrafiteAst.Declarative
435 | Some depth -> GrafiteAst.Procedural depth
437 let prefix = match prefix with None -> "" | Some prefix -> prefix in
438 GrafiteAst.Inline (loc,style,suri,prefix)
439 | [ IDENT "hint" ] -> GrafiteAst.Hint loc
440 | [ IDENT "whelp"; "match" ] ; t = term ->
441 GrafiteAst.WMatch (loc,t)
442 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
443 GrafiteAst.WInstance (loc,t)
444 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
445 GrafiteAst.WLocate (loc,id)
446 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
447 GrafiteAst.WElim (loc, t)
448 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
449 GrafiteAst.WHint (loc,t)
453 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
454 let alpha = "[a-zA-Z]" in
455 let num = "[0-9]+" in
456 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
457 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
458 let rex = Str.regexp ("^"^ident^"$") in
459 if Str.string_match rex id 0 then
460 if (try ignore (UriManager.uri_of_string uri); true
461 with UriManager.IllFormedUri _ -> false)
463 LexiconAst.Ident_alias (id, uri)
466 (HExtlib.Localized (loc, CicNotationParser.Parse_error (sprintf "Not a valid uri: %s" uri)))
468 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
469 sprintf "Not a valid identifier: %s" id)))
470 | IDENT "symbol"; symbol = QSTRING;
471 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
472 SYMBOL "="; dsc = QSTRING ->
474 match instance with Some i -> i | None -> 0
476 LexiconAst.Symbol_alias (symbol, instance, dsc)
478 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
479 SYMBOL "="; dsc = QSTRING ->
481 match instance with Some i -> i | None -> 0
483 LexiconAst.Number_alias (instance, dsc)
487 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
489 Ast.IdentArg (List.length l, id)
493 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
494 | IDENT "right"; IDENT "associative" -> Gramext.RightA
495 | IDENT "non"; IDENT "associative" -> Gramext.NonA
499 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
502 [ dir = OPT direction; s = QSTRING;
503 assoc = OPT associativity; prec = OPT precedence;
506 [ blob = UNPARSED_AST ->
507 add_raw_attribute ~text:(sprintf "@{%s}" blob)
508 (CicNotationParser.parse_level2_ast
509 (Ulexing.from_utf8_string blob))
510 | blob = UNPARSED_META ->
511 add_raw_attribute ~text:(sprintf "${%s}" blob)
512 (CicNotationParser.parse_level2_meta
513 (Ulexing.from_utf8_string blob))
517 | None -> default_associativity
518 | Some assoc -> assoc
522 | None -> default_precedence
526 add_raw_attribute ~text:s
527 (CicNotationParser.parse_level1_pattern
528 (Ulexing.from_utf8_string s))
530 (dir, p1, assoc, prec, p2)
534 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
535 | id = IDENT -> Ast.VarPattern id
536 | SYMBOL "_" -> Ast.ImplicitPattern
537 | LPAREN; terms = LIST1 SELF; RPAREN ->
541 | terms -> Ast.ApplPattern terms)
545 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
551 IDENT "include" ; path = QSTRING ->
552 loc,path,LexiconAst.WithPreferences
553 | IDENT "include'" ; path = QSTRING ->
554 loc,path,LexiconAst.WithoutPreferences
558 IDENT "set"; n = QSTRING; v = QSTRING ->
559 GrafiteAst.Set (loc, n, v)
560 | IDENT "drop" -> GrafiteAst.Drop loc
561 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
562 | IDENT "qed" -> GrafiteAst.Qed loc
563 | IDENT "variant" ; name = IDENT; SYMBOL ":";
564 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
567 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
568 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
569 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
570 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
571 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
574 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
575 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
576 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
577 | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
578 defs = CicNotationParser.let_defs ->
579 (* In case of mutual definitions here we produce just
580 the syntax tree for the first one. The others will be
581 generated from the completely specified term just before
582 insertion in the environment. We use the flavour
583 `MutualDefinition to rememer this. *)
586 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
589 (fun var ty -> Ast.Binder (`Pi,var,ty)
593 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
597 let body = Ast.Ident (name,None) in
599 if List.length defs = 1 then
604 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
605 Some (Ast.LetRec (ind_kind, defs, body))))
606 | IDENT "inductive"; spec = inductive_spec ->
607 let (params, ind_types) = spec in
608 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
609 | IDENT "coinductive"; spec = inductive_spec ->
610 let (params, ind_types) = spec in
611 let ind_types = (* set inductive flags to false (coinductive) *)
612 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
615 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
616 | IDENT "coercion" ; suri = URI ; arity = OPT int ->
617 let arity = match arity with None -> 0 | Some x -> x in
618 GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
619 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
620 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
621 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
622 let uris = List.map UriManager.uri_of_string uris in
623 GrafiteAst.Default (loc,what,uris)
624 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
625 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
626 refl = tactic_term -> refl ] ;
627 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
628 sym = tactic_term -> sym ] ;
629 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
630 trans = tactic_term -> trans ] ;
632 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
635 IDENT "alias" ; spec = alias_spec ->
636 LexiconAst.Alias (loc, spec)
637 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
638 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
639 | IDENT "interpretation"; id = QSTRING;
640 (symbol, args, l3) = interpretation ->
641 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
644 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
645 | tac = tactical; punct = punctuation_tactical ->
646 GrafiteAst.Tactical (loc, tac, Some punct)
647 | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
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))
674 (GrafiteAst.Executable
675 (loc,GrafiteAst.Command
676 (loc,GrafiteAst.Include (iloc,buri))))
677 | scom = lexicon_command ; SYMBOL "." ->
678 fun ~include_paths status ->
679 let status = LexiconEngine.eval_command status scom in
681 | EOI -> raise End_of_file
686 let exc_located_wrapper f =
690 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
691 | Stdpp.Exc_located (floc, Stream.Error msg) ->
692 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
693 | Stdpp.Exc_located (floc, exn) ->
695 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
697 let parse_statement lexbuf =
699 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))