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     }