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     }