diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e3674fae0e..79db4a9c45 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -247,7 +247,8 @@ let add_equation env e = (* accès a une equation *) let get_equation env id = try Hashtbl.find env.equations id - with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e + with Not_found as e -> + Printf.printf "Omega Equation %d non trouvée\n" id; raise e (* Affichage des termes réifiés *) let rec oprint ch = function @@ -349,7 +350,8 @@ let rec reified_of_formula env = function app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |] let reified_of_formula env f = - begin try reified_of_formula env f with e -> oprint stderr f; raise e end + try reified_of_formula env f + with reraise -> oprint stderr f; raise reraise let rec reified_of_proposition env = function Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) -> @@ -380,8 +382,8 @@ let rec reified_of_proposition env = function | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] let reified_of_proposition env f = - begin try reified_of_proposition env f - with e -> pprint stderr f; raise e end + try reified_of_proposition env f + with reraise -> pprint stderr f; raise reraise (* \subsection{Omega vers COQ réifié} *) @@ -397,11 +399,8 @@ let reified_of_omega env body constant = List.fold_right mk_coeff body coeff_constant let reified_of_omega env body c = - begin try - reified_of_omega env body c - with e -> - display_eq display_omega_var (body,c); raise e - end + try reified_of_omega env body c + with reraise -> display_eq display_omega_var (body,c); raise reraise (* \section{Opérations sur les équations} Ces fonctions préparent les traces utilisées par la tactique réfléchie @@ -930,8 +929,12 @@ let filter_compatible_systems required systems = if List.mem x required then select l else if List.mem (barre x) required then raise Exit else x :: select l - | [] -> [] in - List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems + | [] -> [] + in + List.map_filter + (function (sol, splits) -> + try Some (sol, select splits) with Exit -> None) + systems let rec equas_of_solution_tree = function Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) @@ -1000,10 +1003,11 @@ let rec solve_with_constraints all_solutions path = let weighted = filter_compatible_systems path all_solutions in let (winner_sol,winner_deps) = try select_smaller weighted - with e -> + with reraise -> Printf.printf "%d - %d\n" (List.length weighted) (List.length all_solutions); - List.iter display_depend path; raise e in + List.iter display_depend path; raise reraise + in build_tree winner_sol (List.rev path) winner_deps let find_path {o_hyp=id;o_path=p} env = |