+(** splits a list of goals in three groups: closed propositional goals,
+ open propositional goals and non proposotional goals *)
+
+let split proof l =
+ let _,metasenv,_,_ = proof in
+ List.fold_left
+ (fun (c,o,z,n) g ->
+ try
+ let (_, ey, ty) = CicUtil.lookup_meta g metasenv in
+ let ty_sort,u =
+ CicTypeChecker.type_of_aux' metasenv ey ty CicUniv.empty_ugraph in
+ let b,_ =
+ CicReduction.are_convertible ey (Cic.Sort Cic.Prop) ty_sort u in
+ if b then
+ (if CicUtil.is_meta_closed ty then
+ (g::c,o,z,n)
+ else
+ (c,g::o,z,n))
+ else (c,o,z,g::n)
+ with
+ CicUtil.Meta_not_found _ -> (c,o,g::z,n)
+ )
+ ([],[],[],[]) l
+;;
+
+let my_weight dbd sign proof g =
+ let res =
+ search_theorems_in_context (proof,g) in
+ (* @
+ (List.map snd (MetadataQuery.experimental_hint
+ ~dbd ~facts:false ?signature:sign (proof,g))) in *)
+ List.fold_left
+ (fun n (_,(_,l)) -> n+(List.length l)+1)
+ 0 res
+;;
+
+let add_weight dbd sign proof =
+ List.map (function g -> (g,my_weight dbd sign proof g))
+
+;;
+
+
+(* let reorder_goals dbd sign proof goals =
+ List.rev goals *)
+
+(* let reorder_goals dbd sign proof goals =
+ let (c,o,z,n) = split proof goals
+ in c@o@n@z *)
+
+let reorder_goals dbd sign proof goals =
+ let (c,o,z,n) = split proof goals in
+ match o with
+ [] -> c@n@z
+ | [g] ->c@[g]@n@z
+ | l ->
+ let l' = add_weight dbd sign proof l in
+ c@(List.map fst (List.sort (fun (_,x) (_,y) -> x - y) l'))@n@z
+
+let compare_goals 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
+ CicUniv.empty_ugraph in
+ let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
+ CicUniv.empty_ugraph in
+ let prop1 =
+ let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
+ CicUniv.empty_ugraph in
+ if b then 0 else 1
+ in
+ let prop2 =
+ let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
+ CicUniv.empty_ugraph in
+ if b then 0 else 1
+ in
+ prop1 - prop2
+
+
+let new_search_theorems f dbd proof goal depth sign =