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 ->
185 GrafiteAst.NApply (loc, t)
189 [ IDENT "absurd"; t = tactic_term ->
190 GrafiteAst.Absurd (loc, t)
191 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
192 GrafiteAst.ApplyRule (loc, t)
193 | IDENT "apply"; t = tactic_term ->
194 GrafiteAst.Apply (loc, t)
195 | IDENT "applyP"; t = tactic_term ->
196 GrafiteAst.ApplyP (loc, t)
197 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
198 GrafiteAst.ApplyS (loc, t, params)
199 | IDENT "assumption" ->
200 GrafiteAst.Assumption loc
201 | IDENT "autobatch"; params = auto_params ->
202 GrafiteAst.AutoBatch (loc,params)
203 | IDENT "cases"; what = tactic_term;
204 pattern = OPT pattern_spec;
205 specs = intros_spec ->
206 let pattern = match pattern with
207 | None -> None, [], Some Ast.UserInput
208 | Some pattern -> pattern
210 GrafiteAst.Cases (loc, what, pattern, specs)
211 | IDENT "clear"; ids = LIST1 IDENT ->
212 GrafiteAst.Clear (loc, ids)
213 | IDENT "clearbody"; id = IDENT ->
214 GrafiteAst.ClearBody (loc,id)
215 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
216 GrafiteAst.Change (loc, what, t)
217 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
218 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
219 let times = match times with None -> 1 | Some i -> i in
220 GrafiteAst.Compose (loc, t1, t2, times, specs)
221 | IDENT "constructor"; n = int ->
222 GrafiteAst.Constructor (loc, n)
223 | IDENT "contradiction" ->
224 GrafiteAst.Contradiction loc
225 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
226 GrafiteAst.Cut (loc, ident, t)
227 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
228 let idents = match idents with None -> [] | Some idents -> idents in
229 GrafiteAst.Decompose (loc, idents)
230 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
231 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
232 GrafiteAst.Destruct (loc, xts)
233 | IDENT "elim"; what = tactic_term; using = using;
234 pattern = OPT pattern_spec;
235 ispecs = intros_spec ->
236 let pattern = match pattern with
237 | None -> None, [], Some Ast.UserInput
238 | Some pattern -> pattern
240 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
241 | IDENT "elimType"; what = tactic_term; using = using;
242 (num, idents) = intros_spec ->
243 GrafiteAst.ElimType (loc, what, using, (num, idents))
244 | IDENT "exact"; t = tactic_term ->
245 GrafiteAst.Exact (loc, t)
247 GrafiteAst.Exists loc
248 | IDENT "fail" -> GrafiteAst.Fail loc
249 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
252 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
253 ("the pattern cannot specify the term to replace, only its"
254 ^ " paths in the hypotheses and in the conclusion")))
256 GrafiteAst.Fold (loc, kind, t, p)
258 GrafiteAst.Fourier loc
259 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
260 let idents = match idents with None -> [] | Some idents -> idents in
261 GrafiteAst.FwdSimpl (loc, hyp, idents)
262 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
263 GrafiteAst.Generalize (loc,p,id)
264 | IDENT "id" -> GrafiteAst.IdTac loc
265 | IDENT "intro"; ident = OPT IDENT ->
266 let idents = match ident with None -> [] | Some id -> [Some id] in
267 GrafiteAst.Intros (loc, (Some 1, idents))
268 | IDENT "intros"; specs = intros_spec ->
269 GrafiteAst.Intros (loc, specs)
270 | IDENT "inversion"; t = tactic_term ->
271 GrafiteAst.Inversion (loc, t)
273 linear = OPT [ IDENT "linear" ];
274 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
276 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
277 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
278 let linear = match linear with None -> false | Some _ -> true in
279 let to_what = match to_what with None -> [] | Some to_what -> to_what in
280 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
281 | IDENT "left" -> GrafiteAst.Left loc
282 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
283 GrafiteAst.LetIn (loc, t, where)
284 | kind = reduction_kind; p = pattern_spec ->
285 GrafiteAst.Reduce (loc, kind, p)
286 | IDENT "reflexivity" ->
287 GrafiteAst.Reflexivity loc
288 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
289 GrafiteAst.Replace (loc, p, t)
290 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
291 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
295 (HExtlib.Localized (loc,
296 (CicNotationParser.Parse_error
297 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
299 let n = match xnames with None -> [] | Some names -> names in
300 GrafiteAst.Rewrite (loc, d, t, p, n)
307 | IDENT "symmetry" ->
308 GrafiteAst.Symmetry loc
309 | IDENT "transitivity"; t = tactic_term ->
310 GrafiteAst.Transitivity (loc, t)
311 (* Produzioni Aggiunte *)
312 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
313 GrafiteAst.Assume (loc, id, t)
314 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
315 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
316 t' = tactic_term -> t']->
317 GrafiteAst.Suppose (loc, t, id, t1)
318 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
319 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
320 id2 = IDENT ; RPAREN ->
321 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
323 [ IDENT "using"; t=tactic_term -> `Term t
324 | params = auto_params -> `Auto params] ;
325 cont=by_continuation ->
327 BYC_done -> GrafiteAst.Bydone (loc, just)
328 | BYC_weproved (ty,id,t1) ->
329 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
330 | BYC_letsuchthat (id1,t1,id2,t2) ->
331 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
332 | BYC_wehaveand (id1,t1,id2,t2) ->
333 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
334 | 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']->
335 GrafiteAst.We_need_to_prove (loc, t, id, t1)
336 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
337 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
338 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
339 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
340 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
341 GrafiteAst.Byinduction(loc, t, id)
342 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
343 GrafiteAst.Thesisbecomes(loc, t)
344 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
345 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
346 GrafiteAst.Case(loc,id,params)
347 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
349 termine = tactic_term;
353 [ IDENT "using"; t=tactic_term -> `Term t
354 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
355 | IDENT "proof" -> `Proof
356 | params = auto_params -> `Auto params];
357 cont = rewriting_step_continuation ->
358 GrafiteAst.RewritingStep(loc, Some (None,termine), t1, t2, cont)
359 | IDENT "obtain" ; name = IDENT;
360 termine = tactic_term;
364 [ IDENT "using"; t=tactic_term -> `Term t
365 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
366 | IDENT "proof" -> `Proof
367 | params = auto_params -> `Auto params];
368 cont = rewriting_step_continuation ->
369 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
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, None, t1, t2, cont)
382 [ IDENT "paramodulation"
394 i = auto_fixed_param -> i,""
395 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
396 string_of_int v | v = IDENT -> v ] -> i,v ];
397 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
398 (match tl with Some l -> l | None -> []),
403 [ 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)
404 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
405 "done" -> BYC_weproved (ty,None,t1)
407 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
408 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
409 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
410 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
411 BYC_wehaveand (id1,t1,id2,t2)
414 rewriting_step_continuation : [
421 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
424 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
427 GrafiteAst.Seq (loc, ts)
430 [ tac = SELF; SYMBOL ";";
431 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
432 (GrafiteAst.Then (loc, tac, tacs))
435 [ IDENT "do"; count = int; tac = SELF ->
436 GrafiteAst.Do (loc, count, tac)
437 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
441 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
442 GrafiteAst.First (loc, tacs)
443 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
445 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
446 GrafiteAst.Solve (loc, tacs)
447 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
448 | LPAREN; tac = SELF; RPAREN -> tac
449 | tac = tactic -> tac
452 punctuation_tactical:
454 [ SYMBOL "[" -> GrafiteAst.Branch loc
455 | SYMBOL "|" -> GrafiteAst.Shift loc
456 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
457 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
458 | SYMBOL "]" -> GrafiteAst.Merge loc
459 | SYMBOL ";" -> GrafiteAst.Semicolon loc
460 | SYMBOL "." -> GrafiteAst.Dot loc
463 non_punctuation_tactical:
465 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
466 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
467 | IDENT "skip" -> GrafiteAst.Skip loc
471 [ [ IDENT "ntheorem" ] -> `Theorem
475 [ [ IDENT "definition" ] -> `Definition
476 | [ IDENT "fact" ] -> `Fact
477 | [ IDENT "lemma" ] -> `Lemma
478 | [ IDENT "remark" ] -> `Remark
479 | [ IDENT "theorem" ] -> `Theorem
483 [ attr = theorem_flavour -> attr
484 | [ IDENT "axiom" ] -> `Axiom
485 | [ IDENT "mutual" ] -> `MutualDefinition
490 params = LIST0 protected_binder_vars;
491 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
492 fst_constructors = LIST0 constructor SEP SYMBOL "|";
495 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
496 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
497 (name, true, typ, constructors) ] SEP "with" -> types
501 (fun (names, typ) acc ->
502 (List.map (fun name -> (name, typ)) names) @ acc)
505 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
506 let tl_ind_types = match tl with None -> [] | Some types -> types in
507 let ind_types = fst_ind_type :: tl_ind_types in
513 params = LIST0 protected_binder_vars;
514 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
518 SYMBOL ":" -> false,0
519 | SYMBOL ":"; SYMBOL ">" -> true,0
520 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
523 let b,n = coercion in
525 ] SEP SYMBOL ";"; SYMBOL "}" ->
528 (fun (names, typ) acc ->
529 (List.map (fun name -> (name, typ)) names) @ acc)
532 (params,name,typ,fields)
536 [ [ IDENT "check" ]; t = term ->
537 GrafiteAst.Check (loc, t)
538 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
539 GrafiteAst.Eval (loc, kind, t)
541 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
542 suri = QSTRING; prefix = OPT QSTRING;
543 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
544 let style = match style with
545 | None -> GrafiteAst.Declarative
546 | Some depth -> GrafiteAst.Procedural depth
548 let prefix = match prefix with None -> "" | Some prefix -> prefix in
549 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
550 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
551 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
552 | IDENT "auto"; params = auto_params ->
553 GrafiteAst.AutoInteractive (loc,params)
554 | [ IDENT "whelp"; "match" ] ; t = term ->
555 GrafiteAst.WMatch (loc,t)
556 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
557 GrafiteAst.WInstance (loc,t)
558 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
559 GrafiteAst.WLocate (loc,id)
560 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
561 GrafiteAst.WElim (loc, t)
562 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
563 GrafiteAst.WHint (loc,t)
567 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
568 let alpha = "[a-zA-Z]" in
569 let num = "[0-9]+" in
570 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
571 let decoration = "\\'" in
572 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
573 let rex = Str.regexp ("^"^ident^"$") in
574 if Str.string_match rex id 0 then
575 if (try ignore (UriManager.uri_of_string uri); true
576 with UriManager.IllFormedUri _ -> false)
578 LexiconAst.Ident_alias (id, uri)
581 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
583 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
584 Printf.sprintf "Not a valid identifier: %s" id)))
585 | IDENT "symbol"; symbol = QSTRING;
586 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
587 SYMBOL "="; dsc = QSTRING ->
589 match instance with Some i -> i | None -> 0
591 LexiconAst.Symbol_alias (symbol, instance, dsc)
593 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
594 SYMBOL "="; dsc = QSTRING ->
596 match instance with Some i -> i | None -> 0
598 LexiconAst.Number_alias (instance, dsc)
602 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
604 Ast.IdentArg (List.length l, id)
608 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
609 | IDENT "right"; IDENT "associative" -> Gramext.RightA
610 | IDENT "non"; IDENT "associative" -> Gramext.NonA
614 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
617 [ dir = OPT direction; s = QSTRING;
618 assoc = OPT associativity; prec = precedence;
621 [ blob = UNPARSED_AST ->
622 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
623 (CicNotationParser.parse_level2_ast
624 (Ulexing.from_utf8_string blob))
625 | blob = UNPARSED_META ->
626 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
627 (CicNotationParser.parse_level2_meta
628 (Ulexing.from_utf8_string blob))
632 | None -> default_associativity
633 | Some assoc -> assoc
636 add_raw_attribute ~text:s
637 (CicNotationParser.parse_level1_pattern prec
638 (Ulexing.from_utf8_string s))
640 (dir, p1, assoc, prec, p2)
644 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
645 | id = IDENT -> Ast.VarPattern id
646 | SYMBOL "_" -> Ast.ImplicitPattern
647 | LPAREN; terms = LIST1 SELF; RPAREN ->
651 | terms -> Ast.ApplPattern terms)
655 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
661 IDENT "include" ; path = QSTRING ->
662 loc,path,LexiconAst.WithPreferences
663 | IDENT "include'" ; path = QSTRING ->
664 loc,path,LexiconAst.WithoutPreferences
668 IDENT "set"; n = QSTRING; v = QSTRING ->
669 GrafiteAst.Set (loc, n, v)
670 | IDENT "drop" -> GrafiteAst.Drop loc
671 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
672 | IDENT "qed" -> GrafiteAst.Qed loc
673 | IDENT "variant" ; name = IDENT; SYMBOL ":";
674 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
677 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
678 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
679 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
680 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
681 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
682 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
683 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
684 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
687 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
688 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
689 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
690 | LETCOREC ; defs = let_defs ->
691 mk_rec_corec `CoInductive defs loc
692 | LETREC ; defs = let_defs ->
693 mk_rec_corec `Inductive defs loc
694 | IDENT "inductive"; spec = inductive_spec ->
695 let (params, ind_types) = spec in
696 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
697 | IDENT "coinductive"; spec = inductive_spec ->
698 let (params, ind_types) = spec in
699 let ind_types = (* set inductive flags to false (coinductive) *)
700 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
703 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
705 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
706 arity = OPT int ; saturations = OPT int;
707 composites = OPT (IDENT "nocomposites") ->
708 let arity = match arity with None -> 0 | Some x -> x in
709 let saturations = match saturations with None -> 0 | Some x -> x in
710 let composites = match composites with None -> true | Some _ -> false in
712 (loc, t, composites, arity, saturations)
713 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
714 GrafiteAst.PreferCoercion (loc, t)
715 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
716 GrafiteAst.UnificationHint (loc, t, n)
717 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
718 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
719 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
720 let uris = List.map UriManager.uri_of_string uris in
721 GrafiteAst.Default (loc,what,uris)
722 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
723 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
724 refl = tactic_term -> refl ] ;
725 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
726 sym = tactic_term -> sym ] ;
727 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
728 trans = tactic_term -> trans ] ;
730 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
733 IDENT "alias" ; spec = alias_spec ->
734 LexiconAst.Alias (loc, spec)
735 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
736 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
737 | IDENT "interpretation"; id = QSTRING;
738 (symbol, args, l3) = interpretation ->
739 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
742 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
743 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
744 GrafiteAst.Tactic (loc, Some tac, punct)
745 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
746 | tac = ntactic; punct = punctuation_tactical ->
747 GrafiteAst.NTactic (loc, tac, punct)
748 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
749 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
750 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
754 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
755 GrafiteAst.Code (loc, ex)
757 GrafiteAst.Note (loc, str)
762 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
764 fun ?(never_include=false) ~include_paths status ->
765 status,LSome (GrafiteAst.Comment (loc, com))
766 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
768 fun ?(never_include=false) ~include_paths status ->
769 let _root, buri, fullpath, _rrelpath =
770 Librarian.baseuri_of_script ~include_paths fname
773 if never_include then raise (NoInclusionPerformed fullpath)
774 else LexiconEngine.eval_command status
775 (LexiconAst.Include (iloc,buri,mode,fullpath))
779 (GrafiteAst.Executable
780 (loc,GrafiteAst.Command
781 (loc,GrafiteAst.Include (iloc,buri))))
782 | scom = lexicon_command ; SYMBOL "." ->
783 fun ?(never_include=false) ~include_paths status ->
784 let status = LexiconEngine.eval_command status scom in
786 | EOI -> raise End_of_file
793 let _ = initialize_parser () ;;
795 let exc_located_wrapper f =
799 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
800 | Stdpp.Exc_located (floc, Stream.Error msg) ->
801 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
802 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
804 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
805 | Stdpp.Exc_located (floc, exn) ->
807 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
809 let parse_statement lexbuf =
811 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
813 let statement () = !grafite_parser.statement
815 let history = ref [] ;;
819 history := !grafite_parser :: !history;
820 grafite_parser := initial_parser ();
829 grafite_parser := gp;
833 (* vim:set foldmethod=marker: *)