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