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 = MQueryLevels2.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
;;
(*
(* to be used on "obj" *)
let add_user_must33 user_must must =
List.map2
- (fun (b, i) (p, u) -> U.set_full_position p (if b then i else None), u)
- user_must must
+ (fun (b, i) (p, u) ->
+ if b then Some (U.set_full_position p i, u) else None)
+ user_must must
in
(* to be used on "rel" *)
let add_user_must22 user_must must =
List.map2
- (fun (b, i) p -> U.set_main_position p (if b then i else None))
- user_must must
+ (fun (b, i) p -> if b then Some (U.set_main_position p i) else None)
+ user_must must
in
(* to be used on "sort" *)
let add_user_must32 user_must must =
List.map2
- (fun (b, i) (p, s) -> U.set_main_position p (if b then i else None), s)
- user_must must
+ (fun (b, i) (p, s)-> if b then Some (U.set_main_position p i, s) else None)
+ 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] ->
(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
+ let rec filter_some =
+ function
+ [] -> []
+ | None::tl -> filter_some tl
+ | (Some x)::tl -> x::(filter_some tl)
+ in
+ filter_some (add_user_must33 user_obj obj),
+ filter_some (add_user_must22 user_rel rel),
+ filter_some (add_user_must32 user_sort sort)
in
(must', only')
| _ -> failwith ("Can't parse constraint string: " ^ constraints)
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
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 ;
projects / helm.git / blobdiff