-let elim term =
- let module T = CicTypeChecker in
- let module U = UriManager in
- let module R = CicReduction in
- let module C = Cic in
- let curi,metasenv =
- match !proof with
- None -> assert false
- | Some (curi,metasenv,_,_) -> curi,metasenv
- in
- let (metano,context,ty) =
- match !goal with
- None -> assert false
- | Some (metano,(context,ty)) ->
- assert (ty = List.assoc metano metasenv) ;
- (* Invariant: context is the actual context of the meta in the proof *)
- metano,context,ty
- in
- let ciccontext = cic_context_of_named_context context in
- let termty = T.type_of_aux' metasenv ciccontext term in
- let uri,cookingno,typeno,args =
- match termty with
- C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
- | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
- (uri,cookingno,typeno,args)
- | _ -> raise NotAnInductiveTypeToEliminate
- in
- let eliminator_uri =
- let buri = U.buri_of_uri uri in
- let name =
- match CicEnvironment.get_cooked_obj uri cookingno with
- C.InductiveDefinition (tys,_,_) ->
- let (name,_,_,_) = List.nth tys typeno in
- name
- | _ -> assert false
- in
- let ext =
- match T.type_of_aux' metasenv ciccontext ty with
- C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.Type -> "_rect"
- | _ -> assert false
- in
- U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
- in
- let eliminator_cookingno =
- UriManager.relative_depth curi eliminator_uri 0
- in
- let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
- let ety =
- T.type_of_aux' [] [] eliminator_ref
- in
- let (econclusion,newmetas,newmeta,lastmeta) =
- new_metasenv_for_apply ety
- 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 meta_of_corpse = Cic.Meta (lastmeta - 1) in
- let newmetasenv = newmetas @ metasenv in
-prerr_endline ("ECONCLUSION: " ^ CicPp.ppterm econclusion) ;
-flush stderr ;
- let subst1 =
- CicUnification.fo_unif newmetasenv ciccontext term meta_of_corpse
- in
- let ueconclusion = CicUnification.apply_subst subst1 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 ty' = CicUnification.apply_subst subst1 ty in
- let eta_expanded_ty =
- List.fold_left (eta_expand metasenv ciccontext) ty' fargs
- in
-prerr_endline ("ETAEXPANDEDTY:" ^ CicPp.ppterm eta_expanded_ty) ; flush stdout ;
- let subst2 =
-(*CSC: passo newmetasenv, ma alcune variabili sono gia' state sostituite
-da subst1!!!! Dovrei rimuoverle o sono innocue?*)
- CicUnification.fo_unif
- newmetasenv ciccontext ueconclusion eta_expanded_ty
- in
-prerr_endline "Dopo la seconda unificazione" ; flush stdout ;
-prerr_endline "unwind"; flush stderr;
- let in_subst_domain i =
- let eq_to_i = function (j,_) -> i=j in
- List.exists eq_to_i subst1 ||
- List.exists eq_to_i subst2
- in
- (* When unwinding the META that corresponds to the elimination *)
- (* predicate (which is emeta), we must also perform one-step *)
- (* beta-reduction. *)
- let apply_subst =
- function t ->
- let t' = CicUnification.apply_subst subst1 t in
- CicUnification.apply_subst_reducing
- subst2 (Some (emeta,List.length fargs)) t'
- in
- let newmetasenv' =
- List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
- in
- let old_uninstantiatedmetas,new_uninstantiatedmetas =
- classify_metas newmeta in_subst_domain apply_subst newmetasenv
- in
- let arguments =
- List.map apply_subst
- (List.map (function (i,_) -> C.Meta i) newmetas)
- in
- let bo' = Cic.Appl (eliminator_ref::arguments) in
-prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
-List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
- refine_meta_with_brand_new_metasenv metano bo'
- (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
- match new_uninstantiatedmetas with
- [] -> goal := None
- | (i,ty)::_ -> goal := Some (i,(context,ty))
-;;