+ let consno = ref (conslen + 1) in
+ let eliminator_body =
+ let fix = Cic.Rel (rightno + 2) in
+ let is_recursive = recursive_type uri typeno constructors in
+ let recshift = if is_recursive then 1 else 0 in
+ let (_, branches) =
+ List.fold_right
+ (fun (_, ty) (shift, branches) ->
+ let head = Cic.Rel (rightno + shift + 1 + recshift) in
+ let b =
+ branch (uri, typeno) false
+ (rightno + conslen + 2 + recshift) leftno ty fix head []
+ in
+ (shift + 1, b :: branches))
+ constructors (1, [])
+ in
+ let shiftno = conslen + rightno + 2 + recshift in
+ let outtype =
+ if dependent then
+ Cic.Rel shiftno
+ else
+ let head =
+ if rightno = 0 then
+ CicSubstitution.lift 1 (Cic.Rel shiftno)
+ else
+ Cic.Appl
+ ((CicSubstitution.lift (rightno + 1) (Cic.Rel shiftno)) ::
+ mk_rels 1 rightno)
+ in
+ add_right_lambda true leftno shiftno 1 rightno indty head ty
+ in
+ let mutcase =
+ Cic.MutCase (uri, typeno, outtype, Cic.Rel 1, branches)
+ in
+ let body =
+ if is_recursive then
+ let fixfun =
+ add_right_lambda dependent leftno (conslen + 2) 1 rightno
+ indty mutcase ty
+ in
+ (* rightno is the decreasing argument, i.e. the argument of
+ * inductive type *)
+ Cic.Fix (0, ["f", rightno, final_ty, fixfun])
+ else
+ add_right_lambda dependent leftno (conslen + 1) 1 rightno indty
+ mutcase ty
+ in
+ let cic =
+ 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 (),
+ (delta (uri, typeno) dependent leftno !consno
+ constructor p [mk_constructor !consno]),
+ acc))
+ constructors body))
+ in
+ add_params (fun b s t -> Cic.Lambda (b, s, t)) leftno ty cic
+ in
+(*
+debug_print (CicPp.ppterm eliminator_type);
+debug_print (CicPp.ppterm eliminator_body);
+*)
+ let eliminator_type =
+ FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in
+ let eliminator_body =
+ FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in
+(*
+debug_print (CicPp.ppterm eliminator_type);
+debug_print (CicPp.ppterm eliminator_body);
+*)
+ let (computed_type, ugraph) =
+ try
+ CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+ with CicTypeChecker.TypeCheckerFailure msg ->
+ raise (Elim_failure (sprintf
+ "type checker failure while type checking:\n%s\nerror:\n%s"
+ (CicPp.ppterm eliminator_body) msg))
+ in
+ if not (fst (CicReduction.are_convertible []
+ eliminator_type computed_type ugraph))
+ then
+ raise (Failure (sprintf
+ "internal error: type mismatch on eliminator type\n%s\n%s"
+ (CicPp.ppterm eliminator_type) (CicPp.ppterm computed_type)));
+ let suffix =
+ match sort with
+ | Cic.Prop -> "_ind"
+ | Cic.Set -> "_rec"
+ | Cic.Type _ -> "_rect"
+ | _ -> assert false
+ in
+ let name = UriManager.name_of_uri uri ^ suffix in
+ let buri = UriManager.buri_of_uri uri in
+ let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in
+ let obj_attrs = [`Class (`Elim sort); `Generated] in
+ uri,
+ Cic.Constant (name, Some eliminator_body, eliminator_type, [], obj_attrs)
+ | _ ->
+ failwith (sprintf "not an inductive definition (%s)"
+ (UriManager.string_of_uri uri))