- more resilient to proof checking failures during pretty printing

- do not compute inner types for sequents

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 81cfaaf099e7290d52a37ddccb2724c4defa92ea..1cdabc09fe673dd8ca222b5e376772612318e255 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -51,7 +51,14 @@ let type_of_aux'_add_time = ref 0.0;; *)
 
 let xxx_type_of_aux' m c t =
 (*  let t1 = Sys.time () in *)
- let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
+ let res,_ =
+   try
+    CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
+   with
+   | CicTypeChecker.AssertFailure _
+   | CicTypeChecker.TypeCheckerFailure _ ->
+       Cic.Sort Cic.Prop, CicUniv.empty_ugraph
+  in
 (*  let t2 = Sys.time () in
  type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
  res
@@ -89,8 +96,9 @@ let rec get_nth l n =
   | (_,_) -> raise NotEnoughElements
 ;;
 
-let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
-     ids_to_inner_types metasenv context idrefs t expectedty
+let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
+  seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types
+  metasenv context idrefs t expectedty
 =
  let module D = DoubleTypeInference in
  let module C = Cic in
@@ -107,7 +115,10 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
    prerr_endline ("*** Fine double_type_inference:" ^ (string_of_float (time2 -. time1)));
      res 
 *)
-    D.double_type_of metasenv context t expectedty
+    if global_computeinnertypes then
+     D.double_type_of metasenv context t expectedty
+    else
+     D.CicHash.empty ()
    in
 (*
    let time2 = Sys.time () in
@@ -150,10 +161,13 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
          else
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)
-          {D.synthesized =
+          { D.synthesized =
 (***CSC: patch per provare i tempi
             CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
-Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
+            if global_computeinnertypes then
+              Cic.Sort (Cic.Type (CicUniv.fresh()))
+            else
+              CicReduction.whd context (xxx_type_of_aux' metasenv context tt);
           D.expected = None}
         in
 (*          incr number_new_type_of_aux' ; *)
@@ -355,23 +369,25 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
            ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
           res
 *)
-        aux true None context idrefs t
+        aux global_computeinnertypes None context idrefs t
 ;;
 
-let acic_of_cic_context metasenv context idrefs t =
+let acic_of_cic_context ~computeinnertypes metasenv context idrefs t =
  let ids_to_terms = Hashtbl.create 503 in
  let ids_to_father_ids = Hashtbl.create 503 in
  let ids_to_inner_sorts = Hashtbl.create 503 in
  let ids_to_inner_types = Hashtbl.create 503 in
  let seed = ref 0 in
-   acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+   acic_of_cic_context' ~computeinnertypes seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
     ids_to_inner_types metasenv context idrefs t,
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
 
 let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids 
   ids_to_inner_sorts ids_to_inner_types ids_to_hypotheses hypotheses_seed
-  metasenv (metano,context,goal) = 
+  metasenv (metano,context,goal)
+= 
+  let computeinnertypes = false in
   let acic_of_cic_context =
     acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       ids_to_inner_types  metasenv in
@@ -383,11 +399,11 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            incr hypotheses_seed ;
            match binding with
                Some (n,Cic.Def (t,_)) ->
-                 let acic = acic_of_cic_context context idrefs t None in
+                 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
                  (binding::context),
                    ((hid,Some (n,Cic.ADef acic))::acontext),(hid::idrefs)
              | Some (n,Cic.Decl t) ->
-                 let acic = acic_of_cic_context context idrefs t None in
+                 let acic = acic_of_cic_context ~computeinnertypes context idrefs t None in
                  (binding::context),
                    ((hid,Some (n,Cic.ADecl acic))::acontext),(hid::idrefs)
              | None ->
@@ -396,7 +412,7 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
          ) context ([],[],[])
        )
   in 
-  let agoal = acic_of_cic_context context final_idrefs goal None in
+  let agoal = acic_of_cic_context ~computeinnertypes context final_idrefs goal None in
   (metano,acontext,agoal)
 ;;
 
@@ -465,13 +481,13 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
       C.Constant (id,Some bo,ty,params,attrs) ->
        let bo' = eta_fix [] [] bo in
        let ty' = eta_fix [] [] ty in
-       let abo = acic_term_of_cic_term' bo' (Some ty') in
-       let aty = acic_term_of_cic_term' ty' None in
+       let abo = acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty') in
+       let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
         C.AConstant
          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty,params,attrs)
     | C.Constant (id,None,ty,params,attrs) ->
        let ty' = eta_fix [] [] ty in
-       let aty = acic_term_of_cic_term' ty' None in
+       let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
         C.AConstant
          ("mettereaposto",None,id,None,aty,params,attrs)
     | C.Variable (id,bo,ty,params,attrs) ->
@@ -481,9 +497,9 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
            None -> None
          | Some bo ->
             let bo' = eta_fix [] [] bo in
-             Some (acic_term_of_cic_term' bo' (Some ty'))
+             Some (acic_term_of_cic_term' ~computeinnertypes:true bo' (Some ty'))
        in
-       let aty = acic_term_of_cic_term' ty' None in
+       let aty = acic_term_of_cic_term' ~computeinnertypes:false ty' None in
         C.AVariable
          ("mettereaposto",id,abo,aty,params,attrs)
     | C.CurrentProof (id,conjectures,bo,ty,params,attrs) ->
@@ -532,8 +548,8 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
        DoubleTypeInference.syntactic_equality_add_time := 0.0 ;
 *)
        let abo =
-        acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
-       let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
+        acic_term_of_cic_term_context' ~computeinnertypes:true conjectures' [] [] bo' (Some ty') in
+       let aty = acic_term_of_cic_term_context' ~computeinnertypes:false conjectures' [] [] ty' None in
 (*
        let time3 = Sys.time () in
        prerr_endline
@@ -569,10 +585,11 @@ let acic_object_of_cic_object ?(eta_fix=true) obj =
             List.map
              (function (name,ty) ->
                (name,
-                 acic_term_of_cic_term_context' [] context idrefs ty None)
+                 acic_term_of_cic_term_context' ~computeinnertypes:false [] context idrefs ty None)
              ) cons
            in
-            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
+            (id,name,inductive,
+             acic_term_of_cic_term' ~computeinnertypes:false ty None,acons)
          ) (List.rev idrefs) tys
        in
         C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.ml b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
index b514319c1f42bee7b8883b604f31cae8d02666ee..69287243918419218848f810371f5c0c1843fa83 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.ml
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.ml
@@ -324,12 +324,17 @@ let type_of_mutual_inductive_constr uri i j =
 ;;
 
 module CicHash =
- Hashtbl.Make
-  (struct
-    type t = Cic.term
-    let equal = (==)
-    let hash = Hashtbl.hash
-   end)
+  struct
+    module Tmp = 
+     Hashtbl.Make
+      (struct
+        type t = Cic.term
+        let equal = (==)
+        let hash = Hashtbl.hash
+       end)
+    include Tmp
+    let empty () = Tmp.create 1
+  end
 ;;
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)

diff --git a/helm/ocaml/cic_omdoc/doubleTypeInference.mli b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
index 20230e3bb0529ca2a36a0eb4ab94df8aa7d4cfe7..138aad83440bcb062b00e637ca8a93bbfdf3898e 100644 (file)
--- a/helm/ocaml/cic_omdoc/doubleTypeInference.mli
+++ b/helm/ocaml/cic_omdoc/doubleTypeInference.mli
@@ -18,6 +18,7 @@ module CicHash :
   sig
     type 'a t
     val find : 'a t -> Cic.term -> 'a
+    val empty: unit -> 'a t
   end
 ;;