Some modifications due to instance.

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 5f83dd608b28df8760760ffb8e725e46c7e654a0..d0b384e750cfc92ba922fc9136637d294350fb57 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -351,30 +351,90 @@ let elim ~dbd uri =
 
 
 let fill_with_dummy_constants t =
-  let rec aux i =
+  let rec aux i types =
     function
        Cic.Lambda (n,s,t) -> 
          let dummy_uri = 
            UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
-         (aux (i+1) (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
-      | t -> t
-  in aux 0 t
+           (aux (i+1) (s::types)
+              (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
+      | t -> t,types
+  in 
+  let t,types = aux 0 [] t in
+  t, List.rev types
       
 let instance ~dbd t =
-  let t' = fill_with_dummy_constants t in 
+  let t',types = fill_with_dummy_constants t in 
   let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
+  List.iter 
+    (fun x -> 
+       prerr_endline 
+        (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
+    metadata;
   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 no_full = MetadataDb.count_distinct `Statement metadata in
   let is_dummy =
       function
          `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" 
-       | _ -> false in
-  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
+       | _ -> 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
+  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
+    | 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)