From 4c9da07604c4f8b66e4e92861ee38129422d23fb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 22 May 2003 14:49:52 +0000 Subject: [PATCH] mathql query generator interface patched --- helm/gTopLevel/Makefile | 4 +- helm/gTopLevel/gTopLevel.ml | 2 +- helm/ocaml/META.helm-mquery_generator.src | 5 - helm/ocaml/META.helm-tactics.src | 2 +- helm/ocaml/Makefile.in | 2 +- helm/ocaml/cic_textual_parser/.depend | 4 +- helm/ocaml/getter/.depend | 4 +- helm/ocaml/mquery_generator/.cvsignore | 5 - helm/ocaml/mquery_generator/.depend | 7 - helm/ocaml/mquery_generator/Makefile | 13 - .../ocaml/mquery_generator/mQueryGenerator.ml | 503 ------------------ .../mquery_generator/mQueryGenerator.mli | 43 -- helm/ocaml/mquery_generator/mQueryLevels.ml | 148 ------ helm/ocaml/mquery_generator/mQueryLevels.mli | 36 -- helm/ocaml/mquery_generator/mQueryLevels2.ml | 200 ------- helm/ocaml/mquery_generator/mQueryLevels2.mli | 36 -- helm/ocaml/tactics/.depend | 4 +- helm/ocaml/tactics/Makefile | 2 +- helm/ocaml/tactics/tacticChaser.ml | 2 +- helm/ocaml/tex_cic_textual_parser/.depend | 4 +- helm/searchEngine/Makefile | 2 +- helm/searchEngine/searchEngine.ml | 2 +- 22 files changed, 16 insertions(+), 1014 deletions(-) delete mode 100644 helm/ocaml/META.helm-mquery_generator.src delete mode 100644 helm/ocaml/mquery_generator/.cvsignore delete mode 100644 helm/ocaml/mquery_generator/.depend delete mode 100644 helm/ocaml/mquery_generator/Makefile delete mode 100644 helm/ocaml/mquery_generator/mQueryGenerator.ml delete mode 100644 helm/ocaml/mquery_generator/mQueryGenerator.mli delete mode 100644 helm/ocaml/mquery_generator/mQueryLevels.ml delete mode 100644 helm/ocaml/mquery_generator/mQueryLevels.mli delete mode 100644 helm/ocaml/mquery_generator/mQueryLevels2.ml delete mode 100644 helm/ocaml/mquery_generator/mQueryLevels2.mli diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 6076d9712..a94767f01 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -1,8 +1,8 @@ BIN_DIR = /usr/local/bin REQUIRES = lablgtkmathview helm-cic_textual_parser helm-tex_cic_textual_parser \ helm-cic_proof_checking helm-xml gdome2-xslt helm-cic_unification \ - helm-tactics helm-mathql helm-mathql_interpreter \ - helm-mquery_generator threads hbugs-client mathml-editor + helm-mathql helm-mathql_interpreter helm-mathql_generator \ + helm-tactics threads hbugs-client mathml-editor PREDICATES = "gnome,init,glade" OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o OCAMLFIND = ocamlfind diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 6f6b85404..e3f498931 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1920,7 +1920,7 @@ let completeSearchPattern () = let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = MQueryLevels2.get_constraints expr in let must',only = refine_constraints must in - let query = MQG.searchPattern must' only in + let query = MQG.query_of_constraints None must' only in let results = MQI.execute mqi_handle query in show_query_results results with diff --git a/helm/ocaml/META.helm-mquery_generator.src b/helm/ocaml/META.helm-mquery_generator.src deleted file mode 100644 index eb2c442b1..000000000 --- a/helm/ocaml/META.helm-mquery_generator.src +++ /dev/null @@ -1,5 +0,0 @@ -requires="helm-urimanager postgres natile-galax helm-mathql helm-mathql_interpreter helm-cic helm-cic_proof_checking" -version="0.0.1" -archive(byte)="mquery_generator.cma" -archive(native)="mquery_generator.cmxa" -linkopts="" diff --git a/helm/ocaml/META.helm-tactics.src b/helm/ocaml/META.helm-tactics.src index c05d5a4c8..cffd94f6b 100644 --- a/helm/ocaml/META.helm-tactics.src +++ b/helm/ocaml/META.helm-tactics.src @@ -1,4 +1,4 @@ -requires="helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification helm-mquery_generator" +requires="helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification helm-mathql_generator" version="0.0.1" archive(byte)="tactics.cma" archive(native)="tactics.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 4775ab302..c0ca10b0a 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 \ - mquery_generator mathql_test tactics + mathql_generator mathql_test tactics OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ diff --git a/helm/ocaml/cic_textual_parser/.depend b/helm/ocaml/cic_textual_parser/.depend index d7aabf85c..f5ce25fb9 100644 --- a/helm/ocaml/cic_textual_parser/.depend +++ b/helm/ocaml/cic_textual_parser/.depend @@ -6,5 +6,5 @@ cicTextualParserContext.cmo: cicTextualParser.cmi cicTextualParser0.cmo \ cicTextualParserContext.cmi cicTextualParserContext.cmx: cicTextualParser.cmx cicTextualParser0.cmx \ cicTextualParserContext.cmi -cicTextualLexer.cmo: cicTextualParser.cmi -cicTextualLexer.cmx: cicTextualParser.cmx +cicTextualLexer.cmo: cicTextualParser.cmi cicTextualParser0.cmo +cicTextualLexer.cmx: cicTextualParser.cmx cicTextualParser0.cmx diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index 2013e9b3e..c51f1a8e4 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -1,6 +1,6 @@ configuration.cmo: configuration.cmi configuration.cmx: configuration.cmi -clientHTTP.cmo: configuration.cmi clientHTTP.cmi -clientHTTP.cmx: configuration.cmx clientHTTP.cmi +clientHTTP.cmo: clientHTTP.cmi +clientHTTP.cmx: clientHTTP.cmi getter.cmo: clientHTTP.cmi configuration.cmi getter.cmi getter.cmx: clientHTTP.cmx configuration.cmx getter.cmi diff --git a/helm/ocaml/mquery_generator/.cvsignore b/helm/ocaml/mquery_generator/.cvsignore deleted file mode 100644 index 539f5b5ab..000000000 --- a/helm/ocaml/mquery_generator/.cvsignore +++ /dev/null @@ -1,5 +0,0 @@ -*.cmi -*.cmo -*.cma -*.cmx -*.cmxa diff --git a/helm/ocaml/mquery_generator/.depend b/helm/ocaml/mquery_generator/.depend deleted file mode 100644 index 8a5d89b72..000000000 --- a/helm/ocaml/mquery_generator/.depend +++ /dev/null @@ -1,7 +0,0 @@ -mQueryLevels2.cmi: 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 diff --git a/helm/ocaml/mquery_generator/Makefile b/helm/ocaml/mquery_generator/Makefile deleted file mode 100644 index 2e1ed8e7d..000000000 --- a/helm/ocaml/mquery_generator/Makefile +++ /dev/null @@ -1,13 +0,0 @@ -PACKAGE = mquery_generator -REQUIRES = helm-urimanager helm-mathql helm-cic helm-cic_proof_checking -PREDICATES = - -INTERFACE_FILES = mQueryLevels.mli mQueryLevels2.mli mQueryGenerator.mli - -IMPLEMENTATION_FILES = mQueryLevels.ml mQueryLevels2.ml mQueryGenerator.ml - -EXTRA_OBJECTS_TO_INSTALL = - -EXTRA_OBJECTS_TO_CLEAN = - -include ../Makefile.common diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.ml b/helm/ocaml/mquery_generator/mQueryGenerator.ml deleted file mode 100644 index f4d838266..000000000 --- a/helm/ocaml/mquery_generator/mQueryGenerator.ml +++ /dev/null @@ -1,503 +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/. - *) - -(* Query issuing functions **************************************************) - -type uri = string -type position = string -type depth = int option -type sort = string - -type r_obj = (uri * position * depth) -type r_rel = (position* depth) -type r_sort = (position* depth * sort) - -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) - -let builtin s = - let ns = "h:" in - match s with - | "MH" -> ns ^ "MainHypothesis" - | "IH" -> ns ^ "InHypothesis" - | "MC" -> ns ^ "MainConclusion" - | "IC" -> ns ^ "InConclusion" - | "IB" -> ns ^ "InBody" - | "SET" -> ns ^ "Set" - | "PROP" -> ns ^ "Prop" - | "TYPE" -> ns ^ "Type" - | _ -> raise (Failure "MQueryGenerator.builtin") - -(* Query building functions ************************************************) - -module M = MathQL - -let locate s = - M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s])) - -let searchPattern must_use can_use = - let in_path s = (s, []) in - let assign v p = (in_path v, in_path p) in - -(* can restrictions *) - - let (cr_o,cr_r,cr_s) = can_use in - - let uri_of_entry (r, p, d) = r in - - let universe = - match cr_o with - None -> [] - | Some cr_o -> List.map uri_of_entry cr_o - in - - let tfst (a,b,c) = a in - let tsnd (a,b,c) = b in - let trd (a,b,c) = c in - - let to_int_list l d = - match d with - None -> l - | Some d -> l@[d] - in - - let opos = - match cr_o with - None -> [] - | Some cr_o -> (List.map tsnd cr_o) in - - let odep = - match cr_o with - None -> [] - | Some cr_o -> List.map trd cr_o - (* let odep_option_list = List.map trd cr_o in - let lo_dep_int = List.fold_left to_int_list [] odep_option_list in - List.map string_of_int lo_dep_int*) - in - print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout; - print_endline""; - let rpos = - match cr_r with - None -> [] - | Some cr_r -> (List.map fst cr_r) in - - let rdep = - match cr_r with - None -> [] - | Some cr_r -> List.map snd cr_r - (* let rdep_option_list = List.map snd cr_r in - let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in - List.map string_of_int lr_dep_int *) - in - - - let spos = - match cr_s with - None -> [] - | Some cr_s -> (List.map tfst cr_s) in - - - let sdep = - match cr_s with - None -> [] - | Some cr_s -> List.map tsnd cr_s - (* let sdep_option_list = List.map tsnd cr_s in - let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in - List.map string_of_int ls_dep_int*) - in - - - let sor = - match cr_s with - None -> [] - | Some cr_s -> List.map trd cr_s in - - (* let q_where_obj = function - Some l -> - if odep = [] then - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]), - M.Ex ["uri"] - (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))), - M.VVar "universe") - else - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (M.And - ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))), - (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d"))))) - ) - ), - M.VVar "universe" - ) - - | None -> M.True - in*) - - - - let q_where_obj n = function - Some l -> - let rec q_ex n = function - [] -> M.True - | [(u,p,None)] -> - M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")) - - | [(u,p,d)] -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.And - (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")), - M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))) - | (u,p,None)::tl -> - M.Or - (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")), - q_ex (n+1) tl) - | (u,p,d)::tl -> - print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; - print_endline""; - M.Or - ((M.And - ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))), - (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))), - q_ex (n+1) tl) - in - M.Sub - (M.RefOf - (M.Select - ("uri", - M.Relation - (false, M.RefineExact, in_path "refObj", - M.Ref (M.RefOf (M.RVar "uri0")), - [assign "p" "position"; assign "d" "depth"] - ), - M.Ex ["uri"] - (q_ex 1 l))), - M.VVar "universe") - | None -> M.True - in - - - - - let rec q_where_rel n cr_r= (*function*) - (* Some l ->*) - let q0 = - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["position"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_position" ^ string_of_int n)) - in - match cr_r with - Some [] -> M.True - | Some [(p,None)] -> q0 - | Some [(p,d)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))) - | Some ((p,None)::tl) -> - M.Or - (q0, - q_where_rel (n+1) (Some tl)) - | Some ((p,d)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refRel", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("rel_depth" ^ string_of_int n))), - q_where_rel (n+1) (Some tl)) - | None -> M.True - in - - let rec q_where_sort n cr_s = (*function *) - (* Some l ->*) - let q0 = - M.And - (M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["position"]), - M.RefOf(M.RVar "uri0") - ), - M.VVar ("sort_position" ^ string_of_int n)), - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["sort"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort" ^ string_of_int n))) - in - match cr_s with - Some [] -> M.True - | Some [(p,None,s)] -> q0 - - | Some [(p,d,s)] -> - M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))) - - | Some ((p,None,s)::tl) -> - M.Or - (q0, - q_where_sort (n+1) (Some tl)) - - | Some((p,d,s)::tl) -> - M.Or - (M.And - (q0, - M.Sub - (M.Property - (false, M.RefineExact, ("refSort", ["depth"]), - M.RefOf(M.RVar "uri0")), - M.VVar ("sort_depth" ^ string_of_int n))), - q_where_sort (n+1) (Some tl)) - | None -> M.True - in - - - - - let q_where cr = - let (cr_o,cr_r,cr_s) = cr in - M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s)) - - in - -(* must restrictions *) - - let build_select_obj (r, pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position"]), - M.Ex ["uri"] - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (false, M.RefineExact, ("backPointer", []), - M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_rel (pos, dep) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))) - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) - in - - let build_select_sort (pos, dep, sor) = - match dep with - None -> M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - - | Some dep -> let string_dep = string_of_int dep in - M.Select - ("uri", - M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), - M.Ex ["uri"] - (M.And - ((M.And - ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), - (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))), - (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) - in - - let rec build_intersect_obj = function - [] -> M.Pattern (M.Const ["[.]*"]) - | [hd] -> build_select_obj hd - | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl) - in - - let rec build_intersect_rel = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_rel hd - | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl) - in - - let rec build_intersect_sort = function - [] -> M.Ref(M.Const []) - | [hd] -> build_select_sort hd - | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl) - in - - let build_intersect = function -(* let tostring_sort (a,b,c) = - let b1 = string_of_int b in - (a,b1,c) - in - let tostring_rel (a,b) = - let b1 = string_of_int b in - (a,b1) - in*) - -(* let (l1,l2,l3) = must in - match (l1,l2,l3) with *) - l1,[],[] -> build_intersect_obj l1 - | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - build_intersect_rel l2 - | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*) - build_intersect_sort l3 - | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*) - M.Intersect (build_intersect_obj l1, build_intersect_rel l2) - | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *) - M.Intersect (build_intersect_obj l1, build_intersect_sort l3) - | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in*) - M.Intersect (build_intersect_rel l2, build_intersect_sort l3) - | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in - let lsort = List.map tostring_sort l3 in *) - M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3) - in - - let q_in = build_intersect must_use in - let q_select = M.Select ("uri0", q_in, q_where can_use) in - -(* variables for can restrictions *) - - let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in - - let rec q_let_s sor n = - match sor with - [] -> q_let_u - | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u) - | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1)) - in - -(* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *) - - let rec q_let_ds sdep n = - match sdep with - [] - | [None] -> q_let_s sor 1 - | (None)::tl -> q_let_ds tl (n+1) - | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1) - | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1)) - in - -(* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *) - - let rec q_let_dr rdep n = - match rdep with - [] - | [None] -> q_let_ds sdep 1 - | (None)::tl -> q_let_dr tl (n+1) - | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1) - | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1)) - in - - - (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*) - - let rec q_let_do odep n = - match odep with - [] - | [None] -> q_let_dr rdep 1 - | (None)::tl -> q_let_do tl (n+1) - | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1) - | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1)) - in - - -(* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *) - - - let rec q_let_ps spos n = - match spos with - [] -> q_let_do odep 1 - | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1) - | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1)) - in - - -(* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *) - - - let rec q_let_pr rpos n = - match rpos with - [] -> q_let_ps spos 1 - | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1) - | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1)) - in - - - -(* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *) - - let rec q_let_po opos n = - match opos with - [] -> q_let_pr rpos 1 - | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1) - | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1)) - in - - (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*) - - let query = (M.Ref (M.RefOf (q_let_po opos 1))) in - -print_endline "### "; MQueryUtil.text_of_query print_string query "\n"; flush stdout; - query diff --git a/helm/ocaml/mquery_generator/mQueryGenerator.mli b/helm/ocaml/mquery_generator/mQueryGenerator.mli deleted file mode 100644 index e1ad25caf..000000000 --- a/helm/ocaml/mquery_generator/mQueryGenerator.mli +++ /dev/null @@ -1,43 +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/. - *) - -type uri = string -type position = string -type depth = int option -type sort = string - -type r_obj = (uri * position * depth) -type r_rel = (position * depth) -type r_sort = (position * depth * sort) - -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) - -val locate : string -> MathQL.query - -val searchPattern : must_restrictions -> only_restrictions -> MathQL.query - -val builtin : MathQL.vvar -> string diff --git a/helm/ocaml/mquery_generator/mQueryLevels.ml b/helm/ocaml/mquery_generator/mQueryLevels.ml deleted file mode 100644 index 977638dba..000000000 --- a/helm/ocaml/mquery_generator/mQueryLevels.ml +++ /dev/null @@ -1,148 +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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -let levels_of_term metasenv context term = - let module TC = CicTypeChecker in - let module Red = CicReduction in - let module Util = MQueryUtil in - let degree t = - let rec degree_aux = function - | Cic.Sort _ -> 1 - | Cic.Cast (u, _) -> degree_aux u - | Cic.Prod (_, _, t) -> degree_aux t - | _ -> 2 - in - let u = TC.type_of_aux' metasenv context t in - degree_aux (Red.whd context u) - in - let entry_eq (s1, b1, v1) (s2, b2, v2) = - s1 = s2 && b1 = b2 - in - let rec entry_in e = function - | [] -> [e] - | head :: tail -> - head :: if entry_eq head e then tail else entry_in e tail - in - let inspect_uri main l uri tc v term = - let d = degree term in - entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l - in - let rec inspect_term main l v term = match term with - Cic.Rel _ -> l - | Cic.Meta _ -> l - | Cic.Sort _ -> l - | Cic.Implicit -> l - | Cic.Var (u,exp_named_subst) -> - let l' = inspect_uri main l u [] v term in - inspect_exp_named_subst l' (v+1) exp_named_subst - | Cic.Const (u,exp_named_subst) -> - let l' = inspect_uri main l u [] v term in - inspect_exp_named_subst l' (v+1) exp_named_subst - | Cic.MutInd (u, t, exp_named_subst) -> - let l' = inspect_uri main l u [t] v term in - inspect_exp_named_subst l' (v+1) exp_named_subst - | Cic.MutConstruct (u, t, c, exp_named_subst) -> - let l' = inspect_uri main l u [t; c] v term in - inspect_exp_named_subst l' (v+1) exp_named_subst - | Cic.Cast (uu, _) -> - inspect_term main l v uu - | Cic.Prod (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term main luu (v + 1) tt - | Cic.Lambda (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Cic.LetIn (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Cic.Appl m -> inspect_list main l true v m - | Cic.MutCase (u, t, tt, uu, m) -> - let lu = inspect_uri main l u [t] (v + 1) term in - let ltt = inspect_term false lu (v + 1) tt in - let luu = inspect_term false ltt (v + 1) uu in - inspect_list main luu false (v + 1) m - | Cic.Fix (_, m) -> inspect_ind l (v + 1) m - | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m - and inspect_list main l head v = function - | [] -> l - | tt :: m -> - let ltt = inspect_term main l (if head then v else v + 1) tt in - inspect_list false ltt false v m - and inspect_exp_named_subst l v = function - [] -> l - | (_,t) :: tl -> - let l' = inspect_term false l v t in - inspect_exp_named_subst l' v tl - and inspect_ind l v = function - | [] -> l - | (_, _, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_ind luu v m - and inspect_coind l v = function - | [] -> l - | (_, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_coind luu v m - in - let rec inspect_backbone = function - | Cic.Cast (uu, _) -> inspect_backbone uu - | Cic.Prod (_, _, tt) -> inspect_backbone tt - | Cic.LetIn (_, uu, tt) -> inspect_backbone tt - | t -> inspect_term true [] 0 t - in - inspect_backbone term - -let out_restr e c t = - let can = levels_of_term e c t in (* can restrictions *) -prerr_endline ""; -prerr_endline - ("#### IN LEVELS @@@@ lunghezza can: " ^ string_of_int (List.length can)); -prerr_endline ""; -(* let rest = restrict level levels in *) - let uri_pos (u,b,v) = (u,b) in - let can_use = List.map uri_pos can in - let lofl (u,b,v) = [(u,b)] in - let rec organize_restr rlist prev_r= - match rlist with - [] -> [] - | r::tl ->let curr_r = r@prev_r in - curr_r::(organize_restr tl curr_r) - in - let mrest = List.map lofl can in - let must_use = organize_restr mrest [] in (* must restrictions *) - (must_use,can_use) -;; diff --git a/helm/ocaml/mquery_generator/mQueryLevels.mli b/helm/ocaml/mquery_generator/mQueryLevels.mli deleted file mode 100644 index 5b214b733..000000000 --- a/helm/ocaml/mquery_generator/mQueryLevels.mli +++ /dev/null @@ -1,36 +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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list) diff --git a/helm/ocaml/mquery_generator/mQueryLevels2.ml b/helm/ocaml/mquery_generator/mQueryLevels2.ml deleted file mode 100644 index 968d2a35e..000000000 --- a/helm/ocaml/mquery_generator/mQueryLevels2.ml +++ /dev/null @@ -1,200 +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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 02/12/2002 *) -(* *) -(* Missing description *) -(* *) -(******************************************************************************) - -type classification = - Backbone of int - | Branch of int - | InConclusion - | InHypothesis -;; - -let soften_classification = - function - Backbone _ -> InConclusion - | Branch _ -> InHypothesis - | k -> k -;; - -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 -;; - -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 - in - merge l1 l1', merge l2 l2', merge l3 l3' -;; - -let get_constraints term = - let module U = UriManager in - let module C = Cic in - 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) - | C.Rel _ -> - let kind',depth = !!kind in - (match depth with - None -> [],[],[] - | Some d -> [],[kind',Some d],[]) - | C.Sort s -> - (match kind with - Backbone _ - | Branch _ -> - let s' = - match s with - Cic.Prop -> - "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop" - | Cic.Set -> - "http://www.cs.unibo.it/helm/schemas/schema-helm#Set" - | Cic.Type -> - "http://www.cs.unibo.it/helm/schemas/schema-helm#Type" - in - let kind',depth = !!kind in - (match depth with - None -> assert false - | Some d -> [],[],[kind',Some d,s']) - | _ -> [],[],[]) - | C.Meta _ - | C.Implicit -> assert false - | C.Cast (te,_) -> - (* type ignored *) - process_type_aux kind te - | C.Prod (_,sou,ta) -> - let (source_kind,target_kind) = - match kind with - Backbone n -> (Branch 0, Backbone (n+1)) - | Branch n -> (InHypothesis, Branch (n+1)) - | k -> (k,k) - in - process_type_aux source_kind sou @@ - process_type_aux target_kind ta - | C.Lambda (_,sou,ta) -> - let kind' = soften_classification kind in - process_type_aux kind' sou @@ - process_type_aux kind' ta - | C.LetIn (_,te,ta)-> - let kind' = soften_classification kind in - process_type_aux kind' te @@ - process_type_aux kind ta - | C.Appl (he::tl) -> - let kind' = soften_classification kind in - process_type_aux kind he @@ - 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],[],[] - | 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],[],[]) @@ - (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) - | C.MutCase (_,_,_,term,patterns) -> - (* outtype ignored *) - let kind' = soften_classification kind in - process_type_aux kind' term @@ - List.fold_left (fun i t -> i @@ process_type_aux kind' t) - ([],[],[]) patterns - | C.Fix (_,funs) -> - let kind' = soften_classification kind in - List.fold_left - (fun i (_,_,bo,ty) -> - i @@ - process_type_aux kind' bo @@ - process_type_aux kind' ty - ) ([],[],[]) funs - | C.CoFix (_,funs) -> - let kind' = soften_classification kind in - List.fold_left - (fun i (_,bo,ty) -> - i @@ - process_type_aux kind' bo @@ - process_type_aux kind' ty - ) ([],[],[]) funs - and process_type_aux_expl_named_subst kind = - List.fold_left - (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t)) - ([],[],[]) -in - let obj_constraints,rel_constraints,sort_constraints = - process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term) - in - (obj_constraints,rel_constraints,sort_constraints) -;; - -(*CSC: Debugging only *) -let get_constraints term = - let res = get_constraints term in - let (objs,rels,sorts) = res 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 ; - 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 ; - 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) - ) sorts ; - res -;; diff --git a/helm/ocaml/mquery_generator/mQueryLevels2.mli b/helm/ocaml/mquery_generator/mQueryLevels2.mli deleted file mode 100644 index 805f1064d..000000000 --- a/helm/ocaml/mquery_generator/mQueryLevels2.mli +++ /dev/null @@ -1,36 +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/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -val get_constraints: Cic.term -> MQueryGenerator.must_restrictions diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 8d0d98338..fd3a652e8 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -76,5 +76,5 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ tacticals.cmx fourierR.cmi -tacticChaser.cmo: tacticChaser.cmi -tacticChaser.cmx: tacticChaser.cmi +tacticChaser.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticChaser.cmi +tacticChaser.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticChaser.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 35cd53517..0018ce230 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -1,7 +1,7 @@ PACKAGE = tactics REQUIRES = \ helm-cic_textual_parser helm-cic_proof_checking helm-cic_unification \ - helm-mquery_generator + helm-mathql_interpreter helm-mathql_generator INTERFACE_FILES = \ proofEngineReduction.mli proofEngineHelpers.mli \ diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index f38258d1e..6f83c3fd6 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -52,7 +52,7 @@ let searchPattern mqi_handle ?(output_html = (fun _ -> ())) ~choose_must () ~sta let rigth_only = Some (List.map torigth_restriction only) in let result = MQueryInterpreter.execute mqi_handle - (MQueryGenerator.searchPattern + (MQueryGenerator.query_of_constraints None (rigth_must,[],[]) (rigth_only,None,None)) in let uris = List.map diff --git a/helm/ocaml/tex_cic_textual_parser/.depend b/helm/ocaml/tex_cic_textual_parser/.depend index 28a4689f8..71156776a 100644 --- a/helm/ocaml/tex_cic_textual_parser/.depend +++ b/helm/ocaml/tex_cic_textual_parser/.depend @@ -1,6 +1,4 @@ -texCicTextualParser.cmi: texCicTextualParser0.cmo -texCicTextualParserContext.cmi: texCicTextualParser.cmi \ - texCicTextualParser0.cmo +texCicTextualParserContext.cmi: texCicTextualParser.cmi texCicTextualParser.cmo: texCicTextualParser0.cmo texCicTextualParser.cmi texCicTextualParser.cmx: texCicTextualParser0.cmx texCicTextualParser.cmi texCicTextualParserContext.cmo: texCicTextualParser.cmi \ diff --git a/helm/searchEngine/Makefile b/helm/searchEngine/Makefile index 7145312c0..a2287e77d 100644 --- a/helm/searchEngine/Makefile +++ b/helm/searchEngine/Makefile @@ -1,6 +1,6 @@ REQUIRES = http helm-cic_textual_parser helm-cic_proof_checking \ helm-xml gdome2-xslt helm-cic_unification helm-mathql \ - helm-mathql_interpreter helm-mquery_generator netclient + helm-mathql_interpreter helm-mathql_generator netclient OCAMLOPTIONS = -package "$(REQUIRES)" -pp camlp4o -I ../gTopLevel OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index ecedf5ab7..ef4b1e033 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -592,7 +592,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; constraints_choice_TPL; raise Chat_unfinished) in - let query = MQueryGenerator.searchPattern must'' only' in + let query = MQueryGenerator.query_of_constraints None must'' only' in let results = MQueryInterpreter.execute mqi_handle query in Http_daemon.send_basic_headers ~code:200 outchan ; Http_daemon.send_CRLF outchan ; -- 2.39.2