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

  from cic objects while constraints are used to query the database

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 "\'") "\\'"
 

diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli
index 59cb0427eb26edbaff92dab9481a92be55bae6d7..ec6d81f38d35a53c9f7abfc5a03658c5825a646f 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.mli
+++ b/helm/ocaml/metadata/metadataConstraints.mli
@@ -57,7 +57,7 @@ val at_least:
   dbh:Dbi.connection ->
   ?concl_card:cardinality_condition ->
   ?full_card:cardinality_condition ->
-  MetadataTypes.metadata list ->
+  MetadataTypes.constr list ->
     string list
 
 val signature_of: Cic.term -> term_signature

diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 9f9b721f69f60184fa47244088ee9595a4e1ea57..d06e9a4bf5197b0da61bc34efe335e984222bfc3 100644 (file)
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -28,19 +28,19 @@ open Printf
 open MetadataTypes
 
 let is_main_pos = function
-  | `MainConclusion
-  | `MainHypothesis -> true
+  | `MainConclusion _
+  | `MainHypothesis _ -> true
   | _ -> false
 
 let main_pos (pos: position): main_position =
   match pos with
-  | `MainConclusion -> `MainConclusion
-  | `MainHypothesis -> `MainHypothesis
+  | `MainConclusion depth -> `MainConclusion depth
+  | `MainHypothesis depth -> `MainHypothesis depth
   | _ -> assert false
 
 let next_pos = function
-  | `MainConclusion -> `InConclusion
-  | `MainHypothesis -> `InHypothesis
+  | `MainConclusion _ -> `InConclusion
+  | `MainHypothesis _ -> `InHypothesis
   | pos -> pos
 
 let string_of_uri = UriManager.string_of_uri
@@ -50,8 +50,8 @@ module OrderedMetadata =
     type t = MetadataTypes.metadata
     let compare m1 m2 = (* ignore universes in Cic.Type sort *)
       match (m1, m2) with
-      | `Sort (Cic.Type _, p1, d1), `Sort (Cic.Type _, p2, d2) ->
-          Pervasives.compare (p1, d2) (p2, d2)
+      | `Sort (Cic.Type _, pos1), `Sort (Cic.Type _, pos2) ->
+          Pervasives.compare pos1 pos2
       | _ -> Pervasives.compare m1 m2
   end
 
@@ -63,14 +63,15 @@ module S = MetadataSet
 let unopt = function Some x -> x | None -> assert false
 
 let incr_depth = function
-  | None -> assert false
-  | Some x -> Some (x + 1)
+  | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
+  | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
+  | _ -> assert false
 
 let compute_term pos term =
-  let rec aux (pos: position) pi_depth set = function
+  let rec aux (pos: position) set = function
     | Cic.Rel _ ->
         if is_main_pos pos then
-          S.add (`Rel (main_pos pos, unopt pi_depth)) set
+          S.add (`Rel (main_pos pos)) set
         else
           set
     | Cic.Var _ -> set
@@ -79,96 +80,96 @@ let compute_term pos term =
           (fun set context ->
             match context with
             | None -> set
-            | Some term -> aux pos pi_depth set term)
+            | Some term -> aux pos set term)
           set
           local_context
     | Cic.Sort sort ->
         if is_main_pos pos then
-          S.add (`Sort (sort, main_pos pos, unopt pi_depth)) set
+          S.add (`Sort (sort, main_pos pos)) set
         else
           set
     | Cic.Implicit _ -> assert false
     | Cic.Cast (term, ty) ->
         (* TODO consider also ty? *)
-        aux pos pi_depth set term
+        aux pos set term
     | Cic.Prod (_, source, target) ->
         (match pos with
-        | `MainConclusion ->
-            let set = aux `MainHypothesis (Some 0) set source in
-            aux pos (incr_depth pi_depth) set target
-        | `MainHypothesis ->
-            let set = aux `InHypothesis None set source in
-            aux pos (incr_depth pi_depth) set target
+        | `MainConclusion _ ->
+            let set = aux (`MainHypothesis (Some 0)) set source in
+            aux (incr_depth pos) set target
+        | `MainHypothesis _ ->
+            let set = aux `InHypothesis set source in
+            aux (incr_depth pos) set target
         | `InConclusion
         | `InHypothesis
         | `InBody ->
-            let set = aux pos None set source in
-            aux pos None set target)
+            let set = aux pos set source in
+            aux pos set target)
     | Cic.Lambda (_, source, target) ->
         assert (not (is_main_pos pos));
-        let set = aux pos None set source in
-        aux pos None set target
+        let set = aux pos set source in
+        aux pos set target
     | Cic.LetIn (_, term, target) ->
         if is_main_pos pos then
-          aux pos pi_depth set (CicSubstitution.subst term target)
+          aux pos set (CicSubstitution.subst term target)
         else
-          let set = aux pos None set term in
-          aux pos None set target
+          let set = aux pos set term in
+          aux pos set target
     | Cic.Appl [] -> assert false
     | Cic.Appl (hd :: tl) ->
-        let set = aux pos pi_depth set hd in
+        let set = aux pos set hd in
         List.fold_left
-          (fun set term -> aux (next_pos pos) None set term)
+          (fun set term -> aux (next_pos pos) set term)
           set tl
     | Cic.Const (uri, subst) ->
-        let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in
+        let set = S.add (`Obj (string_of_uri uri, pos)) set in
         List.fold_left
-          (fun set (_, term) -> aux (next_pos pos) None set term)
+          (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutInd (uri, typeno, subst) ->
         let uri = UriManager.string_of_uriref (uri, [typeno]) in
-        let set = S.add (`Obj (uri, pos, pi_depth)) set in
-        List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
+        let set = S.add (`Obj (uri, pos)) set in
+        List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutConstruct (uri, typeno, consno, subst) ->
         let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
-        let set = S.add (`Obj (uri, pos, pi_depth)) set in
-        List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
+        let set = S.add (`Obj (uri, pos)) set in
+        List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
           set subst
     | Cic.MutCase (uri, _, outtype, term, pats) ->
         let pos = next_pos pos in
-        let set = aux pos None set term in
-        let set = aux pos None set outtype in
-        List.fold_left (fun set term -> aux pos None set term) set pats
+        let set = aux pos set term in
+        let set = aux pos set outtype in
+        List.fold_left (fun set term -> aux pos set term) set pats
     | Cic.Fix (_, funs) ->
         let pos = next_pos pos in
         List.fold_left
           (fun set (_, _, ty, body) ->
-            let set = aux pos None set ty in
-            aux pos None set body)
+            let set = aux pos set ty in
+            aux pos set body)
           set funs
     | Cic.CoFix (_, funs) ->
         let pos = next_pos pos in
         List.fold_left
           (fun set (_, ty, body) ->
-            let set = aux pos None set ty in
-            aux pos None set body)
+            let set = aux pos set ty in
+            aux pos set body)
           set funs
   in
-  aux pos (Some 0) S.empty term
+  aux pos S.empty term
 
 let compute_type uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
     (UriManager.string_of_uriref (uri, [typeno]), name,
-    S.elements (compute_term `MainConclusion ty))
+    S.elements (compute_term (`MainConclusion (Some 0)) ty))
   in
   let constructors_metadata =
     List.map
       (fun (name, term) ->
         incr consno;
         let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
-        (uri, name, S.elements (compute_term `MainConclusion term)))
+        (uri, name, S.elements (compute_term (`MainConclusion (Some 0)) term)))
       constructors
   in
   type_metadata :: constructors_metadata
@@ -178,7 +179,7 @@ let compute_ind ~uri ~types =
   List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
 
 let compute ~body ~ty =
-  let type_metadata = compute_term `MainConclusion ty in
+  let type_metadata = compute_term (`MainConclusion (Some 0)) ty in
   let body_metadata =
     match body with
     | None -> S.empty
@@ -188,7 +189,7 @@ let compute ~body ~ty =
     S.fold
       (fun metadata uris ->
         match metadata with
-        | `Obj (uri, _, _) -> StringSet.add uri uris
+        | `Obj (uri, _) -> StringSet.add uri uris
         | _ -> uris)
       type_metadata StringSet.empty
   in
@@ -196,7 +197,7 @@ let compute ~body ~ty =
     (S.union
       (S.filter
         (function
-          | `Obj (uri, _, _) when StringSet.mem uri uris -> false
+          | `Obj (uri, _) when StringSet.mem uri uris -> false
           | _ -> true)
         body_metadata)
       type_metadata)

diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml
index 5b8ae4e7a55c2ca88c6ef2102b0437344f2e1756..2ce9f22267d05548d00160e203de347eb65de3ea 100644 (file)
--- a/helm/ocaml/metadata/metadataPp.ml
+++ b/helm/ocaml/metadata/metadataPp.ml
@@ -26,14 +26,34 @@
 open Printf
 
 let pp_position = function
-  | `MainConclusion -> "MainConclusion"
-  | `MainHypothesis -> "MainHypothesis"
+  | `MainConclusion (Some d) -> sprintf "MainConclusion(%d)" d
+  | `MainConclusion None -> sprintf "MainConclusion"
+  | `MainHypothesis (Some d) -> sprintf "MainHypothesis(%d)" d
+  | `MainHypothesis None -> "MainHypothesis"
   | `InConclusion -> "InConclusion"
   | `InHypothesis -> "InHypothesis"
   | `InBody -> "InBody"
 
+let pp_position_tag = function
+  | `MainConclusion _ -> "MainConclusion"
+  | `MainHypothesis _ -> "MainHypothesis"
+  | `InConclusion -> "InConclusion"
+  | `InHypothesis -> "InHypothesis"
+  | `InBody -> "InBody"
+
+let columns_of_position = function
+  | `MainConclusion (Some d) -> `String "MainConclusion", `Int d
+  | `MainConclusion None -> `String "MainConclusion", `Null
+  | `MainHypothesis (Some d) -> `String "MainHypothesis", `Int d
+  | `MainHypothesis None -> `String "MainHypothesis", `Null
+  | `InConclusion -> `String "InConclusion", `Null
+  | `InHypothesis -> `String "InHypothesis", `Null
+  | `InBody -> `String "InBody", `Null
+
+(*
 let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm"
 let uri_of_pos pos = String.concat "#" [metadata_ns; pp_position pos]
+*)
 
 let pp_sort = function
   | Cic.Prop -> "Prop"
@@ -44,22 +64,22 @@ let pp_sort = function
 type t = [ `Int of int | `String of string | `Null ]
 
 let columns_of_metadata ~about metadatas =
-  let position p = `String (pp_position p) in
   let sort s = `String (pp_sort s) in
   let source = `String about in
-  let depth d = `Int d in
-  let depth_opt = function None -> `Null | Some d -> `Int d in
   let occurrence u = `String u in
   List.fold_left
     (fun (sort_cols, rel_cols, obj_cols) metadata ->
       match metadata with
-      | `Sort (s, p, d) ->
-          [source; position p; depth d; sort s] :: sort_cols, rel_cols, obj_cols
-      | `Rel (p, d) ->
-          sort_cols, [source; position p; depth d] :: rel_cols, obj_cols
-      | `Obj (o, p, d) ->
+      | `Sort (s, p) ->
+          let (p, d) = columns_of_position p in
+          [source; p; d; sort s] :: sort_cols, rel_cols, obj_cols
+      | `Rel p ->
+          let (p, d) = columns_of_position p in
+          sort_cols, [source; p; d] :: rel_cols, obj_cols
+      | `Obj (o, p) ->
+          let (p, d) = columns_of_position p in
           sort_cols, rel_cols,
-          [source; occurrence o; position p; depth_opt d] :: obj_cols)
+          [source; occurrence o; p; d] :: obj_cols)
     ([], [], []) metadatas
 
 let columns_of_ind_metadata ind_metadata =

diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli
index ba987dca3223fa7375fd1983488ab31c63673453..14a98ba413a265e6331ed58cc92cd82e435d6502 100644 (file)
--- a/helm/ocaml/metadata/metadataPp.mli
+++ b/helm/ocaml/metadata/metadataPp.mli
@@ -26,6 +26,8 @@
 (** metadata -> string *)
 
 val pp_position: MetadataTypes.position -> string
+val pp_position_tag: MetadataTypes.position -> string
+(* val pp_constr: MetadataTypes.constr -> string *)
 val pp_sort: Cic.sort -> string
 
 (** Pretty printer and OCamlDBI friendly interface *)

diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml
index 0db48f299dde415b8e8584556527d163167f8a8f..a5bbfaf097ad128f280fde538769b1a54907c6eb 100644 (file)
--- a/helm/ocaml/metadata/metadataTypes.ml
+++ b/helm/ocaml/metadata/metadataTypes.ml
@@ -23,7 +23,10 @@
  * http://helm.cs.unibo.it/
  *)
 
-type main_position = [ `MainConclusion | `MainHypothesis ]
+type main_position =
+  [ `MainConclusion of int option (* Pi depth *)
+  | `MainHypothesis of int option (* Pi depth *)
+  ]
 
 type position =
   [ main_position
@@ -35,11 +38,22 @@ type position =
 type pi_depth = int
 
 type metadata =
-  [ `Sort of Cic.sort * main_position * pi_depth
-  | `Rel of main_position * pi_depth
-  | `Obj of string * position * pi_depth option
+  [ `Sort of Cic.sort * main_position
+  | `Rel of main_position
+  | `Obj of string * position
+  ]
+
+type constr =
+  [ `Sort of Cic.sort * main_position list
+  | `Rel of main_position list
+  | `Obj of string * position list
   ]
 
+let constr_of_metadata: metadata -> constr = function
+  | `Sort (sort, pos) -> `Sort (sort, [pos])
+  | `Rel pos -> `Rel [pos]
+  | `Obj (uri, pos) -> `Obj (uri, [pos])
+
 let sort_tbl = "refSort"
 let rel_tbl = "refRel"
 let obj_tbl = "refObj"