summaryrefslogtreecommitdiff
path: root/plugins/romega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega')
-rw-r--r--plugins/romega/ReflOmegaCore.v46
-rw-r--r--plugins/romega/const_omega.ml86
-rw-r--r--plugins/romega/refl_omega.ml4
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 23:03:26 +0000