- 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