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