summaryrefslogtreecommitdiff
path: root/contrib/romega/refl_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/romega/refl_omega.ml')
-rw-r--r--contrib/romega/refl_omega.ml1307
1 files changed, 1307 insertions, 0 deletions
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
new file mode 100644
index 00000000..ef68c587
--- /dev/null
+++ b/contrib/romega/refl_omega.ml
@@ -0,0 +1,1307 @@
+(*************************************************************************
+
+ PROJET RNRT Calife - 2001
+ Author: Pierre Crégut - France Télécom R&D
+ Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+open Const_omega
+
+
+(* \section{Useful functions and flags} *)
+(* Especially useful debugging functions *)
+let debug = ref false
+
+let show_goal gl =
+ if !debug then Pp.ppnl (Tacmach.pr_gls gl); Tacticals.tclIDTAC gl
+
+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 (i+1) 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}
+ \subsection{How to walk in a term}
+ To represent how to get to a proposition. Only choice points are
+ kept (branch to choose in a disjunction and identifier of the disjunctive
+ connector) *)
+type direction = Left of int | Right of int
+
+(* Step to find a proposition (operators are at most binary). A list is
+ a path *)
+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}
+
+(* \subsection{refiable formulas} *)
+type oformula =
+ (* integer *)
+ | Oint of int
+ (* recognized binary and unary operations *)
+ | Oplus of oformula * oformula
+ | Omult of oformula * oformula
+ | Ominus of oformula * oformula
+ | Oopp of oformula
+ (* an atome in the environment *)
+ | Oatom of int
+ (* weird expression that cannot be translated *)
+ | Oufo of 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
+ * quantifications sont externes au langage) *)
+type oproposition =
+ Pequa of Term.constr * oequation
+ | Ptrue
+ | Pfalse
+ | Pnot of oproposition
+ | Por of int * oproposition * oproposition
+ | Pand of int * oproposition * oproposition
+ | Pimp of int * oproposition * oproposition
+ | Pprop of Term.constr
+
+(* 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_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: Omega2.afine (* la fonction normalisée *)
+ }
+
+(* \subsection{Proof context}
+ This environment codes
+ \begin{itemize}
+ \item the terms and propositions that are given as
+ parameters of the reified proof (and are represented as variables in the
+ reified goals)
+ \item translation functions linking the decision procedure and the Coq proof
+ \end{itemize} *)
+
+type environment = {
+ (* La liste des termes non reifies constituant l'environnement global *)
+ mutable terms : Term.constr list;
+ (* La meme chose pour les propositions *)
+ 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 *)
+ real_indices : (int,int) Hashtbl.t;
+ mutable cnt_connectors : int;
+ equations : (int,oequation) Hashtbl.t;
+ constructors : (int, occurence) Hashtbl.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 *)
+type solution = {
+ s_index : int;
+ s_equa_deps : int list;
+ s_trace : Omega2.action list }
+
+(* 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
+ (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 *)
+
+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__"
+
+(* 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;
+}
+
+(* Génération d'un nom d'équation *)
+let new_eq_id env =
+ env.cnt_connectors <- env.cnt_connectors + 1; env.cnt_connectors
+
+(* Calcul de la branche complémentaire *)
+let barre = function Left x -> Right x | Right x -> Left x
+
+(* Identifiant associé à une branche *)
+let indice = function Left x | Right x -> x
+
+(* 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"
+ | t :: l ->
+ Printf.printf "(%c%02d) : " c i;
+ Pp.ppnl (Printer.prterm t);
+ Pp.flush_all ();
+ loop c (i+1) l in
+ Printf.printf "PROPOSITIONS :\n\n"; loop 'P' 0 env.props;
+ Printf.printf "TERMES :\n\n"; loop 'V' 0 env.terms
+
+
+(* \subsection{Gestion des environnements de variable pour Omega} *)
+(* generation d'identifiant d'equation pour Omega *)
+let new_omega_id = let cpt = ref 0 in function () -> incr cpt; !cpt
+(* Affichage des variables d'un système *)
+let display_omega_id i = Printf.sprintf "O%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
+ le terme d'un monome (le plus souvent un atome) *)
+
+let intern_omega env t =
+ begin try List.assoc t env.om_vars
+ with Not_found ->
+ let v = new_omega_id () in
+ env.om_vars <- (t,v) :: env.om_vars; v
+ end
+
+(* Ajout forcé d'un lien entre un terme et une variable Omega. Cas ou la
+ variable est crée par Omega et ou il faut la lier après coup a 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 *)
+let unintern_omega env id =
+ let rec loop = function
+ [] -> failwith "unintern"
+ | ((t,j)::l) -> if id = j then t else loop l in
+ loop env.om_vars
+
+(* \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
+ calcul des variables utiles. *)
+
+let add_reified_atom t env =
+ try list_index 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 _ -> failwith "get_reified_atom"
+
+(* \subsection{Gestion de l'environnement de proposition pour Omega} *)
+(* ajout d'une proposition *)
+let add_prop env t =
+ try list_index t env.props
+ with Not_found ->
+ let i = List.length env.props in env.props <- env.props @ [t]; i
+
+(* accès a une proposition *)
+let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+
+(* \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.Omega2.id in
+ try let _ = Hashtbl.find env.equations id in ()
+ with Not_found -> Hashtbl.add env.equations id 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
+
+(* Affichage des termes réifiés *)
+let rec oprint ch = function
+ | Oint n -> Printf.fprintf ch "%d" n
+ | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2
+ | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2
+ | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2
+ | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1
+ | Oatom n -> Printf.fprintf ch "V%02d" n
+ | Oufo x -> Printf.fprintf ch "?"
+
+let rec pprint ch = function
+ Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) ->
+ let connector =
+ match comp with
+ Eq -> "=" | Leq -> "=<" | Geq -> ">="
+ | Gt -> ">" | Lt -> "<" | Neq -> "!=" in
+ Printf.fprintf ch "%a %s %a" oprint t1 connector oprint t2
+ | Ptrue -> Printf.fprintf ch "TT"
+ | Pfalse -> Printf.fprintf ch "FF"
+ | Pnot t -> Printf.fprintf ch "not(%a)" pprint t
+ | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2
+ | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2
+ | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2
+ | Pprop c -> Printf.fprintf ch "Prop"
+
+let rec weight env = function
+ | Oint _ -> -1
+ | Oopp c -> weight env c
+ | Omult(c,_) -> weight env c
+ | Oplus _ -> failwith "weight"
+ | Ominus _ -> failwith "weight minus"
+ | Oufo _ -> -1
+ | Oatom _ as c -> (intern_omega env c)
+
+(* \section{Passage entre oformules et représentation interne de Omega} *)
+
+(* \subsection{Oformula vers Omega} *)
+
+let omega_of_oformula env kind =
+ let rec loop accu = function
+ | Oplus(Omult(v,Oint n),r) ->
+ loop ({Omega2.v=intern_omega env v; Omega2.c=n} :: accu) r
+ | Oint n ->
+ let id = new_omega_id () in
+ (*i tag_equation name id; i*)
+ {Omega2.kind = kind; Omega2.body = List.rev accu;
+ Omega2.constant = n; Omega2.id = id}
+ | t -> print_string "CO"; oprint stdout t; failwith "compile_equation" in
+ loop []
+
+(* \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
+ | ({Omega2.v=v; Omega2.c=n}::r) ->
+ Oplus(Omult(unintern_omega env v,Oint n),loop r)
+ | [] -> Oint af.Omega2.constant in
+ loop af.Omega2.body
+
+let app f v = mkApp(Lazy.force f,v)
+
+(* \subsection{Oformula vers COQ reel} *)
+
+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
+ | 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
+ loop t
+
+(* \subsection{Oformula vers COQ reifié} *)
+
+let rec reified_of_formula env = function
+ | Oplus (t1,t2) ->
+ app coq_t_plus [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Oopp t ->
+ 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 |]
+ | Oufo t -> reified_of_formula env t
+ | Oatom i -> app coq_t_var [| mk_nat (reified_of_atom env i) |]
+ | Ominus(t1,t2) ->
+ 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
+
+let rec reified_of_proposition env = function
+ Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
+ app coq_p_eq [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Pequa (_,{ e_comp=Leq; e_left=t1; e_right=t2 }) ->
+ app coq_p_leq [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Pequa(_,{ e_comp=Geq; e_left=t1; e_right=t2 }) ->
+ app coq_p_geq [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Pequa(_,{ e_comp=Gt; e_left=t1; e_right=t2 }) ->
+ app coq_p_gt [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Pequa(_,{ e_comp=Lt; e_left=t1; e_right=t2 }) ->
+ app coq_p_lt [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Pequa(_,{ e_comp=Neq; e_left=t1; e_right=t2 }) ->
+ app coq_p_neq [| reified_of_formula env t1; reified_of_formula env t2 |]
+ | Ptrue -> Lazy.force coq_p_true
+ | Pfalse -> Lazy.force coq_p_false
+ | Pnot t ->
+ app coq_p_not [| reified_of_proposition env t |]
+ | Por (_,t1,t2) ->
+ app coq_p_or
+ [| reified_of_proposition env t1; reified_of_proposition env t2 |]
+ | Pand(_,t1,t2) ->
+ app coq_p_and
+ [| reified_of_proposition env t1; reified_of_proposition env t2 |]
+ | Pimp(_,t1,t2) ->
+ app coq_p_imp
+ [| reified_of_proposition env t1; reified_of_proposition env t2 |]
+ | 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
+
+(* \subsection{Omega vers COQ réifié} *)
+
+let reified_of_omega env body constant =
+ let coeff_constant =
+ app coq_t_int [| mk_Z constant |] in
+ let mk_coeff {Omega2.c=c; Omega2.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_plus [|coef; t |] in
+ 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 ->
+ Omega2.display_eq display_omega_id (body,c); raise e
+ end
+
+(* \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 *)
+
+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)
+ | 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))
+
+(* \subsection{Multiplication par un scalaire} *)
+
+let rec scalar n = function
+ Oplus(t1,t2) ->
+ let tac1,t1' = scalar n t1 and
+ tac2,t2' = scalar n t2 in
+ do_list [Lazy.force coq_c_mult_plus_distr; do_both tac1 tac2],
+ Oplus(t1',t2')
+ | Oopp t ->
+ do_list [Lazy.force coq_c_mult_opp_left], Omult(t,Oint(-n))
+ | 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"
+ | (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))
+ | Ominus _ -> failwith "scalar minus"
+
+(* \subsection{Propagation de l'inversion} *)
+
+let rec negate = function
+ Oplus(t1,t2) ->
+ let tac1,t1' = negate t1 and
+ tac2,t2' = negate t2 in
+ do_list [Lazy.force coq_c_opp_plus ; (do_both tac1 tac2)],
+ Oplus(t1',t2')
+ | Oopp t ->
+ do_list [Lazy.force coq_c_opp_opp], t
+ | Omult(t1,Oint x) ->
+ do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (-x))
+ | Omult(t1,t2) ->
+ Util.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(-1))
+ | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(-i)
+ | Oufo c -> do_list [], Oufo (Oopp c)
+ | Ominus _ -> failwith "negate minus"
+
+let rec norm l = (List.length l)
+
+(* \subsection{Mélange (fusion) de deux équations} *)
+(* \subsubsection{Version avec coefficients} *)
+let rec shuffle_path k1 e1 k2 e2 =
+ let rec loop = function
+ (({Omega2.c=c1;Omega2.v=v1}::l1) as l1'),
+ (({Omega2.c=c2;Omega2.v=v2}::l2) as l2') ->
+ if v1 = v2 then
+ if k1*c1 + k2 * c2 = 0 then (
+ Lazy.force coq_f_cancel :: loop (l1,l2))
+ else (
+ Lazy.force coq_f_equal :: loop (l1,l2) )
+ else if v1 > v2 then (
+ Lazy.force coq_f_left :: loop(l1,l2'))
+ else (
+ Lazy.force coq_f_right :: loop(l1',l2))
+ | ({Omega2.c=c1;Omega2.v=v1}::l1), [] ->
+ Lazy.force coq_f_left :: loop(l1,[])
+ | [],({Omega2.c=c2;Omega2.v=v2}::l2) ->
+ Lazy.force coq_f_right :: loop([],l2)
+ | [],[] -> flush stdout; [] in
+ mk_shuffle_list (loop (e1,e2))
+
+(* \subsubsection{Version sans coefficients} *)
+let rec shuffle env (t1,t2) =
+ match t1,t2 with
+ Oplus(l1,r1), Oplus(l2,r2) ->
+ if weight env l1 > weight env l2 then
+ let l_action,t' = shuffle env (r1,t2) in
+ do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action], Oplus(l1,t')
+ else
+ let l_action,t' = shuffle env (t1,r2) in
+ do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
+ | Oplus(l1,r1), t2 ->
+ if weight env l1 > weight env t2 then
+ let (l_action,t') = shuffle env (r1,t2) in
+ do_list [Lazy.force coq_c_plus_assoc_r;do_right l_action],Oplus(l1, t')
+ else do_list [Lazy.force coq_c_plus_sym], Oplus(t2,t1)
+ | t1,Oplus(l2,r2) ->
+ if weight env l2 > weight env t1 then
+ let (l_action,t') = shuffle env (t1,r2) in
+ do_list [Lazy.force coq_c_plus_permute;do_right l_action], Oplus(l2,t')
+ else do_list [],Oplus(t1,t2)
+ | Oint t1,Oint t2 ->
+ do_list [Lazy.force coq_c_reduce], Oint(t1+t2)
+ | t1,t2 ->
+ if weight env t1 < weight env t2 then
+ do_list [Lazy.force coq_c_plus_sym], Oplus(t2,t1)
+ else do_list [],Oplus(t1,t2)
+
+(* \subsection{Fusion avec réduction} *)
+
+let shrink_pair f1 f2 =
+ begin match f1,f2 with
+ Oatom v,Oatom _ ->
+ Lazy.force coq_c_red1, Omult(Oatom v,Oint 2)
+ | Oatom v, Omult(_,c2) ->
+ Lazy.force coq_c_red2, Omult(Oatom v,Oplus(c2,Oint 1))
+ | Omult (v1,c1),Oatom v ->
+ Lazy.force coq_c_red3, Omult(Oatom v,Oplus(c1,Oint 1))
+ | Omult (Oatom v,c1),Omult (v2,c2) ->
+ 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"
+ end
+
+(* \subsection{Calcul d'une sous formule constante} *)
+
+let reduce_factor = function
+ Oatom v ->
+ let r = Omult(Oatom v,Oint 1) in
+ [Lazy.force coq_c_red0],r
+ | Omult(Oatom v,Oint n) as f -> [],f
+ | Omult(Oatom v,c) ->
+ let rec compute = function
+ Oint n -> n
+ | Oplus(t1,t2) -> compute t1 + compute t2
+ | _ -> Util.error "condense.1" in
+ [Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
+ | t -> Util.error "reduce_factor.1"
+
+(* \subsection{Réordonancement} *)
+
+let rec condense env = function
+ Oplus(f1,(Oplus(f2,r) as t)) ->
+ if 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
+ assoc_tac :: do_left (do_list [shrink_tac]) :: tac_list, t'
+ end else begin
+ let tac,f = reduce_factor f1 in
+ let tac',t' = condense env t in
+ [do_both (do_list tac) (do_list tac')], Oplus(f,t')
+ end
+ | (Oplus(f1,Oint n) as t) ->
+ 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
+ let tac_shrink,t = shrink_pair f1 f2 in
+ let tac,t' = condense env t in
+ tac_shrink :: tac,t'
+ end else begin
+ let tac,f = reduce_factor f1 in
+ let tac',t' = condense env f2 in
+ [do_both (do_list tac) (do_list tac')],Oplus(f,t')
+ end
+ | (Oint _ as t)-> [],t
+ | t ->
+ let tac,t' = reduce_factor t in
+ let final = Oplus(t',Oint 0) in
+ tac @ [Lazy.force coq_c_red6], final
+
+(* \subsection{Elimination des zéros} *)
+
+let rec clear_zero = function
+ Oplus(Omult(Oatom v,Oint 0),r) ->
+ 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)
+ | t -> [],t;;
+
+(* \subsection{Transformation des hypothèses} *)
+
+let rec reduce env = function
+ Oplus(t1,t2) ->
+ let t1', trace1 = reduce env t1 in
+ let t2', trace2 = reduce env t2 in
+ let trace3,t' = shuffle env (t1',t2') in
+ t', do_list [do_both trace1 trace2; trace3]
+ | Ominus(t1,t2) ->
+ let t,trace = reduce env (Oplus(t1, Oopp t2)) in
+ t, do_list [Lazy.force coq_c_minus; trace]
+ | Omult(t1,t2) as t ->
+ let t1', trace1 = reduce env t1 in
+ let t2', trace2 = reduce env t2 in
+ begin match t1',t2' with
+ | (_, Oint n) ->
+ let tac,t' = scalar n t1' in
+ t', do_list [do_both trace1 trace2; tac]
+ | (Oint n,_) ->
+ let tac,t' = scalar n t2' in
+ t', do_list [do_both trace1 trace2; Lazy.force coq_c_mult_sym; tac]
+ | _ -> Oufo t, Lazy.force coq_c_nop
+ end
+ | Oopp t ->
+ let t',trace = reduce env t in
+ let trace',t'' = negate t' in
+ t'', do_list [do_left trace; trace']
+ | (Oint _ | Oatom _ | Oufo _) as t -> t, Lazy.force coq_c_nop
+
+let normalize_linear_term env t =
+ let t1,trace1 = reduce env t in
+ let trace2,t2 = condense env t1 in
+ 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] *)
+let negate_oper = function
+ Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq
+
+let normalize_equation env (negated,depends,origin,path) (oper,t1,t2) =
+ let mk_step t1 t2 f kind =
+ let t = f t1 t2 in
+ let trace, oterm = normalize_linear_term env t in
+ let equa = omega_of_oformula env kind oterm in
+ { e_comp = oper; e_left = t1; e_right = t2;
+ e_negated = negated; e_depends = depends;
+ e_origin = { o_hyp = origin; o_path = List.rev path };
+ e_trace = trace; e_omega = equa } in
+ try match (if negated then (negate_oper oper) else oper) with
+ | Eq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.EQUA
+ | Neq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.DISE
+ | Leq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o2,Oopp o1)) Omega2.INEQ
+ | Geq -> mk_step t1 t2 (fun o1 o2 -> Oplus (o1,Oopp o2)) Omega2.INEQ
+ | Lt ->
+ mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o2,Oint (-1)),Oopp o1))
+ Omega2.INEQ
+ | Gt ->
+ mk_step t1 t2 (fun o1 o2 -> Oplus (Oplus(o1,Oint (-1)),Oopp o2))
+ Omega2.INEQ
+ with e when Logic.catchable_exception e -> raise e
+
+(* \section{Compilation des hypothèses} *)
+
+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]) ->binop env (fun x y -> Omult(x,y)) t1 t2
+ | 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)
+ add_to_depends neg1 gl c t1 t2 =
+ let i = new_eq_id env in
+ 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};
+ let t1' =
+ 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. *)
+ c i t1' t2'
+
+and mk_equation env ctxt c connector t1 t2 =
+ let t1' = oformula_of_constr env t1 in
+ let t2' = oformula_of_constr env t2 in
+ (* On ajoute l'equation dans l'environnement. *)
+ let omega = normalize_equation env ctxt (connector,t1',t2') in
+ add_equation env omega;
+ 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]) ->
+ binprop env ctxt (not negated) negated gl (fun i x y -> Por(i,x,y)) t1 t2
+ | Kapp("and",[t1;t2]) ->
+ binprop env ctxt negated negated gl
+ (fun i x y -> Pand(i,x,y)) t1 t2
+ | Kimp(t1,t2) ->
+ binprop env ctxt (not negated) (not negated) gl
+ (fun i x y -> Pimp(i,x,y)) t1 t2
+ | _ -> Pprop c
+ with e when Logic.catchable_exception e -> Pprop c
+
+(* Destructuration des hypothèses et de la conclusion *)
+
+let reify_gl env gl =
+ let concl = Tacmach.pf_concl gl in
+ let t_concl =
+ Pnot (oproposition_of_constr env (true,[],id_concl,[O_mono]) gl concl) in
+ if !debug then begin
+ Printf.printf "CONCL: "; pprint stdout t_concl; Printf.printf "\n"
+ end;
+ let rec loop = function
+ (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);
+ pprint stdout t';
+ Printf.printf "\n"
+ end;
+ (i,t') :: loop lhyps
+ | [] ->
+ if !debug then print_env_reification env;
+ [] in
+ let t_lhyps = loop (Tacmach.pf_hyps_types gl) in
+ (id_concl,t_concl) :: t_lhyps
+
+let rec destructurate_pos_hyp orig list_equations list_depends = function
+ | Pequa (_,e) -> [e :: list_equations]
+ | Ptrue | Pfalse | Pprop _ -> [list_equations]
+ | Pnot t -> destructurate_neg_hyp orig list_equations list_depends t
+ | Por (i,t1,t2) ->
+ let s1 =
+ destructurate_pos_hyp orig list_equations (i::list_depends) t1 in
+ let s2 =
+ destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
+ s1 @ s2
+ | Pand(i,t1,t2) ->
+ let list_s1 =
+ destructurate_pos_hyp orig list_equations (list_depends) t1 in
+ let rec loop = function
+ le1 :: ll -> destructurate_pos_hyp orig le1 list_depends t2 @ loop ll
+ | [] -> [] in
+ loop list_s1
+ | Pimp(i,t1,t2) ->
+ let s1 =
+ destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
+ let s2 =
+ destructurate_pos_hyp orig list_equations (i::list_depends) t2 in
+ s1 @ s2
+
+and destructurate_neg_hyp orig list_equations list_depends = function
+ | Pequa (_,e) -> [e :: list_equations]
+ | Ptrue | Pfalse | Pprop _ -> [list_equations]
+ | Pnot t -> destructurate_pos_hyp orig list_equations list_depends t
+ | Pand (i,t1,t2) ->
+ let s1 =
+ destructurate_neg_hyp orig list_equations (i::list_depends) t1 in
+ let s2 =
+ destructurate_neg_hyp orig list_equations (i::list_depends) t2 in
+ s1 @ s2
+ | Por(_,t1,t2) ->
+ let list_s1 =
+ destructurate_neg_hyp orig list_equations list_depends t1 in
+ let rec loop = function
+ le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
+ | [] -> [] in
+ loop list_s1
+ | Pimp(_,t1,t2) ->
+ let list_s1 =
+ destructurate_pos_hyp orig list_equations list_depends t1 in
+ let rec loop = function
+ le1 :: ll -> destructurate_neg_hyp orig le1 list_depends t2 @ loop ll
+ | [] -> [] in
+ loop list_s1
+
+let destructurate_hyps syst =
+ let rec loop = function
+ (i,t) :: l ->
+ let l_syst1 = destructurate_pos_hyp i [] [] t in
+ let l_syst2 = loop l in
+ cartesien l_syst1 l_syst2
+ | [] -> [[]] in
+ loop syst
+
+(* \subsection{Affichage d'un système d'équation} *)
+
+(* 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
+
+let display_systems syst_list =
+ let display_omega om_e =
+ Printf.printf "%d : %a %s 0\n"
+ om_e.Omega2.id
+ (fun _ -> Omega2.display_eq display_omega_id)
+ (om_e.Omega2.body, om_e.Omega2.constant)
+ (Omega2.operator_of_eq om_e.Omega2.kind) in
+
+ let display_equation oformula_eq =
+ pprint stdout (Pequa (Lazy.force coq_c_nop,oformula_eq)); print_newline ();
+ display_omega oformula_eq.e_omega;
+ Printf.printf " Depends on:";
+ List.iter display_depend oformula_eq.e_depends;
+ Printf.printf "\n Path: %s"
+ (String.concat ""
+ (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"
+ (Names.string_of_id oformula_eq.e_origin.o_hyp)
+ (if oformula_eq.e_negated then "yes" else "false") in
+
+ let display_system syst =
+ Printf.printf "=SYSTEME==================================\n";
+ 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 *)
+
+let rec hyps_used_in_trace = function
+ | act :: l ->
+ begin match act with
+ | Omega2.HYP e -> e.Omega2.id :: hyps_used_in_trace l
+ | Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) ->
+ hyps_used_in_trace act1 @ hyps_used_in_trace act2
+ | _ -> hyps_used_in_trace l
+ 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 *)
+
+let rec variable_stated_in_trace = function
+ | act :: l ->
+ begin match act with
+ | Omega2.STATE action ->
+ (*i nlle_equa: afine, def: afine, eq_orig: afine, i*)
+ (*i coef: int, var:int i*)
+ action :: variable_stated_in_trace l
+ | Omega2.SPLIT_INEQ (_,(_,act1),(_,act2)) ->
+ variable_stated_in_trace act1 @ variable_stated_in_trace act2
+ | _ -> variable_stated_in_trace l
+ end
+ | [] -> []
+;;
+
+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 -> x.Omega2.st_var - y.Omega2.st_var) (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.Omega2.st_def in
+ (* 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 coq_Z; 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
+ (* enregistre le lien entre la variable omega et la variable Coq *)
+ intern_omega_force env (Oatom v) st.Omega2.st_var;
+ (v, term_to_generalize,term_to_reify,st.Omega2.st_def.Omega2.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 *)
+
+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)
+ | [] -> []
+
+let select_smaller l =
+ let comp (_,x) (_,y) = 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
+ | [] -> [] in
+ map_exc (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)
+ | Leaf s -> s.s_equa_deps
+
+
+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.Omega2.id l_equa then Some c else None
+ | Ptrue -> None
+ | Pfalse -> 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
+ | Pprop t -> 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
+ match loop c with
+ None -> Pprop (real_of 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)))
+ | Tree(i,t1,t2) ->
+ Printf.fprintf ch "S%d(%a,%a)" i
+ display_solution_tree t1 display_solution_tree t2
+
+let rec solve_with_constraints all_solutions path =
+ let rec build_tree sol buf = function
+ [] -> Leaf sol
+ | (Left i :: remainder) ->
+ Tree(i,
+ build_tree sol (Left i :: buf) remainder,
+ solve_with_constraints all_solutions (List.rev(Right i :: buf)))
+ | (Right i :: remainder) ->
+ Tree(i,
+ solve_with_constraints all_solutions (List.rev (Left i :: buf)),
+ build_tree sol (Right i :: buf) remainder) in
+ let weighted = filter_compatible_systems path all_solutions in
+ let (winner_sol,winner_deps) =
+ try select_smaller weighted
+ with e ->
+ Printf.printf "%d - %d\n"
+ (List.length weighted) (List.length all_solutions);
+ List.iter display_depend path; raise e in
+ build_tree winner_sol (List.rev path) winner_deps
+
+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)
+ | _ -> None in
+ let rec loop_id i = function
+ CCHyp{o_hyp=id';o_path=p'} :: l when id = id' ->
+ begin match loop_path (p',p) with
+ Some r -> i,r
+ | None -> loop_id (i+1) l
+ end
+ | _ :: l -> loop_id (i+1) l
+ | [] -> failwith "find_path" in
+ loop_id 0 env
+
+let mk_direction_list l =
+ let trans = function
+ O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in
+ mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l)
+
+
+(* \section{Rejouer l'historique} *)
+
+let get_hyp env_hyp i =
+ try list_index (CCEqua i) env_hyp
+ with Not_found -> failwith (Printf.sprintf "get_hyp %d" i)
+
+let replay_history env env_hyp =
+ let rec loop env_hyp t =
+ match t with
+ | Omega2.CONTRADICTION (e1,e2) :: l ->
+ let trace = mk_nat (List.length e1.Omega2.body) in
+ mkApp (Lazy.force coq_s_contradiction,
+ [| trace ; mk_nat (get_hyp env_hyp e1.Omega2.id);
+ mk_nat (get_hyp env_hyp e2.Omega2.id) |])
+ | Omega2.DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+ mkApp (Lazy.force coq_s_div_approx,
+ [| mk_Z k; mk_Z d;
+ reified_of_omega env e2.Omega2.body e2.Omega2.constant;
+ mk_nat (List.length e2.Omega2.body);
+ loop env_hyp l; mk_nat (get_hyp env_hyp e1.Omega2.id) |])
+ | Omega2.NOT_EXACT_DIVIDE (e1,k) :: l ->
+ let e2_constant = Omega2.floor_div e1.Omega2.constant k in
+ let d = e1.Omega2.constant - e2_constant * k in
+ let e2_body = Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
+ mkApp (Lazy.force coq_s_not_exact_divide,
+ [|mk_Z k; mk_Z d;
+ reified_of_omega env e2_body e2_constant;
+ mk_nat (List.length e2_body);
+ mk_nat (get_hyp env_hyp e1.Omega2.id)|])
+ | Omega2.EXACT_DIVIDE (e1,k) :: l ->
+ let e2_body =
+ Omega2.map_eq_linear (fun c -> c / k) e1.Omega2.body in
+ let e2_constant = Omega2.floor_div e1.Omega2.constant k in
+ mkApp (Lazy.force coq_s_exact_divide,
+ [|mk_Z 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.Omega2.id)|])
+ | (Omega2.MERGE_EQ(e3,e1,e2)) :: l ->
+ let n1 = get_hyp env_hyp e1.Omega2.id and n2 = get_hyp env_hyp e2 in
+ mkApp (Lazy.force coq_s_merge_eq,
+ [| mk_nat (List.length e1.Omega2.body);
+ mk_nat n1; mk_nat n2;
+ loop (CCEqua e3:: env_hyp) l |])
+ | Omega2.SUM(e3,(k1,e1),(k2,e2)) :: l ->
+ let n1 = get_hyp env_hyp e1.Omega2.id
+ and n2 = get_hyp env_hyp e2.Omega2.id in
+ let trace = shuffle_path k1 e1.Omega2.body k2 e2.Omega2.body in
+ mkApp (Lazy.force coq_s_sum,
+ [| mk_Z k1; mk_nat n1; mk_Z k2;
+ mk_nat n2; trace; (loop (CCEqua e3 :: env_hyp) l) |])
+ | Omega2.CONSTANT_NOT_NUL(e,k) :: l ->
+ mkApp (Lazy.force coq_s_constant_not_nul,
+ [| mk_nat (get_hyp env_hyp e) |])
+ | Omega2.CONSTANT_NEG(e,k) :: l ->
+ mkApp (Lazy.force coq_s_constant_neg,
+ [| mk_nat (get_hyp env_hyp e) |])
+ | Omega2.STATE {Omega2.st_new_eq=new_eq; Omega2.st_def =def;
+ Omega2.st_orig=orig; Omega2.st_coef=m;
+ Omega2.st_var=sigma } :: l ->
+ let n1 = get_hyp env_hyp orig.Omega2.id
+ and n2 = get_hyp env_hyp def.Omega2.id in
+ let v = unintern_omega env sigma in
+ let o_def = oformula_of_omega env def in
+ let o_orig = oformula_of_omega env orig in
+ let body =
+ 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;
+ loop (CCEqua new_eq.Omega2.id :: env_hyp) l |])
+ | Omega2.HYP _ :: l -> loop env_hyp l
+ | Omega2.CONSTANT_NUL e :: l ->
+ mkApp (Lazy.force coq_s_constant_nul,
+ [| mk_nat (get_hyp env_hyp e) |])
+ | Omega2.NEGATE_CONTRADICT(e1,e2,b) :: l ->
+ mkApp (Lazy.force coq_s_negate_contradict,
+ [| mk_nat (get_hyp env_hyp e1.Omega2.id);
+ mk_nat (get_hyp env_hyp e2.Omega2.id) |])
+ | Omega2.SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
+ let i = get_hyp env_hyp e.Omega2.id in
+ let r1 = loop (CCEqua e1 :: env_hyp) l1 in
+ let r2 = loop (CCEqua e2 :: env_hyp) l2 in
+ mkApp (Lazy.force coq_s_split_ineq,
+ [| mk_nat (List.length e.Omega2.body); mk_nat i; r1 ; r2 |])
+ | (Omega2.FORGET_C _ | Omega2.FORGET _ | Omega2.FORGET_I _) :: l ->
+ loop env_hyp l
+ | (Omega2.WEAKEN _ ) :: l -> failwith "not_treated"
+ | [] -> failwith "no contradiction"
+ in loop env_hyp
+
+let rec decompose_tree env ctxt = function
+ Tree(i,left,right) ->
+ let org =
+ try Hashtbl.find env.constructors i
+ with Not_found ->
+ failwith (Printf.sprintf "Cannot find constructor %d" i) in
+ let (index,path) = find_path org ctxt in
+ let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in
+ let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in
+ app coq_e_split
+ [| mk_nat index;
+ mk_direction_list path;
+ 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
+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
+ with Not_found ->
+ failwith (Printf.sprintf "Cannot find equation %d" i) in
+ let (index,path) = find_path equation.e_origin ctxt in
+ let full_path = if equation.e_negated then path @ [O_mono] else path in
+ let cont =
+ decompose_tree_hyps trace env
+ (CCEqua equation.e_omega.Omega2.id :: ctxt) l in
+ app coq_e_extract [|mk_nat index;
+ mk_direction_list full_path;
+ cont |]
+
+(* \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
+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 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 =
+ Omega2.simplify_strong
+ ((fun () -> new_eq_id env),new_omega_id,display_omega_id)
+ system in
+ (* 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
+ Printf.printf "SYSTEME %d\n" index;
+ Omega2.display_action display_omega_id trace;
+ print_string "\n Depend :";
+ List.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 solution_tree = solve_with_constraints all_solutions [] in
+ if !debug then begin
+ 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 = list_uniq (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 = 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 = vars_of_equations equations 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,_,_) -> 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
+ - 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
+ var :: l ->
+ let t = get_reified_atom env var in
+ Hashtbl.add env.real_indices var i; t :: loop (i+1) l
+ | [] -> [] in
+ loop 0 all_vars_env in
+ let env_terms_reified = mk_list (Lazy.force coq_Z) 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
+ let reified_concl =
+ match useful_hyps with
+ (Pnot p) :: _ ->
+ reified_of_proposition env (really_useful_prop useful_equa_id p)
+ | _ -> reified_of_proposition env Pfalse in
+ let l_reified_terms =
+ (List.map
+ (fun p ->
+ reified_of_proposition env (really_useful_prop useful_equa_id p))
+ (List.tl useful_hyps)) in
+ let env_props_reified = mk_plist env.props in
+ let reified_goal =
+ mk_list (Lazy.force coq_proposition)
+ (l_reified_stated @ l_reified_terms) in
+ let reified =
+ app coq_interp_sequent
+ [| env_props_reified;env_terms_reified;reified_concl;reified_goal |] in
+ let normalize_equation e =
+ let rec loop = function
+ [] -> app (if e.e_negated then coq_p_invert else coq_p_step)
+ [| e.e_trace |]
+ | ((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
+ | (O_right :: l) -> app coq_p_right [| loop l |] in
+ app coq_pair_step
+ [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ;
+ loop e.e_origin.o_path |] in
+ let normalization_trace =
+ 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
+ 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 Term.mkVar (List.tl l_hyps)) >>
+ Tactics.change_in_concl None reified >>
+ Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|]) >>
+ show_goal >>
+ Tactics.normalise_in_concl >>
+ Tactics.apply (Lazy.force coq_I)
+
+let total_reflexive_omega_tactic gl =
+ if !Options.v7 then Util.error "ROmega does not work in v7 mode";
+ try
+ let env = new_environment () in
+ let full_reified_goal = reify_gl env gl in
+ let systems_list = destructurate_hyps full_reified_goal in
+ if !debug then begin
+ display_systems systems_list
+ end;
+ resolution env full_reified_goal systems_list gl
+ with Omega2.NO_CONTRADICTION -> Util.error "ROmega can't solve this system"
+
+
+(*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 00:15:05 +0000