- shows also version in usage string

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

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index df3bdabf905f56cde36802c5f7fe9c8a82ae41f5..f08bb877a1029eac2d5ee939245e76d431a329e0 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -70,8 +70,8 @@ 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"
@@ -125,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) ->
@@ -166,10 +180,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 +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 ;