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