X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2acic.ml;h=608f6d7c3aa8af0faf616c448a2f693bb75de074;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=cf9760c2565dd4ae86c6ae445a1c62ee0ae88c6f;hpb=7df065750ec593fb409ae8627f81927397602b9b;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index cf9760c25..608f6d7c3 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -23,23 +23,44 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let hashtbl_add_time = ref 0.0;;
+type sort_kind = [ `Prop | `Set | `Type | `CProp ]
+
+let sort_of_string = function
+  | "Prop" -> `Prop
+  | "Set" -> `Set
+  | "Type" -> `Type
+  | "CProp" -> `CProp
+  | _ -> assert false
+
+let string_of_sort = function
+  | `Prop -> "Prop"
+  | `Set -> "Set"
+  | `Type -> "Type"
+  | `CProp -> "CProp"
+
+let sort_of_sort = function
+  | Cic.Prop  -> `Prop
+  | Cic.Set   -> `Set
+  | Cic.Type _ -> `Type
+  | Cic.CProp -> `CProp
+
+(* let hashtbl_add_time = ref 0.0;; *)
 
 let xxx_add h k v =
- let t1 = Sys.time () in
+(*  let t1 = Sys.time () in *)
   Hashtbl.add h k v ;
-  let t2 = Sys.time () in
-   hashtbl_add_time := !hashtbl_add_time +. t2 -. t1
+(*   let t2 = Sys.time () in
+   hashtbl_add_time := !hashtbl_add_time +. t2 -. t1 *)
 ;;
 
-let number_new_type_of_aux' = ref 0;;
-let type_of_aux'_add_time = ref 0.0;;
+(* let number_new_type_of_aux' = ref 0;;
+let type_of_aux'_add_time = ref 0.0;; *)
 
 let xxx_type_of_aux' m c t =
- let t1 = Sys.time () in
+(*  let t1 = Sys.time () in *)
  let res,_ = CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph in
- let t2 = Sys.time () in
- type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
+(*  let t2 = Sys.time () in
+ type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ; *)
  res
 ;;
 
@@ -83,8 +104,8 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
 (*    let time1 = Sys.time () in *)
    let terms_to_types =
-     let time0 = Sys.time () in
 (*
+     let time0 = Sys.time () in
      let prova = CicTypeChecker.type_of_aux' metasenv context t in
      let time1 = Sys.time () in
      prerr_endline ("*** Fine type_inference:" ^ (string_of_float (time1 -. time0)));
@@ -109,17 +130,15 @@ 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 t =
+      let sort_of t =
        match CicReduction.whd context t with 
-          C.Sort C.Prop  -> "Prop"
-        | C.Sort C.Set   -> "Set"
-        | C.Sort (C.Type _) -> "Type" (* TASSI OK*)
-        | C.Sort C.CProp -> "CProp"
-        | C.Meta _       ->
-prerr_endline "Cic2acic: string_of_sort applied to a meta" ;
-           "?"
+          C.Sort C.Prop  -> `Prop
+        | C.Sort C.Set   -> `Set
+        | C.Sort (C.Type _)
+        | C.Meta _       -> `Type
+        | C.Sort C.CProp -> `CProp
         | t              ->
-prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ;
+            prerr_endline ("Cic2acic.sort_of applied to: " ^ CicPp.ppterm t) ;
             assert false
       in
        let ainnertypes,innertype,innersort,expected_available =
@@ -144,7 +163,7 @@ prerr_endline ("Cic2acic: string_of_sort applied to: " ^ CicPp.ppterm t) ;
 Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
           D.expected = None}
         in
-         incr number_new_type_of_aux' ;
+(*          incr number_new_type_of_aux' ; *)
          let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
           let ainnertypes,expected_available =
            if computeinnertypes then
@@ -164,12 +183,12 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
            else
             None,false
           in
-           ainnertypes,synthesized, string_of_sort innersort, expected_available
+           ainnertypes,synthesized, sort_of innersort, expected_available
 (*XXXXXXXX *)
         with
          Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
           (* CSC: Type or Set? I can not tell *)
-          None,Cic.Sort (Cic.Type (CicUniv.fresh())),"Type",false 
+          None,Cic.Sort (Cic.Type (CicUniv.fresh())),`Type,false 
 	  (* TASSI non dovrebbe fare danni *)
 (* *)
        in
@@ -186,12 +205,12 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
                | _ -> "__" ^ string_of_int n
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-              if innersort = "Prop"  && expected_available then
+              if innersort = `Prop  && expected_available then
                add_inner_type fresh_id'' ;
               C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
           | C.Var (uri,exp_named_subst) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop"  && expected_available then
+             if innersort = `Prop  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
               List.map
@@ -201,7 +220,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
           | C.Meta (n,l) ->
              let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop"  && expected_available then
+             if innersort = `Prop  && expected_available then
               add_inner_type fresh_id'' ;
              C.AMeta (fresh_id'', n,
               (List.map2
@@ -215,15 +234,15 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
           | C.Implicit annotation -> C.AImplicit (fresh_id'', annotation)
           | C.Cast (v,t) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop" then
+             if innersort = `Prop then
               add_inner_type fresh_id'' ;
              C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
           | C.Prod (n,s,t) ->
               xxx_add ids_to_inner_sorts fresh_id''
-               (string_of_sort innertype) ;
+               (sort_of innertype) ;
 	            let sourcetype = xxx_type_of_aux' metasenv context s in
 	             xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
-	              (string_of_sort sourcetype) ;
+	              (sort_of sourcetype) ;
               let n' =
                match n with
                   C.Anonymous -> n
@@ -240,8 +259,8 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
 	           let sourcetype = xxx_type_of_aux' metasenv context s in
 	            xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
-	             (string_of_sort sourcetype) ;
-              if innersort = "Prop" then
+	             (sort_of sourcetype) ;
+              if innersort = `Prop then
                begin
                 let father_is_lambda =
                  match father with
@@ -259,19 +278,19 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop" then
+             if innersort = `Prop then
               add_inner_type fresh_id'' ;
              C.ALetIn
               (fresh_id'', n, aux' context idrefs s,
                aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop" then
+             if innersort = `Prop then
               add_inner_type fresh_id'' ;
              C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
           | C.Const (uri,exp_named_subst) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop"  && expected_available then
+             if innersort = `Prop  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
               List.map
@@ -286,7 +305,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
               C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
           | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop"  && expected_available then
+             if innersort = `Prop  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
               List.map
@@ -295,7 +314,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
               C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
           | C.MutCase (uri, tyno, outty, term, patterns) ->
              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop" then
+             if innersort = `Prop then
               add_inner_type fresh_id'' ;
              C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
               aux' context idrefs term, List.map (aux' context idrefs) patterns)
@@ -307,7 +326,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
               List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-              if innersort = "Prop" then
+              if innersort = `Prop then
                add_inner_type fresh_id'' ;
               C.AFix (fresh_id'', funno,
                List.map2
@@ -324,7 +343,7 @@ Cic.Sort (Cic.Type (CicUniv.fresh())); (* TASSI: non dovrebbe fare danni *)
               List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
              in
               xxx_add ids_to_inner_sorts fresh_id'' innersort ;
-              if innersort = "Prop" then
+              if innersort = `Prop then
                add_inner_type fresh_id'' ;
               C.ACoFix (fresh_id'', funno,
                List.map2