-(** 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