+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 -> is_concl_pos pos)
+ 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
+
+(*
+ format:
+ <must_obj> ':' <must_rel> ':' <must_sort> ':' <only_obj> ':' <only_rel> ':' <only_sort>
+
+ <must_*> ::= ('0'|'1') ('_'|<int>) (',' ('0'|'1') ('_'|<int>))*
+ <only> ::= '0'|'1'
+*)
+let add_user_constraints ~constraints
+ ((obj, rel, sort), (only_obj, only_rel, only_sort))
+=
+ let parse_must s =
+ let l = Pcre.split ~pat:"," s in
+ (try
+ List.map
+ (fun s ->
+ let subs = Pcre.extract ~pat:"^(.)(\\d+|_)$" s in
+ (bool_of_string' subs.(1), int_of_string' subs.(2)))
+ l
+ with
+ Not_found -> failwith ("Can't parse constraint string: " ^ constraints)
+ )
+ in
+ (* to be used on "obj" *)
+ let add_user_must33 user_must must =
+ List.map2
+ (fun (b, i) (p1, p2, p3) -> if b then (p1, p2, i) else (p1, p2, None))
+ user_must must
+ in
+ (* to be used on "rel" *)
+ let add_user_must22 user_must must =
+ List.map2
+ (fun (b, i) (p1, p2) -> if b then (p1, i) else (p1, None))
+ user_must must
+ in
+ (* to be used on "sort" *)
+ let add_user_must32 user_must must =
+ List.map2
+ (fun (b, i) (p1, p2, p3) -> if b then (p1, i, p3) else (p1, None, p3))
+ user_must must
+ in
+ match Pcre.split ~pat:":" constraints with
+ | [user_obj;user_rel;user_sort;user_only_obj;user_only_rel;user_only_sort] ->
+ let
+ (user_obj,user_rel,user_sort,user_only_obj,user_only_rel,user_only_sort)
+ =
+ (parse_must user_obj,
+ parse_must user_rel,
+ parse_must user_sort,
+ bool_of_string' user_only_obj,
+ bool_of_string' user_only_rel,
+ bool_of_string' user_only_sort)
+ in
+ let only' =
+ (if user_only_obj then only_obj else None),
+ (if user_only_rel then only_rel else None),
+ (if user_only_sort then only_sort else None)
+ in
+ let must' =
+ add_user_must33 user_obj obj,
+ add_user_must22 user_rel rel,
+ add_user_must32 user_sort sort
+ in
+ (must', only')
+ | _ -> failwith ("Can't parse constraint string: " ^ constraints)
+in