let module CTP0 = CicTextualParser0 in
match interp id with
None -> raise (UnknownIdentifier id)
- | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno)) -> (uri,tyno)
+ | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
| Some _ -> raise InductiveTypeURIExpected
;;
%token <UriManager.uri> VARURI
%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 NONE
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%right ARROW
%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
%%
main:
- expr EOF { $1 }
+ | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
+ | expr EOF { $1 }
+ | expr SEMICOLON { $1 } /* FG: to read several terms in a row
+ * Do we need to clear some static variables?
+ */
;
expr2:
CONURI exp_named_subst
{ let dom,mk_substitutionlist = $3 in
dom, function interp -> Meta ($1, mk_substitutionlist interp)
}
- | LPAREN expr expr exprlist RPAREN
- { let dom1,mk_expr1 = $2 in
- let dom2,mk_expr2 = $3 in
- let dom3,mk_exprlist = $4 in
- let dom = union dom1 (union dom2 dom3) in
- dom,
- function interp ->
- Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
+ | LPAREN expr exprlist RPAREN
+ { let length,dom2,mk_exprlist = $3 in
+ match length with
+ 0 -> $2
+ | _ ->
+ let dom1,mk_expr1 = $2 in
+ let dom = union dom1 dom2 in
+ dom,
+ function interp ->
+ Appl ((mk_expr1 interp)::(mk_exprlist interp))
}
;
exp_named_subst :
let dom,mk_expr = $1 in
Anonymous, (dom, function interp -> mk_expr interp)
}
- | LPAREN expr RPAREN ARROW
- { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
- let dom,mk_expr = $2 in
- Anonymous, (dom, function interp -> mk_expr interp)
- }
| PROD ID DOT
{ CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
let newmeta = new_meta () in
;
exprlist:
- { [], function _ -> [] }
+ { 0, [], function _ -> [] }
| expr exprlist
{ let dom1,mk_expr = $1 in
- let dom2,mk_exprlist = $2 in
+ let length,dom2,mk_exprlist = $2 in
let dom = union dom1 dom2 in
- dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+ length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
}
;
exprseplist: