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 let mk_rec_corec ind_kind defs loc =
62 (* In case of mutual definitions here we produce just
63 the syntax tree for the first one. The others will be
64 generated from the completely specified term just before
65 insertion in the environment. We use the flavour
66 `MutualDefinition to rememer this. *)
69 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
72 (fun var ty -> Ast.Binder (`Pi,var,ty)
76 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
80 let body = Ast.Ident (name,None) in
82 if List.length defs = 1 then
87 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
88 Some (Ast.LetRec (ind_kind, defs, body))))
90 type by_continuation =
92 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
93 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
94 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
97 GLOBAL: term statement;
98 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
99 tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
101 [ id = IDENT -> Some id
102 | SYMBOL "_" -> None ]
104 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
106 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
109 [ IDENT "normalize" -> `Normalize
110 | IDENT "simplify" -> `Simpl
111 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
112 | IDENT "whd" -> `Whd ]
114 sequent_pattern_spec: [
118 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
119 (id,match path with Some p -> p | None -> Ast.UserInput) ];
120 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
122 match goal_path, hyp_paths with
123 None, [] -> Some Ast.UserInput
125 | Some goal_path, _ -> Some goal_path
134 [ "match" ; wanted = tactic_term ;
135 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
137 | sps = sequent_pattern_spec ->
140 let wanted,hyp_paths,goal_path =
141 match wanted_and_sps with
142 wanted,None -> wanted, [], Some Ast.UserInput
143 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
145 wanted, hyp_paths, goal_path ] ->
147 None -> None,[],Some Ast.UserInput
151 [ SYMBOL ">" -> `LeftToRight
152 | SYMBOL "<" -> `RightToLeft ]
154 int: [ [ num = NUMBER -> int_of_string num ] ];
156 [ idents = OPT ident_list0 ->
157 match idents with None -> [] | Some idents -> idents
161 [ OPT [ IDENT "names" ];
162 num = OPT [ num = int -> num ];
163 idents = intros_names ->
167 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
169 [ IDENT "absurd"; t = tactic_term ->
170 GrafiteAst.Absurd (loc, t)
171 | IDENT "apply"; t = tactic_term ->
172 GrafiteAst.Apply (loc, t)
173 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
174 GrafiteAst.ApplyS (loc, t, params)
175 | IDENT "assumption" ->
176 GrafiteAst.Assumption loc
177 | IDENT "autobatch"; params = auto_params ->
178 GrafiteAst.AutoBatch (loc,params)
179 | IDENT "cases"; what = tactic_term;
180 specs = intros_spec ->
181 GrafiteAst.Cases (loc, what, specs)
182 | IDENT "clear"; ids = LIST1 IDENT ->
183 GrafiteAst.Clear (loc, ids)
184 | IDENT "clearbody"; id = IDENT ->
185 GrafiteAst.ClearBody (loc,id)
186 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
187 GrafiteAst.Change (loc, what, t)
188 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
189 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
190 let times = match times with None -> 1 | Some i -> i in
191 GrafiteAst.Compose (loc, t1, t2, times, specs)
192 | IDENT "constructor"; n = int ->
193 GrafiteAst.Constructor (loc, n)
194 | IDENT "contradiction" ->
195 GrafiteAst.Contradiction loc
196 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
197 GrafiteAst.Cut (loc, ident, t)
198 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
199 let idents = match idents with None -> [] | Some idents -> idents in
200 GrafiteAst.Decompose (loc, idents)
201 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
202 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
203 GrafiteAst.Destruct (loc, xts)
204 | IDENT "elim"; what = tactic_term; using = using;
205 pattern = OPT pattern_spec;
206 (num, idents) = intros_spec ->
207 let pattern = match pattern with
208 | None -> None, [], Some Ast.UserInput
209 | Some pattern -> pattern
211 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
212 | IDENT "elimType"; what = tactic_term; using = using;
213 (num, idents) = intros_spec ->
214 GrafiteAst.ElimType (loc, what, using, (num, idents))
215 | IDENT "exact"; t = tactic_term ->
216 GrafiteAst.Exact (loc, t)
218 GrafiteAst.Exists loc
219 | IDENT "fail" -> GrafiteAst.Fail loc
220 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
223 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
224 ("the pattern cannot specify the term to replace, only its"
225 ^ " paths in the hypotheses and in the conclusion")))
227 GrafiteAst.Fold (loc, kind, t, p)
229 GrafiteAst.Fourier loc
230 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
231 let idents = match idents with None -> [] | Some idents -> idents in
232 GrafiteAst.FwdSimpl (loc, hyp, idents)
233 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
234 GrafiteAst.Generalize (loc,p,id)
235 | IDENT "id" -> GrafiteAst.IdTac loc
236 | IDENT "intro"; ident = OPT IDENT ->
237 let idents = match ident with None -> [] | Some id -> [Some id] in
238 GrafiteAst.Intros (loc, (Some 1, idents))
239 | IDENT "intros"; specs = intros_spec ->
240 GrafiteAst.Intros (loc, specs)
241 | IDENT "inversion"; t = tactic_term ->
242 GrafiteAst.Inversion (loc, t)
244 linear = OPT [ IDENT "linear" ];
245 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
247 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
248 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
249 let linear = match linear with None -> false | Some _ -> true in
250 let to_what = match to_what with None -> [] | Some to_what -> to_what in
251 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
252 | IDENT "left" -> GrafiteAst.Left loc
253 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
254 GrafiteAst.LetIn (loc, t, where)
255 | kind = reduction_kind; p = pattern_spec ->
256 GrafiteAst.Reduce (loc, kind, p)
257 | IDENT "reflexivity" ->
258 GrafiteAst.Reflexivity loc
259 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
260 GrafiteAst.Replace (loc, p, t)
261 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
262 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
266 (HExtlib.Localized (loc,
267 (CicNotationParser.Parse_error
268 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
270 let n = match xnames with None -> [] | Some names -> names in
271 GrafiteAst.Rewrite (loc, d, t, p, n)
278 | IDENT "symmetry" ->
279 GrafiteAst.Symmetry loc
280 | IDENT "transitivity"; t = tactic_term ->
281 GrafiteAst.Transitivity (loc, t)
282 (* Produzioni Aggiunte *)
283 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
284 GrafiteAst.Assume (loc, id, t)
285 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
286 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
287 t' = tactic_term -> t']->
288 GrafiteAst.Suppose (loc, t, id, t1)
289 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
290 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
291 id2 = IDENT ; RPAREN ->
292 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
294 [ IDENT "using"; t=tactic_term -> `Term t
295 | params = auto_params -> `Auto params] ;
296 cont=by_continuation ->
298 BYC_done -> GrafiteAst.Bydone (loc, just)
299 | BYC_weproved (ty,id,t1) ->
300 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
301 | BYC_letsuchthat (id1,t1,id2,t2) ->
302 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
303 | BYC_wehaveand (id1,t1,id2,t2) ->
304 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
305 | 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']->
306 GrafiteAst.We_need_to_prove (loc, t, id, t1)
307 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
308 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
309 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
310 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
311 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
312 GrafiteAst.Byinduction(loc, t, id)
313 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
314 GrafiteAst.Thesisbecomes(loc, t)
315 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
316 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
317 GrafiteAst.Case(loc,id,params)
318 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
320 termine = tactic_term;
324 [ IDENT "using"; t=tactic_term -> `Term t
325 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
326 | IDENT "proof" -> `Proof
327 | params = auto_params -> `Auto params];
328 cont = rewriting_step_continuation ->
329 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
330 | IDENT "obtain" ; name = IDENT;
331 termine = tactic_term;
335 [ IDENT "using"; t=tactic_term -> `Term t
336 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
337 | IDENT "proof" -> `Proof
338 | params = auto_params -> `Auto params];
339 cont = rewriting_step_continuation ->
340 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
344 [ IDENT "using"; t=tactic_term -> `Term t
345 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
346 | IDENT "proof" -> `Proof
347 | params = auto_params -> `Auto params];
348 cont = rewriting_step_continuation ->
349 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
353 [ IDENT "paramodulation"
365 i = auto_fixed_param -> i,""
366 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
367 string_of_int v | v = IDENT -> v ] -> i,v ];
368 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
369 (match tl with Some l -> l | None -> []),
374 [ WEPROVED; 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)
375 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
376 "done" -> BYC_weproved (ty,None,t1)
378 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
379 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
380 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
381 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
382 BYC_wehaveand (id1,t1,id2,t2)
385 rewriting_step_continuation : [
392 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
395 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
398 GrafiteAst.Seq (loc, ts)
401 [ tac = SELF; SYMBOL ";";
402 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
403 (GrafiteAst.Then (loc, tac, tacs))
406 [ IDENT "do"; count = int; tac = SELF ->
407 GrafiteAst.Do (loc, count, tac)
408 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
412 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
413 GrafiteAst.First (loc, tacs)
414 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
416 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
417 GrafiteAst.Solve (loc, tacs)
418 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
419 | LPAREN; tac = SELF; RPAREN -> tac
420 | tac = tactic -> tac
423 punctuation_tactical:
425 [ SYMBOL "[" -> GrafiteAst.Branch loc
426 | SYMBOL "|" -> GrafiteAst.Shift loc
427 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
428 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
429 | SYMBOL "]" -> GrafiteAst.Merge loc
430 | SYMBOL ";" -> GrafiteAst.Semicolon loc
431 | SYMBOL "." -> GrafiteAst.Dot loc
434 non_punctuation_tactical:
436 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
437 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
438 | IDENT "skip" -> GrafiteAst.Skip loc
442 [ [ IDENT "definition" ] -> `Definition
443 | [ IDENT "fact" ] -> `Fact
444 | [ IDENT "lemma" ] -> `Lemma
445 | [ IDENT "remark" ] -> `Remark
446 | [ IDENT "theorem" ] -> `Theorem
450 fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
451 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
452 fst_constructors = LIST0 constructor SEP SYMBOL "|";
455 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
456 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
457 (name, true, typ, constructors) ] SEP "with" -> types
461 (fun (names, typ) acc ->
462 (List.map (fun name -> (name, typ)) names) @ acc)
465 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
466 let tl_ind_types = match tl with None -> [] | Some types -> types in
467 let ind_types = fst_ind_type :: tl_ind_types in
472 name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
473 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
477 SYMBOL ":" -> false,0
478 | SYMBOL ":"; SYMBOL ">" -> true,0
479 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
482 let b,n = coercion in
484 ] SEP SYMBOL ";"; SYMBOL "}" ->
487 (fun (names, typ) acc ->
488 (List.map (fun name -> (name, typ)) names) @ acc)
491 (params,name,typ,fields)
495 [ [ IDENT "check" ]; t = term ->
496 GrafiteAst.Check (loc, t)
498 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
499 suri = QSTRING; prefix = OPT QSTRING ->
500 let style = match style with
501 | None -> GrafiteAst.Declarative
502 | Some depth -> GrafiteAst.Procedural depth
504 let prefix = match prefix with None -> "" | Some prefix -> prefix in
505 GrafiteAst.Inline (loc,style,suri,prefix)
506 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
507 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
508 | IDENT "auto"; params = auto_params ->
509 GrafiteAst.AutoInteractive (loc,params)
510 | [ IDENT "whelp"; "match" ] ; t = term ->
511 GrafiteAst.WMatch (loc,t)
512 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
513 GrafiteAst.WInstance (loc,t)
514 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
515 GrafiteAst.WLocate (loc,id)
516 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
517 GrafiteAst.WElim (loc, t)
518 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
519 GrafiteAst.WHint (loc,t)
523 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
524 let alpha = "[a-zA-Z]" in
525 let num = "[0-9]+" in
526 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
527 let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
528 let rex = Str.regexp ("^"^ident^"$") in
529 if Str.string_match rex id 0 then
530 if (try ignore (UriManager.uri_of_string uri); true
531 with UriManager.IllFormedUri _ -> false)
533 LexiconAst.Ident_alias (id, uri)
536 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
538 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
539 Printf.sprintf "Not a valid identifier: %s" id)))
540 | IDENT "symbol"; symbol = QSTRING;
541 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
542 SYMBOL "="; dsc = QSTRING ->
544 match instance with Some i -> i | None -> 0
546 LexiconAst.Symbol_alias (symbol, instance, dsc)
548 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
549 SYMBOL "="; dsc = QSTRING ->
551 match instance with Some i -> i | None -> 0
553 LexiconAst.Number_alias (instance, dsc)
557 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
559 Ast.IdentArg (List.length l, id)
563 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
564 | IDENT "right"; IDENT "associative" -> Gramext.RightA
565 | IDENT "non"; IDENT "associative" -> Gramext.NonA
569 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
572 [ dir = OPT direction; s = QSTRING;
573 assoc = OPT associativity; prec = OPT precedence;
576 [ blob = UNPARSED_AST ->
577 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
578 (CicNotationParser.parse_level2_ast
579 (Ulexing.from_utf8_string blob))
580 | blob = UNPARSED_META ->
581 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
582 (CicNotationParser.parse_level2_meta
583 (Ulexing.from_utf8_string blob))
587 | None -> default_associativity
588 | Some assoc -> assoc
592 | None -> default_precedence
596 add_raw_attribute ~text:s
597 (CicNotationParser.parse_level1_pattern
598 (Ulexing.from_utf8_string s))
600 (dir, p1, assoc, prec, p2)
604 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
605 | id = IDENT -> Ast.VarPattern id
606 | SYMBOL "_" -> Ast.ImplicitPattern
607 | LPAREN; terms = LIST1 SELF; RPAREN ->
611 | terms -> Ast.ApplPattern terms)
615 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
621 IDENT "include" ; path = QSTRING ->
622 loc,path,LexiconAst.WithPreferences
623 | IDENT "include'" ; path = QSTRING ->
624 loc,path,LexiconAst.WithoutPreferences
628 IDENT "set"; n = QSTRING; v = QSTRING ->
629 GrafiteAst.Set (loc, n, v)
630 | IDENT "drop" -> GrafiteAst.Drop loc
631 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
632 | IDENT "qed" -> GrafiteAst.Qed loc
633 | IDENT "variant" ; name = IDENT; SYMBOL ":";
634 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
637 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
638 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
639 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
640 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
641 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
644 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
645 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
646 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
647 | LETCOREC ; defs = CicNotationParser.let_defs ->
648 mk_rec_corec `CoInductive defs loc
649 | LETREC ; defs = CicNotationParser.let_defs ->
650 mk_rec_corec `Inductive defs loc
651 | IDENT "inductive"; spec = inductive_spec ->
652 let (params, ind_types) = spec in
653 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
654 | IDENT "coinductive"; spec = inductive_spec ->
655 let (params, ind_types) = spec in
656 let ind_types = (* set inductive flags to false (coinductive) *)
657 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
660 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
661 | IDENT "coercion" ; suri = URI ; arity = OPT int ;
662 saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
663 let arity = match arity with None -> 0 | Some x -> x in
664 let saturations = match saturations with None -> 0 | Some x -> x in
665 let composites = match composites with None -> true | Some _ -> false in
667 (loc, UriManager.uri_of_string suri, composites, arity, saturations)
668 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
669 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
670 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
671 let uris = List.map UriManager.uri_of_string uris in
672 GrafiteAst.Default (loc,what,uris)
673 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
674 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
675 refl = tactic_term -> refl ] ;
676 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
677 sym = tactic_term -> sym ] ;
678 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
679 trans = tactic_term -> trans ] ;
681 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
684 IDENT "alias" ; spec = alias_spec ->
685 LexiconAst.Alias (loc, spec)
686 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
687 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
688 | IDENT "interpretation"; id = QSTRING;
689 (symbol, args, l3) = interpretation ->
690 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
693 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
694 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
695 GrafiteAst.Tactic (loc, Some tac, punct)
696 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
697 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
698 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
699 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
703 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
704 GrafiteAst.Code (loc, ex)
706 GrafiteAst.Note (loc, str)
711 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
713 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
714 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
715 fun ?(never_include=false) ~include_paths status ->
716 let _root, buri, fullpath, _rrelpath =
717 Librarian.baseuri_of_script ~include_paths fname
720 if never_include then raise (NoInclusionPerformed fullpath)
721 else LexiconEngine.eval_command status
722 (LexiconAst.Include (iloc,buri,mode,fullpath))
727 (GrafiteAst.Executable
728 (loc,GrafiteAst.Command
729 (loc,GrafiteAst.Include (iloc,buri))))
730 | scom = lexicon_command ; SYMBOL "." ->
731 fun ?(never_include=false) ~include_paths status ->
732 let status = LexiconEngine.eval_command status scom in
734 | EOI -> raise End_of_file
739 let exc_located_wrapper f =
743 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
744 | Stdpp.Exc_located (floc, Stream.Error msg) ->
745 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
746 | Stdpp.Exc_located (floc, exn) ->
748 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
750 let parse_statement lexbuf =
752 (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))