-let split c t =
- let add s v c = Some (s, C.Decl v) :: c in
- let rec aux whd a n c = function
- | C.Prod (s, v, t) -> aux false (v :: a) (succ n) (add s v c) t
- | v when whd -> v :: a, n
- | v -> aux true a n c (Rd.whd ~delta:true c v)
- in
- aux false [] 0 c t
+let clear_absts m =
+ let rec aux k n = function
+ | C.Lambda (s, v, t) when k > 0 ->
+ C.Lambda (s, v, aux (pred k) n t)
+ | C.Lambda (_, _, t) when n > 0 ->
+ aux 0 (pred n) (S.lift (-1) t)
+ | t when n > 0 ->
+ Printf.eprintf "CicPPP clear_absts: %u %s\n" n (Pp.ppterm t);
+ assert false
+ | t -> t
+ in
+ aux m
+
+let rec add_abst k = function
+ | C.Lambda (s, v, t) when k > 0 -> C.Lambda (s, v, add_abst (pred k) t)
+ | t when k > 0 -> assert false
+ | t -> C.Lambda (C.Anonymous, C.Implicit None, S.lift 1 t)
+
+let get_ind_type uri tyno =
+ match E.get_obj Un.empty_ugraph uri with
+ | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
+ | _ -> assert false
+
+let get_ind_parameters c t =
+ let ty = get_type c t in
+ let ps = match get_tail c ty with
+ | C.MutInd _ -> []
+ | C.Appl (C.MutInd _ :: args) -> args
+ | _ -> assert false
+ in
+ let disp = match get_tail c (get_type c ty) with
+ | C.Sort C.Prop -> 0
+ | C.Sort _ -> 1
+ | _ -> assert false
+ in
+ ps, disp
+
+let get_default_eliminator context uri tyno ty =
+ let _, (name, _, _, _) = get_ind_type uri tyno in
+ let ext = match get_tail context (get_type context ty) with
+ | C.Sort C.Prop -> "_ind"
+ | C.Sort C.Set -> "_rec"
+ | C.Sort C.CProp -> "_rec"
+ | C.Sort (C.Type _) -> "_rect"
+ | t ->
+ Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
+ assert false
+ in
+ let buri = UM.buri_of_uri uri in
+ let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
+ C.Const (uri, [])