* Many improvements (expecially in exceptions handling)

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 5f64134b50dc6db1995f091f5ac3f6c335dcfce2..ac828a9598c794ca832edbfbc7a0c76e41b86d72 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -28,7 +28,21 @@ let cic_context_of_named_context =
   )
 ;;
 
-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
@@ -37,7 +51,7 @@ let refine_meta_with_brand_new_metasenv meta term newmetasenv =
   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)
 ;;
@@ -236,9 +250,9 @@ let new_metasenv_for_apply 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
@@ -247,7 +261,7 @@ let classify_metas newmeta in_subst_domain apply_subst =
        ((i,ty')::old_uninst),new_uninst
       else
        old_uninst,((i,ty')::new_uninst)
-  ) ([],[])
+  ) metasenv ([],[])
 ;;
 
 (* The term bo must be closed in the current context *)
@@ -276,6 +290,14 @@ let apply term =
        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
@@ -289,11 +311,18 @@ let apply term =
             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 =
@@ -449,11 +478,25 @@ prerr_endline "unwind"; flush stderr;
                (* 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
@@ -469,6 +512,7 @@ prerr_endline "unwind"; flush stderr;
 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