]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
new configure.ac with support for compile time configuration of termeditor/parser/...
[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualParser.mly
1 /* Copyright (C) 2000, 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://cs.unibo.it/helm/.
24  */
25
26 %{
27  open Cic;;
28  module U = UriManager;;
29
30  exception InvalidSuffix of string;;
31  exception InductiveTypeURIExpected;;
32  exception UnknownIdentifier of string;;
33  exception ExplicitNamedSubstitutionAppliedToRel;;
34  exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
35  
36  (* merge removing duplicates of two lists free of duplicates *)
37  let union dom1 dom2 =
38   let rec filter =
39    function
40       [] -> []
41     | he::tl ->
42        if List.mem he dom1 then filter tl else he::(filter tl)
43   in
44    dom1 @ (filter dom2)
45  ;;
46
47  let get_index_in_list e =
48   let rec aux i =
49    function
50       [] -> raise Not_found
51     | (Some he)::_ when he = e -> i
52     | _::tl -> aux (i+1) tl
53   in
54    aux 1
55  ;;
56
57  (* Returns the first meta whose number is above the *)
58  (* number of the higher meta.                       *)
59  (*CSC: cut&pasted from proofEngine.ml *)
60  let new_meta () =
61   let rec aux =
62    function
63       None,[] -> 1
64     | Some n,[] -> n
65     | None,(n,_,_)::tl -> aux (Some n,tl)
66     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
67   in
68    1 + aux (None,!TexCicTextualParser0.metasenv)
69  ;;
70
71  (* identity_relocation_list_for_metavariable i canonical_context         *)
72  (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
73  (* where n = List.length [canonical_context]                             *)
74  (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
75  (*CSC: cut&pasted from proofEngine.ml *)
76  let identity_relocation_list_for_metavariable canonical_context =
77   let canonical_context_length = List.length canonical_context in
78    let rec aux =
79     function
80        (_,[]) -> []
81      | (n,None::tl) -> None::(aux ((n+1),tl))
82      | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
83    in
84     aux (1,canonical_context)
85  ;;
86
87  let deoptionize_exp_named_subst =
88   function
89      None -> [], (function _ -> [])
90    | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
91  ;;
92
93  let term_of_con_uri uri exp_named_subst =
94   Const (uri,exp_named_subst)
95  ;;
96
97  let term_of_var_uri uri exp_named_subst =
98   Var (uri,exp_named_subst)
99  ;;
100
101  let term_of_indty_uri (uri,tyno) exp_named_subst =
102   MutInd (uri, tyno, exp_named_subst)
103  ;;
104
105  let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
106   MutConstruct (uri, tyno, consno, exp_named_subst)
107  ;;
108
109  let term_of_uri uri =
110   match uri with
111      CicTextualParser0.ConUri uri ->
112       term_of_con_uri uri
113    | CicTextualParser0.VarUri uri ->
114       term_of_var_uri uri
115    | CicTextualParser0.IndTyUri (uri,tyno) ->
116       term_of_indty_uri (uri,tyno) 
117    | CicTextualParser0.IndConUri (uri,tyno,consno) ->
118       term_of_indcon_uri (uri,tyno,consno)
119  ;;
120
121  let var_uri_of_id id interp =
122   let module CTP0 = CicTextualParser0 in
123    match interp (CicTextualParser0.Id id) with
124       None -> raise (UnknownIdentifier id)
125     | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
126     | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
127  ;;
128
129  let indty_uri_of_id id interp =
130   let module CTP0 = CicTextualParser0 in
131    match interp (CicTextualParser0.Id id) with
132       None -> raise (UnknownIdentifier id)
133     | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
134     | Some _ -> raise InductiveTypeURIExpected
135  ;;
136
137  let mk_implicit () =
138   let newmeta = new_meta () in
139    let new_canonical_context = [] in
140     let irl =
141      identity_relocation_list_for_metavariable new_canonical_context
142     in
143      TexCicTextualParser0.metasenv :=
144       [newmeta, new_canonical_context, Sort Type ;
145        newmeta+1, new_canonical_context, Meta (newmeta,irl);
146        newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
147       ] @ !TexCicTextualParser0.metasenv ;
148      [], function _ -> Meta (newmeta+2,irl)
149  ;;
150 %}
151 %token <string> ID
152 %token <int> META
153 %token <int> NUM
154 %token <int> RNUM
155 %token <UriManager.uri> CONURI
156 %token <UriManager.uri> VARURI
157 %token <UriManager.uri * int> INDTYURI
158 %token <UriManager.uri * int * int> INDCONURI
159 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
160 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
161 %token DOLLAR
162 %token RPLUS RMINUS RTIMES RDIV
163 %token PLUS MINUS TIMES EQT EQ NEQT
164 %right ARROW
165 %nonassoc EQ EQT NEQT
166 %left PLUS MINUS RPLUS RMINUS
167 %left TIMES RTIMES RDIV
168 %start main
169 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
170 %%
171 main:
172  | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
173  | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
174  | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
175  | expr EOF { $1 }
176  | DOLLAR expr DOLLAR EOF { $2 }
177  | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 }
178  | expr SEMICOLON { $1 } /*  FG: to read several terms in a row
179                           *  Do we need to clear some static variables? 
180                           */
181 ;
182 expr2:
183  | RNUM
184    { [], function interp ->
185       let rec cic_real_of_real =
186        function
187           0 ->
188            Cic.Const
189             (UriManager.uri_of_string
190               "cic:/Coq/Reals/Rdefinitions/R0.con",[])
191         | 1 ->
192            Cic.Const
193             (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con",[])
194         | n ->
195           Cic.Appl
196            [ Cic.Const
197                (UriManager.uri_of_string
198                   "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
199              Cic.Const (UriManager.uri_of_string
200               "cic:/Coq/Reals/Rdefinitions/R1.con",[]);
201              cic_real_of_real (n - 1)
202            ]
203       in
204        cic_real_of_real $1
205    }
206  | NUM
207    { [], function interp ->
208       let rec cic_int_of_int =
209        function
210           0 ->
211            Cic.MutConstruct
212             (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
213              0,1,[])
214         | n ->
215           Cic.Appl
216            [ Cic.MutConstruct
217               (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
218                0,2,[]) ;
219              cic_int_of_int (n - 1)
220            ]
221       in
222        cic_int_of_int $1
223    }
224  | expr2 RPLUS expr2
225    { let dom1,mk_expr1 = $1 in
226      let dom2,mk_expr2 = $3 in
227       let dom = union dom1 dom2 in
228        dom, function interp ->
229         Cic.Appl
230          [Cic.Const
231            (UriManager.uri_of_string
232               "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
233           (mk_expr1 interp) ;
234           (mk_expr2 interp)
235          ]
236    }
237  | expr2 RMINUS expr2
238    { let dom1,mk_expr1 = $1 in
239      let dom2,mk_expr2 = $3 in
240       let dom = union dom1 dom2 in
241        dom, function interp ->
242         Cic.Appl
243          [Cic.Const
244            (UriManager.uri_of_string
245               "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ;
246           (mk_expr1 interp) ;
247           (mk_expr2 interp)
248          ]
249    }
250  | expr2 RTIMES expr2
251    { let dom1,mk_expr1 = $1 in
252      let dom2,mk_expr2 = $3 in
253       let dom = union dom1 dom2 in
254        dom, function interp ->
255         Cic.Appl
256          [Cic.Const
257            (UriManager.uri_of_string
258               "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ;
259           (mk_expr1 interp) ;
260           (mk_expr2 interp)
261          ]
262    }
263  | expr2 RDIV expr2
264    { let dom1,mk_expr1 = $1 in
265      let dom2,mk_expr2 = $3 in
266       let dom = union dom1 dom2 in
267        dom, function interp ->
268         Cic.Appl
269          [Cic.Const
270            (UriManager.uri_of_string
271               "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ;
272           (mk_expr1 interp) ;
273           (mk_expr2 interp)
274          ]
275    }
276  | expr2 PLUS expr2
277    { let dom1,mk_expr1 = $1 in
278      let dom2,mk_expr2 = $3 in
279       let dom = union dom1 dom2 in
280        dom, function interp ->
281         Cic.Appl
282          [Cic.Const
283            (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
284           (mk_expr1 interp) ;
285           (mk_expr2 interp)
286          ]
287    }
288  | expr2 MINUS expr2
289    { let dom1,mk_expr1 = $1 in
290      let dom2,mk_expr2 = $3 in
291       let dom = union dom1 dom2 in
292        dom, function interp ->
293         Cic.Appl
294          [Cic.Const
295            (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
296           (mk_expr1 interp) ;
297           (mk_expr2 interp)
298          ]
299    }
300  | expr2 TIMES expr2
301    { let dom1,mk_expr1 = $1 in
302      let dom2,mk_expr2 = $3 in
303       let dom = union dom1 dom2 in
304        dom, function interp ->
305         Cic.Appl
306          [Cic.Const
307            (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
308           (mk_expr1 interp) ;
309           (mk_expr2 interp)
310          ]
311    }
312  | expr2 EQT expr2
313    { let dom1,mk_expr1 = $1 in
314      let dom2,mk_expr2 = $3 in
315      let dom3,mk_expr3 = mk_implicit () in
316       let dom = union dom1 (union dom2 dom3) in
317        dom, function interp ->
318         Cic.Appl
319          [Cic.MutInd
320            (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
321           (mk_expr3 interp) ;
322           (mk_expr1 interp) ;
323           (mk_expr2 interp)
324          ]
325    }
326  | expr2 NEQT expr2
327    { let dom1,mk_expr1 = $1 in
328      let dom2,mk_expr2 = $3 in
329      let dom3,mk_expr3 = mk_implicit () in
330       let dom = union dom1 (union dom2 dom3) in
331        dom, function interp ->
332         Cic.Appl [
333          Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]);
334          Cic.Appl
335           [Cic.MutInd
336             (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
337            (mk_expr3 interp) ;
338            (mk_expr1 interp) ;
339            (mk_expr2 interp)
340           ]]
341    }
342  | expr2 EQ expr2
343    { let dom1,mk_expr1 = $1 in
344      let dom2,mk_expr2 = $3 in
345      let dom3,mk_expr3 = mk_implicit () in
346       let dom = union dom1 (union dom2 dom3) in
347        dom, function interp ->
348         Cic.Appl
349          [Cic.MutInd
350            (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
351           (mk_expr3 interp) ;
352           (mk_expr1 interp) ;
353           (mk_expr2 interp)
354          ]
355    }
356  | CONURI exp_named_subst
357    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
358       dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
359    }
360  | VARURI exp_named_subst
361    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
362       dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
363    }
364  | INDTYURI exp_named_subst
365    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
366       dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
367    }
368  | INDCONURI exp_named_subst
369    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
370       dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
371    }
372  | ID exp_named_subst
373    { try
374       let res =
375        Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders)
376       in
377        (match $2 with
378            None -> ([], function _ -> res)
379          | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
380        )
381      with
382       Not_found ->
383        let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
384         let dom = union dom1 [CicTextualParser0.Id $1] in
385          dom,
386           function interp ->
387            match interp (CicTextualParser0.Id $1) with
388               None  -> raise (UnknownIdentifier $1)
389             | Some (CicTextualParser0.Uri uri) ->
390                term_of_uri uri (mk_exp_named_subst interp)
391             | Some CicTextualParser0.Implicit ->
392                (*CSC: not very clean; to maximize code reusage *)
393                snd (mk_implicit ()) ""
394             | Some (CicTextualParser0.Term mk_term) ->
395                (mk_term interp)
396    }
397  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
398     { let dom1,mk_expr1 = $3 in
399       let dom2,mk_expr2 = $7 in
400       let dom3,mk_expr3 = $10 in
401        let dom = union dom1 (union dom2 dom3) in
402         dom,
403         function interp ->
404          MutCase
405           (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
406     }
407  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
408     { let dom1,mk_expr1 = $3 in
409       let dom2,mk_expr2 = $7 in
410       let dom3,mk_expr3 = $10 in
411        let dom =
412         union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3))
413        in
414         dom,
415         function interp ->
416          let uri,typeno = indty_uri_of_id $5 interp in
417           MutCase
418            (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
419              (mk_expr3 interp))
420     }
421  | fixheader LCURLY exprseplist RCURLY
422     { let dom1,foo,ids_and_indexes,mk_types = $1 in
423       let dom2,mk_exprseplist = $3 in
424        let dom = union dom1 dom2 in
425         for i = 1 to List.length ids_and_indexes do
426          TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders
427         done ;
428         dom,
429          function interp ->
430           let types = mk_types interp in
431           let fixfunsbodies = (mk_exprseplist interp) in
432            let idx =
433             let rec find idx =
434              function
435                 [] -> raise Not_found
436               | (name,_)::_  when name = foo -> idx
437               | _::tl -> find (idx+1) tl
438             in
439              find 0 ids_and_indexes
440            in
441             let fixfuns =
442              List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
443               (List.combine ids_and_indexes types) fixfunsbodies
444             in
445              Fix (idx,fixfuns)
446     }
447  | cofixheader LCURLY exprseplist RCURLY
448     { let dom1,foo,ids,mk_types = $1 in
449       let dom2,mk_exprseplist = $3 in
450        let dom = union dom1 dom2 in
451         dom,
452          function interp ->
453           let types = mk_types interp in
454           let fixfunsbodies = (mk_exprseplist interp) in
455            let idx =
456             let rec find idx =
457              function
458                 [] -> raise Not_found
459               | name::_  when name = foo -> idx
460               | _::tl -> find (idx+1) tl
461             in
462              find 0 ids
463            in
464             let fixfuns =
465              List.map2 (fun (name,ty) bo -> (name,ty,bo))
466               (List.combine ids types) fixfunsbodies
467             in
468              for i = 1 to List.length fixfuns do
469               TexCicTextualParser0.binders :=
470                List.tl !TexCicTextualParser0.binders
471              done ;
472              CoFix (idx,fixfuns)
473     }
474  | IMPLICIT
475     { mk_implicit () }
476  | SET   { [], function _ -> Sort Set }
477  | PROP  { [], function _ -> Sort Prop }
478  | TYPE  { [], function _ -> Sort Type }
479  | CPROP { [], function _ -> Sort CProp }
480  | LPAREN expr CAST expr RPAREN
481     { let dom1,mk_expr1 = $2 in
482       let dom2,mk_expr2 = $4 in
483        let dom = union dom1 dom2 in
484         dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
485     }
486  | META LBRACKET substitutionlist RBRACKET
487     { let dom,mk_substitutionlist = $3 in
488        dom, function interp -> Meta ($1, mk_substitutionlist interp)
489     } 
490  | LPAREN expr exprlist RPAREN
491     { let length,dom2,mk_exprlist = $3 in
492        match length with
493           0 -> $2
494         | _ ->
495           let dom1,mk_expr1 = $2 in
496            let dom = union dom1 dom2 in
497             dom,
498              function interp ->
499               Appl ((mk_expr1 interp)::(mk_exprlist interp))
500     }
501 ;
502 exp_named_subst :
503     { None }
504  | LCURLY named_substs RCURLY
505     { Some $2 }
506 ;
507 named_substs :
508    VARURI LETIN expr2
509     { let dom,mk_expr = $3 in
510        dom, function interp -> [$1, mk_expr interp] }
511  | ID LETIN expr2
512     { let dom1,mk_expr = $3 in
513        let dom = union [CicTextualParser0.Id $1] dom1 in
514         dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
515  | VARURI LETIN expr2 SEMICOLON named_substs
516     { let dom1,mk_expr = $3 in
517       let dom2,mk_named_substs = $5 in
518        let dom = union dom1 dom2 in
519         dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
520     }
521  | ID LETIN expr2 SEMICOLON named_substs
522     { let dom1,mk_expr = $3 in
523       let dom2,mk_named_substs = $5 in
524        let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
525         dom,
526          function interp ->
527           (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
528     }
529 ;
530 expr :
531    pihead expr
532     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
533       let dom1,mk_expr1 = snd $1 in
534       let dom2,mk_expr2 = $2 in
535        let dom = union dom1 dom2 in
536         dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
537     }
538  | lambdahead expr
539     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
540       let dom1,mk_expr1 = snd $1 in
541       let dom2,mk_expr2 = $2 in
542        let dom = union dom1 dom2 in
543         dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
544     }
545  | letinhead expr
546     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
547       let dom1,mk_expr1 = snd $1 in
548       let dom2,mk_expr2 = $2 in
549        let dom = union dom1 dom2 in
550         dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
551     }
552  | expr2
553     { $1 }
554 ;
555 fixheader:
556    FIX ID LCURLY fixfunsdecl RCURLY
557     { let dom,ids_and_indexes,mk_types = $4 in
558        let bs =
559         List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
560        in
561         TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
562         dom, $2, ids_and_indexes, mk_types
563     }
564 ;
565 fixfunsdecl:
566    ID LPAREN NUM RPAREN COLON expr
567     { let dom,mk_expr = $6 in
568        dom, [$1,$3], function interp -> [mk_expr interp]
569     }
570  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
571     { let dom1,mk_expr = $6 in
572       let dom2,ids_and_indexes,mk_types = $8 in
573        let dom = union dom1 dom2 in
574         dom, ($1,$3)::ids_and_indexes,
575          function interp -> (mk_expr interp)::(mk_types interp)
576     }
577 ;
578 cofixheader:
579    COFIX ID LCURLY cofixfunsdecl RCURLY
580     { let dom,ids,mk_types = $4 in
581        let bs =
582         List.rev_map (function name -> Some (Name name)) ids
583        in
584         TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
585         dom, $2, ids, mk_types
586     }
587 ;
588 cofixfunsdecl:
589    ID COLON expr
590     { let dom,mk_expr = $3 in
591        dom, [$1], function interp -> [mk_expr interp]
592     }
593  | ID COLON expr SEMICOLON cofixfunsdecl
594     { let dom1,mk_expr = $3 in
595       let dom2,ids,mk_types = $5 in
596        let dom = union dom1 dom2 in
597         dom, $1::ids,
598          function interp -> (mk_expr interp)::(mk_types interp)
599     }
600 ;
601 pihead:
602    PROD ID COLON expr DOT
603     { TexCicTextualParser0.binders :=
604        (Some (Name $2))::!TexCicTextualParser0.binders;
605       let dom,mk_expr = $4 in
606        Cic.Name $2, (dom, function interp -> mk_expr interp)
607     }
608  | expr2 ARROW
609    { TexCicTextualParser0.binders :=
610       (Some Anonymous)::!TexCicTextualParser0.binders ;
611      let dom,mk_expr = $1 in
612       Anonymous, (dom, function interp -> mk_expr interp)
613    }
614  | PROD ID DOT
615     { TexCicTextualParser0.binders :=
616        (Some (Name $2))::!TexCicTextualParser0.binders;
617       let newmeta = new_meta () in
618        let new_canonical_context = [] in
619         let irl =
620          identity_relocation_list_for_metavariable new_canonical_context
621         in
622          TexCicTextualParser0.metasenv :=
623           [newmeta, new_canonical_context, Sort Type ;
624            newmeta+1, new_canonical_context, Meta (newmeta,irl)
625           ] @ !TexCicTextualParser0.metasenv ;
626          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
627     }
628 ;
629 lambdahead:
630    LAMBDA ID COLON expr DOT
631     { TexCicTextualParser0.binders :=
632        (Some (Name $2))::!TexCicTextualParser0.binders;
633       let dom,mk_expr = $4 in
634        Cic.Name $2, (dom, function interp -> mk_expr interp)
635     }
636  | LAMBDA ID DOT
637     { TexCicTextualParser0.binders :=
638        (Some (Name $2))::!TexCicTextualParser0.binders;
639       let newmeta = new_meta () in
640        let new_canonical_context = [] in
641         let irl =
642          identity_relocation_list_for_metavariable new_canonical_context
643         in
644          TexCicTextualParser0.metasenv :=
645           [newmeta, new_canonical_context, Sort Type ;
646            newmeta+1, new_canonical_context, Meta (newmeta,irl)
647           ] @ !TexCicTextualParser0.metasenv ;
648          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
649     }
650 ;
651 letinhead:
652   LAMBDA ID LETIN expr DOT
653    { TexCicTextualParser0.binders :=
654       (Some (Name $2))::!TexCicTextualParser0.binders ;
655      let dom,mk_expr = $4 in
656       Cic.Name $2, (dom, function interp -> mk_expr interp)
657    }
658 ;
659 branches:
660     { [], function _ -> [] }
661  | expr SEMICOLON branches
662     { let dom1,mk_expr = $1 in
663       let dom2,mk_branches = $3 in
664        let dom = union dom1 dom2 in
665         dom, function interp -> (mk_expr interp)::(mk_branches interp)
666     }
667  | expr
668     { let dom,mk_expr = $1 in
669        dom, function interp -> [mk_expr interp]
670     }
671 ;
672 exprlist:
673     
674     { 0, [], function _ -> [] }
675  | expr exprlist
676     { let dom1,mk_expr = $1 in
677       let length,dom2,mk_exprlist = $2 in
678        let dom = union dom1 dom2 in
679         length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
680     }
681 ;
682 exprseplist:
683    expr
684     { let dom,mk_expr = $1 in
685        dom, function interp -> [mk_expr interp]
686     }
687  | expr SEMICOLON exprseplist
688     { let dom1,mk_expr = $1 in
689       let dom2,mk_exprseplist = $3 in
690        let dom = union dom1 dom2 in
691         dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
692     }
693 ;
694 substitutionlist:
695     { [], function _ -> [] }
696  | expr SEMICOLON substitutionlist
697     { let dom1,mk_expr = $1 in
698       let dom2,mk_substitutionlist = $3 in
699        let dom = union dom1 dom2 in
700         dom,
701          function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
702     }
703  | NONE SEMICOLON substitutionlist
704     { let dom,mk_exprsubstitutionlist = $3 in
705        dom, function interp -> None::(mk_exprsubstitutionlist interp)
706     }