- added and exposed get_current_status_as_xml

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

diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml
index f50d94c2c4d62acdd8768bda3a0bc503910d2420..977638dba90adbb4d3dbd4008a5d25cc60b5f92a 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.ml
+++ b/helm/gTopLevel/mQueryLevels.ml
@@ -33,10 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* level managing functions *************************************************)
-
-type levels_spec = (string * bool * int) list
-
 let levels_of_term metasenv context term =
    let module TC = CicTypeChecker in
    let module Red = CicReduction in
@@ -130,14 +126,23 @@ let levels_of_term metasenv context term =
    in 
    inspect_backbone term  
 
-let string_of_levels l sep =
-   let entry_out (s, b, v) =
-      let pos = if b then " HEAD: " else " TAIL: " in
-      string_of_int v ^ pos ^ s ^ sep 
-   in
-   let rec levels_out = function
-      | []           -> ""
-      | head :: tail -> entry_out head ^ levels_out tail
-   in
-   levels_out l
-
+let out_restr e c t =   
+  let can = levels_of_term e c t in  (* can restrictions *)
+prerr_endline "";
+prerr_endline
+ ("#### IN LEVELS @@@@ lunghezza can: " ^ string_of_int (List.length can));
+prerr_endline "";
+(*  let rest = restrict level levels in   *)
+  let uri_pos (u,b,v) = (u,b) in
+  let can_use = List.map uri_pos can in
+  let lofl (u,b,v) = [(u,b)] in
+  let rec organize_restr rlist prev_r= 
+    match rlist with
+      [] -> []
+    | r::tl ->let curr_r = r@prev_r in
+                curr_r::(organize_restr tl curr_r)
+  in
+  let mrest = List.map lofl can in
+  let must_use = organize_restr mrest [] in (* must restrictions *)
+  (must_use,can_use)
+;;