aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/const_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega/const_omega.ml')
-rw-r--r--plugins/romega/const_omega.ml278
1 files changed, 109 insertions, 169 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 8d7ae51fc..a10ce68b4 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -10,10 +10,10 @@ let module_refl_name = "ReflOmegaCore"
let module_refl_path = ["Coq"; "romega"; module_refl_name]
type result =
- Kvar of string
- | Kapp of string * Term.constr list
- | Kimp of Term.constr * Term.constr
- | Kufo;;
+ | Kvar of string
+ | Kapp of string * Term.constr list
+ | Kimp of Term.constr * Term.constr
+ | Kufo
let meaningful_submodule = [ "Z"; "N"; "Pos" ]
@@ -30,19 +30,17 @@ let string_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 (string_of_global (Globnames.ConstRef sp), args)
- | Term.Construct (csp,_) , args ->
- Kapp (string_of_global (Globnames.ConstructRef csp), args)
- | Term.Ind (isp,_), args ->
- Kapp (string_of_global (Globnames.IndRef isp), args)
- | Term.Var id,[] -> Kvar(Names.Id.to_string id)
- | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
- | Term.Prod (Names.Name _,_,_),[] ->
- CErrors.error "Omega: Not a quantifier-free goal"
- | _ -> Kufo
-
-exception Destruct
+ | Term.Const (sp,_), args ->
+ Kapp (string_of_global (Globnames.ConstRef sp), args)
+ | Term.Construct (csp,_) , args ->
+ Kapp (string_of_global (Globnames.ConstructRef csp), args)
+ | Term.Ind (isp,_), args ->
+ Kapp (string_of_global (Globnames.IndRef isp), args)
+ | Term.Var id, [] -> Kvar(Names.Id.to_string id)
+ | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
+ | _ -> Kufo
+
+exception DestConstApp
let dest_const_apply t =
let f,args = Term.decompose_app t in
@@ -51,8 +49,8 @@ let dest_const_apply t =
| Term.Const (sp,_) -> Globnames.ConstRef sp
| Term.Construct (csp,_) -> Globnames.ConstructRef csp
| Term.Ind (isp,_) -> Globnames.IndRef isp
- | _ -> raise Destruct
- in Nametab.basename_of_global ref, args
+ | _ -> raise DestConstApp
+ in Nametab.basename_of_global ref, args
let logic_dir = ["Coq";"Logic";"Decidable"]
@@ -81,13 +79,6 @@ let coq_I = lazy(init_constant "I")
(* ReflOmegaCore/ZOmega *)
-let coq_h_step = lazy (constant "h_step")
-let coq_pair_step = lazy (constant "pair_step")
-let coq_p_left = lazy (constant "P_LEFT")
-let coq_p_right = lazy (constant "P_RIGHT")
-let coq_p_invert = lazy (constant "P_INVERT")
-let coq_p_step = lazy (constant "P_STEP")
-
let coq_t_int = lazy (constant "Tint")
let coq_t_plus = lazy (constant "Tplus")
let coq_t_mult = lazy (constant "Tmult")
@@ -110,62 +101,17 @@ let coq_p_and = lazy (constant "Tand")
let coq_p_imp = lazy (constant "Timp")
let coq_p_prop = lazy (constant "Tprop")
-(* Constructors for shuffle tactic *)
-let coq_t_fusion = lazy (constant "t_fusion")
-let coq_f_equal = lazy (constant "F_equal")
-let coq_f_cancel = lazy (constant "F_cancel")
-let coq_f_left = lazy (constant "F_left")
-let coq_f_right = lazy (constant "F_right")
-
-(* Constructors for reordering tactics *)
-let coq_c_do_both = lazy (constant "C_DO_BOTH")
-let coq_c_do_left = lazy (constant "C_LEFT")
-let coq_c_do_right = lazy (constant "C_RIGHT")
-let coq_c_do_seq = lazy (constant "C_SEQ")
-let coq_c_nop = lazy (constant "C_NOP")
-let coq_c_opp_plus = lazy (constant "C_OPP_PLUS")
-let coq_c_opp_opp = lazy (constant "C_OPP_OPP")
-let coq_c_opp_mult_r = lazy (constant "C_OPP_MULT_R")
-let coq_c_opp_one = lazy (constant "C_OPP_ONE")
-let coq_c_reduce = lazy (constant "C_REDUCE")
-let coq_c_mult_plus_distr = lazy (constant "C_MULT_PLUS_DISTR")
-let coq_c_opp_left = lazy (constant "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_r = lazy (constant "C_MULT_ASSOC_R")
-let coq_c_plus_assoc_r = lazy (constant "C_PLUS_ASSOC_R")
-let coq_c_plus_assoc_l = lazy (constant "C_PLUS_ASSOC_L")
-let coq_c_plus_permute = lazy (constant "C_PLUS_PERMUTE")
-let coq_c_plus_comm = lazy (constant "C_PLUS_COMM")
-let coq_c_red0 = lazy (constant "C_RED0")
-let coq_c_red1 = lazy (constant "C_RED1")
-let coq_c_red2 = lazy (constant "C_RED2")
-let coq_c_red3 = lazy (constant "C_RED3")
-let coq_c_red4 = lazy (constant "C_RED4")
-let coq_c_red5 = lazy (constant "C_RED5")
-let coq_c_red6 = lazy (constant "C_RED6")
-let coq_c_mult_opp_left = lazy (constant "C_MULT_OPP_LEFT")
-let coq_c_mult_assoc_reduced = lazy (constant "C_MULT_ASSOC_REDUCED")
-let coq_c_minus = lazy (constant "C_MINUS")
-let coq_c_mult_comm = lazy (constant "C_MULT_COMM")
-
-let coq_s_constant_not_nul = lazy (constant "O_CONSTANT_NOT_NUL")
-let coq_s_constant_neg = lazy (constant "O_CONSTANT_NEG")
-let coq_s_div_approx = lazy (constant "O_DIV_APPROX")
+let coq_s_bad_constant = lazy (constant "O_BAD_CONSTANT")
+let coq_s_divide = lazy (constant "O_DIVIDE")
let coq_s_not_exact_divide = lazy (constant "O_NOT_EXACT_DIVIDE")
-let coq_s_exact_divide = lazy (constant "O_EXACT_DIVIDE")
let coq_s_sum = lazy (constant "O_SUM")
-let coq_s_state = lazy (constant "O_STATE")
-let coq_s_contradiction = lazy (constant "O_CONTRADICTION")
let coq_s_merge_eq = lazy (constant "O_MERGE_EQ")
let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ")
-let coq_s_constant_nul =lazy (constant "O_CONSTANT_NUL")
-let coq_s_negate_contradict =lazy (constant "O_NEGATE_CONTRADICT")
-let coq_s_negate_contradict_inv =lazy (constant "O_NEGATE_CONTRADICT_INV")
(* construction for the [extract_hyp] tactic *)
let coq_direction = lazy (constant "direction")
let coq_d_left = lazy (constant "D_left")
let coq_d_right = lazy (constant "D_right")
-let coq_d_mono = lazy (constant "D_mono")
let coq_e_split = lazy (constant "E_SPLIT")
let coq_e_extract = lazy (constant "E_EXTRACT")
@@ -174,31 +120,6 @@ let coq_e_solve = lazy (constant "E_SOLVE")
let coq_interp_sequent = lazy (constant "interp_goal_concl")
let coq_do_omega = lazy (constant "do_omega")
-(* \subsection{Construction d'expressions} *)
-
-let do_left t =
- 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 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 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 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
- | [] -> Lazy.force coq_c_nop
- | [x] -> x
- | (x::l) -> do_seq x (do_list l)
-
(* Nat *)
let coq_S = lazy(init_constant "S")
@@ -235,8 +156,6 @@ let mk_plist =
fun l -> mk_list type1lev Term.mkProp l
let mk_list = mk_list Univ.Level.set
-let mk_shuffle_list l = mk_list (Lazy.force coq_t_fusion) l
-
type parse_term =
| Tplus of Term.constr * Term.constr
@@ -263,18 +182,40 @@ type parse_rel =
| Riff of Term.constr * Term.constr
| Rother
-let parse_logic_rel c =
- try match destructurate c with
- | Kapp("True",[]) -> Rtrue
- | Kapp("False",[]) -> Rfalse
- | Kapp("not",[t]) -> Rnot t
- | Kapp("or",[t1;t2]) -> Ror (t1,t2)
- | Kapp("and",[t1;t2]) -> Rand (t1,t2)
- | Kimp(t1,t2) -> Rimp (t1,t2)
- | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
- | _ -> Rother
- with e when Logic.catchable_exception e -> Rother
+let parse_logic_rel c = match destructurate c with
+ | Kapp("True",[]) -> Rtrue
+ | Kapp("False",[]) -> Rfalse
+ | Kapp("not",[t]) -> Rnot t
+ | Kapp("or",[t1;t2]) -> Ror (t1,t2)
+ | Kapp("and",[t1;t2]) -> Rand (t1,t2)
+ | Kimp(t1,t2) -> Rimp (t1,t2)
+ | Kapp("iff",[t1;t2]) -> Riff (t1,t2)
+ | _ -> Rother
+
+(* Binary numbers *)
+
+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 coq_N0 = lazy (bin_constant "N0")
+let coq_Npos = lazy (bin_constant "Npos")
+
+let rec mk_positive n =
+ if Bigint.equal n Bigint.one then Lazy.force coq_xH
+ else
+ let (q,r) = Bigint.euclid n Bigint.two in
+ Term.mkApp
+ ((if Bigint.equal r Bigint.zero
+ then Lazy.force coq_xO else Lazy.force coq_xI),
+ [| mk_positive q |])
+let mk_N = function
+ | 0 -> Lazy.force coq_N0
+ | n -> Term.mkApp (Lazy.force coq_Npos,
+ [| mk_positive (Bigint.of_int n) |])
module type Int = sig
val typ : Term.constr Lazy.t
@@ -287,7 +228,7 @@ module type Int = sig
val parse_term : Term.constr -> parse_term
val parse_rel : ([ `NF ], 'r) Proofview.Goal.t -> Term.constr -> parse_rel
(* check whether t is built only with numbers and + * - *)
- val is_scalar : Term.constr -> bool
+ val get_scalar : Term.constr -> Bigint.bigint option
end
module Z : Int = struct
@@ -298,38 +239,29 @@ 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 (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 recognize_pos t =
let rec loop t =
let f,l = dest_const_apply t in
match Names.Id.to_string f,l with
- "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
- | "xO",[t] -> Bigint.mult Bigint.two (loop t)
- | "xH",[] -> Bigint.one
- | _ -> failwith "not a number" in
- let f,l = dest_const_apply t in
- match Names.Id.to_string f,l with
- "Zpos",[t] -> loop t
- | "Zneg",[t] -> Bigint.neg (loop t)
- | "Z0",[] -> Bigint.zero
- | _ -> failwith "not a number";;
+ | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
+ | "xO",[t] -> Bigint.mult Bigint.two (loop t)
+ | "xH",[] -> Bigint.one
+ | _ -> raise DestConstApp
+ in
+ try Some (loop t) with DestConstApp -> None
-let rec mk_positive n =
- if n=Bigint.one then Lazy.force coq_xH
- else
- let (q,r) = Bigint.euclid n Bigint.two in
- Term.mkApp
- ((if r = Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI),
- [| mk_positive q |])
+let recognize_Z t =
+ try
+ let f,l = dest_const_apply t in
+ match Names.Id.to_string f,l with
+ | "Zpos",[t] -> recognize_pos t
+ | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t)
+ | "Z0",[] -> Some Bigint.zero
+ | _ -> None
+ with DestConstApp -> None
let mk_Z n =
- if n = Bigint.zero then Lazy.force coq_Z0
+ if Bigint.equal n Bigint.zero then Lazy.force coq_Z0
else if Bigint.is_strictly_pos n then
Term.mkApp (Lazy.force coq_Zpos, [| mk_positive n |])
else
@@ -338,38 +270,46 @@ let mk_Z n =
let mk = mk_Z
let parse_term t =
- try match destructurate t with
- | 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 e when CErrors.noncritical e -> Tother)
- | _ -> Tother
- with e when Logic.catchable_exception e -> Tother
-
-let pf_nf gl c = Tacmach.New.pf_apply Tacred.simpl gl c
+ match destructurate t with
+ | 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"),_) ->
+ (match recognize_Z t with Some t -> Tnum t | None -> Tother)
+ | _ -> Tother
+
+let pf_nf gl c =
+ EConstr.Unsafe.to_constr
+ (Tacmach.New.pf_apply Tacred.simpl gl (EConstr.of_constr c))
let parse_rel gl t =
- try match destructurate t with
- | Kapp("eq",[typ;t1;t2])
- when destructurate (EConstr.Unsafe.to_constr (pf_nf gl (EConstr.of_constr typ))) = Kapp("Z",[]) -> Req (t1,t2)
- | Kapp("Zne",[t1;t2]) -> Rne (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(("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 e when CErrors.noncritical e -> false
+ match destructurate t with
+ | Kapp("eq",[typ;t1;t2]) ->
+ (match destructurate (pf_nf gl typ) with
+ | Kapp("Z",[]) -> Req (t1,t2)
+ | _ -> Rother)
+ | Kapp("Zne",[t1;t2]) -> Rne (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
+
+let rec get_scalar t =
+ match destructurate t with
+ | Kapp("Z.add", [t1;t2]) ->
+ Option.lift2 Bigint.add (get_scalar t1) (get_scalar t2)
+ | Kapp ("Z.sub",[t1;t2]) ->
+ Option.lift2 Bigint.sub (get_scalar t1) (get_scalar t2)
+ | Kapp ("Z.mul",[t1;t2]) ->
+ Option.lift2 Bigint.mult (get_scalar t1) (get_scalar t2)
+ | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar t)
+ | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar t)
+ | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar t)
+ | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z t
+ | _ -> None
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 03:47:00 +0000