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
165 inverter_param_list: [
166 [ params = tactic_term ->
167 let deannotate = function
168 | Ast.AttributedTerm (_,t) | t -> t
169 in match deannotate params with
170 | Ast.Implicit -> [false]
171 | Ast.UserInput -> [true]
173 List.map (fun x -> match deannotate x with
174 | Ast.Implicit -> false
175 | Ast.UserInput -> true
176 | _ -> raise (Invalid_argument "malformed target parameter list 1")) l
177 | _ -> raise (Invalid_argument ("malformed target parameter list 2\n" ^ CicNotationPp.pp_term params)) ]
180 [ SYMBOL ">" -> `LeftToRight
181 | SYMBOL "<" -> `RightToLeft ]
183 int: [ [ num = NUMBER -> int_of_string num ] ];
185 [ idents = OPT ident_list0 ->
186 match idents with None -> [] | Some idents -> idents
190 [ OPT [ IDENT "names" ];
191 num = OPT [ num = int -> num ];
192 idents = intros_names ->
196 using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
198 [ IDENT "napply"; t = tactic_term -> GrafiteAst.NApply (loc, t)
202 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
203 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
204 SYMBOL <:unicode<def>> ; bo = tactic_term ->
206 SYMBOL <:unicode<vdash>>;
207 concl = tactic_term -> (List.rev hyps,concl) ] ->
208 GrafiteAst.NAssert (loc, seqs)
209 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
210 GrafiteAst.NCases (loc, what, where)
211 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
212 GrafiteAst.NChange (loc, what, with_what)
213 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
214 GrafiteAst.NElim (loc, what, where)
215 | IDENT "ngeneralize"; p=pattern_spec ->
216 GrafiteAst.NGeneralize (loc, p)
217 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
218 where = pattern_spec ->
219 GrafiteAst.NLetIn (loc,where,t,name)
220 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
221 GrafiteAst.NRewrite (loc, dir, what, where)
222 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
223 where = pattern_spec ->
224 let delta = match delta with None -> true | _ -> false in
225 GrafiteAst.NEval (loc, where, `Whd delta)
226 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
227 | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
228 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
229 | SYMBOL "*"; n=IDENT ->
230 GrafiteAst.NCase1 (loc,n)
234 [ IDENT "absurd"; t = tactic_term ->
235 GrafiteAst.Absurd (loc, t)
236 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
237 GrafiteAst.ApplyRule (loc, t)
238 | IDENT "apply"; t = tactic_term ->
239 GrafiteAst.Apply (loc, t)
240 | IDENT "applyP"; t = tactic_term ->
241 GrafiteAst.ApplyP (loc, t)
242 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
243 GrafiteAst.ApplyS (loc, t, params)
244 | IDENT "assumption" ->
245 GrafiteAst.Assumption loc
246 | IDENT "autobatch"; params = auto_params ->
247 GrafiteAst.AutoBatch (loc,params)
248 | IDENT "cases"; what = tactic_term;
249 pattern = OPT pattern_spec;
250 specs = intros_spec ->
251 let pattern = match pattern with
252 | None -> None, [], Some Ast.UserInput
253 | Some pattern -> pattern
255 GrafiteAst.Cases (loc, what, pattern, specs)
256 | IDENT "clear"; ids = LIST1 IDENT ->
257 GrafiteAst.Clear (loc, ids)
258 | IDENT "clearbody"; id = IDENT ->
259 GrafiteAst.ClearBody (loc,id)
260 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
261 GrafiteAst.Change (loc, what, t)
262 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
263 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
264 let times = match times with None -> 1 | Some i -> i in
265 GrafiteAst.Compose (loc, t1, t2, times, specs)
266 | IDENT "constructor"; n = int ->
267 GrafiteAst.Constructor (loc, n)
268 | IDENT "contradiction" ->
269 GrafiteAst.Contradiction loc
270 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
271 GrafiteAst.Cut (loc, ident, t)
272 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
273 let idents = match idents with None -> [] | Some idents -> idents in
274 GrafiteAst.Decompose (loc, idents)
275 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
276 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
277 GrafiteAst.Destruct (loc, xts)
278 | IDENT "elim"; what = tactic_term; using = using;
279 pattern = OPT pattern_spec;
280 ispecs = intros_spec ->
281 let pattern = match pattern with
282 | None -> None, [], Some Ast.UserInput
283 | Some pattern -> pattern
285 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
286 | IDENT "elimType"; what = tactic_term; using = using;
287 (num, idents) = intros_spec ->
288 GrafiteAst.ElimType (loc, what, using, (num, idents))
289 | IDENT "exact"; t = tactic_term ->
290 GrafiteAst.Exact (loc, t)
292 GrafiteAst.Exists loc
293 | IDENT "fail" -> GrafiteAst.Fail loc
294 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
297 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
298 ("the pattern cannot specify the term to replace, only its"
299 ^ " paths in the hypotheses and in the conclusion")))
301 GrafiteAst.Fold (loc, kind, t, p)
303 GrafiteAst.Fourier loc
304 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
305 let idents = match idents with None -> [] | Some idents -> idents in
306 GrafiteAst.FwdSimpl (loc, hyp, idents)
307 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
308 GrafiteAst.Generalize (loc,p,id)
309 | IDENT "id" -> GrafiteAst.IdTac loc
310 | IDENT "intro"; ident = OPT IDENT ->
311 let idents = match ident with None -> [] | Some id -> [Some id] in
312 GrafiteAst.Intros (loc, (Some 1, idents))
313 | IDENT "intros"; specs = intros_spec ->
314 GrafiteAst.Intros (loc, specs)
315 | IDENT "inversion"; t = tactic_term ->
316 GrafiteAst.Inversion (loc, t)
318 linear = OPT [ IDENT "linear" ];
319 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
321 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
322 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
323 let linear = match linear with None -> false | Some _ -> true in
324 let to_what = match to_what with None -> [] | Some to_what -> to_what in
325 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
326 | IDENT "left" -> GrafiteAst.Left loc
327 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
328 GrafiteAst.LetIn (loc, t, where)
329 | kind = reduction_kind; p = pattern_spec ->
330 GrafiteAst.Reduce (loc, kind, p)
331 | IDENT "reflexivity" ->
332 GrafiteAst.Reflexivity loc
333 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
334 GrafiteAst.Replace (loc, p, t)
335 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
336 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
340 (HExtlib.Localized (loc,
341 (CicNotationParser.Parse_error
342 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
344 let n = match xnames with None -> [] | Some names -> names in
345 GrafiteAst.Rewrite (loc, d, t, p, n)
352 | IDENT "symmetry" ->
353 GrafiteAst.Symmetry loc
354 | IDENT "transitivity"; t = tactic_term ->
355 GrafiteAst.Transitivity (loc, t)
356 (* Produzioni Aggiunte *)
357 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
358 GrafiteAst.Assume (loc, id, t)
359 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
360 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
361 t' = tactic_term -> t']->
362 GrafiteAst.Suppose (loc, t, id, t1)
363 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
364 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
365 id2 = IDENT ; RPAREN ->
366 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
368 [ IDENT "using"; t=tactic_term -> `Term t
369 | params = auto_params -> `Auto params] ;
370 cont=by_continuation ->
372 BYC_done -> GrafiteAst.Bydone (loc, just)
373 | BYC_weproved (ty,id,t1) ->
374 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
375 | BYC_letsuchthat (id1,t1,id2,t2) ->
376 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
377 | BYC_wehaveand (id1,t1,id2,t2) ->
378 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
379 | 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']->
380 GrafiteAst.We_need_to_prove (loc, t, id, t1)
381 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
382 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
383 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
384 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
385 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
386 GrafiteAst.Byinduction(loc, t, id)
387 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
388 GrafiteAst.Thesisbecomes(loc, t)
389 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
390 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
391 GrafiteAst.Case(loc,id,params)
392 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
394 termine = tactic_term;
398 [ IDENT "using"; t=tactic_term -> `Term t
399 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
400 | IDENT "proof" -> `Proof
401 | params = auto_params -> `Auto params];
402 cont = rewriting_step_continuation ->
403 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
404 | IDENT "obtain" ; name = IDENT;
405 termine = tactic_term;
409 [ IDENT "using"; t=tactic_term -> `Term t
410 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
411 | IDENT "proof" -> `Proof
412 | params = auto_params -> `Auto params];
413 cont = rewriting_step_continuation ->
414 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
418 [ IDENT "using"; t=tactic_term -> `Term t
419 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
420 | IDENT "proof" -> `Proof
421 | params = auto_params -> `Auto params];
422 cont = rewriting_step_continuation ->
423 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
427 [ IDENT "paramodulation"
441 i = auto_fixed_param -> i,""
442 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
443 string_of_int v | v = IDENT -> v ] -> i,v ];
444 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
445 (match tl with Some l -> l | None -> []),
450 [ 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)
451 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
452 "done" -> BYC_weproved (ty,None,t1)
454 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
455 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
456 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
457 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
458 BYC_wehaveand (id1,t1,id2,t2)
461 rewriting_step_continuation : [
468 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
471 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
474 GrafiteAst.Seq (loc, ts)
477 [ tac = SELF; SYMBOL ";";
478 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
479 (GrafiteAst.Then (loc, tac, tacs))
482 [ IDENT "do"; count = int; tac = SELF ->
483 GrafiteAst.Do (loc, count, tac)
484 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
488 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
489 GrafiteAst.First (loc, tacs)
490 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
492 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
493 GrafiteAst.Solve (loc, tacs)
494 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
495 | LPAREN; tac = SELF; RPAREN -> tac
496 | tac = tactic -> tac
499 punctuation_tactical:
501 [ SYMBOL "[" -> GrafiteAst.Branch loc
502 | SYMBOL "|" -> GrafiteAst.Shift loc
503 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
504 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
505 | SYMBOL "]" -> GrafiteAst.Merge loc
506 | SYMBOL ";" -> GrafiteAst.Semicolon loc
507 | SYMBOL "." -> GrafiteAst.Dot loc
510 non_punctuation_tactical:
512 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
513 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
514 | IDENT "skip" -> GrafiteAst.Skip loc
518 [ [ IDENT "ntheorem" ] -> `Theorem
522 [ [ IDENT "definition" ] -> `Definition
523 | [ IDENT "fact" ] -> `Fact
524 | [ IDENT "lemma" ] -> `Lemma
525 | [ IDENT "remark" ] -> `Remark
526 | [ IDENT "theorem" ] -> `Theorem
530 [ attr = theorem_flavour -> attr
531 | [ IDENT "axiom" ] -> `Axiom
532 | [ IDENT "mutual" ] -> `MutualDefinition
537 params = LIST0 protected_binder_vars;
538 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
539 fst_constructors = LIST0 constructor SEP SYMBOL "|";
542 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
543 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
544 (name, true, typ, constructors) ] SEP "with" -> types
548 (fun (names, typ) acc ->
549 (List.map (fun name -> (name, typ)) names) @ acc)
552 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
553 let tl_ind_types = match tl with None -> [] | Some types -> types in
554 let ind_types = fst_ind_type :: tl_ind_types in
560 params = LIST0 protected_binder_vars;
561 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
565 SYMBOL ":" -> false,0
566 | SYMBOL ":"; SYMBOL ">" -> true,0
567 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
570 let b,n = coercion in
572 ] SEP SYMBOL ";"; SYMBOL "}" ->
575 (fun (names, typ) acc ->
576 (List.map (fun name -> (name, typ)) names) @ acc)
579 (params,name,typ,fields)
583 [ [ IDENT "check" ]; t = term ->
584 GrafiteAst.Check (loc, t)
585 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
586 GrafiteAst.Eval (loc, kind, t)
588 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
589 suri = QSTRING; prefix = OPT QSTRING;
590 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
591 let style = match style with
592 | None -> GrafiteAst.Declarative
593 | Some depth -> GrafiteAst.Procedural depth
595 let prefix = match prefix with None -> "" | Some prefix -> prefix in
596 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
597 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
598 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
599 | IDENT "auto"; params = auto_params ->
600 GrafiteAst.AutoInteractive (loc,params)
601 | [ IDENT "whelp"; "match" ] ; t = term ->
602 GrafiteAst.WMatch (loc,t)
603 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
604 GrafiteAst.WInstance (loc,t)
605 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
606 GrafiteAst.WLocate (loc,id)
607 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
608 GrafiteAst.WElim (loc, t)
609 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
610 GrafiteAst.WHint (loc,t)
614 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
615 let alpha = "[a-zA-Z]" in
616 let num = "[0-9]+" in
617 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
618 let decoration = "\\'" in
619 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
620 let rex = Str.regexp ("^"^ident^"$") in
621 if Str.string_match rex id 0 then
622 if (try ignore (UriManager.uri_of_string uri); true
623 with UriManager.IllFormedUri _ -> false)
625 LexiconAst.Ident_alias (id, uri)
628 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
630 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
631 Printf.sprintf "Not a valid identifier: %s" id)))
632 | IDENT "symbol"; symbol = QSTRING;
633 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
634 SYMBOL "="; dsc = QSTRING ->
636 match instance with Some i -> i | None -> 0
638 LexiconAst.Symbol_alias (symbol, instance, dsc)
640 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
641 SYMBOL "="; dsc = QSTRING ->
643 match instance with Some i -> i | None -> 0
645 LexiconAst.Number_alias (instance, dsc)
649 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
651 Ast.IdentArg (List.length l, id)
655 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
656 | IDENT "right"; IDENT "associative" -> Gramext.RightA
657 | IDENT "non"; IDENT "associative" -> Gramext.NonA
661 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
664 [ dir = OPT direction; s = QSTRING;
665 assoc = OPT associativity; prec = precedence;
668 [ blob = UNPARSED_AST ->
669 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
670 (CicNotationParser.parse_level2_ast
671 (Ulexing.from_utf8_string blob))
672 | blob = UNPARSED_META ->
673 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
674 (CicNotationParser.parse_level2_meta
675 (Ulexing.from_utf8_string blob))
679 | None -> default_associativity
680 | Some assoc -> assoc
683 add_raw_attribute ~text:s
684 (CicNotationParser.parse_level1_pattern prec
685 (Ulexing.from_utf8_string s))
687 (dir, p1, assoc, prec, p2)
691 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
692 | id = IDENT -> Ast.VarPattern id
693 | SYMBOL "_" -> Ast.ImplicitPattern
694 | LPAREN; terms = LIST1 SELF; RPAREN ->
698 | terms -> Ast.ApplPattern terms)
702 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
708 IDENT "include" ; path = QSTRING ->
709 loc,path,LexiconAst.WithPreferences
710 | IDENT "include'" ; path = QSTRING ->
711 loc,path,LexiconAst.WithoutPreferences
715 IDENT "set"; n = QSTRING; v = QSTRING ->
716 GrafiteAst.Set (loc, n, v)
717 | IDENT "drop" -> GrafiteAst.Drop loc
718 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
719 | IDENT "qed" -> GrafiteAst.Qed loc
720 | IDENT "nqed" -> GrafiteAst.NQed loc
721 | IDENT "variant" ; name = IDENT; SYMBOL ":";
722 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
725 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
726 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
727 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
728 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
729 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
730 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
731 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
732 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
735 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
736 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
737 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
738 | LETCOREC ; defs = let_defs ->
739 mk_rec_corec `CoInductive defs loc
740 | LETREC ; defs = let_defs ->
741 mk_rec_corec `Inductive defs loc
742 | IDENT "inductive"; spec = inductive_spec ->
743 let (params, ind_types) = spec in
744 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
745 | IDENT "coinductive"; spec = inductive_spec ->
746 let (params, ind_types) = spec in
747 let ind_types = (* set inductive flags to false (coinductive) *)
748 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
751 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
753 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
754 arity = OPT int ; saturations = OPT int;
755 composites = OPT (IDENT "nocomposites") ->
756 let arity = match arity with None -> 0 | Some x -> x in
757 let saturations = match saturations with None -> 0 | Some x -> x in
758 let composites = match composites with None -> true | Some _ -> false in
760 (loc, t, composites, arity, saturations)
761 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
762 GrafiteAst.PreferCoercion (loc, t)
763 | IDENT "pump" ; steps = int ->
764 GrafiteAst.Pump(loc,steps)
765 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
766 GrafiteAst.UnificationHint (loc, t, n)
767 | IDENT "inverter"; name = IDENT; IDENT "for";
768 indty = tactic_term; paramspec = inverter_param_list ->
770 (loc, name, indty, paramspec)
771 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
772 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
773 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
774 let uris = List.map UriManager.uri_of_string uris in
775 GrafiteAst.Default (loc,what,uris)
776 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
777 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
778 refl = tactic_term -> refl ] ;
779 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
780 sym = tactic_term -> sym ] ;
781 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
782 trans = tactic_term -> trans ] ;
784 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
787 IDENT "alias" ; spec = alias_spec ->
788 LexiconAst.Alias (loc, spec)
789 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
790 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
791 | IDENT "interpretation"; id = QSTRING;
792 (symbol, args, l3) = interpretation ->
793 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
796 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
797 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
798 GrafiteAst.Tactic (loc, Some tac, punct)
799 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
800 | tac = ntactic; punct = punctuation_tactical ->
801 GrafiteAst.NTactic (loc, tac, punct)
802 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
803 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
804 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
805 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
806 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
810 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
811 GrafiteAst.Code (loc, ex)
813 GrafiteAst.Note (loc, str)
818 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
820 fun ?(never_include=false) ~include_paths status ->
821 status,LSome (GrafiteAst.Comment (loc, com))
822 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
824 fun ?(never_include=false) ~include_paths status ->
825 let _root, buri, fullpath, _rrelpath =
826 Librarian.baseuri_of_script ~include_paths fname
829 if never_include then raise (NoInclusionPerformed fullpath)
830 else LexiconEngine.eval_command status
831 (LexiconAst.Include (iloc,buri,mode,fullpath))
835 (GrafiteAst.Executable
836 (loc,GrafiteAst.Command
837 (loc,GrafiteAst.Include (iloc,buri))))
838 | scom = lexicon_command ; SYMBOL "." ->
839 fun ?(never_include=false) ~include_paths status ->
840 let status = LexiconEngine.eval_command status scom in
842 | EOI -> raise End_of_file
849 let _ = initialize_parser () ;;
851 let exc_located_wrapper f =
855 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
856 | Stdpp.Exc_located (floc, Stream.Error msg) ->
857 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
858 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
860 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
861 | Stdpp.Exc_located (floc, exn) ->
863 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
865 let parse_statement lexbuf =
867 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
869 let statement () = !grafite_parser.statement
871 let history = ref [] ;;
875 history := !grafite_parser :: !history;
876 grafite_parser := initial_parser ();
885 grafite_parser := gp;
889 (* vim:set foldmethod=marker: *)