-(* Copyright (C) 2000, HELM Team.
+/* Copyright (C) 2000, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
*
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
- *)
+ */
%{
open Cic;;
exception InvalidSuffix of string;;
exception InductiveTypeURIExpected;;
+ exception UnknownIdentifier of string;;
let uri_of_id_map = Hashtbl.create 53;;
let rec aux i =
function
[] -> raise Not_found
- | he::_ when he = e -> i
+ | (Some he)::_ when he = e -> i
| _::tl -> aux (i+1) tl
in
aux 1
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> INDCONURI
%token ALIAS
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
-%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
+%right ARROW
%start main
%type <Cic.term option> main
%%
| alias { None }
| EOF { raise CicTextualParser0.Eof }
;
-expr:
+expr2:
CONURI
{ let uri = UriManager.string_of_uri $1 in
let suff = (String.sub uri (String.length uri - 3) 3) in
Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
with
Not_found ->
- Hashtbl.find uri_of_id_map $1
+ try
+ Hashtbl.find uri_of_id_map $1
+ with
+ Not_found ->
+ raise (UnknownIdentifier $1)
}
| CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
{ let cookingno = get_cookingno (fst $5) in
| PROP { Sort Prop }
| TYPE { Sort Type }
| LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META { Meta $1 }
+ | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
| LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
- | pihead expr
+;
+expr :
+ pihead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Prod (fst $1, snd $1,$2) }
- | lambdahead expr
+ | lambdahead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Lambda (fst $1, snd $1,$2) }
- | letinhead expr
+ | letinhead expr
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
LetIn (fst $1, snd $1,$2) }
+ | expr2
+ { $1 }
;
fixheader:
FIX ID LCURLY fixfunsdecl RCURLY
- { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
+ { let bs = List.rev_map (function (name,_,_) -> Some (Name name)) $4 in
CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
$2,$4
}
;
cofixheader:
COFIX ID LCURLY cofixfunsdecl RCURLY
- { let bs = List.rev_map (function (name,_) -> Name name) $4 in
+ { let bs = List.rev_map (function (name,_) -> Some (Name name)) $4 in
CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
$2,$4
}
;
pihead:
PROD ID COLON expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
(Cic.Name $2, $4) }
- | expr ARROW
- { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+ | expr2 ARROW
+ { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
(Anonimous, $1) }
| LPAREN expr RPAREN ARROW
- { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some Anonimous)::!CicTextualParser0.binders ;
(Anonimous, $2) }
;
lambdahead:
LAMBDA ID COLON expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
;
letinhead:
LAMBDA ID LETIN expr DOT
- { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
+ { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
;
branches:
expr { [$1] }
| expr SEMICOLON exprseplist { $1::$3 }
;
+substitutionlist:
+ { [] }
+ | expr SEMICOLON substitutionlist { (Some $1)::$3 }
+ | NONE SEMICOLON substitutionlist { None::$3 }
+;
alias:
ALIAS ID CONURI
{ let cookingno = get_cookingno $3 in
Hashtbl.add uri_of_id_map $2
(Cic.MutConstruct (uri, cookingno, indno ,consno))
}
+
+
+