From 2894cb7d5855ac2003e81c9383c3cf3843973d9e Mon Sep 17 00:00:00 2001 From: lordi Date: Wed, 22 May 2002 17:51:53 +0000 Subject: [PATCH] result format changed --- helm/gTopLevel/mquery.ml | 68 ++++++++++------------------------------ 1 file changed, 16 insertions(+), 52 deletions(-) diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml index e27c8e2c0..b53abbe21 100644 --- a/helm/gTopLevel/mquery.ml +++ b/helm/gTopLevel/mquery.ml @@ -1,38 +1,3 @@ -(* 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 Mathql open Cic @@ -54,8 +19,8 @@ let str_fi = function | (Some t, None) -> "#1/" ^ string_of_int t | (Some t, Some c) -> "#1/" ^ string_of_int t ^ "/" ^ string_of_int c -let str_tref (p, u, x, i) = - p ^ ":/" ^ str_up u ^ "." ^ x ^ str_fi i +let str_tref (p, u, i) = + p ^ ":/" ^ str_up u ^ str_fi i let str_uref (u, i) = UriManager.string_of_uri u ^ str_fi i @@ -88,6 +53,7 @@ let out_pat p = out_tref p let out_func = function | MQName -> key "name" + | _ -> assert false let out_str = function | MQCons s -> con s @@ -113,6 +79,7 @@ let rec out_list = function | MQPattern p -> key "pattern" ^ out_pat p | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")" | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")" + | _ -> assert false let out_query = function | MQList l -> out_list l @@ -121,7 +88,7 @@ let out_query = function let rec out_list = function | [] -> "" - | u :: l -> res u ^ nl () ^ out_list l + | u :: l -> res (str_tref u) ^ nl () ^ out_list l let out_result qr = par () ^ "Result:" ^ nl () ^ @@ -135,13 +102,9 @@ let split s = let i = Str.search_forward (Str.regexp_string ":/") s 0 in let p = Str.string_before s i in let q = Str.string_after s (i + 2) in - try - let j = String.rindex q '.' in - (p, Str.string_before q j, Str.string_after q (j + 1)) - with - Not_found -> (p, q, "") + (p, q) with - Not_found -> (s, "", "") + Not_found -> (s, "") let encode = function | Str.Text s -> MQString s @@ -154,10 +117,10 @@ let encode = function let tref_uref (u, i) = let s = UriManager.string_of_uri u in match split s with - | (p, q, r) -> + | (p, q) -> let rx = Str.regexp "\?\|\*\*\|\*\|/" in let l = Str.full_split rx q in - (p, List.map encode l, r, i) + (p, List.map encode l, i) (* CIC term inspecting functions *) @@ -187,13 +150,13 @@ let inspect_uri main l uri t c v = let fi = match (t, c) with | (None, _) -> (None, None) - | (Some t0, c0) -> (Some (t0 + 1), c0) + | (Some t0, c0) -> (Some (t0 + 1), c0) in ie_insert ((uri, fi), main, v) l let rec inspect_term main l v = function | Rel i -> l - | Meta (i, _) -> l + | Meta (i, _) -> l | Sort s -> l | Implicit -> l | Abst u -> l @@ -254,11 +217,11 @@ let build_select (r, b, v) n = let mqs = if b then MQMConclusion else MQConclusion in MQSelect (rvar, MQUse (MQPattern r, svar), - MQIs (MQSVar svar, mqs) - ) + MQIs (MQSVar svar, mqs) + ) let rec build_inter n = function - | [] -> MQPattern ("cic", [MQAstAst], "con", (None, None)) + | [] -> MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)) | [ie] -> build_select ie n | ie :: il -> MQIntersect (build_select ie n, build_inter (n + 1) il) @@ -274,7 +237,7 @@ let close = Mqint.close let locate s = let query = MQList (MQSelect ("ref", - MQPattern ("cic", [MQAstAst], "con", (None, None)), + MQPattern ("cic", [MQAstAst; MQString ".con"], (None, None)), MQIs (MQFunc (MQName, "ref"), MQCons s ) @@ -289,3 +252,4 @@ let backward t n = let til = List.map tie_uie uil in let query = MQList (build_inter 0 til) in par () ^ out_il uil ^ build_result query + -- 2.39.2