Inner-types a la Coscoy now correctly generated even for atoms.

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index df3bdabf905f56cde36802c5f7fe9c8a82ae41f5..7c18674a865ac9eea2fc2df00b389ebd470ebb3e 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -100,6 +100,7 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
                match expected with
                   None -> None,false
                 | Some expectedty' ->
+prerr_endline ("###: " ^ CicPp.ppterm synthesized ^ " <==> " ^ CicPp.ppterm expectedty') ; flush stderr ;
                    Some (aux false (Some fresh_id'') context expectedty'),true
             in
              Some
@@ -125,12 +126,18 @@ 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) ->
              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))
@@ -166,10 +173,12 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
               (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
@@ -177,10 +186,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 ;

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index 024f49ebf6732ca6bf4ad6e82d5011007c1012b7..f58c554fb0990a005f4f790c9691c305ce19cfa9 100644 (file)
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -308,19 +308,24 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
      | C.Appl (he::tl) when List.length tl > 0 ->
-        let hetype = type_of_aux context he None in
-        let tlbody_and_type =
-         let rec aux =
-          function
-             _,[] -> []
-           | C.Prod (n,s,t),he::tl ->
-              (he, type_of_aux context he (Some (head_beta_reduce s)))::
-               (aux (R.whd context (S.subst he t), tl))
-           | _ -> assert false
-         in
-          aux (R.whd context hetype, tl)
+        let expected_hetype =
+         (* Inefficient, the head is computed twice. But I know *)
+         (* of no other solution.                               *)
+         R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
         in
-         eat_prods context hetype tlbody_and_type
+         let hetype = type_of_aux context he (Some expected_hetype) in
+         let tlbody_and_type =
+          let rec aux =
+           function
+              _,[] -> []
+            | C.Prod (n,s,t),he::tl ->
+               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+                (aux (R.whd context (S.subst he t), tl))
+            | _ -> assert false
+          in
+           aux (expected_hetype, tl)
+         in
+          eat_prods context hetype tlbody_and_type
      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
      | C.Const (uri,cookingsno) ->
         cooked_type_of_constant uri cookingsno