+ constructors final_ty))
+ in
+ add_params leftno ty eliminator
+ | _ -> assert false
+
+let rec branch (uri, typeno, subst) insource paramsno t fix head args =
+ assert (subst = []);
+ match t with
+ | Cic.MutInd (uri', typeno', subst') when
+ UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
+ let head = if insource then fix else head in
+ (match args with
+ | [] -> head
+ | _ -> Cic.Appl (head :: args))
+ | Cic.Appl (Cic.MutInd (uri', typeno', subst') :: tl) when
+ UriManager.eq uri uri' && typeno = typeno' && subst = subst' ->
+ let (lparams, rparams) = split tl paramsno in
+ (match args with
+ | [] when insource && rparams = [] -> fix
+ | [] when insource -> Cic.Appl (fix :: rparams)
+ | _ when insource -> Cic.Appl (fix :: rparams @ args)
+ | _ -> Cic.Appl (head :: rparams @ args))
+ | Cic.Prod (binder, src, tgt) ->
+ if recursive uri typeno subst src then
+ let args = List.map (CicSubstitution.lift 1) args in
+ let phi =
+ let fix = CicSubstitution.lift 1 fix in
+ branch (uri, typeno, subst) true paramsno src fix head
+ (args @ [Cic.Rel 1])
+ in
+ let tgt = CicSubstitution.lift 1 tgt in
+ Cic.Lambda (fresh_binder true, src,
+ branch (uri, typeno, subst) insource paramsno tgt
+ (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
+ (args @ [Cic.Rel 1; phi]))
+ else (* non recursive *)
+ let args = List.map (CicSubstitution.lift 1) args in
+ Cic.Lambda (fresh_binder true, src,
+ branch (uri, typeno, subst) insource paramsno tgt
+ (CicSubstitution.lift 1 fix) (CicSubstitution.lift 1 head)
+ (args @ [Cic.Rel 1]))
+ | _ -> assert false
+
+let branch (uri, typeno, subst) insource liftno paramsno t fix head args =
+ let t = strip_left_params liftno paramsno t in
+ branch (uri, typeno, subst) insource paramsno t fix head args
+
+let body_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno =
+ let (obj, univ) = (CicEnvironment.get_obj uri CicUniv.empty_ugraph) in
+ let subst = [] in
+ match obj with
+ | Cic.InductiveDefinition (indTypes, params, leftno) ->
+ let (name, inductive, ty, constructors) =
+ try
+ List.nth indTypes typeno
+ with Failure _ -> assert false
+ in
+ let paramsno = count_pi ty in (* number of (left or right) parameters *)
+ let rightno = paramsno - leftno in
+ let dependent = (strip_pi ty <> Cic.Sort Cic.Prop) in
+ let conslen = List.length constructors in
+ let consno = ref (conslen + 1) in
+ if (not dependent) && (sort <> Cic.Prop) && (conslen > 1) then
+ raise (Failure (sprintf "can't eliminate from Prop to %s"
+ (string_of_sort sort)));
+ let indty =
+ let indty = Cic.MutInd (uri, typeno, subst) in
+ if paramsno = 0 then
+ indty
+ else
+ Cic.Appl (indty :: mk_rels 0 paramsno)
+ in
+ let mk_constructor consno =
+ let constructor = Cic.MutConstruct (uri, typeno, consno, subst) in
+ if leftno = 0 then
+ constructor
+ else
+ Cic.Appl (constructor :: mk_rels consno leftno)
+ in
+ let eliminator =
+ let p_ty = type_of_p sort dependent leftno indty ty in
+ let final_ty =
+ add_right_pi dependent leftno (conslen + 1) 1 rightno indty ty
+ in
+ let fix = Cic.Rel (rightno + 2) in
+ let (_, branches) =
+ List.fold_right
+ (fun (_, ty) (shift, branches) ->
+ let head = Cic.Rel (rightno + shift + 2) in
+ let b =
+ branch (uri, typeno, subst) false (rightno + conslen + 3) leftno
+ ty fix head []
+ in
+ (shift + 1, b :: branches))
+ constructors (1, [])
+ in
+ let case =
+ Cic.MutCase (uri, typeno, Cic.Rel (conslen + rightno + 3), Cic.Rel 1,
+ branches)
+ in
+ let fix_body =
+ add_right_lambda dependent leftno (conslen + 1) 1 rightno
+ indty case ty
+ in
+ let fix = Cic.Fix (0, ["f", 0, final_ty, fix_body]) in
+ Cic.Lambda (Cic.Name "P", p_ty,
+ (List.fold_right
+ (fun (_, constructor) acc ->
+ decr consno;
+ let p = Cic.Rel !consno in
+ Cic.Lambda (fresh_binder true,
+ (delta (uri, typeno, subst) dependent leftno !consno
+ constructor p [mk_constructor !consno]),
+ acc))
+ constructors fix))