diff options
Diffstat (limited to 'plugins')
32 files changed, 452 insertions, 139 deletions
diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v new file mode 100644 index 0000000000..1891772cc2 --- /dev/null +++ b/plugins/extraction/ExtrOCamlFloats.v @@ -0,0 +1,61 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Extraction to OCaml of native binary64 floating-point numbers. + +Note: the extraction of primitive floats relies on Coq's internal file +kernel/float64.ml, so make sure the corresponding binary is available +when linking the extracted OCaml code. + +For example, if you build a (_CoqProject + coq_makefile)-based project +and if you created an empty subfolder "extracted" and a file "test.v" +containing [Cd "extracted". Separate Extraction function_to_extract.], +you will just need to add in the _CoqProject: [test.v], [-I extracted] +and the list of [extracted/*.ml] and [extracted/*.mli] files, then add +[CAMLFLAGS += -w -33] in the Makefile.local file. *) + +From Coq Require Floats Extraction. + +(** Basic data types used by some primitive operators. *) + +Extract Inductive bool => bool [ true false ]. +Extract Inductive prod => "( * )" [ "" ]. + +Extract Inductive FloatClass.float_class => + "Float64.float_class" + [ "PNormal" "NNormal" "PSubn" "NSubn" "PZero" "NZero" "PInf" "NInf" "NaN" ]. +Extract Inductive PrimFloat.float_comparison => + "Float64.float_comparison" + [ "FEq" "FLt" "FGt" "FNotComparable" ]. + +(** Primitive types and operators. *) + +Extract Constant PrimFloat.float => "Float64.t". +Extraction Inline PrimFloat.float. +(* Otherwise, the name conflicts with the primitive OCaml type [float] *) + +Extract Constant PrimFloat.classify => "Float64.classify". +Extract Constant PrimFloat.abs => "Float64.abs". +Extract Constant PrimFloat.sqrt => "Float64.sqrt". +Extract Constant PrimFloat.opp => "Float64.opp". +Extract Constant PrimFloat.eqb => "Float64.eq". +Extract Constant PrimFloat.ltb => "Float64.lt". +Extract Constant PrimFloat.leb => "Float64.le". +Extract Constant PrimFloat.compare => "Float64.compare". +Extract Constant PrimFloat.mul => "Float64.mul". +Extract Constant PrimFloat.add => "Float64.add". +Extract Constant PrimFloat.sub => "Float64.sub". +Extract Constant PrimFloat.div => "Float64.div". +Extract Constant PrimFloat.of_int63 => "Float64.of_int63". +Extract Constant PrimFloat.normfr_mantissa => "Float64.normfr_mantissa". +Extract Constant PrimFloat.frshiftexp => "Float64.frshiftexp". +Extract Constant PrimFloat.ldshiftexp => "Float64.ldshiftexp". +Extract Constant PrimFloat.next_up => "Float64.next_up". +Extract Constant PrimFloat.next_down => "Float64.next_down". diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cca212f332..04f5b66241 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -351,7 +351,7 @@ let rec extract_type env sg db j c args = | (Info, TypeScheme) -> extract_type_app env sg db (r, type_sign env sg ty) args | (Info, Default) -> Tunknown)) - | Cast _ | LetIn _ | Construct _ | Int _ -> assert false + | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], @@ -690,6 +690,7 @@ let rec extract_term env sg mle mlt c args = let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in extract_app env sg mle mlt extract_var args | Int i -> assert (args = []); MLuint i + | Float f -> assert (args = []); MLfloat f | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index e4efbcff0c..4769bef475 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -215,6 +215,8 @@ let rec pp_expr par env args = | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") | MLuint _ -> pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") + | MLfloat _ -> + pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"") and pp_cons_pat par r ppl = pp_par par diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 912a20f389..81b3e1bcdc 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -161,6 +161,10 @@ let rec json_expr env = function ("what", json_str "expr:int"); ("int", json_str (Uint63.to_string i)) ] + | MLfloat f -> json_dict [ + ("what", json_str "expr:float"); + ("float", json_str (Float64.to_string f)) + ] and json_one_pat env (ids,p,t) = let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [ diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index 8b69edbe4c..32e0d3c05d 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -126,7 +126,8 @@ and ml_ast = | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast - | MLuint of Uint63.t + | MLuint of Uint63.t + | MLfloat of Float64.t and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index e3c9635c55..32e0d3c05d 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -127,6 +127,7 @@ and ml_ast = | MLaxiom | MLmagic of ml_ast | MLuint of Uint63.t + | MLfloat of Float64.t and ml_pattern = | Pcons of GlobRef.t * ml_pattern list diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 000df26858..44b95ae4c1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -398,6 +398,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2 +| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2 | _, _ -> false and eq_ml_pattern p1 p2 = match p1, p2 with @@ -430,7 +431,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> () in iter 0 (*s Map over asts. *) @@ -449,7 +450,8 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -467,7 +469,8 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ as a -> a (*s Iter over asts. *) @@ -481,7 +484,8 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ -> () (*S Operations concerning De Bruijn indices. *) @@ -517,7 +521,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0 in nb 1 (* Replace unused variables by _ *) @@ -569,7 +573,7 @@ let dump_unused_vars a = let b' = ren env b in if b' == b then a else MLmagic b' - | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a and ren_branch env ((ids,p,b) as tr) = let occs = List.map (fun _ -> ref false) ids in @@ -1402,7 +1406,8 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom + | MLuint _ | MLfloat _ -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 6b1eef7abb..fe49bfc1ec 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> () + | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index e7004fe9af..34ddf57b40 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -307,6 +307,9 @@ let rec pp_expr par env args = | MLuint i -> assert (args=[]); str "(" ++ str (Uint63.compile i) ++ str ")" + | MLfloat f -> + assert (args=[]); + str "(" ++ str (Float64.compile f) ++ str ")" and pp_record_proj par env typ t pv args = diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index dd840cd929..c341ec8d57 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -131,6 +131,8 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") | MLuint _ -> paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") + | MLfloat _ -> + paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"") and pp_cons_args env = function | MLcons (_,r,args) when is_coinductive r -> diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 7be049269c..6db0a1119b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -692,13 +692,14 @@ let build_proof end | Cast(t,_,_) -> build_proof do_finalize {dyn_infos with info = t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ -> do_finalize dyn_infos g | App(_,_) -> let f,args = decompose_app sigma dyn_infos.info in begin match EConstr.kind sigma f with - | Int _ -> user_err Pp.(str "integer cannot be applied") + | Int _ -> user_err Pp.(str "integer cannot be applied") + | Float _ -> user_err Pp.(str "float cannot be applied") | App _ -> assert false (* we have collected all the app in decompose_app *) | Proj _ -> assert false (*FIXME*) | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 0452665585..6add56dd5b 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -68,7 +68,7 @@ let is_rec names = let check_id id names = Id.Set.mem id names in let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ -> false | GCast(b,_) -> lookup names b | GRec _ -> CErrors.user_err (Pp.str "GRec not handled") | GIf(b,_,lhs,rhs) -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7c17ecdba0..895b6a37ee 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -478,7 +478,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid | GApp(_,_) -> @@ -590,6 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") | GInt _ -> user_err Pp.(str "Cannot apply an integer") + | GFloat _ -> user_err Pp.(str "Cannot apply a float") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -1231,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) let rec compute_cst_params relnames params gt = DAst.with_val (function - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params | GApp(f,args) -> begin match DAst.get f with | GVar relname' when Id.Set.mem relname' relnames -> diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8abccabae6..5f54bad598 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -115,6 +115,7 @@ let change_vars = | GSort _ as x -> x | GHole _ as x -> x | GInt _ as x -> x + | GFloat _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) @@ -295,6 +296,7 @@ let rec alpha_rt excluded rt = | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ | GInt _ + | GFloat _ | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, @@ -354,7 +356,7 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b - | GInt _ -> false + | GInt _ | GFloat _ -> false ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -447,6 +449,7 @@ let replace_var_by_term x_id term = | GSort _ | GHole _ as rt -> rt | GInt _ as rt -> rt + | GFloat _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) @@ -529,7 +532,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map = DAst.map (function - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt | GVar id as rt -> begin try diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 29356df81d..66ed1961ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -270,7 +270,7 @@ let check_not_nested env sigma forbidden e = let rec check_not_nested e = match EConstr.kind sigma e with | Rel _ -> () - | Int _ -> () + | Int _ | Float _ -> () | Var x -> if Id.List.mem x forbidden then user_err ~hdr:"Recdef.check_not_nested" @@ -452,7 +452,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in new_continuation_tac expr_info g diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v index 0288728504..7ad5e313e3 100644 --- a/plugins/micromega/DeclConstant.v +++ b/plugins/micromega/DeclConstant.v @@ -51,7 +51,7 @@ Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3) GT A1 -> GT A2 -> GT (F A1 A2). Defined. -Require Import ZArith. +Require Import QArith_base. Instance DO : DeclaredConstant O := {}. Instance DS : DeclaredConstant S := {}. @@ -64,6 +64,4 @@ Instance DZneg: DeclaredConstant Zneg := {}. Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}. Instance DZpow : DeclaredConstant Z.pow := {}. -Require Import QArith. - Instance DQ : DeclaredConstant Qmake := {}. diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 3351c7ef8a..55a93eade7 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -15,7 +15,7 @@ (************************************************************************) Require Import ZMicromega. -Require Import ZArith. +Require Import ZArith_base. Require Import RingMicromega. Require Import VarMap. Require Import DeclConstant. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 3651b54ed8..6c1852acbf 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -22,6 +22,7 @@ Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. +Require Import Lia. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -192,7 +193,7 @@ Proof. destruct z ; try congruence. compute. congruence. compute. congruence. - generalize (Zle_0_nat n). auto with zarith. + generalize (Zle_0_nat n). auto using Z.le_ge. Qed. Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1). @@ -333,7 +334,7 @@ Proof. apply Qeq_bool_eq in C2. rewrite C2. simpl. - rewrite Qpower0 by auto with zarith. + rewrite Qpower0 by lia. apply Q2R_0. + rewrite Q2RpowerRZ. rewrite IHc. @@ -341,7 +342,7 @@ Proof. rewrite andb_false_iff in C. destruct C. simpl. apply Z.ltb_ge in H. - auto with zarith. + lia. left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index f93fe021f9..6db62e8401 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -15,7 +15,7 @@ (* *) (************************************************************************) -Require Import ZArith. +Require Import ZArith_base. Require Import Coq.Arith.Max. Require Import List. Set Implicit Arguments. diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 26970faf0c..08f3f39204 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -12,9 +12,10 @@ Require Import OrderedRing. Require Import RingMicromega. -Require Import ZArith. +Require Import ZArith_base. Require Import InitialRing. Require Import Setoid. +Require Import ZArithRing. Import OrderedRingSyntax. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index c160e11467..d709fdda14 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -21,7 +21,8 @@ Require Import RingMicromega. Require FSetPositive FSetEqProperties. Require Import ZCoeff. Require Import Refl. -Require Import ZArith. +Require Import ZArith_base. +Require Import ZArithRing. Require PreOmega. (*Declare ML Module "micromega_plugin".*) Local Open Scope Z_scope. diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v new file mode 100644 index 0000000000..0ae3f8c6a5 --- /dev/null +++ b/plugins/ssr/ssrclasses.v @@ -0,0 +1,32 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and required by [ssrunder]. + + Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing + [Require Import ssreflect] does not [Require Import RelationClasses], + and conversely. **) + +Section Defs. + Context {A : Type}. + Class Reflexive (R : A -> A -> Prop) := + reflexivity : forall x : A, R x x. +End Defs. + +Register Reflexive as plugins.ssreflect.reflexive_type. +Register reflexivity as plugins.ssreflect.reflexive_proof. + +Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A. +Instance iff_Reflexive : Reflexive iff := iff_refl. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 9ebdf71329..bc4a57dedd 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -530,102 +530,32 @@ Lemma abstract_context T (P : T -> Type) x : Proof. by move=> /(_ P); apply. Qed. (*****************************************************************************) -(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *) - -Module Type UNDER_EQ. -Parameter Under_eq : - forall (R : Type), R -> R -> Prop. -Parameter Under_eq_from_eq : - forall (T : Type) (x y : T), @Under_eq T x y -> x = y. - -(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *) -Parameter Over_eq : - forall (R : Type), R -> R -> Prop. -Parameter over_eq : - forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. -Parameter over_eq_done : - forall (T : Type) (x : T), @Over_eq T x x. -(* We need both hints below, otherwise the test-suite does not pass *) -Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core. -(* => for [test-suite/ssr/under.v:test_big_patt1] *) -Hint Resolve over_eq_done : core. -(* => for [test-suite/ssr/over.v:test_over_1_1] *) - -(** [under_eq_done]: for Ltac-style over *) -Parameter under_eq_done : - forall (T : Type) (x : T), @Under_eq T x x. -Notation "''Under[' x ]" := (@Under_eq _ x _) - (at level 8, format "''Under[' x ]", only printing). -End UNDER_EQ. - -Module Export Under_eq : UNDER_EQ. -Definition Under_eq := @eq. -Lemma Under_eq_from_eq (T : Type) (x y : T) : - @Under_eq T x y -> x = y. -Proof. by []. Qed. -Definition Over_eq := Under_eq. -Lemma over_eq : - forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y. -Proof. by []. Qed. -Lemma over_eq_done : - forall (T : Type) (x : T), @Over_eq T x x. -Proof. by []. Qed. -Lemma under_eq_done : - forall (T : Type) (x : T), @Under_eq T x x. -Proof. by []. Qed. -End Under_eq. - -Register Under_eq as plugins.ssreflect.Under_eq. -Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq. - -Module Type UNDER_IFF. -Parameter Under_iff : Prop -> Prop -> Prop. -Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y. - -(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *) -Parameter Over_iff : Prop -> Prop -> Prop. -Parameter over_iff : - forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. -Parameter over_iff_done : - forall (x : Prop), @Over_iff x x. -Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core. -Hint Resolve over_iff_done : core. - -(** [under_iff_done]: for Ltac-style over *) -Parameter under_iff_done : - forall (x : Prop), @Under_iff x x. -Notation "''Under[' x ]" := (@Under_iff x _) - (at level 8, format "''Under[' x ]", only printing). -End UNDER_IFF. - -Module Export Under_iff : UNDER_IFF. -Definition Under_iff := iff. -Lemma Under_iff_from_iff (x y : Prop) : - @Under_iff x y -> x <-> y. -Proof. by []. Qed. -Definition Over_iff := Under_iff. -Lemma over_iff : - forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y. -Proof. by []. Qed. -Lemma over_iff_done : - forall (x : Prop), @Over_iff x x. -Proof. by []. Qed. -Lemma under_iff_done : - forall (x : Prop), @Under_iff x x. -Proof. by []. Qed. -End Under_iff. - -Register Under_iff as plugins.ssreflect.Under_iff. -Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff. - -Definition over := (over_eq, over_iff). +(* Material for under/over (to rewrite under binders using "context lemmas") *) +Require Export ssrunder. + +Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => + solve [ apply: Under_rel.over_rel_done ] : core. +Hint Resolve Under_rel.over_rel_done : core. + +Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. +Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel. + +(** Closing rewrite rule *) +Definition over := over_rel. + +(** Closing tactic *) Ltac over := - by [ apply: Under_eq.under_eq_done - | apply: Under_iff.under_iff_done + by [ apply: Under_rel.under_rel_done | rewrite over ]. +(** Convenience rewrite rule to unprotect evars, e.g., to instantiate + them in another way than with reflexivity. *) +Definition UnderE := Under_relE. + +(*****************************************************************************) + (** An interface for non-Prop types; used to avoid improper instantiation of polymorphic lemmas with on-demand implicits when they are used as views. For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y. diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack index 824348fee7..46669998b9 100644 --- a/plugins/ssr/ssreflect_plugin.mlpack +++ b/plugins/ssr/ssreflect_plugin.mlpack @@ -10,4 +10,3 @@ Ssripats Ssrfwd Ssrparser Ssrvernac - diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 43aeeb2dae..baf5288725 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -42,6 +42,9 @@ val mk_rwarg : val norwmult : ssrdir * ssrmult val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option +val ssr_is_setoid : + Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool + val ssrinstancesofrule : Ltac_plugin.Tacinterp.interp_sign -> Ssrast.ssrdir -> diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index cca94c8c9b..b0f56c423f 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -340,6 +340,21 @@ let intro_lock ipats = let hnf' = Proofview.numgoals >>= fun ng -> Proofview.tclDISPATCH (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in + let protect_subgoal env sigma hd args = + Tactics.New.refine ~typecheck:true (fun sigma -> + let lm2 = Array.length args - 2 in + let sigma, carrier = + Typing.type_of env sigma args.(lm2) in + let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in + let rel_args = Array.sub args lm2 2 in + let sigma, under_rel = + Ssrcommon.mkSsrConst "Under_rel" env sigma in + let sigma, under_from_rel = + Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in + let under_rel_args = Array.append [|carrier; rel|] rel_args in + let ty = EConstr.mkApp (under_rel, under_rel_args) in + let sigma, t = Evarutil.new_evar env sigma ty in + sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) in let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ -> Proofview.tclORELSE (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())]) @@ -349,30 +364,23 @@ let intro_lock ipats = let env = Proofview.Goal.env gl in match EConstr.kind_of_type sigma c with | Term.AtomicType(hd, args) when + Array.length args >= 2 && is_app_evar sigma (Array.last args) && + Ssrequality.ssr_is_setoid env sigma hd args + (* if the last condition above [ssr_is_setoid ...] holds + then [Coq.Classes.RelationClasses] has been required *) + || + (* if this is not the case, the tactic can still succeed + when the considered relation is [Coq.Init.Logic.iff] *) Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") && - Array.length args = 2 && is_app_evar sigma args.(1) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under_iff = - Ssrcommon.mkSsrConst "Under_iff" env sigma in - let sigma, under_from_iff = - Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in - let ty = EConstr.mkApp (under_iff,args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|])) + Array.length args = 2 && is_app_evar sigma args.(1) -> + protect_subgoal env sigma hd args | _ -> let t = Reductionops.whd_all env sigma c in match EConstr.kind_of_type sigma t with | Term.AtomicType(hd, args) when Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") && Array.length args = 3 && is_app_evar sigma args.(2) -> - Tactics.New.refine ~typecheck:true (fun sigma -> - let sigma, under = - Ssrcommon.mkSsrConst "Under_eq" env sigma in - let sigma, under_from_eq = - Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in - let ty = EConstr.mkApp (under,args) in - let sigma, t = Evarutil.new_evar env sigma ty in - sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|])) + protect_subgoal env sigma hd args | _ -> ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v new file mode 100644 index 0000000000..609c9d5ab8 --- /dev/null +++ b/plugins/ssr/ssrsetoid.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Compatibility layer for [under] and [setoid_rewrite]. + + This file is intended to be required by [Require Import Setoid]. + + In particular, we can use the [under] tactic with other relations + than [eq] or [iff], e.g. a [RewriteRelation], by doing: + [Require Import ssreflect. Require Setoid.] + + This file's instances have priority 12 > other stdlib instances + and each [Under_rel] instance comes with a [Hint Cut] directive + (otherwise Ring_polynom.v won't compile because of unbounded search). + + (Note: this file could be skipped when porting [under] to stdlib2.) + *) + +Require Import ssrclasses. +Require Import ssrunder. +Require Import RelationClasses. +Require Import Relation_Definitions. + +(** Reconcile [Coq.Classes.RelationClasses.Reflexive] with + [Coq.ssr.ssrclasses.Reflexive] *) + +Instance compat_Reflexive : + forall {A} {R : relation A}, + RelationClasses.Reflexive R -> + ssrclasses.Reflexive R | 12. +Proof. now trivial. Qed. + +(** Add instances so that ['Under[ F i ]] terms, + that is, [Under_rel T R (F i) (?G i)] terms, + can be manipulated with rewrite/setoid_rewrite with lemmas on [R]. + Note that this requires that [R] is a [Prop] relation, otherwise + a [bool] relation may need to be "lifted": see the [TestPreOrder] + section in test-suite/ssr/under.v *) + +Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12. +Proof. now rewrite Under_relE. Qed. + +(* see also Morphisms.trans_co_eq_inv_impl_morphism *) + +Instance Under_Reflexive {A} (R : relation A) : + RelationClasses.Reflexive R -> + RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances. + +(* These instances are a bit off-topic given that (Under_rel A R) will + typically be reflexive, to be able to trigger the [over] terminator + +Instance under_Irreflexive {A} (R : relation A) : + RelationClasses.Irreflexive R -> + RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances. + +Instance under_Asymmetric {A} (R : relation A) : + RelationClasses.Asymmetric R -> + RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances. + +Instance under_StrictOrder {A} (R : relation A) : + RelationClasses.StrictOrder R -> + RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances. + *) + +Instance Under_Symmetric {A} (R : relation A) : + RelationClasses.Symmetric R -> + RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances. + +Instance Under_Transitive {A} (R : relation A) : + RelationClasses.Transitive R -> + RelationClasses.Transitive (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances. + +Instance Under_PreOrder {A} (R : relation A) : + RelationClasses.PreOrder R -> + RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances. + +Instance Under_PER {A} (R : relation A) : + RelationClasses.PER R -> + RelationClasses.PER (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_PER Under_PER] : typeclass_instances. + +Instance Under_Equivalence {A} (R : relation A) : + RelationClasses.Equivalence R -> + RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12. +Proof. now rewrite Under_rel.Under_relE. Qed. + +Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances. + +(* Don't handle Antisymmetric and PartialOrder classes for now, + as these classes depend on two relation symbols... *) diff --git a/plugins/ssr/ssrunder.v b/plugins/ssr/ssrunder.v new file mode 100644 index 0000000000..7c529a6133 --- /dev/null +++ b/plugins/ssr/ssrunder.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + +(** Constants for under/over, to rewrite under binders using "context lemmas" + + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and *exported* by [ssrunder]. + + This preserves the following feature: we can use [Setoid] without + requiring [ssreflect] and use [ssreflect] without requiring [Setoid]. +*) + +Require Import ssrclasses. + +Module Type UNDER_REL. +Parameter Under_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Parameter Under_relE : + forall (A : Type) (eqA : A -> A -> Prop), + @Under_rel A eqA = eqA. + +(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *) +Parameter Over_rel : + forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop. +Parameter over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Parameter over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. + +(** [under_rel_done]: for Ltac-style over *) +Parameter under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Notation "''Under[' x ]" := (@Under_rel _ _ x _) + (at level 8, format "''Under[' x ]", only printing). +End UNDER_REL. + +Module Export Under_rel : UNDER_REL. +Definition Under_rel (A : Type) (eqA : A -> A -> Prop) := + eqA. +Lemma Under_rel_from_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y -> eqA x y. +Proof. now trivial. Qed. +Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) : + @Under_rel A eqA = eqA. +Proof. now trivial. Qed. +Definition Over_rel := Under_rel. +Lemma over_rel : + forall (A : Type) (eqA : A -> A -> Prop) (x y : A), + @Under_rel A eqA x y = @Over_rel A eqA x y. +Proof. now trivial. Qed. +Lemma over_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Over_rel A eqA x x. +Proof. now unfold Over_rel. Qed. +Lemma under_rel_done : + forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A), + @Under_rel A eqA x x. +Proof. now trivial. Qed. +End Under_rel. diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 4d7a04f5ee..9682487a22 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -319,7 +319,7 @@ let iter_constr_LR f c = match kind c with for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ - | Int _) -> () + | Int _ | Float _) -> () (* The comparison used to determine which subterms matches is KEYED *) (* CONVERSION. This looks for convertible terms that either have the same *) diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml new file mode 100644 index 0000000000..3c2e217d1c --- /dev/null +++ b/plugins/syntax/float_syntax.ml @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Glob_term + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "float_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +(*** Constants for locating float constructors ***) + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +(*** Parsing for float in digital notation ***) + +let interp_float ?loc (sign,n) = + let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in + DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n))) + +(* Pretty printing is already handled in constrextern.ml *) + +let uninterp_float _ = None + +(* Actually declares the interpreter for float *) + +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let float_module = ["Coq"; "Floats"; "PrimFloat"] +let float_path = make_path float_module "float" +let float_scope = "float_scope" + +let _ = + register_rawnumeral_interpretation float_scope (interp_float,uninterp_float); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = float_scope; + pt_interp_info = Uid float_scope; + pt_required = (float_path,float_module); + pt_refs = []; + pt_in_match = false } diff --git a/plugins/syntax/float_syntax_plugin.mlpack b/plugins/syntax/float_syntax_plugin.mlpack new file mode 100644 index 0000000000..d69f49bcfe --- /dev/null +++ b/plugins/syntax/float_syntax_plugin.mlpack @@ -0,0 +1 @@ +Float_syntax diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune index 7a23581768..512752135d 100644 --- a/plugins/syntax/plugin_base.dune +++ b/plugins/syntax/plugin_base.dune @@ -25,3 +25,10 @@ (synopsis "Coq syntax plugin: int63") (modules int63_syntax) (libraries coq.vernac)) + +(library + (name float_syntax_plugin) + (public_name coq.plugins.float_syntax) + (synopsis "Coq syntax plugin: float") + (modules float_syntax) + (libraries coq.vernac)) |