X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=1cdabc09fe673dd8ca222b5e376772612318e255;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0d3127c3176be7c7d2b514895f28257ac927b689;hpb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index 0d3127c31..1cdabc09f 100644
--- 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
@@ -382,22 +398,21 @@ let aconjecture_of_conjecture seed ids_to_terms ids_to_father_ids
            Hashtbl.add ids_to_hypotheses hid binding ;
            incr hypotheses_seed ;
            match binding with
-               Some (n,Cic.Def (t,None)) ->
-                 let acic = acic_of_cic_context context idrefs t None in
+               Some (n,Cic.Def (t,_)) ->
+                 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 ->
                  (* Invariant: "" is never looked up *)
                   (None::context),((hid,None)::acontext),""::idrefs
-             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) 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)
 ;;
 
@@ -409,7 +424,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let ids_to_hypotheses = Hashtbl.create 23 in
     let hypotheses_seed = ref 0 in
     let seed = ref 1 in (* 'i0' is used for the whole sequent *)
-    let sequent =
+    let unsh_sequent =
      let i,canonical_context,term = sequent in
       let canonical_context' =
        List.fold_right
@@ -421,7 +436,8 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
                Some (n, Cic.Decl (Unshare.unshare t))
             | Some (n, Cic.Def (t,None)) ->
                Some (n, Cic.Def ((Unshare.unshare t),None))
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some (n, Cic.Def (Unshare.unshare bo,Some (Unshare.unshare ty)))
           in
            d::canonical_context'
         ) canonical_context []
@@ -432,9 +448,10 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
     let (metano,acontext,agoal) = 
       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 sequent in
-    ("i0",metano,acontext,agoal), 
-     ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses
+      metasenv unsh_sequent in
+    (unsh_sequent,
+     (("i0",metano,acontext,agoal), 
+      ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
 let acic_object_of_cic_object ?(eta_fix=true) obj =
@@ -464,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) ->
@@ -480,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) ->
@@ -531,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
@@ -568,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)