- reimplemented tacticChaser and friends in term of Metadata module and friends

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 13a73b561b6e477b164c1f008e351b832e9bdb17..619af110b73afe54387826ed1f22af6ec96e2739 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -29,7 +29,7 @@ module Constr = MetadataConstraints
 
 let locate ~(dbh:Dbi.connection) name =
   let query =
-    dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\""
+    dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
       MetadataTypes.name_tbl name)
   in
   query#execute [];
@@ -73,7 +73,7 @@ let filter_uris_forward ~dbh (main, constants) uris =
   let full_signature =
     List.fold_right Constr.StringSet.add main_uris constants
   in
-  List.filter (Constr.at_most ~dbh full_signature) uris
+  List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris
 
 let filter_uris_backward ~dbh signature uris =
   let siguris =
@@ -81,6 +81,22 @@ let filter_uris_backward ~dbh signature uris =
   in
   intersect uris siguris
 
+let compare_goal_list proof goal1 goal2 =
+  let _,metasenv,_,_ = proof in
+  let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
+  let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
+  let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+  let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+  let prop1 =
+    if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
+    else 1
+  in
+  let prop2 =
+    if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
+    else 1
+  in
+  prop1 - prop2
+
 let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
@@ -109,11 +125,29 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
     end else
       filter_uris_backward ~dbh (main, other_constants) uris
   in
-  List.map
-    (fun uri ->
-      (uri,
-       ProofEngineTypes.apply_tactic
-        (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
-        status))
-    uris
+prerr_endline "URIS";
+List.iter prerr_endline uris;
+  let rec aux = function
+    | [] -> []
+    | uri :: tl ->
+        (let status' =
+            try
+              let (proof, goal_list) =
+                ProofEngineTypes.apply_tactic
+                  (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
+                  status
+              in
+              let goal_list =
+                List.stable_sort (compare_goal_list proof) goal_list
+              in
+              Some (uri, (proof, goal_list))
+            with ProofEngineTypes.Fail _ -> None
+          in
+          match status' with
+          | None -> aux tl
+          | Some status' ->
+              prerr_endline ("HO APPLICATO " ^ uri);
+              status' :: aux tl)
+  in
+  aux uris