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)
(* 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" ->
- 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)
- | req_path ->
- let must = CGSearchPattern.get_constraints term in
- refine_constraints must req_path
+ | "/locateInductivePrinciple" ->
+ None,
+ (CGLocateInductive.get_constraints term),
+ (None,None,None)
+ | "/searchPattern" ->
+ let constr_obj, constr_rel, constr_sort =
+ CGSearchPattern.get_constraints term in
+ (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
+ (Some CGMatchConclusion.universe),
+ (List.nth list_of_must block, [], []), (Some only, None, None)
+ | _ -> assert false
;;
(*
if List.mem server_and_port valid_servers then
Http_daemon.respond
~headers:["Content-Type", "text/html"]
- ~body:(Http_client.Convenience.http_get url)
+ ~body:(Http_client.http_get url)
outchan
else
Http_daemon.respond
let set_metasenv metasenv =
CicTextualParser0.metasenv := metasenv
- let output_html = prerr_endline
+ let output_html ?(append_NL = true) html_msg =
+ let rec collect_string = function
+ | `BR -> "\n"
+ | `T s -> s
+ | `L tags -> String.concat "" (List.map collect_string tags)
+ in
+ match html_msg with
+ | `Error msg | `Msg msg ->
+ (if append_NL then prerr_endline else prerr_string)
+ (collect_string msg ^ (if append_NL then "\n" else ""))
let interactive_user_uri_choice
~selection_mode ?ok
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 ;