let defs =
List.map
(fun (_, n, decr_idx, ty, bo) ->
- ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
+ let params,bo =
+ let rec aux =
+ function
+ Cic.ALambda (_,name,so,ta) ->
+ let params,rest = aux ta in
+ (CicNotationUtil.name_of_cic_name name,Some (k so))::
+ params, rest
+ | t -> [],t
+ in
+ aux bo
+ in
+ let ty =
+ let rec eat_pis =
+ function
+ 0,ty -> ty
+ | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+ | n,ty ->
+ (* I should do a whd here, but I have no context *)
+ assert false
+ in
+ eat_pis ((List.length params),ty)
+ in
+ (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
funs
in
let name =
try
(match List.nth defs no with
- | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+ | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
| _ -> assert false)
with Not_found -> assert false
in
- idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
+ idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
| Cic.ACoFix (id, no, funs) ->
let defs =
List.map
(fun (_, n, ty, bo) ->
- ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
+ let params,bo =
+ let rec aux =
+ function
+ Cic.ALambda (_,name,so,ta) ->
+ let params,rest = aux ta in
+ (CicNotationUtil.name_of_cic_name name,Some (k so))::
+ params, rest
+ | t -> [],t
+ in
+ aux bo
+ in
+ let ty =
+ let rec eat_pis =
+ function
+ 0,ty -> ty
+ | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+ | n,ty ->
+ (* I should do a whd here, but I have no context *)
+ assert false
+ in
+ eat_pis ((List.length params),ty)
+ in
+ (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0))
funs
in
let name =
try
(match List.nth defs no with
- | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+ | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
| _ -> assert false)
with Not_found -> assert false
in