From 503d873ce22e1dd6bfda44c85322d4ee5a792a98 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 20 Oct 2004 10:31:37 +0000 Subject: [PATCH] top level query module --- helm/ocaml/tactics/metadataQuery.ml | 103 +++++++++++++++++++++++++++ helm/ocaml/tactics/metadataQuery.mli | 37 ++++++++++ 2 files changed, 140 insertions(+) create mode 100644 helm/ocaml/tactics/metadataQuery.ml create mode 100644 helm/ocaml/tactics/metadataQuery.mli diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml new file mode 100644 index 000000000..18ea81381 --- /dev/null +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -0,0 +1,103 @@ +(* Copyright (C) 2004, 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 + +module Constr = MetadataConstraints + +let locate ~(dbh:Dbi.connection) name = + let query = + dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\"" + MetadataTypes.name_tbl name) + in + query#execute []; + List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ()) + +let match_term ~(dbh:Dbi.connection) ty = + let metadata = MetadataExtractor.compute ~body:None ~ty in + Constr.at_least ~dbh metadata + +let nonvar (_, s) = + let len = String.length s in + let suffix = String.sub s (len-4) 4 in + not (suffix = ".var") + +let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) + +let signature_of_hypothesis context = + List.fold_left + (fun set hyp -> + match hyp with + | None -> set + | Some (_, Cic.Decl t) + | Some (_, Cic.Def (t, _)) -> + Constr.StringSet.union set (Constr.constants_of t)) + Constr.StringSet.empty context + +let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) = + let (_, metasenv, _, _) = proof in + let (_, context, ty) = CicUtil.lookup_meta goal metasenv in + let (uris, (main, sig_constants)) = + match signature with + | Some signature -> (Constr.sigmatch ~dbh signature, signature) + | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty) + in + let uris = List.filter nonvar uris in +(* + let concl_constants = + match main with + | None -> sig_constants + | Some (main, types) -> + List.fold_right Constr.StringSet.add sig_constants (main :: types) + in +*) + let types_constants = + match main with + | None -> Constr.StringSet.empty + | Some (main, types) -> + List.fold_right Constr.StringSet.add (main :: types) + Constr.StringSet.empty + in + let hyp_constants = + Constr.StringSet.diff (signature_of_hypothesis context) types_constants + in + let other_constants = Constr.StringSet.union sig_constants hyp_constants in + let uris = + if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants)) + then begin + prerr_endline + "MetadataQuery: large signature, falling back to old method"; + List.filter (Filter_auto.filter_new_constants ~dbh all_constants main) + uris + end else + Filter_auto.filter_uris ~dbh all_constants uris main + in + List.map + (fun uri -> + (uri, + ProofEngineTypes.apply_tactic + (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri)) + status)) + diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli new file mode 100644 index 000000000..6bea094a4 --- /dev/null +++ b/helm/ocaml/tactics/metadataQuery.mli @@ -0,0 +1,37 @@ +(* Copyright (C) 2004, 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: dbh:Dbi.connection -> string -> string list + +val hint: + dbh:Dbi.connection -> + ?signature:MetadataConstraints.term_signature -> + ProofEngineTypes.status -> + (string * (ProofEngineTypes.proof * ProofEngineTypes.goal list)) list + +val match_term: dbh:Dbi.connection -> Cic.term -> string list + +(* val elim: dbh:Dbi.connection -> string -> string list *) + -- 2.39.2