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 type parser_status = {
53 term : CicNotationPt.term Grammar.Entry.e;
54 statement : statement Grammar.Entry.e;
57 let initial_parser () =
58 let grammar = CicNotationParser.level2_ast_grammar () in
59 let term = CicNotationParser.term () in
60 let statement = Grammar.Entry.create grammar "statement" in
61 { grammar = grammar; term = term; statement = statement }
64 let grafite_parser = ref (initial_parser ())
66 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
68 let default_associativity = Gramext.NonA
70 let mk_rec_corec ind_kind defs loc =
71 (* In case of mutual definitions here we produce just
72 the syntax tree for the first one. The others will be
73 generated from the completely specified term just before
74 insertion in the environment. We use the flavour
75 `MutualDefinition to rememer this. *)
78 | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
81 (fun var ty -> Ast.Binder (`Pi,var,ty)
85 | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
89 let body = Ast.Ident (name,None) in
91 if List.length defs = 1 then
96 GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
97 Some (Ast.LetRec (ind_kind, defs, body))))
99 type by_continuation =
101 | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
102 | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
103 | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
105 let initialize_parser () =
106 (* {{{ parser initialization *)
107 let term = !grafite_parser.term in
108 let statement = !grafite_parser.statement in
109 let let_defs = CicNotationParser.let_defs () in
110 let protected_binder_vars = CicNotationParser.protected_binder_vars () in
112 GLOBAL: term statement;
113 constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
114 tactic_term: [ [ t = term LEVEL "90" -> t ] ];
116 [ id = IDENT -> Some id
117 | SYMBOL "_" -> None ]
119 ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
121 [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
124 [ IDENT "normalize" -> `Normalize
125 | IDENT "simplify" -> `Simpl
126 | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
127 | IDENT "whd" -> `Whd ]
129 sequent_pattern_spec: [
133 path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
134 (id,match path with Some p -> p | None -> Ast.UserInput) ];
135 goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
137 match goal_path, hyp_paths with
138 None, [] -> Some Ast.UserInput
140 | Some goal_path, _ -> Some goal_path
149 [ "match" ; wanted = tactic_term ;
150 sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
152 | sps = sequent_pattern_spec ->
155 let wanted,hyp_paths,goal_path =
156 match wanted_and_sps with
157 wanted,None -> wanted, [], Some Ast.UserInput
158 | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
160 wanted, hyp_paths, goal_path ] ->
162 None -> None,[],Some Ast.UserInput
166 [ SYMBOL ">" -> `LeftToRight
167 | SYMBOL "<" -> `RightToLeft ]
169 int: [ [ num = NUMBER -> int_of_string num ] ];
171 [ idents = OPT ident_list0 ->
172 match idents with None -> [] | Some idents -> idents
176 [ OPT [ IDENT "names" ];
177 num = OPT [ num = int -> num ];
178 idents = intros_names ->
182 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
184 [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
185 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
186 GrafiteAst.NCases (loc, what, where)
187 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
188 GrafiteAst.NChange (loc, what, with_what)
189 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
190 GrafiteAst.NElim (loc, what, where)
191 | IDENT "ngeneralize"; p=pattern_spec ->
192 GrafiteAst.NGeneralize (loc, p)
193 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
194 GrafiteAst.NRewrite (loc, dir, what, where)
195 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
196 where = pattern_spec ->
197 let delta = match delta with None -> true | _ -> false in
198 GrafiteAst.NEval (loc, where, `Whd delta)
199 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
200 | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
201 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
202 | SYMBOL "*"; n=IDENT ->
203 GrafiteAst.NCase1 (loc,n)
207 [ IDENT "absurd"; t = tactic_term ->
208 GrafiteAst.Absurd (loc, t)
209 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
210 GrafiteAst.ApplyRule (loc, t)
211 | IDENT "apply"; t = tactic_term ->
212 GrafiteAst.Apply (loc, t)
213 | IDENT "applyP"; t = tactic_term ->
214 GrafiteAst.ApplyP (loc, t)
215 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
216 GrafiteAst.ApplyS (loc, t, params)
217 | IDENT "assumption" ->
218 GrafiteAst.Assumption loc
219 | IDENT "autobatch"; params = auto_params ->
220 GrafiteAst.AutoBatch (loc,params)
221 | IDENT "cases"; what = tactic_term;
222 pattern = OPT pattern_spec;
223 specs = intros_spec ->
224 let pattern = match pattern with
225 | None -> None, [], Some Ast.UserInput
226 | Some pattern -> pattern
228 GrafiteAst.Cases (loc, what, pattern, specs)
229 | IDENT "clear"; ids = LIST1 IDENT ->
230 GrafiteAst.Clear (loc, ids)
231 | IDENT "clearbody"; id = IDENT ->
232 GrafiteAst.ClearBody (loc,id)
233 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
234 GrafiteAst.Change (loc, what, t)
235 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
236 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
237 let times = match times with None -> 1 | Some i -> i in
238 GrafiteAst.Compose (loc, t1, t2, times, specs)
239 | IDENT "constructor"; n = int ->
240 GrafiteAst.Constructor (loc, n)
241 | IDENT "contradiction" ->
242 GrafiteAst.Contradiction loc
243 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
244 GrafiteAst.Cut (loc, ident, t)
245 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
246 let idents = match idents with None -> [] | Some idents -> idents in
247 GrafiteAst.Decompose (loc, idents)
248 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
249 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
250 GrafiteAst.Destruct (loc, xts)
251 | IDENT "elim"; what = tactic_term; using = using;
252 pattern = OPT pattern_spec;
253 ispecs = intros_spec ->
254 let pattern = match pattern with
255 | None -> None, [], Some Ast.UserInput
256 | Some pattern -> pattern
258 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
259 | IDENT "elimType"; what = tactic_term; using = using;
260 (num, idents) = intros_spec ->
261 GrafiteAst.ElimType (loc, what, using, (num, idents))
262 | IDENT "exact"; t = tactic_term ->
263 GrafiteAst.Exact (loc, t)
265 GrafiteAst.Exists loc
266 | IDENT "fail" -> GrafiteAst.Fail loc
267 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
270 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
271 ("the pattern cannot specify the term to replace, only its"
272 ^ " paths in the hypotheses and in the conclusion")))
274 GrafiteAst.Fold (loc, kind, t, p)
276 GrafiteAst.Fourier loc
277 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
278 let idents = match idents with None -> [] | Some idents -> idents in
279 GrafiteAst.FwdSimpl (loc, hyp, idents)
280 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
281 GrafiteAst.Generalize (loc,p,id)
282 | IDENT "id" -> GrafiteAst.IdTac loc
283 | IDENT "intro"; ident = OPT IDENT ->
284 let idents = match ident with None -> [] | Some id -> [Some id] in
285 GrafiteAst.Intros (loc, (Some 1, idents))
286 | IDENT "intros"; specs = intros_spec ->
287 GrafiteAst.Intros (loc, specs)
288 | IDENT "inversion"; t = tactic_term ->
289 GrafiteAst.Inversion (loc, t)
291 linear = OPT [ IDENT "linear" ];
292 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
294 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
295 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
296 let linear = match linear with None -> false | Some _ -> true in
297 let to_what = match to_what with None -> [] | Some to_what -> to_what in
298 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
299 | IDENT "left" -> GrafiteAst.Left loc
300 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
301 GrafiteAst.LetIn (loc, t, where)
302 | kind = reduction_kind; p = pattern_spec ->
303 GrafiteAst.Reduce (loc, kind, p)
304 | IDENT "reflexivity" ->
305 GrafiteAst.Reflexivity loc
306 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
307 GrafiteAst.Replace (loc, p, t)
308 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
309 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
313 (HExtlib.Localized (loc,
314 (CicNotationParser.Parse_error
315 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
317 let n = match xnames with None -> [] | Some names -> names in
318 GrafiteAst.Rewrite (loc, d, t, p, n)
325 | IDENT "symmetry" ->
326 GrafiteAst.Symmetry loc
327 | IDENT "transitivity"; t = tactic_term ->
328 GrafiteAst.Transitivity (loc, t)
329 (* Produzioni Aggiunte *)
330 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
331 GrafiteAst.Assume (loc, id, t)
332 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
333 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
334 t' = tactic_term -> t']->
335 GrafiteAst.Suppose (loc, t, id, t1)
336 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
337 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
338 id2 = IDENT ; RPAREN ->
339 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
341 [ IDENT "using"; t=tactic_term -> `Term t
342 | params = auto_params -> `Auto params] ;
343 cont=by_continuation ->
345 BYC_done -> GrafiteAst.Bydone (loc, just)
346 | BYC_weproved (ty,id,t1) ->
347 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
348 | BYC_letsuchthat (id1,t1,id2,t2) ->
349 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
350 | BYC_wehaveand (id1,t1,id2,t2) ->
351 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
352 | 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']->
353 GrafiteAst.We_need_to_prove (loc, t, id, t1)
354 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
355 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
356 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
357 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
358 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
359 GrafiteAst.Byinduction(loc, t, id)
360 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
361 GrafiteAst.Thesisbecomes(loc, t)
362 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
363 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
364 GrafiteAst.Case(loc,id,params)
365 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
367 termine = tactic_term;
371 [ IDENT "using"; t=tactic_term -> `Term t
372 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
373 | IDENT "proof" -> `Proof
374 | params = auto_params -> `Auto params];
375 cont = rewriting_step_continuation ->
376 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
377 | IDENT "obtain" ; name = IDENT;
378 termine = tactic_term;
382 [ IDENT "using"; t=tactic_term -> `Term t
383 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
384 | IDENT "proof" -> `Proof
385 | params = auto_params -> `Auto params];
386 cont = rewriting_step_continuation ->
387 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
391 [ IDENT "using"; t=tactic_term -> `Term t
392 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
393 | IDENT "proof" -> `Proof
394 | params = auto_params -> `Auto params];
395 cont = rewriting_step_continuation ->
396 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
400 [ IDENT "paramodulation"
412 i = auto_fixed_param -> i,""
413 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
414 string_of_int v | v = IDENT -> v ] -> i,v ];
415 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
416 (match tl with Some l -> l | None -> []),
421 [ 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)
422 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
423 "done" -> BYC_weproved (ty,None,t1)
425 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
426 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
427 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
428 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
429 BYC_wehaveand (id1,t1,id2,t2)
432 rewriting_step_continuation : [
439 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
442 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
445 GrafiteAst.Seq (loc, ts)
448 [ tac = SELF; SYMBOL ";";
449 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
450 (GrafiteAst.Then (loc, tac, tacs))
453 [ IDENT "do"; count = int; tac = SELF ->
454 GrafiteAst.Do (loc, count, tac)
455 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
459 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
460 GrafiteAst.First (loc, tacs)
461 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
463 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
464 GrafiteAst.Solve (loc, tacs)
465 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
466 | LPAREN; tac = SELF; RPAREN -> tac
467 | tac = tactic -> tac
470 punctuation_tactical:
472 [ SYMBOL "[" -> GrafiteAst.Branch loc
473 | SYMBOL "|" -> GrafiteAst.Shift loc
474 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
475 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
476 | SYMBOL "]" -> GrafiteAst.Merge loc
477 | SYMBOL ";" -> GrafiteAst.Semicolon loc
478 | SYMBOL "." -> GrafiteAst.Dot loc
481 non_punctuation_tactical:
483 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
484 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
485 | IDENT "skip" -> GrafiteAst.Skip loc
489 [ [ IDENT "ntheorem" ] -> `Theorem
493 [ [ IDENT "definition" ] -> `Definition
494 | [ IDENT "fact" ] -> `Fact
495 | [ IDENT "lemma" ] -> `Lemma
496 | [ IDENT "remark" ] -> `Remark
497 | [ IDENT "theorem" ] -> `Theorem
501 [ attr = theorem_flavour -> attr
502 | [ IDENT "axiom" ] -> `Axiom
503 | [ IDENT "mutual" ] -> `MutualDefinition
508 params = LIST0 protected_binder_vars;
509 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
510 fst_constructors = LIST0 constructor SEP SYMBOL "|";
513 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
514 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
515 (name, true, typ, constructors) ] SEP "with" -> types
519 (fun (names, typ) acc ->
520 (List.map (fun name -> (name, typ)) names) @ acc)
523 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
524 let tl_ind_types = match tl with None -> [] | Some types -> types in
525 let ind_types = fst_ind_type :: tl_ind_types in
531 params = LIST0 protected_binder_vars;
532 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
536 SYMBOL ":" -> false,0
537 | SYMBOL ":"; SYMBOL ">" -> true,0
538 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
541 let b,n = coercion in
543 ] SEP SYMBOL ";"; SYMBOL "}" ->
546 (fun (names, typ) acc ->
547 (List.map (fun name -> (name, typ)) names) @ acc)
550 (params,name,typ,fields)
554 [ [ IDENT "check" ]; t = term ->
555 GrafiteAst.Check (loc, t)
556 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
557 GrafiteAst.Eval (loc, kind, t)
559 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
560 suri = QSTRING; prefix = OPT QSTRING;
561 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
562 let style = match style with
563 | None -> GrafiteAst.Declarative
564 | Some depth -> GrafiteAst.Procedural depth
566 let prefix = match prefix with None -> "" | Some prefix -> prefix in
567 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
568 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
569 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
570 | IDENT "auto"; params = auto_params ->
571 GrafiteAst.AutoInteractive (loc,params)
572 | [ IDENT "whelp"; "match" ] ; t = term ->
573 GrafiteAst.WMatch (loc,t)
574 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
575 GrafiteAst.WInstance (loc,t)
576 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
577 GrafiteAst.WLocate (loc,id)
578 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
579 GrafiteAst.WElim (loc, t)
580 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
581 GrafiteAst.WHint (loc,t)
585 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
586 let alpha = "[a-zA-Z]" in
587 let num = "[0-9]+" in
588 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
589 let decoration = "\\'" in
590 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
591 let rex = Str.regexp ("^"^ident^"$") in
592 if Str.string_match rex id 0 then
593 if (try ignore (UriManager.uri_of_string uri); true
594 with UriManager.IllFormedUri _ -> false)
596 LexiconAst.Ident_alias (id, uri)
599 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
601 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
602 Printf.sprintf "Not a valid identifier: %s" id)))
603 | IDENT "symbol"; symbol = QSTRING;
604 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
605 SYMBOL "="; dsc = QSTRING ->
607 match instance with Some i -> i | None -> 0
609 LexiconAst.Symbol_alias (symbol, instance, dsc)
611 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
612 SYMBOL "="; dsc = QSTRING ->
614 match instance with Some i -> i | None -> 0
616 LexiconAst.Number_alias (instance, dsc)
620 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
622 Ast.IdentArg (List.length l, id)
626 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
627 | IDENT "right"; IDENT "associative" -> Gramext.RightA
628 | IDENT "non"; IDENT "associative" -> Gramext.NonA
632 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
635 [ dir = OPT direction; s = QSTRING;
636 assoc = OPT associativity; prec = precedence;
639 [ blob = UNPARSED_AST ->
640 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
641 (CicNotationParser.parse_level2_ast
642 (Ulexing.from_utf8_string blob))
643 | blob = UNPARSED_META ->
644 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
645 (CicNotationParser.parse_level2_meta
646 (Ulexing.from_utf8_string blob))
650 | None -> default_associativity
651 | Some assoc -> assoc
654 add_raw_attribute ~text:s
655 (CicNotationParser.parse_level1_pattern prec
656 (Ulexing.from_utf8_string s))
658 (dir, p1, assoc, prec, p2)
662 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
663 | id = IDENT -> Ast.VarPattern id
664 | SYMBOL "_" -> Ast.ImplicitPattern
665 | LPAREN; terms = LIST1 SELF; RPAREN ->
669 | terms -> Ast.ApplPattern terms)
673 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
679 IDENT "include" ; path = QSTRING ->
680 loc,path,LexiconAst.WithPreferences
681 | IDENT "include'" ; path = QSTRING ->
682 loc,path,LexiconAst.WithoutPreferences
686 IDENT "set"; n = QSTRING; v = QSTRING ->
687 GrafiteAst.Set (loc, n, v)
688 | IDENT "drop" -> GrafiteAst.Drop loc
689 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
690 | IDENT "qed" -> GrafiteAst.Qed loc
691 | IDENT "variant" ; name = IDENT; SYMBOL ":";
692 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
695 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
696 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
697 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
698 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
699 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
700 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
701 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
702 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
705 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
706 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
707 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
708 | LETCOREC ; defs = let_defs ->
709 mk_rec_corec `CoInductive defs loc
710 | LETREC ; defs = let_defs ->
711 mk_rec_corec `Inductive defs loc
712 | IDENT "inductive"; spec = inductive_spec ->
713 let (params, ind_types) = spec in
714 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
715 | IDENT "coinductive"; spec = inductive_spec ->
716 let (params, ind_types) = spec in
717 let ind_types = (* set inductive flags to false (coinductive) *)
718 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
721 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
723 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
724 arity = OPT int ; saturations = OPT int;
725 composites = OPT (IDENT "nocomposites") ->
726 let arity = match arity with None -> 0 | Some x -> x in
727 let saturations = match saturations with None -> 0 | Some x -> x in
728 let composites = match composites with None -> true | Some _ -> false in
730 (loc, t, composites, arity, saturations)
731 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
732 GrafiteAst.PreferCoercion (loc, t)
733 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
734 GrafiteAst.UnificationHint (loc, t, n)
735 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
736 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
737 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
738 let uris = List.map UriManager.uri_of_string uris in
739 GrafiteAst.Default (loc,what,uris)
740 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
741 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
742 refl = tactic_term -> refl ] ;
743 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
744 sym = tactic_term -> sym ] ;
745 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
746 trans = tactic_term -> trans ] ;
748 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
751 IDENT "alias" ; spec = alias_spec ->
752 LexiconAst.Alias (loc, spec)
753 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
754 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
755 | IDENT "interpretation"; id = QSTRING;
756 (symbol, args, l3) = interpretation ->
757 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
760 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
761 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
762 GrafiteAst.Tactic (loc, Some tac, punct)
763 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
764 | tac = ntactic; punct = punctuation_tactical ->
765 GrafiteAst.NTactic (loc, tac, punct)
766 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
767 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
768 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
769 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
770 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
774 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
775 GrafiteAst.Code (loc, ex)
777 GrafiteAst.Note (loc, str)
782 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
784 fun ?(never_include=false) ~include_paths status ->
785 status,LSome (GrafiteAst.Comment (loc, com))
786 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
788 fun ?(never_include=false) ~include_paths status ->
789 let _root, buri, fullpath, _rrelpath =
790 Librarian.baseuri_of_script ~include_paths fname
793 if never_include then raise (NoInclusionPerformed fullpath)
794 else LexiconEngine.eval_command status
795 (LexiconAst.Include (iloc,buri,mode,fullpath))
799 (GrafiteAst.Executable
800 (loc,GrafiteAst.Command
801 (loc,GrafiteAst.Include (iloc,buri))))
802 | scom = lexicon_command ; SYMBOL "." ->
803 fun ?(never_include=false) ~include_paths status ->
804 let status = LexiconEngine.eval_command status scom in
806 | EOI -> raise End_of_file
813 let _ = initialize_parser () ;;
815 let exc_located_wrapper f =
819 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
820 | Stdpp.Exc_located (floc, Stream.Error msg) ->
821 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
822 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
824 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
825 | Stdpp.Exc_located (floc, exn) ->
827 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
829 let parse_statement lexbuf =
831 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
833 let statement () = !grafite_parser.statement
835 let history = ref [] ;;
839 history := !grafite_parser :: !history;
840 grafite_parser := initial_parser ();
849 grafite_parser := gp;
853 (* vim:set foldmethod=marker: *)