From: Ferruccio Guidi Date: Wed, 2 Jul 2003 11:01:34 +0000 (+0000) Subject: mathql_generator: new constraint format (more type safe) X-Git-Tag: camera_ready~24 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0e74e8e94eada756157addce67e4adeb8dff1feb mathql_generator: new constraint format (more type safe) mathql_test : moved outside ocaml --- diff --git a/helm/Makefile b/helm/Makefile index fb0fac994..721a89621 100644 --- a/helm/Makefile +++ b/helm/Makefile @@ -1,4 +1,4 @@ -DIRS = ocaml hbugs gTopLevel searchEngine +DIRS = ocaml hbugs gTopLevel searchEngine mathql_test DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 0ceb6f2af..f1710cfce 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -39,6 +39,8 @@ open Printf;; module MQI = MQueryInterpreter module MQIC = MQIConn +module MQGT = MQGTypes +module MQGU = MQGUtil module MQG = MQueryGenerator (* GLOBAL CONSTANTS *) @@ -1756,32 +1758,36 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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 = @@ -1804,30 +1810,19 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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 = @@ -1850,30 +1845,22 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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 = @@ -1895,15 +1882,18 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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), @@ -1925,14 +1915,7 @@ let completeSearchPattern () = 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 @@ -2148,7 +2131,7 @@ let searchPattern () = | None -> () | Some metano -> let uris' = - TacticChaser.searchPattern + TacticChaser.matchConclusion mqi_handle ~output_html:(output_html outputhtml) ~choose_must () ~status:(proof, metano) diff --git a/helm/hbugs/tutors/search_pattern_apply_tutor.ml b/helm/hbugs/tutors/search_pattern_apply_tutor.ml index d7b2da2ba..8ba1f8386 100644 --- a/helm/hbugs/tutors/search_pattern_apply_tutor.ml +++ b/helm/hbugs/tutors/search_pattern_apply_tutor.ml @@ -32,7 +32,7 @@ let slave mqi_handle (state, musing_id) = | 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 diff --git a/helm/mathql_test/.cvsignore b/helm/mathql_test/.cvsignore new file mode 100644 index 000000000..180760238 --- /dev/null +++ b/helm/mathql_test/.cvsignore @@ -0,0 +1,2 @@ +*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples* +mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml diff --git a/helm/mathql_test/.depend b/helm/mathql_test/.depend new file mode 100644 index 000000000..b8d9e578a --- /dev/null +++ b/helm/mathql_test/.depend @@ -0,0 +1,6 @@ +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 diff --git a/helm/mathql_test/Makefile b/helm/mathql_test/Makefile new file mode 100644 index 000000000..04fea5185 --- /dev/null +++ b/helm/mathql_test/Makefile @@ -0,0 +1,79 @@ +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 + diff --git a/helm/mathql_test/mQGTopLexer.mll b/helm/mathql_test/mQGTopLexer.mll new file mode 100644 index 000000000..7e69bccf6 --- /dev/null +++ b/helm/mathql_test/mQGTopLexer.mll @@ -0,0 +1,71 @@ +(* 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 + *) + +{ + 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 } diff --git a/helm/mathql_test/mQGTopParser.mly b/helm/mathql_test/mQGTopParser.mly new file mode 100644 index 000000000..3e260d88f --- /dev/null +++ b/helm/mathql_test/mQGTopParser.mly @@ -0,0 +1,107 @@ +/* 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 + */ + +%{ + 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 ID + %token CONURI + %token VARURI + %token INDTYURI + %token INDCONURI + %token ALIAS EOF + + %start interp + %type CicTextualParser0.interpretation_codomain_item option> interp + + %token STR + %token DL DQ LC RC CM + %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV + + %start qstr specs + %type qstr + %type 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 { [] } + ; diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml new file mode 100644 index 000000000..9a7c8d9db --- /dev/null +++ b/helm/mathql_test/mqgtop.ml @@ -0,0 +1,299 @@ +(* 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 + *) + +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 = "

\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 diff --git a/helm/mathql_test/mqitop.ml b/helm/mathql_test/mqitop.ml new file mode 100644 index 000000000..7dd43888c --- /dev/null +++ b/helm/mathql_test/mqitop.ml @@ -0,0 +1,52 @@ +(* 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 + *) + +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) diff --git a/helm/mathql_test/mqtop.ml b/helm/mathql_test/mqtop.ml new file mode 100644 index 000000000..48ffb1e74 --- /dev/null +++ b/helm/mathql_test/mqtop.ml @@ -0,0 +1,40 @@ +(* 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 + *) + +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) diff --git a/helm/ocaml/META.helm-mathql_test.src b/helm/ocaml/META.helm-mathql_test.src deleted file mode 100644 index 4d66fc34d..000000000 --- a/helm/ocaml/META.helm-mathql_test.src +++ /dev/null @@ -1,3 +0,0 @@ -requires="unix helm-cic_textual_parser helm-mathql helm-mathql_interpreter helm-mathql_generator" -version="1.3" -linkopts="" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 96a7522d9..c53affed3 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,7 +2,7 @@ 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@ diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend index 5411fa4e7..769e30c89 100644 --- a/helm/ocaml/mathql/.depend +++ b/helm/ocaml/mathql/.depend @@ -6,5 +6,3 @@ mQueryTLexer.cmo: mQueryTParser.cmi 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 diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index 8a5d89b72..b8ecb1367 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -1,7 +1,11 @@ -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 diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index a694e0376..6b8252c20 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -4,11 +4,12 @@ REQUIRES = helm-cic helm-cic_proof_checking helm-mathql 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 = diff --git a/helm/ocaml/mathql_generator/mQGTypes.ml b/helm/ocaml/mathql_generator/mQGTypes.ml new file mode 100644 index 000000000..2dacfe14c --- /dev/null +++ b/helm/ocaml/mathql_generator/mQGTypes.ml @@ -0,0 +1,74 @@ +(* 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 + * Claudio Sacerdoti Coen + *) + +(* 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 diff --git a/helm/ocaml/mathql_generator/mQGUtil.ml b/helm/ocaml/mathql_generator/mQGUtil.ml new file mode 100644 index 000000000..a7a6bc6a4 --- /dev/null +++ b/helm/ocaml/mathql_generator/mQGUtil.ml @@ -0,0 +1,149 @@ +(* 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 + *) + +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] diff --git a/helm/ocaml/mathql_generator/mQGUtil.mli b/helm/ocaml/mathql_generator/mQGUtil.mli new file mode 100644 index 000000000..bb623cc86 --- /dev/null +++ b/helm/ocaml/mathql_generator/mQGUtil.mli @@ -0,0 +1,74 @@ +(* 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 + *) + +(* 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 diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 2d529c9e8..1a0211102 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -26,58 +26,11 @@ (* AUTOR: Ferruccio Guidi *) -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 = @@ -109,8 +62,10 @@ let compose cl = | 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] [] @@ -123,19 +78,21 @@ let compose cl = 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 @@ -143,7 +100,7 @@ let compose cl = | [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 @@ -173,44 +130,25 @@ let compose cl = 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 @@ -218,19 +156,20 @@ let query_of_constraints u (musts_obj, musts_rel, 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) + diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli index 6081cd028..c4dc0f9e5 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.mli +++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli @@ -26,45 +26,15 @@ (* AUTOR: Ferruccio Guidi *) -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 diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.ml b/helm/ocaml/mathql_generator/mQueryLevels2.ml index d9e9e5359..60633f897 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels2.ml +++ b/helm/ocaml/mathql_generator/mQueryLevels2.ml @@ -34,6 +34,9 @@ (* *) (******************************************************************************) +module T = MQGTypes +module U = MQGUtil + type classification = Backbone of int | Branch of int @@ -50,16 +53,20 @@ let soften_classification = 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 @@ -73,28 +80,24 @@ let get_constraints term = 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 @@ -124,18 +127,15 @@ let get_constraints term = 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 @@ -173,25 +173,17 @@ 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 ;; diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.mli b/helm/ocaml/mathql_generator/mQueryLevels2.mli index f62818363..83f681414 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels2.mli +++ b/helm/ocaml/mathql_generator/mQueryLevels2.mli @@ -34,4 +34,4 @@ (* *) (******************************************************************************) -val get_constraints: Cic.term -> MQueryGenerator.must_restrictions +val get_constraints: Cic.term -> MQGTypes.must_restrictions diff --git a/helm/ocaml/mathql_test/.cvsignore b/helm/ocaml/mathql_test/.cvsignore deleted file mode 100644 index 180760238..000000000 --- a/helm/ocaml/mathql_test/.cvsignore +++ /dev/null @@ -1,2 +0,0 @@ -*.cm[aiox] *.cmxa *.opt mqtop mqitop mqgtop examples* -mQGTopParser.ml mQGTopParser.mli mQGTopLexer.ml diff --git a/helm/ocaml/mathql_test/.depend b/helm/ocaml/mathql_test/.depend deleted file mode 100644 index b8d9e578a..000000000 --- a/helm/ocaml/mathql_test/.depend +++ /dev/null @@ -1,6 +0,0 @@ -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 diff --git a/helm/ocaml/mathql_test/Makefile b/helm/ocaml/mathql_test/Makefile deleted file mode 100644 index 04fea5185..000000000 --- a/helm/ocaml/mathql_test/Makefile +++ /dev/null @@ -1,79 +0,0 @@ -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 - diff --git a/helm/ocaml/mathql_test/mQGTopLexer.mll b/helm/ocaml/mathql_test/mQGTopLexer.mll deleted file mode 100644 index 7e69bccf6..000000000 --- a/helm/ocaml/mathql_test/mQGTopLexer.mll +++ /dev/null @@ -1,71 +0,0 @@ -(* 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 - *) - -{ - 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 } diff --git a/helm/ocaml/mathql_test/mQGTopParser.mly b/helm/ocaml/mathql_test/mQGTopParser.mly deleted file mode 100644 index cf2280dad..000000000 --- a/helm/ocaml/mathql_test/mQGTopParser.mly +++ /dev/null @@ -1,114 +0,0 @@ -/* 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 - */ - -%{ - 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 ID - %token CONURI - %token VARURI - %token INDTYURI - %token INDCONURI - %token ALIAS EOF - - %start interp - %type CicTextualParser0.interpretation_codomain_item option> interp - - %token STR - %token DL DQ LC RC CM - %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV - - %start qstr specs - %type qstr - %type 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 { [] } - ; diff --git a/helm/ocaml/mathql_test/mqgtop.ml b/helm/ocaml/mathql_test/mqgtop.ml deleted file mode 100644 index 0ef1ca981..000000000 --- a/helm/ocaml/mathql_test/mqgtop.ml +++ /dev/null @@ -1,301 +0,0 @@ -(* 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 - *) - -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 = "

\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 diff --git a/helm/ocaml/mathql_test/mqitop.ml b/helm/ocaml/mathql_test/mqitop.ml deleted file mode 100644 index 7dd43888c..000000000 --- a/helm/ocaml/mathql_test/mqitop.ml +++ /dev/null @@ -1,52 +0,0 @@ -(* 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 - *) - -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) diff --git a/helm/ocaml/mathql_test/mqtop.ml b/helm/ocaml/mathql_test/mqtop.ml deleted file mode 100644 index 48ffb1e74..000000000 --- a/helm/ocaml/mathql_test/mqtop.ml +++ /dev/null @@ -1,40 +0,0 @@ -(* 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 - *) - -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) diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 76a58091d..c4bfc5e03 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -33,29 +33,25 @@ (* *) (******************************************************************************) +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 diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli index f514360ac..847dbc8b8 100644 --- a/helm/ocaml/tactics/tacticChaser.mli +++ b/helm/ocaml/tactics/tacticChaser.mli @@ -23,11 +23,11 @@ * 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 diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index ca5076635..6e3b846d2 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -23,6 +23,11 @@ * http://cs.unibo.it/helm/. *) +module T = MQGTypes +module U = MQGUtil +module G = MQueryGenerator +module C = MQIConn + open Http_types ;; let debug = true;; @@ -72,41 +77,29 @@ let int_of_string' = function 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 "%s%s%s" - 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 "" - (match depth with Some i -> string_of_int i | None -> "") + (U.text_of_depth pos "") else "") ;; -let html_of_r_rel (pos, depth) = +let html_of_r_rel pos = sprintf "%s" - 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 "%s%s" - 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 *) @@ -184,37 +177,25 @@ let contype = "Content-Type", "text/html";; (* 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 @@ -225,25 +206,16 @@ let get_constraints term = | _ -> 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: @@ -270,19 +242,19 @@ let add_user_constraints ~constraints (* 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 @@ -318,20 +290,20 @@ let callback (req: Http_types.request) outchan = 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" *) @@ -388,7 +360,7 @@ let callback (req: Http_types.request) outchan = | "/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 @@ -613,7 +585,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; 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 ; @@ -651,7 +623,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; ~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)