+named_substs :
+ VARURI LETIN expr2
+ { let dom,mk_expr = $3 in
+ dom, function interp -> [$1, mk_expr interp] }
+ | ID LETIN expr2
+ { let dom1,mk_expr = $3 in
+ let dom = union [$1] dom1 in
+ dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
+ | VARURI LETIN expr2 SEMICOLON named_substs
+ { let dom1,mk_expr = $3 in
+ let dom2,mk_named_substs = $5 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
+ }
+ | ID LETIN expr2 SEMICOLON named_substs
+ { let dom1,mk_expr = $3 in
+ let dom2,mk_named_substs = $5 in
+ let dom = union [$1] (union dom1 dom2) in
+ dom,
+ function interp ->
+ (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
+ }
+;
+expr :
+ pihead expr
+ { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
+ let dom1,mk_expr1 = snd $1 in
+ let dom2,mk_expr2 = $2 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
+ }
+ | lambdahead expr
+ { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
+ let dom1,mk_expr1 = snd $1 in
+ let dom2,mk_expr2 = $2 in
+ let dom = union dom1 dom2 in
+ dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
+ }
+ | letinhead expr
+ { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
+ let dom1,mk_expr1 = snd $1 in
+ let dom2,mk_expr2 = $2 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
+ }
+ | expr2
+ { $1 }
+;
+fixheader:
+ FIX ID LCURLY fixfunsdecl RCURLY
+ { let dom,mk_fixfunsdecl = $4 in
+ dom,
+ function interp ->
+ let bs =
+ List.rev_map
+ (function (name,_,_) -> Some (Name name)) (mk_fixfunsdecl interp)
+ in
+ CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+ $2,(mk_fixfunsdecl interp)
+ }
+;
+fixfunsdecl:
+ ID LPAREN NUM RPAREN COLON expr
+ { let dom,mk_expr = $6 in
+ dom, function interp -> [$1,$3,mk_expr interp]
+ }
+ | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
+ { let dom1,mk_expr = $6 in
+ let dom2,mk_fixfunsdecl = $8 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> ($1,$3,mk_expr interp)::(mk_fixfunsdecl interp)
+ }
+;
+cofixheader:
+ COFIX ID LCURLY cofixfunsdecl RCURLY
+ { let dom,mk_cofixfunsdecl = $4 in
+ dom,
+ function interp ->
+ let bs =
+ List.rev_map
+ (function (name,_) -> Some (Name name)) (mk_cofixfunsdecl interp)
+ in
+ CicTextualParser0.binders := bs@(!CicTextualParser0.binders) ;
+ $2,(mk_cofixfunsdecl interp)
+ }
+;
+cofixfunsdecl:
+ ID COLON expr
+ { let dom,mk_expr = $3 in
+ dom, function interp -> [$1,(mk_expr interp)]
+ }
+ | ID COLON expr SEMICOLON cofixfunsdecl
+ { let dom1,mk_expr = $3 in
+ let dom2,mk_cofixfunsdecl = $5 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> ($1,(mk_expr interp))::(mk_cofixfunsdecl interp)
+ }