From 6203a9d0d56c7ec7cd11713b5ed56645271154be Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 24 Nov 2005 13:01:31 +0000 Subject: [PATCH] split non-logic level of whelp away from metadataQuery to a new module --- .../METAS/meta.helm-cic_disambiguation.src | 2 +- helm/ocaml/METAS/meta.helm-tactics.src | 2 +- helm/ocaml/METAS/meta.helm-whelp.src | 4 + helm/ocaml/Makefile.in | 1 + helm/ocaml/cic_disambiguation/disambiguate.ml | 2 +- helm/ocaml/tactics/eliminationTactics.ml | 3 +- helm/ocaml/tactics/fwdSimplTactic.ml | 2 +- helm/ocaml/tactics/metadataQuery.ml | 284 +----------------- helm/ocaml/tactics/metadataQuery.mli | 14 - helm/ocaml/whelp/.cvsignore | 7 + helm/ocaml/whelp/.depend | 4 + helm/ocaml/whelp/Makefile | 10 + helm/ocaml/whelp/fwdQueries.ml | 113 +++++++ helm/ocaml/whelp/fwdQueries.mli | 28 ++ helm/ocaml/whelp/whelp.ml | 213 +++++++++++++ helm/ocaml/whelp/whelp.mli | 30 ++ 16 files changed, 423 insertions(+), 296 deletions(-) create mode 100644 helm/ocaml/METAS/meta.helm-whelp.src create mode 100644 helm/ocaml/whelp/.cvsignore create mode 100644 helm/ocaml/whelp/.depend create mode 100644 helm/ocaml/whelp/Makefile create mode 100644 helm/ocaml/whelp/fwdQueries.ml create mode 100644 helm/ocaml/whelp/fwdQueries.mli create mode 100644 helm/ocaml/whelp/whelp.ml create mode 100644 helm/ocaml/whelp/whelp.mli diff --git a/helm/ocaml/METAS/meta.helm-cic_disambiguation.src b/helm/ocaml/METAS/meta.helm-cic_disambiguation.src index 80d468c4a..1d084c4e3 100644 --- a/helm/ocaml/METAS/meta.helm-cic_disambiguation.src +++ b/helm/ocaml/METAS/meta.helm-cic_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-tactics helm-cic_notation" +requires="helm-whelp helm-cic_notation helm-cic_unification" version="0.0.1" archive(byte)="cic_disambiguation.cma" archive(native)="cic_disambiguation.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-tactics.src b/helm/ocaml/METAS/meta.helm-tactics.src index d12fe16fd..6e704ba06 100644 --- a/helm/ocaml/METAS/meta.helm-tactics.src +++ b/helm/ocaml/METAS/meta.helm-tactics.src @@ -1,4 +1,4 @@ -requires="helm-cic_proof_checking helm-cic_unification helm-metadata" +requires="helm-cic_proof_checking helm-cic_unification helm-whelp" version="0.0.1" archive(byte)="tactics.cma" archive(native)="tactics.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-whelp.src b/helm/ocaml/METAS/meta.helm-whelp.src new file mode 100644 index 000000000..20ea84329 --- /dev/null +++ b/helm/ocaml/METAS/meta.helm-whelp.src @@ -0,0 +1,4 @@ +requires="helm-metadata" +version="0.0.1" +archive(byte)="whelp.cma" +archive(native)="whelp.cmxa" diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 6b2bf09cb..4147a9226 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -16,6 +16,7 @@ MODULES = \ cic_unification \ cic_omdoc \ metadata \ + whelp \ tactics \ cic_notation \ cic_transformations \ diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 8bdb409e9..3acfd3904 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -687,7 +687,7 @@ end module Make (C: Callbacks) = struct let choices_of_id dbd id = - let uris = MetadataQuery.locate ~dbd id in + let uris = Whelp.locate ~dbd id in let uris = match uris with | [] -> diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 27cb1cc33..17d416ea9 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -30,7 +30,6 @@ module S = ProofEngineStructuralRules module F = FreshNamesGenerator module E = ProofEngineTypes module H = ProofEngineHelpers -module Q = MetadataQuery (* let induction_tac ~term status = @@ -147,7 +146,7 @@ let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) let (proof, goal) = status in let _, metasenv,_,_ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in - let types = List.rev_append user_types (Q.decomposables dbd) in + let types = List.rev_append user_types (FwdQueries.decomposables dbd) in let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in let old_context_length = List.length context in let tac = T.then_ ~start:(tactic ~what) diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index a5c7878c7..a40dd42b3 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -132,7 +132,7 @@ let fwd_simpl_tac let _, metasenv, _, _ = proof in let _, context, ty = CicUtil.lookup_meta goal metasenv in let index, major = PEH.lookup_type metasenv context hyp in - match MetadataQuery.fwd_simpl ~dbd major with + match FwdQueries.fwd_simpl ~dbd major with | [] -> error fail_msg2 | uri :: _ -> Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr; diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index eaa146ed1..535509a88 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -25,85 +25,15 @@ open Printf +let nonvar uri = not (UriManager.uri_is_var uri) + module Constr = MetadataConstraints -module PET = ProofEngineTypes exception Goal_is_not_an_equation let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) - (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for - * the "like" operator (which uses '%' and '_'). Does not support escaping. *) -let sqlpat_of_shellglob = - let star_RE, qmark_RE, percent_RE, uscore_RE = - Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" - in - fun shellglob -> - Pcre.replace ~rex:star_RE ~templ:"%" - (Pcre.replace ~rex:qmark_RE ~templ:"_" - (Pcre.replace ~rex:percent_RE ~templ:"\\%" - (Pcre.replace ~rex:uscore_RE ~templ:"\\_" - shellglob))) - -let nonvar uri = not (UriManager.uri_is_var uri) - -let locate ~(dbd:HMysql.dbd) ?(vars = false) pat = - let sql_pat = sqlpat_of_shellglob pat in - let query = - sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^ - "SELECT source FROM %s WHERE value LIKE \"%s\"") - (MetadataTypes.name_tbl ()) sql_pat - MetadataTypes.library_name_tbl sql_pat - in - let result = HMysql.exec dbd query in - List.filter nonvar - (HMysql.map result - (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)) - -let match_term ~(dbd:HMysql.dbd) ty = -(* debug_print (lazy (CicPp.ppterm ty)); *) - let metadata = MetadataExtractor.compute ~body:None ~ty in - let constants_no = - MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty) - in - let full_card, diff = - if CicUtil.is_meta_closed ty then - Some (MetadataConstraints.Eq constants_no), None - else - let diff_no = - let (hyp_constants, concl_constants) = - (* collect different constants in hypotheses and conclusions *) - List.fold_left - (fun ((hyp, concl) as acc) metadata -> - match (metadata: MetadataTypes.metadata) with - | `Sort _ | `Rel _ -> acc - | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) - when not (List.mem uri concl) -> (hyp, uri :: concl) - | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) - when not (List.mem uri hyp) -> (uri :: hyp, concl) - | `Obj _ -> acc) - ([], []) - metadata - in - List.length hyp_constants - List.length concl_constants - in - let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in - let diff = - if MetadataExtractor.IntSet.equal concl_metas hyp_metas then - Some (MetadataConstraints.Eq diff_no) - else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then - Some (MetadataConstraints.Gt (diff_no - 1)) - else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then - Some (MetadataConstraints.Lt (diff_no + 1)) - else - None - in - None, diff - in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ?full_card ?diff constraints - let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) let signature_of_hypothesis context = @@ -133,7 +63,9 @@ let sigmatch = let profiler = CicUtil.profile "sigmatch" in fun ~dbd ~facts ~where signature -> profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature -*) let at_most = Constr.at_most let sigmatch = MetadataConstraints.sigmatch +*) +let at_most = Constr.at_most +let sigmatch = MetadataConstraints.sigmatch let filter_uris_forward ~dbd (main, constants) uris = let main_uris = @@ -234,7 +166,9 @@ let sigmatch = let cmatch' = let profiler = CicUtil.profile "cmatch'" in fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature -*) let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose let cmatch' = Constr.cmatch' +*) +let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose +let cmatch' = Constr.cmatch' let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) = let (_, metasenv, _, _) = proof in @@ -429,205 +363,3 @@ let new_experimental_hint Pervasives.compare (List.length goals1) (List.length goals2)) (aux uris) -let elim ~dbd uri = - let constraints = - [`Rel [`MainConclusion None]; - `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]); - `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); - `Obj (uri,[`InHypothesis]); - ] - in - MetadataConstraints.at_least ~rating:`Hits ~dbd constraints - - -let fill_with_dummy_constants t = - let rec aux i types = - function - Cic.Lambda (n,s,t) -> - let dummy_uri = - UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in - (aux (i+1) (s::types) - (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) - | t -> t,types - in - let t,types = aux 0 [] t in - t, List.rev types - -let instance ~dbd t = - let t',types = fill_with_dummy_constants t in - let metadata = MetadataExtractor.compute ~body:None ~ty:t' in -(* List.iter - (fun x -> - debug_print - (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) - metadata; *) - let no_concl = MetadataDb.count_distinct `Conclusion metadata in - let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in - let no_full = MetadataDb.count_distinct `Statement metadata in - let is_dummy = function - | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy" - | _ -> true - in - let rec look_for_dummy_main = function - | [] -> None - | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ - when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> - let s = UriManager.string_of_uri s in - let len = String.length s in - let dummy_index = int_of_string (String.sub s 11 (len-15)) in - let dummy_type = List.nth types dummy_index in - Some (d,dummy_type) - | _::l -> look_for_dummy_main l - in - match (look_for_dummy_main metadata) with - | None-> -(* debug_print (lazy "Caso None"); *) - (* no dummy in main position *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints - | Some (depth, dummy_type) -> -(* debug_print - (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *) - (* a dummy in main position *) - let metadata_for_dummy_type = - MetadataExtractor.compute ~body:None ~ty:dummy_type in - (* Let us skip this for the moment - let main_of_dummy_type = - look_for_dummy_main metadata_for_dummy_type in *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let metadata_for_dummy_type = - List.filter is_dummy metadata_for_dummy_type in - let metadata_for_dummy_type, depth' = - (* depth' = the depth of the A -> A -> Prop *) - List.fold_left (fun (acc,dep) c -> - match c with - | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> - (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i - | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type - in - let constraints_for_dummy_type = - List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in - (* start with the dummy constant in main conlusion *) - let from = ["refObj as table0"] in - let where = - [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; - sprintf "table0.h_depth >= %d" depth] in - let (n,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:2) - (2,from,where) constraints in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - let (n,from,where) = - MetadataConstraints.add_all_constr - (n,from,where) concl_card full_card diff in - (* join with the constraints over the type of the constant *) - let where = - (sprintf "table0.h_occurrence = table%d.source" n)::where in - let where = - sprintf "table0.h_depth - table%d.h_depth = %d" - n (depth - depth')::where - in - let (m,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:n) - (n,from,where) constraints_for_dummy_type in - Constr.exec ~dbd (m,from,where) - -(* fwd_simpl ****************************************************************) - -let rec map_filter f n = function - | [] -> [] - | hd :: tl -> - match f n hd with - | None -> map_filter f (succ n) tl - | Some hd -> hd :: map_filter f (succ n) tl - -let get_uri t = - let aux = function - | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl) - | hd -> Some (CicUtil.uri_of_term hd, []) - in - try aux t with - | Invalid_argument "uri_of_term" -> None - -let get_metadata t = - let f n t = - match get_uri t with - | None -> None - | Some (uri, _) -> Some (n, uri) - in - match get_uri t with - | None -> None - | Some (uri, args) -> Some (uri, map_filter f 1 args) - -let debug_metadata = function - | None -> () - | Some (outer, inners) -> - let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in - Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer); - List.iter f inners; prerr_newline () - -let fwd_simpl ~dbd t = - let map inners row = - match row.(0), row.(1), row.(2) with - | Some source, Some inner, Some index -> - source, - List.mem - (int_of_string index, (UriManager.uri_of_string inner)) inners - | _ -> "", false - in - let rec rank ranks (source, ok) = - match ranks, ok with - | [], false -> [source, 0] - | [], true -> [source, 1] - | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl - | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl - | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl - | hd :: tl, _ -> hd :: rank tl (source, ok) - in - let compare (_, x) (_, y) = compare x y in - let filter n (uri, rank) = - if rank > 0 then Some (UriManager.uri_of_string uri) else None - in - let metadata = get_metadata t in debug_metadata metadata; - match metadata with - | None -> [] - | Some (outer, inners) -> - let select = "source, h_inner, h_index" in - let from = "genLemma" in - let where = - Printf.sprintf "h_outer = \"%s\"" - (HMysql.escape (UriManager.string_of_uri outer)) in - let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in - let result = HMysql.exec dbd query in - let lemmas = HMysql.map ~f:(map inners) result in - let ranked = List.fold_left rank [] lemmas in - let ordered = List.rev (List.fast_sort compare ranked) in - map_filter filter 0 ordered - -(* get_decomposables ********************************************************) - -let decomposables ~dbd = - let map row = match row.(0) with - | None -> None - | Some str -> - match CicUtil.term_of_uri (UriManager.uri_of_string str) with - | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno) - | _ -> - raise (UriManager.IllFormedUri str) - in - let select, from = "source", "decomposables" in - let query = Printf.sprintf "SELECT %s FROM %s" select from in - let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in - map_filter (fun _ x -> x) 0 decomposables diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli index 747844226..b65a23fa9 100644 --- a/helm/ocaml/tactics/metadataQuery.mli +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -34,10 +34,6 @@ val signature_of_goal: val equations_for_goal: dbd:HMysql.dbd -> ProofEngineTypes.status -> UriManager.uri list -val locate: - dbd:HMysql.dbd -> - ?vars:bool -> string -> UriManager.uri list - val experimental_hint: dbd:HMysql.dbd -> ?facts:bool -> @@ -57,13 +53,3 @@ val new_experimental_hint: ((Cic.term -> Cic.term) * (ProofEngineTypes.proof * ProofEngineTypes.goal list))) list -val match_term: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list - - (** @param string is an uri *) -val elim: dbd:HMysql.dbd -> UriManager.uri -> UriManager.uri list - -val instance: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list - -val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list - -val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int) list diff --git a/helm/ocaml/whelp/.cvsignore b/helm/ocaml/whelp/.cvsignore new file mode 100644 index 000000000..780c0115b --- /dev/null +++ b/helm/ocaml/whelp/.cvsignore @@ -0,0 +1,7 @@ +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.o diff --git a/helm/ocaml/whelp/.depend b/helm/ocaml/whelp/.depend new file mode 100644 index 000000000..39f37dfa9 --- /dev/null +++ b/helm/ocaml/whelp/.depend @@ -0,0 +1,4 @@ +whelp.cmo: whelp.cmi +whelp.cmx: whelp.cmi +fwdQueries.cmo: fwdQueries.cmi +fwdQueries.cmx: fwdQueries.cmi diff --git a/helm/ocaml/whelp/Makefile b/helm/ocaml/whelp/Makefile new file mode 100644 index 000000000..f43c77fa9 --- /dev/null +++ b/helm/ocaml/whelp/Makefile @@ -0,0 +1,10 @@ +PACKAGE = whelp + +INTERFACE_FILES = \ + whelp.mli \ + fwdQueries.mli \ + $(NULL) + +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +include ../Makefile.common diff --git a/helm/ocaml/whelp/fwdQueries.ml b/helm/ocaml/whelp/fwdQueries.ml new file mode 100644 index 000000000..4e056b6b0 --- /dev/null +++ b/helm/ocaml/whelp/fwdQueries.ml @@ -0,0 +1,113 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +(* fwd_simpl ****************************************************************) + +let rec filter_map_n f n = function + | [] -> [] + | hd :: tl -> + match f n hd with + | None -> filter_map_n f (succ n) tl + | Some hd -> hd :: filter_map_n f (succ n) tl + +let get_uri t = + let aux = function + | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl) + | hd -> Some (CicUtil.uri_of_term hd, []) + in + try aux t with + | Invalid_argument "uri_of_term" -> None + +let get_metadata t = + let f n t = + match get_uri t with + | None -> None + | Some (uri, _) -> Some (n, uri) + in + match get_uri t with + | None -> None + | Some (uri, args) -> Some (uri, filter_map_n f 1 args) + +let debug_metadata = function + | None -> () + | Some (outer, inners) -> + let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in + Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer); + List.iter f inners; prerr_newline () + +let fwd_simpl ~dbd t = + let map inners row = + match row.(0), row.(1), row.(2) with + | Some source, Some inner, Some index -> + source, + List.mem + (int_of_string index, (UriManager.uri_of_string inner)) inners + | _ -> "", false + in + let rec rank ranks (source, ok) = + match ranks, ok with + | [], false -> [source, 0] + | [], true -> [source, 1] + | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl + | (uri, 0) :: tl, true when uri = source -> (uri, 0) :: tl + | (uri, i) :: tl, true when uri = source -> (uri, succ i) :: tl + | hd :: tl, _ -> hd :: rank tl (source, ok) + in + let compare (_, x) (_, y) = compare x y in + let filter n (uri, rank) = + if rank > 0 then Some (UriManager.uri_of_string uri) else None + in + let metadata = get_metadata t in debug_metadata metadata; + match metadata with + | None -> [] + | Some (outer, inners) -> + let select = "source, h_inner, h_index" in + let from = "genLemma" in + let where = + Printf.sprintf "h_outer = \"%s\"" + (HMysql.escape (UriManager.string_of_uri outer)) in + let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in + let result = HMysql.exec dbd query in + let lemmas = HMysql.map ~f:(map inners) result in + let ranked = List.fold_left rank [] lemmas in + let ordered = List.rev (List.fast_sort compare ranked) in + filter_map_n filter 0 ordered + +(* get_decomposables ********************************************************) + +let decomposables ~dbd = + let map row = match row.(0) with + | None -> None + | Some str -> + match CicUtil.term_of_uri (UriManager.uri_of_string str) with + | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno) + | _ -> + raise (UriManager.IllFormedUri str) + in + let select, from = "source", "decomposables" in + let query = Printf.sprintf "SELECT %s FROM %s" select from in + let decomposables = HMysql.map ~f:map (HMysql.exec dbd query) in + filter_map_n (fun _ x -> x) 0 decomposables + diff --git a/helm/ocaml/whelp/fwdQueries.mli b/helm/ocaml/whelp/fwdQueries.mli new file mode 100644 index 000000000..7f580a541 --- /dev/null +++ b/helm/ocaml/whelp/fwdQueries.mli @@ -0,0 +1,28 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +val fwd_simpl: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list +val decomposables: dbd:HMysql.dbd -> (UriManager.uri * int) list + diff --git a/helm/ocaml/whelp/whelp.ml b/helm/ocaml/whelp/whelp.ml new file mode 100644 index 000000000..d670b4372 --- /dev/null +++ b/helm/ocaml/whelp/whelp.ml @@ -0,0 +1,213 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +open Printf + +let nonvar uri = not (UriManager.uri_is_var uri) + + (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for + * the "like" operator (which uses '%' and '_'). Does not support escaping. *) +let sqlpat_of_shellglob = + let star_RE, qmark_RE, percent_RE, uscore_RE = + Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_" + in + fun shellglob -> + Pcre.replace ~rex:star_RE ~templ:"%" + (Pcre.replace ~rex:qmark_RE ~templ:"_" + (Pcre.replace ~rex:percent_RE ~templ:"\\%" + (Pcre.replace ~rex:uscore_RE ~templ:"\\_" + shellglob))) + +let locate ~(dbd:HMysql.dbd) ?(vars = false) pat = + let sql_pat = sqlpat_of_shellglob pat in + let query = + sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^ + "SELECT source FROM %s WHERE value LIKE \"%s\"") + (MetadataTypes.name_tbl ()) sql_pat + MetadataTypes.library_name_tbl sql_pat + in + let result = HMysql.exec dbd query in + List.filter nonvar + (HMysql.map result + (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)) + +let match_term ~(dbd:HMysql.dbd) ty = +(* debug_print (lazy (CicPp.ppterm ty)); *) + let metadata = MetadataExtractor.compute ~body:None ~ty in + let constants_no = + MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty) + in + let full_card, diff = + if CicUtil.is_meta_closed ty then + Some (MetadataConstraints.Eq constants_no), None + else + let diff_no = + let (hyp_constants, concl_constants) = + (* collect different constants in hypotheses and conclusions *) + List.fold_left + (fun ((hyp, concl) as acc) metadata -> + match (metadata: MetadataTypes.metadata) with + | `Sort _ | `Rel _ -> acc + | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) + when not (List.mem uri concl) -> (hyp, uri :: concl) + | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) + when not (List.mem uri hyp) -> (uri :: hyp, concl) + | `Obj _ -> acc) + ([], []) + metadata + in + List.length hyp_constants - List.length concl_constants + in + let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in + let diff = + if MetadataExtractor.IntSet.equal concl_metas hyp_metas then + Some (MetadataConstraints.Eq diff_no) + else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then + Some (MetadataConstraints.Gt (diff_no - 1)) + else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then + Some (MetadataConstraints.Lt (diff_no + 1)) + else + None + in + None, diff + in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + MetadataConstraints.at_least ~dbd ?full_card ?diff constraints + +let fill_with_dummy_constants t = + let rec aux i types = + function + Cic.Lambda (n,s,t) -> + let dummy_uri = + UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in + (aux (i+1) (s::types) + (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t)) + | t -> t,types + in + let t,types = aux 0 [] t in + t, List.rev types + +let instance ~dbd t = + let t',types = fill_with_dummy_constants t in + let metadata = MetadataExtractor.compute ~body:None ~ty:t' in +(* List.iter + (fun x -> + debug_print + (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x)))) + metadata; *) + let no_concl = MetadataDb.count_distinct `Conclusion metadata in + let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in + let no_full = MetadataDb.count_distinct `Statement metadata in + let is_dummy = function + | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy" + | _ -> true + in + let rec look_for_dummy_main = function + | [] -> None + | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ + when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> + let s = UriManager.string_of_uri s in + let len = String.length s in + let dummy_index = int_of_string (String.sub s 11 (len-15)) in + let dummy_type = List.nth types dummy_index in + Some (d,dummy_type) + | _::l -> look_for_dummy_main l + in + match (look_for_dummy_main metadata) with + | None-> +(* debug_print (lazy "Caso None"); *) + (* no dummy in main position *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff + constraints + | Some (depth, dummy_type) -> +(* debug_print + (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *) + (* a dummy in main position *) + let metadata_for_dummy_type = + MetadataExtractor.compute ~body:None ~ty:dummy_type in + (* Let us skip this for the moment + let main_of_dummy_type = + look_for_dummy_main metadata_for_dummy_type in *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let metadata_for_dummy_type = + List.filter is_dummy metadata_for_dummy_type in + let metadata_for_dummy_type, depth' = + (* depth' = the depth of the A -> A -> Prop *) + List.fold_left (fun (acc,dep) c -> + match c with + | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type + in + let constraints_for_dummy_type = + List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in + (* start with the dummy constant in main conlusion *) + let from = ["refObj as table0"] in + let where = + [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; + sprintf "table0.h_depth >= %d" depth] in + let (n,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:2) + (2,from,where) constraints in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + let (n,from,where) = + MetadataConstraints.add_all_constr + (n,from,where) concl_card full_card diff in + (* join with the constraints over the type of the constant *) + let where = + (sprintf "table0.h_occurrence = table%d.source" n)::where in + let where = + sprintf "table0.h_depth - table%d.h_depth = %d" + n (depth - depth')::where + in + let (m,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:n) + (n,from,where) constraints_for_dummy_type in + MetadataConstraints.exec ~dbd (m,from,where) + +let elim ~dbd uri = + let constraints = + [`Rel [`MainConclusion None]; + `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]); + `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); + `Obj (uri,[`InHypothesis]); + ] + in + MetadataConstraints.at_least ~rating:`Hits ~dbd constraints + diff --git a/helm/ocaml/whelp/whelp.mli b/helm/ocaml/whelp/whelp.mli new file mode 100644 index 000000000..9ff03ea20 --- /dev/null +++ b/helm/ocaml/whelp/whelp.mli @@ -0,0 +1,30 @@ +(* Copyright (C) 2005, 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://helm.cs.unibo.it/ + *) + +val locate: dbd:HMysql.dbd -> ?vars:bool -> string -> UriManager.uri list +val elim: dbd:HMysql.dbd -> UriManager.uri -> UriManager.uri list +val instance: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list +val match_term: dbd:HMysql.dbd -> Cic.term -> UriManager.uri list + -- 2.39.2