written a new sort function to postpone the resolution of some types of the goals

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index e917555ce3e63f87a4052c224321f5416205f4c2..561997f6f86b317ba415c4a36adb82917a13d38a 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -143,10 +143,6 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
     (* TODO ristretto per ragioni di efficienza *)
     List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
   *)
-  (*
-  let uris =
-    List.filter  (fun _,uri -> not (Pcre.pmatch ~pat:"^cic:/Coq/ring" uri)) uris in
-  *)
   (* concl_cost are the costants in the conclusion of the proof 
      while hyp_const are the constants in the hypothesis *)
   let (_,concl_const) = NewConstraints.constants_of ty in
@@ -191,6 +187,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
      filter_out uris
    in
      prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris'));
+   
      uris'
 ;;
 
@@ -214,7 +211,6 @@ let choose_must list_of_must only =
      List.nth list_of_must 0 *)
 
 let  searchTheorems mqi_handle (proof,goal) =
-(*prerr_endline "1";*)
   let subproofs =
     matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
  let res =
@@ -229,6 +225,25 @@ let  searchTheorems mqi_handle (proof,goal) =
     subproofs
  in
   (* now we may drop the prefix tag *)
- List.map snd res
+ (*let res' =
+   List.map snd res in*)
+ let order_goal_list proof goal1 goal2 =
+   let _,metasenv,_,_ = proof in
+   let (ey1, ty1) =  
+          let (_, ey ,ty) = CicUtil.lookup_meta goal1 metasenv in
+           (ey, ty) in
+   let (ey2, ty2) =  
+          let (_, ey ,ty) = CicUtil.lookup_meta goal2 metasenv in
+           (ey, ty) in 
+   let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
+   let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey1 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 in
+ List.map (fun (level,(proof,goallist)) -> (proof, (List.stable_sort (order_goal_list proof) goallist))) res  
 ;;