- let connames_and_argsno =
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- C.InductiveDefinition (dl,_,paramsno,_) ->
- let (_,_,_,cons) = get_nth dl (n1+1) in
- List.map
- (fun (id,ty) ->
- (* this is just an approximation since we do not have
- reduction yet! *)
- let rec count_prods toskip =
- function
- C.Prod (_,_,bo) when toskip > 0 ->
- count_prods (toskip - 1) bo
- | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
- | _ -> 0
- in
- qualified_name_of_uri current_module_name ~capitalize:true
- (UriManager.uri_of_string
- (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
- count_prods paramsno ty
- ) cons
- | _ -> raise CicExportationInternalError
- )
- in
- let connames_and_argsno_and_patterns =
- let rec combine =
- function
- [],[] -> []
- | [],l -> List.map (fun x -> "???",0,Some x) l
- | l,[] -> List.map (fun (x,no) -> x,no,None) l
- | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
- in
- combine (connames_and_argsno,patterns)
- in
- "\n(match " ^ pp te context ^ " with \n" ^
- (String.concat "\n | "
- (List.map
- (fun (x,argsno,y) ->
- let rec aux argsno context =
- function
- Cic.Lambda (name,ty,bo) when argsno > 0 ->
- let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo in
- (match name with C.Anonymous -> "_" | C.Name s -> s)::args,
- res
- | t when argsno = 0 -> [],pp t context
- | t -> ["{" ^ string_of_int argsno ^ " args missing}"],pp t context
- in
- let pattern,body =
- match y with
- None -> x,""
- | Some y when argsno = 0 -> x,pp y context
- | Some y ->
- let args,body = aux argsno context y in
- let sargs = String.concat "," args in
- x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),body
+ if patterns = [] then "assert false"
+ else
+ (let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,paramsno,_) ->
+ let (_,_,_,cons) = get_nth dl (n1+1) in
+ let rc =
+ List.map
+ (fun (id,ty) ->
+ (* this is just an approximation since we do not have
+ reduction yet! *)
+ let rec count_prods toskip =
+ function
+ C.Prod (_,_,bo) when toskip > 0 ->
+ count_prods (toskip - 1) bo
+ | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
+ | _ -> 0
+ in
+ qualified_name_of_uri current_module_uri
+ ~capitalize:true
+ (UriManager.uri_of_string
+ (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
+ count_prods paramsno ty
+ ) cons