From 96134b9ec1030ed15cea00d751dd4d744463f62c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 17 Jul 2003 12:30:26 +0000 Subject: [PATCH] - 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 --- helm/gTopLevel/Makefile | 2 +- helm/gTopLevel/gTopLevel.ml | 10 +-- helm/mathql_test/mqgtop.ml | 25 ++++--- helm/ocaml/mathql_generator/.depend | 11 +-- helm/ocaml/mathql_generator/Makefile | 2 +- .../{mQueryLevels.ml => cGMatchConclusion.ml} | 74 +++++++++++++------ ...mQueryLevels.mli => cGMatchConclusion.mli} | 4 +- .../{mQueryLevels2.ml => cGSearchPattern.ml} | 0 ...{mQueryLevels2.mli => cGSearchPattern.mli} | 0 .../ocaml/mathql_generator/mQueryGenerator.ml | 16 +++- .../mathql_generator/mQueryGenerator.mli | 6 +- helm/ocaml/tactics/tacticChaser.ml | 9 +-- helm/ocaml/tactics/tacticChaser.mli | 7 +- helm/searchEngine/searchEngine.ml | 10 ++- 14 files changed, 113 insertions(+), 63 deletions(-) rename helm/ocaml/mathql_generator/{mQueryLevels.ml => cGMatchConclusion.ml} (68%) rename helm/ocaml/mathql_generator/{mQueryLevels.mli => cGMatchConclusion.mli} (88%) rename helm/ocaml/mathql_generator/{mQueryLevels2.ml => cGSearchPattern.ml} (100%) rename helm/ocaml/mathql_generator/{mQueryLevels2.mli => cGSearchPattern.mli} (100%) 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/mQueryLevels.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml similarity index 68% rename from helm/ocaml/mathql_generator/mQueryLevels.ml rename to helm/ocaml/mathql_generator/cGMatchConclusion.ml index d10f5d659..9f1f64512 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels.ml +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml @@ -26,6 +26,18 @@ (* 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 @@ -59,35 +71,35 @@ let levels_of_term metasenv context term = | 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 + 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' (v+1) exp_named_subst + 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' (v+1) exp_named_subst + 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' (v+1) exp_named_subst + 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 (v + 1) uu in - inspect_term main luu (v + 1) 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 (v + 1) uu in - inspect_term false luu (v + 1) 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 (v + 1) uu in - inspect_term false luu (v + 1) 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] (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 + 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 -> @@ -119,13 +131,27 @@ let levels_of_term metasenv context term = 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 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 @@ -138,4 +164,4 @@ prerr_endline ""; 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/cGMatchConclusion.mli similarity index 88% rename from helm/ocaml/mathql_generator/mQueryLevels.mli rename to helm/ocaml/mathql_generator/cGMatchConclusion.mli index c16d12bc1..a8340312f 100644 --- a/helm/ocaml/mathql_generator/mQueryLevels.mli +++ b/helm/ocaml/mathql_generator/cGMatchConclusion.mli @@ -26,4 +26,6 @@ (* AUTOR: Ferruccio Guidi *) -val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list) +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/mQueryLevels2.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml similarity index 100% rename from helm/ocaml/mathql_generator/mQueryLevels2.ml rename to helm/ocaml/mathql_generator/cGSearchPattern.ml diff --git a/helm/ocaml/mathql_generator/mQueryLevels2.mli b/helm/ocaml/mathql_generator/cGSearchPattern.mli similarity index 100% rename from helm/ocaml/mathql_generator/mQueryLevels2.mli rename to helm/ocaml/mathql_generator/cGSearchPattern.mli 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/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 -- 2.39.2