X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2FmQIUtil.ml;fp=helm%2Focaml%2Fmathql_interpreter%2FmQIUtil.ml;h=0000000000000000000000000000000000000000;hp=00f5390b512a545b9fb29b5cd672cfbe7e5c4b7a;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/mathql_interpreter/mQIUtil.ml b/helm/ocaml/mathql_interpreter/mQIUtil.ml deleted file mode 100644 index 00f5390b5..000000000 --- a/helm/ocaml/mathql_interpreter/mQIUtil.ml +++ /dev/null @@ -1,153 +0,0 @@ -(* 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/. - *) - -(* AUTOR: Ferruccio Guidi - *) - -(* boolean constants *******************************************************) - -let mql_false = [] - -let mql_true = [""] - -(* set theoretic operations *************************************************) - -let rec set_sub v1 v2 = - match v1, v2 with - | [], _ -> mql_true - | _, [] -> mql_false - | h1 :: _, h2 :: _ when h1 < h2 -> mql_false - | h1 :: _, h2 :: t2 when h1 > h2 -> set_sub v1 t2 - | _ :: t1, _ :: t2 -> set_sub t1 t2 - -let rec set_meet v1 v2 = - match v1, v2 with - | [], _ -> mql_false - | _, [] -> mql_false - | h1 :: t1, h2 :: _ when h1 < h2 -> set_meet t1 v2 - | h1 :: _, h2 :: t2 when h1 > h2 -> set_meet v1 t2 - | _, _ -> mql_true - -let set_eq v1 v2 = - if v1 = v2 then mql_true else mql_false - -let rec set_union v1 v2 = - match v1, v2 with - | [], v -> v - | v, [] -> v - | h1 :: t1, h2 :: t2 when h1 < h2 -> h1 :: set_union t1 v2 - | h1 :: t1, h2 :: t2 when h1 > h2 -> h2 :: set_union v1 t2 - | h1 :: t1, _ :: t2 -> h1 :: set_union t1 t2 - -let rec set_intersect v1 v2 = - match v1, v2 with - | [], v -> [] - | v, [] -> [] - | h1 :: t1, h2 :: _ when h1 < h2 -> set_intersect t1 v2 - | h1 :: _, h2 :: t2 when h1 > h2 -> set_intersect v1 t2 - | h1 :: t1, _ :: t2 -> h1 :: set_intersect t1 t2 - -let rec iter f = function - | [] -> [] - | head :: tail -> set_union (f head) (iter f tail) - -(* MathQL specific set operations ******************************************) - -let rec mql_union s1 s2 = - match s1, s2 with - | [], s -> s - | s, [] -> s - | (r1, g1) :: t1, (r2, _) :: _ when r1 < r2 -> - (r1, g1) :: mql_union t1 s2 - | (r1, _) :: _, (r2, g2) :: t2 when r1 > r2 -> - (r2, g2) :: mql_union s1 t2 - | (r1, g1) :: t1, (_, g2) :: t2 -> - (r1, set_union g1 g2) :: mql_union t1 t2 - -let rec mql_iter f = function - | [] -> [] - | head :: tail -> mql_union (f head) (mql_iter f tail) - -let rec mql_iter2 f l1 l2 = match l1, l2 with - | [], [] -> [] - | h1 :: t1, h2 :: t2 -> mql_union (f h1 h2) (mql_iter2 f t1 t2) - | _ -> raise (Invalid_argument "mql_iter2") - -let rec mql_prod g1 g2 = - let mql_prod_aux a = iter (fun h -> [mql_union a h]) g2 in - iter mql_prod_aux g1 - -let rec mql_intersect s1 s2 = - match s1, s2 with - | [], s -> [] - | s, [] -> [] - | (r1, _) :: t1, (r2, _) :: _ when r1 < r2 -> mql_intersect t1 s2 - | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_intersect s1 t2 - | (r1, g1) :: t1, (_, g2) :: t2 -> - (r1, set_intersect g1 g2) :: mql_intersect t1 t2 - -let rec mql_diff s1 s2 = - match s1, s2 with - | [], _ -> [] - | s, [] -> s - | (r1, g1) :: t1 , (r2, _) ::_ when r1 < r2 -> - (r1, g1) :: (mql_diff t1 s2) - | (r1, _) :: _, (r2, _) :: t2 when r1 > r2 -> mql_diff s1 t2 - | _ :: t1, _ :: t2 -> mql_diff t1 t2 - -(* logic operations ********************************************************) - -let xor v1 v2 = - let b = v1 <> mql_false in - if b && v2 <> mql_false then mql_false else - if b then v1 else v2 - -(* numeric operations ******************************************************) - -let int_of_list = function - | [s] -> int_of_string s - | _ -> raise (Failure "int_of_list") - -let le v1 v2 = - try if int_of_list v1 <= int_of_list v2 then mql_true else mql_false - with _ -> mql_false - -let lt v1 v2 = - try if int_of_list v1 < int_of_list v2 then mql_true else mql_false - with _ -> mql_false - -let align n v = - let c = String.length v in - try - let l = int_of_list [n] in - if c < l then [(String.make (l - c) ' ') ^ v] else [v] - with _ -> [v] - -(* context handling ********************************************************) - -let rec set ap = function - | [] -> [ap] - | head :: tail when fst head = fst ap -> ap :: tail - | head :: tail -> head :: set ap tail