diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /plugins/romega | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'plugins/romega')
-rw-r--r-- | plugins/romega/ReflOmegaCore.v | 46 | ||||
-rw-r--r-- | plugins/romega/const_omega.ml | 86 | ||||
-rw-r--r-- | plugins/romega/refl_omega.ml | 4 |
3 files changed, 73 insertions, 63 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index c82abfc8..56ae921e 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -868,11 +868,11 @@ Inductive term : Set := | Tvar : nat -> term. Delimit Scope romega_scope with term. -Arguments Scope Tint [Int_scope]. -Arguments Scope Tplus [romega_scope romega_scope]. -Arguments Scope Tmult [romega_scope romega_scope]. -Arguments Scope Tminus [romega_scope romega_scope]. -Arguments Scope Topp [romega_scope romega_scope]. +Arguments Tint _%I. +Arguments Tplus (_ _)%term. +Arguments Tmult (_ _)%term. +Arguments Tminus (_ _)%term. +Arguments Topp _%term. Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. @@ -1014,7 +1014,7 @@ Inductive h_step : Set := (* This type allows to navigate in the logical constructors that form the predicats of the hypothesis in order to decompose them. This allows in particular to extract one hypothesis from a - conjonction with possibly the right level of negations. *) + conjunction with possibly the right level of negations. *) Inductive direction : Set := | D_left : direction @@ -2038,12 +2038,12 @@ Qed. (* \subsection{La fonction de normalisation des termes (moteur de réécriture)} *) -Fixpoint rewrite (s : step) : term -> term := +Fixpoint t_rewrite (s : step) : term -> term := match s with - | C_DO_BOTH s1 s2 => apply_both (rewrite s1) (rewrite s2) - | C_LEFT s => apply_left (rewrite s) - | C_RIGHT s => apply_right (rewrite s) - | C_SEQ s1 s2 => fun t : term => rewrite s2 (rewrite s1 t) + | C_DO_BOTH s1 s2 => apply_both (t_rewrite s1) (t_rewrite s2) + | C_LEFT s => apply_left (t_rewrite s) + | C_RIGHT s => apply_right (t_rewrite s) + | C_SEQ s1 s2 => fun t : term => t_rewrite s2 (t_rewrite s1 t) | C_NOP => fun t : term => t | C_OPP_PLUS => Topp_plus | C_OPP_OPP => Topp_opp @@ -2069,7 +2069,7 @@ Fixpoint rewrite (s : step) : term -> term := | C_MULT_COMM => Tmult_comm end. -Theorem rewrite_stable : forall s : step, term_stable (rewrite s). +Theorem t_rewrite_stable : forall s : step, term_stable (t_rewrite s). Proof. simple induction s; simpl in |- *; [ intros; apply apply_both_stable; auto @@ -2453,7 +2453,7 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) := match prop2 with | EqTerm b2 b3 => if beq Null 0 - then EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term) + then EqTerm (Tint 0) (t_rewrite s (b1 + (- b3 + b2) * Tint m)%term) else TrueTerm | _ => TrueTerm end @@ -2463,7 +2463,7 @@ Definition state (m : int) (s : step) (prop1 prop2 : proposition) := Theorem state_valid : forall (m : int) (s : step), valid2 (state m s). Proof. unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify; - simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; + simpl in |- *; auto; elim (t_rewrite_stable s e); simpl in |- *; intros H1 H2; elim H1. now rewrite H2, plus_opp_l, plus_0_l, mult_0_l. Qed. @@ -2585,19 +2585,19 @@ Qed. Definition move_right (s : step) (p : proposition) := match p with - | EqTerm t1 t2 => EqTerm (Tint 0) (rewrite s (t1 + - t2)%term) - | LeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + - t1)%term) - | GeqTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + - t2)%term) - | LtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t2 + Tint (-(1)) + - t1)%term) - | GtTerm t1 t2 => LeqTerm (Tint 0) (rewrite s (t1 + Tint (-(1)) + - t2)%term) - | NeqTerm t1 t2 => NeqTerm (Tint 0) (rewrite s (t1 + - t2)%term) + | EqTerm t1 t2 => EqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) + | LeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + - t1)%term) + | GeqTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) + | LtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t2 + Tint (-(1)) + - t1)%term) + | GtTerm t1 t2 => LeqTerm (Tint 0) (t_rewrite s (t1 + Tint (-(1)) + - t2)%term) + | NeqTerm t1 t2 => NeqTerm (Tint 0) (t_rewrite s (t1 + - t2)%term) | p => p end. Theorem move_right_valid : forall s : step, valid1 (move_right s). Proof. unfold valid1, move_right in |- *; intros s ep e p; Simplify; simpl in |- *; - elim (rewrite_stable s e); simpl in |- *; + elim (t_rewrite_stable s e); simpl in |- *; [ symmetry in |- *; apply egal_left; assumption | intro; apply le_left; assumption | intro; apply le_left; rewrite <- ge_le_iff; assumption @@ -2950,14 +2950,14 @@ Qed. Theorem move_right_stable : forall s : step, prop_stable (move_right s). Proof. unfold move_right, prop_stable in |- *; intros s ep e p; split; - [ Simplify; simpl in |- *; elim (rewrite_stable s e); simpl in |- *; + [ Simplify; simpl in |- *; elim (t_rewrite_stable s e); simpl in |- *; [ symmetry in |- *; apply egal_left; assumption | intro; apply le_left; assumption | intro; apply le_left; rewrite <- ge_le_iff; assumption | intro; apply lt_left; rewrite <- gt_lt_iff; assumption | intro; apply lt_left; assumption | intro; apply ne_left_2; assumption ] - | case p; simpl in |- *; intros; auto; generalize H; elim (rewrite_stable s); + | case p; simpl in |- *; intros; auto; generalize H; elim (t_rewrite_stable s); simpl in |- *; intro H1; [ rewrite (plus_0_r_reverse (interp_term e t0)); rewrite H1; rewrite plus_permute; rewrite plus_opp_r; diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index f4368a1b..e810e15c 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -15,21 +15,27 @@ type result = | Kimp of Term.constr * Term.constr | Kufo;; +let meaningful_submodule = [ "Z"; "N"; "Pos" ] + +let string_of_global r = + let dp = Nametab.dirpath_of_global r in + let prefix = match Names.repr_dirpath dp with + | [] -> "" + | m::_ -> + let s = Names.string_of_id m in + if List.mem s meaningful_submodule then s^"." else "" + in + prefix^(Names.string_of_id (Nametab.basename_of_global r)) + let destructurate t = let c, args = Term.decompose_app t in match Term.kind_of_term c, args with | Term.Const sp, args -> - Kapp (Names.string_of_id - (Nametab.basename_of_global (Libnames.ConstRef sp)), - args) + Kapp (string_of_global (Libnames.ConstRef sp), args) | Term.Construct csp , args -> - Kapp (Names.string_of_id - (Nametab.basename_of_global (Libnames.ConstructRef csp)), - args) + Kapp (string_of_global (Libnames.ConstructRef csp), args) | Term.Ind isp, args -> - Kapp (Names.string_of_id - (Nametab.basename_of_global (Libnames.IndRef isp)), - args) + Kapp (string_of_global (Libnames.IndRef isp), args) | Term.Var id,[] -> Kvar(Names.string_of_id id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> @@ -56,9 +62,13 @@ let coq_modules = @ [module_refl_path] @ [module_refl_path@["ZOmega"]] +let bin_module = [["Coq";"Numbers";"BinNums"]] +let z_module = [["Coq";"ZArith";"BinInt"]] let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules +let z_constant = Coqlib.gen_constant_in_modules "Omega" z_module +let bin_constant = Coqlib.gen_constant_in_modules "Omega" bin_module (* Logic *) let coq_eq = lazy(init_constant "eq") @@ -168,21 +178,21 @@ let coq_do_omega = lazy (constant "do_omega") (* \subsection{Construction d'expressions} *) let do_left t = - if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop + if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop else Term.mkApp (Lazy.force coq_c_do_left, [|t |] ) let do_right t = - if t = Lazy.force coq_c_nop then Lazy.force coq_c_nop + if Term.eq_constr t (Lazy.force coq_c_nop) then Lazy.force coq_c_nop else Term.mkApp (Lazy.force coq_c_do_right, [|t |]) let do_both t1 t2 = - if t1 = Lazy.force coq_c_nop then do_right t2 - else if t2 = Lazy.force coq_c_nop then do_left t1 + if Term.eq_constr t1 (Lazy.force coq_c_nop) then do_right t2 + else if Term.eq_constr t2 (Lazy.force coq_c_nop) then do_left t1 else Term.mkApp (Lazy.force coq_c_do_both , [|t1; t2 |]) let do_seq t1 t2 = - if t1 = Lazy.force coq_c_nop then t2 - else if t2 = Lazy.force coq_c_nop then t1 + if Term.eq_constr t1 (Lazy.force coq_c_nop) then t2 + else if Term.eq_constr t2 (Lazy.force coq_c_nop) then t1 else Term.mkApp (Lazy.force coq_c_do_seq, [|t1; t2 |]) let rec do_list = function @@ -271,18 +281,18 @@ end module Z : Int = struct -let typ = lazy (constant "Z") -let plus = lazy (constant "Zplus") -let mult = lazy (constant "Zmult") -let opp = lazy (constant "Zopp") -let minus = lazy (constant "Zminus") +let typ = lazy (bin_constant "Z") +let plus = lazy (z_constant "Z.add") +let mult = lazy (z_constant "Z.mul") +let opp = lazy (z_constant "Z.opp") +let minus = lazy (z_constant "Z.sub") -let coq_xH = lazy (constant "xH") -let coq_xO = lazy (constant "xO") -let coq_xI = lazy (constant "xI") -let coq_Z0 = lazy (constant "Z0") -let coq_Zpos = lazy (constant "Zpos") -let coq_Zneg = lazy (constant "Zneg") +let coq_xH = lazy (bin_constant "xH") +let coq_xO = lazy (bin_constant "xO") +let coq_xI = lazy (bin_constant "xI") +let coq_Z0 = lazy (bin_constant "Z0") +let coq_Zpos = lazy (bin_constant "Zpos") +let coq_Zneg = lazy (bin_constant "Zneg") let recognize t = let rec loop t = @@ -318,12 +328,12 @@ let mk = mk_Z let parse_term t = try match destructurate t with - | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2) - | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2) - | Kapp("Zmult",[t1;t2]) -> Tmult (t1,t2) - | Kapp("Zopp",[t]) -> Topp t - | Kapp("Zsucc",[t]) -> Tsucc t - | Kapp("Zpred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) + | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) + | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) + | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) + | Kapp("Z.opp",[t]) -> Topp t + | Kapp("Z.succ",[t]) -> Tsucc t + | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> (try Tnum (recognize t) with _ -> Tother) | _ -> Tother @@ -334,17 +344,17 @@ let parse_rel gl t = | Kapp("eq",[typ;t1;t2]) when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) - | Kapp("Zle",[t1;t2]) -> Rle (t1,t2) - | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2) - | Kapp("Zge",[t1;t2]) -> Rge (t1,t2) - | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2) + | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) + | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) + | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) + | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) | _ -> parse_logic_rel t with e when Logic.catchable_exception e -> Rother 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"|"Zpred"),[t]) -> aux t + | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 & aux t2 + | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in try aux t with _ -> false diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 570bb187..4a6d462e 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -219,7 +219,7 @@ let unintern_omega env id = calcul des variables utiles. *) let add_reified_atom t env = - try list_index0 t env.terms + try list_index0_f Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -230,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_index0 t env.props + try list_index0_f Term.eq_constr t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i |