]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed instance
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 May 2005 15:21:00 +0000 (15:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 16 May 2005 15:21:00 +0000 (15:21 +0000)
helm/ocaml/metadata/metadataConstraints.ml
helm/ocaml/metadata/metadataExtractor.ml
helm/ocaml/metadata/metadataPp.ml
helm/ocaml/metadata/metadataPp.mli
helm/ocaml/metadata/metadataTypes.ml
helm/ocaml/metadata/metadataTypes.mli
helm/ocaml/tactics/metadataQuery.ml

index da4f271b5ae6be34936d6c14cd02b4b6a21a80ab..fe972b0bbd471a667777aff9d8c158998fcf385d 100644 (file)
@@ -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)) ^
   ")"
 
index 0ffe5980d183cd7ad8a4d8807c2b3adb5d0a55eb..f9a26637d968db9c4e7cc3129d7f1223af035e55 100644 (file)
@@ -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 
index 63a1a0955a55b8ee1f5189aaa3b58f3672c1e06d..fdbbaf071f133afc377845f71ccfdbf844dce824 100644 (file)
@@ -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))
 *)
 
+
index 8566ed727917f522516bb7a361d07f6a6289dfe3..d9ef885ed43277034d085581eea41023ef7e8fd8 100644 (file)
@@ -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
+
index 5284d96b5dd48377585ce62d8133cd0459dd824e..3345530833da879e46b45713f81cae3b390451b1 100644 (file)
@@ -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 =
index 73f9a703e8625eb659fdbcc1daacf6fb11757dd9..5a2456de10fb2b1a62da4ebb431174807b18ddc6 100644 (file)
@@ -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 =
index d0b384e750cfc92ba922fc9136637d294350fb57..a232c67e4e621244ebae425102b1303b6c6608b1 100644 (file)
@@ -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)