From: Enrico Tassi Date: Mon, 16 May 2005 15:21:00 +0000 (+0000) Subject: fixed instance X-Git-Tag: single_binding~59 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e6023677f34f426d32a1bdbe391978ea7f7c44f6;p=helm.git fixed instance --- diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index da4f271b5..fe972b0bb 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -71,10 +71,11 @@ let mk_positions positions cur_tbl = | `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) + | `MainConclusion (Some r) + | `MainHypothesis (Some r) -> + let depth = MetadataPp.pp_relation r in + sprintf "(%s.h_position = \"%s\" and %s.h_depth %s)" + cur_tbl pos_str cur_tbl depth) (positions :> MetadataTypes.position list)) ^ ")" diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml index 0ffe5980d..f9a26637d 100644 --- a/helm/ocaml/metadata/metadataExtractor.ml +++ b/helm/ocaml/metadata/metadataExtractor.ml @@ -63,8 +63,8 @@ module S = MetadataSet let unopt = function Some x -> x | None -> assert false let incr_depth = function - | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1)) - | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1)) + | `MainConclusion (Some (Eq depth)) -> `MainConclusion (Some (Eq (depth + 1))) + | `MainHypothesis (Some (Eq depth)) -> `MainHypothesis (Some (Eq (depth + 1))) | _ -> assert false let var_has_body uri = @@ -103,7 +103,7 @@ let compute_term pos term = | Cic.Prod (_, source, target) -> (match pos with | `MainConclusion _ -> - let set = aux (`MainHypothesis (Some 0)) set source in + let set = aux (`MainHypothesis (Some (Eq 0))) set source in aux (incr_depth pos) set target | `MainHypothesis _ -> let set = aux `InHypothesis set source in @@ -300,8 +300,8 @@ let rec compute_var pos uri = List.flatten (List.map (compute_var (next_pos pos)) params) in (match pos with - | `MainHypothesis (Some 0) -> - let pos = `MainHypothesis (Some (depth_offset params)) in + | `MainHypothesis (Some (Eq 0)) -> + let pos = `MainHypothesis (Some (Eq (depth_offset params))) in (compute pos ~body:None ~ty)@metadata_of_vars | `InHypothesis -> (compute pos ~body:None ~ty)@metadata_of_vars @@ -313,23 +313,23 @@ let compute_obj uri = match o with | Cic.Variable (_, body, ty, params, _) | Cic.Constant (_, body, ty, params, _) -> - let pos = `MainConclusion (Some (depth_offset params)) in + let pos = `MainConclusion (Some (Eq (depth_offset params))) in let metadata = compute pos ~body ~ty in let metadata_of_vars = List.flatten - (List.map (compute_var (`MainHypothesis (Some 0))) params) + (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) in [UriManager.string_of_uri uri, UriManager.name_of_uri uri,metadata @ metadata_of_vars] | Cic.InductiveDefinition (types, params, _, _) -> - let pos = `MainConclusion(Some (depth_offset params)) in + let pos = `MainConclusion(Some (Eq (depth_offset params))) in let metadata_of_vars = List.flatten - (List.map (compute_var (`MainHypothesis (Some 0))) params) in + (List.map (compute_var (`MainHypothesis (Some (Eq 0)))) params) in let metadata = compute_ind pos ~uri ~types in List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata | Cic.CurrentProof _ -> assert false -let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty +let compute ~body ~ty = compute (`MainConclusion (Some (Eq 0))) ~body ~ty diff --git a/helm/ocaml/metadata/metadataPp.ml b/helm/ocaml/metadata/metadataPp.ml index 63a1a0955..fdbbaf071 100644 --- a/helm/ocaml/metadata/metadataPp.ml +++ b/helm/ocaml/metadata/metadataPp.ml @@ -27,10 +27,18 @@ open Printf open MetadataTypes +let pp_relation r = + match r with + | Eq i -> sprintf "= %d" i + | Ge i -> sprintf ">= %d" i + | Gt i -> sprintf "> %d" i + | Le i -> sprintf "<= %d" i + | Lt i -> sprintf "< %d" i + let pp_position = function - | `MainConclusion (Some d) -> sprintf "MainConclusion(%d)" d + | `MainConclusion (Some d) -> sprintf "MainConclusion(%s)" (pp_relation d) | `MainConclusion None -> sprintf "MainConclusion" - | `MainHypothesis (Some d) -> sprintf "MainHypothesis(%d)" d + | `MainHypothesis (Some d) -> sprintf "MainHypothesis(%s)" (pp_relation d) | `MainHypothesis None -> "MainHypothesis" | `InConclusion -> "InConclusion" | `InHypothesis -> "InHypothesis" @@ -43,14 +51,16 @@ let pp_position_tag = function | `InHypothesis -> inhyp_pos | `InBody -> inbody_pos -let columns_of_position = function - | `MainConclusion (Some d) -> `String mainconcl_pos, `Int d +let columns_of_position pos = + match pos with + | `MainConclusion (Some (Eq d)) -> `String mainconcl_pos, `Int d | `MainConclusion None -> `String mainconcl_pos, `Null - | `MainHypothesis (Some d) -> `String mainhyp_pos, `Int d + | `MainHypothesis (Some (Eq d)) -> `String mainhyp_pos, `Int d | `MainHypothesis None -> `String mainhyp_pos, `Null | `InConclusion -> `String inconcl_pos, `Null | `InHypothesis -> `String inhyp_pos, `Null | `InBody -> `String inbody_pos, `Null + | _ -> assert false (* let metadata_ns = "http://www.cs.unibo.it/helm/schemas/schema-helm" @@ -67,10 +77,10 @@ let columns_of_metadata_aux ~about metadata = (fun (sort_cols, rel_cols, obj_cols) metadata -> match metadata with | `Sort (s, p) -> - let (p, d) = columns_of_position p in + let (p, d) = columns_of_position (p :> position) in [source; p; d; sort s] :: sort_cols, rel_cols, obj_cols | `Rel p -> - let (p, d) = columns_of_position p in + let (p, d) = columns_of_position (p :> position) in sort_cols, [source; p; d] :: rel_cols, obj_cols | `Obj (o, p) -> let (p, d) = columns_of_position p in @@ -102,3 +112,4 @@ let pp_columns ?(sep = "\n") (sort_cols, rel_cols, obj_cols) = [ "Obj" ] @ List.map Dbi.sdebug (obj_cols :> Dbi.sql_t list list)) *) + diff --git a/helm/ocaml/metadata/metadataPp.mli b/helm/ocaml/metadata/metadataPp.mli index 8566ed727..d9ef885ed 100644 --- a/helm/ocaml/metadata/metadataPp.mli +++ b/helm/ocaml/metadata/metadataPp.mli @@ -45,3 +45,5 @@ val columns_of_metadata: val pp_columns: ?sep:string -> t list list * t list list * t list list -> string *) +val pp_relation: MetadataTypes.relation -> string + diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml index 5284d96b5..334553083 100644 --- a/helm/ocaml/metadata/metadataTypes.ml +++ b/helm/ocaml/metadata/metadataTypes.ml @@ -32,9 +32,16 @@ let mainhyp_pos = position_prefix ^ "MainHypothesis" let inhyp_pos = position_prefix ^ "InHypothesis" let inbody_pos = position_prefix ^ "InBody" +type relation = + | Eq of int + | Le of int + | Lt of int + | Ge of int + | Gt of int + type main_position = - [ `MainConclusion of int option (* Pi depth *) - | `MainHypothesis of int option (* Pi depth *) + [ `MainConclusion of relation option (* Pi depth *) + | `MainHypothesis of relation option (* Pi depth *) ] type position = diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli index 73f9a703e..5a2456de1 100644 --- a/helm/ocaml/metadata/metadataTypes.mli +++ b/helm/ocaml/metadata/metadataTypes.mli @@ -29,9 +29,16 @@ val mainhyp_pos : string val inhyp_pos : string val inbody_pos : string +type relation = + | Eq of int + | Le of int + | Lt of int + | Ge of int + | Gt of int + type main_position = - [ `MainConclusion of int option (* Pi depth *) - | `MainHypothesis of int option (* Pi depth *) + [ `MainConclusion of relation option (* Pi depth *) + | `MainHypothesis of relation option (* Pi depth *) ] type position = diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index d0b384e75..a232c67e4 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -342,8 +342,8 @@ let experimental_hint let elim ~dbd uri = let constraints = [`Rel [`MainConclusion None]; - `Sort (Cic.Prop,[`MainHypothesis (Some 1)]); - `Obj (uri,[`MainHypothesis (Some 0)]); + `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Gt 1))]); + `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]); `Obj (uri,[`InHypothesis]); ] in @@ -374,67 +374,83 @@ let instance ~dbd t = let no_concl = MetadataDb.count_distinct `Conclusion metadata in let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in let no_full = MetadataDb.count_distinct `Statement metadata in - let is_dummy = - function - `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" - | _ -> true in - let rec look_for_dummy_main = - function - [] -> None - | `Obj(s,`MainConclusion (Some d))::_ - when ((String.sub s 0 10) = "cic:/dummy") -> - let len = String.length s in - let dummy_index = int_of_string (String.sub s 11 (len-11)) in - let dummy_type = List.nth types dummy_index in - Some (d,dummy_type) - | _::l -> look_for_dummy_main l in + let is_dummy = function + | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" + | _ -> true + in + let rec look_for_dummy_main = function + | [] -> None + | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ + when ((String.sub s 0 10) = "cic:/dummy") -> + let len = String.length s in + let dummy_index = int_of_string (String.sub s 11 (len-11)) in + let dummy_type = List.nth types dummy_index in + Some (d,dummy_type) + | _::l -> look_for_dummy_main l + in match (look_for_dummy_main metadata) with - None-> - prerr_endline "Caso None"; - (* no dummy in main position *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints + | None-> + prerr_endline "Caso None"; + (* no dummy in main position *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints | Some (depth, dummy_type) -> prerr_endline - (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); - (* a dummy in main position *) - let metadata_for_dummy_type = - MetadataExtractor.compute ~body:None ~ty:dummy_type in - (* Let us skip this for the moment - let main_of_dummy_type = - look_for_dummy_main metadata_for_dummy_type in *) - let metadata = List.filter is_dummy metadata in - let constraints = List.map MetadataTypes.constr_of_metadata metadata in - let metadata_for_dummy_type = - List.filter is_dummy metadata_for_dummy_type in - let constraints_for_dummy_type = - List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in - (* start with the dummy constant in main conlusion *) - let from = ["refObj as table0"] in - let where = - [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; - sprintf "table0.h_depth = %d" depth] in - let (n,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:2) - (2,from,where) constraints in - let concl_card = Some (MetadataConstraints.Eq no_concl) in - let full_card = Some (MetadataConstraints.Eq no_full) in - let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in - let (n,from,where) = - MetadataConstraints.add_all_constr - (n,from,where) concl_card full_card diff in - (* join with the constraints over the type of the constant *) - let where = - (sprintf "table0.h_occurrence = table%d.source" n)::where in - let (m,from,where) = - List.fold_left - (MetadataConstraints.add_constraint ~start:n) - (n,from,where) constraints_for_dummy_type in - Constr.exec ~dbd (m,from,where) + (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); + (* a dummy in main position *) + let metadata_for_dummy_type = + MetadataExtractor.compute ~body:None ~ty:dummy_type in + (* Let us skip this for the moment + let main_of_dummy_type = + look_for_dummy_main metadata_for_dummy_type in *) + let metadata = List.filter is_dummy metadata in + let constraints = List.map MetadataTypes.constr_of_metadata metadata in + let metadata_for_dummy_type = + List.filter is_dummy metadata_for_dummy_type in + let metadata_for_dummy_type, depth' = + (* depth' = the depth of the A -> A -> Prop *) + List.fold_left (fun (acc,dep) c -> + match c with + | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) -> + (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i + | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type + in + let constraints_for_dummy_type = + List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in + (* start with the dummy constant in main conlusion *) + let from = ["refObj as table0"] in + let where = + [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos; + sprintf "table0.h_depth >= %d" depth] in + let (n,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:2) + (2,from,where) constraints in + let concl_card = Some (MetadataConstraints.Eq no_concl) in + let full_card = Some (MetadataConstraints.Eq no_full) in + let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in + let (n,from,where) = + MetadataConstraints.add_all_constr + (n,from,where) concl_card full_card diff in + (* join with the constraints over the type of the constant *) + let where = + (sprintf "table0.h_occurrence = table%d.source" n)::where in + let where = + sprintf "table0.h_depth - table%d.h_depth = %d" + n (depth - depth')::where + in + let (m,from,where) = + List.fold_left + (MetadataConstraints.add_constraint ~start:n) + (n,from,where) constraints_for_dummy_type in + Constr.exec ~dbd (m,from,where)