- split metadata type in metadata and constraints. Metadata are computed

[helm.git] / helm / ocaml / metadata / metadataConstraints.ml

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 3a985deb9304c34537029fab103294cc9648198a..314ceba5345e616b18a80120d4f3f9cffc460712 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -39,10 +39,32 @@ type cardinality_condition =
 
 let tbln n = "table" ^ string_of_int n
 
+(*
 let add_depth_constr depth_opt cur_tbl where =
   match depth_opt with
   | None -> where
   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
+*)
+
+let mk_positions positions cur_tbl =
+  "(" ^
+  String.concat " or "
+    (List.map
+      (fun pos ->
+        let pos_str = MetadataPp.pp_position_tag pos in
+        match pos with
+        | `InBody
+        | `InConclusion
+        | `InHypothesis
+        | `MainConclusion None
+        | `MainHypothesis None ->
+            sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
+        | `MainConclusion (Some d)
+        | `MainHypothesis (Some d) ->
+            sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
+              cur_tbl pos_str cur_tbl d)
+      (positions :> MetadataTypes.position list)) ^
+  ")"
 
 let add_card_constr tbl (n,from,where) = function
   | None -> (n,from,where)
@@ -62,51 +84,45 @@ let add_card_constr tbl (n,from,where) = function
         where))
 
 let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card
-  (metadata: MetadataTypes.metadata list)
+  (metadata: MetadataTypes.constr list)
 =
   if (metadata = []) && concl_card = None && full_card = None then
     failwith "MetadataQuery.at_least: no constraints given";
   let add_constraint (n,from,where) metadata =
     let cur_tbl = tbln n in
     match metadata with
-    | `Obj (uri, pos, depth_opt) ->
+    | `Obj (uri, positions) ->
         let tbl = MetadataTypes.obj_tbl in
-        let pos_str = MetadataPp.pp_position pos in
         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
         let where =
-          (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
           (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
+          mk_positions positions cur_tbl ::
           (if n=0 then []
           else [sprintf "table0.source = %s.source" cur_tbl]) @
           where
         in
-        let where = add_depth_constr depth_opt cur_tbl where in
         ((n+1), from, where)
-    | `Rel (pos, depth) ->
+    | `Rel positions ->
         let tbl = MetadataTypes.rel_tbl in
-        let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
         let where =
-          (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
+          mk_positions positions cur_tbl ::
           (if n=0 then []
           else [sprintf "table0.source = %s.source" cur_tbl]) @
           where
         in
-        let where = add_depth_constr (Some depth) cur_tbl where in
         ((n+1), from, where)
-    | `Sort (sort, pos, depth) ->
+    | `Sort (sort, positions) ->
         let tbl = MetadataTypes.sort_tbl in
-        let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
         let sort_str = MetadataPp.pp_sort sort in
         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
         let where =
-          (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
+          mk_positions positions cur_tbl ::
           (if n=0 then []
           else [sprintf "table0.source = %s.source" cur_tbl]) @
           where
         in
-        let where = add_depth_constr (Some depth) cur_tbl where in
         ((n+1), from, where)
   in
   let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
@@ -347,8 +363,8 @@ let union l =
   drop_repetitions (List.sort Pervasives.compare (List.concat l))
 
 let must_of_prefix m s =
-  let s' = List.map (fun u -> `Obj (u, `InConclusion, None)) s in
-  `Obj (m, `MainConclusion, None) :: s'
+  let s' = List.map (fun u -> `Obj (u, [`InConclusion])) s in
+  `Obj (m, [`MainConclusion None]) :: s'
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"