+let rec join f v1 v2 =
+ match v1, v2 with
+ | [], v -> f v
+ | v, [] -> f v
+ | h1 :: t1, h2 :: _ when h1 < h2 ->
+ let g h = f (h1 :: h) in join g t1 v2
+ | h1 :: _, h2 :: t2 when h1 > h2 ->
+ let g h = f (h2 :: h) in join g v1 t2
+ | h1 :: t1, _ :: t2 ->
+ let g h = f (h1 :: h) in join g t1 t2
+
+let rec diff f v1 v2 =
+ match v1, v2 with
+ | [], _ -> f []
+ | _, [] -> f v1
+ | h1 :: t1, h2 :: _ when h1 < h2 ->
+ let g h = f (h1 :: h) in diff g t1 v2
+ | h1 :: _, h2 :: t2 when h1 > h2 -> diff f v1 t2
+ | _ :: t1, _ :: t2 -> diff f t1 t2
+
+let add f r k l = join f r [M.string_of_uriref (k, l)]
+
+let rec add_cons f r k i j = function
+ | [] -> f r
+ | _ :: tl ->
+ let g s = add f s k [i; j] in
+ add_cons g r k i (succ j) tl
+
+let rec refobj_l refobj_t map f r = function
+ | [] -> f r
+ | h :: tail ->
+ let f r = refobj_l refobj_t map f r tail in
+ refobj_t f r (map h)
+
+let rec refobj_t f r = function
+ | Cic.Implicit _
+ | Cic.Meta _
+ | Cic.Sort _
+ | Cic.Rel _ -> f r
+ | Cic.Cast (t, u)
+ | Cic.Prod (_, t, u)
+ | Cic.Lambda (_, t, u)
+ | Cic.LetIn (_, t, u) ->
+ let f r = refobj_t f r u in refobj_t f r t
+ | Cic.Appl tl ->
+ refobj_l refobj_t (fun x -> x) f r tl
+ | Cic.Fix (_, tl) ->
+ let f r = refobj_l refobj_t (fun (_, _, _, u) -> u) f r tl in
+ refobj_l refobj_t (fun (_, _, t, _) -> t) f r tl
+ | Cic.CoFix (_, tl) ->
+ let f r = refobj_l refobj_t (fun (_, _, u) -> u) f r tl in
+ refobj_l refobj_t (fun (_, t, _) -> t) f r tl
+ | Cic.Var (k, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k []
+ | Cic.Const (k, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k []
+ | Cic.MutInd (k, i, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k [i]
+ | Cic.MutConstruct (k, i, j, tl) ->
+ let f r = refobj_l refobj_t (fun (_, u) -> u) f r tl in
+ add f r k [i; j]
+ | Cic.MutCase (k, i, t, u, tl) ->
+ let f r = refobj_l refobj_t (fun u -> u) f r tl in
+ let f r = refobj_t f r u in
+ let f r = refobj_t f r t in
+ let f r = add f r k [i] in
+ add_cons f r k i 1 tl
+
+let get_refobj f r uri =
+ let body, ty = M.get_object (M.uriref_of_string uri) in
+ let f r = diff f r [uri] in
+ let f r = refobj_t f r body in
+ refobj_t f r ty
+
+let rec get_refobj_l f r = function
+ | [] -> f r
+ | uri :: l ->
+ let f r = get_refobj_l f r l in
+ get_refobj f r uri
+
+let show_refobj uri =
+ let f = List.iter print_endline in
+ get_refobj f [] uri
+
+let compute_shells uri =
+ let rec aux r d n =
+ let f p r =
+ let l = List.length r in
+ Printf.printf "found %i objects\n" l; flush stdout;
+ let f d = if l > 0 then aux r d (succ n) in
+ join f d p
+ in
+ Printf.printf "shells: computing level %i ... " n; flush stdout;
+ let f r = get_refobj_l (f r) [] r in
+ diff f r d
+ in
+ aux [uri] [] 0
+