+let refine_constraints (constr_obj, constr_rel, constr_sort) =
+ function
+ "/searchPattern" ->
+ (constr_obj, constr_rel, constr_sort),
+ (Some constr_obj, Some constr_rel, Some constr_sort)
+ | "/matchConclusion" ->
+ let constr_obj' =
+ List.map
+ (function (uri,pos,_) -> (uri,pos,None))
+ (List.filter
+ (function (uri,pos,depth) as constr ->
+ pos="http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
+ or
+ pos="http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
+ ) constr_obj)
+ in
+ (*CSC: we must select the must constraints here!!! *)
+ (constr_obj',[],[]),(Some constr_obj', None, None)
+ | _ -> assert false
+in
+
+let get_constraints term =
+ function
+ "/locateInductivePrinciple" ->
+ let uri =
+ match term with
+ Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
+ | _ -> raise NotAnInductiveDefinition
+ in
+ let constr_obj =
+ [uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis",
+ None ;
+ uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+ Some 0
+ ]
+ in
+ let constr_rel =
+ ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion",
+ None] in
+ let constr_sort =
+ ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
+ Some 1, "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"]
+ in
+ (constr_obj, constr_rel, constr_sort), (None,None,None)
+ | req_path ->
+ let must = MQueryLevels2.get_constraints term in
+ refine_constraints must req_path
+in