diff options
81 files changed, 459 insertions, 3895 deletions
@@ -8,6 +8,10 @@ Plugins externally, the Coq development team can provide assistance for extracting the plugin and setting up a new repository. +Tactics + +- Removed the deprecated `romega` tactics. + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -69,6 +73,10 @@ Tactics - The `romega` tactics have been deprecated; please use `lia` instead. +- Names of existential variables occurring in Ltac functions + (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted + the same way as other variable names occurring in Ltac functions. + Focusing - Focusing bracket `{` now supports named goal selectors, diff --git a/META.coq.in b/META.coq.in index a7bf08ec49..1ccde1338f 100644 --- a/META.coq.in +++ b/META.coq.in @@ -301,18 +301,6 @@ package "plugins" ( archive(native) = "omega_plugin.cmx" ) - package "romega" ( - - description = "Coq romega plugin" - version = "8.10" - - requires = "coq.plugins.omega" - directory = "romega" - - archive(byte) = "romega_plugin.cmo" - archive(native) = "romega_plugin.cmx" - ) - package "micromega" ( description = "Coq micromega plugin" diff --git a/Makefile.common b/Makefile.common index 69dea1d284..f90919a4bc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -95,7 +95,7 @@ CORESRCDIRS:=\ tactics vernac stm toplevel PLUGINDIRS:=\ - omega romega micromega \ + omega micromega \ setoid_ring extraction \ cc funind firstorder derive \ rtauto nsatz syntax btauto \ @@ -129,7 +129,6 @@ GRAMMARCMA:=grammar/grammar.cma ########################################################################### OMEGACMO:=plugins/omega/omega_plugin.cmo -ROMEGACMO:=plugins/romega/romega_plugin.cmo MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo RINGCMO:=plugins/setoid_ring/newring_plugin.cmo NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo @@ -150,7 +149,7 @@ LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo SSRCMO:=plugins/ssr/ssreflect_plugin.cmo -PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ +PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \ $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ diff --git a/Makefile.dev b/Makefile.dev index 2a7e61126a..82b81908ac 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -169,7 +169,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ ################ OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) -ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) @@ -181,7 +180,7 @@ CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) -omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) +omega: $(OMEGAVO) $(OMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) setoid_ring: $(RINGVO) $(RINGCMO) nsatz: $(NSATZVO) $(NSATZCMO) diff --git a/checker/environ.ml b/checker/environ.ml index 74cf237763..b172acb126 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -183,7 +183,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined.") + Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8f11e01c33..1fd86bc368 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds = (************************************************************************) (************************************************************************) +let print_mutind ind = + let kn = MutInd.user ind in + str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn)) + let check_inductive env kn mib = - Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); + Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn); (* check mind_constraints: should be consistent with env *) let env0 = match mib.mind_universes with diff --git a/checker/typeops.ml b/checker/typeops.ml index 138fe8bc95..e4c3f4ae4b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index bccd3fefb4..85bb04efe0 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ - -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ + -I $COQTOP/plugins/ring \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6b7960c92f..dd3908c25f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -765,8 +765,6 @@ Conflicts exists between integers and constrs. %% plugins/ring \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}} \nlsep \TERM{ring}~\STAR{\tacconstr} -%% plugins/romega -\nlsep \TERM{romega} \SEPDEF \DEFNT{orient} \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 47cfeb98d7..ea126e2756 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -10,7 +10,7 @@ let ppripos (ri,pos) = | Reloc_annot a -> let sp,i = a.ci.ci_ind in print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index d03a31c044..3b9760f586 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -112,11 +112,11 @@ and checked to be :math:`-1`. .. tacn:: lia :name: lia -This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega` -tactics. Roughly speaking, the deductive power of lia is the combined deductive -power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear -goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following -so-called *omega nightmare* :cite:`TheOmegaPaper`. + This tactic offers an alternative to the :tacn:`omega` tactic. Roughly + speaking, the deductive power of lia is the combined deductive power of + :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals + that :tacn:`omega` does not solve, such as the following so-called *omega + nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and -:tacn:`romega` is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 828505b850..03d4f148e3 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -23,13 +23,6 @@ Description of ``omega`` If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. -.. tacv:: romega - :name: romega - - .. deprecated:: 8.9 - - Use :tacn:`lia` instead. - Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/engine/termops.ml b/engine/termops.ml index 156d1370e3..710743e92d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -49,6 +49,8 @@ let pr_puniverses p u = if Univ.Instance.is_empty u then p else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" +(* Minimalistic constr printer, typically for debugging *) + let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" diff --git a/engine/termops.mli b/engine/termops.mli index b967bb6abb..9ce2db9234 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,11 +311,17 @@ val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t -(** debug printer: do not use to display terms to the casual user... *) +(** Internal hook to register user-level printer *) val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit + +(** User-level printers *) + val print_constr : constr -> Pp.t val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t + +(** debug printer: do not use to display terms to the casual user... *) + val print_named_context : env -> Pp.t val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ddc0a5c000..3996a1756c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -102,7 +102,7 @@ let _show_inactive_notations () = (function | NotationRule (scopt, ntn) -> Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) - | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn))) + | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)))) !inactive_notations_table let deactivate_notation nr = @@ -135,8 +135,9 @@ let reactivate_notation nr = ++ str "is already active" ++ show_scope scopt ++ str ".") | SynDefRule kn -> + let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in Feedback.msg_warning - (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn) + (str "Notation" ++ spc () ++ str s ++ spc () ++ str "is already active.") diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fd9394025a..c4c96c9b55 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -281,7 +281,7 @@ let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache} as infos) tab ref = +let ref_value_cache ({i_cache = cache;_} as infos) tab ref = try Some (KeyTable.find tab ref) with Not_found -> @@ -289,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let body = match ref with | RelKey n -> - let open Context.Rel.Declaration in + let open! Context.Rel.Declaration in let i = n - 1 in let (d, _) = try Range.get cache.i_rels i @@ -837,7 +837,7 @@ let eta_expand_ind_stack env ind m s (f, s') = arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in + let (depth, args, _s) = strip_update_shift_app m s in (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> @@ -925,7 +925,7 @@ and knht info e t stk = | Fix _ -> knh info (mk_clos2 e t) stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p,c) -> knh info (mk_clos2 e t) stk + | Proj (_p,_c) -> knh info (mk_clos2 e t) stk | (Lambda _|Prod _|Construct _|CoFix _|Ind _| LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> (mk_clos2 e t, stk) @@ -952,7 +952,7 @@ let rec knr info tab m stk = (match ref_value_cache info tab (RelKey k) with Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) -> + | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then @@ -1018,7 +1018,7 @@ let rec zip_term zfun m stk = zip_term zfun h s | Zshift(n)::s -> zip_term zfun (lift n m) s - | Zupdate(rf)::s -> + | Zupdate(_rf)::s -> zip_term zfun m s (* Computes the strong normal form of a term. @@ -1038,7 +1038,7 @@ let rec kl info tab m = and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with - | FLambda(n,tys,f,e) -> + | FLambda(_n,tys,f,e) -> let (e',rvtys) = List.fold_left (fun (e,ctxt) (na,ty) -> (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ed3bd866a4..c63795b295 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -126,8 +126,8 @@ let compare e1 e2 = match e1, e2 with | FVrel r1, FVrel r2 -> Int.compare r1 r2 | FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 -| FVuniv_var i1, FVevar _ -> -1 +| FVuniv_var _i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _i1, FVevar _ -> -1 | FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 | FVevar e1, FVevar e2 -> Evar.compare e1 e2 diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5362f9a814..73620ae578 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -413,7 +413,7 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant cenv sc sz cont = +let compile_structured_constant _cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont @@ -534,7 +534,7 @@ let rec compile_lam env cenv lam sz cont = comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - | Llet (id,def,body) -> + | Llet (_id,def,body) -> compile_lam env cenv def sz (Kpush :: compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) @@ -561,7 +561,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end - | Lfix ((rec_args, init), (decl, types, bodies)) -> + | Lfix ((rec_args, init), (_decl, types, bodies)) -> let ndef = Array.length types in let rfv = ref empty_fv in let lbl_types = Array.make ndef Label.no in @@ -594,7 +594,7 @@ let rec compile_lam env cenv lam sz cont = (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - | Lcofix(init, (decl,types,bodies)) -> + | Lcofix(init, (_decl,types,bodies)) -> let ndef = Array.length types in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 31dede6f5d..c21ce22421 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -107,7 +107,7 @@ let rec pp_lam lam = | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim((kn,_u),ar,op,args) -> + | Lprim((kn,_u),_ar,_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ @@ -215,7 +215,7 @@ let rec map_lam_with_binders g f n lam = let u' = map_uint g f n u in if u == u' then lam else Luint u' -and map_uint g f n u = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(args) -> @@ -532,7 +532,7 @@ struct size = 0; } - let extend v = + let extend (v : 'a t) = if v.size = Array.length v.elems then let new_size = min (2*v.size) Sys.max_array_length in if new_size <= v.size then raise (Invalid_argument "Vect.extend"); @@ -545,12 +545,12 @@ struct v.elems.(v.size) <- a; v.size <- v.size + 1 - let popn v n = + let popn (v : 'a t) n = v.size <- max 0 (v.size - n) let pop v = popn v 1 - let get_last v n = + let get_last (v : 'a t) n = if v.size <= n then raise (Invalid_argument "Vect.get:index out of bounds"); v.elems.(v.size - n - 1) @@ -715,7 +715,7 @@ let rec lambda_of_constr env c = and lambda_of_app env f args = match Constr.kind f with - | Const (kn,u as c) -> + | Const (kn,_u as c) -> let kn = get_alias env.global_env kn in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function diff --git a/kernel/constr.ml b/kernel/constr.ml index c73fe7fbde..b25f38d630 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -360,17 +360,17 @@ let destConst c = match kind c with (* Destructs an existential variable *) let destEvar c = match kind c with - | Evar (kn, a as r) -> r + | Evar (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a (co)inductive type named kn *) let destInd c = match kind c with - | Ind (kn, a as r) -> r + | Ind (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a constructor *) let destConstruct c = match kind c with - | Construct (kn, a as r) -> r + | Construct (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) @@ -421,12 +421,12 @@ let fold f acc c = match kind c with | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c + | Proj (_p,c) -> f acc c | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> + | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> + | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl (* [iter f c] iters [f] on the immediate subterms of [c]; it is @@ -441,7 +441,7 @@ let iter f c = match kind c with | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c + | Proj (_p,c) -> f c | Evar (_,l) -> Array.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -463,7 +463,7 @@ let iter_with_binders g f n c = match kind c with | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> Array.Fun1.iter f n l | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl - | Proj (p,c) -> f n c + | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl @@ -483,19 +483,19 @@ let fold_constr_with_binders g f n acc c = | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g n) (f n acc t) c - | Lambda (na,t,c) -> f (g n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | Prod (_na,t,c) -> f (g n) (f n acc t) c + | Lambda (_na,t,c) -> f (g n) (f n acc t) c + | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c + | Proj (_p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -963,11 +963,11 @@ let constr_ord_int f t1 t2 = | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | App _, _ -> -1 | _, App _ -> 1 - | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -1226,9 +1226,9 @@ let rec hash t = combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) - | Fix (ln ,(_, tl, bl)) -> + | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) - | CoFix(ln, (_, tl, bl)) -> + | CoFix(_ln, (_, tl, bl)) -> combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n diff --git a/kernel/context.ml b/kernel/context.ml index 4a7204b75c..3d98381fbb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,8 +142,8 @@ struct (** Reduce all terms in a given declaration to a single value. *) let fold_constr f decl acc = match decl with - | LocalAssum (n,ty) -> f ty acc - | LocalDef (n,v,ty) -> f ty (f v acc) + | LocalAssum (_n,ty) -> f ty acc + | LocalDef (_n,v,ty) -> f ty (f v acc) let to_tuple = function | LocalAssum (na, ty) -> na, None, ty @@ -151,7 +151,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (na, v, ty) -> LocalAssum (na, ty) + | LocalDef (na, _v, ty) -> LocalAssum (na, ty) end @@ -356,7 +356,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (id, v, ty) -> LocalAssum (id, ty) + | LocalDef (id, _v, ty) -> LocalAssum (id, ty) let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 7ef63c1860..c74f2ab318 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -42,7 +42,7 @@ let empty = { cst_trstate = Cpred.full; } -let get_strategy { var_opacity; cst_opacity } f = function +let get_strategy { var_opacity; cst_opacity; _ } f = function | VarKey id -> (try Id.Map.find id var_opacity with Not_found -> default) @@ -51,7 +51,7 @@ let get_strategy { var_opacity; cst_opacity } f = function with Not_found -> default) | RelKey _ -> Expand -let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = +let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l = match k with | VarKey id -> let var_opacity = @@ -75,13 +75,13 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = { oracle with cst_opacity; cst_trstate; } | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") -let fold_strategy f { var_opacity; cst_opacity; } accu = +let fold_strategy f { var_opacity; cst_opacity; _ } accu = let fvar id lvl accu = f (VarKey id) lvl accu in let fcst cst lvl accu = f (ConstKey cst) lvl accu in let accu = Id.Map.fold fvar var_opacity accu in Cmap.fold fcst cst_opacity accu -let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) +let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 657478a106..b361e36bbf 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -91,7 +91,7 @@ let update_case_info cache ci modlist = try let ind, n = match share cache (IndRef ci.ci_ind) modlist with - | (IndRef f,(u,l)) -> (f, Array.length l) + | (IndRef f,(_u,l)) -> (f, Array.length l) | _ -> assert false in { ci with ci_ind = ind; ci_npar = ci.ci_npar + n } with Not_found -> diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index bb9231d000..8bef6aec42 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -173,7 +173,7 @@ and slot_for_fv env fv = | Some (v, _) -> v end | FVevar evk -> val_of_evar evk - | FVuniv_var idu -> + | FVuniv_var _idu -> assert false and eval_to_patch env (buff,pl,fv) = @@ -192,5 +192,5 @@ and val_of_constr env c = | Some v -> eval_to_patch env (to_memory v) | None -> assert false -let set_transparent_const kn = () (* !?! *) -let set_opaque_const kn = () (* !?! *) +let set_transparent_const _kn = () (* !?! *) +let set_opaque_const _kn = () (* !?! *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 51ec3defb3..d995786d97 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -181,7 +181,7 @@ let subst_regular_ind_arity sub s = if uar' == s.mind_user_arity then s else { mind_user_arity = uar'; mind_sort = s.mind_sort } -let subst_template_ind_arity sub s = s +let subst_template_ind_arity _sub s = s (* FIXME records *) let subst_ind_arity = @@ -240,14 +240,14 @@ let inductive_polymorphic_context mib = let inductive_is_polymorphic mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> true - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> true + | Cumulative_ind _cumi -> true let inductive_is_cumulative mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> false - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> false + | Cumulative_ind _cumi -> true let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with diff --git a/kernel/dune b/kernel/dune index 011af9c28c..a503238907 100644 --- a/kernel/dune +++ b/kernel/dune @@ -13,3 +13,8 @@ (documentation (package coq)) + +; In dev profile, we check the kernel against a more strict set of +; warnings. +(env + (dev (flags :standard -w +a-4-44-50))) diff --git a/kernel/environ.ml b/kernel/environ.ml index 3bfcaa7f52..dffcd70282 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -296,12 +296,12 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) -open Context.Named.Declaration - let named_type id env = + let open Context.Named.Declaration in get_type (lookup_named id env) let named_body id env = + let open Context.Named.Declaration in get_value (lookup_named id env) let evaluable_named id env = @@ -333,7 +333,7 @@ let fold_named_context f env ~init = let rec fold_right env = match match_named_context_val env.env_named_context with | None -> init - | Some (d, v, rem) -> + | Some (d, _v, rem) -> let env = reset_with_named_context rem env in f env d (fold_right env) @@ -415,7 +415,7 @@ let constant_type env (kn,u) = let cb = lookup_constant kn env in match cb.const_universes with | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty - | Polymorphic_const ctx -> + | Polymorphic_const _ctx -> let csts = constraints_of cb u in (subst_instance_constr u cb.const_type, csts) @@ -508,14 +508,14 @@ let get_projections env ind = Declareops.inductive_make_projections ind mib (* Mutual Inductives *) -let polymorphic_ind (mind,i) env = +let polymorphic_ind (mind,_i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false else polymorphic_ind ind env -let type_in_type_ind (mind,i) env = +let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes let template_polymorphic_ind (mind,i) env = @@ -527,7 +527,7 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn (mind, _ as mind_key) env = +let add_mind_key kn (_mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = { env.env_globals with @@ -543,7 +543,7 @@ let lookup_constant_variables c env = let cmap = lookup_constant c env in Context.Named.to_vars cmap.const_hyps -let lookup_inductive_variables (kn,i) env = +let lookup_inductive_variables (kn,_i) env = let mis = lookup_mind kn env in Context.Named.to_vars mis.mind_hyps @@ -579,6 +579,7 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = + let open! Context.Named.Declaration in Context.Named.fold_inside (fun need decl -> if Id.Set.mem (get_id decl) need then @@ -594,6 +595,7 @@ let really_needed env needed = (named_context env) let keep_hyps env needed = + let open Context.Named.Declaration in let really_needed = really_needed env needed in Context.Named.fold_outside (fun d nsign -> @@ -647,6 +649,7 @@ type unsafe_type_judgment = types punsafe_type_judgment exception Hyp_not_found let apply_to_hyp ctxt id f = + let open Context.Named.Declaration in let rec aux rtail ctxt = match match_named_context_val ctxt with | Some (d, v, ctxt) -> @@ -663,6 +666,7 @@ let remove_hyps ids check_context check_value ctxt = let rec remove_hyps ctxt = match match_named_context_val ctxt with | None -> empty_named_context_val, false | Some (d, v, rctxt) -> + let open Context.Named.Declaration in let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) else if not seen then ctxt, false diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7abf8027bd..b976469ff7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -242,7 +242,7 @@ let check_subtyping cumi paramsctxt env_ar inds = in let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) - Array.iter (fun (id,cn,lc,(sign,arity)) -> + Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; @@ -368,7 +368,7 @@ let typecheck_inductive env mie = RegularArity (not is_natural,full_arity,defu) in let template_polymorphic () = - let _, s = + let _sign, s = try dest_arity env full_arity with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) in @@ -428,7 +428,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum let explain_ind_err id ntyp env nparamsctxt c err = - let (lparams,c') = mind_extract_params nparamsctxt c in + let (_lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt)))) @@ -596,7 +596,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) - | err -> + | _err -> (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) @@ -613,7 +613,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( defined types, not one of the types of the mutually inductive block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) - and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = + and check_positive_nested (env,n,ntypes,_ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnrecpar = mib.mind_nparams_rec in let auxnnonrecpar = mib.mind_nparams - auxnrecpar in @@ -664,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( the type [c]) is checked to be the right (properly applied) inductive type. *) and check_constructors ienv check_head nmr c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = + let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -813,7 +813,7 @@ let compute_projections (kn, i as ind) mib = in let projections decl (i, j, labs, pbs, letsubst) = match decl with - | LocalDef (na,c,t) -> + | LocalDef (_na,c,_t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in @@ -841,7 +841,7 @@ let compute_projections (kn, i as ind) mib = (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, labs, pbs, letsubst) = + let (_, _, labs, pbs, _letsubst) = List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev labs), diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1d2f22b006..9bbcf07f7e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -154,10 +154,10 @@ let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) - | d::sign, None::exp, args -> + | _d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in make subst (sign, exp, args) - | d::sign, Some u::exp, a::args -> + | _d::sign, Some u::exp, a::args -> (* We recover the level of the argument, but we don't change the *) (* level in the corresponding type in the arity; this level in the *) (* arity is a global level which, at typing time, will be enforce *) @@ -165,7 +165,7 @@ let make_subst env = (* a useless extra constraint *) let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | LocalAssum (na,t) :: sign, Some u::exp, [] -> + | LocalAssum (_na,_t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -173,7 +173,7 @@ let make_subst env = (* update its image [x] by [sup x u] in order not to forget the *) (* dependency in [u] that remains to be fullfilled. *) make (remember_subst u subst) (sign, exp, []) - | sign, [], _ -> + | _sign, [], _ -> (* Uniform parameters are exhausted *) subst | [], _, _ -> @@ -199,7 +199,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -215,12 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = let type_of_inductive env pind = type_of_inductive_gen env pind [||] -let constrained_type_of_inductive env ((mib,mip),u as pind) = +let constrained_type_of_inductive env ((mib,_mip),u as pind) = let ty = type_of_inductive env pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = +let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = let ty = type_of_inductive_gen env pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -249,7 +249,7 @@ let type_of_constructor (cstr, u) (mib,mip) = if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = +let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let ty = type_of_constructor cstru ind in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -279,7 +279,7 @@ let inductive_sort_family mip = let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (ind,u) (mib,mip) params = +let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s @@ -563,7 +563,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_all env s) in + let i,_l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -635,10 +635,10 @@ let get_recargs_approx env tree ind args = build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end - | err -> + | _err -> mk_norec - and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = + and build_recargs_nested (env,_ra_env as ienv) tree (((mind,i),u), largs) = (* If the inferred tree already disallows recursion, no need to go further *) if eq_wf_paths tree mk_norec then tree else @@ -676,7 +676,7 @@ let get_recargs_approx env tree ind args = (Rtree.mk_rec irecargs).(i) and build_recargs_constructors ienv trees c = - let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = + let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -685,7 +685,7 @@ let get_recargs_approx env tree ind args = let recarg = build_recargs ienv (List.hd trees) b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d - | hd -> + | _hd -> List.rev lrec in recargs_constr_rec ienv trees [] c @@ -794,7 +794,7 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> + | Subterm (_s, wf) -> (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) @@ -964,7 +964,7 @@ let check_one_fix renv recpos trees def = else check_rec_call renv' [] body) bodies - | Const (kn,u as cu) -> + | Const (kn,_u as cu) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> @@ -983,7 +983,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b - | CoFix (i,(_,typarray,bodies as recdef)) -> + | CoFix (_i,(_,typarray,bodies as recdef)) -> List.iter (check_rec_call renv []) l; Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in @@ -992,13 +992,13 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Proj (p, c) -> + | Proj (_p, c) -> List.iter (check_rec_call renv []) l; check_rec_call renv [] c | Var id -> begin - let open Context.Named.Declaration in + let open! Context.Named.Declaration in match lookup_named id renv.env with | LocalAssum _ -> List.iter (check_rec_call renv []) l @@ -1129,10 +1129,10 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct ((_,i as cstr_kn),u) -> + | Construct ((_,i as cstr_kn),_u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in - let (mib,mip) = lookup_mind_specif env mI in + let (mib,_mip) = lookup_mind_specif env mI in let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> @@ -1157,7 +1157,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - | CoFix (j,(_,varit,vdefs as recdef)) -> + | CoFix (_j,(_,varit,vdefs as recdef)) -> if List.for_all (noccur_with_meta n nbfix) args then if Array.for_all (noccur_with_meta n nbfix) varit then @@ -1203,7 +1203,7 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = +let check_cofix env (_bodynum,(names,types,bodies as recdef)) = let flags = Environ.typing_flags env in if flags.check_guarded then let nbfix = Array.length bodies in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f1d08ef6dd..bff3092655 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -319,12 +319,12 @@ let subst_con sub cst = let subst_con_kn sub con = subst_con sub (con,Univ.Instance.empty) -let subst_pcon sub (con,u as pcon) = - try let con', can = subst_con0 sub pcon in +let subst_pcon sub (_con,u as pcon) = + try let con', _can = subst_con0 sub pcon in con',u with No_subst -> pcon -let subst_pcon_term sub (con,u as pcon) = +let subst_pcon_term sub (_con,u as pcon) = try let con', can = subst_con0 sub pcon in (con',u), can with No_subst -> pcon, mkConstU pcon @@ -441,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn = let rec mp_in_mp mp mp1 = match mp1 with | _ when ModPath.equal mp1 mp -> true - | MPdot (mp2,l) -> mp_in_mp mp mp2 + | MPdot (mp2,_l) -> mp_in_mp mp mp2 | _ -> false let subset_prefixed_by mp resolver = diff --git a/kernel/modops.ml b/kernel/modops.ml index 9435f46c6b..424d329e09 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -138,7 +138,7 @@ let rec functor_smart_map fty f0 funct = match funct with let a' = f0 a in if a==a' then funct else NoFunctor a' let rec functor_iter fty f0 = function - |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e + |MoreFunctor (_mbid,ty,e) -> fty ty; functor_iter fty f0 e |NoFunctor a -> f0 a (** {6 Misc operations } *) @@ -171,7 +171,7 @@ let implem_iter fs fa impl = match impl with (** {6 Substitutions of modular structures } *) -let id_delta x y = x +let id_delta x _y = x let subst_with_body sub = function |WithMod(id,mp) as orig -> @@ -200,7 +200,7 @@ let rec subst_structure sub do_delta sign = and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> - let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in let mp' = subst_mp sub mp in let sub = if ModPath.equal mp mp' then sub @@ -371,7 +371,7 @@ and strengthen_sig mp_from struc mp_to reso = match struc with let item' = l,SFBmodule mb' in let reso',rest' = strengthen_sig mp_from rest mp_to reso in add_delta_resolver reso' mb.mod_delta, item':: rest' - |(l,SFBmodtype mty as item) :: rest -> + |(_l,SFBmodtype _mty as item) :: rest -> let reso',rest' = strengthen_sig mp_from rest mp_to reso in reso',item::rest' @@ -628,7 +628,7 @@ let join_structure except otab s = let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type - and join_field (l,body) = match body with + and join_field (_l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () |SFBmodule m -> diff --git a/kernel/names.ml b/kernel/names.ml index 933cefe993..6d33f233e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -207,7 +207,7 @@ struct let repr mbid = mbid - let to_string (i, s, p) = + let to_string (_i, s, p) = DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = @@ -328,7 +328,7 @@ module ModPath = struct let rec dp = function | MPfile sl -> sl | MPbound (_,_,dp) -> dp - | MPdot (mp,l) -> dp mp + | MPdot (mp,_l) -> dp mp module Self_Hashcons = struct type t = module_path @@ -420,7 +420,7 @@ module KerName = struct let hash kn = let h = kn.refhash in if h < 0 then - let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in + let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in (* Ensure positivity on all platforms. *) let h = h land 0x3FFFFFFF in @@ -623,8 +623,8 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let inductive_of_constructor (ind, i) = ind -let index_of_constructor (ind, i) = i +let inductive_of_constructor (ind, _i) = ind +let index_of_constructor (_ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index eed25a4ca4..74b075f4a5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1007,7 +1007,7 @@ let compile_prim decl cond paux = *) let rec opt_prim_aux paux = match paux with - | PAprim(prefix, kn, op, args) -> + | PAprim(_prefix, _kn, op, args) -> let args = Array.map opt_prim_aux args in app_prim (Coq_primitive(op,None)) args (* @@ -1071,7 +1071,7 @@ let ml_of_instance instance u = match t with | Lrel(id ,i) -> get_rel env id i | Lvar id -> get_var env id - | Lmeta(mv,ty) -> + | Lmeta(mv,_ty) -> let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) @@ -1184,7 +1184,7 @@ let ml_of_instance instance u = let lf,env_n = push_rels (empty_env env.env_univ ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in - let mk_let envi (id,def) t = MLlet (id,def,t) in + let mk_let _envi (id,def) t = MLlet (id,def,t) in let mk_lam_or_let (params,lets,env) (id,def) = let ln,env' = push_rel env id in match def with @@ -1217,7 +1217,7 @@ let ml_of_instance instance u = (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in (* Compilation of fix *) let fv_args = fv_args env fvn fvr in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in let mk_norm = MLapp(MLglobal norm, fv_args) in let mkrec i lname = @@ -1272,9 +1272,9 @@ let ml_of_instance instance u = let mk_norm = MLapp(MLglobal norm, fv_args) in let lnorm = fresh_lname Anonymous in let ltype = fresh_lname Anonymous in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in - let upd i lname cont = + let upd i _lname cont = let paramsi = t_params.(i) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in let uniti = fresh_lname Anonymous in @@ -1305,7 +1305,7 @@ let ml_of_instance instance u = (lname, paramsi, body) in MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) - | Lmakeblock (prefix,(cn,u),_,args) -> + | Lmakeblock (prefix,(cn,_u),_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) | Lconstruct (prefix, (cn,u)) -> @@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,dp,l) = KerName.repr kn in + let (mp,_dp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l @@ -1987,7 +1987,7 @@ let compile_mind mb mind stack = (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in - let add_proj proj_arg acc pb = + let add_proj proj_arg acc _pb = let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -2053,9 +2053,9 @@ let compile_mind_deps env prefix ~interactive let compile_deps env sigma prefix ~interactive init t = let rec aux env lvl init t = match kind t with - | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind + | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in + let c,_u = get_alias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref @@ -2074,11 +2074,11 @@ let compile_deps env sigma prefix ~interactive init t = let comp_stack = code@comp_stack in let const_updates = Cmap_env.add c (nameref, name) const_updates in comp_stack, (mind_updates, const_updates) - | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind + | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in aux env lvl init c - | Case (ci, p, c, ac) -> + | Case (ci, _p, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in fold_constr_with_binders succ (aux env) lvl init t diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c75dde843e..054b6a2d17 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -25,9 +25,9 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in conv_val env CONV (lvl+1) (f1 v) (f2 v) cu - | Vfun f1, _ -> + | Vfun _f1, _ -> conv_val env CONV lvl v1 (fun x -> v2 x) cu - | _, Vfun f2 -> + | _, Vfun _f2 -> conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> conv_accu env pb lvl k1 k2 cu @@ -110,7 +110,7 @@ and conv_atom env pb lvl a1 a2 cu = else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu - | Aprod(_,d1,c1), Aprod(_,d2,c2) -> + | Aprod(_,d1,_c1), Aprod(_,d2,_c2) -> let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index ab40c643f9..70cb8691c6 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -142,7 +142,7 @@ let rec map_lam_with_binders g f n lam = let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') -and map_uint g f n u = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(prefix,c,args) -> @@ -203,7 +203,7 @@ let can_subst lam = let can_merge_if bt bf = match bt, bf with - | Llam(idst,_), Llam(idsf,_) -> true + | Llam(_idst,_), Llam(_idsf,_) -> true | _ -> false let merge_if t bt bf = @@ -370,7 +370,7 @@ module Cache = let is_lazy env prefix t = match kind t with - | App (f,args) -> + | App (f,_args) -> begin match kind f with | Construct (c,_) -> let gr = GlobRef.IndRef (fst c) in @@ -431,7 +431,7 @@ let rec lambda_of_constr cache env sigma c = | Sort s -> Lsort s - | Ind (ind,u as pind) -> + | Ind (ind,_u as pind) -> let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) @@ -529,7 +529,7 @@ let rec lambda_of_constr cache env sigma c = and lambda_of_app cache env sigma f args = match kind f with - | Const (kn,u as c) -> + | Const (_kn,_u as c) -> let kn,u = get_alias env c in let cb = lookup_constant kn env in (try diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f784509b6f..b4126dd68c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -40,7 +40,7 @@ let include_dirs () = [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) -let load_obj = ref (fun x -> () : string -> unit) +let load_obj = ref (fun _x -> () : string -> unit) let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) @@ -113,7 +113,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true - | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> warn_native_compiler_failed (Inl res); false in res, link_filename @@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds = (try if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix - with Dynlink.Error e as exn -> + with Dynlink.Error _ as exn -> let exn = CErrors.push exn in if fatal then iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index edce9367fc..8ac3538fc5 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -29,7 +29,7 @@ and translate_field prefix mp env acc (l,x) = | SFBconst cb -> let con = Constant.make3 mp DirPath.empty l in (if !Flags.debug then - let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in + let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); compile_constant_field env prefix con acc cb | SFBmind mb -> diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index f8b71e4564..303cb06c55 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -87,21 +87,21 @@ let discharge_direct_opaque ~cook_constr ci = function | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp } = function +let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> ignore(Future.join cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in ignore(Future.join fp) -let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function +let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some (Future.uuid cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some (Future.uuid (snd (Int.Map.find i prfs))) else None -let force_proof { opaque_val = prfs; opaque_dir = odp } = function +let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> fst(Future.force cu) | Indirect (l,dp,i) -> @@ -112,7 +112,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints { opaque_val = prfs; opaque_dir = odp } = function +let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp @@ -121,14 +121,14 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | None -> Univ.ContextSet.empty | Some u -> Future.force u -let get_constraints { opaque_val = prfs; opaque_dir = odp } = function +let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof { opaque_val = prfs; opaque_dir = odp } = function +let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = @@ -144,7 +144,7 @@ let a_constr = Future.from_val (mkRel 1) let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : cooking_info list = [] -let dump { opaque_val = otab; opaque_len = n } = +let dump { opaque_val = otab; opaque_len = n; _ } = let opaque_table = Array.make n a_constr in let univ_table = Array.make n a_univ in let disch_table = Array.make n a_discharge in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c701b53fe4..2abb4b485c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -53,9 +53,9 @@ let compare_stack_shape stk1 stk2 = | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2 | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 - | (Zproj p1::s1, Zproj p2::s2) -> + | (Zproj _p1::s1, Zproj _p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> + | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -261,7 +261,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u s | Declarations.Polymorphic_ind _ -> cmp_instances u1 u2 s - | Declarations.Cumulative_ind cumi -> + | Declarations.Cumulative_ind _cumi -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s @@ -296,7 +296,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = (match (z1,z2) with | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,l1),Zlproj (c2,l2)) -> + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> if not (Projection.Repr.equal c1 c2) then raise NotConvertible else cu1 @@ -498,7 +498,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with - | FConstruct ((ind2,j2),u2) -> + | FConstruct ((ind2,_j2),_u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -515,7 +515,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with - | FConstruct ((ind1,j1),u1) -> + | FConstruct ((ind1,_j1),_u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -554,14 +554,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Eta expansion of records *) - | (FConstruct ((ind1,j1),u1), _) -> + | (FConstruct ((ind1,_j1),_u1), _) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) - | (_, FConstruct ((ind2,j2),u2)) -> + | (_, FConstruct ((ind2,_j2),_u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -659,14 +659,14 @@ let check_sort_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible | Set, Prop -> raise NotConvertible | Set, Type u -> check_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> check_pb u Univ.type0_univ | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances ~flex u u' univs = +let check_convert_instances ~flex:_ u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible @@ -707,7 +707,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 @@ -781,7 +781,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -let default_conv cv_pb ?(l2r=false) env t1 t2 = +let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL @@ -912,7 +912,7 @@ let is_arity env c = with NotArity -> false let eta_expand env t ty = - let ctxt, codom = dest_prod env ty in + let ctxt, _codom = dest_prod env ty in let ctxt',t = dest_lam env t in let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in let eta_args = List.rev_map mkRel (List.interval 1 d) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 74042f9e04..bfe68671a2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -138,7 +138,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 + cst (inductive_is_polymorphic mib1) (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in let check_packet cst p1 p2 = @@ -162,10 +162,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst in let mind = MutInd.make1 kn1 in - let check_cons_types i cst p1 p2 = + let check_cons_types _i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - (inductive_is_polymorphic mib1) infer_conv env t1 t2) + (inductive_is_polymorphic mib1) (infer_conv ?l2r:None ?evars:None ?ts:None) env t1 t2) cst p2.mind_consnames (arities_of_specif (mind, inst) (mib1, p1)) @@ -229,7 +229,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = let err = NotConvertibleTypeField (env, t1, t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in match info1 with | Constant cb1 -> @@ -268,14 +268,14 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = Anyway [check_conv] will handle that afterwards. *) let c1 = Mod_subst.force_constr lc1 in let c2 = Mod_subst.force_constr lc2 in - check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2)) - | IndType ((kn,i),mind1) -> + check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2)) + | IndType ((_kn,_i),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ "name.") - | IndConstr (((kn,i),j),mind1) -> + | IndConstr (((_kn,_i),_j),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 4851a9c0d0..795cdeb040 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -54,13 +54,13 @@ let mkProd_wo_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkProd (na, t, c) - | LocalDef (na,b,t) -> subst1 b c + | LocalDef (_na,b,_t) -> subst1 b c let mkNamedProd_wo_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c - | LocalDef (id,b,t) -> subst1 b (subst_var id c) + | LocalDef (id,b,_t) -> subst1 b (subst_var id c) (* non-dependent product t1 -> t2 *) let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) @@ -81,7 +81,7 @@ let mkNamedLambda_or_LetIn decl c = (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = let rec prodrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) | _ -> assert false in @@ -93,7 +93,7 @@ let compose_prod l b = prodn (List.length l) l b (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *) let lamn n env b = let rec lamrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) | _ -> assert false in @@ -276,7 +276,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") + | _ -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -297,7 +297,7 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") + | _c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -313,7 +313,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") + | _ -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f59e07098b..47247ff25e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -73,7 +73,7 @@ type _ trust = let uniq_seff_rev = SideEffects.repr let uniq_seff l = let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff } -> eff) ans + List.map_append (fun { eff ; _ } -> eff) ans let empty_seff = SideEffects.empty let add_seff mb eff effs = @@ -103,12 +103,7 @@ let inline_side_effects env body ctx side_eff = if List.is_empty side_eff then (body, ctx, sigs) else (** Second step: compute the lifts and substitutions to apply *) - let cname c = - let name = Constant.to_string c in - let map c = if c == '.' || c == '#' then '_' else c in - let name = String.map map name in - Name (Id.of_string name) - in + let cname c = Name (Label.to_id (Constant.label c)) in let fold (subst, var, ctx, args) (c, cb, b) = let (b, opaque) = match cb.const_body, b with | Def b, _ -> (Mod_subst.force_constr b, false) @@ -122,7 +117,7 @@ let inline_side_effects env body ctx side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const auctx -> + | Polymorphic_const _auctx -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) @@ -250,9 +245,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_universes = Monomorphic_const_entry univs } as c) -> + const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> @@ -288,8 +283,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let (body, ctx), side_eff = Future.join body in let body, ctx, _ = match trust with | Pure -> body, ctx, [] @@ -348,7 +343,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration kn env result = +let build_constant_declaration _kn env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -478,7 +473,7 @@ let export_eff eff = (eff.seff_constant, eff.seff_body, eff.seff_role) let export_side_effects mb env c = - let { const_entry_body = body } = c in + let { const_entry_body = body; _ } = c in let _, eff = Future.force body in let ce = { c with const_entry_body = Future.chain body @@ -493,7 +488,7 @@ let export_side_effects mb env c = let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in let push_seff env eff = - let { seff_constant = kn; seff_body = cb } = eff in + let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn cb env in match cb.const_universes with | Polymorphic_const _ -> env @@ -511,7 +506,7 @@ let export_side_effects mb env c = if Int.equal sl 0 then let env, cbs = List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in + let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in let eff = { eff with @@ -543,7 +538,7 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons r) -let translate_local_def env id centry = +let translate_local_def env _id centry = let open Cooking in let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 25c1cbff3a..7456ecea56 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -118,14 +118,14 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant env (kn,u as cst) = +let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let type_of_constant_in env (kn,u as cst) = +let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in constant_type_in env cst @@ -142,7 +142,7 @@ let type_of_constant_in env (kn,u as cst) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let type_of_abstraction env name var ty = +let type_of_abstraction _env name var ty = mkProd (name, var, ty) (* Type of an application. *) @@ -204,7 +204,7 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let type_of_product env name s1 s2 = +let type_of_product env _name s1 s2 = let s = sort_of_product env s1 s2 in mkSort s @@ -247,7 +247,7 @@ let check_cast env c ct k expected_type = dynamic constraints of the form u<=v are enforced *) let type_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in + let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args @@ -264,7 +264,7 @@ let type_of_inductive env (ind,u as indu) = (* Constructors. *) -let type_of_constructor env (c,u as cu) = +let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in @@ -285,7 +285,7 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let type_of_case env ci p pt c ct lf lft = +let type_of_case env ci p pt c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in @@ -399,7 +399,7 @@ let rec execute env cstr = let lft = execute_array env lf in type_of_case env ci p pt c ct lf lft - | Fix ((vn,i as vni),recdef) -> + | Fix ((_vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in check_fix env fix; fix_ty @@ -432,12 +432,12 @@ and execute_array env = Array.map (execute env) (* Derived functions *) -let universe_levels_of_constr env c = +let universe_levels_of_constr _env c = let rec aux s c = match kind c with - | Const (c, u) -> + | Const (_c, u) -> LSet.fold LSet.add (Instance.levels u) s - | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in @@ -530,7 +530,7 @@ let judge_of_product env x varj outj = make_judge (mkProd (x, varj.utj_val, outj.utj_val)) (mkSort (sort_of_product env varj.utj_type outj.utj_type)) -let judge_of_letin env name defj typj j = +let judge_of_letin _env name defj typj j = make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) (subst1 defj.uj_val j.uj_type) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 95d71965df..9ff51fca55 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -194,7 +194,7 @@ let check_universes_invariants g = UMap.iter (fun l u -> match u with | Canonical u -> - UMap.iter (fun v strict -> + UMap.iter (fun v _strict -> incr n_edges; let v = repr g v in assert (topo_compare u v = -1); @@ -435,7 +435,7 @@ let reorder g u v = | n0::q0 -> (* Computing new root. *) let root, rank_rest = - List.fold_left (fun ((best, rank_rest) as acc) n -> + List.fold_left (fun ((best, _rank_rest) as acc) n -> if n.rank >= best.rank then n, best.rank else acc) (n0, min_int) q0 in @@ -809,7 +809,7 @@ let normalize_universes g = in UMap.fold (fun _ u g -> match u with - | Equiv u -> g + | Equiv _u -> g | Canonical u -> let _, u, g = get_ltle g u in let _, _, g = get_gtge g u in @@ -821,7 +821,7 @@ let constraints_of_universes g = let uf = UF.create () in let constraints_of u v acc = match v with - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc @@ -943,7 +943,7 @@ let check_eq_instances g t1 t2 = (** Pretty-printing *) let pr_arc prl = function - | _, Canonical {univ=u; ltle} -> + | _, Canonical {univ=u; ltle; _} -> if UMap.is_empty ltle then mt () else prl u ++ str " " ++ @@ -963,7 +963,7 @@ let pr_universes prl g = let dump_universes output g = let dump_arc u = function - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in diff --git a/kernel/univ.ml b/kernel/univ.ml index 311477daca..747a901f45 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -86,7 +86,7 @@ struct | Level (n,d) as x -> let d' = Names.DirPath.hcons d in if d' == d then x else Level (n,d') - | Var n as x -> x + | Var _n as x -> x open Hashset.Combine @@ -206,13 +206,13 @@ module LMap = struct include M let union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some _, _ -> l | _, _ -> r) l r let subst_union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some (Some _), _ -> l | Some None, None -> l @@ -365,14 +365,14 @@ struct else f v ++ str"+" ++ int n let is_level = function - | (v, 0) -> true + | (_v, 0) -> true | _ -> false let level = function | (v,0) -> Some v | _ -> None - let get_level (v,n) = v + let get_level (v,_n) = v let map f (v, n as x) = let v' = f v in @@ -582,7 +582,7 @@ struct prl u2 ++ fnl () ) c (str "") let universes_of c = - fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty + fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end let universes_of_constraints = Constraint.universes_of @@ -907,7 +907,7 @@ let subst_instance_constraints s csts = type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t -let out_punivs (x, y) = x +let out_punivs (x, _y) = x let in_punivs x = (x, Instance.empty) let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' @@ -932,8 +932,8 @@ struct let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) - let instance (univs, cst) = univs - let constraints (univs, cst) = cst + let instance (univs, _cst) = univs + let constraints (_univs, cst) = cst let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' @@ -952,7 +952,7 @@ struct include UContext let repr (inst, cst) = - (Array.mapi (fun i l -> Level.var i) inst, cst) + (Array.mapi (fun i _l -> Level.var i) inst, cst) let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); @@ -988,8 +988,8 @@ struct let hcons (univs, variance) = (* should variance be hconsed? *) (UContext.hcons univs, variance) - let univ_context (univs, subtypcst) = univs - let variance (univs, variance) = variance + let univ_context (univs, _subtypcst) = univs + let variance (_univs, variance) = variance (** This function takes a universe context representing constraints of an inductive and produces a CumulativityInfo.t with the @@ -1066,8 +1066,8 @@ struct if is_empty ctx then mt() else h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) - let constraints (univs, cst) = cst - let levels (univs, cst) = univs + let constraints (_univs, cst) = cst + let levels (univs, _cst) = univs let size (univs,_) = LSet.cardinal univs end @@ -1155,7 +1155,7 @@ let make_inverse_instance_subst i = LMap.empty arr let make_abstract_instance (ctx, _) = - Array.mapi (fun i l -> Level.var i) ctx + Array.mapi (fun i _l -> Level.var i) ctx let abstract_universes ctx = let instance = UContext.instance ctx in diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f588a6302..9d5d79124b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -66,7 +66,7 @@ let isMeta c = match Constr.kind c with let noccur_with_meta n m term = let rec occur_rec n c = match Constr.kind c with | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur - | Constr.App(f,cl) -> + | Constr.App(f,_cl) -> (match Constr.kind f with | Constr.Cast (c,_,_) when isMeta c -> () | Constr.Meta _ -> () @@ -188,7 +188,7 @@ let adjust_rel_to_rel_context sign n = let open RelDecl in match sign with | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) - | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | LocalDef (_,_c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) | [] -> (0,n) in snd (aux sign) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index d19bea5199..5965853e1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -11,7 +11,7 @@ open Csymtable let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2) - | Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2) + | Zfix(_f1,args1), Zfix(_f2,args2) -> Int.equal (nargs args1) (nargs args2) | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false @@ -84,7 +84,7 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ((mi,i) as ind1) , Aind ind2 -> + | Aind ((mi,_i) as ind1) , Aind ind2 -> if eq_ind ind1 ind2 && compare_stack stk1 stk2 then if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in diff --git a/kernel/vm.ml b/kernel/vm.ml index 9917e94a35..eaf64ba4af 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -187,5 +187,5 @@ let apply_whd k whd = interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v - | Vuniv_level lvl -> assert false + | Vuniv_level _lvl -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 8edd49f77f..217ef4b8e5 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -100,7 +100,7 @@ let eq_structured_constant c1 c2 = match c1, c2 with | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false | Const_val v1, Const_val v2 -> eq_structured_values v1 v2 -| Const_val v1, _ -> false +| Const_val _v1, _ -> false let hash_structured_constant c = let open Hashset.Combine in @@ -245,7 +245,7 @@ type id_key = | RelKey of Int.t | EvarKey of Evar.t -let eq_id_key k1 k2 = match k1, k2 with +let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 @@ -304,9 +304,9 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" + | Vconstr_const _i -> str "Vconstr_const" + | Vconstr_block _b -> str "Vconstr_block" + | Vatom_stk (_a,_stk) -> str "Vatom_stk" | _ -> assert false in CErrors.anomaly @@ -444,7 +444,7 @@ struct type t = id_key let equal = eq_id_key open Hashset.Combine - let hash = function + let hash : t -> tag = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) @@ -658,7 +658,7 @@ and pr_whd w = | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" + | Vconstr_block _b -> str "Vconstr_block" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = @@ -668,6 +668,6 @@ and pr_stack stk = and pr_zipper z = Pp.(match z with | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" + | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch _s -> str "Zswitch(...)" | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 3bd7cd622c..d82e8ae8ad 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. +Require Import Bool DecidableClass Algebra Ring PArith Omega. Section Bool. diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 803d35d07c..b219ee25ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -272,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence pr prods with Not_found -> + (* FIXME: This key, moreover printed with a low-level printer, + has no meaning user-side *) KerName.print key let pr_alias_gen pr_gen lev key l = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 67ffae59cc..9f34df4608 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1298,7 +1298,7 @@ and tactic_of_value ist vle = match appl with UnnamedAppl -> "An unnamed user-defined tactic" | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in match nms with [] -> assert false | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) diff --git a/plugins/romega/README b/plugins/romega/README deleted file mode 100644 index 86c9e58afd..0000000000 --- a/plugins/romega/README +++ /dev/null @@ -1,6 +0,0 @@ -This work was done for the RNRT Project Calife. -As such it is distributed under the LGPL licence. - -Report bugs to : - pierre.cregut@francetelecom.com - diff --git a/plugins/romega/ROmega.v b/plugins/romega/ROmega.v deleted file mode 100644 index 657aae90e8..0000000000 --- a/plugins/romega/ROmega.v +++ /dev/null @@ -1,14 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -Require Import ReflOmegaCore. -Require Export Setoid. -Require Export PreOmega. -Require Export ZArith_base. -Require Import OmegaPlugin. -Declare ML Module "romega_plugin". diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v deleted file mode 100644 index da86f4274d..0000000000 --- a/plugins/romega/ReflOmegaCore.v +++ /dev/null @@ -1,1874 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence du projet : LGPL version 2.1 - - *************************************************************************) - -Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. -Declare Scope Int_scope. -Delimit Scope Int_scope with I. - -(** * Abstract Integers. *) - -Module Type Int. - - Parameter t : Set. - - Bind Scope Int_scope with t. - - Parameter Inline zero : t. - Parameter Inline one : t. - Parameter Inline plus : t -> t -> t. - Parameter Inline opp : t -> t. - Parameter Inline minus : t -> t -> t. - Parameter Inline mult : t -> t -> t. - - Notation "0" := zero : Int_scope. - Notation "1" := one : Int_scope. - Infix "+" := plus : Int_scope. - Infix "-" := minus : Int_scope. - Infix "*" := mult : Int_scope. - Notation "- x" := (opp x) : Int_scope. - - Open Scope Int_scope. - - (** First, Int is a ring: *) - Axiom ring : @ring_theory t 0 1 plus mult minus opp (@eq t). - - (** Int should also be ordered: *) - - Parameter Inline le : t -> t -> Prop. - Parameter Inline lt : t -> t -> Prop. - Parameter Inline ge : t -> t -> Prop. - Parameter Inline gt : t -> t -> Prop. - Notation "x <= y" := (le x y): Int_scope. - Notation "x < y" := (lt x y) : Int_scope. - Notation "x >= y" := (ge x y) : Int_scope. - Notation "x > y" := (gt x y): Int_scope. - Axiom le_lt_iff : forall i j, (i<=j) <-> ~(j<i). - Axiom ge_le_iff : forall i j, (i>=j) <-> (j<=i). - Axiom gt_lt_iff : forall i j, (i>j) <-> (j<i). - - (** Basic properties of this order *) - Axiom lt_trans : forall i j k, i<j -> j<k -> i<k. - Axiom lt_not_eq : forall i j, i<j -> i<>j. - - (** Compatibilities *) - Axiom lt_0_1 : 0<1. - Axiom plus_le_compat : forall i j k l, i<=j -> k<=l -> i+k<=j+l. - Axiom opp_le_compat : forall i j, i<=j -> (-j)<=(-i). - Axiom mult_lt_compat_l : - forall i j k, 0 < k -> i < j -> k*i<k*j. - - (** We should have a way to decide the equality and the order*) - Parameter compare : t -> t -> comparison. - Infix "?=" := compare (at level 70, no associativity) : Int_scope. - Axiom compare_Eq : forall i j, compare i j = Eq <-> i=j. - Axiom compare_Lt : forall i j, compare i j = Lt <-> i<j. - Axiom compare_Gt : forall i j, compare i j = Gt <-> i>j. - - (** Up to here, these requirements could be fulfilled - by any totally ordered ring. Let's now be int-specific: *) - Axiom le_lt_int : forall x y, x<y <-> x<=y+-(1). - - (** Btw, lt_0_1 could be deduced from this last axiom *) - - (** Now we also require a division function. - It is deliberately underspecified, since that's enough - for the proofs below. But the most appropriate variant - (and the one needed to stay in sync with the omega engine) - is "Floor" (the historical version of Coq's [Z.div]). *) - - Parameter diveucl : t -> t -> t * t. - Notation "i / j" := (fst (diveucl i j)). - Notation "i 'mod' j" := (snd (diveucl i j)). - Axiom diveucl_spec : - forall i j, j<>0 -> i = j * (i/j) + (i mod j). - -End Int. - - - -(** Of course, Z is a model for our abstract int *) - -Module Z_as_Int <: Int. - - Open Scope Z_scope. - - Definition t := Z. - Definition zero := 0. - Definition one := 1. - Definition plus := Z.add. - Definition opp := Z.opp. - Definition minus := Z.sub. - Definition mult := Z.mul. - - Lemma ring : @ring_theory t zero one plus mult minus opp (@eq t). - Proof. - constructor. - exact Z.add_0_l. - exact Z.add_comm. - exact Z.add_assoc. - exact Z.mul_1_l. - exact Z.mul_comm. - exact Z.mul_assoc. - exact Z.mul_add_distr_r. - unfold minus, Z.sub; auto. - exact Z.add_opp_diag_r. - Qed. - - Definition le := Z.le. - Definition lt := Z.lt. - Definition ge := Z.ge. - Definition gt := Z.gt. - Definition le_lt_iff := Z.le_ngt. - Definition ge_le_iff := Z.ge_le_iff. - Definition gt_lt_iff := Z.gt_lt_iff. - - Definition lt_trans := Z.lt_trans. - Definition lt_not_eq := Z.lt_neq. - - Definition lt_0_1 := Z.lt_0_1. - Definition plus_le_compat := Z.add_le_mono. - Definition mult_lt_compat_l := Zmult_lt_compat_l. - Lemma opp_le_compat i j : i<=j -> (-j)<=(-i). - Proof. apply -> Z.opp_le_mono. Qed. - - Definition compare := Z.compare. - Definition compare_Eq := Z.compare_eq_iff. - Lemma compare_Lt i j : compare i j = Lt <-> i<j. - Proof. reflexivity. Qed. - Lemma compare_Gt i j : compare i j = Gt <-> i>j. - Proof. reflexivity. Qed. - - Definition le_lt_int := Z.lt_le_pred. - - Definition diveucl := Z.div_eucl. - Definition diveucl_spec := Z.div_mod. - -End Z_as_Int. - - -(** * Properties of abstract integers *) - -Module IntProperties (I:Int). - Import I. - Local Notation int := I.t. - - (** Primo, some consequences of being a ring theory... *) - - Definition two := 1+1. - Notation "2" := two : Int_scope. - - (** Aliases for properties packed in the ring record. *) - - Definition plus_assoc := ring.(Radd_assoc). - Definition plus_comm := ring.(Radd_comm). - Definition plus_0_l := ring.(Radd_0_l). - Definition mult_assoc := ring.(Rmul_assoc). - Definition mult_comm := ring.(Rmul_comm). - Definition mult_1_l := ring.(Rmul_1_l). - Definition mult_plus_distr_r := ring.(Rdistr_l). - Definition opp_def := ring.(Ropp_def). - Definition minus_def := ring.(Rsub_def). - - Opaque plus_assoc plus_comm plus_0_l mult_assoc mult_comm mult_1_l - mult_plus_distr_r opp_def minus_def. - - (** More facts about [plus] *) - - Lemma plus_0_r : forall x, x+0 = x. - Proof. intros; rewrite plus_comm; apply plus_0_l. Qed. - - Lemma plus_permute : forall x y z, x+(y+z) = y+(x+z). - Proof. intros; do 2 rewrite plus_assoc; f_equal; apply plus_comm. Qed. - - Lemma plus_reg_l : forall x y z, x+y = x+z -> y = z. - Proof. - intros. - rewrite <- (plus_0_r y), <- (plus_0_r z), <-(opp_def x). - now rewrite plus_permute, plus_assoc, H, <- plus_assoc, plus_permute. - Qed. - - (** More facts about [mult] *) - - Lemma mult_plus_distr_l : forall x y z, x*(y+z)=x*y+x*z. - Proof. - intros. - rewrite (mult_comm x (y+z)), (mult_comm x y), (mult_comm x z). - apply mult_plus_distr_r. - Qed. - - Lemma mult_0_l x : 0*x = 0. - Proof. - assert (H := mult_plus_distr_r 0 1 x). - rewrite plus_0_l, mult_1_l, plus_comm in H. - apply plus_reg_l with x. - now rewrite <- H, plus_0_r. - Qed. - - Lemma mult_0_r x : x*0 = 0. - Proof. - rewrite mult_comm. apply mult_0_l. - Qed. - - Lemma mult_1_r x : x*1 = x. - Proof. - rewrite mult_comm. apply mult_1_l. - Qed. - - (** More facts about [opp] *) - - Definition plus_opp_r := opp_def. - - Lemma plus_opp_l : forall x, -x + x = 0. - Proof. intros; now rewrite plus_comm, opp_def. Qed. - - Lemma mult_opp_comm : forall x y, - x * y = x * - y. - Proof. - intros. - apply plus_reg_l with (x*y). - rewrite <- mult_plus_distr_l, <- mult_plus_distr_r. - now rewrite opp_def, opp_def, mult_0_l, mult_comm, mult_0_l. - Qed. - - Lemma opp_eq_mult_neg_1 : forall x, -x = x * -(1). - Proof. - intros; now rewrite mult_comm, mult_opp_comm, mult_1_l. - Qed. - - Lemma opp_involutive : forall x, -(-x) = x. - Proof. - intros. - apply plus_reg_l with (-x). - now rewrite opp_def, plus_comm, opp_def. - Qed. - - Lemma opp_plus_distr : forall x y, -(x+y) = -x + -y. - Proof. - intros. - apply plus_reg_l with (x+y). - rewrite opp_def. - rewrite plus_permute. - do 2 rewrite plus_assoc. - now rewrite (plus_comm (-x)), opp_def, plus_0_l, opp_def. - Qed. - - Lemma opp_mult_distr_r : forall x y, -(x*y) = x * -y. - Proof. - intros. - rewrite <- mult_opp_comm. - apply plus_reg_l with (x*y). - now rewrite opp_def, <-mult_plus_distr_r, opp_def, mult_0_l. - Qed. - - Lemma egal_left n m : 0 = n+-m <-> n = m. - Proof. - split; intros. - - apply plus_reg_l with (-m). - rewrite plus_comm, <- H. symmetry. apply plus_opp_l. - - symmetry. subst; apply opp_def. - Qed. - - (** Specialized distributivities *) - - Hint Rewrite mult_plus_distr_l mult_plus_distr_r mult_assoc : int. - Hint Rewrite <- plus_assoc : int. - - Hint Rewrite plus_0_l plus_0_r mult_0_l mult_0_r mult_1_l mult_1_r : int. - - Lemma OMEGA10 v c1 c2 l1 l2 k1 k2 : - v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2) = - (v * c1 + l1) * k1 + (v * c2 + l2) * k2. - Proof. - autorewrite with int; f_equal; now rewrite plus_permute. - Qed. - - Lemma OMEGA11 v1 c1 l1 l2 k1 : - v1 * (c1 * k1) + (l1 * k1 + l2) = (v1 * c1 + l1) * k1 + l2. - Proof. - now autorewrite with int. - Qed. - - Lemma OMEGA12 v2 c2 l1 l2 k2 : - v2 * (c2 * k2) + (l1 + l2 * k2) = l1 + (v2 * c2 + l2) * k2. - Proof. - autorewrite with int; now rewrite plus_permute. - Qed. - - Lemma sum1 a b c d : 0 = a -> 0 = b -> 0 = a * c + b * d. - Proof. - intros; subst. now autorewrite with int. - Qed. - - - (** Secondo, some results about order (and equality) *) - - Lemma lt_irrefl : forall n, ~ n<n. - Proof. - intros n H. - elim (lt_not_eq _ _ H); auto. - Qed. - - Lemma lt_antisym : forall n m, n<m -> m<n -> False. - Proof. - intros; elim (lt_irrefl _ (lt_trans _ _ _ H H0)); auto. - Qed. - - Lemma lt_le_weak : forall n m, n<m -> n<=m. - Proof. - intros; rewrite le_lt_iff; intro H'; eapply lt_antisym; eauto. - Qed. - - Lemma le_refl : forall n, n<=n. - Proof. - intros; rewrite le_lt_iff; apply lt_irrefl; auto. - Qed. - - Lemma le_antisym : forall n m, n<=m -> m<=n -> n=m. - Proof. - intros n m; do 2 rewrite le_lt_iff; intros. - rewrite <- compare_Lt in H0. - rewrite <- gt_lt_iff, <- compare_Gt in H. - rewrite <- compare_Eq. - destruct compare; intuition. - Qed. - - Lemma lt_eq_lt_dec : forall n m, { n<m }+{ n=m }+{ m<n }. - Proof. - intros. - generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). - destruct compare; [ left; right | left; left | right ]; intuition. - rewrite gt_lt_iff in H1; intuition. - Qed. - - Lemma lt_dec : forall n m: int, { n<m } + { ~n<m }. - Proof. - intros. - generalize (compare_Lt n m)(compare_Eq n m)(compare_Gt n m). - destruct compare; [ right | left | right ]; intuition discriminate. - Qed. - - Lemma lt_le_iff : forall n m, (n<m) <-> ~(m<=n). - Proof. - intros. - rewrite le_lt_iff. - destruct (lt_dec n m); intuition. - Qed. - - Lemma le_dec : forall n m: int, { n<=m } + { ~n<=m }. - Proof. - intros; destruct (lt_dec m n); [right|left]; rewrite le_lt_iff; intuition. - Qed. - - Lemma le_lt_dec : forall n m, { n<=m } + { m<n }. - Proof. - intros; destruct (le_dec n m); [left|right]; auto; now rewrite lt_le_iff. - Qed. - - - Definition beq i j := match compare i j with Eq => true | _ => false end. - - Infix "=?" := beq : Int_scope. - - Lemma beq_iff i j : (i =? j) = true <-> i=j. - Proof. - unfold beq. rewrite <- (compare_Eq i j). now destruct compare. - Qed. - - Lemma beq_reflect i j : reflect (i=j) (i =? j). - Proof. - apply iff_reflect. symmetry. apply beq_iff. - Qed. - - Lemma eq_dec : forall n m:int, { n=m } + { n<>m }. - Proof. - intros n m; generalize (beq_iff n m); destruct beq; [left|right]; intuition. - Qed. - - Definition blt i j := match compare i j with Lt => true | _ => false end. - - Infix "<?" := blt : Int_scope. - - Lemma blt_iff i j : (i <? j) = true <-> i<j. - Proof. - unfold blt. rewrite <- (compare_Lt i j). now destruct compare. - Qed. - - Lemma blt_reflect i j : reflect (i<j) (i <? j). - Proof. - apply iff_reflect. symmetry. apply blt_iff. - Qed. - - Lemma le_is_lt_or_eq : forall n m, n<=m -> { n<m } + { n=m }. - Proof. - intros n m Hnm. - destruct (eq_dec n m) as [H'|H']. - - right; intuition. - - left; rewrite lt_le_iff. - contradict H'. - now apply le_antisym. - Qed. - - Lemma le_neq_lt : forall n m, n<=m -> n<>m -> n<m. - Proof. - intros n m H. now destruct (le_is_lt_or_eq _ _ H). - Qed. - - Lemma le_trans : forall n m p, n<=m -> m<=p -> n<=p. - Proof. - intros n m p; rewrite 3 le_lt_iff; intros A B C. - destruct (lt_eq_lt_dec p m) as [[H|H]|H]; subst; auto. - generalize (lt_trans _ _ _ H C); intuition. - Qed. - - Lemma not_eq (a b:int) : ~ a <> b <-> a = b. - Proof. - destruct (eq_dec a b); intuition. - Qed. - - (** Order and operations *) - - Lemma le_0_neg n : n <= 0 <-> 0 <= -n. - Proof. - rewrite <- (mult_0_l (-(1))) at 2. - rewrite <- opp_eq_mult_neg_1. - split; intros. - - now apply opp_le_compat. - - rewrite <-(opp_involutive 0), <-(opp_involutive n). - now apply opp_le_compat. - Qed. - - Lemma plus_le_reg_r : forall n m p, n + p <= m + p -> n <= m. - Proof. - intros. - replace n with ((n+p)+-p). - replace m with ((m+p)+-p). - apply plus_le_compat; auto. - apply le_refl. - now rewrite <- plus_assoc, opp_def, plus_0_r. - now rewrite <- plus_assoc, opp_def, plus_0_r. - Qed. - - Lemma plus_le_lt_compat : forall n m p q, n<=m -> p<q -> n+p<m+q. - Proof. - intros. - apply le_neq_lt. - apply plus_le_compat; auto. - apply lt_le_weak; auto. - rewrite lt_le_iff in H0. - contradict H0. - apply plus_le_reg_r with m. - rewrite (plus_comm q m), <-H0, (plus_comm p m). - apply plus_le_compat; auto. - apply le_refl; auto. - Qed. - - Lemma plus_lt_compat : forall n m p q, n<m -> p<q -> n+p<m+q. - Proof. - intros. - apply plus_le_lt_compat; auto. - apply lt_le_weak; auto. - Qed. - - Lemma opp_lt_compat : forall n m, n<m -> -m < -n. - Proof. - intros n m; do 2 rewrite lt_le_iff; intros H; contradict H. - rewrite <-(opp_involutive m), <-(opp_involutive n). - apply opp_le_compat; auto. - Qed. - - Lemma lt_0_neg n : n < 0 <-> 0 < -n. - Proof. - rewrite <- (mult_0_l (-(1))) at 2. - rewrite <- opp_eq_mult_neg_1. - split; intros. - - now apply opp_lt_compat. - - rewrite <-(opp_involutive 0), <-(opp_involutive n). - now apply opp_lt_compat. - Qed. - - Lemma mult_lt_0_compat : forall n m, 0 < n -> 0 < m -> 0 < n*m. - Proof. - intros. - rewrite <- (mult_0_l n), mult_comm. - apply mult_lt_compat_l; auto. - Qed. - - Lemma mult_integral_r n m : 0 < n -> n * m = 0 -> m = 0. - Proof. - intros Hn H. - destruct (lt_eq_lt_dec 0 m) as [[Hm| <- ]|Hm]; auto; exfalso. - - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite H. - exact (lt_irrefl 0). - - rewrite lt_0_neg in Hm. - generalize (mult_lt_0_compat _ _ Hn Hm). - rewrite <- opp_mult_distr_r, opp_eq_mult_neg_1, H, mult_0_l. - exact (lt_irrefl 0). - Qed. - - Lemma mult_integral n m : n * m = 0 -> n = 0 \/ m = 0. - Proof. - intros H. - destruct (lt_eq_lt_dec 0 n) as [[Hn|Hn]|Hn]. - - right; apply (mult_integral_r n m); trivial. - - now left. - - right; apply (mult_integral_r (-n) m). - + now apply lt_0_neg. - + rewrite mult_comm, <- opp_mult_distr_r, mult_comm, H. - now rewrite opp_eq_mult_neg_1, mult_0_l. - Qed. - - Lemma mult_le_compat_l i j k : - 0<=k -> i<=j -> k*i <= k*j. - Proof. - intros Hk Hij. - apply le_is_lt_or_eq in Hk. apply le_is_lt_or_eq in Hij. - destruct Hk as [Hk | <-], Hij as [Hij | <-]; - rewrite ? mult_0_l; try apply le_refl. - now apply lt_le_weak, mult_lt_compat_l. - Qed. - - Lemma mult_le_compat i j k l : - i<=j -> k<=l -> 0<=i -> 0<=k -> i*k<=j*l. - Proof. - intros Hij Hkl Hi Hk. - apply le_trans with (i*l). - - now apply mult_le_compat_l. - - rewrite (mult_comm i), (mult_comm j). - apply mult_le_compat_l; trivial. - now apply le_trans with k. - Qed. - - Lemma sum5 a b c d : 0 <> c -> 0 <> a -> 0 = b -> 0 <> a * c + b * d. - Proof. - intros Hc Ha <-. autorewrite with int. contradict Hc. - symmetry in Hc. destruct (mult_integral _ _ Hc); congruence. - Qed. - - Lemma le_left n m : n <= m <-> 0 <= m + - n. - Proof. - split; intros. - - rewrite <- (opp_def m). - apply plus_le_compat. - apply le_refl. - apply opp_le_compat; auto. - - apply plus_le_reg_r with (-n). - now rewrite plus_opp_r. - Qed. - - Lemma OMEGA8 x y : 0 <= x -> 0 <= y -> x = - y -> x = 0. - Proof. - intros. - assert (y=-x). - subst x; symmetry; apply opp_involutive. - clear H1; subst y. - destruct (eq_dec 0 x) as [H'|H']; auto. - assert (H'':=le_neq_lt _ _ H H'). - generalize (plus_le_lt_compat _ _ _ _ H0 H''). - rewrite plus_opp_l, plus_0_l. - intros. - elim (lt_not_eq _ _ H1); auto. - Qed. - - Lemma sum2 a b c d : - 0 <= d -> 0 = a -> 0 <= b -> 0 <= a * c + b * d. - Proof. - intros Hd <- Hb. autorewrite with int. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - Qed. - - Lemma sum3 a b c d : - 0 <= c -> 0 <= d -> 0 <= a -> 0 <= b -> 0 <= a * c + b * d. - Proof. - intros. - rewrite <- (plus_0_l 0). - apply plus_le_compat; auto. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - rewrite <- (mult_0_l 0). - apply mult_le_compat; auto; apply le_refl. - Qed. - - (** Lemmas specific to integers (they use [le_lt_int]) *) - - Lemma lt_left n m : n < m <-> 0 <= m + -n + -(1). - Proof. - rewrite <- plus_assoc, (plus_comm (-n)), plus_assoc. - rewrite <- le_left. - apply le_lt_int. - Qed. - - Lemma OMEGA4 x y z : 0 < x -> x < y -> z * y + x <> 0. - Proof. - intros H H0 H'. - assert (0 < y) by now apply lt_trans with x. - destruct (lt_eq_lt_dec z 0) as [[G|G]|G]. - - - generalize (plus_le_lt_compat _ _ _ _ (le_refl (z*y)) H0). - rewrite H'. - rewrite <-(mult_1_l y) at 2. rewrite <-mult_plus_distr_r. - apply le_lt_iff. - rewrite mult_comm. rewrite <- (mult_0_r y). - apply mult_le_compat_l; auto using lt_le_weak. - apply le_0_neg. rewrite opp_plus_distr. - apply le_lt_int. now apply lt_0_neg. - - - apply (lt_not_eq 0 (z*y+x)); auto. - subst. now autorewrite with int. - - - apply (lt_not_eq 0 (z*y+x)); auto. - rewrite <- (plus_0_l 0). - auto using plus_lt_compat, mult_lt_0_compat. - Qed. - - Lemma OMEGA19 x : x<>0 -> 0 <= x + -(1) \/ 0 <= x * -(1) + -(1). - Proof. - intros. - do 2 rewrite <- le_lt_int. - rewrite <- opp_eq_mult_neg_1. - destruct (lt_eq_lt_dec 0 x) as [[H'|H']|H']. - auto. - congruence. - right. - rewrite <-(mult_0_l (-(1))), <-(opp_eq_mult_neg_1 0). - apply opp_lt_compat; auto. - Qed. - - Lemma mult_le_approx n m p : - 0 < n -> p < n -> 0 <= m * n + p -> 0 <= m. - Proof. - do 2 rewrite le_lt_iff; intros Hn Hpn H Hm. destruct H. - apply lt_0_neg, le_lt_int, le_left in Hm. - rewrite lt_0_neg. - rewrite opp_plus_distr, mult_comm, opp_mult_distr_r. - rewrite le_lt_int. apply lt_left. - rewrite le_lt_int. - apply le_trans with (n+-(1)); [ now apply le_lt_int | ]. - apply plus_le_compat; [ | apply le_refl ]. - rewrite <- (mult_1_r n) at 1. - apply mult_le_compat_l; auto using lt_le_weak. - Qed. - - (** Some decidabilities *) - - Lemma dec_eq : forall i j:int, decidable (i=j). - Proof. - red; intros; destruct (eq_dec i j); auto. - Qed. - - Lemma dec_ne : forall i j:int, decidable (i<>j). - Proof. - red; intros; destruct (eq_dec i j); auto. - Qed. - - Lemma dec_le : forall i j:int, decidable (i<=j). - Proof. - red; intros; destruct (le_dec i j); auto. - Qed. - - Lemma dec_lt : forall i j:int, decidable (i<j). - Proof. - red; intros; destruct (lt_dec i j); auto. - Qed. - - Lemma dec_ge : forall i j:int, decidable (i>=j). - Proof. - red; intros; rewrite ge_le_iff; destruct (le_dec j i); auto. - Qed. - - Lemma dec_gt : forall i j:int, decidable (i>j). - Proof. - red; intros; rewrite gt_lt_iff; destruct (lt_dec j i); auto. - Qed. - -End IntProperties. - - -(** * The Coq side of the romega tactic *) - -Module IntOmega (I:Int). -Import I. -Module IP:=IntProperties(I). -Import IP. -Local Notation int := I.t. - -(* ** Definition of reified integer expressions - - Terms are either: - - integers [Tint] - - variables [Tvar] - - operation over integers (addition, product, opposite, subtraction) - - Opposite and subtraction are translated in additions and products. - Note that we'll only deal with products for which at least one side - is [Tint]. *) - -Inductive term : Set := - | Tint : int -> term - | Tplus : term -> term -> term - | Tmult : term -> term -> term - | Tminus : term -> term -> term - | Topp : term -> term - | Tvar : N -> term. - -Declare Scope romega_scope. -Bind Scope romega_scope with term. -Delimit Scope romega_scope with term. -Arguments Tint _%I. -Arguments Tplus (_ _)%term. -Arguments Tmult (_ _)%term. -Arguments Tminus (_ _)%term. -Arguments Topp _%term. - -Infix "+" := Tplus : romega_scope. -Infix "*" := Tmult : romega_scope. -Infix "-" := Tminus : romega_scope. -Notation "- x" := (Topp x) : romega_scope. -Notation "[ x ]" := (Tvar x) (at level 0) : romega_scope. - -(* ** Definition of reified goals - - Very restricted definition of handled predicates that should be extended - to cover a wider set of operations. - Taking care of negations and disequations require solving more than a - goal in parallel. This is a major improvement over previous versions. *) - -Inductive proposition : Set := - (** First, basic equations, disequations, inequations *) - | EqTerm : term -> term -> proposition - | NeqTerm : term -> term -> proposition - | LeqTerm : term -> term -> proposition - | GeqTerm : term -> term -> proposition - | GtTerm : term -> term -> proposition - | LtTerm : term -> term -> proposition - (** Then, the supported logical connectors *) - | TrueTerm : proposition - | FalseTerm : proposition - | Tnot : proposition -> proposition - | Tor : proposition -> proposition -> proposition - | Tand : proposition -> proposition -> proposition - | Timp : proposition -> proposition -> proposition - (** Everything else is left as a propositional atom (and ignored). *) - | Tprop : nat -> proposition. - -(** Definition of goals as a list of hypothesis *) -Notation hyps := (list proposition). - -(** Definition of lists of subgoals (set of open goals) *) -Notation lhyps := (list hyps). - -(** A single goal packed in a subgoal list *) -Notation singleton := (fun a : hyps => a :: nil). - -(** An absurd goal *) -Definition absurd := FalseTerm :: nil. - -(** ** Decidable equality on terms *) - -Fixpoint eq_term (t1 t2 : term) {struct t2} : bool := - match t1, t2 with - | Tint i1, Tint i2 => i1 =? i2 - | (t11 + t12), (t21 + t22) => eq_term t11 t21 && eq_term t12 t22 - | (t11 * t12), (t21 * t22) => eq_term t11 t21 && eq_term t12 t22 - | (t11 - t12), (t21 - t22) => eq_term t11 t21 && eq_term t12 t22 - | (- t1), (- t2) => eq_term t1 t2 - | [v1], [v2] => N.eqb v1 v2 - | _, _ => false - end%term. - -Infix "=?" := eq_term : romega_scope. - -Theorem eq_term_iff (t t' : term) : - (t =? t')%term = true <-> t = t'. -Proof. - revert t'. induction t; destruct t'; simpl in *; - rewrite ?andb_true_iff, ?beq_iff, ?N.eqb_eq, ?IHt, ?IHt1, ?IHt2; - intuition congruence. -Qed. - -Theorem eq_term_reflect (t t' : term) : reflect (t=t') (t =? t')%term. -Proof. - apply iff_reflect. symmetry. apply eq_term_iff. -Qed. - -(** ** Interpretations of terms (as integers). *) - -Fixpoint Nnth {A} (n:N)(l:list A)(default:A) := - match n, l with - | _, nil => default - | 0%N, x::_ => x - | _, _::l => Nnth (N.pred n) l default - end. - -Fixpoint interp_term (env : list int) (t : term) : int := - match t with - | Tint x => x - | (t1 + t2)%term => interp_term env t1 + interp_term env t2 - | (t1 * t2)%term => interp_term env t1 * interp_term env t2 - | (t1 - t2)%term => interp_term env t1 - interp_term env t2 - | (- t)%term => - interp_term env t - | [n]%term => Nnth n env 0 - end. - -(** ** Interpretation of predicats (as Coq propositions) *) - -Fixpoint interp_prop (envp : list Prop) (env : list int) - (p : proposition) : Prop := - match p with - | EqTerm t1 t2 => interp_term env t1 = interp_term env t2 - | NeqTerm t1 t2 => (interp_term env t1) <> (interp_term env t2) - | LeqTerm t1 t2 => interp_term env t1 <= interp_term env t2 - | GeqTerm t1 t2 => interp_term env t1 >= interp_term env t2 - | GtTerm t1 t2 => interp_term env t1 > interp_term env t2 - | LtTerm t1 t2 => interp_term env t1 < interp_term env t2 - | TrueTerm => True - | FalseTerm => False - | Tnot p' => ~ interp_prop envp env p' - | Tor p1 p2 => interp_prop envp env p1 \/ interp_prop envp env p2 - | Tand p1 p2 => interp_prop envp env p1 /\ interp_prop envp env p2 - | Timp p1 p2 => interp_prop envp env p1 -> interp_prop envp env p2 - | Tprop n => nth n envp True - end. - -(** ** Intepretation of hypothesis lists (as Coq conjunctions) *) - -Fixpoint interp_hyps (envp : list Prop) (env : list int) (l : hyps) - : Prop := - match l with - | nil => True - | p' :: l' => interp_prop envp env p' /\ interp_hyps envp env l' - end. - -(** ** Interpretation of conclusion + hypotheses - - Here we use Coq implications : it's less easy to manipulate, - but handy to relate to the Coq original goal (cf. the use of - [generalize], and lighter (no repetition of types in intermediate - conjunctions). *) - -Fixpoint interp_goal_concl (c : proposition) (envp : list Prop) - (env : list int) (l : hyps) : Prop := - match l with - | nil => interp_prop envp env c - | p' :: l' => - interp_prop envp env p' -> interp_goal_concl c envp env l' - end. - -Notation interp_goal := (interp_goal_concl FalseTerm). - -(** Equivalence between these two interpretations. *) - -Theorem goal_to_hyps : - forall (envp : list Prop) (env : list int) (l : hyps), - (interp_hyps envp env l -> False) -> interp_goal envp env l. -Proof. - induction l; simpl; auto. -Qed. - -Theorem hyps_to_goal : - forall (envp : list Prop) (env : list int) (l : hyps), - interp_goal envp env l -> interp_hyps envp env l -> False. -Proof. - induction l; simpl; auto. - intros H (H1,H2). auto. -Qed. - -(** ** Interpretations of list of goals - - Here again, two flavours... *) - -Fixpoint interp_list_hyps (envp : list Prop) (env : list int) - (l : lhyps) : Prop := - match l with - | nil => False - | h :: l' => interp_hyps envp env h \/ interp_list_hyps envp env l' - end. - -Fixpoint interp_list_goal (envp : list Prop) (env : list int) - (l : lhyps) : Prop := - match l with - | nil => True - | h :: l' => interp_goal envp env h /\ interp_list_goal envp env l' - end. - -(** Equivalence between the two flavours. *) - -Theorem list_goal_to_hyps : - forall (envp : list Prop) (env : list int) (l : lhyps), - (interp_list_hyps envp env l -> False) -> interp_list_goal envp env l. -Proof. - induction l; simpl; intuition. now apply goal_to_hyps. -Qed. - -Theorem list_hyps_to_goal : - forall (envp : list Prop) (env : list int) (l : lhyps), - interp_list_goal envp env l -> interp_list_hyps envp env l -> False. -Proof. - induction l; simpl; intuition. eapply hyps_to_goal; eauto. -Qed. - -(** ** Stabiliy and validity of operations *) - -(** An operation on terms is stable if the interpretation is unchanged. *) - -Definition term_stable (f : term -> term) := - forall (e : list int) (t : term), interp_term e t = interp_term e (f t). - -(** An operation on one hypothesis is valid if this hypothesis implies - the result of this operation. *) - -Definition valid1 (f : proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 : proposition), - interp_prop ep e p1 -> interp_prop ep e (f p1). - -Definition valid2 (f : proposition -> proposition -> proposition) := - forall (ep : list Prop) (e : list int) (p1 p2 : proposition), - interp_prop ep e p1 -> - interp_prop ep e p2 -> interp_prop ep e (f p1 p2). - -(** Same for lists of hypotheses, and for list of goals *) - -Definition valid_hyps (f : hyps -> hyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_hyps ep e lp -> interp_hyps ep e (f lp). - -Definition valid_list_hyps (f : hyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_hyps ep e lp -> interp_list_hyps ep e (f lp). - -Definition valid_list_goal (f : hyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : hyps), - interp_list_goal ep e (f lp) -> interp_goal ep e lp. - -(** Some results about these validities. *) - -Theorem valid_goal : - forall (ep : list Prop) (env : list int) (l : hyps) (a : hyps -> hyps), - valid_hyps a -> interp_goal ep env (a l) -> interp_goal ep env l. -Proof. - intros; simpl; apply goal_to_hyps; intro H1; - apply (hyps_to_goal ep env (a l) H0); apply H; assumption. -Qed. - -Theorem goal_valid : - forall f : hyps -> lhyps, valid_list_hyps f -> valid_list_goal f. -Proof. - unfold valid_list_goal; intros f H ep e lp H1; apply goal_to_hyps; - intro H2; apply list_hyps_to_goal with (1 := H1); - apply (H ep e lp); assumption. -Qed. - -Theorem append_valid : - forall (ep : list Prop) (e : list int) (l1 l2 : lhyps), - interp_list_hyps ep e l1 \/ interp_list_hyps ep e l2 -> - interp_list_hyps ep e (l1 ++ l2). -Proof. - induction l1; simpl in *. - - now intros l2 [H| H]. - - intros l2 [[H| H]| H]. - + auto. - + right; apply IHl1; now left. - + right; apply IHl1; now right. -Qed. - -(** ** Valid operations on hypotheses *) - -(** Extract an hypothesis from the list *) - -Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. - -Theorem nth_valid : - forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), - interp_hyps ep e l -> interp_prop ep e (nth_hyps i l). -Proof. - unfold nth_hyps. induction i; destruct l; simpl in *; try easy. - intros (H1,H2). now apply IHi. -Qed. - -(** Apply a valid operation on two hypotheses from the list, and - store the result in the list. *) - -Definition apply_oper_2 (i j : nat) - (f : proposition -> proposition -> proposition) (l : hyps) := - f (nth_hyps i l) (nth_hyps j l) :: l. - -Theorem apply_oper_2_valid : - forall (i j : nat) (f : proposition -> proposition -> proposition), - valid2 f -> valid_hyps (apply_oper_2 i j f). -Proof. - intros i j f Hf; unfold apply_oper_2, valid_hyps; simpl; - intros lp Hlp; split. - - apply Hf; apply nth_valid; assumption. - - assumption. -Qed. - -(** In-place modification of an hypothesis by application of - a valid operation. *) - -Fixpoint apply_oper_1 (i : nat) (f : proposition -> proposition) - (l : hyps) {struct i} : hyps := - match l with - | nil => nil - | p :: l' => - match i with - | O => f p :: l' - | S j => p :: apply_oper_1 j f l' - end - end. - -Theorem apply_oper_1_valid : - forall (i : nat) (f : proposition -> proposition), - valid1 f -> valid_hyps (apply_oper_1 i f). -Proof. - unfold valid_hyps. - induction i; intros f Hf ep e [ | p lp]; simpl; intuition. -Qed. - -(** ** A tactic for proving stability *) - -Ltac loop t := - match t with - (* Global *) - | (?X1 = ?X2) => loop X1 || loop X2 - | (_ -> ?X1) => loop X1 - (* Interpretations *) - | (interp_hyps _ _ ?X1) => loop X1 - | (interp_list_hyps _ _ ?X1) => loop X1 - | (interp_prop _ _ ?X1) => loop X1 - | (interp_term _ ?X1) => loop X1 - (* Propositions *) - | (EqTerm ?X1 ?X2) => loop X1 || loop X2 - | (LeqTerm ?X1 ?X2) => loop X1 || loop X2 - (* Terms *) - | (?X1 + ?X2)%term => loop X1 || loop X2 - | (?X1 - ?X2)%term => loop X1 || loop X2 - | (?X1 * ?X2)%term => loop X1 || loop X2 - | (- ?X1)%term => loop X1 - | (Tint ?X1) => loop X1 - (* Eliminations *) - | (if ?X1 =? ?X2 then _ else _) => - let H := fresh "H" in - case (beq_reflect X1 X2); intro H; - try (rewrite H in *; clear H); simpl; auto; Simplify - | (if ?X1 <? ?X2 then _ else _) => - case (blt_reflect X1 X2); intro; simpl; auto; Simplify - | (if (?X1 =? ?X2)%term then _ else _) => - let H := fresh "H" in - case (eq_term_reflect X1 X2); intro H; - try (rewrite H in *; clear H); simpl; auto; Simplify - | (if _ && _ then _ else _) => rewrite andb_if; Simplify - | (if negb _ then _ else _) => rewrite negb_if; Simplify - | match N.compare ?X1 ?X2 with _ => _ end => - destruct (N.compare_spec X1 X2); Simplify - | match ?X1 with _ => _ end => destruct X1; auto; Simplify - | _ => fail - end - -with Simplify := match goal with - | |- ?X1 => try loop X1 - | _ => idtac - end. - -(** ** Operations on equation bodies *) - -(** The operations below handle in priority _normalized_ terms, i.e. - terms of the form: - [([v1]*Tint k1 + ([v2]*Tint k2 + (... + Tint cst)))] - with [v1>v2>...] and all [ki<>0]. - See [normalize] below for a way to put terms in this form. - - These operations also produce a correct (but suboptimal) - result in case of non-normalized input terms, but this situation - should normally not happen when running [romega]. - - /!\ Do not modify this section (especially [fusion] and [normalize]) - without tweaking the corresponding functions in [refl_omega.ml]. -*) - -(** Multiplication and sum by two constants. Invariant: [k1<>0]. *) - -Fixpoint scalar_mult_add (t : term) (k1 k2 : int) : term := - match t with - | v1 * Tint x1 + l1 => - v1 * Tint (x1 * k1) + scalar_mult_add l1 k1 k2 - | Tint x => Tint (k1 * x + k2) - | _ => t * Tint k1 + Tint k2 (* shouldn't happen *) - end%term. - -Theorem scalar_mult_add_stable e t k1 k2 : - interp_term e (scalar_mult_add t k1 k2) = - interp_term e (t * Tint k1 + Tint k2). -Proof. - induction t; simpl; Simplify; simpl; auto. f_equal. apply mult_comm. - rewrite IHt2. simpl. apply OMEGA11. -Qed. - -(** Multiplication by a (non-nul) constant. *) - -Definition scalar_mult (t : term) (k : int) := scalar_mult_add t k 0. - -Theorem scalar_mult_stable e t k : - interp_term e (scalar_mult t k) = - interp_term e (t * Tint k). -Proof. - unfold scalar_mult. rewrite scalar_mult_add_stable. simpl. - apply plus_0_r. -Qed. - -(** Adding a constant - - Instead of using [scalar_norm_add t 1 k], the following - definition spares some computations. - *) - -Fixpoint scalar_add (t : term) (k : int) : term := - match t with - | m + l => m + scalar_add l k - | Tint x => Tint (x + k) - | _ => t + Tint k - end%term. - -Theorem scalar_add_stable e t k : - interp_term e (scalar_add t k) = interp_term e (t + Tint k). -Proof. - induction t; simpl; Simplify; simpl; auto. - rewrite IHt2. simpl. apply plus_assoc. -Qed. - -(** Division by a constant - - All the non-constant coefficients should be exactly dividable *) - -Fixpoint scalar_div (t : term) (k : int) : option (term * int) := - match t with - | v * Tint x + l => - let (q,r) := diveucl x k in - if (r =? 0)%I then - match scalar_div l k with - | None => None - | Some (u,c) => Some (v * Tint q + u, c) - end - else None - | Tint x => - let (q,r) := diveucl x k in - Some (Tint q, r) - | _ => None - end%term. - -Lemma scalar_div_stable e t k u c : k<>0 -> - scalar_div t k = Some (u,c) -> - interp_term e (u * Tint k + Tint c) = interp_term e t. -Proof. - revert u c. - induction t; simpl; Simplify; try easy. - - intros u c Hk. assert (H := diveucl_spec t0 k Hk). - simpl in H. - destruct diveucl as (q,r). simpl in H. rewrite H. - injection 1 as <- <-. simpl. f_equal. apply mult_comm. - - intros u c Hk. - destruct t1; simpl; Simplify; try easy. - destruct t1_2; simpl; Simplify; try easy. - assert (H := diveucl_spec t0 k Hk). - simpl in H. - destruct diveucl as (q,r). simpl in H. rewrite H. - case beq_reflect; [intros -> | easy]. - destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy]. - injection 1 as <- ->. simpl. - rewrite <- (IHt2 u' c Hk); simpl; auto. - rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11. -Qed. - - -(** Fusion of two equations. - - From two normalized equations, this fusion will produce - a normalized output corresponding to the coefficiented sum. - Invariant: [k1<>0] and [k2<>0]. -*) - -Fixpoint fusion (t1 t2 : term) (k1 k2 : int) : term := - match t1 with - | [v1] * Tint x1 + l1 => - (fix fusion_t1 t2 : term := - match t2 with - | [v2] * Tint x2 + l2 => - match N.compare v1 v2 with - | Eq => - let k := (k1 * x1 + k2 * x2)%I in - if (k =? 0)%I then fusion l1 l2 k1 k2 - else [v1] * Tint k + fusion l1 l2 k1 k2 - | Lt => [v2] * Tint (k2 * x2) + fusion_t1 l2 - | Gt => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2 - end - | Tint x2 => [v1] * Tint (k1 * x1) + fusion l1 t2 k1 k2 - | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *) - end) t2 - | Tint x1 => scalar_mult_add t2 k2 (k1 * x1) - | _ => t1 * Tint k1 + t2 * Tint k2 (* shouldn't happen *) - end%term. - -Theorem fusion_stable e t1 t2 k1 k2 : - interp_term e (fusion t1 t2 k1 k2) = - interp_term e (t1 * Tint k1 + t2 * Tint k2). -Proof. - revert t2; induction t1; simpl; Simplify; simpl; auto. - - intros; rewrite scalar_mult_add_stable. simpl. - rewrite plus_comm. f_equal. apply mult_comm. - - intros. Simplify. induction t2; simpl; Simplify; simpl; auto. - + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11. - + rewrite IHt1_2. simpl. subst n0. - rewrite (mult_comm k1), (mult_comm k2) in H0. - rewrite <- OMEGA10, H0. now autorewrite with int. - + rewrite IHt1_2. simpl. subst n0. - rewrite (mult_comm k1), (mult_comm k2); apply OMEGA10. - + rewrite IHt2_2. simpl. rewrite (mult_comm k2); apply OMEGA12. - + rewrite IHt1_2. simpl. rewrite (mult_comm k1); apply OMEGA11. -Qed. - -(** Term normalization. - - Precondition: all [Tmult] should be on at least one [Tint]. - Postcondition: a normalized equivalent term (see below). -*) - -Fixpoint normalize t := - match t with - | Tint n => Tint n - | [n]%term => ([n] * Tint 1 + Tint 0)%term - | (t + t')%term => fusion (normalize t) (normalize t') 1 1 - | (- t)%term => scalar_mult (normalize t) (-(1)) - | (t - t')%term => fusion (normalize t) (normalize t') 1 (-(1)) - | (Tint k * t)%term | (t * Tint k)%term => - if k =? 0 then Tint 0 else scalar_mult (normalize t) k - | (t1 * t2)%term => (t1 * t2)%term (* shouldn't happen *) - end. - -Theorem normalize_stable : term_stable normalize. -Proof. - intros e t. - induction t; simpl; Simplify; simpl; - rewrite ?scalar_mult_stable; simpl in *; rewrite <- ?IHt1; - rewrite ?fusion_stable; simpl; autorewrite with int; auto. - - now f_equal. - - rewrite mult_comm. now f_equal. - - rewrite <- opp_eq_mult_neg_1, <-minus_def. now f_equal. - - rewrite <- opp_eq_mult_neg_1. now f_equal. -Qed. - -(** ** Normalization of a proposition. - - The only basic facts left after normalization are - [0 = ...] or [0 <> ...] or [0 <= ...]. - When a fact is in negative position, we factorize a [Tnot] - out of it, and normalize the reversed fact inside. - - /!\ Here again, do not change this code without corresponding - modifications in [refl_omega.ml]. -*) - -Fixpoint normalize_prop (negated:bool)(p:proposition) := - match p with - | EqTerm t1 t2 => - if negated then Tnot (NeqTerm (Tint 0) (normalize (t1-t2))) - else EqTerm (Tint 0) (normalize (t1-t2)) - | NeqTerm t1 t2 => - if negated then Tnot (EqTerm (Tint 0) (normalize (t1-t2))) - else NeqTerm (Tint 0) (normalize (t1-t2)) - | LeqTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1))))) - else LeqTerm (Tint 0) (normalize (t2-t1)) - | GeqTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1))))) - else LeqTerm (Tint 0) (normalize (t1-t2)) - | LtTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t1-t2))) - else LeqTerm (Tint 0) (normalize (t2-t1+Tint (-(1)))) - | GtTerm t1 t2 => - if negated then Tnot (LeqTerm (Tint 0) (normalize (t2-t1))) - else LeqTerm (Tint 0) (normalize (t1-t2+Tint (-(1)))) - | Tnot p => Tnot (normalize_prop (negb negated) p) - | Tor p p' => Tor (normalize_prop negated p) (normalize_prop negated p') - | Tand p p' => Tand (normalize_prop negated p) (normalize_prop negated p') - | Timp p p' => Timp (normalize_prop (negb negated) p) - (normalize_prop negated p') - | Tprop _ | TrueTerm | FalseTerm => p - end. - -Definition normalize_hyps := List.map (normalize_prop false). - -Local Ltac simp := cbn -[normalize]. - -Theorem normalize_prop_valid b e ep p : - interp_prop e ep (normalize_prop b p) <-> interp_prop e ep p. -Proof. - revert b. - induction p; intros; simp; try tauto. - - destruct b; simp; - rewrite <- ?normalize_stable; simpl; rewrite ?minus_def. - + rewrite not_eq. apply egal_left. - + apply egal_left. - - destruct b; simp; - rewrite <- ?normalize_stable; simpl; rewrite ?minus_def; - apply not_iff_compat, egal_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + symmetry. rewrite le_lt_iff. apply not_iff_compat, lt_left. - + now rewrite <- le_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + symmetry. rewrite ge_le_iff, le_lt_iff. - apply not_iff_compat, lt_left. - + rewrite ge_le_iff. now rewrite <- le_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + rewrite gt_lt_iff, lt_le_iff. apply not_iff_compat. - now rewrite <- le_left. - + symmetry. rewrite gt_lt_iff. apply lt_left. - - destruct b; simp; - rewrite <- ? normalize_stable; simpl; rewrite ?minus_def. - + rewrite lt_le_iff. apply not_iff_compat. - now rewrite <- le_left. - + symmetry. apply lt_left. - - now rewrite IHp. - - now rewrite IHp1, IHp2. - - now rewrite IHp1, IHp2. - - now rewrite IHp1, IHp2. -Qed. - -Theorem normalize_hyps_valid : valid_hyps normalize_hyps. -Proof. - intros e ep l. induction l; simpl; intuition. - now rewrite normalize_prop_valid. -Qed. - -Theorem normalize_hyps_goal (ep : list Prop) (env : list int) (l : hyps) : - interp_goal ep env (normalize_hyps l) -> interp_goal ep env l. -Proof. - intros; apply valid_goal with (2 := H); apply normalize_hyps_valid. -Qed. - -(** ** A simple decidability checker - - For us, everything is considered decidable except - propositional atoms [Tprop _]. *) - -Fixpoint decidability (p : proposition) : bool := - match p with - | Tnot t => decidability t - | Tand t1 t2 => decidability t1 && decidability t2 - | Timp t1 t2 => decidability t1 && decidability t2 - | Tor t1 t2 => decidability t1 && decidability t2 - | Tprop _ => false - | _ => true - end. - -Theorem decidable_correct : - forall (ep : list Prop) (e : list int) (p : proposition), - decidability p = true -> decidable (interp_prop ep e p). -Proof. - induction p; simpl; intros Hp; try destruct (andb_prop _ _ Hp). - - apply dec_eq. - - apply dec_ne. - - apply dec_le. - - apply dec_ge. - - apply dec_gt. - - apply dec_lt. - - left; auto. - - right; unfold not; auto. - - apply dec_not; auto. - - apply dec_or; auto. - - apply dec_and; auto. - - apply dec_imp; auto. - - discriminate. -Qed. - -(** ** Omega steps - - The following inductive type describes steps as they can be - found in the trace coming from the decision procedure Omega. - We consider here only normalized equations [0=...], disequations - [0<>...] or inequations [0<=...]. - - First, the final steps leading to a contradiction: - - [O_BAD_CONSTANT i] : hypothesis i has a constant body - and this constant is not compatible with the kind of i. - - [O_NOT_EXACT_DIVIDE i k] : - equation i can be factorized as some [k*t+c] with [0<c<k]. - - Now, the intermediate steps leading to a new hypothesis: - - [O_DIVIDE i k cont] : - the body of hypothesis i could be factorized as [k*t+c] - with either [k<>0] and [c=0] for a (dis)equation, or - [0<k] and [c<k] for an inequation. We change in-place the - body of i for [t]. - - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose - kind depends on the kind of hypotheses [i1] and [i2], and - whose body is [k1*body(i1) + k2*body(i2)]. Depending of the - situation, [k1] or [k2] might have to be positive or non-nul. - - [O_MERGE_EQ i j cont] : - inequations i and j have opposite bodies, we add an equation - with one these bodies. - - [O_SPLIT_INEQ i cont1 cont2] : - disequation i is split into a disjonction of inequations. -*) - -Definition idx := nat. (** Index of an hypothesis in the list *) - -Inductive t_omega : Set := - | O_BAD_CONSTANT : idx -> t_omega - | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega - - | O_DIVIDE : idx -> int -> t_omega -> t_omega - | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega - | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega - | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega. - -(** ** Actual resolution steps of an omega normalized goal *) - -(** First, the final steps, leading to a contradiction *) - -(** [O_BAD_CONSTANT] *) - -Definition bad_constant (i : nat) (h : hyps) := - match nth_hyps i h with - | EqTerm (Tint Nul) (Tint n) => if n =? Nul then h else absurd - | NeqTerm (Tint Nul) (Tint n) => if n =? Nul then absurd else h - | LeqTerm (Tint Nul) (Tint n) => if n <? Nul then absurd else h - | _ => h - end. - -Theorem bad_constant_valid i : valid_hyps (bad_constant i). -Proof. - unfold valid_hyps, bad_constant; intros ep e lp H. - generalize (nth_valid ep e i lp H); Simplify. - rewrite le_lt_iff. intuition. -Qed. - -(** [O_NOT_EXACT_DIVIDE] *) - -Definition not_exact_divide (i : nat) (k : int) (l : hyps) := - match nth_hyps i l with - | EqTerm (Tint Nul) b => - match scalar_div b k with - | Some (body,c) => - if (Nul =? 0) && (0 <? c) && (c <? k) then absurd - else l - | None => l - end - | _ => l - end. - -Theorem not_exact_divide_valid i k : - valid_hyps (not_exact_divide i k). -Proof. - unfold valid_hyps, not_exact_divide; intros. - generalize (nth_valid ep e i lp). - destruct (nth_hyps i lp); simpl; auto. - destruct t0; auto. - destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto. - Simplify. - assert (k <> 0). - { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H'; rewrite <- H' in E; auto. - exfalso. revert E. now apply OMEGA4. -Qed. - -(** Now, the steps generating a new equation. *) - -(** [O_DIVIDE] *) - -Definition divide (k : int) (prop : proposition) := - match prop with - | EqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (c =? 0) && negb (k =? 0) - then EqTerm (Tint 0) body - else TrueTerm - | None => TrueTerm - end - | NeqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (c =? 0) && negb (k =? 0) - then NeqTerm (Tint 0) body - else TrueTerm - | None => TrueTerm - end - | LeqTerm (Tint o) b => - match scalar_div b k with - | Some (body,c) => - if (o =? 0) && (0 <? k) && (c <? k) - then LeqTerm (Tint 0) body - else prop - | None => prop - end - | _ => TrueTerm - end. - -Theorem divide_valid k : valid1 (divide k). -Proof. - unfold valid1, divide; intros ep e p; - destruct p; simpl; auto; - destruct t0; simpl; auto; - destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto. - - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H'; rewrite <- H' in E. rewrite plus_0_r in E. - apply mult_integral in E. intuition. - - apply (scalar_div_stable e) in E; auto. simpl in E. - intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E. - - assert (k <> 0). - { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } - apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E. - intro H'. now apply mult_le_approx with (3 := H'). -Qed. - -(** [O_SUM]. Invariant: [k1] and [k2] non-nul. *) - -Definition sum (k1 k2 : int) (prop1 prop2 : proposition) := - match prop1 with - | EqTerm (Tint o) b1 => - match prop2 with - | EqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) - then EqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | LeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && (0 <? k2) - then LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | NeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && negb (k2 =? 0) - then NeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - | LeqTerm (Tint o) b1 => - if (o =? 0) && (0 <? k1) - then match prop2 with - | EqTerm (Tint o') b2 => - if o' =? 0 then - LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | LeqTerm (Tint o') b2 => - if (o' =? 0) && (0 <? k2) - then LeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - else TrueTerm - | NeqTerm (Tint o) b1 => - match prop2 with - | EqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && negb (k1 =? 0) - then NeqTerm (Tint 0) (fusion b1 b2 k1 k2) - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem sum_valid : - forall (k1 k2 : int), valid2 (sum k1 k2). -Proof. - unfold valid2; intros k1 k2 t ep e p1 p2; unfold sum; - Simplify; simpl; rewrite ?fusion_stable; - simpl; intros; auto. - - apply sum1; auto. - - rewrite plus_comm. apply sum5; auto. - - apply sum2; auto using lt_le_weak. - - apply sum5; auto. - - rewrite plus_comm. apply sum2; auto using lt_le_weak. - - apply sum3; auto using lt_le_weak. -Qed. - -(** [MERGE_EQ] *) - -Definition merge_eq (prop1 prop2 : proposition) := - match prop1 with - | LeqTerm (Tint o) b1 => - match prop2 with - | LeqTerm (Tint o') b2 => - if (o =? 0) && (o' =? 0) && - (b1 =? scalar_mult b2 (-(1)))%term - then EqTerm (Tint 0) b1 - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem merge_eq_valid : valid2 merge_eq. -Proof. - unfold valid2, merge_eq; intros ep e p1 p2; Simplify; simpl; auto. - rewrite scalar_mult_stable. simpl. - intros; symmetry ; apply OMEGA8 with (2 := H0). - - assumption. - - elim opp_eq_mult_neg_1; trivial. -Qed. - -(** [O_SPLIT_INEQ] (only step to produce two subgoals). *) - -Definition split_ineq (i : nat) (f1 f2 : hyps -> lhyps) (l : hyps) := - match nth_hyps i l with - | NeqTerm (Tint o) b1 => - if o =? 0 then - f1 (LeqTerm (Tint 0) (scalar_add b1 (-(1))) :: l) ++ - f2 (LeqTerm (Tint 0) (scalar_mult_add b1 (-(1)) (-(1))) :: l) - else l :: nil - | _ => l :: nil - end. - -Theorem split_ineq_valid : - forall (i : nat) (f1 f2 : hyps -> lhyps), - valid_list_hyps f1 -> - valid_list_hyps f2 -> valid_list_hyps (split_ineq i f1 f2). -Proof. - unfold valid_list_hyps, split_ineq; intros i f1 f2 H1 H2 ep e lp H; - generalize (nth_valid _ _ i _ H); case (nth_hyps i lp); - simpl; auto; intros t1 t2; case t1; simpl; - auto; intros z; simpl; auto; intro H3. - Simplify. - apply append_valid; elim (OMEGA19 (interp_term e t2)). - - intro H4; left; apply H1; simpl; rewrite scalar_add_stable; - simpl; auto. - - intro H4; right; apply H2; simpl; rewrite scalar_mult_add_stable; - simpl; auto. - - generalize H3; unfold not; intros E1 E2; apply E1; - symmetry ; trivial. -Qed. - -(** ** Replaying the resolution trace *) - -Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := - match t with - | O_BAD_CONSTANT i => singleton (bad_constant i l) - | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l) - | O_DIVIDE i k cont => - execute_omega cont (apply_oper_1 i (divide k) l) - | O_SUM k1 i1 k2 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l) - | O_MERGE_EQ i1 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 merge_eq l) - | O_SPLIT_INEQ i cont1 cont2 => - split_ineq i (execute_omega cont1) (execute_omega cont2) l - end. - -Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). -Proof. - simple induction tr; unfold valid_list_hyps, valid_hyps; simpl. - - intros; left; now apply bad_constant_valid. - - intros; left; now apply not_exact_divide_valid. - - intros m k t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_1_valid m (divide k) - (divide_valid k) ep e lp H). - - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e - lp H). - - intros i1 i2 t' Ht' ep e lp H; apply Ht'; - apply - (apply_oper_2_valid i1 i2 merge_eq merge_eq_valid ep e - lp H). - - intros i k1 H1 k2 H2 ep e lp H; - apply - (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e - lp H). -Qed. - - -(** ** Rules for decomposing the hypothesis - - This type allows navigation 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 conjunction. - NB: negations are now silently traversed. *) - -Inductive direction : Set := - | D_left : direction - | D_right : direction. - -(** This type allows extracting useful components from hypothesis, either - hypothesis generated by splitting a disjonction, or equations. - The last constructor indicates how to solve the obtained system - via the use of the trace type of Omega [t_omega] *) - -Inductive e_step : Set := - | E_SPLIT : nat -> list direction -> e_step -> e_step -> e_step - | E_EXTRACT : nat -> list direction -> e_step -> e_step - | E_SOLVE : t_omega -> e_step. - -(** Selection of a basic fact inside an hypothesis. *) - -Fixpoint extract_hyp_pos (s : list direction) (p : proposition) : - proposition := - match p, s with - | Tand x y, D_left :: l => extract_hyp_pos l x - | Tand x y, D_right :: l => extract_hyp_pos l y - | Tnot x, _ => extract_hyp_neg s x - | _, _ => p - end - - with extract_hyp_neg (s : list direction) (p : proposition) : - proposition := - match p, s with - | Tor x y, D_left :: l => extract_hyp_neg l x - | Tor x y, D_right :: l => extract_hyp_neg l y - | Timp x y, D_left :: l => - if decidability x then extract_hyp_pos l x else Tnot p - | Timp x y, D_right :: l => extract_hyp_neg l y - | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p - | _, _ => Tnot p - end. - -Theorem extract_valid : - forall s : list direction, valid1 (extract_hyp_pos s). -Proof. - assert (forall p s ep e, - (interp_prop ep e p -> - interp_prop ep e (extract_hyp_pos s p)) /\ - (interp_prop ep e (Tnot p) -> - interp_prop ep e (extract_hyp_neg s p))). - { induction p; destruct s; simpl; auto; split; try destruct d; try easy; - intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto; - destruct decidability eqn:D; auto; - apply (decidable_correct ep e) in D; unfold decidable in D; - (apply IHp || apply IHp1); tauto. } - red. intros. now apply H. -Qed. - -(** Attempt to shorten error messages if romega goes rogue... - NB: [interp_list_goal _ _ BUG = False /\ True]. *) -Definition BUG : lhyps := nil :: nil. - -(** Split and extract in hypotheses *) - -Fixpoint decompose_solve (s : e_step) (h : hyps) : lhyps := - match s with - | E_SPLIT i dl s1 s2 => - match extract_hyp_pos dl (nth_hyps i h) with - | Tor x y => decompose_solve s1 (x :: h) ++ decompose_solve s2 (y :: h) - | Tnot (Tand x y) => - if decidability x - then - decompose_solve s1 (Tnot x :: h) ++ - decompose_solve s2 (Tnot y :: h) - else BUG - | Timp x y => - if decidability x then - decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h) - else BUG - | _ => BUG - end - | E_EXTRACT i dl s1 => - decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h) - | E_SOLVE t => execute_omega t h - end. - -Theorem decompose_solve_valid (s : e_step) : - valid_list_goal (decompose_solve s). -Proof. - apply goal_valid. red. induction s; simpl; intros ep e lp H. - - assert (H' : interp_prop ep e (extract_hyp_pos l (nth_hyps n lp))). - { now apply extract_valid, nth_valid. } - destruct extract_hyp_pos; simpl in *; auto. - + destruct p; simpl; auto. - destruct decidability eqn:D; [ | simpl; auto]. - apply (decidable_correct ep e) in D. - apply append_valid. simpl in *. destruct D. - * right. apply IHs2. simpl; auto. - * left. apply IHs1. simpl; auto. - + apply append_valid. destruct H'. - * left. apply IHs1. simpl; auto. - * right. apply IHs2. simpl; auto. - + destruct decidability eqn:D; [ | simpl; auto]. - apply (decidable_correct ep e) in D. - apply append_valid. destruct D. - * right. apply IHs2. simpl; auto. - * left. apply IHs1. simpl; auto. - - apply IHs; simpl; split; auto. - now apply extract_valid, nth_valid. - - now apply omega_valid. -Qed. - -(** Reduction of subgoal list by discarding the contradictory subgoals. *) - -Definition valid_lhyps (f : lhyps -> lhyps) := - forall (ep : list Prop) (e : list int) (lp : lhyps), - interp_list_hyps ep e lp -> interp_list_hyps ep e (f lp). - -Fixpoint reduce_lhyps (lp : lhyps) : lhyps := - match lp with - | nil => nil - | (FalseTerm :: nil) :: lp' => reduce_lhyps lp' - | x :: lp' => BUG - end. - -Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps. -Proof. - unfold valid_lhyps; intros ep e lp; elim lp. - - simpl; auto. - - intros a l HR; elim a. - + simpl; tauto. - + intros a1 l1; case l1; case a1; simpl; tauto. -Qed. - -Theorem do_reduce_lhyps : - forall (envp : list Prop) (env : list int) (l : lhyps), - interp_list_goal envp env (reduce_lhyps l) -> interp_list_goal envp env l. -Proof. - intros envp env l H; apply list_goal_to_hyps; intro H1; - apply list_hyps_to_goal with (1 := H); apply reduce_lhyps_valid; - assumption. -Qed. - -(** Pushing the conclusion into the hypotheses. *) - -Definition concl_to_hyp (p : proposition) := - if decidability p then Tnot p else TrueTerm. - -Definition do_concl_to_hyp : - forall (envp : list Prop) (env : list int) (c : proposition) (l : hyps), - interp_goal envp env (concl_to_hyp c :: l) -> - interp_goal_concl c envp env l. -Proof. - induction l; simpl. - - unfold concl_to_hyp; simpl. - destruct decidability eqn:D; [ | simpl; tauto ]. - apply (decidable_correct envp env) in D. unfold decidable in D. - simpl. tauto. - - simpl in *; tauto. -Qed. - -(** The omega tactic : all steps together *) - -Definition omega_tactic (t1 : e_step) (c : proposition) (l : hyps) := - reduce_lhyps (decompose_solve t1 (normalize_hyps (concl_to_hyp c :: l))). - -Theorem do_omega : - forall (t : e_step) (envp : list Prop) - (env : list int) (c : proposition) (l : hyps), - interp_list_goal envp env (omega_tactic t c l) -> - interp_goal_concl c envp env l. -Proof. - unfold omega_tactic; intros t ep e c l H. - apply do_concl_to_hyp. - apply normalize_hyps_goal. - apply (decompose_solve_valid t). - now apply do_reduce_lhyps. -Qed. - -End IntOmega. - -(** For now, the above modular construction is instanciated on Z, - in order to retrieve the initial ROmega. *) - -Module ZOmega := IntOmega(Z_as_Int). diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml deleted file mode 100644 index 949cba2dbe..0000000000 --- a/plugins/romega/const_omega.ml +++ /dev/null @@ -1,332 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -open Names - -let module_refl_name = "ReflOmegaCore" -let module_refl_path = ["Coq"; "romega"; module_refl_name] - -type result = - | Kvar of string - | Kapp of string * EConstr.t list - | Kimp of EConstr.t * EConstr.t - | Kufo - -let meaningful_submodule = [ "Z"; "N"; "Pos" ] - -let string_of_global r = - let dp = Nametab.dirpath_of_global r in - let prefix = match Names.DirPath.repr dp with - | [] -> "" - | m::_ -> - let s = Names.Id.to_string m in - if Util.String.List.mem s meaningful_submodule then s^"." else "" - in - prefix^(Names.Id.to_string (Nametab.basename_of_global r)) - -let destructurate sigma t = - let c, args = EConstr.decompose_app sigma t in - let open Constr in - match EConstr.kind sigma c, args with - | Const (sp,_), args -> - Kapp (string_of_global (Globnames.ConstRef sp), args) - | Construct (csp,_) , args -> - Kapp (string_of_global (Globnames.ConstructRef csp), args) - | Ind (isp,_), args -> - Kapp (string_of_global (Globnames.IndRef isp), args) - | Var id, [] -> Kvar(Names.Id.to_string id) - | Prod (Anonymous,typ,body), [] -> Kimp(typ,body) - | _ -> Kufo - -exception DestConstApp - -let dest_const_apply sigma t = - let open Constr in - let f,args = EConstr.decompose_app sigma t in - let ref = - match EConstr.kind sigma f with - | Const (sp,_) -> Globnames.ConstRef sp - | Construct (csp,_) -> Globnames.ConstructRef csp - | Ind (isp,_) -> Globnames.IndRef isp - | _ -> raise DestConstApp - in Nametab.basename_of_global ref, args - -let logic_dir = ["Coq";"Logic";"Decidable"] - -let coq_modules = - Coqlib.init_modules @ [logic_dir] @ Coqlib.arith_modules @ Coqlib.zarith_base_modules - @ [["Coq"; "Lists"; "List"]] - @ [module_refl_path] - @ [module_refl_path@["ZOmega"]] - -let bin_module = [["Coq";"Numbers";"BinNums"]] -let z_module = [["Coq";"ZArith";"BinInt"]] - -let init_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x -let constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" coq_modules x -let z_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" z_module x -let bin_constant x = - EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.gen_reference_in_modules "Omega" bin_module x - -(* Logic *) -let coq_refl_equal = lazy(init_constant "eq_refl") -let coq_and = lazy(init_constant "and") -let coq_not = lazy(init_constant "not") -let coq_or = lazy(init_constant "or") -let coq_True = lazy(init_constant "True") -let coq_False = lazy(init_constant "False") -let coq_I = lazy(init_constant "I") - -(* ReflOmegaCore/ZOmega *) - -let coq_t_int = lazy (constant "Tint") -let coq_t_plus = lazy (constant "Tplus") -let coq_t_mult = lazy (constant "Tmult") -let coq_t_opp = lazy (constant "Topp") -let coq_t_minus = lazy (constant "Tminus") -let coq_t_var = lazy (constant "Tvar") - -let coq_proposition = lazy (constant "proposition") -let coq_p_eq = lazy (constant "EqTerm") -let coq_p_leq = lazy (constant "LeqTerm") -let coq_p_geq = lazy (constant "GeqTerm") -let coq_p_lt = lazy (constant "LtTerm") -let coq_p_gt = lazy (constant "GtTerm") -let coq_p_neq = lazy (constant "NeqTerm") -let coq_p_true = lazy (constant "TrueTerm") -let coq_p_false = lazy (constant "FalseTerm") -let coq_p_not = lazy (constant "Tnot") -let coq_p_or = lazy (constant "Tor") -let coq_p_and = lazy (constant "Tand") -let coq_p_imp = lazy (constant "Timp") -let coq_p_prop = lazy (constant "Tprop") - -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_sum = lazy (constant "O_SUM") -let coq_s_merge_eq = lazy (constant "O_MERGE_EQ") -let coq_s_split_ineq =lazy (constant "O_SPLIT_INEQ") - -(* 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_e_split = lazy (constant "E_SPLIT") -let coq_e_extract = lazy (constant "E_EXTRACT") -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") - -(* Nat *) - -let coq_S = lazy(init_constant "S") -let coq_O = lazy(init_constant "O") - -let rec mk_nat = function - | 0 -> Lazy.force coq_O - | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) - -(* Lists *) - -let mkListConst c = - let r = - Coqlib.coq_reference "" ["Init";"Datatypes"] c - in - let inst = - if Global.is_polymorphic r then - fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|]) - else - fun _ -> EConstr.EInstance.empty - in - fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u) - -let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = EConstr.mkApp (mkListConst "nil" univ, [|typ|]) - -let mk_list univ typ l = - let rec loop = function - | [] -> coq_nil univ typ - | (step :: l) -> - EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in - loop l - -let mk_plist = - let type1lev = UnivGen.new_univ_level () in - fun l -> mk_list type1lev EConstr.mkProp l - -let mk_list = mk_list Univ.Level.set - -type parse_term = - | Tplus of EConstr.t * EConstr.t - | Tmult of EConstr.t * EConstr.t - | Tminus of EConstr.t * EConstr.t - | Topp of EConstr.t - | Tsucc of EConstr.t - | Tnum of Bigint.bigint - | Tother - -type parse_rel = - | Req of EConstr.t * EConstr.t - | Rne of EConstr.t * EConstr.t - | Rlt of EConstr.t * EConstr.t - | Rle of EConstr.t * EConstr.t - | Rgt of EConstr.t * EConstr.t - | Rge of EConstr.t * EConstr.t - | Rtrue - | Rfalse - | Rnot of EConstr.t - | Ror of EConstr.t * EConstr.t - | Rand of EConstr.t * EConstr.t - | Rimp of EConstr.t * EConstr.t - | Riff of EConstr.t * EConstr.t - | Rother - -let parse_logic_rel sigma c = match destructurate sigma 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_Z = lazy (bin_constant "Z") -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 - EConstr.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 -> EConstr.mkApp (Lazy.force coq_Npos, - [| mk_positive (Bigint.of_int n) |]) - -module type Int = sig - val typ : EConstr.t Lazy.t - val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool - val plus : EConstr.t Lazy.t - val mult : EConstr.t Lazy.t - val opp : EConstr.t Lazy.t - val minus : EConstr.t Lazy.t - - val mk : Bigint.bigint -> EConstr.t - val parse_term : Evd.evar_map -> EConstr.t -> parse_term - val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel - (* check whether t is built only with numbers and + * - *) - val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option -end - -module Z : Int = struct - -let typ = coq_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 recognize_pos sigma t = - let rec loop t = - let f,l = dest_const_apply sigma t in - match 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 - | _ -> raise DestConstApp - in - try Some (loop t) with DestConstApp -> None - -let recognize_Z sigma t = - try - let f,l = dest_const_apply sigma t in - match Id.to_string f,l with - | "Zpos",[t] -> recognize_pos sigma t - | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t) - | "Z0",[] -> Some Bigint.zero - | _ -> None - with DestConstApp -> None - -let mk_Z n = - if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 - else if Bigint.is_strictly_pos n then - EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) - else - EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) - -let mk = mk_Z - -let parse_term sigma t = - match destructurate sigma 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 sigma t with Some t -> Tnum t | None -> Tother) - | _ -> Tother - -let is_int_typ gl t = - Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z) - -let parse_rel gl t = - let sigma = Proofview.Goal.sigma gl in - match destructurate sigma t with - | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> 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 sigma t - -let rec get_scalar sigma t = - match destructurate sigma t with - | Kapp("Z.add", [t1;t2]) -> - Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp ("Z.sub",[t1;t2]) -> - Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp ("Z.mul",[t1;t2]) -> - Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2) - | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t) - | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t) - | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t - | _ -> None - -end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli deleted file mode 100644 index 64668df007..0000000000 --- a/plugins/romega/const_omega.mli +++ /dev/null @@ -1,124 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - - -(** Coq objects used in romega *) - -(* from Logic *) -val coq_refl_equal : EConstr.t lazy_t -val coq_and : EConstr.t lazy_t -val coq_not : EConstr.t lazy_t -val coq_or : EConstr.t lazy_t -val coq_True : EConstr.t lazy_t -val coq_False : EConstr.t lazy_t -val coq_I : EConstr.t lazy_t - -(* from ReflOmegaCore/ZOmega *) - -val coq_t_int : EConstr.t lazy_t -val coq_t_plus : EConstr.t lazy_t -val coq_t_mult : EConstr.t lazy_t -val coq_t_opp : EConstr.t lazy_t -val coq_t_minus : EConstr.t lazy_t -val coq_t_var : EConstr.t lazy_t - -val coq_proposition : EConstr.t lazy_t -val coq_p_eq : EConstr.t lazy_t -val coq_p_leq : EConstr.t lazy_t -val coq_p_geq : EConstr.t lazy_t -val coq_p_lt : EConstr.t lazy_t -val coq_p_gt : EConstr.t lazy_t -val coq_p_neq : EConstr.t lazy_t -val coq_p_true : EConstr.t lazy_t -val coq_p_false : EConstr.t lazy_t -val coq_p_not : EConstr.t lazy_t -val coq_p_or : EConstr.t lazy_t -val coq_p_and : EConstr.t lazy_t -val coq_p_imp : EConstr.t lazy_t -val coq_p_prop : EConstr.t lazy_t - -val coq_s_bad_constant : EConstr.t lazy_t -val coq_s_divide : EConstr.t lazy_t -val coq_s_not_exact_divide : EConstr.t lazy_t -val coq_s_sum : EConstr.t lazy_t -val coq_s_merge_eq : EConstr.t lazy_t -val coq_s_split_ineq : EConstr.t lazy_t - -val coq_direction : EConstr.t lazy_t -val coq_d_left : EConstr.t lazy_t -val coq_d_right : EConstr.t lazy_t - -val coq_e_split : EConstr.t lazy_t -val coq_e_extract : EConstr.t lazy_t -val coq_e_solve : EConstr.t lazy_t - -val coq_interp_sequent : EConstr.t lazy_t -val coq_do_omega : EConstr.t lazy_t - -val mk_nat : int -> EConstr.t -val mk_N : int -> EConstr.t - -(** Precondition: the type of the list is in Set *) -val mk_list : EConstr.t -> EConstr.t list -> EConstr.t -val mk_plist : EConstr.types list -> EConstr.types - -(** Analyzing a coq term *) - -(* The generic result shape of the analysis of a term. - One-level depth, except when a number is found *) -type parse_term = - Tplus of EConstr.t * EConstr.t - | Tmult of EConstr.t * EConstr.t - | Tminus of EConstr.t * EConstr.t - | Topp of EConstr.t - | Tsucc of EConstr.t - | Tnum of Bigint.bigint - | Tother - -(* The generic result shape of the analysis of a relation. - One-level depth. *) -type parse_rel = - Req of EConstr.t * EConstr.t - | Rne of EConstr.t * EConstr.t - | Rlt of EConstr.t * EConstr.t - | Rle of EConstr.t * EConstr.t - | Rgt of EConstr.t * EConstr.t - | Rge of EConstr.t * EConstr.t - | Rtrue - | Rfalse - | Rnot of EConstr.t - | Ror of EConstr.t * EConstr.t - | Rand of EConstr.t * EConstr.t - | Rimp of EConstr.t * EConstr.t - | Riff of EConstr.t * EConstr.t - | Rother - -(* A module factorizing what we should now about the number representation *) -module type Int = - sig - (* the coq type of the numbers *) - val typ : EConstr.t Lazy.t - (* Is a constr expands to the type of these numbers *) - val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool - (* the operations on the numbers *) - val plus : EConstr.t Lazy.t - val mult : EConstr.t Lazy.t - val opp : EConstr.t Lazy.t - val minus : EConstr.t Lazy.t - (* building a coq number *) - val mk : Bigint.bigint -> EConstr.t - (* parsing a term (one level, except if a number is found) *) - val parse_term : Evd.evar_map -> EConstr.t -> parse_term - (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel - (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option - end - -(* Currently, we only use Z numbers *) -module Z : Int diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg deleted file mode 100644 index ac4f30b1db..0000000000 --- a/plugins/romega/g_romega.mlg +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - - -DECLARE PLUGIN "romega_plugin" - -{ - -open Ltac_plugin -open Names -open Refl_omega -open Stdarg - -let eval_tactic name = - let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in - let tac = Tacenv.interp_ltac kn in - Tacinterp.eval_tactic tac - -let romega_tactic unsafe l = - let tacs = List.map - (function - | "nat" -> eval_tactic "zify_nat" - | "positive" -> eval_tactic "zify_positive" - | "N" -> eval_tactic "zify_N" - | "Z" -> eval_tactic "zify_op" - | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) - (Util.List.sort_uniquize String.compare l) - in - Tacticals.New.tclTHEN - (Tacticals.New.tclREPEAT (Proofview.tclPROGRESS (Tacticals.New.tclTHENLIST tacs))) - (Tacticals.New.tclTHEN - (* because of the contradiction process in (r)omega, - we'd better leave as little as possible in the conclusion, - for an easier decidability argument. *) - (Tactics.intros) - (total_reflexive_omega_tactic unsafe)) - -let romega_depr = - Vernacinterp.mk_deprecation - ~since:(Some "8.9") - ~note:(Some "Use lia instead.") - () - -} - -TACTIC EXTEND romega -DEPRECATED { romega_depr } -| [ "romega" ] -> { romega_tactic false [] } -| [ "unsafe_romega" ] -> { romega_tactic true [] } -END - -TACTIC EXTEND romega' -DEPRECATED { romega_depr } -| [ "romega" "with" ne_ident_list(l) ] -> - { romega_tactic false (List.map Names.Id.to_string l) } -| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } -END diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune deleted file mode 100644 index 49b0e10edf..0000000000 --- a/plugins/romega/plugin_base.dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name romega_plugin) - (public_name coq.plugins.romega) - (synopsis "Coq's romega plugin") - (libraries coq.plugins.omega)) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml deleted file mode 100644 index 930048400a..0000000000 --- a/plugins/romega/refl_omega.ml +++ /dev/null @@ -1,1071 +0,0 @@ -(************************************************************************* - - PROJET RNRT Calife - 2001 - Author: Pierre Crégut - France Télécom R&D - Licence : LGPL version 2.1 - - *************************************************************************) - -open Pp -open Util -open Constr -open Const_omega -module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) -open OmegaSolver - -module Id = Names.Id -module IntSet = Int.Set -module IntHtbl = Hashtbl.Make(Int) - -(* \section{Useful functions and flags} *) -(* Especially useful debugging functions *) -let debug = ref false - -let show_goal = Tacticals.New.tclIDTAC - -let pp i = print_int i; print_newline (); flush stdout - -(* More readable than the prefix notation *) -let (>>) = Tacticals.New.tclTHEN - -(* \section{Types} - \subsection{How to walk in a term} - To represent how to get to a proposition. Only choice points are - kept (branch to choose in a disjunction and identifier of the disjunctive - connector) *) -type direction = Left of int | Right of int - -(* Step to find a proposition (operators are at most binary). A list is - a path *) -type occ_step = O_left | O_right | O_mono -type occ_path = occ_step list - -(* chemin identifiant une proposition sous forme du nom de l'hypothèse et - d'une liste de pas à partir de la racine de l'hypothèse *) -type occurrence = {o_hyp : Id.t; o_path : occ_path} - -type atom_index = int - -(* \subsection{reifiable formulas} *) -type oformula = - (* integer *) - | Oint of Bigint.bigint - (* recognized binary and unary operations *) - | Oplus of oformula * oformula - | Omult of oformula * oformula (* Invariant : one side is [Oint] *) - | Ominus of oformula * oformula - | Oopp of oformula - (* an atom in the environment *) - | Oatom of atom_index - -(* Operators for comparison recognized by Omega *) -type comparaison = Eq | Leq | Geq | Gt | Lt | Neq - -(* Representation of reified predicats (fragment of propositional calculus, - no quantifier here). *) -(* Note : in [Pprop p], the non-reified constr [p] should be closed - (it could contains some [Term.Var] but no [Term.Rel]). So no need to - lift when breaking or creating arrows. *) -type oproposition = - Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *) - | Ptrue - | Pfalse - | Pnot of oproposition - | Por of int * oproposition * oproposition - | Pand of int * oproposition * oproposition - | Pimp of int * oproposition * oproposition - | Pprop of EConstr.t - -(* The equations *) -and oequation = { - e_comp: comparaison; (* comparaison *) - e_left: oformula; (* formule brute gauche *) - e_right: oformula; (* formule brute droite *) - e_origin: occurrence; (* l'hypothèse dont vient le terme *) - e_negated: bool; (* vrai si apparait en position nié - après normalisation *) - e_depends: direction list; (* liste des points de disjonction dont - dépend l'accès à l'équation avec la - direction (branche) pour y accéder *) - e_omega: OmegaSolver.afine (* normalized formula *) - } - -(* \subsection{Proof context} - This environment codes - \begin{itemize} - \item the terms and propositions that are given as - parameters of the reified proof (and are represented as variables in the - reified goals) - \item translation functions linking the decision procedure and the Coq proof - \end{itemize} *) - -type environment = { - (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : EConstr.t list; - (* La meme chose pour les propositions *) - mutable props : EConstr.t list; - (* Traduction des indices utilisés ici en les indices finaux utilisés par - * la tactique Omega après dénombrement des variables utiles *) - real_indices : int IntHtbl.t; - mutable cnt_connectors : int; - equations : oequation IntHtbl.t; - constructors : occurrence IntHtbl.t -} - -(* \subsection{Solution tree} - Définition d'une solution trouvée par Omega sous la forme d'un identifiant, - d'un ensemble d'équation dont dépend la solution et d'une trace *) - -type solution = { - s_index : int; - s_equa_deps : IntSet.t; - s_trace : OmegaSolver.action list } - -(* Arbre de solution résolvant complètement un ensemble de systèmes *) -type solution_tree = - Leaf of solution - (* un noeud interne représente un point de branchement correspondant à - l'élimination d'un connecteur générant plusieurs buts - (typ. disjonction). Le premier argument - est l'identifiant du connecteur *) - | Tree of int * solution_tree * solution_tree - -(* Représentation de l'environnement extrait du but initial sous forme de - chemins pour extraire des equations ou d'hypothèses *) - -type context_content = - CCHyp of occurrence - | CCEqua of int - -(** Some dedicated equality tests *) - -let occ_step_eq s1 s2 = match s1, s2 with -| O_left, O_left | O_right, O_right | O_mono, O_mono -> true -| _ -> false - -let rec oform_eq f f' = match f,f' with - | Oint i, Oint i' -> Bigint.equal i i' - | Oplus (f1,f2), Oplus (f1',f2') - | Omult (f1,f2), Omult (f1',f2') - | Ominus (f1,f2), Ominus (f1',f2') -> oform_eq f1 f1' && oform_eq f2 f2' - | Oopp f, Oopp f' -> oform_eq f f' - | Oatom a, Oatom a' -> Int.equal a a' - | _ -> false - -let dir_eq d d' = match d, d' with - | Left i, Left i' | Right i, Right i' -> Int.equal i i' - | _ -> false - -(* \section{Specific utility functions to handle base types} *) -(* Nom arbitraire de l'hypothèse codant la négation du but final *) -let id_concl = Id.of_string "__goal__" - -(* Initialisation de l'environnement de réification de la tactique *) -let new_environment () = { - terms = []; props = []; cnt_connectors = 0; - real_indices = IntHtbl.create 7; - equations = IntHtbl.create 7; - constructors = IntHtbl.create 7; -} - -(* Génération d'un nom d'équation *) -let new_connector_id env = - env.cnt_connectors <- succ env.cnt_connectors; env.cnt_connectors - -(* Calcul de la branche complémentaire *) -let barre = function Left x -> Right x | Right x -> Left x - -(* Identifiant associé à une branche *) -let indice = function Left x | Right x -> x - -(* Affichage de l'environnement de réification (termes et propositions) *) -let print_env_reification env = - let rec loop c i = function - [] -> str " ===============================\n\n" - | t :: l -> - let sigma, env = Pfedit.get_current_context () in - let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ - loop c (succ i) l - in - let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in - let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in - Feedback.msg_debug (prop_info ++ fnl () ++ term_info) - -(* \subsection{Gestion des environnements de variable pour Omega} *) -(* generation d'identifiant d'equation pour Omega *) - -let new_omega_eq, rst_omega_eq = - let cpt = ref (-1) in - (function () -> incr cpt; !cpt), - (function () -> cpt:=(-1)) - -(* generation d'identifiant de variable pour Omega *) - -let new_omega_var, rst_omega_var, set_omega_maxvar = - let cpt = ref (-1) in - (function () -> incr cpt; !cpt), - (function () -> cpt:=(-1)), - (function n -> cpt:=n) - -(* Affichage des variables d'un système *) - -let display_omega_var i = Printf.sprintf "OV%d" i - -(* \subsection{Gestion des environnements de variable pour la réflexion} - Gestion des environnements de traduction entre termes des constructions - non réifiés et variables des termes reifies. Attention il s'agit de - l'environnement initial contenant tout. Il faudra le réduire après - calcul des variables utiles. *) - -let add_reified_atom sigma t env = - try List.index0 (EConstr.eq_constr sigma) t env.terms - with Not_found -> - let i = List.length env.terms in - env.terms <- env.terms @ [t]; i - -let get_reified_atom env = - try List.nth env.terms with Invalid_argument _ -> failwith "get_reified_atom" - -(** When the omega resolution has created a variable [v], we re-sync - the environment with this new variable. To be done in the right order. *) - -let set_reified_atom v t env = - assert (Int.equal v (List.length env.terms)); - env.terms <- env.terms @ [t] - -(* \subsection{Gestion de l'environnement de proposition pour Omega} *) -(* ajout d'une proposition *) -let add_prop sigma env t = - try List.index0 (EConstr.eq_constr sigma) t env.props - with Not_found -> - let i = List.length env.props in env.props <- env.props @ [t]; i - -(* accès a une proposition *) -let get_prop v env = - try List.nth v env with Invalid_argument _ -> failwith "get_prop" - -(* \subsection{Gestion du nommage des équations} *) -(* Ajout d'une equation dans l'environnement de reification *) -let add_equation env e = - let id = e.e_omega.id in - if IntHtbl.mem env.equations id then () else IntHtbl.add env.equations id e - -(* accès a une equation *) -let get_equation env id = - try IntHtbl.find env.equations id - with Not_found as e -> - Printf.printf "Omega Equation %d non trouvée\n" id; raise e - -(* Affichage des termes réifiés *) -let rec oprint ch = function - | Oint n -> Printf.fprintf ch "%s" (Bigint.to_string n) - | Oplus (t1,t2) -> Printf.fprintf ch "(%a + %a)" oprint t1 oprint t2 - | Omult (t1,t2) -> Printf.fprintf ch "(%a * %a)" oprint t1 oprint t2 - | Ominus(t1,t2) -> Printf.fprintf ch "(%a - %a)" oprint t1 oprint t2 - | Oopp t1 ->Printf.fprintf ch "~ %a" oprint t1 - | Oatom n -> Printf.fprintf ch "V%02d" n - -let print_comp = function - | Eq -> "=" | Leq -> "<=" | Geq -> ">=" - | Gt -> ">" | Lt -> "<" | Neq -> "!=" - -let rec pprint ch = function - Pequa (_,{ e_comp=comp; e_left=t1; e_right=t2 }) -> - Printf.fprintf ch "%a %s %a" oprint t1 (print_comp comp) oprint t2 - | Ptrue -> Printf.fprintf ch "TT" - | Pfalse -> Printf.fprintf ch "FF" - | Pnot t -> Printf.fprintf ch "not(%a)" pprint t - | Por (_,t1,t2) -> Printf.fprintf ch "(%a or %a)" pprint t1 pprint t2 - | Pand(_,t1,t2) -> Printf.fprintf ch "(%a and %a)" pprint t1 pprint t2 - | Pimp(_,t1,t2) -> Printf.fprintf ch "(%a => %a)" pprint t1 pprint t2 - | Pprop c -> Printf.fprintf ch "Prop" - -(* \subsection{Omega vers Oformula} *) - -let oformula_of_omega af = - let rec loop = function - | ({v=v; c=n}::r) -> Oplus(Omult(Oatom v,Oint n),loop r) - | [] -> Oint af.constant - in - loop af.body - -let app f v = EConstr.mkApp(Lazy.force f,v) - -(* \subsection{Oformula vers COQ reel} *) - -let coq_of_formula env t = - let rec loop = function - | Oplus (t1,t2) -> app Z.plus [| loop t1; loop t2 |] - | Oopp t -> app Z.opp [| loop t |] - | Omult(t1,t2) -> app Z.mult [| loop t1; loop t2 |] - | Oint v -> Z.mk v - | Oatom var -> - (* attention ne traite pas les nouvelles variables si on ne les - * met pas dans env.term *) - get_reified_atom env var - | Ominus(t1,t2) -> app Z.minus [| loop t1; loop t2 |] in - loop t - -(* \subsection{Oformula vers COQ reifié} *) - -let reified_of_atom env i = - try IntHtbl.find env.real_indices i - with Not_found -> - Printf.printf "Atome %d non trouvé\n" i; - IntHtbl.iter (fun k v -> Printf.printf "%d -> %d\n" k v) env.real_indices; - raise Not_found - -let reified_binop = function - | Oplus _ -> app coq_t_plus - | Ominus _ -> app coq_t_minus - | Omult _ -> app coq_t_mult - | _ -> assert false - -let rec reified_of_formula env t = match t with - | Oplus (t1,t2) | Omult (t1,t2) | Ominus (t1,t2) -> - reified_binop t [| reified_of_formula env t1; reified_of_formula env t2 |] - | Oopp t -> app coq_t_opp [| reified_of_formula env t |] - | Oint v -> app coq_t_int [| Z.mk v |] - | Oatom i -> app coq_t_var [| mk_N (reified_of_atom env i) |] - -let reified_of_formula env f = - try reified_of_formula env f - with reraise -> oprint stderr f; raise reraise - -let reified_cmp = function - | Eq -> app coq_p_eq - | Leq -> app coq_p_leq - | Geq -> app coq_p_geq - | Gt -> app coq_p_gt - | Lt -> app coq_p_lt - | Neq -> app coq_p_neq - -let reified_conn = function - | Por _ -> app coq_p_or - | Pand _ -> app coq_p_and - | Pimp _ -> app coq_p_imp - | _ -> assert false - -let rec reified_of_oprop sigma env t = match t with - | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) -> - reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |] - | Ptrue -> Lazy.force coq_p_true - | Pfalse -> Lazy.force coq_p_false - | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |] - | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) -> - reified_conn t - [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |] - | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |] - -let reified_of_proposition sigma env f = - try reified_of_oprop sigma env f - with reraise -> pprint stderr f; raise reraise - -let reified_of_eq env (l,r) = - app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |] - -(* \section{Opérations sur les équations} -Ces fonctions préparent les traces utilisées par la tactique réfléchie -pour faire des opérations de normalisation sur les équations. *) - -(* \subsection{Extractions des variables d'une équation} *) -(* Extraction des variables d'une équation. *) -(* Chaque fonction retourne une liste triée sans redondance *) - -let (@@) = IntSet.union - -let rec vars_of_formula = function - | Oint _ -> IntSet.empty - | Oplus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Omult (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Ominus (e1,e2) -> (vars_of_formula e1) @@ (vars_of_formula e2) - | Oopp e -> vars_of_formula e - | Oatom i -> IntSet.singleton i - -let rec vars_of_equations = function - | [] -> IntSet.empty - | e::l -> - (vars_of_formula e.e_left) @@ - (vars_of_formula e.e_right) @@ - (vars_of_equations l) - -let rec vars_of_prop = function - | Pequa(_,e) -> vars_of_equations [e] - | Pnot p -> vars_of_prop p - | Por(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pand(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pimp(_,p1,p2) -> (vars_of_prop p1) @@ (vars_of_prop p2) - | Pprop _ | Ptrue | Pfalse -> IntSet.empty - -(* Normalized formulas : - - - sorted list of monomials, largest index first, - with non-null coefficients - - a constant coefficient - - /!\ Keep in sync with the corresponding functions in ReflOmegaCore ! -*) - -type nformula = - { coefs : (atom_index * Bigint.bigint) list; - cst : Bigint.bigint } - -let scale n { coefs; cst } = - { coefs = List.map (fun (v,k) -> (v,k*n)) coefs; - cst = cst*n } - -let shuffle nf1 nf2 = - let rec merge l1 l2 = match l1,l2 with - | [],_ -> l2 - | _,[] -> l1 - | (v1,k1)::r1,(v2,k2)::r2 -> - if Int.equal v1 v2 then - let k = k1+k2 in - if Bigint.equal k Bigint.zero then merge r1 r2 - else (v1,k) :: merge r1 r2 - else if v1 > v2 then (v1,k1) :: merge r1 l2 - else (v2,k2) :: merge l1 r2 - in - { coefs = merge nf1.coefs nf2.coefs; - cst = nf1.cst + nf2.cst } - -let rec normalize = function - | Oplus(t1,t2) -> shuffle (normalize t1) (normalize t2) - | Ominus(t1,t2) -> normalize (Oplus (t1, Oopp(t2))) - | Oopp(t) -> scale negone (normalize t) - | Omult(t,Oint n) | Omult (Oint n, t) -> - if Bigint.equal n Bigint.zero then { coefs = []; cst = zero } - else scale n (normalize t) - | Omult _ -> assert false (* invariant on Omult *) - | Oint n -> { coefs = []; cst = n } - | Oatom v -> { coefs = [v,Bigint.one]; cst=Bigint.zero} - -(* From normalized formulas to omega representations *) - -let omega_of_nformula env kind nf = - { id = new_omega_eq (); - kind; - constant=nf.cst; - body = List.map (fun (v,c) -> { v; c }) nf.coefs } - - -let negate_oper = function - Eq -> Neq | Neq -> Eq | Leq -> Gt | Geq -> Lt | Lt -> Geq | Gt -> Leq - -let normalize_equation env (negated,depends,origin,path) oper t1 t2 = - let mk_step t kind = - let equa = omega_of_nformula env kind (normalize t) in - { e_comp = oper; e_left = t1; e_right = t2; - e_negated = negated; e_depends = depends; - e_origin = { o_hyp = origin; o_path = List.rev path }; - e_omega = equa } - in - try match (if negated then (negate_oper oper) else oper) with - | Eq -> mk_step (Oplus (t1,Oopp t2)) EQUA - | Neq -> mk_step (Oplus (t1,Oopp t2)) DISE - | Leq -> mk_step (Oplus (t2,Oopp t1)) INEQ - | Geq -> mk_step (Oplus (t1,Oopp t2)) INEQ - | Lt -> mk_step (Oplus (Oplus(t2,Oint negone),Oopp t1)) INEQ - | Gt -> mk_step (Oplus (Oplus(t1,Oint negone),Oopp t2)) INEQ - with e when Logic.catchable_exception e -> raise e - -(* \section{Compilation des hypothèses} *) - -let mkPor i x y = Por (i,x,y) -let mkPand i x y = Pand (i,x,y) -let mkPimp i x y = Pimp (i,x,y) - -let rec oformula_of_constr sigma env t = - match Z.parse_term sigma t with - | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2 - | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2 - | Tmult (t1,t2) -> - (match Z.get_scalar sigma t1 with - | Some n -> Omult (Oint n,oformula_of_constr sigma env t2) - | None -> - match Z.get_scalar sigma t2 with - | Some n -> Omult (oformula_of_constr sigma env t1, Oint n) - | None -> Oatom (add_reified_atom sigma t env)) - | Topp t -> Oopp(oformula_of_constr sigma env t) - | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one) - | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom sigma t env) - -and binop sigma env c t1 t2 = - let t1' = oformula_of_constr sigma env t1 in - let t2' = oformula_of_constr sigma env t2 in - c t1' t2' - -and binprop sigma env (neg2,depends,origin,path) - add_to_depends neg1 gl c t1 t2 = - let i = new_connector_id env in - let depends1 = if add_to_depends then Left i::depends else depends in - let depends2 = if add_to_depends then Right i::depends else depends in - if add_to_depends then - IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; - let t1' = - oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in - let t2' = - oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in - (* On numérote le connecteur dans l'environnement. *) - c i t1' t2' - -and mk_equation sigma env ctxt c connector t1 t2 = - let t1' = oformula_of_constr sigma env t1 in - let t2' = oformula_of_constr sigma env t2 in - (* On ajoute l'equation dans l'environnement. *) - let omega = normalize_equation env ctxt connector t1' t2' in - add_equation env omega; - Pequa (c,omega) - -and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c = - match Z.parse_rel gl c with - | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2 - | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2 - | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2 - | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2 - | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2 - | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2 - | Rtrue -> Ptrue - | Rfalse -> Pfalse - | Rnot t -> - let ctxt' = (not negated, depends, origin,(O_mono::path)) in - Pnot (oproposition_of_constr sigma env ctxt' gl t) - | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2 - | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2 - | Rimp (t1,t2) -> - binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2 - | Riff (t1,t2) -> - (* No lifting here, since Omega only works on closed propositions. *) - binprop sigma env ctxt negated negated gl mkPand - (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1) - | _ -> Pprop c - -(* Destructuration des hypothèses et de la conclusion *) - -let display_gl env t_concl t_lhyps = - Printf.printf "REIFED PROBLEM\n\n"; - Printf.printf " CONCL: %a\n" pprint t_concl; - List.iter - (fun (i,_,t) -> Printf.printf " %s: %a\n" (Id.to_string i) pprint t) - t_lhyps; - print_env_reification env - -type defined = Defined | Assumed - -let reify_hyp sigma env gl i = - let open Context.Named.Declaration in - let ctxt = (false,[],i,[]) in - match Tacmach.New.pf_get_hyp i gl with - | LocalDef (_,d,t) when Z.is_int_typ gl t -> - let dummy = Lazy.force coq_True in - let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in - i,Defined,p - | LocalDef (_,_,t) | LocalAssum (_,t) -> - let p = oproposition_of_constr sigma env ctxt gl t in - i,Assumed,p - -let reify_gl env gl = - let sigma = Proofview.Goal.sigma gl in - let concl = Tacmach.New.pf_concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in - let ctxt_concl = (true,[],id_concl,[O_mono]) in - let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in - let t_lhyps = List.map (reify_hyp sigma env gl) hyps in - let () = if !debug then display_gl env t_concl t_lhyps in - t_concl, t_lhyps - -let rec destruct_pos_hyp eqns = function - | Pequa (_,e) -> [e :: eqns] - | Ptrue | Pfalse | Pprop _ -> [eqns] - | Pnot t -> destruct_neg_hyp eqns t - | Por (_,t1,t2) -> - let s1 = destruct_pos_hyp eqns t1 in - let s2 = destruct_pos_hyp eqns t2 in - s1 @ s2 - | Pand(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_pos_hyp le1 t2) - (destruct_pos_hyp eqns t1) - | Pimp(_,t1,t2) -> - let s1 = destruct_neg_hyp eqns t1 in - let s2 = destruct_pos_hyp eqns t2 in - s1 @ s2 - -and destruct_neg_hyp eqns = function - | Pequa (_,e) -> [e :: eqns] - | Ptrue | Pfalse | Pprop _ -> [eqns] - | Pnot t -> destruct_pos_hyp eqns t - | Pand (_,t1,t2) -> - let s1 = destruct_neg_hyp eqns t1 in - let s2 = destruct_neg_hyp eqns t2 in - s1 @ s2 - | Por(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_neg_hyp le1 t2) - (destruct_neg_hyp eqns t1) - | Pimp(_,t1,t2) -> - List.map_append - (fun le1 -> destruct_neg_hyp le1 t2) - (destruct_pos_hyp eqns t1) - -let rec destructurate_hyps = function - | [] -> [[]] - | (i,_,t) :: l -> - let l_syst1 = destruct_pos_hyp [] t in - let l_syst2 = destructurate_hyps l in - List.cartesian (@) l_syst1 l_syst2 - -(* \subsection{Affichage d'un système d'équation} *) - -(* Affichage des dépendances de système *) -let display_depend = function - Left i -> Printf.printf " L%d" i - | Right i -> Printf.printf " R%d" i - -let display_systems syst_list = - let display_omega om_e = - Printf.printf " E%d : %a %s 0\n" - om_e.id - (fun _ -> display_eq display_omega_var) - (om_e.body, om_e.constant) - (operator_of_eq om_e.kind) in - - let display_equation oformula_eq = - pprint stdout (Pequa (Lazy.force coq_I,oformula_eq)); print_newline (); - display_omega oformula_eq.e_omega; - Printf.printf " Depends on:"; - List.iter display_depend oformula_eq.e_depends; - Printf.printf "\n Path: %s" - (String.concat "" - (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M") - oformula_eq.e_origin.o_path)); - Printf.printf "\n Origin: %s (negated : %s)\n\n" - (Id.to_string oformula_eq.e_origin.o_hyp) - (if oformula_eq.e_negated then "yes" else "no") in - - let display_system syst = - Printf.printf "=SYSTEM===================================\n"; - List.iter display_equation syst in - List.iter display_system syst_list - -(* Extraction des prédicats utilisées dans une trace. Permet ensuite le - calcul des hypothèses *) - -let rec hyps_used_in_trace = function - | [] -> IntSet.empty - | act :: l -> - match act with - | HYP e -> IntSet.add e.id (hyps_used_in_trace l) - | SPLIT_INEQ (_,(_,act1),(_,act2)) -> - hyps_used_in_trace act1 @@ hyps_used_in_trace act2 - | _ -> hyps_used_in_trace l - -(** Retreive variables declared as extra equations during resolution - and declare them into the environment. - We should consider these variables in their introduction order, - otherwise really bad things will happen. *) - -let state_cmp x y = Int.compare x.st_var y.st_var - -module StateSet = - Set.Make (struct type t = state_action let compare = state_cmp end) - -let rec stated_in_trace = function - | [] -> StateSet.empty - | [SPLIT_INEQ (_,(_,t1),(_,t2))] -> - StateSet.union (stated_in_trace t1) (stated_in_trace t2) - | STATE action :: l -> StateSet.add action (stated_in_trace l) - | _ :: l -> stated_in_trace l - -let rec stated_in_tree = function - | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) - | Leaf s -> stated_in_trace s.s_trace - -let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|] - -let digest_stated_equations env tree = - let do_equation st (vars,gens,eqns,ids) = - (** We turn the definition of [v] - - into a reified formula : *) - let v_def = oformula_of_omega st.st_def in - (** - into a concrete Coq formula - (this uses only older vars already in env) : *) - let coq_v = coq_of_formula env v_def in - (** We then update the environment *) - set_reified_atom st.st_var coq_v env; - (** The term we'll introduce *) - let term_to_generalize = mk_refl coq_v in - (** Its representation as equation (but not reified yet, - we lack the proper env to do that). *) - let term_to_reify = (v_def,Oatom st.st_var) in - (st.st_var::vars, - term_to_generalize::gens, - term_to_reify::eqns, - CCEqua st.st_def.id :: ids) - in - let (vars,gens,eqns,ids) = - StateSet.fold do_equation (stated_in_tree tree) ([],[],[],[]) - in - (List.rev vars, List.rev gens, List.rev eqns, List.rev ids) - -(* Calcule la liste des éclatements à réaliser sur les hypothèses - nécessaires pour extraire une liste d'équations donnée *) - -(* PL: experimentally, the result order of the following function seems - _very_ crucial for efficiency. No idea why. Do not remove the List.rev - or modify the current semantics of Util.List.union (some elements of first - arg, then second arg), unless you know what you're doing. *) - -let rec get_eclatement env = function - | [] -> [] - | i :: r -> - let l = try (get_equation env i).e_depends with Not_found -> [] in - List.union dir_eq (List.rev l) (get_eclatement env r) - -let select_smaller l = - let comp (_,x) (_,y) = Int.compare (List.length x) (List.length y) in - try List.hd (List.sort comp l) with Failure _ -> failwith "select_smaller" - -let filter_compatible_systems required systems = - let rec select = function - | [] -> [] - | (x::l) -> - if List.mem_f dir_eq x required then select l - else if List.mem_f dir_eq (barre x) required then raise Exit - else x :: select l - in - List.map_filter - (function (sol, splits) -> - try Some (sol, select splits) with Exit -> None) - systems - -let rec equas_of_solution_tree = function - | Tree(_,t1,t2) -> - (equas_of_solution_tree t1)@@(equas_of_solution_tree t2) - | Leaf s -> s.s_equa_deps - -(** [maximize_prop] pushes useless props in a new Pprop atom. - The reified formulas get shorter, but be careful with decidabilities. - For instance, anything that contains a Pprop is considered to be - undecidable in [ReflOmegaCore], whereas a Pfalse for instance at - the same spot will lead to a decidable formula. - In particular, do not use this function on the conclusion. - Even in hypotheses, we could probably build pathological examples - that romega won't handle correctly, but they should be pretty rare. -*) - -let maximize_prop equas c = - let rec loop c = match c with - | Pequa(t,e) -> if IntSet.mem e.e_omega.id equas then c else Pprop t - | Pnot t -> - (match loop t with - | Pprop p -> Pprop (app coq_not [|p|]) - | t' -> Pnot t') - | Por(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (app coq_or [|p1;p2|]) - | t1', t2' -> Por(i,t1',t2')) - | Pand(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (app coq_and [|p1;p2|]) - | t1', t2' -> Pand(i,t1',t2')) - | Pimp(i,t1,t2) -> - (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *) - | t1', t2' -> Pimp(i,t1',t2')) - | Ptrue -> Pprop (app coq_True [||]) - | Pfalse -> Pprop (app coq_False [||]) - | Pprop _ -> c - in loop c - -let rec display_solution_tree ch = function - Leaf t -> - output_string ch - (Printf.sprintf "%d[%s]" - t.s_index - (String.concat " " (List.map string_of_int - (IntSet.elements t.s_equa_deps)))) - | Tree(i,t1,t2) -> - Printf.fprintf ch "S%d(%a,%a)" i - display_solution_tree t1 display_solution_tree t2 - -let rec solve_with_constraints all_solutions path = - let rec build_tree sol buf = function - [] -> Leaf sol - | (Left i :: remainder) -> - Tree(i, - build_tree sol (Left i :: buf) remainder, - solve_with_constraints all_solutions (List.rev(Right i :: buf))) - | (Right i :: remainder) -> - Tree(i, - solve_with_constraints all_solutions (List.rev (Left i :: buf)), - build_tree sol (Right i :: buf) remainder) in - let weighted = filter_compatible_systems path all_solutions in - let (winner_sol,winner_deps) = - try select_smaller weighted - with reraise -> - Printf.printf "%d - %d\n" - (List.length weighted) (List.length all_solutions); - List.iter display_depend path; raise reraise - in - build_tree winner_sol (List.rev path) winner_deps - -let find_path {o_hyp=id;o_path=p} env = - let rec loop_path = function - ([],l) -> Some l - | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2) - | _ -> None in - let rec loop_id i = function - CCHyp{o_hyp=id';o_path=p'} :: l when Id.equal id id' -> - begin match loop_path (p',p) with - Some r -> i,r - | None -> loop_id (succ i) l - end - | _ :: l -> loop_id (succ i) l - | [] -> failwith "find_path" in - loop_id 0 env - -let mk_direction_list l = - let trans = function - | O_left -> Some (Lazy.force coq_d_left) - | O_right -> Some (Lazy.force coq_d_right) - | O_mono -> None (* No more [D_mono] constructor now *) - in - mk_list (Lazy.force coq_direction) (List.map_filter trans l) - - -(* \section{Rejouer l'historique} *) - -let hyp_idx env_hyp i = - let rec loop count = function - | [] -> failwith (Printf.sprintf "get_hyp %d" i) - | CCEqua i' :: _ when Int.equal i i' -> mk_nat count - | _ :: l -> loop (succ count) l - in loop 0 env_hyp - - -(* We now expand NEGATE_CONTRADICT and CONTRADICTION into - a O_SUM followed by a O_BAD_CONSTANT *) - -let sum_bad inv i1 i2 = - let open EConstr in - mkApp (Lazy.force coq_s_sum, - [| Z.mk Bigint.one; i1; - Z.mk (if inv then negone else Bigint.one); i2; - mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|]) - -let rec reify_trace env env_hyp = - let open EConstr in - function - | CONSTANT_NOT_NUL(e,_) :: [] - | CONSTANT_NEG(e,_) :: [] - | CONSTANT_NUL e :: [] -> - mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |]) - | NEGATE_CONTRADICT(e1,e2,direct) :: [] -> - sum_bad direct (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id) - | CONTRADICTION (e1,e2) :: [] -> - sum_bad false (hyp_idx env_hyp e1.id) (hyp_idx env_hyp e2.id) - | NOT_EXACT_DIVIDE (e1,k) :: [] -> - mkApp (Lazy.force coq_s_not_exact_divide, - [| hyp_idx env_hyp e1.id; Z.mk k |]) - | DIVIDE_AND_APPROX (e1,_,k,_) :: l - | EXACT_DIVIDE (e1,k) :: l -> - mkApp (Lazy.force coq_s_divide, - [| hyp_idx env_hyp e1.id; Z.mk k; - reify_trace env env_hyp l |]) - | MERGE_EQ(e3,e1,e2) :: l -> - mkApp (Lazy.force coq_s_merge_eq, - [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2; - reify_trace env (CCEqua e3:: env_hyp) l |]) - | SUM(e3,(k1,e1),(k2,e2)) :: l -> - mkApp (Lazy.force coq_s_sum, - [| Z.mk k1; hyp_idx env_hyp e1.id; - Z.mk k2; hyp_idx env_hyp e2.id; - reify_trace env (CCEqua e3 :: env_hyp) l |]) - | STATE {st_new_eq; st_def; st_orig; st_coef } :: l -> - (* we now produce a [O_SUM] here *) - mkApp (Lazy.force coq_s_sum, - [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id; - Z.mk st_coef; hyp_idx env_hyp st_def.id; - reify_trace env (CCEqua st_new_eq.id :: env_hyp) l |]) - | HYP _ :: l -> reify_trace env env_hyp l - | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ -> - let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in - let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in - mkApp (Lazy.force coq_s_split_ineq, - [| hyp_idx env_hyp e.id; r1 ; r2 |]) - | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l - | WEAKEN _ :: l -> failwith "not_treated" - | _ -> failwith "bad history" - -let rec decompose_tree env ctxt = function - Tree(i,left,right) -> - let org = - try IntHtbl.find env.constructors i - with Not_found -> - failwith (Printf.sprintf "Cannot find constructor %d" i) in - let (index,path) = find_path org ctxt in - let left_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_left]} in - let right_hyp = CCHyp{o_hyp=org.o_hyp;o_path=org.o_path @ [O_right]} in - app coq_e_split - [| mk_nat index; - mk_direction_list path; - decompose_tree env (left_hyp::ctxt) left; - decompose_tree env (right_hyp::ctxt) right |] - | Leaf s -> - decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps) -and decompose_tree_hyps trace env ctxt = function - [] -> app coq_e_solve [| reify_trace env ctxt trace |] - | (i::l) -> - let equation = - try IntHtbl.find env.equations i - with Not_found -> - failwith (Printf.sprintf "Cannot find equation %d" i) in - let (index,path) = find_path equation.e_origin ctxt in - let cont = - decompose_tree_hyps trace env - (CCEqua equation.e_omega.id :: ctxt) l in - app coq_e_extract [|mk_nat index; mk_direction_list path; cont |] - -let solve_system env index list_eq = - let system = List.map (fun eq -> eq.e_omega) list_eq in - let trace = - OmegaSolver.simplify_strong - (new_omega_eq,new_omega_var,display_omega_var) - system - in - (* Hypotheses used for this solution *) - let vars = hyps_used_in_trace trace in - let splits = get_eclatement env (IntSet.elements vars) in - if !debug then - begin - Printf.printf "SYSTEME %d\n" index; - display_action display_omega_var trace; - print_string "\n Depend :"; - IntSet.iter (fun i -> Printf.printf " %d" i) vars; - print_string "\n Split points :"; - List.iter display_depend splits; - Printf.printf "\n------------------------------------\n" - end; - {s_index = index; s_trace = trace; s_equa_deps = vars}, splits - -(* \section{La fonction principale} *) - (* Cette fonction construit la -trace pour la procédure de décision réflexive. A partir des résultats -de l'extraction des systèmes, elle lance la résolution par Omega, puis -l'extraction d'un ensemble minimal de solutions permettant la -résolution globale du système et enfin construit la trace qui permet -de faire rejouer cette solution par la tactique réflexive. *) - -let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = - if !debug then Printf.printf "\n====================================\n"; - let all_solutions = List.mapi (solve_system env) systems_list in - let solution_tree = solve_with_constraints all_solutions [] in - if !debug then begin - display_solution_tree stdout solution_tree; - print_newline() - end; - (** Collect all hypotheses and variables used in the solution tree *) - let useful_equa_ids = equas_of_solution_tree solution_tree in - let useful_hypnames, useful_vars = - IntSet.fold - (fun i (hyps,vars) -> - let e = get_equation env i in - Id.Set.add e.e_origin.o_hyp hyps, - vars_of_equations [e] @@ vars) - useful_equa_ids - (Id.Set.empty, vars_of_prop reified_concl) - in - let useful_hypnames = - Id.Set.elements (Id.Set.remove id_concl useful_hypnames) - in - - (** Parts coming from equations introduced by omega: *) - let stated_vars, l_generalize_arg, to_reify_stated, hyp_stated_vars = - digest_stated_equations env solution_tree - in - (** The final variables are either coming from: - - useful hypotheses (and conclusion) - - equations introduced during resolution *) - let all_vars_env = (IntSet.elements useful_vars) @ stated_vars - in - (** We prepare the renumbering from all variables to useful ones. - Since [all_var_env] is sorted, this renumbering will preserve - order: this way, the equations in ReflOmegaCore will have - the same normal forms as here. *) - let reduced_term_env = - let rec loop i = function - | [] -> [] - | var :: l -> - let t = get_reified_atom env var in - IntHtbl.add env.real_indices var i; t :: loop (succ i) l - in - mk_list (Lazy.force Z.typ) (loop 0 all_vars_env) - in - (** The environment [env] (and especially [env.real_indices]) is now - ready for the coming reifications: *) - let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in - let reified_concl = reified_of_proposition sigma env reified_concl in - let l_reified_terms = - List.map - (fun id -> - match Id.Map.find id reified_hyps with - | Defined,p -> - reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id) - | Assumed,p -> - reified_of_proposition sigma env (maximize_prop useful_equa_ids p), - EConstr.mkVar id - | exception Not_found -> assert false) - useful_hypnames - in - let l_reified_terms, l_reified_hypnames = List.split l_reified_terms in - let env_props_reified = mk_plist env.props in - let reified_goal = - mk_list (Lazy.force coq_proposition) - (l_reified_stated @ l_reified_terms) in - let reified = - app coq_interp_sequent - [| reified_concl;env_props_reified;reduced_term_env;reified_goal|] - in - let mk_occ id = {o_hyp=id;o_path=[]} in - let initial_context = - List.map (fun id -> CCHyp (mk_occ id)) useful_hypnames in - let context = - CCHyp (mk_occ id_concl) :: hyp_stated_vars @ initial_context in - let decompose_tactic = decompose_tree env context solution_tree in - - Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check reified DEFAULTcast >> - Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> - show_goal >> - (if unsafe then - (* Trust the produced term. Faster, but might fail later at Qed. - Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check (Lazy.force coq_True) VMcast - else - Tactics.normalise_vm_in_concl) >> - Tactics.apply (Lazy.force coq_I) - -let total_reflexive_omega_tactic unsafe = - Proofview.Goal.enter begin fun gl -> - Coqlib.check_required_library ["Coq";"romega";"ROmega"]; - rst_omega_eq (); - rst_omega_var (); - try - let env = new_environment () in - let (concl,hyps) = reify_gl env gl in - (* Register all atom indexes created during reification as omega vars *) - set_omega_maxvar (pred (List.length env.terms)); - let full_reified_goal = (id_concl,Assumed,Pnot concl) :: hyps in - let systems_list = destructurate_hyps full_reified_goal in - let hyps = - List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps - in - if !debug then display_systems systems_list; - let sigma = Proofview.Goal.sigma gl in - resolution unsafe sigma env (concl,hyps) systems_list - with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") - end - diff --git a/plugins/romega/romega_plugin.mlpack b/plugins/romega/romega_plugin.mlpack deleted file mode 100644 index 38d0e94111..0000000000 --- a/plugins/romega/romega_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Const_omega -Refl_omega -G_romega diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 20ea8b3667..aadb4fe5f6 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1366,7 +1366,7 @@ let ssrpatterntac _ist arg gl = let concl0 = pf_concl gl in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index fc24e9b3a9..265909980b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_cbv:=a); } -let pr_key = function +let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp | VarKey id -> Names.Id.print id | RelKey n -> Pp.(str "REL_" ++ int n) @@ -320,14 +320,14 @@ and norm_head_ref k info env stack normt = if red_set_ref (info_flags info.infos) normt then match ref_value_cache info.infos info.tab normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 12788e5ec5..25510826cc 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -55,16 +55,16 @@ let env env = env.static_env let vars_of_env env = Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env) -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as na -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ - spc () ++ str "is not bound to an identifier." ++ - spc () ++str "It cannot be used in a binder.") - else na +let ltac_interp_id { ltac_idents ; ltac_genargs } id = + try Id.Map.find id ltac_idents + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ + spc () ++ str "is not bound to an identifier." ++ + spc () ++str "It cannot be used in a binder.") + else id + +let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) let push_rel sigma d env = let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in @@ -182,6 +182,8 @@ let interp_ltac_variable ?loc typing_fun env sigma id = end; raise Not_found +let interp_ltac_id env id = ltac_interp_id env.lvar id + module ConstrInterpObj = struct type ('r, 'g, 't) obj = diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 4038523211..70a7ee6e2f 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -76,6 +76,11 @@ val hide_variable : t -> Name.t -> Id.t -> t val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) -> t -> evar_map -> Id.t -> unsafe_judgment +(** Interp an identifier as an ltac variable bound to an identifier, + or as the identifier itself if not bound to an ltac variable *) + +val interp_ltac_id : t -> Id.t -> Id.t + (** Interpreting a generic argument, typically a "ltac:(...)", taking into account the possible renaming *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ec0ff73062..b040e63cd2 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches = not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + str" on inductive type " ++ print_constr_env env sigma (mkInd ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e3aa90fbcf..a4c2cb2352 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -480,6 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref | GEvar (id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) + let id = interp_ltac_id env id in let evk = try Evd.evar_key id !evdref with Not_found -> @@ -499,6 +500,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> + let open Namegen in + let naming = match naming with + | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id) + | IntroAnonymous -> IntroAnonymous + | IntroFresh id -> IntroFresh (interp_ltac_id env id) in let ty = match tycon with | Some ty -> ty diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bd41e61b34..77ad96d2cf 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -334,19 +334,19 @@ let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ - str(description))) + description)) let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp - | _ -> error_not_structure ref "Expected an instance of a record or structure." + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref "Could not find its value in the global environment." in + | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let env = Global.env () in let evd = Evd.from_env env in let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in @@ -354,18 +354,18 @@ let check_and_decompose_canonical_structure ref = let f,args = match kind body with | App (f,args) -> f,args | _ -> - error_not_structure ref "Expected a record or structure constructor applied to arguments." in + error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref "Expected an instance of a record or structure." in + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let s = try lookup_structure indsp with Not_found -> error_not_structure ref - ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in + (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref "Got too few arguments to the record or structure constructor."; + error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f4c8a6cd66..a0d20b7ce4 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -341,6 +341,7 @@ struct | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list + (* Debugging printer *) let rec pr_member pr_c member = let open Pp in let pr_c x = hov 1 (pr_c x) in @@ -351,7 +352,7 @@ struct prvect_with_sep (pr_bar) pr_c br ++ str ")" | Proj (p,cst) -> - str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")" + str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -368,11 +369,11 @@ struct let open Pp in match c with | Cst_const (c, u) -> - if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ + if Univ.Instance.is_empty u then Constant.debug_print c + else str"(" ++ Constant.debug_print c ++ str ", " ++ Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> - str".(" ++ Constant.print (Projection.constant p) ++ str")" + str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" let empty = [] let is_empty = CList.is_empty diff --git a/printing/printer.ml b/printing/printer.ml index 67d71332b0..5ca330d377 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -944,9 +944,16 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> + (* FIXME? *) let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in + let safe_pr_inductive env kn = + try pr_inductive env (kn,0) + with Not_found -> + (* FIXME? *) + MutInd.print kn + in let safe_pr_ltype env sigma typ = try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () @@ -961,7 +968,7 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") | Guarded kn -> hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 837865e644..878e2b1f01 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -655,12 +655,11 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> Constant.to_string kn - | Var id -> Id.to_string id - | _ -> "\b" + | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim + | _ -> mt () in user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in let branchsigns = compute_constructor_signatures ~rec_flag ind in diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 1507fa4bf0..bd9bac37ef 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,8 +19,6 @@ Proof. omega. Qed. -Require Import ZArith ROmega. - Open Scope Z_scope. Definition Z' := Z. @@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. - Undo. - romega. Qed. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 7326f137c2..8a00cd3fe5 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,25 +1,25 @@ The command has indeed failed with message: -The user-defined tactic "Top.foo" was not fully applied: +The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There are missing arguments for variables y and _, an argument was provided for variable x. The command has indeed failed with message: -The user-defined tactic "Top.baz" was not fully applied: +The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.qux" was not fully applied: +The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.mydo" was not fully applied: +The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: @@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.rec" was not fully applied: +The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v new file mode 100644 index 0000000000..422bb95fdf --- /dev/null +++ b/test-suite/ssr/ssrpattern.v @@ -0,0 +1,7 @@ +Require Import ssrmatching. + +Goal forall n, match n with 0 => 0 | _ => 0 end = 0. +Proof. + intro n. + ssrpattern (match _ with 0 => _ | S n' => _ end). +Abort. diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 0df3d5685d..a97afa7ff0 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -1,5 +1,7 @@ - -Require Import ZArith ROmega. +(* This file used to test the `romega` tactics. + In Coq 8.9 (end of 2018), these tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) +Require Import ZArith Lia. (* Submitted by Xavier Urbain 18 Jan 2002 *) @@ -7,14 +9,14 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. -romega. +lia. Qed. (* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. - romega. + lia. Qed. (* Proposed by Jean-Christophe Filliâtre *) @@ -22,7 +24,7 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. -romega. +lia. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) @@ -32,7 +34,7 @@ Section A. Variable x y : Z. Hypothesis H : (x > y)%Z. Lemma lem4 : (x > y)%Z. - romega. + lia. Qed. End A. @@ -48,7 +50,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1. Hypothesis M : (H <= 2 * S)%Z. Hypothesis N : (S < H)%Z. Lemma lem5 : (H > 0)%Z. - romega. + lia. Qed. End B. @@ -56,11 +58,10 @@ End B. Lemma lem6 : forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. intros. - romega. + lia. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Import Omega. Section C. Parameter g : forall m : nat, m <> 0 -> Prop. Parameter f : forall (m : nat) (H : m <> 0), g m H. @@ -68,23 +69,21 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - romega with nat. + lia. Qed. End C. (* Problem of dependencies *) -Require Import Omega. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. intros. -romega with nat. +lia. Qed. (* Bug that what caused by the use of intro_using in Omega *) -Require Import Omega. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. intros. -romega with nat. +lia. Qed. (* Check that the interpretation of mult on nat enforces its positivity *) @@ -92,5 +91,5 @@ Qed. (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) Lemma lem10 : forall n m : nat, le n (plus n (mult n m)). Proof. -intros; romega with nat. +intros; lia. Qed. diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 3ddf6a40fb..7f69422ab3 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -1,25 +1,27 @@ -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) -Lemma test_romega_0 : +Lemma test_lia_0 : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_0b : +Lemma test_lia_0b : forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. -romega. +lia. Qed. -Lemma test_romega_1 : +Lemma test_lia_1 : forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> @@ -29,10 +31,10 @@ Lemma test_romega_1 : z >= 0. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_1b : +Lemma test_lia_1b : forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> @@ -42,24 +44,24 @@ Lemma test_romega_1b : z >= 0. Proof. intros z z1 z2. -romega. +lia. Qed. -Lemma test_romega_2 : forall a b c:Z, +Lemma test_lia_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_2b : forall a b c:Z, +Lemma test_lia_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. -romega. +lia. Qed. -Lemma test_romega_3 : forall a b h hl hr ha hb, +Lemma test_lia_3 : forall a b h hl hr ha hb, 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> @@ -70,10 +72,10 @@ Lemma test_romega_3 : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_3b : forall a b h hl hr ha hb, +Lemma test_lia_3b : forall a b h hl hr ha hb, 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> @@ -84,79 +86,79 @@ Lemma test_romega_3b : forall a b h hl hr ha hb, 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. -romega. +lia. Qed. -Lemma test_romega_4 : forall hr ha, +Lemma test_lia_4 : forall hr ha, ha = 0 -> (ha = 0 -> hr =0) -> hr = 0. Proof. intros hr ha. -romega. +lia. Qed. -Lemma test_romega_5 : forall hr ha, +Lemma test_lia_5 : forall hr ha, ha = 0 -> (~ha = 0 \/ hr =0) -> hr = 0. Proof. intros hr ha. -romega. +lia. Qed. -Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False. +Lemma test_lia_6 : forall z, z>=0 -> 0>z+2 -> False. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False. +Lemma test_lia_6b : forall z, z>=0 -> 0>z+2 -> False. Proof. intros z. -romega. +lia. Qed. -Lemma test_romega_7 : forall z, +Lemma test_lia_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_7b : forall z, +Lemma test_lia_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. -romega. +lia. Qed. (* Magaud BZ#240 *) -Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Lemma test_lia_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. intros. -romega. +lia. Qed. -Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. +Lemma test_lia_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x. Proof. intros x y. -romega. +lia. Qed. (* Besson BZ#1298 *) -Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False. +Lemma test_lia9 : forall z z':Z, z<>z' -> z'=z -> False. Proof. intros. -romega. +lia. Qed. (* Letouzey, May 2017 *) -Lemma test_romega10 : forall x a a' b b', +Lemma test_lia10 : forall x a a' b b', a' <= b -> a <= b' -> b < b' -> @@ -164,5 +166,5 @@ Lemma test_romega10 : forall x a a' b b', a <= x < b' <-> a <= x < b \/ a' <= x < b'. Proof. intros. - romega. + lia. Qed. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 43eda67ea3..e3b090699d 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -1,4 +1,6 @@ -Require Import ZArith ROmega. +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) +Require Import ZArith Lia. (* Submitted by Yegor Bryukhov (BZ#922) *) @@ -13,7 +15,7 @@ forall v1 v2 v5 : Z, 0 < v2 -> 4*v2 <> 5*v1. intros. -romega. +lia. Qed. @@ -37,5 +39,5 @@ forall v1 v2 v3 v4 v5 : Z, ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) -> False. intros. -romega. +lia. Qed. diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v index fd4ff260b5..ef9cb17b4b 100644 --- a/test-suite/success/ROmega3.v +++ b/test-suite/success/ROmega3.v @@ -1,10 +1,14 @@ -Require Import ZArith ROmega. +Require Import ZArith Lia. Local Open Scope Z_scope. (** Benchmark provided by Chantal Keller, that romega used to solve far too slowly (compared to omega or lia). *) +(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) + + Parameter v4 : Z. Parameter v3 : Z. Parameter o4 : Z. @@ -27,5 +31,5 @@ Lemma lemma_5833 : (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 + (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024. Proof. -Timeout 1 romega. (* should take a few milliseconds, not seconds *) +Timeout 1 lia. (* should take a few milliseconds, not seconds *) Timeout 1 Qed. (* ditto *) diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index fa659273e1..6ca32f450f 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -1,127 +1,123 @@ -Require Import ZArith Nnat ROmega. +Require Import ZArith Nnat Lia. Open Scope Z_scope. (** Test of the zify preprocessor for (R)Omega *) +(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated. + The tests in this file remain but now call the `lia` tactic. *) (* More details in file PreOmega.v - - (r)omega with Z : starts with zify_op - (r)omega with nat : starts with zify_nat - (r)omega with positive : starts with zify_positive - (r)omega with N : starts with uses zify_N - (r)omega with * : starts zify (a saturation of the others) *) (* zify_op *) Goal forall a:Z, Z.max a a = a. intros. -romega with *. +lia. Qed. Goal forall a b:Z, Z.max a b = Z.max b a. intros. -romega with *. +lia. Qed. Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. -romega with *. +lia. Qed. Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. -romega with *. +lia. Qed. Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. -intuition; subst; romega. (* pure multiplication: omega alone can't do it *) +intuition; subst; lia. (* pure multiplication: omega alone can't do it *) Qed. Goal forall a:Z, Z.abs a = a -> a >= 0. intros. -romega with *. +lia. Qed. Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. -romega with *. +lia. Qed. (* zify_nat *) Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. intros. -romega with *. +lia. Qed. Goal forall m:nat, (m<1)%nat -> (m=0)%nat. intros. -romega with *. +lia. Qed. Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. intros. -romega with *. +lia. Qed. (* 2000 instead of 200: works, but quite slow *) Goal forall m: nat, (m*m>=0)%nat. intros. -romega with *. +lia. Qed. (* zify_positive *) Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. intros. -romega with *. +lia. Qed. Goal forall m:positive, (m<2)%positive -> (m=1)%positive. intros. -romega with *. +lia. Qed. Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. intros. -romega with *. +lia. Qed. Goal forall m: positive, (m*m>=1)%positive. intros. -romega with *. +lia. Qed. (* zify_N *) Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m<1)%N -> (m=0)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. intros. -romega with *. +lia. Qed. Goal forall m:N, (m*m>=0)%N. intros. -romega with *. +lia. Qed. (* mix of datatypes *) Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. -romega with *. +lia. Qed. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 4404ff3f16..448febed25 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -377,3 +377,30 @@ f y true. Abort. End LtacNames. + +(* Test binding of the name of existential variables in Ltac *) + +Module EvarNames. + +Ltac pick x := eexists ?[x]. +Goal exists y, y = 0. +pick foo. +[foo]:exact 0. +auto. +Qed. + +Ltac goal x := refine ?[x]. + +Goal forall n, n + 0 = n. +Proof. + induction n; [ goal Base | goal Rec ]. + [Base]: { + easy. + } + [Rec]: { + simpl. + now f_equal. + } +Qed. + +End EvarNames. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index e33aa38173..3bf3925b4b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -543,7 +543,7 @@ let eqI ind l = and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" - (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); + (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) |