From 7509f5c8eab84fda5a9029329c6b70758259765f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 17 May 2017 13:39:59 +0200 Subject: ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT --- plugins/omega/omega.ml | 4 ---- 1 file changed, 4 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 334b03de1..f655c176f 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -587,10 +587,6 @@ let rec depend relie_on accu = function end | [] -> relie_on, accu -let solve (new_eq_id,new_eq_var,print_var) system = - try let _ = simplify new_eq_id false system in failwith "no contradiction" - with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) - let negation (eqs,ineqs) = let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in let normal = function -- cgit v1.2.3 From 107ef2db28b7abc75afe32350e7c2eb3c8ddbe82 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 19 May 2017 13:24:16 +0200 Subject: refl_omega: some code refactoring --- plugins/omega/omega.ml | 2 +- plugins/romega/refl_omega.ml | 255 ++++++++++++++++++++++--------------------- 2 files changed, 129 insertions(+), 128 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index f655c176f..2a018fa3f 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -96,7 +96,7 @@ type afine = { type state_action = { st_new_eq : afine; - st_def : afine; + st_def : afine; (* /!\ this represents [st_def = st_var] *) st_orig : afine; st_coef : bigint; st_var : int } diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index a8741b690..6ef53837c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -89,7 +89,7 @@ and oequation = { e_depends: direction list; (* liste des points de disjonction dont dépend l'accès à l'équation avec la direction (branche) pour y accéder *) - e_omega: afine (* la fonction normalisée *) + e_omega: OmegaSolver.afine (* normalized formula *) } (* \subsection{Proof context} @@ -121,7 +121,7 @@ type environment = { type solution = { s_index : int; s_equa_deps : IntSet.t; - s_trace : action list } + s_trace : OmegaSolver.action list } (* Arbre de solution résolvant complètement un ensemble de systèmes *) type solution_tree = @@ -362,12 +362,15 @@ let reified_of_proposition env f = try reified_of_oprop env f with reraise -> pprint stderr f; raise reraise +let reified_of_eq env (l,r) = + app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |] + (* \subsection{Omega vers COQ réifié} *) let reified_of_omega env body constant = let coeff_constant = app coq_t_int [| Z.mk constant |] in - let mk_coeff {c=c; v=v} t = + let mk_coeff {c;v} t = let coef = app coq_t_mult [| reified_of_formula env (Oatom v); @@ -422,8 +425,8 @@ let rec vars_of_prop = function *) type nformula = - { coefs : (atom_index * bigint) list; - cst : bigint } + { coefs : (atom_index * Bigint.bigint) list; + cst : Bigint.bigint } let scale n { coefs; cst } = { coefs = List.map (fun (v,k) -> (v,k*n)) coefs; @@ -667,46 +670,53 @@ let rec hyps_used_in_trace = function 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 *) +(** Retreive variables declared as extra equations during resolution + and declare them into the environment. + We should consider these variables in their introduction order, + otherwise really bad things will happen. *) -let rec variable_stated_in_trace = function - | [] -> [] - | 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 = 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) - in loop tree - in - let add_env st = - (* On retransforme la définition de v en formule reifiée *) +let state_cmp x y = Int.compare x.st_var y.st_var + +module StateSet = + Set.Make (struct type t = state_action let compare = state_cmp end) + +let rec stated_in_trace = function + | [] -> StateSet.empty + | [SPLIT_INEQ (_,(_,t1),(_,t2))] -> + StateSet.union (stated_in_trace t1) (stated_in_trace t2) + | STATE action :: l -> StateSet.add action (stated_in_trace l) + | _ :: l -> stated_in_trace l + +let rec stated_in_tree = function + | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) + | Leaf s -> stated_in_trace s.s_trace + +let digest_stated_equations env tree = + let do_equation st (vars,gens,eqns,ids) = + (** We turn the definition of [v] + - into a reified formula : *) let v_def = oformula_of_omega st.st_def in - (* Notez que si l'ordre de création des variables n'est pas respecté, - * ca va planter *) + (** - into a concrete Coq formula + (this uses only older vars already in env) : *) let coq_v = coq_of_formula env v_def in + (** We then update the environment *) set_reified_atom st.st_var coq_v env; - (* Le terme qu'il va falloir introduire *) - let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in - (* sa représentation sous forme d'équation mais non réifié car on n'a pas - * l'environnement pour le faire correctement *) + (** The term we'll introduce *) + let term_to_generalize = + EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; coq_v|]) + in + (** Its representation as equation (but not reified yet, + we lack the proper env to do that). *) let term_to_reify = (v_def,Oatom st.st_var) in - (st.st_var, term_to_generalize,term_to_reify,st.st_def.id) in - List.map add_env stated_equations + (st.st_var::vars, + term_to_generalize::gens, + term_to_reify::eqns, + CCEqua st.st_def.id :: ids) + in + let (vars,gens,eqns,ids) = + StateSet.fold do_equation (stated_in_tree tree) ([],[],[],[]) + in + (List.rev vars, List.rev gens, List.rev eqns, List.rev ids) (* Calcule la liste des éclatements à réaliser sur les hypothèses nécessaires pour extraire une liste d'équations donnée *) @@ -740,46 +750,43 @@ let filter_compatible_systems required systems = systems let rec equas_of_solution_tree = function - Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) + | Tree(_,t1,t2) -> + (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) | Leaf s -> s.s_equa_deps -(* [really_useful_prop] pushes useless props in a new Pprop variable *) -(* Things get shorter, but may also get wrong, since a Prop is considered - to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance - Pfalse is decidable. So should not be used on conclusion (??) *) - -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|] - | Pimp(_,t1,t2) -> - (* No lifting here, since Omega only works on closed propositions. *) - Term.mkArrow (coq_of_oprop t1) (coq_of_oprop t2) - | Pprop t -> t +(** [maximize_prop] pushes useless props in a new Pprop atom. + The reified formulas get shorter, but be careful with decidabilities. + For instance, anything that contains a Pprop is considered to be + undecidable in [ReflOmegaCore], whereas a Pfalse for instance at + the same spot will lead to a decidable formula. + In particular, do not use this function on the conclusion. + Even in hypotheses, we could probably build pathological examples + that romega won't handle correctly, but they should be pretty rare. +*) -let really_useful_prop equas c = +let maximize_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 - | 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 - | 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 (coq_of_oprop t2))) - | None,Some t2' -> Some (f(Pprop (coq_of_oprop t1),t2')) - end - in - match loop c with - | None -> Pprop (coq_of_oprop c) - | Some t -> t + | Pequa(t,e) -> if IntSet.mem e.e_omega.id equas then c else Pprop t + | Pnot t -> + (match loop t with + | Pprop p -> Pprop (app coq_not [|p|]) + | t' -> Pnot t') + | Por(i,t1,t2) -> + (match loop t1, loop t2 with + | Pprop p1, Pprop p2 -> Pprop (app coq_or [|p1;p2|]) + | t1', t2' -> Por(i,t1',t2')) + | Pand(i,t1,t2) -> + (match loop t1, loop t2 with + | Pprop p1, Pprop p2 -> Pprop (app coq_and [|p1;p2|]) + | t1', t2' -> Pand(i,t1',t2')) + | Pimp(i,t1,t2) -> + (match loop t1, loop t2 with + | Pprop p1, Pprop p2 -> Pprop (Term.mkArrow p1 p2) (* no lift (closed) *) + | t1', t2' -> Pimp(i,t1',t2')) + | Ptrue -> Pprop (app coq_True [||]) + | Pfalse -> Pprop (app coq_False [||]) + | Pprop _ -> c + in loop c let rec display_solution_tree ch = function Leaf t -> @@ -938,6 +945,28 @@ and decompose_tree_hyps trace env ctxt = function (CCEqua equation.e_omega.id :: ctxt) l in app coq_e_extract [|mk_nat index; mk_direction_list path; cont |] +let solve_system env index list_eq = + let system = List.map (fun eq -> eq.e_omega) list_eq in + let trace = + OmegaSolver.simplify_strong + (new_omega_eq,new_omega_var,display_omega_var) + system + in + (* Hypotheses used for this solution *) + let vars = hyps_used_in_trace trace 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 :"; + IntSet.iter (fun i -> Printf.printf " %d" i) vars; + print_string "\n Split points :"; + List.iter display_depend splits; + Printf.printf "\n------------------------------------\n" + end; + {s_index = index; s_trace = trace; s_equa_deps = vars}, splits + (* \section{La fonction principale} *) (* Cette fonction construit la trace pour la procédure de décision réflexive. A partir des résultats @@ -947,36 +976,14 @@ 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 unsafe env (reified_concl,reified_hyps) systems_list = - let num = ref 0 in - let solve_system list_eq = - let index = !num in - let system = List.map (fun eq -> eq.e_omega) list_eq in - let trace = - simplify_strong - (new_omega_eq,new_omega_var,display_omega_var) - system in - (* Hypotheses used for this solution *) - let vars = hyps_used_in_trace trace 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 :"; - IntSet.iter (fun i -> Printf.printf " %d" i) vars; - print_string "\n Split points :"; - List.iter display_depend splits; - Printf.printf "\n------------------------------------\n" - end; - incr num; - {s_index = index; s_trace = trace; s_equa_deps = vars}, splits in if !debug then Printf.printf "\n====================================\n"; - let all_solutions = List.map solve_system systems_list in + let all_solutions = List.mapi (solve_system env) systems_list in let solution_tree = solve_with_constraints all_solutions [] in if !debug then begin display_solution_tree stdout solution_tree; print_newline() end; - (* Collect all hypotheses used in the solution tree *) + (** 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 @@ -990,37 +997,35 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = 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 - let l_generalize_arg = List.map (fun (_,t,_,_) -> EConstr.of_constr t) to_introduce in - let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in - (* 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 = (IntSet.elements useful_vars) @ stated_vars in - let basic_env = + (** Parts coming from equations introduced by omega: *) + let stated_vars, l_generalize_arg, to_reify_stated, hyp_stated_vars = + digest_stated_equations env solution_tree + in + (** The final variables are either coming from: + - useful hypotheses (and conclusion) + - equations introduced during resolution *) + let all_vars_env = (IntSet.elements useful_vars) @ stated_vars + in + (** We prepare the renumbering from all variables to useful ones. + Since [all_var_env] is sorted, this renumbering will preserve + order: this way, the equations in ReflOmegaCore will have + the same normal forms as here. *) + let reduced_term_env = let rec loop i = function | [] -> [] | 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 - (* Since [all_vars_env] is sorted, this renumbering of variables - should have preserved order *) - 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 *) - let l_reified_stated = - List.map (fun (_,_,(l,r),_) -> - app coq_p_eq [| reified_of_formula env l; - reified_of_formula env r |]) - to_introduce in + mk_list (Lazy.force Z.typ) (loop 0 all_vars_env) + in + (** The environment [env] (and especially [env.real_indices]) is now + ready for the coming reifications: *) + let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in let reified_concl = reified_of_proposition env reified_concl in let l_reified_terms = List.map - (fun p -> - reified_of_proposition env (really_useful_prop useful_equa_ids p)) + (fun p -> reified_of_proposition env (maximize_prop useful_equa_ids p)) useful_hyptypes in let env_props_reified = mk_plist env.props in @@ -1029,7 +1034,7 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (l_reified_stated @ l_reified_terms) in let reified = app coq_interp_sequent - [| reified_concl;env_props_reified;env_terms_reified;reified_goal|] + [| reified_concl;env_props_reified;reduced_term_env;reified_goal|] in let initial_context = List.map (fun id -> CCHyp{o_hyp=id;o_path=[]}) useful_hypnames in @@ -1067,7 +1072,3 @@ let total_reflexive_omega_tactic unsafe = resolution unsafe env reified_goal systems_list with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" end } - -(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) - - -- cgit v1.2.3