From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Dec 2002 13:15:28 +0000 (+0000)
Subject: 1. The depth constraint on Rels and Sorts is now optional.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e220814540ca1c8dd99189ad7bdb8838764650e;p=helm.git

1. The depth constraint on Rels and Sorts is now optional.
2. "only" (ex "can") constraints are copies of the "must" constraints
---

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index c4bf895dd..afd0ee42b 100644
--- 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 _
@@ -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,8 +166,11 @@ 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),
+   (Some obj_constraints,Some rel_constraints,Some sort_constraints)
 ;;
 
 (*CSC: Debugging only *)
@@ -184,10 +187,16 @@ 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 ;
+  prerr_endline "The \"only\" constraints are the same." ;
   res
 ;;
diff --git a/helm/gTopLevel/mQueryLevels2.mli b/helm/gTopLevel/mQueryLevels2.mli
index 822564d3a..584ec6909 100644
--- a/helm/gTopLevel/mQueryLevels2.mli
+++ b/helm/gTopLevel/mQueryLevels2.mli
@@ -35,10 +35,4 @@
 
 val get_constraints:
  Cic.term ->
-(*
-  MQueryGenerator.must_restrictions * MQueryGenerator.can_restrictions
-*)
- ((string * string * int option) list * (string * int) list *
-  (string * int * string) list) *
- ((string * string * int option) list option * (string * int) list option *
-  (string * int * string) list option)
+  MQueryGenerator.must_restrictions * MQueryGenerator.only_restrictions