From 8207214be059c22b92976623035ee94e45e24486 Mon Sep 17 00:00:00 2001 From: no author Date: Tue, 17 Sep 2002 09:00:31 +0000 Subject: [PATCH] This commit was manufactured by cvs2svn to create branch 'new_mathql'. --- helm/gTopLevel/mQueryGenerator.ml | 247 +++++++++++++++++++ helm/gTopLevel/topLevel/topLevel.ml | 115 +++++++++ helm/ocaml/mathql_interpreter/mqint.ml | 302 ++++++++++++++++++++++++ helm/ocaml/mathql_interpreter/mqint.mli | 30 +++ 4 files changed, 694 insertions(+) create mode 100644 helm/gTopLevel/mQueryGenerator.ml create mode 100644 helm/gTopLevel/topLevel/topLevel.ml create mode 100644 helm/ocaml/mathql_interpreter/mqint.ml create mode 100644 helm/ocaml/mathql_interpreter/mqint.mli diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml new file mode 100644 index 000000000..bb27633bb --- /dev/null +++ b/helm/gTopLevel/mQueryGenerator.ml @@ -0,0 +1,247 @@ +(* 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 *) +(* *) +(* Ferruccio Guidi *) +(* 30/04/2002 *) +(* *) +(* *) +(******************************************************************************) + +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 + save (html ^ out_result result) + else "" + +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 + ) + ) + ) + +let locate s = Mqint.execute (locate_query s) +let locate_html s = build_result (locate_query s) + +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 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 r = build_result query'' in + if r <> "" then + begin + print_endline ("GEN = " ^ string_of_int (List.length il) ^ ":" ^ + string_of_float (Sys.time () -. t0) ^ "s"); + par () ^ il_out il ^ r + end else "" diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml new file mode 100644 index 000000000..9992e4093 --- /dev/null +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -0,0 +1,115 @@ +let use_db = ref true + +let db_down = ref true + +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 + +let get_terms () = + let terms = ref [] in + let lexbuf = Lexing.from_channel stdin in + try + while true do + match CicTextualParserContext.main + (UriManager.uri_of_string "cic:/dummy") [] [] + CicTextualLexer.token lexbuf + with + | None -> () + | Some (_, expr) -> terms := expr :: ! terms + done; + ! terms + with + CicTextualParser0.Eof -> ! terms + +let pp_type_of uri = + let u = UriManager.uri_of_string uri in + let s = match (CicEnvironment.get_obj u) with + | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty + | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty + | Cic.Variable (_, _, ty) -> CicPp.ppterm ty + | _ -> "Current proof or inductive definition." +(* + | Cic.CurrentProof (_,conjs,te,ty) -> + | C.InductiveDefinition _ -> +*) + in print_endline s; flush stdout + +let locate name = + check_db (); + print_endline (MQueryGenerator.locate_html name); + flush stdout + +let rec display = function + | [] -> () + | term :: tail -> + display tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

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

"); + print_endline (MQueryGenerator.levels [] [] term); + flush stdout + +let mbackward n m l = + let queries = ref [] in + let issue query = + if List.mem query ! queries then false + else begin queries := query :: ! queries; true end + in + let rec backward level = function + | [] -> () + | term :: tail -> + backward level tail; + print_endline ("? " ^ CicPp.ppterm term ^ "

"); + print_endline (MQueryGenerator.backward [] [] term level); + flush stdout + in + check_db (); + MQueryGenerator.call_back issue; + for level = max m n downto min m n do + prerr_endline ("toplevel: backward: trying level " ^ + string_of_int level); + backward level l + done; + prerr_endline ("toplevel: backward: " ^ + string_of_int (List.length ! queries) ^ + " queries issued"); + MQueryGenerator.call_back (fun _ -> true) + +let parse_args () = + let rec parse = function + | [] -> () + | ("-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 + | ("-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 -> + let m = (int_of_string arg) in + mbackward m 0 (get_terms ()) + | _ :: rem -> parse rem + in + parse (List.tl (Array.to_list Sys.argv)) + +let _ = + CicCooking.init () ; + Logger.log_callback := + (Logger.log_to_html + ~print_and_flush:(function s -> print_string s ; flush stdout)) ; + parse_args (); + if not ! db_down then MQueryGenerator.close (); + prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ + " seconds"); + exit 0 diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml new file mode 100644 index 000000000..053e20c74 --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mqint.ml @@ -0,0 +1,302 @@ +(* 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/. + *) + +(* + * implementazione del'interprete MathQL + *) + +(* +(* FG: ROBA VECCHIA DA BUTTARE (tranne apertura e chiusura database *) + +open MathQL;; +open Eval;; +open Utility;; +open Dbconn;; +open Pattern;; +open Union;; +open Intersect;; +open Diff;; +open Sortedby;; +open Use;; +open Select;; +open Letin;; +open Mathql_semantics;; + + + +let prop_pool = ref None;; + +let fi_to_string fi = + match fi with + (None, _) -> + "" + | (Some i, y) -> + "#xpointer(1/" ^ + string_of_int i ^ + ( + match y with + None -> + "" + | Some j -> + "/" ^ (string_of_int j) + ) ^ + ")" +;; + +let see_prop_pool () = + let _ = print_endline "eccomi" in + List.iter + (fun elem -> print_endline (fst elem ^ ": " ^ snd elem)) + (match !prop_pool with Some l -> l | _ -> print_endline "ciao"; assert false) +;; + +(* + * inizializzazione della connessione al database + *) +let init () = + let _ = Dbconn.init () in + let c = pgc () in + let res = + c#exec "select name,id from property where ns_id in (select id from namespace where url='http://www.cs.unibo.it/helm/schemas/mattone.rdf#')" + in + prop_pool := Some + ( + List.map + (function + a::b::_ -> (a, b) + | _ -> print_endline "no"; assert false + ) + res#get_list + ) +;; + +let get_prop_id prop = + if prop="refObj" then "F" + else if prop="backPointer" then "B" + else List.assoc prop (match !prop_pool with Some l -> l | _ -> assert false) +;; + +(* execute_ex env q *) +(* [env] is the attributed uri environment in which the query [q] *) +(* must be evaluated *) +(* [q] is the query to evaluate *) +(* It returns a [Mathql_semantics.result] *) +let rec execute_ex env = + function + MQSelect (apvar, alist, abool) -> + select_ex env apvar (execute_ex env alist) abool + | MQUsedBy (alist, asvar) -> + use_ex (execute_ex env alist) asvar (get_prop_id "refObj") (* "F" (*"refObj"*) *) + | MQUse (alist, asvar) -> + use_ex (execute_ex env alist) asvar (get_prop_id "backPointer") (* "B" (*"backPointer"*) *) + | MQPattern (apreamble, apattern, afragid) -> + pattern_ex (apreamble, apattern, afragid) + | MQUnion (l1, l2) -> + union_ex (execute_ex env l1) (execute_ex env l2) + | MQDiff (l1, l2) -> + diff_ex (execute_ex env l1) (execute_ex env l2) + | MQSortedBy (l, o, f) -> + sortedby_ex (execute_ex env l) o f + | MQIntersect (l1, l2) -> + intersect_ex (execute_ex env l1) (execute_ex env l2) + | MQListRVar rvar -> [List.assoc rvar env] + | MQLetIn (lvar, l1, l2) -> + let t = Unix.time () in + let res = + (*CSC: The interesting code *) + let _ = letin_ex lvar (execute_ex env l1) in + execute_ex env l2 + (*CSC: end of the interesting code *) + in + letdispose (); + print_string ("LETIN = " ^ string_of_int (List.length res) ^ ": ") ; + print_endline (string_of_float (Unix.time () -. t) ^ "s") ; + flush stdout ; + res + | MQListLVar lvar -> + letref_ex lvar + | MQReference l -> + let rec build_result = function + | [] -> [] + | s :: tail -> + {uri = s ; attributes = [] ; extra = ""} :: build_result tail + in build_result (List.sort compare l) +;; + +(* Let's initialize the execute in Select, creating a cyclical recursion *) +Select.execute := execute_ex;; + +(* + * converte il risultato interno di una query (uri + contesto) + * in un risultato di sole uri + * + * parametri: + * l: string list list; + * + * output: mqresult; + * + * note: + * il tipo del risultato mantenuto internamente e' diverso dal tipo di risultato + * restituito in output poiche', mentre chi effettua le query vuole come risultato + * solo le eventuali uri che soddisfano le query stesse, internamente ad una uri + * sono associati anche i valori delle variabili che ancora non sono state valutate + * perche', ad esempio, si trovano in altri rami dell'albero. + * + * Esempio: + * SELECT x IN USE PATTERN "cic:/**.con" POSITION $a WHERE $a IS MainConclusion + * L'albero corrispondente a questa query e': + * + * SELECT + * / | \ + * x USE IS + * / \ /\ + * PATTERN $a $a MainConclusion + * + * Nel momento in cui si esegue il ramo USE non sono noti i vincoli sullla variabile $a + * percui e' necessario considerare, oltre alle uri, i valori della variabile per i quali + * la uri puo' far parte del risultato. + *) +let xres_to_res l = + MQRefs (List.map (function {Mathql_semantics.uri = uri} -> uri) l) +(* + let tmp = List.map (function {Mathql_semantics.uri = uri} -> uri) l in + MQRefs + (List.map + (function l -> + (*let _ = print_endline ("DEBUG: (mqint.ml: xres_to_res)" ^ l) in*) + match Str.split (Str.regexp ":\|#\|/\|(\|)") l with + hd::""::tl -> ( + match List.rev tl with + n::"1"::"xpointer"::tail -> + ( + Some hd, + List.fold_left + (fun par t -> + match par with + [] -> [MQBC t] + | _ -> (MQBC t) :: MQBD :: par + ) + [] + tail, + [MQFC (int_of_string n)] + ) + | n::m::"1"::"xpointer"::tail -> + ( + Some hd, + List.fold_left + (fun par t -> + match par with + [] -> [MQBC t] + | _ -> (MQBC t) :: MQBD :: par + ) + [] + tail, + [MQFC (int_of_string m); MQFC (int_of_string n)] + ) + | tail -> + ( + Some hd, + List.fold_left + (fun par t -> + match par with + [] -> [MQBC t] + | _ -> (MQBC t) :: MQBD :: par + ) + [] + tail, + [] + ) + ) + | _ -> assert false + ) + tmp + ) +*) +;; + + +(* + * + *) +let execute q = + match q with + MQList qq -> xres_to_res (execute_ex [] qq) +;; + +(* + * chiusura della connessione al database + *) +let close () = Dbconn.close ();; + +*****************************************************************************) + +let init () = () (* FG: implementare l'apertura del database *) + +let close () = () (* FG: implementare la chiusura del database *) + + +(* contexts *****************************************************************) + +type svar_context = (MathQL.svar * MathQL.resource_set) list + +type rvar_context = (MathQL.rvar * MathQL.resource) list + +type group_context = (MathQL.rvar * MathQL.attribute_group) list + + +let svars = ref [] (* contesto delle svar *) + +let rvars = ref [] (* contesto delle rvar *) + +let groups = ref [] (* contesto dei gruppi *) + + +(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) + +let rec exec_set_exp = function + | MathQL.Ref x -> [] + + +(* valuta una MathQL.boole_exp e ritorna un boole *) + +and exec_boole_exp = function + | MathQL.False -> false + | MathQL.True -> true + | MathQL.Not x -> not (exec_boole_exp x) + | MathQL.And (x, y) -> (exec_boole_exp x) && (exec_boole_exp y) + | MathQL.Or (x, y) -> (exec_boole_exp x) || (exec_boole_exp y) + + +(* valuta una MathQL.val_exp e ritorna un MathQL.value *) + +and exec_val_exp = function + | MathQL.Const l -> [] + + +(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) + +let execute x = + svars := []; rvars := []; groups := []; + exec_set_exp x diff --git a/helm/ocaml/mathql_interpreter/mqint.mli b/helm/ocaml/mathql_interpreter/mqint.mli new file mode 100644 index 000000000..45e8b60ef --- /dev/null +++ b/helm/ocaml/mathql_interpreter/mqint.mli @@ -0,0 +1,30 @@ +(* 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/. + *) + +val init : unit -> unit (* open database *) + +val execute : MathQL.query -> MathQL.result (* execute query *) + +val close : unit -> unit (* close database *) -- 2.39.2