- added and exposed get_current_status_as_xml

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

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index 80bbdf1b62682caed44567599f4809a4f8af8836..968d2a35e8d6439c65c0549bc35d7f58c372f383 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.ml
+++ b/helm/gTopLevel/mQueryLevels2.ml
@@ -80,7 +80,7 @@ let get_constraints term =
        let kind',depth = !!kind in
         (match depth with
             None -> [],[],[]
-          | Some d -> [],[kind',d],[])
+          | Some d -> [],[kind',Some d],[])
     | C.Sort s ->
        (match kind with
            Backbone _
@@ -88,7 +88,7 @@ let get_constraints term =
             let s' =
              match s with
                 Cic.Prop ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prod"
+                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
               | Cic.Set ->
                  "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
               | Cic.Type ->
@@ -97,7 +97,7 @@ let get_constraints term =
              let kind',depth = !!kind in
               (match depth with
                   None -> assert false
-                | Some d -> [],[],[kind',d,s'])
+                | Some d -> [],[],[kind',Some d,s'])
          | _ -> [],[],[])
     | C.Meta _
     | C.Implicit -> assert false
@@ -166,14 +166,16 @@ let get_constraints term =
    (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
    ([],[],[])
 in
- process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term),
-  (None,None,None)
+ let obj_constraints,rel_constraints,sort_constraints =
+  process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
+ in
+  (obj_constraints,rel_constraints,sort_constraints)
 ;;
 
 (*CSC: Debugging only *)
 let get_constraints term =
  let res = get_constraints term in
- let ((objs,rels,sorts),can) = res in
+ let (objs,rels,sorts) = res in
   prerr_endline "Constraints on objs:" ;
   List.iter
    (function (s1,s2,n) ->
@@ -184,10 +186,15 @@ let get_constraints term =
   prerr_endline "Constraints on Rels:" ;
   List.iter
    (function (s,n) ->
-     prerr_endline (s ^ " " ^ string_of_int n)) rels ;
+     prerr_endline
+      (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
+   ) rels ;
   prerr_endline "Constraints on Sorts:" ;
   List.iter
    (function (s1,n,s2) ->
-     prerr_endline (s1 ^ " " ^ string_of_int n ^ " " ^ s2)) sorts ;
+     prerr_endline
+      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
+        " " ^ s2)
+   ) sorts ;
   res
 ;;