]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_parser/grafiteParser.ml
snapshot
[helm.git] / components / grafite_parser / grafiteParser.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 let out = ref ignore
29 let set_callback f = out := f
30
31 module Ast = CicNotationPt
32
33 type 'a localized_option =
34    LSome of 'a
35  | LNone of GrafiteAst.loc
36
37 type ast_statement =
38   (CicNotationPt.term, CicNotationPt.term,
39    CicNotationPt.term GrafiteAst.reduction, 
40    CicNotationPt.term CicNotationPt.obj, string)
41     GrafiteAst.statement
42
43 type statement =
44   include_paths:string list ->
45   LexiconEngine.status ->
46     LexiconEngine.status * ast_statement localized_option
47
48 let grammar = CicNotationParser.level2_ast_grammar
49
50 let term = CicNotationParser.term
51 let statement = Grammar.Entry.create grammar "statement"
52
53 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
54
55 let default_precedence = 50
56 let default_associativity = Gramext.NonA
57
58 type by_continuation =
59    BYC_done
60  | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option
61  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
62  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
63
64 EXTEND
65   GLOBAL: term statement;
66   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
67   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
68   new_name: [
69     [ id = IDENT -> Some id
70     | SYMBOL "_" -> None ]
71     ];
72   ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
73   tactic_term_list1: [
74     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
75   ];
76   reduction_kind: [
77     [ IDENT "normalize" -> `Normalize
78     | IDENT "reduce" -> `Reduce
79     | IDENT "simplify" -> `Simpl
80     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
81     | IDENT "whd" -> `Whd ]
82   ];
83   sequent_pattern_spec: [
84    [ hyp_paths =
85       LIST0
86        [ id = IDENT ;
87          path = OPT [SYMBOL ":" ; path = tactic_term -> path ] ->
88          (id,match path with Some p -> p | None -> Ast.UserInput) ];
89      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = tactic_term -> term ] ->
90       let goal_path =
91        match goal_path, hyp_paths with
92           None, [] -> Some Ast.UserInput
93         | None, _::_ -> None
94         | Some goal_path, _ -> Some goal_path
95       in
96        hyp_paths,goal_path
97    ]
98   ];
99   pattern_spec: [
100     [ res = OPT [
101        "in";
102        wanted_and_sps =
103         [ "match" ; wanted = tactic_term ;
104           sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] ->
105            Some wanted,sps
106         | sps = sequent_pattern_spec ->
107            None,Some sps
108         ] ->
109          let wanted,hyp_paths,goal_path =
110           match wanted_and_sps with
111              wanted,None -> wanted, [], Some Ast.UserInput
112            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
113          in
114           wanted, hyp_paths, goal_path ] ->
115       match res with
116          None -> None,[],Some Ast.UserInput
117        | Some ps -> ps]
118   ];
119   direction: [
120     [ SYMBOL ">" -> `LeftToRight
121     | SYMBOL "<" -> `RightToLeft ]
122   ];
123   int: [ [ num = NUMBER -> int_of_string num ] ];
124   intros_names: [
125    [ idents = OPT ident_list0 ->
126       match idents with None -> [] | Some idents -> idents
127    ]
128   ];
129   intros_spec: [
130     [ OPT [ IDENT "names" ]; 
131       num = OPT [ num = int -> num ]; 
132       idents = intros_names ->
133         num, idents
134     ]
135   ];
136   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
137   tactic: [
138     [ IDENT "absurd"; t = tactic_term ->
139         GrafiteAst.Absurd (loc, t)
140     | IDENT "apply"; t = tactic_term ->
141         GrafiteAst.Apply (loc, t)
142     | IDENT "applyS"; t = tactic_term ; params = 
143         LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
144           string_of_int v | v = IDENT -> v ] -> i,v ] ->
145         GrafiteAst.ApplyS (loc, t, params)
146     | IDENT "assumption" ->
147         GrafiteAst.Assumption loc
148     | IDENT "autobatch";  params = auto_params ->
149         GrafiteAst.AutoBatch (loc,params)
150     | IDENT "cases"; what = tactic_term;
151       specs = intros_spec ->
152         GrafiteAst.Cases (loc, what, specs)
153     | IDENT "clear"; ids = LIST1 IDENT ->
154         GrafiteAst.Clear (loc, ids)
155     | IDENT "clearbody"; id = IDENT ->
156         GrafiteAst.ClearBody (loc,id)
157     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
158         GrafiteAst.Change (loc, what, t)
159     | IDENT "compose"; times = OPT int; t1 = tactic_term; t2 = 
160       OPT [ "with"; t = tactic_term -> t ]; specs = intros_spec ->
161         let times = match times with None -> 1 | Some i -> i in
162         GrafiteAst.Compose (loc, t1, t2, times, specs)
163     | IDENT "constructor"; n = int ->
164         GrafiteAst.Constructor (loc, n)
165     | IDENT "contradiction" ->
166         GrafiteAst.Contradiction loc
167     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
168         GrafiteAst.Cut (loc, ident, t)
169     | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
170         let idents = match idents with None -> [] | Some idents -> idents in
171         GrafiteAst.Decompose (loc, idents)
172     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
173     | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] ->
174         GrafiteAst.Destruct (loc, xt)
175     | IDENT "elim"; what = tactic_term; using = using; 
176        pattern = OPT pattern_spec;
177        (num, idents) = intros_spec ->
178         let pattern = match pattern with
179            | None         -> None, [], Some Ast.UserInput
180            | Some pattern -> pattern   
181         in
182         GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
183     | IDENT "elimType"; what = tactic_term; using = using;
184       (num, idents) = intros_spec ->
185         GrafiteAst.ElimType (loc, what, using, (num, idents))
186     | IDENT "exact"; t = tactic_term ->
187         GrafiteAst.Exact (loc, t)
188     | IDENT "exists" ->
189         GrafiteAst.Exists loc
190     | IDENT "fail" -> GrafiteAst.Fail loc
191     | IDENT "fold"; kind = reduction_kind; t = tactic_term; p = pattern_spec ->
192         let (pt,_,_) = p in
193           if pt <> None then
194             raise (HExtlib.Localized (loc, CicNotationParser.Parse_error
195               ("the pattern cannot specify the term to replace, only its"
196               ^ " paths in the hypotheses and in the conclusion")))
197         else
198          GrafiteAst.Fold (loc, kind, t, p)
199     | IDENT "fourier" ->
200         GrafiteAst.Fourier loc
201     | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
202         let idents = match idents with None -> [] | Some idents -> idents in
203         GrafiteAst.FwdSimpl (loc, hyp, idents)
204     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
205        GrafiteAst.Generalize (loc,p,id)
206     | IDENT "id" -> GrafiteAst.IdTac loc
207     | IDENT "intro"; ident = OPT IDENT ->
208         let idents = match ident with None -> [] | Some id -> [Some id] in
209         GrafiteAst.Intros (loc, (Some 1, idents))
210     | IDENT "intros"; specs = intros_spec ->
211         GrafiteAst.Intros (loc, specs)
212     | IDENT "inversion"; t = tactic_term ->
213         GrafiteAst.Inversion (loc, t)
214     | IDENT "lapply"; 
215       linear = OPT [ IDENT "linear" ];
216       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
217       what = tactic_term; 
218       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
219       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
220         let linear = match linear with None -> false | Some _ -> true in 
221         let to_what = match to_what with None -> [] | Some to_what -> to_what in
222         GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
223     | IDENT "left" -> GrafiteAst.Left loc
224     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
225         GrafiteAst.LetIn (loc, t, where)
226     | kind = reduction_kind; p = pattern_spec ->
227         GrafiteAst.Reduce (loc, kind, p)
228     | IDENT "reflexivity" ->
229         GrafiteAst.Reflexivity loc
230     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
231         GrafiteAst.Replace (loc, p, t)
232     | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
233        xnames = OPT [ "as"; n = ident_list0 -> n ] ->
234        let (pt,_,_) = p in
235         if pt <> None then
236          raise
237           (HExtlib.Localized (loc,
238            (CicNotationParser.Parse_error
239             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
240         else
241          let n = match xnames with None -> [] | Some names -> names in 
242          GrafiteAst.Rewrite (loc, d, t, p, n)
243     | IDENT "right" ->
244         GrafiteAst.Right loc
245     | IDENT "ring" ->
246         GrafiteAst.Ring loc
247     | IDENT "split" ->
248         GrafiteAst.Split loc
249     | IDENT "symmetry" ->
250         GrafiteAst.Symmetry loc
251     | IDENT "transitivity"; t = tactic_term ->
252         GrafiteAst.Transitivity (loc, t)
253      (* Produzioni Aggiunte *)
254     | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
255         GrafiteAst.Assume (loc, id, t)
256     | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t' = tactic_term -> t']->
257         GrafiteAst.Suppose (loc, t, id, t1)
258     | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
259       cont=by_continuation ->
260        let t' = match t with LNone _ -> None | LSome t -> Some t in
261        (match cont with
262            BYC_done -> GrafiteAst.Bydone (loc, t')
263          | BYC_weproved (ty,id,t1) ->
264             GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
265          | BYC_letsuchthat (id1,t1,id2,t2) ->
266            (* (match t with
267                 LNone floc ->
268                  raise (HExtlib.Localized
269                   (floc,CicNotationParser.Parse_error
270                     "tactic_term expected here"))
271               | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
272          | BYC_wehaveand (id1,t1,id2,t2) ->
273             (match t with
274                 LNone floc ->
275                  raise (HExtlib.Localized
276                   (floc,CicNotationParser.Parse_error
277                     "tactic_term expected here"))
278               | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
279     | 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']->
280         GrafiteAst.We_need_to_prove (loc, t, id, t1)
281     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "cases" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
282         GrafiteAst.We_proceed_by_cases_on (loc, t, t1)
283     | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
284         GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
285     | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
286         GrafiteAst.Byinduction(loc, t, id)
287     | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
288         GrafiteAst.Thesisbecomes(loc, t)
289     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
290         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
291          GrafiteAst.Case(loc,id,params)
292     | start =
293        [ IDENT "conclude" -> None
294        | IDENT "obtain" ; name = IDENT -> Some name ] ;
295       termine = tactic_term ;
296       SYMBOL "=" ;
297       t1=tactic_term ;
298       IDENT "by" ;
299       t2 =
300        [ t=tactic_term -> `Term t
301        | SYMBOL "_" ; params = auto_params' -> `Auto params
302        | IDENT "proof" -> `Proof] ;
303       cont = rewriting_step_continuation ->
304        GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
305     | SYMBOL "=" ;
306       t1=tactic_term ;
307       IDENT "by" ;
308       t2=
309        [ t=tactic_term -> `Term t
310        | SYMBOL "_" ; params = auto_params' -> `Auto params
311        | IDENT "proof" -> `Proof] ;
312       cont=rewriting_step_continuation ->
313        GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
314   ]
315 ];
316   auto_params: [
317    [ params =
318       LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
319        string_of_int v | v = IDENT -> v ] -> i,v ] ->
320       params
321    ]
322 ];
323   auto_params': [
324    [ LPAREN; params = auto_params; RPAREN -> params
325    | -> []
326    ]
327 ];
328   by_continuation: [
329     [ IDENT "we" ; IDENT "proved" ; 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)
330     | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; 
331             IDENT "done" -> BYC_weproved (ty,None,t1)
332     | IDENT "done" -> BYC_done
333     | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
334       IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ; RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
335     | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;"and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
336               BYC_wehaveand (id1,t1,id2,t2)
337     ]
338 ];
339   rewriting_step_continuation : [
340     [ IDENT "done" -> true
341     | -> false
342     ]
343 ];
344   atomic_tactical:
345     [ "sequence" LEFTA
346       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
347           let ts =
348             match t1 with
349             | GrafiteAst.Seq (_, l) -> l @ [ t2 ]
350             | _ -> [ t1; t2 ]
351           in
352           GrafiteAst.Seq (loc, ts)
353       ]
354     | "then" NONA
355       [ tac = SELF; SYMBOL ";";
356         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
357           (GrafiteAst.Then (loc, tac, tacs))
358       ]
359     | "loops" RIGHTA
360       [ IDENT "do"; count = int; tac = SELF ->
361           GrafiteAst.Do (loc, count, tac)
362       | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
363       ]
364     | "simple" NONA
365       [ IDENT "first";
366         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
367           GrafiteAst.First (loc, tacs)
368       | IDENT "try"; tac = SELF -> GrafiteAst.Try (loc, tac)
369       | IDENT "solve";
370         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
371           GrafiteAst.Solve (loc, tacs)
372       | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
373       | LPAREN; tac = SELF; RPAREN -> tac
374       | tac = tactic -> tac
375       ]
376     ];
377   punctuation_tactical:
378     [
379       [ SYMBOL "[" -> GrafiteAst.Branch loc
380       | SYMBOL "|" -> GrafiteAst.Shift loc
381       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
382       | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
383       | SYMBOL "]" -> GrafiteAst.Merge loc
384       | SYMBOL ";" -> GrafiteAst.Semicolon loc
385       | SYMBOL "." -> GrafiteAst.Dot loc
386       ]
387     ];
388   non_punctuation_tactical:
389     [ "simple" NONA
390       [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
391       | IDENT "unfocus" -> GrafiteAst.Unfocus loc
392       | IDENT "skip" -> GrafiteAst.Skip loc
393       ]
394     ];
395   theorem_flavour: [
396     [ [ IDENT "definition"  ] -> `Definition
397     | [ IDENT "fact"        ] -> `Fact
398     | [ IDENT "lemma"       ] -> `Lemma
399     | [ IDENT "remark"      ] -> `Remark
400     | [ IDENT "theorem"     ] -> `Theorem
401     ]
402   ];
403   inductive_spec: [ [
404     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
405     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
406     fst_constructors = LIST0 constructor SEP SYMBOL "|";
407     tl = OPT [ "with";
408       types = LIST1 [
409         name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>;
410        OPT SYMBOL "|"; constructors = LIST0 constructor SEP SYMBOL "|" ->
411           (name, true, typ, constructors) ] SEP "with" -> types
412     ] ->
413       let params =
414         List.fold_right
415           (fun (names, typ) acc ->
416             (List.map (fun name -> (name, typ)) names) @ acc)
417           params []
418       in
419       let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
420       let tl_ind_types = match tl with None -> [] | Some types -> types in
421       let ind_types = fst_ind_type :: tl_ind_types in
422       (params, ind_types)
423   ] ];
424   
425   record_spec: [ [
426     name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
427      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
428      fields = LIST0 [ 
429        name = IDENT ; 
430        coercion = [ 
431            SYMBOL ":" -> false,0 
432          | SYMBOL ":"; SYMBOL ">" -> true,0
433          | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
434        ]; 
435        ty = term -> 
436          let b,n = coercion in 
437          (name,ty,b,n) 
438      ] SEP SYMBOL ";"; SYMBOL "}" -> 
439       let params =
440         List.fold_right
441           (fun (names, typ) acc ->
442             (List.map (fun name -> (name, typ)) names) @ acc)
443           params []
444       in
445       (params,name,typ,fields)
446   ] ];
447   
448   macro: [
449     [ [ IDENT "check"   ]; t = term ->
450         GrafiteAst.Check (loc, t)
451     | [ IDENT "inline"]; 
452         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
453         suri = QSTRING; prefix = OPT QSTRING ->
454          let style = match style with 
455             | None       -> GrafiteAst.Declarative
456             | Some depth -> GrafiteAst.Procedural depth
457          in
458          let prefix = match prefix with None -> "" | Some prefix -> prefix in
459          GrafiteAst.Inline (loc,style,suri,prefix)
460     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
461          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
462     | IDENT "auto"; params = auto_params ->
463         GrafiteAst.AutoInteractive (loc,params)
464     | [ IDENT "whelp"; "match" ] ; t = term -> 
465         GrafiteAst.WMatch (loc,t)
466     | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
467         GrafiteAst.WInstance (loc,t)
468     | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
469         GrafiteAst.WLocate (loc,id)
470     | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
471         GrafiteAst.WElim (loc, t)
472     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
473         GrafiteAst.WHint (loc,t)
474     ]
475   ];
476   alias_spec: [
477     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
478       let alpha = "[a-zA-Z]" in
479       let num = "[0-9]+" in
480       let ident_cont = "\\("^alpha^"\\|"^num^"\\|_\\|\\\\\\)" in
481       let ident = "\\("^alpha^ident_cont^"*\\|_"^ident_cont^"+\\)" in
482       let rex = Str.regexp ("^"^ident^"$") in
483       if Str.string_match rex id 0 then
484         if (try ignore (UriManager.uri_of_string uri); true
485             with UriManager.IllFormedUri _ -> false)
486         then
487           LexiconAst.Ident_alias (id, uri)
488         else 
489           raise
490            (HExtlib.Localized (loc, CicNotationParser.Parse_error (Printf.sprintf "Not a valid uri: %s" uri)))
491       else
492         raise (HExtlib.Localized (loc, CicNotationParser.Parse_error (
493           Printf.sprintf "Not a valid identifier: %s" id)))
494     | IDENT "symbol"; symbol = QSTRING;
495       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
496       SYMBOL "="; dsc = QSTRING ->
497         let instance =
498           match instance with Some i -> i | None -> 0
499         in
500         LexiconAst.Symbol_alias (symbol, instance, dsc)
501     | IDENT "num";
502       instance = OPT [ LPAREN; IDENT "instance"; n = int; RPAREN -> n ];
503       SYMBOL "="; dsc = QSTRING ->
504         let instance =
505           match instance with Some i -> i | None -> 0
506         in
507         LexiconAst.Number_alias (instance, dsc)
508     ]
509   ];
510   argument: [
511     [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
512       id = IDENT ->
513         Ast.IdentArg (List.length l, id)
514     ]
515   ];
516   associativity: [
517     [ IDENT "left";  IDENT "associative" -> Gramext.LeftA
518     | IDENT "right"; IDENT "associative" -> Gramext.RightA
519     | IDENT "non"; IDENT "associative" -> Gramext.NonA
520     ]
521   ];
522   precedence: [
523     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
524   ];
525   notation: [
526     [ dir = OPT direction; s = QSTRING;
527       assoc = OPT associativity; prec = OPT precedence;
528       IDENT "for";
529       p2 = 
530         [ blob = UNPARSED_AST ->
531             add_raw_attribute ~text:(Printf.sprintf "@{%s}" blob)
532               (CicNotationParser.parse_level2_ast
533                 (Ulexing.from_utf8_string blob))
534         | blob = UNPARSED_META ->
535             add_raw_attribute ~text:(Printf.sprintf "${%s}" blob)
536               (CicNotationParser.parse_level2_meta
537                 (Ulexing.from_utf8_string blob))
538         ] ->
539           let assoc =
540             match assoc with
541             | None -> default_associativity
542             | Some assoc -> assoc
543           in
544           let prec =
545             match prec with
546             | None -> default_precedence
547             | Some prec -> prec
548           in
549           let p1 =
550             add_raw_attribute ~text:s
551               (CicNotationParser.parse_level1_pattern
552                 (Ulexing.from_utf8_string s))
553           in
554           (dir, p1, assoc, prec, p2)
555     ]
556   ];
557   level3_term: [
558     [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
559     | id = IDENT -> Ast.VarPattern id
560     | SYMBOL "_" -> Ast.ImplicitPattern
561     | LPAREN; terms = LIST1 SELF; RPAREN ->
562         (match terms with
563         | [] -> assert false
564         | [term] -> term
565         | terms -> Ast.ApplPattern terms)
566     ]
567   ];
568   interpretation: [
569     [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
570         (s, args, t)
571     ]
572   ];
573   
574   include_command: [ [
575       IDENT "include" ; path = QSTRING -> 
576         loc,path,LexiconAst.WithPreferences
577     | IDENT "include'" ; path = QSTRING -> 
578         loc,path,LexiconAst.WithoutPreferences
579    ]];
580
581   grafite_command: [ [
582       IDENT "set"; n = QSTRING; v = QSTRING ->
583         GrafiteAst.Set (loc, n, v)
584     | IDENT "drop" -> GrafiteAst.Drop loc
585     | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
586     | IDENT "qed" -> GrafiteAst.Qed loc
587     | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
588       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
589         GrafiteAst.Obj (loc, 
590           Ast.Theorem 
591             (`Variant,name,typ,Some (Ast.Ident (newname, None))))
592     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
593       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
594         GrafiteAst.Obj (loc, Ast.Theorem (flavour, name, typ, body))
595     | flavour = theorem_flavour; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *);
596       body = term ->
597         GrafiteAst.Obj (loc,
598           Ast.Theorem (flavour, name, Ast.Implicit, Some body))
599     | IDENT "axiom"; name = IDENT; SYMBOL ":"; typ = term ->
600         GrafiteAst.Obj (loc, Ast.Theorem (`Axiom, name, typ, None))
601     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
602         defs = CicNotationParser.let_defs -> 
603          (* In case of mutual definitions here we produce just
604             the syntax tree for the first one. The others will be
605             generated from the completely specified term just before
606             insertion in the environment. We use the flavour
607             `MutualDefinition to rememer this. *)
608           let name,ty = 
609             match defs with
610             | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
611                 let ty =
612                  List.fold_right
613                   (fun var ty -> Ast.Binder (`Pi,var,ty)
614                   ) params ty
615                 in
616                  name,ty
617             | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
618                 name, Ast.Implicit
619             | _ -> assert false 
620           in
621           let body = Ast.Ident (name,None) in
622           let flavour =
623            if List.length defs = 1 then
624             `Definition
625            else
626             `MutualDefinition
627           in
628            GrafiteAst.Obj (loc, Ast.Theorem(flavour, name, ty,
629              Some (Ast.LetRec (ind_kind, defs, body))))
630     | IDENT "inductive"; spec = inductive_spec ->
631         let (params, ind_types) = spec in
632         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
633     | IDENT "coinductive"; spec = inductive_spec ->
634         let (params, ind_types) = spec in
635         let ind_types = (* set inductive flags to false (coinductive) *)
636           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
637             ind_types
638         in
639         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
640     | IDENT "coercion" ; suri = URI ; arity = OPT int ; saturations = OPT int ->
641         let arity = match arity with None -> 0 | Some x -> x in
642         let saturations = match saturations with None -> 0 | Some x -> x in
643         GrafiteAst.Coercion
644          (loc, UriManager.uri_of_string suri, true, arity, saturations)
645     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
646         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
647     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
648        let uris = List.map UriManager.uri_of_string uris in
649         GrafiteAst.Default (loc,what,uris)
650     | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
651       refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
652                    refl = tactic_term -> refl ] ;
653       sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
654                    sym = tactic_term -> sym ] ;
655       trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
656                    trans = tactic_term -> trans ] ;
657       "as" ; id = IDENT ->
658        GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
659   ]];
660   lexicon_command: [ [
661       IDENT "alias" ; spec = alias_spec ->
662         LexiconAst.Alias (loc, spec)
663     | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
664         LexiconAst.Notation (loc, dir, l1, assoc, prec, l2)
665     | IDENT "interpretation"; id = QSTRING;
666       (symbol, args, l3) = interpretation ->
667         LexiconAst.Interpretation (loc, id, (symbol, args), l3)
668   ]];
669   executable: [
670     [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
671     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
672         GrafiteAst.Tactic (loc, Some tac, punct)
673     | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
674     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
675         GrafiteAst.NonPunctuationTactical (loc, tac, punct)
676     | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
677     ]
678   ];
679   comment: [
680     [ BEGINCOMMENT ; ex = executable ; ENDCOMMENT -> 
681        GrafiteAst.Code (loc, ex)
682     | str = NOTE -> 
683        GrafiteAst.Note (loc, str)
684     ]
685   ];
686   statement: [
687     [ ex = executable ->
688        fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex))
689     | com = comment ->
690        fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
691     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
692        fun ~include_paths status ->
693         let buri, fullpath = 
694           DependenciesParser.baseuri_of_script ~include_paths fname 
695         in
696         let status =
697          LexiconEngine.eval_command status 
698            (LexiconAst.Include (iloc,buri,mode,fullpath))
699         in
700          !out fname;
701          status,
702           LSome
703           (GrafiteAst.Executable
704            (loc,GrafiteAst.Command
705             (loc,GrafiteAst.Include (iloc,buri))))
706     | scom = lexicon_command ; SYMBOL "." ->
707        fun ~include_paths status ->
708         let status = LexiconEngine.eval_command status scom in
709          status,LNone loc
710     | EOI -> raise End_of_file
711     ]
712   ];
713 END
714
715 let exc_located_wrapper f =
716   try
717     f ()
718   with
719   | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
720   | Stdpp.Exc_located (floc, Stream.Error msg) ->
721       raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
722   | Stdpp.Exc_located (floc, exn) ->
723       raise
724        (HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
725
726 let parse_statement lexbuf =
727   exc_located_wrapper
728     (fun () -> (Grammar.Entry.parse statement (Obj.magic lexbuf)))