+ { let dom1,mk_expr1 = $3 in
+ let dom2,mk_expr2 = $7 in
+ let dom3,mk_expr3 = $10 in
+ let dom = union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3)) in
+ dom,
+ function interp ->
+ let uri,typeno = indty_uri_of_id $5 interp in
+ MutCase
+ (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
+ (mk_expr3 interp))
+ }
+ | fixheader LCURLY exprseplist RCURLY
+ { let dom1,foo,ids_and_indexes,mk_types = $1 in
+ let dom2,mk_exprseplist = $3 in
+ let dom = union dom1 dom2 in
+ for i = 1 to List.length ids_and_indexes do
+ CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+ done ;
+ dom,
+ function interp ->
+ let types = mk_types interp in
+ let fixfunsbodies = (mk_exprseplist interp) in
+ let idx =
+ let rec find idx =
+ function
+ [] -> raise Not_found
+ | (name,_)::_ when name = foo -> idx
+ | _::tl -> find (idx+1) tl
+ in
+ find 0 ids_and_indexes
+ in
+ let fixfuns =
+ List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
+ (List.combine ids_and_indexes types) fixfunsbodies
+ in
+ Fix (idx,fixfuns)
+ }
+ | cofixheader LCURLY exprseplist RCURLY
+ { let dom1,foo,ids,mk_types = $1 in
+ let dom2,mk_exprseplist = $3 in
+ let dom = union dom1 dom2 in
+ dom,
+ function interp ->
+ let types = mk_types interp in
+ let fixfunsbodies = (mk_exprseplist interp) in
+ let idx =
+ let rec find idx =
+ function
+ [] -> raise Not_found
+ | name::_ when name = foo -> idx
+ | _::tl -> find (idx+1) tl
+ in
+ find 0 ids
+ in
+ let fixfuns =
+ List.map2 (fun (name,ty) bo -> (name,ty,bo))
+ (List.combine ids types) fixfunsbodies
+ in
+ for i = 1 to List.length fixfuns do
+ CicTextualParser0.binders := List.tl !CicTextualParser0.binders
+ done ;
+ CoFix (idx,fixfuns)
+ }
+ | IMPLICIT
+ { mk_implicit () }
+ | SET { [], function _ -> Sort Set }
+ | PROP { [], function _ -> Sort Prop }
+ | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)}
+ | CPROP { [], function _ -> Sort CProp }
+ | LPAREN expr CAST expr RPAREN
+ { let dom1,mk_expr1 = $2 in
+ let dom2,mk_expr2 = $4 in
+ let dom = union dom1 dom2 in
+ dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
+ }
+ | META LBRACKET substitutionlist RBRACKET
+ { let dom,mk_substitutionlist = $3 in
+ dom, function interp -> Meta ($1, mk_substitutionlist 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 :
+ { None }
+ | LCURLY named_substs RCURLY
+ { Some $2 }
+;
+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 [CicTextualParser0.Id $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 [CicTextualParser0.Id $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,ids_and_indexes,mk_types = $4 in
+ let bs =
+ List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes