- { let cofixfunsdecls = (snd $1) in
- let cofixfunsbodies = $3 in
- let idx =
- let rec find idx =
- function
- [] -> raise Not_found
- | (name,_)::_ when name = (fst $1) -> idx
- | _::tl -> find (idx+1) tl
- in
- find 0 cofixfunsdecls
- in
- let cofixfuns =
- List.map2 (fun (name,ty) bo -> (name,ty,bo))
- cofixfunsdecls cofixfunsbodies
- in
- for i = 1 to List.length cofixfuns do
- CicTextualParser0.binders := List.tl !CicTextualParser0.binders
- done ;
- CoFix (idx,cofixfuns)
- }
- | IMPLICIT { Implicit }
- | SET { Sort Set }
- | PROP { Sort Prop }
- | TYPE { Sort Type }
- | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
- | META LBRACKET substitutionlist RBRACKET { Meta ($1, $3) }
- | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
+ { 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 }
+ | 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)
+ }