summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
6102d4a)
the wrong way. No more conflicts left.
exception InvalidSuffix of string;;
exception InductiveTypeURIExpected;;
exception InvalidSuffix of string;;
exception InductiveTypeURIExpected;;
+ exception UnknownIdentifier of string;;
let uri_of_id_map = Hashtbl.create 53;;
let uri_of_id_map = Hashtbl.create 53;;
%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 ALIAS
%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
%start main
%type <Cic.term option> main
%%
%start main
%type <Cic.term option> main
%%
| alias { None }
| EOF { raise CicTextualParser0.Eof }
;
| alias { None }
| EOF { raise CicTextualParser0.Eof }
;
CONURI
{ let uri = UriManager.string_of_uri $1 in
let suff = (String.sub uri (String.length uri - 3) 3) in
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 ->
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
}
| CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
{ let cookingno = get_cookingno (fst $5) in
| LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
| META { Meta $1 }
| LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
| LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
| META { Meta $1 }
| LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Prod (fst $1, snd $1,$2) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Prod (fst $1, snd $1,$2) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Lambda (fst $1, snd $1,$2) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
Lambda (fst $1, snd $1,$2) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
LetIn (fst $1, snd $1,$2) }
{ CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
LetIn (fst $1, snd $1,$2) }
;
fixheader:
FIX ID LCURLY fixfunsdecl RCURLY
;
fixheader:
FIX ID LCURLY fixfunsdecl RCURLY
PROD ID COLON expr DOT
{ CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
PROD ID COLON expr DOT
{ CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
(Cic.Name $2, $4) }
{ CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
(Anonimous, $1) }
| LPAREN expr RPAREN ARROW
{ CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
(Anonimous, $1) }
| LPAREN expr RPAREN ARROW