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