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  let uri_of_id_map = Hashtbl.create 53;;
  37
  38  let get_index_in_list e =
  39   let rec aux i =
  40    function
  41       [] -> raise Not_found
  42     | (Some he)::_ when he = e -> i
  43     | _::tl -> aux (i+1) tl
  44   in
  45    aux 1
  46  ;;
  47
  48  (* Returns the first meta whose number is above the *)
  49  (* number of the higher meta.                       *)
  50  (*CSC: cut&pasted from proofEngine.ml *)
  51  let new_meta () =
  52   let rec aux =
  53    function
  54       None,[] -> 1
  55     | Some n,[] -> n
  56     | None,(n,_,_)::tl -> aux (Some n,tl)
  57     | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  58   in
  59    1 + aux (None,!CicTextualParser0.metasenv)
  60  ;;
  61
  62  (* identity_relocation_list_for_metavariable i canonical_context         *)
  63  (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
  64  (* where n = List.length [canonical_context]                             *)
  65  (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
  66  (*CSC: cut&pasted from proofEngine.ml *)
  67  let identity_relocation_list_for_metavariable canonical_context =
  68   let canonical_context_length = List.length canonical_context in
  69    let rec aux =
  70     function
  71        (_,[]) -> []
  72      | (n,None::tl) -> None::(aux ((n+1),tl))
  73      | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
  74    in
  75     aux (1,canonical_context)
  76  ;;
  77
  78  let term_of_con_uri uri exp_named_subst =
  79   Const (uri,exp_named_subst)
  80  ;;
  81
  82  let term_of_var_uri uri exp_named_subst =
  83   Var (uri,exp_named_subst)
  84  ;;
  85
  86  let term_of_indty_uri (uri,tyno) exp_named_subst =
  87   MutInd (uri, tyno, exp_named_subst)
  88  ;;
  89
  90  let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
  91   MutConstruct (uri, tyno, consno, exp_named_subst)
  92  ;;
  93
  94  let term_of_uri uri =
  95   match uri with
  96      CicTextualParser0.ConUri uri -> term_of_con_uri uri
  97    | CicTextualParser0.VarUri uri -> term_of_var_uri uri
  98    | CicTextualParser0.IndTyUri (uri,tyno) -> term_of_indty_uri (uri,tyno)
  99    | CicTextualParser0.IndConUri (uri,tyno,consno) ->
 100       term_of_indcon_uri (uri,tyno,consno)
 101  ;;
 102
 103  let var_uri_of_id id =
 104   try
 105    (match Hashtbl.find uri_of_id_map id with
 106        CicTextualParser0.VarUri uri -> uri
 107      | _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
 108    )
 109   with
 110    Not_found ->
 111     match !CicTextualParser0.locate_object id with
 112        None -> raise (UnknownIdentifier id)
 113      | Some (CicTextualParser0.VarUri uri as varuri) ->
 114         Hashtbl.add uri_of_id_map id varuri;
 115         uri
 116      | Some _ ->
 117         raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
 118  ;;
 119
 120 %}
 121 %token <string> ID
 122 %token <int> META
 123 %token <int> NUM
 124 %token <UriManager.uri> CONURI
 125 %token <UriManager.uri> VARURI
 126 %token <UriManager.uri * int> INDTYURI
 127 %token <UriManager.uri * int * int> INDCONURI
 128 %token ALIAS
 129 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
 130 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 131 %right ARROW
 132 %start main
 133 %type <Cic.term option> main
 134 %%
 135 main:
 136    expr  { Some $1 }
 137  | alias { None }
 138  | EOF   { raise CicTextualParser0.Eof }
 139 ;
 140 expr2:
 141    CONURI exp_named_subst
 142    { term_of_con_uri $1 $2 }
 143  | VARURI exp_named_subst
 144    { term_of_var_uri $1 $2 }
 145  | INDTYURI exp_named_subst
 146    { term_of_indty_uri $1 $2 }
 147  | INDCONURI exp_named_subst
 148    { term_of_indcon_uri $1 $2 }
 149  | ID exp_named_subst
 150    { try
 151       let res =
 152        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
 153       in
 154        if $2 = [] then res else raise (ExplicitNamedSubstitutionAppliedToRel)
 155      with
 156       Not_found ->
 157        try
 158         term_of_uri (Hashtbl.find uri_of_id_map $1) $2
 159        with
 160         Not_found ->
 161          match !CicTextualParser0.locate_object $1 with
 162           | None      -> raise (UnknownIdentifier $1)
 163           | Some uri ->
 164              Hashtbl.add uri_of_id_map $1 uri;
 165              term_of_uri uri $2
 166    }
 167  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
 168     { MutCase (fst $5, snd $5, $7, $3, $10) }
 169  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
 170     { try
 171        let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
 172         raise InductiveTypeURIExpected
 173       with
 174        Not_found ->
 175         match Hashtbl.find uri_of_id_map $5 with
 176            CicTextualParser0.IndTyUri (uri,typeno) ->
 177             MutCase (uri, typeno, $7, $3, $10)
 178          | _ -> raise InductiveTypeURIExpected
 179     }
 180  | fixheader LCURLY exprseplist RCURLY
 181     { let fixfunsdecls = snd $1 in
 182       let fixfunsbodies = $3 in
 183        let idx =
 184         let rec find idx =
 185          function
 186             [] -> raise Not_found
 187           | (name,_,_)::_  when name = (fst $1) -> idx
 188           | _::tl -> find (idx+1) tl
 189         in
 190          find 0 fixfunsdecls
 191        in
 192         let fixfuns =
 193          List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
 194           fixfunsdecls fixfunsbodies
 195         in
 196          for i = 1 to List.length fixfuns do
 197           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
 198          done ;
 199          Fix (idx,fixfuns)
 200     }
 201  | cofixheader LCURLY exprseplist RCURLY
 202     { let cofixfunsdecls = (snd $1) in
 203       let cofixfunsbodies = $3 in
 204        let idx =
 205         let rec find idx =
 206          function
 207             [] -> raise Not_found
 208           | (name,_)::_  when name = (fst $1) -> idx
 209           | _::tl -> find (idx+1) tl
 210         in
 211          find 0 cofixfunsdecls
 212        in
 213         let cofixfuns =
 214          List.map2 (fun (name,ty) bo -> (name,ty,bo))
 215           cofixfunsdecls cofixfunsbodies
 216         in
 217          for i = 1 to List.length cofixfuns do
 218           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
 219          done ;
 220          CoFix (idx,cofixfuns)
 221     }
 222  | IMPLICIT
 223     { let newmeta = new_meta () in
 224        let new_canonical_context = [] in
 225         let irl =
 226          identity_relocation_list_for_metavariable new_canonical_context
 227         in
 228          CicTextualParser0.metasenv :=
 229           [newmeta, new_canonical_context, Sort Type ;
 230            newmeta+1, new_canonical_context, Meta (newmeta,irl);
 231            newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
 232           ] @ !CicTextualParser0.metasenv ;
 233          Meta (newmeta+2,irl)
 234     }
 235  | SET { Sort Set }
 236  | PROP { Sort Prop }
 237  | TYPE { Sort Type }
 238  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
 239  | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
 240  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 241 ;
 242 exp_named_subst :
 243     { [] }
 244  | LCURLY named_substs RCURLY
 245     { $2 }
 246 ;
 247 named_substs :
 248    VARURI LETIN expr2
 249     { [$1,$3] }
 250  | ID LETIN expr2
 251     { [var_uri_of_id $1,$3] }
 252  | VARURI LETIN expr2 SEMICOLON named_substs
 253     { ($1,$3)::$5 }
 254  | ID LETIN expr2 SEMICOLON named_substs
 255     { (var_uri_of_id $1,$3)::$5 }
 256 ;
 257 expr :
 258    pihead expr
 259     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 260       Prod (fst $1, snd $1,$2) }
 261  | lambdahead expr
 262     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 263       Lambda (fst $1, snd $1,$2) }
 264  | letinhead expr
 265     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 266       LetIn (fst $1, snd $1,$2) }
 267  | expr2
 268     { $1 }
 269 ;
 270 fixheader:
 271    FIX ID LCURLY fixfunsdecl RCURLY
 272     { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
 273        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
 274        $2,$4
 275     }
 276 ;
 277 fixfunsdecl:
 278    ID LPAREN NUM RPAREN COLON expr
 279     { [$1,$3,$6] }
 280  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
 281     { ($1,$3,$6)::$8 }
 282 ;
 283 cofixheader:
 284    COFIX ID LCURLY cofixfunsdecl RCURLY
 285     { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
 286        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
 287        $2,$4
 288     }
 289 ;
 290 cofixfunsdecl:
 291    ID COLON expr
 292     { [$1,$3] }
 293  | ID COLON expr SEMICOLON cofixfunsdecl
 294     { ($1,$3)::$5 }
 295 ;
 296 pihead:
 297    PROD ID COLON expr DOT
 298     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
 299       (Cic.Name $2, $4) }
 300  | expr2 ARROW
 301    { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
 302      (Anonymous, $1) }
 303  | LPAREN expr RPAREN ARROW
 304    { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
 305      (Anonymous, $2) }
 306 ;
 307 lambdahead:
 308   LAMBDA ID COLON expr DOT
 309    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
 310      (Cic.Name $2, $4) }
 311 ;
 312 letinhead:
 313   LAMBDA ID LETIN expr DOT
 314    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
 315      (Cic.Name $2, $4) }
 316 ;
 317 branches:
 318                             { [] }
 319  | expr SEMICOLON branches  { $1::$3 }
 320  | expr                     { [$1] }
 321 ;
 322 exprlist:
 323                   { [] }
 324  | expr exprlist  { $1::$2 }
 325 ;
 326 exprseplist:
 327    expr                        { [$1] }
 328  | expr SEMICOLON exprseplist  { $1::$3 }
 329 ;
 330 substitutionlist:
 331                                      { [] }
 332  | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
 333  | NONE SEMICOLON substitutionlist   { None::$3 }
 334 ;
 335 alias:
 336    ALIAS ID CONURI
 337     { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.ConUri $3) }
 338  | ALIAS ID VARURI
 339     { Hashtbl.add uri_of_id_map $2 (CicTextualParser0.VarUri $3) }
 340  | ALIAS ID INDTYURI
 341     { Hashtbl.add uri_of_id_map $2
 342        (CicTextualParser0.IndTyUri (fst $3, snd $3))
 343     }
 344  | ALIAS ID INDCONURI
 345     { let uri,indno,consno = $3 in
 346        Hashtbl.add uri_of_id_map $2
 347         (CicTextualParser0.IndConUri (uri, indno, consno))
 348     }