(* 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/. *) (* Query issuing functions **************************************************) type uri = string type position = string type depth = int option type sort = string type r_obj = (uri * position * depth) type r_rel = (position* depth) type r_sort = (position* depth * sort) type must_restrictions = (r_obj list * r_rel list * r_sort list) type only_restrictions = (r_obj list option * r_rel list option * r_sort list option) type universe = position list option let builtin s = let ns = "h:" in match s with | "MH" -> ns ^ "MainHypothesis" | "IH" -> ns ^ "InHypothesis" | "MC" -> ns ^ "MainConclusion" | "IC" -> ns ^ "InConclusion" | "IB" -> ns ^ "InBody" | "SET" -> ns ^ "Set" | "PROP" -> ns ^ "Prop" | "TYPE" -> ns ^ "Type" | _ -> raise (Failure "MQueryGenerator.builtin") (* Query building functions ************************************************) module M = MathQL let locate s = M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s])) let query_of_constraints univ must_use can_use = (* FG : The (univ : universe) is not used in this implementation *) let in_path s = (s, []) in let assign v p = (in_path v, in_path p) in (* can restrictions *) let (cr_o,cr_r,cr_s) = can_use in let uri_of_entry (r, p, d) = r in let universe = match cr_o with None -> [] | Some cr_o -> List.map uri_of_entry cr_o in let tfst (a,b,c) = a in let tsnd (a,b,c) = b in let trd (a,b,c) = c in let to_int_list l d = match d with None -> l | Some d -> l@[d] in let opos = match cr_o with None -> [] | Some cr_o -> (List.map tsnd cr_o) in let odep = match cr_o with None -> [] | Some cr_o -> List.map trd cr_o (* let odep_option_list = List.map trd cr_o in let lo_dep_int = List.fold_left to_int_list [] odep_option_list in List.map string_of_int lo_dep_int*) in print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout; print_endline""; let rpos = match cr_r with None -> [] | Some cr_r -> (List.map fst cr_r) in let rdep = match cr_r with None -> [] | Some cr_r -> List.map snd cr_r (* let rdep_option_list = List.map snd cr_r in let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in List.map string_of_int lr_dep_int *) in let spos = match cr_s with None -> [] | Some cr_s -> (List.map tfst cr_s) in let sdep = match cr_s with None -> [] | Some cr_s -> List.map tsnd cr_s (* let sdep_option_list = List.map tsnd cr_s in let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in List.map string_of_int ls_dep_int*) in let sor = match cr_s with None -> [] | Some cr_s -> List.map trd cr_s in (* let q_where_obj = function Some l -> if odep = [] then M.Sub (M.RefOf (M.Select ("uri", M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]), M.Ex ["uri"] (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))), M.VVar "universe") else M.Sub (M.RefOf (M.Select ("uri", M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "p" "position"; assign "d" "depth"] ), M.Ex ["uri"] (M.And ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))), (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d"))))) ) ), M.VVar "universe" ) | None -> M.True in*) let q_where_obj n = function Some l -> let rec q_ex n = function [] -> M.True | [(u,p,None)] -> M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")) | [(u,p,d)] -> print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; print_endline""; M.And (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")), M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))) | (u,p,None)::tl -> M.Or (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")), q_ex (n+1) tl) | (u,p,d)::tl -> print_string "@@@@@ IN-WHERE-OBJ"; flush stdout; print_endline""; M.Or ((M.And ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))), (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))), q_ex (n+1) tl) in M.Sub (M.RefOf (M.Select ("uri", M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "p" "position"; assign "d" "depth"] ), M.Ex ["uri"] (q_ex 1 l))), M.VVar "universe") | None -> M.True in let rec q_where_rel n cr_r= (*function*) (* Some l ->*) let q0 = M.Sub (M.Property (false, M.RefineExact, ("refRel", ["position"]), M.RefOf(M.RVar "uri0")), M.VVar ("rel_position" ^ string_of_int n)) in match cr_r with Some [] -> M.True | Some [(p,None)] -> q0 | Some [(p,d)] -> M.And (q0, M.Sub (M.Property (false, M.RefineExact, ("refRel", ["depth"]), M.RefOf(M.RVar "uri0")), M.VVar ("rel_depth" ^ string_of_int n))) | Some ((p,None)::tl) -> M.Or (q0, q_where_rel (n+1) (Some tl)) | Some ((p,d)::tl) -> M.Or (M.And (q0, M.Sub (M.Property (false, M.RefineExact, ("refRel", ["depth"]), M.RefOf(M.RVar "uri0")), M.VVar ("rel_depth" ^ string_of_int n))), q_where_rel (n+1) (Some tl)) | None -> M.True in let rec q_where_sort n cr_s = (*function *) (* Some l ->*) let q0 = M.And (M.Sub (M.Property (false, M.RefineExact, ("refSort", ["position"]), M.RefOf(M.RVar "uri0") ), M.VVar ("sort_position" ^ string_of_int n)), M.Sub (M.Property (false, M.RefineExact, ("refSort", ["sort"]), M.RefOf(M.RVar "uri0")), M.VVar ("sort" ^ string_of_int n))) in match cr_s with Some [] -> M.True | Some [(p,None,s)] -> q0 | Some [(p,d,s)] -> M.And (q0, M.Sub (M.Property (false, M.RefineExact, ("refSort", ["depth"]), M.RefOf(M.RVar "uri0")), M.VVar ("sort_depth" ^ string_of_int n))) | Some ((p,None,s)::tl) -> M.Or (q0, q_where_sort (n+1) (Some tl)) | Some((p,d,s)::tl) -> M.Or (M.And (q0, M.Sub (M.Property (false, M.RefineExact, ("refSort", ["depth"]), M.RefOf(M.RVar "uri0")), M.VVar ("sort_depth" ^ string_of_int n))), q_where_sort (n+1) (Some tl)) | None -> M.True in let q_where cr = let (cr_o,cr_r,cr_s) = cr in M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s)) in (* must restrictions *) let build_select_obj (r, pos, dep) = match dep with None -> M.Select ("uri", M.Relation (false, M.RefineExact, ("backPointer", []), M.Ref (M.Const [r]), [assign "p" "position"]), M.Ex ["uri"] ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))))) | Some dep -> let string_dep = string_of_int dep in M.Select ("uri", M.Relation (false, M.RefineExact, ("backPointer", []), M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]), M.Ex ["uri"] (M.And ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) in let build_select_rel (pos, dep) = match dep with None -> M.Select ("uri", M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))) | Some dep -> let string_dep = string_of_int dep in M.Select ("uri", M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), M.Ex ["uri"] (M.And ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d")))))) in let build_select_sort (pos, dep, sor) = match dep with None -> M.Select ("uri", M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), M.Ex ["uri"] (M.And ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) | Some dep -> let string_dep = string_of_int dep in M.Select ("uri", M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), M.Ex ["uri"] (M.And ((M.And ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))), (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))), (M.Sub (M.Const [sor], M.Record ("uri", in_path "s")))))) in let rec build_intersect_obj = function [] -> M.Pattern (M.Const ["[.]*"]) | [hd] -> build_select_obj hd | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl) in let rec build_intersect_rel = function [] -> M.Ref(M.Const []) | [hd] -> build_select_rel hd | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl) in let rec build_intersect_sort = function [] -> M.Ref(M.Const []) | [hd] -> build_select_sort hd | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl) in let build_intersect = function (* let tostring_sort (a,b,c) = let b1 = string_of_int b in (a,b1,c) in let tostring_rel (a,b) = let b1 = string_of_int b in (a,b1) in*) (* let (l1,l2,l3) = must in match (l1,l2,l3) with *) l1,[],[] -> build_intersect_obj l1 | [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*) build_intersect_rel l2 | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*) build_intersect_sort l3 | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*) M.Intersect (build_intersect_obj l1, build_intersect_rel l2) | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in *) M.Intersect (build_intersect_obj l1, build_intersect_sort l3) | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in let lsort = List.map tostring_sort l3 in*) M.Intersect (build_intersect_rel l2, build_intersect_sort l3) | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in let lsort = List.map tostring_sort l3 in *) M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3) in let q_in = build_intersect must_use in let q_select = M.Select ("uri0", q_in, q_where can_use) in (* variables for can restrictions *) let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in let rec q_let_s sor n = match sor with [] -> q_let_u | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u) | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1)) in (* let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *) let rec q_let_ds sdep n = match sdep with [] | [None] -> q_let_s sor 1 | (None)::tl -> q_let_ds tl (n+1) | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1) | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1)) in (* let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in *) let rec q_let_dr rdep n = match rdep with [] | [None] -> q_let_ds sdep 1 | (None)::tl -> q_let_dr tl (n+1) | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1) | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1)) in (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*) let rec q_let_do odep n = match odep with [] | [None] -> q_let_dr rdep 1 | (None)::tl -> q_let_do tl (n+1) | [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1) | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1)) in (* let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in *) let rec q_let_ps spos n = match spos with [] -> q_let_do odep 1 | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1) | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1)) in (* let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *) let rec q_let_pr rpos n = match rpos with [] -> q_let_ps spos 1 | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1) | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1)) in (* let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *) let rec q_let_po opos n = match opos with [] -> q_let_pr rpos 1 | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1) | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1)) in (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*) let query = (M.Ref (M.RefOf (q_let_po opos 1))) in print_endline "### "; MQueryUtil.text_of_query print_string query "\n"; flush stdout; query