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