diff options
Diffstat (limited to 'plugins/romega/refl_omega.ml')
| -rw-r--r-- | plugins/romega/refl_omega.ml | 299 |
1 files changed, 153 insertions, 146 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e57230cb..8156e841 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1,11 +1,12 @@ (************************************************************************* PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D + Author: Pierre Crégut - France Télécom R&D Licence : LGPL version 2.1 *************************************************************************) +open Pp open Util open Const_omega module OmegaSolver = Omega.MakeOmegaSolver (Bigint) @@ -16,7 +17,7 @@ open OmegaSolver let debug = ref false let show_goal gl = - if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl + if !debug then (); Tacticals.tclIDTAC gl let pp i = print_int i; print_newline (); flush stdout @@ -37,9 +38,13 @@ type direction = Left of int | Right of int type occ_step = O_left | O_right | O_mono type occ_path = occ_step list -(* 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 occurence = {o_hyp : Names.identifier; o_path : occ_path} +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 occurence = {o_hyp : Names.Id.t; o_path : occ_path} (* \subsection{refiable formulas} *) type oformula = @@ -58,7 +63,7 @@ type oformula = (* Operators for comparison recognized by Omega *) type comparaison = Eq | Leq | Geq | Gt | Lt | Neq -(* Type des prédicats réifiés (fragment de calcul propositionnel. Les +(* Type des prédicats réifiés (fragment de calcul propositionnel. Les * quantifications sont externes au langage) *) type oproposition = Pequa of Term.constr * oequation @@ -70,19 +75,19 @@ type oproposition = | Pimp of int * oproposition * oproposition | Pprop of Term.constr -(* Les équations ou proposiitions atomiques utiles du calcul *) +(* Les équations ou proposiitions atomiques utiles du calcul *) and oequation = { e_comp: comparaison; (* comparaison *) e_left: oformula; (* formule brute gauche *) e_right: oformula; (* formule brute droite *) e_trace: Term.constr; (* tactique de normalisation *) - e_origin: occurence; (* l'hypothèse dont vient le terme *) - e_negated: bool; (* vrai si apparait en position nié - après normalisation *) + e_origin: occurence; (* l'hypothèse dont vient le terme *) + e_negated: bool; (* vrai si apparait en position nié + après normalisation *) 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 *) + dépend l'accès à l'équation avec la + direction (branche) pour y accéder *) + e_omega: afine (* la fonction normalisée *) } (* \subsection{Proof context} @@ -101,8 +106,8 @@ type environment = { mutable props : Term.constr list; (* Les variables introduites par omega *) 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 *) + (* 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; mutable cnt_connectors : int; equations : (int,oequation) Hashtbl.t; @@ -110,35 +115,35 @@ 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 *) + 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_trace : action list } -(* Arbre de solution résolvant complètement un ensemble de systèmes *) +(* Arbre de solution résolvant complètement un ensemble de systèmes *) type solution_tree = Leaf of solution - (* un noeud interne représente un point de branchement correspondant à - l'élimination d'un connecteur générant plusieurs buts + (* un noeud interne représente un point de branchement correspondant à + l'élimination d'un connecteur générant plusieurs buts (typ. disjonction). Le premier argument est l'identifiant du connecteur *) | Tree of int * solution_tree * solution_tree -(* Représentation de l'environnement extrait du but initial sous forme de - chemins pour extraire des equations ou d'hypothèses *) +(* Représentation de l'environnement extrait du but initial sous forme de + chemins pour extraire des equations ou d'hypothèses *) type context_content = CCHyp of occurence | CCEqua of int (* \section{Specific utility functions to handle base types} *) -(* Nom arbitraire de l'hypothèse codant la négation du but final *) -let id_concl = Names.id_of_string "__goal__" +(* Nom arbitraire de l'hypothèse codant la négation du but final *) +let id_concl = Names.Id.of_string "__goal__" -(* Initialisation de l'environnement de réification de la tactique *) +(* 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; @@ -146,29 +151,28 @@ let new_environment () = { constructors = Hashtbl.create 7; } -(* Génération d'un nom d'équation *) +(* Génération d'un nom d'équation *) let new_connector_id env = env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors -(* Calcul de la branche complémentaire *) +(* Calcul de la branche complémentaire *) let barre = function Left x -> Right x | Right x -> Left x -(* Identifiant associé à une branche *) +(* Identifiant associé à une branche *) let indice = function Left x | Right x -> x -(* Affichage de l'environnement de réification (termes et propositions) *) +(* Affichage de l'environnement de réification (termes et propositions) *) let print_env_reification env = let rec loop c i = function - [] -> Printf.printf " ===============================\n\n" + [] -> str " ===============================\n\n" | t :: l -> - Printf.printf " (%c%02d) := " c i; - Pp.ppnl (Printer.pr_lconstr t); - Pp.flush_all (); - loop c (succ i) l in - print_newline (); - Printf.printf " ENVIRONMENT OF PROPOSITIONS :\n\n"; loop 'P' 0 env.props; - Printf.printf " ENVIRONMENT OF TERMS :\n\n"; loop 'V' 0 env.terms - + let s = Printf.sprintf "(%c%02d)" c i in + spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++ + loop c (succ i) l + in + let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in + let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in + msg_debug (prop_info ++ fnl () ++ term_info) (* \subsection{Gestion des environnements de variable pour Omega} *) (* generation d'identifiant d'equation pour Omega *) @@ -185,75 +189,73 @@ let new_omega_var, rst_omega_var = (function () -> incr cpt; !cpt), (function () -> cpt:=0) -(* Affichage des variables d'un système *) +(* Affichage des variables d'un système *) let display_omega_var i = Printf.sprintf "OV%d" i -(* Recherche la variable codant un terme pour Omega et crée la variable dans - l'environnement si il n'existe pas. Cas ou la variable dans Omega représente +(* Recherche la variable codant un terme pour Omega et crée la variable dans + l'environnement si il n'existe pas. Cas ou la variable dans Omega représente le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = - begin try List.assoc t env.om_vars + begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *) 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 - réifié introduit de force *) +(* 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 + réifié introduit de force *) let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars -(* Récupère le terme associé à une variable *) +(* Récupère le terme associé à une variable *) let unintern_omega env id = let rec loop = function [] -> failwith "unintern" - | ((t,j)::l) -> if id = j then t else loop l in + | ((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} +(* \subsection{Gestion des environnements de variable pour la réflexion} Gestion des environnements de traduction entre termes des constructions - non réifiés et variables des termes reifies. Attention il s'agit de - l'environnement initial contenant tout. Il faudra le réduire après + non réifiés et variables des termes reifies. Attention il s'agit de + l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) let add_reified_atom t env = - try list_index0_f Term.eq_constr t env.terms + try List.index0 Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i let get_reified_atom env = - try List.nth env.terms - with e when Errors.noncritical e -> failwith "get_reified_atom" + try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom" (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) let add_prop env t = - try list_index0_f Term.eq_constr t env.props + try List.index0 Term.eq_constr t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i -(* accès a une proposition *) +(* accès a une proposition *) let get_prop v env = - try List.nth v env - with e when Errors.noncritical e -> failwith "get_prop" + try List.nth v env with Invalid_argument _ -> failwith "get_prop" -(* \subsection{Gestion du nommage des équations} *) +(* \subsection{Gestion du nommage des équations} *) (* 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 -(* accès a une equation *) +(* accès a une equation *) let get_equation env id = try Hashtbl.find env.equations id with Not_found as e -> - Printf.printf "Omega Equation %d non trouvée\n" id; raise e + Printf.printf "Omega Equation %d non trouvée\n" id; raise e -(* Affichage des termes réifiés *) +(* Affichage des termes réifiés *) let rec oprint ch = function | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 @@ -287,7 +289,7 @@ let rec weight env = function | Oufo _ -> -1 | Oatom _ as c -> (intern_omega env c) -(* \section{Passage entre oformules et représentation interne de Omega} *) +(* \section{Passage entre oformules et représentation interne de Omega} *) (* \subsection{Oformula vers Omega} *) @@ -305,7 +307,7 @@ let omega_of_oformula env kind = (* \subsection{Omega vers Oformula} *) -let rec oformula_of_omega env af = +let oformula_of_omega env af = let rec loop = function | ({v=v; c=n}::r) -> Oplus(Omult(unintern_omega env v,Oint n),loop r) @@ -316,7 +318,7 @@ let app f v = mkApp(Lazy.force f,v) (* \subsection{Oformula vers COQ reel} *) -let rec coq_of_formula env t = +let coq_of_formula env t = let rec loop = function | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |] | Oopp t -> app Z.opp [| loop t |] @@ -330,12 +332,12 @@ let rec coq_of_formula env t = | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in loop t -(* \subsection{Oformula vers COQ reifié} *) +(* \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; + 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 @@ -388,7 +390,7 @@ let reified_of_proposition env f = try reified_of_proposition env f with reraise -> pprint stderr f; raise reraise -(* \subsection{Omega vers COQ réifié} *) +(* \subsection{Omega vers COQ réifié} *) let reified_of_omega env body constant = let coeff_constant = @@ -402,21 +404,18 @@ let reified_of_omega env body constant = List.fold_right mk_coeff body coeff_constant let reified_of_omega env body c = - try - reified_of_omega env body c - with reraise -> - display_eq display_omega_var (body,c); raise reraise + 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 +pour faire des opérations de normalisation sur les équations. *) -(* \section{Opérations sur les équations} -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. *) +(* Chaque fonction retourne une liste triée sans redondance *) -(* \subsection{Extractions 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 (@@) = List.merge_uniq compare let rec vars_of_formula = function | Oint _ -> [] @@ -455,7 +454,7 @@ let rec scalar n = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [], Omult(t,Oint n) | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i) | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n)) @@ -474,23 +473,23 @@ let rec negate = function | Omult(t1,Oint x) -> do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x)) | Omult(t1,t2) -> - Util.error "Omega: Can't solve a goal with non-linear products" + Errors.error "Omega: Can't solve a goal with non-linear products" | (Oatom _ as t) -> do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone)) | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i) | Oufo c -> do_list [], Oufo (Oopp c) | Ominus _ -> failwith "negate minus" -let rec norm l = (List.length l) +let norm l = (List.length l) -(* \subsection{Mélange (fusion) de deux équations} *) +(* \subsection{Mélange (fusion) de deux équations} *) (* \subsubsection{Version avec coefficients} *) -let rec shuffle_path k1 e1 k2 e2 = +let shuffle_path k1 e1 k2 e2 = let rec loop = function (({c=c1;v=v1}::l1) as l1'), (({c=c2;v=v2}::l2) as l2') -> - if v1 = v2 then - if k1*c1 + k2 * c2 = zero then ( + if Int.equal v1 v2 then + if Bigint.equal (k1 * c1 + k2 * c2) zero then ( Lazy.force coq_f_cancel :: loop (l1,l2)) else ( Lazy.force coq_f_equal :: loop (l1,l2) ) @@ -532,7 +531,7 @@ let rec shuffle env (t1,t2) = do_list [Lazy.force coq_c_plus_comm], Oplus(t2,t1) else do_list [],Oplus(t1,t2) -(* \subsection{Fusion avec réduction} *) +(* \subsection{Fusion avec réduction} *) let shrink_pair f1 f2 = begin match f1,f2 with @@ -546,7 +545,7 @@ let shrink_pair f1 f2 = Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2)) | t1,t2 -> oprint stdout t1; print_newline (); oprint stdout t2; print_newline (); - flush Pervasives.stdout; Util.error "shrink.1" + flush Pervasives.stdout; Errors.error "shrink.1" end (* \subsection{Calcul d'une sous formule constante} *) @@ -560,15 +559,15 @@ let reduce_factor = function let rec compute = function Oint n -> n | Oplus(t1,t2) -> compute t1 + compute t2 - | _ -> Util.error "condense.1" in + | _ -> Errors.error "condense.1" in [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c)) - | t -> Util.error "reduce_factor.1" + | t -> Errors.error "reduce_factor.1" -(* \subsection{Réordonnancement} *) +(* \subsection{Réordonnancement} *) let rec condense env = function Oplus(f1,(Oplus(f2,r) as t)) -> - if weight env f1 = weight env f2 then begin + if Int.equal (weight env f1) (weight env f2) then begin let shrink_tac,t = shrink_pair f1 f2 in let assoc_tac = Lazy.force coq_c_plus_assoc_l in let tac_list,t' = condense env (Oplus(t,r)) in @@ -582,7 +581,7 @@ let rec condense env = function let tac,f1' = reduce_factor f1 in [do_left (do_list tac)],Oplus(f1',Oint n) | Oplus(f1,f2) -> - if weight env f1 = weight env f2 then begin + if Int.equal (weight env f1) (weight env f2) then begin let tac_shrink,t = shrink_pair f1 f2 in let tac,t' = condense env t in tac_shrink :: tac,t' @@ -597,18 +596,18 @@ let rec condense env = function let final = Oplus(t',Oint zero) in tac @ [Lazy.force coq_c_red6], final -(* \subsection{Elimination des zéros} *) +(* \subsection{Elimination des zéros} *) let rec clear_zero = function - Oplus(Omult(Oatom v,Oint n),r) when n=zero -> + Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero -> let tac',t = clear_zero r in Lazy.force coq_c_red5 :: tac',t | Oplus(f,r) -> let tac,t = clear_zero r in - (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t) + (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t) | t -> [],t;; -(* \subsection{Transformation des hypothèses} *) +(* \subsection{Transformation des hypothèses} *) let rec reduce env = function Oplus(t1,t2) -> @@ -643,7 +642,7 @@ let normalize_linear_term env t = let trace3,t3 = clear_zero t2 in do_list [trace1; do_list trace2; do_list trace3], t3 -(* Cette fonction reproduit très exactement le comportement de [p_invert] *) +(* Cette fonction reproduit très exactement le comportement de [p_invert] *) let negate_oper = function Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq @@ -669,7 +668,7 @@ let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) = INEQ with e when Logic.catchable_exception e -> raise e -(* \section{Compilation des hypothèses} *) +(* \section{Compilation des hypothèses} *) let rec oformula_of_constr env t = match Z.parse_term t with @@ -698,7 +697,7 @@ and binprop env (neg2,depends,origin,path) oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in - (* On numérote le connecteur dans l'environnement. *) + (* On numérote le connecteur dans l'environnement. *) c i t1' t2' and mk_equation env ctxt c connector t1 t2 = @@ -737,7 +736,7 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) | _ -> Pprop c -(* Destructuration des hypothèses et de la conclusion *) +(* Destructuration des hypothèses et de la conclusion *) let reify_gl env gl = let concl = Tacmach.pf_concl gl in @@ -751,7 +750,7 @@ let reify_gl env gl = (i,t) :: lhyps -> let t' = oproposition_of_constr env (false,[],i,[]) gl t in if !debug then begin - Printf.printf " %s: " (Names.string_of_id i); + Printf.printf " %s: " (Names.Id.to_string i); pprint stdout t'; Printf.printf "\n" end; @@ -816,13 +815,13 @@ let destructurate_hyps syst = (i,t) :: l -> let l_syst1 = destructurate_pos_hyp i [] [] t in let l_syst2 = loop l in - list_cartesian (@) l_syst1 l_syst2 + List.cartesian (@) l_syst1 l_syst2 | [] -> [[]] in loop syst -(* \subsection{Affichage d'un système d'équation} *) +(* \subsection{Affichage d'un système d'équation} *) -(* Affichage des dépendances de système *) +(* Affichage des dépendances de système *) let display_depend = function Left i -> Printf.printf " L%d" i | Right i -> Printf.printf " R%d" i @@ -845,7 +844,7 @@ let display_systems syst_list = (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") oformula_eq.e_origin.o_path)); Printf.printf "\n Origin: %s (negated : %s)\n\n" - (Names.string_of_id oformula_eq.e_origin.o_hyp) + (Names.Id.to_string oformula_eq.e_origin.o_hyp) (if oformula_eq.e_negated then "yes" else "no") in let display_system syst = @@ -853,8 +852,8 @@ let display_systems syst_list = List.iter display_equation syst in List.iter display_system syst_list -(* Extraction des prédicats utilisées dans une trace. Permet ensuite le - calcul des hypothèses *) +(* Extraction des prédicats utilisées dans une trace. Permet ensuite le + calcul des hypothèses *) let rec hyps_used_in_trace = function | act :: l -> @@ -866,9 +865,9 @@ let rec hyps_used_in_trace = function end | [] -> [] -(* 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 *) +(* 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 -> @@ -886,7 +885,7 @@ let rec variable_stated_in_trace = function 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 *) + de définir dans le mauvais ordre *) let stated_equations = let cmpvar x y = Pervasives.(-) x.st_var y.st_var in let rec loop = function @@ -895,15 +894,15 @@ let add_stated_equations env tree = in loop tree in let add_env st = - (* On retransforme la définition de v en formule reifiée *) + (* On retransforme la définition de v en formule reifiée *) let v_def = oformula_of_omega env st.st_def in - (* Notez que si l'ordre de création des variables n'est pas respecté, + (* Notez que si l'ordre de création des variables n'est pas respecté, * ca va planter *) 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 Z.typ; coq_v|] in - (* sa représentation sous forme d'équation mais non réifié car on n'a pas + (* 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 (* enregistre le lien entre la variable omega et la variable Coq *) @@ -911,18 +910,18 @@ let add_stated_equations env tree = (v, term_to_generalize,term_to_reify,st.st_def.id) in List.map add_env stated_equations -(* Calcule la liste des éclatements à réaliser sur les hypothèses - nécessaires pour extraire une liste d'équations donnée *) +(* 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 + 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 (List.rev l) (get_eclatement env r) + List.union Pervasives.(=) (List.rev l) (get_eclatement env r) | [] -> [] let select_smaller l = @@ -933,10 +932,14 @@ 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 failwith "Exit" + else if List.mem (barre x) required then raise Exit else x :: select l - | [] -> [] in - map_succeed (function (sol,splits) -> (sol,select splits)) 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) @@ -955,7 +958,7 @@ let really_useful_prop l_equa c = | 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 ! *) + (* 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 = @@ -1015,10 +1018,10 @@ let rec solve_with_constraints all_solutions path = let find_path {o_hyp=id;o_path=p} env = let rec loop_path = function ([],l) -> Some l - | (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2) + | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2) | _ -> None in let rec loop_id i = function - CCHyp{o_hyp=id';o_path=p'} :: l when id = id' -> + CCHyp{o_hyp=id';o_path=p'} :: l when Names.Id.equal id id' -> begin match loop_path (p',p) with Some r -> i,r | None -> loop_id (succ i) l @@ -1036,7 +1039,7 @@ let mk_direction_list l = (* \section{Rejouer l'historique} *) let get_hyp env_hyp i = - try list_index0 (CCEqua i) env_hyp + try List.index0 Pervasives.(=) (CCEqua i) env_hyp with Not_found -> failwith (Printf.sprintf "get_hyp %d" i) let replay_history env env_hyp = @@ -1163,11 +1166,11 @@ and decompose_tree_hyps trace env ctxt = function (* \section{La fonction principale} *) (* Cette fonction construit la -trace pour la procédure de décision réflexive. A partir des résultats -de l'extraction des systèmes, elle lance la résolution par Omega, puis +trace pour la procédure de décision réflexive. A partir des résultats +de l'extraction des systèmes, elle lance la résolution par Omega, puis 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. *) +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 num = ref 0 in @@ -1178,7 +1181,7 @@ 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 *) + (* calcule les hypotheses utilisées pour la solution *) let vars = hyps_used_in_trace trace in let splits = get_eclatement env vars in if !debug then begin @@ -1199,17 +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 *) + (* 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_concl l_hyps' in + let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in + let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in let useful_hyps = - List.map (fun id -> List.assoc id full_reified_goal) l_hyps in + List.map + (fun id -> List.assoc_f Names.Id.equal 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 + let concl_vars = + vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal) + in really_useful_vars @@ concl_vars in (* variables a introduire *) @@ -1218,8 +1225,8 @@ let resolution env full_reified_goal systems_list = let l_generalize_arg = List.map (fun (_,t,_,_) -> 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 *) + - 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 basic_env = let rec loop i = function @@ -1229,7 +1236,7 @@ let resolution env full_reified_goal systems_list = | [] -> [] 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 *) + (* 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; @@ -1258,10 +1265,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_index0 e.e_origin.o_hyp l_hyps in + let i = List.index0 Names.Id.equal 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 Pervasives.(+) i (List.length to_introduce) + if Int.equal 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 = @@ -1275,8 +1282,8 @@ let resolution env full_reified_goal systems_list = Tactics.generalize (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >> - Tactics.change_in_concl None reified >> - Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >> + Proofview.V82.of_tactic (Tactics.change_concl reified) >> + Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >> show_goal >> Tactics.normalise_vm_in_concl >> (*i Alternatives to the previous line: @@ -1285,7 +1292,7 @@ let resolution env full_reified_goal systems_list = - Skip the conversion check and rely directly on the QED: Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >> i*) - Tactics.apply (Lazy.force coq_I) + Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I)) let total_reflexive_omega_tactic gl = Coqlib.check_required_library ["Coq";"romega";"ROmega"]; @@ -1297,7 +1304,7 @@ let total_reflexive_omega_tactic gl = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution env full_reified_goal systems_list gl - with NO_CONTRADICTION -> Util.error "ROmega can't solve this system" + with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system" (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*) |