...

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

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 81e94419699624d13c167accbe0b8bccff80f3e7..f08bb877a1029eac2d5ee939245e76d431a329e0 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -70,14 +70,14 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
       (*CSC: This is a very inefficient way of computing inner types *)
       (*CSC: and inner sorts: very deep terms have their types/sorts *)
       (*CSC: computed again and again.                               *)
-      let string_of_sort =
-       function 
+      let string_of_sort t =
+       match CicReduction.whd context t with 
           C.Sort C.Prop -> "Prop"
         | C.Sort C.Set  -> "Set"
         | C.Sort C.Type -> "Type"
         | _ -> assert false
       in
-       let ainnertypes,innertype,innersort =
+       let ainnertypes,innertype,innersort,expected_available =
 (*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 poor. As a very weak    *)
@@ -94,21 +94,23 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
            D.expected = None}
         in
          let innersort = T.type_of_aux' metasenv context synthesized in
-          let ainnertypes =
+          let ainnertypes,expected_available =
            if computeinnertypes then
-            Some
-             {annsynthesized =
-               aux false (Some fresh_id'') context synthesized ;
-              annexpected =
+            let annexpected,expected_available =
                match expected with
-                  None -> None
+                  None -> None,false
                 | Some expectedty' ->
-                   Some (aux false (Some fresh_id'') context expectedty')
-             }
+                   Some (aux false (Some fresh_id'') context expectedty'),true
+            in
+             Some
+              {annsynthesized =
+                aux false (Some fresh_id'') context synthesized ;
+               annexpected = annexpected
+              }, expected_available
            else
-            None
+            None,false
           in
-           ainnertypes, synthesized, string_of_sort innersort
+           ainnertypes,synthesized, string_of_sort innersort, expected_available
        in
         let add_inner_type id =
          match ainnertypes with
@@ -123,15 +125,29 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                | _ -> raise NameExpected
              in
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+              if innersort = "Prop"  && expected_available then
+               add_inner_type fresh_id'' ;
               C.ARel (fresh_id'', n, id)
           | C.Var uri ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             if innersort = "Prop"  && expected_available then
+              add_inner_type fresh_id'' ;
              C.AVar (fresh_id'', uri)
           | C.Meta (n,l) ->
+             let (_,canonical_context,_) =
+              List.find (function (m,_,_) -> n = m) metasenv
+             in
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             if innersort = "Prop"  && expected_available then
+              add_inner_type fresh_id'' ;
              C.AMeta (fresh_id'', n,
-              (List.map
-                (function None -> None | Some t -> Some (aux' context t)) l))
+              (List.map2
+                (fun ct t ->
+                  match (ct, t) with
+                  | None, _ -> None
+                  | _, Some t -> Some (aux' context t)
+                  | Some _, None -> assert false (* due to typing rules *))
+                canonical_context l))
           | C.Sort s -> C.ASort (fresh_id'', s)
           | C.Implicit -> C.AImplicit (fresh_id'')
           | C.Cast (v,t) ->
@@ -157,17 +173,19 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                        C.Lambda _ -> true
                      | _ -> false
                in
-                if not father_is_lambda then
+                if (not father_is_lambda) || expected_available then
                  add_inner_type fresh_id''
               end ;
              C.ALambda
               (fresh_id'',n, aux' context s,
                aux' ((Some (n, C.Decl s)::context)) t)
           | C.LetIn (n,s,t) ->
-            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
-            C.ALetIn
-             (fresh_id'', n, aux' context s,
-              aux' ((Some (n, C.Def s))::context) t)
+             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             if innersort = "Prop" then
+              add_inner_type fresh_id'' ;
+             C.ALetIn
+              (fresh_id'', n, aux' context s,
+               aux' ((Some (n, C.Def s))::context) t)
           | C.Appl l ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
@@ -175,10 +193,14 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
              C.AAppl (fresh_id'', List.map (aux' context) l)
           | C.Const (uri,cn) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             if innersort = "Prop"  && expected_available then
+              add_inner_type fresh_id'' ;
              C.AConst (fresh_id'', uri, cn)
           | C.MutInd (uri,cn,tyno) -> C.AMutInd (fresh_id'', uri, cn, tyno)
           | C.MutConstruct (uri,cn,tyno,consno) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             if innersort = "Prop"  && expected_available then
+              add_inner_type fresh_id'' ;
              C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
           | C.MutCase (uri, cn, tyno, outty, term, patterns) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;