Changed type of ids_to_inner_sort table used in transformation.

[helm.git] / helm / ocaml / cic_transformations / cic2Xml.ml

diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml
index 5d614db055d92d8cd570f7f93c1b79bb6766296d..3be3ba7f115ea5cc7b8cd72e624f6a30c7cdbf07 100644 (file)
--- a/helm/ocaml/cic_transformations/cic2Xml.ml
+++ b/helm/ocaml/cic_transformations/cic2Xml.ml
@@ -41,24 +41,27 @@ let param_attribute_of_params params =
 
 (*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
 let print_term ~ids_to_inner_sorts =
+ let find_sort id =
+   Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
+ in
  let rec aux =
   let module C = Cic in
   let module X = Xml in
   let module U = UriManager in
     function
        C.ARel (id,idref,n,b) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_empty "REL"
           [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
            None,"idref",idref ; None,"sort",sort]
      | C.AVar (id,uri,exp_named_subst) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          aux_subst uri
           (X.xml_empty "VAR"
             [None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
           exp_named_subst
      | C.AMeta (id,n,l) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "META"
           [None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
           (List.fold_left
@@ -70,12 +73,8 @@ let print_term ~ids_to_inner_sorts =
                   [< i ; X.xml_empty "substitution" [] >]
             ) [< >] l)
      | C.ASort (id,s) ->
-        let string_of_sort =
-         function
-            C.Prop  -> "Prop"
-          | C.Set   -> "Set"
-          | C.Type _ -> "Type" (* TASSI *)
-         | C.CProp -> "CProp"
+        let string_of_sort s =
+          Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
         in
          X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
      | C.AImplicit _ -> raise NotImplemented
@@ -88,13 +87,11 @@ let print_term ~ids_to_inner_sorts =
           | t -> [],t
         in
          let prods,t = eat_prods prods in
-          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+          let sort = find_sort last_id in
            X.xml_nempty "PROD" [None,"type",sort]
             [< List.fold_left
                 (fun i (id,binder,s) ->
-                  let sort =
-                   Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
-                  in
+                  let sort = find_sort (Cic2acic.source_id_of_id id) in
                    let attrs =
                     (None,"id",id)::(None,"type",sort)::
                     match binder with
@@ -106,7 +103,7 @@ let print_term ~ids_to_inner_sorts =
                X.xml_nempty "target" [] (aux t)
             >]
      | C.ACast (id,v,t) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
           [< X.xml_nempty "term" [] (aux v) ;
              X.xml_nempty "type" [] (aux t)
@@ -120,13 +117,11 @@ let print_term ~ids_to_inner_sorts =
           | t -> [],t
         in
          let lambdas,t = eat_lambdas lambdas in
-          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+          let sort = find_sort last_id in
            X.xml_nempty "LAMBDA" [None,"sort",sort]
             [< List.fold_left
                 (fun i (id,binder,s) ->
-                  let sort =
-                   Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id)
-                  in
+                  let sort = find_sort (Cic2acic.source_id_of_id id) in
                    let attrs =
                     (None,"id",id)::(None,"type",sort)::
                     match binder with
@@ -148,11 +143,11 @@ let print_term ~ids_to_inner_sorts =
           | t -> [],t
         in
          let letins,t = eat_letins letins in
-          let sort = Hashtbl.find ids_to_inner_sorts last_id in
+          let sort = find_sort last_id in
            X.xml_nempty "LETIN" [None,"sort",sort]
             [< List.fold_left
                 (fun i (id,binder,s) ->
-                  let sort = Hashtbl.find ids_to_inner_sorts id in
+                  let sort = find_sort id in
                    let attrs =
                     (None,"id",id)::(None,"sort",sort)::
                     match binder with
@@ -164,12 +159,12 @@ let print_term ~ids_to_inner_sorts =
                X.xml_nempty "target" [] (aux t)
             >]
      | C.AAppl (id,li) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
           [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
           >]
      | C.AConst (id,uri,exp_named_subst) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          aux_subst uri
           (X.xml_empty "CONST"
             [None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
@@ -182,7 +177,7 @@ let print_term ~ids_to_inner_sorts =
             None, "id", id]
          ) exp_named_subst
      | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          aux_subst uri
           (X.xml_empty "MUTCONSTRUCT"
             [None,"uri", (U.string_of_uri uri) ;
@@ -191,7 +186,7 @@ let print_term ~ids_to_inner_sorts =
              None,"id",id ; None,"sort",sort]
           ) exp_named_subst
      | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "MUTCASE"
           [None,"uriType",(U.string_of_uri uri) ;
            None,"noType", (string_of_int typeno) ;
@@ -203,7 +198,7 @@ let print_term ~ids_to_inner_sorts =
               patterns [<>]
           >]
      | C.AFix (id, no, funs) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "FIX"
           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
           [< List.fold_right
@@ -219,7 +214,7 @@ let print_term ~ids_to_inner_sorts =
               ) funs [<>]
           >]
      | C.ACoFix (id,no,funs) ->
-        let sort = Hashtbl.find ids_to_inner_sorts id in
+        let sort = find_sort id in
          X.xml_nempty "COFIX"
           [None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
           [< List.fold_right
@@ -269,6 +264,9 @@ let print_term ~ids_to_inner_sorts =
 let xml_of_attrs attributes = [< >]
 
 let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+ let find_sort id =
+   Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)
+ in
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
@@ -436,7 +434,8 @@ let
                 [< print_term ids_to_inner_sorts synty >] ;
                  match expty with
                    None -> [<>]
-                 | Some expty' -> X.xml_nempty "expected" [] [< print_term ids_to_inner_sorts expty' >]
+                 | Some expty' -> X.xml_nempty "expected" []
+                    [< print_term ids_to_inner_sorts expty' >]
                >]
            >]
          ) ids_to_inner_types [<>]