lazy proof term to increase sharing and decrease memory consumption.

[helm.git] / helm / software / components / tactics / inversion_principle.ml

diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml
index b0f4d236ff5aa23e3fefad53b73e831c578e3274..0f50116cb5ed7be0ce46d09178e8317a8dc1f8fe 100644 (file)
--- a/helm/software/components/tactics/inversion_principle.ml
+++ b/helm/software/components/tactics/inversion_principle.ml
@@ -145,7 +145,7 @@ let build_inversion uri obj =
           debug_print 
             (lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
           let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem  
-            CicUniv.empty_ugraph in
+            CicUniv.oblivion_ugraph in
             (*DEBUG*) debug_print 
             (lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
             let buri = UriManager.buri_of_uri uri in
@@ -154,8 +154,10 @@ let build_inversion uri obj =
             let goal = CicMkImplicit.new_meta metasenv [] in
             let metasenv' = (goal,[],ref_theorem)::metasenv in
             let attrs = [`Class (`InversionPrinciple); `Generated] in
+       let _subst = [] in
             let proof= 
-              (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in 
+              (Some inversor_uri,metasenv',_subst,
+                 lazy (Cic.Meta(goal,[])),ref_theorem, attrs) in 
             let _,applies =
               List.fold_right
                 (fun _ (i,applies) ->
@@ -186,15 +188,30 @@ let build_inversion uri obj =
                 (proof,goal) 
             in
             let metasenv,bo,ty, attrs =
-              match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
+              match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
             in
               assert (metasenv = []);
               Some
                 (inversor_uri,
                  Cic.Constant 
-                   (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
+                   (UriManager.name_of_uri inversor_uri,Some (Lazy.force bo),ty,[],[]))
        with
-          Inversion.EqualityNotDefinedYet -> None
+         Inversion.EqualityNotDefinedYet -> None
+        | CicRefine.RefineFailure ls ->
+           HLog.warn
+            ("CicRefine.RefineFailure during generation of inversion principle: " ^
+             Lazy.force ls) ;
+           None
+        | CicRefine.Uncertain ls ->
+           HLog.warn
+            ("CicRefine.Uncertain during generation of inversion principle: " ^
+             Lazy.force ls) ;
+           None
+        | CicRefine.AssertFailure ls ->
+           HLog.warn
+            ("CicRefine.AssertFailure during generation of inversion principle: " ^
+             Lazy.force ls) ;
+           None
  in
    match obj with
      | Cic.InductiveDefinition (tys,_,nleft,_) ->