From 32a45f819c88c73487ea42a15e7391169ad14db2 Mon Sep 17 00:00:00 2001 From: Matteo Selmi Date: Tue, 25 May 2004 07:07:19 +0000 Subject: [PATCH] written a new sort function to postpone the resolution of some types of the goals --- helm/ocaml/tactics/tacticChaser.ml | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index e917555ce..561997f6f 100644 --- 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 ;; -- 2.39.2