(* SEARCH ENGINE functions *)
-let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =
- function
- "/searchPattern" ->
- U.universe_for_search_pattern,
- (constr_obj, constr_rel, constr_sort),
- (Some constr_obj, Some constr_rel, Some constr_sort)
- | "/matchConclusion" ->
- let constr_obj' =
- List.map
- (function (pos, uri) -> U.set_full_position pos None, uri)
- (List.filter
- (function (pos, _) -> U.is_conclusion pos)
- constr_obj)
- in
- U.universe_for_match_conclusion,
- (*CSC: we must select the must constraints here!!! *)
- (constr_obj',[],[]),(Some constr_obj', None, None)
- | _ -> assert false
-;;
-
let get_constraints term =
function
- "/locateInductivePrinciple" ->
+ | "/locateInductivePrinciple" ->
let uri =
match term with
Cic.MutInd (uri,t,_) -> MQueryUtil.string_of_uriref (uri,[t])
let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
U.universe_for_search_pattern,
(constr_obj, constr_rel, constr_sort), (None,None,None)
- | req_path ->
- let must = CGSearchPattern.get_constraints term in
- refine_constraints must req_path
+ | "/searchPattern" ->
+ let constr_obj, constr_rel, constr_sort =
+ CGSearchPattern.get_constraints term in
+ U.universe_for_search_pattern,
+ (constr_obj, constr_rel, constr_sort),
+ (Some constr_obj, Some constr_rel, Some constr_sort)
+ | "/matchConclusion" ->
+ let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in
+(* FG: there is no way to choose the block number ***************************)
+ let block = pred (List.length list_of_must) in
+ U.universe_for_match_conclusion,
+ (List.nth list_of_must block, [], []), (Some only, None, None)
+ | _ -> assert false
;;
(*