- let earity = CicUnification.get_arity ety in
- let mgu = Array.init earity (fun i -> (C.Meta i)) in
- let mgut = Array.make earity C.Implicit in
- (* Here we assume that we have only one inductive hypothesis to *)
- (* eliminate and that it is the last hypothesis of the theorem. *)
- (* A better approach would be fingering the hypotheses in some *)
- (* way. *)
- let hypothesis_to_eliminate,econclusion =
- (* aux n h t *)
- (* traverses the backbone [t] looking for the last hypothesis *)
- (* and substituting Pi-abstractions with META declarations. *)
- (* [h] is the last hypothesis met up to now. [n] is the next *)
- (* unused META. *)
- let rec aux n h =
- function
- C.Prod (_,s,t) ->
- mgut.(n) <- s ;
- aux (n+1) (Some s) (CicSubstitution.subst (C.Meta n) t)
- | C.Cast (te,_) -> aux n h te
- | t -> match h with
- None -> raise NoHypothesesFound
- | Some h' -> h',t
- in
- aux 0 None ety
- in
-prerr_endline ("HTOELIM: " ^ CicPp.ppterm hypothesis_to_eliminate) ;
-prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
-flush stderr ;
- ignore (CicUnification.fo_unif_mgu 0 hypothesis_to_eliminate termty mgu) ;
- ignore (CicUnification.fo_unif_mgu 0 term (C.Meta (earity - 1)) mgu) ;
- let mgu = CicUnification.unwind mgu in
-prerr_endline "Dopo l'unwind dell'mgu"; flush stderr ;
- let mark = Array.make earity 1 in
- let ueconclusion =
- CicUnification.unwind_meta mgu mark econclusion
- in
-prerr_endline ("ECONCLUSION DOPO UNWIND: " ^ CicPp.ppterm ueconclusion) ;
-flush stderr ;
- (* The conclusion of our elimination principle is *)
- (* (?i farg1 ... fargn) *)
- (* The conclusion of our goal is ty. So, we can *)
- (* eta-expand ty w.r.t. farg1 .... fargn to get *)
- (* a new ty equal to (P farg1 ... fargn). Now *)
- (* ?i can be instantiated with P and we are ready *)
- (* to refine the term. *)
- let emeta, fargs =
- match ueconclusion with
- C.Appl ((C.Meta emeta)::fargs) -> emeta,fargs
- | _ -> raise NotTheRightEliminatorShape
- in
- let eta_expanded_ty =
-(*CSC: metasenv e ?????????????*)
- List.fold_left (eta_expand metasenv ciccontext) ty fargs
- in
-(*CSC: 0????????*)
-prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
- ignore (CicUnification.fo_unif_mgu 0 ueconclusion eta_expanded_ty mgu) ;
-prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
- let mgu = CicUnification.unwind mgu in
- print_endline "unwind"; flush stdout;
- (* When unwinding the META that corresponds to the elimination *)
- (* predicate (which is emeta), we must also perform one-step *)
- (* beta-reduction. *)
- let mgut =
- let mark = Array.make (Array.length mgu) 1 in
- Array.map
- (CicUnification.unwind_meta_reducing mgu mark (Some emeta))
- mgut ;
- in
- print_endline "unwind_array"; flush stdout;
- let mgu' = Array.copy mgu in
- let mgut' = CicUnification.list_of_array mgut in
- print_endline "list"; flush stdout;
- Array.iteri
- (fun i ty ->
-prerr_endline ("META " ^ string_of_int i ^ ": " ^ CicPp.ppterm mgu'.(i) ^
- " == " ^ CicPp.ppterm ty) ; flush stderr ;
- let ty' =
- CicTypeChecker.type_of_aux' mgut' ciccontext mgu'.(i)
- in
- ignore (CicUnification.fo_unif_mgu 0 ty ty' mgu)
- ) mgut ;
- let mgu = CicUnification.unwind mgu in
- let mgut = CicUnification.unwind_array mgu mgut in
-prerr_endline "Dopo le unwind dell'mgut" ; flush stdout ;
- let mgul',uninstantiatedmetas = fix_andreas_meta mgu mgut in
-prerr_endline "Dopo il fissaggio" ; flush stdout ;
- let bo' = Cic.Appl (eliminator_ref::mgul') in
-prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
- refine_meta metano bo' uninstantiatedmetas ;
-prerr_endline "dopo refine meta" ; flush stdout ;
- match uninstantiatedmetas with
- (n,ty)::tl -> goal := Some (n,(context,ty))
- | [] -> goal := None
-;;