--- /dev/null
+(* 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
projects / helm.git / blobdiff