From 0fe4d837191de481184cc995558ca3774253be0c Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 9 May 2017 18:13:57 +0200 Subject: refl_omega: more refactoring (e.g. IntSets instead of sorted lists) --- plugins/romega/refl_omega.ml | 259 +++++++++++++++++++++++-------------------- 1 file changed, 136 insertions(+), 123 deletions(-) (limited to 'plugins') diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index b3135a164..bb4ab37ff 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -14,6 +14,8 @@ module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver module Id = Names.Id +module IntSet = Int.Set +module IntHtbl = Hashtbl.Make(Int) (* \section{Useful functions and flags} *) (* Especially useful debugging functions *) @@ -40,10 +42,6 @@ type direction = Left of int | Right of int type occ_step = O_left | O_right | O_mono type occ_path = occ_step list -let occ_step_eq s1 s2 = match s1, s2 with -| O_left, O_left | O_right, O_right | O_mono, O_mono -> true -| _ -> false - (* chemin identifiant une proposition sous forme du nom de l'hypothèse et d'une liste de pas à partir de la racine de l'hypothèse *) type occurrence = {o_hyp : Id.t; o_path : occ_path} @@ -110,19 +108,19 @@ type environment = { mutable om_vars : (oformula * int) list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) - real_indices : (int,int) Hashtbl.t; + real_indices : int IntHtbl.t; mutable cnt_connectors : int; - equations : (int,oequation) Hashtbl.t; - constructors : (int, occurrence) Hashtbl.t + equations : oequation IntHtbl.t; + constructors : occurrence IntHtbl.t } (* \subsection{Solution tree} Définition d'une solution trouvée par Omega sous la forme d'un identifiant, d'un ensemble d'équation dont dépend la solution et d'une trace *) -(* La liste des dépendances est triée et sans redondance *) + type solution = { s_index : int; - s_equa_deps : int list; + s_equa_deps : IntSet.t; s_trace : action list } (* Arbre de solution résolvant complètement un ensemble de systèmes *) @@ -141,6 +139,26 @@ type context_content = CCHyp of occurrence | CCEqua of int +(** Some dedicated equality tests *) + +let occ_step_eq s1 s2 = match s1, s2 with +| O_left, O_left | O_right, O_right | O_mono, O_mono -> true +| _ -> false + +let rec oform_eq f f' = match f,f' with + | Oint i, Oint i' -> Bigint.equal i i' + | Oplus (f1,f2), Oplus (f1',f2') + | Omult (f1,f2), Omult (f1',f2') + | Ominus (f1,f2), Ominus (f1',f2') -> oform_eq f1 f1' && oform_eq f2 f2' + | Oopp f, Oopp f' -> oform_eq f f' + | Oatom a, Oatom a' -> Int.equal a a' + | Oufo f, Oufo f' -> oform_eq f f' + | _ -> false + +let dir_eq d d' = match d, d' with + | Left i, Left i' | Right i, Right i' -> Int.equal i i' + | _ -> false + (* \section{Specific utility functions to handle base types} *) (* Nom arbitraire de l'hypothèse codant la négation du but final *) let id_concl = Id.of_string "__goal__" @@ -148,9 +166,9 @@ let id_concl = Id.of_string "__goal__" (* Initialisation de l'environnement de réification de la tactique *) let new_environment () = { terms = []; props = []; om_vars = []; cnt_connectors = 0; - real_indices = Hashtbl.create 7; - equations = Hashtbl.create 7; - constructors = Hashtbl.create 7; + real_indices = IntHtbl.create 7; + equations = IntHtbl.create 7; + constructors = IntHtbl.create 7; } (* Génération d'un nom d'équation *) @@ -200,11 +218,10 @@ let display_omega_var i = Printf.sprintf "OV%d" i le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = - begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *) + try List.assoc_f oform_eq t env.om_vars with Not_found -> let v = new_omega_var () in env.om_vars <- (t,v) :: env.om_vars; v - end (* Ajout forcé d'un lien entre un terme et une variable Cas où la variable est créée par Omega et où il faut la lier après coup à un atome @@ -214,8 +231,8 @@ let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars (* Récupère le terme associé à une variable *) let unintern_omega env id = let rec loop = function - [] -> failwith "unintern" - | ((t,j)::l) -> if Int.equal id j then t else loop l in + | [] -> failwith "unintern" + | ((t,j)::l) -> if Int.equal id j then t else loop l in loop env.om_vars (* \subsection{Gestion des environnements de variable pour la réflexion} @@ -248,12 +265,11 @@ let get_prop v env = (* Ajout d'une equation dans l'environnement de reification *) let add_equation env e = let id = e.e_omega.id in - try let _ = Hashtbl.find env.equations id in () - with Not_found -> Hashtbl.add env.equations id e + if IntHtbl.mem env.equations id then () else IntHtbl.add env.equations id e (* accès a une equation *) let get_equation env id = - try Hashtbl.find env.equations id + try IntHtbl.find env.equations id with Not_found as e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e @@ -337,10 +353,10 @@ let coq_of_formula env t = (* \subsection{Oformula vers COQ reifié} *) let reified_of_atom env i = - try Hashtbl.find env.real_indices i + try IntHtbl.find env.real_indices i with Not_found -> Printf.printf "Atome %d non trouvé\n" i; - Hashtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; + IntHtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; raise Not_found let rec reified_of_formula env = function @@ -417,19 +433,19 @@ pour faire des opérations de normalisation sur les équations. *) (* Extraction des variables d'une équation. *) (* Chaque fonction retourne une liste triée sans redondance *) -let (@@) = List.merge_uniq compare +let (@@) = IntSet.union let rec vars_of_formula = function - | Oint _ -> [] + | Oint _ -> IntSet.empty | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) | Oopp e -> vars_of_formula e - | Oatom i -> [i] - | Oufo _ -> [] + | Oatom i -> IntSet.singleton i + | Oufo _ -> IntSet.empty let rec vars_of_equations = function - | [] -> [] + | [] -> IntSet.empty | e::l -> (vars_of_formula e.e_left) @@ (vars_of_formula e.e_right) @@ @@ -441,7 +457,7 @@ let rec vars_of_prop = function | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pprop _ | Ptrue | Pfalse -> [] + | Pprop _ | Ptrue | Pfalse -> IntSet.empty (* \subsection{Multiplication par un scalaire} *) @@ -694,7 +710,7 @@ and binprop env (neg2,depends,origin,path) let depends1 = if add_to_depends then Left i::depends else depends in let depends2 = if add_to_depends then Right i::depends else depends in if add_to_depends then - Hashtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; + IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; let t1' = oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = @@ -754,14 +770,14 @@ let reify_gl env gl = let hyps = Tacmach.New.pf_hyps_types gl in let hyps = List.map (fun (i,t) -> (i,EConstr.Unsafe.to_constr t)) hyps in let t_concl = - Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in + oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl in let t_lhyps = List.map (fun (i,t) -> i,oproposition_of_constr env (false,[],i,[]) gl t) hyps in let () = if !debug then display_gl env t_concl t_lhyps in - (id_concl,t_concl) :: t_lhyps + t_concl, t_lhyps let rec destruct_pos_hyp eqns = function | Pequa (_,e) -> [e :: eqns] @@ -841,38 +857,35 @@ let display_systems syst_list = calcul des hypothèses *) let rec hyps_used_in_trace = function + | [] -> IntSet.empty | act :: l -> - begin match act with - | HYP e -> [e.id] @@ (hyps_used_in_trace l) - | SPLIT_INEQ (_,(_,act1),(_,act2)) -> - hyps_used_in_trace act1 @@ hyps_used_in_trace act2 - | _ -> hyps_used_in_trace l - end - | [] -> [] + match act with + | HYP e -> IntSet.add e.id (hyps_used_in_trace l) + | SPLIT_INEQ (_,(_,act1),(_,act2)) -> + hyps_used_in_trace act1 @@ hyps_used_in_trace act2 + | _ -> hyps_used_in_trace l (* Extraction des variables déclarées dans une équation. Permet ensuite de les déclarer dans l'environnement de la procédure réflexive et éviter les créations de variable au vol *) let rec variable_stated_in_trace = function - | act :: l -> - begin match act with - | STATE action -> - (*i nlle_equa: afine, def: afine, eq_orig: afine, i*) - (*i coef: int, var:int i*) - action :: variable_stated_in_trace l - | SPLIT_INEQ (_,(_,act1),(_,act2)) -> - variable_stated_in_trace act1 @ variable_stated_in_trace act2 - | _ -> variable_stated_in_trace l - end | [] -> [] -;; + | act :: l -> + match act with + | STATE action -> + (*i nlle_equa: afine, def: afine, eq_orig: afine, i*) + (*i coef: int, var:int i*) + action :: variable_stated_in_trace l + | SPLIT_INEQ (_,(_,act1),(_,act2)) -> + variable_stated_in_trace act1 @ variable_stated_in_trace act2 + | _ -> variable_stated_in_trace l let add_stated_equations env tree = (* Il faut trier les variables par ordre d'introduction pour ne pas risquer de définir dans le mauvais ordre *) let stated_equations = - let cmpvar x y = Pervasives.(-) x.st_var y.st_var in + let cmpvar x y = Int.compare x.st_var y.st_var in let rec loop = function | Tree(_,t1,t2) -> List.merge cmpvar (loop t1) (loop t2) | Leaf s -> List.sort cmpvar (variable_stated_in_trace s.s_trace) @@ -904,22 +917,22 @@ let add_stated_equations env tree = arg, then second arg), unless you know what you're doing. *) let rec get_eclatement env = function - i :: r -> - let l = try (get_equation env i).e_depends with Not_found -> [] in - List.union Pervasives.(=) (List.rev l) (get_eclatement env r) | [] -> [] + | i :: r -> + let l = try (get_equation env i).e_depends with Not_found -> [] in + List.union dir_eq (List.rev l) (get_eclatement env r) let select_smaller l = - let comp (_,x) (_,y) = Pervasives.(-) (List.length x) (List.length y) in + let comp (_,x) (_,y) = Int.compare (List.length x) (List.length y) in try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller" let filter_compatible_systems required systems = let rec select = function - (x::l) -> - if List.mem x required then select l - else if List.mem (barre x) required then raise Exit - else x :: select l | [] -> [] + | (x::l) -> + if List.mem_f dir_eq x required then select l + else if List.mem_f dir_eq (barre x) required then raise Exit + else x :: select l in List.map_filter (function (sol, splits) -> @@ -935,46 +948,45 @@ let rec equas_of_solution_tree = function to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance Pfalse is decidable. So should not be used on conclusion (??) *) -let really_useful_prop l_equa c = - let rec real_of = function - Pequa(t,_) -> t - | Ptrue -> app coq_True [||] - | Pfalse -> app coq_False [||] - | Pnot t1 -> app coq_not [|real_of t1|] - | Por(_,t1,t2) -> app coq_or [|real_of t1; real_of t2|] - | Pand(_,t1,t2) -> app coq_and [|real_of t1; real_of t2|] - (* Attention : implications sur le lifting des variables à comprendre ! *) - | Pimp(_,t1,t2) -> Term.mkArrow (real_of t1) (real_of t2) - | Pprop t -> t in - let rec loop c = - match c with - Pequa(_,e) -> - if List.mem e.e_omega.id l_equa then Some c else None - | Ptrue -> None - | Pfalse -> None +let rec coq_of_oprop = function + | Pequa(t,_) -> t + | Ptrue -> app coq_True [||] + | Pfalse -> app coq_False [||] + | Pnot t1 -> app coq_not [|coq_of_oprop t1|] + | Por(_,t1,t2) -> app coq_or [|coq_of_oprop t1; coq_of_oprop t2|] + | Pand(_,t1,t2) -> app coq_and [|coq_of_oprop t1; coq_of_oprop t2|] + (* Attention : implications sur le lifting des variables à comprendre ! *) + | Pimp(_,t1,t2) -> Term.mkArrow (coq_of_oprop t1) (coq_of_oprop t2) + | Pprop t -> t + +let really_useful_prop equas c = + let rec loop c = match c with + | Pequa(_,e) -> if IntSet.mem e.e_omega.id equas then Some c else None | Pnot t1 -> - begin match loop t1 with None -> None | Some t1' -> Some (Pnot t1') end + begin match loop t1 with None -> None | Some t1' -> Some (Pnot t1') end | Por(i,t1,t2) -> binop (fun (t1,t2) -> Por(i,t1,t2)) t1 t2 | Pand(i,t1,t2) -> binop (fun (t1,t2) -> Pand(i,t1,t2)) t1 t2 | Pimp(i,t1,t2) -> binop (fun (t1,t2) -> Pimp(i,t1,t2)) t1 t2 - | Pprop t -> None + | Ptrue | Pfalse | Pprop _ -> None and binop f t1 t2 = begin match loop t1, loop t2 with None, None -> None | Some t1',Some t2' -> Some (f(t1',t2')) - | Some t1',None -> Some (f(t1',Pprop (real_of t2))) - | None,Some t2' -> Some (f(Pprop (real_of t1),t2')) - end in + | Some t1',None -> Some (f(t1',Pprop (coq_of_oprop t2))) + | None,Some t2' -> Some (f(Pprop (coq_of_oprop t1),t2')) + end + in match loop c with - None -> Pprop (real_of c) + | None -> Pprop (coq_of_oprop c) | Some t -> t let rec display_solution_tree ch = function Leaf t -> output_string ch (Printf.sprintf "%d[%s]" - t.s_index - (String.concat " " (List.map string_of_int t.s_equa_deps))) + t.s_index + (String.concat " " (List.map string_of_int + (IntSet.elements t.s_equa_deps)))) | Tree(i,t1,t2) -> Printf.fprintf ch "S%d(%a,%a)" i display_solution_tree t1 display_solution_tree t2 @@ -1024,8 +1036,11 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) let get_hyp env_hyp i = - try List.index0 Pervasives.(=) (CCEqua i) env_hyp - with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) + let rec loop count = function + | [] -> failwith (Printf.sprintf "get_hyp %d" i) + | CCEqua i' :: _ when Int.equal i i' -> count + | _ :: l -> loop (succ count) l + in loop 0 env_hyp let replay_history env env_hyp = let rec loop env_hyp t = @@ -1120,7 +1135,7 @@ let replay_history env env_hyp = let rec decompose_tree env ctxt = function Tree(i,left,right) -> let org = - try Hashtbl.find env.constructors i + try IntHtbl.find env.constructors i with Not_found -> failwith (Printf.sprintf "Cannot find constructor %d" i) in let (index,path) = find_path org ctxt in @@ -1132,12 +1147,12 @@ let rec decompose_tree env ctxt = function decompose_tree env (left_hyp::ctxt) left; decompose_tree env (right_hyp::ctxt) right |] | Leaf s -> - decompose_tree_hyps s.s_trace env ctxt s.s_equa_deps + decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps) and decompose_tree_hyps trace env ctxt = function [] -> app coq_e_solve [| replay_history env ctxt trace |] | (i::l) -> let equation = - try Hashtbl.find env.equations i + try IntHtbl.find env.equations i with Not_found -> failwith (Printf.sprintf "Cannot find equation %d" i) in let (index,path) = find_path equation.e_origin ctxt in @@ -1157,7 +1172,7 @@ l'extraction d'un ensemble minimal de solutions permettant la résolution globale du système et enfin construit la trace qui permet de faire rejouer cette solution par la tactique réflexive. *) -let resolution env full_reified_goal systems_list = +let resolution env (reified_concl,reified_hyps) systems_list = let num = ref 0 in let solve_system list_eq = let index = !num in @@ -1166,14 +1181,14 @@ let resolution env full_reified_goal systems_list = simplify_strong (new_omega_eq,new_omega_var,display_omega_var) system in - (* calcule les hypotheses utilisées pour la solution *) + (* Hypotheses used for this solution *) let vars = hyps_used_in_trace trace in - let splits = get_eclatement env vars in + let splits = get_eclatement env (IntSet.elements vars) in if !debug then begin Printf.printf "SYSTEME %d\n" index; display_action display_omega_var trace; print_string "\n Depend :"; - List.iter (fun i -> Printf.printf " %d" i) vars; + IntSet.iter (fun i -> Printf.printf " %d" i) vars; print_string "\n Split points :"; List.iter display_depend splits; Printf.printf "\n------------------------------------\n" @@ -1187,23 +1202,21 @@ let resolution env full_reified_goal systems_list = display_solution_tree stdout solution_tree; print_newline() end; - (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) - let useful_equa_id = equas_of_solution_tree solution_tree in - (* recupere explicitement ces equations *) - let equations = List.map (get_equation env) useful_equa_id in - let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in - let l_hyps = id_concl :: List.remove Id.equal id_concl l_hyps' in - let useful_hyps = - List.map - (fun id -> List.assoc_f Id.equal id full_reified_goal) l_hyps + (* Collect all hypotheses used in the solution tree *) + let useful_equa_ids = equas_of_solution_tree solution_tree in + let equations = List.map (get_equation env) (IntSet.elements useful_equa_ids) in - let useful_vars = - let really_useful_vars = vars_of_equations equations in - let concl_vars = - vars_of_prop (List.assoc_f Id.equal id_concl full_reified_goal) - in - really_useful_vars @@ concl_vars + let hyps_of_eqns = + List.fold_left (fun s e -> Id.Set.add e.e_origin.o_hyp s) Id.Set.empty in + let hyps = hyps_of_eqns equations in + let useful_hypnames = Id.Set.elements (Id.Set.remove id_concl hyps) in + let all_names = id_concl :: useful_hypnames in + let useful_hyptypes = + List.map (fun id -> List.assoc_f Id.equal id reified_hyps) useful_hypnames + in + let useful_vars = vars_of_equations equations @@ vars_of_prop reified_concl in + (* variables a introduire *) let to_introduce = add_stated_equations env solution_tree in let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in @@ -1212,13 +1225,14 @@ let resolution env full_reified_goal systems_list = (* L'environnement de base se construit en deux morceaux : - les variables des équations utiles (et de la conclusion) - les nouvelles variables declarées durant les preuves *) - let all_vars_env = useful_vars @ stated_vars in + let all_vars_env = (IntSet.elements useful_vars) @ stated_vars in let basic_env = let rec loop i = function - var :: l -> - let t = get_reified_atom env var in - Hashtbl.add env.real_indices var i; t :: loop (succ i) l - | [] -> [] in + | [] -> [] + | var :: l -> + let t = get_reified_atom env var in + IntHtbl.add env.real_indices var i; t :: loop (succ i) l + in loop 0 all_vars_env in let env_terms_reified = mk_list (Lazy.force Z.typ) basic_env in (* On peut maintenant généraliser le but : env est a jour *) @@ -1227,15 +1241,13 @@ let resolution env full_reified_goal systems_list = app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |]) to_introduce in - let reified_concl = - match useful_hyps with - (Pnot p) :: _ -> reified_of_proposition env p - | _ -> reified_of_proposition env Pfalse in + let reified_concl = reified_of_proposition env reified_concl in let l_reified_terms = - (List.map + List.map (fun p -> - reified_of_proposition env (really_useful_prop useful_equa_id p)) - (List.tl useful_hyps)) in + reified_of_proposition env (really_useful_prop useful_equa_ids p)) + useful_hyptypes + in let env_props_reified = mk_plist env.props in let reified_goal = mk_list (Lazy.force coq_proposition) @@ -1251,7 +1263,7 @@ let resolution env full_reified_goal systems_list = | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |] | (O_right :: l) -> app coq_p_right [| loop l |] in let correct_index = - let i = List.index0 Id.equal e.e_origin.o_hyp l_hyps in + let i = List.index0 Id.equal e.e_origin.o_hyp all_names in (* PL: it seems that additionally introduced hyps are in the way during normalization, hence this index shifting... *) if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce) @@ -1261,13 +1273,13 @@ let resolution env full_reified_goal systems_list = mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in let initial_context = - List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) (List.tl l_hyps) in + List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames in let context = CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize - (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps)) >> + (l_generalize_arg @ List.map EConstr.mkVar useful_hypnames) >> Tactics.change_concl reified >> Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> @@ -1287,10 +1299,11 @@ let total_reflexive_omega_tactic = rst_omega_var (); try let env = new_environment () in - let full_reified_goal = reify_gl env gl in + let (concl,hyps) as reified_goal = reify_gl env gl in + let full_reified_goal = (id_concl,Pnot concl) :: hyps in let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; - resolution env full_reified_goal systems_list + resolution env reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" end } -- cgit v1.2.3