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