From: Ferruccio Guidi Date: Thu, 17 Jul 2003 12:30:26 +0000 (+0000) Subject: - new generated query "unreferred" implemented at server side X-Git-Tag: LucaOK~66 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=96134b9ec1030ed15cea00d751dd4d744463f62c - new generated query "unreferred" implemented at server side - fixed some aspects of the constraint generator for "matchConclusion" - fixed a bug that prevented to "make opt" in ocaml/gTopLevel --- diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 6dfa38622..e44967305 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -26,7 +26,7 @@ DEPOBJS = \ gTopLevel.ml TOPLEVELOBJS = \ - doubleTypeInference.cmo eta_fixing.cmo content2cic.cmo \ + eta_fixing.cmo content2cic.cmo \ proofEngine.cmo logicalOperations.cmo \ disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \ invokeTactics.cmo hbugs.cmo gTopLevel.cmo diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 0aefe5393..189f17d3c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1915,7 +1915,7 @@ let completeSearchPattern () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in - let must = MQueryLevels2.get_constraints expr in + let must = CGSearchPattern.get_constraints expr in let must',only = refine_constraints must in let query = MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only @@ -2042,10 +2042,10 @@ let choose_must list_of_must only = in ignore (List.map - (function (uri,position) -> + (function (position, uri) -> let n = clist#append - [uri; if position then "MainConclusion" else "Conclusion"] + [uri; MQGUtil.text_of_position position] in clist#set_row ~selectable:false n ) must @@ -2074,10 +2074,10 @@ let choose_must list_of_must only = in ignore (List.map - (function (uri,position) -> + (function (position, uri) -> let n = clist#append - [uri; if position then "MainConclusion" else "Conclusion"] + [uri; MQGUtil.text_of_position position] in clist#set_row ~selectable:true n ) only diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index 9a7c8d9db..2bf4e5f82 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -46,8 +46,8 @@ module L = MQGTopLexer module P = MQGTopParser module TL = CicTextualLexer module TP = CicTextualParser -module C2 = MQueryLevels2 -module C1 = MQueryLevels +module C2 = CGSearchPattern +module C1 = CGMatchConclusion module GU = MQGUtil let get_handle () = @@ -156,6 +156,11 @@ let locate name = issue handle (G.locate name); C.close handle +let unreferred target source = + let handle = get_handle () in + issue handle (G.unreferred target source); + C.close handle + let mpattern n m l = let queries = ref [] in let univ = Some GU.universe_for_search_pattern in @@ -193,9 +198,6 @@ let mpattern n m l = 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 @@ -204,12 +206,10 @@ let mbackward n m l = 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 list_of_must, only = C1.get_constraints [] [] 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 + let q = G.query_of_constraints univ (must, [], []) (Some only , None, None) in if not (List.mem q ! queries) then begin issue handle q; @@ -261,7 +261,8 @@ let prerr_help () = 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 " on all CIC terms in the input file"; + prerr_endline "-U T_PATTERN S_PATTERN issues the \"Unreferred\" query for the given patterns\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"; @@ -280,13 +281,15 @@ let rec parse = function | ("-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 -> + | ("-B"|"-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 + | ("-U"|"-unreferred") :: arg1 :: arg2 :: rem -> + unreferred arg1 arg2; parse rem | _ :: rem -> parse rem let _ = diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index b8ecb1367..b3e8556fb 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -1,11 +1,12 @@ mQGUtil.cmi: mQGTypes.cmo mQueryGenerator.cmi: mQGTypes.cmo -mQueryLevels2.cmi: mQGTypes.cmo +cGMatchConclusion.cmi: mQGTypes.cmo +cGSearchPattern.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: mQGTypes.cmo mQGUtil.cmi mQueryLevels2.cmi -mQueryLevels2.cmx: mQGTypes.cmx mQGUtil.cmx mQueryLevels2.cmi +cGMatchConclusion.cmo: cGMatchConclusion.cmi +cGMatchConclusion.cmx: cGMatchConclusion.cmi +cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi +cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi diff --git a/helm/ocaml/mathql_generator/Makefile b/helm/ocaml/mathql_generator/Makefile index 6b8252c20..5b0135a3d 100644 --- a/helm/ocaml/mathql_generator/Makefile +++ b/helm/ocaml/mathql_generator/Makefile @@ -5,7 +5,7 @@ REQUIRES = helm-cic helm-cic_proof_checking helm-mathql PREDICATES = INTERFACE_FILES = mQGUtil.mli mQueryGenerator.mli \ - mQueryLevels.mli mQueryLevels2.mli + cGMatchConclusion.mli cGSearchPattern.mli IMPLEMENTATION_FILES = mQGTypes.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml new file mode 100644 index 000000000..9f1f64512 --- /dev/null +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -0,0 +1,167 @@ +(* 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 text_of_entries out entries = + out "(** MatchConclusion: results of the term inspection **)\n"; + let text_of_entry (u, b, v) = + out (string_of_int v ^ " "); + out (if b then "$MC " else "$IC "); + out (u ^ "\n") + in List.iter text_of_entry entries + +let sort_entries entries = + let comparator (_, _, v1) (_, _, v2) = compare v1 v2 in + List.fast_sort comparator entries + +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' (succ v) exp_named_subst + | Cic.Const (u,exp_named_subst) -> + let l' = inspect_uri main l u [] v term in + inspect_exp_named_subst l' (succ v) 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' (succ v) 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' (succ v) exp_named_subst + | Cic.Cast (uu, _) -> + inspect_term main l v uu + | Cic.Prod (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term main luu (succ v) tt + | Cic.Lambda (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term false luu (succ v) tt + | Cic.LetIn (_, uu, tt) -> + let luu = inspect_term false l (succ v) uu in + inspect_term false luu (succ v) 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] (succ v) term in + let ltt = inspect_term false lu (succ v) tt in + let luu = inspect_term false ltt (succ v) uu in + inspect_list main luu false (succ v) m + | Cic.Fix (_, m) -> inspect_ind l (succ v) m + | Cic.CoFix (_, m) -> inspect_coind l (succ v) 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 get_constraints e c t = + let can = sort_entries (levels_of_term e c t) in (* can restrictions *) + text_of_entries prerr_string can; flush stderr; (* logging *) + let rest_of (u, b, _) = + let p = if b then `MainConclusion None else `InConclusion in (p, u) + in + let rec split vp = function + | [], ((_, _, v) as hd) :: tl -> split v ([rest_of hd], tl) + | prev, ((_, _, ve) as hd) :: tl when vp = ve -> + split vp (rest_of hd :: prev, tl) + | p, l -> p, l + in + let rec mk_musts prev acc = function + | [] -> prev, acc + | l -> + let slice, next = split 0 ([], l) in + let acc = acc @ slice in + mk_musts (prev @ [acc]) acc next + in + mk_musts [] [] can +(* + 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/mathql_generator/cGMatchConclusion.mli b/helm/ocaml/mathql_generator/cGMatchConclusion.mli new file mode 100644 index 000000000..a8340312f --- /dev/null +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.mli @@ -0,0 +1,31 @@ +(* 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 + *) + +val get_constraints: Cic.metasenv -> Cic.context -> Cic.term -> + MQGTypes.r_obj list list * + MQGTypes.r_obj list diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml new file mode 100644 index 000000000..60633f897 --- /dev/null +++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml @@ -0,0 +1,189 @@ +(* 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 *) +(* *) +(******************************************************************************) + +module T = MQGTypes +module U = MQGUtil + +type classification = + Backbone of int + | Branch of int + | InConclusion + | InHypothesis +;; + +let soften_classification = + function + Backbone _ -> InConclusion + | Branch _ -> InHypothesis + | k -> k +;; + +let (!!) = + function + 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 + 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) -> + ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ + (process_type_aux_expl_named_subst kind expl_named_subst) + | C.Rel _ -> + (match kind with + | InConclusion + | InHypothesis -> [],[],[] + | _ -> [],[!!kind],[]) + | C.Sort s -> + (match kind with + Backbone _ + | Branch _ -> + let s' = + match s with + Cic.Prop -> T.Prop + | Cic.Set -> T.Set + | Cic.Type -> T.Type + in + [],[],[!!kind,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,_) -> + [!!!kind, UriManager.string_of_uri uri],[],[] + | C.MutInd (uri,typeno,expl_named_subst) -> + ([!!!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) -> + ([!!!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 + 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 + 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 (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ; + prerr_endline "Constraints on Rels:" ; + List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ; + prerr_endline "Constraints on Sorts:" ; + List.iter + (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/cGSearchPattern.mli b/helm/ocaml/mathql_generator/cGSearchPattern.mli new file mode 100644 index 000000000..83f681414 --- /dev/null +++ b/helm/ocaml/mathql_generator/cGSearchPattern.mli @@ -0,0 +1,37 @@ +(* 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 *) +(* *) +(******************************************************************************) + +val get_constraints: Cic.term -> MQGTypes.must_restrictions diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 1a0211102..40c0ea0b8 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -38,6 +38,19 @@ let locate s = false (M.Const s) in M.StatQuery query +let unreferred target_pattern source_pattern = + let query = + M.Bin M.BinFDiff + ( + M.Property false M.RefineExact [] [] [] [] [] + true (M.Const target_pattern) + ) ( + M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] [] + true (M.Const source_pattern) + + ) + in M.StatQuery query + let compose cl = let letin = ref [] in let must = ref [] in @@ -100,7 +113,8 @@ let compose cl = | [head] -> (f head) | head :: tail -> let t = (iter f g tail) in g (f head) t in - U.mathql_of_specs prerr_string cl; + prerr_endline "(** Compose: received constraints **)"; + U.mathql_of_specs prerr_string cl; flush stderr; aux cl; let must_query = if ! must = [] then diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.mli b/helm/ocaml/mathql_generator/mQueryGenerator.mli index c4dc0f9e5..decaa0ea7 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.mli +++ b/helm/ocaml/mathql_generator/mQueryGenerator.mli @@ -28,9 +28,11 @@ (* interface for the low-level constraints *********************************) -val locate : string -> MathQL.query +val locate : string -> MathQL.query -val compose : MQGTypes.spec list -> MathQL.query +val unreferred : string -> string -> MathQL.query + +val compose : MQGTypes.spec list -> MathQL.query (* interface for the high-level constraints ********************************) diff --git a/helm/ocaml/mathql_generator/mQueryLevels.ml b/helm/ocaml/mathql_generator/mQueryLevels.ml deleted file mode 100644 index d10f5d659..000000000 --- a/helm/ocaml/mathql_generator/mQueryLevels.ml +++ /dev/null @@ -1,141 +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 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/mathql_generator/mQueryLevels.mli b/helm/ocaml/mathql_generator/mQueryLevels.mli deleted file mode 100644 index c16d12bc1..000000000 --- a/helm/ocaml/mathql_generator/mQueryLevels.mli +++ /dev/null @@ -1,29 +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 - *) - -val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list) diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.ml b/helm/ocaml/mathql_generator/mQueryLevels2.ml deleted file mode 100644 index 60633f897..000000000 --- a/helm/ocaml/mathql_generator/mQueryLevels2.ml +++ /dev/null @@ -1,189 +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 *) -(* *) -(******************************************************************************) - -module T = MQGTypes -module U = MQGUtil - -type classification = - Backbone of int - | Branch of int - | InConclusion - | InHypothesis -;; - -let soften_classification = - function - Backbone _ -> InConclusion - | Branch _ -> InHypothesis - | k -> k -;; - -let (!!) = - function - 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 - 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) -> - ([!!!kind, UriManager.string_of_uri uri],[],[]) @@ - (process_type_aux_expl_named_subst kind expl_named_subst) - | C.Rel _ -> - (match kind with - | InConclusion - | InHypothesis -> [],[],[] - | _ -> [],[!!kind],[]) - | C.Sort s -> - (match kind with - Backbone _ - | Branch _ -> - let s' = - match s with - Cic.Prop -> T.Prop - | Cic.Set -> T.Set - | Cic.Type -> T.Type - in - [],[],[!!kind,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,_) -> - [!!!kind, UriManager.string_of_uri uri],[],[] - | C.MutInd (uri,typeno,expl_named_subst) -> - ([!!!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) -> - ([!!!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 - 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 - 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 (p, u) -> prerr_endline (text_of_pos p ^ " " ^ u)) objs ; - prerr_endline "Constraints on Rels:" ; - List.iter (function p -> prerr_endline (text_of_pos (p:>T.full_position))) rels ; - prerr_endline "Constraints on Sorts:" ; - List.iter - (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 deleted file mode 100644 index 83f681414..000000000 --- a/helm/ocaml/mathql_generator/mQueryLevels2.mli +++ /dev/null @@ -1,37 +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 *) -(* *) -(******************************************************************************) - -val get_constraints: Cic.term -> MQGTypes.must_restrictions diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index c4bfc5e03..f248735df 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -41,18 +41,13 @@ module G = MQueryGenerator 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 list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in let must = choose_must list_of_must only in - let torigth_restriction (u,b) = - (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 = I.execute mqi_handle (G.query_of_constraints (Some U.universe_for_match_conclusion) - (rigth_must,[],[]) (rigth_only,None,None)) in + (must,[],[]) (Some only,None,None)) in let uris = List.map (function uri,_ -> diff --git a/helm/ocaml/tactics/tacticChaser.mli b/helm/ocaml/tactics/tacticChaser.mli index 847dbc8b8..d54de4603 100644 --- a/helm/ocaml/tactics/tacticChaser.mli +++ b/helm/ocaml/tactics/tacticChaser.mli @@ -25,9 +25,8 @@ val matchConclusion : MQIConn.handle -> ?output_html:(string -> unit) -> - (* boolean value: true = in main position *) - choose_must:((MQGTypes.uri * bool) list list -> - (MQGTypes.uri * bool) list -> - (MQGTypes.uri * bool) list) -> + choose_must:(MQGTypes.r_obj list list -> + MQGTypes.r_obj list -> + MQGTypes.r_obj list) -> unit -> status: ProofEngineTypes.status -> string list diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index aaa5f48fa..35650c8c6 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -213,7 +213,7 @@ let get_constraints term = U.universe_for_search_pattern, (constr_obj, constr_rel, constr_sort), (None,None,None) | req_path -> - let must = MQueryLevels2.get_constraints term in + let must = CGSearchPattern.get_constraints term in refine_constraints must req_path ;; @@ -312,6 +312,14 @@ let callback (req: Http_types.request) outchan = let result = MQueryInterpreter.execute mqi_handle query in C.close mqi_handle; Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan + | "/unreferred" -> + let mqi_handle = C.init mqi_flags debug_print in + let target = req#param "target" in + let source = req#param "source" in + let query = G.unreferred target source in + let result = MQueryInterpreter.execute mqi_handle query in + C.close mqi_handle; + Http_daemon.respond ~headers:[contype] ~body:(pp_result result) outchan | "/getpage" -> (* TODO implement "is_permitted" *) (let is_permitted _ = true in