Pcre.regexp "@VARIABLES_INITIALIZATION@")
let server_and_port_url_RE = Pcre.regexp "^http://([^/]+)/.*$"
-exception NotAnInductiveDefinition
-
let port =
try
int_of_string (Sys.getenv port_env_var)
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 =
- [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
- in
- let constr_rel = [`MainConclusion None] in
- let constr_sort = [(`MainHypothesis (Some 1), T.Prop)] in
- U.universe_for_search_pattern,
- (constr_obj, constr_rel, constr_sort), (None,None,None)
+ None,
+ (CGLocateInductive.get_constraints term),
+ (None,None,None)
| "/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)
+ (Some CGSearchPattern.universe),
+ (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,
+ (Some CGMatchConclusion.universe),
(List.nth list_of_must block, [], []), (Some only, None, None)
| _ -> assert false
;;
let msg = Pcre.replace ~pat:"\'" ~templ:"\\\'" msg in
(match selection_mode with
| `SINGLE -> assert false
- | `EXTENDED ->
+ | `MULTIPLE ->
Http_daemon.send_basic_headers ~code:200 outchan ;
Http_daemon.send_CRLF outchan ;
iter_file
raise Chat_unfinished)
in
let query =
- G.query_of_constraints (Some universe) must'' only'
+ G.query_of_constraints universe must'' only'
in
let results = MQueryInterpreter.execute mqi_handle query in
Http_daemon.send_basic_headers ~code:200 outchan ;