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 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
192 | SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")
193 | SYMBOL "*"; n=IDENT ->
194 GrafiteAst.NCase1 (loc,n)
198 [ IDENT "absurd"; t = tactic_term ->
199 GrafiteAst.Absurd (loc, t)
200 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
201 GrafiteAst.ApplyRule (loc, t)
202 | IDENT "apply"; t = tactic_term ->
203 GrafiteAst.Apply (loc, t)
204 | IDENT "applyP"; t = tactic_term ->
205 GrafiteAst.ApplyP (loc, t)
206 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
207 GrafiteAst.ApplyS (loc, t, params)
208 | IDENT "assumption" ->
209 GrafiteAst.Assumption loc
210 | IDENT "autobatch"; params = auto_params ->
211 GrafiteAst.AutoBatch (loc,params)
212 | IDENT "cases"; what = tactic_term;
213 pattern = OPT pattern_spec;
214 specs = intros_spec ->
215 let pattern = match pattern with
216 | None -> None, [], Some Ast.UserInput
217 | Some pattern -> pattern
219 GrafiteAst.Cases (loc, what, pattern, specs)
220 | IDENT "clear"; ids = LIST1 IDENT ->
221 GrafiteAst.Clear (loc, ids)
222 | IDENT "clearbody"; id = IDENT ->
223 GrafiteAst.ClearBody (loc,id)
224 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
225 GrafiteAst.Change (loc, what, t)
226 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
227 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
228 let times = match times with None -> 1 | Some i -> i in
229 GrafiteAst.Compose (loc, t1, t2, times, specs)
230 | IDENT "constructor"; n = int ->
231 GrafiteAst.Constructor (loc, n)
232 | IDENT "contradiction" ->
233 GrafiteAst.Contradiction loc
234 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
235 GrafiteAst.Cut (loc, ident, t)
236 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
237 let idents = match idents with None -> [] | Some idents -> idents in
238 GrafiteAst.Decompose (loc, idents)
239 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
240 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
241 GrafiteAst.Destruct (loc, xts)
242 | IDENT "elim"; what = tactic_term; using = using;
243 pattern = OPT pattern_spec;
244 ispecs = intros_spec ->
245 let pattern = match pattern with
246 | None -> None, [], Some Ast.UserInput
247 | Some pattern -> pattern
249 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
250 | IDENT "elimType"; what = tactic_term; using = using;
251 (num, idents) = intros_spec ->
252 GrafiteAst.ElimType (loc, what, using, (num, idents))
253 | IDENT "exact"; t = tactic_term ->
254 GrafiteAst.Exact (loc, t)
256 GrafiteAst.Exists loc
257 | IDENT "fail" -> GrafiteAst.Fail loc
258 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
261 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
262 ("the pattern cannot specify the term to replace, only its"
263 ^ " paths in the hypotheses and in the conclusion")))
265 GrafiteAst.Fold (loc, kind, t, p)
267 GrafiteAst.Fourier loc
268 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
269 let idents = match idents with None -> [] | Some idents -> idents in
270 GrafiteAst.FwdSimpl (loc, hyp, idents)
271 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
272 GrafiteAst.Generalize (loc,p,id)
273 | IDENT "id" -> GrafiteAst.IdTac loc
274 | IDENT "intro"; ident = OPT IDENT ->
275 let idents = match ident with None -> [] | Some id -> [Some id] in
276 GrafiteAst.Intros (loc, (Some 1, idents))
277 | IDENT "intros"; specs = intros_spec ->
278 GrafiteAst.Intros (loc, specs)
279 | IDENT "inversion"; t = tactic_term ->
280 GrafiteAst.Inversion (loc, t)
282 linear = OPT [ IDENT "linear" ];
283 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
285 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
286 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
287 let linear = match linear with None -> false | Some _ -> true in
288 let to_what = match to_what with None -> [] | Some to_what -> to_what in
289 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
290 | IDENT "left" -> GrafiteAst.Left loc
291 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
292 GrafiteAst.LetIn (loc, t, where)
293 | kind = reduction_kind; p = pattern_spec ->
294 GrafiteAst.Reduce (loc, kind, p)
295 | IDENT "reflexivity" ->
296 GrafiteAst.Reflexivity loc
297 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
298 GrafiteAst.Replace (loc, p, t)
299 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
300 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
304 (HExtlib.Localized (loc,
305 (CicNotationParser.Parse_error
306 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
308 let n = match xnames with None -> [] | Some names -> names in
309 GrafiteAst.Rewrite (loc, d, t, p, n)
316 | IDENT "symmetry" ->
317 GrafiteAst.Symmetry loc
318 | IDENT "transitivity"; t = tactic_term ->
319 GrafiteAst.Transitivity (loc, t)
320 (* Produzioni Aggiunte *)
321 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
322 GrafiteAst.Assume (loc, id, t)
323 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
324 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
325 t' = tactic_term -> t']->
326 GrafiteAst.Suppose (loc, t, id, t1)
327 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
328 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
329 id2 = IDENT ; RPAREN ->
330 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
332 [ IDENT "using"; t=tactic_term -> `Term t
333 | params = auto_params -> `Auto params] ;
334 cont=by_continuation ->
336 BYC_done -> GrafiteAst.Bydone (loc, just)
337 | BYC_weproved (ty,id,t1) ->
338 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
339 | BYC_letsuchthat (id1,t1,id2,t2) ->
340 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
341 | BYC_wehaveand (id1,t1,id2,t2) ->
342 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
343 | 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']->
344 GrafiteAst.We_need_to_prove (loc, t, id, t1)
345 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
346 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
347 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
348 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
349 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
350 GrafiteAst.Byinduction(loc, t, id)
351 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
352 GrafiteAst.Thesisbecomes(loc, t)
353 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
354 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
355 GrafiteAst.Case(loc,id,params)
356 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
358 termine = tactic_term;
362 [ IDENT "using"; t=tactic_term -> `Term t
363 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
364 | IDENT "proof" -> `Proof
365 | params = auto_params -> `Auto params];
366 cont = rewriting_step_continuation ->
367 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
368 | IDENT "obtain" ; name = IDENT;
369 termine = tactic_term;
373 [ IDENT "using"; t=tactic_term -> `Term t
374 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
375 | IDENT "proof" -> `Proof
376 | params = auto_params -> `Auto params];
377 cont = rewriting_step_continuation ->
378 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
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, None, t1, t2, cont)
391 [ IDENT "paramodulation"
403 i = auto_fixed_param -> i,""
404 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
405 string_of_int v | v = IDENT -> v ] -> i,v ];
406 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
407 (match tl with Some l -> l | None -> []),
412 [ 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)
413 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
414 "done" -> BYC_weproved (ty,None,t1)
416 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
417 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
418 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
419 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
420 BYC_wehaveand (id1,t1,id2,t2)
423 rewriting_step_continuation : [
430 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
433 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
436 GrafiteAst.Seq (loc, ts)
439 [ tac = SELF; SYMBOL ";";
440 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
441 (GrafiteAst.Then (loc, tac, tacs))
444 [ IDENT "do"; count = int; tac = SELF ->
445 GrafiteAst.Do (loc, count, tac)
446 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
450 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
451 GrafiteAst.First (loc, tacs)
452 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
454 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
455 GrafiteAst.Solve (loc, tacs)
456 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
457 | LPAREN; tac = SELF; RPAREN -> tac
458 | tac = tactic -> tac
461 punctuation_tactical:
463 [ SYMBOL "[" -> GrafiteAst.Branch loc
464 | SYMBOL "|" -> GrafiteAst.Shift loc
465 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
466 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
467 | SYMBOL "]" -> GrafiteAst.Merge loc
468 | SYMBOL ";" -> GrafiteAst.Semicolon loc
469 | SYMBOL "." -> GrafiteAst.Dot loc
472 non_punctuation_tactical:
474 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
475 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
476 | IDENT "skip" -> GrafiteAst.Skip loc
480 [ [ IDENT "ntheorem" ] -> `Theorem
484 [ [ IDENT "definition" ] -> `Definition
485 | [ IDENT "fact" ] -> `Fact
486 | [ IDENT "lemma" ] -> `Lemma
487 | [ IDENT "remark" ] -> `Remark
488 | [ IDENT "theorem" ] -> `Theorem
492 [ attr = theorem_flavour -> attr
493 | [ IDENT "axiom" ] -> `Axiom
494 | [ IDENT "mutual" ] -> `MutualDefinition
499 params = LIST0 protected_binder_vars;
500 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
501 fst_constructors = LIST0 constructor SEP SYMBOL "|";
504 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
505 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
506 (name, true, typ, constructors) ] SEP "with" -> types
510 (fun (names, typ) acc ->
511 (List.map (fun name -> (name, typ)) names) @ acc)
514 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
515 let tl_ind_types = match tl with None -> [] | Some types -> types in
516 let ind_types = fst_ind_type :: tl_ind_types in
522 params = LIST0 protected_binder_vars;
523 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
527 SYMBOL ":" -> false,0
528 | SYMBOL ":"; SYMBOL ">" -> true,0
529 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
532 let b,n = coercion in
534 ] SEP SYMBOL ";"; SYMBOL "}" ->
537 (fun (names, typ) acc ->
538 (List.map (fun name -> (name, typ)) names) @ acc)
541 (params,name,typ,fields)
545 [ [ IDENT "check" ]; t = term ->
546 GrafiteAst.Check (loc, t)
547 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
548 GrafiteAst.Eval (loc, kind, t)
550 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
551 suri = QSTRING; prefix = OPT QSTRING;
552 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
553 let style = match style with
554 | None -> GrafiteAst.Declarative
555 | Some depth -> GrafiteAst.Procedural depth
557 let prefix = match prefix with None -> "" | Some prefix -> prefix in
558 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
559 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
560 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
561 | IDENT "auto"; params = auto_params ->
562 GrafiteAst.AutoInteractive (loc,params)
563 | [ IDENT "whelp"; "match" ] ; t = term ->
564 GrafiteAst.WMatch (loc,t)
565 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
566 GrafiteAst.WInstance (loc,t)
567 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
568 GrafiteAst.WLocate (loc,id)
569 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
570 GrafiteAst.WElim (loc, t)
571 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
572 GrafiteAst.WHint (loc,t)
576 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
577 let alpha = "[a-zA-Z]" in
578 let num = "[0-9]+" in
579 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
580 let decoration = "\\'" in
581 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
582 let rex = Str.regexp ("^"^ident^"$") in
583 if Str.string_match rex id 0 then
584 if (try ignore (UriManager.uri_of_string uri); true
585 with UriManager.IllFormedUri _ -> false)
587 LexiconAst.Ident_alias (id, uri)
590 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
592 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
593 Printf.sprintf "Not a valid identifier: %s" id)))
594 | IDENT "symbol"; symbol = QSTRING;
595 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
596 SYMBOL "="; dsc = QSTRING ->
598 match instance with Some i -> i | None -> 0
600 LexiconAst.Symbol_alias (symbol, instance, dsc)
602 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
603 SYMBOL "="; dsc = QSTRING ->
605 match instance with Some i -> i | None -> 0
607 LexiconAst.Number_alias (instance, dsc)
611 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
613 Ast.IdentArg (List.length l, id)
617 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
618 | IDENT "right"; IDENT "associative" -> Gramext.RightA
619 | IDENT "non"; IDENT "associative" -> Gramext.NonA
623 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
626 [ dir = OPT direction; s = QSTRING;
627 assoc = OPT associativity; prec = precedence;
630 [ blob = UNPARSED_AST ->
631 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
632 (CicNotationParser.parse_level2_ast
633 (Ulexing.from_utf8_string blob))
634 | blob = UNPARSED_META ->
635 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
636 (CicNotationParser.parse_level2_meta
637 (Ulexing.from_utf8_string blob))
641 | None -> default_associativity
642 | Some assoc -> assoc
645 add_raw_attribute ~text:s
646 (CicNotationParser.parse_level1_pattern prec
647 (Ulexing.from_utf8_string s))
649 (dir, p1, assoc, prec, p2)
653 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
654 | id = IDENT -> Ast.VarPattern id
655 | SYMBOL "_" -> Ast.ImplicitPattern
656 | LPAREN; terms = LIST1 SELF; RPAREN ->
660 | terms -> Ast.ApplPattern terms)
664 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
670 IDENT "include" ; path = QSTRING ->
671 loc,path,LexiconAst.WithPreferences
672 | IDENT "include'" ; path = QSTRING ->
673 loc,path,LexiconAst.WithoutPreferences
677 IDENT "set"; n = QSTRING; v = QSTRING ->
678 GrafiteAst.Set (loc, n, v)
679 | IDENT "drop" -> GrafiteAst.Drop loc
680 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
681 | IDENT "qed" -> GrafiteAst.Qed loc
682 | IDENT "variant" ; name = IDENT; SYMBOL ":";
683 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
686 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
687 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
688 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
689 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
690 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
691 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
692 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
693 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
696 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
697 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
698 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
699 | LETCOREC ; defs = let_defs ->
700 mk_rec_corec `CoInductive defs loc
701 | LETREC ; defs = let_defs ->
702 mk_rec_corec `Inductive defs loc
703 | IDENT "inductive"; spec = inductive_spec ->
704 let (params, ind_types) = spec in
705 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
706 | IDENT "coinductive"; spec = inductive_spec ->
707 let (params, ind_types) = spec in
708 let ind_types = (* set inductive flags to false (coinductive) *)
709 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
712 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
714 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
715 arity = OPT int ; saturations = OPT int;
716 composites = OPT (IDENT "nocomposites") ->
717 let arity = match arity with None -> 0 | Some x -> x in
718 let saturations = match saturations with None -> 0 | Some x -> x in
719 let composites = match composites with None -> true | Some _ -> false in
721 (loc, t, composites, arity, saturations)
722 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
723 GrafiteAst.PreferCoercion (loc, t)
724 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
725 GrafiteAst.UnificationHint (loc, t, n)
726 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
727 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
728 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
729 let uris = List.map UriManager.uri_of_string uris in
730 GrafiteAst.Default (loc,what,uris)
731 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
732 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
733 refl = tactic_term -> refl ] ;
734 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
735 sym = tactic_term -> sym ] ;
736 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
737 trans = tactic_term -> trans ] ;
739 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
742 IDENT "alias" ; spec = alias_spec ->
743 LexiconAst.Alias (loc, spec)
744 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
745 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
746 | IDENT "interpretation"; id = QSTRING;
747 (symbol, args, l3) = interpretation ->
748 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
751 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
752 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
753 GrafiteAst.Tactic (loc, Some tac, punct)
754 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
755 | tac = ntactic; punct = punctuation_tactical ->
756 GrafiteAst.NTactic (loc, tac, punct)
757 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
758 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
759 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
760 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
761 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
765 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
766 GrafiteAst.Code (loc, ex)
768 GrafiteAst.Note (loc, str)
773 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
775 fun ?(never_include=false) ~include_paths status ->
776 status,LSome (GrafiteAst.Comment (loc, com))
777 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
779 fun ?(never_include=false) ~include_paths status ->
780 let _root, buri, fullpath, _rrelpath =
781 Librarian.baseuri_of_script ~include_paths fname
784 if never_include then raise (NoInclusionPerformed fullpath)
785 else LexiconEngine.eval_command status
786 (LexiconAst.Include (iloc,buri,mode,fullpath))
790 (GrafiteAst.Executable
791 (loc,GrafiteAst.Command
792 (loc,GrafiteAst.Include (iloc,buri))))
793 | scom = lexicon_command ; SYMBOL "." ->
794 fun ?(never_include=false) ~include_paths status ->
795 let status = LexiconEngine.eval_command status scom in
797 | EOI -> raise End_of_file
804 let _ = initialize_parser () ;;
806 let exc_located_wrapper f =
810 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
811 | Stdpp.Exc_located (floc, Stream.Error msg) ->
812 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
813 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
815 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
816 | Stdpp.Exc_located (floc, exn) ->
818 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
820 let parse_statement lexbuf =
822 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
824 let statement () = !grafite_parser.statement
826 let history = ref [] ;;
830 history := !grafite_parser :: !history;
831 grafite_parser := initial_parser ();
840 grafite_parser := gp;
844 (* vim:set foldmethod=marker: *)