From 0b2c5757a7d7d87adc0144f790ca5294f9433175 Mon Sep 17 00:00:00 2001 From: natile Date: Mon, 21 Oct 2002 13:42:42 +0000 Subject: [PATCH] Merge of the new_mathql branch with the main branch: - new query language implemented - the locate query is now bug-free (and a _LOT_ faster) --- helm/gTopLevel/.depend | 8 +- helm/gTopLevel/gTopLevel.ml | 57 +++- helm/gTopLevel/mQueryGenerator.ml | 411 +++++++++++++--------------- helm/gTopLevel/mQueryGenerator.mli | 25 +- helm/gTopLevel/topLevel/topLevel.ml | 143 +++++++--- 5 files changed, 369 insertions(+), 275 deletions(-) diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index e1b553d30..2b88f0c85 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -22,8 +22,12 @@ ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ proofEngineTypes.cmx tacticals.cmx ring.cmi ring.cmi: proofEngineTypes.cmo -fourierR.cmo: fourier.cmo primitiveTactics.cmi tacticals.cmi fourierR.cmi -fourierR.cmx: fourier.cmx primitiveTactics.cmx tacticals.cmx fourierR.cmi +fourierR.cmo: fourier.cmo primitiveTactics.cmi proofEngineHelpers.cmi \ + proofEngineReduction.cmi proofEngineTypes.cmo ring.cmi tacticals.cmi \ + fourierR.cmi +fourierR.cmx: fourier.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ + proofEngineReduction.cmx proofEngineTypes.cmx ring.cmx tacticals.cmx \ + fourierR.cmi fourierR.cmi: proofEngineTypes.cmo proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ proofEngineReduction.cmi proofEngineStructuralRules.cmi \ diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index c980f723b..83d959ca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -33,6 +33,18 @@ (* *) (******************************************************************************) + +(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) +let wrong_xpointer_format_from_wrong_xpointer_format' uri = + try + let index_sharp = String.index uri '#' in + let index_rest = index_sharp + 10 in + let baseuri = String.sub uri 0 index_sharp in + let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in + baseuri ^ "#" ^ rest + with Not_found -> uri +;; + (* GLOBAL CONSTANTS *) let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; @@ -47,9 +59,15 @@ let htmlfooter = "" ;; +(* let prooffile = "/home/tassi/miohelm/tmp/currentproof";; +*) +let prooffile = "/public/sacerdot/currentproof";; (*CSC: the getter should handle the innertypes, not the FS *) +(* let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +*) +let innertypesfile = "/public/sacerdot/innertypes";; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -1108,6 +1126,14 @@ let user_uri_choice uris = String.sub uri 4 (String.length uri - 4) ;; +(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +let get_last_query = + let query = ref "" in + MQueryGenerator.set_confirm_query + (function q -> query := MQueryUtil.text_of_query q ; true) ; + function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" +;; + let locate rendering_window () = let inputt = (rendering_window#inputt : GEdit.text) in let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -1118,7 +1144,12 @@ let locate rendering_window () = [] -> () | head :: tail -> inputt#delete_text 0 inputlen ; - let MathQL.MQRefs uris, html = MQueryGenerator.locate head in + let result = MQueryGenerator.locate head in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in output_html outputhtml html ; let uri' = user_uri_choice uris in ignore ((inputt#insert_text uri') ~pos:0) @@ -1144,9 +1175,16 @@ let backward rendering_window () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let MathQL.MQRefs uris, html = - MQueryGenerator.backward metasenv ey ty level - in + let result = MQueryGenerator.backward metasenv ey ty level in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = + "

Backward Query:

" ^ + "

Levels:

" ^ + MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" in output_html outputhtml html ; let uri' = user_uri_choice uris in inputt#delete_text 0 inputlen ; @@ -1549,10 +1587,15 @@ let _ = CicCooking.init () ; if !usedb then begin - MQueryGenerator.init () ; + Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; CicTextualParser0.set_locate_object (function id -> - let MathQL.MQRefs uris, html = MQueryGenerator.locate id in + let result = MQueryGenerator.locate id in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = ("

Locate Query: 

" ^ get_last_query result ^ "
") in begin match !rendering_window with None -> assert false @@ -1606,5 +1649,5 @@ let _ = end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then MQueryGenerator.close (); + if !usedb then Mqint.close (); ;; diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml index eabc234aa..4deaf8c7a 100644 --- a/helm/gTopLevel/mQueryGenerator.ml +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -33,229 +33,196 @@ (* *) (******************************************************************************) -open Cic -open MathQL -open MQueryHTML -open MQueryUtil - -(* CIC term inspecting functions ********************************************) - -let env = ref [] (* metasemv *) -let cont = ref [] (* context *) - -let ie_out (r, b, v) = - let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in - res (pos ^ str_uref r) ^ nl () - (* FG: si puo' usare xp_str_uref se si vuole xpointer *) - -let rec il_out = function - | [] -> "" - | head :: tail -> ie_out head ^ il_out tail - -let rec il_max = function - | [] -> 0 - | (_, _, v) :: tail -> - let v0 = il_max tail in - if v > v0 then v else v0 - -let ie_str_uri (u, b, v) = xp_str_uref u - -let rec il_restrict level = function - | [] -> [] - | (u, b, v) :: tail -> - if v <= level then (u, b, v) :: il_restrict level tail - else il_restrict level tail - -let ie_eq ((u1, f1), b1, v1) ((u2, f2), b2, v2) = - UriManager.eq u1 u2 && f1 = f2 && b1 = b2 - -let rec ie_insert ie = function - | [] -> [ie] - | head :: tail -> - head :: if ie_eq head ie then tail else ie_insert ie tail - -let degree t = - let u0 = CicTypeChecker.type_of_aux' !env !cont t in - let u = CicReduction.whd !cont u0 in - let rec deg = function - | Sort _ -> 1 - | Cast (uu, _) -> deg uu - | Prod (_, _, tt) -> deg tt - | _ -> 2 - in deg u - -let inspect_uri main l uri tc v term = - let d = degree term in - let fi = match tc with - | t0 :: c0 :: _ -> [t0 + 1; c0] - | t0 :: _ -> [t0 + 1] - | [] -> [] - in ie_insert ((uri, fi), main, 2 * v + d - 1) l - -let rec inspect_term main l v term = - match term with - | Rel _ -> l - | Meta (_, _) -> l - | Sort _ -> l - | Implicit -> l - | Var u -> inspect_uri main l u [] v term - | Const (u, _) -> inspect_uri main l u [] v term - | MutInd (u, _, t) -> inspect_uri main l u [t] v term - | MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term - | Cast (uu, _) -> - inspect_term main l v uu - | Prod (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term main luu (v + 1) tt - | Lambda (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | LetIn (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Appl m -> inspect_list main l true v m - | 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 - | Fix (_, m) -> inspect_ind l (v + 1) m - | 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_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 - -let rec inspect_backbone = function - | Cast (uu, _) -> inspect_backbone uu - | Prod (_, _, tt) -> inspect_backbone tt - | LetIn (_, uu, tt) -> inspect_backbone tt - | t -> inspect_term true [] 0 t - -let inspect t = inspect_backbone t - -(* query building functions *************************************************) - -let issue = ref (fun _ -> true) - -let save s = - let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text] - (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in - output_string och s; flush och; s - -let build_result query = - if ! issue query then - let html = par () ^ out_query query ^ nl () in - let result = Mqint.execute query in - result, save (html ^ out_result result) - else MQRefs [], "" - -let build_select (r, b, v) n = - let rvar = "ref" ^ string_of_int n in - let svar = "str" ^ string_of_int n in - let mqs = if b then MQMConclusion else MQConclusion in - MQSelect (rvar, - MQUse (MQReference [xp_str_uref r], svar), - MQIs (MQStringSVar svar, mqs) - ) - -let rec build_inter n = function - | [] -> MQPattern (None, [MQBSS], [MQFSS]) - | [ie] -> build_select ie n - | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) - -let restrict_universe query = - function - [] -> query (* no constraints ===> the universe is the library *) - | l -> - let universe = - MQReference (List.map ie_str_uri l) - in - MQLetIn ( - "universe", universe, - MQSelect ( - "uri", query, - MQSubset ( - MQSelect ( - "uri2", - MQUsedBy (MQListRVar "uri", "pos"), - MQOr ( - MQIs (MQStringSVar "pos", MQConclusion), - MQIs (MQStringSVar "pos", MQMConclusion) - ) - ), - MQListLVar "universe" - ) - ) - ) - -let init = Mqint.init - -let close = Mqint.close - -let locate_query s = -(*CSC: next query to be fixed - 1) I am exploiting the bug that does not quote '|' - 2) I am searching only constants and mutual inductive definition blocks - (i.e. no fragment identifier at all) -*) - MQList (MQSelect ("ref", - MQPattern (Some "cic", [MQBSS ; MQBC ".con|.ind"],[]), - MQIs (MQFunc (MQName, "ref"), - MQCons s - ) - ) - ) +(* level managing functions *************************************************) + +type levels_spec = (string * bool * int) list + +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 -> inspect_uri main l u [] v term + | Cic.Const (u, _) -> inspect_uri main l u [] v term + | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term + | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term + | 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_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 string_of_levels l sep = + let entry_out (s, b, v) = + let pos = if b then " HEAD: " else " TAIL: " in + string_of_int v ^ pos ^ s ^ sep + in + let rec levels_out = function + | [] -> "" + | head :: tail -> entry_out head ^ levels_out tail + in + levels_out l + +(* Query issuing functions **************************************************) + +exception Discard + +let nl = "

\n" + +let query_num = ref 1 + +let log_file = ref "" + +let confirm_query = ref (fun _ -> true) + +let info = ref [] + +let set_log_file f = + log_file := f + +let set_confirm_query f = + confirm_query := f + +let get_query_info () = ! info + +let execute_query query = + let module Util = MQueryUtil in + let mode = [Open_wronly; Open_append; Open_creat; Open_text] in + let perm = 64 * 6 + 8 * 6 + 4 in + let time () = + let lt = Unix.localtime (Unix.time ()) in + "NEW LOG: " ^ + string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^ + string_of_int (lt.Unix.tm_year + 1900) ^ " " ^ + string_of_int (lt.Unix.tm_hour) ^ ":" ^ + string_of_int (lt.Unix.tm_min) ^ ":" ^ + string_of_int (lt.Unix.tm_sec) + in + let log q r = + let och = open_out_gen mode perm ! log_file in + if ! query_num = 1 then output_string och (time () ^ nl); + let str = "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ + "Result:" ^ nl ^ Util.text_of_result r nl in + output_string och str; + flush och + in + let execute q = + let r = Mqint.execute q in + if ! log_file <> "" then log q r; + info := string_of_int ! query_num :: ! info; + incr query_num; + r + in + if ! confirm_query query then execute query else raise Discard + +(* Query building functions ************************************************) let locate s = - let MQRefs uris, html = build_result (locate_query s) in -(*CSC: here I am mapping .ind URIs to .ind#1/1, i.e. the first type of *) -(*CSC: the mutual inductive block. It must be removed once the query *) -(*CSC: works reasonably. *) - MQRefs ( - List.map - (function uri -> - if String.sub uri (String.length uri - 4) 4 = ".ind" then - uri ^ "#1/1" - else - uri - ) uris - ), html -;; - -let levels e c t = - env := e; cont := c; - let il = inspect t in - par () ^ il_out il ^ nl () - -let call_back f = - issue := f + let module M = MathQL in + let q = M.Ref (M.Fun "reference" (M.Const [s])) in + execute_query q let backward e c t level = - let t0 = Sys.time () in - env := e; cont := c; - let il = inspect t in - let query = build_inter 0 (il_restrict level il) in - let query' = restrict_universe query il in - let query'' = MQList query' in - let res = build_result query'' in - let r,html = res in - if html <> "" then - begin - print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^ - string_of_float (Sys.time () -. t0) ^ "s"); - r, par () ^ il_out il ^ html - end else res + let module M = MathQL in + let v_pos = M.Const ["MainConclusion"; "InConclusion"] in + let q_where = M.Sub (M.RefOf ( + M.Select ("uri", + M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]), + M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) + )), M.VVar "universe" + ) + in + let uri_of_entry (r, b, v) = 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) = + let pos = if b then "MainConclusion" else "InConclusion" in + M.Select ("uri", + M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]), + M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos"))) + ) + in + let rec build_intersect = function + | [] -> M.Pattern (M.Const [".*"]) + | [hd] -> build_select hd + | hd :: tl -> M.Intersect (build_select hd, build_intersect tl) + in + let levels = 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 + let q_select = M.Select ("uri0", q_in, q_where) in + let universe = M.Const (List.map uri_of_entry levels) 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 + execute_query q_let_p diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli index 694fdcf12..57137974f 100644 --- a/helm/gTopLevel/mQueryGenerator.mli +++ b/helm/gTopLevel/mQueryGenerator.mli @@ -33,18 +33,23 @@ (* *) (******************************************************************************) -val levels : Cic.metasenv -> Cic.context -> Cic.term -> string - (* level assignment testing function *) +exception Discard -val call_back : (MathQL.mquery -> bool) -> unit +type levels_spec = (string * bool * int) list -val init : unit -> unit (* INIT database function *) +val levels_of_term : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec -val close : unit -> unit (* CLOSE database function *) +val string_of_levels : levels_spec -> string -> string -val locate : string -> MathQL.mqresult * string - (* LOCATE query building function *) +val set_log_file : string -> unit -val backward : - Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.mqresult * string - (* BACKWARD query building function *) +(* the callback function must return false iff the query must be skipped *) +val set_confirm_query : (MathQL.query -> bool) -> unit + +val execute_query : MathQL.query -> MathQL.result + +val locate : string -> MathQL.result + +val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result + +val get_query_info : unit -> string list diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml index 1fa790b64..cc1b3034b 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -1,15 +1,25 @@ +let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm" + +let show_queries = ref false + let use_db = ref true let db_down = ref true +let nl = "

\n" + let check_db () = - if ! db_down then begin - if ! use_db then begin - MQueryGenerator.init (); db_down := false - end else - raise (Failure "Operation impossible in restricted mode") - end - + if ! db_down then + if ! use_db then begin Mqint.init connection_param; db_down := false; true end + else begin print_endline "Not issuing in restricted mode"; false end + else true + +let default_confirm q = + let module Util = MQueryUtil in + if ! show_queries then print_string (Util.text_of_query q ^ nl); + let b = check_db () in + if ! db_down then print_endline "db_down"; b + let get_terms () = let terms = ref [] in let lexbuf = Lexing.from_channel stdin in @@ -39,42 +49,76 @@ let pp_type_of uri = *) in print_endline s; flush stdout -let locate name = - check_db (); - print_endline (snd (MQueryGenerator.locate name)) ; - flush stdout +let dbc () = + let on = check_db () in + if on then ignore (Mqint.check ()) let rec display = function | [] -> () | term :: tail -> display tail; - print_endline ("? " ^ CicPp.ppterm term ^ "

"); + print_string ("? " ^ CicPp.ppterm term ^ nl); flush stdout -let rec levels = function - | [] -> () - | term :: tail -> - levels tail; - print_endline ("? " ^ CicPp.ppterm term ^ "

"); - print_endline (MQueryGenerator.levels [] [] term); +let levels l = + let module Gen = MQueryGenerator in + let rec levels_aux = function + | [] -> () + | term :: tail -> + levels_aux tail; + print_string ("? " ^ CicPp.ppterm term ^ nl); + print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl); + flush stdout + in + levels_aux l + +let execute ich = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + let q = Util.query_of_text (Lexing.from_channel ich) in + print_endline (Util.text_of_result (Gen.execute_query q) nl); + flush stdout + with Gen.Discard -> () + +let locate name = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in + Gen.set_confirm_query default_confirm; + try + print_endline (Util.text_of_result (Gen.locate name) nl); flush stdout - -let mbackward n m l = + with Gen.Discard -> () + +let mbackward n m l = + let module Util = MQueryUtil in + let module Gen = MQueryGenerator in let queries = ref [] in - let issue query = - if List.mem query ! queries then false - else begin queries := query :: ! queries; true end + let confirm query = + if List.mem query ! queries then false + else begin queries := query :: ! queries; default_confirm query end in let rec backward level = function | [] -> () | term :: tail -> backward level tail; - print_endline ("? " ^ CicPp.ppterm term ^ "

"); - print_endline (snd (MQueryGenerator.backward [] [] term level)) ; - flush stdout + try + if Mqint.get_stat () then + print_string ("? " ^ CicPp.ppterm term ^ nl); + let t0 = Sys.time () in + let r = Gen.backward [] [] term level in + let t1 = Sys.time () -. t0 in + let info = Gen.get_query_info () in + let num = List.nth info 0 in + let gen = List.nth info 1 in + if Mqint.get_stat () then + print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl); + print_string (Util.text_of_result r nl); + flush stdout + with Gen.Discard -> () in - check_db (); - MQueryGenerator.call_back issue; + Gen.set_confirm_query confirm; for level = max m n downto min m n do prerr_endline ("toplevel: backward: trying level " ^ string_of_int level); @@ -82,21 +126,48 @@ let mbackward n m l = done; prerr_endline ("toplevel: backward: " ^ string_of_int (List.length ! queries) ^ - " queries issued"); - MQueryGenerator.call_back (fun _ -> true) - + " queries issued") + +let prerr_help () = + prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n"; + prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; + prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output"; + prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; + prerr_endline "OPTIONS:\n"; + prerr_endline "-h -help shows this help message"; + prerr_endline "-q -show-queries outputs generated queries"; + prerr_endline "-s -stat outputs interpreter statistics"; + prerr_endline "-c -db-check checks the database connection"; + prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued"; + prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; + prerr_endline "-x -execute issues a query given in the input file"; + prerr_endline "-d -disply outputs the CIC terms given in the input file"; + prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file"; + prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; + prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms"; + prerr_endline " in the input file"; + prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all"; + prerr_endline " CIC terms in the input file\n"; + prerr_endline "NOTES: CIC terms are read with the HELM CIC Textual Parser"; + prerr_endline " -typeof does not work with inductive types and proofs in progress\n" + let parse_args () = let rec parse = function | [] -> () + | ("-h"|"-help") :: rem -> prerr_help () | ("-d"|"-display") :: rem -> display (get_terms ()) | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem | ("-l"|"-levels") :: rem -> levels (get_terms ()) - | ("-r"|"-restricted") :: rem -> use_db := false; parse rem + | ("-x"|"-execute") :: rem -> execute stdin; parse rem + | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem + | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem + | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem + | ("-c"|"-db-check") :: rem -> dbc (); parse rem | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem | ("-B"|"-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m m (get_terms ()) - | ("-MB"|"-mbackward") :: arg :: rem -> + | ("-MB"|"-multi-backward") :: arg :: rem -> let m = (int_of_string arg) in mbackward m 0 (get_terms ()) | _ :: rem -> parse rem @@ -104,12 +175,16 @@ let parse_args () = parse (List.tl (Array.to_list Sys.argv)) let _ = + let module Gen = MQueryGenerator in CicCooking.init () ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + Mqint.set_stat false; + Gen.set_log_file "MQGenLog.htm"; parse_args (); - if not ! db_down then MQueryGenerator.close (); + if not ! db_down then Mqint.close (); + Gen.set_confirm_query (fun _ -> true); prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ " seconds"); exit 0 -- 2.39.2