- let ety,_ =
- T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
- let rec find_args_no =
- function
- C.Prod (_,_,t) -> 1 + find_args_no t
- | C.Cast (s,_) -> find_args_no s
- | C.LetIn (_,_,t) -> 0 + find_args_no t
- | _ -> 0
- in
- let args_no = find_args_no ety in
- let term_to_refine =
- let rec make_tl base_case =
- function
- 0 -> [base_case]
- | n -> (C.Implicit None)::(make_tl base_case (n - 1))
- in
- C.Appl (eliminator_ref :: make_tl term (args_no - 1))
+ let ety,_ugraph =
+ TC.type_of_aux' metasenv' context eliminator_ref ugraph in
+(* FG: ADDED PART ***********************************************************)
+(* FG: we can not assume eliminator is the default eliminator ***************)
+(*
+ let add_lambdas n t =
+ let rec aux n t =
+ if n <= 0 then t
+ else C.Lambda (C.Anonymous, C.Implicit None, aux (pred n) t)
+ in
+ aux n (S.lift n t)
+ in
+*)
+ let rec args_init n f =
+ if n <= 0 then [] else f n :: args_init (pred n) f
+ in
+ let splits, args_no = PEH.split_with_whd (context, ety) in
+ let pred_pos = match List.hd splits with
+ | _, C.Rel i when i > 1 && i <= args_no -> i
+ | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
+ | _ -> raise NotAnEliminator
+ in
+(*
+ let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
+ let termty_ty =
+ let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
+ CicReduction.whd context termty_ty
+ in
+*)
+(*
+ let metasenv', term, pred, upto = match cpatt, termty_ty with
+ | C.Implicit (Some `Hole), _
+ | _, C.Sort C.Prop when lambdas = 0 -> metasenv', term, C.Implicit None, 0
+ | _ ->
+(* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ ~subst:[] metasenv' context C.Anonymous ~typ:termty
+ in
+ let lazy_term c m u =
+ let distance = List.length c - List.length context in
+ S.lift distance term, m, u
+ in
+ let pattern = Some lazy_term, [], Some cpatt in
+ let subst, metasenv', _ugraph, _conjecture, selected_terms =
+ ProofEngineHelpers.select
+ ~metasenv:metasenv' ~ugraph ~conjecture ~pattern
+ in
+ let metasenv' = MS.apply_subst_metasenv subst metasenv' in
+ let map (_context_of_t, t) l = t :: l in
+ let what = List.fold_right map selected_terms [] in
+ let ty = MS.apply_subst subst ty in
+ let term = MS.apply_subst subst term in
+ let termty = MS.apply_subst subst termty in
+ let abstr_ty = PER.replace_with_rel_1_from ~equality:(==) ~what 1 ty in
+ let abstr_ty = MS.apply_subst subst abstr_ty in
+ let pred_body = C.Lambda (fresh_name, termty, abstr_ty) in
+ metasenv', term, add_lambdas (pred lambdas) pred_body, lambdas
+ in
+(* FG: END OF ADDED PART ****************************************************)
+*)
+ let pred, upto = C.Implicit None, 0 in
+
+ let term_to_refine =
+ let f n =
+ if n = pred_pos then pred else
+ if n = 1 then term else C.Implicit None
+ in
+ C.Appl (eliminator_ref :: args_init args_no f)