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