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