diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 28 |
1 files changed, 1 insertions, 27 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f55458de8d..446e71b40c 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -42,7 +42,6 @@ let elim_id id = simplest_elim (mkVar id) let resolve_id id = apply (mkVar id) -let display_time_flag = ref false let display_system_flag = ref false let display_action_flag = ref false let old_style_flag = ref false @@ -114,10 +113,6 @@ let new_identifier = let cpt = intref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s) -let new_identifier_state = - let cpt = intref 0 in - (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) - let new_identifier_var = let cpt = intref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s) @@ -153,7 +148,6 @@ let mk_then tacs = tclTHENLIST tacs let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c]) let generalize_tac t = generalize t -let elim t = simplest_elim t let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let pf_nf gl c = pf_apply Tacred.simpl gl c @@ -165,10 +159,9 @@ let rev_assoc k = in loop -let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = +let tag_hypothesis, hyp_of_tag, clear_tags = let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> try Id.List.assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), (fun () -> l := []) @@ -363,23 +356,18 @@ let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) -let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) -let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) let sp_not = lazy (evaluable_ref_of_constr "not" coq_not) -let mk_var v = mkVar (Id.of_string v) let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |]) let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |]) let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |]) let mk_gen_eq ty t1 t2 = mkApp (Lazy.force coq_eq, [| ty; t1; t2 |]) let mk_eq t1 t2 = mk_gen_eq (Lazy.force coq_Z) t1 t2 -let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |]) let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |]) let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |]) let mk_and t1 t2 = mkApp (Lazy.force coq_and, [| t1; t2 |]) let mk_or t1 t2 = mkApp (Lazy.force coq_or, [| t1; t2 |]) let mk_not t = mkApp (Lazy.force coq_not, [| t |]) -let mk_eq_rel t1 t2 = mk_gen_eq (Lazy.force coq_comparison) t1 t2 let mk_inj t = mkApp (Lazy.force coq_Z_of_nat, [| t |]) let mk_integer n = @@ -403,10 +391,6 @@ type omega_constant = | Le | Lt | Ge | Gt | Other of string -type omega_proposition = - | Keq of constr * constr * constr - | Kn - type result = | Kvar of Id.t | Kapp of omega_constant * constr list @@ -584,7 +568,6 @@ let focused_simpl path = focused_simpl path type oformula = | Oplus of oformula * oformula - | Oinv of oformula | Otimes of oformula * oformula | Oatom of Id.t | Oz of bigint @@ -594,7 +577,6 @@ let rec oprint = function | Oplus(t1,t2) -> print_string "("; oprint t1; print_string "+"; oprint t2; print_string ")" - | Oinv t -> print_string "~"; oprint t | Otimes (t1,t2) -> print_string "("; oprint t1; print_string "*"; oprint t2; print_string ")" @@ -605,7 +587,6 @@ let rec oprint = function let rec weight = function | Oatom c -> intern_id c | Oz _ -> -1 - | Oinv c -> weight c | Otimes(c,_) -> weight c | Oplus _ -> failwith "weight" | Oufo _ -> -1 @@ -613,7 +594,6 @@ let rec weight = function let rec val_of = function | Oatom c -> mkVar c | Oz c -> mk_integer c - | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |]) | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |]) | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |]) | Oufo c -> c @@ -908,10 +888,6 @@ let rec scalar p n = function clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zmult_plus_distr_l) :: (tac1 @ tac2), Oplus(t1',t2') - | Oinv t -> - [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] - (Lazy.force coq_fast_Zmult_opp_comm); - focused_simpl (P_APP 2 :: p)], Otimes(t,Oz(neg n)) | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zmult_assoc_reverse); @@ -963,8 +939,6 @@ let rec negate p = function (Lazy.force coq_fast_Zopp_plus_distr) :: (tac1 @ tac2), Oplus(t1',t2') - | Oinv t -> - [clever_rewrite p [[P_APP 1;P_APP 1]] (Lazy.force coq_fast_Zopp_involutive)], t | Otimes(t1,Oz x) -> [clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 1;P_APP 2]] (Lazy.force coq_fast_Zopp_mult_distr_r); |