diff options
Diffstat (limited to 'contrib/romega/refl_omega.ml')
-rw-r--r-- | contrib/romega/refl_omega.ml | 285 |
1 files changed, 106 insertions, 179 deletions
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index e7e7b3c5..fc4f7a8f 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -6,10 +6,7 @@ *************************************************************************) -(* The addition on int, since it while be hidden soon by the one on BigInt *) - -let (+.) = (+) - +open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -26,65 +23,6 @@ let pp i = print_int i; print_newline (); flush stdout (* More readable than the prefix notation *) let (>>) = Tacticals.tclTHEN -(* [list_index t l = i] \eqv $nth l i = t \wedge \forall j < i nth l j != t$ *) - -let list_index t = - let rec loop i = function - | (u::l) -> if u = t then i else loop (succ i) l - | [] -> raise Not_found in - loop 0 - -(* [list_uniq l = filter_i (x i -> nth l (i-1) != x) l] *) -let list_uniq l = - let rec uniq = function - x :: ((y :: _) as l) when x = y -> uniq l - | x :: l -> x :: uniq l - | [] -> [] in - uniq (List.sort compare l) - -(* $\forall x. mem x (list\_union l1 l2) \eqv x \in \{l1\} \cup \{l2\}$ *) -let list_union l1 l2 = - let rec loop buf = function - x :: r -> if List.mem x l2 then loop buf r else loop (x :: buf) r - | [] -> buf in - loop l2 l1 - -(* $\forall x. - mem \;\; x \;\; (list\_intersect\;\; l1\;\;l2) \eqv x \in \{l1\} - \cap \{l2\}$ *) -let list_intersect l1 l2 = - let rec loop buf = function - x :: r -> if List.mem x l2 then loop (x::buf) r else loop buf r - | [] -> buf in - loop [] l1 - -(* cartesian product. Elements are lists and are concatenated. - $cartesian [x_1 ... x_n] [y_1 ... y_p] = [x_1 @ y_1, x_2 @ y_1 ... x_n @ y_1 , x_1 @ y_2 ... x_n @ y_p]$ *) - -let rec cartesien l1 l2 = - let rec loop = function - (x2 :: r2) -> List.map (fun x1 -> x1 @ x2) l1 @ loop r2 - | [] -> [] in - loop l2 - -(* remove element e from list l *) -let list_remove e l = - let rec loop = function - x :: l -> if x = e then loop l else x :: loop l - | [] -> [] in - loop l - -(* equivalent of the map function but no element is added when the function - raises an exception (and the computation silently continues) *) -let map_exc f = - let rec loop = function - (x::l) -> - begin match try Some (f x) with exc -> None with - Some v -> v :: loop l | None -> loop l - end - | [] -> [] in - loop - let mkApp = Term.mkApp (* \section{Types} @@ -174,6 +112,7 @@ type environment = { (* \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; @@ -280,7 +219,7 @@ let unintern_omega env id = calcul des variables utiles. *) let add_reified_atom t env = - try list_index t env.terms + try list_index0 t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -291,7 +230,7 @@ let get_reified_atom env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try list_index t env.props + try list_index0 t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -362,13 +301,6 @@ let omega_of_oformula env kind = (* \subsection{Omega vers Oformula} *) -let reified_of_atom env i = - try Hashtbl.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; - raise Not_found - let rec oformula_of_omega env af = let rec loop = function | ({v=v; c=n}::r) -> @@ -382,20 +314,27 @@ let app f v = mkApp(Lazy.force f,v) let rec coq_of_formula env t = let rec loop = function - | Oplus (t1,t2) -> app coq_Zplus [| loop t1; loop t2 |] - | Oopp t -> app coq_Zopp [| loop t |] - | Omult(t1,t2) -> app coq_Zmult [| loop t1; loop t2 |] - | Oint v -> mk_Z v + | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |] + | Oopp t -> app Z.opp [| loop t |] + | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |] + | Oint v -> Z.mk v | Oufo t -> loop t | Oatom var -> (* attention ne traite pas les nouvelles variables si on ne les * met pas dans env.term *) get_reified_atom env var - | Ominus(t1,t2) -> app coq_Zminus [| loop t1; loop t2 |] in + | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in loop t (* \subsection{Oformula vers COQ reifié} *) +let reified_of_atom env i = + try Hashtbl.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; + raise Not_found + let rec reified_of_formula env = function | Oplus (t1,t2) -> app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |] @@ -403,7 +342,7 @@ let rec reified_of_formula env = function app coq_t_opp [| reified_of_formula env t |] | Omult(t1,t2) -> app coq_t_mult [| reified_of_formula env t1; reified_of_formula env t2 |] - | Oint v -> app coq_t_int [| mk_Z v |] + | Oint v -> app coq_t_int [| Z.mk v |] | Oufo t -> reified_of_formula env t | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |] | Ominus(t1,t2) -> @@ -448,12 +387,12 @@ let reified_of_proposition env f = let reified_of_omega env body constant = let coeff_constant = - app coq_t_int [| mk_Z constant |] in + app coq_t_int [| Z.mk constant |] in let mk_coeff {c=c; v=v} t = let coef = app coq_t_mult [| reified_of_formula env (unintern_omega env v); - app coq_t_int [| mk_Z c |] |] in + app coq_t_int [| Z.mk c |] |] in app coq_t_plus [|coef; t |] in List.fold_right mk_coeff body coeff_constant @@ -469,22 +408,34 @@ Ces fonctions préparent les traces utilisées par la tactique réfléchie pour faire des opérations de normalisation sur les équations. *) (* \subsection{Extractions des variables d'une équation} *) -(* Extraction des variables d'une équation *) +(* Extraction des variables d'une équation. *) +(* Chaque fonction retourne une liste triée sans redondance *) + +let (@@) = list_merge_uniq compare let rec vars_of_formula = function | Oint _ -> [] - | 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) + | 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 _ -> [] -let vars_of_equations l = - let rec loop = function - e :: l -> vars_of_formula e.e_left @ vars_of_formula e.e_right @ loop l - | [] -> [] in - list_uniq (List.sort compare (loop l)) +let rec vars_of_equations = function + | [] -> [] + | e::l -> + (vars_of_formula e.e_left) @@ + (vars_of_formula e.e_right) @@ + (vars_of_equations l) + +let rec vars_of_prop = function + | Pequa(_,e) -> vars_of_equations [e] + | Pnot p -> vars_of_prop p + | 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 -> [] (* \subsection{Multiplication par un scalaire} *) @@ -715,36 +666,23 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = (* \section{Compilation des hypothèses} *) -let is_scalar t = - let rec aux t = match destructurate t with - | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2 - | Kapp(("Zopp"|"Zsucc"),[t]) -> aux t - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize_number t in true - | _ -> false in - try aux t with _ -> false - let rec oformula_of_constr env t = - try match destructurate t with - | Kapp("Zplus",[t1;t2]) -> binop env (fun x y -> Oplus(x,y)) t1 t2 - | Kapp("Zminus",[t1;t2]) -> binop env (fun x y -> Ominus(x,y)) t1 t2 - | Kapp("Zmult",[t1;t2]) when is_scalar t1 or is_scalar t2 -> - binop env (fun x y -> Omult(x,y)) t1 t2 - | Kapp("Zopp",[t]) -> Oopp(oformula_of_constr env t) - | Kapp("Zsucc",[t]) -> Oplus(oformula_of_constr env t, Oint one) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - begin try Oint(recognize_number t) - with _ -> Oatom (add_reified_atom t env) end - | _ -> - Oatom (add_reified_atom t env) - with e when Logic.catchable_exception e -> - Oatom (add_reified_atom t env) - -and binop env c t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in - c t1' t2' - -and binprop env (neg2,depends,origin,path) + match Z.parse_term t with + | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2 + | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2 + | Tmult (t1,t2) when Z.is_scalar t1 || Z.is_scalar t2 -> + binop env (fun x y -> Omult(x,y)) t1 t2 + | Topp t -> Oopp(oformula_of_constr env t) + | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) + | Tnum n -> Oint n + | _ -> Oatom (add_reified_atom t env) + +and binop env c t1 t2 = + let t1' = oformula_of_constr env t1 in + let t2' = oformula_of_constr env t2 in + c t1' t2' + +and binprop env (neg2,depends,origin,path) add_to_depends neg1 gl c t1 t2 = let i = new_connector_id env in let depends1 = if add_to_depends then Left i::depends else depends in @@ -767,40 +705,32 @@ and mk_equation env ctxt c connector t1 t2 = Pequa (c,omega) and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = - try match destructurate c with - | Kapp("eq",[typ;t1;t2]) - when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> - mk_equation env ctxt c Eq t1 t2 - | Kapp("Zne",[t1;t2]) -> - mk_equation env ctxt c Neq t1 t2 - | Kapp("Zle",[t1;t2]) -> - mk_equation env ctxt c Leq t1 t2 - | Kapp("Zlt",[t1;t2]) -> - mk_equation env ctxt c Lt t1 t2 - | Kapp("Zge",[t1;t2]) -> - mk_equation env ctxt c Geq t1 t2 - | Kapp("Zgt",[t1;t2]) -> - mk_equation env ctxt c Gt t1 t2 - | Kapp("True",[]) -> Ptrue - | Kapp("False",[]) -> Pfalse - | Kapp("not",[t]) -> - let t' = - oproposition_of_constr - env (not negated, depends, origin,(O_mono::path)) gl t in - Pnot t' - | Kapp("or",[t1;t2]) -> + match Z.parse_rel gl c with + | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2 + | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2 + | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2 + | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2 + | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2 + | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2 + | Rtrue -> Ptrue + | Rfalse -> Pfalse + | Rnot t -> + let t' = + oproposition_of_constr + env (not negated, depends, origin,(O_mono::path)) gl t in + Pnot t' + | Ror (t1,t2) -> binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2 - | Kapp("and",[t1;t2]) -> + | Rand (t1,t2) -> binprop env ctxt negated negated gl (fun i x y -> Pand(i,x,y)) t1 t2 - | Kimp(t1,t2) -> + | Rimp (t1,t2) -> binprop env ctxt (not negated) (not negated) gl (fun i x y -> Pimp(i,x,y)) t1 t2 - | Kapp("iff",[t1;t2]) -> + | Riff (t1,t2) -> binprop env ctxt negated negated gl (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c - with e when Logic.catchable_exception e -> Pprop c (* Destructuration des hypothèses et de la conclusion *) @@ -881,7 +811,7 @@ let destructurate_hyps syst = (i,t) :: l -> let l_syst1 = destructurate_pos_hyp i [] [] t in let l_syst2 = loop l in - cartesien l_syst1 l_syst2 + list_cartesian (@) l_syst1 l_syst2 | [] -> [[]] in loop syst @@ -924,9 +854,9 @@ let display_systems syst_list = let rec hyps_used_in_trace = function | act :: l -> begin match act with - | HYP e -> e.id :: hyps_used_in_trace l + | 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 act1 @@ hyps_used_in_trace act2 | _ -> hyps_used_in_trace l end | [] -> [] @@ -950,14 +880,15 @@ let rec variable_stated_in_trace = function ;; let add_stated_equations env tree = - let rec loop = function - Tree(_,t1,t2) -> - list_union (loop t1) (loop t2) - | Leaf s -> variable_stated_in_trace s.s_trace in (* Il faut trier les variables par ordre d'introduction pour ne pas risquer de définir dans le mauvais ordre *) let stated_equations = - List.sort (fun x y -> Pervasives.(-) x.st_var y.st_var) (loop tree) in + let cmpvar x y = Pervasives.(-) 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 v_def = oformula_of_omega env st.st_def in @@ -966,7 +897,7 @@ let add_stated_equations env tree = let coq_v = coq_of_formula env v_def in let v = add_reified_atom coq_v env in (* Le terme qu'il va falloir introduire *) - let term_to_generalize = app coq_refl_equal [|Lazy.force coq_Z; coq_v|] in + 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 *) let term_to_reify = (v_def,Oatom v) in @@ -978,10 +909,15 @@ let add_stated_equations env tree = (* Calcule la liste des éclatements à réaliser sur les hypothèses nécessaires pour extraire une liste d'équations donnée *) +(* PL: experimentally, the result order of the following function seems + _very_ crucial for efficiency. No idea why. Do not remove the List.rev + or modify the current semantics of Util.list_union (some elements of first + 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 l (get_eclatement env r) + list_union (List.rev l) (get_eclatement env r) | [] -> [] let select_smaller l = @@ -992,14 +928,13 @@ 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 if List.mem (barre x) required then failwith "Exit" else x :: select l | [] -> [] in - map_exc (function (sol,splits) -> (sol,select splits)) systems + map_succeed (function (sol,splits) -> (sol,select splits)) systems let rec equas_of_solution_tree = function - Tree(_,t1,t2) -> - list_union (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 *) @@ -1041,14 +976,6 @@ let really_useful_prop l_equa c = None -> Pprop (real_of c) | Some t -> t -let rec vars_of_prop = function - | Pequa(_,e) -> vars_of_equations [e] - | Pnot p -> vars_of_prop p - | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) - | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) - | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2) - | _ -> [] - let rec display_solution_tree ch = function Leaf t -> output_string ch @@ -1103,7 +1030,7 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) let get_hyp env_hyp i = - try list_index (CCEqua i) env_hyp + try list_index0 (CCEqua i) env_hyp with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) let replay_history env env_hyp = @@ -1116,7 +1043,7 @@ let replay_history env env_hyp = mk_nat (get_hyp env_hyp e2.id) |]) | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> mkApp (Lazy.force coq_s_div_approx, - [| mk_Z k; mk_Z d; + [| Z.mk k; Z.mk d; reified_of_omega env e2.body e2.constant; mk_nat (List.length e2.body); loop env_hyp l; mk_nat (get_hyp env_hyp e1.id) |]) @@ -1125,7 +1052,7 @@ let replay_history env env_hyp = let d = e1.constant - e2_constant * k in let e2_body = map_eq_linear (fun c -> c / k) e1.body in mkApp (Lazy.force coq_s_not_exact_divide, - [|mk_Z k; mk_Z d; + [|Z.mk k; Z.mk d; reified_of_omega env e2_body e2_constant; mk_nat (List.length e2_body); mk_nat (get_hyp env_hyp e1.id)|]) @@ -1134,7 +1061,7 @@ let replay_history env env_hyp = map_eq_linear (fun c -> c / k) e1.body in let e2_constant = floor_div e1.constant k in mkApp (Lazy.force coq_s_exact_divide, - [|mk_Z k; + [|Z.mk k; reified_of_omega env e2_body e2_constant; mk_nat (List.length e2_body); loop env_hyp l; mk_nat (get_hyp env_hyp e1.id)|]) @@ -1149,7 +1076,7 @@ let replay_history env env_hyp = and n2 = get_hyp env_hyp e2.id in let trace = shuffle_path k1 e1.body k2 e2.body in mkApp (Lazy.force coq_s_sum, - [| mk_Z k1; mk_nat n1; mk_Z k2; + [| Z.mk k1; mk_nat n1; Z.mk k2; mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |]) | CONSTANT_NOT_NUL(e,k) :: l -> mkApp (Lazy.force coq_s_constant_not_nul, @@ -1169,7 +1096,7 @@ let replay_history env env_hyp = Oplus (o_orig,Omult (Oplus (Oopp v,o_def), Oint m)) in let trace,_ = normalize_linear_term env body in mkApp (Lazy.force coq_s_state, - [| mk_Z m; trace; mk_nat n1; mk_nat n2; + [| Z.mk m; trace; mk_nat n1; mk_nat n2; loop (CCEqua new_eq.id :: env_hyp) l |]) | HYP _ :: l -> loop env_hyp l | CONSTANT_NUL e :: l -> @@ -1267,17 +1194,17 @@ let resolution env full_reified_goal systems_list = print_newline() end; (* calcule la liste de toutes les hypothèses utilisées dans l'arbre de solution *) - let useful_equa_id = list_uniq (equas_of_solution_tree solution_tree) in + 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_uniq (List.map (fun e -> e.e_origin.o_hyp) equations) 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_concl l_hyps' in let useful_hyps = List.map (fun id -> List.assoc id full_reified_goal) l_hyps in let useful_vars = let really_useful_vars = vars_of_equations equations in let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in - list_uniq (List.sort compare (really_useful_vars @ concl_vars)) + really_useful_vars @@ concl_vars in (* variables a introduire *) let to_introduce = add_stated_equations env solution_tree in @@ -1295,7 +1222,7 @@ let resolution env full_reified_goal systems_list = Hashtbl.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 coq_Z) basic_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 *) let l_reified_stated = List.map (fun (_,_,(l,r),_) -> @@ -1325,10 +1252,10 @@ 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_index e.e_origin.o_hyp l_hyps in + let i = list_index0 e.e_origin.o_hyp l_hyps in (* PL: it seems that additionnally introduced hyps are in the way during normalization, hence this index shifting... *) - if i=0 then 0 else i +. List.length to_introduce + if i=0 then 0 else Pervasives.(+) i (List.length to_introduce) in app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in let normalization_trace = |