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 %}
  51 %token <string> ID
  52 %token <int> META
  53 %token <int> NUM
  54 %token <UriManager.uri> CONURI
  55 %token <UriManager.uri * int> INDTYURI
  56 %token <UriManager.uri * int * int> INDCONURI
  57 %token ALIAS
  58 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
  59 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
  60 %right ARROW
  61 %start main
  62 %type <Cic.term option> main
  63 %%
  64 main:
  65    expr  { Some $1 }
  66  | alias { None }
  67  | EOF   { raise CicTextualParser0.Eof }
  68 ;
  69 expr2:
  70    CONURI
  71    { let uri = UriManager.string_of_uri $1 in
  72      let suff = (String.sub uri (String.length uri - 3) 3) in
  73       match suff with
  74          "con" ->
  75            let cookingno = get_cookingno $1 in
  76             Const ($1,cookingno)
  77        | "var" -> Var $1
  78        | _ -> raise (InvalidSuffix suff)
  79    }
  80  | INDTYURI
  81     { let cookingno = get_cookingno (fst $1) in
  82        MutInd (fst $1, cookingno, snd $1) }
  83  | INDCONURI
  84    { let (uri,tyno,consno) = $1 in
  85       let cookingno = get_cookingno uri in
  86        MutConstruct (uri, cookingno, tyno, consno) }
  87  | ID
  88    { try
  89        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
  90      with
  91       Not_found ->
  92        try
  93         Hashtbl.find uri_of_id_map $1
  94        with
  95         Not_found ->
  96          raise (UnknownIdentifier $1)
  97    }
  98  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
  99     { let cookingno = get_cookingno (fst $5) in
 100        MutCase (fst $5, cookingno, snd $5, $7, $3, $10) }
 101  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
 102     { try
 103        let _ = get_index_in_list (Name $5) !CicTextualParser0.binders in
 104         raise InductiveTypeURIExpected
 105       with
 106        Not_found ->
 107         match Hashtbl.find uri_of_id_map $5 with
 108            MutInd (uri,cookingno,typeno) ->
 109             MutCase (uri, cookingno, typeno, $7, $3, $10)
 110          | _ -> raise InductiveTypeURIExpected
 111     }
 112  | fixheader LCURLY exprseplist RCURLY
 113     { let fixfunsdecls = snd $1 in
 114       let fixfunsbodies = $3 in
 115        let idx =
 116         let rec find idx =
 117          function
 118             [] -> raise Not_found
 119           | (name,_,_)::_  when name = (fst $1) -> idx
 120           | _::tl -> find (idx+1) tl
 121         in
 122          find 0 fixfunsdecls
 123        in
 124         let fixfuns =
 125          List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
 126           fixfunsdecls fixfunsbodies
 127         in
 128          for i = 1 to List.length fixfuns do
 129           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
 130          done ;
 131          Fix (idx,fixfuns)
 132     }
 133  | cofixheader LCURLY exprseplist RCURLY
 134     { let cofixfunsdecls = (snd $1) in
 135       let cofixfunsbodies = $3 in
 136        let idx =
 137         let rec find idx =
 138          function
 139             [] -> raise Not_found
 140           | (name,_)::_  when name = (fst $1) -> idx
 141           | _::tl -> find (idx+1) tl
 142         in
 143          find 0 cofixfunsdecls
 144        in
 145         let cofixfuns =
 146          List.map2 (fun (name,ty) bo -> (name,ty,bo))
 147           cofixfunsdecls cofixfunsbodies
 148         in
 149          for i = 1 to List.length cofixfuns do
 150           CicTextualParser0.binders := List.tl !CicTextualParser0.binders
 151          done ;
 152          CoFix (idx,cofixfuns)
 153     }
 154  | IMPLICIT { Implicit }
 155  | SET { Sort Set }
 156  | PROP { Sort Prop }
 157  | TYPE { Sort Type }
 158  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
 159  | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
 160  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 161 ;
 162 expr :
 163    pihead expr
 164     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 165       Prod (fst $1, snd $1,$2) }
 166  | lambdahead expr
 167     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 168       Lambda (fst $1, snd $1,$2) }
 169  | letinhead expr
 170     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
 171       LetIn (fst $1, snd $1,$2) }
 172  | expr2
 173     { $1 }
 174 ;
 175 fixheader:
 176    FIX ID LCURLY fixfunsdecl RCURLY
 177     { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
 178        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
 179        $2,$4
 180     }
 181 ;
 182 fixfunsdecl:
 183    ID LPAREN NUM RPAREN COLON expr
 184     { [$1,$3,$6] }
 185  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
 186     { ($1,$3,$6)::$8 }
 187 ;
 188 cofixheader:
 189    COFIX ID LCURLY cofixfunsdecl RCURLY
 190     { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
 191        CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
 192        $2,$4
 193     }
 194 ;
 195 cofixfunsdecl:
 196    ID COLON expr
 197     { [$1,$3] }
 198  | ID COLON expr SEMICOLON cofixfunsdecl
 199     { ($1,$3)::$5 }
 200 ;
 201 pihead:
 202    PROD ID COLON expr DOT
 203     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
 204       (Cic.Name $2, $4) }
 205  | expr2 ARROW
 206    { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
 207      (Anonimous, $1) }
 208  | LPAREN expr RPAREN ARROW
 209    { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
 210      (Anonimous, $2) }
 211 ;
 212 lambdahead:
 213   LAMBDA ID COLON expr DOT
 214    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
 215      (Cic.Name $2, $4) }
 216 ;
 217 letinhead:
 218   LAMBDA ID LETIN expr DOT
 219    { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
 220      (Cic.Name $2, $4) }
 221 ;
 222 branches:
 223                             { [] }
 224  | expr SEMICOLON branches  { $1::$3 }
 225  | expr                     { [$1] }
 226 ;
 227 exprlist:
 228                   { [] }
 229  | expr exprlist  { $1::$2 }
 230 ;
 231 exprseplist:
 232    expr                        { [$1] }
 233  | expr SEMICOLON exprseplist  { $1::$3 }
 234 ;
 235 substitutionlist:
 236                                      { [] }
 237  | expr SEMICOLON substitutionlist   { (Some $1)::$3 }
 238  | NONE SEMICOLON substitutionlist   { None::$3 }
 239 ;
 240 alias:
 241    ALIAS ID CONURI
 242     { let cookingno = get_cookingno $3 in
 243        Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,cookingno)) }
 244  | ALIAS ID INDTYURI
 245     { let cookingno = get_cookingno (fst $3) in
 246        Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, cookingno, snd $3)) }
 247  | ALIAS ID INDCONURI
 248     { let uri,indno,consno = $3 in
 249        let cookingno = get_cookingno uri in
 250         Hashtbl.add uri_of_id_map $2
 251          (Cic.MutConstruct (uri, cookingno, indno ,consno))
 252     }
 253
 254
 255