(* 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 = MQueryLevels2.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
;;
(*
let result = MQueryInterpreter.execute mqi_handle query in
C.close mqi_handle;
Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
+ | "/unreferred" ->
+ let mqi_handle = C.init mqi_flags debug_print in
+ let target = req#param "target" in
+ let source = req#param "source" in
+ let query = G.unreferred target source in
+ let result = MQueryInterpreter.execute mqi_handle query in
+ C.close mqi_handle;
+ Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
| "/getpage" ->
(* TODO implement "is_permitted" *)
(let is_permitted _ = true in