* doubleTypeInference.ml* added. For now, it just computes the synthesized type.

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

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index ffe9dbd4db98f0e1abe90fc2851b84484c3680c8..7b9511da11d1653d9db106c626235dc17b986d67 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -53,9 +53,11 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
  let module T = CicTypeChecker in
  let module C = Cic in
   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
+   let terms_to_types = DoubleTypeInference.double_type_of metasenv context t in
    let rec aux computeinnertypes father context tt =
     let fresh_id'' = fresh_id' father tt in
-    let aux' = aux true (Some fresh_id'') in
+    (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
+    let aux' = aux computeinnertypes (Some fresh_id'') in
      (* First of all we compute the inner type and the inner sort *)
      (* of the term. They may be useful in what follows.          *)
      (*CSC: This is a very inefficient way of computing inner types *)
@@ -71,11 +73,19 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       let ainnertype,innertype,innersort =
 (*CSC: Here we need the algorithm for Coscoy's double type-inference  *)
 (*CSC: (expected type + inferred type). Just for now we use the usual *)
-(*CSC: type-inference, but the result is very poort. As a very weak   *)
+(*CSC: type-inference, but the result is very poor. As a very weak    *)
 (*CSC: patch, I apply whd to the computed type. Full beta             *)
 (*CSC: reduction would be a much better option.                       *)
         let innertype =
-         CicReduction.whd context (T.type_of_aux' metasenv context tt)
+         if computeinnertypes then
+          let {DoubleTypeInference.synthesized = synthesized} =
+           DoubleTypeInference.CicHash.find terms_to_types tt
+          in
+           synthesized
+         else
+          (* We are already in an inner-type and Coscoy's double *)
+          (* type inference algorithm has not been applied.      *)
+          CicReduction.whd context (T.type_of_aux' metasenv context tt)
         in
          let innersort = T.type_of_aux' metasenv context innertype in
           let ainnertype =
@@ -203,8 +213,6 @@ let acic_of_cic_context metasenv context t =
    ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
 
-exception Found of (Cic.name * Cic.context_entry) list;;
-
 let acic_object_of_cic_object obj =
  let module C = Cic in
   let ids_to_terms = Hashtbl.create 503 in