X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Fcic2acic.ml;h=3285dcc15fc53e343ffbe7a5de18d2a6a6ea9de8;hb=HEAD;hp=b039b7e5ba0405ea1ca507916eff07935c7a131c;hpb=c031aa4ca97d0d563a772d7bd247ff7814c51b04;p=helm.git

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index b039b7e5b..3285dcc15 100644
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -25,19 +25,22 @@
 
 (* $Id$ *)
 
-type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
+type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp of CicUniv.universe | `NType of string | `NCProp of string]
 
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
-  | `CProp -> "CProp"
+  | `NType s -> "Type[" ^ s ^ "]"
+  | `NCProp s -> "CProp[" ^ s ^ "]"
+  | `CProp u -> "CProp:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
+
 
 let sort_of_sort = function
   | Cic.Prop  -> `Prop
   | Cic.Set   -> `Set
   | Cic.Type u -> `Type u
-  | Cic.CProp -> `CProp
+  | Cic.CProp u -> `CProp u
 
 (* let hashtbl_add_time = ref 0.0;; *)
 
@@ -149,7 +152,7 @@ let acic_of_cic_context' ~computeinnertypes:global_computeinnertypes
         | C.Sort C.Set   -> `Set
         | C.Sort (C.Type u) -> `Type u
         | C.Meta _       -> `Type (CicUniv.fresh())
-        | C.Sort C.CProp -> `CProp
+        | C.Sort (C.CProp u) -> `CProp u
         | t              ->
             prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
             assert false
@@ -489,7 +492,7 @@ let asequent_of_sequent (metasenv:Cic.metasenv) (sequent:Cic.conjecture) =
       ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses))
 ;;
 
-let acic_object_of_cic_object ?(eta_fix=false) obj =
+let acic_term_or_object_of_cic_term_or_object ?(eta_fix=false) () =
  let module C = Cic in
  let module E = Eta_fixing in
   let ids_to_terms = Hashtbl.create 503 in
@@ -511,6 +514,19 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
    let eta_fix_and_unshare metasenv context t =
     let t = if eta_fix then E.eta_fix metasenv context t else t in
      Unshare.unshare t in
+   (fun context t ->
+     let map = function
+        | None                     -> None
+	| Some (n, C.Decl ty)      -> Some (n, C.Decl (Unshare.unshare ty))
+        | Some (n, C.Def (bo, ty)) ->
+	    Some (n, C.Def (Unshare.unshare bo, Unshare.unshare ty))
+     in
+     let t = Unshare.unshare t in
+     let context = List.map map context in
+     let idrefs = List.map (function _ -> gen_id seed) context in
+     let t = acic_term_of_cic_term_context' ~computeinnertypes:true [] context idrefs t None in
+     t, ids_to_inner_sorts, ids_to_inner_types
+   ),(function obj ->
    let aobj =
     match obj with
       C.Constant (id,Some bo,ty,params,attrs) ->
@@ -632,7 +648,10 @@ let acic_object_of_cic_object ?(eta_fix=false) obj =
    in
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses
-;;
+);;
+
+let acic_object_of_cic_object ?eta_fix =
+   snd (acic_term_or_object_of_cic_term_or_object ?eta_fix ()) 
 
 let plain_acic_term_of_cic_term =
  let module C = Cic in
@@ -773,3 +792,6 @@ let plain_acic_object_of_cic_object obj =
      in
       C.AInductiveDefinition ("mettereaposto",atys,params,paramsno,attrs)
 ;;
+
+let acic_term_of_cic_term ?eta_fix =
+   fst (acic_term_or_object_of_cic_term_or_object ?eta_fix ())