From 9cd69dd86ed337478461241d497265ccc59f819a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 21 Oct 2004 07:25:27 +0000 Subject: [PATCH] - split metadata type in metadata and constraints. Metadata are computed from cic objects while constraints are used to query the database --- helm/ocaml/metadata/metadataConstraints.ml | 46 ++++++---- helm/ocaml/metadata/metadataConstraints.mli | 2 +- helm/ocaml/metadata/metadataExtractor.ml | 99 +++++++++++---------- helm/ocaml/metadata/metadataPp.ml | 42 ++++++--- helm/ocaml/metadata/metadataPp.mli | 2 + helm/ocaml/metadata/metadataTypes.ml | 22 ++++- 6 files changed, 133 insertions(+), 80 deletions(-) diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 3a985deb9..314ceba53 100644 --- 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 59cb0427e..ec6d81f38 100644 --- 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 9f9b721f6..d06e9a4bf 100644 --- 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 5b8ae4e7a..2ce9f2226 100644 --- 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 ba987dca3..14a98ba41 100644 --- 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 0db48f299..a5bbfaf09 100644 --- 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" -- 2.39.2