]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
added `Coer print_kind
[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 newuniv = CicUniv.fresh () in
140    let new_canonical_context = [] in
141     let irl =
142      identity_relocation_list_for_metavariable new_canonical_context
143     in
144      TexCicTextualParser0.metasenv :=
145       [newmeta, new_canonical_context, Sort (Type newuniv);
146        (* TASSI: ?? *)
147        newmeta+1, new_canonical_context, Meta (newmeta,irl);
148        newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
149       ] @ !TexCicTextualParser0.metasenv ;
150      [], function _ -> Meta (newmeta+2,irl)
151  ;;
152 %}
153 %token <string> ID
154 %token <int> META
155 %token <int> NUM
156 %token <int> RNUM
157 %token <UriManager.uri> CONURI
158 %token <UriManager.uri> VARURI
159 %token <UriManager.uri * int> INDTYURI
160 %token <UriManager.uri * int * int> INDCONURI
161 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
162 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
163 %token DOLLAR
164 %token RPLUS RMINUS RTIMES RDIV
165 %token PLUS MINUS TIMES EQT EQ NEQT
166 %right ARROW
167 %nonassoc EQ EQT NEQT
168 %left PLUS MINUS RPLUS RMINUS
169 %left TIMES RTIMES RDIV
170 %start main
171 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
172 %%
173 main:
174  | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
175  | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
176  | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
177  | expr EOF { $1 }
178  | DOLLAR expr DOLLAR EOF { $2 }
179  | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 }
180  | expr SEMICOLON { $1 } /*  FG: to read several terms in a row
181                           *  Do we need to clear some static variables? 
182                           */
183 ;
184 expr2:
185  | RNUM
186    { [], function interp ->
187       let rec cic_real_of_real =
188        function
189           0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, [])
190         | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[])
191         | n ->
192           Cic.Appl
193            [ Cic.Const
194                (HelmLibraryObjects.Reals.rplus_URI,[]) ;
195              Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);
196              cic_real_of_real (n - 1)
197            ]
198       in
199        cic_real_of_real $1
200    }
201  | NUM
202    { [], function interp ->
203       let rec cic_int_of_int =
204        function
205           0 ->
206            Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,1,[])
207         | n ->
208           Cic.Appl
209            [ Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,2,[]) ;
210              cic_int_of_int (n - 1)
211            ]
212       in
213        cic_int_of_int $1
214    }
215  | expr2 RPLUS expr2
216    { let dom1,mk_expr1 = $1 in
217      let dom2,mk_expr2 = $3 in
218       let dom = union dom1 dom2 in
219        dom, function interp ->
220         Cic.Appl
221          [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
222           (mk_expr1 interp) ;
223           (mk_expr2 interp)
224          ]
225    }
226  | expr2 RMINUS expr2
227    { let dom1,mk_expr1 = $1 in
228      let dom2,mk_expr2 = $3 in
229       let dom = union dom1 dom2 in
230        dom, function interp ->
231         Cic.Appl
232          [Cic.Const (HelmLibraryObjects.Reals.rminus_URI,[]);
233           (mk_expr1 interp) ;
234           (mk_expr2 interp)
235          ]
236    }
237  | expr2 RTIMES 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 (HelmLibraryObjects.Reals.rmult_URI,[]) ;
244           (mk_expr1 interp) ;
245           (mk_expr2 interp)
246          ]
247    }
248  | expr2 RDIV expr2
249    { let dom1,mk_expr1 = $1 in
250      let dom2,mk_expr2 = $3 in
251       let dom = union dom1 dom2 in
252        dom, function interp ->
253         Cic.Appl
254          [Cic.Const (HelmLibraryObjects.Reals.rdiv_URI,[]) ;
255           (mk_expr1 interp) ;
256           (mk_expr2 interp)
257          ]
258    }
259  | expr2 PLUS expr2
260    { let dom1,mk_expr1 = $1 in
261      let dom2,mk_expr2 = $3 in
262       let dom = union dom1 dom2 in
263        dom, function interp ->
264         Cic.Appl
265          [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
266           (mk_expr1 interp) ;
267           (mk_expr2 interp)
268          ]
269    }
270  | expr2 MINUS expr2
271    { let dom1,mk_expr1 = $1 in
272      let dom2,mk_expr2 = $3 in
273       let dom = union dom1 dom2 in
274        dom, function interp ->
275         Cic.Appl
276          [Cic.Const (HelmLibraryObjects.Peano.minus_URI,[]) ;
277           (mk_expr1 interp) ;
278           (mk_expr2 interp)
279          ]
280    }
281  | expr2 TIMES expr2
282    { let dom1,mk_expr1 = $1 in
283      let dom2,mk_expr2 = $3 in
284       let dom = union dom1 dom2 in
285        dom, function interp ->
286         Cic.Appl
287          [Cic.Const (HelmLibraryObjects.Peano.mult_URI,[]) ;
288           (mk_expr1 interp) ;
289           (mk_expr2 interp)
290          ]
291    }
292  | expr2 EQ expr2
293    { let dom1,mk_expr1 = $1 in
294      let dom2,mk_expr2 = $3 in
295      let dom3,mk_expr3 = mk_implicit () in
296       let dom = union dom1 (union dom2 dom3) in
297        dom, function interp ->
298         Cic.Appl
299          [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI,0,[]) ;
300           (mk_expr3 interp) ;
301           (mk_expr1 interp) ;
302           (mk_expr2 interp)
303          ]
304    }
305  | CONURI exp_named_subst
306    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
307       dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
308    }
309  | VARURI exp_named_subst
310    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
311       dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
312    }
313  | INDTYURI exp_named_subst
314    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
315       dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
316    }
317  | INDCONURI exp_named_subst
318    { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
319       dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
320    }
321  | ID exp_named_subst
322    { try
323       let res =
324        Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders)
325       in
326        (match $2 with
327            None -> ([], function _ -> res)
328          | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
329        )
330      with
331       Not_found ->
332        let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
333         let dom = union dom1 [CicTextualParser0.Id $1] in
334          dom,
335           function interp ->
336            match interp (CicTextualParser0.Id $1) with
337               None  -> raise (UnknownIdentifier $1)
338             | Some (CicTextualParser0.Uri uri) ->
339                term_of_uri uri (mk_exp_named_subst interp)
340             | Some CicTextualParser0.Implicit ->
341                (*CSC: not very clean; to maximize code reusage *)
342                snd (mk_implicit ()) ""
343             | Some (CicTextualParser0.Term mk_term) ->
344                (mk_term interp)
345    }
346  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
347     { let dom1,mk_expr1 = $3 in
348       let dom2,mk_expr2 = $7 in
349       let dom3,mk_expr3 = $10 in
350        let dom = union dom1 (union dom2 dom3) in
351         dom,
352         function interp ->
353          MutCase
354           (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
355     }
356  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
357     { let dom1,mk_expr1 = $3 in
358       let dom2,mk_expr2 = $7 in
359       let dom3,mk_expr3 = $10 in
360        let dom =
361         union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3))
362        in
363         dom,
364         function interp ->
365          let uri,typeno = indty_uri_of_id $5 interp in
366           MutCase
367            (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
368              (mk_expr3 interp))
369     }
370  | fixheader LCURLY exprseplist RCURLY
371     { let dom1,foo,ids_and_indexes,mk_types = $1 in
372       let dom2,mk_exprseplist = $3 in
373        let dom = union dom1 dom2 in
374         for i = 1 to List.length ids_and_indexes do
375          TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders
376         done ;
377         dom,
378          function interp ->
379           let types = mk_types interp in
380           let fixfunsbodies = (mk_exprseplist interp) in
381            let idx =
382             let rec find idx =
383              function
384                 [] -> raise Not_found
385               | (name,_)::_  when name = foo -> idx
386               | _::tl -> find (idx+1) tl
387             in
388              find 0 ids_and_indexes
389            in
390             let fixfuns =
391              List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
392               (List.combine ids_and_indexes types) fixfunsbodies
393             in
394              Fix (idx,fixfuns)
395     }
396  | cofixheader LCURLY exprseplist RCURLY
397     { let dom1,foo,ids,mk_types = $1 in
398       let dom2,mk_exprseplist = $3 in
399        let dom = union dom1 dom2 in
400         dom,
401          function interp ->
402           let types = mk_types interp in
403           let fixfunsbodies = (mk_exprseplist interp) in
404            let idx =
405             let rec find idx =
406              function
407                 [] -> raise Not_found
408               | name::_  when name = foo -> idx
409               | _::tl -> find (idx+1) tl
410             in
411              find 0 ids
412            in
413             let fixfuns =
414              List.map2 (fun (name,ty) bo -> (name,ty,bo))
415               (List.combine ids types) fixfunsbodies
416             in
417              for i = 1 to List.length fixfuns do
418               TexCicTextualParser0.binders :=
419                List.tl !TexCicTextualParser0.binders
420              done ;
421              CoFix (idx,fixfuns)
422     }
423  | IMPLICIT
424     { mk_implicit () }
425  | SET   { [], function _ -> Sort Set }
426  | PROP  { [], function _ -> Sort Prop }
427  | TYPE  { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)}
428  | CPROP { [], function _ -> Sort CProp }
429  | LPAREN expr CAST expr RPAREN
430     { let dom1,mk_expr1 = $2 in
431       let dom2,mk_expr2 = $4 in
432        let dom = union dom1 dom2 in
433         dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
434     }
435  | META LBRACKET substitutionlist RBRACKET
436     { let dom,mk_substitutionlist = $3 in
437        dom, function interp -> Meta ($1, mk_substitutionlist interp)
438     } 
439  | LPAREN expr exprlist RPAREN
440     { let length,dom2,mk_exprlist = $3 in
441        match length with
442           0 -> $2
443         | _ ->
444           let dom1,mk_expr1 = $2 in
445            let dom = union dom1 dom2 in
446             dom,
447              function interp ->
448               Appl ((mk_expr1 interp)::(mk_exprlist interp))
449     }
450 ;
451 exp_named_subst :
452     { None }
453  | LCURLY named_substs RCURLY
454     { Some $2 }
455 ;
456 named_substs :
457    VARURI LETIN expr2
458     { let dom,mk_expr = $3 in
459        dom, function interp -> [$1, mk_expr interp] }
460  | ID LETIN expr2
461     { let dom1,mk_expr = $3 in
462        let dom = union [CicTextualParser0.Id $1] dom1 in
463         dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
464  | VARURI LETIN expr2 SEMICOLON named_substs
465     { let dom1,mk_expr = $3 in
466       let dom2,mk_named_substs = $5 in
467        let dom = union dom1 dom2 in
468         dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
469     }
470  | ID LETIN expr2 SEMICOLON named_substs
471     { let dom1,mk_expr = $3 in
472       let dom2,mk_named_substs = $5 in
473        let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
474         dom,
475          function interp ->
476           (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
477     }
478 ;
479 expr :
480    pihead expr
481     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
482       let dom1,mk_expr1 = snd $1 in
483       let dom2,mk_expr2 = $2 in
484        let dom = union dom1 dom2 in
485         dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
486     }
487  | lambdahead expr
488     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
489       let dom1,mk_expr1 = snd $1 in
490       let dom2,mk_expr2 = $2 in
491        let dom = union dom1 dom2 in
492         dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
493     }
494  | letinhead expr
495     { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
496       let dom1,mk_expr1 = snd $1 in
497       let dom2,mk_expr2 = $2 in
498        let dom = union dom1 dom2 in
499         dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
500     }
501  | expr2
502     { $1 }
503 ;
504 fixheader:
505    FIX ID LCURLY fixfunsdecl RCURLY
506     { let dom,ids_and_indexes,mk_types = $4 in
507        let bs =
508         List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
509        in
510         TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
511         dom, $2, ids_and_indexes, mk_types
512     }
513 ;
514 fixfunsdecl:
515    ID LPAREN NUM RPAREN COLON expr
516     { let dom,mk_expr = $6 in
517        dom, [$1,$3], function interp -> [mk_expr interp]
518     }
519  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
520     { let dom1,mk_expr = $6 in
521       let dom2,ids_and_indexes,mk_types = $8 in
522        let dom = union dom1 dom2 in
523         dom, ($1,$3)::ids_and_indexes,
524          function interp -> (mk_expr interp)::(mk_types interp)
525     }
526 ;
527 cofixheader:
528    COFIX ID LCURLY cofixfunsdecl RCURLY
529     { let dom,ids,mk_types = $4 in
530        let bs =
531         List.rev_map (function name -> Some (Name name)) ids
532        in
533         TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
534         dom, $2, ids, mk_types
535     }
536 ;
537 cofixfunsdecl:
538    ID COLON expr
539     { let dom,mk_expr = $3 in
540        dom, [$1], function interp -> [mk_expr interp]
541     }
542  | ID COLON expr SEMICOLON cofixfunsdecl
543     { let dom1,mk_expr = $3 in
544       let dom2,ids,mk_types = $5 in
545        let dom = union dom1 dom2 in
546         dom, $1::ids,
547          function interp -> (mk_expr interp)::(mk_types interp)
548     }
549 ;
550 pihead:
551    PROD ID COLON expr DOT
552     { TexCicTextualParser0.binders :=
553        (Some (Name $2))::!TexCicTextualParser0.binders;
554       let dom,mk_expr = $4 in
555        Cic.Name $2, (dom, function interp -> mk_expr interp)
556     }
557  | expr2 ARROW
558    { TexCicTextualParser0.binders :=
559       (Some Anonymous)::!TexCicTextualParser0.binders ;
560      let dom,mk_expr = $1 in
561       Anonymous, (dom, function interp -> mk_expr interp)
562    }
563  | PROD ID DOT
564     { TexCicTextualParser0.binders :=
565        (Some (Name $2))::!TexCicTextualParser0.binders;
566       let newmeta = new_meta () in
567       let newuniv = CicUniv.fresh () in
568        let new_canonical_context = [] in
569         let irl =
570          identity_relocation_list_for_metavariable new_canonical_context
571         in
572          TexCicTextualParser0.metasenv :=
573           [newmeta, new_canonical_context, Sort (Type newuniv);
574            (* TASSI: ?? *)
575            newmeta+1, new_canonical_context, Meta (newmeta,irl)
576           ] @ !TexCicTextualParser0.metasenv ;
577          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
578     }
579 ;
580 lambdahead:
581    LAMBDA ID COLON expr DOT
582     { TexCicTextualParser0.binders :=
583        (Some (Name $2))::!TexCicTextualParser0.binders;
584       let dom,mk_expr = $4 in
585        Cic.Name $2, (dom, function interp -> mk_expr interp)
586     }
587  | LAMBDA ID DOT
588     { TexCicTextualParser0.binders :=
589        (Some (Name $2))::!TexCicTextualParser0.binders;
590       let newmeta = new_meta () in
591       let newuniv = CicUniv.fresh () in
592        let new_canonical_context = [] in
593         let irl =
594          identity_relocation_list_for_metavariable new_canonical_context
595         in
596          TexCicTextualParser0.metasenv :=
597           [newmeta, new_canonical_context, Sort (Type newuniv) ;
598            (* TASSI: ?? *)
599            newmeta+1, new_canonical_context, Meta (newmeta,irl)
600           ] @ !TexCicTextualParser0.metasenv ;
601          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
602     }
603 ;
604 letinhead:
605   LAMBDA ID LETIN expr DOT
606    { TexCicTextualParser0.binders :=
607       (Some (Name $2))::!TexCicTextualParser0.binders ;
608      let dom,mk_expr = $4 in
609       Cic.Name $2, (dom, function interp -> mk_expr interp)
610    }
611 ;
612 branches:
613     { [], function _ -> [] }
614  | expr SEMICOLON branches
615     { let dom1,mk_expr = $1 in
616       let dom2,mk_branches = $3 in
617        let dom = union dom1 dom2 in
618         dom, function interp -> (mk_expr interp)::(mk_branches interp)
619     }
620  | expr
621     { let dom,mk_expr = $1 in
622        dom, function interp -> [mk_expr interp]
623     }
624 ;
625 exprlist:
626     
627     { 0, [], function _ -> [] }
628  | expr exprlist
629     { let dom1,mk_expr = $1 in
630       let length,dom2,mk_exprlist = $2 in
631        let dom = union dom1 dom2 in
632         length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
633     }
634 ;
635 exprseplist:
636    expr
637     { let dom,mk_expr = $1 in
638        dom, function interp -> [mk_expr interp]
639     }
640  | expr SEMICOLON exprseplist
641     { let dom1,mk_expr = $1 in
642       let dom2,mk_exprseplist = $3 in
643        let dom = union dom1 dom2 in
644         dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
645     }
646 ;
647 substitutionlist:
648     { [], function _ -> [] }
649  | expr SEMICOLON substitutionlist
650     { let dom1,mk_expr = $1 in
651       let dom2,mk_substitutionlist = $3 in
652        let dom = union dom1 dom2 in
653         dom,
654          function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
655     }
656  | NONE SEMICOLON substitutionlist
657     { let dom,mk_exprsubstitutionlist = $3 in
658        dom, function interp -> None::(mk_exprsubstitutionlist interp)
659     }