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 "absurd"; t = tactic_term ->
185 GrafiteAst.Absurd (loc, t)
186 | IDENT "apply"; t = tactic_term ->
187 GrafiteAst.Apply (loc, t)
188 | IDENT "applyP"; t = tactic_term ->
189 GrafiteAst.ApplyP (loc, t)
190 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
191 GrafiteAst.ApplyS (loc, t, params)
192 | IDENT "assumption" ->
193 GrafiteAst.Assumption loc
194 | IDENT "autobatch"; params = auto_params ->
195 GrafiteAst.AutoBatch (loc,params)
196 | IDENT "cases"; what = tactic_term;
197 pattern = OPT pattern_spec;
198 specs = intros_spec ->
199 let pattern = match pattern with
200 | None -> None, [], Some Ast.UserInput
201 | Some pattern -> pattern
203 GrafiteAst.Cases (loc, what, pattern, specs)
204 | IDENT "clear"; ids = LIST1 IDENT ->
205 GrafiteAst.Clear (loc, ids)
206 | IDENT "clearbody"; id = IDENT ->
207 GrafiteAst.ClearBody (loc,id)
208 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
209 GrafiteAst.Change (loc, what, t)
210 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
211 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
212 let times = match times with None -> 1 | Some i -> i in
213 GrafiteAst.Compose (loc, t1, t2, times, specs)
214 | IDENT "constructor"; n = int ->
215 GrafiteAst.Constructor (loc, n)
216 | IDENT "contradiction" ->
217 GrafiteAst.Contradiction loc
218 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
219 GrafiteAst.Cut (loc, ident, t)
220 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
221 let idents = match idents with None -> [] | Some idents -> idents in
222 GrafiteAst.Decompose (loc, idents)
223 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
224 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
225 GrafiteAst.Destruct (loc, xts)
226 | IDENT "elim"; what = tactic_term; using = using;
227 pattern = OPT pattern_spec;
228 (num, idents) = intros_spec ->
229 let pattern = match pattern with
230 | None -> None, [], Some Ast.UserInput
231 | Some pattern -> pattern
233 GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
234 | IDENT "elimType"; what = tactic_term; using = using;
235 (num, idents) = intros_spec ->
236 GrafiteAst.ElimType (loc, what, using, (num, idents))
237 | IDENT "exact"; t = tactic_term ->
238 GrafiteAst.Exact (loc, t)
240 GrafiteAst.Exists loc
241 | IDENT "fail" -> GrafiteAst.Fail loc
242 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
245 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
246 ("the pattern cannot specify the term to replace, only its"
247 ^ " paths in the hypotheses and in the conclusion")))
249 GrafiteAst.Fold (loc, kind, t, p)
251 GrafiteAst.Fourier loc
252 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
253 let idents = match idents with None -> [] | Some idents -> idents in
254 GrafiteAst.FwdSimpl (loc, hyp, idents)
255 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
256 GrafiteAst.Generalize (loc,p,id)
257 | IDENT "id" -> GrafiteAst.IdTac loc
258 | IDENT "intro"; ident = OPT IDENT ->
259 let idents = match ident with None -> [] | Some id -> [Some id] in
260 GrafiteAst.Intros (loc, (Some 1, idents))
261 | IDENT "intros"; specs = intros_spec ->
262 GrafiteAst.Intros (loc, specs)
263 | IDENT "inversion"; t = tactic_term ->
264 GrafiteAst.Inversion (loc, t)
266 linear = OPT [ IDENT "linear" ];
267 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
269 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
270 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
271 let linear = match linear with None -> false | Some _ -> true in
272 let to_what = match to_what with None -> [] | Some to_what -> to_what in
273 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
274 | IDENT "left" -> GrafiteAst.Left loc
275 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
276 GrafiteAst.LetIn (loc, t, where)
277 | kind = reduction_kind; p = pattern_spec ->
278 GrafiteAst.Reduce (loc, kind, p)
279 | IDENT "reflexivity" ->
280 GrafiteAst.Reflexivity loc
281 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
282 GrafiteAst.Replace (loc, p, t)
283 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
284 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
288 (HExtlib.Localized (loc,
289 (CicNotationParser.Parse_error
290 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
292 let n = match xnames with None -> [] | Some names -> names in
293 GrafiteAst.Rewrite (loc, d, t, p, n)
300 | IDENT "symmetry" ->
301 GrafiteAst.Symmetry loc
302 | IDENT "transitivity"; t = tactic_term ->
303 GrafiteAst.Transitivity (loc, t)
304 (* Produzioni Aggiunte *)
305 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
306 GrafiteAst.Assume (loc, id, t)
307 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
308 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
309 t' = tactic_term -> t']->
310 GrafiteAst.Suppose (loc, t, id, t1)
311 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
312 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
313 id2 = IDENT ; RPAREN ->
314 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
316 [ IDENT "using"; t=tactic_term -> `Term t
317 | params = auto_params -> `Auto params] ;
318 cont=by_continuation ->
320 BYC_done -> GrafiteAst.Bydone (loc, just)
321 | BYC_weproved (ty,id,t1) ->
322 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
323 | BYC_letsuchthat (id1,t1,id2,t2) ->
324 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
325 | BYC_wehaveand (id1,t1,id2,t2) ->
326 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
327 | 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']->
328 GrafiteAst.We_need_to_prove (loc, t, id, t1)
329 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
330 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
331 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
332 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
333 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
334 GrafiteAst.Byinduction(loc, t, id)
335 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
336 GrafiteAst.Thesisbecomes(loc, t)
337 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
338 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
339 GrafiteAst.Case(loc,id,params)
340 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
342 termine = tactic_term;
346 [ IDENT "using"; t=tactic_term -> `Term t
347 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
348 | IDENT "proof" -> `Proof
349 | params = auto_params -> `Auto params];
350 cont = rewriting_step_continuation ->
351 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
352 | IDENT "obtain" ; name = IDENT;
353 termine = tactic_term;
357 [ IDENT "using"; t=tactic_term -> `Term t
358 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
359 | IDENT "proof" -> `Proof
360 | params = auto_params -> `Auto params];
361 cont = rewriting_step_continuation ->
362 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
366 [ IDENT "using"; t=tactic_term -> `Term t
367 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
368 | IDENT "proof" -> `Proof
369 | params = auto_params -> `Auto params];
370 cont = rewriting_step_continuation ->
371 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
375 [ IDENT "paramodulation"
387 i = auto_fixed_param -> i,""
388 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
389 string_of_int v | v = IDENT -> v ] -> i,v ];
390 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
391 (match tl with Some l -> l | None -> []),
396 [ 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)
397 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
398 "done" -> BYC_weproved (ty,None,t1)
400 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
401 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
402 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
403 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
404 BYC_wehaveand (id1,t1,id2,t2)
407 rewriting_step_continuation : [
414 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
417 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
420 GrafiteAst.Seq (loc, ts)
423 [ tac = SELF; SYMBOL ";";
424 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
425 (GrafiteAst.Then (loc, tac, tacs))
428 [ IDENT "do"; count = int; tac = SELF ->
429 GrafiteAst.Do (loc, count, tac)
430 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
434 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
435 GrafiteAst.First (loc, tacs)
436 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
438 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
439 GrafiteAst.Solve (loc, tacs)
440 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
441 | LPAREN; tac = SELF; RPAREN -> tac
442 | tac = tactic -> tac
445 punctuation_tactical:
447 [ SYMBOL "[" -> GrafiteAst.Branch loc
448 | SYMBOL "|" -> GrafiteAst.Shift loc
449 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
450 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
451 | SYMBOL "]" -> GrafiteAst.Merge loc
452 | SYMBOL ";" -> GrafiteAst.Semicolon loc
453 | SYMBOL "." -> GrafiteAst.Dot loc
456 non_punctuation_tactical:
458 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
459 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
460 | IDENT "skip" -> GrafiteAst.Skip loc
464 [ [ IDENT "definition" ] -> `Definition
465 | [ IDENT "fact" ] -> `Fact
466 | [ IDENT "lemma" ] -> `Lemma
467 | [ IDENT "remark" ] -> `Remark
468 | [ IDENT "theorem" ] -> `Theorem
472 [ attr = theorem_flavour -> attr
473 | [ IDENT "axiom" ] -> `Axiom
474 | [ IDENT "mutual" ] -> `MutualDefinition
479 params = LIST0 protected_binder_vars;
480 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
481 fst_constructors = LIST0 constructor SEP SYMBOL "|";
484 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
485 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
486 (name, true, typ, constructors) ] SEP "with" -> types
490 (fun (names, typ) acc ->
491 (List.map (fun name -> (name, typ)) names) @ acc)
494 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
495 let tl_ind_types = match tl with None -> [] | Some types -> types in
496 let ind_types = fst_ind_type :: tl_ind_types in
502 params = LIST0 protected_binder_vars;
503 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
507 SYMBOL ":" -> false,0
508 | SYMBOL ":"; SYMBOL ">" -> true,0
509 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
512 let b,n = coercion in
514 ] SEP SYMBOL ";"; SYMBOL "}" ->
517 (fun (names, typ) acc ->
518 (List.map (fun name -> (name, typ)) names) @ acc)
521 (params,name,typ,fields)
525 [ [ IDENT "check" ]; t = term ->
526 GrafiteAst.Check (loc, t)
528 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
529 suri = QSTRING; prefix = OPT QSTRING;
530 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
531 let style = match style with
532 | None -> GrafiteAst.Declarative
533 | Some depth -> GrafiteAst.Procedural depth
535 let prefix = match prefix with None -> "" | Some prefix -> prefix in
536 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
537 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
538 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
539 | IDENT "auto"; params = auto_params ->
540 GrafiteAst.AutoInteractive (loc,params)
541 | [ IDENT "whelp"; "match" ] ; t = term ->
542 GrafiteAst.WMatch (loc,t)
543 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
544 GrafiteAst.WInstance (loc,t)
545 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
546 GrafiteAst.WLocate (loc,id)
547 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
548 GrafiteAst.WElim (loc, t)
549 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
550 GrafiteAst.WHint (loc,t)
554 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
555 let alpha = "[a-zA-Z]" in
556 let num = "[0-9]+" in
557 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
558 let decoration = "\\'" in
559 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
560 let rex = Str.regexp ("^"^ident^"$") in
561 if Str.string_match rex id 0 then
562 if (try ignore (UriManager.uri_of_string uri); true
563 with UriManager.IllFormedUri _ -> false)
565 LexiconAst.Ident_alias (id, uri)
568 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
570 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
571 Printf.sprintf "Not a valid identifier: %s" id)))
572 | IDENT "symbol"; symbol = QSTRING;
573 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
574 SYMBOL "="; dsc = QSTRING ->
576 match instance with Some i -> i | None -> 0
578 LexiconAst.Symbol_alias (symbol, instance, dsc)
580 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
581 SYMBOL "="; dsc = QSTRING ->
583 match instance with Some i -> i | None -> 0
585 LexiconAst.Number_alias (instance, dsc)
589 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
591 Ast.IdentArg (List.length l, id)
595 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
596 | IDENT "right"; IDENT "associative" -> Gramext.RightA
597 | IDENT "non"; IDENT "associative" -> Gramext.NonA
601 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
604 [ dir = OPT direction; s = QSTRING;
605 assoc = OPT associativity; prec = precedence;
608 [ blob = UNPARSED_AST ->
609 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
610 (CicNotationParser.parse_level2_ast
611 (Ulexing.from_utf8_string blob))
612 | blob = UNPARSED_META ->
613 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
614 (CicNotationParser.parse_level2_meta
615 (Ulexing.from_utf8_string blob))
619 | None -> default_associativity
620 | Some assoc -> assoc
623 add_raw_attribute ~text:s
624 (CicNotationParser.parse_level1_pattern prec
625 (Ulexing.from_utf8_string s))
627 (dir, p1, assoc, prec, p2)
631 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
632 | id = IDENT -> Ast.VarPattern id
633 | SYMBOL "_" -> Ast.ImplicitPattern
634 | LPAREN; terms = LIST1 SELF; RPAREN ->
638 | terms -> Ast.ApplPattern terms)
642 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
648 IDENT "include" ; path = QSTRING ->
649 loc,path,LexiconAst.WithPreferences
650 | IDENT "include'" ; path = QSTRING ->
651 loc,path,LexiconAst.WithoutPreferences
655 IDENT "set"; n = QSTRING; v = QSTRING ->
656 GrafiteAst.Set (loc, n, v)
657 | IDENT "drop" -> GrafiteAst.Drop loc
658 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
659 | IDENT "qed" -> GrafiteAst.Qed loc
660 | IDENT "variant" ; name = IDENT; SYMBOL ":";
661 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
664 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
665 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
666 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
667 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
668 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
671 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
672 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
673 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
674 | LETCOREC ; defs = let_defs ->
675 mk_rec_corec `CoInductive defs loc
676 | LETREC ; defs = let_defs ->
677 mk_rec_corec `Inductive defs loc
678 | IDENT "inductive"; spec = inductive_spec ->
679 let (params, ind_types) = spec in
680 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
681 | IDENT "coinductive"; spec = inductive_spec ->
682 let (params, ind_types) = spec in
683 let ind_types = (* set inductive flags to false (coinductive) *)
684 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
687 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
689 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
690 arity = OPT int ; saturations = OPT int;
691 composites = OPT (IDENT "nocomposites") ->
692 let arity = match arity with None -> 0 | Some x -> x in
693 let saturations = match saturations with None -> 0 | Some x -> x in
694 let composites = match composites with None -> true | Some _ -> false in
696 (loc, t, composites, arity, saturations)
697 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
698 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
699 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
700 let uris = List.map UriManager.uri_of_string uris in
701 GrafiteAst.Default (loc,what,uris)
702 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
703 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
704 refl = tactic_term -> refl ] ;
705 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
706 sym = tactic_term -> sym ] ;
707 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
708 trans = tactic_term -> trans ] ;
710 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
713 IDENT "alias" ; spec = alias_spec ->
714 LexiconAst.Alias (loc, spec)
715 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
716 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
717 | IDENT "interpretation"; id = QSTRING;
718 (symbol, args, l3) = interpretation ->
719 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
722 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
723 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
724 GrafiteAst.Tactic (loc, Some tac, punct)
725 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
726 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
727 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
728 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
732 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
733 GrafiteAst.Code (loc, ex)
735 GrafiteAst.Note (loc, str)
740 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
742 fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
743 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
745 fun ?(never_include=false) ~include_paths status ->
746 let _root, buri, fullpath, _rrelpath =
747 Librarian.baseuri_of_script ~include_paths fname
750 if never_include then raise (NoInclusionPerformed fullpath)
751 else LexiconEngine.eval_command status
752 (LexiconAst.Include (iloc,buri,mode,fullpath))
756 (GrafiteAst.Executable
757 (loc,GrafiteAst.Command
758 (loc,GrafiteAst.Include (iloc,buri))))
759 | scom = lexicon_command ; SYMBOL "." ->
760 fun ?(never_include=false) ~include_paths status ->
761 let status = LexiconEngine.eval_command status scom in
763 | EOI -> raise End_of_file
770 let _ = initialize_parser () ;;
772 let exc_located_wrapper f =
776 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
777 | Stdpp.Exc_located (floc, Stream.Error msg) ->
778 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
779 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
781 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
782 | Stdpp.Exc_located (floc, exn) ->
784 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
786 let parse_statement lexbuf =
788 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
790 let statement () = !grafite_parser.statement
792 let history = ref [] ;;
796 history := !grafite_parser :: !history;
797 grafite_parser := initial_parser ();
806 grafite_parser := gp;
810 (* vim:set foldmethod=marker: *)