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 "nchange"; what = pattern_spec; "with"; with_what = tactic_term ->
186 GrafiteAst.NChange (loc, what, with_what)
187 | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
188 GrafiteAst.NElim (loc, what, where)
189 | SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
193 [ IDENT "absurd"; t = tactic_term ->
194 GrafiteAst.Absurd (loc, t)
195 | IDENT "apply"; IDENT "rule"; t = tactic_term ->
196 GrafiteAst.ApplyRule (loc, t)
197 | IDENT "apply"; t = tactic_term ->
198 GrafiteAst.Apply (loc, t)
199 | IDENT "applyP"; t = tactic_term ->
200 GrafiteAst.ApplyP (loc, t)
201 | IDENT "applyS"; t = tactic_term ; params = auto_params ->
202 GrafiteAst.ApplyS (loc, t, params)
203 | IDENT "assumption" ->
204 GrafiteAst.Assumption loc
205 | IDENT "autobatch"; params = auto_params ->
206 GrafiteAst.AutoBatch (loc,params)
207 | IDENT "cases"; what = tactic_term;
208 pattern = OPT pattern_spec;
209 specs = intros_spec ->
210 let pattern = match pattern with
211 | None -> None, [], Some Ast.UserInput
212 | Some pattern -> pattern
214 GrafiteAst.Cases (loc, what, pattern, specs)
215 | IDENT "clear"; ids = LIST1 IDENT ->
216 GrafiteAst.Clear (loc, ids)
217 | IDENT "clearbody"; id = IDENT ->
218 GrafiteAst.ClearBody (loc,id)
219 | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
220 GrafiteAst.Change (loc, what, t)
221 | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 =
222 OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
223 let times = match times with None -> 1 | Some i -> i in
224 GrafiteAst.Compose (loc, t1, t2, times, specs)
225 | IDENT "constructor"; n = int ->
226 GrafiteAst.Constructor (loc, n)
227 | IDENT "contradiction" ->
228 GrafiteAst.Contradiction loc
229 | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
230 GrafiteAst.Cut (loc, ident, t)
231 | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
232 let idents = match idents with None -> [] | Some idents -> idents in
233 GrafiteAst.Decompose (loc, idents)
234 | IDENT "demodulate"; p = auto_params -> GrafiteAst.Demodulate (loc, p)
235 | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
236 GrafiteAst.Destruct (loc, xts)
237 | IDENT "elim"; what = tactic_term; using = using;
238 pattern = OPT pattern_spec;
239 ispecs = intros_spec ->
240 let pattern = match pattern with
241 | None -> None, [], Some Ast.UserInput
242 | Some pattern -> pattern
244 GrafiteAst.Elim (loc, what, using, pattern, ispecs)
245 | IDENT "elimType"; what = tactic_term; using = using;
246 (num, idents) = intros_spec ->
247 GrafiteAst.ElimType (loc, what, using, (num, idents))
248 | IDENT "exact"; t = tactic_term ->
249 GrafiteAst.Exact (loc, t)
251 GrafiteAst.Exists loc
252 | IDENT "fail" -> GrafiteAst.Fail loc
253 | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
256 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
257 ("the pattern cannot specify the term to replace, only its"
258 ^ " paths in the hypotheses and in the conclusion")))
260 GrafiteAst.Fold (loc, kind, t, p)
262 GrafiteAst.Fourier loc
263 | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
264 let idents = match idents with None -> [] | Some idents -> idents in
265 GrafiteAst.FwdSimpl (loc, hyp, idents)
266 | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
267 GrafiteAst.Generalize (loc,p,id)
268 | IDENT "id" -> GrafiteAst.IdTac loc
269 | IDENT "intro"; ident = OPT IDENT ->
270 let idents = match ident with None -> [] | Some id -> [Some id] in
271 GrafiteAst.Intros (loc, (Some 1, idents))
272 | IDENT "intros"; specs = intros_spec ->
273 GrafiteAst.Intros (loc, specs)
274 | IDENT "inversion"; t = tactic_term ->
275 GrafiteAst.Inversion (loc, t)
277 linear = OPT [ IDENT "linear" ];
278 depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
280 to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
281 ident = OPT [ "as" ; ident = IDENT -> ident ] ->
282 let linear = match linear with None -> false | Some _ -> true in
283 let to_what = match to_what with None -> [] | Some to_what -> to_what in
284 GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
285 | IDENT "left" -> GrafiteAst.Left loc
286 | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
287 GrafiteAst.LetIn (loc, t, where)
288 | kind = reduction_kind; p = pattern_spec ->
289 GrafiteAst.Reduce (loc, kind, p)
290 | IDENT "reflexivity" ->
291 GrafiteAst.Reflexivity loc
292 | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
293 GrafiteAst.Replace (loc, p, t)
294 | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
295 xnames = OPT [ "as"; n = ident_list0 -> n ] ->
299 (HExtlib.Localized (loc,
300 (CicNotationParser.Parse_error
301 "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
303 let n = match xnames with None -> [] | Some names -> names in
304 GrafiteAst.Rewrite (loc, d, t, p, n)
311 | IDENT "symmetry" ->
312 GrafiteAst.Symmetry loc
313 | IDENT "transitivity"; t = tactic_term ->
314 GrafiteAst.Transitivity (loc, t)
315 (* Produzioni Aggiunte *)
316 | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
317 GrafiteAst.Assume (loc, id, t)
318 | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ;
319 t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ;
320 t' = tactic_term -> t']->
321 GrafiteAst.Suppose (loc, t, id, t1)
322 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
323 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
324 id2 = IDENT ; RPAREN ->
325 GrafiteAst.ExistsElim (loc, `Auto ([],[]), id1, t1, id2, t2)
327 [ IDENT "using"; t=tactic_term -> `Term t
328 | params = auto_params -> `Auto params] ;
329 cont=by_continuation ->
331 BYC_done -> GrafiteAst.Bydone (loc, just)
332 | BYC_weproved (ty,id,t1) ->
333 GrafiteAst.By_just_we_proved(loc, just, ty, id, t1)
334 | BYC_letsuchthat (id1,t1,id2,t2) ->
335 GrafiteAst.ExistsElim (loc, just, id1, t1, id2, t2)
336 | BYC_wehaveand (id1,t1,id2,t2) ->
337 GrafiteAst.AndElim (loc, just, id1, t1, id2, t2))
338 | 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']->
339 GrafiteAst.We_need_to_prove (loc, t, id, t1)
340 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
341 GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
342 | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->
343 GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
344 | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
345 GrafiteAst.Byinduction(loc, t, id)
346 | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
347 GrafiteAst.Thesisbecomes(loc, t)
348 | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
349 SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
350 GrafiteAst.Case(loc,id,params)
351 (* DO NOT FACTORIZE with the two following, camlp5 sucks*)
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 (None,termine), t1, t2, cont)
363 | IDENT "obtain" ; name = IDENT;
364 termine = tactic_term;
368 [ IDENT "using"; t=tactic_term -> `Term t
369 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
370 | IDENT "proof" -> `Proof
371 | params = auto_params -> `Auto params];
372 cont = rewriting_step_continuation ->
373 GrafiteAst.RewritingStep(loc, Some (Some name,termine), t1, t2, cont)
377 [ IDENT "using"; t=tactic_term -> `Term t
378 | IDENT "using"; IDENT "once"; term=tactic_term -> `SolveWith term
379 | IDENT "proof" -> `Proof
380 | params = auto_params -> `Auto params];
381 cont = rewriting_step_continuation ->
382 GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
386 [ IDENT "paramodulation"
398 i = auto_fixed_param -> i,""
399 | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
400 string_of_int v | v = IDENT -> v ] -> i,v ];
401 tl = OPT [ IDENT "by"; tl = tactic_term_list1 -> tl] ->
402 (match tl with Some l -> l | None -> []),
407 [ 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)
408 | WEPROVED; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ;
409 "done" -> BYC_weproved (ty,None,t1)
411 | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
412 IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ;
413 id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
414 | WEHAVE; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
415 BYC_wehaveand (id1,t1,id2,t2)
418 rewriting_step_continuation : [
425 [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
428 | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
431 GrafiteAst.Seq (loc, ts)
434 [ tac = SELF; SYMBOL ";";
435 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
436 (GrafiteAst.Then (loc, tac, tacs))
439 [ IDENT "do"; count = int; tac = SELF ->
440 GrafiteAst.Do (loc, count, tac)
441 | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
445 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
446 GrafiteAst.First (loc, tacs)
447 | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
449 SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
450 GrafiteAst.Solve (loc, tacs)
451 | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
452 | LPAREN; tac = SELF; RPAREN -> tac
453 | tac = tactic -> tac
456 punctuation_tactical:
458 [ SYMBOL "[" -> GrafiteAst.Branch loc
459 | SYMBOL "|" -> GrafiteAst.Shift loc
460 | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
461 | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
462 | SYMBOL "]" -> GrafiteAst.Merge loc
463 | SYMBOL ";" -> GrafiteAst.Semicolon loc
464 | SYMBOL "." -> GrafiteAst.Dot loc
467 non_punctuation_tactical:
469 [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
470 | IDENT "unfocus" -> GrafiteAst.Unfocus loc
471 | IDENT "skip" -> GrafiteAst.Skip loc
475 [ [ IDENT "ntheorem" ] -> `Theorem
479 [ [ IDENT "definition" ] -> `Definition
480 | [ IDENT "fact" ] -> `Fact
481 | [ IDENT "lemma" ] -> `Lemma
482 | [ IDENT "remark" ] -> `Remark
483 | [ IDENT "theorem" ] -> `Theorem
487 [ attr = theorem_flavour -> attr
488 | [ IDENT "axiom" ] -> `Axiom
489 | [ IDENT "mutual" ] -> `MutualDefinition
494 params = LIST0 protected_binder_vars;
495 SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
496 fst_constructors = LIST0 constructor SEP SYMBOL "|";
499 name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
500 OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
501 (name, true, typ, constructors) ] SEP "with" -> types
505 (fun (names, typ) acc ->
506 (List.map (fun name -> (name, typ)) names) @ acc)
509 let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
510 let tl_ind_types = match tl with None -> [] | Some types -> types in
511 let ind_types = fst_ind_type :: tl_ind_types in
517 params = LIST0 protected_binder_vars;
518 SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ;
522 SYMBOL ":" -> false,0
523 | SYMBOL ":"; SYMBOL ">" -> true,0
524 | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
527 let b,n = coercion in
529 ] SEP SYMBOL ";"; SYMBOL "}" ->
532 (fun (names, typ) acc ->
533 (List.map (fun name -> (name, typ)) names) @ acc)
536 (params,name,typ,fields)
540 [ [ IDENT "check" ]; t = term ->
541 GrafiteAst.Check (loc, t)
542 | [ IDENT "eval" ]; kind = reduction_kind; "on"; t = tactic_term ->
543 GrafiteAst.Eval (loc, kind, t)
545 style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
546 suri = QSTRING; prefix = OPT QSTRING;
547 flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
548 let style = match style with
549 | None -> GrafiteAst.Declarative
550 | Some depth -> GrafiteAst.Procedural depth
552 let prefix = match prefix with None -> "" | Some prefix -> prefix in
553 GrafiteAst.Inline (loc,style,suri,prefix, flavour)
554 | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite") ->
555 if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
556 | IDENT "auto"; params = auto_params ->
557 GrafiteAst.AutoInteractive (loc,params)
558 | [ IDENT "whelp"; "match" ] ; t = term ->
559 GrafiteAst.WMatch (loc,t)
560 | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->
561 GrafiteAst.WInstance (loc,t)
562 | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING ->
563 GrafiteAst.WLocate (loc,id)
564 | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
565 GrafiteAst.WElim (loc, t)
566 | [ IDENT "whelp"; IDENT "hint" ] ; t = term ->
567 GrafiteAst.WHint (loc,t)
571 [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
572 let alpha = "[a-zA-Z]" in
573 let num = "[0-9]+" in
574 let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
575 let decoration = "\\'" in
576 let ident = "\\("^alpha^ident_cont^"*"^decoration^"*\\|_"^ident_cont^"+"^decoration^"*\\)" in
577 let rex = Str.regexp ("^"^ident^"$") in
578 if Str.string_match rex id 0 then
579 if (try ignore (UriManager.uri_of_string uri); true
580 with UriManager.IllFormedUri _ -> false)
582 LexiconAst.Ident_alias (id, uri)
585 (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
587 raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
588 Printf.sprintf "Not a valid identifier: %s" id)))
589 | IDENT "symbol"; symbol = QSTRING;
590 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
591 SYMBOL "="; dsc = QSTRING ->
593 match instance with Some i -> i | None -> 0
595 LexiconAst.Symbol_alias (symbol, instance, dsc)
597 instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
598 SYMBOL "="; dsc = QSTRING ->
600 match instance with Some i -> i | None -> 0
602 LexiconAst.Number_alias (instance, dsc)
606 [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
608 Ast.IdentArg (List.length l, id)
612 [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
613 | IDENT "right"; IDENT "associative" -> Gramext.RightA
614 | IDENT "non"; IDENT "associative" -> Gramext.NonA
618 [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
621 [ dir = OPT direction; s = QSTRING;
622 assoc = OPT associativity; prec = precedence;
625 [ blob = UNPARSED_AST ->
626 add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
627 (CicNotationParser.parse_level2_ast
628 (Ulexing.from_utf8_string blob))
629 | blob = UNPARSED_META ->
630 add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
631 (CicNotationParser.parse_level2_meta
632 (Ulexing.from_utf8_string blob))
636 | None -> default_associativity
637 | Some assoc -> assoc
640 add_raw_attribute ~text:s
641 (CicNotationParser.parse_level1_pattern prec
642 (Ulexing.from_utf8_string s))
644 (dir, p1, assoc, prec, p2)
648 [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
649 | id = IDENT -> Ast.VarPattern id
650 | SYMBOL "_" -> Ast.ImplicitPattern
651 | LPAREN; terms = LIST1 SELF; RPAREN ->
655 | terms -> Ast.ApplPattern terms)
659 [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
665 IDENT "include" ; path = QSTRING ->
666 loc,path,LexiconAst.WithPreferences
667 | IDENT "include'" ; path = QSTRING ->
668 loc,path,LexiconAst.WithoutPreferences
672 IDENT "set"; n = QSTRING; v = QSTRING ->
673 GrafiteAst.Set (loc, n, v)
674 | IDENT "drop" -> GrafiteAst.Drop loc
675 | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
676 | IDENT "qed" -> GrafiteAst.Qed loc
677 | IDENT "variant" ; name = IDENT; SYMBOL ":";
678 typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
681 (`Variant,name,typ,Some (Ast.Ident (newname, None))))
682 | nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
683 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
684 GrafiteAst.NObj (loc, Ast.Theorem (nflavour, name, typ, body))
685 | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
686 body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
687 GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
688 | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
691 Ast.Theorem (flavour, name, Ast.Implicit, Some body))
692 | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
693 GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
694 | LETCOREC ; defs = let_defs ->
695 mk_rec_corec `CoInductive defs loc
696 | LETREC ; defs = let_defs ->
697 mk_rec_corec `Inductive defs loc
698 | IDENT "inductive"; spec = inductive_spec ->
699 let (params, ind_types) = spec in
700 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
701 | IDENT "coinductive"; spec = inductive_spec ->
702 let (params, ind_types) = spec in
703 let ind_types = (* set inductive flags to false (coinductive) *)
704 List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
707 GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
709 t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
710 arity = OPT int ; saturations = OPT int;
711 composites = OPT (IDENT "nocomposites") ->
712 let arity = match arity with None -> 0 | Some x -> x in
713 let saturations = match saturations with None -> 0 | Some x -> x in
714 let composites = match composites with None -> true | Some _ -> false in
716 (loc, t, composites, arity, saturations)
717 | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
718 GrafiteAst.PreferCoercion (loc, t)
719 | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
720 GrafiteAst.UnificationHint (loc, t, n)
721 | IDENT "record" ; (params,name,ty,fields) = record_spec ->
722 GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
723 | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
724 let uris = List.map UriManager.uri_of_string uris in
725 GrafiteAst.Default (loc,what,uris)
726 | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
727 refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
728 refl = tactic_term -> refl ] ;
729 sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
730 sym = tactic_term -> sym ] ;
731 trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
732 trans = tactic_term -> trans ] ;
734 GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
737 IDENT "alias" ; spec = alias_spec ->
738 LexiconAst.Alias (loc, spec)
739 | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
740 LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
741 | IDENT "interpretation"; id = QSTRING;
742 (symbol, args, l3) = interpretation ->
743 LexiconAst.Interpretation (loc, id, (symbol, args), l3)
746 [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
747 | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
748 GrafiteAst.Tactic (loc, Some tac, punct)
749 | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
750 | tac = ntactic; punct = punctuation_tactical ->
751 GrafiteAst.NTactic (loc, tac, punct)
752 | SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
753 GrafiteAst.NTactic (loc, GrafiteAst.NId loc, punct)
754 | tac = non_punctuation_tactical; punct = punctuation_tactical ->
755 GrafiteAst.NonPunctuationTactical (loc, tac, punct)
756 | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
760 [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT ->
761 GrafiteAst.Code (loc, ex)
763 GrafiteAst.Note (loc, str)
768 fun ?(never_include=false) ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
770 fun ?(never_include=false) ~include_paths status ->
771 status,LSome (GrafiteAst.Comment (loc, com))
772 | (iloc,fname,mode) = include_command ; SYMBOL "." ->
774 fun ?(never_include=false) ~include_paths status ->
775 let _root, buri, fullpath, _rrelpath =
776 Librarian.baseuri_of_script ~include_paths fname
779 if never_include then raise (NoInclusionPerformed fullpath)
780 else LexiconEngine.eval_command status
781 (LexiconAst.Include (iloc,buri,mode,fullpath))
785 (GrafiteAst.Executable
786 (loc,GrafiteAst.Command
787 (loc,GrafiteAst.Include (iloc,buri))))
788 | scom = lexicon_command ; SYMBOL "." ->
789 fun ?(never_include=false) ~include_paths status ->
790 let status = LexiconEngine.eval_command status scom in
792 | EOI -> raise End_of_file
799 let _ = initialize_parser () ;;
801 let exc_located_wrapper f =
805 | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
806 | Stdpp.Exc_located (floc, Stream.Error msg) ->
807 raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
808 | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
810 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
811 | Stdpp.Exc_located (floc, exn) ->
813 (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
815 let parse_statement lexbuf =
817 (fun () -> (Grammar.Entry.parse !grafite_parser.statement (Obj.magic lexbuf)))
819 let statement () = !grafite_parser.statement
821 let history = ref [] ;;
825 history := !grafite_parser :: !history;
826 grafite_parser := initial_parser ();
835 grafite_parser := gp;
839 (* vim:set foldmethod=marker: *)