)
;;
-let refine_meta_with_brand_new_metasenv meta term newmetasenv =
+(* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing *)
+(* newmetasenv *)
+(* This (heavy) function must be called when a tactic can instantiate old *)
+(* metavariables (i.e. existential variables). It substitues the metasenv *)
+(* of the proof with the result of removing [meta] from the domain of *)
+(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
+(* in the current proof. Finally it applies [apply_subst_replacing] to *)
+(* current proof. *)
+(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
+(*CSC: ci ripasso sopra apply_subst!!! *)
+(*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
+(*CSC: newmetasenv!!! *)
+let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
+ newmetasenv
+=
let (uri,bo,ty) =
match !proof with
None -> assert false
let subst_in t =
ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
in
- let bo' = subst_in bo in
+ let bo' = apply_subst_replacing (subst_in bo) in
let metasenv' = List.remove_assoc meta newmetasenv in
proof := Some (uri,metasenv',bo',ty)
;;
;;
(*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
-let classify_metas newmeta in_subst_domain apply_subst =
- List.fold_left
- (fun (old_uninst,new_uninst) (i,ty) ->
+let classify_metas newmeta in_subst_domain apply_subst metasenv =
+ List.fold_right
+ (fun (i,ty) (old_uninst,new_uninst) ->
if in_subst_domain i then
old_uninst,new_uninst
else
((i,ty')::old_uninst),new_uninst
else
old_uninst,((i,ty')::new_uninst)
- ) ([],[])
+ ) metasenv ([],[])
;;
(* The term bo must be closed in the current context *)
let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
let apply_subst = CicUnification.apply_subst subst in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+ let apply_subst_replacing t =
+ List.fold_left
+ (fun t (i,bo) ->
+ ProofEngineReduction.replace
+ ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+ t subst
+ in
let old_uninstantiatedmetas,new_uninstantiatedmetas =
classify_metas newmeta in_subst_domain apply_subst newmetasenv
in
in
Cic.Appl (term::arguments)
in
- refine_meta_with_brand_new_metasenv metano bo'
+ refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
(new_uninstantiatedmetas@old_uninstantiatedmetas) ;
+prerr_endline "QUI4" ; flush stderr ; (
match new_uninstantiatedmetas with
[] -> goal := None
| (i,ty)::_ -> goal := Some (i,(context,ty))
+) ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
+; prerr_endline "FATTO" ; flush stderr ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
+prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
+; prerr_endline "FATTO2" ; flush stderr
;;
let eta_expand metasenv ciccontext t arg =
(* 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'
+ let apply_subst t =
+ let t' = CicUnification.apply_subst subst1 t in
+ CicUnification.apply_subst_reducing
+ subst2 (Some (emeta,List.length fargs)) t'
+ in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+ let apply_subst_replacing t =
+ let t' =
+ List.fold_left
+ (fun t (i,bo) ->
+ ProofEngineReduction.replace
+ ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+ t subst1
+ in
+ List.fold_left
+ (fun t (i,bo) ->
+ ProofEngineReduction.replace
+ ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+ t' subst2
in
let newmetasenv' =
List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
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'
+ apply_subst_replacing
(new_uninstantiatedmetas@old_uninstantiatedmetas) ;
match new_uninstantiatedmetas with
[] -> goal := None