* Many improvements

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

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 8b6a257be33b66a6174901893450e625fe4eaefd..789a72b91a34cb9b9b85e240272acc93c538589a 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -48,14 +48,14 @@ let rec get_nth l n =
 ;;
 
 let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
-     metasenv env t
+     ids_to_inner_types metasenv env t
 =
  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 rec aux father bs tt =
+   let rec aux computeinnertypes father bs tt =
     let fresh_id'' = fresh_id' father tt in
-    let aux' = aux (Some fresh_id'') in
+    let aux' = aux true (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 *)
@@ -68,11 +68,22 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
        | C.Sort C.Type -> "Type"
        | _ -> assert false
      in
-      let innertype,innersort =
+      let ainnertype,innertype,innersort =
        let cicenv = List.map (function (_,ty) -> ty) bs in
         let innertype = T.type_of_aux' metasenv cicenv tt in
          let innersort = T.type_of_aux' metasenv cicenv innertype in
-          innertype, string_of_sort innersort
+          let ainnertype =
+           if computeinnertypes then
+            Some (aux false (Some fresh_id'') bs innertype)
+           else
+            None
+          in
+           ainnertype, innertype, string_of_sort innersort
+      in
+      let add_inner_type id =
+       match ainnertype with
+          None -> ()
+        | Some ainnertype -> Hashtbl.add ids_to_inner_types id ainnertype
       in
        match tt with
           C.Rel n ->
@@ -93,6 +104,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
         | C.Implicit -> C.AImplicit (fresh_id'')
         | C.Cast (v,t) ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+           if innersort = "Prop" then
+            add_inner_type fresh_id'' ;
            C.ACast (fresh_id'', aux' bs v, aux' bs t)
         | C.Prod (n,s,t) ->
             Hashtbl.add ids_to_inner_sorts fresh_id''
@@ -100,6 +113,22 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
             C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t)
         | C.Lambda (n,s,t) ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+           if innersort = "Prop" then
+            begin
+             let father_is_lambda =
+              match father with
+                 None -> false
+               | Some father' ->
+                  match Hashtbl.find ids_to_father_ids father' with
+                     None -> assert false
+                   | Some fatherid ->
+                      match Hashtbl.find ids_to_terms fatherid with
+                         C.Lambda _ -> true
+                       | _ -> false
+             in
+              if not father_is_lambda then
+               add_inner_type fresh_id''
+            end ;
            C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
         | C.LetIn (n,s,t) ->
 (*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-(
@@ -108,6 +137,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
 *) assert false
         | C.Appl l ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+           if innersort = "Prop" then
+            add_inner_type fresh_id'' ;
            C.AAppl (fresh_id'', List.map (aux' bs) l)
         | C.Const (uri,cn) ->
            Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
@@ -119,11 +150,15 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
            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 ;
+           if innersort = "Prop" then
+            add_inner_type fresh_id'' ;
            C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
             aux' bs term, List.map (aux' bs) patterns)
         | C.Fix (funno, funs) ->
            let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+            if innersort = "Prop" then
+             add_inner_type fresh_id'' ;
             C.AFix (fresh_id'', funno,
              List.map
               (fun (name, indidx, ty, bo) ->
@@ -133,6 +168,8 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
         | C.CoFix (funno, funs) ->
            let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+            if innersort = "Prop" then
+             add_inner_type fresh_id'' ;
             C.ACoFix (fresh_id'', funno,
              List.map
               (fun (name, ty, bo) ->
@@ -140,17 +177,18 @@ let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
               ) funs
             )
       in
-       aux None env t
+       aux true None env t
 ;;
 
 let acic_of_cic_env metasenv env 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_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
-    metasenv env t,
-   ids_to_terms, ids_to_father_ids, ids_to_inner_sorts
+    ids_to_inner_types metasenv env t,
+   ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
 ;;
 
 exception Found of (Cic.name * Cic.term) list;;
@@ -220,9 +258,11 @@ let acic_object_of_cic_object obj =
   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
   let acic_term_of_cic_term_env' =
-   acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts in
+   acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+    ids_to_inner_types in
   let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in
    let aobj =
     match obj with
@@ -246,5 +286,5 @@ let acic_object_of_cic_object obj =
         C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
     | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
    in
-    aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts
+    aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
 ;;