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