From 2208a75027ccad441dc0778101f57eff9555f8ea Mon Sep 17 00:00:00 2001 From: natile Date: Fri, 29 Nov 2002 18:47:41 +0000 Subject: [PATCH] Now MQueryGenerator generates the query and MQueryLevels produces the restrictions (must and can). --- helm/gTopLevel/.depend | 10 ++++++---- helm/gTopLevel/gTopLevel.ml | 13 ++++++++----- helm/gTopLevel/mQueryGenerator.ml | 22 ++++++++++++---------- helm/gTopLevel/mQueryGenerator.mli | 2 +- helm/gTopLevel/mQueryLevels.ml | 29 +++++++++++++++++++++++++++++ helm/gTopLevel/mQueryLevels.mli | 8 +++++++- helm/gTopLevel/topLevel/topLevel.ml | 5 ++++- 7 files changed, 67 insertions(+), 22 deletions(-) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 7dce2d61f..fa76e97ae 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -61,9 +61,11 @@ sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi mQueryLevels.cmo: mQueryLevels.cmi mQueryLevels.cmx: mQueryLevels.cmi -mQueryGenerator.cmo: mQueryGenerator.cmi -mQueryGenerator.cmx: mQueryGenerator.cmi +mQueryGenerator.cmo: mQueryLevels.cmi mQueryGenerator.cmi +mQueryGenerator.cmx: mQueryLevels.cmx mQueryGenerator.cmi gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \ - mQueryGenerator.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi + mQueryGenerator.cmi mQueryLevels.cmi proofEngine.cmi sequentPp.cmi \ + xml2Gdome.cmi gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \ - mQueryGenerator.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx + mQueryGenerator.cmx mQueryLevels.cmx proofEngine.cmx sequentPp.cmx \ + xml2Gdome.cmx diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 0546d02b5..5ad73d2be 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -65,8 +65,8 @@ let prooffile = "/home/tassi/miohelm/tmp/currentproof";; let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; *) -let prooffile = "/public/sacerdot/currentproof";; -let prooffiletype = "/public/sacerdot/currentprooftype";; +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) @@ -75,8 +75,8 @@ let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; *) -let innertypesfile = "/public/sacerdot/innertypes";; -let constanttypefile = "/public/sacerdot/constanttype";; +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; let empty_id_to_uris = ([],function _ -> None);; @@ -2008,7 +2008,10 @@ let searchPattern () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let result = MQueryGenerator.searchPattern metasenv ey ty level in + let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in + let len = List.length list_of_must in + let must = if level < len then List.nth list_of_must level else can in + let result = MQueryGenerator.searchPattern metasenv ey ty must can in let uris = List.map (function uri,_ -> diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index 843eb96c0..c925e27a6 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -96,7 +96,7 @@ let locate s = in execute_query q -let searchPattern e c t level = +let searchPattern e c t must_use can_use = let module M = MathQL in let module L = MQueryLevels in let mainConclusion = @@ -121,14 +121,15 @@ let searchPattern e c t level = ), M.VVar "universe" ) in - let uri_of_entry (r, b, v) = r in - let rec restrict level = function + let uri_of_entry (r, b) = r in + (*let rec restrict level = function | [] -> [] | (u, b, v) :: tail -> if v <= level then (u, b, v) :: restrict level tail else restrict level tail - in - let build_select (r, b, v) = + in*) + let build_select (r, b) = + print_endline (">>>>LA URI: "^r); let pos = if b then mainConclusion else inConclusion in M.Select ("uri", @@ -140,13 +141,14 @@ let searchPattern e c t level = | [hd] -> build_select hd | hd :: tl -> M.Intersect (build_select hd, build_intersect tl) in - let levels = L.levels_of_term e c t in + + (* let levels = L.levels_of_term e c t in let rest = restrict level levels in - info := [string_of_int (List.length rest)]; - let q_in = build_intersect rest in + info := [string_of_int (List.length rest)];*) + let q_in = build_intersect must_use in let q_select = M.Select ("uri0", q_in, q_where) in - let universe = M.Const (List.map uri_of_entry levels) in + let universe = M.Const (List.map uri_of_entry can_use) in let q_let_u = M.LetVVar ("universe", universe, q_select) in let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in -prerr_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ; +print_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ; flush stdout; execute_query q_let_p diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli index 68c2ea257..8723f9c9f 100644 --- a/helm/gTopLevel/mQueryGenerator.mli +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -44,6 +44,6 @@ val execute_query : MathQL.query -> MathQL.result val locate : string -> MathQL.result -val searchPattern : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result +val searchPattern : Cic.metasenv -> Cic.context -> Cic.term -> (string * bool) list -> (string * bool) list -> MathQL.result val get_query_info : unit -> string list diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml index f50d94c2c..ecadbd84b 100644 --- a/helm/gTopLevel/mQueryLevels.ml +++ b/helm/gTopLevel/mQueryLevels.ml @@ -141,3 +141,32 @@ let string_of_levels l sep = in levels_out l + +let out_restr e c t = +(* let rec restrict level = function + | [] -> [] + | (u, b, v) :: tail -> + if v <= level then (u, b, v) :: restrict level tail + else restrict level tail + in*) + + let can = levels_of_term e c t in (* can restrictions *) +print_endline ""; + print_string "#### IN LEVELS @@@@ lunghezza can:"; + print_int (List.length can); flush stdout; + print_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/gTopLevel/mQueryLevels.mli b/helm/gTopLevel/mQueryLevels.mli index bc1dc7414..82fb7c699 100644 --- a/helm/gTopLevel/mQueryLevels.mli +++ b/helm/gTopLevel/mQueryLevels.mli @@ -33,8 +33,14 @@ (* *) (******************************************************************************) +(*type can_restrictions = (string * bool) list + +type must_restrictions = ((string * bool) list) list*) + type levels_spec = (string * bool * int) list -val levels_of_term : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec +val levels_of_term: Cic.metasenv -> Cic.context -> Cic.term -> levels_spec + +val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list) val string_of_levels : levels_spec -> string -> string diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index 4825c5b36..cb7c7fca1 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -120,7 +120,10 @@ let mbackward n m l = if Mqint.get_stat () then print_string ("? " ^ CicPp.ppterm term ^ nl); let t0 = Sys.time () in - let r = Gen.searchPattern [] [] term level in + let list_of_must,can = MQueryLevels.out_restr [] [] term in + let len = List.length list_of_must in + let must = if level < len then List.nth list_of_must level else can in + let r = Gen.searchPattern [] [] term must can in let t1 = Sys.time () -. t0 in let info = Gen.get_query_info () in let num = List.nth info 0 in -- 2.39.2