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