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)
187 [ id = IDENT ; SYMBOL ":" ; ty = tactic_term -> id,`Decl ty
188 | id = IDENT ; SYMBOL ":" ; ty = tactic_term ;
189 SYMBOL <:unicode<def>> ; bo = tactic_term ->
191 SYMBOL <:unicode<vdash>>;
192 concl = tactic_term ->
193 GrafiteAst.NAssert (loc, hyps, concl)
194 | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
195 GrafiteAst.NCases (loc, what, where)
196 | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
197 GrafiteAst.NChange (loc, what, with_what)
198 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
199 GrafiteAst.NElim (loc, what, where)
200 | IDENT "ngeneralize"; p=pattern_spec ->
201 GrafiteAst.NGeneralize (loc, p)
202 | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
203 where = pattern_spec ->
204 GrafiteAst.NLetIn (loc,where,t,name)
205 | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
206 GrafiteAst.NRewrite (loc, dir, what, where)
207 | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
208 where = pattern_spec ->
209 let delta = match delta with None -> true | _ -> false in
210 GrafiteAst.NEval (loc, where, `Whd delta)
211 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
212 | SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
213 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
214 | SYMBOL "*"; n=IDENT ->
215 GrafiteAst.NCase1 (loc,n)
219 [ IDENT "absurd"; t = tactic_term ->
220 GrafiteAst.Absurd (loc, t)
221 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
222 GrafiteAst.ApplyRule (loc, t)
223 | IDENT "apply"; t = tactic_term ->
224 GrafiteAst.Apply (loc, t)
225 | IDENT "applyP"; t = tactic_term ->
226 GrafiteAst.ApplyP (loc, t)
227 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
228 GrafiteAst.ApplyS (loc, t, params)
229 | IDENT "assumption" ->
230 GrafiteAst.Assumption loc
231 | IDENT "autobatch"; params = auto_params ->
232 GrafiteAst.AutoBatch (loc,params)
233 | IDENT "cases"; what = tactic_term;
234 pattern = OPT pattern_spec;
235 specs = intros_spec ->
236 let pattern = match pattern with
237 | None -> None, [], Some Ast.UserInput
238 | Some pattern -> pattern
240 GrafiteAst.Cases (loc, what, pattern, specs)
241 | IDENT "clear"; ids = LIST1 IDENT ->
242 GrafiteAst.Clear (loc, ids)
243 | IDENT "clearbody"; id = IDENT ->
244 GrafiteAst.ClearBody (loc,id)
245 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
246 GrafiteAst.Change (loc, what, t)
247 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
248 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
249 let times = match times with None -> 1 | Some i -> i in
250 GrafiteAst.Compose (loc, t1, t2, times, specs)
251 | IDENT "constructor"; n = int ->
252 GrafiteAst.Constructor (loc, n)
253 | IDENT "contradiction" ->
254 GrafiteAst.Contradiction loc
255 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
256 GrafiteAst.Cut (loc, ident, t)
257 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
258 let idents = match idents with None -> [] | Some idents -> idents in
259 GrafiteAst.Decompose (loc, idents)
260 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
261 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
262 GrafiteAst.Destruct (loc, xts)
263 | IDENT "elim"; what = tactic_term; using = using;
264 pattern = OPT pattern_spec;
265 ispecs = intros_spec ->
266 let pattern = match pattern with
267 | None -> None, [], Some Ast.UserInput
268 | Some pattern -> pattern
270 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
271 | IDENT "elimType"; what = tactic_term; using = using;
272 (num, idents) = intros_spec ->
273 GrafiteAst.ElimType (loc, what, using, (num, idents))
274 | IDENT "exact"; t = tactic_term ->
275 GrafiteAst.Exact (loc, t)
277 GrafiteAst.Exists loc
278 | IDENT "fail" -> GrafiteAst.Fail loc
279 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
282 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
283 ("the pattern cannot specify the term to replace, only its"
284 ^ " paths in the hypotheses and in the conclusion")))
286 GrafiteAst.Fold (loc, kind, t, p)
288 GrafiteAst.Fourier loc
289 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
290 let idents = match idents with None -> [] | Some idents -> idents in
291 GrafiteAst.FwdSimpl (loc, hyp, idents)
292 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
293 GrafiteAst.Generalize (loc,p,id)
294 | IDENT "id" -> GrafiteAst.IdTac loc
295 | IDENT "intro"; ident = OPT IDENT ->
296 let idents = match ident with None -> [] | Some id -> [Some id] in
297 GrafiteAst.Intros (loc, (Some 1, idents))
298 | IDENT "intros"; specs = intros_spec ->
299 GrafiteAst.Intros (loc, specs)
300 | IDENT "inversion"; t = tactic_term ->
301 GrafiteAst.Inversion (loc, t)
303 linear = OPT [ IDENT "linear" ];
304 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
306 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
307 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
308 let linear = match linear with None -> false | Some _ -> true in
309 let to_what = match to_what with None -> [] | Some to_what -> to_what in
310 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
311 | IDENT "left" -> GrafiteAst.Left loc
312 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
313 GrafiteAst.LetIn (loc, t, where)
314 | kind = reduction_kind; p = pattern_spec ->
315 GrafiteAst.Reduce (loc, kind, p)
316 | IDENT "reflexivity" ->
317 GrafiteAst.Reflexivity loc
318 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
319 GrafiteAst.Replace (loc, p, t)
320 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
321 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
325 (HExtlib.Localized (loc,
326 (CicNotationParser.Parse_error
327 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
329 let n = match xnames with None -> [] | Some names -> names in
330 GrafiteAst.Rewrite (loc, d, t, p, n)
337 | IDENT "symmetry" ->
338 GrafiteAst.Symmetry loc
339 | IDENT "transitivity"; t = tactic_term ->
340 GrafiteAst.Transitivity (loc, t)
341 (* Produzioni Aggiunte *)
342 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
343 GrafiteAst.Assume (loc, id, t)
344 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
345 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
346 t' = tactic_term -> t']->
347 GrafiteAst.Suppose (loc, t, id, t1)
348 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
349 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
350 id2 = IDENT ; RPAREN ->
351 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
353 [ IDENT "using"; t=tactic_term -> `Term t
354 | params = auto_params -> `Auto params] ;
355 cont=by_continuation ->
357 BYC_done -> GrafiteAst.Bydone (loc, just)
358 | BYC_weproved (ty,id,t1) ->
359 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
360 | BYC_letsuchthat (id1,t1,id2,t2) ->
361 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
362 | BYC_wehaveand (id1,t1,id2,t2) ->
363 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
364 | 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']->
365 GrafiteAst.We_need_to_prove (loc, t, id, t1)
366 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
367 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
368 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
369 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
370 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
371 GrafiteAst.Byinduction(loc, t, id)
372 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
373 GrafiteAst.Thesisbecomes(loc, t)
374 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
375 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
376 GrafiteAst.Case(loc,id,params)
377 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
379 termine = tactic_term;
383 [ IDENT "using"; t=tactic_term -> `Term t
384 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
385 | IDENT "proof" -> `Proof
386 | params = auto_params -> `Auto params];
387 cont = rewriting_step_continuation ->
388 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
389 | IDENT "obtain" ; name = IDENT;
390 termine = tactic_term;
394 [ IDENT "using"; t=tactic_term -> `Term t
395 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
396 | IDENT "proof" -> `Proof
397 | params = auto_params -> `Auto params];
398 cont = rewriting_step_continuation ->
399 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
403 [ IDENT "using"; t=tactic_term -> `Term t
404 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
405 | IDENT "proof" -> `Proof
406 | params = auto_params -> `Auto params];
407 cont = rewriting_step_continuation ->
408 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
412 [ IDENT "paramodulation"
424 i = auto_fixed_param -> i,""
425 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
426 string_of_int v | v = IDENT -> v ] -> i,v ];
427 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
428 (match tl with Some l -> l | None -> []),
433 [ 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)
434 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
435 "done" -> BYC_weproved (ty,None,t1)
437 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
438 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
439 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
440 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
441 BYC_wehaveand (id1,t1,id2,t2)
444 rewriting_step_continuation : [
451 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
454 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
457 GrafiteAst.Seq (loc, ts)
460 [ tac = SELF; SYMBOL ";";
461 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
462 (GrafiteAst.Then (loc, tac, tacs))
465 [ IDENT "do"; count = int; tac = SELF ->
466 GrafiteAst.Do (loc, count, tac)
467 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
471 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
472 GrafiteAst.First (loc, tacs)
473 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
475 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
476 GrafiteAst.Solve (loc, tacs)
477 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
478 | LPAREN; tac = SELF; RPAREN -> tac
479 | tac = tactic -> tac
482 punctuation_tactical:
484 [ SYMBOL "[" -> GrafiteAst.Branch loc
485 | SYMBOL "|" -> GrafiteAst.Shift loc
486 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
487 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
488 | SYMBOL "]" -> GrafiteAst.Merge loc
489 | SYMBOL ";" -> GrafiteAst.Semicolon loc
490 | SYMBOL "." -> GrafiteAst.Dot loc
493 non_punctuation_tactical:
495 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
496 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
497 | IDENT "skip" -> GrafiteAst.Skip loc
501 [ [ IDENT "ntheorem" ] -> `Theorem
505 [ [ IDENT "definition" ] -> `Definition
506 | [ IDENT "fact" ] -> `Fact
507 | [ IDENT "lemma" ] -> `Lemma
508 | [ IDENT "remark" ] -> `Remark
509 | [ IDENT "theorem" ] -> `Theorem
513 [ attr = theorem_flavour -> attr
514 | [ IDENT "axiom" ] -> `Axiom
515 | [ IDENT "mutual" ] -> `MutualDefinition
520 params = LIST0 protected_binder_vars;
521 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
522 fst_constructors = LIST0 constructor SEP SYMBOL "|";
525 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
526 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
527 (name, true, typ, constructors) ] SEP "with" -> types
531 (fun (names, typ) acc ->
532 (List.map (fun name -> (name, typ)) names) @ acc)
535 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
536 let tl_ind_types = match tl with None -> [] | Some types -> types in
537 let ind_types = fst_ind_type :: tl_ind_types in
543 params = LIST0 protected_binder_vars;
544 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
548 SYMBOL ":" -> false,0
549 | SYMBOL ":"; SYMBOL ">" -> true,0
550 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
553 let b,n = coercion in
555 ] SEP SYMBOL ";"; SYMBOL "}" ->
558 (fun (names, typ) acc ->
559 (List.map (fun name -> (name, typ)) names) @ acc)
562 (params,name,typ,fields)
566 [ [ IDENT "check" ]; t = term ->
567 GrafiteAst.Check (loc, t)
568 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
569 GrafiteAst.Eval (loc, kind, t)
571 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
572 suri = QSTRING; prefix = OPT QSTRING;
573 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
574 let style = match style with
575 | None -> GrafiteAst.Declarative
576 | Some depth -> GrafiteAst.Procedural depth
578 let prefix = match prefix with None -> "" | Some prefix -> prefix in
579 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
580 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
581 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
582 | IDENT "auto"; params = auto_params ->
583 GrafiteAst.AutoInteractive (loc,params)
584 | [ IDENT "whelp"; "match" ] ; t = term ->
585 GrafiteAst.WMatch (loc,t)
586 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
587 GrafiteAst.WInstance (loc,t)
588 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
589 GrafiteAst.WLocate (loc,id)
590 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
591 GrafiteAst.WElim (loc, t)
592 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
593 GrafiteAst.WHint (loc,t)
597 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
598 let alpha = "[a-zA-Z]" in
599 let num = "[0-9]+" in
600 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
601 let decoration = "\\'" in
602 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
603 let rex = Str.regexp ("^"^ident^"$") in
604 if Str.string_match rex id 0 then
605 if (try ignore (UriManager.uri_of_string uri); true
606 with UriManager.IllFormedUri _ -> false)
608 LexiconAst.Ident_alias (id, uri)
611 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
613 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
614 Printf.sprintf "Not a valid identifier: %s" id)))
615 | IDENT "symbol"; symbol = QSTRING;
616 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
617 SYMBOL "="; dsc = QSTRING ->
619 match instance with Some i -> i | None -> 0
621 LexiconAst.Symbol_alias (symbol, instance, dsc)
623 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
624 SYMBOL "="; dsc = QSTRING ->
626 match instance with Some i -> i | None -> 0
628 LexiconAst.Number_alias (instance, dsc)
632 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
634 Ast.IdentArg (List.length l, id)
638 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
639 | IDENT "right"; IDENT "associative" -> Gramext.RightA
640 | IDENT "non"; IDENT "associative" -> Gramext.NonA
644 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
647 [ dir = OPT direction; s = QSTRING;
648 assoc = OPT associativity; prec = precedence;
651 [ blob = UNPARSED_AST ->
652 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
653 (CicNotationParser.parse_level2_ast
654 (Ulexing.from_utf8_string blob))
655 | blob = UNPARSED_META ->
656 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
657 (CicNotationParser.parse_level2_meta
658 (Ulexing.from_utf8_string blob))
662 | None -> default_associativity
663 | Some assoc -> assoc
666 add_raw_attribute ~text:s
667 (CicNotationParser.parse_level1_pattern prec
668 (Ulexing.from_utf8_string s))
670 (dir, p1, assoc, prec, p2)
674 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
675 | id = IDENT -> Ast.VarPattern id
676 | SYMBOL "_" -> Ast.ImplicitPattern
677 | LPAREN; terms = LIST1 SELF; RPAREN ->
681 | terms -> Ast.ApplPattern terms)
685 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
691 IDENT "include" ; path = QSTRING ->
692 loc,path,LexiconAst.WithPreferences
693 | IDENT "include'" ; path = QSTRING ->
694 loc,path,LexiconAst.WithoutPreferences
698 IDENT "set"; n = QSTRING; v = QSTRING ->
699 GrafiteAst.Set (loc, n, v)
700 | IDENT "drop" -> GrafiteAst.Drop loc
701 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
702 | IDENT "qed" -> GrafiteAst.Qed loc
703 | IDENT "variant" ; name = IDENT; SYMBOL ":";
704 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
707 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
708 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
709 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
710 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
711 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
712 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
713 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
714 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
717 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
718 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
719 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
720 | LETCOREC ; defs = let_defs ->
721 mk_rec_corec `CoInductive defs loc
722 | LETREC ; defs = let_defs ->
723 mk_rec_corec `Inductive defs loc
724 | IDENT "inductive"; spec = inductive_spec ->
725 let (params, ind_types) = spec in
726 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
727 | IDENT "coinductive"; spec = inductive_spec ->
728 let (params, ind_types) = spec in
729 let ind_types = (* set inductive flags to false (coinductive) *)
730 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
733 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
735 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
736 arity = OPT int ; saturations = OPT int;
737 composites = OPT (IDENT "nocomposites") ->
738 let arity = match arity with None -> 0 | Some x -> x in
739 let saturations = match saturations with None -> 0 | Some x -> x in
740 let composites = match composites with None -> true | Some _ -> false in
742 (loc, t, composites, arity, saturations)
743 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
744 GrafiteAst.PreferCoercion (loc, t)
745 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
746 GrafiteAst.UnificationHint (loc, t, n)
747 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
748 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
749 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
750 let uris = List.map UriManager.uri_of_string uris in
751 GrafiteAst.Default (loc,what,uris)
752 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
753 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
754 refl = tactic_term -> refl ] ;
755 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
756 sym = tactic_term -> sym ] ;
757 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
758 trans = tactic_term -> trans ] ;
760 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
763 IDENT "alias" ; spec = alias_spec ->
764 LexiconAst.Alias (loc, spec)
765 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
766 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
767 | IDENT "interpretation"; id = QSTRING;
768 (symbol, args, l3) = interpretation ->
769 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
772 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
773 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
774 GrafiteAst.Tactic (loc, Some tac, punct)
775 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
776 | tac = ntactic; punct = punctuation_tactical ->
777 GrafiteAst.NTactic (loc, tac, punct)
778 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
779 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
780 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
781 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
782 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
786 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
787 GrafiteAst.Code (loc, ex)
789 GrafiteAst.Note (loc, str)
794 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
796 fun ?(never_include=false) ~include_paths status ->
797 status,LSome (GrafiteAst.Comment (loc, com))
798 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
800 fun ?(never_include=false) ~include_paths status ->
801 let _root, buri, fullpath, _rrelpath =
802 Librarian.baseuri_of_script ~include_paths fname
805 if never_include then raise (NoInclusionPerformed fullpath)
806 else LexiconEngine.eval_command status
807 (LexiconAst.Include (iloc,buri,mode,fullpath))
811 (GrafiteAst.Executable
812 (loc,GrafiteAst.Command
813 (loc,GrafiteAst.Include (iloc,buri))))
814 | scom = lexicon_command ; SYMBOL "." ->
815 fun ?(never_include=false) ~include_paths status ->
816 let status = LexiconEngine.eval_command status scom in
818 | EOI -> raise End_of_file
825 let _ = initialize_parser () ;;
827 let exc_located_wrapper f =
831 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
832 | Stdpp.Exc_located (floc, Stream.Error msg) ->
833 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
834 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
836 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
837 | Stdpp.Exc_located (floc, exn) ->
839 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
841 let parse_statement lexbuf =
843 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
845 let statement () = !grafite_parser.statement
847 let history = ref [] ;;
851 history := !grafite_parser :: !history;
852 grafite_parser := initial_parser ();
861 grafite_parser := gp;
865 (* vim:set foldmethod=marker: *)