-DIRS = ocaml hbugs gTopLevel searchEngine
+DIRS = ocaml hbugs gTopLevel searchEngine mathql_test
DIRS_BYTE = $(patsubst %,%.byte,$(DIRS))
DIRS_OPT = $(patsubst %,%.opt,$(DIRS))
module MQI = MQueryInterpreter
module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
GBin.scrolled_window ~border_width:10 ~height ~width:600
~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+ let mutable_ref = ref (Some d) in
+ let depthb =
+ GButton.toggle_button
+ ~label:("depth = " ^ string_of_int d)
+ ~active:true
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore
+ (depthb#connect#toggled
+ (function () ->
+ let sel_depth = if depthb#active then Some d else None in
+ mutable_ref := sel_depth
+ )) ; mutable_ref
+ in
let rel_constraints =
List.map
- (function (position,depth) ->
+ (function p ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:position
+ ~text:(MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button
- ~label:("depth = " ^ string_of_int depth') ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
) must_rel in
(* Sort constraints *)
let label =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let sort_constraints =
List.map
- (function (position,depth,sort) ->
+ (function (p, sort) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(sort ^ " " ^ position)
+ ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None, sort
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref, sort
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, sort
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort
) must_sort in
(* Obj constraints *)
let label =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let obj_constraints =
List.map
- (function (uri,position,depth) ->
+ (function (p, uri) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(uri ^ " " ^ position)
+ ~text:(uri ^ " " ^ (MQGU.text_of_position p))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> uri, position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- uri, position, mutable_ref
+ match p with
+ | `InBody
+ | `InHypothesis
+ | `InConclusion
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, uri
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
) must_obj in
(* Confirm/abort buttons *)
let hbox =
if !chosen then
let chosen_must_rel =
List.map
- (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+ (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+ rel_constraints
+ in
let chosen_must_sort =
List.map
- (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+ (function (position, ref_depth, sort) ->
+ MQGU.set_main_position position !ref_depth,sort)
sort_constraints
in
let chosen_must_obj =
List.map
- (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+ (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
obj_constraints
in
(chosen_must_obj,chosen_must_rel,chosen_must_sort),
let must = MQueryLevels2.get_constraints expr in
let must',only = refine_constraints must in
let query =
- MQG.query_of_constraints
- (Some
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
- ])
- must' only
+ MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.searchPattern
+ TacticChaser.matchConclusion
mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
| hd::tl -> hd
in
let uris =
- TacticChaser.searchPattern mqi_handle
+ TacticChaser.matchConclusion mqi_handle
~output_html:prerr_endline ~choose_must () ~status:(proof, goal)
in
if uris = [] then
--- /dev/null
+*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples*
+mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
--- /dev/null
+mqgtop.cmo: mQGTopLexer.cmo mQGTopParser.cmi
+mqgtop.cmx: mQGTopLexer.cmx mQGTopParser.cmx
+mQGTopParser.cmo: mQGTopParser.cmi
+mQGTopParser.cmx: mQGTopParser.cmi
+mQGTopLexer.cmo: mQGTopParser.cmi
+mQGTopLexer.cmx: mQGTopParser.cmx
--- /dev/null
+BIN_DIR = /usr/local/bin
+REQUIRES = unix helm-cic_textual_parser \
+ helm-mathql helm-mathql_interpreter helm-mathql_generator
+PREDICATES =
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
+OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
+OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
+OCAMLDEP = ocamldep
+OCAMLYACC = ocamlyacc
+OCAMLLEX = ocamllex
+
+LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+
+MQTOP = mqtop.ml
+MQITOP = mqitop.ml
+MQGTOP = mqgtop.ml
+
+DEPOBJS = $(MQTOP) $(MQITOP) $(MQGTOP)
+AUXOBJS = mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
+
+all: $(DEPOBJS:.ml=)
+opt: $(DEPOBJS:.ml=.opt)
+
+depend: $(AUXOBJS)
+ $(OCAMLDEP) $(DEPOBJS) $(AUXOBJS) > .depend
+
+mqtop: $(MQTOP:.ml=.cmo) $(LIBRARIES)
+ $(OCAMLC) -linkpkg -o mqtop $(MQTOP:.ml=.cmo)
+
+mqtop.opt: $(MQTOP:.ml=.cmx) $(LIBRARIES_OPT)
+ $(OCAMLOPT) -linkpkg -o mqtop.opt $(MQTOP:.ml=.cmx)
+
+mqitop: $(MQITOP:.ml=.cmo) $(LIBRARIES)
+ $(OCAMLC) -linkpkg -o mqitop $(MQITOP:.ml=.cmo)
+
+mqitop.opt: $(MQITOP:.ml=.cmx) $(LIBRARIES_OPT)
+ $(OCAMLOPT) -linkpkg -o mqitop.opt $(MQITOP:.ml=.cmx)
+
+mqgtop: mQGTopParser.cmi $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo) $(LIBRARIES)
+ $(OCAMLC) -linkpkg -o mqgtop $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo)
+
+mqgtop.opt: $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx) $(LIBRARIES_OPT)
+ $(OCAMLOPT) -linkpkg -o mqgtop.opt $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx)
+
+.SUFFIXES: .ml .mli .cmo .cmi .cmx .mly .mll
+.ml.cmo: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.mli.cmi: $(LIBRARIES)
+ $(OCAMLC) -c $<
+.ml.cmx: $(LIBRARIES_OPT)
+ $(OCAMLOPT) -c $<
+.mly.ml:
+ $(OCAMLYACC) $<
+.mly.mli:
+ $(OCAMLYACC) $<
+.mll.ml:
+ $(OCAMLLEX) $<
+
+$(DEPOBJS:%.ml=%.cmo): $(LIBRARIES)
+$(DEPOBJS:%.ml=%.cmx): $(LIBRARIES_OPT)
+
+clean:
+ rm -f *.cm[iox] *.o $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) \
+ mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
+
+install:
+ cp $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) $(BIN_DIR)
+
+uninstall:
+ cd $(BIN_DIR)
+ rm -f $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt)
+
+.PHONY: install uninstall clean
+
+ifneq ($(MAKECMDGOALS), depend)
+ include .depend
+endif
+
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+{
+ open MQGTopParser
+
+ let debug = false
+
+ let out s = if debug then prerr_endline s
+}
+
+let SPC = [' ' '\t' '\n']+
+let ALPHA = ['A'-'Z' 'a'-'z' '_']
+let NUM = ['0'-'9']
+let IDEN = ALPHA (NUM | ALPHA)*
+let QSTR = [^ '"' '\\']+
+
+rule comm_token = parse
+ | "(*" { comm_token lexbuf; comm_token lexbuf }
+ | "*)" { () }
+ | ['*' '('] { comm_token lexbuf }
+ | [^ '*' '(']* { comm_token lexbuf }
+and string_token = parse
+ | '"' { DQ }
+ | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) }
+ | QSTR { STR (Lexing.lexeme lexbuf) }
+ | eof { EOF }
+and spec_token = parse
+ | "(*" { comm_token lexbuf; spec_token lexbuf }
+ | SPC { spec_token lexbuf }
+ | '"' { let str = qstr string_token lexbuf in
+ out ("STR " ^ str); STR str }
+ | '{' { out "LC"; LC }
+ | '}' { out "RC"; RC }
+ | ',' { out "CM"; CM }
+ | '$' { out "DL"; DL }
+ | "mustobj" { out "MOBJ" ; MOBJ }
+ | "mustsort" { out "MSORT" ; MSORT }
+ | "mustrel" { out "MREL" ; MREL }
+ | "onlyobj" { out "OOBJ" ; OOBJ }
+ | "onlysort" { out "OSORT" ; OSORT }
+ | "onlyrel" { out "OREL" ; OREL }
+ | "universe" { out "UNIV" ; UNIV }
+ | IDEN { let id = Lexing.lexeme lexbuf in
+ out ("ID " ^ id); ID id }
+ | eof { EOF }
--- /dev/null
+/* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ */
+
+%{
+ let f (x, y, z) = x
+ let s (x, y, z) = y
+ let t (x, y, z) = z
+
+ module T = MQGTypes
+ module U = MQGUtil
+%}
+ %token <string> ID
+ %token <UriManager.uri> CONURI
+ %token <UriManager.uri> VARURI
+ %token <UriManager.uri * int> INDTYURI
+ %token <UriManager.uri * int * int> INDCONURI
+ %token ALIAS EOF
+
+ %start interp
+ %type <CicTextualParser0.interpretation_domain_item -> CicTextualParser0.interpretation_codomain_item option> interp
+
+ %token <string> STR
+ %token DL DQ LC RC CM
+ %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV
+
+ %start qstr specs
+ %type <string> qstr
+ %type <MQGTypes.spec list> specs
+%%
+ uri:
+ | CONURI { CicTextualParser0.ConUri $1 }
+ | VARURI { CicTextualParser0.VarUri $1 }
+ | INDTYURI { CicTextualParser0.IndTyUri ((fst $1), (snd $1)) }
+ | INDCONURI { CicTextualParser0.IndConUri ((f $1), (s $1), (t $1)) }
+ ;
+ alias:
+ | ALIAS ID uri { ($2, CicTextualParser0.Uri $3) }
+ ;
+ aliases:
+ | alias aliases { $1 :: $2 }
+ | EOF { [] }
+ ;
+ interp:
+ | aliases { function CicTextualParser0.Id s -> (try Some (List.assoc s $1)
+ with Not_found -> None)
+ | _ -> None }
+ ;
+
+ qstr:
+ | DQ { "" }
+ | STR qstr { $1 ^ $2 }
+ ;
+ strs:
+ | STR CM strs { $1 :: $3 }
+ | STR { [$1] }
+ | { [] }
+ ;
+ uri_list:
+ | LC strs RC { List.map U.uri_of_mathql $2 }
+ ;
+ sort_list:
+ | LC strs RC { List.map U.sort_of_mathql $2 }
+ ;
+ pos_list:
+ | LC strs RC { List.map U.position_of_mathql $2 }
+ ;
+ depth_list:
+ | LC strs RC { List.map U.depth_of_mathql $2 }
+ ;
+ spec:
+ | MOBJ uri_list pos_list depth_list { T.MustObj ($2, $3, $4) }
+ | MSORT sort_list pos_list depth_list { T.MustSort ($2, $3, $4) }
+ | MREL pos_list depth_list { T.MustRel ($2, $3) }
+ | OOBJ uri_list pos_list depth_list { T.OnlyObj ($2, $3, $4) }
+ | OSORT sort_list pos_list depth_list { T.OnlySort ($2, $3, $4) }
+ | OREL pos_list depth_list { T.OnlyRel ($2, $3) }
+ | UNIV pos_list { T.Universe $2 }
+ ;
+ specs:
+ | spec specs { $1 :: $2 }
+ | EOF { [] }
+ ;
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+let query_num = ref 1
+
+let interp_file = ref "interp.cic"
+
+let log_file = ref ""
+
+let show_queries = ref false
+
+let int_options = ref ""
+
+let nl = " <p>\n"
+
+module U = MQueryUtil
+module I = MQueryInterpreter
+module C = MQIConn
+module G = MQueryGenerator
+module L = MQGTopLexer
+module P = MQGTopParser
+module TL = CicTextualLexer
+module TP = CicTextualParser
+module C2 = MQueryLevels2
+module C1 = MQueryLevels
+module GU = MQGUtil
+
+let get_handle () =
+ C.init (C.flags_of_string ! int_options)
+ (fun s -> print_string s; flush stdout)
+
+let issue handle q =
+ let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
+ let perm = 64 * 6 + 8 * 6 + 4 in
+ let time () =
+ let lt = Unix.localtime (Unix.time ()) in
+ "NEW LOG: " ^
+ string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
+ string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
+ string_of_int (lt.Unix.tm_hour) ^ ":" ^
+ string_of_int (lt.Unix.tm_min) ^ ":" ^
+ string_of_int (lt.Unix.tm_sec)
+ in
+ let log q r =
+ let och = open_out_gen mode perm ! log_file in
+ let out = output_string och in
+ if ! query_num = 1 then out (time () ^ nl);
+ out ("Query: " ^ string_of_int ! query_num ^ nl);
+ U.text_of_query out q nl;
+ out ("Result: " ^ nl);
+ U.text_of_result out r nl;
+ close_out och
+ in
+ if ! show_queries then U.text_of_query (output_string stdout) q nl;
+ let r = I.execute handle q in
+ U.text_of_result (output_string stdout) r nl;
+ if ! log_file <> "" then log q r;
+ incr query_num;
+ flush stdout
+
+let get_interp () =
+ let lexer = function
+ | TP.ID s -> P.ID s
+ | TP.CONURI u -> P.CONURI u
+ | TP.VARURI u -> P.VARURI u
+ | TP.INDTYURI (u, p) -> P.INDTYURI (u, p)
+ | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
+ | TP.LETIN -> P.ALIAS
+ | TP.EOF -> P.EOF
+ | _ -> assert false
+ in
+ let ich = open_in ! interp_file in
+ let lexbuf = Lexing.from_channel ich in
+ let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
+ close_in ich; f
+
+let get_terms interp =
+ let interp = get_interp () in
+ let lexbuf = Lexing.from_channel stdin in
+ let rec aux () =
+ try
+ let dom, mk_term =
+ CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+ in
+ (snd (mk_term interp)) :: aux ()
+ with
+ CicTextualParser0.Eof -> []
+ in
+ aux ()
+
+let pp_type_of uri =
+ let u = UriManager.uri_of_string uri in
+ let s = match (CicEnvironment.get_obj u) with
+ | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
+ | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
+ | _ -> "Current proof or inductive definition."
+(*
+ | Cic.CurrentProof (_,conjs,te,ty) ->
+ | C.InductiveDefinition _ ->
+*)
+ in print_endline s; flush stdout
+
+let rec display = function
+ | [] -> ()
+ | term :: tail ->
+ display tail;
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ flush stdout
+
+let execute ich =
+ let lexbuf = Lexing.from_channel ich in
+ let handle = get_handle () in
+ let rec execute_aux () =
+ try
+ let q = U.query_of_text lexbuf in
+ issue handle q; execute_aux ()
+ with End_of_file -> ()
+ in
+ execute_aux ();
+ C.close handle
+
+let compose () =
+ let handle = get_handle () in
+ let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
+ issue handle (G.compose cl);
+ C.close handle
+
+let locate name =
+ let handle = get_handle () in
+ issue handle (G.locate name);
+ C.close handle
+
+let mpattern n m l =
+ let queries = ref [] in
+ let univ = Some GU.universe_for_search_pattern in
+ let handle = get_handle () in
+ let rec pattern level = function
+ | [] -> ()
+ | term :: tail ->
+ pattern level tail;
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ let t = U.start_time () in
+ let om,rm,sm = C2.get_constraints term in
+ let oml,rml,sml = List.length om, List.length rm, List.length sm in
+ let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
+ let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
+ let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
+ let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in
+ if not (List.mem q ! queries) then
+ begin
+ issue handle q;
+ Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
+ Printf.printf "%i GEN = %i: %s"
+ (pred ! query_num) (oml + rml + sml + ool + rol + sol)
+ (U.stop_time t ^ nl);
+ flush stdout; queries := q :: ! queries
+ end
+ in
+ for level = max m n downto min m n do
+ Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level;
+ flush stderr; pattern level l
+ done;
+ Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
+ (List.length ! queries);
+ flush stderr;
+ C.close handle
+
+let mbackward n m l =
+ let queries = ref [] in
+ let torigth_restriction (u, b) =
+ let p = if b then `MainConclusion None else `InConclusion in (p, u)
+ in
+ let univ = Some GU.universe_for_match_conclusion in
+ let handle = get_handle () in
+ let rec backward level = function
+ | [] -> ()
+ | term :: tail ->
+ backward level tail;
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ let t = U.start_time () in
+ let list_of_must, only = C1.out_restr [] [] term in
+ let max_level = pred (List.length list_of_must) in
+ let must = List.nth list_of_must (min level max_level) in
+ let rigth_must = List.map torigth_restriction must in
+ let rigth_only = Some (List.map torigth_restriction only) in
+ let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in
+ if not (List.mem q ! queries) then
+ begin
+ issue handle q;
+ Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
+ Printf.printf "%i GEN = %i: %s"
+ (pred ! query_num) (List.length must)
+ (U.stop_time t ^ nl);
+ flush stdout; queries := q :: ! queries
+ end
+ in
+ for level = max m n downto min m n do
+ Printf.eprintf "\nmqgtop: backward: trying level %i\n" level;
+ flush stderr; backward level l
+ done;
+ Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
+ (List.length ! queries);
+ flush stderr;
+ C.close handle
+
+let check () =
+ let handle = get_handle () in
+ Printf.eprintf
+ "mqgtop: current options: %s, connection: %s\n"
+ ! int_options (if C.connected handle then "on" else "off");
+ C.close handle
+
+let prerr_help () =
+ prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
+ prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
+ prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output";
+ prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
+ prerr_endline "OPTIONS:\n";
+ prerr_endline "-h -help shows this help message";
+ prerr_endline "-q -show-queries outputs generated queries";
+ prerr_endline "-l -log-file FILE sets the log file";
+ prerr_endline "-o -options STRING sets the interpreter options";
+ prerr_endline "-c -check checks the database connection";
+ prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
+ prerr_endline "-x -execute issues a query given in the input file";
+ prerr_endline "-i -interp FILE sets the CIC short names interpretation file";
+ prerr_endline "-d -disply outputs the CIC terms given in the input file";
+ prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
+ prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
+ prerr_endline " from the input file";
+ prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all";
+ prerr_endline " CIC terms in the input file";
+ prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
+ prerr_endline " on all CIC terms in the input file";
+ prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
+ prerr_endline " CIC terms in the input file";
+ prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0";
+ prerr_endline " on all CIC terms in the input file\n";
+ prerr_endline "NOTES: * current interpreter options are:";
+ prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)";
+ prerr_endline " * CIC terms are read with the HELM CIC Textual Parser";
+ prerr_endline " * -typeof does not work with inductive types and proofs in progress\n"
+
+let rec parse = function
+ | [] -> ()
+ | ("-h"|"-help") :: rem -> prerr_help (); parse rem
+ | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
+ | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
+ | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
+ | ("-x"|"-execute") :: rem -> execute stdin; parse rem
+ | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
+ | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
+ | ("-c"|"-check") :: rem -> check (); parse rem
+ | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
+ | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
+ | ("-C"|"-compose") :: rem -> compose (); parse rem
+ | ("-M"|"-backward") :: arg :: rem ->
+ let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
+ | ("-MB"|"-multi-backward") :: arg :: rem ->
+ let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
+ | ("-P"|"-pattern") :: arg :: rem ->
+ let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
+ | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
+ | _ :: rem -> parse rem
+
+let _ =
+ let t = U.start_time () in
+ Logger.log_callback :=
+ (Logger.log_to_html
+ ~print_and_flush:(fun s -> print_string s; flush stdout)) ;
+ parse (List.tl (Array.to_list Sys.argv));
+ prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
+ exit 0
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+module U = MQueryUtil
+module I = MQueryInterpreter
+module C = MQIConn
+
+let _ =
+ let t = U.start_time () in
+ let ich = Lexing.from_channel stdin in
+ let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in
+ let log s = print_string s; flush stdout in
+ let handle = C.init (C.flags_of_string flags) log in
+ if not (C.connected handle) then begin
+ print_endline "mqitop: no connection"; flush stdout
+ end;
+ let rec aux () =
+ let t = U.start_time () in
+ let r = I.execute handle (U.query_of_text ich) in
+(* U.text_of_result log r "\n";
+*) Printf.printf "mqitop: query: %s,%i\n" (U.stop_time t) (List.length r);
+ flush stdout; aux()
+
+ in
+ begin try aux() with End_of_file -> () end;
+ C.close handle;
+ Printf.printf "mqitop: done: %s\n" (U.stop_time t)
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+let _ =
+ let module U = MQueryUtil in
+ let t = U.start_time () in
+ let ich = Lexing.from_channel stdin in
+ let rec aux () =
+ let t = U.start_time () in
+ U.text_of_query print_string (U.query_of_text ich) "\n";
+ Printf.printf "mqtop: query: %s\n" (U.stop_time t);
+ flush stdout; aux()
+ in
+ begin try aux() with End_of_file -> () end;
+ Printf.printf "mqtop: done: %s\n" (U.stop_time t)
+++ /dev/null
-requires="unix helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mathql_generator"
-version="1.3"
-linkopts=""
MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \
cic_cache cic_proof_checking cic_textual_parser \
tex_cic_textual_parser cic_unification mathql mathql_interpreter \
- mathql_generator mathql_test tactics
+ mathql_generator tactics
OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@
mQueryTLexer.cmx: mQueryTParser.cmx
mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi
mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi
-mQueryMisc.cmo: mQueryMisc.cmi
-mQueryMisc.cmx: mQueryMisc.cmi
-mQueryLevels2.cmi: mQueryGenerator.cmi
+mQGUtil.cmi: mQGTypes.cmo
+mQueryGenerator.cmi: mQGTypes.cmo
+mQueryLevels2.cmi: mQGTypes.cmo
+mQGUtil.cmo: mQGTypes.cmo mQGUtil.cmi
+mQGUtil.cmx: mQGTypes.cmx mQGUtil.cmi
+mQueryGenerator.cmo: mQGTypes.cmo mQGUtil.cmi mQueryGenerator.cmi
+mQueryGenerator.cmx: mQGTypes.cmx mQGUtil.cmx mQueryGenerator.cmi
mQueryLevels.cmo: mQueryLevels.cmi
mQueryLevels.cmx: mQueryLevels.cmi
-mQueryLevels2.cmo: mQueryLevels2.cmi
-mQueryLevels2.cmx: mQueryLevels2.cmi
-mQueryGenerator.cmo: mQueryGenerator.cmi
-mQueryGenerator.cmx: mQueryGenerator.cmi
+mQueryLevels2.cmo: mQGTypes.cmo mQGUtil.cmi mQueryLevels2.cmi
+mQueryLevels2.cmx: mQGTypes.cmx mQGUtil.cmx mQueryLevels2.cmi
PREDICATES =
-INTERFACE_FILES = mQueryLevels.mli mQueryLevels2.mli mQueryGenerator.mli
+INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \
+ mQueryLevels.mli mQueryLevels2.mli
-IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
+IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml)
-EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_INSTALL = mQGTypes.ml mQGTypes.cmi
EXTRA_OBJECTS_TO_CLEAN =
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTORS: Ferruccio Guidi <fguidi@cs.unibo.it>
+ * Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
+ *)
+
+(* low level types *********************************************************)
+
+type uri = string
+type position = MainHypothesis
+ | InHypothesis
+ | MainConclusion
+ | InConclusion
+ | InBody
+type depth = int
+type sort = Set
+ | Prop
+ | Type
+
+type spec = MustObj of uri list * position list * depth list
+ | MustSort of sort list * position list * depth list
+ | MustRel of position list * depth list
+ | OnlyObj of uri list * position list * depth list
+ | OnlySort of sort list * position list * depth list
+ | OnlyRel of position list * depth list
+ | Universe of position list
+
+(* high-level types ********************************************************)
+
+type optional_depth = int option
+
+type full_position = [ `MainHypothesis of optional_depth
+ | `MainConclusion of optional_depth
+ | `InHypothesis
+ | `InConclusion
+ | `InBody
+ ]
+
+type main_position = [ `MainHypothesis of optional_depth
+ | `MainConclusion of optional_depth
+ ]
+
+type r_obj = full_position * uri
+type r_sort = main_position * sort
+type r_rel = main_position
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type only_restrictions =
+ (r_obj list option * r_rel list option * r_sort list option)
+
+type universe = position list
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+module T = MQGTypes
+
+(* low level functions *****************************************************)
+
+let string_of_position p =
+ let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
+ match p with
+ | T.MainHypothesis -> ns ^ "MainHypothesis"
+ | T.InHypothesis -> ns ^ "InHypothesis"
+ | T.MainConclusion -> ns ^ "MainConclusion"
+ | T.InConclusion -> ns ^ "InConclusion"
+ | T.InBody -> ns ^ "InBody"
+
+let string_of_sort = function
+ | T.Set -> "Set"
+ | T.Prop -> "Prop"
+ | T.Type -> "Type"
+
+let string_of_depth = string_of_int
+
+let mathql_of_position = function
+ | T.MainHypothesis -> "$MH"
+ | T.InHypothesis -> "$IH"
+ | T.MainConclusion -> "$MC"
+ | T.InConclusion -> "$IC"
+ | T.InBody -> "$IB"
+
+let mathql_of_sort = function
+ | T.Set -> "$SET"
+ | T.Prop -> "$PROP"
+ | T.Type -> "$TYPE"
+
+let mathql_of_depth = string_of_int
+
+let mathql_of_uri u = u
+
+let mathql_of_specs out l =
+ let rec iter f = function
+ | [] -> ()
+ | [s] -> out "\""; out (f s); out "\""
+ | s :: tail -> out "\""; out (f s); out "\", "; iter f tail
+ in
+ let txt_uri l = out "{"; iter mathql_of_uri l; out "} " in
+ let txt_pos l = out "{"; iter mathql_of_position l; out "} " in
+ let txt_sort l = out "{"; iter mathql_of_sort l; out "} " in
+ let txt_depth l = out "{"; iter mathql_of_depth l; out "} " in
+ let txt_spec = function
+ | T.MustObj (u, p, d) -> out "mustobj "; txt_uri u; txt_pos p; txt_depth d; out "\n"
+ | T.MustSort (s, p, d) -> out "mustsort "; txt_sort s; txt_pos p; txt_depth d; out "\n"
+ | T.MustRel ( p, d) -> out "mustrel "; txt_pos p; txt_depth d; out "\n"
+ | T.OnlyObj (u, p, d) -> out "onlyobj "; txt_uri u; txt_pos p; txt_depth d; out "\n"
+ | T.OnlySort (s, p, d) -> out "onlysort "; txt_sort s; txt_pos p; txt_depth d; out "\n"
+ | T.OnlyRel ( p, d) -> out "onlyrel "; txt_pos p; txt_depth d; out "\n"
+ | T.Universe ( p ) -> out "universe "; txt_pos p; out "\n"
+ in
+ List.iter txt_spec l
+
+let position_of_mathql = function
+ | "$MH" -> T.MainHypothesis
+ | "$IH" -> T.InHypothesis
+ | "$MC" -> T.MainConclusion
+ | "$IC" -> T.InConclusion
+ | "$IB" -> T.InBody
+ | _ -> raise Parsing.Parse_error
+
+let sort_of_mathql = function
+ | "$SET" -> T.Set
+ | "$PROP" -> T.Prop
+ | "$TYPE" -> T.Type
+ | _ -> raise Parsing.Parse_error
+
+let depth_of_mathql s =
+ try
+ let d = int_of_string s in
+ if d < 0 then raise (Failure "") else d
+ with Failure _ -> raise Parsing.Parse_error
+
+let uri_of_mathql s = s
+
+(* high level functions ****************************************************)
+
+let text_of_position = function
+ | `MainHypothesis _ -> "MainHypothesis"
+ | `MainConclusion _ -> "MainConclusion"
+ | `InHypothesis -> "InHypothesis"
+ | `InConclusion -> "InConclusion"
+ | `InBody -> "InBody"
+
+let text_of_depth pos no_depth_text = match pos with
+ | `MainHypothesis (Some d)
+ | `MainConclusion (Some d) -> string_of_int d
+ | _ -> no_depth_text
+
+let text_of_sort = function
+ | T.Set -> "Set"
+ | T.Prop -> "Prop"
+ | T.Type -> "Type"
+
+let is_main_position = function
+ | `MainHypothesis _
+ | `MainConclusion _ -> true
+ | _ -> false
+
+let is_conclusion = function
+ | `MainConclusion _
+ | `InConclusion -> true
+ | _ -> false
+
+let set_full_position pos depth = match pos with
+ | `MainHypothesis _ -> `MainHypothesis depth
+ | `MainConclusion _ -> `MainConclusion depth
+ | _ -> pos
+
+let set_main_position pos depth = match pos with
+ | `MainHypothesis _ -> `MainHypothesis depth
+ | `MainConclusion _ -> `MainConclusion depth
+
+let universe_for_search_pattern =
+ [T.MainHypothesis; T.InHypothesis; T.MainConclusion; T.InConclusion]
+
+let universe_for_match_conclusion = [T.MainConclusion; T.InConclusion]
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
+ *)
+
+(* low level functions *****************************************************)
+
+(* these functions give the string representation used in the db ----------*)
+
+val string_of_position : MQGTypes.position -> string
+val string_of_depth : MQGTypes.depth -> string
+val string_of_sort : MQGTypes.sort -> string
+
+(* these functions give the string representation used in MathQL ----------*)
+
+val mathql_of_position : MQGTypes.position -> string
+val mathql_of_depth : MQGTypes.depth -> string
+val mathql_of_uri : MQGTypes.uri -> string
+val mathql_of_sort : MQGTypes.sort -> string
+
+val mathql_of_specs : (string -> unit) -> MQGTypes.spec list -> unit
+
+val position_of_mathql : string -> MQGTypes.position
+val depth_of_mathql : string -> MQGTypes.depth
+val uri_of_mathql : string -> MQGTypes.uri
+val sort_of_mathql : string -> MQGTypes.sort
+
+(* high level functions ****************************************************)
+
+(* these functions give the textual representation used by umans ----------*)
+
+val text_of_position : MQGTypes.full_position -> string
+val text_of_depth : MQGTypes.full_position -> string -> string
+val text_of_sort : MQGTypes.sort -> string
+
+(* these functions classify the positions ---------------------------------*)
+
+val is_main_position : MQGTypes.full_position -> bool
+val is_conclusion : MQGTypes.full_position -> bool
+
+(* these function apply changes to positions ------------------------------*)
+
+val set_full_position : MQGTypes.full_position -> MQGTypes.optional_depth ->
+ MQGTypes.full_position
+val set_main_position : MQGTypes.main_position -> MQGTypes.optional_depth ->
+ MQGTypes.main_position
+
+(* these functions give some universes for "query_of_constraints" ---------*)
+
+val universe_for_search_pattern : MQGTypes.universe
+val universe_for_match_conclusion : MQGTypes.universe
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-type uri = string
-type position = string
-type depth = string
-type sort = string
-
-type spec = MustObj of uri list * position list * depth list
- | MustSort of sort list * position list * depth list
- | MustRel of position list * depth list
- | OnlyObj of uri list * position list * depth list
- | OnlySort of sort list * position list * depth list
- | OnlyRel of position list * depth list
- | Universe of position list
-
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
-
-let text_of_builtin s =
- let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
- if s = ns ^ "MainHypothesis" then "$MH" else
- if s = ns ^ "InHypothesis" then "$IH" else
- if s = ns ^ "MainConclusion" then "$MC" else
- if s = ns ^ "InConclusion" then "$IC" else
- if s = ns ^ "InBody" then "$IB" else
- if s = "Set" then "$SET" else
- if s = "Prop" then "$PROP" else
- if s = "Type" then "$TYPE" else s
-
-let text_of_spec out l =
- let rec iter = function
- | [] -> ()
- | [s] -> out "\""; out (text_of_builtin s); out "\""
- | s :: tail -> out "\""; out (text_of_builtin s); out "\", "; iter tail
- in
- let txt_list l = out "{"; iter l; out "} " in
- let txt_spec = function
- | MustObj (u, p, d) -> out "mustobj "; txt_list u; txt_list p; txt_list d; out "\n"
- | MustSort (s, p, d) -> out "mustsort "; txt_list s; txt_list p; txt_list d; out "\n"
- | MustRel ( p, d) -> out "mustrel "; txt_list p; txt_list d; out "\n"
- | OnlyObj (u, p, d) -> out "onlyobj "; txt_list u; txt_list p; txt_list d; out "\n"
- | OnlySort (s, p, d) -> out "onlysort "; txt_list s; txt_list p; txt_list d; out "\n"
- | OnlyRel ( p, d) -> out "onlyrel "; txt_list p; txt_list d; out "\n"
- | Universe ( p ) -> out "universe "; txt_list p; out "\n"
- in
- List.iter txt_spec l
-
module M = MathQL
+module T = MQGTypes
+module U = MQGUtil
+
+(* low level functions *****************************************************)
let locate s =
let query =
| l -> [(false, [p], set_val l)]
in
only := o;
- con "h:occurrence" r @ con "h:sort" s @
- con "h:position" p @ con "h:depth" d
+ con "h:occurrence" r @
+ con "h:sort" (List.map U.string_of_sort s) @
+ con "h:position" (List.map U.string_of_position p) @
+ con "h:depth" (List.map U.string_of_depth d)
in
let property_must n c =
M.Property true M.RefineExact [n] []
in
let rec aux = function
| [] -> ()
- | Universe l :: tail ->
- only := true; univ := [(false, ["h:position"], set_val l)]; aux tail
- | MustObj r p d :: tail ->
+ | T.Universe l :: tail ->
+ only := true;
+ let l = List.map U.string_of_position l in
+ univ := [(false, ["h:position"], set_val l)]; aux tail
+ | T.MustObj r p d :: tail ->
must := property_must "refObj" (r, [], p, d) :: ! must; aux tail
- | MustSort s p d :: tail ->
+ | T.MustSort s p d :: tail ->
must := property_must "refSort" ([], s, p, d) :: ! must; aux tail
- | MustRel p d :: tail ->
+ | T.MustRel p d :: tail ->
must := property_must "refRel" ([], [], p, d) :: ! must; aux tail
- | OnlyObj r p d :: tail ->
+ | T.OnlyObj r p d :: tail ->
onlyobj := (r, [], p, d) :: ! onlyobj; aux tail
- | OnlySort s p d :: tail ->
+ | T.OnlySort s p d :: tail ->
onlysort := ([], s, p, d) :: ! onlysort; aux tail
- | OnlyRel p d :: tail ->
+ | T.OnlyRel p d :: tail ->
onlyrel := ([], [], p, d) :: ! onlyrel; aux tail
in
let rec iter f g = function
| [head] -> (f head)
| head :: tail -> let t = (iter f g tail) in g (f head) t
in
- text_of_spec prerr_string cl;
+ U.mathql_of_specs prerr_string cl;
aux cl;
let must_query =
if ! must = [] then
in
M.StatQuery (letin_query (select_query must_query))
-let builtin s =
- let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
- match s with
- | MainHypothesis -> ns ^ "MainHypothesis"
- | InHypothesis -> ns ^ "InHypothesis"
- | MainConclusion -> ns ^ "MainConclusion"
- | InConclusion -> ns ^ "InConclusion"
- | InBody -> ns ^ "InBody"
- | Set -> "Set"
- | Prop -> "Prop"
- | Type -> "Type"
-
-(* conversion functions from the old constraints ***************************)
-
-type old_depth = int option
-
-type r_obj = uri * position * old_depth
-type r_rel = position * old_depth
-type r_sort = position * old_depth * sort
-
-type universe = position list option
-
-type must_restrictions = r_obj list * r_rel list * r_sort list
-type only_restrictions =
- r_obj list option * r_rel list option * r_sort list option
+(* high-level functions ****************************************************)
let query_of_constraints u (musts_obj, musts_rel, musts_sort)
(onlys_obj, onlys_rel, onlys_sort) =
let conv = function
- | None -> []
- | Some i -> [string_of_int i]
+ | `MainHypothesis None -> [T.MainHypothesis], []
+ | `MainHypothesis (Some d) -> [T.MainHypothesis], [d]
+ | `MainConclusion None -> [T.MainConclusion], []
+ | `MainConclusion (Some d) -> [T.MainConclusion], [d]
+ | `InHypothesis -> [T.InHypothesis], []
+ | `InConclusion -> [T.InConclusion], []
+ | `InBody -> [T.InBody], []
in
- let must_obj (r, p, d) = MustObj ([r], [p], conv d) in
- let must_sort (p, d, s) = MustSort ([s], [p], conv d) in
- let must_rel (p, d) = MustRel ([p], conv d) in
- let only_obj (r, p, d) = OnlyObj ([r], [p], conv d) in
- let only_sort (p, d, s) = OnlySort ([s], [p], conv d) in
- let only_rel (p, d) = OnlyRel ([p], conv d) in
+ let must_obj (p, u) = let p, d = conv p in T.MustObj ([u], p, d) in
+ let must_sort (p, s) = let p, d = conv p in T.MustSort ([s], p, d) in
+ let must_rel p = let p, d = conv p in T.MustRel (p, d) in
+ let only_obj (p, u) = let p, d = conv p in T.OnlyObj ([u], p, d) in
+ let only_sort (p, s) = let p, d = conv p in T.OnlySort ([s], p, d) in
+ let only_rel p = let p, d = conv p in T.OnlyRel (p, d) in
let must = List.map must_obj musts_obj @
List.map must_rel musts_rel @
List.map must_sort musts_sort
let only =
(match onlys_obj with
| None -> []
- | Some [] -> [OnlyObj ([], [], [])]
+ | Some [] -> [T.OnlyObj ([], [], [])]
| Some l -> List.map only_obj l
) @
(match onlys_rel with
| None -> []
- | Some [] -> [OnlyRel ([], [])]
+ | Some [] -> [T.OnlyRel ([], [])]
| Some l -> List.map only_rel l
) @
(match onlys_sort with
| None -> []
- | Some [] -> [OnlySort ([], [], [])]
+ | Some [] -> [T.OnlySort ([], [], [])]
| Some l -> List.map only_sort l
)
in
- let univ = match u with None -> [] | Some l -> [Universe l] in
+ let univ = match u with None -> [] | Some l -> [T.Universe l] in
compose (must @ only @ univ)
+
(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
*)
-type uri = string
-type position = string
-type depth = string
-type sort = string
-
-type spec = MustObj of uri list * position list * depth list
- | MustSort of sort list * position list * depth list
- | MustRel of position list * depth list
- | OnlyObj of uri list * position list * depth list
- | OnlySort of sort list * position list * depth list
- | OnlyRel of position list * depth list
- | Universe of position list
-
-type builtin_t = MainHypothesis
- | InHypothesis
- | MainConclusion
- | InConclusion
- | InBody
- | Set
- | Prop
- | Type
+(* interface for the low-level constraints *********************************)
val locate : string -> MathQL.query
-val compose : spec list -> MathQL.query
-
-val builtin : builtin_t -> string
-
-(* interface for the old constraints ***************************************)
-
-type old_depth = int option
-
-type r_obj = uri * position * old_depth
-type r_rel = position * old_depth
-type r_sort = position * old_depth * sort
+val compose : MQGTypes.spec list -> MathQL.query
-type must_restrictions = (r_obj list * r_rel list * r_sort list)
-type only_restrictions =
- (r_obj list option * r_rel list option * r_sort list option)
-type universe = position list option
+(* interface for the high-level constraints ********************************)
-val query_of_constraints : universe -> must_restrictions -> only_restrictions -> MathQL.query
+val query_of_constraints : MQGTypes.universe option ->
+ MQGTypes.must_restrictions ->
+ MQGTypes.only_restrictions ->
+ MathQL.query
(* *)
(******************************************************************************)
+module T = MQGTypes
+module U = MQGUtil
+
type classification =
Backbone of int
| Branch of int
let (!!) =
function
- Backbone n ->
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
- | Branch n ->
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
- | InConclusion ->
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
- | InHypothesis ->
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
+ Backbone n -> `MainConclusion (Some n)
+ | Branch n -> `MainHypothesis (Some n)
+ | _ -> assert false
+;;
+
+let (!!!) =
+ function
+ Backbone n -> `MainConclusion (Some n)
+ | Branch n -> `MainHypothesis (Some n)
+ | InConclusion -> `InConclusion
+ | InHypothesis -> `InHypothesis
;;
+
let (@@) (l1,l2,l3) (l1',l2',l3') =
let merge l1 l2 =
List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
let rec process_type_aux kind =
function
C.Var (uri,expl_named_subst) ->
- let kind',depth = !!kind in
- ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
- (process_type_aux_expl_named_subst kind expl_named_subst)
+ ([!!!kind, UriManager.string_of_uri uri],[],[]) @@
+ (process_type_aux_expl_named_subst kind expl_named_subst)
| C.Rel _ ->
- let kind',depth = !!kind in
- (match depth with
- None -> [],[],[]
- | Some d -> [],[kind',Some d],[])
+ (match kind with
+ | InConclusion
+ | InHypothesis -> [],[],[]
+ | _ -> [],[!!kind],[])
| C.Sort s ->
(match kind with
Backbone _
| Branch _ ->
let s' =
match s with
- Cic.Prop -> "Prop"
- | Cic.Set -> "Set"
- | Cic.Type -> "Type"
+ Cic.Prop -> T.Prop
+ | Cic.Set -> T.Set
+ | Cic.Type -> T.Type
in
- let kind',depth = !!kind in
- (match depth with
- None -> assert false
- | Some d -> [],[],[kind',Some d,s'])
+ [],[],[!!kind,s']
| _ -> [],[],[])
| C.Meta _
| C.Implicit -> assert false
List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
| C.Appl _ -> assert false
| C.Const (uri,_) ->
- let kind',depth = !!kind in
- [UriManager.string_of_uri uri,kind',depth],[],[]
+ [!!!kind, UriManager.string_of_uri uri],[],[]
| C.MutInd (uri,typeno,expl_named_subst) ->
- let kind',depth = !!kind in
- ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
- ")", kind', depth],[],[]) @@
+ ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (typeno + 1) ^ ")"],[],[]) @@
(process_type_aux_expl_named_subst kind expl_named_subst)
| C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
- let kind',depth = !!kind in
- ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
- "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
- (process_type_aux_expl_named_subst kind expl_named_subst)
+ ([!!!kind, U.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")"],[],[])
+ @@ (process_type_aux_expl_named_subst kind expl_named_subst)
| C.MutCase (_,_,_,term,patterns) ->
(* outtype ignored *)
let kind' = soften_classification kind in
let get_constraints term =
let res = get_constraints term in
let (objs,rels,sorts) = res in
+ let text_of_pos p =
+ U.text_of_position p ^ " " ^ U.text_of_depth p "NULL"
+ in
prerr_endline "Constraints on objs:" ;
List.iter
- (function (s1,s2,n) ->
- prerr_endline
- (s1 ^ " " ^ s2 ^ " " ^
- match n with None -> "NULL" | Some n -> string_of_int n)
- ) objs ;
+ (function (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ;
prerr_endline "Constraints on Rels:" ;
- List.iter
- (function (s,n) ->
- prerr_endline
- (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
- ) rels ;
+ List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ;
prerr_endline "Constraints on Sorts:" ;
List.iter
- (function (s1,n,s2) ->
- prerr_endline
- (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
- " " ^ s2)
+ (function (p, s) -> prerr_endline (text_of_pos (p:>T.full_position) ^ " " ^ U.text_of_sort s)
) sorts ;
res
;;
(* *)
(******************************************************************************)
-val get_constraints: Cic.term -> MQueryGenerator.must_restrictions
+val get_constraints: Cic.term -> MQGTypes.must_restrictions
+++ /dev/null
-*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples*
-mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
+++ /dev/null
-mqgtop.cmo: mQGTopLexer.cmo mQGTopParser.cmi
-mqgtop.cmx: mQGTopLexer.cmx mQGTopParser.cmx
-mQGTopParser.cmo: mQGTopParser.cmi
-mQGTopParser.cmx: mQGTopParser.cmi
-mQGTopLexer.cmo: mQGTopParser.cmi
-mQGTopLexer.cmx: mQGTopParser.cmx
+++ /dev/null
-BIN_DIR = /usr/local/bin
-REQUIRES = unix helm-cic_textual_parser \
- helm-mathql helm-mathql_interpreter helm-mathql_generator
-PREDICATES =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
-OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
-OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS)
-OCAMLDEP = ocamldep
-OCAMLYACC = ocamlyacc
-OCAMLLEX = ocamllex
-
-LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-
-MQTOP = mqtop.ml
-MQITOP = mqitop.ml
-MQGTOP = mqgtop.ml
-
-DEPOBJS = $(MQTOP) $(MQITOP) $(MQGTOP)
-AUXOBJS = mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
-
-all: $(DEPOBJS:.ml=)
-opt: $(DEPOBJS:.ml=.opt)
-
-depend: $(AUXOBJS)
- $(OCAMLDEP) $(DEPOBJS) $(AUXOBJS) > .depend
-
-mqtop: $(MQTOP:.ml=.cmo) $(LIBRARIES)
- $(OCAMLC) -linkpkg -o mqtop $(MQTOP:.ml=.cmo)
-
-mqtop.opt: $(MQTOP:.ml=.cmx) $(LIBRARIES_OPT)
- $(OCAMLOPT) -linkpkg -o mqtop.opt $(MQTOP:.ml=.cmx)
-
-mqitop: $(MQITOP:.ml=.cmo) $(LIBRARIES)
- $(OCAMLC) -linkpkg -o mqitop $(MQITOP:.ml=.cmo)
-
-mqitop.opt: $(MQITOP:.ml=.cmx) $(LIBRARIES_OPT)
- $(OCAMLOPT) -linkpkg -o mqitop.opt $(MQITOP:.ml=.cmx)
-
-mqgtop: mQGTopParser.cmi $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo) $(LIBRARIES)
- $(OCAMLC) -linkpkg -o mqgtop $(AUXOBJS:.ml=.cmo) $(MQGTOP:.ml=.cmo)
-
-mqgtop.opt: $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx) $(LIBRARIES_OPT)
- $(OCAMLOPT) -linkpkg -o mqgtop.opt $(AUXOBJS:.ml=.cmx) $(MQGTOP:.ml=.cmx)
-
-.SUFFIXES: .ml .mli .cmo .cmi .cmx .mly .mll
-.ml.cmo: $(LIBRARIES)
- $(OCAMLC) -c $<
-.mli.cmi: $(LIBRARIES)
- $(OCAMLC) -c $<
-.ml.cmx: $(LIBRARIES_OPT)
- $(OCAMLOPT) -c $<
-.mly.ml:
- $(OCAMLYACC) $<
-.mly.mli:
- $(OCAMLYACC) $<
-.mll.ml:
- $(OCAMLLEX) $<
-
-$(DEPOBJS:%.ml=%.cmo): $(LIBRARIES)
-$(DEPOBJS:%.ml=%.cmx): $(LIBRARIES_OPT)
-
-clean:
- rm -f *.cm[iox] *.o $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) \
- mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml
-
-install:
- cp $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt) $(BIN_DIR)
-
-uninstall:
- cd $(BIN_DIR)
- rm -f $(DEPOBJS:.ml=) $(DEPOBJS:.ml=.opt)
-
-.PHONY: install uninstall clean
-
-ifneq ($(MAKECMDGOALS), depend)
- include .depend
-endif
-
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-{
- open MQGTopParser
-
- let debug = false
-
- let out s = if debug then prerr_endline s
-}
-
-let SPC = [' ' '\t' '\n']+
-let ALPHA = ['A'-'Z' 'a'-'z' '_']
-let NUM = ['0'-'9']
-let IDEN = ALPHA (NUM | ALPHA)*
-let QSTR = [^ '"' '\\']+
-
-rule comm_token = parse
- | "(*" { comm_token lexbuf; comm_token lexbuf }
- | "*)" { () }
- | ['*' '('] { comm_token lexbuf }
- | [^ '*' '(']* { comm_token lexbuf }
-and string_token = parse
- | '"' { DQ }
- | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) }
- | QSTR { STR (Lexing.lexeme lexbuf) }
- | eof { EOF }
-and spec_token = parse
- | "(*" { comm_token lexbuf; spec_token lexbuf }
- | SPC { spec_token lexbuf }
- | '"' { let str = qstr string_token lexbuf in
- out ("STR " ^ str); STR str }
- | '{' { out "LC"; LC }
- | '}' { out "RC"; RC }
- | ',' { out "CM"; CM }
- | '$' { out "DL"; DL }
- | "mustobj" { out "MOBJ" ; MOBJ }
- | "mustsort" { out "MSORT" ; MSORT }
- | "mustrel" { out "MREL" ; MREL }
- | "onlyobj" { out "OOBJ" ; OOBJ }
- | "onlysort" { out "OSORT" ; OSORT }
- | "onlyrel" { out "OREL" ; OREL }
- | "universe" { out "UNIV" ; UNIV }
- | IDEN { let id = Lexing.lexeme lexbuf in
- out ("ID " ^ id); ID id }
- | eof { EOF }
+++ /dev/null
-/* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- */
-
-/* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- */
-
-%{
- let f (x, y, z) = x
- let s (x, y, z) = y
- let t (x, y, z) = z
-
- let builtin s =
- let ns = "http://www.cs.unibo.it/helm/schemas/schema-helm#" in
- match s with
- | "MH" -> ns ^ "MainHypothesis"
- | "IH" -> ns ^ "InHypothesis"
- | "MC" -> ns ^ "MainConclusion"
- | "IC" -> ns ^ "InConclusion"
- | "IB" -> ns ^ "InBody"
- | "SET" -> "Set"
- | "PROP" -> "Prop"
- | "TYPE" -> "Type"
- | _ -> raise Parsing.Parse_error
-
- module G = MQueryGenerator
-%}
- %token <string> ID
- %token <UriManager.uri> CONURI
- %token <UriManager.uri> VARURI
- %token <UriManager.uri * int> INDTYURI
- %token <UriManager.uri * int * int> INDCONURI
- %token ALIAS EOF
-
- %start interp
- %type <CicTextualParser0.interpretation_domain_item -> CicTextualParser0.interpretation_codomain_item option> interp
-
- %token <string> STR
- %token DL DQ LC RC CM
- %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV
-
- %start qstr specs
- %type <string> qstr
- %type <MQueryGenerator.spec list> specs
-%%
- uri:
- | CONURI { CicTextualParser0.ConUri $1 }
- | VARURI { CicTextualParser0.VarUri $1 }
- | INDTYURI { CicTextualParser0.IndTyUri ((fst $1), (snd $1)) }
- | INDCONURI { CicTextualParser0.IndConUri ((f $1), (s $1), (t $1)) }
- ;
- alias:
- | ALIAS ID uri { ($2, CicTextualParser0.Uri $3) }
- ;
- aliases:
- | alias aliases { $1 :: $2 }
- | EOF { [] }
- ;
- interp:
- | aliases { function CicTextualParser0.Id s -> (try Some (List.assoc s $1)
- with Not_found -> None)
- | _ -> None }
- ;
-
- qstr:
- | DQ { "" }
- | STR qstr { $1 ^ $2 }
- ;
- str:
- | STR { $1 }
- | DL ID { builtin $2 }
- ;
- strs:
- | str CM strs { $1 :: $3 }
- | str { [$1] }
- | { [] }
- ;
- list:
- | LC strs RC { $2 }
- ;
- spec:
- | MOBJ list list list { G.MustObj ($2, $3, $4) }
- | MSORT list list list { G.MustSort ($2, $3, $4) }
- | MREL list list { G.MustRel ($2, $3) }
- | OOBJ list list list { G.OnlyObj ($2, $3, $4) }
- | OSORT list list list { G.OnlySort ($2, $3, $4) }
- | OREL list list { G.OnlyRel ($2, $3) }
- | UNIV list { G.Universe $2 }
- ;
- specs:
- | spec specs { $1 :: $2 }
- | EOF { [] }
- ;
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-let query_num = ref 1
-
-let interp_file = ref "interp.cic"
-
-let log_file = ref ""
-
-let show_queries = ref false
-
-let int_options = ref ""
-
-let nl = " <p>\n"
-
-module U = MQueryUtil
-module I = MQueryInterpreter
-module C = MQIConn
-module G = MQueryGenerator
-module L = MQGTopLexer
-module P = MQGTopParser
-module TL = CicTextualLexer
-module TP = CicTextualParser
-module C2 = MQueryLevels2
-module C1 = MQueryLevels
-
-let get_handle () =
- C.init (C.flags_of_string ! int_options)
- (fun s -> print_string s; flush stdout)
-
-let issue handle q =
- let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
- let perm = 64 * 6 + 8 * 6 + 4 in
- let time () =
- let lt = Unix.localtime (Unix.time ()) in
- "NEW LOG: " ^
- string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
- string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
- string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
- string_of_int (lt.Unix.tm_hour) ^ ":" ^
- string_of_int (lt.Unix.tm_min) ^ ":" ^
- string_of_int (lt.Unix.tm_sec)
- in
- let log q r =
- let och = open_out_gen mode perm ! log_file in
- let out = output_string och in
- if ! query_num = 1 then out (time () ^ nl);
- out ("Query: " ^ string_of_int ! query_num ^ nl);
- U.text_of_query out q nl;
- out ("Result: " ^ nl);
- U.text_of_result out r nl;
- close_out och
- in
- if ! show_queries then U.text_of_query (output_string stdout) q nl;
- let r = I.execute handle q in
- U.text_of_result (output_string stdout) r nl;
- if ! log_file <> "" then log q r;
- incr query_num;
- flush stdout
-
-let get_interp () =
- let lexer = function
- | TP.ID s -> P.ID s
- | TP.CONURI u -> P.CONURI u
- | TP.VARURI u -> P.VARURI u
- | TP.INDTYURI (u, p) -> P.INDTYURI (u, p)
- | TP.INDCONURI (u, p, s) -> P.INDCONURI (u, p, s)
- | TP.LETIN -> P.ALIAS
- | TP.EOF -> P.EOF
- | _ -> assert false
- in
- let ich = open_in ! interp_file in
- let lexbuf = Lexing.from_channel ich in
- let f = P.interp (fun x -> lexer (TL.token x)) lexbuf in
- close_in ich; f
-
-let get_terms interp =
- let interp = get_interp () in
- let lexbuf = Lexing.from_channel stdin in
- let rec aux () =
- try
- let dom, mk_term =
- CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
- in
- (snd (mk_term interp)) :: aux ()
- with
- CicTextualParser0.Eof -> []
- in
- aux ()
-
-let pp_type_of uri =
- let u = UriManager.uri_of_string uri in
- let s = match (CicEnvironment.get_obj u) with
- | Cic.Constant (_, _, ty, _) -> CicPp.ppterm ty
- | Cic.Variable (_, _, ty, _) -> CicPp.ppterm ty
- | _ -> "Current proof or inductive definition."
-(*
- | Cic.CurrentProof (_,conjs,te,ty) ->
- | C.InductiveDefinition _ ->
-*)
- in print_endline s; flush stdout
-
-let rec display = function
- | [] -> ()
- | term :: tail ->
- display tail;
- print_string ("? " ^ CicPp.ppterm term ^ nl);
- flush stdout
-
-let execute ich =
- let lexbuf = Lexing.from_channel ich in
- let handle = get_handle () in
- let rec execute_aux () =
- try
- let q = U.query_of_text lexbuf in
- issue handle q; execute_aux ()
- with End_of_file -> ()
- in
- execute_aux ();
- C.close handle
-
-let compose () =
- let handle = get_handle () in
- let cl = P.specs L.spec_token (Lexing.from_channel stdin) in
- issue handle (G.compose cl);
- C.close handle
-
-let locate name =
- let handle = get_handle () in
- issue handle (G.locate name);
- C.close handle
-
-let mpattern n m l =
- let queries = ref [] in
- let univ = Some [G.builtin G.MainHypothesis; G.builtin G.InHypothesis;
- G.builtin G.MainConclusion; G.builtin G.InConclusion] in
- let handle = get_handle () in
- let rec pattern level = function
- | [] -> ()
- | term :: tail ->
- pattern level tail;
- print_string ("? " ^ CicPp.ppterm term ^ nl);
- let t = U.start_time () in
- let om,rm,sm = C2.get_constraints term in
- let oml,rml,sml = List.length om, List.length rm, List.length sm in
- let oo, ool = if level land 1 = 0 then None, 0 else Some om, oml in
- let ro, rol = if level land 2 = 0 then None, 0 else Some rm, rml in
- let so, sol = if level land 4 = 0 then None, 0 else Some sm, sml in
- let q = G.query_of_constraints univ (om,rm,sm) (oo,ro,so) in
- if not (List.mem q ! queries) then
- begin
- issue handle q;
- Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
- Printf.printf "%i GEN = %i: %s"
- (pred ! query_num) (oml + rml + sml + ool + rol + sol)
- (U.stop_time t ^ nl);
- flush stdout; queries := q :: ! queries
- end
- in
- for level = max m n downto min m n do
- Printf.eprintf "\nmqgtop: pattern: trying level %i\n" level;
- flush stderr; pattern level l
- done;
- Printf.eprintf "\nmqgtop: pattern: %i queries issued\n"
- (List.length ! queries);
- flush stderr;
- C.close handle
-
-let mbackward n m l =
- let queries = ref [] in
- let torigth_restriction (u, b) =
- let p = if b then G.builtin G.MainConclusion
- else G.builtin G.InConclusion in
- (u, p, None)
- in
- let univ = Some [G.builtin G.MainConclusion; G.builtin G.InConclusion] in
- let handle = get_handle () in
- let rec backward level = function
- | [] -> ()
- | term :: tail ->
- backward level tail;
- print_string ("? " ^ CicPp.ppterm term ^ nl);
- let t = U.start_time () in
- let list_of_must, only = C1.out_restr [] [] term in
- let max_level = pred (List.length list_of_must) in
- let must = List.nth list_of_must (min level max_level) in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) in
- let q = G.query_of_constraints univ (rigth_must, [], []) (rigth_only , None, None) in
- if not (List.mem q ! queries) then
- begin
- issue handle q;
- Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
- Printf.printf "%i GEN = %i: %s"
- (pred ! query_num) (List.length must)
- (U.stop_time t ^ nl);
- flush stdout; queries := q :: ! queries
- end
- in
- for level = max m n downto min m n do
- Printf.eprintf "\nmqgtop: backward: trying level %i\n" level;
- flush stderr; backward level l
- done;
- Printf.eprintf "\nmqgtop: backward: %i queries issued\n"
- (List.length ! queries);
- flush stderr;
- C.close handle
-
-let check () =
- let handle = get_handle () in
- Printf.eprintf
- "mqgtop: current options: %s, connection: %s\n"
- ! int_options (if C.connected handle then "on" else "off");
- C.close handle
-
-let prerr_help () =
- prerr_endline "\nUSAGE: mqgtop.opt OPTIONS < INPUTFILE\n";
- prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for";
- prerr_endline "testing purposes. mqgtop reads its input from stdin and produces ith output";
- prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
- prerr_endline "OPTIONS:\n";
- prerr_endline "-h -help shows this help message";
- prerr_endline "-q -show-queries outputs generated queries";
- prerr_endline "-l -log-file FILE sets the log file";
- prerr_endline "-o -options STRING sets the interpreter options";
- prerr_endline "-c -check checks the database connection";
- prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
- prerr_endline "-x -execute issues a query given in the input file";
- prerr_endline "-i -interp FILE sets the CIC short names interpretation file";
- prerr_endline "-d -disply outputs the CIC terms given in the input file";
- prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
- prerr_endline "-C -compose issues the \"Compose\" query reading its specifications";
- prerr_endline " from the input file";
- prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all";
- prerr_endline " CIC terms in the input file";
- prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0";
- prerr_endline " on all CIC terms in the input file";
- prerr_endline "-P -pattern LEVEL issues the \"Pattern\" query for the given level on all";
- prerr_endline " CIC terms in the input file";
- prerr_endline "-MP -multi-pattern issues the \"Pattern\" query for each level from 7 to 0";
- prerr_endline " on all CIC terms in the input file\n";
- prerr_endline "NOTES: * current interpreter options are:";
- prerr_endline " P (postgres), G (Galax), S (show statistics), Q (quiet)";
- prerr_endline " * CIC terms are read with the HELM CIC Textual Parser";
- prerr_endline " * -typeof does not work with inductive types and proofs in progress\n"
-
-let rec parse = function
- | [] -> ()
- | ("-h"|"-help") :: rem -> prerr_help (); parse rem
- | ("-i"|"-interp") :: arg :: rem -> interp_file := arg; parse rem
- | ("-d"|"-display") :: rem -> display (get_terms ()); parse rem
- | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
- | ("-x"|"-execute") :: rem -> execute stdin; parse rem
- | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
- | ("-o"|"-options") :: arg :: rem -> int_options := arg; parse rem
- | ("-c"|"-check") :: rem -> check (); parse rem
- | ("-l"|"-log-file") :: arg :: rem -> log_file := arg; parse rem
- | ("-L"|"-Locate") :: arg :: rem -> locate arg; parse rem
- | ("-C"|"-compose") :: rem -> compose (); parse rem
- | ("-M"|"-backward") :: arg :: rem ->
- let m = (int_of_string arg) in mbackward m m (get_terms ()); parse rem
- | ("-MB"|"-multi-backward") :: arg :: rem ->
- let m = (int_of_string arg) in mbackward m 0 (get_terms ()); parse rem
- | ("-P"|"-pattern") :: arg :: rem ->
- let m = (int_of_string arg) in mpattern m m (get_terms ()); parse rem
- | ("-MP"|"-multi-pattern") :: rem -> mpattern 7 0 (get_terms ()); parse rem
- | _ :: rem -> parse rem
-
-let _ =
- let t = U.start_time () in
- Logger.log_callback :=
- (Logger.log_to_html
- ~print_and_flush:(fun s -> print_string s; flush stdout)) ;
- parse (List.tl (Array.to_list Sys.argv));
- prerr_endline ("mqgtop: done in " ^ (U.stop_time t));
- exit 0
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-module U = MQueryUtil
-module I = MQueryInterpreter
-module C = MQIConn
-
-let _ =
- let t = U.start_time () in
- let ich = Lexing.from_channel stdin in
- let flags = if Array.length Sys.argv >= 2 then Sys.argv.(1) else "" in
- let log s = print_string s; flush stdout in
- let handle = C.init (C.flags_of_string flags) log in
- if not (C.connected handle) then begin
- print_endline "mqitop: no connection"; flush stdout
- end;
- let rec aux () =
- let t = U.start_time () in
- let r = I.execute handle (U.query_of_text ich) in
-(* U.text_of_result log r "\n";
-*) Printf.printf "mqitop: query: %s,%i\n" (U.stop_time t) (List.length r);
- flush stdout; aux()
-
- in
- begin try aux() with End_of_file -> () end;
- C.close handle;
- Printf.printf "mqitop: done: %s\n" (U.stop_time t)
+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(* AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
- *)
-
-let _ =
- let module U = MQueryUtil in
- let t = U.start_time () in
- let ich = Lexing.from_channel stdin in
- let rec aux () =
- let t = U.start_time () in
- U.text_of_query print_string (U.query_of_text ich) "\n";
- Printf.printf "mqtop: query: %s\n" (U.stop_time t);
- flush stdout; aux()
- in
- begin try aux() with End_of_file -> () end;
- Printf.printf "mqtop: done: %s\n" (U.stop_time t)
(* *)
(******************************************************************************)
+module I = MQueryInterpreter
+module U = MQGUtil
+module G = MQueryGenerator
+
(* search arguments on which Apply tactic doesn't fail *)
-let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
+let matchConclusion mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~status =
let ((_, metasenv, _, _), metano) = status in
let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
let must = choose_must list_of_must only in
let torigth_restriction (u,b) =
- let p =
- if b then
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- else
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
- in
- (u,p,None)
+ (if b then `MainConclusion None else `InConclusion), u
in
let rigth_must = List.map torigth_restriction must in
let rigth_only = Some (List.map torigth_restriction only) in
let result =
- MQueryInterpreter.execute mqi_handle
- (MQueryGenerator.query_of_constraints
- (Some
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"])
+ I.execute mqi_handle
+ (G.query_of_constraints
+ (Some U.universe_for_match_conclusion)
(rigth_must,[],[]) (rigth_only,None,None)) in
let uris =
List.map
* http://cs.unibo.it/helm/.
*)
-val searchPattern : MQIConn.handle ->
+val matchConclusion : MQIConn.handle ->
?output_html:(string -> unit) ->
(* boolean value: true = in main position *)
- choose_must:((MQueryGenerator.uri * bool) list list ->
- (MQueryGenerator.uri * bool) list ->
- (MQueryGenerator.uri * bool) list) ->
+ choose_must:((MQGTypes.uri * bool) list list ->
+ (MQGTypes.uri * bool) list ->
+ (MQGTypes.uri * bool) list) ->
unit -> status: ProofEngineTypes.status -> string list
* http://cs.unibo.it/helm/.
*)
+module T = MQGTypes
+module U = MQGUtil
+module G = MQueryGenerator
+module C = MQIConn
+
open Http_types ;;
let debug = true;;
failwith ("Can't parse an int option from string: " ^ s)
;;
-let is_concl_pos pos =
- pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- or
- pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
-;;
-
-let is_main_pos pos =
- pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- or
- pos = "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis"
-;;
-
(* HTML pretty printers for mquery_generator types *)
-let html_of_r_obj (uri, pos, depth) =
+let html_of_r_obj (pos, uri) =
sprintf
"<tr><td><input type='checkbox' name='constr_obj' checked='on'/></td><td>%s</td><td>%s</td><td>%s</td></tr>"
- uri (Str.string_after pos ((String.rindex pos '#') + 1))
- (if is_main_pos pos then
+ uri (U.text_of_position pos)
+ (if U.is_main_position pos then
sprintf "<input name='obj_depth' size='2' type='text' value='%s' />"
- (match depth with Some i -> string_of_int i | None -> "")
+ (U.text_of_depth pos "")
else
"<input type=\"hidden\" name=\"obj_depth\" />")
;;
-let html_of_r_rel (pos, depth) =
+let html_of_r_rel pos =
sprintf
"<tr><td><input type='checkbox' name='constr_rel' checked='on'/></td><td>%s</td><td><input name='rel_depth' size='2' type='text' value='%s' /></td></tr>"
- pos (match depth with Some i -> string_of_int i | None -> "")
+ (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
;;
-let html_of_r_sort (pos, depth, sort) =
+let html_of_r_sort (pos, sort) =
sprintf
"<tr><td><input type='checkbox' name='constr_sort' checked='on'/></td><td>%s</td><td>%s</td><td><input name='sort_depth' size='2' type='text' value='%s'/></td></tr>"
- sort pos (match depth with Some i -> string_of_int i | None -> "")
+ (U.text_of_sort sort) (U.text_of_position (pos:>T.full_position)) (U.text_of_depth (pos:>T.full_position) "")
;;
(** pretty print a MathQL query result to an HELM theory file *)
(* SEARCH ENGINE functions *)
-let whole_statement_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"]
-;;
-
-let only_conclusion_universe =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"]
-;;
-
-let refine_constraints (constr_obj, constr_rel, constr_sort) =
+let refine_constraints ((constr_obj:T.r_obj list), (constr_rel:T.r_rel list), (constr_sort:T.r_sort list)) =
function
"/searchPattern" ->
- whole_statement_universe,
+ 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 (uri,pos,_) -> (uri,pos,None))
+ (function (pos, uri) -> U.set_full_position pos None, uri)
(List.filter
- (function (uri,pos,depth) as constr -> is_concl_pos pos)
+ (function (pos, _) -> U.is_conclusion pos)
constr_obj)
in
- only_conclusion_universe,
+ U.universe_for_match_conclusion,
(*CSC: we must select the must constraints here!!! *)
(constr_obj',[],[]),(Some constr_obj', None, None)
| _ -> assert false
-in
+;;
let get_constraints term =
function
| _ -> raise NotAnInductiveDefinition
in
let constr_obj =
- [uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis",
- None ;
- uri,"http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
- Some 0
- ]
+ [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
in
- let constr_rel =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion",
- None] in
- let constr_sort =
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis",
- Some 1, "Prop"]
- in
- whole_statement_universe,
+ 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
-in
+;;
(*
format:
(* to be used on "obj" *)
let add_user_must33 user_must must =
List.map2
- (fun (b, i) (p1, p2, p3) -> if b then (p1, p2, i) else (p1, p2, None))
+ (fun (b, i) (p, u) -> U.set_full_position p (if b then i else None), u)
user_must must
in
(* to be used on "rel" *)
let add_user_must22 user_must must =
List.map2
- (fun (b, i) (p1, p2) -> if b then (p1, i) else (p1, None))
+ (fun (b, i) p -> U.set_main_position p (if b then i else None))
user_must must
in
(* to be used on "sort" *)
let add_user_must32 user_must must =
List.map2
- (fun (b, i) (p1, p2, p3) -> if b then (p1, i, p3) else (p1, None, p3))
+ (fun (b, i) (p, s) -> U.set_main_position p (if b then i else None), s)
user_must must
in
match Pcre.split ~pat:":" constraints with
debug_print (sprintf "Received request: %s" req#path);
(match req#path with
| "/execute" ->
- let mqi_handle = MQIConn.init mqi_flags debug_print in
+ let mqi_handle = C.init mqi_flags debug_print in
let query_string = req#param "query" in
let lexbuf = Lexing.from_string query_string in
let query = MQueryUtil.query_of_text lexbuf in
let result = MQueryInterpreter.execute mqi_handle query in
let result_string = pp_result result in
- MQIConn.close mqi_handle;
+ C.close mqi_handle;
Http_daemon.respond ~body:result_string ~headers:[contype] outchan
| "/locate" ->
- let mqi_handle = MQIConn.init mqi_flags debug_print in
+ let mqi_handle = C.init mqi_flags debug_print in
let id = req#param "id" in
- let query = MQueryGenerator.locate id in
+ let query = G.locate id in
let result = MQueryInterpreter.execute mqi_handle query in
- MQIConn.close mqi_handle;
+ C.close mqi_handle;
Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan
| "/getpage" ->
(* TODO implement "is_permitted" *)
| "/searchPattern"
| "/matchConclusion"
| "/locateInductivePrinciple" ->
- let mqi_handle = MQIConn.init mqi_flags debug_print in
+ let mqi_handle = C.init mqi_flags debug_print in
let term_string = req#param "term" in
let lexbuf = Lexing.from_string term_string in
let (context, metasenv) = ([], []) in
raise Chat_unfinished)
in
let query =
- MQueryGenerator.query_of_constraints (Some universe) must'' only'
+ G.query_of_constraints (Some universe) must'' only'
in
let results = MQueryInterpreter.execute mqi_handle query in
Http_daemon.send_basic_headers ~code:200 outchan ;
~headers:[contype]
~body:"some implicit variables are still unistantiated :-("
outchan);
- MQIConn.close mqi_handle
+ C.close mqi_handle
| invalid_request ->
Http_daemon.respond_error ~status:(`Client_error `Bad_request) outchan);
debug_print (sprintf "%s done!" req#path)
projects / helm.git / commitdiff