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