- (* this context is used to compute dependencies between constructor arguments *)
- let kctx = List.map2 (fun t ty -> t, NCic.Decl ty) (List.rev ts) (List.rev (arg_list leftno kty)) in
- let ts = List.map mk_id ts in
- (* compute graph of dependencies *)
- let deps,_ = List.fold_left
- (fun (acc,i) (t,_) ->
- let name,_ = List.nth kctx (i-1) in
- (name,fst (cascade_select_in_ctx status ~subst:[] kctx [] i))::acc,i+1) ([],1) kctx
- in
- (* transpose graph *)
- let deps = List.fold_left
- (fun acc (t,_) ->
- let t_deps = List.map fst (List.filter (fun (name,rev_deps) -> List.mem t rev_deps) deps) in
- (t,t_deps)::acc) [] deps
- in
- prerr_endline ("deps dump!");
- List.iter (fun (x,xs) -> prerr_endline (x ^ ": " ^ (String.concat ", " xs))) deps;
- let deps = List.map (fun (x,xs) -> mk_id x, (List.map mk_id) xs) deps in
- let max_dep = List.fold_left max 0 (List.map (fun (_,xs) -> List.length xs) deps) in
- if (max_dep > 4 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i));
-
- let nones =